1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Mathias Preiner, Haniel Barbosa |
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 class that encapsulates techniques for a single |
14 |
|
* (SyGuS) synthesis conjecture. |
15 |
|
*/ |
16 |
|
#include "theory/quantifiers/sygus/synth_conjecture.h" |
17 |
|
|
18 |
|
#include "base/configuration.h" |
19 |
|
#include "expr/skolem_manager.h" |
20 |
|
#include "options/base_options.h" |
21 |
|
#include "options/datatypes_options.h" |
22 |
|
#include "options/quantifiers_options.h" |
23 |
|
#include "printer/printer.h" |
24 |
|
#include "smt/logic_exception.h" |
25 |
|
#include "smt/smt_engine_scope.h" |
26 |
|
#include "smt/smt_statistics_registry.h" |
27 |
|
#include "theory/datatypes/sygus_datatype_utils.h" |
28 |
|
#include "theory/quantifiers/first_order_model.h" |
29 |
|
#include "theory/quantifiers/instantiate.h" |
30 |
|
#include "theory/quantifiers/quantifiers_attributes.h" |
31 |
|
#include "theory/quantifiers/sygus/enum_stream_substitution.h" |
32 |
|
#include "theory/quantifiers/sygus/sygus_enumerator.h" |
33 |
|
#include "theory/quantifiers/sygus/sygus_enumerator_basic.h" |
34 |
|
#include "theory/quantifiers/sygus/sygus_grammar_cons.h" |
35 |
|
#include "theory/quantifiers/sygus/sygus_pbe.h" |
36 |
|
#include "theory/quantifiers/sygus/synth_engine.h" |
37 |
|
#include "theory/quantifiers/sygus/term_database_sygus.h" |
38 |
|
#include "theory/quantifiers/term_util.h" |
39 |
|
#include "theory/rewriter.h" |
40 |
|
#include "theory/smt_engine_subsolver.h" |
41 |
|
|
42 |
|
using namespace cvc5::kind; |
43 |
|
using namespace std; |
44 |
|
|
45 |
|
namespace cvc5 { |
46 |
|
namespace theory { |
47 |
|
namespace quantifiers { |
48 |
|
|
49 |
1529 |
SynthConjecture::SynthConjecture(QuantifiersState& qs, |
50 |
|
QuantifiersInferenceManager& qim, |
51 |
|
QuantifiersRegistry& qr, |
52 |
|
TermRegistry& tr, |
53 |
1529 |
SygusStatistics& s) |
54 |
|
: d_qstate(qs), |
55 |
|
d_qim(qim), |
56 |
|
d_qreg(qr), |
57 |
|
d_treg(tr), |
58 |
|
d_stats(s), |
59 |
1529 |
d_tds(tr.getTermDatabaseSygus()), |
60 |
|
d_hasSolution(false), |
61 |
1529 |
d_ceg_si(new CegSingleInv(tr, s)), |
62 |
1529 |
d_templInfer(new SygusTemplateInfer), |
63 |
1529 |
d_ceg_proc(new SynthConjectureProcess), |
64 |
1529 |
d_ceg_gc(new CegGrammarConstructor(d_tds, this)), |
65 |
1529 |
d_sygus_rconst(new SygusRepairConst(d_tds)), |
66 |
1529 |
d_exampleInfer(new ExampleInfer(d_tds)), |
67 |
1529 |
d_ceg_pbe(new SygusPbe(qim, d_tds, this)), |
68 |
1529 |
d_ceg_cegis(new Cegis(qim, d_tds, this)), |
69 |
1529 |
d_ceg_cegisUnif(new CegisUnif(qs, qim, d_tds, this)), |
70 |
1529 |
d_sygus_ccore(new CegisCoreConnective(qim, d_tds, this)), |
71 |
|
d_master(nullptr), |
72 |
|
d_set_ce_sk_vars(false), |
73 |
|
d_repair_index(0), |
74 |
|
d_refine_count(0), |
75 |
18348 |
d_guarded_stream_exc(false) |
76 |
|
{ |
77 |
1529 |
if (options::sygusSymBreakPbe() || options::sygusUnifPbe()) |
78 |
|
{ |
79 |
1529 |
d_modules.push_back(d_ceg_pbe.get()); |
80 |
|
} |
81 |
1529 |
if (options::sygusUnifPi() != options::SygusUnifPiMode::NONE) |
82 |
|
{ |
83 |
32 |
d_modules.push_back(d_ceg_cegisUnif.get()); |
84 |
|
} |
85 |
1529 |
if (options::sygusCoreConnective()) |
86 |
|
{ |
87 |
72 |
d_modules.push_back(d_sygus_ccore.get()); |
88 |
|
} |
89 |
1529 |
d_modules.push_back(d_ceg_cegis.get()); |
90 |
1529 |
} |
91 |
|
|
92 |
1529 |
SynthConjecture::~SynthConjecture() {} |
93 |
|
|
94 |
1505 |
void SynthConjecture::presolve() |
95 |
|
{ |
96 |
|
// we don't have a solution yet |
97 |
1505 |
d_hasSolution = false; |
98 |
1505 |
} |
99 |
|
|
100 |
325 |
void SynthConjecture::assign(Node q) |
101 |
|
{ |
102 |
325 |
Assert(d_embed_quant.isNull()); |
103 |
325 |
Assert(q.getKind() == FORALL); |
104 |
325 |
Trace("cegqi") << "SynthConjecture : assign : " << q << std::endl; |
105 |
325 |
d_quant = q; |
106 |
325 |
NodeManager* nm = NodeManager::currentNM(); |
107 |
325 |
SkolemManager* sm = nm->getSkolemManager(); |
108 |
|
|
109 |
|
// initialize the guard |
110 |
325 |
d_feasible_guard = sm->mkDummySkolem("G", nm->booleanType()); |
111 |
325 |
d_feasible_guard = Rewriter::rewrite(d_feasible_guard); |
112 |
325 |
d_feasible_guard = d_qstate.getValuation().ensureLiteral(d_feasible_guard); |
113 |
325 |
AlwaysAssert(!d_feasible_guard.isNull()); |
114 |
|
|
115 |
|
// pre-simplify the quantified formula based on the process utility |
116 |
325 |
d_simp_quant = d_ceg_proc->preSimplify(d_quant); |
117 |
|
|
118 |
|
// compute its attributes |
119 |
648 |
QAttributes qa; |
120 |
325 |
QuantAttributes::computeQuantAttributes(q, qa); |
121 |
|
|
122 |
648 |
std::map<Node, Node> templates; |
123 |
648 |
std::map<Node, Node> templates_arg; |
124 |
|
// register with single invocation if applicable |
125 |
325 |
if (qa.d_sygus) |
126 |
|
{ |
127 |
325 |
d_ceg_si->initialize(d_simp_quant); |
128 |
325 |
d_simp_quant = d_ceg_si->getSimplifiedConjecture(); |
129 |
325 |
if (!d_ceg_si->isSingleInvocation()) |
130 |
|
{ |
131 |
325 |
d_templInfer->initialize(d_simp_quant); |
132 |
|
} |
133 |
|
// carry the templates |
134 |
824 |
for (const Node& v : q[0]) |
135 |
|
{ |
136 |
998 |
Node templ = d_templInfer->getTemplate(v); |
137 |
499 |
if (!templ.isNull()) |
138 |
|
{ |
139 |
29 |
templates[v] = templ; |
140 |
29 |
templates_arg[v] = d_templInfer->getTemplateArg(v); |
141 |
|
} |
142 |
|
} |
143 |
|
} |
144 |
|
|
145 |
|
// post-simplify the quantified formula based on the process utility |
146 |
325 |
d_simp_quant = d_ceg_proc->postSimplify(d_simp_quant); |
147 |
|
|
148 |
|
// finished simplifying the quantified formula at this point |
149 |
|
|
150 |
|
// convert to deep embedding and finalize single invocation here |
151 |
325 |
d_embed_quant = d_ceg_gc->process(d_simp_quant, templates, templates_arg); |
152 |
650 |
Trace("cegqi") << "SynthConjecture : converted to embedding : " |
153 |
325 |
<< d_embed_quant << std::endl; |
154 |
|
|
155 |
648 |
Node sc = qa.d_sygusSideCondition; |
156 |
325 |
if (!sc.isNull()) |
157 |
|
{ |
158 |
|
// convert to deep embedding |
159 |
15 |
d_embedSideCondition = d_ceg_gc->convertToEmbedding(sc); |
160 |
30 |
Trace("cegqi") << "SynthConjecture : side condition : " |
161 |
15 |
<< d_embedSideCondition << std::endl; |
162 |
|
} |
163 |
|
|
164 |
|
// we now finalize the single invocation module, based on the syntax |
165 |
|
// restrictions |
166 |
325 |
if (qa.d_sygus) |
167 |
|
{ |
168 |
325 |
d_ceg_si->finishInit(d_ceg_gc->isSyntaxRestricted()); |
169 |
|
} |
170 |
|
|
171 |
325 |
Assert(d_candidates.empty()); |
172 |
648 |
std::vector<Node> vars; |
173 |
824 |
for (unsigned i = 0; i < d_embed_quant[0].getNumChildren(); i++) |
174 |
|
{ |
175 |
499 |
vars.push_back(d_embed_quant[0][i]); |
176 |
998 |
Node e = sm->mkDummySkolem("e", d_embed_quant[0][i].getType()); |
177 |
499 |
d_candidates.push_back(e); |
178 |
|
} |
179 |
650 |
Trace("cegqi") << "Base quantified formula is : " << d_embed_quant |
180 |
325 |
<< std::endl; |
181 |
|
// construct base instantiation |
182 |
650 |
d_base_inst = Rewriter::rewrite(d_qim.getInstantiate()->getInstantiation( |
183 |
325 |
d_embed_quant, vars, d_candidates)); |
184 |
325 |
if (!d_embedSideCondition.isNull() && !vars.empty()) |
185 |
|
{ |
186 |
30 |
d_embedSideCondition = d_embedSideCondition.substitute( |
187 |
15 |
vars.begin(), vars.end(), d_candidates.begin(), d_candidates.end()); |
188 |
|
} |
189 |
325 |
Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl; |
190 |
|
|
191 |
|
// initialize the sygus constant repair utility |
192 |
325 |
if (options::sygusRepairConst()) |
193 |
|
{ |
194 |
8 |
d_sygus_rconst->initialize(d_base_inst.negate(), d_candidates); |
195 |
16 |
if (options::sygusConstRepairAbort()) |
196 |
|
{ |
197 |
|
if (!d_sygus_rconst->isActive()) |
198 |
|
{ |
199 |
|
// no constant repair is possible: abort |
200 |
|
std::stringstream ss; |
201 |
|
ss << "Grammar does not allow repair constants." << std::endl; |
202 |
|
throw LogicException(ss.str()); |
203 |
|
} |
204 |
|
} |
205 |
|
} |
206 |
|
// initialize the example inference utility |
207 |
325 |
if (!d_exampleInfer->initialize(d_base_inst, d_candidates)) |
208 |
|
{ |
209 |
|
// there is a contradictory example pair, the conjecture is infeasible. |
210 |
4 |
Node infLem = d_feasible_guard.negate(); |
211 |
2 |
d_qim.lemma(infLem, InferenceId::QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA); |
212 |
|
// we don't need to continue initialization in this case |
213 |
2 |
return; |
214 |
|
} |
215 |
|
|
216 |
|
// register this term with sygus database and other utilities that impact |
217 |
|
// the enumerative sygus search |
218 |
646 |
std::vector<Node> guarded_lemmas; |
219 |
323 |
if (!isSingleInvocation()) |
220 |
|
{ |
221 |
233 |
d_ceg_proc->initialize(d_base_inst, d_candidates); |
222 |
424 |
for (unsigned i = 0, size = d_modules.size(); i < size; i++) |
223 |
|
{ |
224 |
848 |
if (d_modules[i]->initialize( |
225 |
424 |
d_simp_quant, d_base_inst, d_candidates, guarded_lemmas)) |
226 |
|
{ |
227 |
233 |
d_master = d_modules[i]; |
228 |
233 |
break; |
229 |
|
} |
230 |
|
} |
231 |
233 |
Assert(d_master != nullptr); |
232 |
|
} |
233 |
|
|
234 |
323 |
Assert(d_qreg.getQuantAttributes().isSygus(q)); |
235 |
|
// if the base instantiation is an existential, store its variables |
236 |
323 |
if (d_base_inst.getKind() == NOT && d_base_inst[0].getKind() == FORALL) |
237 |
|
{ |
238 |
852 |
for (const Node& v : d_base_inst[0][0]) |
239 |
|
{ |
240 |
671 |
d_inner_vars.push_back(v); |
241 |
|
} |
242 |
|
} |
243 |
|
|
244 |
|
// register the strategy |
245 |
969 |
d_feasible_strategy.reset( |
246 |
|
new DecisionStrategySingleton("sygus_feasible", |
247 |
|
d_feasible_guard, |
248 |
323 |
d_qstate.getSatContext(), |
249 |
646 |
d_qstate.getValuation())); |
250 |
323 |
d_qim.getDecisionManager()->registerStrategy( |
251 |
|
DecisionManager::STRAT_QUANT_SYGUS_FEASIBLE, d_feasible_strategy.get()); |
252 |
|
// this must be called, both to ensure that the feasible guard is |
253 |
|
// decided on with true polariy, but also to ensure that output channel |
254 |
|
// has been used on this call to check. |
255 |
323 |
d_qim.requirePhase(d_feasible_guard, true); |
256 |
|
|
257 |
646 |
Node gneg = d_feasible_guard.negate(); |
258 |
326 |
for (unsigned i = 0; i < guarded_lemmas.size(); i++) |
259 |
|
{ |
260 |
6 |
Node lem = nm->mkNode(OR, gneg, guarded_lemmas[i]); |
261 |
6 |
Trace("cegqi-lemma") << "Cegqi::Lemma : initial (guarded) lemma : " << lem |
262 |
3 |
<< std::endl; |
263 |
3 |
d_qim.lemma(lem, InferenceId::UNKNOWN); |
264 |
|
} |
265 |
|
|
266 |
646 |
Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation() |
267 |
323 |
<< std::endl; |
268 |
|
} |
269 |
|
|
270 |
3879 |
Node SynthConjecture::getGuard() const { return d_feasible_guard; } |
271 |
|
|
272 |
40946 |
bool SynthConjecture::isSingleInvocation() const |
273 |
|
{ |
274 |
40946 |
return d_ceg_si->isSingleInvocation(); |
275 |
|
} |
276 |
|
|
277 |
4585 |
bool SynthConjecture::needsCheck() |
278 |
|
{ |
279 |
|
bool value; |
280 |
4585 |
Assert(!d_feasible_guard.isNull()); |
281 |
|
// non or fully single invocation : look at guard only |
282 |
4585 |
if (d_qstate.getValuation().hasSatValue(d_feasible_guard, value)) |
283 |
|
{ |
284 |
4585 |
if (!value) |
285 |
|
{ |
286 |
8 |
Trace("sygus-engine-debug") << "Conjecture is infeasible." << std::endl; |
287 |
8 |
Warning() << "Warning : the SyGuS conjecture may be infeasible" |
288 |
|
<< std::endl; |
289 |
8 |
return false; |
290 |
|
} |
291 |
|
else |
292 |
|
{ |
293 |
9154 |
Trace("sygus-engine-debug") << "Feasible guard " << d_feasible_guard |
294 |
4577 |
<< " assigned true." << std::endl; |
295 |
|
} |
296 |
|
} |
297 |
|
else |
298 |
|
{ |
299 |
|
Trace("cegqi-warn") << "WARNING: Guard " << d_feasible_guard |
300 |
|
<< " is not assigned!" << std::endl; |
301 |
|
Assert(false); |
302 |
|
} |
303 |
4577 |
return true; |
304 |
|
} |
305 |
|
|
306 |
109824 |
bool SynthConjecture::needsRefinement() const { return d_set_ce_sk_vars; } |
307 |
38857 |
bool SynthConjecture::doCheck(std::vector<Node>& lems) |
308 |
|
{ |
309 |
38857 |
if (isSingleInvocation()) |
310 |
|
{ |
311 |
|
// We now try to solve with the single invocation solver, which may or may |
312 |
|
// not succeed in solving the conjecture. In either case, we are done and |
313 |
|
// return true. |
314 |
80 |
if (d_ceg_si->solve()) |
315 |
|
{ |
316 |
72 |
d_hasSolution = true; |
317 |
|
// the conjecture has a solution, so its negation holds |
318 |
72 |
lems.push_back(d_quant.negate()); |
319 |
|
} |
320 |
80 |
return true; |
321 |
|
} |
322 |
38777 |
Assert(d_master != nullptr); |
323 |
38777 |
Assert(!d_hasSolution); |
324 |
|
|
325 |
|
// get the list of terms that the master strategy is interested in |
326 |
77554 |
std::vector<Node> terms; |
327 |
38777 |
d_master->getTermList(d_candidates, terms); |
328 |
|
|
329 |
38777 |
Assert(!d_candidates.empty()); |
330 |
|
|
331 |
77554 |
Trace("cegqi-check") << "CegConjuncture : check, build candidates..." |
332 |
38777 |
<< std::endl; |
333 |
77554 |
std::vector<Node> candidate_values; |
334 |
38777 |
bool constructed_cand = false; |
335 |
|
|
336 |
|
// If a module is not trying to repair constants in solutions and the option |
337 |
|
// sygusRepairConst is true, we use a default scheme for trying to repair |
338 |
|
// constants here. |
339 |
|
bool doRepairConst = |
340 |
38777 |
options::sygusRepairConst() && !d_master->usingRepairConst(); |
341 |
38777 |
if (doRepairConst) |
342 |
|
{ |
343 |
|
// have we tried to repair the previous solution? |
344 |
|
// if not, call the repair constant utility |
345 |
|
unsigned ninst = d_cinfo[d_candidates[0]].d_inst.size(); |
346 |
|
if (d_repair_index < ninst) |
347 |
|
{ |
348 |
|
std::vector<Node> fail_cvs; |
349 |
|
for (const Node& cprog : d_candidates) |
350 |
|
{ |
351 |
|
Assert(d_repair_index < d_cinfo[cprog].d_inst.size()); |
352 |
|
fail_cvs.push_back(d_cinfo[cprog].d_inst[d_repair_index]); |
353 |
|
} |
354 |
|
if (Trace.isOn("sygus-engine")) |
355 |
|
{ |
356 |
|
Trace("sygus-engine") << "CegConjuncture : repair previous solution "; |
357 |
|
for (const Node& fc : fail_cvs) |
358 |
|
{ |
359 |
|
std::stringstream ss; |
360 |
|
TermDbSygus::toStreamSygus(ss, fc); |
361 |
|
Trace("sygus-engine") << ss.str() << " "; |
362 |
|
} |
363 |
|
Trace("sygus-engine") << std::endl; |
364 |
|
} |
365 |
|
d_repair_index++; |
366 |
|
if (d_sygus_rconst->repairSolution( |
367 |
|
d_candidates, fail_cvs, candidate_values, true)) |
368 |
|
{ |
369 |
|
constructed_cand = true; |
370 |
|
} |
371 |
|
} |
372 |
|
} |
373 |
|
|
374 |
77555 |
bool printDebug = options::debugSygus(); |
375 |
38777 |
if (!constructed_cand) |
376 |
|
{ |
377 |
|
// get the model value of the relevant terms from the master module |
378 |
55304 |
std::vector<Node> enum_values; |
379 |
38777 |
bool activeIncomplete = false; |
380 |
38777 |
bool fullModel = getEnumeratedValues(terms, enum_values, activeIncomplete); |
381 |
|
|
382 |
|
// if the master requires a full model and the model is partial, we fail |
383 |
38768 |
if (!d_master->allowPartialModel() && !fullModel) |
384 |
|
{ |
385 |
|
// we retain the values in d_ev_active_gen_waiting |
386 |
19017 |
Trace("sygus-engine-debug") << "...partial model, fail." << std::endl; |
387 |
|
// if we are partial due to an active enumerator, we may still succeed |
388 |
|
// on the next call |
389 |
19017 |
return !activeIncomplete; |
390 |
|
} |
391 |
|
// the waiting values are passed to the module below, clear |
392 |
19751 |
d_ev_active_gen_waiting.clear(); |
393 |
|
|
394 |
19751 |
Assert(terms.size() == enum_values.size()); |
395 |
19751 |
bool emptyModel = true; |
396 |
42695 |
for (unsigned i = 0, size = terms.size(); i < size; i++) |
397 |
|
{ |
398 |
22944 |
if (!enum_values[i].isNull()) |
399 |
|
{ |
400 |
19283 |
emptyModel = false; |
401 |
|
} |
402 |
|
} |
403 |
19751 |
if (emptyModel) |
404 |
|
{ |
405 |
3233 |
Trace("sygus-engine-debug") << "...empty model, fail." << std::endl; |
406 |
3233 |
return !activeIncomplete; |
407 |
|
} |
408 |
|
// Must separately compute whether trace is on due to compilation of |
409 |
|
// Trace.isOn. |
410 |
16518 |
bool traceIsOn = Trace.isOn("sygus-engine"); |
411 |
16518 |
if (printDebug || traceIsOn) |
412 |
|
{ |
413 |
2 |
Trace("sygus-engine") << " * Value is : "; |
414 |
4 |
std::stringstream sygusEnumOut; |
415 |
2 |
FirstOrderModel* m = d_treg.getModel(); |
416 |
4 |
for (unsigned i = 0, size = terms.size(); i < size; i++) |
417 |
|
{ |
418 |
4 |
Node nv = enum_values[i]; |
419 |
4 |
Node onv = nv.isNull() ? m->getValue(terms[i]) : nv; |
420 |
4 |
TypeNode tn = onv.getType(); |
421 |
4 |
std::stringstream ss; |
422 |
2 |
TermDbSygus::toStreamSygus(ss, onv); |
423 |
2 |
if (printDebug) |
424 |
|
{ |
425 |
2 |
sygusEnumOut << " " << ss.str(); |
426 |
|
} |
427 |
2 |
Trace("sygus-engine") << terms[i] << " -> "; |
428 |
2 |
if (nv.isNull()) |
429 |
|
{ |
430 |
|
Trace("sygus-engine") << "[EXC: " << ss.str() << "] "; |
431 |
|
} |
432 |
|
else |
433 |
|
{ |
434 |
2 |
Trace("sygus-engine") << ss.str() << " "; |
435 |
2 |
if (Trace.isOn("sygus-engine-rr")) |
436 |
|
{ |
437 |
|
Node bv = d_tds->sygusToBuiltin(nv, tn); |
438 |
|
bv = Rewriter::rewrite(bv); |
439 |
|
Trace("sygus-engine-rr") << " -> " << bv << std::endl; |
440 |
|
} |
441 |
|
} |
442 |
|
} |
443 |
2 |
Trace("sygus-engine") << std::endl; |
444 |
2 |
if (printDebug) |
445 |
|
{ |
446 |
2 |
Options& sopts = smt::currentSmtEngine()->getOptions(); |
447 |
2 |
std::ostream& out = *sopts.getOut(); |
448 |
2 |
out << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl; |
449 |
|
} |
450 |
|
} |
451 |
16518 |
Assert(candidate_values.empty()); |
452 |
33036 |
constructed_cand = d_master->constructCandidates( |
453 |
16518 |
terms, enum_values, d_candidates, candidate_values, lems); |
454 |
|
// now clear the evaluation caches |
455 |
18707 |
for (std::pair<const Node, std::unique_ptr<ExampleEvalCache> >& ecp : |
456 |
16518 |
d_exampleEvalCache) |
457 |
|
{ |
458 |
18707 |
ExampleEvalCache* eec = ecp.second.get(); |
459 |
18707 |
if (eec != nullptr) |
460 |
|
{ |
461 |
3357 |
eec->clearEvaluationAll(); |
462 |
|
} |
463 |
|
} |
464 |
|
} |
465 |
|
|
466 |
16518 |
NodeManager* nm = NodeManager::currentNM(); |
467 |
16518 |
SkolemManager* sm = nm->getSkolemManager(); |
468 |
|
|
469 |
|
// check the side condition if we constructed a candidate |
470 |
16518 |
if (constructed_cand) |
471 |
|
{ |
472 |
1750 |
if (!checkSideCondition(candidate_values)) |
473 |
|
{ |
474 |
70 |
excludeCurrentSolution(terms, candidate_values); |
475 |
70 |
Trace("sygus-engine") << "...failed side condition" << std::endl; |
476 |
70 |
return false; |
477 |
|
} |
478 |
|
} |
479 |
|
|
480 |
|
// must get a counterexample to the value of the current candidate |
481 |
32896 |
Node inst; |
482 |
16448 |
if (constructed_cand) |
483 |
|
{ |
484 |
1680 |
if (Trace.isOn("cegqi-check")) |
485 |
|
{ |
486 |
|
Trace("cegqi-check") << "CegConjuncture : check candidate : " |
487 |
|
<< std::endl; |
488 |
|
for (unsigned i = 0, size = candidate_values.size(); i < size; i++) |
489 |
|
{ |
490 |
|
Trace("cegqi-check") << " " << i << " : " << d_candidates[i] << " -> " |
491 |
|
<< candidate_values[i] << std::endl; |
492 |
|
} |
493 |
|
} |
494 |
1680 |
Assert(candidate_values.size() == d_candidates.size()); |
495 |
1680 |
inst = d_base_inst.substitute(d_candidates.begin(), |
496 |
|
d_candidates.end(), |
497 |
|
candidate_values.begin(), |
498 |
|
candidate_values.end()); |
499 |
|
} |
500 |
|
else |
501 |
|
{ |
502 |
14768 |
inst = d_base_inst; |
503 |
|
} |
504 |
|
|
505 |
16448 |
if (!constructed_cand) |
506 |
|
{ |
507 |
14768 |
return false; |
508 |
|
} |
509 |
|
|
510 |
|
// if we trust the sampling we ran, we terminate now |
511 |
1680 |
if (options::cegisSample() == options::CegisSampleMode::TRUST) |
512 |
|
{ |
513 |
|
// we have that the current candidate passed a sample test |
514 |
|
// since we trust sampling in this mode, we assert there is no |
515 |
|
// counterexample to the conjecture here. |
516 |
1 |
lems.push_back(d_quant.negate()); |
517 |
1 |
recordSolution(candidate_values); |
518 |
1 |
return true; |
519 |
|
} |
520 |
1679 |
Assert(!d_set_ce_sk_vars); |
521 |
|
|
522 |
|
// immediately skolemize inner existentials |
523 |
3358 |
Node query; |
524 |
|
// introduce the skolem variables |
525 |
3358 |
std::vector<Node> sks; |
526 |
3358 |
std::vector<Node> vars; |
527 |
1679 |
if (constructed_cand) |
528 |
|
{ |
529 |
1679 |
if (printDebug) |
530 |
|
{ |
531 |
2 |
Options& sopts = smt::currentSmtEngine()->getOptions(); |
532 |
2 |
std::ostream& out = *sopts.getOut(); |
533 |
2 |
out << "(sygus-candidate "; |
534 |
2 |
Assert(d_quant[0].getNumChildren() == candidate_values.size()); |
535 |
4 |
for (unsigned i = 0, ncands = candidate_values.size(); i < ncands; i++) |
536 |
|
{ |
537 |
4 |
Node v = candidate_values[i]; |
538 |
4 |
std::stringstream ss; |
539 |
2 |
TermDbSygus::toStreamSygus(ss, v); |
540 |
2 |
out << "(" << d_quant[0][i] << " " << ss.str() << ")"; |
541 |
|
} |
542 |
2 |
out << ")" << std::endl; |
543 |
|
} |
544 |
1679 |
if (inst.getKind() == NOT && inst[0].getKind() == FORALL) |
545 |
|
{ |
546 |
2379 |
for (const Node& v : inst[0][0]) |
547 |
|
{ |
548 |
3938 |
Node sk = sm->mkDummySkolem("rsk", v.getType()); |
549 |
1969 |
sks.push_back(sk); |
550 |
1969 |
vars.push_back(v); |
551 |
3938 |
Trace("cegqi-check-debug") |
552 |
1969 |
<< " introduce skolem " << sk << " for " << v << "\n"; |
553 |
|
} |
554 |
410 |
query = inst[0][1].substitute( |
555 |
|
vars.begin(), vars.end(), sks.begin(), sks.end()); |
556 |
410 |
query = query.negate(); |
557 |
|
} |
558 |
|
else |
559 |
|
{ |
560 |
|
// use the instance itself |
561 |
1269 |
query = inst; |
562 |
|
} |
563 |
|
} |
564 |
1679 |
d_ce_sk_vars.insert(d_ce_sk_vars.end(), sks.begin(), sks.end()); |
565 |
1679 |
d_set_ce_sk_vars = true; |
566 |
|
|
567 |
1679 |
if (query.isNull()) |
568 |
|
{ |
569 |
|
// no lemma to check |
570 |
|
return false; |
571 |
|
} |
572 |
|
|
573 |
|
// simplify the lemma based on the term database sygus utility |
574 |
1679 |
query = d_tds->rewriteNode(query); |
575 |
|
// eagerly unfold applications of evaluation function |
576 |
1679 |
Trace("cegqi-debug") << "pre-unfold counterexample : " << query << std::endl; |
577 |
|
// Record the solution, which may be falsified below. We require recording |
578 |
|
// here since the result of the satisfiability test may be unknown. |
579 |
1679 |
recordSolution(candidate_values); |
580 |
|
|
581 |
1679 |
if (!query.isConst() || query.getConst<bool>()) |
582 |
|
{ |
583 |
539 |
Trace("sygus-engine") << " *** Verify with subcall..." << std::endl; |
584 |
653 |
Result r = checkWithSubsolver(query, d_ce_sk_vars, d_ce_sk_var_mvs); |
585 |
539 |
Trace("sygus-engine") << " ...got " << r << std::endl; |
586 |
539 |
if (r.asSatisfiabilityResult().isSat() == Result::SAT) |
587 |
|
{ |
588 |
409 |
if (Trace.isOn("sygus-engine")) |
589 |
|
{ |
590 |
|
Trace("sygus-engine") << " * Verification lemma failed for:\n "; |
591 |
|
for (unsigned i = 0, size = d_ce_sk_vars.size(); i < size; i++) |
592 |
|
{ |
593 |
|
Trace("sygus-engine") |
594 |
|
<< d_ce_sk_vars[i] << " -> " << d_ce_sk_var_mvs[i] << " "; |
595 |
|
} |
596 |
|
Trace("sygus-engine") << std::endl; |
597 |
|
} |
598 |
409 |
if (Configuration::isAssertionBuild()) |
599 |
|
{ |
600 |
|
// the values for the query should be a complete model |
601 |
|
Node squery = query.substitute(d_ce_sk_vars.begin(), |
602 |
|
d_ce_sk_vars.end(), |
603 |
|
d_ce_sk_var_mvs.begin(), |
604 |
818 |
d_ce_sk_var_mvs.end()); |
605 |
409 |
Trace("cegqi-debug") << "...squery : " << squery << std::endl; |
606 |
409 |
squery = Rewriter::rewrite(squery); |
607 |
409 |
Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl; |
608 |
409 |
Assert(options::sygusRecFun() |
609 |
|
|| (squery.isConst() && squery.getConst<bool>())); |
610 |
|
} |
611 |
409 |
return false; |
612 |
|
} |
613 |
130 |
else if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) |
614 |
|
{ |
615 |
|
// In the rare case that the subcall is unknown, we simply exclude the |
616 |
|
// solution, without adding a counterexample point. This should only |
617 |
|
// happen if the quantifier free logic is undecidable. |
618 |
16 |
excludeCurrentSolution(terms, candidate_values); |
619 |
|
// We should set incomplete, since a "sat" answer should not be |
620 |
|
// interpreted as "infeasible", which would make a difference in the rare |
621 |
|
// case where e.g. we had a finite grammar and exhausted the grammar. |
622 |
16 |
d_qim.setIncomplete(IncompleteId::QUANTIFIERS_SYGUS_NO_VERIFY); |
623 |
16 |
return false; |
624 |
|
} |
625 |
|
// otherwise we are unsat, and we will process the solution below |
626 |
|
} |
627 |
|
// now mark that we have a solution |
628 |
1254 |
d_hasSolution = true; |
629 |
1254 |
if (options::sygusStream()) |
630 |
|
{ |
631 |
|
// immediately print the current solution |
632 |
1068 |
printAndContinueStream(terms, candidate_values); |
633 |
|
// streaming means now we immediately are looking for a new solution |
634 |
1068 |
d_hasSolution = false; |
635 |
1068 |
return false; |
636 |
|
} |
637 |
|
// Use lemma to terminate with "unsat", this is justified by the verification |
638 |
|
// check above, which confirms the synthesis conjecture is solved. |
639 |
186 |
lems.push_back(d_quant.negate()); |
640 |
186 |
return true; |
641 |
|
} |
642 |
|
|
643 |
1750 |
bool SynthConjecture::checkSideCondition(const std::vector<Node>& cvals) const |
644 |
|
{ |
645 |
1750 |
if (!d_embedSideCondition.isNull()) |
646 |
|
{ |
647 |
242 |
Node sc = d_embedSideCondition; |
648 |
156 |
if (!cvals.empty()) |
649 |
|
{ |
650 |
156 |
sc = sc.substitute( |
651 |
|
d_candidates.begin(), d_candidates.end(), cvals.begin(), cvals.end()); |
652 |
|
} |
653 |
156 |
Trace("sygus-engine") << "Check side condition..." << std::endl; |
654 |
156 |
Trace("cegqi-debug") << "Check side condition : " << sc << std::endl; |
655 |
242 |
Result r = checkWithSubsolver(sc); |
656 |
156 |
Trace("cegqi-debug") << "...got side condition : " << r << std::endl; |
657 |
156 |
if (r == Result::UNSAT) |
658 |
|
{ |
659 |
70 |
return false; |
660 |
|
} |
661 |
86 |
Trace("sygus-engine") << "...passed side condition" << std::endl; |
662 |
|
} |
663 |
1680 |
return true; |
664 |
|
} |
665 |
|
|
666 |
409 |
bool SynthConjecture::doRefine() |
667 |
|
{ |
668 |
818 |
std::vector<Node> lems; |
669 |
409 |
Assert(d_set_ce_sk_vars); |
670 |
|
|
671 |
|
// first, make skolem substitution |
672 |
818 |
Trace("cegqi-refine") << "doRefine : construct skolem substitution..." |
673 |
409 |
<< std::endl; |
674 |
818 |
std::vector<Node> sk_vars; |
675 |
818 |
std::vector<Node> sk_subs; |
676 |
|
// collect the substitution over all disjuncts |
677 |
409 |
if (!d_ce_sk_vars.empty()) |
678 |
|
{ |
679 |
255 |
Trace("cegqi-refine") << "Get model values for skolems..." << std::endl; |
680 |
255 |
Assert(d_inner_vars.size() == d_ce_sk_vars.size()); |
681 |
255 |
if (d_ce_sk_var_mvs.empty()) |
682 |
|
{ |
683 |
|
std::vector<Node> model_values; |
684 |
|
for (const Node& v : d_ce_sk_vars) |
685 |
|
{ |
686 |
|
Node mv = getModelValue(v); |
687 |
|
Trace("cegqi-refine") << " " << v << " -> " << mv << std::endl; |
688 |
|
model_values.push_back(mv); |
689 |
|
} |
690 |
|
sk_subs.insert(sk_subs.end(), model_values.begin(), model_values.end()); |
691 |
|
} |
692 |
|
else |
693 |
|
{ |
694 |
255 |
Assert(d_ce_sk_var_mvs.size() == d_ce_sk_vars.size()); |
695 |
255 |
sk_subs.insert( |
696 |
510 |
sk_subs.end(), d_ce_sk_var_mvs.begin(), d_ce_sk_var_mvs.end()); |
697 |
|
} |
698 |
255 |
sk_vars.insert(sk_vars.end(), d_inner_vars.begin(), d_inner_vars.end()); |
699 |
|
} |
700 |
|
else |
701 |
|
{ |
702 |
154 |
Assert(d_inner_vars.empty()); |
703 |
|
} |
704 |
|
|
705 |
818 |
std::vector<Node> lem_c; |
706 |
818 |
Trace("cegqi-refine") << "doRefine : Construct refinement lemma..." |
707 |
409 |
<< std::endl; |
708 |
818 |
Trace("cegqi-refine-debug") |
709 |
409 |
<< " For counterexample skolems : " << d_ce_sk_vars << std::endl; |
710 |
818 |
Node base_lem; |
711 |
409 |
if (d_base_inst.getKind() == NOT && d_base_inst[0].getKind() == FORALL) |
712 |
|
{ |
713 |
255 |
base_lem = d_base_inst[0][1]; |
714 |
|
} |
715 |
|
else |
716 |
|
{ |
717 |
154 |
base_lem = d_base_inst.negate(); |
718 |
|
} |
719 |
|
|
720 |
409 |
Assert(sk_vars.size() == sk_subs.size()); |
721 |
|
|
722 |
409 |
Trace("cegqi-refine") << "doRefine : substitute..." << std::endl; |
723 |
409 |
base_lem = base_lem.substitute( |
724 |
|
sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end()); |
725 |
409 |
Trace("cegqi-refine") << "doRefine : rewrite..." << std::endl; |
726 |
409 |
base_lem = d_tds->rewriteNode(base_lem); |
727 |
818 |
Trace("cegqi-refine") << "doRefine : register refinement lemma " << base_lem |
728 |
409 |
<< "..." << std::endl; |
729 |
409 |
d_master->registerRefinementLemma(sk_vars, base_lem, lems); |
730 |
409 |
Trace("cegqi-refine") << "doRefine : finished" << std::endl; |
731 |
409 |
d_set_ce_sk_vars = false; |
732 |
409 |
d_ce_sk_vars.clear(); |
733 |
409 |
d_ce_sk_var_mvs.clear(); |
734 |
|
|
735 |
|
// now send the lemmas |
736 |
409 |
bool addedLemma = false; |
737 |
818 |
for (const Node& lem : lems) |
738 |
|
{ |
739 |
818 |
Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem |
740 |
409 |
<< std::endl; |
741 |
409 |
bool res = d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); |
742 |
409 |
if (res) |
743 |
|
{ |
744 |
251 |
++(d_stats.d_cegqi_lemmas_refine); |
745 |
251 |
d_refine_count++; |
746 |
251 |
addedLemma = true; |
747 |
|
} |
748 |
|
else |
749 |
|
{ |
750 |
158 |
Trace("cegqi-warn") << " ...FAILED to add refinement!" << std::endl; |
751 |
|
} |
752 |
|
} |
753 |
409 |
if (addedLemma) |
754 |
|
{ |
755 |
251 |
Trace("sygus-engine-debug") << " ...refine candidate." << std::endl; |
756 |
|
} |
757 |
|
else |
758 |
|
{ |
759 |
316 |
Trace("sygus-engine-debug") << " ...(warning) failed to refine candidate, " |
760 |
158 |
"manually exclude candidate." |
761 |
158 |
<< std::endl; |
762 |
316 |
std::vector<Node> cvals; |
763 |
316 |
for (const Node& c : d_candidates) |
764 |
|
{ |
765 |
158 |
cvals.push_back(d_cinfo[c].d_inst.back()); |
766 |
|
} |
767 |
|
// something went wrong, exclude the current candidate |
768 |
158 |
excludeCurrentSolution(d_candidates, cvals); |
769 |
|
// Note this happens when evaluation is incapable of disproving a candidate |
770 |
|
// for counterexample point c, but satisfiability checking happened to find |
771 |
|
// the the same point c is indeed a true counterexample. It is sound |
772 |
|
// to exclude the candidate in this case. |
773 |
|
} |
774 |
818 |
return addedLemma; |
775 |
|
} |
776 |
|
|
777 |
327 |
void SynthConjecture::preregisterConjecture(Node q) |
778 |
|
{ |
779 |
327 |
d_ceg_si->preregisterConjecture(q); |
780 |
327 |
} |
781 |
|
|
782 |
38777 |
bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n, |
783 |
|
std::vector<Node>& v, |
784 |
|
bool& activeIncomplete) |
785 |
|
{ |
786 |
77554 |
std::vector<Node> ncheck = n; |
787 |
38777 |
n.clear(); |
788 |
38777 |
bool ret = true; |
789 |
82508 |
for (unsigned i = 0, size = ncheck.size(); i < size; i++) |
790 |
|
{ |
791 |
87464 |
Node e = ncheck[i]; |
792 |
|
// if it is not active, we return null |
793 |
87464 |
Node g = d_tds->getActiveGuardForEnumerator(e); |
794 |
43740 |
if (!g.isNull()) |
795 |
|
{ |
796 |
70132 |
Node gstatus = d_qstate.getValuation().getSatValue(g); |
797 |
35090 |
if (gstatus.isNull() || !gstatus.getConst<bool>()) |
798 |
|
{ |
799 |
32 |
Trace("sygus-engine-debug") |
800 |
16 |
<< "Enumerator " << e << " is inactive." << std::endl; |
801 |
16 |
continue; |
802 |
|
} |
803 |
|
} |
804 |
87448 |
Node nv = getEnumeratedValue(e, activeIncomplete); |
805 |
43715 |
n.push_back(e); |
806 |
43715 |
v.push_back(nv); |
807 |
43715 |
ret = ret && !nv.isNull(); |
808 |
|
} |
809 |
77536 |
return ret; |
810 |
|
} |
811 |
|
|
812 |
43724 |
Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete) |
813 |
|
{ |
814 |
43724 |
bool isEnum = d_tds->isEnumerator(e); |
815 |
|
|
816 |
43724 |
if (isEnum && !e.getAttribute(SygusSymBreakOkAttribute())) |
817 |
|
{ |
818 |
|
// if the current model value of e was not registered by the datatypes |
819 |
|
// sygus solver, or was excluded by symmetry breaking, then it does not |
820 |
|
// have a proper model value that we should consider, thus we return null. |
821 |
3944 |
Trace("sygus-engine-debug") |
822 |
1972 |
<< "Enumerator " << e << " does not have proper model value." |
823 |
1972 |
<< std::endl; |
824 |
1972 |
return Node::null(); |
825 |
|
} |
826 |
|
|
827 |
41752 |
if (!isEnum || d_tds->isPassiveEnumerator(e)) |
828 |
|
{ |
829 |
6822 |
return getModelValue(e); |
830 |
|
} |
831 |
|
|
832 |
|
// management of actively generated enumerators goes here |
833 |
|
|
834 |
|
// initialize the enumerated value generator for e |
835 |
|
std::map<Node, std::unique_ptr<EnumValGenerator> >::iterator iteg = |
836 |
34930 |
d_evg.find(e); |
837 |
34930 |
if (iteg == d_evg.end()) |
838 |
|
{ |
839 |
114 |
if (d_tds->isVariableAgnosticEnumerator(e)) |
840 |
|
{ |
841 |
1 |
d_evg[e].reset(new EnumStreamConcrete(d_tds)); |
842 |
|
} |
843 |
|
else |
844 |
|
{ |
845 |
|
// Actively-generated enumerators are currently either variable agnostic |
846 |
|
// or basic. The auto mode always prefers the optimized enumerator over |
847 |
|
// the basic one. |
848 |
113 |
Assert(d_tds->isBasicEnumerator(e)); |
849 |
1284 |
if (options::sygusActiveGenMode() |
850 |
113 |
== options::SygusActiveGenMode::ENUM_BASIC) |
851 |
|
{ |
852 |
|
d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType())); |
853 |
|
} |
854 |
|
else |
855 |
|
{ |
856 |
113 |
Assert(options::sygusActiveGenMode() |
857 |
|
== options::SygusActiveGenMode::ENUM |
858 |
|
|| options::sygusActiveGenMode() |
859 |
|
== options::SygusActiveGenMode::AUTO); |
860 |
113 |
d_evg[e].reset(new SygusEnumerator(d_tds, this, d_stats)); |
861 |
|
} |
862 |
|
} |
863 |
228 |
Trace("sygus-active-gen") |
864 |
114 |
<< "Active-gen: initialize for " << e << std::endl; |
865 |
114 |
d_evg[e]->initialize(e); |
866 |
114 |
d_ev_curr_active_gen[e] = Node::null(); |
867 |
114 |
iteg = d_evg.find(e); |
868 |
114 |
Trace("sygus-active-gen-debug") << "...finish" << std::endl; |
869 |
|
} |
870 |
|
// if we have a waiting value, return it |
871 |
34930 |
std::map<Node, Node>::iterator itw = d_ev_active_gen_waiting.find(e); |
872 |
34930 |
if (itw != d_ev_active_gen_waiting.end()) |
873 |
|
{ |
874 |
|
Trace("sygus-active-gen-debug") |
875 |
|
<< "Active-gen: return waiting " << itw->second << std::endl; |
876 |
|
return itw->second; |
877 |
|
} |
878 |
|
// Check if there is an (abstract) value absE we were actively generating |
879 |
|
// values based on. |
880 |
69860 |
Node absE = d_ev_curr_active_gen[e]; |
881 |
34930 |
bool firstTime = false; |
882 |
34930 |
if (absE.isNull()) |
883 |
|
{ |
884 |
|
// None currently exist. The next abstract value is the model value for e. |
885 |
114 |
absE = getModelValue(e); |
886 |
114 |
if (Trace.isOn("sygus-active-gen")) |
887 |
|
{ |
888 |
|
Trace("sygus-active-gen") << "Active-gen: new abstract value : "; |
889 |
|
TermDbSygus::toStreamSygus("sygus-active-gen", e); |
890 |
|
Trace("sygus-active-gen") << " -> "; |
891 |
|
TermDbSygus::toStreamSygus("sygus-active-gen", absE); |
892 |
|
Trace("sygus-active-gen") << std::endl; |
893 |
|
} |
894 |
114 |
d_ev_curr_active_gen[e] = absE; |
895 |
114 |
iteg->second->addValue(absE); |
896 |
114 |
firstTime = true; |
897 |
|
} |
898 |
34930 |
bool inc = true; |
899 |
34930 |
if (!firstTime) |
900 |
|
{ |
901 |
34816 |
inc = iteg->second->increment(); |
902 |
|
} |
903 |
69860 |
Node v; |
904 |
34930 |
if (inc) |
905 |
|
{ |
906 |
34925 |
v = iteg->second->getCurrent(); |
907 |
|
} |
908 |
69842 |
Trace("sygus-active-gen-debug") << "...generated " << v |
909 |
34921 |
<< ", with increment success : " << inc |
910 |
34921 |
<< std::endl; |
911 |
34921 |
if (!inc) |
912 |
|
{ |
913 |
|
// No more concrete values generated from absE. |
914 |
5 |
NodeManager* nm = NodeManager::currentNM(); |
915 |
5 |
d_ev_curr_active_gen[e] = Node::null(); |
916 |
10 |
std::vector<Node> exp; |
917 |
|
// If we are a basic enumerator, a single abstract value maps to *all* |
918 |
|
// concrete values of its type, thus we don't depend on the current |
919 |
|
// solution. |
920 |
5 |
if (!d_tds->isBasicEnumerator(e)) |
921 |
|
{ |
922 |
|
// We must block e = absE |
923 |
1 |
d_tds->getExplain()->getExplanationForEquality(e, absE, exp); |
924 |
2 |
for (unsigned i = 0, size = exp.size(); i < size; i++) |
925 |
|
{ |
926 |
1 |
exp[i] = exp[i].negate(); |
927 |
|
} |
928 |
|
} |
929 |
10 |
Node g = d_tds->getActiveGuardForEnumerator(e); |
930 |
5 |
if (!g.isNull()) |
931 |
|
{ |
932 |
5 |
if (d_ev_active_gen_first_val.find(e) == d_ev_active_gen_first_val.end()) |
933 |
|
{ |
934 |
5 |
exp.push_back(g.negate()); |
935 |
5 |
d_ev_active_gen_first_val[e] = absE; |
936 |
|
} |
937 |
|
} |
938 |
|
else |
939 |
|
{ |
940 |
|
Assert(false); |
941 |
|
} |
942 |
10 |
Node lem = exp.size() == 1 ? exp[0] : nm->mkNode(OR, exp); |
943 |
10 |
Trace("cegqi-lemma") << "Cegqi::Lemma : actively-generated enumerator " |
944 |
5 |
"exclude current solution : " |
945 |
5 |
<< lem << std::endl; |
946 |
5 |
if (Trace.isOn("sygus-active-gen-debug")) |
947 |
|
{ |
948 |
|
Trace("sygus-active-gen-debug") << "Active-gen: block "; |
949 |
|
TermDbSygus::toStreamSygus("sygus-active-gen-debug", absE); |
950 |
|
Trace("sygus-active-gen-debug") << std::endl; |
951 |
|
} |
952 |
5 |
d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_EXCLUDE_CURRENT); |
953 |
|
} |
954 |
|
else |
955 |
|
{ |
956 |
|
// We are waiting to send e -> v to the module that requested it. |
957 |
34916 |
if (v.isNull()) |
958 |
|
{ |
959 |
20835 |
activeIncomplete = true; |
960 |
|
} |
961 |
|
else |
962 |
|
{ |
963 |
14081 |
d_ev_active_gen_waiting[e] = v; |
964 |
|
} |
965 |
34916 |
if (Trace.isOn("sygus-active-gen")) |
966 |
|
{ |
967 |
|
Trace("sygus-active-gen") << "Active-gen : " << e << " : "; |
968 |
|
TermDbSygus::toStreamSygus("sygus-active-gen", absE); |
969 |
|
Trace("sygus-active-gen") << " -> "; |
970 |
|
TermDbSygus::toStreamSygus("sygus-active-gen", v); |
971 |
|
Trace("sygus-active-gen") << std::endl; |
972 |
|
} |
973 |
|
} |
974 |
|
|
975 |
34921 |
return v; |
976 |
|
} |
977 |
|
|
978 |
7400 |
Node SynthConjecture::getModelValue(Node n) |
979 |
|
{ |
980 |
7400 |
Trace("cegqi-mv") << "getModelValue for : " << n << std::endl; |
981 |
7400 |
return d_treg.getModel()->getValue(n); |
982 |
|
} |
983 |
|
|
984 |
|
void SynthConjecture::debugPrint(const char* c) |
985 |
|
{ |
986 |
|
Trace(c) << "Synthesis conjecture : " << d_embed_quant << std::endl; |
987 |
|
Trace(c) << " * Candidate programs : " << d_candidates << std::endl; |
988 |
|
Trace(c) << " * Counterexample skolems : " << d_ce_sk_vars << std::endl; |
989 |
|
} |
990 |
|
|
991 |
1068 |
void SynthConjecture::printAndContinueStream(const std::vector<Node>& enums, |
992 |
|
const std::vector<Node>& values) |
993 |
|
{ |
994 |
1068 |
Assert(d_master != nullptr); |
995 |
|
// we have generated a solution, print it |
996 |
|
// get the current output stream |
997 |
1068 |
Options& sopts = smt::currentSmtEngine()->getOptions(); |
998 |
1068 |
printSynthSolutionInternal(*sopts.getOut()); |
999 |
1068 |
excludeCurrentSolution(enums, values); |
1000 |
1068 |
} |
1001 |
|
|
1002 |
1312 |
void SynthConjecture::excludeCurrentSolution(const std::vector<Node>& enums, |
1003 |
|
const std::vector<Node>& values) |
1004 |
|
{ |
1005 |
2624 |
Trace("cegqi-debug") << "Exclude current solution: " << enums << " / " |
1006 |
1312 |
<< values << std::endl; |
1007 |
|
// We will not refine the current candidate solution since it is a solution |
1008 |
|
// thus, we clear information regarding the current refinement |
1009 |
1312 |
d_set_ce_sk_vars = false; |
1010 |
1312 |
d_ce_sk_vars.clear(); |
1011 |
1312 |
d_ce_sk_var_mvs.clear(); |
1012 |
|
// However, we need to exclude the current solution using an explicit |
1013 |
|
// blocking clause, so that we proceed to the next solution. We do this only |
1014 |
|
// for passively-generated enumerators (TermDbSygus::isPassiveEnumerator). |
1015 |
2624 |
std::vector<Node> exp; |
1016 |
2672 |
for (unsigned i = 0, tsize = enums.size(); i < tsize; i++) |
1017 |
|
{ |
1018 |
2720 |
Node cprog = enums[i]; |
1019 |
1360 |
Assert(d_tds->isEnumerator(cprog)); |
1020 |
1360 |
if (d_tds->isPassiveEnumerator(cprog)) |
1021 |
|
{ |
1022 |
138 |
Node cval = values[i]; |
1023 |
|
// add to explanation of exclusion |
1024 |
69 |
d_tds->getExplain()->getExplanationForEquality(cprog, cval, exp); |
1025 |
|
} |
1026 |
|
} |
1027 |
1312 |
if (!exp.empty()) |
1028 |
|
{ |
1029 |
21 |
if (!d_guarded_stream_exc) |
1030 |
|
{ |
1031 |
6 |
d_guarded_stream_exc = true; |
1032 |
6 |
exp.push_back(d_feasible_guard); |
1033 |
|
} |
1034 |
21 |
Node exc_lem = exp.size() == 1 |
1035 |
|
? exp[0] |
1036 |
42 |
: NodeManager::currentNM()->mkNode(kind::AND, exp); |
1037 |
21 |
exc_lem = exc_lem.negate(); |
1038 |
42 |
Trace("cegqi-lemma") << "Cegqi::Lemma : stream exclude current solution : " |
1039 |
21 |
<< exc_lem << std::endl; |
1040 |
21 |
d_qim.lemma(exc_lem, InferenceId::QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT); |
1041 |
|
} |
1042 |
1312 |
} |
1043 |
|
|
1044 |
1068 |
void SynthConjecture::printSynthSolutionInternal(std::ostream& out) |
1045 |
|
{ |
1046 |
1068 |
Trace("cegqi-sol-debug") << "Printing synth solution..." << std::endl; |
1047 |
1068 |
Assert(d_quant[0].getNumChildren() == d_embed_quant[0].getNumChildren()); |
1048 |
2136 |
std::vector<Node> sols; |
1049 |
2136 |
std::vector<int8_t> statuses; |
1050 |
1068 |
if (!getSynthSolutionsInternal(sols, statuses)) |
1051 |
|
{ |
1052 |
|
return; |
1053 |
|
} |
1054 |
1068 |
NodeManager* nm = NodeManager::currentNM(); |
1055 |
2136 |
for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++) |
1056 |
|
{ |
1057 |
2136 |
Node sol = sols[i]; |
1058 |
1068 |
if (!sol.isNull()) |
1059 |
|
{ |
1060 |
2136 |
Node prog = d_embed_quant[0][i]; |
1061 |
1068 |
int8_t status = statuses[i]; |
1062 |
2136 |
TypeNode tn = prog.getType(); |
1063 |
1068 |
const DType& dt = tn.getDType(); |
1064 |
2136 |
std::stringstream ss; |
1065 |
1068 |
ss << prog; |
1066 |
2136 |
std::string f(ss.str()); |
1067 |
1068 |
f.erase(f.begin()); |
1068 |
1068 |
++(d_stats.d_solutions); |
1069 |
|
|
1070 |
1068 |
bool is_unique_term = true; |
1071 |
|
|
1072 |
1068 |
if (status != 0 |
1073 |
2132 |
&& (options::sygusRewSynth() || options::sygusQueryGen() |
1074 |
60 |
|| options::sygusFilterSolMode() |
1075 |
|
!= options::SygusFilterSolMode::NONE)) |
1076 |
|
{ |
1077 |
1064 |
Trace("cegqi-sol-debug") << "Run expression mining..." << std::endl; |
1078 |
|
std::map<Node, ExpressionMinerManager>::iterator its = |
1079 |
1064 |
d_exprm.find(prog); |
1080 |
1064 |
if (its == d_exprm.end()) |
1081 |
|
{ |
1082 |
27 |
d_exprm[prog].initializeSygus( |
1083 |
18 |
d_tds, d_candidates[i], options::sygusSamples(), true); |
1084 |
9 |
if (options::sygusRewSynth()) |
1085 |
|
{ |
1086 |
7 |
d_exprm[prog].enableRewriteRuleSynth(); |
1087 |
|
} |
1088 |
9 |
if (options::sygusQueryGen()) |
1089 |
|
{ |
1090 |
|
d_exprm[prog].enableQueryGeneration(options::sygusQueryGenThresh()); |
1091 |
|
} |
1092 |
18 |
if (options::sygusFilterSolMode() |
1093 |
9 |
!= options::SygusFilterSolMode::NONE) |
1094 |
|
{ |
1095 |
4 |
if (options::sygusFilterSolMode() |
1096 |
2 |
== options::SygusFilterSolMode::STRONG) |
1097 |
|
{ |
1098 |
2 |
d_exprm[prog].enableFilterStrongSolutions(); |
1099 |
|
} |
1100 |
|
else if (options::sygusFilterSolMode() |
1101 |
|
== options::SygusFilterSolMode::WEAK) |
1102 |
|
{ |
1103 |
|
d_exprm[prog].enableFilterWeakSolutions(); |
1104 |
|
} |
1105 |
|
} |
1106 |
9 |
its = d_exprm.find(prog); |
1107 |
|
} |
1108 |
1064 |
bool rew_print = false; |
1109 |
1064 |
is_unique_term = d_exprm[prog].addTerm(sol, out, rew_print); |
1110 |
1064 |
if (rew_print) |
1111 |
|
{ |
1112 |
103 |
++(d_stats.d_candidate_rewrites_print); |
1113 |
|
} |
1114 |
1064 |
if (!is_unique_term) |
1115 |
|
{ |
1116 |
253 |
++(d_stats.d_filtered_solutions); |
1117 |
|
} |
1118 |
|
} |
1119 |
1068 |
if (is_unique_term) |
1120 |
|
{ |
1121 |
815 |
out << "(define-fun " << f << " "; |
1122 |
|
// Only include variables that are truly bound variables of the |
1123 |
|
// function-to-synthesize. This means we exclude variables that encode |
1124 |
|
// external terms. This ensures that --sygus-stream prints |
1125 |
|
// solutions with no arguments on the predicate for responses to |
1126 |
|
// the get-abduct command. |
1127 |
|
// pvs stores the variables that will be printed in the argument list |
1128 |
|
// below. |
1129 |
1630 |
std::vector<Node> pvs; |
1130 |
1630 |
Node vl = dt.getSygusVarList(); |
1131 |
815 |
if (!vl.isNull()) |
1132 |
|
{ |
1133 |
815 |
Assert(vl.getKind() == BOUND_VAR_LIST); |
1134 |
|
SygusVarToTermAttribute sta; |
1135 |
2723 |
for (const Node& v : vl) |
1136 |
|
{ |
1137 |
1908 |
if (!v.hasAttribute(sta)) |
1138 |
|
{ |
1139 |
1824 |
pvs.push_back(v); |
1140 |
|
} |
1141 |
|
} |
1142 |
|
} |
1143 |
815 |
if (pvs.empty()) |
1144 |
|
{ |
1145 |
21 |
out << "() "; |
1146 |
|
} |
1147 |
|
else |
1148 |
|
{ |
1149 |
794 |
vl = nm->mkNode(BOUND_VAR_LIST, pvs); |
1150 |
794 |
out << vl << " "; |
1151 |
|
} |
1152 |
815 |
out << dt.getSygusType() << " "; |
1153 |
815 |
if (status == 0) |
1154 |
|
{ |
1155 |
|
out << sol; |
1156 |
|
} |
1157 |
|
else |
1158 |
|
{ |
1159 |
1630 |
Node bsol = datatypes::utils::sygusToBuiltin(sol, true); |
1160 |
815 |
out << bsol; |
1161 |
|
} |
1162 |
815 |
out << ")" << std::endl; |
1163 |
|
} |
1164 |
|
} |
1165 |
|
} |
1166 |
|
} |
1167 |
|
|
1168 |
249 |
bool SynthConjecture::getSynthSolutions( |
1169 |
|
std::map<Node, std::map<Node, Node> >& sol_map) |
1170 |
|
{ |
1171 |
249 |
NodeManager* nm = NodeManager::currentNM(); |
1172 |
498 |
std::vector<Node> sols; |
1173 |
498 |
std::vector<int8_t> statuses; |
1174 |
249 |
Trace("cegqi-debug") << "getSynthSolutions..." << std::endl; |
1175 |
249 |
if (!getSynthSolutionsInternal(sols, statuses)) |
1176 |
|
{ |
1177 |
|
Trace("cegqi-debug") << "...failed internal" << std::endl; |
1178 |
|
return false; |
1179 |
|
} |
1180 |
|
// we add it to the solution map, indexed by this conjecture |
1181 |
249 |
std::map<Node, Node>& smc = sol_map[d_quant]; |
1182 |
624 |
for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++) |
1183 |
|
{ |
1184 |
750 |
Node sol = sols[i]; |
1185 |
375 |
int8_t status = statuses[i]; |
1186 |
750 |
Trace("cegqi-debug") << "...got " << i << ": " << sol |
1187 |
375 |
<< ", status=" << status << std::endl; |
1188 |
|
// get the builtin solution |
1189 |
750 |
Node bsol = sol; |
1190 |
375 |
if (status != 0) |
1191 |
|
{ |
1192 |
|
// Convert sygus to builtin here. |
1193 |
|
// We must use the external representation to ensure bsol matches the |
1194 |
|
// grammar. |
1195 |
224 |
bsol = datatypes::utils::sygusToBuiltin(sol, true); |
1196 |
|
} |
1197 |
|
// convert to lambda |
1198 |
750 |
TypeNode tn = d_embed_quant[0][i].getType(); |
1199 |
375 |
const DType& dt = tn.getDType(); |
1200 |
750 |
Node fvar = d_quant[0][i]; |
1201 |
750 |
Node bvl = dt.getSygusVarList(); |
1202 |
375 |
if (!bvl.isNull()) |
1203 |
|
{ |
1204 |
|
// since we don't have function subtyping, this assertion should only |
1205 |
|
// check the return type |
1206 |
291 |
Assert(fvar.getType().isFunction()); |
1207 |
291 |
Assert(fvar.getType().getRangeType().isComparableTo(bsol.getType())); |
1208 |
291 |
bsol = nm->mkNode(LAMBDA, bvl, bsol); |
1209 |
|
} |
1210 |
|
else |
1211 |
|
{ |
1212 |
84 |
Assert(fvar.getType().isComparableTo(bsol.getType())); |
1213 |
|
} |
1214 |
|
// store in map |
1215 |
375 |
smc[fvar] = bsol; |
1216 |
375 |
Trace("cegqi-debug") << "...return " << bsol << std::endl; |
1217 |
|
} |
1218 |
249 |
return true; |
1219 |
|
} |
1220 |
|
|
1221 |
1680 |
void SynthConjecture::recordSolution(std::vector<Node>& vs) |
1222 |
|
{ |
1223 |
1680 |
Assert(vs.size() == d_candidates.size()); |
1224 |
1680 |
d_cinfo.clear(); |
1225 |
3525 |
for (unsigned i = 0; i < vs.size(); i++) |
1226 |
|
{ |
1227 |
1845 |
d_cinfo[d_candidates[i]].d_inst.push_back(vs[i]); |
1228 |
|
} |
1229 |
1680 |
} |
1230 |
|
|
1231 |
1317 |
bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols, |
1232 |
|
std::vector<int8_t>& statuses) |
1233 |
|
{ |
1234 |
1317 |
if (!d_hasSolution) |
1235 |
|
{ |
1236 |
|
return false; |
1237 |
|
} |
1238 |
2760 |
for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++) |
1239 |
|
{ |
1240 |
2886 |
Node prog = d_embed_quant[0][i]; |
1241 |
1443 |
Trace("cegqi-debug") << " get solution for " << prog << std::endl; |
1242 |
2886 |
TypeNode tn = prog.getType(); |
1243 |
1443 |
Assert(tn.isDatatype()); |
1244 |
|
// get the solution |
1245 |
2886 |
Node sol; |
1246 |
1443 |
int8_t status = -1; |
1247 |
1443 |
if (isSingleInvocation()) |
1248 |
|
{ |
1249 |
159 |
Assert(d_ceg_si != NULL); |
1250 |
159 |
sol = d_ceg_si->getSolution(i, tn, status, true); |
1251 |
159 |
if (sol.isNull()) |
1252 |
|
{ |
1253 |
|
return false; |
1254 |
|
} |
1255 |
159 |
sol = sol.getKind() == LAMBDA ? sol[1] : sol; |
1256 |
|
} |
1257 |
|
else |
1258 |
|
{ |
1259 |
2568 |
Node cprog = d_candidates[i]; |
1260 |
1284 |
if (!d_cinfo[cprog].d_inst.empty()) |
1261 |
|
{ |
1262 |
|
// the solution is just the last instantiated term |
1263 |
1284 |
sol = d_cinfo[cprog].d_inst.back(); |
1264 |
1284 |
status = 1; |
1265 |
|
|
1266 |
|
// check if there was a template |
1267 |
2568 |
Node sf = d_quant[0][i]; |
1268 |
2568 |
Node templ = d_templInfer->getTemplate(sf); |
1269 |
1284 |
if (!templ.isNull()) |
1270 |
|
{ |
1271 |
32 |
Trace("cegqi-inv-debug") |
1272 |
16 |
<< sf << " used template : " << templ << std::endl; |
1273 |
|
// if it was not embedded into the grammar |
1274 |
16 |
if (!options::sygusTemplEmbedGrammar()) |
1275 |
|
{ |
1276 |
32 |
TNode templa = d_templInfer->getTemplateArg(sf); |
1277 |
|
// make the builtin version of the full solution |
1278 |
16 |
sol = d_tds->sygusToBuiltin(sol, sol.getType()); |
1279 |
32 |
Trace("cegqi-inv") << "Builtin version of solution is : " << sol |
1280 |
16 |
<< ", type : " << sol.getType() << std::endl; |
1281 |
32 |
TNode tsol = sol; |
1282 |
16 |
sol = templ.substitute(templa, tsol); |
1283 |
16 |
Trace("cegqi-inv-debug") << "With template : " << sol << std::endl; |
1284 |
16 |
sol = Rewriter::rewrite(sol); |
1285 |
16 |
Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl; |
1286 |
|
// now, reconstruct to the syntax |
1287 |
16 |
sol = d_ceg_si->reconstructToSyntax(sol, tn, status, true); |
1288 |
16 |
sol = sol.getKind() == LAMBDA ? sol[1] : sol; |
1289 |
32 |
Trace("cegqi-inv-debug") |
1290 |
16 |
<< "Reconstructed to syntax : " << sol << std::endl; |
1291 |
|
} |
1292 |
|
else |
1293 |
|
{ |
1294 |
|
Trace("cegqi-inv-debug") |
1295 |
|
<< "...was embedding into grammar." << std::endl; |
1296 |
|
} |
1297 |
|
} |
1298 |
|
else |
1299 |
|
{ |
1300 |
2536 |
Trace("cegqi-inv-debug") |
1301 |
1268 |
<< sf << " did not use template" << std::endl; |
1302 |
|
} |
1303 |
|
} |
1304 |
|
else |
1305 |
|
{ |
1306 |
|
Trace("cegqi-warn") << "WARNING : No recorded instantiations for " |
1307 |
|
"syntax-guided solution!" |
1308 |
|
<< std::endl; |
1309 |
|
} |
1310 |
|
} |
1311 |
1443 |
sols.push_back(sol); |
1312 |
1443 |
statuses.push_back(status); |
1313 |
|
} |
1314 |
1317 |
return true; |
1315 |
|
} |
1316 |
|
|
1317 |
8474 |
Node SynthConjecture::getSymmetryBreakingPredicate( |
1318 |
|
Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth) |
1319 |
|
{ |
1320 |
16948 |
std::vector<Node> sb_lemmas; |
1321 |
|
|
1322 |
|
// based on simple preprocessing |
1323 |
|
Node ppred = |
1324 |
16948 |
d_ceg_proc->getSymmetryBreakingPredicate(x, e, tn, tindex, depth); |
1325 |
8474 |
if (!ppred.isNull()) |
1326 |
|
{ |
1327 |
|
sb_lemmas.push_back(ppred); |
1328 |
|
} |
1329 |
|
|
1330 |
|
// other static conjecture-dependent symmetry breaking goes here |
1331 |
|
|
1332 |
8474 |
if (!sb_lemmas.empty()) |
1333 |
|
{ |
1334 |
|
return sb_lemmas.size() == 1 |
1335 |
|
? sb_lemmas[0] |
1336 |
|
: NodeManager::currentNM()->mkNode(kind::AND, sb_lemmas); |
1337 |
|
} |
1338 |
|
else |
1339 |
|
{ |
1340 |
8474 |
return Node::null(); |
1341 |
|
} |
1342 |
|
} |
1343 |
|
|
1344 |
18586 |
ExampleEvalCache* SynthConjecture::getExampleEvalCache(Node e) |
1345 |
|
{ |
1346 |
|
std::map<Node, std::unique_ptr<ExampleEvalCache> >::iterator it = |
1347 |
18586 |
d_exampleEvalCache.find(e); |
1348 |
18586 |
if (it != d_exampleEvalCache.end()) |
1349 |
|
{ |
1350 |
18286 |
return it->second.get(); |
1351 |
|
} |
1352 |
600 |
Node f = d_tds->getSynthFunForEnumerator(e); |
1353 |
|
// if f does not have examples, we don't construct the utility |
1354 |
300 |
if (!d_exampleInfer->hasExamples(f) || d_exampleInfer->getNumExamples(f) == 0) |
1355 |
|
{ |
1356 |
172 |
d_exampleEvalCache[e].reset(nullptr); |
1357 |
172 |
return nullptr; |
1358 |
|
} |
1359 |
128 |
d_exampleEvalCache[e].reset(new ExampleEvalCache(d_tds, this, f, e)); |
1360 |
128 |
return d_exampleEvalCache[e].get(); |
1361 |
|
} |
1362 |
|
|
1363 |
|
} // namespace quantifiers |
1364 |
|
} // namespace theory |
1365 |
28191 |
} // namespace cvc5 |