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