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