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