1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Aina Niemetz, Andres Noetzli |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Implementation of candidate_rewrite_database. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/quantifiers/candidate_rewrite_database.h" |
17 |
|
|
18 |
|
#include "options/base_options.h" |
19 |
|
#include "printer/printer.h" |
20 |
|
#include "smt/smt_engine.h" |
21 |
|
#include "smt/smt_engine_scope.h" |
22 |
|
#include "smt/smt_statistics_registry.h" |
23 |
|
#include "theory/datatypes/sygus_datatype_utils.h" |
24 |
|
#include "theory/quantifiers/sygus/term_database_sygus.h" |
25 |
|
#include "theory/quantifiers/term_util.h" |
26 |
|
#include "theory/rewriter.h" |
27 |
|
|
28 |
|
using namespace std; |
29 |
|
using namespace cvc5::kind; |
30 |
|
using namespace cvc5::context; |
31 |
|
|
32 |
|
namespace cvc5 { |
33 |
|
namespace theory { |
34 |
|
namespace quantifiers { |
35 |
|
|
36 |
62 |
CandidateRewriteDatabase::CandidateRewriteDatabase( |
37 |
62 |
Env& env, bool doCheck, bool rewAccel, bool silent, bool filterPairs) |
38 |
|
: ExprMiner(env), |
39 |
|
d_tds(nullptr), |
40 |
|
d_useExtRewriter(false), |
41 |
|
d_doCheck(doCheck), |
42 |
|
d_rewAccel(rewAccel), |
43 |
|
d_silent(silent), |
44 |
|
d_filterPairs(filterPairs), |
45 |
62 |
d_using_sygus(false) |
46 |
|
{ |
47 |
62 |
} |
48 |
53 |
void CandidateRewriteDatabase::initialize(const std::vector<Node>& vars, |
49 |
|
SygusSampler* ss) |
50 |
|
{ |
51 |
53 |
Assert(ss != nullptr); |
52 |
53 |
d_candidate = Node::null(); |
53 |
53 |
d_using_sygus = false; |
54 |
53 |
d_tds = nullptr; |
55 |
53 |
d_useExtRewriter = false; |
56 |
53 |
if (d_filterPairs) |
57 |
|
{ |
58 |
|
d_crewrite_filter.initialize(ss, nullptr, false); |
59 |
|
} |
60 |
53 |
ExprMiner::initialize(vars, ss); |
61 |
53 |
} |
62 |
|
|
63 |
7 |
void CandidateRewriteDatabase::initializeSygus(const std::vector<Node>& vars, |
64 |
|
TermDbSygus* tds, |
65 |
|
Node f, |
66 |
|
SygusSampler* ss) |
67 |
|
{ |
68 |
7 |
Assert(ss != nullptr); |
69 |
7 |
d_candidate = f; |
70 |
7 |
d_using_sygus = true; |
71 |
7 |
d_tds = tds; |
72 |
7 |
d_useExtRewriter = false; |
73 |
7 |
if (d_filterPairs) |
74 |
|
{ |
75 |
7 |
d_crewrite_filter.initialize(ss, d_tds, d_using_sygus); |
76 |
|
} |
77 |
7 |
ExprMiner::initialize(vars, ss); |
78 |
7 |
} |
79 |
|
|
80 |
1776 |
Node CandidateRewriteDatabase::addTerm(Node sol, |
81 |
|
bool rec, |
82 |
|
std::ostream& out, |
83 |
|
bool& rew_print) |
84 |
|
{ |
85 |
|
// have we added this term before? |
86 |
1776 |
std::unordered_map<Node, Node>::iterator itac = d_add_term_cache.find(sol); |
87 |
1776 |
if (itac != d_add_term_cache.end()) |
88 |
|
{ |
89 |
53 |
return itac->second; |
90 |
|
} |
91 |
|
|
92 |
1723 |
if (rec) |
93 |
|
{ |
94 |
|
// if recursive, we first add all subterms |
95 |
|
for (const Node& solc : sol) |
96 |
|
{ |
97 |
|
// whether a candidate rewrite is printed for any subterm is irrelevant |
98 |
|
bool rew_printc = false; |
99 |
|
addTerm(solc, rec, out, rew_printc); |
100 |
|
} |
101 |
|
} |
102 |
|
// register the term |
103 |
1723 |
bool is_unique_term = true; |
104 |
3446 |
Node eq_sol = d_sampler->registerTerm(sol); |
105 |
|
// eq_sol is a candidate solution that is equivalent to sol |
106 |
1723 |
if (eq_sol != sol) |
107 |
|
{ |
108 |
355 |
is_unique_term = false; |
109 |
|
// should we filter the pair? |
110 |
355 |
if (!d_filterPairs || !d_crewrite_filter.filterPair(sol, eq_sol)) |
111 |
|
{ |
112 |
|
// get the actual term |
113 |
490 |
Node solb = sol; |
114 |
490 |
Node eq_solb = eq_sol; |
115 |
245 |
if (d_using_sygus) |
116 |
|
{ |
117 |
119 |
Assert(d_tds != nullptr); |
118 |
119 |
solb = d_tds->sygusToBuiltin(sol); |
119 |
119 |
eq_solb = d_tds->sygusToBuiltin(eq_sol); |
120 |
|
} |
121 |
|
// get the rewritten form |
122 |
490 |
Node solbr; |
123 |
490 |
Node eq_solr; |
124 |
245 |
if (d_useExtRewriter) |
125 |
|
{ |
126 |
119 |
solbr = extendedRewrite(solb); |
127 |
119 |
eq_solr = extendedRewrite(eq_solb); |
128 |
|
} |
129 |
|
else |
130 |
|
{ |
131 |
126 |
solbr = Rewriter::rewrite(solb); |
132 |
126 |
eq_solr = Rewriter::rewrite(eq_solb); |
133 |
|
} |
134 |
245 |
bool verified = false; |
135 |
245 |
Trace("rr-check") << "Check candidate rewrite..." << std::endl; |
136 |
|
// verify it if applicable |
137 |
245 |
if (d_doCheck) |
138 |
|
{ |
139 |
402 |
Node crr = solbr.eqNode(eq_solr).negate(); |
140 |
201 |
Trace("rr-check") << "Check candidate rewrite : " << crr << std::endl; |
141 |
|
|
142 |
|
// Notice we don't set produce-models. rrChecker takes the same |
143 |
|
// options as the SmtEngine we belong to, where we ensure that |
144 |
|
// produce-models is set. |
145 |
402 |
std::unique_ptr<SmtEngine> rrChecker; |
146 |
201 |
initializeChecker(rrChecker, crr); |
147 |
402 |
Result r = rrChecker->checkSat(); |
148 |
201 |
Trace("rr-check") << "...result : " << r << std::endl; |
149 |
201 |
if (r.asSatisfiabilityResult().isSat() == Result::SAT) |
150 |
|
{ |
151 |
125 |
Trace("rr-check") << "...rewrite does not hold for: " << std::endl; |
152 |
125 |
is_unique_term = true; |
153 |
250 |
std::vector<Node> vars; |
154 |
125 |
d_sampler->getVariables(vars); |
155 |
250 |
std::vector<Node> pt; |
156 |
433 |
for (const Node& v : vars) |
157 |
|
{ |
158 |
616 |
Node val; |
159 |
616 |
Node refv = v; |
160 |
|
// if a bound variable, map to the skolem we introduce before |
161 |
|
// looking up the model value |
162 |
308 |
if (v.getKind() == BOUND_VARIABLE) |
163 |
|
{ |
164 |
308 |
std::map<Node, Node>::iterator itf = d_fv_to_skolem.find(v); |
165 |
308 |
if (itf == d_fv_to_skolem.end()) |
166 |
|
{ |
167 |
|
// not in conjecture, can use arbitrary value |
168 |
|
val = v.getType().mkGroundTerm(); |
169 |
|
} |
170 |
|
else |
171 |
|
{ |
172 |
|
// get the model value of its skolem |
173 |
308 |
refv = itf->second; |
174 |
|
} |
175 |
|
} |
176 |
308 |
if (val.isNull()) |
177 |
|
{ |
178 |
308 |
Assert(!refv.isNull() && refv.getKind() != BOUND_VARIABLE); |
179 |
308 |
val = rrChecker->getValue(refv); |
180 |
|
} |
181 |
308 |
Trace("rr-check") << " " << v << " -> " << val << std::endl; |
182 |
308 |
pt.push_back(val); |
183 |
|
} |
184 |
125 |
d_sampler->addSamplePoint(pt); |
185 |
|
// add the solution again |
186 |
|
// by construction of the above point, we should be unique now |
187 |
125 |
eq_sol = d_sampler->registerTerm(sol); |
188 |
125 |
Assert(eq_sol == sol); |
189 |
|
} |
190 |
|
else |
191 |
|
{ |
192 |
76 |
verified = !r.asSatisfiabilityResult().isUnknown(); |
193 |
|
} |
194 |
|
} |
195 |
|
else |
196 |
|
{ |
197 |
|
// just insist that constants are not relevant pairs |
198 |
44 |
if (solb.isConst() && eq_solb.isConst()) |
199 |
|
{ |
200 |
|
is_unique_term = true; |
201 |
|
eq_sol = sol; |
202 |
|
} |
203 |
|
} |
204 |
245 |
if (!is_unique_term) |
205 |
|
{ |
206 |
|
// register this as a relevant pair (helps filtering) |
207 |
120 |
if (d_filterPairs) |
208 |
|
{ |
209 |
103 |
d_crewrite_filter.registerRelevantPair(sol, eq_sol); |
210 |
|
} |
211 |
|
// The analog of terms sol and eq_sol are equivalent under |
212 |
|
// sample points but do not rewrite to the same term. Hence, |
213 |
|
// this indicates a candidate rewrite. |
214 |
120 |
if (!d_silent) |
215 |
|
{ |
216 |
103 |
out << "(" << (verified ? "" : "candidate-") << "rewrite "; |
217 |
103 |
if (d_using_sygus) |
218 |
|
{ |
219 |
103 |
TermDbSygus::toStreamSygus(out, sol); |
220 |
103 |
out << " "; |
221 |
103 |
TermDbSygus::toStreamSygus(out, eq_sol); |
222 |
|
} |
223 |
|
else |
224 |
|
{ |
225 |
|
out << sol << " " << eq_sol; |
226 |
|
} |
227 |
103 |
out << ")" << std::endl; |
228 |
|
} |
229 |
|
// we count this as printed, despite not literally printing it |
230 |
120 |
rew_print = true; |
231 |
|
// debugging information |
232 |
120 |
if (Trace.isOn("sygus-rr-debug")) |
233 |
|
{ |
234 |
|
Trace("sygus-rr-debug") << "; candidate #1 ext-rewrites to: " << solbr |
235 |
|
<< std::endl; |
236 |
|
Trace("sygus-rr-debug") |
237 |
|
<< "; candidate #2 ext-rewrites to: " << eq_solr << std::endl; |
238 |
|
} |
239 |
120 |
if (d_rewAccel && d_using_sygus) |
240 |
|
{ |
241 |
|
Assert(d_tds != nullptr); |
242 |
|
// Add a symmetry breaking clause that excludes the larger |
243 |
|
// of sol and eq_sol. This effectively states that we no longer |
244 |
|
// wish to enumerate any term that contains sol (resp. eq_sol) |
245 |
|
// as a subterm. |
246 |
|
Node exc_sol = sol; |
247 |
|
unsigned sz = datatypes::utils::getSygusTermSize(sol); |
248 |
|
unsigned eqsz = datatypes::utils::getSygusTermSize(eq_sol); |
249 |
|
if (eqsz > sz) |
250 |
|
{ |
251 |
|
sz = eqsz; |
252 |
|
exc_sol = eq_sol; |
253 |
|
} |
254 |
|
TypeNode ptn = d_candidate.getType(); |
255 |
|
Node x = d_tds->getFreeVar(ptn, 0); |
256 |
|
Node lem = d_tds->getExplain()->getExplanationForEquality(x, exc_sol); |
257 |
|
lem = lem.negate(); |
258 |
|
Trace("sygus-rr-sb") << "Symmetry breaking lemma : " << lem |
259 |
|
<< std::endl; |
260 |
|
d_tds->registerSymBreakLemma(d_candidate, lem, ptn, sz); |
261 |
|
} |
262 |
|
} |
263 |
|
} |
264 |
|
// We count this as a rewrite if we did not explicitly rule it out. |
265 |
|
// The value of is_unique_term is false iff this call resulted in a rewrite. |
266 |
|
// Notice that when --sygus-rr-synth-check is enabled, |
267 |
|
// statistics on number of candidate rewrite rules is |
268 |
|
// an accurate count of (#enumerated_terms-#unique_terms) only if |
269 |
|
// the option sygus-rr-synth-filter-order is disabled. The reason |
270 |
|
// is that the sygus sampler may reason that a candidate rewrite |
271 |
|
// rule is not useful since its variables are unordered, whereby |
272 |
|
// it discards it as a redundant candidate rewrite rule before |
273 |
|
// checking its correctness. |
274 |
|
} |
275 |
1723 |
d_add_term_cache[sol] = eq_sol; |
276 |
1723 |
return eq_sol; |
277 |
|
} |
278 |
|
|
279 |
768 |
Node CandidateRewriteDatabase::addTerm(Node sol, bool rec, std::ostream& out) |
280 |
|
{ |
281 |
768 |
bool rew_print = false; |
282 |
768 |
return addTerm(sol, rec, out, rew_print); |
283 |
|
} |
284 |
|
bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out) |
285 |
|
{ |
286 |
|
Node rsol = addTerm(sol, false, out); |
287 |
|
return sol == rsol; |
288 |
|
} |
289 |
|
|
290 |
7 |
void CandidateRewriteDatabase::setSilent(bool flag) { d_silent = flag; } |
291 |
|
|
292 |
7 |
void CandidateRewriteDatabase::enableExtendedRewriter() |
293 |
|
{ |
294 |
7 |
d_useExtRewriter = true; |
295 |
7 |
} |
296 |
|
|
297 |
|
} // namespace quantifiers |
298 |
|
} // namespace theory |
299 |
29574 |
} // namespace cvc5 |