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