Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Mathias Preiner, Andrew Reynolds, Aina Niemetz
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 : : * SyGuS instantiator class.
14 : : */
15 : :
16 : : #include "theory/quantifiers/sygus_inst.h"
17 : :
18 : : #include <sstream>
19 : : #include <unordered_set>
20 : :
21 : : #include "expr/node_algorithm.h"
22 : : #include "expr/skolem_manager.h"
23 : : #include "options/quantifiers_options.h"
24 : : #include "printer/smt2/smt2_printer.h"
25 : : #include "theory/bv/theory_bv_utils.h"
26 : : #include "theory/datatypes/sygus_datatype_utils.h"
27 : : #include "theory/quantifiers/first_order_model.h"
28 : : #include "theory/quantifiers/sygus/sygus_enumerator.h"
29 : : #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
30 : : #include "theory/quantifiers/sygus/synth_engine.h"
31 : : #include "theory/quantifiers/term_util.h"
32 : : #include "theory/rewriter.h"
33 : :
34 : : namespace cvc5::internal {
35 : : namespace theory {
36 : : namespace quantifiers {
37 : :
38 : : namespace {
39 : :
40 : : /**
41 : : * Collect maximal ground terms with type tn in node n.
42 : : *
43 : : * @param n: Node to traverse.
44 : : * @param tn: Collects only terms with type tn.
45 : : * @param terms: Collected terms.
46 : : * @param cache: Caches visited nodes.
47 : : * @param skip_quant: Do not traverse quantified formulas (skip quantifiers).
48 : : */
49 : 409 : void getMaxGroundTerms(const Options& options,
50 : : TNode n,
51 : : TypeNode tn,
52 : : std::unordered_set<Node>& terms,
53 : : std::unordered_set<TNode>& cache,
54 : : bool skip_quant = false)
55 : : {
56 [ + - ]: 409 : if (options.quantifiers.sygusInstTermSel != options::SygusInstTermSelMode::MAX
57 [ + - ]: 409 : && options.quantifiers.sygusInstTermSel
58 : : != options::SygusInstTermSelMode::BOTH)
59 : : {
60 : 409 : return;
61 : : }
62 : :
63 [ - - ]: 0 : Trace("sygus-inst-term") << "Find maximal terms with type " << tn
64 : 0 : << " in: " << n << std::endl;
65 : :
66 : 0 : Node cur;
67 : 0 : std::vector<TNode> visit;
68 : :
69 : 0 : visit.push_back(n);
70 : 0 : do
71 : : {
72 : 0 : cur = visit.back();
73 : 0 : visit.pop_back();
74 : :
75 [ - - ]: 0 : if (cache.find(cur) != cache.end())
76 : : {
77 : 0 : continue;
78 : : }
79 : 0 : cache.insert(cur);
80 : :
81 : 0 : if (expr::hasBoundVar(cur) || cur.getType() != tn)
82 : : {
83 : 0 : if (!skip_quant || cur.getKind() != Kind::FORALL)
84 : : {
85 : 0 : visit.insert(visit.end(), cur.begin(), cur.end());
86 : : }
87 : : }
88 : : else
89 : : {
90 : 0 : terms.insert(cur);
91 [ - - ]: 0 : Trace("sygus-inst-term") << " found: " << cur << std::endl;
92 : : }
93 [ - - ]: 0 : } while (!visit.empty());
94 : : }
95 : :
96 : : /*
97 : : * Collect minimal ground terms with type tn in node n.
98 : : *
99 : : * @param n: Node to traverse.
100 : : * @param tn: Collects only terms with type tn.
101 : : * @param terms: Collected terms.
102 : : * @param cache: Caches visited nodes and flags indicating whether a minimal
103 : : * term was already found in a subterm.
104 : : * @param skip_quant: Do not traverse quantified formulas (skip quantifiers).
105 : : */
106 : 409 : void getMinGroundTerms(const Options& options,
107 : : TNode n,
108 : : TypeNode tn,
109 : : std::unordered_set<Node>& terms,
110 : : std::unordered_map<TNode, std::pair<bool, bool>>& cache,
111 : : bool skip_quant = false)
112 : : {
113 [ - + ]: 409 : if (options.quantifiers.sygusInstTermSel != options::SygusInstTermSelMode::MIN
114 [ - - ]: 0 : && options.quantifiers.sygusInstTermSel
115 : : != options::SygusInstTermSelMode::BOTH)
116 : : {
117 : 0 : return;
118 : : }
119 : :
120 [ + - ]: 818 : Trace("sygus-inst-term") << "Find minimal terms with type " << tn
121 : 409 : << " in: " << n << std::endl;
122 : :
123 : 818 : Node cur;
124 : 818 : std::vector<TNode> visit;
125 : :
126 : 409 : visit.push_back(n);
127 : 16656 : do
128 : : {
129 : 17065 : cur = visit.back();
130 : 17065 : visit.pop_back();
131 : :
132 : 17065 : auto it = cache.find(cur);
133 [ + + ]: 17065 : if (it == cache.end())
134 : : {
135 : 7173 : cache.emplace(cur, std::make_pair(false, false));
136 [ - + ][ - - ]: 7173 : if (!skip_quant || cur.getKind() != Kind::FORALL)
[ + - ]
137 : : {
138 : 7173 : visit.push_back(cur);
139 : 7173 : visit.insert(visit.end(), cur.begin(), cur.end());
140 : : }
141 : : }
142 : : /* up-traversal */
143 [ + + ]: 9892 : else if (!it->second.first)
144 : : {
145 : 7173 : bool found_min_term = false;
146 : :
147 : : /* Check if we found a minimal term in one of the children. */
148 [ + + ]: 11928 : for (const Node& c : cur)
149 : : {
150 : 7827 : found_min_term |= cache[c].second;
151 [ + + ]: 7827 : if (found_min_term) break;
152 : : }
153 : :
154 : : /* If we haven't found a minimal term yet, add this term if it has the
155 : : * right type. */
156 : 7173 : if (cur.getType() == tn && !expr::hasBoundVar(cur) && !found_min_term)
157 : : {
158 : 919 : terms.insert(cur);
159 : 919 : found_min_term = true;
160 [ + - ]: 919 : Trace("sygus-inst-term") << " found: " << cur << std::endl;
161 : : }
162 : :
163 : 7173 : it->second.first = true;
164 : 7173 : it->second.second = found_min_term;
165 : : }
166 [ + + ]: 17065 : } while (!visit.empty());
167 : : }
168 : :
169 : : /*
170 : : * Add special values for a given type.
171 : : *
172 : : * @param tn: The type node.
173 : : * @param extra_cons: A map of TypeNode to constants, which are added in
174 : : * addition to the default grammar.
175 : : */
176 : 608 : void addSpecialValues(const TypeNode& tn, std::vector<Node>& extra_cons)
177 : : {
178 [ + + ]: 608 : if (tn.isBitVector())
179 : : {
180 : 10 : uint32_t size = tn.getBitVectorSize();
181 : 10 : extra_cons.push_back(bv::utils::mkOnes(size));
182 : 10 : extra_cons.push_back(bv::utils::mkMinSigned(size));
183 : 10 : extra_cons.push_back(bv::utils::mkMaxSigned(size));
184 : : }
185 : 608 : }
186 : :
187 : : } // namespace
188 : :
189 : 152 : SygusInst::SygusInst(Env& env,
190 : : QuantifiersState& qs,
191 : : QuantifiersInferenceManager& qim,
192 : : QuantifiersRegistry& qr,
193 : 152 : TermRegistry& tr)
194 : : : QuantifiersModule(env, qs, qim, qr, tr),
195 : 304 : d_ce_lemma_added(userContext()),
196 : 304 : d_global_terms(userContext()),
197 : 152 : d_notified_assertions(userContext())
198 : : {
199 : 152 : }
200 : :
201 : 2280 : bool SygusInst::needsCheck(Theory::Effort e)
202 : : {
203 : 2280 : return e >= Theory::EFFORT_LAST_CALL;
204 : : }
205 : :
206 : 290 : QuantifiersModule::QEffort SygusInst::needsModel(Theory::Effort e)
207 : : {
208 : 290 : return QEFFORT_STANDARD;
209 : : }
210 : :
211 : 984 : void SygusInst::reset_round(Theory::Effort e)
212 : : {
213 : 984 : d_active_quant.clear();
214 : 984 : d_inactive_quant.clear();
215 : :
216 : 984 : FirstOrderModel* model = d_treg.getModel();
217 : 984 : uint32_t nasserted = model->getNumAssertedQuantifiers();
218 : :
219 [ + + ]: 3349 : for (uint32_t i = 0; i < nasserted; ++i)
220 : : {
221 : 2365 : Node q = model->getAssertedQuantifier(i);
222 [ + + ]: 2365 : if (d_ce_lits.find(q) == d_ce_lits.end())
223 : : {
224 : : // did not handle this quantified formula, skip
225 : 338 : continue;
226 : : }
227 [ + + ]: 2027 : if (model->isQuantifierActive(q))
228 : : {
229 : 1864 : d_active_quant.insert(q);
230 : 3728 : Node lit = getCeLiteral(q);
231 : :
232 : : bool value;
233 [ + - ]: 1864 : if (d_qstate.getValuation().hasSatValue(lit, value))
234 : : {
235 [ + + ]: 1864 : if (!value)
236 : : {
237 [ + - ]: 16 : if (!d_qstate.getValuation().isDecision(lit))
238 : : {
239 : 16 : model->setQuantifierActive(q, false);
240 : 16 : d_active_quant.erase(q);
241 : 16 : d_inactive_quant.insert(q);
242 [ + - ]: 16 : Trace("sygus-inst") << "Set inactive: " << q << std::endl;
243 : : }
244 : : }
245 : : }
246 : : }
247 : : }
248 : 984 : }
249 : :
250 : 402 : bool SygusInst::shouldProcess(Node q)
251 : : {
252 : : // Note that we currently process quantified formulas that other modules
253 : : // e.g. CEGQI have taken full ownership over.
254 : : // ignore internal quantifiers
255 : 402 : QuantAttributes& qattr = d_qreg.getQuantAttributes();
256 [ + + ]: 402 : if (qattr.isQuantBounded(q))
257 : : {
258 : 10 : return false;
259 : : }
260 : 392 : return true;
261 : : }
262 : :
263 : 612 : void SygusInst::check(Theory::Effort e, QEffort quant_e)
264 : : {
265 [ + - ]: 612 : Trace("sygus-inst") << "Check " << e << ", " << quant_e << std::endl;
266 : :
267 [ + + ]: 612 : if (quant_e != QEFFORT_STANDARD) return;
268 : :
269 : 290 : beginCallDebug();
270 : 290 : FirstOrderModel* model = d_treg.getModel();
271 : 290 : Instantiate* inst = d_qim.getInstantiate();
272 : 290 : TermDbSygus* db = d_treg.getTermDatabaseSygus();
273 : 580 : SygusExplain syexplain(d_env, db);
274 : 290 : NodeManager* nm = nodeManager();
275 : 290 : options::SygusInstMode mode = options().quantifiers.sygusInstMode;
276 : :
277 [ + + ]: 692 : for (const Node& q : d_active_quant)
278 : : {
279 : 402 : const std::vector<Node>& inst_constants = d_inst_constants.at(q);
280 : 402 : const std::vector<Node>& dt_evals = d_var_eval.at(q);
281 [ - + ][ - + ]: 402 : Assert(inst_constants.size() == dt_evals.size());
[ - - ]
282 [ - + ][ - + ]: 402 : Assert(inst_constants.size() == q[0].getNumChildren());
[ - - ]
283 : :
284 : 804 : std::vector<Node> terms, values, eval_unfold_lemmas;
285 [ + + ]: 2365 : for (size_t i = 0, size = q[0].getNumChildren(); i < size; ++i)
286 : : {
287 : 3926 : Node dt_var = inst_constants[i];
288 : 3926 : Node dt_eval = dt_evals[i];
289 : 3926 : Node value = model->getValue(dt_var);
290 : 3926 : Node t = datatypes::utils::sygusToBuiltin(value);
291 : 1963 : terms.push_back(t);
292 : 1963 : values.push_back(value);
293 : :
294 : 3926 : std::vector<Node> exp;
295 : 1963 : syexplain.getExplanationForEquality(dt_var, value, exp);
296 : 3926 : Node lem;
297 [ - + ]: 1963 : if (exp.empty())
298 : : {
299 : 0 : lem = dt_eval.eqNode(t);
300 : : }
301 : : else
302 : : {
303 : 5889 : lem = nm->mkNode(Kind::IMPLIES,
304 [ + + ]: 3926 : exp.size() == 1 ? exp[0] : nm->mkNode(Kind::AND, exp),
305 : 5889 : dt_eval.eqNode(t));
306 : : }
307 : 1963 : eval_unfold_lemmas.push_back(lem);
308 : : }
309 : :
310 [ + - ]: 402 : if (mode == options::SygusInstMode::PRIORITY_INST)
311 : : {
312 : 402 : if (!inst->addInstantiation(q,
313 : : terms,
314 : : InferenceId::QUANTIFIERS_INST_SYQI,
315 [ + + ]: 804 : nm->mkNode(Kind::SEXPR, values)))
316 : : {
317 : 130 : sendEvalUnfoldLemmas(eval_unfold_lemmas);
318 : : }
319 : : }
320 [ - - ]: 0 : else if (mode == options::SygusInstMode::PRIORITY_EVAL)
321 : : {
322 [ - - ]: 0 : if (!sendEvalUnfoldLemmas(eval_unfold_lemmas))
323 : : {
324 : 0 : inst->addInstantiation(q,
325 : : terms,
326 : : InferenceId::QUANTIFIERS_INST_SYQI,
327 : 0 : nm->mkNode(Kind::SEXPR, values));
328 : : }
329 : : }
330 : : else
331 : : {
332 : 0 : Assert(mode == options::SygusInstMode::INTERLEAVE);
333 : 0 : inst->addInstantiation(q,
334 : : terms,
335 : : InferenceId::QUANTIFIERS_INST_SYQI,
336 : 0 : nm->mkNode(Kind::SEXPR, values));
337 : 0 : sendEvalUnfoldLemmas(eval_unfold_lemmas);
338 : : }
339 : : }
340 : 290 : endCallDebug();
341 : : }
342 : :
343 : 130 : bool SygusInst::sendEvalUnfoldLemmas(const std::vector<Node>& lemmas)
344 : : {
345 : 130 : bool added_lemma = false;
346 [ + + ]: 1006 : for (const Node& lem : lemmas)
347 : : {
348 [ + - ]: 876 : Trace("sygus-inst") << "Evaluation unfolding: " << lem << std::endl;
349 : 876 : added_lemma |=
350 : 876 : d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_SYQI_EVAL_UNFOLD);
351 : : }
352 : 130 : return added_lemma;
353 : : }
354 : :
355 : 0 : bool SygusInst::checkCompleteFor(Node q)
356 : : {
357 : 0 : return d_inactive_quant.find(q) != d_inactive_quant.end();
358 : : }
359 : :
360 : 402 : void SygusInst::registerQuantifier(Node q)
361 : : {
362 [ - + ][ - + ]: 402 : Assert(d_ce_lemmas.find(q) == d_ce_lemmas.end());
[ - - ]
363 : :
364 [ + + ]: 402 : if (!shouldProcess(q))
365 : : {
366 : 18 : return;
367 : : }
368 : :
369 [ + - ]: 392 : Trace("sygus-inst") << "Register " << q << std::endl;
370 : :
371 : 392 : std::vector<Node> extra_cons;
372 : :
373 : : /* Collect relevant local ground terms for each variable type. */
374 : 392 : if (options().quantifiers.sygusInstScope == options::SygusInstScope::IN
375 [ - + ][ - - ]: 392 : || options().quantifiers.sygusInstScope == options::SygusInstScope::BOTH)
[ + - ]
376 : : {
377 : 784 : std::unordered_map<TypeNode, std::unordered_set<Node>> relevant_terms;
378 [ + + ]: 1000 : for (const Node& var : q[0])
379 : : {
380 : 1216 : TypeNode tn = var.getType();
381 : :
382 : : /* Collect relevant ground terms for type tn. */
383 [ + + ]: 608 : if (relevant_terms.find(tn) == relevant_terms.end())
384 : : {
385 : 818 : std::unordered_set<Node> terms;
386 : 818 : std::unordered_set<TNode> cache_max;
387 : 818 : std::unordered_map<TNode, std::pair<bool, bool>> cache_min;
388 : :
389 : 409 : getMinGroundTerms(options(), q, tn, terms, cache_min);
390 : 409 : getMaxGroundTerms(options(), q, tn, terms, cache_max);
391 : 409 : relevant_terms.emplace(tn, terms);
392 : : }
393 : :
394 : : /* Add relevant ground terms to grammar. */
395 : 608 : auto& terms = relevant_terms[tn];
396 [ + + ]: 2206 : for (const auto& t : terms)
397 : : {
398 : 1598 : TypeNode ttn = t.getType();
399 : 1598 : extra_cons.push_back(t);
400 [ + - ]: 1598 : Trace("sygus-inst") << "Adding (local) extra cons: " << t << std::endl;
401 : : }
402 : : }
403 : : }
404 : :
405 : : /* Collect relevant global ground terms for each variable type. */
406 : 392 : if (options().quantifiers.sygusInstScope == options::SygusInstScope::OUT
407 [ + - ][ - + ]: 392 : || options().quantifiers.sygusInstScope == options::SygusInstScope::BOTH)
[ - + ]
408 : : {
409 [ - - ]: 0 : for (const Node& var : q[0])
410 : : {
411 : 0 : TypeNode tn = var.getType();
412 : :
413 : : /* Collect relevant ground terms for type tn. */
414 [ - - ]: 0 : if (d_global_terms.find(tn) == d_global_terms.end())
415 : : {
416 : 0 : std::unordered_set<Node> terms;
417 : 0 : std::unordered_set<TNode> cache_max;
418 : 0 : std::unordered_map<TNode, std::pair<bool, bool>> cache_min;
419 : :
420 [ - - ]: 0 : for (const Node& a : d_notified_assertions)
421 : : {
422 : 0 : getMinGroundTerms(options(), a, tn, terms, cache_min, true);
423 : 0 : getMaxGroundTerms(options(), a, tn, terms, cache_max, true);
424 : : }
425 : 0 : d_global_terms.insert(tn, terms);
426 : : }
427 : :
428 : : /* Add relevant ground terms to grammar. */
429 : 0 : auto it = d_global_terms.find(tn);
430 [ - - ]: 0 : if (it != d_global_terms.end())
431 : : {
432 [ - - ]: 0 : for (const auto& t : (*it).second)
433 : : {
434 : 0 : TypeNode ttn = t.getType();
435 : 0 : extra_cons.push_back(t);
436 [ - - ]: 0 : Trace("sygus-inst")
437 : 0 : << "Adding (global) extra cons: " << t << std::endl;
438 : : }
439 : : }
440 : : }
441 : : }
442 : :
443 : : /* Construct grammar for each bound variable of 'q'. */
444 [ + - ]: 392 : Trace("sygus-inst") << "Process variables of " << q << std::endl;
445 : 392 : std::vector<TypeNode> types;
446 [ + + ]: 992 : for (const Node& var : q[0])
447 : : {
448 : 608 : addSpecialValues(var.getType(), extra_cons);
449 : : TypeNode tn = SygusGrammarCons::mkDefaultSygusType(
450 : 1216 : d_env, var.getType(), Node(), extra_cons);
451 : 608 : types.push_back(tn);
452 : :
453 [ + - ]: 1216 : Trace("sygus-inst") << "Construct (default) datatype for " << var
454 : 0 : << std::endl
455 [ - + ][ - - ]: 608 : << printer::smt2::Smt2Printer::sygusGrammarString(tn)
456 : 608 : << std::endl;
457 : : // In the rare case that the sygus grammar is not well-founded, we abort.
458 : : // This can happen, e.g. for datatypes whose only values involve
459 : : // uninterpreted sort subfields.
460 [ + + ]: 608 : if (!tn.isWellFounded())
461 : : {
462 : 8 : return;
463 : : }
464 : : }
465 : :
466 : 384 : registerCeLemma(q, types);
467 : : }
468 : :
469 : : /* Construct grammars for all bound variables of quantifier 'q'. Currently,
470 : : * we use the default grammar of the variable's type.
471 : : */
472 : 402 : void SygusInst::preRegisterQuantifier(Node q)
473 : : {
474 [ + + ]: 402 : if (d_ce_lemmas.find(q) == d_ce_lemmas.end())
475 : : {
476 : : // did not allocate a cex lemma for this
477 : 18 : return;
478 : : }
479 [ + - ]: 384 : Trace("sygus-inst") << "preRegister " << q << std::endl;
480 : 384 : addCeLemma(q);
481 : : }
482 : :
483 : 147 : void SygusInst::ppNotifyAssertions(const std::vector<Node>& assertions)
484 : : {
485 [ + + ]: 666 : for (const Node& a : assertions)
486 : : {
487 : 519 : d_notified_assertions.insert(a);
488 : : }
489 : 147 : }
490 : :
491 : 0 : std::string SygusInst::identify() const { return "sygus-inst"; }
492 : :
493 : : /*****************************************************************************/
494 : : /* private methods */
495 : : /*****************************************************************************/
496 : :
497 : 2248 : Node SygusInst::getCeLiteral(Node q)
498 : : {
499 : 2248 : auto it = d_ce_lits.find(q);
500 [ + + ]: 2248 : if (it != d_ce_lits.end())
501 : : {
502 : 1864 : return it->second;
503 : : }
504 : :
505 : 384 : NodeManager* nm = nodeManager();
506 : 1152 : Node sk = NodeManager::mkDummySkolem("CeLiteral", nm->booleanType());
507 : 768 : Node lit = d_qstate.getValuation().ensureLiteral(sk);
508 : 384 : d_ce_lits[q] = lit;
509 : 384 : return lit;
510 : : }
511 : :
512 : 384 : void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types)
513 : : {
514 [ - + ][ - + ]: 384 : Assert(q[0].getNumChildren() == types.size());
[ - - ]
515 [ - + ][ - + ]: 384 : Assert(d_ce_lemmas.find(q) == d_ce_lemmas.end());
[ - - ]
516 [ - + ][ - + ]: 384 : Assert(d_inst_constants.find(q) == d_inst_constants.end());
[ - - ]
517 [ - + ][ - + ]: 384 : Assert(d_var_eval.find(q) == d_var_eval.end());
[ - - ]
518 : :
519 [ + - ]: 384 : Trace("sygus-inst") << "Register CE Lemma for " << q << std::endl;
520 : :
521 : : /* Generate counterexample lemma for 'q'. */
522 : 384 : NodeManager* nm = nodeManager();
523 : 384 : SkolemManager* sm = nm->getSkolemManager();
524 : 384 : TermDbSygus* db = d_treg.getTermDatabaseSygus();
525 : :
526 : : // For each variable x_i of \forall x_i . P[x_i], create a fresh datatype
527 : : // instantiation constant ic_i with type types[i], and a Skolem eval_i whose
528 : : // type is is the same as x_i, and whose value will be used to instantiate x_i
529 : 768 : std::vector<Node> evals;
530 : 768 : std::vector<Node> inst_constants;
531 : : InstConstantAttribute ica;
532 [ + + ]: 984 : for (size_t i = 0, size = types.size(); i < size; ++i)
533 : : {
534 : 1200 : TypeNode tn = types[i];
535 : 1800 : TNode var = q[0][i];
536 : :
537 : : /* Create the instantiation constant and set attribute accordingly. */
538 : 1200 : Node ic = nm->mkInstConstant(tn);
539 : 600 : ic.setAttribute(ica, q);
540 [ + - ]: 600 : Trace("sygus-inst") << "Create " << ic << " for " << var << std::endl;
541 : :
542 : 600 : db->registerEnumerator(ic, ic, nullptr, ROLE_ENUM_MULTI_SOLUTION);
543 : :
544 : 2400 : std::vector<Node> args = {ic};
545 : 1200 : Node svl = tn.getDType().getSygusVarList();
546 [ - + ]: 600 : if (!svl.isNull())
547 : : {
548 : 0 : args.insert(args.end(), svl.begin(), svl.end());
549 : : }
550 : 1200 : Node eval = nm->mkNode(Kind::DT_SYGUS_EVAL, args);
551 : : // we use a Skolem constant here, instead of an application of an
552 : : // evaluation function, since we are not using the builtin support
553 : : // for evaluation functions. We use the DT_SYGUS_EVAL term so that the
554 : : // skolem construction here is deterministic and reproducible.
555 : 1200 : Node k = sm->mkPurifySkolem(eval);
556 : : // Requires instantiation constant attribute as well. This ensures that
557 : : // other instantiation methods, e.g. E-matching do not consider this term
558 : : // for instantiation, as it is model-unsound to do so.
559 : 600 : k.setAttribute(ica, q);
560 : :
561 : 600 : inst_constants.push_back(ic);
562 : 600 : evals.push_back(k);
563 : : }
564 : :
565 : 384 : d_inst_constants.emplace(q, inst_constants);
566 : 384 : d_var_eval.emplace(q, evals);
567 : :
568 : 768 : Node lit = getCeLiteral(q);
569 : 384 : d_qim.addPendingPhaseRequirement(lit, true);
570 : :
571 : : /* The decision strategy for quantified formula 'q' ensures that its
572 : : * counterexample literal is decided on first. It is user-context dependent.
573 : : */
574 [ - + ][ - + ]: 384 : Assert(d_dstrat.find(q) == d_dstrat.end());
[ - - ]
575 : : DecisionStrategy* ds = new DecisionStrategySingleton(
576 : 384 : d_env, "CeLiteral", lit, d_qstate.getValuation());
577 : :
578 : 384 : d_dstrat[q].reset(ds);
579 : 384 : d_qim.getDecisionManager()->registerStrategy(
580 : : DecisionManager::STRAT_QUANT_CEGQI_FEASIBLE, ds);
581 : :
582 : : /* Add counterexample lemma (lit => ~P[x_i/eval_i]) */
583 : : Node body =
584 : 1152 : q[1].substitute(q[0].begin(), q[0].end(), evals.begin(), evals.end());
585 : 768 : Node lem = nm->mkNode(Kind::OR, lit.negate(), body.negate());
586 : :
587 : 384 : d_ce_lemmas.emplace(std::make_pair(q, lem));
588 [ + - ]: 384 : Trace("sygus-inst") << "Register CE Lemma: " << lem << std::endl;
589 : 384 : }
590 : :
591 : 384 : void SygusInst::addCeLemma(Node q)
592 : : {
593 [ - + ][ - + ]: 384 : Assert(d_ce_lemmas.find(q) != d_ce_lemmas.end());
[ - - ]
594 : :
595 : : /* Already added in previous contexts. */
596 [ - + ]: 384 : if (d_ce_lemma_added.find(q) != d_ce_lemma_added.end()) return;
597 : :
598 : 384 : Node lem = d_ce_lemmas[q];
599 : 384 : d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_SYQI_CEX);
600 : 384 : d_ce_lemma_added.insert(q);
601 [ + - ]: 384 : Trace("sygus-inst") << "Add CE Lemma: " << lem << std::endl;
602 : : }
603 : :
604 : : } // namespace quantifiers
605 : : } // namespace theory
606 : : } // namespace cvc5::internal
|
