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