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