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 : 18693 : Cegis::Cegis(Env& env,
36 : : QuantifiersState& qs,
37 : : QuantifiersInferenceManager& qim,
38 : : TermDbSygus* tds,
39 : 18693 : SynthConjecture* p)
40 : : : SygusModule(env, qs, qim, tds, p),
41 : 37386 : d_eval_unfold(tds->getEvalUnfold()),
42 : 18693 : d_cexClosedEnum(false),
43 : 18693 : d_cegis_sampler(env),
44 : 18693 : d_usingSymCons(false),
45 : 37386 : d_doEvalUnfold(false)
46 : : {
47 : 18693 : }
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 : 4752 : }
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 : 15 : }
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 : 1741 : }
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 [ + + ][ + + ]: 2277 : }
[ + + ][ + + ]
[ + + ]
119 : : }
120 : 2059 : return processInitialize(conj, n, candidates);
121 : : }
122 : :
123 : 1130 : bool Cegis::processInitialize(Node conj,
124 : : CVC5_UNUSED 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 : 1212 : 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 : 1212 : }
154 [ + - ]: 1220 : Trace("cegis") << std::endl;
155 : 1220 : Node e = candidates[i];
156 : 1220 : d_tds->registerEnumerator(e, e, d_parent, erole);
157 : 1220 : Node g = d_tds->getActiveGuardForEnumerator(e);
158 [ + + ]: 1220 : if (!g.isNull())
159 : : {
160 : 996 : activeGuards.push_back(g);
161 : : }
162 : 1220 : }
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 : 996 : }
176 : 1130 : return true;
177 : 1130 : }
178 : :
179 : 98517 : void Cegis::getTermList(const std::vector<Node>& candidates,
180 : : std::vector<Node>& enums)
181 : : {
182 : 98517 : enums.insert(enums.end(), candidates.begin(), candidates.end());
183 : 98517 : }
184 : :
185 : 45378 : 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 : 45378 : bool doGen = true;
198 [ + + ]: 130308 : for (const Node& v : candidates)
199 : : {
200 : : // if it is relevant to refinement
201 [ + + ]: 120956 : if (d_refinement_lemma_vars.find(v) != d_refinement_lemma_vars.end())
202 : : {
203 [ + + ]: 109302 : if (!d_tds->isPassiveEnumerator(v))
204 : : {
205 : 36026 : doGen = false;
206 : 36026 : break;
207 : : }
208 : : }
209 : : }
210 : 45378 : NodeManager* nm = nodeManager();
211 : 45378 : bool addedEvalLemmas = false;
212 : : // Refinement evaluation should not be done for grammars with symbolic
213 : : // constructors.
214 [ + + ]: 45378 : if (!d_usingSymCons)
215 : : {
216 [ + - ]: 90406 : Trace("sygus-engine") << " *** Do refinement lemma evaluation"
217 [ - - ]: 45203 : << (doGen ? " with conjecture-specific refinement"
218 : 0 : : "")
219 : 45203 : << "..." << std::endl;
220 : : // see if any refinement lemma is refuted by evaluation
221 [ + + ]: 45203 : if (doGen)
222 : : {
223 : 9319 : std::vector<Node> cre_lems;
224 : 9319 : getRefinementEvalLemmas(candidates, candidate_values, cre_lems);
225 [ + + ]: 9319 : if (!cre_lems.empty())
226 : : {
227 [ + + ]: 8160 : for (const Node& cl : cre_lems)
228 : : {
229 : 4797 : d_qim.addPendingLemma(cl, InferenceId::QUANTIFIERS_SYGUS_REFINE_EVAL);
230 : : }
231 : 3363 : 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 : 9319 : }
236 : : else
237 : : {
238 : : // just check whether the refinement lemmas are satisfied, fail if not
239 [ + + ]: 35884 : 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 [ + + ][ + + ]: 10713 : bool doEvalUnfold = (doGen && d_doEvalUnfold);
250 [ + + ]: 10713 : if (doEvalUnfold)
251 : : {
252 [ + - ]: 9348 : Trace("sygus-engine") << " *** Do evaluation unfolding..." << std::endl;
253 : 9348 : std::vector<Node> eager_terms, eager_vals, eager_exps;
254 [ + + ]: 94274 : for (unsigned i = 0, size = candidates.size(); i < size; ++i)
255 : : {
256 [ + - ]: 169852 : Trace("cegqi-debug") << " register " << candidates[i] << " -> "
257 : 84926 : << candidate_values[i] << std::endl;
258 : 84926 : d_eval_unfold->registerModelValue(candidates[i],
259 : 84926 : candidate_values[i],
260 : : eager_terms,
261 : : eager_vals,
262 : : eager_exps);
263 : : }
264 [ + - ]: 18696 : Trace("cegqi-debug") << "...produced " << eager_terms.size()
265 : 9348 : << " evaluation unfold lemmas.\n";
266 [ + + ]: 37168 : for (unsigned i = 0, size = eager_terms.size(); i < size; ++i)
267 : : {
268 : : Node lem = nm->mkNode(Kind::OR,
269 : 55640 : eager_exps[i].negate(),
270 : 111280 : 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 : 27820 : lem = d_euSubs.apply(lem);
274 : 27820 : d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_SYGUS_EVAL_UNFOLD);
275 : 27820 : addedEvalLemmas = true;
276 [ + - ]: 55640 : Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation unfold : " << lem
277 : 27820 : << std::endl;
278 : 27820 : }
279 : 9348 : }
280 : 10713 : return addedEvalLemmas;
281 : : }
282 : :
283 : 574 : Node Cegis::getRefinementLemmaFormula()
284 : : {
285 : 574 : std::vector<Node> conj;
286 : 1148 : 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 : 574 : }
306 : :
307 : 45976 : 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 [ - + ]: 45976 : 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 [ + + ][ + - ]: 45976 : 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 : 598 : 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 : 574 : 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 : 340 : }
380 [ + - ]: 1148 : Trace("cegis") << "...solution was processed via repair, success = "
381 : 574 : << ret << std::endl;
382 : 574 : return ret;
383 : 598 : }
384 : : }
385 : :
386 : : // evaluate on refinement lemmas
387 : 45378 : bool addedEvalLemmas = addEvalLemmas(enums, enum_values);
388 : :
389 : : // try to construct candidates
390 [ + + ]: 45378 : if (!processConstructCandidates(
391 : 45378 : enums, enum_values, candidates, candidate_values, !addedEvalLemmas))
392 : : {
393 [ + - ]: 41353 : Trace("cegis") << "...construct candidates failed" << std::endl;
394 : 41353 : return false;
395 : : }
396 : :
397 : 4025 : if (options().quantifiers.cegisSample != options::CegisSampleMode::NONE
398 [ + + ][ + + ]: 4025 : && !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 [ + + ]: 83 : if (sampleAddRefinementLemma(candidates, candidate_values))
403 : : {
404 : 14 : candidate_values.clear();
405 : : // restart (should be guaranteed to add evaluation lemmas on this call)
406 : 14 : return constructCandidates(
407 : 14 : enums, enum_values, candidates, candidate_values);
408 : : }
409 : : }
410 [ + - ]: 4011 : Trace("cegis") << "...success" << std::endl;
411 : 4011 : return true;
412 : : }
413 : :
414 : 40422 : bool Cegis::processConstructCandidates(
415 : : CVC5_UNUSED const std::vector<Node>& enums,
416 : : const std::vector<Node>& enum_values,
417 : : CVC5_UNUSED const std::vector<Node>& candidates,
418 : : std::vector<Node>& candidate_values,
419 : : bool satisfiedRl)
420 : : {
421 [ + + ]: 40422 : if (satisfiedRl)
422 : : {
423 : 5362 : candidate_values.insert(
424 : 2681 : candidate_values.end(), enum_values.begin(), enum_values.end());
425 : 2681 : return true;
426 : : }
427 : 37741 : return false;
428 : : }
429 : :
430 : 1704 : void Cegis::addRefinementLemma(Node lem)
431 : : {
432 [ + - ]: 1704 : Trace("cegis-rl") << "Cegis::addRefinementLemma: " << lem << std::endl;
433 : 1704 : d_refinement_lemmas.push_back(lem);
434 : : // apply existing substitution
435 : 1704 : Node slem = lem;
436 [ + + ]: 1704 : if (!d_rl_eval_hds.empty())
437 : : {
438 : 1748 : slem = lem.substitute(d_rl_eval_hds.begin(),
439 : : d_rl_eval_hds.end(),
440 : : d_rl_vals.begin(),
441 : 874 : d_rl_vals.end());
442 : : }
443 : : // rewrite with extended rewriter
444 : 1704 : slem = d_tds->rewriteNode(slem);
445 : : // collect all variables in slem
446 : 1704 : expr::getSymbols(slem, d_refinement_lemma_vars);
447 : 1704 : std::vector<Node> waiting;
448 : 1704 : waiting.push_back(lem);
449 : 1704 : unsigned wcounter = 0;
450 : : // while we are not done adding lemmas
451 [ + + ]: 4106 : while (wcounter < waiting.size())
452 : : {
453 : : // add the conjunct, possibly propagating
454 : 2402 : addRefinementLemmaConjunct(wcounter, waiting);
455 : 2402 : wcounter++;
456 : : }
457 : 1704 : }
458 : :
459 : 2402 : void Cegis::addRefinementLemmaConjunct(unsigned wcounter,
460 : : std::vector<Node>& waiting)
461 : : {
462 : 2402 : Node lem = waiting[wcounter];
463 : 2402 : lem = rewrite(lem);
464 : : // apply substitution and rewrite if applicable
465 [ + + ]: 2402 : if (lem.isConst())
466 : : {
467 [ - + ]: 20 : if (!lem.getConst<bool>())
468 : : {
469 : : // conjecture is infeasible
470 : : }
471 : : else
472 : : {
473 : 0 : return;
474 : : }
475 : : }
476 : : // break into conjunctions
477 [ + + ]: 2402 : if (lem.getKind() == Kind::AND)
478 : : {
479 [ + + ]: 893 : for (const Node& lc : lem)
480 : : {
481 : 696 : waiting.push_back(lc);
482 : 696 : }
483 : 197 : return;
484 : : }
485 : : // does this correspond to a substitution?
486 : 2205 : NodeManager* nm = nodeManager();
487 : 2205 : TNode term;
488 : 2205 : TNode val;
489 [ + + ]: 2205 : if (lem.getKind() == Kind::EQUAL)
490 : : {
491 [ + + ]: 1745 : for (unsigned i = 0; i < 2; i++)
492 : : {
493 : 1422 : if (lem[i].isConst() && d_tds->isEvaluationPoint(lem[1 - i]))
494 : : {
495 : 426 : term = lem[1 - i];
496 : 426 : val = lem[i];
497 : 426 : break;
498 : : }
499 : : }
500 : : }
501 : : else
502 : : {
503 [ + + ]: 1456 : term = lem.getKind() == Kind::NOT ? lem[0] : lem;
504 : : // predicate case: the conjunct is a (negated) evaluation point
505 [ + + ]: 1456 : if (d_tds->isEvaluationPoint(term))
506 : : {
507 : 991 : val = nm->mkConst(lem.getKind() != Kind::NOT);
508 : : }
509 : : }
510 [ + + ]: 2205 : if (!val.isNull())
511 : : {
512 [ + + ]: 1417 : if (d_refinement_lemma_unit.find(lem) != d_refinement_lemma_unit.end())
513 : : {
514 : : // already added
515 : 487 : return;
516 : : }
517 [ + - ]: 1860 : Trace("cegis-rl") << "* cegis-rl: propagate: " << term << " -> " << val
518 : 930 : << std::endl;
519 : 930 : d_rl_eval_hds.push_back(term);
520 : 930 : d_rl_vals.push_back(val);
521 : 930 : d_refinement_lemma_unit.insert(lem);
522 : :
523 : : // apply to waiting lemmas beyond this one
524 [ + + ]: 1318 : for (unsigned i = wcounter + 1, size = waiting.size(); i < size; i++)
525 : : {
526 : 388 : waiting[i] = waiting[i].substitute(term, val);
527 : : }
528 : : // apply to all existing refinement lemmas
529 : 930 : std::vector<Node> to_rem;
530 [ + + ]: 1546 : for (const Node& rl : d_refinement_lemma_conj)
531 : : {
532 : 1232 : Node srl = rl.substitute(term, val);
533 [ + + ]: 616 : if (srl != rl)
534 : : {
535 [ + - ]: 4 : Trace("cegis-rl") << "* cegis-rl: replace: " << rl << " -> " << srl
536 : 2 : << std::endl;
537 : 2 : waiting.push_back(srl);
538 : 2 : to_rem.push_back(rl);
539 : : }
540 : 616 : }
541 [ + + ]: 932 : for (const Node& tr : to_rem)
542 : : {
543 : 2 : d_refinement_lemma_conj.erase(tr);
544 : : }
545 : 930 : }
546 : : else
547 : : {
548 [ - + ]: 788 : if (TraceIsOn("cegis-rl"))
549 : : {
550 [ - - ]: 0 : if (d_refinement_lemma_conj.find(lem) == d_refinement_lemma_conj.end())
551 : : {
552 [ - - ]: 0 : Trace("cegis-rl") << "cegis-rl: add: " << lem << std::endl;
553 : : }
554 : : }
555 : 788 : d_refinement_lemma_conj.insert(lem);
556 : : }
557 [ + + ][ + + ]: 3376 : }
[ + + ]
558 : :
559 : 1528 : void Cegis::registerRefinementLemma(CVC5_UNUSED const std::vector<Node>& vars,
560 : : Node lem)
561 : : {
562 : 1528 : addRefinementLemma(lem);
563 : : // must be closed enumerable
564 [ + + ][ + + ]: 1528 : if (d_cexClosedEnum && d_doEvalUnfold)
565 : : {
566 : : // Make the refinement lemma and add it to lems.
567 : : // This lemma is guarded by the parent's conjecture, which has the semantics
568 : : // "this conjecture has a solution", hence this lemma states:
569 : : // if the parent conjecture has a solution, it satisfies the specification
570 : : // for the given concrete point.
571 : 1481 : Node rlem = nodeManager()->mkNode(
572 : 2962 : Kind::OR, d_parent->getConjecture().negate(), lem);
573 : 1481 : d_qim.addPendingLemma(rlem, InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE);
574 : 1481 : }
575 : 1528 : }
576 : :
577 : 101215 : bool Cegis::usingRepairConst() { return true; }
578 : 9319 : bool Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs,
579 : : const std::vector<Node>& ms,
580 : : std::vector<Node>& lems)
581 : : {
582 [ + - ]: 18638 : Trace("sygus-cref-eval") << "Cref eval : conjecture has "
583 : 0 : << d_refinement_lemma_unit.size() << " unit and "
584 : 9319 : << d_refinement_lemma_conj.size()
585 : 0 : << " non-unit refinement lemma conjunctions."
586 : 9319 : << std::endl;
587 [ - + ][ - + ]: 9319 : Assert(vs.size() == ms.size());
[ - - ]
588 : :
589 : 9319 : NodeManager* nm = nodeManager();
590 : :
591 : 9319 : Node nfalse = nm->mkConst(false);
592 : 9319 : Node neg_guard = d_parent->getConjecture().negate();
593 : 9319 : bool ret = false;
594 : :
595 [ + + ]: 23332 : for (unsigned r = 0; r < 2; r++)
596 : : {
597 [ + + ]: 17376 : std::unordered_set<Node>& rlemmas =
598 : : r == 0 ? d_refinement_lemma_unit : d_refinement_lemma_conj;
599 [ + + ]: 88641 : for (const Node& lem : rlemmas)
600 : : {
601 [ - + ][ - + ]: 71265 : Assert(!lem.isNull());
[ - - ]
602 : 71265 : std::map<Node, Node> visited;
603 : 71265 : std::map<Node, std::vector<Node> > exp;
604 : 71265 : EvalSygusInvarianceTest vsit(d_env.getRewriter());
605 [ + - ]: 142530 : Trace("sygus-cref-eval") << "Check refinement lemma conjunct " << lem
606 : 71265 : << " against current model." << std::endl;
607 [ + - ]: 142530 : Trace("sygus-cref-eval2") << "Check refinement lemma conjunct " << lem
608 : 71265 : << " against current model." << std::endl;
609 : 71265 : Node cre_lem;
610 : 71265 : Node lemcs = lem.substitute(vs.begin(), vs.end(), ms.begin(), ms.end());
611 [ + - ]: 142530 : Trace("sygus-cref-eval2")
612 : 71265 : << "...under substitution it is : " << lemcs << std::endl;
613 : 71265 : Node lemcsu = d_tds->rewriteNode(lemcs);
614 [ + - ]: 142530 : Trace("sygus-cref-eval2")
615 : 71265 : << "...after unfolding is : " << lemcsu << std::endl;
616 [ + + ][ + + ]: 71265 : if (lemcsu.isConst() && !lemcsu.getConst<bool>())
[ + + ]
617 : : {
618 : 7797 : ret = true;
619 : 7797 : std::vector<Node> msu;
620 : 7797 : std::vector<Node> mexp;
621 : 7797 : msu.insert(msu.end(), ms.begin(), ms.end());
622 : 7797 : std::map<TypeNode, size_t> var_count;
623 [ + + ]: 52190 : for (unsigned k = 0; k < vs.size(); k++)
624 : : {
625 : 44393 : vsit.setUpdatedTerm(msu[k]);
626 : 44393 : msu[k] = vs[k];
627 : : // substitute for everything except this
628 : : Node sconj =
629 : 44393 : lem.substitute(vs.begin(), vs.end(), msu.begin(), msu.end());
630 : 44393 : vsit.init(sconj, vs[k], nfalse);
631 : : // get minimal explanation for this
632 : 44393 : Node ut = vsit.getUpdatedTerm();
633 [ + - ]: 88786 : Trace("sygus-cref-eval2-debug")
634 : 0 : << " compute min explain of : " << vs[k] << " = " << ut
635 : 44393 : << std::endl;
636 : 88786 : d_tds->getExplain()->getExplanationFor(
637 : 44393 : vs[k], ut, mexp, vsit, var_count, false);
638 [ + - ]: 44393 : Trace("sygus-cref-eval2-debug") << "exp now: " << mexp << std::endl;
639 : 44393 : msu[k] = vsit.getUpdatedTerm();
640 [ + - ]: 88786 : Trace("sygus-cref-eval2-debug")
641 : 44393 : << "updated term : " << msu[k] << std::endl;
642 : 44393 : }
643 [ + + ]: 7797 : if (!mexp.empty())
644 : : {
645 [ + + ]: 7796 : Node en = mexp.size() == 1 ? mexp[0] : nm->mkNode(Kind::AND, mexp);
646 : 7796 : cre_lem = nm->mkNode(Kind::OR, en.negate(), neg_guard);
647 : 7796 : }
648 : : else
649 : : {
650 : 1 : cre_lem = neg_guard;
651 : : }
652 [ + + ]: 7797 : if (std::find(lems.begin(), lems.end(), cre_lem) == lems.end())
653 : : {
654 [ + - ]: 9594 : Trace("sygus-cref-eval") << "...produced lemma : " << cre_lem
655 : 4797 : << std::endl;
656 : 4797 : lems.push_back(cre_lem);
657 : : }
658 : 7797 : }
659 : 71265 : }
660 [ + + ]: 17376 : if (!lems.empty())
661 : : {
662 : 3363 : break;
663 : : }
664 : : }
665 : 9319 : return ret;
666 : 9319 : }
667 : :
668 : 35884 : bool Cegis::checkRefinementEvalLemmas(const std::vector<Node>& vs,
669 : : const std::vector<Node>& ms)
670 : : {
671 : : // Maybe we already evaluated some terms in refinement lemmas.
672 : : // In particular, the example eval cache for f may have some evaluations
673 : : // cached, which we add to evalVisited and pass to the evaluator below.
674 : 35884 : std::unordered_map<Node, Node> evalVisited;
675 : 35884 : ExampleInfer* ei = d_parent->getExampleInfer();
676 [ + + ]: 71768 : for (unsigned i = 0, vsize = vs.size(); i < vsize; i++)
677 : : {
678 : 35884 : Node f = vs[i];
679 : 35884 : ExampleEvalCache* eec = d_parent->getExampleEvalCache(f);
680 [ + + ]: 35884 : if (eec != nullptr)
681 : : {
682 : : // get the results we obtained through the example evaluation utility
683 : 2497 : std::vector<Node> vsProc;
684 : 2497 : std::vector<Node> msProc;
685 : 2497 : Node bmsi = d_tds->sygusToBuiltin(ms[i]);
686 : 2497 : ei->getExampleTerms(f, vsProc);
687 : 2497 : eec->evaluateVec(bmsi, msProc);
688 [ - + ][ - + ]: 2497 : Assert(vsProc.size() == msProc.size());
[ - - ]
689 [ + + ]: 23796 : for (unsigned j = 0, psize = vsProc.size(); j < psize; j++)
690 : : {
691 : 21299 : evalVisited[vsProc[j]] = msProc[j];
692 [ - + ][ - + ]: 21299 : Assert(vsProc[j].getType() == msProc[j].getType());
[ - - ]
693 : : }
694 : 2497 : }
695 : 35884 : }
696 : :
697 [ + + ]: 38530 : for (unsigned r = 0; r < 2; r++)
698 : : {
699 [ + + ]: 37311 : std::unordered_set<Node>& rlemmas =
700 : : r == 0 ? d_refinement_lemma_unit : d_refinement_lemma_conj;
701 [ + + ]: 63480 : for (const Node& lem : rlemmas)
702 : : {
703 : : // We may have computed the evaluation of some function applications
704 : : // via example-based symmetry breaking, stored in evalVisited.
705 : 60834 : Node lemcsu = evaluate(lem, vs, ms, evalVisited);
706 [ + + ][ + + ]: 60834 : if (lemcsu.isConst() && !lemcsu.getConst<bool>())
[ + + ]
707 : : {
708 : 34665 : return true;
709 : : }
710 [ + + ]: 60834 : }
711 : : }
712 : 1219 : return false;
713 : 35884 : }
714 : :
715 : 83 : bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates,
716 : : const std::vector<Node>& vals)
717 : : {
718 [ + - ]: 83 : Trace("sygus-engine") << " *** Do sample add refinement..." << std::endl;
719 [ - + ]: 83 : if (TraceIsOn("cegis-sample"))
720 : : {
721 [ - - ]: 0 : Trace("cegis-sample") << "Check sampling for candidate solution"
722 : 0 : << std::endl;
723 [ - - ]: 0 : for (unsigned i = 0, size = vals.size(); i < size; i++)
724 : : {
725 [ - - ]: 0 : Trace("cegis-sample") << " " << candidates[i] << " -> " << vals[i]
726 : 0 : << std::endl;
727 : : }
728 : : }
729 [ - + ][ - + ]: 83 : Assert(vals.size() == candidates.size());
[ - - ]
730 : : Node sbody = d_base_body.substitute(
731 : 83 : candidates.begin(), candidates.end(), vals.begin(), vals.end());
732 [ + - ]: 83 : Trace("cegis-sample-debug2") << "Sample " << sbody << std::endl;
733 : : // do eager rewriting
734 : 83 : sbody = rewrite(sbody);
735 [ + - ]: 83 : Trace("cegis-sample") << "Sample (after rewriting): " << sbody << std::endl;
736 : :
737 : 83 : NodeManager* nm = nodeManager();
738 [ + + ]: 69927 : for (size_t i = 0, size = d_cegis_sampler.getNumSamplePoints(); i < size; i++)
739 : : {
740 [ + + ]: 69858 : if (d_cegis_sample_refine.find(i) == d_cegis_sample_refine.end())
741 : : {
742 : 69835 : Node ev = d_cegis_sampler.evaluate(sbody, i);
743 [ + - ]: 139670 : Trace("cegis-sample-debug") << "...evaluate point #" << i << " to " << ev
744 : 69835 : << std::endl;
745 [ - + ][ - + ]: 69835 : Assert(ev.getType().isBoolean());
[ - - ]
746 : : // if it evaluates to false
747 [ + + ][ + + ]: 69835 : if (ev.isConst() && !ev.getConst<bool>())
[ + + ]
748 : : {
749 [ + - ]: 14 : Trace("cegis-sample-debug") << "...false for point #" << i << std::endl;
750 : : // mark this as a CEGIS point (no longer sampled)
751 : 14 : d_cegis_sample_refine.insert(i);
752 : 14 : const std::vector<Node>& pt = d_cegis_sampler.getSamplePoint(i);
753 [ - + ][ - + ]: 14 : Assert(d_base_vars.size() == pt.size());
[ - - ]
754 : : Node rlem = d_base_body.substitute(
755 : 14 : d_base_vars.begin(), d_base_vars.end(), pt.begin(), pt.end());
756 : 14 : rlem = rewrite(rlem);
757 : 14 : if (std::find(
758 : : d_refinement_lemmas.begin(), d_refinement_lemmas.end(), rlem)
759 [ + - ]: 28 : == d_refinement_lemmas.end())
760 : : {
761 [ - + ]: 14 : if (TraceIsOn("cegis-sample"))
762 : : {
763 [ - - ]: 0 : Trace("cegis-sample") << " false for point #" << i << " : ";
764 [ - - ]: 0 : for (const Node& cn : pt)
765 : : {
766 [ - - ]: 0 : Trace("cegis-sample") << cn << " ";
767 : : }
768 [ - - ]: 0 : Trace("cegis-sample") << std::endl;
769 : : }
770 [ + - ]: 14 : Trace("sygus-engine") << " *** Refine by sampling" << std::endl;
771 : 14 : addRefinementLemma(rlem);
772 : : // if trust, we are not interested in sending out refinement lemmas
773 : 14 : if (options().quantifiers.cegisSample
774 [ + + ]: 14 : != options::CegisSampleMode::TRUST)
775 : : {
776 : : Node lem =
777 : 12 : nm->mkNode(Kind::OR, d_parent->getConjecture().negate(), rlem);
778 : 6 : d_qim.addPendingLemma(
779 : : lem, InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE_SAMPLE);
780 : 6 : }
781 : 14 : return true;
782 : : }
783 : : else
784 : : {
785 [ - - ]: 0 : Trace("cegis-sample-debug") << "...duplicate." << std::endl;
786 : : }
787 [ - + ]: 14 : }
788 [ + + ]: 69835 : }
789 : : }
790 : 69 : return false;
791 : 83 : }
792 : :
793 : : } // namespace quantifiers
794 : : } // namespace theory
795 : : } // namespace cvc5::internal
|
