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
108
109
110
111
112
113
114
115
116
117
118
|
/********************* */
/*! \file expr_miner.cpp
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 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 "options/quantifiers_options.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "theory/quantifiers/term_util.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,
ExprManager& em,
ExprManagerMapCollection& varMap,
Node query,
bool& needExport)
{
// Convert bound variables to skolems. This ensures the satisfiability
// check is ground.
Node squery = convertToSkolem(query);
NodeManager* nm = NodeManager::currentNM();
if (options::sygusExprMinerCheckTimeout.wasSetByUser()
|| options::sygusRewSynthInput())
{
// To support a separate timeout for the subsolver, we need to create
// a separate ExprManager with its own options. This requires that
// the expressions sent to the subsolver can be exported from on
// ExprManager to another. If the export fails, we throw an
// OptionException.
try
{
checker.reset(new SmtEngine(&em));
checker->setTimeLimit(options::sygusExprMinerCheckTimeout(), true);
checker->setLogic(smt::currentSmtEngine()->getLogicInfo());
checker->setOption("sygus-rr-synth-input", false);
Expr equery = squery.toExpr().exportTo(&em, varMap);
checker->assertFormula(equery);
}
catch (const CVC4::ExportUnsupportedException& e)
{
std::stringstream msg;
msg << "Unable to export " << squery
<< " but exporting expressions is "
"required for an expression "
"miner check.";
throw OptionException(msg.str());
}
needExport = true;
}
else
{
needExport = false;
checker.reset(new SmtEngine(nm->toExprManager()));
checker->assertFormula(squery.toExpr());
}
}
} // namespace quantifiers
} // namespace theory
} // namespace CVC4
|
