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 : : * Model-based quantifier instantiation
11 : : */
12 : :
13 : : #include "theory/quantifiers/inst_strategy_mbqi.h"
14 : :
15 : : #include "expr/node_algorithm.h"
16 : : #include "expr/skolem_manager.h"
17 : : #include "expr/subs.h"
18 : : #include "options/arrays_options.h"
19 : : #include "printer/smt2/smt2_printer.h"
20 : : #include "smt/set_defaults.h"
21 : : #include "theory/quantifiers/first_order_model.h"
22 : : #include "theory/quantifiers/instantiate.h"
23 : : #include "theory/quantifiers/mbqi_enum.h"
24 : : #include "theory/quantifiers/quantifiers_rewriter.h"
25 : : #include "theory/quantifiers/skolemize.h"
26 : : #include "theory/quantifiers/term_util.h"
27 : : #include "theory/strings/theory_strings_utils.h"
28 : : #include "theory/uf/function_const.h"
29 : :
30 : : using namespace std;
31 : : using namespace cvc5::internal::kind;
32 : :
33 : : namespace cvc5::internal {
34 : : namespace theory {
35 : : namespace quantifiers {
36 : :
37 : 540 : InstStrategyMbqi::InstStrategyMbqi(Env& env,
38 : : QuantifiersState& qs,
39 : : QuantifiersInferenceManager& qim,
40 : : QuantifiersRegistry& qr,
41 : 540 : TermRegistry& tr)
42 : 540 : : QuantifiersModule(env, qs, qim, qr, tr), d_globalSyms(userContext())
43 : : {
44 : : // some kinds may appear in model values that cannot be asserted
45 : : // if arraysExp is enabled, we allow STORE_ALL terms in assertions.
46 [ + - ]: 540 : if (!options().arrays.arraysExp)
47 : : {
48 : 540 : d_nonClosedKinds.insert(Kind::STORE_ALL);
49 : : }
50 : 540 : d_nonClosedKinds.insert(Kind::CODATATYPE_BOUND_VARIABLE);
51 : 540 : d_nonClosedKinds.insert(Kind::UNINTERPRETED_SORT_VALUE);
52 : : // may appear in certain models e.g. strings of excessive length
53 : 540 : d_nonClosedKinds.insert(Kind::WITNESS);
54 : :
55 [ + + ]: 540 : if (options().quantifiers.mbqiEnum)
56 : : {
57 : 353 : d_msenum.reset(new MbqiEnum(env, *this));
58 : : }
59 : 540 : d_subOptions.copyValues(options());
60 : 540 : d_subOptions.write_quantifiers().instMaxRounds = 5;
61 : 540 : smt::SetDefaults::disableChecking(d_subOptions);
62 : 540 : }
63 : :
64 : 1174 : void InstStrategyMbqi::ppNotifyAssertions(const std::vector<Node>& assertions)
65 : : {
66 : : // collecting global symbols from all available assertions
67 : 1174 : Skolemize* sk = d_qim.getSkolemize();
68 [ + + ]: 5244 : for (const Node& a : assertions)
69 : : {
70 : 4070 : std::unordered_set<Node> cur_syms;
71 : 4070 : expr::getSymbols(a, cur_syms);
72 : : // Iterate over the symbols in the current assertion
73 [ + + ]: 9710 : for (const Node& s : cur_syms)
74 : : {
75 : : // Add the symbol to syms if it's not already present
76 : 5640 : d_globalSyms.insert(s);
77 : : }
78 [ + + ]: 4070 : if (a.getKind() == Kind::FORALL)
79 : : {
80 : 416 : continue;
81 : : }
82 : : // also consider skolems for (non-top-level) quantified formulas.
83 : 3654 : std::unordered_set<Node> qs;
84 : 3654 : expr::getSubtermsKind(Kind::FORALL, a, qs, false);
85 [ + + ]: 3910 : for (const Node& q : qs)
86 : : {
87 : 256 : std::vector<Node> ks = sk->getSkolemConstants(q);
88 [ + + ]: 722 : for (const Node& s : ks)
89 : : {
90 : 466 : d_globalSyms.insert(s);
91 : : }
92 : 256 : }
93 [ + + ]: 4070 : }
94 : 1174 : }
95 : :
96 : 0 : const context::CDHashSet<Node>& InstStrategyMbqi::getGlobalSyms() const
97 : : {
98 : 0 : return d_globalSyms;
99 : : }
100 : :
101 : 874 : void InstStrategyMbqi::reset_round(CVC5_UNUSED Theory::Effort e)
102 : : {
103 : 874 : d_quantChecked.clear();
104 : 874 : }
105 : :
106 : 1276 : bool InstStrategyMbqi::needsCheck(Theory::Effort e)
107 : : {
108 : 1276 : return e >= Theory::EFFORT_LAST_CALL;
109 : : }
110 : :
111 : 354 : QuantifiersModule::QEffort InstStrategyMbqi::needsModel(
112 : : CVC5_UNUSED Theory::Effort e)
113 : : {
114 : 354 : return QEFFORT_MODEL;
115 : : }
116 : :
117 : 998 : void InstStrategyMbqi::check(Theory::Effort e, QEffort quant_e)
118 : : {
119 [ + - ][ + + ]: 998 : if (e != Theory::EFFORT_LAST_CALL || quant_e != QEFFORT_MODEL)
120 : : {
121 : 717 : return;
122 : : }
123 : 281 : beginCallDebug();
124 : 281 : FirstOrderModel* fm = d_treg.getModel();
125 [ - + ]: 281 : if (TraceIsOn("mbqi-model-exp"))
126 : : {
127 : 0 : eq::EqualityEngine* ee = fm->getEqualityEngine();
128 [ - - ]: 0 : Trace("mbqi-model-exp") << "=== InstStrategyMbqi::check" << std::endl;
129 [ - - ]: 0 : Trace("mbqi-model-exp") << "Ground model:" << std::endl;
130 : 0 : Trace("mbqi-model-exp") << ee->debugPrintEqc() << std::endl;
131 [ - - ]: 0 : Trace("mbqi-model-exp") << std::endl;
132 : : }
133 : : // see if the negation of each quantified formula is satisfiable in the model
134 : 281 : std::vector<Node> disj;
135 : 281 : std::vector<TNode> visit;
136 [ + + ]: 623 : for (size_t i = 0, nquant = fm->getNumAssertedQuantifiers(); i < nquant; i++)
137 : : {
138 : 342 : Node q = fm->getAssertedQuantifier(i);
139 [ - + ]: 342 : if (!d_qreg.hasOwnership(q, this))
140 : : {
141 : 0 : continue;
142 : : }
143 : 342 : process(q);
144 [ + - ]: 342 : }
145 [ + - ]: 562 : Trace("mbqi-model-exp") << "=== InstStrategyMbqi::check finished"
146 : 281 : << std::endl;
147 : 281 : endCallDebug();
148 : 281 : }
149 : :
150 : 41 : bool InstStrategyMbqi::checkCompleteFor(Node q)
151 : : {
152 : 41 : return d_quantChecked.find(q) != d_quantChecked.end();
153 : : }
154 : :
155 : 342 : void InstStrategyMbqi::process(Node q)
156 : : {
157 [ - + ][ - + ]: 342 : Assert(q.getKind() == Kind::FORALL);
[ - - ]
158 [ + - ]: 342 : Trace("mbqi-model-exp") << "* Process quantified formula: " << q << std::endl;
159 [ + - ]: 342 : Trace("mbqi") << "Process quantified formula: " << q << std::endl;
160 : : // Cache mapping terms in the skolemized body of q to the form passed to
161 : : // the subsolver. This is local to this call.
162 : 342 : std::unordered_map<Node, Node> tmpConvertMap;
163 : : // list of fresh variables per type
164 : 342 : std::map<TypeNode, std::unordered_set<Node> > freshVarType;
165 : : // model values to the fresh variables
166 : 342 : std::map<Node, Node> mvToFreshVar;
167 : :
168 : 342 : NodeManager* nm = nodeManager();
169 : 342 : const RepSet* rs = d_treg.getModel()->getRepSet();
170 : 342 : FirstOrderModel* fm = d_treg.getModel();
171 : :
172 : : // allocate the skolem variables
173 : 342 : Subs skolems;
174 [ + + ]: 813 : for (const Node& v : q[0])
175 : : {
176 : 471 : Node k = mkMbqiSkolem(v);
177 : 471 : skolems.add(v, k);
178 : : // do not take its model value (which does not exist) in conversion below
179 : 471 : tmpConvertMap[k] = k;
180 : 813 : }
181 : : // compute the skolemization in a separate traversal instead of mapping
182 : : // bound variables to skolems. This is to ensure we avoid variable shadowing
183 : : // for model values for functions
184 : 342 : Node skq = skolems.apply(q[1]);
185 : : // convert to query
186 : 342 : Node cbody = convertToQuery(skq, tmpConvertMap, freshVarType);
187 [ + - ]: 342 : Trace("mbqi") << "- converted body: " << cbody << std::endl;
188 : :
189 : : // check if there are any bad kinds
190 [ + + ]: 342 : if (cbody.isNull())
191 : : {
192 [ + - ]: 4 : Trace("mbqi-model-exp") << "...INTERNAL FAIL" << std::endl;
193 [ + - ]: 4 : Trace("mbqi") << "...failed to convert to query" << std::endl;
194 : 4 : return;
195 : : }
196 [ - + ][ - + ]: 338 : Assert(!expr::hasSubtermKinds(d_nonClosedKinds, cbody));
[ - - ]
197 : :
198 : 338 : std::vector<Node> constraints;
199 : :
200 : : // constraint: the negation of the skolemized body
201 : 676 : Node bquery = rewrite(cbody.negate());
202 [ + + ]: 338 : if (!bquery.isConst())
203 : : {
204 : : // if no nested check, don't assert the subquery if it contains quantifiers
205 : 891 : if (options().quantifiers.mbqiNestedCheck
206 [ - + ][ - - ]: 297 : || !expr::hasSubtermKind(Kind::FORALL, bquery))
[ - + ][ + - ]
[ - - ]
207 : : {
208 : 297 : constraints.push_back(bquery);
209 : : }
210 : : }
211 [ + + ]: 41 : else if (!bquery.getConst<bool>())
212 : : {
213 : 39 : d_quantChecked.insert(q);
214 [ + - ]: 39 : Trace("mbqi-model-exp") << "...SUCCESS, by rewriting" << std::endl;
215 [ + - ]: 39 : Trace("mbqi") << "...success, by rewriting" << std::endl;
216 : 39 : return;
217 : : }
218 : : // ensure the entire domain of uninterpreted sorts are converted
219 : 299 : std::unordered_set<TypeNode> processedUsort;
220 [ + + ]: 721 : for (const Node& k : skolems.d_subs)
221 : : {
222 : 422 : TypeNode tn = k.getType();
223 : 422 : if (!tn.isUninterpretedSort()
224 [ + + ][ + + ]: 422 : || processedUsort.find(tn) != processedUsort.end())
[ + + ]
225 : : {
226 : 369 : continue;
227 : : }
228 : 53 : processedUsort.insert(tn);
229 : 53 : const std::vector<Node>* treps = rs->getTypeRepsOrNull(tn);
230 [ + + ]: 53 : if (treps != nullptr)
231 : : {
232 [ + + ]: 229 : for (const Node& r : *treps)
233 : : {
234 : 183 : Node rv = fm->getValue(r);
235 [ - + ][ - + ]: 183 : Assert(rv.getKind() == Kind::UNINTERPRETED_SORT_VALUE);
[ - - ]
236 : 183 : convertToQuery(rv, tmpConvertMap, freshVarType);
237 : 183 : }
238 : : }
239 [ + + ]: 422 : }
240 : : // constraint: the skolems of the given type are equal to one of the variables
241 : : // introduced for uninterpreted sorts
242 : 299 : std::map<TypeNode, std::unordered_set<Node> >::iterator itk;
243 [ + + ]: 721 : for (const Node& k : skolems.d_subs)
244 : : {
245 : 422 : TypeNode tn = k.getType();
246 [ + + ]: 422 : if (!tn.isUninterpretedSort())
247 : : {
248 : : // not an uninterpreted sort, continue
249 : 341 : continue;
250 : : }
251 : 81 : itk = freshVarType.find(tn);
252 [ + - ][ - + ]: 81 : if (itk == freshVarType.end() || itk->second.empty())
[ - + ]
253 : : {
254 [ - - ]: 0 : Trace("mbqi") << "warning: failed to get vars for type " << tn
255 : 0 : << std::endl;
256 : : // this should never happen but we explicitly guard for it, since
257 : : // otherwise we would be model unsound below
258 : 0 : DebugUnhandled();
259 : : continue;
260 : : }
261 : 81 : std::vector<Node> disj;
262 [ + + ]: 411 : for (const Node& fv : itk->second)
263 : : {
264 : 330 : disj.push_back(k.eqNode(fv));
265 : : }
266 : 81 : Node instCardCons = nm->mkOr(disj);
267 : 81 : constraints.push_back(instCardCons);
268 [ + + ]: 422 : }
269 : :
270 : : // constraint: distinctness of variables introduced for uninterpreted
271 : : // constants
272 : 299 : std::vector<Node> allVars;
273 : 299 : for (const std::pair<const TypeNode, std::unordered_set<Node> >& fv :
274 [ + + ]: 686 : freshVarType)
275 : : {
276 [ - + ][ - + ]: 88 : Assert(!fv.second.empty());
[ - - ]
277 : 88 : allVars.insert(allVars.end(), fv.second.begin(), fv.second.end());
278 [ + + ]: 88 : if (fv.second.size() > 1)
279 : : {
280 : 53 : std::vector<Node> fvars(fv.second.begin(), fv.second.end());
281 : 53 : constraints.push_back(nm->mkNode(Kind::DISTINCT, fvars));
282 : 53 : }
283 : : }
284 : :
285 : : // make the query
286 : 299 : Node query = nm->mkAnd(constraints);
287 : 299 : query = extendedRewrite(query);
288 : :
289 : 299 : std::unique_ptr<SolverEngine> mbqiChecker;
290 : 299 : SubsolverSetupInfo ssi(d_env, d_subOptions);
291 : 299 : initializeSubsolver(d_env.getNodeManager(), mbqiChecker, ssi);
292 : 299 : mbqiChecker->setOption("produce-models", "true");
293 : : // set the time limit if applicable
294 [ + - ]: 299 : if (options().quantifiers.mbqiCheckTimeout != 0)
295 : : {
296 : 299 : mbqiChecker->setTimeLimit(options().quantifiers.mbqiCheckTimeout);
297 : : }
298 : 299 : mbqiChecker->assertFormula(query);
299 [ + - ]: 299 : Trace("mbqi") << "*** Check sat..." << std::endl;
300 : 598 : Trace("mbqi") << " query is : " << SkolemManager::getOriginalForm(query)
301 : 299 : << std::endl;
302 : 299 : Result r = mbqiChecker->checkSat();
303 [ + - ]: 299 : Trace("mbqi") << " ...got : " << r << std::endl;
304 [ + + ]: 299 : if (r.getStatus() == Result::UNSAT)
305 : : {
306 [ + - ]: 14 : Trace("mbqi-model-exp") << "...SUCCESS" << std::endl;
307 : 14 : d_quantChecked.insert(q);
308 [ + - ]: 14 : Trace("mbqi") << "...success, SAT" << std::endl;
309 : 14 : return;
310 : : }
311 [ + - ]: 285 : Trace("mbqi-model-exp") << "...FAIL, will instantiate" << std::endl;
312 : :
313 : : // get the model values for all fresh variables
314 [ + + ]: 489 : for (const Node& v : allVars)
315 : : {
316 : 204 : Node mv = mbqiChecker->getValue(v);
317 : 204 : mvToFreshVar[mv] = v;
318 [ + - ]: 204 : Trace("mbqi-debug") << "mvToFreshVar " << mv << " is " << v << std::endl;
319 : 204 : }
320 : :
321 : : // get the model values for skolems
322 : 285 : std::vector<Node> vars = skolems.d_subs;
323 : 285 : std::vector<Node> mvs;
324 : 285 : getModelFromSubsolver(*mbqiChecker.get(), vars, mvs);
325 [ - + ]: 285 : if (TraceIsOn("mbqi"))
326 : : {
327 [ - - ]: 0 : Trace("mbqi") << "...model from subsolver is: " << std::endl;
328 [ - - ]: 0 : for (size_t i = 0, nterms = skolems.size(); i < nterms; i++)
329 : : {
330 [ - - ]: 0 : Trace("mbqi") << " " << skolems.d_subs[i] << " -> " << mvs[i]
331 : 0 : << std::endl;
332 : : }
333 : : }
334 [ + + ]: 285 : if (options().quantifiers.mbqiEnum)
335 : : {
336 : 204 : std::vector<Node> smvs(mvs);
337 [ + + ]: 204 : if (d_msenum->constructInstantiation(q, query, vars, smvs, mvToFreshVar))
338 : : {
339 [ + - ]: 197 : Trace("mbqi-enum") << "Successfully added instantiation." << std::endl;
340 : 197 : return;
341 : : }
342 [ + - ]: 14 : Trace("mbqi-enum")
343 : 7 : << "Failed to add instantiation, revert to normal MBQI..." << std::endl;
344 [ + + ]: 204 : }
345 : 88 : tryInstantiation(q, mvs, InferenceId::QUANTIFIERS_INST_MBQI, mvToFreshVar);
346 [ + + ][ + + ]: 3772 : }
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
347 : :
348 : 292 : bool InstStrategyMbqi::tryInstantiation(
349 : : const Node& q,
350 : : const std::vector<Node>& mvs,
351 : : InferenceId id,
352 : : const std::map<Node, Node>& mvToFreshVar)
353 : : {
354 : 292 : const RepSet* rs = d_treg.getModel()->getRepSet();
355 : 292 : std::vector<Node> terms;
356 : : // try to convert those terms to an instantiation
357 : 292 : std::unordered_map<Node, Node> tmpConvertMap;
358 [ + + ]: 693 : for (const Node& v : mvs)
359 : : {
360 : 401 : Node vc = convertFromModel(v, tmpConvertMap, mvToFreshVar);
361 [ - + ]: 401 : if (vc.isNull())
362 : : {
363 [ - - ]: 0 : Trace("mbqi") << "...failed to convert " << v << " from model" << std::endl;
364 : 0 : return false;
365 : : }
366 [ + + ]: 401 : if (expr::hasSubtermKinds(d_nonClosedKinds, vc))
367 : : {
368 [ + - ]: 8 : Trace("mbqi") << "warning: failed to process model value " << vc
369 : 0 : << ", from " << v
370 : 4 : << ", use arbitrary term for instantiation" << std::endl;
371 : 4 : vc = NodeManager::mkGroundTerm(v.getType());
372 : : }
373 : 401 : terms.push_back(vc);
374 [ + - ]: 401 : }
375 : :
376 : : // get a term that has the same model value as the value each fresh variable
377 : : // represents
378 : 292 : NodeManager* nm = nodeManager();
379 : 292 : SkolemManager* sm = nm->getSkolemManager();
380 : 292 : Subs fvToInst;
381 [ + + ]: 503 : for (const std::pair<const Node, Node>& mvf : mvToFreshVar)
382 : : {
383 : 211 : Node v = mvf.second;
384 : : // get a term that witnesses this variable
385 : 211 : Node ov = sm->getOriginalForm(v);
386 : 211 : Node mvt = rs->getTermForRepresentative(ov);
387 : : // ensure that this term does not contain cex variables, in case CEQGI
388 : : // is combined with MBQI
389 : 211 : if (mvt.isNull() || !TermUtil::getInstConstAttr(mvt).isNull())
390 : : {
391 [ + - ]: 36 : Trace("mbqi") << "warning: failed to get term from value " << ov
392 : 18 : << ", use arbitrary term in query" << std::endl;
393 : 18 : mvt = NodeManager::mkGroundTerm(ov.getType());
394 : : }
395 [ - + ][ - + ]: 211 : Assert(v.getType() == mvt.getType());
[ - - ]
396 : 211 : fvToInst.add(v, mvt);
397 : 211 : }
398 : :
399 : : // now convert fresh variables into terms
400 [ + + ]: 693 : for (Node& v : terms)
401 : : {
402 : 401 : v = fvToInst.apply(v);
403 : : }
404 : :
405 : : // try to add instantiation
406 : 292 : Instantiate* qinst = d_qim.getInstantiate();
407 [ + + ]: 292 : if (!qinst->addInstantiation(q, terms, id))
408 : : {
409 : : // AlwaysAssert(false);
410 [ + - ]: 16 : Trace("mbqi") << "...failed to add instantiation" << std::endl;
411 : 16 : return false;
412 : : }
413 [ + - ]: 276 : Trace("mbqi") << "...success, instantiated" << std::endl;
414 : 276 : return true;
415 : 292 : }
416 : :
417 : 5492 : Node InstStrategyMbqi::convertToQuery(
418 : : Node t,
419 : : std::unordered_map<Node, Node>& cmap,
420 : : std::map<TypeNode, std::unordered_set<Node> >& freshVarType)
421 : : {
422 : 5492 : NodeManager* nm = nodeManager();
423 : 5492 : SkolemManager* sm = nm->getSkolemManager();
424 : 5492 : FirstOrderModel* fm = d_treg.getModel();
425 : 5492 : std::unordered_map<Node, Node>::iterator it;
426 : 5492 : std::map<Node, Node> modelValue;
427 : 5492 : std::unordered_set<Node> processingChildren;
428 : 5492 : std::vector<TNode> visit;
429 : 5492 : visit.push_back(t);
430 : 5492 : TNode cur;
431 : : do
432 : : {
433 : 67947 : cur = visit.back();
434 : 67947 : visit.pop_back();
435 : 67947 : it = cmap.find(cur);
436 [ + - ]: 135894 : Trace("mbqi-debug") << "convertToQuery: " << cur << " " << cur.getKind()
437 [ - + ][ - - ]: 67947 : << " " << cur.getType() << std::endl;
438 [ + + ]: 67947 : if (it != cmap.end())
439 : : {
440 : : // already computed
441 : 51885 : continue;
442 : : }
443 [ + + ]: 58574 : if (processingChildren.find(cur) == processingChildren.end())
444 : : {
445 : 42516 : Kind ck = cur.getKind();
446 [ + + ]: 42516 : if (ck == Kind::BOUND_VARIABLE)
447 : : {
448 : 1136 : cmap[cur] = cur;
449 : : }
450 [ + + ]: 41368 : else if (ck == Kind::CONST_SEQUENCE || ck == Kind::FUNCTION_ARRAY_CONST
451 [ + + ][ + + ]: 82748 : || cur.isVar())
[ + + ]
452 : : {
453 : : // constant sequences and variables require two passes
454 [ + + ]: 15159 : if (!cur.getType().isFirstClass())
455 : : {
456 : : // can be e.g. tester/constructor/selector
457 : 131 : cmap[cur] = cur;
458 : : }
459 : : else
460 : : {
461 : 15028 : std::map<Node, Node>::iterator itm = modelValue.find(cur);
462 [ + + ]: 15028 : if (itm == modelValue.end())
463 : : {
464 : 7518 : Node mval;
465 [ + + ]: 7518 : if (ck == Kind::CONST_SEQUENCE)
466 : : {
467 : 8 : mval = strings::utils::mkConcatForConstSequence(cur);
468 : : }
469 [ + + ]: 7510 : else if (ck == Kind::FUNCTION_ARRAY_CONST)
470 : : {
471 : 14 : mval = uf::FunctionConst::toLambda(cur);
472 : : }
473 : : else
474 : : {
475 : 7496 : mval = fm->getValue(cur);
476 : : }
477 [ + - ]: 7518 : Trace("mbqi-model") << " M[" << cur << "] = " << mval << "\n";
478 : 7518 : modelValue[cur] = mval;
479 [ + + ]: 7518 : if (expr::hasSubterm(mval, cur))
480 : : {
481 : : // failed to evaluate in model, keep itself
482 : 4 : cmap[cur] = cur;
483 : : }
484 : : else
485 : : {
486 : 7514 : visit.push_back(cur);
487 : 7514 : visit.push_back(mval);
488 : : }
489 : 7518 : }
490 : : else
491 : : {
492 : 7510 : Assert(cmap.find(itm->second) != cmap.end())
493 : 0 : << "Missing " << itm->second;
494 : 7510 : cmap[cur] = cmap[itm->second];
495 : : }
496 : : }
497 : : }
498 [ + + ]: 26221 : else if (d_nonClosedKinds.find(ck) != d_nonClosedKinds.end())
499 : : {
500 : : // if its a constant, we can continue, we will assume it is distinct
501 : : // from all others of its type
502 [ + + ]: 369 : if (cur.isConst())
503 : : {
504 : : // return the fresh variable for this term
505 : 365 : Node k = sm->mkPurifySkolem(cur);
506 : 365 : freshVarType[cur.getType()].insert(k);
507 : 365 : cmap[cur] = k;
508 : 365 : continue;
509 : 365 : }
510 : : // if this is a bad kind, fail immediately
511 : 8 : return Node::null();
512 : : }
513 [ + + ]: 25852 : else if (cur.getNumChildren() == 0)
514 : : {
515 : 9766 : cmap[cur] = cur;
516 : : }
517 : : else
518 : : {
519 : 16086 : processingChildren.insert(cur);
520 : 16086 : visit.push_back(cur);
521 [ + + ]: 16086 : if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
522 : : {
523 : 1949 : visit.push_back(cur.getOperator());
524 : : }
525 : 16086 : visit.insert(visit.end(), cur.begin(), cur.end());
526 : : }
527 : 42147 : continue;
528 : 42147 : }
529 : 16058 : processingChildren.erase(cur);
530 : 16058 : bool childChanged = false;
531 : 16058 : std::vector<Node> children;
532 [ + + ]: 16058 : if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
533 : : {
534 : 1949 : children.push_back(cur.getOperator());
535 : : }
536 : 16058 : children.insert(children.end(), cur.begin(), cur.end());
537 [ + + ]: 47387 : for (Node& cn : children)
538 : : {
539 : 31329 : it = cmap.find(cn);
540 [ - + ][ - + ]: 31329 : Assert(it != cmap.end());
[ - - ]
541 [ - + ][ - + ]: 31329 : Assert(!it->second.isNull());
[ - - ]
542 [ + + ][ + + ]: 31329 : childChanged = childChanged || cn != it->second;
543 : 31329 : cn = it->second;
544 : : }
545 : 16058 : Node ret = cur;
546 [ + + ]: 16058 : if (childChanged)
547 : : {
548 : 12714 : ret = rewrite(nm->mkNode(cur.getKind(), children));
549 : : }
550 : 16058 : cmap[cur] = ret;
551 [ + + ]: 84001 : } while (!visit.empty());
552 : :
553 [ - + ][ - + ]: 5488 : Assert(cmap.find(cur) != cmap.end());
[ - - ]
554 : 5488 : return cmap[cur];
555 : 5492 : }
556 : :
557 : 485 : Node InstStrategyMbqi::convertFromModel(
558 : : Node t,
559 : : std::unordered_map<Node, Node>& cmap,
560 : : const std::map<Node, Node>& mvToFreshVar)
561 : : {
562 : 485 : NodeManager* nm = nodeManager();
563 : 485 : std::unordered_map<Node, Node>::iterator it;
564 : 485 : std::map<Node, Node> modelValue;
565 : 485 : std::unordered_set<Node> processingChildren;
566 : 485 : std::vector<TNode> visit;
567 : 485 : visit.push_back(t);
568 : 485 : TNode cur;
569 : : do
570 : : {
571 : 2045 : cur = visit.back();
572 : 2045 : visit.pop_back();
573 : 2045 : it = cmap.find(cur);
574 [ + - ]: 4090 : Trace("mbqi-debug") << "convertFromModel: " << cur << " " << cur.getKind()
575 [ - + ][ - - ]: 2045 : << " " << cur.getType() << std::endl;
576 [ + + ]: 2045 : if (it != cmap.end())
577 : : {
578 : : // already computed
579 : 1511 : continue;
580 : : }
581 [ + + ]: 1796 : if (processingChildren.find(cur) == processingChildren.end())
582 : : {
583 : 1262 : Kind ck = cur.getKind();
584 [ + + ]: 1262 : if (ck == Kind::UNINTERPRETED_SORT_VALUE)
585 : : {
586 : : // converting from query, find the variable that it is equal to
587 : 158 : std::map<Node, Node>::const_iterator itmv = mvToFreshVar.find(cur);
588 [ + + ]: 158 : if (itmv != mvToFreshVar.end())
589 : : {
590 : 130 : cmap[cur] = itmv->second;
591 : : }
592 : : else
593 : : {
594 : : // Just use the purification skolem if it does not exist. This
595 : : // can happen if our query involved parameteric types (e.g. functions,
596 : : // arrays) over uninterpreted sorts, where their models cannot be
597 : : // statically enforced to be in the finite domain.
598 : 28 : SkolemManager* sm = nm->getSkolemManager();
599 : 28 : cmap[cur] = sm->mkPurifySkolem(cur);
600 : : }
601 : 158 : continue;
602 : 158 : }
603 : : // must convert to concat of sequence units
604 : : // must convert function array constant to lambda
605 : 1104 : Node cconv;
606 [ - + ]: 1104 : if (ck == Kind::CONST_SEQUENCE)
607 : : {
608 : 0 : cconv = strings::utils::mkConcatForConstSequence(cur);
609 : : }
610 [ - + ]: 1104 : else if (ck == Kind::FUNCTION_ARRAY_CONST)
611 : : {
612 : 0 : cconv = uf::FunctionConst::toLambda(cur);
613 : : }
614 : : // TODO (wishue #143): could convert RAN to witness term here
615 [ - + ]: 1104 : if (!cconv.isNull())
616 : : {
617 : 0 : Node cconvRet = convertFromModel(cconv, cmap, mvToFreshVar);
618 [ - - ]: 0 : if (cconvRet.isNull())
619 : : {
620 : 0 : return cconvRet;
621 : : }
622 : 0 : cmap[cur] = cconvRet;
623 : 0 : continue;
624 [ - - ]: 0 : }
625 [ + + ]: 1104 : else if (cur.getNumChildren() == 0)
626 : : {
627 : 570 : cmap[cur] = cur;
628 : 570 : continue;
629 : : }
630 : 534 : processingChildren.insert(cur);
631 : 534 : visit.push_back(cur);
632 [ + + ]: 534 : if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
633 : : {
634 : 44 : visit.push_back(cur.getOperator());
635 : : }
636 : 534 : visit.insert(visit.end(), cur.begin(), cur.end());
637 : 534 : continue;
638 [ + - ]: 1104 : }
639 : 534 : processingChildren.erase(cur);
640 : 534 : bool childChanged = false;
641 : 534 : std::vector<Node> children;
642 [ + + ]: 534 : if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
643 : : {
644 : 44 : children.push_back(cur.getOperator());
645 : : }
646 : 534 : children.insert(children.end(), cur.begin(), cur.end());
647 [ + + ]: 1560 : for (Node& cn : children)
648 : : {
649 : 1026 : it = cmap.find(cn);
650 [ - + ][ - + ]: 1026 : Assert(it != cmap.end());
[ - - ]
651 [ - + ][ - + ]: 1026 : Assert(!it->second.isNull());
[ - - ]
652 [ + + ][ + + ]: 1026 : childChanged = childChanged || cn != it->second;
653 : 1026 : cn = it->second;
654 : : }
655 : 534 : Node ret = cur;
656 [ + + ]: 534 : if (childChanged)
657 : : {
658 : 84 : ret = rewrite(nm->mkNode(cur.getKind(), children));
659 : : }
660 : 534 : cmap[cur] = ret;
661 [ + + ]: 2579 : } while (!visit.empty());
662 : :
663 [ - + ][ - + ]: 485 : Assert(cmap.find(cur) != cmap.end());
[ - - ]
664 : 485 : return cmap[cur];
665 : 485 : }
666 : :
667 : 471 : Node InstStrategyMbqi::mkMbqiSkolem(const Node& t)
668 : : {
669 : 471 : SkolemManager* skm = nodeManager()->getSkolemManager();
670 : 471 : return skm->mkInternalSkolemFunction(
671 : 1413 : InternalSkolemId::MBQI_INPUT, t.getType(), {t});
672 : : }
673 : :
674 : 0 : Result InstStrategyMbqi::checkWithSubsolverSimple(
675 : : Node query, const SubsolverSetupInfo& info)
676 : : {
677 : 0 : query = extendedRewrite(query);
678 : 0 : if (!options().quantifiers.mbqiNestedCheck
679 : 0 : && expr::hasSubtermKind(Kind::FORALL, query))
680 : : {
681 [ - - ]: 0 : Trace("mbqi") << "*** SKIP " << query << std::endl;
682 : 0 : return Result();
683 : : }
684 : : return checkWithSubsolver(query,
685 : : info,
686 : 0 : options().quantifiers.mbqiCheckTimeout != 0,
687 : 0 : options().quantifiers.mbqiCheckTimeout);
688 : : }
689 : :
690 : : } // namespace quantifiers
691 : : } // namespace theory
692 : : } // namespace cvc5::internal
|
