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