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