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 : : * A class for augmenting model-based instantiations via fast sygus enumeration.
11 : : */
12 : :
13 : : #include "theory/quantifiers/mbqi_enum.h"
14 : :
15 : : #include "expr/node_algorithm.h"
16 : : #include "expr/skolem_manager.h"
17 : : #include "expr/subs.h"
18 : : #include "printer/smt2/smt2_printer.h"
19 : : #include "smt/set_defaults.h"
20 : : #include "theory/datatypes/sygus_datatype_utils.h"
21 : : #include "theory/quantifiers/inst_strategy_mbqi.h"
22 : : #include "theory/quantifiers/instantiate.h"
23 : : #include "theory/quantifiers/sygus/sygus_enumerator.h"
24 : : #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
25 : : #include "theory/smt_engine_subsolver.h"
26 : : #include "util/random.h"
27 : :
28 : : namespace cvc5::internal {
29 : : namespace theory {
30 : : namespace quantifiers {
31 : :
32 : : class MbqiEnumTermEnumeratorCallback : protected EnvObj,
33 : : public SygusTermEnumeratorCallback
34 : : {
35 : : public:
36 : 14 : MbqiEnumTermEnumeratorCallback(Env& env) : EnvObj(env) {}
37 : 28 : virtual ~MbqiEnumTermEnumeratorCallback() {}
38 : : /** Filter duplicate/invalid built-in terms during SyGuS enumeration. */
39 : 924 : bool addTerm(const Node& n, std::unordered_set<Node>& bterms) override
40 : : {
41 : 924 : Node bn = datatypes::utils::sygusToBuiltin(n);
42 : 924 : bn = extendedRewrite(bn);
43 [ + + ]: 924 : if (bterms.find(bn) != bterms.end())
44 : : {
45 : 651 : return false;
46 : : }
47 [ + + ]: 273 : if (bn.getKind() == Kind::WITNESS)
48 : : {
49 [ + + ]: 63 : if (!expr::hasSubterm(bn[1], bn[0][0]))
50 : : {
51 : 35 : return false;
52 : : }
53 : : }
54 : 238 : bterms.insert(bn);
55 : 238 : return true;
56 : 924 : }
57 : : };
58 : :
59 : : /**
60 : : * Decide whether to inject witness/choice terms for grammar non-terminal `tn`.
61 : : **/
62 : 112 : bool introduceChoice(const Options& opts,
63 : : const TypeNode& tn,
64 : : const TypeNode& retType)
65 : : {
66 : : // never for Booleans or functions
67 [ + + ][ + + ]: 112 : if (tn.isBoolean() || tn.isFunction())
[ + + ]
68 : : {
69 : 77 : return false;
70 : : }
71 [ - + ]: 35 : if (opts.quantifiers.mbqiEnumChoiceGrammarAll)
72 : : {
73 : 0 : return true;
74 : : }
75 : 35 : return tn == retType;
76 : : }
77 : :
78 : : /**
79 : : * Decide whether MBQI term enumeration should be used for type `tn`.
80 : : */
81 : 259 : bool shouldEnumerate(CVC5_UNUSED const Options& opts, const TypeNode& tn)
82 : : {
83 : : // It may make sense to enumerate choice for FO uninterpreted sorts, but
84 : : // seems to not work well in practice.
85 [ + + ]: 259 : if (tn.isUninterpretedSort())
86 : : {
87 : 77 : return false;
88 : : }
89 : 182 : return true;
90 : : }
91 : :
92 : 91 : void MVarInfo::initialize(Env& env,
93 : : const Node& q,
94 : : const Node& v,
95 : : const std::vector<Node>& etrules)
96 : : {
97 : 91 : NodeManager* nm = env.getNodeManager();
98 : 91 : TypeNode tn = v.getType();
99 [ - + ][ - + ]: 91 : Assert(shouldEnumerate(env.getOptions(), tn));
[ - - ]
100 : 91 : TypeNode retType = tn;
101 : 91 : std::vector<Node> trules;
102 [ + + ]: 91 : if (tn.isFunction())
103 : : {
104 : 84 : std::vector<TypeNode> argTypes = tn.getArgTypes();
105 : 84 : retType = tn.getRangeType();
106 : 84 : std::vector<Node> vs;
107 [ + + ]: 173 : for (const TypeNode& tnc : argTypes)
108 : : {
109 : 89 : Node vc = NodeManager::mkBoundVar(tnc);
110 : 89 : vs.push_back(vc);
111 : 89 : }
112 : 84 : d_lamVars = nm->mkNode(Kind::BOUND_VAR_LIST, vs);
113 : 84 : trules.insert(trules.end(), vs.begin(), vs.end());
114 : 84 : }
115 : : // include free symbols from body of quantified formula if applicable
116 [ + - ]: 91 : if (env.getOptions().quantifiers.mbqiEnumFreeSymsGrammar)
117 : : {
118 : 91 : std::unordered_set<Node> syms;
119 : 91 : expr::getSymbols(q[1], syms);
120 : 91 : trules.insert(trules.end(), syms.begin(), syms.end());
121 : 91 : }
122 : : // include the external terminal rules
123 [ + + ]: 313 : for (const Node& symbol : etrules)
124 : : {
125 [ + + ]: 222 : if (std::find(trules.begin(), trules.end(), symbol) == trules.end())
126 : : {
127 : 84 : trules.push_back(symbol);
128 : : }
129 : : }
130 [ + - ]: 91 : Trace("mbqi-enum-grammar") << "Symbols: " << trules << std::endl;
131 : : SygusGrammarCons sgc;
132 : 91 : Node bvl;
133 : 91 : TypeNode tng = sgc.mkDefaultSygusType(env, retType, bvl, trules);
134 [ - + ]: 91 : if (TraceIsOn("mbqi-enum"))
135 : : {
136 [ - - ]: 0 : Trace("mbqi-enum") << "Enumerate terms for " << retType;
137 [ - - ]: 0 : if (!d_lamVars.isNull())
138 : : {
139 [ - - ]: 0 : Trace("mbqi-enum") << ", variable list " << d_lamVars;
140 : : }
141 [ - - ]: 0 : Trace("mbqi-enum") << std::endl;
142 [ - - ]: 0 : Trace("mbqi-enum-grammar") << "Based on grammar:" << std::endl;
143 [ - - ]: 0 : Trace("mbqi-enum-grammar")
144 : 0 : << printer::smt2::Smt2Printer::sygusGrammarString(tng) << std::endl;
145 : : }
146 : 91 : TypeNode tuse = tng;
147 : 91 : const Options& opts = env.getOptions();
148 [ + + ]: 91 : if (opts.quantifiers.mbqiEnumChoiceGrammar)
149 : : {
150 : : // we will be eliminating choice
151 : 21 : d_cenc.reset(new ChoiceElimNodeConverter(nm));
152 : 21 : TypeNode bt = nm->booleanType();
153 : : // take the original grammar
154 : 21 : SygusGrammar sgg({}, tng);
155 : 21 : const std::vector<Node>& nts = sgg.getNtSyms();
156 : 21 : std::vector<Node> ntAll = nts;
157 : : // Note we have to delay adding rules to the final combined grammar until
158 : : // all the non-terminals have been determined. This means we have to
159 : : // remember temporary information here. Note this would be easier if we
160 : : // could add non-terminals to grammars dynamically.
161 : 21 : std::map<TypeNode, std::shared_ptr<SygusGrammar>> typeToPredGrammar;
162 : 21 : std::map<TypeNode, Node> typeToWitnessRule;
163 [ + + ]: 91 : for (const Node& nt : nts)
164 : : {
165 : 70 : TypeNode ntt = nt.getType();
166 : : // choice for Boolean is not worthwhile
167 : : // in the rare case multiple nonterminals of the same type, skip
168 : 70 : if (!introduceChoice(opts, ntt, retType)
169 [ + + ][ - + ]: 70 : || typeToPredGrammar.find(ntt) != typeToPredGrammar.end())
[ + + ]
170 : : {
171 : 56 : continue;
172 : : }
173 : : // not Boolean?
174 : 28 : Node x = nm->mkBoundVar("x", ntt);
175 : 14 : trules.push_back(x);
176 [ + - ]: 28 : Trace("mbqi-enum-choice-grammar")
177 : 14 : << "Make predicate grammar " << trules << std::endl;
178 : 14 : TypeNode tnb = sgc.mkDefaultSygusType(env, bt, bvl, trules);
179 [ + - ]: 14 : Trace("mbqi-enum-choice-grammar") << "Predicate grammar:" << std::endl;
180 [ + - ]: 28 : Trace("mbqi-enum-choice-grammar")
181 [ - + ][ - - ]: 14 : << printer::smt2::Smt2Printer::sygusGrammarString(tnb) << std::endl;
182 : 14 : std::vector<Node> emptyVec;
183 : 14 : typeToPredGrammar[ntt] = std::make_shared<SygusGrammar>(emptyVec, tnb);
184 : 14 : SygusGrammar& sgb = *typeToPredGrammar[ntt].get();
185 : 14 : const std::vector<Node>& ntsb = sgb.getNtSyms();
186 : 14 : ntAll.insert(ntAll.end(), ntsb.begin(), ntsb.end());
187 : 14 : Node ntBool;
188 [ + - ]: 14 : for (const Node& snt : ntsb)
189 : : {
190 [ + - ]: 14 : if (snt.getType().isBoolean())
191 : : {
192 [ + - ]: 28 : Trace("mbqi-enum-choice-grammar")
193 : 14 : << "...found " << ntBool << std::endl;
194 : 14 : ntBool = snt;
195 : 14 : break;
196 : : }
197 : : }
198 [ - + ][ - + ]: 14 : Assert(!ntBool.isNull());
[ - - ]
199 : : Node witness = nm->mkNode(
200 : 28 : Kind::WITNESS, nm->mkNode(Kind::BOUND_VAR_LIST, x), ntBool);
201 : 14 : typeToWitnessRule[ntt] = witness;
202 : 14 : trules.pop_back();
203 [ + + ]: 70 : }
204 [ + + ]: 21 : if (!typeToPredGrammar.empty())
205 : : {
206 [ + - ]: 28 : Trace("mbqi-enum-choice-grammar")
207 : 14 : << "Make combined " << ntAll << std::endl;
208 : 14 : SygusGrammar sgcom({}, ntAll);
209 : : // get the non-terminal for Bool of the predicate grammar
210 [ + - ]: 28 : Trace("mbqi-enum-choice-grammar")
211 : 14 : << "Find non-terminal Bool in predicate grammar..." << std::endl;
212 : : // fill in the predicate grammars
213 : 14 : for (std::pair<const TypeNode, std::shared_ptr<SygusGrammar>>& tpg :
214 [ + + ]: 42 : typeToPredGrammar)
215 : : {
216 : 14 : SygusGrammar& sgb = *tpg.second.get();
217 : 14 : const std::vector<Node>& ntsb = sgb.getNtSyms();
218 [ + + ]: 56 : for (const Node& nt : ntsb)
219 : : {
220 : 42 : const std::vector<Node>& rules = sgb.getRulesFor(nt);
221 : 42 : sgcom.addRules(nt, rules);
222 : : }
223 : : }
224 : : // fill in the main grammar
225 [ + + ]: 56 : for (const Node& nt : nts)
226 : : {
227 [ + - ]: 84 : Trace("mbqi-enum-choice-grammar")
228 : 42 : << "- non-terminal in sgg: " << nt << std::endl;
229 : 42 : std::vector<Node> rules = sgg.getRulesFor(nt);
230 : 42 : TypeNode ntt = nt.getType();
231 [ + + ]: 42 : if (introduceChoice(opts, ntt, retType))
232 : : {
233 [ - + ][ - + ]: 14 : Assert(typeToWitnessRule.find(ntt) != typeToWitnessRule.end());
[ - - ]
234 : 14 : Node witness = typeToWitnessRule[ntt];
235 [ + - ]: 28 : Trace("mbqi-enum-choice-grammar")
236 : 14 : << "...add " << witness << " to " << nt << std::endl;
237 : 14 : rules.insert(rules.begin(), witness);
238 : 14 : }
239 : 42 : sgcom.addRules(nt, rules);
240 : 42 : }
241 : 14 : TypeNode gcom = sgcom.resolve();
242 [ + - ]: 14 : Trace("mbqi-enum-choice-grammar") << "Combined grammar:" << std::endl;
243 [ + - ]: 28 : Trace("mbqi-enum-choice-grammar")
244 [ - + ][ - - ]: 14 : << printer::smt2::Smt2Printer::sygusGrammarString(gcom) << std::endl;
245 : 14 : tuse = gcom;
246 [ + - ]: 14 : d_senumCb.reset(new MbqiEnumTermEnumeratorCallback(env));
247 : 14 : }
248 : 21 : }
249 : 91 : d_senum.reset(new SygusTermEnumerator(env, tuse, d_senumCb.get()));
250 : 91 : }
251 : :
252 : 21 : MVarInfo::ChoiceElimNodeConverter::ChoiceElimNodeConverter(NodeManager* nm)
253 : 21 : : NodeConverter(nm)
254 : : {
255 : 21 : }
256 : 220 : Node MVarInfo::ChoiceElimNodeConverter::postConvert(Node n)
257 : : {
258 [ + + ]: 220 : if (n.getKind() == Kind::WITNESS)
259 : : {
260 : 28 : NodeManager* nm = d_nm;
261 [ + - ]: 28 : Trace("mbqi-enum-choice-grammar") << "---> convert " << n << std::endl;
262 : 28 : std::unordered_set<Node> fvs;
263 : 28 : expr::getFreeVariables(n, fvs);
264 : 56 : Node exists = nm->mkNode(Kind::FORALL, n[0], n[1].negate());
265 : 56 : TypeNode retType = n[0][0].getType();
266 : 28 : std::vector<TypeNode> argTypes;
267 : 28 : std::vector<Node> ubvl;
268 [ + + ]: 56 : for (const Node& v : fvs)
269 : : {
270 : 28 : ubvl.push_back(v);
271 : 28 : argTypes.push_back(v.getType());
272 : : }
273 [ + - ]: 28 : if (!argTypes.empty())
274 : : {
275 : 28 : retType = nm->mkFunctionType(argTypes, retType);
276 : : }
277 : 28 : SkolemManager* skm = nm->getSkolemManager();
278 : 28 : Node sym = skm->mkInternalSkolemFunction(
279 : 56 : InternalSkolemId::MBQI_CHOICE_FUN, retType, {n});
280 [ + - ]: 56 : Trace("mbqi-enum-choice-fun")
281 : 28 : << "Choice: " << sym << " for " << n << std::endl;
282 : 28 : Node h = sym;
283 [ + - ]: 28 : if (!ubvl.empty())
284 : : {
285 : 28 : std::vector<Node> wchildren;
286 : 28 : wchildren.push_back(h);
287 : 28 : wchildren.insert(wchildren.end(), ubvl.begin(), ubvl.end());
288 : 28 : h = nm->mkNode(Kind::APPLY_UF, wchildren);
289 : 28 : }
290 [ - + ][ - + ]: 84 : AssertEqual(h.getType(), n.getType());
[ - - ]
291 : 28 : Subs subs;
292 : 28 : subs.add(n[0][0], h);
293 : 28 : Node kpred = subs.apply(n[1]);
294 : 56 : Node lem = nm->mkNode(Kind::OR, exists, kpred);
295 [ + - ]: 28 : if (!ubvl.empty())
296 : : {
297 : : // use h(x) as the trigger, which is a legal trigger since it is applied
298 : : // to the exact variable list of the quantified formula.
299 : : Node ipl = nm->mkNode(Kind::INST_PATTERN_LIST,
300 : 56 : nm->mkNode(Kind::INST_PATTERN, h));
301 : 112 : lem = nm->mkNode(
302 : 84 : Kind::FORALL, nm->mkNode(Kind::BOUND_VAR_LIST, ubvl), lem, ipl);
303 : 28 : }
304 [ + - ]: 28 : Trace("mbqi-enum-debug") << sym << " for " << n << std::endl;
305 [ + - ]: 28 : Trace("mbqi-enum-choice-grammar") << "-----> lemma " << lem << std::endl;
306 : 28 : d_lemmas[sym] = lem;
307 : 28 : return h;
308 : 28 : }
309 : 192 : return n;
310 : : }
311 : :
312 : 315 : std::vector<std::pair<Node, InferenceId>> MVarInfo::getEnumeratedLemmas(
313 : : const Node& t)
314 : : {
315 : 315 : std::vector<std::pair<Node, InferenceId>> lemmas;
316 [ + + ]: 315 : if (d_cenc != nullptr)
317 : : {
318 : 70 : lemmas = d_cenc->getEnumeratedLemmas(t);
319 : : }
320 : 315 : return lemmas;
321 : 0 : }
322 : :
323 : : std::vector<std::pair<Node, InferenceId>>
324 : 70 : MVarInfo::ChoiceElimNodeConverter::getEnumeratedLemmas(const Node& t)
325 : : {
326 : 70 : std::vector<std::pair<Node, InferenceId>> lemmas;
327 : 70 : std::unordered_set<Node> syms;
328 : 70 : expr::getSymbols(t, syms, d_visited);
329 [ + - ]: 70 : Trace("mbqi-enum-debug") << "getEnumeratedLemmas for " << t << std::endl;
330 : 70 : std::map<Node, Node>::iterator itl;
331 [ + + ]: 119 : for (const Node& s : syms)
332 : : {
333 [ + - ]: 49 : Trace("mbqi-enum-debug") << "...is lemma sym " << s << "?" << std::endl;
334 : 49 : itl = d_lemmas.find(s);
335 [ + + ]: 49 : if (itl != d_lemmas.end())
336 : : {
337 : 28 : lemmas.emplace_back(itl->second,
338 : 56 : InferenceId::QUANTIFIERS_MBQI_ENUM_CHOICE);
339 : : }
340 : : }
341 : 140 : return lemmas;
342 : 70 : }
343 : :
344 : 8334 : Node MVarInfo::getEnumeratedTerm(NodeManager* nm, size_t i)
345 : : {
346 : 8334 : size_t nullCount = 0;
347 [ + + ]: 22608 : while (i >= d_enum.size())
348 : : {
349 : 14339 : Node curr = d_senum->getCurrent();
350 [ + - ]: 14339 : Trace("mbqi-enum-debug") << "Enumerate: " << curr << std::endl;
351 [ + + ]: 14339 : if (!curr.isNull())
352 : : {
353 : : // use converter if it exists
354 [ + + ]: 3468 : if (d_cenc != nullptr)
355 : : {
356 : 89 : curr = d_cenc->convert(curr);
357 : : }
358 [ + + ]: 3468 : if (!d_lamVars.isNull())
359 : : {
360 : 843 : curr = nm->mkNode(Kind::LAMBDA, d_lamVars, curr);
361 : : }
362 [ - + ][ - + ]: 3468 : Assert(!curr.isNull());
[ - - ]
363 : 3468 : d_enum.push_back(curr);
364 : 3468 : nullCount = 0;
365 : : }
366 : : else
367 : : {
368 : 10871 : nullCount++;
369 [ + + ]: 10871 : if (nullCount > 100)
370 : : {
371 : : // break if we aren't making progress
372 : 65 : break;
373 : : }
374 : : }
375 [ - + ]: 14274 : if (!d_senum->incrementPartial())
376 : : {
377 : : // enumeration is finished
378 : 0 : break;
379 : : }
380 [ + + ]: 14339 : }
381 [ + + ]: 8334 : if (i >= d_enum.size())
382 : : {
383 [ + - ]: 65 : Trace("mbqi-enum-debug") << "... return null" << std::endl;
384 : 65 : return Node::null();
385 : : }
386 [ - + ][ - + ]: 8269 : Assert(!d_enum[i].isNull());
[ - - ]
387 : 8269 : return d_enum[i];
388 : : }
389 : :
390 : 133 : void MQuantInfo::initialize(Env& env, InstStrategyMbqi& parent, const Node& q)
391 : : {
392 : : // The externally provided terminal rules. This set is shared between
393 : : // all variables we instantiate.
394 : 133 : std::vector<Node> etrules;
395 : : // include the global symbols if applicable
396 [ + - ]: 133 : if (env.getOptions().quantifiers.mbqiEnumGlobalSymGrammar)
397 : : {
398 : 133 : const context::CDHashSet<Node>& gsyms = parent.getGlobalSyms();
399 [ + + ]: 565 : for (const Node& v : gsyms)
400 : : {
401 : 432 : etrules.push_back(v);
402 : 432 : }
403 : : }
404 [ + + ]: 301 : for (const Node& v : q[0])
405 : : {
406 : 168 : size_t index = d_vinfo.size();
407 : 168 : d_vinfo.emplace_back();
408 : 168 : TypeNode vtn = v.getType();
409 : : // if enumerated, add to list
410 [ + + ]: 168 : if (shouldEnumerate(env.getOptions(), vtn))
411 : : {
412 : 91 : d_indices.push_back(index);
413 : : }
414 : : else
415 : : {
416 : 77 : d_nindices.push_back(index);
417 : : // include variables defined in terms of others if applicable
418 [ + - ]: 77 : if (env.getOptions().quantifiers.mbqiEnumExtVarsGrammar)
419 : : {
420 : 77 : etrules.push_back(v);
421 : : }
422 : : }
423 : 301 : }
424 : : // initialize the variables we are instantiating
425 [ + + ]: 224 : for (size_t index : d_indices)
426 : : {
427 : : // initialize the variables we are instantiating
428 : 91 : d_vinfo[index].initialize(env, q, q[0][index], etrules);
429 : : }
430 : 133 : }
431 : :
432 : 651 : MVarInfo& MQuantInfo::getVarInfo(size_t index)
433 : : {
434 [ - + ][ - + ]: 651 : Assert(index < d_vinfo.size());
[ - - ]
435 : 651 : return d_vinfo[index];
436 : : }
437 : :
438 : 434 : std::vector<size_t> MQuantInfo::getInstIndices() { return d_indices; }
439 : 434 : std::vector<size_t> MQuantInfo::getNoInstIndices() { return d_nindices; }
440 : :
441 : 1087 : MbqiEnum::MbqiEnum(Env& env, InstStrategyMbqi& parent)
442 : 1087 : : EnvObj(env), d_parent(parent)
443 : : {
444 : 1087 : d_subOptions.copyValues(options());
445 : 1087 : d_subOptions.write_quantifiers().instMaxRounds = 5;
446 : 1087 : smt::SetDefaults::disableChecking(d_subOptions);
447 : 1087 : }
448 : :
449 : 434 : MQuantInfo& MbqiEnum::getOrMkQuantInfo(const Node& q)
450 : : {
451 : 434 : auto [it, inserted] = d_qinfo.try_emplace(q);
452 [ + + ]: 434 : if (inserted)
453 : : {
454 : 133 : it->second.initialize(d_env, d_parent, q);
455 : : }
456 : 434 : return it->second;
457 : : }
458 : :
459 : 434 : bool MbqiEnum::constructInstantiation(
460 : : const Node& q,
461 : : const Node& query,
462 : : const std::vector<Node>& vars,
463 : : std::vector<Node>& mvs,
464 : : const std::map<Node, Node>& mvFreshVar,
465 : : std::vector<std::pair<Node, InferenceId>>& auxLemmas)
466 : : {
467 [ - + ][ - + ]: 434 : Assert(q[0].getNumChildren() == vars.size());
[ - - ]
468 [ - + ][ - + ]: 434 : Assert(vars.size() == mvs.size());
[ - - ]
469 [ - + ]: 434 : if (TraceIsOn("mbqi-enum"))
470 : : {
471 [ - - ]: 0 : Trace("mbqi-enum") << "Instantiate " << q << std::endl;
472 [ - - ]: 0 : for (size_t i = 0, nvars = vars.size(); i < nvars; i++)
473 : : {
474 : 0 : Trace("mbqi-enum") << " " << q[0][i] << " -> " << mvs[i] << std::endl;
475 : : }
476 : : }
477 : 434 : SubsolverSetupInfo ssi(d_env, d_subOptions);
478 : 434 : MQuantInfo& qi = getOrMkQuantInfo(q);
479 : 434 : std::vector<size_t> indices = qi.getInstIndices();
480 : 434 : std::vector<size_t> nindices = qi.getNoInstIndices();
481 : 434 : Subs inst;
482 : 434 : Subs vinst;
483 : 434 : std::unordered_map<Node, Node> tmpCMap;
484 [ + + ]: 602 : for (size_t i : nindices)
485 : : {
486 : 168 : Node v = mvs[i];
487 : 168 : v = d_parent.convertFromModel(v, tmpCMap, mvFreshVar);
488 [ - + ]: 168 : if (v.isNull())
489 : : {
490 [ - - ]: 0 : Trace("mbqi-enum-model") << "Failed to convert " << v << std::endl;
491 : 0 : return false;
492 : : }
493 [ + - ]: 336 : Trace("mbqi-enum-model")
494 : 168 : << "* Assume: " << q[0][i] << " -> " << v << std::endl;
495 : : // if we don't enumerate it, we are already considering this instantiation
496 : 168 : inst.add(vars[i], v);
497 : 168 : vinst.add(q[0][i], v);
498 [ + - ]: 168 : }
499 : 434 : Node queryCurr = query;
500 [ + - ]: 434 : Trace("mbqi-enum-model") << "...query is " << queryCurr << std::endl;
501 : 434 : queryCurr = rewrite(inst.apply(queryCurr));
502 [ + - ]: 434 : Trace("mbqi-enum-model") << "...processed is " << queryCurr << std::endl;
503 : : // consider variables in random order, for diversity of instantiations
504 : 434 : std::shuffle(indices.begin(), indices.end(), Random::getRandom());
505 : 434 : bool addedInst = false;
506 [ + + ]: 749 : for (size_t i = 0, isize = indices.size(); i < isize; i++)
507 : : {
508 : 336 : size_t ii = indices[i];
509 : 336 : TNode v = vars[ii];
510 : 336 : MVarInfo& vi = qi.getVarInfo(ii);
511 : 336 : size_t cindex = 0;
512 : 336 : bool success = false;
513 : : bool successEnum;
514 : 336 : bool lastVar = (i + 1 == isize);
515 : : do
516 : : {
517 : 8334 : Node ret = vi.getEnumeratedTerm(nodeManager(), cindex);
518 : 8334 : cindex++;
519 : 8334 : Node retc;
520 [ + + ]: 8334 : if (!ret.isNull())
521 : : {
522 [ + - ]: 16538 : Trace("mbqi-enum-debug") << "- Try candidate: " << q.getId() << " " << v
523 : 8269 : << " " << cindex << " " << ret << std::endl;
524 [ + - ]: 8269 : Trace("mbqi-enum") << "- Try candidate: " << ret << std::endl;
525 : : // apply current substitution (to account for cases where ret has
526 : : // other variables in its grammar).
527 : 8269 : ret = vinst.apply(ret);
528 : 8269 : retc = ret;
529 : 8269 : successEnum = true;
530 : : // now convert the value
531 : 8269 : std::unordered_map<Node, Node> tmpConvertMap;
532 : 8269 : std::map<TypeNode, std::unordered_set<Node>> freshVarType;
533 : 8269 : retc = d_parent.convertToQuery(retc, tmpConvertMap, freshVarType);
534 : 8269 : }
535 : : else
536 : : {
537 [ + - ]: 130 : Trace("mbqi-enum-debug")
538 : 65 : << "- Failed to enumerate candidate" << std::endl;
539 : : // if we failed to enumerate, just try the original
540 : 65 : Node mc = d_parent.convertFromModel(mvs[ii], tmpCMap, mvFreshVar);
541 [ - + ]: 65 : if (mc.isNull())
542 : : {
543 [ - - ]: 0 : Trace("mbqi-enum-debug")
544 : 0 : << "Failed to convert " << mvs[ii] << std::endl;
545 : : // if failed to convert, we fail
546 : 0 : return false;
547 : : }
548 : 65 : ret = mc;
549 : 65 : retc = mc;
550 : 65 : successEnum = false;
551 [ + - ]: 65 : }
552 [ + - ]: 16668 : Trace("mbqi-enum-model")
553 : 8334 : << "- Converted candidate: " << v << " -> " << retc << std::endl;
554 : 8334 : Node queryCheck;
555 : : // see if it is still satisfiable, if still SAT, we replace
556 : 8334 : queryCheck = queryCurr.substitute(v, TNode(retc));
557 : 8334 : queryCheck = rewrite(queryCheck);
558 [ + - ]: 8334 : Trace("mbqi-enum-model") << "...check " << queryCheck << std::endl;
559 : 8334 : Result r = d_parent.checkWithSubsolverSimple(queryCheck, ssi);
560 : 8334 : success = (r != Result::UNSAT);
561 [ + + ]: 8334 : if (success)
562 : : {
563 : : // remember the updated query
564 : 637 : queryCurr = queryCheck;
565 [ + - ]: 637 : Trace("mbqi-enum-model") << "...success" << std::endl;
566 : 1274 : Trace("mbqi-enum") << "* Enumerated " << q[0][ii] << " -> " << ret
567 : 637 : << std::endl;
568 : 637 : mvs[ii] = ret;
569 : 637 : vinst.add(q[0][ii], ret);
570 : : }
571 : : // We verify the lemma is successfully added here. If it is not, then
572 : : // success is false and we continue the enumeration.
573 [ + - ][ + + ]: 8334 : if (lastVar && success)
574 : : {
575 : 637 : success = d_parent.tryInstantiation(
576 : : q, mvs, InferenceId::QUANTIFIERS_INST_MBQI_ENUM, mvFreshVar);
577 [ + - ][ + + ]: 631 : addedInst = addedInst || success;
578 : : }
579 : :
580 [ + + ][ + + ]: 8328 : if (!success && !successEnum)
581 : : {
582 : : // we did not enumerate a candidate, and tried the original, which
583 : : // failed.
584 [ + - ]: 15 : Trace("mbqi-enum-debug") << "Failed to enumerate" << std::endl;
585 : 15 : return false;
586 : : }
587 [ + + ][ + + ]: 16710 : } while (!success);
[ + + ][ + + ]
[ + + ]
588 [ + + ]: 336 : }
589 : : // See if there are auxiliary lemmas, if so, add them to the returned
590 : : // vector.
591 [ + - ]: 413 : Trace("mbqi-enum-debug") << "Instantiate: " << q.getId() << std::endl;
592 [ + + ]: 728 : for (size_t i = 0, isize = indices.size(); i < isize; i++)
593 : : {
594 : 315 : size_t ii = indices[i];
595 : 315 : TNode v = vars[ii];
596 [ + - ]: 315 : Trace("mbqi-enum-debug") << "- " << v << " -> " << mvs[ii] << std::endl;
597 : 315 : MVarInfo& vi = qi.getVarInfo(ii);
598 : : std::vector<std::pair<Node, InferenceId>> alv =
599 : 315 : vi.getEnumeratedLemmas(mvs[ii]);
600 [ + - ]: 630 : Trace("mbqi-enum-debug")
601 : 315 : << "..." << alv.size() << " aux lemmas" << std::endl;
602 : 315 : auxLemmas.insert(auxLemmas.end(), alv.begin(), alv.end());
603 : 315 : }
604 : 413 : return addedInst;
605 : 470 : }
606 : : } // namespace quantifiers
607 : : } // namespace theory
608 : : } // namespace cvc5::internal
|
