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