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 quantifiers engine class.
11 : : */
12 : :
13 : : #include "theory/quantifiers_engine.h"
14 : :
15 : : #include "options/base_options.h"
16 : : #include "options/printer_options.h"
17 : : #include "options/quantifiers_options.h"
18 : : #include "options/smt_options.h"
19 : : #include "options/strings_options.h"
20 : : #include "options/uf_options.h"
21 : : #include "theory/quantifiers/equality_query.h"
22 : : #include "theory/quantifiers/first_order_model.h"
23 : : #include "theory/quantifiers/fmf/first_order_model_fmc.h"
24 : : #include "theory/quantifiers/fmf/full_model_check.h"
25 : : #include "theory/quantifiers/fmf/model_builder.h"
26 : : #include "theory/quantifiers/ieval/inst_evaluator_manager.h"
27 : : #include "theory/quantifiers/quant_module.h"
28 : : #include "theory/quantifiers/quantifiers_inference_manager.h"
29 : : #include "theory/quantifiers/quantifiers_modules.h"
30 : : #include "theory/quantifiers/quantifiers_registry.h"
31 : : #include "theory/quantifiers/quantifiers_rewriter.h"
32 : : #include "theory/quantifiers/quantifiers_state.h"
33 : : #include "theory/quantifiers/quantifiers_statistics.h"
34 : : #include "theory/quantifiers/relevant_domain.h"
35 : : #include "theory/quantifiers/skolemize.h"
36 : : #include "theory/quantifiers/term_registry.h"
37 : : #include "theory/theory_engine.h"
38 : :
39 : : using namespace std;
40 : : using namespace cvc5::internal::kind;
41 : : using namespace cvc5::internal::theory::quantifiers;
42 : :
43 : : namespace cvc5::internal {
44 : : namespace theory {
45 : :
46 : 27165 : QuantifiersEngine::QuantifiersEngine(Env& env,
47 : : QuantifiersState& qs,
48 : : QuantifiersRegistry& qr,
49 : : TermRegistry& tr,
50 : : QuantifiersInferenceManager& qim,
51 : 27165 : ProofNodeManager* pnm)
52 : : : EnvObj(env),
53 : 27165 : d_qstate(qs),
54 : 27165 : d_qim(qim),
55 : 27165 : d_te(nullptr),
56 : 27165 : d_pnm(pnm),
57 : 27165 : d_qreg(qr),
58 : 27165 : d_treg(tr),
59 : 27165 : d_model(nullptr),
60 : 27165 : d_quants_prereg(userContext()),
61 : 27165 : d_quants_red(userContext()),
62 : 27165 : d_numInstRoundsLemma(0)
63 : : {
64 : 27165 : options::FmfMbqiMode mmode = options().quantifiers.fmfMbqiMode;
65 [ + - ]: 54330 : Trace("quant-init-debug")
66 : 0 : << "Initialize model engine, mbqi : " << mmode << " "
67 : 27165 : << options().quantifiers.fmfBound << std::endl;
68 : : // Finite model finding requires specialized ways of building the model.
69 : : // We require constructing the model here, since it is required for
70 : : // initializing the CombinationEngine and the rest of quantifiers engine.
71 [ + + ]: 54025 : if (options().quantifiers.fmfBound || options().strings.stringExp
72 [ + + ][ + + ]: 54211 : || (options().quantifiers.finiteModelFind
[ + + ]
73 [ + + ]: 186 : && (mmode == options::FmfMbqiMode::FMC
74 [ + + ]: 6 : || mmode == options::FmfMbqiMode::TRUST)))
75 : : {
76 [ + - ]: 13347 : Trace("quant-init-debug") << "...make fmc builder." << std::endl;
77 : 13347 : d_builder.reset(new fmcheck::FullModelChecker(env, qs, qim, qr, tr));
78 : : }
79 : : else
80 : : {
81 [ + - ]: 13818 : Trace("quant-init-debug") << "...make default model builder." << std::endl;
82 : 13818 : d_builder.reset(new QModelBuilder(env, qs, qim, qr, tr));
83 : : }
84 : : // set the model object
85 : 27165 : d_builder->finishInit();
86 : 27165 : d_model = d_builder->getModel();
87 : :
88 : : // Finish initializing the term registry by hooking it up to the model and the
89 : : // inference manager. The former is required since theories are not given
90 : : // access to the model in their constructors currently.
91 : : // The latter is required due to a cyclic dependency between the term
92 : : // database and the instantiate module. Term database needs inference manager
93 : : // since it sends out lemmas when term indexing is inconsistent, instantiate
94 : : // needs term database for entailment checks.
95 : 27165 : d_treg.finishInit(d_model, &d_qim);
96 : :
97 : : // initialize the utilities
98 : 27165 : d_util.push_back(d_model->getEqualityQuery());
99 : : // quantifiers registry must come before the remaining utilities
100 : 27165 : d_util.push_back(&d_qreg);
101 : 27165 : d_util.push_back(tr.getTermDatabase());
102 : 27165 : d_util.push_back(qim.getInstantiate());
103 : 27165 : d_util.push_back(tr.getTermPools());
104 : 27165 : d_util.push_back(tr.getInstEvaluatorManager());
105 : 27165 : }
106 : :
107 : 54304 : QuantifiersEngine::~QuantifiersEngine() {}
108 : :
109 : 21242 : void QuantifiersEngine::finishInit(TheoryEngine* te)
110 : : {
111 : : // connect the quantifiers model to the underlying theory model
112 : 21242 : d_model->finishInit(te->getModel());
113 : 21242 : d_te = te;
114 : : // Initialize the modules and the utilities here.
115 : 21242 : d_qmodules.reset(new QuantifiersModules());
116 : 42484 : d_qmodules->initialize(
117 : 21242 : d_env, d_qstate, d_qim, d_qreg, d_treg, d_builder.get(), d_modules);
118 [ + + ]: 21242 : if (d_qmodules->d_rel_dom.get())
119 : : {
120 : 289 : d_util.push_back(d_qmodules->d_rel_dom.get());
121 : : }
122 : :
123 : : // handle any circular dependencies
124 : :
125 : : // quantifiers bound inference needs to be informed of the bounded integers
126 : : // module, which has information about which quantifiers have finite bounds
127 : 21242 : d_qreg.getQuantifiersBoundInference().finishInit(d_qmodules->d_bint.get());
128 : 21242 : }
129 : :
130 : 0 : QuantifiersRegistry& QuantifiersEngine::getQuantifiersRegistry()
131 : : {
132 : 0 : return d_qreg;
133 : : }
134 : :
135 : 21242 : QModelBuilder* QuantifiersEngine::getModelBuilder() const
136 : : {
137 : 21242 : return d_builder.get();
138 : : }
139 : :
140 : : /// !!!!!!!!!!!!!! temporary (project #15)
141 : :
142 : 3857 : TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() const
143 : : {
144 : 3857 : return d_treg.getTermDatabaseSygus();
145 : : }
146 : : /// !!!!!!!!!!!!!!
147 : :
148 : 21240 : void QuantifiersEngine::presolve()
149 : : {
150 [ + - ]: 21240 : Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl;
151 : 21240 : d_numInstRoundsLemma = 0;
152 : 21240 : d_qim.clearPending();
153 [ + + ]: 148963 : for (QuantifiersUtil*& u : d_util)
154 : : {
155 : 127723 : u->presolve();
156 : : }
157 [ + + ]: 147188 : for (QuantifiersModule*& mdl : d_modules)
158 : : {
159 : 125948 : mdl->presolve();
160 : : }
161 : 21240 : }
162 : :
163 : 24202 : void QuantifiersEngine::ppNotifyAssertions(const std::vector<Node>& assertions)
164 : : {
165 [ + - ]: 48404 : Trace("quant-engine-proc")
166 : 24202 : << "ppNotifyAssertions in QE, #assertions = " << assertions.size()
167 : 24202 : << std::endl;
168 [ + + ]: 24202 : if (options().quantifiers.instMaxLevel != -1)
169 : : {
170 [ + + ]: 373 : for (const Node& a : assertions)
171 : : {
172 : 367 : QuantAttributes::setInstantiationLevelAttr(a, 0);
173 : : }
174 : : }
175 : : // notify all modules
176 [ + + ]: 169608 : for (QuantifiersModule*& mdl : d_modules)
177 : : {
178 : 145406 : mdl->ppNotifyAssertions(assertions);
179 : : }
180 [ + + ]: 24202 : if (options().quantifiers.mbqi)
181 : : {
182 : : // may need to be notified of assertions, for mbqi-enum
183 : 1243 : quantifiers::InstStrategyMbqi* mi = d_qmodules->d_mbqi.get();
184 : 1243 : mi->ppNotifyAssertions(assertions);
185 : : }
186 : 24202 : }
187 : 176914 : void QuantifiersEngine::check(Theory::Effort e)
188 : : {
189 : 176914 : IncompleteId setModelUnsoundId = IncompleteId::NONE;
190 : 176914 : checkInternal(e, setModelUnsoundId);
191 : : // SAT case
192 [ + + ][ + + ]: 176895 : if (e == Theory::EFFORT_LAST_CALL && !d_qstate.getValuation().needCheck())
[ + + ]
193 : : {
194 : : // if we are about to say "unknown", see if anything can be done as a last
195 : : // resort to avoid this
196 : 18436 : if (setModelUnsoundId != IncompleteId::NONE
197 [ + + ][ + + ]: 9218 : && shouldRecheck(e, setModelUnsoundId))
[ + + ]
198 : : {
199 [ + - ]: 318 : Trace("quant-engine-debug") << "*** Run recheck" << std::endl;
200 : : // We simply mark the output channel is used, which will ensure we are
201 : : // called again to check.
202 : : // We do this instead of checking again here since some modules (e.g. fmf)
203 : : // assume that models are only built once per last call effort check.
204 : 318 : d_qim.markUsed();
205 : : }
206 : : else
207 : : {
208 [ + + ]: 8900 : if (setModelUnsoundId != IncompleteId::NONE)
209 : : {
210 [ + - ]: 767 : Trace("quant-engine") << "Set incomplete flag." << std::endl;
211 : 767 : d_qim.setModelUnsound(setModelUnsoundId);
212 : : }
213 : : // output debug stats
214 : 8900 : d_qim.getInstantiate()->debugPrintModel();
215 : : }
216 : : }
217 : 176895 : d_qim.clearPending();
218 : 176895 : }
219 : :
220 : 1085 : bool QuantifiersEngine::shouldRecheck(CVC5_UNUSED Theory::Effort e,
221 : : IncompleteId setModelUnsoundId)
222 : : {
223 : : // special case: IncompleteId::QUANTIFIERS_RECORDED_INST indicates we wish
224 : : // to intentionally answer unknown for partial quantifier elimination
225 [ + + ]: 1085 : if (setModelUnsoundId == IncompleteId::QUANTIFIERS_RECORDED_INST)
226 : : {
227 : 1 : return false;
228 : : }
229 : : // do not recheck with sygus
230 [ + + ]: 1084 : if (options().quantifiers.sygus)
231 : : {
232 : 601 : return false;
233 : : }
234 : : // If the term database mode is relevant, we instead now mark all terms
235 : : // as relevant.
236 : 483 : if (options().quantifiers.termDbMode
237 [ + - ]: 483 : == options::TermDbMode::RELEVANT_ALL_DELAY)
238 : : {
239 : 483 : TermDb* tdb = d_treg.getTermDatabase();
240 : 483 : eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
241 [ - + ][ - + ]: 483 : Assert(ee->consistent());
[ - - ]
242 : 483 : bool recheck = false;
243 : 483 : eq::EqClassesIterator eqcsi = eq::EqClassesIterator(ee);
244 [ + + ]: 19702 : while (!eqcsi.isFinished())
245 : : {
246 : 19219 : eq::EqClassIterator eqci = eq::EqClassIterator(*eqcsi, ee);
247 [ + + ]: 58321 : while (!eqci.isFinished())
248 : : {
249 : 39102 : Node n = *eqci;
250 : : // to ensure we saturate, we only recheck if at least one new term
251 : : // was added to the term database
252 [ + + ]: 39102 : if (!tdb->hasTermCurrent(n))
253 : : {
254 : 5990 : tdb->setHasTerm(*eqci);
255 : 5990 : recheck = true;
256 : : }
257 : 39102 : ++eqci;
258 : 39102 : }
259 : 19219 : ++eqcsi;
260 : : }
261 : 483 : return recheck;
262 : : }
263 : 0 : return false;
264 : : }
265 : :
266 : 176914 : void QuantifiersEngine::checkInternal(Theory::Effort e,
267 : : IncompleteId& setModelUnsoundId)
268 : : {
269 : 176914 : QuantifiersStatistics& stats = d_qstate.getStats();
270 : 176914 : CodeTimer codeTimer(stats.d_time);
271 [ - + ][ - + ]: 176914 : Assert(d_qstate.getEqualityEngine() != nullptr);
[ - - ]
272 [ - + ]: 176914 : if (!d_qstate.getEqualityEngine()->consistent())
273 : : {
274 [ - - ]: 0 : Trace("quant-engine-debug")
275 : 0 : << "Master equality engine not consistent, return." << std::endl;
276 : 0 : return;
277 : : }
278 [ - + ]: 176914 : if (d_qstate.isInConflict())
279 : : {
280 [ - - ]: 0 : if (e < Theory::EFFORT_LAST_CALL)
281 : : {
282 : : // this can happen in rare cases when quantifiers is the first to realize
283 : : // there is a quantifier-free conflict, for example, when it discovers
284 : : // disequal and congruent terms in the master equality engine during
285 : : // term indexing. In such cases, quantifiers reports a "conflicting lemma"
286 : : // that is, one that is entailed to be false by the current assignment.
287 : : // If this lemma is not a SAT conflict, we may get another call to full
288 : : // effort check and the quantifier-free solvers still haven't realized
289 : : // there is a conflict. In this case, we return, trusting that theory
290 : : // combination will do the right thing (split on equalities until there is
291 : : // a conflict at the quantifier-free level).
292 [ - - ]: 0 : Trace("quant-engine-debug")
293 : 0 : << "Conflicting lemma already reported by quantifiers, return."
294 : 0 : << std::endl;
295 : 0 : return;
296 : : }
297 : : // we reported what we thought was a conflicting lemma, but now we have
298 : : // gotten a check at LAST_CALL effort, indicating that the lemma we reported
299 : : // was not conflicting. This should never happen, but in production mode, we
300 : : // proceed with the check.
301 : 0 : DebugUnhandled();
302 : : }
303 : 176914 : bool needsCheck = d_qim.hasPendingLemma();
304 : 176914 : QuantifiersModule::QEffort needsModelE = QuantifiersModule::QEFFORT_NONE;
305 : 176914 : std::vector<QuantifiersModule*> qm;
306 [ + + ]: 176914 : if (d_model->checkNeeded())
307 : : {
308 : 118199 : needsCheck =
309 [ + + ][ + + ]: 118199 : needsCheck || e >= Theory::EFFORT_LAST_CALL; // always need to check at
310 : : // or above last call
311 [ + + ]: 807975 : for (QuantifiersModule*& mdl : d_modules)
312 : : {
313 [ + + ]: 689776 : if (mdl->needsCheck(e))
314 : : {
315 : 167758 : qm.push_back(mdl);
316 : 167758 : needsCheck = true;
317 : : // can only request model at last call since theory combination can find
318 : : // inconsistencies
319 [ + + ]: 167758 : if (e >= Theory::EFFORT_LAST_CALL)
320 : : {
321 : 108390 : QuantifiersModule::QEffort me = mdl->needsModel(e);
322 [ + + ]: 108390 : needsModelE = me < needsModelE ? me : needsModelE;
323 : : }
324 : : }
325 : : }
326 : : }
327 : :
328 : 176914 : d_qim.reset();
329 : 176914 : if (options().quantifiers.instMaxRounds >= 0
330 [ + + ][ + + ]: 185928 : && d_numInstRoundsLemma
331 [ + + ]: 9014 : >= static_cast<uint32_t>(options().quantifiers.instMaxRounds))
332 : : {
333 : 282 : needsCheck = false;
334 : 282 : setModelUnsoundId = IncompleteId::QUANTIFIERS_MAX_INST_ROUNDS;
335 : : }
336 : :
337 [ + - ]: 353828 : Trace("quant-engine-debug2")
338 : 0 : << "Quantifiers Engine call to check, level = " << e
339 : 176914 : << ", needsCheck=" << needsCheck << std::endl;
340 [ + + ]: 176914 : if (needsCheck)
341 : : {
342 : : // flush previous lemmas (for instance, if was interrupted), or other lemmas
343 : : // to process
344 : 62869 : d_qim.doPending();
345 [ + + ]: 62869 : if (d_qim.hasSentLemma())
346 : : {
347 : 254 : return;
348 : : }
349 : :
350 : 62615 : double clSet = 0;
351 [ - + ]: 62615 : if (TraceIsOn("quant-engine"))
352 : : {
353 : 0 : clSet = double(clock()) / double(CLOCKS_PER_SEC);
354 [ - - ]: 0 : Trace("quant-engine") << ">>>>> Quantifiers Engine Round, effort = " << e
355 : 0 : << " <<<<<" << std::endl;
356 : : }
357 : :
358 [ - + ]: 62615 : if (TraceIsOn("quant-engine-debug"))
359 : : {
360 [ - - ]: 0 : Trace("quant-engine-debug")
361 : 0 : << "Quantifiers Engine check, level = " << e << std::endl;
362 [ - - ]: 0 : Trace("quant-engine-debug")
363 : 0 : << " depth : " << d_qstate.getInstRoundDepth() << std::endl;
364 [ - - ]: 0 : Trace("quant-engine-debug") << " modules to check : ";
365 [ - - ]: 0 : for (unsigned i = 0; i < qm.size(); i++)
366 : : {
367 : 0 : Trace("quant-engine-debug") << qm[i]->identify() << " ";
368 : : }
369 [ - - ]: 0 : Trace("quant-engine-debug") << std::endl;
370 [ - - ]: 0 : Trace("quant-engine-debug")
371 : 0 : << " # quantified formulas = "
372 : 0 : << d_model->getNumAssertedQuantifiers() << std::endl;
373 [ - - ]: 0 : if (d_qim.hasPendingLemma())
374 : : {
375 [ - - ]: 0 : Trace("quant-engine-debug")
376 : 0 : << " lemmas waiting = " << d_qim.numPendingLemmas() << std::endl;
377 : : }
378 [ - - ]: 0 : Trace("quant-engine-debug")
379 : 0 : << " Theory engine finished : "
380 : 0 : << !d_qstate.getValuation().needCheck() << std::endl;
381 [ - - ]: 0 : Trace("quant-engine-debug")
382 : 0 : << " Needs model effort : " << needsModelE << std::endl;
383 [ - - ]: 0 : Trace("quant-engine-debug")
384 : 0 : << " In conflict : " << d_qstate.isInConflict() << std::endl;
385 : : }
386 [ - + ]: 62615 : if (TraceIsOn("quant-engine-ee-pre"))
387 : : {
388 [ - - ]: 0 : Trace("quant-engine-ee-pre")
389 : 0 : << "Equality engine (pre-inference): " << std::endl;
390 : 0 : d_qstate.debugPrintEqualityEngine("quant-engine-ee-pre");
391 : : }
392 [ - + ]: 62615 : if (TraceIsOn("quant-engine-assert"))
393 : : {
394 [ - - ]: 0 : Trace("quant-engine-assert") << "Assertions : " << std::endl;
395 : 0 : d_te->printAssertions("quant-engine-assert");
396 : : }
397 : :
398 : : // reset utilities
399 [ + - ]: 62615 : Trace("quant-engine-debug") << "Resetting all utilities..." << std::endl;
400 [ + + ]: 441414 : for (QuantifiersUtil*& util : d_util)
401 : : {
402 [ + - ]: 757598 : Trace("quant-engine-debug2")
403 [ - + ][ - - ]: 378799 : << "Reset " << util->identify().c_str() << "..." << std::endl;
404 [ - + ]: 378799 : if (!util->reset(e))
405 : : {
406 : 0 : d_qim.doPending();
407 [ - - ]: 0 : if (d_qim.hasSentLemma())
408 : : {
409 : 0 : return;
410 : : }
411 : : else
412 : : {
413 : : // should only fail reset if added a lemma
414 : 0 : DebugUnhandled();
415 : : }
416 : : }
417 : : }
418 : :
419 [ - + ]: 62615 : if (TraceIsOn("quant-engine-ee"))
420 : : {
421 [ - - ]: 0 : Trace("quant-engine-ee") << "Equality engine : " << std::endl;
422 : 0 : d_qstate.debugPrintEqualityEngine("quant-engine-ee");
423 : : }
424 : :
425 : : // reset the model
426 [ + - ]: 62615 : Trace("quant-engine-debug") << "Reset model..." << std::endl;
427 : 62615 : d_model->reset_round();
428 : :
429 : : // reset the modules
430 [ + - ]: 62615 : Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
431 [ + + ]: 422855 : for (QuantifiersModule*& mdl : d_modules)
432 : : {
433 [ + - ]: 720480 : Trace("quant-engine-debug2")
434 [ - + ][ - - ]: 360240 : << "Reset " << mdl->identify().c_str() << std::endl;
435 : 360240 : mdl->reset_round(e);
436 : : }
437 [ + - ]: 62615 : Trace("quant-engine-debug") << "Done resetting all modules." << std::endl;
438 : : // reset may have added lemmas
439 : 62615 : d_qim.doPending();
440 [ - + ]: 62615 : if (d_qim.hasSentLemma())
441 : : {
442 : 0 : return;
443 : : }
444 : :
445 [ + + ]: 62615 : if (e == Theory::EFFORT_LAST_CALL)
446 : : {
447 : 25122 : ++(stats.d_instantiation_rounds_lc);
448 : : }
449 [ + + ]: 37493 : else if (e == Theory::EFFORT_FULL)
450 : : {
451 : 37405 : ++(stats.d_instantiation_rounds);
452 : : }
453 [ + - ]: 125230 : Trace("quant-engine-debug")
454 : 62615 : << "Check modules that needed check..." << std::endl;
455 : 247575 : for (unsigned qef = QuantifiersModule::QEFFORT_CONFLICT;
456 [ + + ]: 247575 : qef <= QuantifiersModule::QEFFORT_LAST_CALL;
457 : : ++qef)
458 : : {
459 : 209666 : QuantifiersModule::QEffort quant_e =
460 : : static_cast<QuantifiersModule::QEffort>(qef);
461 : : // Force the theory engine to build the model if any module requested it.
462 [ + + ]: 209666 : if (needsModelE == quant_e)
463 : : {
464 [ + - ]: 22227 : Trace("quant-engine-debug") << "Build model..." << std::endl;
465 [ + + ]: 22227 : if (!d_te->buildModel())
466 : : {
467 : : // If we failed to build the model, flush all pending lemmas and
468 : : // finish.
469 : 178 : d_qim.doPending();
470 : 24687 : break;
471 : : }
472 : : }
473 [ + - ]: 209488 : if (!d_qim.hasSentLemma())
474 : : {
475 : : // check each module
476 [ + + ]: 736870 : for (QuantifiersModule*& mdl : qm)
477 : : {
478 [ + - ]: 1054892 : Trace("quant-engine-debug")
479 [ - + ][ - - ]: 527446 : << "Check " << mdl->identify().c_str() << " at effort " << quant_e
480 : 527446 : << "..." << std::endl;
481 : 527446 : mdl->check(e, quant_e);
482 [ + + ]: 527428 : if (d_qstate.isInConflict())
483 : : {
484 [ + - ]: 46 : Trace("quant-engine-debug") << "...conflict!" << std::endl;
485 : 46 : break;
486 : : }
487 : : }
488 : : // flush all current lemmas
489 : 209470 : d_qim.doPending();
490 : : }
491 : : // If we have added a lemma, stop. We also stop if we are in conflict.
492 : : // In very rare cases, it may be the case that quantifiers knows there
493 : : // is a conflict without adding a lemma, e.g. if it sent a duplicate
494 : : // QUANTIFIERS_TDB_DEQ_CONG lemma, which can occur if it has detected
495 : : // a quantifier-free conflict during term indexing but the quantifier
496 : : // free theories haven't caused a backtrack yet. This should never happen
497 : : // at LAST_CALL effort.
498 [ + + ][ - + ]: 209469 : if (d_qim.hasSentLemma() || d_qstate.isInConflict())
[ + + ]
499 : : {
500 [ - + ][ - - ]: 23717 : Assert(d_qim.hasSentLemma() || e != Theory::EFFORT_LAST_CALL);
[ - + ][ - + ]
[ - - ]
501 : 23717 : break;
502 : : }
503 : : else
504 : : {
505 [ + + ]: 185752 : if (quant_e == QuantifiersModule::QEFFORT_CONFLICT)
506 : : {
507 : : // increment the instantiation round counter only if we did not find a
508 : : // conflict or lemma at QEFFORT_CONFLICT above.
509 : 59156 : d_qstate.incrementInstRoundCounters(e);
510 : : }
511 [ + + ]: 126596 : else if (quant_e == QuantifiersModule::QEFFORT_MODEL)
512 : : {
513 [ + + ]: 39033 : if (e == Theory::EFFORT_LAST_CALL)
514 : : {
515 : : // sources of incompleteness
516 [ + + ]: 45562 : for (QuantifiersUtil*& util : d_util)
517 : : {
518 [ + + ]: 39137 : if (!util->checkComplete(setModelUnsoundId))
519 : : {
520 [ + - ]: 2 : Trace("quant-engine-debug") << "Set incomplete because utility "
521 [ - + ][ - - ]: 1 : << util->identify().c_str()
522 : 1 : << " was incomplete." << std::endl;
523 : : }
524 : : }
525 [ - + ]: 6425 : if (d_qstate.isInConflict())
526 : : {
527 : : // we reported a conflicting lemma, should return
528 : 0 : setModelUnsoundId = IncompleteId::QUANTIFIERS;
529 : : }
530 : : // if we have a chance not to set incomplete
531 [ + + ]: 6425 : if (setModelUnsoundId == IncompleteId::NONE)
532 : : {
533 : : // check if we should set the incomplete flag
534 [ + + ]: 42073 : for (QuantifiersModule*& mdl : d_modules)
535 : : {
536 [ + + ]: 35855 : if (!mdl->checkComplete(setModelUnsoundId))
537 : : {
538 [ + - ]: 412 : Trace("quant-engine-debug")
539 : 0 : << "Set incomplete because module "
540 [ - + ][ - - ]: 206 : << mdl->identify().c_str() << " was incomplete."
541 : 206 : << std::endl;
542 : 206 : break;
543 : : }
544 : : }
545 [ + + ]: 6424 : if (setModelUnsoundId == IncompleteId::NONE)
546 : : {
547 : : // look at individual quantified formulas, one module must claim
548 : : // completeness for each one
549 [ + + ]: 8120 : for (unsigned i = 0; i < d_model->getNumAssertedQuantifiers();
550 : : i++)
551 : : {
552 : 7328 : bool hasCompleteM = false;
553 : 7328 : Node q = d_model->getAssertedQuantifier(i);
554 : 7328 : QuantifiersModule* qmd = d_qreg.getOwner(q);
555 [ + + ]: 7328 : if (qmd != nullptr)
556 : : {
557 : 4707 : hasCompleteM = qmd->checkCompleteFor(q);
558 : : }
559 : : else
560 : : {
561 [ + + ]: 13745 : for (unsigned j = 0; j < d_modules.size(); j++)
562 : : {
563 [ + + ]: 12778 : if (d_modules[j]->checkCompleteFor(q))
564 : : {
565 : 1654 : qmd = d_modules[j];
566 : 1654 : hasCompleteM = true;
567 : 1654 : break;
568 : : }
569 : : }
570 : : }
571 [ + + ]: 7328 : if (!hasCompleteM)
572 : : {
573 [ + - ]: 10852 : Trace("quant-engine-debug")
574 : 0 : << "Set incomplete because " << q
575 : 5426 : << " was not fully processed." << std::endl;
576 : 5426 : setModelUnsoundId = IncompleteId::QUANTIFIERS;
577 : 5426 : break;
578 : : }
579 : : else
580 : : {
581 [ - + ][ - + ]: 1902 : Assert(qmd != nullptr);
[ - - ]
582 [ + - ]: 3804 : Trace("quant-engine-debug2")
583 : 0 : << "Complete for " << q << " due to "
584 [ - + ][ - - ]: 1902 : << qmd->identify().c_str() << std::endl;
585 : : }
586 [ + + ]: 7328 : }
587 : : }
588 : : }
589 : : // if setModelUnsoundId is not set, we will answer SAT, otherwise we
590 : : // will run at quant_e QEFFORT_LAST_CALL
591 [ + + ]: 6425 : if (setModelUnsoundId == IncompleteId::NONE)
592 : : {
593 : 792 : break;
594 : : }
595 : : }
596 : : }
597 : : }
598 : : }
599 [ + - ]: 125192 : Trace("quant-engine-debug")
600 : 62596 : << "Done check modules that needed check." << std::endl;
601 : : // debug print
602 [ + + ]: 62596 : if (d_qim.hasSentLemma())
603 : : {
604 : 23717 : d_qim.getInstantiate()->notifyEndRound();
605 : 23717 : d_numInstRoundsLemma++;
606 : : }
607 [ - + ]: 62596 : if (TraceIsOn("quant-engine"))
608 : : {
609 : 0 : double clSet2 = double(clock()) / double(CLOCKS_PER_SEC);
610 [ - - ]: 0 : Trace("quant-engine")
611 : 0 : << "Finished quantifiers engine, total time = " << (clSet2 - clSet);
612 [ - - ]: 0 : Trace("quant-engine") << ", sent lemma = " << d_qim.hasSentLemma();
613 [ - - ]: 0 : Trace("quant-engine") << std::endl;
614 : : }
615 : :
616 [ + - ]: 125192 : Trace("quant-engine-debug2")
617 : 62596 : << "Finished quantifiers engine check." << std::endl;
618 : : }
619 : : else
620 : : {
621 [ + - ]: 228090 : Trace("quant-engine-debug2")
622 : 114045 : << "Quantifiers Engine does not need check." << std::endl;
623 : : // increment counter
624 : 114045 : d_qstate.incrementInstRoundCounters(e);
625 : : }
626 [ + + ][ + + ]: 177187 : }
627 : :
628 : 34129 : void QuantifiersEngine::notifyCombineTheories()
629 : : {
630 : : // If allowing theory combination to happen at most once between instantiation
631 : : // rounds, this would reset d_ierCounter to 1 and d_ierCounterLastLc to -1
632 : : // in quantifiers state.
633 : 34129 : }
634 : :
635 : 146978 : bool QuantifiersEngine::reduceQuantifier(Node q)
636 : : {
637 : : // TODO: this can be unified with preregistration: AlphaEquivalence takes
638 : : // ownership of reducable quants
639 : 146978 : BoolMap::const_iterator it = d_quants_red.find(q);
640 [ + + ]: 146978 : if (it == d_quants_red.end())
641 : : {
642 : 49140 : TrustNode tlem;
643 : 49140 : InferenceId id = InferenceId::UNKNOWN;
644 [ + - ]: 49140 : if (d_qmodules->d_alpha_equiv)
645 : : {
646 [ + - ]: 98280 : Trace("quant-engine-red")
647 : 49140 : << "Alpha equivalence " << q << "?" << std::endl;
648 : : // add equivalence with another quantified formula
649 : 49140 : tlem = d_qmodules->d_alpha_equiv->reduceQuantifier(q);
650 : 49140 : id = InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ;
651 [ + + ]: 49140 : if (!tlem.isNull())
652 : : {
653 [ + - ]: 8944 : Trace("quant-engine-red")
654 : 4472 : << "...alpha equivalence success." << std::endl;
655 : 4472 : ++(d_qstate.getStats().d_red_alpha_equiv);
656 : : }
657 : : }
658 [ + + ]: 49140 : if (!tlem.isNull())
659 : : {
660 : 4472 : d_qim.trustedLemma(tlem, id);
661 : : }
662 : 49140 : d_quants_red[q] = !tlem.isNull();
663 : 49140 : return !tlem.isNull();
664 : 49140 : }
665 : 97838 : return (*it).second;
666 : : }
667 : :
668 : 112754 : void QuantifiersEngine::registerQuantifierInternal(Node f)
669 : : {
670 : 112754 : std::map<Node, bool>::iterator it = d_quants.find(f);
671 [ + + ]: 112754 : if (it == d_quants.end())
672 : : {
673 [ + - ]: 44626 : Trace("quant") << "QuantifiersEngine : Register quantifier ";
674 [ + - ]: 44626 : Trace("quant") << " : " << f << std::endl;
675 : 44626 : size_t prev_lemma_waiting = d_qim.numPendingLemmas();
676 : 44626 : ++(d_qstate.getStats().d_num_quant);
677 [ - + ][ - + ]: 44626 : Assert(f.getKind() == Kind::FORALL);
[ - - ]
678 : : // register with utilities
679 [ + + ]: 321945 : for (unsigned i = 0; i < d_util.size(); i++)
680 : : {
681 : 277319 : d_util[i]->registerQuantifier(f);
682 : : }
683 : :
684 [ + + ]: 297084 : for (QuantifiersModule*& mdl : d_modules)
685 : : {
686 [ + - ][ - + ]: 504916 : Trace("quant-debug") << "check ownership with " << mdl->identify()
[ - - ]
687 : 252458 : << "..." << std::endl;
688 : 252458 : mdl->checkOwnership(f);
689 : : }
690 : 44626 : QuantifiersModule* qm = d_qreg.getOwner(f);
691 : 89252 : Trace("quant") << " Owner : " << (qm == nullptr ? "[none]" : qm->identify())
692 : 44626 : << std::endl;
693 : : // register with each module
694 [ + + ]: 297084 : for (QuantifiersModule*& mdl : d_modules)
695 : : {
696 [ + - ][ - + ]: 504916 : Trace("quant-debug") << "register with " << mdl->identify() << "..."
[ - - ]
697 : 252458 : << std::endl;
698 : 252458 : mdl->registerQuantifier(f);
699 : : // since this is context-independent, we should not add any lemmas during
700 : : // this call
701 [ - + ][ - + ]: 252458 : Assert(d_qim.numPendingLemmas() == prev_lemma_waiting);
[ - - ]
702 : : }
703 [ + - ]: 44626 : Trace("quant-debug") << "...finish." << std::endl;
704 : 44626 : d_quants[f] = true;
705 [ - + ][ - + ]: 44626 : AlwaysAssert(d_qim.numPendingLemmas() == prev_lemma_waiting);
[ - - ]
706 : : }
707 : 112754 : }
708 : :
709 : 56005 : void QuantifiersEngine::preRegisterQuantifier(Node q)
710 : : {
711 : 56005 : NodeSet::const_iterator it = d_quants_prereg.find(q);
712 [ + + ]: 56005 : if (it != d_quants_prereg.end())
713 : : {
714 : 11337 : return;
715 : : }
716 [ + - ]: 49140 : Trace("quant-debug") << "QuantifiersEngine : Pre-register " << q << std::endl;
717 : 49140 : d_quants_prereg.insert(q);
718 : : // try to reduce
719 [ + + ]: 49140 : if (reduceQuantifier(q))
720 : : {
721 : : // if we can reduce it, nothing left to do
722 : 4472 : return;
723 : : }
724 : : // ensure that it is registered
725 : 44668 : registerQuantifierInternal(q);
726 : : // register with each module
727 [ + + ]: 297368 : for (QuantifiersModule*& mdl : d_modules)
728 : : {
729 [ + - ][ - + ]: 505400 : Trace("quant-debug") << "pre-register with " << mdl->identify() << "..."
[ - - ]
730 : 252700 : << std::endl;
731 : 252700 : mdl->preRegisterQuantifier(q);
732 : : }
733 : : // flush the lemmas
734 : 44668 : d_qim.doPending();
735 [ + - ]: 44668 : Trace("quant-debug") << "...finish pre-register " << q << "..." << std::endl;
736 : : }
737 : :
738 : 97838 : void QuantifiersEngine::assertQuantifier(Node f, bool pol)
739 : : {
740 [ + + ]: 97838 : if (reduceQuantifier(f))
741 : : {
742 : : // if we can reduce it, nothing left to do
743 : 9644 : return;
744 : : }
745 [ + + ]: 88194 : if (!pol)
746 : : {
747 : : // do skolemization
748 : 20108 : TrustNode lem = d_qim.getSkolemize()->process(f);
749 [ + + ]: 20108 : if (!lem.isNull())
750 : : {
751 [ - + ]: 5366 : if (TraceIsOn("quantifiers-sk-debug"))
752 : : {
753 : 0 : Node slem = rewrite(lem.getNode());
754 [ - - ]: 0 : Trace("quantifiers-sk-debug")
755 : 0 : << "Skolemize lemma : " << slem << std::endl;
756 : 0 : }
757 : 5366 : d_qim.trustedLemma(lem,
758 : : InferenceId::QUANTIFIERS_SKOLEMIZE,
759 : : LemmaProperty::NEEDS_JUSTIFY);
760 : : }
761 : 20108 : return;
762 : 20108 : }
763 : : // ensure the quantified formula is registered
764 : 68086 : registerQuantifierInternal(f);
765 : : // assert it to each module
766 : 68086 : d_model->assertQuantifier(f);
767 [ + + ]: 467854 : for (QuantifiersModule*& mdl : d_modules)
768 : : {
769 : 399768 : mdl->assertNode(f);
770 : : }
771 : : // add term to the registry
772 : 68086 : d_treg.addQuantifierBody(d_qreg.getInstConstantBody(f));
773 : : }
774 : :
775 : 1750048 : void QuantifiersEngine::eqNotifyNewClass(TNode t)
776 : : {
777 : 1750048 : d_treg.eqNotifyNewClass(t);
778 : 1750048 : }
779 : :
780 : 9018955 : void QuantifiersEngine::eqNotifyMerge(TNode t1, TNode t2)
781 : : {
782 : 9018955 : d_treg.eqNotifyMerge(t1, t2);
783 : 9018955 : }
784 : :
785 : 0 : void QuantifiersEngine::markRelevant(Node q) { d_model->markRelevant(q); }
786 : :
787 : 71 : void QuantifiersEngine::getInstantiationTermVectors(
788 : : Node q, std::vector<std::vector<Node> >& tvecs)
789 : : {
790 : 71 : d_qim.getInstantiate()->getInstantiationTermVectors(q, tvecs);
791 : 71 : }
792 : :
793 : 10 : void QuantifiersEngine::getInstantiationTermVectors(
794 : : std::map<Node, std::vector<std::vector<Node> > >& insts)
795 : : {
796 : 10 : d_qim.getInstantiate()->getInstantiationTermVectors(insts);
797 : 10 : }
798 : :
799 : 26 : void QuantifiersEngine::getInstantiations(Node q, std::vector<Node>& insts)
800 : : {
801 : 26 : d_qim.getInstantiate()->getInstantiations(q, insts);
802 : 26 : }
803 : :
804 : 97 : void QuantifiersEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
805 : : {
806 : 97 : d_qim.getInstantiate()->getInstantiatedQuantifiedFormulas(qs);
807 : 97 : }
808 : :
809 : 10 : void QuantifiersEngine::getSkolemTermVectors(
810 : : std::map<Node, std::vector<Node> >& sks) const
811 : : {
812 : 10 : d_qim.getSkolemize()->getSkolemTermVectors(sks);
813 : 10 : }
814 : :
815 : 0 : Node QuantifiersEngine::getNameForQuant(Node q) const
816 : : {
817 : 0 : return d_qreg.getNameForQuant(q);
818 : : }
819 : :
820 : 26 : bool QuantifiersEngine::getNameForQuant(Node q, Node& name, bool req) const
821 : : {
822 : 26 : return d_qreg.getNameForQuant(q, name, req);
823 : : }
824 : :
825 : 736 : bool QuantifiersEngine::getSynthSolutions(
826 : : std::map<Node, std::map<Node, Node> >& sol_map)
827 : : {
828 : 736 : return d_qmodules->d_synth_e->getSynthSolutions(sol_map);
829 : : }
830 : 28 : void QuantifiersEngine::declarePool(Node p, const std::vector<Node>& initValue)
831 : : {
832 : 28 : d_treg.declarePool(p, initValue);
833 : 28 : }
834 : :
835 : 9 : void QuantifiersEngine::declareOracleFun(Node f)
836 : : {
837 [ - + ]: 9 : if (d_qmodules->d_oracleEngine.get() == nullptr)
838 : : {
839 : 0 : warning() << "Cannot declare oracle function when oracles are disabled"
840 : 0 : << std::endl;
841 : 0 : return;
842 : : }
843 : 9 : d_qmodules->d_oracleEngine->declareOracleFun(f);
844 : : }
845 : 0 : std::vector<Node> QuantifiersEngine::getOracleFuns() const
846 : : {
847 [ - - ]: 0 : if (d_qmodules->d_oracleEngine.get() == nullptr)
848 : : {
849 : 0 : return {};
850 : : }
851 : 0 : return d_qmodules->d_oracleEngine->getOracleFuns();
852 : : }
853 : :
854 : : } // namespace theory
855 : : } // namespace cvc5::internal
|
