GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/expr_miner.cpp Lines: 38 41 92.7 %
Date: 2021-03-23 Branches: 47 114 41.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file expr_miner.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, Abdalrhman Mohamed
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Implementation of expr_miner
13
 **/
14
15
#include "theory/quantifiers/expr_miner.h"
16
17
#include "api/cvc4cpp.h"
18
#include "options/quantifiers_options.h"
19
#include "smt/smt_engine.h"
20
#include "smt/smt_engine_scope.h"
21
#include "theory/quantifiers/term_util.h"
22
#include "theory/rewriter.h"
23
#include "theory/smt_engine_subsolver.h"
24
25
using namespace std;
26
using namespace CVC4::kind;
27
28
namespace CVC4 {
29
namespace theory {
30
namespace quantifiers {
31
32
12
void ExprMiner::initialize(const std::vector<Node>& vars, SygusSampler* ss)
33
{
34
12
  d_sampler = ss;
35
12
  d_vars.insert(d_vars.end(), vars.begin(), vars.end());
36
12
}
37
38
224
Node ExprMiner::convertToSkolem(Node n)
39
{
40
448
  std::vector<Node> fvs;
41
224
  TermUtil::computeVarContains(n, fvs);
42
224
  if (fvs.empty())
43
  {
44
1
    return n;
45
  }
46
446
  std::vector<Node> sfvs;
47
446
  std::vector<Node> sks;
48
  // map to skolems
49
223
  NodeManager* nm = NodeManager::currentNM();
50
748
  for (unsigned i = 0, size = fvs.size(); i < size; i++)
51
  {
52
1050
    Node v = fvs[i];
53
    // only look at the sampler variables
54
525
    if (std::find(d_vars.begin(), d_vars.end(), v) != d_vars.end())
55
    {
56
525
      sfvs.push_back(v);
57
525
      std::map<Node, Node>::iterator itf = d_fv_to_skolem.find(v);
58
525
      if (itf == d_fv_to_skolem.end())
59
      {
60
40
        Node sk = nm->mkSkolem("rrck", v.getType());
61
20
        d_fv_to_skolem[v] = sk;
62
20
        sks.push_back(sk);
63
      }
64
      else
65
      {
66
505
        sks.push_back(itf->second);
67
      }
68
    }
69
  }
70
223
  return n.substitute(sfvs.begin(), sfvs.end(), sks.begin(), sks.end());
71
}
72
73
224
void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
74
                                  Node query)
75
{
76
224
  Assert (!query.isNull());
77
224
  initializeSubsolver(checker);
78
  // also set the options
79
224
  checker->setOption("sygus-rr-synth-input", "false");
80
224
  checker->setOption("input-language", "smt2");
81
  // Convert bound variables to skolems. This ensures the satisfiability
82
  // check is ground.
83
448
  Node squery = convertToSkolem(query);
84
224
  checker->assertFormula(squery);
85
224
}
86
87
108
Result ExprMiner::doCheck(Node query)
88
{
89
216
  Node queryr = Rewriter::rewrite(query);
90
108
  if (queryr.isConst())
91
  {
92
    if (!queryr.getConst<bool>())
93
    {
94
      return Result(Result::UNSAT);
95
    }
96
    else
97
    {
98
      return Result(Result::SAT);
99
    }
100
  }
101
216
  std::unique_ptr<SmtEngine> smte;
102
108
  initializeChecker(smte, query);
103
108
  return smte->checkSat();
104
}
105
106
}  // namespace quantifiers
107
}  // namespace theory
108
26685
}  // namespace CVC4