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 cegis.
11 : : */
12 : :
13 : : #include "theory/quantifiers/sygus/cegis.h"
14 : :
15 : : #include "expr/node_algorithm.h"
16 : : #include "options/base_options.h"
17 : : #include "options/quantifiers_options.h"
18 : : #include "printer/printer.h"
19 : : #include "theory/quantifiers/sygus/example_min_eval.h"
20 : : #include "theory/quantifiers/sygus/synth_conjecture.h"
21 : : #include "theory/quantifiers/sygus/term_database_sygus.h"
22 : : #include "theory/rewriter.h"
23 : :
24 : : using namespace std;
25 : : using namespace cvc5::internal::kind;
26 : : using namespace cvc5::context;
27 : :
28 : : namespace cvc5::internal {
29 : : namespace theory {
30 : : namespace quantifiers {
31 : :
32 : 11265 : Cegis::Cegis(Env& env,
33 : : QuantifiersState& qs,
34 : : QuantifiersInferenceManager& qim,
35 : : TermDbSygus* tds,
36 : 11265 : SynthConjecture* p)
37 : : : SygusModule(env, qs, qim, tds, p),
38 : 22530 : d_eval_unfold(tds->getEvalUnfold()),
39 : 11265 : d_cexClosedEnum(false),
40 : 11265 : d_cegis_sampler(env),
41 : 11265 : d_usingSymCons(false),
42 : 22530 : d_doEvalUnfold(false)
43 : : {
44 : 11265 : }
45 : :
46 : 744 : bool Cegis::initialize(Node conj, Node n, const std::vector<Node>& candidates)
47 : : {
48 : 744 : d_base_body = n;
49 : 744 : d_cexClosedEnum = true;
50 : 2232 : if (d_base_body.getKind() == Kind::NOT
51 [ + + ][ + + ]: 744 : && d_base_body[0].getKind() == Kind::FORALL)
[ + + ][ + + ]
[ - - ]
52 : : {
53 [ + + ]: 2149 : for (const Node& v : d_base_body[0][0])
54 : : {
55 : 1674 : d_base_vars.push_back(v);
56 [ + + ]: 1674 : if (!v.getType().isClosedEnumerable())
57 : : {
58 : : // not closed enumerable, refinement lemmas cannot be sent to the
59 : : // quantifier-free datatype solver
60 : 81 : d_cexClosedEnum = false;
61 : : }
62 : 2149 : }
63 : 475 : d_base_body = d_base_body[0][1];
64 : : }
65 : :
66 : : // assign the cegis sampler if applicable
67 [ + + ]: 744 : if (options().quantifiers.cegisSample != options::CegisSampleMode::NONE)
68 : : {
69 [ + - ]: 30 : Trace("cegis-sample") << "Initialize sampler for " << d_base_body << "..."
70 : 15 : << std::endl;
71 : 15 : TypeNode bt = d_base_body.getType();
72 : 15 : d_cegis_sampler.initialize(
73 : 15 : bt, d_base_vars, options().quantifiers.sygusSamples);
74 : 15 : }
75 [ - + ][ - + ]: 744 : Assert(conj.getKind() == Kind::FORALL);
[ - - ]
76 [ - + ][ - + ]: 744 : Assert(conj[0].getNumChildren() == candidates.size());
[ - - ]
77 : : // construct the substitution d_euSubs if evaluation unfolding is enabled.
78 : 744 : if (options().quantifiers.sygusEvalUnfoldMode
79 [ + - ]: 744 : != options::SygusEvalUnfoldMode::NONE)
80 : : {
81 : 744 : d_doEvalUnfold = true;
82 : 744 : NodeManager* nm = nodeManager();
83 [ + + ]: 1686 : for (size_t i = 0, nvars = conj[0].getNumChildren(); i < nvars; i++)
84 : : {
85 : 950 : TypeNode tn = candidates[i].getType();
86 : 950 : SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
87 : 950 : const std::vector<Node>& vars = ti.getVarList();
88 : 950 : std::vector<Node> vs;
89 [ + + ]: 2606 : for (const Node& v : vars)
90 : : {
91 : 1656 : vs.push_back(NodeManager::mkBoundVar(v.getType()));
92 : : }
93 : 950 : std::vector<Node> eargs;
94 : 950 : eargs.push_back(candidates[i]);
95 : 950 : Node ret;
96 [ + + ]: 950 : if (!vs.empty())
97 : : {
98 : 708 : Node lvl = nm->mkNode(Kind::BOUND_VAR_LIST, vs);
99 : 708 : eargs.insert(eargs.end(), vs.begin(), vs.end());
100 : 1416 : ret = nm->mkNode(
101 : 2124 : Kind::LAMBDA, lvl, nm->mkNode(Kind::DT_SYGUS_EVAL, eargs));
102 : 708 : }
103 : : else
104 : : {
105 : 242 : ret = nm->mkNode(Kind::DT_SYGUS_EVAL, eargs);
106 : : }
107 : 950 : TypeNode rt = ret.getType();
108 [ + + ][ + + ]: 950 : if (rt.isRegExp() || (rt.isFunction() && rt.getRangeType().isRegExp()))
[ - + ][ + + ]
[ + + ][ - - ]
109 : : {
110 : : // cannot do evaluation unfolding for regular expressions
111 : 8 : d_doEvalUnfold = false;
112 : 8 : break;
113 : : }
114 : 942 : d_euSubs.add(conj[0][i], ret);
115 [ + + ][ + + ]: 982 : }
[ + + ][ + + ]
[ + + ]
116 : : }
117 : 744 : return processInitialize(conj, n, candidates);
118 : : }
119 : :
120 : 390 : bool Cegis::processInitialize(Node conj,
121 : : CVC5_UNUSED Node n,
122 : : const std::vector<Node>& candidates)
123 : : {
124 [ + - ]: 390 : Trace("cegis") << "Initialize cegis..." << std::endl;
125 : 390 : size_t csize = candidates.size();
126 : : // The role of enumerators is to be either the single solution or part of
127 : : // a solution involving multiple enumerators.
128 : 390 : EnumeratorRole erole =
129 [ + + ]: 390 : csize == 1 ? ROLE_ENUM_SINGLE_SOLUTION : ROLE_ENUM_MULTI_SOLUTION;
130 : : // initialize an enumerator for each candidate
131 : 390 : std::vector<Node> activeGuards;
132 [ + + ]: 880 : for (size_t i = 0; i < csize; i++)
133 : : {
134 [ + - ]: 490 : Trace("cegis") << "...register enumerator " << candidates[i];
135 : : // We use symbolic constants if we are doing repair constants or if the
136 : : // grammar construction was not simple.
137 : 490 : if (options().quantifiers.sygusRepairConst
138 [ + + ][ - + ]: 490 : || options().quantifiers.sygusGrammarConsMode
[ + + ]
139 : : != options::SygusGrammarConsMode::SIMPLE)
140 : : {
141 : 478 : TypeNode ctn = candidates[i].getType();
142 : 478 : d_tds->registerSygusType(ctn);
143 : 478 : SygusTypeInfo& cti = d_tds->getTypeInfo(ctn);
144 [ + + ]: 478 : if (cti.hasSubtermSymbolicCons())
145 : : {
146 : : // remember that we are using symbolic constructors
147 : 49 : d_usingSymCons = true;
148 [ + - ]: 49 : Trace("cegis") << " (using symbolic constructors)";
149 : : }
150 : 478 : }
151 [ + - ]: 490 : Trace("cegis") << std::endl;
152 : 490 : Node e = candidates[i];
153 : 490 : d_tds->registerEnumerator(e, e, d_parent, erole);
154 : 490 : Node g = d_tds->getActiveGuardForEnumerator(e);
155 [ + + ]: 490 : if (!g.isNull())
156 : : {
157 : 248 : activeGuards.push_back(g);
158 : : }
159 : 490 : }
160 [ + + ]: 390 : if (!activeGuards.empty())
161 : : {
162 : : // This lemma has the semantics "if the conjecture holds, then there must
163 : : // be another value to enumerate for each function to synthesize". Note
164 : : // that active guards are only assigned for "actively generated"
165 : : // enumerators, e.g. when using sygus-enum=fast. Thus, this lemma is
166 : : // typically only added for single function conjectures.
167 : : // This lemma allows us to answer infeasible when we run out of values (for
168 : : // finite grammars).
169 : 248 : NodeManager* nm = nodeManager();
170 : 496 : Node enumLem = nm->mkNode(Kind::IMPLIES, conj, nm->mkAnd(activeGuards));
171 : 248 : d_qim.lemma(enumLem, InferenceId::QUANTIFIERS_SYGUS_COMPLETE_ENUM);
172 : 248 : }
173 : 390 : return true;
174 : 390 : }
175 : :
176 : 93401 : void Cegis::getTermList(const std::vector<Node>& candidates,
177 : : std::vector<Node>& enums)
178 : : {
179 : 93401 : enums.insert(enums.end(), candidates.begin(), candidates.end());
180 : 93401 : }
181 : :
182 : 43538 : bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
183 : : const std::vector<Node>& candidate_values)
184 : : {
185 : : // First, decide if this call will apply "conjecture-specific refinement".
186 : : // In other words, in some settings, the following method will identify and
187 : : // block a class of solutions {candidates -> S} that generalizes the current
188 : : // one (given by {candidates -> candidate_values}), such that for each
189 : : // candidate_values' in S, we have that {candidates -> candidate_values'} is
190 : : // also not a solution for the given conjecture. We may not
191 : : // apply this form of refinement if any (relevant) enumerator in candidates is
192 : : // "actively generated" (see TermDbSygs::isPassiveEnumerator), since its
193 : : // model values are themselves interpreted as classes of solutions.
194 : 43538 : bool doGen = true;
195 [ + + ]: 128318 : for (const Node& v : candidates)
196 : : {
197 : : // if it is relevant to refinement
198 [ + + ]: 119442 : if (d_refinement_lemma_vars.find(v) != d_refinement_lemma_vars.end())
199 : : {
200 [ + + ]: 108748 : if (!d_tds->isPassiveEnumerator(v))
201 : : {
202 : 34662 : doGen = false;
203 : 34662 : break;
204 : : }
205 : : }
206 : : }
207 : 43538 : NodeManager* nm = nodeManager();
208 : 43538 : bool addedEvalLemmas = false;
209 : : // Refinement evaluation should not be done for grammars with symbolic
210 : : // constructors.
211 [ + + ]: 43538 : if (!d_usingSymCons)
212 : : {
213 [ + - ]: 86442 : Trace("sygus-engine") << " *** Do refinement lemma evaluation"
214 [ - - ]: 43221 : << (doGen ? " with conjecture-specific refinement"
215 : 0 : : "")
216 : 43221 : << "..." << std::endl;
217 : : // see if any refinement lemma is refuted by evaluation
218 [ + + ]: 43221 : if (doGen)
219 : : {
220 : 8741 : std::vector<Node> cre_lems;
221 : 8741 : getRefinementEvalLemmas(candidates, candidate_values, cre_lems);
222 [ + + ]: 8741 : if (!cre_lems.empty())
223 : : {
224 [ + + ]: 9044 : for (const Node& cl : cre_lems)
225 : : {
226 : 5258 : d_qim.addPendingLemma(cl, InferenceId::QUANTIFIERS_SYGUS_REFINE_EVAL);
227 : : }
228 : 3786 : addedEvalLemmas = true;
229 : : /* we could, but do not return here. experimentally, it is better to
230 : : add the lemmas below as well, in parallel. */
231 : : }
232 : 8741 : }
233 : : else
234 : : {
235 : : // just check whether the refinement lemmas are satisfied, fail if not
236 [ + + ]: 34480 : if (checkRefinementEvalLemmas(candidates, candidate_values))
237 : : {
238 [ + - ]: 67458 : Trace("sygus-engine") << "...(actively enumerated) candidate failed "
239 : 0 : "refinement lemma evaluation."
240 : 33729 : << std::endl;
241 : 33729 : return true;
242 : : }
243 : : }
244 : : }
245 : : // we only do evaluation unfolding for passive enumerators
246 [ + + ][ + + ]: 9809 : bool doEvalUnfold = (doGen && d_doEvalUnfold);
247 [ + + ]: 9809 : if (doEvalUnfold)
248 : : {
249 [ + - ]: 8872 : Trace("sygus-engine") << " *** Do evaluation unfolding..." << std::endl;
250 : 8872 : std::vector<Node> eager_terms, eager_vals, eager_exps;
251 [ + + ]: 93648 : for (unsigned i = 0, size = candidates.size(); i < size; ++i)
252 : : {
253 [ + - ]: 169552 : Trace("cegqi-debug") << " register " << candidates[i] << " -> "
254 : 84776 : << candidate_values[i] << std::endl;
255 : 84776 : d_eval_unfold->registerModelValue(candidates[i],
256 : 84776 : candidate_values[i],
257 : : eager_terms,
258 : : eager_vals,
259 : : eager_exps);
260 : : }
261 [ + - ]: 17744 : Trace("cegqi-debug") << "...produced " << eager_terms.size()
262 : 8872 : << " evaluation unfold lemmas.\n";
263 [ + + ]: 46084 : for (unsigned i = 0, size = eager_terms.size(); i < size; ++i)
264 : : {
265 : 111636 : Node lem = nm->mkNode(
266 : : Kind::OR,
267 : 74424 : {eager_exps[i].negate(), eager_terms[i].eqNode(eager_vals[i])});
268 : : // apply the substitution, which ensures that this lemma does not
269 : : // contain free variables (e.g. if using forward declarations).
270 : 37212 : lem = d_euSubs.apply(lem);
271 : 37212 : d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_SYGUS_EVAL_UNFOLD);
272 : 37212 : addedEvalLemmas = true;
273 [ + - ]: 74424 : Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation unfold : " << lem
274 : 37212 : << std::endl;
275 : 37212 : }
276 : 8872 : }
277 : 9809 : return addedEvalLemmas;
278 : : }
279 : :
280 : 1820 : Node Cegis::getRefinementLemmaFormula()
281 : : {
282 : 1820 : std::vector<Node> conj;
283 : 3640 : conj.insert(
284 : 1820 : conj.end(), d_refinement_lemmas.begin(), d_refinement_lemmas.end());
285 : : // get the propagated values
286 [ + + ]: 17466 : for (unsigned i = 0, nprops = d_rl_eval_hds.size(); i < nprops; i++)
287 : : {
288 : 15646 : conj.push_back(d_rl_eval_hds[i].eqNode(d_rl_vals[i]));
289 : : }
290 : : // make the formula
291 : 1820 : NodeManager* nm = nodeManager();
292 : 1820 : Node ret;
293 [ + + ]: 1820 : if (conj.empty())
294 : : {
295 : 12 : ret = nm->mkConst(true);
296 : : }
297 : : else
298 : : {
299 [ - + ]: 1808 : ret = conj.size() == 1 ? conj[0] : nm->mkNode(Kind::AND, conj);
300 : : }
301 : 3640 : return ret;
302 : 1820 : }
303 : :
304 : 45390 : bool Cegis::constructCandidates(const std::vector<Node>& enums,
305 : : const std::vector<Node>& enum_values,
306 : : const std::vector<Node>& candidates,
307 : : std::vector<Node>& candidate_values)
308 : : {
309 [ - + ]: 45390 : if (TraceIsOn("cegis"))
310 : : {
311 [ - - ]: 0 : Trace("cegis") << " Enumerators :\n";
312 [ - - ]: 0 : for (unsigned i = 0, size = enums.size(); i < size; ++i)
313 : : {
314 [ - - ]: 0 : Trace("cegis") << " " << enums[i] << " -> ";
315 : 0 : TermDbSygus::toStreamSygus("cegis", enum_values[i]);
316 [ - - ]: 0 : Trace("cegis") << "\n";
317 : : }
318 : : }
319 : : // if we are using grammar-based repair
320 [ + + ][ + - ]: 45390 : if (d_usingSymCons && options().quantifiers.sygusRepairConst)
[ + + ]
321 : : {
322 : 2169 : SygusRepairConst* src = d_parent->getRepairConst();
323 [ - + ][ - + ]: 2169 : Assert(src != nullptr);
[ - - ]
324 : : // check if any enum_values have symbolic terms that must be repaired
325 : 2169 : bool mustRepair = false;
326 [ + + ]: 2914 : for (const Node& c : enum_values)
327 : : {
328 [ + + ]: 2597 : if (SygusRepairConst::mustRepair(c))
329 : : {
330 : 1852 : mustRepair = true;
331 : 1852 : break;
332 : : }
333 : : }
334 [ + - ]: 2169 : Trace("cegis-debug") << "must repair is: " << mustRepair << std::endl;
335 : : // if the solution contains a subterm that must be repaired
336 [ + + ]: 2169 : if (mustRepair)
337 : : {
338 : 1852 : std::vector<Node> fail_cvs = enum_values;
339 [ - + ][ - + ]: 1852 : Assert(candidates.size() == fail_cvs.size());
[ - - ]
340 : : // try to solve entire problem?
341 [ + + ]: 1852 : if (src->repairSolution(candidates, fail_cvs, candidate_values))
342 : : {
343 [ + - ]: 32 : Trace("cegis") << "...solution is repaired" << std::endl;
344 : 32 : return true;
345 : : }
346 : 1820 : Node rl = getRefinementLemmaFormula();
347 : : // try to solve for the refinement lemmas only
348 : : bool ret =
349 : 1820 : src->repairSolution(rl, candidates, fail_cvs, candidate_values);
350 : : // Even if ret is true, we will exclude the skeleton as well; this means
351 : : // that we have one chance to repair each skeleton. It is possible however
352 : : // that we might want to repair the same skeleton multiple times.
353 : 1820 : std::vector<Node> exp;
354 : 1820 : bool doExplain = true;
355 [ + + ]: 5600 : for (unsigned i = 0, size = enums.size(); i < size; i++)
356 : : {
357 [ + + ]: 4052 : if (!d_tds->isPassiveEnumerator(enums[i]))
358 : : {
359 : : // don't exclude active (fast) enumerators
360 : 272 : doExplain = false;
361 : 272 : break;
362 : : }
363 : 11340 : d_tds->getExplain()->getExplanationForEquality(
364 : 7560 : enums[i], enum_values[i], exp);
365 : : }
366 [ + + ]: 1820 : if (doExplain)
367 : : {
368 [ - + ][ - + ]: 1548 : Assert(!exp.empty());
[ - - ]
369 : 1548 : NodeManager* nm = nodeManager();
370 [ + + ]: 1548 : Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(Kind::AND, exp);
371 : : // must guard it
372 [ + + ][ - - ]: 7740 : expn = nm->mkNode(Kind::OR,
373 : 6192 : {d_parent->getConjecture().negate(), expn.negate()});
374 : 1548 : d_qim.addPendingLemma(
375 : : expn, InferenceId::QUANTIFIERS_SYGUS_REPAIR_CONST_EXCLUDE);
376 : 1548 : }
377 [ + - ]: 3640 : Trace("cegis") << "...solution was processed via repair, success = "
378 : 1820 : << ret << std::endl;
379 : 1820 : return ret;
380 : 1852 : }
381 : : }
382 : :
383 : : // evaluate on refinement lemmas
384 : 43538 : bool addedEvalLemmas = addEvalLemmas(enums, enum_values);
385 : :
386 : : // try to construct candidates
387 [ + + ]: 43538 : if (!processConstructCandidates(
388 : 43538 : enums, enum_values, candidates, candidate_values, !addedEvalLemmas))
389 : : {
390 [ + - ]: 40894 : Trace("cegis") << "...construct candidates failed" << std::endl;
391 : 40894 : return false;
392 : : }
393 : :
394 : 2644 : if (options().quantifiers.cegisSample != options::CegisSampleMode::NONE
395 [ + + ][ + + ]: 2644 : && !addedEvalLemmas)
[ + + ]
396 : : {
397 : : // if we didn't add a lemma, trying sampling to add a refinement lemma
398 : : // that immediately refutes the candidate we just constructed
399 [ + + ]: 73 : if (sampleAddRefinementLemma(candidates, candidate_values))
400 : : {
401 : 10 : candidate_values.clear();
402 : : // restart (should be guaranteed to add evaluation lemmas on this call)
403 : 10 : return constructCandidates(
404 : 10 : enums, enum_values, candidates, candidate_values);
405 : : }
406 : : }
407 [ + - ]: 2634 : Trace("cegis") << "...success" << std::endl;
408 : 2634 : return true;
409 : : }
410 : :
411 : 39127 : bool Cegis::processConstructCandidates(
412 : : CVC5_UNUSED const std::vector<Node>& enums,
413 : : const std::vector<Node>& enum_values,
414 : : CVC5_UNUSED const std::vector<Node>& candidates,
415 : : std::vector<Node>& candidate_values,
416 : : bool satisfiedRl)
417 : : {
418 [ + + ]: 39127 : if (satisfiedRl)
419 : : {
420 : 3244 : candidate_values.insert(
421 : 1622 : candidate_values.end(), enum_values.begin(), enum_values.end());
422 : 1622 : return true;
423 : : }
424 : 37505 : return false;
425 : : }
426 : :
427 : 1377 : void Cegis::addRefinementLemma(Node lem)
428 : : {
429 [ + - ]: 1377 : Trace("cegis-rl") << "Cegis::addRefinementLemma: " << lem << std::endl;
430 : 1377 : d_refinement_lemmas.push_back(lem);
431 : : // apply existing substitution
432 : 1377 : Node slem = lem;
433 [ + + ]: 1377 : if (!d_rl_eval_hds.empty())
434 : : {
435 : 1432 : slem = lem.substitute(d_rl_eval_hds.begin(),
436 : : d_rl_eval_hds.end(),
437 : : d_rl_vals.begin(),
438 : 716 : d_rl_vals.end());
439 : : }
440 : : // rewrite with extended rewriter
441 : 1377 : slem = d_tds->rewriteNode(slem);
442 : : // collect all variables in slem
443 : 1377 : expr::getSymbols(slem, d_refinement_lemma_vars);
444 : 1377 : std::vector<Node> waiting;
445 : 1377 : waiting.push_back(lem);
446 : 1377 : unsigned wcounter = 0;
447 : : // while we are not done adding lemmas
448 [ + + ]: 3754 : while (wcounter < waiting.size())
449 : : {
450 : : // add the conjunct, possibly propagating
451 : 2377 : addRefinementLemmaConjunct(wcounter, waiting);
452 : 2377 : wcounter++;
453 : : }
454 : 1377 : }
455 : :
456 : 2377 : void Cegis::addRefinementLemmaConjunct(unsigned wcounter,
457 : : std::vector<Node>& waiting)
458 : : {
459 : 2377 : Node lem = waiting[wcounter];
460 : 2377 : lem = rewrite(lem);
461 : : // apply substitution and rewrite if applicable
462 [ + + ]: 2377 : if (lem.isConst())
463 : : {
464 [ + + ]: 13 : if (!lem.getConst<bool>())
465 : : {
466 : : // conjecture is infeasible
467 : : }
468 : : else
469 : : {
470 : 1 : return;
471 : : }
472 : : }
473 : : // break into conjunctions
474 [ + + ]: 2376 : if (lem.getKind() == Kind::AND)
475 : : {
476 [ + + ]: 1269 : for (const Node& lc : lem)
477 : : {
478 : 996 : waiting.push_back(lc);
479 : 996 : }
480 : 273 : return;
481 : : }
482 : : // does this correspond to a substitution?
483 : 2103 : NodeManager* nm = nodeManager();
484 : 2103 : TNode term;
485 : 2103 : TNode val;
486 [ + + ]: 2103 : if (lem.getKind() == Kind::EQUAL)
487 : : {
488 [ + + ]: 1943 : for (unsigned i = 0; i < 2; i++)
489 : : {
490 : 1620 : if (lem[i].isConst() && d_tds->isEvaluationPoint(lem[1 - i]))
491 : : {
492 : 610 : term = lem[1 - i];
493 : 610 : val = lem[i];
494 : 610 : break;
495 : : }
496 : : }
497 : : }
498 : : else
499 : : {
500 [ + + ]: 1170 : term = lem.getKind() == Kind::NOT ? lem[0] : lem;
501 : : // predicate case: the conjunct is a (negated) evaluation point
502 [ + + ]: 1170 : if (d_tds->isEvaluationPoint(term))
503 : : {
504 : 655 : val = nm->mkConst(lem.getKind() != Kind::NOT);
505 : : }
506 : : }
507 [ + + ]: 2103 : if (!val.isNull())
508 : : {
509 [ + + ]: 1265 : if (d_refinement_lemma_unit.find(lem) != d_refinement_lemma_unit.end())
510 : : {
511 : : // already added
512 : 657 : return;
513 : : }
514 [ + - ]: 1216 : Trace("cegis-rl") << "* cegis-rl: propagate: " << term << " -> " << val
515 : 608 : << std::endl;
516 : 608 : d_rl_eval_hds.push_back(term);
517 : 608 : d_rl_vals.push_back(val);
518 : 608 : d_refinement_lemma_unit.insert(lem);
519 : :
520 : : // apply to waiting lemmas beyond this one
521 [ + + ]: 1301 : for (unsigned i = wcounter + 1, size = waiting.size(); i < size; i++)
522 : : {
523 : 693 : waiting[i] = waiting[i].substitute(term, val);
524 : : }
525 : : // apply to all existing refinement lemmas
526 : 608 : std::vector<Node> to_rem;
527 [ + + ]: 1140 : for (const Node& rl : d_refinement_lemma_conj)
528 : : {
529 : 1064 : Node srl = rl.substitute(term, val);
530 [ + + ]: 532 : if (srl != rl)
531 : : {
532 [ + - ]: 8 : Trace("cegis-rl") << "* cegis-rl: replace: " << rl << " -> " << srl
533 : 4 : << std::endl;
534 : 4 : waiting.push_back(srl);
535 : 4 : to_rem.push_back(rl);
536 : : }
537 : 532 : }
538 [ + + ]: 612 : for (const Node& tr : to_rem)
539 : : {
540 : 4 : d_refinement_lemma_conj.erase(tr);
541 : : }
542 : 608 : }
543 : : else
544 : : {
545 [ - + ]: 838 : if (TraceIsOn("cegis-rl"))
546 : : {
547 [ - - ]: 0 : if (d_refinement_lemma_conj.find(lem) == d_refinement_lemma_conj.end())
548 : : {
549 [ - - ]: 0 : Trace("cegis-rl") << "cegis-rl: add: " << lem << std::endl;
550 : : }
551 : : }
552 : 838 : d_refinement_lemma_conj.insert(lem);
553 : : }
554 [ + + ][ + + ]: 3691 : }
[ + + ]
555 : :
556 : 1213 : void Cegis::registerRefinementLemma(CVC5_UNUSED const std::vector<Node>& vars,
557 : : Node lem)
558 : : {
559 : 1213 : addRefinementLemma(lem);
560 : : // must be closed enumerable
561 [ + + ][ + + ]: 1213 : if (d_cexClosedEnum && d_doEvalUnfold)
562 : : {
563 : : // Make the refinement lemma and add it to lems.
564 : : // This lemma is guarded by the parent's conjecture, which has the semantics
565 : : // "this conjecture has a solution", hence this lemma states:
566 : : // if the parent conjecture has a solution, it satisfies the specification
567 : : // for the given concrete point.
568 : 1167 : Node rlem = nodeManager()->mkNode(
569 : 2334 : Kind::OR, d_parent->getConjecture().negate(), lem);
570 : 1167 : d_qim.addPendingLemma(rlem, InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE);
571 : 1167 : }
572 : 1213 : }
573 : :
574 : 96101 : bool Cegis::usingRepairConst() { return true; }
575 : 8741 : bool Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs,
576 : : const std::vector<Node>& ms,
577 : : std::vector<Node>& lems)
578 : : {
579 [ + - ]: 17482 : Trace("sygus-cref-eval") << "Cref eval : conjecture has "
580 : 0 : << d_refinement_lemma_unit.size() << " unit and "
581 : 8741 : << d_refinement_lemma_conj.size()
582 : 0 : << " non-unit refinement lemma conjunctions."
583 : 8741 : << std::endl;
584 [ - + ][ - + ]: 8741 : Assert(vs.size() == ms.size());
[ - - ]
585 : :
586 : 8741 : NodeManager* nm = nodeManager();
587 : :
588 : 8741 : Node nfalse = nm->mkConst(false);
589 : 8741 : Node neg_guard = d_parent->getConjecture().negate();
590 : 8741 : bool ret = false;
591 : :
592 [ + + ]: 21039 : for (unsigned r = 0; r < 2; r++)
593 : : {
594 [ + + ]: 16084 : std::unordered_set<Node>& rlemmas =
595 : : r == 0 ? d_refinement_lemma_unit : d_refinement_lemma_conj;
596 [ + + ]: 92368 : for (const Node& lem : rlemmas)
597 : : {
598 [ - + ][ - + ]: 76284 : Assert(!lem.isNull());
[ - - ]
599 : 76284 : std::map<Node, Node> visited;
600 : 76284 : std::map<Node, std::vector<Node> > exp;
601 : 76284 : EvalSygusInvarianceTest vsit(d_env.getRewriter());
602 [ + - ]: 152568 : Trace("sygus-cref-eval") << "Check refinement lemma conjunct " << lem
603 : 76284 : << " against current model." << std::endl;
604 [ + - ]: 152568 : Trace("sygus-cref-eval2") << "Check refinement lemma conjunct " << lem
605 : 76284 : << " against current model." << std::endl;
606 : 76284 : Node cre_lem;
607 : 76284 : Node lemcs = lem.substitute(vs.begin(), vs.end(), ms.begin(), ms.end());
608 [ + - ]: 152568 : Trace("sygus-cref-eval2")
609 : 76284 : << "...under substitution it is : " << lemcs << std::endl;
610 : 76284 : Node lemcsu = d_tds->rewriteNode(lemcs);
611 [ + - ]: 152568 : Trace("sygus-cref-eval2")
612 : 76284 : << "...after unfolding is : " << lemcsu << std::endl;
613 [ + + ][ + + ]: 76284 : if (lemcsu.isConst() && !lemcsu.getConst<bool>())
[ + + ]
614 : : {
615 : 8106 : ret = true;
616 : 8106 : std::vector<Node> msu;
617 : 8106 : std::vector<Node> mexp;
618 : 8106 : msu.insert(msu.end(), ms.begin(), ms.end());
619 : 8106 : std::map<TypeNode, size_t> var_count;
620 [ + + ]: 59736 : for (unsigned k = 0; k < vs.size(); k++)
621 : : {
622 : 51630 : vsit.setUpdatedTerm(msu[k]);
623 : 51630 : msu[k] = vs[k];
624 : : // substitute for everything except this
625 : : Node sconj =
626 : 51630 : lem.substitute(vs.begin(), vs.end(), msu.begin(), msu.end());
627 : 51630 : vsit.init(sconj, vs[k], nfalse);
628 : : // get minimal explanation for this
629 : 51630 : Node ut = vsit.getUpdatedTerm();
630 [ + - ]: 103260 : Trace("sygus-cref-eval2-debug")
631 : 0 : << " compute min explain of : " << vs[k] << " = " << ut
632 : 51630 : << std::endl;
633 : 103260 : d_tds->getExplain()->getExplanationFor(
634 : 51630 : vs[k], ut, mexp, vsit, var_count, false);
635 [ + - ]: 51630 : Trace("sygus-cref-eval2-debug") << "exp now: " << mexp << std::endl;
636 : 51630 : msu[k] = vsit.getUpdatedTerm();
637 [ + - ]: 103260 : Trace("sygus-cref-eval2-debug")
638 : 51630 : << "updated term : " << msu[k] << std::endl;
639 : 51630 : }
640 [ + + ]: 8106 : if (!mexp.empty())
641 : : {
642 [ + + ]: 8104 : Node en = mexp.size() == 1 ? mexp[0] : nm->mkNode(Kind::AND, mexp);
643 : 8104 : cre_lem = nm->mkNode(Kind::OR, en.negate(), neg_guard);
644 : 8104 : }
645 : : else
646 : : {
647 : 2 : cre_lem = neg_guard;
648 : : }
649 [ + + ]: 8106 : if (std::find(lems.begin(), lems.end(), cre_lem) == lems.end())
650 : : {
651 [ + - ]: 10516 : Trace("sygus-cref-eval")
652 : 5258 : << "...produced lemma : " << cre_lem << std::endl;
653 : 5258 : lems.push_back(cre_lem);
654 : : }
655 : 8106 : }
656 : 76284 : }
657 [ + + ]: 16084 : if (!lems.empty())
658 : : {
659 : 3786 : break;
660 : : }
661 : : }
662 : 8741 : return ret;
663 : 8741 : }
664 : :
665 : 34480 : bool Cegis::checkRefinementEvalLemmas(const std::vector<Node>& vs,
666 : : const std::vector<Node>& ms)
667 : : {
668 : : // Maybe we already evaluated some terms in refinement lemmas.
669 : : // In particular, the example eval cache for f may have some evaluations
670 : : // cached, which we add to evalVisited and pass to the evaluator below.
671 : 34480 : std::unordered_map<Node, Node> evalVisited;
672 : 34480 : ExampleInfer* ei = d_parent->getExampleInfer();
673 [ + + ]: 68960 : for (unsigned i = 0, vsize = vs.size(); i < vsize; i++)
674 : : {
675 : 34480 : Node f = vs[i];
676 : 34480 : ExampleEvalCache* eec = d_parent->getExampleEvalCache(f);
677 [ + + ]: 34480 : if (eec != nullptr)
678 : : {
679 : : // get the results we obtained through the example evaluation utility
680 : 2504 : std::vector<Node> vsProc;
681 : 2504 : std::vector<Node> msProc;
682 : 2504 : Node bmsi = d_tds->sygusToBuiltin(ms[i]);
683 : 2504 : ei->getExampleTerms(f, vsProc);
684 : 2504 : eec->evaluateVec(bmsi, msProc);
685 [ - + ][ - + ]: 2504 : Assert(vsProc.size() == msProc.size());
[ - - ]
686 [ + + ]: 23816 : for (unsigned j = 0, psize = vsProc.size(); j < psize; j++)
687 : : {
688 : 21312 : evalVisited[vsProc[j]] = msProc[j];
689 [ - + ][ - + ]: 63936 : AssertEqual(vsProc[j].getType(), msProc[j].getType());
[ - - ]
690 : : }
691 : 2504 : }
692 : 34480 : }
693 : :
694 [ + + ]: 36190 : for (unsigned r = 0; r < 2; r++)
695 : : {
696 [ + + ]: 35439 : std::unordered_set<Node>& rlemmas =
697 : : r == 0 ? d_refinement_lemma_unit : d_refinement_lemma_conj;
698 [ + + ]: 72082 : for (const Node& lem : rlemmas)
699 : : {
700 : : // We may have computed the evaluation of some function applications
701 : : // via example-based symmetry breaking, stored in evalVisited.
702 : 70372 : Node lemcsu = evaluate(lem, vs, ms, evalVisited);
703 [ + + ][ + + ]: 70372 : if (lemcsu.isConst() && !lemcsu.getConst<bool>())
[ + + ]
704 : : {
705 : 33729 : return true;
706 : : }
707 [ + + ]: 70372 : }
708 : : }
709 : 751 : return false;
710 : 34480 : }
711 : :
712 : 73 : bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates,
713 : : const std::vector<Node>& vals)
714 : : {
715 [ + - ]: 73 : Trace("sygus-engine") << " *** Do sample add refinement..." << std::endl;
716 [ - + ]: 73 : if (TraceIsOn("cegis-sample"))
717 : : {
718 [ - - ]: 0 : Trace("cegis-sample") << "Check sampling for candidate solution"
719 : 0 : << std::endl;
720 [ - - ]: 0 : for (unsigned i = 0, size = vals.size(); i < size; i++)
721 : : {
722 [ - - ]: 0 : Trace("cegis-sample")
723 : 0 : << " " << candidates[i] << " -> " << vals[i] << std::endl;
724 : : }
725 : : }
726 [ - + ][ - + ]: 73 : Assert(vals.size() == candidates.size());
[ - - ]
727 : : Node sbody = d_base_body.substitute(
728 : 73 : candidates.begin(), candidates.end(), vals.begin(), vals.end());
729 [ + - ]: 73 : Trace("cegis-sample-debug2") << "Sample " << sbody << std::endl;
730 : : // do eager rewriting
731 : 73 : sbody = rewrite(sbody);
732 [ + - ]: 73 : Trace("cegis-sample") << "Sample (after rewriting): " << sbody << std::endl;
733 : :
734 : 73 : NodeManager* nm = nodeManager();
735 [ + + ]: 63091 : for (size_t i = 0, size = d_cegis_sampler.getNumSamplePoints(); i < size; i++)
736 : : {
737 [ + + ]: 63028 : if (d_cegis_sample_refine.find(i) == d_cegis_sample_refine.end())
738 : : {
739 : 63016 : Node ev = d_cegis_sampler.evaluate(sbody, i);
740 [ + - ]: 126032 : Trace("cegis-sample-debug")
741 : 63016 : << "...evaluate point #" << i << " to " << ev << std::endl;
742 [ - + ][ - + ]: 63016 : Assert(ev.getType().isBoolean());
[ - - ]
743 : : // if it evaluates to false
744 [ + + ][ + + ]: 63016 : if (ev.isConst() && !ev.getConst<bool>())
[ + + ]
745 : : {
746 [ + - ]: 10 : Trace("cegis-sample-debug") << "...false for point #" << i << std::endl;
747 : : // mark this as a CEGIS point (no longer sampled)
748 : 10 : d_cegis_sample_refine.insert(i);
749 : 10 : const std::vector<Node>& pt = d_cegis_sampler.getSamplePoint(i);
750 [ - + ][ - + ]: 10 : Assert(d_base_vars.size() == pt.size());
[ - - ]
751 : : Node rlem = d_base_body.substitute(
752 : 10 : d_base_vars.begin(), d_base_vars.end(), pt.begin(), pt.end());
753 : 10 : rlem = rewrite(rlem);
754 : 10 : if (std::find(
755 : : d_refinement_lemmas.begin(), d_refinement_lemmas.end(), rlem)
756 [ + - ]: 20 : == d_refinement_lemmas.end())
757 : : {
758 [ - + ]: 10 : if (TraceIsOn("cegis-sample"))
759 : : {
760 [ - - ]: 0 : Trace("cegis-sample") << " false for point #" << i << " : ";
761 [ - - ]: 0 : for (const Node& cn : pt)
762 : : {
763 [ - - ]: 0 : Trace("cegis-sample") << cn << " ";
764 : : }
765 [ - - ]: 0 : Trace("cegis-sample") << std::endl;
766 : : }
767 [ + - ]: 10 : Trace("sygus-engine") << " *** Refine by sampling" << std::endl;
768 : 10 : addRefinementLemma(rlem);
769 : : // if trust, we are not interested in sending out refinement lemmas
770 : 10 : if (options().quantifiers.cegisSample
771 [ + + ]: 10 : != options::CegisSampleMode::TRUST)
772 : : {
773 : : Node lem =
774 : 8 : nm->mkNode(Kind::OR, d_parent->getConjecture().negate(), rlem);
775 : 4 : d_qim.addPendingLemma(
776 : : lem, InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE_SAMPLE);
777 : 4 : }
778 : 10 : return true;
779 : : }
780 : : else
781 : : {
782 [ - - ]: 0 : Trace("cegis-sample-debug") << "...duplicate." << std::endl;
783 : : }
784 [ - + ]: 10 : }
785 [ + + ]: 63016 : }
786 : : }
787 : 63 : return false;
788 : 73 : }
789 : :
790 : : } // namespace quantifiers
791 : : } // namespace theory
792 : : } // namespace cvc5::internal
|
