Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Gereon Kremer, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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/node_algorithm.h"
20 : : #include "expr/skolem_manager.h"
21 : : #include "options/base_options.h"
22 : : #include "options/datatypes_options.h"
23 : : #include "options/quantifiers_options.h"
24 : : #include "printer/printer.h"
25 : : #include "smt/logic_exception.h"
26 : : #include "theory/datatypes/sygus_datatype_utils.h"
27 : : #include "theory/quantifiers/first_order_model.h"
28 : : #include "theory/quantifiers/instantiate.h"
29 : : #include "theory/quantifiers/quantifiers_attributes.h"
30 : : #include "theory/quantifiers/sygus/embedding_converter.h"
31 : : #include "theory/quantifiers/sygus/enum_value_manager.h"
32 : : #include "theory/quantifiers/sygus/print_sygus_to_builtin.h"
33 : : #include "theory/quantifiers/sygus/sygus_enumerator.h"
34 : : #include "theory/quantifiers/sygus/sygus_pbe.h"
35 : : #include "theory/quantifiers/sygus/synth_engine.h"
36 : : #include "theory/quantifiers/sygus/term_database_sygus.h"
37 : : #include "theory/quantifiers/term_util.h"
38 : : #include "theory/rewriter.h"
39 : : #include "theory/smt_engine_subsolver.h"
40 : :
41 : : using namespace cvc5::internal::kind;
42 : : using namespace std;
43 : :
44 : : namespace cvc5::internal {
45 : : namespace theory {
46 : : namespace quantifiers {
47 : :
48 : 7265 : SynthConjecture::SynthConjecture(Env& env,
49 : : QuantifiersState& qs,
50 : : QuantifiersInferenceManager& qim,
51 : : QuantifiersRegistry& qr,
52 : : TermRegistry& tr,
53 : 7265 : SygusStatistics& s)
54 : : : EnvObj(env),
55 : : d_qstate(qs),
56 : : d_qim(qim),
57 : : d_qreg(qr),
58 : : d_treg(tr),
59 : : d_stats(s),
60 : 14530 : d_tds(tr.getTermDatabaseSygus()),
61 : : d_verify(env, d_tds),
62 : : d_hasSolution(false),
63 : : d_computedSolution(false),
64 : 14530 : d_runExprMiner(options().quantifiers.sygusFilterSolMode
65 : 7265 : != options::SygusFilterSolMode::NONE),
66 : 7265 : d_ceg_si(new CegSingleInv(env, tr, s)),
67 : 7265 : d_templInfer(new SygusTemplateInfer(env)),
68 : 7265 : d_ceg_proc(new SynthConjectureProcess(env)),
69 : 7265 : d_embConv(new EmbeddingConverter(env, d_tds, this)),
70 : 7265 : d_sygus_rconst(new SygusRepairConst(env, qim, d_tds)),
71 : 7265 : d_exampleInfer(new ExampleInfer(d_tds)),
72 : 7265 : d_ceg_pbe(new SygusPbe(env, qs, qim, d_tds, this)),
73 : 7265 : d_ceg_cegis(new Cegis(env, qs, qim, d_tds, this)),
74 : 7265 : d_ceg_cegisUnif(new CegisUnif(env, qs, qim, d_tds, this)),
75 : 7265 : d_sygus_ccore(new CegisCoreConnective(env, qs, qim, d_tds, this)),
76 : : d_master(nullptr),
77 : : d_repair_index(0),
78 : 79915 : d_verifyWarned(false)
79 : : {
80 : 7265 : if (options().datatypes.sygusSymBreakPbe
81 [ - + ][ - - ]: 7265 : || options().quantifiers.sygusUnifPbe)
[ + - ]
82 : : {
83 : 7265 : d_modules.push_back(d_ceg_pbe.get());
84 : : }
85 [ + + ]: 7265 : if (options().quantifiers.sygusUnifPi != options::SygusUnifPiMode::NONE)
86 : : {
87 : 45 : d_modules.push_back(d_ceg_cegisUnif.get());
88 : : }
89 [ + + ]: 7265 : if (options().quantifiers.sygusCoreConnective)
90 : : {
91 : 7259 : d_modules.push_back(d_sygus_ccore.get());
92 : : }
93 : 7265 : d_modules.push_back(d_ceg_cegis.get());
94 : 7265 : }
95 : :
96 : 14316 : SynthConjecture::~SynthConjecture() {}
97 : :
98 : 5064 : void SynthConjecture::presolve()
99 : : {
100 : : // If we previously had a solution, block it. Notice that
101 : : // excludeCurrentSolution in the block below ensures we implement a
102 : : // policy where a *new* solution is generated for check-synth if the set of
103 : : // SyGuS constraints has not changed. This call will block solutions for
104 : : // *smart* enumerators only. This behavior makes smart enumeration have
105 : : // a consistent policy with *fast* enumerators, which will generate
106 : : // a new, next solution in their enumeration.
107 [ + + ]: 5064 : if (d_hasSolution)
108 : : {
109 : 205 : excludeCurrentSolution(d_solutionValues.back(),
110 : : InferenceId::QUANTIFIERS_SYGUS_INC_EXCLUDE_CURRENT);
111 : : // we don't have a solution yet
112 : 205 : d_hasSolution = false;
113 : 205 : d_computedSolution = false;
114 : 205 : d_sol.clear();
115 : 205 : d_solStatus.clear();
116 : : }
117 : 5064 : }
118 : :
119 : 1760 : void SynthConjecture::assign(Node q)
120 : : {
121 [ - + ][ - + ]: 1760 : Assert(d_embed_quant.isNull());
[ - - ]
122 [ - + ][ - + ]: 1760 : Assert(q.getKind() == Kind::FORALL);
[ - - ]
123 [ + - ]: 1760 : Trace("cegqi") << "SynthConjecture : assign : " << q << std::endl;
124 : 1760 : d_quant = q;
125 : 1760 : NodeManager* nm = nodeManager();
126 : 1760 : SkolemManager* sm = nm->getSkolemManager();
127 : :
128 : : // pre-simplify the quantified formula based on the process utility
129 : 1760 : d_simp_quant = d_ceg_proc->preSimplify(d_quant);
130 : :
131 : : // compute its attributes
132 : 1760 : QAttributes qa;
133 : 1760 : QuantAttributes::computeQuantAttributes(q, qa);
134 : :
135 : 1760 : Node sc = qa.d_sygusSideCondition;
136 : : // we check whether the conjecture is single invocation if we are marked
137 : : // with the sygus attribute and don't have a side condition
138 [ + - ][ + + ]: 1760 : bool checkSingleInvocation = qa.d_sygus && sc.isNull();
139 : :
140 : 1760 : std::map<Node, Node> templates;
141 : 1760 : std::map<Node, Node> templates_arg;
142 : : // register with single invocation if applicable
143 [ + + ]: 1760 : if (checkSingleInvocation)
144 : : {
145 : 1162 : d_ceg_si->initialize(d_simp_quant);
146 : 1162 : d_simp_quant = d_ceg_si->getSimplifiedConjecture();
147 [ + - ]: 1162 : if (!d_ceg_si->isSingleInvocation())
148 : : {
149 : 1162 : d_templInfer->initialize(d_simp_quant);
150 : : }
151 : : // carry the templates
152 [ + + ]: 2658 : for (const Node& v : q[0])
153 : : {
154 : 2992 : Node templ = d_templInfer->getTemplate(v);
155 [ + + ]: 1496 : if (!templ.isNull())
156 : : {
157 : 48 : templates[v] = templ;
158 : 48 : templates_arg[v] = d_templInfer->getTemplateArg(v);
159 : : }
160 : : }
161 : : }
162 : :
163 : : // post-simplify the quantified formula based on the process utility
164 : 1760 : d_simp_quant = d_ceg_proc->postSimplify(d_simp_quant);
165 : :
166 : : // finished simplifying the quantified formula at this point
167 : :
168 : : // convert to deep embedding and finalize single invocation here
169 : 1760 : d_embed_quant = d_embConv->process(d_simp_quant, templates, templates_arg);
170 [ + - ]: 3520 : Trace("cegqi") << "SynthConjecture : converted to embedding : "
171 : 1760 : << d_embed_quant << std::endl;
172 : :
173 [ + + ]: 1760 : if (!sc.isNull())
174 : : {
175 [ + - ]: 598 : Trace("cegqi-debug") << "Side condition is: " << sc << std::endl;
176 : : // Immediately check if unsat, use lambda returning true for functions
177 : : // to synthesize.
178 : 598 : std::vector<Node> vars;
179 : 598 : std::vector<Node> subs;
180 [ + + ]: 1196 : for (const Node& v : q[0])
181 : : {
182 : 598 : vars.push_back(v);
183 : 1196 : TypeNode vtype = v.getType();
184 : 1187 : Assert(vtype.isBoolean()
185 : : || (vtype.isFunction() && vtype.getRangeType().isBoolean()));
186 : 1196 : Node s = nm->mkConst(true);
187 [ + + ]: 598 : if (vtype.isFunction())
188 : : {
189 : 1178 : std::vector<TypeNode> atypes = vtype.getArgTypes();
190 : 589 : std::vector<Node> lvars;
191 [ + + ]: 1860 : for (const TypeNode& tn : atypes)
192 : : {
193 : 1271 : lvars.push_back(nm->mkBoundVar(tn));
194 : : }
195 : 2356 : s = nm->mkNode(
196 : 1767 : Kind::LAMBDA, nm->mkNode(Kind::BOUND_VAR_LIST, lvars), s);
197 : : }
198 : 598 : subs.push_back(s);
199 : : }
200 : : Node ksc =
201 : 598 : sc.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
202 : 598 : Result r = d_verify.verify(ksc);
203 : : // if infeasible, we are done
204 [ + + ]: 598 : if (r.getStatus() == Result::UNSAT)
205 : : {
206 : 5 : d_qim.lemma(d_quant.negate(),
207 : : InferenceId::QUANTIFIERS_SYGUS_SC_INFEASIBLE);
208 : 5 : return;
209 : : }
210 : : // convert to deep embedding
211 : 593 : d_embedSideCondition = d_embConv->convertToEmbedding(sc);
212 [ + - ]: 1186 : Trace("cegqi") << "SynthConjecture : side condition : "
213 : 593 : << d_embedSideCondition << std::endl;
214 : : }
215 : :
216 : : // we now finalize the single invocation module, based on the syntax
217 : : // restrictions
218 [ + + ]: 1755 : if (checkSingleInvocation)
219 : : {
220 : 1162 : d_ceg_si->finishInit(d_embConv->isSyntaxRestricted());
221 : : }
222 : :
223 [ - + ][ - + ]: 1755 : Assert(d_candidates.empty());
[ - - ]
224 : 1755 : std::vector<Node> vars;
225 [ + + ]: 3844 : for (size_t i = 0, nvars = d_embed_quant[0].getNumChildren(); i < nvars; i++)
226 : : {
227 : 4178 : Node v = d_embed_quant[0][i];
228 : 2089 : vars.push_back(v);
229 : : Node e = sm->mkInternalSkolemFunction(
230 : : InternalSkolemId::QUANTIFIERS_SYNTH_FUN_EMBED,
231 : 4178 : v.getType(),
232 : 12534 : {d_simp_quant[0][i]});
233 : 2089 : d_candidates.push_back(e);
234 : : }
235 [ + - ]: 3510 : Trace("cegqi") << "Base quantified formula is : " << d_embed_quant
236 : 1755 : << std::endl;
237 : : // construct base instantiation
238 : 1755 : Subs bsubs;
239 : 1755 : bsubs.add(vars, d_candidates);
240 : 1755 : d_base_inst = d_tds->rewriteNode(bsubs.apply(d_embed_quant[1]));
241 : 1755 : d_checkBody = d_embed_quant[1];
242 : 5265 : if (d_checkBody.getKind() == Kind::NOT
243 [ + + ][ + + ]: 1755 : && d_checkBody[0].getKind() == Kind::FORALL)
[ + + ][ + + ]
[ - - ]
244 : : {
245 [ + + ]: 3438 : for (const Node& v : d_checkBody[0][0])
246 : : {
247 : 7584 : Node sk = sm->mkDummySkolem("rsk", v.getType());
248 : 2528 : bsubs.add(v, sk);
249 : 2528 : d_innerVars.push_back(v);
250 : 2528 : d_innerSks.push_back(sk);
251 : : }
252 : 910 : d_checkBody = d_checkBody[0][1].negate();
253 : : }
254 : 1755 : d_checkBody = bsubs.apply(d_checkBody);
255 : 1755 : d_checkBody = d_tds->rewriteNode(d_checkBody);
256 [ + + ][ + - ]: 1755 : if (!d_embedSideCondition.isNull() && !vars.empty())
[ + + ]
257 : : {
258 : 1186 : d_embedSideCondition = d_embedSideCondition.substitute(
259 : 593 : vars.begin(), vars.end(), d_candidates.begin(), d_candidates.end());
260 : : }
261 [ + - ]: 1755 : Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl;
262 : :
263 : : // initialize the sygus constant repair utility
264 [ + + ]: 1755 : if (options().quantifiers.sygusRepairConst)
265 : : {
266 : 1747 : d_sygus_rconst->initialize(d_base_inst.negate(), d_candidates);
267 [ - + ]: 1747 : if (options().quantifiers.sygusConstRepairAbort)
268 : : {
269 [ - - ]: 0 : if (!d_sygus_rconst->isActive())
270 : : {
271 : : // no constant repair is possible: abort
272 : 0 : std::stringstream ss;
273 : 0 : ss << "Grammar does not allow repair constants." << std::endl;
274 : 0 : throw LogicException(ss.str());
275 : : }
276 : : }
277 : : }
278 : : // initialize the example inference utility
279 : : // Notice that we must also consider the side condition when inferring
280 : : // whether the conjecture is PBE. This ensures we do not prune solutions
281 : : // that may satisfy the side condition based on equivalence-up-to-examples
282 : : // with solutions that do not.
283 : 1755 : Node conjForExamples = d_base_inst;
284 [ + + ]: 1755 : if (!d_embedSideCondition.isNull())
285 : : {
286 : 593 : conjForExamples = nm->mkNode(Kind::AND, d_embedSideCondition, d_base_inst);
287 : : }
288 [ + - ][ + + ]: 1755 : if (d_exampleInfer!=nullptr && !d_exampleInfer->initialize(conjForExamples, d_candidates))
[ + - ][ + + ]
[ - - ]
289 : : {
290 : : // there is a contradictory example pair, the conjecture is infeasible.
291 : 2 : Node infLem = d_quant.negate();
292 : 2 : d_qim.lemma(infLem, InferenceId::QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA);
293 : : // we don't need to continue initialization in this case
294 : 2 : return;
295 : : }
296 : :
297 : : // register this term with sygus database and other utilities that impact
298 : : // the enumerative sygus search
299 [ + + ]: 1753 : if (!isSingleInvocation())
300 : : {
301 : 1612 : d_ceg_proc->initialize(d_base_inst, d_candidates);
302 [ + - ]: 4368 : for (unsigned i = 0, size = d_modules.size(); i < size; i++)
303 : : {
304 [ + + ]: 4368 : if (d_modules[i]->initialize(d_simp_quant, d_base_inst, d_candidates))
305 : : {
306 : 1612 : d_master = d_modules[i];
307 : 1612 : break;
308 : : }
309 : : }
310 [ - + ][ - + ]: 1612 : Assert(d_master != nullptr);
[ - - ]
311 : : }
312 : :
313 [ - + ][ - + ]: 1753 : Assert(d_qreg.getQuantAttributes().isSygus(q));
[ - - ]
314 : :
315 [ + - ]: 3506 : Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation()
316 : 1753 : << std::endl;
317 : : }
318 : :
319 : :
320 : 119069 : bool SynthConjecture::isSingleInvocation() const
321 : : {
322 : 119069 : return d_ceg_si->isSingleInvocation();
323 : : }
324 : :
325 : 14417 : bool SynthConjecture::needsCheck()
326 : : {
327 : 14417 : return true;
328 : : }
329 : :
330 : 114279 : bool SynthConjecture::doCheck()
331 : : {
332 [ + + ]: 114279 : if (d_hasSolution)
333 : : {
334 : 4 : return true;
335 : : }
336 [ + + ]: 114275 : if (isSingleInvocation())
337 : : {
338 : : // We now try to solve with the single invocation solver, which may or may
339 : : // not succeed in solving the conjecture. In either case, we are done and
340 : : // return true.
341 : 141 : Result res = d_ceg_si->solve();
342 [ + + ]: 141 : if (res.getStatus() == Result::UNSAT)
343 : : {
344 : 129 : d_hasSolution = true;
345 : : // the conjecture has a solution, we set incomplete
346 : 129 : d_qim.setModelUnsound(IncompleteId::QUANTIFIERS_SYGUS_SOLVED);
347 : : }
348 [ + - ]: 12 : else if (res.getStatus() == Result::SAT)
349 : : {
350 : : // the conjecture is definitely infeasible
351 : 12 : d_qim.lemma(d_quant.negate(),
352 : : InferenceId::QUANTIFIERS_SYGUS_SI_INFEASIBLE);
353 : : }
354 : 141 : return true;
355 : : }
356 [ - + ][ - + ]: 114134 : Assert(d_master != nullptr);
[ - - ]
357 : :
358 : : // get the list of terms that the master strategy is interested in
359 : 228268 : std::vector<Node> terms;
360 : 114134 : d_master->getTermList(d_candidates, terms);
361 : :
362 [ - + ][ - + ]: 114134 : Assert(!d_candidates.empty());
[ - - ]
363 : :
364 [ + - ]: 228268 : Trace("sygus-engine-debug")
365 : 114134 : << "CegConjuncture : check, build candidates..." << std::endl;
366 : 228268 : std::vector<Node> candidate_values;
367 : 114134 : bool constructed_cand = false;
368 : :
369 : : // If a module is not trying to repair constants in solutions and the option
370 : : // sygusRepairConst is true, we use a default scheme for trying to repair
371 : : // constants here.
372 : : bool doRepairConst =
373 [ + + ][ + + ]: 114134 : options().quantifiers.sygusRepairConst && !d_master->usingRepairConst();
374 [ + + ]: 114134 : if (doRepairConst)
375 : : {
376 : : // have we tried to repair the previous solution?
377 : : // if not, call the repair constant utility
378 : 11640 : size_t ninst = d_solutionValues.size();
379 [ - + ]: 11640 : if (d_repair_index < ninst)
380 : : {
381 : 0 : std::vector<Node> fail_cvs = d_solutionValues[d_repair_index];
382 [ - - ]: 0 : if (TraceIsOn("sygus-engine"))
383 : : {
384 [ - - ]: 0 : Trace("sygus-engine") << "CegConjuncture : repair previous solution ";
385 [ - - ]: 0 : for (const Node& fc : fail_cvs)
386 : : {
387 : 0 : std::stringstream ss;
388 : 0 : TermDbSygus::toStreamSygus(ss, fc);
389 : 0 : Trace("sygus-engine") << ss.str() << " ";
390 : : }
391 [ - - ]: 0 : Trace("sygus-engine") << std::endl;
392 : : }
393 : 0 : d_repair_index++;
394 [ - - ]: 0 : if (d_sygus_rconst->repairSolution(
395 : 0 : d_candidates, fail_cvs, candidate_values))
396 : : {
397 : 0 : constructed_cand = true;
398 : : }
399 : : }
400 : : else
401 : : {
402 [ + - ]: 11640 : Trace("sygus-engine-debug") << "...no candidates to repair" << std::endl;
403 : : }
404 : : }
405 : : else
406 : : {
407 [ + - ]: 102494 : Trace("sygus-engine-debug") << "...not repairing" << std::endl;
408 : : }
409 : :
410 : 114134 : bool printDebug = isOutputOn(OutputTag::SYGUS);
411 [ + - ]: 114134 : if (!constructed_cand)
412 : : {
413 : : // get the model value of the relevant terms from the master module
414 : 114138 : std::vector<Node> enum_values;
415 : 114134 : bool activeIncomplete = false;
416 : 114134 : bool fullModel = getEnumeratedValues(terms, enum_values, activeIncomplete);
417 : :
418 : : // if the master requires a full model and the model is partial, we fail
419 [ + + ][ + + ]: 114130 : if (!d_master->allowPartialModel() && !fullModel)
[ + + ]
420 : : {
421 : : // we retain the values in d_ev_active_gen_waiting
422 [ + - ]: 56276 : Trace("sygus-engine-debug") << "...partial model, fail." << std::endl;
423 : : // if we are partial due to an active enumerator, we may still succeed
424 : : // on the next call
425 : 56276 : return !activeIncomplete;
426 : : }
427 : : // determine if we had at least one value for an enumerator
428 [ - + ][ - + ]: 57854 : Assert(terms.size() == enum_values.size());
[ - - ]
429 : 57854 : bool modelSuccess = false;
430 [ + + ]: 193840 : for (unsigned i = 0, size = terms.size(); i < size; i++)
431 : : {
432 [ + + ]: 135986 : if (!enum_values[i].isNull())
433 : : {
434 : 123909 : modelSuccess = true;
435 : : }
436 : : }
437 [ + + ]: 57854 : if (modelSuccess)
438 : : {
439 : : // Must separately compute whether trace is on due to compilation of
440 : : // TraceIsOn.
441 : 47517 : bool traceIsOn = TraceIsOn("sygus-engine");
442 [ + + ][ - + ]: 47517 : if (printDebug || traceIsOn)
443 : : {
444 [ + - ]: 4 : Trace("sygus-engine") << " * Value is : ";
445 : 8 : std::stringstream sygusEnumOut;
446 : 4 : FirstOrderModel* m = d_treg.getModel();
447 [ + + ]: 8 : for (unsigned i = 0, size = terms.size(); i < size; i++)
448 : : {
449 : 8 : Node nv = enum_values[i];
450 [ - + ][ - + ]: 8 : Node onv = nv.isNull() ? m->getValue(terms[i]) : nv;
[ - - ]
451 : 8 : TypeNode tn = onv.getType();
452 : 8 : std::stringstream ss;
453 : 4 : TermDbSygus::toStreamSygus(ss, onv);
454 [ + - ]: 4 : if (printDebug)
455 : : {
456 : 4 : sygusEnumOut << " " << ss.str();
457 : : }
458 [ + - ]: 4 : Trace("sygus-engine") << terms[i] << " -> ";
459 [ - + ]: 4 : if (nv.isNull())
460 : : {
461 : 0 : Trace("sygus-engine") << "[EXC: " << ss.str() << "] ";
462 : : }
463 : : else
464 : : {
465 [ + - ][ - + ]: 4 : Trace("sygus-engine") << ss.str() << " ";
[ - - ]
466 [ - + ]: 4 : if (TraceIsOn("sygus-engine-rr"))
467 : : {
468 : 0 : Node bv = d_tds->sygusToBuiltin(nv, tn);
469 : 0 : bv = d_tds->rewriteNode(bv);
470 [ - - ]: 0 : Trace("sygus-engine-rr") << " -> " << bv << std::endl;
471 : : }
472 : : }
473 : : }
474 [ + - ]: 4 : Trace("sygus-engine") << std::endl;
475 [ + - ]: 4 : if (d_env.isOutputOn(OutputTag::SYGUS))
476 : : {
477 : 4 : d_env.output(OutputTag::SYGUS)
478 : 4 : << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl;
479 : : }
480 : : }
481 [ - + ][ - + ]: 47517 : Assert(candidate_values.empty());
[ - - ]
482 : 47517 : constructed_cand = d_master->constructCandidates(
483 : 47517 : terms, enum_values, d_candidates, candidate_values);
484 : : }
485 : : // notify the enumerator managers of the status of the candidate
486 : 139936 : for (std::pair<const Node, std::unique_ptr<EnumValueManager>>& ecp :
487 [ + + ]: 337726 : d_enumManager)
488 : : {
489 : 139936 : ecp.second->notifyCandidate(modelSuccess);
490 : : }
491 : : // if we did not generate a candidate, return now
492 [ + + ]: 57854 : if (!modelSuccess)
493 : : {
494 [ + - ]: 10337 : Trace("sygus-engine-debug") << "...empty model, fail." << std::endl;
495 : 10337 : return !activeIncomplete;
496 : : }
497 : : }
498 : :
499 [ + + ]: 47517 : if (constructed_cand)
500 : : {
501 : : // check the side condition if we constructed a candidate
502 [ + + ]: 4334 : if (!checkSideCondition(candidate_values))
503 : : {
504 : 35 : excludeCurrentSolution(candidate_values,
505 : : InferenceId::QUANTIFIERS_SYGUS_SC_EXCLUDE_CURRENT);
506 [ + - ]: 35 : Trace("sygus-engine") << "...failed side condition" << std::endl;
507 : 35 : return false;
508 : : }
509 : : }
510 : : else
511 : : {
512 : 43183 : return false;
513 : : }
514 : :
515 : : // must get a counterexample to the value of the current candidate
516 : 8598 : Node query;
517 [ - + ]: 4299 : if (TraceIsOn("sygus-engine-debug"))
518 : : {
519 [ - - ]: 0 : Trace("sygus-engine-debug")
520 : 0 : << "CegConjuncture : check candidate : " << std::endl;
521 [ - - ]: 0 : for (unsigned i = 0, size = candidate_values.size(); i < size; i++)
522 : : {
523 [ - - ]: 0 : Trace("sygus-engine-debug") << " " << i << " : " << d_candidates[i]
524 : 0 : << " -> " << candidate_values[i] << std::endl;
525 : : }
526 : : }
527 [ - + ][ - + ]: 4299 : Assert(candidate_values.size() == d_candidates.size());
[ - - ]
528 : 8598 : query = d_checkBody.substitute(d_candidates.begin(),
529 : : d_candidates.end(),
530 : : candidate_values.begin(),
531 : 4299 : candidate_values.end());
532 : 4299 : query = rewrite(query);
533 [ + - ]: 4299 : Trace("sygus-engine-debug") << "Rewritten query is " << query << std::endl;
534 [ + + ]: 4299 : if (expr::hasFreeVar(query))
535 : : {
536 [ + - ]: 12 : Trace("sygus-engine-debug")
537 : 6 : << "Free variable, from fwd-decls?" << std::endl;
538 : 6 : NodeManager* nm = nodeManager();
539 : 12 : std::vector<Node> qconj;
540 : 6 : qconj.push_back(query);
541 : 6 : Subs psubs;
542 [ + + ]: 18 : for (size_t i = 0, size = d_candidates.size(); i < size; i++)
543 : : {
544 : 24 : Node bsol = datatypes::utils::sygusToBuiltin(candidate_values[i], false);
545 : : // convert to lambda
546 : 24 : TypeNode tn = d_candidates[i].getType();
547 : 12 : const DType& dt = tn.getDType();
548 : 24 : Node fvar = d_quant[0][i];
549 : 12 : Node bvl = dt.getSygusVarList();
550 [ + + ]: 12 : if (!bvl.isNull())
551 : : {
552 : : // since we don't have function subtyping, this assertion should only
553 : : // check the return type
554 [ - + ][ - + ]: 8 : Assert(fvar.getType().isFunction());
[ - - ]
555 [ - + ][ - + ]: 8 : Assert(fvar.getType().getRangeType() == bsol.getType());
[ - - ]
556 : 8 : bsol = nm->mkNode(Kind::LAMBDA, bvl, bsol);
557 : : }
558 [ + - ]: 24 : Trace("sygus-engine-debug")
559 : 12 : << "Builtin sol: " << d_quant[0][i] << " -> " << bsol << std::endl;
560 : : // add purifying substitution, in case the dependencies are recusive
561 : 12 : psubs.add(d_quant[0][i]);
562 : : // conjoin higher-order equality
563 : 12 : qconj.push_back(d_quant[0][i].eqNode(bsol));
564 : : }
565 : 6 : query = nm->mkAnd(qconj);
566 : 6 : query = rewrite(psubs.apply(query));
567 : : }
568 : :
569 : : // if we trust the sampling we ran, we terminate now
570 [ + + ]: 4299 : if (options().quantifiers.cegisSample == options::CegisSampleMode::TRUST)
571 : : {
572 : : // we have that the current candidate passed a sample test
573 : : // since we trust sampling in this mode, we assume there is a solution here
574 : : // and set incomplete.
575 : 4 : d_hasSolution = true;
576 : 4 : d_qim.setModelUnsound(IncompleteId::QUANTIFIERS_SYGUS_SOLVED);
577 : 4 : recordSolution(candidate_values);
578 : 4 : return true;
579 : : }
580 : :
581 : : // print the candidate solution for debugging
582 [ + - ][ + + ]: 4295 : if (constructed_cand && printDebug)
583 : : {
584 : 4 : std::ostream& out = output(OutputTag::SYGUS);
585 : 4 : out << "(sygus-candidate ";
586 [ - + ][ - + ]: 4 : Assert(d_quant[0].getNumChildren() == candidate_values.size());
[ - - ]
587 [ + + ]: 8 : for (size_t i = 0, ncands = candidate_values.size(); i < ncands; i++)
588 : : {
589 : 8 : Node v = candidate_values[i];
590 : 4 : out << "(" << d_quant[0][i] << " ";
591 : 4 : TermDbSygus::toStreamSygus(out, v);
592 : 4 : out << ")";
593 : : }
594 : 4 : out << ")" << std::endl;
595 : : }
596 : :
597 : : // Record the solution, which may be falsified below. We require recording
598 : : // here since the result of the satisfiability test may be unknown.
599 : 4295 : recordSolution(candidate_values);
600 : :
601 : 8590 : std::vector<Node> skModel;
602 : 8590 : Result r = d_verify.verify(query, d_innerSks, skModel);
603 : :
604 [ + + ]: 4295 : if (r.getStatus() == Result::SAT)
605 : : {
606 : : // we have a counterexample
607 : 1591 : return processCounterexample(skModel);
608 : : }
609 [ + + ]: 2704 : else if (r.getStatus() != Result::UNSAT)
610 : : {
611 [ + + ]: 116 : if (!d_verifyWarned)
612 : : {
613 : 6 : d_verifyWarned = true;
614 : 6 : std::stringstream ss;
615 : : ss << "Warning: The SyGuS solver failed to verify a canidate solution, "
616 : 6 : "likely due to the base logic being undecidable.";
617 [ + - ]: 6 : if (!options().quantifiers.fullSygusVerify)
618 : : {
619 : : ss << " The option --full-sygus-verify can be used to put more effort "
620 : 6 : "into verifying individual candidate solutions.";
621 : : }
622 : 6 : ss << " Use -q to silence this warning.";
623 [ + - ][ - + ]: 6 : Warning() << ss.str() << std::endl;
[ - - ]
624 : : }
625 : : // In the rare case that the subcall is unknown, we simply exclude the
626 : : // solution, without adding a counterexample point. This should only
627 : : // happen if the quantifier free logic is undecidable.
628 : 116 : excludeCurrentSolution(
629 : : candidate_values,
630 : : InferenceId::QUANTIFIERS_SYGUS_NO_VERIFY_EXCLUDE_CURRENT);
631 : : // We should set refutation unsound, since an "unsat" answer should not be
632 : : // interpreted as "infeasible", which would make a difference in the rare
633 : : // case where e.g. we had a finite grammar and exhausted the grammar.
634 : : // In other words, we are unsound by excluding the current candidate
635 : : // which we could not verify whether or not it was a solution.
636 : 116 : d_qim.setRefutationUnsound(IncompleteId::QUANTIFIERS_SYGUS_NO_VERIFY);
637 : 116 : return false;
638 : : }
639 : : // otherwise we are unsat, and we will process the solution below
640 : :
641 : : // now mark that we have a solution
642 : 2588 : d_hasSolution = true;
643 : 2588 : ++(d_stats.d_solutions);
644 : : // determine if we should filter this solution, e.g. based on expression
645 : : // mining or sygus stream
646 [ + + ]: 2588 : if (runExprMiner())
647 : : {
648 : : // excluded due to expression mining
649 : 895 : excludeCurrentSolution(
650 : : candidate_values,
651 : : InferenceId::QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT);
652 : : // streaming means now we immediately are looking for a new solution
653 : 895 : d_hasSolution = false;
654 : 895 : d_computedSolution = false;
655 : 895 : d_sol.clear();
656 : 895 : d_solStatus.clear();
657 : 895 : return false;
658 : : }
659 : : // We set incomplete and terminate with unknown.
660 : 1693 : d_qim.setModelUnsound(IncompleteId::QUANTIFIERS_SYGUS_SOLVED);
661 : 1693 : return true;
662 : : }
663 : :
664 : 4334 : bool SynthConjecture::checkSideCondition(const std::vector<Node>& cvals)
665 : : {
666 [ + + ]: 4334 : if (d_embedSideCondition.isNull())
667 : : {
668 : 2706 : return true;
669 : : }
670 : 3256 : Node sc = d_embedSideCondition;
671 [ + - ]: 1628 : if (!cvals.empty())
672 : : {
673 : 3256 : sc = sc.substitute(
674 : 1628 : d_candidates.begin(), d_candidates.end(), cvals.begin(), cvals.end());
675 : : }
676 [ + - ]: 1628 : Trace("sygus-engine") << "Check side condition..." << std::endl;
677 : 3256 : Result r = d_verify.verify(sc);
678 [ + - ]: 3256 : Trace("sygus-engine") << "...result of check side condition : " << r
679 : 1628 : << std::endl;
680 [ + + ]: 1628 : if (r == Result::UNSAT)
681 : : {
682 : 35 : return false;
683 : : }
684 [ + - ]: 1593 : Trace("sygus-engine") << "...passed side condition" << std::endl;
685 : 1593 : return true;
686 : : }
687 : :
688 : 1591 : bool SynthConjecture::processCounterexample(const std::vector<Node>& skModel)
689 : : {
690 [ + - ]: 3182 : Trace("cegqi-refine") << "doRefine : Construct refinement lemma..."
691 : 1591 : << std::endl;
692 [ + - ]: 3182 : Trace("cegqi-refine-debug")
693 : 1591 : << " For counterexample skolems : " << d_innerSks << std::endl;
694 : 1591 : Node base_lem = d_checkBody.negate();
695 : :
696 [ - + ][ - + ]: 1591 : Assert(d_innerSks.size() == skModel.size());
[ - - ]
697 : :
698 [ + - ]: 1591 : Trace("cegqi-refine") << "doRefine : substitute..." << std::endl;
699 : 3182 : base_lem = base_lem.substitute(
700 : 1591 : d_innerSks.begin(), d_innerSks.end(), skModel.begin(), skModel.end());
701 [ + - ]: 1591 : Trace("cegqi-refine") << "doRefine : rewrite..." << std::endl;
702 : 1591 : base_lem = d_tds->rewriteNode(base_lem);
703 [ + - ]: 3182 : Trace("cegqi-refine") << "doRefine : register refinement lemma " << base_lem
704 : 1591 : << "..." << std::endl;
705 : 1591 : size_t prevPending = d_qim.numPendingLemmas();
706 : 1591 : d_master->registerRefinementLemma(d_innerSks, base_lem);
707 [ + - ]: 1591 : Trace("cegqi-refine") << "doRefine : finished" << std::endl;
708 : :
709 : : // check if we added a lemma
710 : 1591 : bool addedLemma = d_qim.numPendingLemmas() > prevPending;
711 [ + + ]: 1591 : if (addedLemma)
712 : : {
713 [ + - ]: 1114 : Trace("sygus-engine-debug") << " ...refine candidate." << std::endl;
714 : : }
715 : : else
716 : : {
717 [ + - ]: 954 : Trace("sygus-engine-debug") << " ...(warning) failed to refine candidate, "
718 : 0 : "manually exclude candidate."
719 : 477 : << std::endl;
720 : 954 : std::vector<Node> cvals = d_solutionValues.back();
721 : : // something went wrong, exclude the current candidate
722 : 477 : excludeCurrentSolution(
723 : : cvals, InferenceId::QUANTIFIERS_SYGUS_REPEAT_CEX_EXCLUDE_CURRENT);
724 : : // Note this happens when evaluation is incapable of disproving a candidate
725 : : // for counterexample point c, but satisfiability checking happened to find
726 : : // the the same point c is indeed a true counterexample. It is sound
727 : : // to exclude the candidate in this case.
728 : : }
729 : 3182 : return addedLemma;
730 : : }
731 : :
732 : 1764 : void SynthConjecture::ppNotifyConjecture(Node q)
733 : : {
734 : 1764 : d_ceg_si->ppNotifyConjecture(q);
735 : 1764 : }
736 : :
737 : 114134 : bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n,
738 : : std::vector<Node>& v,
739 : : bool& activeIncomplete)
740 : : {
741 [ + - ]: 114134 : Trace("sygus-engine-debug") << "getEnumeratedValues" << std::endl;
742 : 114138 : std::vector<Node> ncheck = n;
743 : 114134 : n.clear();
744 : 114134 : bool ret = true;
745 [ + + ]: 311056 : for (unsigned i = 0, size = ncheck.size(); i < size; i++)
746 : : {
747 : 196930 : Node e = ncheck[i];
748 : : // if it is not active, we return null
749 : 196930 : Node g = d_tds->getActiveGuardForEnumerator(e);
750 [ + + ]: 196926 : if (!g.isNull())
751 : : {
752 : 106256 : Node gstatus = d_qstate.getValuation().getSatValue(g);
753 [ + - ][ + + ]: 106256 : if (gstatus.isNull() || !gstatus.getConst<bool>())
[ + + ]
754 : : {
755 [ + - ]: 660 : Trace("sygus-engine-debug")
756 : 330 : << "Enumerator " << e << " is inactive." << std::endl;
757 : 330 : continue;
758 : : }
759 : : }
760 : 196596 : EnumValueManager* eman = getEnumValueManagerFor(e);
761 [ + - ]: 196596 : Trace("sygus-engine-debug2") << "- get value for " << e << std::endl;
762 : 196596 : Node nv = eman->getEnumeratedValue(activeIncomplete);
763 [ + - ]: 196592 : Trace("sygus-engine-debug2") << " ...return " << nv << std::endl;
764 : 196592 : n.push_back(e);
765 : 196592 : v.push_back(nv);
766 [ + + ][ + + ]: 196592 : ret = ret && !nv.isNull();
767 : : }
768 : 228260 : return ret;
769 : : }
770 : :
771 : 245640 : EnumValueManager* SynthConjecture::getEnumValueManagerFor(Node e)
772 : : {
773 : : std::map<Node, std::unique_ptr<EnumValueManager>>::iterator it =
774 : 245640 : d_enumManager.find(e);
775 [ + + ]: 245640 : if (it != d_enumManager.end())
776 : : {
777 : 243662 : return it->second.get();
778 : : }
779 : : // otherwise, allocate it
780 : 1978 : Node f = d_tds->getSynthFunForEnumerator(e);
781 [ + + ][ - - ]: 3956 : bool hasExamples = (d_exampleInfer != nullptr && d_exampleInfer->hasExamples(f)
782 [ + - ][ + + ]: 3956 : && d_exampleInfer->getNumExamples(f) != 0);
[ + + ][ + - ]
[ - - ]
783 : 3956 : d_enumManager[e].reset(new EnumValueManager(
784 : 1978 : d_env, d_qstate, d_qim, d_treg, d_stats, e, hasExamples));
785 : 1978 : EnumValueManager* eman = d_enumManager[e].get();
786 : : // set up the examples
787 [ + + ]: 1978 : if (hasExamples)
788 : : {
789 : 589 : ExampleEvalCache* eec = eman->getExampleEvalCache();
790 [ - + ][ - + ]: 589 : Assert(eec != nullptr);
[ - - ]
791 [ + + ]: 1904 : for (unsigned i = 0, nex = d_exampleInfer->getNumExamples(f); i < nex; i++)
792 : : {
793 : 2630 : std::vector<Node> input;
794 : 1315 : d_exampleInfer->getExample(f, i, input);
795 : 1315 : eec->addExample(input);
796 : : }
797 : : }
798 : 1978 : return eman;
799 : : }
800 : :
801 : 1487 : ExpressionMinerManager* SynthConjecture::getExprMinerManagerFor(Node e)
802 : : {
803 [ + + ]: 1487 : if (!d_runExprMiner)
804 : : {
805 : 8 : return nullptr;
806 : : }
807 : : std::map<Node, std::unique_ptr<ExpressionMinerManager>>::iterator its =
808 : 1479 : d_exprm.find(e);
809 [ + + ]: 1479 : if (its != d_exprm.end())
810 : : {
811 : 968 : return its->second.get();
812 : : }
813 : 511 : d_exprm[e].reset(new ExpressionMinerManager(d_env));
814 : 511 : ExpressionMinerManager* emm = d_exprm[e].get();
815 : 511 : emm->initializeSygus(e.getType());
816 : 511 : return emm;
817 : : }
818 : :
819 : 25678 : Node SynthConjecture::getModelValue(Node n)
820 : : {
821 [ + - ]: 25678 : Trace("cegqi-mv") << "getModelValue for : " << n << std::endl;
822 : 25678 : return d_treg.getModel()->getValue(n);
823 : : }
824 : :
825 : 0 : void SynthConjecture::debugPrint(const char* c)
826 : : {
827 [ - - ]: 0 : Trace(c) << "Synthesis conjecture : " << d_embed_quant << std::endl;
828 [ - - ]: 0 : Trace(c) << " * Candidate programs : " << d_candidates << std::endl;
829 [ - - ]: 0 : Trace(c) << " * Counterexample skolems : " << d_innerSks << std::endl;
830 : 0 : }
831 : :
832 : 1728 : void SynthConjecture::excludeCurrentSolution(const std::vector<Node>& values,
833 : : InferenceId id)
834 : : {
835 [ - + ][ - + ]: 1728 : Assert(values.size() == d_candidates.size());
[ - - ]
836 [ + - ]: 1728 : Trace("cegqi-debug") << "Exclude current solution: " << values << std::endl;
837 : : // However, we need to exclude the current solution using an explicit
838 : : // blocking clause, so that we proceed to the next solution. We do this only
839 : : // for passively-generated enumerators (TermDbSygus::isPassiveEnumerator).
840 : 1728 : std::vector<Node> exp;
841 [ + + ]: 1890 : for (size_t i = 0, tsize = d_candidates.size(); i < tsize; i++)
842 : : {
843 : 1734 : Node cprog = d_candidates[i];
844 [ - + ][ - + ]: 1734 : Assert(d_tds->isEnumerator(cprog));
[ - - ]
845 [ + + ]: 1734 : if (!d_tds->isPassiveEnumerator(cprog))
846 : : {
847 : : // If any candidate is actively generated, then we should not add the
848 : : // lemma below. We never mix fast and smart enumerators.
849 : 1572 : return;
850 : : }
851 : 162 : Node cval = values[i];
852 : : // add to explanation of exclusion
853 : 162 : d_tds->getExplain()->getExplanationForEquality(cprog, cval, exp);
854 : : }
855 [ + - ]: 156 : if (!exp.empty())
856 : : {
857 : : Node exc_lem =
858 [ + + ]: 156 : exp.size() == 1 ? exp[0] : nodeManager()->mkNode(Kind::AND, exp);
859 : 156 : exc_lem = exc_lem.negate();
860 [ + - ]: 312 : Trace("cegqi-lemma") << "Cegqi::Lemma : exclude current solution : "
861 : 156 : << exc_lem << " by " << id << std::endl;
862 : 156 : d_qim.lemma(exc_lem, id);
863 : : }
864 : : }
865 : :
866 : 2588 : bool SynthConjecture::runExprMiner()
867 : : {
868 : : // if not using expression mining and sygus stream
869 [ + + ][ + + ]: 2588 : if (!d_runExprMiner && !options().quantifiers.sygusStream)
[ + + ]
870 : : {
871 : 1101 : return false;
872 : : }
873 [ + - ]: 1487 : Trace("cegqi-sol-debug") << "Run expression mining..." << std::endl;
874 [ - + ][ - + ]: 1487 : Assert(d_quant[0].getNumChildren() == d_embed_quant[0].getNumChildren());
[ - - ]
875 : 2974 : std::vector<Node> sols;
876 : 2974 : std::vector<int8_t> statuses;
877 [ - + ]: 1487 : if (!getSynthSolutionsInternal(sols, statuses))
878 : : {
879 : 0 : return false;
880 : : }
881 : : // always exclude if sygus stream is enabled
882 : 1487 : bool doExclude = options().quantifiers.sygusStream;
883 : 1487 : NodeManager* nm = nodeManager();
884 : 1487 : std::ostream& out = options().base.out;
885 [ + + ]: 2974 : for (size_t i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
886 : : {
887 : 1487 : Node sol = sols[i];
888 [ - + ]: 1487 : if (sol.isNull())
889 : : {
890 : : // failed to reconstruct to syntax, skip
891 : 0 : continue;
892 : : }
893 : 1487 : Node e = d_embed_quant[0][i];
894 : 1487 : int8_t status = statuses[i];
895 : : // run expression mining
896 [ + - ]: 1487 : if (status != 0)
897 : : {
898 : 1487 : ExpressionMinerManager* emm = getExprMinerManagerFor(e);
899 [ + + ]: 1487 : if (emm != nullptr)
900 : : {
901 : 1479 : bool ret = emm->addTerm(sol);
902 [ + + ]: 1479 : if (!ret)
903 : : {
904 : : // count the number of filtered solutions
905 : 861 : ++(d_stats.d_filtered_solutions);
906 : : // if any term is excluded due to mining, its output is excluded
907 : : // from sygus stream, and the entire solution is excluded.
908 : 861 : doExclude = true;
909 : 861 : continue;
910 : : }
911 : : }
912 : : }
913 : : // print to stream
914 [ + + ]: 626 : if (options().quantifiers.sygusStream)
915 : : {
916 : 68 : TypeNode tn = e.getType();
917 : 34 : const DType& dt = tn.getDType();
918 : 68 : std::stringstream ss;
919 : 34 : ss << e;
920 : 68 : std::string f(ss.str());
921 : 34 : f.erase(f.begin());
922 : 34 : out << "(define-fun " << f << " ";
923 : : // Only include variables that are truly bound variables of the
924 : : // function-to-synthesize. This means we exclude variables that encode
925 : : // external terms. This ensures that --sygus-stream prints
926 : : // solutions with no arguments on the predicate for responses to
927 : : // the get-abduct command.
928 : : // pvs stores the variables that will be printed in the argument list
929 : : // below.
930 : 68 : std::vector<Node> pvs;
931 : 68 : Node vl = dt.getSygusVarList();
932 [ + - ]: 34 : if (!vl.isNull())
933 : : {
934 [ - + ][ - + ]: 34 : Assert(vl.getKind() == Kind::BOUND_VAR_LIST);
[ - - ]
935 : : SygusVarToTermAttribute sta;
936 [ + + ]: 154 : for (const Node& v : vl)
937 : : {
938 [ + + ]: 120 : if (!v.hasAttribute(sta))
939 : : {
940 : 16 : pvs.push_back(v);
941 : : }
942 : : }
943 : : }
944 [ + + ]: 34 : if (pvs.empty())
945 : : {
946 : 26 : out << "() ";
947 : : }
948 : : else
949 : : {
950 : 8 : vl = nm->mkNode(Kind::BOUND_VAR_LIST, pvs);
951 : 8 : out << vl << " ";
952 : : }
953 : 34 : out << dt.getSygusType() << " ";
954 [ - + ]: 34 : if (status == 0)
955 : : {
956 : 0 : out << sol;
957 : : }
958 : : else
959 : : {
960 : 34 : Node bsol = datatypes::utils::sygusToBuiltin(sol, true);
961 : 34 : out << bsol;
962 : : }
963 : 34 : out << ")" << std::endl;
964 : : }
965 : : }
966 : 1487 : return doExclude;
967 : : }
968 : :
969 : 2718 : bool SynthConjecture::getSynthSolutions(
970 : : std::map<Node, std::map<Node, Node> >& sol_map)
971 : : {
972 : 2718 : NodeManager* nm = nodeManager();
973 : 5436 : std::vector<Node> sols;
974 : 5436 : std::vector<int8_t> statuses;
975 [ + - ]: 2718 : Trace("cegqi-debug") << "getSynthSolutions..." << std::endl;
976 [ + + ]: 2718 : if (!getSynthSolutionsInternal(sols, statuses))
977 : : {
978 [ + - ]: 135 : Trace("cegqi-debug") << "...failed internal" << std::endl;
979 : 135 : return false;
980 : : }
981 : : // we add it to the solution map, indexed by this conjecture
982 : 2583 : std::map<Node, Node>& smc = sol_map[d_quant];
983 [ + + ]: 5490 : for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
984 : : {
985 : 5814 : Node sol = sols[i];
986 : 2907 : int8_t status = statuses[i];
987 [ + - ]: 5814 : Trace("cegqi-debug") << "...got " << i << ": " << sol
988 : 2907 : << ", status=" << status << std::endl;
989 : : // get the builtin solution
990 : 5814 : Node bsol = sol;
991 [ + + ]: 2907 : if (status != 0)
992 : : {
993 : : // Convert sygus to builtin here.
994 : : // We must use the external representation to ensure bsol matches the
995 : : // grammar.
996 : 2559 : bsol = datatypes::utils::sygusToBuiltin(sol, true);
997 : : }
998 : : // convert to lambda
999 : 8721 : TypeNode tn = d_embed_quant[0][i].getType();
1000 : 2907 : const DType& dt = tn.getDType();
1001 : 5814 : Node fvar = d_quant[0][i];
1002 : 2907 : Node bvl = dt.getSygusVarList();
1003 [ + + ]: 2907 : if (!bvl.isNull())
1004 : : {
1005 : : // since we don't have function subtyping, this assertion should only
1006 : : // check the return type
1007 [ - + ][ - + ]: 1983 : Assert(fvar.getType().isFunction());
[ - - ]
1008 [ - + ][ - + ]: 1983 : Assert(fvar.getType().getRangeType() == bsol.getType());
[ - - ]
1009 : 1983 : bsol = nm->mkNode(Kind::LAMBDA, bvl, bsol);
1010 : : }
1011 : : else
1012 : : {
1013 [ - + ][ - + ]: 924 : Assert(fvar.getType() == bsol.getType());
[ - - ]
1014 : : }
1015 : : // store in map
1016 : 2907 : smc[fvar] = bsol;
1017 [ + - ]: 2907 : Trace("cegqi-debug") << "...return " << bsol << std::endl;
1018 : : }
1019 : 2583 : return true;
1020 : : }
1021 : :
1022 : 4299 : void SynthConjecture::recordSolution(const std::vector<Node>& vs)
1023 : : {
1024 [ - + ][ - + ]: 4299 : Assert(vs.size() == d_candidates.size());
[ - - ]
1025 : 4299 : d_solutionValues.clear();
1026 : 4299 : d_solutionValues.push_back(vs);
1027 : 4299 : }
1028 : :
1029 : 4205 : bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
1030 : : std::vector<int8_t>& statuses)
1031 : : {
1032 [ + + ]: 4205 : if (!d_hasSolution)
1033 : : {
1034 : 131 : return false;
1035 : : }
1036 [ + + ]: 4074 : if (d_computedSolution)
1037 : : {
1038 : 1353 : sols.insert(sols.end(), d_sol.begin(), d_sol.end());
1039 : 1353 : statuses.insert(statuses.end(), d_solStatus.begin(), d_solStatus.end());
1040 : 1353 : return true;
1041 : : }
1042 : 2721 : d_computedSolution = true;
1043 : : // get the (SyGuS datatype) values of the solutions, if they exist
1044 : 5442 : std::vector<Node> svals;
1045 [ + + ]: 2721 : if (!d_solutionValues.empty())
1046 : : {
1047 : 2592 : svals = d_solutionValues.back();
1048 : : }
1049 [ + + ]: 5758 : for (size_t i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
1050 : : {
1051 : 3041 : Node prog = d_embed_quant[0][i];
1052 [ + - ]: 3041 : Trace("cegqi-debug") << " get solution for " << prog << std::endl;
1053 : 3041 : TypeNode tn = prog.getType();
1054 [ - + ][ - + ]: 3041 : Assert(tn.isDatatype());
[ - - ]
1055 : : // get the solution
1056 : 3041 : Node sol;
1057 : 3041 : int8_t status = -1;
1058 [ + + ]: 3041 : if (isSingleInvocation())
1059 : : {
1060 [ - + ][ - + ]: 359 : Assert(d_ceg_si != NULL);
[ - - ]
1061 : 359 : sol = d_ceg_si->getSolution(i, tn, status, true);
1062 [ + + ]: 359 : if (sol.isNull())
1063 : : {
1064 : 4 : return false;
1065 : : }
1066 [ + + ]: 355 : sol = sol.getKind() == Kind::LAMBDA ? sol[1] : sol;
1067 : : }
1068 : : else
1069 : : {
1070 : 5364 : Node cprog = d_candidates[i];
1071 [ + - ]: 2682 : if (!svals.empty())
1072 : : {
1073 : : // the solution is the value of the last term
1074 : 2682 : sol = svals[i];
1075 : 2682 : status = 1;
1076 : :
1077 : : // check if there was a template
1078 : 5364 : Node sf = d_quant[0][i];
1079 : 5364 : Node templ = d_templInfer->getTemplate(sf);
1080 [ + + ]: 2682 : if (!templ.isNull())
1081 : : {
1082 [ + - ]: 66 : Trace("cegqi-inv-debug")
1083 : 33 : << sf << " used template : " << templ << std::endl;
1084 : 99 : TNode templa = d_templInfer->getTemplateArg(sf);
1085 : : // make the builtin version of the full solution
1086 : 33 : sol = d_tds->sygusToBuiltin(sol, sol.getType());
1087 [ + - ]: 66 : Trace("cegqi-inv") << "Builtin version of solution is : " << sol
1088 [ - + ][ - - ]: 33 : << ", type : " << sol.getType() << std::endl;
1089 : 33 : TNode tsol = sol;
1090 : 33 : sol = templ.substitute(templa, tsol);
1091 [ + - ]: 33 : Trace("cegqi-inv-debug") << "With template : " << sol << std::endl;
1092 : 33 : sol = rewrite(sol);
1093 [ + - ]: 33 : Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl;
1094 : : // now, reconstruct to the syntax
1095 : 33 : sol = d_ceg_si->reconstructToSyntax(sol, tn, status, true);
1096 [ - + ]: 33 : sol = sol.getKind() == Kind::LAMBDA ? sol[1] : sol;
1097 [ + - ]: 66 : Trace("cegqi-inv-debug")
1098 : 33 : << "Reconstructed to syntax : " << sol << std::endl;
1099 : : }
1100 : : else
1101 : : {
1102 [ + - ]: 5298 : Trace("cegqi-inv-debug")
1103 : 2649 : << sf << " did not use template" << std::endl;
1104 : : }
1105 : : }
1106 : : else
1107 : : {
1108 [ - - ]: 0 : Trace("cegqi-warn") << "WARNING : No recorded instantiations for "
1109 : 0 : "syntax-guided solution!"
1110 : 0 : << std::endl;
1111 : : }
1112 : : }
1113 : 3037 : d_sol.push_back(sol);
1114 : 3037 : d_solStatus.push_back(status);
1115 : : // Note that this assumes that the name of the resulting datatype matches
1116 : : // the original name from the user. This is usually the case, although
1117 : : // if grammar normalization is used, it is not. If it is not, the names
1118 : : // in the annotation will not match, but no failures will occur.
1119 : : // Also note that we do not print annotations if the solution was not
1120 : : // reconstructed to the grammar (status != 1), which is the case if the
1121 : : // grammar is ignored by single invocation above. On the other hand,
1122 : : // annotations will be printed correctly if the solution was successfully
1123 : : // reconstructed by single invocation (status == 1).
1124 [ + + ][ + - ]: 3037 : if (isOutputOn(OutputTag::SYGUS_SOL_GTERM) && status == 1)
[ + + ]
1125 : : {
1126 : 2 : Node psol = getPrintableSygusToBuiltin(sol);
1127 : 2 : d_env.output(OutputTag::SYGUS_SOL_GTERM)
1128 : 4 : << "(sygus-sol-gterm (" << d_quant[0][i] << " " << psol << "))"
1129 : 2 : << std::endl;
1130 : : }
1131 : : }
1132 : 2717 : sols.insert(sols.end(), d_sol.begin(), d_sol.end());
1133 : 2717 : statuses.insert(statuses.end(), d_solStatus.begin(), d_solStatus.end());
1134 : 2717 : return true;
1135 : : }
1136 : :
1137 : 18622 : Node SynthConjecture::getSymmetryBreakingPredicate(
1138 : : Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth)
1139 : : {
1140 : 37244 : std::vector<Node> sb_lemmas;
1141 : :
1142 : : // based on simple preprocessing
1143 : : Node ppred =
1144 : 55866 : d_ceg_proc->getSymmetryBreakingPredicate(x, e, tn, tindex, depth);
1145 [ - + ]: 18622 : if (!ppred.isNull())
1146 : : {
1147 : 0 : sb_lemmas.push_back(ppred);
1148 : : }
1149 : :
1150 : : // other static conjecture-dependent symmetry breaking goes here
1151 : :
1152 [ - + ]: 18622 : if (!sb_lemmas.empty())
1153 : : {
1154 : 0 : return sb_lemmas.size() == 1 ? sb_lemmas[0]
1155 [ - - ]: 0 : : nodeManager()->mkNode(Kind::AND, sb_lemmas);
1156 : : }
1157 : : else
1158 : : {
1159 : 18622 : return Node::null();
1160 : : }
1161 : : }
1162 : :
1163 : 49044 : ExampleEvalCache* SynthConjecture::getExampleEvalCache(Node e)
1164 : : {
1165 : 49044 : EnumValueManager* eman = getEnumValueManagerFor(e);
1166 : 49044 : return eman->getExampleEvalCache();
1167 : : }
1168 : :
1169 : : } // namespace quantifiers
1170 : : } // namespace theory
1171 : : } // namespace cvc5::internal
|
