1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Mathias Preiner, 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 cegis core connective module. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/quantifiers/sygus/cegis_core_connective.h" |
17 |
|
|
18 |
|
#include "expr/dtype_cons.h" |
19 |
|
#include "options/base_options.h" |
20 |
|
#include "printer/printer.h" |
21 |
|
#include "proof/unsat_core.h" |
22 |
|
#include "smt/smt_engine.h" |
23 |
|
#include "smt/smt_engine_scope.h" |
24 |
|
#include "theory/datatypes/theory_datatypes_utils.h" |
25 |
|
#include "theory/quantifiers/sygus/ce_guided_single_inv.h" |
26 |
|
#include "theory/quantifiers/sygus/transition_inference.h" |
27 |
|
#include "theory/quantifiers/term_util.h" |
28 |
|
#include "theory/rewriter.h" |
29 |
|
#include "theory/smt_engine_subsolver.h" |
30 |
|
#include "util/random.h" |
31 |
|
|
32 |
|
using namespace cvc5::kind; |
33 |
|
|
34 |
|
namespace cvc5 { |
35 |
|
namespace theory { |
36 |
|
namespace quantifiers { |
37 |
|
|
38 |
15 |
bool VariadicTrie::add(Node n, const std::vector<Node>& i) |
39 |
|
{ |
40 |
15 |
VariadicTrie* curr = this; |
41 |
35 |
for (const Node& ic : i) |
42 |
|
{ |
43 |
20 |
curr = &(curr->d_children[ic]); |
44 |
|
} |
45 |
15 |
if (curr->d_data.isNull()) |
46 |
|
{ |
47 |
15 |
curr->d_data = n; |
48 |
15 |
return true; |
49 |
|
} |
50 |
|
return false; |
51 |
|
} |
52 |
|
|
53 |
329 |
bool VariadicTrie::hasSubset(const std::vector<Node>& is) const |
54 |
|
{ |
55 |
329 |
if (!d_data.isNull()) |
56 |
|
{ |
57 |
142 |
return true; |
58 |
|
} |
59 |
685 |
for (const std::pair<const Node, VariadicTrie>& p : d_children) |
60 |
|
{ |
61 |
1149 |
Node n = p.first; |
62 |
651 |
if (std::find(is.begin(), is.end(), n) != is.end()) |
63 |
|
{ |
64 |
155 |
if (p.second.hasSubset(is)) |
65 |
|
{ |
66 |
153 |
return true; |
67 |
|
} |
68 |
|
} |
69 |
|
} |
70 |
34 |
return false; |
71 |
|
} |
72 |
|
|
73 |
1529 |
CegisCoreConnective::CegisCoreConnective(QuantifiersInferenceManager& qim, |
74 |
|
TermDbSygus* tds, |
75 |
1529 |
SynthConjecture* p) |
76 |
1529 |
: Cegis(qim, tds, p) |
77 |
|
{ |
78 |
1529 |
d_true = NodeManager::currentNM()->mkConst(true); |
79 |
1529 |
d_false = NodeManager::currentNM()->mkConst(false); |
80 |
1529 |
} |
81 |
|
|
82 |
5 |
bool CegisCoreConnective::processInitialize(Node conj, |
83 |
|
Node n, |
84 |
|
const std::vector<Node>& candidates, |
85 |
|
std::vector<Node>& lemmas) |
86 |
|
{ |
87 |
5 |
Trace("sygus-ccore-init") << "CegisCoreConnective::initialize" << std::endl; |
88 |
5 |
Trace("sygus-ccore-init") << " conjecture : " << conj << std::endl; |
89 |
5 |
Trace("sygus-ccore-init") << " candidates : " << candidates << std::endl; |
90 |
5 |
if (candidates.size() != 1) |
91 |
|
{ |
92 |
|
Trace("sygus-ccore-init") |
93 |
|
<< "...only applies to single candidate conjectures." << std::endl; |
94 |
|
return false; |
95 |
|
} |
96 |
5 |
d_candidate = candidates[0]; |
97 |
5 |
Assert(conj.getKind() == FORALL); |
98 |
5 |
Assert(conj[0].getNumChildren() == 1); |
99 |
10 |
Node body = conj[1]; |
100 |
5 |
if (body.getKind() == NOT && body[0].getKind() == FORALL) |
101 |
|
{ |
102 |
4 |
body = body[0][1]; |
103 |
|
} |
104 |
|
else |
105 |
|
{ |
106 |
1 |
body = TermUtil::simpleNegate(body); |
107 |
|
} |
108 |
5 |
Trace("sygus-ccore-init") << " body : " << body << std::endl; |
109 |
|
|
110 |
10 |
TransitionInference ti; |
111 |
5 |
ti.process(body, conj[0][0]); |
112 |
|
|
113 |
5 |
if (!ti.isComplete()) |
114 |
|
{ |
115 |
|
Trace("sygus-ccore-init") << "...could not infer predicate." << std::endl; |
116 |
|
return false; |
117 |
|
} |
118 |
5 |
if (ti.isTrivial()) |
119 |
|
{ |
120 |
|
// not necessary to use this class if the conjecture is trivial (does |
121 |
|
// not contain the function-to-synthesize). |
122 |
1 |
Trace("sygus-ccore-init") << "...conjecture is trivial." << std::endl; |
123 |
1 |
return false; |
124 |
|
} |
125 |
8 |
Node trans = ti.getTransitionRelation(); |
126 |
4 |
Trace("sygus-ccore-init") << " transition relation: " << trans << std::endl; |
127 |
4 |
if (!trans.isConst() || trans.getConst<bool>()) |
128 |
|
{ |
129 |
|
Trace("sygus-ccore-init") |
130 |
|
<< "...does not apply conjectures with transition relations." |
131 |
|
<< std::endl; |
132 |
|
return false; |
133 |
|
} |
134 |
|
|
135 |
|
// the grammar must allow AND / OR when applicable |
136 |
8 |
TypeNode gt = d_candidate.getType(); |
137 |
|
|
138 |
8 |
Node f = ti.getFunction(); |
139 |
4 |
Assert(!f.isNull()); |
140 |
4 |
Trace("sygus-ccore-init") << " predicate: " << f << std::endl; |
141 |
4 |
ti.getVariables(d_vars); |
142 |
4 |
Trace("sygus-ccore-init") << " variables: " << d_vars << std::endl; |
143 |
|
// make the evaluation function |
144 |
8 |
std::vector<Node> echildren; |
145 |
4 |
echildren.push_back(d_candidate); |
146 |
4 |
echildren.insert(echildren.end(), d_vars.begin(), d_vars.end()); |
147 |
4 |
d_eterm = NodeManager::currentNM()->mkNode(DT_SYGUS_EVAL, echildren); |
148 |
4 |
Trace("sygus-ccore-init") << " evaluation term: " << d_eterm << std::endl; |
149 |
|
|
150 |
8 |
Node prePost[2]; |
151 |
4 |
prePost[0] = ti.getPreCondition(); |
152 |
|
// negate the post condition |
153 |
4 |
prePost[1] = TermUtil::simpleNegate(ti.getPostCondition()); |
154 |
4 |
Trace("sygus-ccore-init") << " precondition: " << prePost[0] << std::endl; |
155 |
4 |
Trace("sygus-ccore-init") << " postcondition: " << prePost[1] << std::endl; |
156 |
|
|
157 |
|
// side condition? |
158 |
8 |
QAttributes qa; |
159 |
4 |
QuantAttributes::computeQuantAttributes(conj, qa); |
160 |
8 |
Node sc = qa.d_sygusSideCondition; |
161 |
4 |
if (!sc.isNull()) |
162 |
|
{ |
163 |
4 |
Trace("sygus-ccore-init") << " side condition: " << sc << std::endl; |
164 |
4 |
if (sc.getKind() == EXISTS) |
165 |
|
{ |
166 |
4 |
sc = sc[1]; |
167 |
|
} |
168 |
8 |
Node scb = TermUtil::simpleNegate(sc); |
169 |
8 |
TransitionInference tisc; |
170 |
4 |
tisc.process(scb, conj[0][0]); |
171 |
8 |
Node scTrans = ti.getTransitionRelation(); |
172 |
8 |
Trace("sygus-ccore-init") |
173 |
4 |
<< " transition relation of SC: " << scTrans << std::endl; |
174 |
4 |
if (tisc.isComplete() && scTrans.isConst() && !scTrans.getConst<bool>()) |
175 |
|
{ |
176 |
8 |
std::vector<Node> scVars; |
177 |
4 |
tisc.getVariables(scVars); |
178 |
8 |
Node scPre = tisc.getPreCondition(); |
179 |
4 |
scPre = scPre.substitute( |
180 |
|
scVars.begin(), scVars.end(), d_vars.begin(), d_vars.end()); |
181 |
8 |
Node scPost = TermUtil::simpleNegate(tisc.getPostCondition()); |
182 |
4 |
scPost = scPost.substitute( |
183 |
|
scVars.begin(), scVars.end(), d_vars.begin(), d_vars.end()); |
184 |
8 |
Trace("sygus-ccore-init") |
185 |
4 |
<< " precondition of SC: " << scPre << std::endl; |
186 |
8 |
Trace("sygus-ccore-init") |
187 |
4 |
<< " postcondition of SC: " << scPost << std::endl; |
188 |
|
// We are extracting the side condition to be used by this algorithm |
189 |
|
// from the side condition ascribed to the synthesis conjecture. |
190 |
|
// A sygus conjecture of the form, for predicate-to-synthesize I: |
191 |
|
// exists I. forall x. P[I,x] |
192 |
|
// whose ascribed side condition is C[I], has the semantics: |
193 |
|
// exists I. C[I] ^ forall x. P[I,x]. |
194 |
|
// Notice that this side condition C may be an arbitrary formula over the |
195 |
|
// function to synthesize. However, the algorithm implemented by this |
196 |
|
// class is restricted to side conditions of the form: |
197 |
|
// exists k. A[k] ^ I(k) |
198 |
|
// The above condition guards for this case, and runs this block of code, |
199 |
|
// where we use the TransitionInference utility to extract A[k] from |
200 |
|
// A[k] ^ I(k). In the end, we set d_sc to A[d_vars]; notice the variables |
201 |
|
// d_vars are those introduced by the TransitionInference utility |
202 |
|
// for normalization. |
203 |
4 |
d_sc = scPost; |
204 |
|
} |
205 |
|
} |
206 |
|
|
207 |
|
// We use the postcondition if it non-trivial and the grammar gt for our |
208 |
|
// candidate has the production rule gt -> AND( gt, gt ). Similarly for |
209 |
|
// precondition and OR. |
210 |
4 |
Assert(gt.isDatatype()); |
211 |
4 |
const DType& gdt = gt.getDType(); |
212 |
4 |
SygusTypeInfo& gti = d_tds->getTypeInfo(gt); |
213 |
12 |
for (unsigned r = 0; r < 2; r++) |
214 |
|
{ |
215 |
12 |
Node node = prePost[r]; |
216 |
8 |
if (node.isConst()) |
217 |
|
{ |
218 |
|
// this direction is trivial, ignore |
219 |
4 |
continue; |
220 |
|
} |
221 |
4 |
Component& c = r == 0 ? d_pre : d_post; |
222 |
4 |
Kind rk = r == 0 ? OR : AND; |
223 |
4 |
int i = gti.getKindConsNum(rk); |
224 |
7 |
if (i != -1 && gdt[i].getNumArgs() == 2 |
225 |
7 |
&& gdt[i].getArgType(0) == gt |
226 |
7 |
&& gdt[i].getArgType(1) == gt) |
227 |
|
{ |
228 |
6 |
Trace("sygus-ccore-init") << " will do " << (r == 0 ? "pre" : "post") |
229 |
3 |
<< "condition." << std::endl; |
230 |
6 |
Node cons = gdt[i].getConstructor(); |
231 |
3 |
c.initialize(node, cons); |
232 |
|
// Register the symmetry breaking lemma: do not do top-level solutions |
233 |
|
// with this constructor (e.g. we want to enumerate literals, not |
234 |
|
// conjunctions). |
235 |
6 |
Node tst = datatypes::utils::mkTester(d_candidate, i, gdt); |
236 |
3 |
Trace("sygus-ccore-init") << "Sym break lemma " << tst << std::endl; |
237 |
3 |
lemmas.push_back(tst.negate()); |
238 |
|
} |
239 |
|
} |
240 |
4 |
if (!isActive()) |
241 |
|
{ |
242 |
1 |
return false; |
243 |
|
} |
244 |
|
// initialize the enumerator |
245 |
3 |
return Cegis::processInitialize(conj, n, candidates, lemmas); |
246 |
|
} |
247 |
|
|
248 |
46 |
bool CegisCoreConnective::processConstructCandidates( |
249 |
|
const std::vector<Node>& enums, |
250 |
|
const std::vector<Node>& enum_values, |
251 |
|
const std::vector<Node>& candidates, |
252 |
|
std::vector<Node>& candidate_values, |
253 |
|
bool satisfiedRl, |
254 |
|
std::vector<Node>& lems) |
255 |
|
{ |
256 |
46 |
Assert(isActive()); |
257 |
46 |
bool ret = constructSolution(enums, enum_values, candidate_values); |
258 |
|
|
259 |
|
// exclude in the basic way if passive |
260 |
46 |
Assert(enums.size() == 1); |
261 |
46 |
NodeManager* nm = NodeManager::currentNM(); |
262 |
92 |
for (unsigned i = 0, esize = enums.size(); i < esize; i++) |
263 |
|
{ |
264 |
92 |
Node e = enums[i]; |
265 |
46 |
if (!d_tds->isPassiveEnumerator(e)) |
266 |
|
{ |
267 |
|
continue; |
268 |
|
} |
269 |
92 |
Node v = enum_values[i]; |
270 |
92 |
Node lem = d_tds->getExplain()->getExplanationForEquality(e, v).negate(); |
271 |
92 |
Node g = d_tds->getActiveGuardForEnumerator(e); |
272 |
46 |
if (!g.isNull()) |
273 |
|
{ |
274 |
|
lem = nm->mkNode(OR, g.negate(), lem); |
275 |
|
} |
276 |
46 |
lems.push_back(lem); |
277 |
|
} |
278 |
46 |
return ret; |
279 |
|
} |
280 |
|
|
281 |
96 |
bool CegisCoreConnective::isActive() const |
282 |
|
{ |
283 |
96 |
return d_pre.isActive() || d_post.isActive(); |
284 |
|
} |
285 |
|
|
286 |
46 |
bool CegisCoreConnective::constructSolution( |
287 |
|
const std::vector<Node>& candidates, |
288 |
|
const std::vector<Node>& candidate_values, |
289 |
|
std::vector<Node>& solv) |
290 |
|
{ |
291 |
|
// if the conjecture is not the right shape, no repair is possible |
292 |
46 |
if (!isActive()) |
293 |
|
{ |
294 |
|
return false; |
295 |
|
} |
296 |
46 |
Assert(candidates.size() == candidate_values.size()); |
297 |
92 |
Trace("sygus-ccore-summary") |
298 |
46 |
<< "CegisCoreConnective: construct solution..." << std::endl; |
299 |
46 |
if (Trace.isOn("sygus-ccore")) |
300 |
|
{ |
301 |
|
Trace("sygus-ccore") |
302 |
|
<< "CegisCoreConnective: Construct candidate solutions..." << std::endl; |
303 |
|
for (unsigned i = 0, size = candidates.size(); i < size; i++) |
304 |
|
{ |
305 |
|
std::stringstream ss; |
306 |
|
TermDbSygus::toStreamSygus(ss, candidate_values[i]); |
307 |
|
Trace("sygus-ccore") << " " << candidates[i] << " -> " << ss.str() |
308 |
|
<< std::endl; |
309 |
|
} |
310 |
|
} |
311 |
46 |
Assert(candidates.size() == 1 && candidates[0] == d_candidate); |
312 |
92 |
TNode cval = candidate_values[0]; |
313 |
92 |
Node ets = d_eterm.substitute(d_candidate, cval); |
314 |
92 |
Node etsr = Rewriter::rewrite(ets); |
315 |
46 |
Trace("sygus-ccore-debug") << "...predicate is: " << etsr << std::endl; |
316 |
46 |
NodeManager* nm = NodeManager::currentNM(); |
317 |
135 |
for (unsigned d = 0; d < 2; d++) |
318 |
|
{ |
319 |
92 |
Component& ccheck = d == 0 ? d_pre : d_post; |
320 |
92 |
if (!ccheck.isActive()) |
321 |
|
{ |
322 |
|
// not trying this direction |
323 |
92 |
continue; |
324 |
|
} |
325 |
46 |
Component& cfilter = d == 0 ? d_post : d_pre; |
326 |
|
// In terms of the algorithm described in the h file, this gets the formula |
327 |
|
// A (or B, depending on the direction d). |
328 |
89 |
Node fpred = cfilter.getFormula(); |
329 |
46 |
if (!fpred.isNull() && !fpred.isConst()) |
330 |
|
{ |
331 |
|
// check refinement points |
332 |
|
Node etsrn = d == 0 ? etsr : etsr.negate(); |
333 |
|
std::unordered_set<Node> visited; |
334 |
|
std::vector<Node> pt; |
335 |
|
Node rid = cfilter.getRefinementPt(this, etsrn, visited, pt); |
336 |
|
if (!rid.isNull()) |
337 |
|
{ |
338 |
|
// failed a refinement point |
339 |
|
continue; |
340 |
|
} |
341 |
|
Node fassert = nm->mkNode(AND, fpred, etsrn); |
342 |
|
Trace("sygus-ccore-debug") |
343 |
|
<< "...check filter " << fassert << "..." << std::endl; |
344 |
|
std::vector<Node> mvs; |
345 |
|
Result r = checkSat(fassert, mvs); |
346 |
|
Trace("sygus-ccore-debug") << "...got " << r << std::endl; |
347 |
|
if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) |
348 |
|
{ |
349 |
|
// failed the filter, remember the refinement point |
350 |
|
if (r.asSatisfiabilityResult().isSat() == Result::SAT) |
351 |
|
{ |
352 |
|
cfilter.addRefinementPt(fassert, mvs); |
353 |
|
} |
354 |
|
continue; |
355 |
|
} |
356 |
|
} |
357 |
92 |
Trace("sygus-ccore-debug") |
358 |
46 |
<< "...add to pool in direction " << d << std::endl; |
359 |
|
// implements e.g. pool(B) += e_i. |
360 |
46 |
ccheck.addToPool(etsr, cval); |
361 |
|
|
362 |
|
// ----- get the pool of assertions and randomize it |
363 |
89 |
std::vector<Node> passerts; |
364 |
46 |
ccheck.getTermPool(passerts); |
365 |
46 |
std::shuffle(passerts.begin(), passerts.end(), Random::getRandom()); |
366 |
|
|
367 |
|
// ----- check for entailment, adding based on models of failed points |
368 |
89 |
std::vector<Node> asserts; |
369 |
89 |
Node sol = constructSolutionFromPool(ccheck, asserts, passerts); |
370 |
46 |
if (!sol.isNull()) |
371 |
|
{ |
372 |
3 |
solv.push_back(sol); |
373 |
3 |
Trace("sygus-ccore-summary") << "...success" << std::endl; |
374 |
3 |
return true; |
375 |
|
} |
376 |
43 |
if (Trace.isOn("sygus-ccore-summary")) |
377 |
|
{ |
378 |
|
std::stringstream ss; |
379 |
|
ccheck.debugPrintSummary(ss); |
380 |
|
Trace("sygus-ccore-summary") |
381 |
|
<< "C[d=" << d << "] " << ss.str() << std::endl; |
382 |
|
} |
383 |
|
} |
384 |
86 |
Trace("sygus-ccore") << "CegisCoreConnective: failed to generate candidate" |
385 |
43 |
<< std::endl; |
386 |
43 |
Trace("sygus-ccore-summary") << "...failed" << std::endl; |
387 |
43 |
return false; |
388 |
|
} |
389 |
|
|
390 |
3 |
void CegisCoreConnective::Component::initialize(Node n, Node c) |
391 |
|
{ |
392 |
3 |
d_this = n; |
393 |
3 |
d_scons = c; |
394 |
3 |
} |
395 |
|
|
396 |
46 |
void CegisCoreConnective::Component::addToPool(Node n, Node s) |
397 |
|
{ |
398 |
46 |
d_cpool.push_back(n); |
399 |
46 |
d_cpoolToSol[n] = s; |
400 |
46 |
} |
401 |
|
|
402 |
3 |
Node CegisCoreConnective::Component::getSygusSolution( |
403 |
|
std::vector<Node>& conjs) const |
404 |
|
{ |
405 |
3 |
std::sort(conjs.begin(), conjs.end()); |
406 |
3 |
Node sol; |
407 |
3 |
std::map<Node, Node>::const_iterator itu; |
408 |
3 |
NodeManager* nm = NodeManager::currentNM(); |
409 |
11 |
for (const Node& u : conjs) |
410 |
|
{ |
411 |
8 |
itu = d_cpoolToSol.find(u); |
412 |
8 |
Assert(itu != d_cpoolToSol.end()); |
413 |
16 |
Node s = itu->second; |
414 |
8 |
Trace("sygus-ccore-debug-sy") << " uc-s " << s << std::endl; |
415 |
8 |
if (sol.isNull()) |
416 |
|
{ |
417 |
3 |
sol = s; |
418 |
|
} |
419 |
|
else |
420 |
|
{ |
421 |
5 |
sol = nm->mkNode(APPLY_CONSTRUCTOR, d_scons, s, sol); |
422 |
|
} |
423 |
|
} |
424 |
3 |
return sol; |
425 |
|
} |
426 |
|
void CegisCoreConnective::Component::debugPrintSummary(std::ostream& os) const |
427 |
|
{ |
428 |
|
os << "size(pool/pts/cores): " << d_cpool.size() << "/" << d_numRefPoints |
429 |
|
<< "/" << d_numFalseCores; |
430 |
|
} |
431 |
|
|
432 |
10 |
void CegisCoreConnective::Component::addRefinementPt( |
433 |
|
Node id, const std::vector<Node>& pt) |
434 |
|
{ |
435 |
10 |
d_numRefPoints++; |
436 |
10 |
bool res = d_refinementPt.addTerm(id, pt); |
437 |
|
// this should always be a new point |
438 |
10 |
AlwaysAssert(res); |
439 |
10 |
} |
440 |
15 |
void CegisCoreConnective::Component::addFalseCore(Node id, |
441 |
|
const std::vector<Node>& u) |
442 |
|
{ |
443 |
15 |
d_numFalseCores++; |
444 |
15 |
d_falseCores.add(id, u); |
445 |
15 |
} |
446 |
|
|
447 |
87 |
Node CegisCoreConnective::Component::getRefinementPt( |
448 |
|
CegisCoreConnective* p, |
449 |
|
Node n, |
450 |
|
std::unordered_set<Node>& visited, |
451 |
|
std::vector<Node>& ss) |
452 |
|
{ |
453 |
174 |
std::vector<Node> ctx; |
454 |
|
|
455 |
87 |
unsigned depth = p->d_vars.size(); |
456 |
174 |
std::map<NodeTrie*, std::map<Node, NodeTrie>::iterator> vt; |
457 |
87 |
std::map<NodeTrie*, std::map<Node, NodeTrie>::iterator>::iterator itvt; |
458 |
87 |
std::map<Node, NodeTrie>::iterator itv; |
459 |
174 |
std::vector<NodeTrie*> visit; |
460 |
|
NodeTrie* cur; |
461 |
87 |
visit.push_back(&d_refinementPt); |
462 |
2483 |
do |
463 |
|
{ |
464 |
2570 |
cur = visit.back(); |
465 |
2570 |
Trace("sygus-ccore-ref") << "process trie " << cur << std::endl; |
466 |
2570 |
if (ctx.size() == depth) |
467 |
|
{ |
468 |
113 |
Trace("sygus-ccore-ref") << "...at depth " << std::endl; |
469 |
|
// at leaf |
470 |
161 |
Node id = cur->getData(); |
471 |
113 |
Trace("sygus-ccore-ref") << "...data is " << id << std::endl; |
472 |
113 |
Assert(!id.isNull()); |
473 |
113 |
AlwaysAssert(id.getType().isBoolean()); |
474 |
113 |
if (visited.find(id) == visited.end()) |
475 |
|
{ |
476 |
78 |
visited.insert(id); |
477 |
78 |
Trace("sygus-ccore-ref") << "...eval " << std::endl; |
478 |
|
// check if it is true |
479 |
91 |
Node en = p->evaluate(n, id, ctx); |
480 |
78 |
if (en.isConst() && en.getConst<bool>()) |
481 |
|
{ |
482 |
65 |
ss = ctx; |
483 |
65 |
return id; |
484 |
|
} |
485 |
|
} |
486 |
48 |
visit.pop_back(); |
487 |
48 |
ctx.pop_back(); |
488 |
|
} |
489 |
|
else |
490 |
|
{ |
491 |
|
// get the current child iterator for this node |
492 |
2457 |
itvt = vt.find(cur); |
493 |
2457 |
if (itvt == vt.end()) |
494 |
|
{ |
495 |
1774 |
Trace("sygus-ccore-ref") << "...initialize iterator " << std::endl; |
496 |
|
// initialize the iterator |
497 |
1774 |
itv = cur->d_data.begin(); |
498 |
1774 |
vt[cur] = itv; |
499 |
1774 |
Trace("sygus-ccore-ref") << "...finished init" << std::endl; |
500 |
|
} |
501 |
|
else |
502 |
|
{ |
503 |
683 |
Trace("sygus-ccore-ref") << "...continue iterator " << std::endl; |
504 |
683 |
itv = itvt->second; |
505 |
|
} |
506 |
2457 |
Trace("sygus-ccore-ref") << "...now check status" << std::endl; |
507 |
|
// are we done iterating children? |
508 |
2457 |
if (itv == cur->d_data.end()) |
509 |
|
{ |
510 |
657 |
Trace("sygus-ccore-ref") << "...finished iterating " << std::endl; |
511 |
|
// yes, pop back |
512 |
657 |
if (!ctx.empty()) |
513 |
|
{ |
514 |
635 |
ctx.pop_back(); |
515 |
|
} |
516 |
657 |
visit.pop_back(); |
517 |
657 |
vt.erase(cur); |
518 |
|
} |
519 |
|
else |
520 |
|
{ |
521 |
1800 |
Trace("sygus-ccore-ref") << "...recurse " << itv->first << std::endl; |
522 |
|
// recurse |
523 |
1800 |
ctx.push_back(itv->first); |
524 |
1800 |
visit.push_back(&(itv->second)); |
525 |
1800 |
++vt[cur]; |
526 |
|
} |
527 |
|
} |
528 |
|
|
529 |
2505 |
} while (!visit.empty()); |
530 |
22 |
return Node::null(); |
531 |
|
} |
532 |
|
|
533 |
46 |
void CegisCoreConnective::Component::getTermPool( |
534 |
|
std::vector<Node>& passerts) const |
535 |
|
{ |
536 |
46 |
passerts.insert(passerts.end(), d_cpool.begin(), d_cpool.end()); |
537 |
46 |
} |
538 |
|
|
539 |
75 |
bool CegisCoreConnective::Component::addToAsserts(CegisCoreConnective* p, |
540 |
|
std::vector<Node>& passerts, |
541 |
|
const std::vector<Node>& mvs, |
542 |
|
Node mvId, |
543 |
|
std::vector<Node>& asserts, |
544 |
|
Node& an) |
545 |
|
{ |
546 |
|
// point should be valid |
547 |
75 |
Assert(!mvId.isNull()); |
548 |
150 |
Node n; |
549 |
75 |
unsigned currIndex = 0; |
550 |
142 |
do |
551 |
|
{ |
552 |
|
// select condition from passerts that evaluates to false on mvs |
553 |
843 |
for (unsigned i = currIndex, psize = passerts.size(); i < psize; i++) |
554 |
|
{ |
555 |
1426 |
Node cn = passerts[i]; |
556 |
1426 |
Node cne = p->evaluate(cn, mvId, mvs); |
557 |
800 |
if (cne.isConst() && !cne.getConst<bool>()) |
558 |
|
{ |
559 |
174 |
n = cn; |
560 |
|
// remove n from the pool |
561 |
174 |
passerts.erase(passerts.begin() + i, passerts.begin() + i + 1); |
562 |
174 |
currIndex = i; |
563 |
174 |
break; |
564 |
|
} |
565 |
|
} |
566 |
217 |
if (n.isNull()) |
567 |
|
{ |
568 |
|
// could not find any |
569 |
43 |
return false; |
570 |
|
} |
571 |
174 |
Trace("sygus-ccore-debug") << "...try adding " << n << "..." << std::endl; |
572 |
174 |
asserts.push_back(n); |
573 |
|
// is it already part of a false core? |
574 |
174 |
if (d_falseCores.hasSubset(asserts)) |
575 |
|
{ |
576 |
284 |
Trace("sygus-ccore-debug") |
577 |
142 |
<< "..." << n << " was rejected due to previous false core" |
578 |
142 |
<< std::endl; |
579 |
142 |
asserts.pop_back(); |
580 |
142 |
n = Node::null(); |
581 |
|
} |
582 |
174 |
} while (n.isNull()); |
583 |
64 |
Trace("sygus-ccore") << "--- Insert " << n << " to falsify " << mvs |
584 |
32 |
<< std::endl; |
585 |
|
// success |
586 |
32 |
if (an.isConst()) |
587 |
|
{ |
588 |
21 |
Assert(an.getConst<bool>()); |
589 |
21 |
an = n; |
590 |
|
} |
591 |
|
else |
592 |
|
{ |
593 |
11 |
an = NodeManager::currentNM()->mkNode(AND, n, an); |
594 |
|
} |
595 |
32 |
return true; |
596 |
|
} |
597 |
|
|
598 |
10 |
void CegisCoreConnective::getModel(SmtEngine& smt, |
599 |
|
std::vector<Node>& vals) const |
600 |
|
{ |
601 |
113 |
for (const Node& v : d_vars) |
602 |
|
{ |
603 |
206 |
Node mv = smt.getValue(v); |
604 |
103 |
Trace("sygus-ccore-model") << v << " -> " << mv << " "; |
605 |
103 |
vals.push_back(mv); |
606 |
|
} |
607 |
10 |
} |
608 |
|
|
609 |
29 |
bool CegisCoreConnective::getUnsatCore( |
610 |
|
SmtEngine& smt, |
611 |
|
const std::unordered_set<Node>& queryAsserts, |
612 |
|
std::vector<Node>& uasserts) const |
613 |
|
{ |
614 |
58 |
UnsatCore uc = smt.getUnsatCore(); |
615 |
29 |
bool hasQuery = false; |
616 |
99 |
for (UnsatCore::const_iterator i = uc.begin(); i != uc.end(); ++i) |
617 |
|
{ |
618 |
113 |
Node uassert = *i; |
619 |
70 |
Trace("sygus-ccore-debug") << " uc " << uassert << std::endl; |
620 |
97 |
if (queryAsserts.find(uassert) != queryAsserts.end()) |
621 |
|
{ |
622 |
27 |
hasQuery = true; |
623 |
27 |
continue; |
624 |
|
} |
625 |
43 |
uasserts.push_back(uassert); |
626 |
|
} |
627 |
58 |
return hasQuery; |
628 |
|
} |
629 |
|
|
630 |
|
Result CegisCoreConnective::checkSat(Node n, std::vector<Node>& mvs) const |
631 |
|
{ |
632 |
|
Trace("sygus-ccore-debug") << "...check-sat " << n << "..." << std::endl; |
633 |
|
Result r = checkWithSubsolver(n, d_vars, mvs); |
634 |
|
Trace("sygus-ccore-debug") << "...got " << r << std::endl; |
635 |
|
return r; |
636 |
|
} |
637 |
|
|
638 |
908 |
Node CegisCoreConnective::evaluate(Node n, |
639 |
|
Node id, |
640 |
|
const std::vector<Node>& mvs) |
641 |
|
{ |
642 |
908 |
Kind nk = n.getKind(); |
643 |
908 |
if (nk == AND || nk == OR) |
644 |
|
{ |
645 |
10 |
NodeManager* nm = NodeManager::currentNM(); |
646 |
10 |
bool expRes = nk == OR; |
647 |
|
// split AND/OR |
648 |
30 |
for (const Node& nc : n) |
649 |
|
{ |
650 |
40 |
Node enc = evaluate(nc, id, mvs); |
651 |
20 |
Assert(enc.isConst()); |
652 |
20 |
if (enc.getConst<bool>() == expRes) |
653 |
|
{ |
654 |
|
return nm->mkConst(expRes); |
655 |
|
} |
656 |
|
} |
657 |
10 |
return nm->mkConst(!expRes); |
658 |
|
} |
659 |
898 |
std::unordered_map<Node, Node>& ec = d_eval_cache[n]; |
660 |
898 |
if (!id.isNull()) |
661 |
|
{ |
662 |
878 |
std::unordered_map<Node, Node>::iterator it = ec.find(id); |
663 |
878 |
if (it != ec.end()) |
664 |
|
{ |
665 |
769 |
return it->second; |
666 |
|
} |
667 |
|
} |
668 |
|
// use evaluator |
669 |
258 |
Node cn = d_eval.eval(n, d_vars, mvs); |
670 |
129 |
if (cn.isNull()) |
671 |
|
{ |
672 |
|
cn = n.substitute(d_vars.begin(), d_vars.end(), mvs.begin(), mvs.end()); |
673 |
|
cn = Rewriter::rewrite(cn); |
674 |
|
} |
675 |
129 |
if (!id.isNull()) |
676 |
|
{ |
677 |
109 |
ec[id] = cn; |
678 |
|
} |
679 |
129 |
return cn; |
680 |
|
} |
681 |
|
|
682 |
61 |
Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, |
683 |
|
std::vector<Node>& asserts, |
684 |
|
std::vector<Node>& passerts) |
685 |
|
{ |
686 |
|
// In terms of Variant #2 from the header file, the set D is represented by |
687 |
|
// asserts. The available set of prediates pool(B) is represented by passerts. |
688 |
61 |
NodeManager* nm = NodeManager::currentNM(); |
689 |
61 |
Trace("sygus-ccore") << "------ Get initial candidate..." << std::endl; |
690 |
61 |
Node an = asserts.empty() |
691 |
|
? d_true |
692 |
122 |
: (asserts.size() == 1 ? asserts[0] : nm->mkNode(AND, asserts)); |
693 |
122 |
std::vector<Node> mvs; |
694 |
122 |
std::unordered_set<Node> visited; |
695 |
61 |
bool addSuccess = true; |
696 |
|
// Ensure that the current conjunction evaluates to false on all refinement |
697 |
|
// points. We get refinement points until we have exhausted. |
698 |
|
// In terms of Variant #2, this is inner while loop that adds points to D |
699 |
|
// while there exists a point in pts(B) such that D is true. |
700 |
122 |
Node mvId; |
701 |
26 |
do |
702 |
|
{ |
703 |
87 |
mvs.clear(); |
704 |
87 |
Trace("sygus-ccore-debug") << "...get refinement pt..." << std::endl; |
705 |
|
// In terms of Variant #2, this implements the line: |
706 |
|
// "D[v] is true for some v in pts(B)", |
707 |
|
// where v is stored in mvs. |
708 |
87 |
mvId = ccheck.getRefinementPt(this, an, visited, mvs); |
709 |
87 |
if (!mvId.isNull()) |
710 |
|
{ |
711 |
65 |
Trace("sygus-ccore-debug") << "...got " << mvs << std::endl; |
712 |
|
// In terms of Variant #2, this checks the conditions: |
713 |
|
// "d'[v] is false for some d' in pool(B)" and |
714 |
|
// "no element of cores(B) is a subset of D ++ { d' }" |
715 |
|
// and adds d' to D (asserts) if possible. |
716 |
65 |
addSuccess = ccheck.addToAsserts(this, passerts, mvs, mvId, asserts, an); |
717 |
130 |
Trace("sygus-ccore-debug") |
718 |
65 |
<< "...add success is " << addSuccess << std::endl; |
719 |
|
} |
720 |
|
else |
721 |
|
{ |
722 |
22 |
Trace("sygus-ccore-debug") << "...failed" << std::endl; |
723 |
|
} |
724 |
87 |
} while (!mvId.isNull() && addSuccess); |
725 |
61 |
if (!addSuccess) |
726 |
|
{ |
727 |
78 |
Trace("sygus-ccore") << ">>> Failed to generate initial candidate" |
728 |
39 |
<< std::endl; |
729 |
39 |
return Node::null(); |
730 |
|
} |
731 |
22 |
Trace("sygus-ccore") << "----- Initial candidate is " << an << std::endl; |
732 |
|
|
733 |
|
// We now have constructed an initial candidate for D. In terms of Variant #2, |
734 |
|
// we now enter the block code within "if D is false for all v in pts(B)". |
735 |
|
// Further refinements to D are made as the following do-while loop proceeds. |
736 |
10 |
do |
737 |
|
{ |
738 |
28 |
addSuccess = false; |
739 |
|
// try a new core |
740 |
38 |
std::unique_ptr<SmtEngine> checkSol; |
741 |
28 |
initializeSubsolver(checkSol); |
742 |
28 |
Trace("sygus-ccore") << "----- Check candidate " << an << std::endl; |
743 |
38 |
std::vector<Node> rasserts = asserts; |
744 |
28 |
rasserts.push_back(d_sc); |
745 |
28 |
rasserts.push_back(ccheck.getFormula()); |
746 |
28 |
std::shuffle(rasserts.begin(), rasserts.end(), Random::getRandom()); |
747 |
38 |
Node query = rasserts.size() == 1 ? rasserts[0] : nm->mkNode(AND, rasserts); |
748 |
130 |
for (const Node& a : rasserts) |
749 |
|
{ |
750 |
102 |
checkSol->assertFormula(a); |
751 |
|
} |
752 |
38 |
Result r = checkSol->checkSat(); |
753 |
28 |
Trace("sygus-ccore") << "----- check-sat returned " << r << std::endl; |
754 |
|
// In terms of Variant #2, this is the check "if (S ^ D) => B" |
755 |
28 |
if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) |
756 |
|
{ |
757 |
|
// it entails the postcondition, now get the unsat core |
758 |
|
// In terms of Variant #2, this is the line |
759 |
|
// "Let U be a subset of D such that S ^ U ^ ~B is unsat." |
760 |
|
// and uasserts is set to U. |
761 |
36 |
std::vector<Node> uasserts; |
762 |
36 |
std::unordered_set<Node> queryAsserts; |
763 |
18 |
queryAsserts.insert(ccheck.getFormula()); |
764 |
18 |
queryAsserts.insert(d_sc); |
765 |
18 |
bool hasQuery = getUnsatCore(*checkSol, queryAsserts, uasserts); |
766 |
|
// now, check the side condition |
767 |
18 |
bool falseCore = false; |
768 |
18 |
if (!d_sc.isNull()) |
769 |
|
{ |
770 |
18 |
if (!hasQuery) |
771 |
|
{ |
772 |
|
// Already know it trivially rewrites to false, don't need |
773 |
|
// to use unsat cores. |
774 |
4 |
falseCore = true; |
775 |
|
} |
776 |
|
else |
777 |
|
{ |
778 |
|
// In terms of Variant #2, this is the check "if S ^ U is unsat" |
779 |
14 |
Trace("sygus-ccore") << "----- Check side condition" << std::endl; |
780 |
28 |
std::unique_ptr<SmtEngine> checkSc; |
781 |
14 |
initializeSubsolver(checkSc); |
782 |
28 |
std::vector<Node> scasserts; |
783 |
14 |
scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end()); |
784 |
14 |
scasserts.push_back(d_sc); |
785 |
14 |
std::shuffle(scasserts.begin(), scasserts.end(), Random::getRandom()); |
786 |
51 |
for (const Node& sca : scasserts) |
787 |
|
{ |
788 |
37 |
checkSc->assertFormula(sca); |
789 |
|
} |
790 |
28 |
Result rsc = checkSc->checkSat(); |
791 |
28 |
Trace("sygus-ccore") |
792 |
14 |
<< "----- check-sat returned " << rsc << std::endl; |
793 |
14 |
if (rsc.asSatisfiabilityResult().isSat() == Result::UNSAT) |
794 |
|
{ |
795 |
|
// In terms of Variant #2, this is the line |
796 |
|
// "Let W be a subset of D such that S ^ W is unsat." |
797 |
|
// and uasserts is set to W. |
798 |
11 |
uasserts.clear(); |
799 |
22 |
std::unordered_set<Node> queryAsserts2; |
800 |
11 |
queryAsserts2.insert(d_sc); |
801 |
11 |
getUnsatCore(*checkSc, queryAsserts2, uasserts); |
802 |
11 |
falseCore = true; |
803 |
|
} |
804 |
|
} |
805 |
|
} |
806 |
|
|
807 |
18 |
if (!falseCore) |
808 |
|
{ |
809 |
|
// In terms of Variant #2, this is the line: |
810 |
|
// "return u_1 AND ... AND u_m where U = { u_1, ..., u_m }". |
811 |
3 |
Trace("sygus-ccore") << ">>> Solution : " << uasserts << std::endl; |
812 |
|
// We convert the builtin solution to a sygus datatype to |
813 |
|
// communicate with the sygus solver. |
814 |
6 |
Node sol = ccheck.getSygusSolution(uasserts); |
815 |
3 |
Trace("sygus-ccore-sy") << "Sygus solution : " << sol << std::endl; |
816 |
3 |
return sol; |
817 |
|
} |
818 |
|
else |
819 |
|
{ |
820 |
15 |
Assert(!uasserts.empty()); |
821 |
30 |
Node xu = uasserts[0]; |
822 |
30 |
Trace("sygus-ccore") |
823 |
15 |
<< "--- Add false core : " << uasserts << std::endl; |
824 |
|
// notice that a singleton false core could be removed from pool |
825 |
|
// in the case that (uasserts.size() == 1). |
826 |
15 |
std::sort(uasserts.begin(), uasserts.end()); |
827 |
|
// In terms of Variant #2, this is "cores(B) += W". |
828 |
15 |
ccheck.addFalseCore(query, uasserts); |
829 |
|
// remove and continue |
830 |
|
// In terms of Variant #2, this is "remove some d'' in W from D". |
831 |
|
std::vector<Node>::iterator ita = |
832 |
15 |
std::find(asserts.begin(), asserts.end(), xu); |
833 |
15 |
Assert(ita != asserts.end()); |
834 |
15 |
asserts.erase(ita); |
835 |
|
// Start over, since now we don't know which points are required to |
836 |
|
// falsify. |
837 |
15 |
return constructSolutionFromPool(ccheck, asserts, passerts); |
838 |
|
} |
839 |
|
} |
840 |
10 |
else if (r.asSatisfiabilityResult().isSat() == Result::SAT) |
841 |
|
{ |
842 |
|
// it does not entail the postcondition, add an assertion that blocks |
843 |
|
// the current point |
844 |
10 |
mvs.clear(); |
845 |
10 |
getModel(*checkSol, mvs); |
846 |
|
// should evaluate to true |
847 |
20 |
Node ean = evaluate(an, Node::null(), mvs); |
848 |
10 |
Assert(ean.isConst() && ean.getConst<bool>()); |
849 |
10 |
Trace("sygus-ccore") << "--- Add refinement point " << mvs << std::endl; |
850 |
|
// In terms of Variant #2, this is the line: |
851 |
|
// "pts(B) += { v } where { x -> v } is a model for D ^ ~B". |
852 |
10 |
ccheck.addRefinementPt(query, mvs); |
853 |
10 |
Trace("sygus-ccore-debug") << "...get new assertion..." << std::endl; |
854 |
|
// In terms of Variant #2, this rechecks the condition of the inner while |
855 |
|
// loop and attempts to add a new assertion to D. |
856 |
10 |
addSuccess = ccheck.addToAsserts(this, passerts, mvs, query, asserts, an); |
857 |
10 |
Trace("sygus-ccore-debug") << "...success is " << addSuccess << std::endl; |
858 |
|
} |
859 |
|
} while (addSuccess); |
860 |
4 |
return Node::null(); |
861 |
|
} |
862 |
|
|
863 |
|
} // namespace quantifiers |
864 |
|
} // namespace theory |
865 |
28194 |
} // namespace cvc5 |