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 : : * Implementation of instantiate.
11 : : */
12 : :
13 : : #include "theory/quantifiers/instantiate.h"
14 : :
15 : : #include "expr/node_algorithm.h"
16 : : #include "options/base_options.h"
17 : : #include "options/quantifiers_options.h"
18 : : #include "options/smt_options.h"
19 : : #include "proof/lazy_proof.h"
20 : : #include "proof/proof_node_manager.h"
21 : : #include "smt/logic_exception.h"
22 : : #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
23 : : #include "theory/quantifiers/entailment_check.h"
24 : : #include "theory/quantifiers/first_order_model.h"
25 : : #include "theory/quantifiers/quantifiers_attributes.h"
26 : : #include "theory/quantifiers/quantifiers_preprocess.h"
27 : : #include "theory/quantifiers/term_database.h"
28 : : #include "theory/quantifiers/term_enumeration.h"
29 : : #include "theory/quantifiers/term_registry.h"
30 : : #include "theory/quantifiers/term_util.h"
31 : : #include "theory/rewriter.h"
32 : :
33 : : using namespace cvc5::internal::kind;
34 : : using namespace cvc5::context;
35 : :
36 : : namespace cvc5::internal {
37 : : namespace theory {
38 : : namespace quantifiers {
39 : :
40 : 50938 : Instantiate::Instantiate(Env& env,
41 : : QuantifiersState& qs,
42 : : QuantifiersInferenceManager& qim,
43 : : QuantifiersRegistry& qr,
44 : 50938 : TermRegistry& tr)
45 : : : QuantifiersUtil(env),
46 : 50938 : d_statistics(statisticsRegistry()),
47 : 50938 : d_qstate(qs),
48 : 50938 : d_qim(qim),
49 : 50938 : d_qreg(qr),
50 : 50938 : d_treg(tr),
51 : 50938 : d_insts(userContext()),
52 : 50938 : d_uimt(userContext()),
53 : 50938 : d_cimt(context()),
54 : 72302 : d_pfInst(isProofEnabled()
55 : 21364 : ? new CDProof(env, userContext(), "Instantiate::pfInst")
56 : 152814 : : nullptr)
57 : : {
58 : : // We need to use user context-dependent trie for the main instantiation
59 : : // trie if incremental.
60 : 50938 : d_useCdInstTrie = options().base.incrementalSolving;
61 : 50938 : }
62 : :
63 : 101186 : Instantiate::~Instantiate() {}
64 : :
65 : 68843 : bool Instantiate::reset(Theory::Effort e)
66 : : {
67 [ + - ]: 68843 : Trace("inst-debug") << "Reset, effort " << e << std::endl;
68 : : // clear explicitly recorded instantiations
69 : 68843 : d_recordedInst.clear();
70 : 68843 : d_instDebugTemp.clear();
71 : 68843 : return true;
72 : : }
73 : :
74 : 54043 : void Instantiate::registerQuantifier(CVC5_UNUSED Node q) {}
75 : 7947 : bool Instantiate::checkComplete(IncompleteId& incId)
76 : : {
77 [ + + ]: 7947 : if (!d_recordedInst.empty())
78 : : {
79 [ + - ]: 2 : Trace("quant-engine-debug")
80 : 1 : << "Set incomplete due to recorded instantiations." << std::endl;
81 : 1 : incId = IncompleteId::QUANTIFIERS_RECORDED_INST;
82 : 1 : return false;
83 : : }
84 : 7946 : return true;
85 : : }
86 : :
87 : 43865 : void Instantiate::addRewriter(InstantiationRewriter* ir)
88 : : {
89 : 43865 : d_instRewrite.push_back(ir);
90 : 43865 : }
91 : :
92 : 186775 : bool Instantiate::addInstantiation(
93 : : Node q, std::vector<Node>& terms, InferenceId id, Node pfArg, bool doVts)
94 : : {
95 : : // do the instantiation
96 : 186791 : bool ret = addInstantiationInternal(q, terms, id, pfArg, doVts);
97 : : // process the instantiation with callbacks via term registry
98 : 186767 : d_treg.processInstantiation(q, terms);
99 : : // return whether the instantiation was successful
100 : 186767 : return ret;
101 : : }
102 : :
103 : 186775 : bool Instantiate::addInstantiationInternal(
104 : : Node q, std::vector<Node>& terms, InferenceId id, Node pfArg, bool doVts)
105 : : {
106 : : // For resource-limiting (also does a time check).
107 : 186775 : d_qim.safePoint(Resource::QuantifierStep);
108 [ - + ][ - + ]: 186767 : Assert(!d_qstate.isInConflict());
[ - - ]
109 [ - + ][ - + ]: 186767 : Assert(q.getKind() == Kind::FORALL);
[ - - ]
110 [ - + ][ - + ]: 186767 : Assert(terms.size() == q[0].getNumChildren());
[ - - ]
111 [ - + ]: 186767 : if (TraceIsOn("inst-add-debug"))
112 : : {
113 [ - - ]: 0 : Trace("inst-add-debug") << "For quantified formula " << q
114 : 0 : << ", add instantiation: " << std::endl;
115 [ - - ]: 0 : for (size_t i = 0, size = terms.size(); i < size; i++)
116 : : {
117 : 0 : Trace("inst-add-debug") << " " << q[0][i];
118 [ - - ]: 0 : Trace("inst-add-debug") << " -> " << terms[i];
119 [ - - ]: 0 : Trace("inst-add-debug") << std::endl;
120 : : }
121 [ - - ]: 0 : Trace("inst-add-debug") << "id is " << id << std::endl;
122 [ - - ]: 0 : Trace("inst-add-debug") << "doVts is " << doVts << std::endl;
123 : : }
124 : : // ensure the terms are non-null and well-typed
125 [ + + ]: 634745 : for (size_t i = 0, size = terms.size(); i < size; i++)
126 : : {
127 [ + + ]: 447978 : if (terms[i].isNull())
128 : : {
129 : 33 : terms[i] = d_treg.getTermForType(q[0][i].getType());
130 : : }
131 : : }
132 : : #ifdef CVC5_ASSERTIONS
133 [ + + ]: 634745 : for (size_t i = 0, size = terms.size(); i < size; i++)
134 : : {
135 : 895956 : TypeNode tn = q[0][i].getType();
136 [ - + ][ - + ]: 447978 : Assert(!terms[i].isNull());
[ - - ]
137 [ - + ][ - + ]: 447978 : Assert(terms[i].getType() == tn);
[ - - ]
138 : 447978 : bool bad_inst = false;
139 [ - + ]: 447978 : if (TermUtil::containsUninterpretedConstant(terms[i]))
140 : : {
141 [ - - ]: 0 : Trace("inst") << "***& inst contains uninterpreted constant : "
142 : 0 : << terms[i] << std::endl;
143 : 0 : bad_inst = true;
144 : : }
145 [ - + ]: 1791912 : else if (!CVC5_EQUAL(terms[i].getType(), q[0][i].getType()))
146 : : {
147 [ - - ]: 0 : Trace("inst") << "***& inst bad type : " << terms[i] << " "
148 : 0 : << terms[i].getType() << "/" << q[0][i].getType()
149 : 0 : << std::endl;
150 : 0 : bad_inst = true;
151 : : }
152 : : else
153 : : {
154 : : // This checks whether the term represents a "counterexample". It is
155 : : // model-unsound to instantiate with such terms.
156 : : // Note we check this even if cegqi is false, since sygusInst also
157 : : // introduces terms with this attribute.
158 : 447978 : Node icf = TermUtil::getInstConstAttr(terms[i]);
159 [ + + ]: 447978 : if (!icf.isNull())
160 : : {
161 [ - + ]: 242 : if (icf == q)
162 : : {
163 [ - - ]: 0 : Trace("inst") << "***& inst contains inst constant attr : "
164 : 0 : << terms[i] << std::endl;
165 : 0 : bad_inst = true;
166 : : }
167 [ - + ]: 242 : else if (expr::hasSubterm(terms[i], d_qreg.d_inst_constants[q]))
168 : : {
169 [ - - ]: 0 : Trace("inst") << "***& inst contains inst constants : " << terms[i]
170 : 0 : << std::endl;
171 : 0 : bad_inst = true;
172 : : }
173 : : }
174 : 447978 : }
175 : : // this assertion is critical to soundness
176 [ - + ]: 447978 : if (bad_inst)
177 : : {
178 [ - - ]: 0 : Trace("inst") << "***& Bad Instantiate [" << id << "] " << q << " with "
179 : 0 : << std::endl;
180 [ - - ]: 0 : for (unsigned j = 0; j < terms.size(); j++)
181 : : {
182 [ - - ]: 0 : Trace("inst") << " " << terms[j] << std::endl;
183 : : }
184 : 0 : DebugUnhandled();
185 : : }
186 : 447978 : }
187 : : #endif
188 : 186767 : bool isLocal = false;
189 [ - + ]: 186767 : if (options().quantifiers.instLocal)
190 : : {
191 : : // determine if it is an instantiation type that is treated as local
192 : 0 : isLocal = isLocalInstId(id);
193 : : }
194 : :
195 : : // Note we check for entailment before checking for term vector duplication.
196 : : // Although checking for term vector duplication is a faster check, it is
197 : : // included automatically with recordInstantiationInternal, hence we prefer
198 : : // two checks instead of three. In experiments, it is 1% slower or so to call
199 : : // existsInstantiation here.
200 : : // Alternatively, we could return an (index, trie node) in the call to
201 : : // existsInstantiation here, where this would return the node in the trie
202 : : // where we determined that there is definitely no duplication, and then
203 : : // continue from that point in recordInstantiation below. However, for
204 : : // simplicity, we do not pursue this option (as it would likely only
205 : : // lead to very small gains).
206 : :
207 : : // check for positive entailment
208 [ + + ]: 186767 : if (options().quantifiers.instNoEntail)
209 : : {
210 : 180027 : EntailmentCheck* ec = d_treg.getEntailmentCheck();
211 : : // should check consistency of equality engine
212 : : // (if not aborting on utility's reset)
213 : 180027 : std::map<TNode, TNode> subs;
214 [ + + ]: 574178 : for (unsigned i = 0, size = terms.size(); i < size; i++)
215 : : {
216 : 394151 : subs[q[0][i]] = terms[i];
217 : : }
218 [ + + ]: 180027 : if (ec->isEntailed(q[1], subs, false, true))
219 : : {
220 [ + - ]: 24612 : Trace("inst-add-debug") << " --> Currently entailed." << std::endl;
221 : 24612 : ++(d_statistics.d_inst_duplicate_ent);
222 : 24612 : return false;
223 : : }
224 [ + + ]: 180027 : }
225 : :
226 : : // check based on instantiation level
227 [ + + ]: 162155 : if (options().quantifiers.instMaxLevel != -1)
228 : : {
229 : 452 : TermDb* tdb = d_treg.getTermDatabase();
230 [ + + ]: 1566 : for (const Node& t : terms)
231 : : {
232 [ - + ]: 1114 : if (!tdb->isTermEligibleForInstantiation(t, q))
233 : : {
234 : 0 : return false;
235 : : }
236 : : }
237 : : }
238 : :
239 : : // record the instantiation
240 : 162155 : bool recorded = recordInstantiationInternal(q, terms, isLocal);
241 [ + + ]: 162155 : if (!recorded)
242 : : {
243 [ + - ]: 59861 : Trace("inst-add-debug") << " --> Already exists (no record)." << std::endl;
244 : 59861 : ++(d_statistics.d_inst_duplicate_eq);
245 : 59861 : return false;
246 : : }
247 : :
248 : : // Set up a proof if proofs are enabled. This proof stores a proof of
249 : : // the instantiation body with q as a free assumption.
250 : 102294 : std::shared_ptr<LazyCDProof> pfTmp;
251 [ + + ]: 102294 : if (isProofEnabled())
252 : : {
253 : 119408 : pfTmp.reset(new LazyCDProof(
254 : 59704 : d_env, nullptr, nullptr, "Instantiate::LazyCDProof::tmp"));
255 : : }
256 : :
257 : : // construct the instantiation
258 [ + - ]: 102294 : Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
259 [ - + ][ - + ]: 102294 : Assert(d_qreg.d_vars[q].size() == terms.size());
[ - - ]
260 : : // get the instantiation
261 : : Node body = getInstantiation(
262 : 204588 : q, d_qreg.d_vars[q], terms, id, pfArg, doVts, pfTmp.get());
263 : 102294 : Node orig_body = body;
264 : : // now preprocess, storing the trust node for the rewrite
265 : 102294 : TrustNode tpBody = d_qreg.getPreprocess().preprocess(body, true);
266 [ + + ]: 102294 : if (!tpBody.isNull())
267 : : {
268 [ - + ][ - + ]: 7 : Assert(tpBody.getKind() == TrustNodeKind::REWRITE);
[ - - ]
269 : 7 : body = tpBody.getNode();
270 : : // do a tranformation step
271 [ + + ]: 7 : if (pfTmp != nullptr)
272 : : {
273 : : // ----------------- from preprocess
274 : : // orig_body orig_body = body
275 : : // ------------------------------ EQ_RESOLVE
276 : : // body
277 : 4 : Node proven = tpBody.getProven();
278 : : // add the transformation proof, or the trusted rule if none provided
279 : 4 : pfTmp->addLazyStep(proven,
280 : : tpBody.getGenerator(),
281 : : TrustId::QUANTIFIERS_PREPROCESS,
282 : : true,
283 : : "Instantiate::getInstantiation:qpreprocess");
284 [ + + ][ - - ]: 12 : pfTmp->addStep(body, ProofRule::EQ_RESOLVE, {orig_body, proven}, {});
285 : 4 : }
286 : : }
287 [ + - ]: 102294 : Trace("inst-debug") << "...preprocess to " << body << std::endl;
288 : :
289 : : // construct the lemma
290 [ + - ]: 102294 : Trace("inst-assert") << "(assert " << body << ")" << std::endl;
291 : :
292 : : // construct the instantiation, and rewrite the lemma
293 : 204588 : Node lem = NodeManager::mkNode(Kind::IMPLIES, q, body);
294 : :
295 : : // If proofs are enabled, construct the proof, which is of the form:
296 : : // ... free assumption q ...
297 : : // ------------------------- from pfTmp
298 : : // body
299 : : // ------------------------- SCOPE
300 : : // (=> q body)
301 : : // -------------------------- MACRO_SR_PRED_ELIM
302 : : // lem
303 : 102294 : bool hasProof = false;
304 [ + + ]: 102294 : if (isProofEnabled())
305 : : {
306 : : // make the proof of body
307 : 59704 : std::shared_ptr<ProofNode> pfn = pfTmp->getProofFor(body);
308 : : // make the scope proof to get (=> q body)
309 : 59704 : std::vector<Node> assumps;
310 : 59704 : assumps.push_back(q);
311 : : std::shared_ptr<ProofNode> pfns =
312 : 119408 : d_env.getProofNodeManager()->mkScope({pfn}, assumps);
313 [ + - ][ + - ]: 59704 : Assert(assumps.size() == 1 && assumps[0] == q);
[ - + ][ - + ]
[ - - ]
314 : : // store in the main proof
315 : 59704 : d_pfInst->addProof(pfns);
316 : 59704 : Node prevLem = lem;
317 : 59704 : lem = rewrite(lem);
318 [ + + ]: 59704 : if (prevLem != lem)
319 : : {
320 : 55692 : d_pfInst->addStep(lem, ProofRule::MACRO_SR_PRED_ELIM, {prevLem}, {});
321 : : }
322 : 59704 : hasProof = true;
323 : 59704 : }
324 : : else
325 : : {
326 : 42590 : lem = rewrite(lem);
327 : : }
328 : :
329 : : // added lemma, which checks for lemma duplication
330 : 102294 : bool addedLem = false;
331 : 102294 : LemmaProperty p = LemmaProperty::INPROCESS;
332 [ - + ]: 102294 : if (isLocal)
333 : : {
334 : 0 : p = LemmaProperty::LOCAL;
335 : : }
336 [ + + ]: 102294 : if (hasProof)
337 : : {
338 : : // use proof generator
339 [ + - ]: 59704 : addedLem = d_qim.addPendingLemma(lem, id, p, d_pfInst.get());
340 : : }
341 : : else
342 : : {
343 : 42590 : addedLem = d_qim.addPendingLemma(lem, id, p);
344 : : }
345 : :
346 [ + + ]: 102294 : if (!addedLem)
347 : : {
348 [ + - ]: 1841 : Trace("inst-add-debug") << " --> Lemma already exists." << std::endl;
349 : 1841 : ++(d_statistics.d_inst_duplicate);
350 : 1841 : return false;
351 : : }
352 : :
353 : : // add to list of instantiations
354 : 100453 : InstLemmaList* ill = getOrMkInstLemmaList(q);
355 : 100453 : ill->d_list.push_back(body);
356 : : // add to temporary debug statistics (# inst on this round)
357 : 100453 : d_instDebugTemp[q]++;
358 [ - + ]: 100453 : if (TraceIsOn("inst"))
359 : : {
360 [ - - ]: 0 : Trace("inst") << "*** Instantiate [" << id << "] " << q << " with "
361 : 0 : << std::endl;
362 [ - - ]: 0 : for (size_t i = 0, size = terms.size(); i < size; i++)
363 : : {
364 [ - - ]: 0 : if (TraceIsOn("inst"))
365 : : {
366 [ - - ]: 0 : Trace("inst") << " " << terms[i];
367 [ - - ]: 0 : if (TraceIsOn("inst-debug"))
368 : : {
369 : 0 : Trace("inst-debug") << ", type=" << terms[i].getType()
370 : 0 : << ", var_type=" << q[0][i].getType();
371 : : }
372 [ - - ]: 0 : Trace("inst") << std::endl;
373 : : }
374 : : }
375 : : }
376 [ + + ]: 100453 : if (options().quantifiers.instMaxLevel != -1)
377 : : {
378 [ - + ][ - + ]: 423 : Assert(lem.getKind() == Kind::IMPLIES);
[ - - ]
379 : 423 : uint64_t maxInstLevel = 0;
380 : : uint64_t clevel;
381 [ + + ]: 1484 : for (const Node& tc : terms)
382 : : {
383 [ - + ]: 1061 : if (!QuantAttributes::getInstantiationLevel(tc, clevel))
384 : : {
385 : : // ensure it is set to zero.
386 : 0 : QuantAttributes::setInstantiationLevelAttr(tc, 0);
387 : 0 : continue;
388 : : }
389 [ - + ]: 1061 : if (clevel > maxInstLevel)
390 : : {
391 : 0 : maxInstLevel = clevel;
392 : : }
393 : : }
394 : 423 : QuantAttributes::setInstantiationLevelAttr(lem[1], maxInstLevel + 1);
395 : : }
396 [ + - ]: 100453 : Trace("inst-add-debug") << " --> Success." << std::endl;
397 : 100453 : ++(d_statistics.d_instantiations);
398 : 100453 : return true;
399 : 102294 : }
400 : :
401 : 0 : bool Instantiate::isLocalInstId(InferenceId id)
402 : : {
403 [ - - ]: 0 : switch (id)
404 : : {
405 : 0 : case InferenceId::QUANTIFIERS_INST_E_MATCHING:
406 : : case InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE:
407 : : case InferenceId::QUANTIFIERS_INST_E_MATCHING_MT:
408 : : case InferenceId::QUANTIFIERS_INST_E_MATCHING_MTL:
409 : : case InferenceId::QUANTIFIERS_INST_E_MATCHING_HO:
410 : : case InferenceId::QUANTIFIERS_INST_E_MATCHING_VAR_GEN:
411 : : case InferenceId::QUANTIFIERS_INST_E_MATCHING_RELATIONAL:
412 : : case InferenceId::QUANTIFIERS_INST_CBQI_CONFLICT:
413 : 0 : case InferenceId::QUANTIFIERS_INST_CBQI_PROP: return true;
414 : 0 : default: break;
415 : : }
416 : 0 : return false;
417 : : }
418 : :
419 : 32952 : void Instantiate::processInstantiationRep(Node q, std::vector<Node>& terms)
420 : : {
421 [ - + ][ - + ]: 32952 : Assert(q.getKind() == Kind::FORALL);
[ - - ]
422 [ - + ][ - + ]: 32952 : Assert(terms.size() == q[0].getNumChildren());
[ - - ]
423 [ + + ]: 111537 : for (size_t i = 0, size = terms.size(); i < size; i++)
424 : : {
425 [ - + ][ - + ]: 78585 : Assert(!terms[i].isNull());
[ - - ]
426 : : // pick the best possible representative for instantiation, based on past
427 : : // use and simplicity of term
428 : 78585 : terms[i] = d_treg.getModel()->getInternalRepresentative(terms[i], q, i);
429 : : // Note it may be a null representative here, it is then replaced
430 : : // by an arbitrary term if necessary during addInstantiation.
431 : : }
432 : 32952 : }
433 : :
434 : 12494 : bool Instantiate::addInstantiationExpFail(Node q,
435 : : std::vector<Node>& terms,
436 : : std::vector<bool>& failMask,
437 : : InferenceId id,
438 : : Node pfArg,
439 : : bool doVts,
440 : : bool expFull)
441 : : {
442 [ + + ]: 12494 : if (addInstantiation(q, terms, id, pfArg, doVts))
443 : : {
444 : 2670 : return true;
445 : : }
446 : 9824 : size_t tsize = terms.size();
447 : 9824 : failMask.resize(tsize, true);
448 [ + + ]: 9824 : if (tsize == 1)
449 : : {
450 : : // will never succeed with 1 variable
451 : 3685 : return false;
452 : : }
453 : 6139 : EntailmentCheck* echeck = d_treg.getEntailmentCheck();
454 [ + - ]: 6139 : Trace("inst-exp-fail") << "Explain inst failure..." << terms << std::endl;
455 : : // set up information for below
456 : 6139 : std::vector<Node>& vars = d_qreg.d_vars[q];
457 [ - + ][ - + ]: 6139 : Assert(tsize == vars.size());
[ - - ]
458 : 6139 : std::map<TNode, TNode> subs;
459 [ + + ]: 33953 : for (size_t i = 0; i < tsize; i++)
460 : : {
461 : 27814 : subs[vars[i]] = terms[i];
462 : : }
463 : : // get the instantiation body
464 : 6139 : InferenceId idNone = InferenceId::UNKNOWN;
465 : 6139 : Node nulln;
466 : 12278 : Node ibody = getInstantiation(q, vars, terms, idNone, nulln, doVts);
467 : 6139 : ibody = rewrite(ibody);
468 [ + + ]: 33841 : for (size_t i = 0; i < tsize; i++)
469 : : {
470 : : // process consecutively in reverse order, which is important since we use
471 : : // the fail mask for incrementing in a lexicographic order
472 : 27814 : size_t ii = (tsize - 1) - i;
473 : : // replace with the identity substitution
474 : 27814 : Node prev = terms[ii];
475 : 27814 : terms[ii] = vars[ii];
476 : 27814 : subs.erase(vars[ii]);
477 [ + + ]: 27814 : if (subs.empty())
478 : : {
479 : : // will never succeed with empty substitution
480 : 112 : break;
481 : : }
482 [ + - ]: 27702 : Trace("inst-exp-fail") << "- revert " << ii << std::endl;
483 : : // check whether we are still redundant
484 : 27702 : bool success = false;
485 : : // check entailment, only if option is set
486 [ + - ]: 27702 : if (options().quantifiers.instNoEntail)
487 : : {
488 [ + - ]: 27702 : Trace("inst-exp-fail") << " check entailment" << std::endl;
489 : 27702 : success = echeck->isEntailed(q[1], subs, false, true);
490 [ + - ]: 27702 : Trace("inst-exp-fail") << " entailed: " << success << std::endl;
491 : : }
492 : : // check whether the instantiation rewrites to the same thing
493 [ + + ]: 27702 : if (!success)
494 : : {
495 : 46894 : Node ibodyc = getInstantiation(q, vars, terms, idNone, nulln, doVts);
496 : 23447 : ibodyc = rewrite(ibodyc);
497 : 23447 : success = (ibodyc == ibody);
498 [ + - ]: 23447 : Trace("inst-exp-fail") << " rewrite invariant: " << success << std::endl;
499 : 23447 : }
500 [ + + ]: 27702 : if (success)
501 : : {
502 : : // if we still fail, we are not critical
503 : 4605 : failMask[ii] = false;
504 : : }
505 : : else
506 : : {
507 : 23097 : subs[vars[ii]] = prev;
508 : 23097 : terms[ii] = prev;
509 : : // not necessary to proceed if expFull is false
510 [ - + ]: 23097 : if (!expFull)
511 : : {
512 : 0 : break;
513 : : }
514 : : }
515 [ + + ]: 27814 : }
516 [ - + ]: 6139 : if (TraceIsOn("inst-exp-fail"))
517 : : {
518 [ - - ]: 0 : Trace("inst-exp-fail") << "Fail mask: ";
519 [ - - ]: 0 : for (bool b : failMask)
520 : : {
521 : 0 : Trace("inst-exp-fail") << (b ? 1 : 0);
522 : : }
523 [ - - ]: 0 : Trace("inst-exp-fail") << std::endl;
524 : : }
525 : 6139 : return false;
526 : 6139 : }
527 : :
528 : 1 : void Instantiate::recordInstantiation(Node q,
529 : : const std::vector<Node>& terms,
530 : : bool doVts)
531 : : {
532 [ + - ]: 1 : Trace("inst-debug") << "Record instantiation for " << q << std::endl;
533 : : // get the instantiation list, which ensures that q is marked as a quantified
534 : : // formula we instantiated, despite only recording an instantiation here
535 : 1 : getOrMkInstLemmaList(q);
536 : 1 : Node inst = getInstantiation(q, terms, doVts);
537 : 1 : d_recordedInst[q].push_back(inst);
538 : 1 : }
539 : :
540 : 0 : bool Instantiate::existsInstantiation(Node q, const std::vector<Node>& terms)
541 : : {
542 [ - - ]: 0 : if (d_useCdInstTrie)
543 : : {
544 : 0 : NodeInstTrieMap::iterator it = d_uimt.find(q);
545 [ - - ]: 0 : if (it != d_uimt.end())
546 : : {
547 : 0 : return it->second->existsInstMatch(userContext(), q, terms);
548 : : }
549 : : }
550 : : else
551 : : {
552 : 0 : std::map<Node, InstMatchTrie>::iterator it = d_imt.find(q);
553 [ - - ]: 0 : if (it != d_imt.end())
554 : : {
555 : 0 : return it->second.existsInstMatch(q, terms);
556 : : }
557 : : }
558 : 0 : return false;
559 : : }
560 : :
561 : 131881 : Node Instantiate::getInstantiation(Node q,
562 : : const std::vector<Node>& vars,
563 : : const std::vector<Node>& terms,
564 : : InferenceId id,
565 : : Node pfArg,
566 : : bool doVts,
567 : : LazyCDProof* pf)
568 : : {
569 [ - + ][ - + ]: 131881 : Assert(vars.size() == terms.size());
[ - - ]
570 [ - + ][ - + ]: 131881 : Assert(q[0].getNumChildren() == vars.size());
[ - - ]
571 : : // Notice that this could be optimized, but no significant performance
572 : : // improvements were observed with alternative implementations (see #1386).
573 : : Node body =
574 : 131881 : q[1].substitute(vars.begin(), vars.end(), terms.begin(), terms.end());
575 : :
576 : : // store the proof of the instantiated body, with (open) assumption q
577 [ + + ]: 131881 : if (pf != nullptr)
578 : : {
579 : 59704 : std::vector<Node> pfTerms;
580 : : // Include the list of terms as an SEXPR.
581 : 59704 : pfTerms.push_back(nodeManager()->mkNode(Kind::SEXPR, terms));
582 : : // additional arguments: if the inference id is not unknown, include it,
583 : : // followed by the proof argument if non-null. The latter is used e.g.
584 : : // to track which trigger caused an instantiation.
585 [ + - ]: 59704 : if (id != InferenceId::UNKNOWN)
586 : : {
587 : 59704 : pfTerms.push_back(mkInferenceIdNode(nodeManager(), id));
588 [ + + ]: 59704 : if (!pfArg.isNull())
589 : : {
590 : 47585 : pfTerms.push_back(pfArg);
591 : : }
592 : : }
593 : 119408 : pf->addStep(body, ProofRule::INSTANTIATE, {q}, pfTerms);
594 : 59704 : }
595 : :
596 : : // run rewriters to rewrite the instantiation in sequence.
597 [ + + ]: 259895 : for (InstantiationRewriter*& ir : d_instRewrite)
598 : : {
599 : 256028 : TrustNode trn = ir->rewriteInstantiation(q, terms, body, doVts);
600 [ + + ]: 128014 : if (!trn.isNull())
601 : : {
602 : 216 : Node newBody = trn.getNode();
603 : : // if using proofs, we store a preprocess + transformation step.
604 [ + + ]: 216 : if (pf != nullptr)
605 : : {
606 : 118 : Node proven = trn.getProven();
607 : 118 : pf->addLazyStep(proven,
608 : : trn.getGenerator(),
609 : : TrustId::QUANTIFIERS_INST_REWRITE,
610 : : true,
611 : : "Instantiate::getInstantiation:rewrite_inst");
612 [ + + ][ - - ]: 354 : pf->addStep(newBody, ProofRule::EQ_RESOLVE, {body, proven}, {});
613 : 118 : }
614 : 216 : body = newBody;
615 : 216 : }
616 : 128014 : }
617 : 131881 : return body;
618 : 0 : }
619 : :
620 : 1 : Node Instantiate::getInstantiation(Node q,
621 : : const std::vector<Node>& terms,
622 : : bool doVts)
623 : : {
624 [ - + ][ - + ]: 1 : Assert(d_qreg.d_vars.find(q) != d_qreg.d_vars.end());
[ - - ]
625 : : return getInstantiation(
626 : 1 : q, d_qreg.d_vars[q], terms, InferenceId::UNKNOWN, Node::null(), doVts);
627 : : }
628 : :
629 : 162155 : bool Instantiate::recordInstantiationInternal(Node q,
630 : : const std::vector<Node>& terms,
631 : : bool isLocal)
632 : : {
633 [ - + ]: 162155 : if (isLocal)
634 : : {
635 : : // if local, the return value will be based on the SAT-context dependent
636 : : // trie.
637 : : CDInstMatchTrie* trie;
638 : 0 : NodeInstTrieMap::iterator it = d_cimt.find(q);
639 [ - - ]: 0 : if (it != d_cimt.end())
640 : : {
641 : 0 : trie = it->second.get();
642 : : }
643 : : else
644 : : {
645 : : std::shared_ptr<CDInstMatchTrie> strie =
646 : 0 : std::make_shared<CDInstMatchTrie>(context());
647 : 0 : d_cimt.insert(q, strie);
648 : 0 : trie = strie.get();
649 : 0 : }
650 : : // Note that we do not add to the main trie. This means that this
651 : : // instantiation won't be recorded when asked for the global list
652 : : // of instantiations (SolverEngine::getInstantiatedQuantifiedFormulas and
653 : : // related methods). Note that the global list of instantiations is
654 : : // relied on e.g. for quantifier elimination, and for SyGuS single
655 : : // invocation techniques. These applications typically use CEGQI, which
656 : : // should never use local instantiations or else the solutions for
657 : : // QE and sygus will be incorrect.
658 : 0 : return trie->addInstMatch(context(), q, terms);
659 : : }
660 : : bool ret;
661 [ + + ]: 162155 : if (d_useCdInstTrie)
662 : : {
663 : : CDInstMatchTrie* trie;
664 : 7059 : NodeInstTrieMap::iterator it = d_uimt.find(q);
665 [ + + ]: 7059 : if (it != d_uimt.end())
666 : : {
667 : 5311 : trie = it->second.get();
668 : : }
669 : : else
670 : : {
671 [ + - ]: 3496 : Trace("inst-add-debug")
672 : 1748 : << "Adding into context-dependent inst trie" << std::endl;
673 : : std::shared_ptr<CDInstMatchTrie> strie =
674 : 1748 : std::make_shared<CDInstMatchTrie>(userContext());
675 : 1748 : d_uimt.insert(q, strie);
676 : 1748 : trie = strie.get();
677 : 1748 : }
678 : 7059 : ret = trie->addInstMatch(userContext(), q, terms);
679 : : }
680 : : else
681 : : {
682 [ + - ]: 155096 : Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
683 : 155096 : ret = d_imt[q].addInstMatch(q, terms);
684 : : }
685 : 162155 : return ret;
686 : : }
687 : :
688 : 100 : void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs) const
689 : : {
690 : 100 : for (NodeInstListMap::const_iterator it = d_insts.begin();
691 [ + + ]: 201 : it != d_insts.end();
692 : 101 : ++it)
693 : : {
694 : 101 : qs.push_back(it->first);
695 : : }
696 : 100 : }
697 : :
698 : 145 : void Instantiate::getInstantiationTermVectors(
699 : : Node q, std::vector<std::vector<Node> >& tvecs)
700 : : {
701 [ + + ]: 145 : if (d_useCdInstTrie)
702 : : {
703 : 71 : NodeInstTrieMap::const_iterator it = d_uimt.find(q);
704 [ + - ]: 71 : if (it != d_uimt.end())
705 : : {
706 : 71 : it->second->getInstantiations(q, tvecs);
707 : : }
708 : : }
709 : : else
710 : : {
711 : 74 : std::map<Node, InstMatchTrie>::const_iterator it = d_imt.find(q);
712 [ + - ]: 74 : if (it != d_imt.end())
713 : : {
714 : 74 : it->second.getInstantiations(q, tvecs);
715 : : }
716 : : }
717 : 145 : }
718 : :
719 : 75 : void Instantiate::getInstantiationTermVectors(
720 : : std::map<Node, std::vector<std::vector<Node> > >& insts)
721 : : {
722 [ + + ]: 75 : if (d_useCdInstTrie)
723 : : {
724 [ + + ]: 142 : for (const auto& t : d_uimt)
725 : : {
726 : 71 : getInstantiationTermVectors(t.first, insts[t.first]);
727 : : }
728 : : }
729 : : else
730 : : {
731 [ + + ]: 10 : for (const auto& t : d_imt)
732 : : {
733 : 6 : getInstantiationTermVectors(t.first, insts[t.first]);
734 : : }
735 : : }
736 : 75 : }
737 : :
738 : 32 : void Instantiate::getInstantiations(Node q, std::vector<Node>& insts)
739 : : {
740 [ + - ]: 32 : Trace("inst-debug") << "get instantiations for " << q << std::endl;
741 : 32 : InstLemmaList* ill = getOrMkInstLemmaList(q);
742 : 32 : insts.insert(insts.end(), ill->d_list.begin(), ill->d_list.end());
743 : : // also include recorded instantations (for qe-partial)
744 : : std::map<Node, std::vector<Node> >::const_iterator it =
745 : 32 : d_recordedInst.find(q);
746 [ + + ]: 32 : if (it != d_recordedInst.end())
747 : : {
748 : 1 : insts.insert(insts.end(), it->second.begin(), it->second.end());
749 : : }
750 : 32 : }
751 : :
752 : 255526 : bool Instantiate::isProofEnabled() const
753 : : {
754 : 255526 : return d_env.isTheoryProofProducing();
755 : : }
756 : :
757 : 26494 : void Instantiate::notifyEndRound()
758 : : {
759 : : // debug information
760 [ - + ]: 26494 : if (TraceIsOn("inst-per-quant-round"))
761 : : {
762 [ - - ]: 0 : for (std::pair<const Node, uint32_t>& i : d_instDebugTemp)
763 : : {
764 [ - - ]: 0 : Trace("inst-per-quant-round")
765 : 0 : << " * " << i.second << " for " << i.first << std::endl;
766 : : }
767 : : }
768 [ + + ]: 26494 : if (isOutputOn(OutputTag::INST))
769 : : {
770 : 2 : bool req = !options().quantifiers.printInstFull;
771 [ + + ]: 6 : for (std::pair<const Node, uint32_t>& i : d_instDebugTemp)
772 : : {
773 : 4 : Node name;
774 [ - + ]: 4 : if (!d_qreg.getNameForQuant(i.first, name, req))
775 : : {
776 : 0 : continue;
777 : : }
778 : 8 : output(OutputTag::INST) << "(num-instantiations " << name << " "
779 : 4 : << i.second << ")" << std::endl;
780 [ + - ]: 4 : }
781 : : }
782 : 26494 : }
783 : :
784 : 28953 : void Instantiate::debugPrintModel()
785 : : {
786 [ - + ]: 28953 : if (TraceIsOn("inst-per-quant"))
787 : : {
788 [ - - ]: 0 : for (NodeInstListMap::iterator it = d_insts.begin(); it != d_insts.end();
789 : 0 : ++it)
790 : : {
791 [ - - ]: 0 : Trace("inst-per-quant") << " * " << (*it).second->d_list.size() << " for "
792 : 0 : << (*it).first << std::endl;
793 : : }
794 : : }
795 : 28953 : }
796 : :
797 : 100486 : InstLemmaList* Instantiate::getOrMkInstLemmaList(TNode q)
798 : : {
799 : 100486 : NodeInstListMap::iterator it = d_insts.find(q);
800 [ + + ]: 100486 : if (it != d_insts.end())
801 : : {
802 : 86273 : return it->second.get();
803 : : }
804 : : std::shared_ptr<InstLemmaList> ill =
805 : 14213 : std::make_shared<InstLemmaList>(userContext());
806 : 14213 : d_insts.insert(q, ill);
807 : 14213 : return ill.get();
808 : 14213 : }
809 : :
810 : 50938 : Instantiate::Statistics::Statistics(StatisticsRegistry& sr)
811 : 50938 : : d_instantiations(sr.registerInt("Instantiate::Instantiations_Total")),
812 : 50938 : d_inst_duplicate(sr.registerInt("Instantiate::Duplicate_Inst")),
813 : 50938 : d_inst_duplicate_eq(sr.registerInt("Instantiate::Duplicate_Inst_Eq")),
814 : : d_inst_duplicate_ent(
815 : 50938 : sr.registerInt("Instantiate::Duplicate_Inst_Entailed"))
816 : : {
817 : 50938 : }
818 : :
819 : : } // namespace quantifiers
820 : : } // namespace theory
821 : : } // namespace cvc5::internal
|
