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 |
1199 |
CegisCoreConnective::CegisCoreConnective(Env& env, |
72 |
|
QuantifiersState& qs, |
73 |
|
QuantifiersInferenceManager& qim, |
74 |
|
TermDbSygus* tds, |
75 |
1199 |
SynthConjecture* p) |
76 |
1199 |
: Cegis(env, qs, qim, tds, p) |
77 |
|
{ |
78 |
1199 |
d_true = NodeManager::currentNM()->mkConst(true); |
79 |
1199 |
d_false = NodeManager::currentNM()->mkConst(false); |
80 |
1199 |
} |
81 |
|
|
82 |
5 |
bool CegisCoreConnective::processInitialize(Node conj, |
83 |
|
Node n, |
84 |
|
const std::vector<Node>& candidates) |
85 |
|
{ |
86 |
5 |
Trace("sygus-ccore-init") << "CegisCoreConnective::initialize" << std::endl; |
87 |
5 |
Trace("sygus-ccore-init") << " conjecture : " << conj << std::endl; |
88 |
5 |
Trace("sygus-ccore-init") << " candidates : " << candidates << std::endl; |
89 |
5 |
if (candidates.size() != 1) |
90 |
|
{ |
91 |
|
Trace("sygus-ccore-init") |
92 |
|
<< "...only applies to single candidate conjectures." << std::endl; |
93 |
|
return false; |
94 |
|
} |
95 |
5 |
d_candidate = candidates[0]; |
96 |
5 |
Assert(conj.getKind() == FORALL); |
97 |
5 |
Assert(conj[0].getNumChildren() == 1); |
98 |
10 |
Node body = conj[1]; |
99 |
5 |
if (body.getKind() == NOT && body[0].getKind() == FORALL) |
100 |
|
{ |
101 |
4 |
body = body[0][1]; |
102 |
|
} |
103 |
|
else |
104 |
|
{ |
105 |
1 |
body = TermUtil::simpleNegate(body); |
106 |
|
} |
107 |
5 |
Trace("sygus-ccore-init") << " body : " << body << std::endl; |
108 |
|
|
109 |
10 |
TransitionInference ti; |
110 |
5 |
ti.process(body, conj[0][0]); |
111 |
|
|
112 |
5 |
if (!ti.isComplete()) |
113 |
|
{ |
114 |
|
Trace("sygus-ccore-init") << "...could not infer predicate." << std::endl; |
115 |
|
return false; |
116 |
|
} |
117 |
5 |
if (ti.isTrivial()) |
118 |
|
{ |
119 |
|
// not necessary to use this class if the conjecture is trivial (does |
120 |
|
// not contain the function-to-synthesize). |
121 |
1 |
Trace("sygus-ccore-init") << "...conjecture is trivial." << std::endl; |
122 |
1 |
return false; |
123 |
|
} |
124 |
8 |
Node trans = ti.getTransitionRelation(); |
125 |
4 |
Trace("sygus-ccore-init") << " transition relation: " << trans << std::endl; |
126 |
4 |
if (!trans.isConst() || trans.getConst<bool>()) |
127 |
|
{ |
128 |
|
Trace("sygus-ccore-init") |
129 |
|
<< "...does not apply conjectures with transition relations." |
130 |
|
<< std::endl; |
131 |
|
return false; |
132 |
|
} |
133 |
|
|
134 |
|
// the grammar must allow AND / OR when applicable |
135 |
8 |
TypeNode gt = d_candidate.getType(); |
136 |
|
|
137 |
8 |
Node f = ti.getFunction(); |
138 |
4 |
Assert(!f.isNull()); |
139 |
4 |
Trace("sygus-ccore-init") << " predicate: " << f << std::endl; |
140 |
4 |
ti.getVariables(d_vars); |
141 |
4 |
Trace("sygus-ccore-init") << " variables: " << d_vars << std::endl; |
142 |
|
// make the evaluation function |
143 |
8 |
std::vector<Node> echildren; |
144 |
4 |
echildren.push_back(d_candidate); |
145 |
4 |
echildren.insert(echildren.end(), d_vars.begin(), d_vars.end()); |
146 |
4 |
d_eterm = NodeManager::currentNM()->mkNode(DT_SYGUS_EVAL, echildren); |
147 |
4 |
Trace("sygus-ccore-init") << " evaluation term: " << d_eterm << std::endl; |
148 |
|
|
149 |
8 |
Node prePost[2]; |
150 |
4 |
prePost[0] = ti.getPreCondition(); |
151 |
|
// negate the post condition |
152 |
4 |
prePost[1] = TermUtil::simpleNegate(ti.getPostCondition()); |
153 |
4 |
Trace("sygus-ccore-init") << " precondition: " << prePost[0] << std::endl; |
154 |
4 |
Trace("sygus-ccore-init") << " postcondition: " << prePost[1] << std::endl; |
155 |
|
|
156 |
|
// side condition? |
157 |
8 |
QAttributes qa; |
158 |
4 |
QuantAttributes::computeQuantAttributes(conj, qa); |
159 |
8 |
Node sc = qa.d_sygusSideCondition; |
160 |
4 |
if (!sc.isNull()) |
161 |
|
{ |
162 |
4 |
Trace("sygus-ccore-init") << " side condition: " << sc << std::endl; |
163 |
4 |
if (sc.getKind() == EXISTS) |
164 |
|
{ |
165 |
4 |
sc = sc[1]; |
166 |
|
} |
167 |
8 |
Node scb = TermUtil::simpleNegate(sc); |
168 |
8 |
TransitionInference tisc; |
169 |
4 |
tisc.process(scb, conj[0][0]); |
170 |
8 |
Node scTrans = ti.getTransitionRelation(); |
171 |
8 |
Trace("sygus-ccore-init") |
172 |
4 |
<< " transition relation of SC: " << scTrans << std::endl; |
173 |
4 |
if (tisc.isComplete() && scTrans.isConst() && !scTrans.getConst<bool>()) |
174 |
|
{ |
175 |
8 |
std::vector<Node> scVars; |
176 |
4 |
tisc.getVariables(scVars); |
177 |
8 |
Node scPre = tisc.getPreCondition(); |
178 |
4 |
scPre = scPre.substitute( |
179 |
|
scVars.begin(), scVars.end(), d_vars.begin(), d_vars.end()); |
180 |
8 |
Node scPost = TermUtil::simpleNegate(tisc.getPostCondition()); |
181 |
4 |
scPost = scPost.substitute( |
182 |
|
scVars.begin(), scVars.end(), d_vars.begin(), d_vars.end()); |
183 |
8 |
Trace("sygus-ccore-init") |
184 |
4 |
<< " precondition of SC: " << scPre << std::endl; |
185 |
8 |
Trace("sygus-ccore-init") |
186 |
4 |
<< " postcondition of SC: " << scPost << std::endl; |
187 |
|
// We are extracting the side condition to be used by this algorithm |
188 |
|
// from the side condition ascribed to the synthesis conjecture. |
189 |
|
// A sygus conjecture of the form, for predicate-to-synthesize I: |
190 |
|
// exists I. forall x. P[I,x] |
191 |
|
// whose ascribed side condition is C[I], has the semantics: |
192 |
|
// exists I. C[I] ^ forall x. P[I,x]. |
193 |
|
// Notice that this side condition C may be an arbitrary formula over the |
194 |
|
// function to synthesize. However, the algorithm implemented by this |
195 |
|
// class is restricted to side conditions of the form: |
196 |
|
// exists k. A[k] ^ I(k) |
197 |
|
// The above condition guards for this case, and runs this block of code, |
198 |
|
// where we use the TransitionInference utility to extract A[k] from |
199 |
|
// A[k] ^ I(k). In the end, we set d_sc to A[d_vars]; notice the variables |
200 |
|
// d_vars are those introduced by the TransitionInference utility |
201 |
|
// for normalization. |
202 |
4 |
d_sc = scPost; |
203 |
|
} |
204 |
|
} |
205 |
|
|
206 |
|
// We use the postcondition if it non-trivial and the grammar gt for our |
207 |
|
// candidate has the production rule gt -> AND( gt, gt ). Similarly for |
208 |
|
// precondition and OR. |
209 |
4 |
Assert(gt.isDatatype()); |
210 |
4 |
const DType& gdt = gt.getDType(); |
211 |
4 |
SygusTypeInfo& gti = d_tds->getTypeInfo(gt); |
212 |
12 |
for (unsigned r = 0; r < 2; r++) |
213 |
|
{ |
214 |
12 |
Node node = prePost[r]; |
215 |
8 |
if (node.isConst()) |
216 |
|
{ |
217 |
|
// this direction is trivial, ignore |
218 |
4 |
continue; |
219 |
|
} |
220 |
4 |
Component& c = r == 0 ? d_pre : d_post; |
221 |
4 |
Kind rk = r == 0 ? OR : AND; |
222 |
4 |
int i = gti.getKindConsNum(rk); |
223 |
7 |
if (i != -1 && gdt[i].getNumArgs() == 2 |
224 |
7 |
&& gdt[i].getArgType(0) == gt |
225 |
7 |
&& gdt[i].getArgType(1) == gt) |
226 |
|
{ |
227 |
6 |
Trace("sygus-ccore-init") << " will do " << (r == 0 ? "pre" : "post") |
228 |
3 |
<< "condition." << std::endl; |
229 |
6 |
Node cons = gdt[i].getConstructor(); |
230 |
3 |
c.initialize(node, cons); |
231 |
|
// Register the symmetry breaking lemma: do not do top-level solutions |
232 |
|
// with this constructor (e.g. we want to enumerate literals, not |
233 |
|
// conjunctions). |
234 |
6 |
Node tst = datatypes::utils::mkTester(d_candidate, i, gdt); |
235 |
3 |
Trace("sygus-ccore-init") << "Sym break lemma " << tst << std::endl; |
236 |
3 |
d_qim.lemma(tst.negate(), |
237 |
|
InferenceId::QUANTIFIERS_SYGUS_CEGIS_UCL_SYM_BREAK); |
238 |
|
} |
239 |
|
} |
240 |
4 |
if (!isActive()) |
241 |
|
{ |
242 |
1 |
return false; |
243 |
|
} |
244 |
|
// initialize the enumerator |
245 |
3 |
return Cegis::processInitialize(conj, n, candidates); |
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 |
|
{ |
255 |
46 |
Assert(isActive()); |
256 |
46 |
bool ret = constructSolution(enums, enum_values, candidate_values); |
257 |
|
|
258 |
|
// exclude in the basic way if passive |
259 |
46 |
Assert(enums.size() == 1); |
260 |
46 |
NodeManager* nm = NodeManager::currentNM(); |
261 |
92 |
for (unsigned i = 0, esize = enums.size(); i < esize; i++) |
262 |
|
{ |
263 |
92 |
Node e = enums[i]; |
264 |
46 |
if (!d_tds->isPassiveEnumerator(e)) |
265 |
|
{ |
266 |
|
continue; |
267 |
|
} |
268 |
92 |
Node v = enum_values[i]; |
269 |
92 |
Node lem = d_tds->getExplain()->getExplanationForEquality(e, v).negate(); |
270 |
92 |
Node g = d_tds->getActiveGuardForEnumerator(e); |
271 |
46 |
if (!g.isNull()) |
272 |
|
{ |
273 |
|
lem = nm->mkNode(OR, g.negate(), lem); |
274 |
|
} |
275 |
46 |
d_qim.addPendingLemma(lem, |
276 |
|
InferenceId::QUANTIFIERS_SYGUS_CEGIS_UCL_EXCLUDE); |
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 = 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->evaluatePt(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->evaluatePt(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 |
103 |
for (UnsatCore::const_iterator i = uc.begin(); i != uc.end(); ++i) |
617 |
|
{ |
618 |
117 |
Node uassert = *i; |
619 |
74 |
Trace("sygus-ccore-debug") << " uc " << uassert << std::endl; |
620 |
105 |
if (queryAsserts.find(uassert) != queryAsserts.end()) |
621 |
|
{ |
622 |
31 |
hasQuery = true; |
623 |
31 |
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, options(), logicInfo()); |
634 |
|
Trace("sygus-ccore-debug") << "...got " << r << std::endl; |
635 |
|
return r; |
636 |
|
} |
637 |
|
|
638 |
908 |
Node CegisCoreConnective::evaluatePt(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 = evaluatePt(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 = evaluate(n, d_vars, mvs); |
670 |
129 |
Assert(!cn.isNull()); |
671 |
129 |
if (!id.isNull()) |
672 |
|
{ |
673 |
109 |
ec[id] = cn; |
674 |
|
} |
675 |
129 |
return cn; |
676 |
|
} |
677 |
|
|
678 |
61 |
Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, |
679 |
|
std::vector<Node>& asserts, |
680 |
|
std::vector<Node>& passerts) |
681 |
|
{ |
682 |
|
// In terms of Variant #2 from the header file, the set D is represented by |
683 |
|
// asserts. The available set of prediates pool(B) is represented by passerts. |
684 |
61 |
NodeManager* nm = NodeManager::currentNM(); |
685 |
61 |
Trace("sygus-ccore") << "------ Get initial candidate..." << std::endl; |
686 |
61 |
Node an = asserts.empty() |
687 |
|
? d_true |
688 |
122 |
: (asserts.size() == 1 ? asserts[0] : nm->mkNode(AND, asserts)); |
689 |
122 |
std::vector<Node> mvs; |
690 |
122 |
std::unordered_set<Node> visited; |
691 |
61 |
bool addSuccess = true; |
692 |
|
// Ensure that the current conjunction evaluates to false on all refinement |
693 |
|
// points. We get refinement points until we have exhausted. |
694 |
|
// In terms of Variant #2, this is inner while loop that adds points to D |
695 |
|
// while there exists a point in pts(B) such that D is true. |
696 |
122 |
Node mvId; |
697 |
26 |
do |
698 |
|
{ |
699 |
87 |
mvs.clear(); |
700 |
87 |
Trace("sygus-ccore-debug") << "...get refinement pt..." << std::endl; |
701 |
|
// In terms of Variant #2, this implements the line: |
702 |
|
// "D[v] is true for some v in pts(B)", |
703 |
|
// where v is stored in mvs. |
704 |
87 |
mvId = ccheck.getRefinementPt(this, an, visited, mvs); |
705 |
87 |
if (!mvId.isNull()) |
706 |
|
{ |
707 |
65 |
Trace("sygus-ccore-debug") << "...got " << mvs << std::endl; |
708 |
|
// In terms of Variant #2, this checks the conditions: |
709 |
|
// "d'[v] is false for some d' in pool(B)" and |
710 |
|
// "no element of cores(B) is a subset of D ++ { d' }" |
711 |
|
// and adds d' to D (asserts) if possible. |
712 |
65 |
addSuccess = ccheck.addToAsserts(this, passerts, mvs, mvId, asserts, an); |
713 |
130 |
Trace("sygus-ccore-debug") |
714 |
65 |
<< "...add success is " << addSuccess << std::endl; |
715 |
|
} |
716 |
|
else |
717 |
|
{ |
718 |
22 |
Trace("sygus-ccore-debug") << "...failed" << std::endl; |
719 |
|
} |
720 |
87 |
} while (!mvId.isNull() && addSuccess); |
721 |
61 |
if (!addSuccess) |
722 |
|
{ |
723 |
78 |
Trace("sygus-ccore") << ">>> Failed to generate initial candidate" |
724 |
39 |
<< std::endl; |
725 |
39 |
return Node::null(); |
726 |
|
} |
727 |
22 |
Trace("sygus-ccore") << "----- Initial candidate is " << an << std::endl; |
728 |
|
|
729 |
|
// We now have constructed an initial candidate for D. In terms of Variant #2, |
730 |
|
// we now enter the block code within "if D is false for all v in pts(B)". |
731 |
|
// Further refinements to D are made as the following do-while loop proceeds. |
732 |
10 |
do |
733 |
|
{ |
734 |
28 |
addSuccess = false; |
735 |
|
// try a new core |
736 |
38 |
std::unique_ptr<SmtEngine> checkSol; |
737 |
28 |
initializeSubsolver(checkSol, d_env); |
738 |
28 |
Trace("sygus-ccore") << "----- Check candidate " << an << std::endl; |
739 |
38 |
std::vector<Node> rasserts = asserts; |
740 |
28 |
rasserts.push_back(d_sc); |
741 |
28 |
rasserts.push_back(ccheck.getFormula()); |
742 |
28 |
std::shuffle(rasserts.begin(), rasserts.end(), Random::getRandom()); |
743 |
38 |
Node query = rasserts.size() == 1 ? rasserts[0] : nm->mkNode(AND, rasserts); |
744 |
130 |
for (const Node& a : rasserts) |
745 |
|
{ |
746 |
102 |
checkSol->assertFormula(a); |
747 |
|
} |
748 |
38 |
Result r = checkSol->checkSat(); |
749 |
28 |
Trace("sygus-ccore") << "----- check-sat returned " << r << std::endl; |
750 |
|
// In terms of Variant #2, this is the check "if (S ^ D) => B" |
751 |
28 |
if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) |
752 |
|
{ |
753 |
|
// it entails the postcondition, now get the unsat core |
754 |
|
// In terms of Variant #2, this is the line |
755 |
|
// "Let U be a subset of D such that S ^ U ^ ~B is unsat." |
756 |
|
// and uasserts is set to U. |
757 |
36 |
std::vector<Node> uasserts; |
758 |
36 |
std::unordered_set<Node> queryAsserts; |
759 |
18 |
queryAsserts.insert(ccheck.getFormula()); |
760 |
18 |
queryAsserts.insert(d_sc); |
761 |
18 |
bool hasQuery = getUnsatCore(*checkSol, queryAsserts, uasserts); |
762 |
|
// now, check the side condition |
763 |
18 |
bool falseCore = false; |
764 |
18 |
if (!d_sc.isNull()) |
765 |
|
{ |
766 |
18 |
if (!hasQuery) |
767 |
|
{ |
768 |
|
// Already know it trivially rewrites to false, don't need |
769 |
|
// to use unsat cores. |
770 |
4 |
falseCore = true; |
771 |
|
} |
772 |
|
else |
773 |
|
{ |
774 |
|
// In terms of Variant #2, this is the check "if S ^ U is unsat" |
775 |
14 |
Trace("sygus-ccore") << "----- Check side condition" << std::endl; |
776 |
28 |
std::unique_ptr<SmtEngine> checkSc; |
777 |
14 |
initializeSubsolver(checkSc, d_env); |
778 |
28 |
std::vector<Node> scasserts; |
779 |
14 |
scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end()); |
780 |
14 |
scasserts.push_back(d_sc); |
781 |
14 |
std::shuffle(scasserts.begin(), scasserts.end(), Random::getRandom()); |
782 |
51 |
for (const Node& sca : scasserts) |
783 |
|
{ |
784 |
37 |
checkSc->assertFormula(sca); |
785 |
|
} |
786 |
28 |
Result rsc = checkSc->checkSat(); |
787 |
28 |
Trace("sygus-ccore") |
788 |
14 |
<< "----- check-sat returned " << rsc << std::endl; |
789 |
14 |
if (rsc.asSatisfiabilityResult().isSat() == Result::UNSAT) |
790 |
|
{ |
791 |
|
// In terms of Variant #2, this is the line |
792 |
|
// "Let W be a subset of D such that S ^ W is unsat." |
793 |
|
// and uasserts is set to W. |
794 |
11 |
uasserts.clear(); |
795 |
22 |
std::unordered_set<Node> queryAsserts2; |
796 |
11 |
queryAsserts2.insert(d_sc); |
797 |
11 |
getUnsatCore(*checkSc, queryAsserts2, uasserts); |
798 |
11 |
falseCore = true; |
799 |
|
} |
800 |
|
} |
801 |
|
} |
802 |
|
|
803 |
18 |
if (!falseCore) |
804 |
|
{ |
805 |
|
// In terms of Variant #2, this is the line: |
806 |
|
// "return u_1 AND ... AND u_m where U = { u_1, ..., u_m }". |
807 |
3 |
Trace("sygus-ccore") << ">>> Solution : " << uasserts << std::endl; |
808 |
|
// We convert the builtin solution to a sygus datatype to |
809 |
|
// communicate with the sygus solver. |
810 |
6 |
Node sol = ccheck.getSygusSolution(uasserts); |
811 |
3 |
Trace("sygus-ccore-sy") << "Sygus solution : " << sol << std::endl; |
812 |
3 |
return sol; |
813 |
|
} |
814 |
|
else |
815 |
|
{ |
816 |
15 |
Assert(!uasserts.empty()); |
817 |
30 |
Node xu = uasserts[0]; |
818 |
30 |
Trace("sygus-ccore") |
819 |
15 |
<< "--- Add false core : " << uasserts << std::endl; |
820 |
|
// notice that a singleton false core could be removed from pool |
821 |
|
// in the case that (uasserts.size() == 1). |
822 |
15 |
std::sort(uasserts.begin(), uasserts.end()); |
823 |
|
// In terms of Variant #2, this is "cores(B) += W". |
824 |
15 |
ccheck.addFalseCore(query, uasserts); |
825 |
|
// remove and continue |
826 |
|
// In terms of Variant #2, this is "remove some d'' in W from D". |
827 |
|
std::vector<Node>::iterator ita = |
828 |
15 |
std::find(asserts.begin(), asserts.end(), xu); |
829 |
15 |
Assert(ita != asserts.end()); |
830 |
15 |
asserts.erase(ita); |
831 |
|
// Start over, since now we don't know which points are required to |
832 |
|
// falsify. |
833 |
15 |
return constructSolutionFromPool(ccheck, asserts, passerts); |
834 |
|
} |
835 |
|
} |
836 |
10 |
else if (r.asSatisfiabilityResult().isSat() == Result::SAT) |
837 |
|
{ |
838 |
|
// it does not entail the postcondition, add an assertion that blocks |
839 |
|
// the current point |
840 |
10 |
mvs.clear(); |
841 |
10 |
getModel(*checkSol, mvs); |
842 |
|
// should evaluate to true |
843 |
20 |
Node ean = evaluatePt(an, Node::null(), mvs); |
844 |
10 |
Assert(ean.isConst() && ean.getConst<bool>()); |
845 |
10 |
Trace("sygus-ccore") << "--- Add refinement point " << mvs << std::endl; |
846 |
|
// In terms of Variant #2, this is the line: |
847 |
|
// "pts(B) += { v } where { x -> v } is a model for D ^ ~B". |
848 |
10 |
ccheck.addRefinementPt(query, mvs); |
849 |
10 |
Trace("sygus-ccore-debug") << "...get new assertion..." << std::endl; |
850 |
|
// In terms of Variant #2, this rechecks the condition of the inner while |
851 |
|
// loop and attempts to add a new assertion to D. |
852 |
10 |
addSuccess = ccheck.addToAsserts(this, passerts, mvs, query, asserts, an); |
853 |
10 |
Trace("sygus-ccore-debug") << "...success is " << addSuccess << std::endl; |
854 |
|
} |
855 |
|
} while (addSuccess); |
856 |
4 |
return Node::null(); |
857 |
|
} |
858 |
|
|
859 |
|
} // namespace quantifiers |
860 |
|
} // namespace theory |
861 |
22755 |
} // namespace cvc5 |