Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Morgan Deters, Gereon Kremer
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Implementation of quantifiers engine class.
14 : : */
15 : :
16 : : #include "theory/quantifiers_engine.h"
17 : :
18 : : #include "options/base_options.h"
19 : : #include "options/printer_options.h"
20 : : #include "options/quantifiers_options.h"
21 : : #include "options/smt_options.h"
22 : : #include "options/strings_options.h"
23 : : #include "options/uf_options.h"
24 : : #include "theory/quantifiers/equality_query.h"
25 : : #include "theory/quantifiers/first_order_model.h"
26 : : #include "theory/quantifiers/fmf/first_order_model_fmc.h"
27 : : #include "theory/quantifiers/fmf/full_model_check.h"
28 : : #include "theory/quantifiers/fmf/model_builder.h"
29 : : #include "theory/quantifiers/ieval/inst_evaluator_manager.h"
30 : : #include "theory/quantifiers/quant_module.h"
31 : : #include "theory/quantifiers/quantifiers_inference_manager.h"
32 : : #include "theory/quantifiers/quantifiers_modules.h"
33 : : #include "theory/quantifiers/quantifiers_registry.h"
34 : : #include "theory/quantifiers/quantifiers_rewriter.h"
35 : : #include "theory/quantifiers/quantifiers_state.h"
36 : : #include "theory/quantifiers/quantifiers_statistics.h"
37 : : #include "theory/quantifiers/relevant_domain.h"
38 : : #include "theory/quantifiers/skolemize.h"
39 : : #include "theory/quantifiers/term_registry.h"
40 : : #include "theory/theory_engine.h"
41 : :
42 : : using namespace std;
43 : : using namespace cvc5::internal::kind;
44 : : using namespace cvc5::internal::theory::quantifiers;
45 : :
46 : : namespace cvc5::internal {
47 : : namespace theory {
48 : :
49 : 47593 : QuantifiersEngine::QuantifiersEngine(Env& env,
50 : : QuantifiersState& qs,
51 : : QuantifiersRegistry& qr,
52 : : TermRegistry& tr,
53 : : QuantifiersInferenceManager& qim,
54 : 47593 : ProofNodeManager* pnm)
55 : : : EnvObj(env),
56 : : d_qstate(qs),
57 : : d_qim(qim),
58 : : d_te(nullptr),
59 : : d_pnm(pnm),
60 : : d_qreg(qr),
61 : : d_treg(tr),
62 : : d_model(nullptr),
63 : 95186 : d_quants_prereg(userContext()),
64 : 95186 : d_quants_red(userContext()),
65 : 47593 : d_numInstRoundsLemma(0)
66 : : {
67 : 47593 : options::FmfMbqiMode mmode = options().quantifiers.fmfMbqiMode;
68 [ + - ]: 95186 : Trace("quant-init-debug")
69 : 0 : << "Initialize model engine, mbqi : " << mmode << " "
70 : 47593 : << options().quantifiers.fmfBound << std::endl;
71 : : // Finite model finding requires specialized ways of building the model.
72 : : // We require constructing the model here, since it is required for
73 : : // initializing the CombinationEngine and the rest of quantifiers engine.
74 [ + + ]: 94990 : if (options().quantifiers.fmfBound || options().strings.stringExp
75 [ + + ][ + + ]: 95161 : || (options().quantifiers.finiteModelFind
[ + + ]
76 [ + + ]: 171 : && (mmode == options::FmfMbqiMode::FMC
77 [ - + ]: 2 : || mmode == options::FmfMbqiMode::TRUST)))
78 : : {
79 [ + - ]: 30736 : Trace("quant-init-debug") << "...make fmc builder." << std::endl;
80 : 30736 : d_builder.reset(new fmcheck::FullModelChecker(env, qs, qim, qr, tr));
81 : : }
82 : : else
83 : : {
84 [ + - ]: 16857 : Trace("quant-init-debug") << "...make default model builder." << std::endl;
85 : 16857 : d_builder.reset(new QModelBuilder(env, qs, qim, qr, tr));
86 : : }
87 : : // set the model object
88 : 47593 : d_builder->finishInit();
89 : 47593 : d_model = d_builder->getModel();
90 : :
91 : : // Finish initializing the term registry by hooking it up to the model and the
92 : : // inference manager. The former is required since theories are not given
93 : : // access to the model in their constructors currently.
94 : : // The latter is required due to a cyclic dependency between the term
95 : : // database and the instantiate module. Term database needs inference manager
96 : : // since it sends out lemmas when term indexing is inconsistent, instantiate
97 : : // needs term database for entailment checks.
98 : 47593 : d_treg.finishInit(d_model, &d_qim);
99 : :
100 : : // initialize the utilities
101 : 47593 : d_util.push_back(d_model->getEqualityQuery());
102 : : // quantifiers registry must come before the remaining utilities
103 : 47593 : d_util.push_back(&d_qreg);
104 : 47593 : d_util.push_back(tr.getTermDatabase());
105 : 47593 : d_util.push_back(qim.getInstantiate());
106 : 47593 : d_util.push_back(tr.getTermPools());
107 : 47593 : d_util.push_back(tr.getInstEvaluatorManager());
108 : 47593 : }
109 : :
110 : 94674 : QuantifiersEngine::~QuantifiersEngine() {}
111 : :
112 : 41166 : void QuantifiersEngine::finishInit(TheoryEngine* te)
113 : : {
114 : : // connect the quantifiers model to the underlying theory model
115 : 41166 : d_model->finishInit(te->getModel());
116 : 41166 : d_te = te;
117 : : // Initialize the modules and the utilities here.
118 : 41166 : d_qmodules.reset(new QuantifiersModules());
119 : 82332 : d_qmodules->initialize(
120 : 41166 : d_env, d_qstate, d_qim, d_qreg, d_treg, d_builder.get(), d_modules);
121 [ + + ]: 41166 : if (d_qmodules->d_rel_dom.get())
122 : : {
123 : 274 : d_util.push_back(d_qmodules->d_rel_dom.get());
124 : : }
125 : :
126 : : // handle any circular dependencies
127 : :
128 : : // quantifiers bound inference needs to be informed of the bounded integers
129 : : // module, which has information about which quantifiers have finite bounds
130 : 41166 : d_qreg.getQuantifiersBoundInference().finishInit(d_qmodules->d_bint.get());
131 : 41166 : }
132 : :
133 : 0 : QuantifiersRegistry& QuantifiersEngine::getQuantifiersRegistry()
134 : : {
135 : 0 : return d_qreg;
136 : : }
137 : :
138 : 41166 : QModelBuilder* QuantifiersEngine::getModelBuilder() const
139 : : {
140 : 41166 : return d_builder.get();
141 : : }
142 : :
143 : : /// !!!!!!!!!!!!!! temporary (project #15)
144 : :
145 : 7397 : TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() const
146 : : {
147 : 7397 : return d_treg.getTermDatabaseSygus();
148 : : }
149 : : /// !!!!!!!!!!!!!!
150 : :
151 : 36612 : void QuantifiersEngine::presolve() {
152 [ + - ]: 36612 : Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl;
153 : 36612 : d_numInstRoundsLemma = 0;
154 : 36612 : d_qim.clearPending();
155 [ + + ]: 256552 : for (QuantifiersUtil*& u : d_util)
156 : : {
157 : 219940 : u->presolve();
158 : : }
159 [ + + ]: 263118 : for (QuantifiersModule*& mdl : d_modules)
160 : : {
161 : 226506 : mdl->presolve();
162 : : }
163 : 36612 : }
164 : :
165 : 46644 : void QuantifiersEngine::ppNotifyAssertions(
166 : : const std::vector<Node>& assertions) {
167 [ + - ]: 93288 : Trace("quant-engine-proc")
168 : 46644 : << "ppNotifyAssertions in QE, #assertions = " << assertions.size()
169 : 46644 : << std::endl;
170 [ + + ]: 46644 : if (options().quantifiers.instMaxLevel != -1)
171 : : {
172 [ + + ]: 306 : for (const Node& a : assertions)
173 : : {
174 : 301 : QuantAttributes::setInstantiationLevelAttr(a, 0);
175 : : }
176 : : }
177 [ + + ]: 46644 : if (options().quantifiers.sygus)
178 : : {
179 : 6301 : SynthEngine* sye = d_qmodules->d_synth_e.get();
180 [ + + ]: 19126 : for (const Node& a : assertions)
181 : : {
182 : 12825 : sye->ppNotifyAssertion(a);
183 : : }
184 : : }
185 : : /* The SyGuS instantiation module needs a global view of all available
186 : : * assertions to collect global terms that get added to each grammar.
187 : : */
188 [ + + ]: 46644 : if (options().quantifiers.sygusInst)
189 : : {
190 : 128 : SygusInst* si = d_qmodules->d_sygus_inst.get();
191 : 128 : si->ppNotifyAssertions(assertions);
192 : : }
193 : 46644 : }
194 : :
195 : 194793 : void QuantifiersEngine::check( Theory::Effort e ){
196 : 194793 : QuantifiersStatistics& stats = d_qstate.getStats();
197 : 194798 : CodeTimer codeTimer(stats.d_time);
198 [ - + ][ - + ]: 194793 : Assert(d_qstate.getEqualityEngine() != nullptr);
[ - - ]
199 [ + + ]: 194793 : if (!d_qstate.getEqualityEngine()->consistent())
200 : : {
201 [ + - ]: 2 : Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl;
202 : 2 : return;
203 : : }
204 [ - + ]: 194791 : if (d_qstate.isInConflict())
205 : : {
206 [ - - ]: 0 : if (e < Theory::EFFORT_LAST_CALL)
207 : : {
208 : : // this can happen in rare cases when quantifiers is the first to realize
209 : : // there is a quantifier-free conflict, for example, when it discovers
210 : : // disequal and congruent terms in the master equality engine during
211 : : // term indexing. In such cases, quantifiers reports a "conflicting lemma"
212 : : // that is, one that is entailed to be false by the current assignment.
213 : : // If this lemma is not a SAT conflict, we may get another call to full
214 : : // effort check and the quantifier-free solvers still haven't realized
215 : : // there is a conflict. In this case, we return, trusting that theory
216 : : // combination will do the right thing (split on equalities until there is
217 : : // a conflict at the quantifier-free level).
218 [ - - ]: 0 : Trace("quant-engine-debug")
219 : 0 : << "Conflicting lemma already reported by quantifiers, return."
220 : 0 : << std::endl;
221 : 0 : return;
222 : : }
223 : : // we reported what we thought was a conflicting lemma, but now we have
224 : : // gotten a check at LAST_CALL effort, indicating that the lemma we reported
225 : : // was not conflicting. This should never happen, but in production mode, we
226 : : // proceed with the check.
227 : 0 : Assert(false);
228 : : }
229 : 194791 : bool needsCheck = d_qim.hasPendingLemma();
230 : 194791 : QuantifiersModule::QEffort needsModelE = QuantifiersModule::QEFFORT_NONE;
231 : 194796 : std::vector< QuantifiersModule* > qm;
232 [ + + ]: 194791 : if( d_model->checkNeeded() ){
233 [ + + ][ + + ]: 127961 : needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call
234 [ + + ]: 871021 : for (QuantifiersModule*& mdl : d_modules)
235 : : {
236 [ + + ]: 743060 : if (mdl->needsCheck(e))
237 : : {
238 : 150584 : qm.push_back(mdl);
239 : 150584 : needsCheck = true;
240 : : //can only request model at last call since theory combination can find inconsistencies
241 [ + + ]: 150584 : if( e>=Theory::EFFORT_LAST_CALL ){
242 : 114269 : QuantifiersModule::QEffort me = mdl->needsModel(e);
243 [ + + ]: 114269 : needsModelE = me<needsModelE ? me : needsModelE;
244 : : }
245 : : }
246 : : }
247 : : }
248 : :
249 : 194791 : d_qim.reset();
250 : 194791 : bool setModelUnsound = false;
251 : 194791 : IncompleteId setModelUnsoundId = IncompleteId::QUANTIFIERS;
252 : 194791 : if (options().quantifiers.instMaxRounds >= 0
253 [ + + ][ + + ]: 201527 : && d_numInstRoundsLemma
254 [ + + ]: 6736 : >= static_cast<uint32_t>(options().quantifiers.instMaxRounds))
255 : : {
256 : 64 : needsCheck = false;
257 : 64 : setModelUnsound = true;
258 : 64 : setModelUnsoundId = IncompleteId::QUANTIFIERS_MAX_INST_ROUNDS;
259 : : }
260 : :
261 [ + - ]: 194791 : Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl;
262 [ + + ]: 194791 : if( needsCheck ){
263 : : //flush previous lemmas (for instance, if was interrupted), or other lemmas to process
264 : 51213 : d_qim.doPending();
265 [ + + ]: 51213 : if (d_qim.hasSentLemma())
266 : : {
267 : 188 : return;
268 : : }
269 : :
270 : 51025 : double clSet = 0;
271 [ - + ]: 51025 : if( TraceIsOn("quant-engine") ){
272 : 0 : clSet = double(clock())/double(CLOCKS_PER_SEC);
273 [ - - ]: 0 : Trace("quant-engine") << ">>>>> Quantifiers Engine Round, effort = " << e << " <<<<<" << std::endl;
274 : : }
275 : :
276 [ - + ]: 51025 : if( TraceIsOn("quant-engine-debug") ){
277 [ - - ]: 0 : Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl;
278 [ - - ]: 0 : Trace("quant-engine-debug")
279 : 0 : << " depth : " << d_qstate.getInstRoundDepth() << std::endl;
280 [ - - ]: 0 : Trace("quant-engine-debug") << " modules to check : ";
281 [ - - ]: 0 : for( unsigned i=0; i<qm.size(); i++ ){
282 : 0 : Trace("quant-engine-debug") << qm[i]->identify() << " ";
283 : : }
284 [ - - ]: 0 : Trace("quant-engine-debug") << std::endl;
285 [ - - ]: 0 : Trace("quant-engine-debug") << " # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl;
286 [ - - ]: 0 : if (d_qim.hasPendingLemma())
287 : : {
288 [ - - ]: 0 : Trace("quant-engine-debug")
289 : 0 : << " lemmas waiting = " << d_qim.numPendingLemmas() << std::endl;
290 : : }
291 [ - - ]: 0 : Trace("quant-engine-debug")
292 : 0 : << " Theory engine finished : "
293 : 0 : << !d_qstate.getValuation().needCheck() << std::endl;
294 [ - - ]: 0 : Trace("quant-engine-debug") << " Needs model effort : " << needsModelE << std::endl;
295 [ - - ]: 0 : Trace("quant-engine-debug")
296 : 0 : << " In conflict : " << d_qstate.isInConflict() << std::endl;
297 : : }
298 [ - + ]: 51025 : if( TraceIsOn("quant-engine-ee-pre") ){
299 [ - - ]: 0 : Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl;
300 : 0 : d_qstate.debugPrintEqualityEngine("quant-engine-ee-pre");
301 : : }
302 [ - + ]: 51025 : if( TraceIsOn("quant-engine-assert") ){
303 [ - - ]: 0 : Trace("quant-engine-assert") << "Assertions : " << std::endl;
304 : 0 : d_te->printAssertions("quant-engine-assert");
305 : : }
306 : :
307 : : //reset utilities
308 [ + - ]: 51025 : Trace("quant-engine-debug") << "Resetting all utilities..." << std::endl;
309 [ + + ]: 360585 : for (QuantifiersUtil*& util : d_util)
310 : : {
311 [ + - ][ - + ]: 619120 : Trace("quant-engine-debug2") << "Reset " << util->identify().c_str()
[ - - ]
312 : 309560 : << "..." << std::endl;
313 [ - + ]: 309560 : if (!util->reset(e))
314 : : {
315 : 0 : d_qim.doPending();
316 [ - - ]: 0 : if (d_qim.hasSentLemma())
317 : : {
318 : 0 : return;
319 : : }else{
320 : : //should only fail reset if added a lemma
321 : 0 : Assert(false);
322 : : }
323 : : }
324 : : }
325 : :
326 [ - + ]: 51025 : if( TraceIsOn("quant-engine-ee") ){
327 [ - - ]: 0 : Trace("quant-engine-ee") << "Equality engine : " << std::endl;
328 : 0 : d_qstate.debugPrintEqualityEngine("quant-engine-ee");
329 : : }
330 : :
331 : : //reset the model
332 [ + - ]: 51025 : Trace("quant-engine-debug") << "Reset model..." << std::endl;
333 : 51025 : d_model->reset_round();
334 : :
335 : : //reset the modules
336 [ + - ]: 51025 : Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
337 [ + + ]: 346390 : for (QuantifiersModule*& mdl : d_modules)
338 : : {
339 [ + - ][ - + ]: 590730 : Trace("quant-engine-debug2") << "Reset " << mdl->identify().c_str()
[ - - ]
340 : 295365 : << std::endl;
341 : 295365 : mdl->reset_round(e);
342 : : }
343 [ + - ]: 51025 : Trace("quant-engine-debug") << "Done resetting all modules." << std::endl;
344 : : //reset may have added lemmas
345 : 51025 : d_qim.doPending();
346 [ - + ]: 51025 : if (d_qim.hasSentLemma())
347 : : {
348 : 0 : return;
349 : : }
350 : :
351 [ + + ]: 51025 : if( e==Theory::EFFORT_LAST_CALL ){
352 : 26382 : ++(stats.d_instantiation_rounds_lc);
353 [ + + ]: 24643 : }else if( e==Theory::EFFORT_FULL ){
354 : 24516 : ++(stats.d_instantiation_rounds);
355 : : }
356 [ + - ]: 51025 : Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl;
357 : 190921 : for (unsigned qef = QuantifiersModule::QEFFORT_CONFLICT;
358 [ + + ]: 190921 : qef <= QuantifiersModule::QEFFORT_LAST_CALL;
359 : : ++qef)
360 : : {
361 : 163912 : QuantifiersModule::QEffort quant_e =
362 : : static_cast<QuantifiersModule::QEffort>(qef);
363 : : // Force the theory engine to build the model if any module requested it.
364 [ + + ]: 163912 : if (needsModelE == quant_e)
365 : : {
366 [ + - ]: 23944 : Trace("quant-engine-debug") << "Build model..." << std::endl;
367 [ + + ]: 23944 : if (!d_te->buildModel())
368 : : {
369 : : // If we failed to build the model, flush all pending lemmas and
370 : : // finish.
371 : 7 : d_qim.doPending();
372 : 24011 : break;
373 : : }
374 : : }
375 [ + - ]: 163905 : if (!d_qim.hasSentLemma())
376 : : {
377 : : //check each module
378 [ + + ]: 633908 : for (QuantifiersModule*& mdl : qm)
379 : : {
380 [ + - ][ - + ]: 940082 : Trace("quant-engine-debug") << "Check " << mdl->identify().c_str()
[ - - ]
381 : 0 : << " at effort " << quant_e << "..."
382 : 470041 : << std::endl;
383 : 470041 : mdl->check(e, quant_e);
384 [ + + ]: 470037 : if (d_qstate.isInConflict())
385 : : {
386 [ + - ]: 34 : Trace("quant-engine-debug") << "...conflict!" << std::endl;
387 : 34 : break;
388 : : }
389 : : }
390 : : //flush all current lemmas
391 : 163901 : d_qim.doPending();
392 : : }
393 : : // If we have added a lemma, stop. We also stop if we are in conflict.
394 : : // In very rare cases, it may be the case that quantifiers knows there
395 : : // is a conflict without adding a lemma, e.g. if it sent a duplicate
396 : : // QUANTIFIERS_TDB_DEQ_CONG lemma, which can occur if it has detected
397 : : // a quantifier-free conflict during term indexing but the quantifier
398 : : // free theories haven't caused a backtrack yet. This should never happen
399 : : // at LAST_CALL effort.
400 [ + + ][ - + ]: 163900 : if (d_qim.hasSentLemma() || d_qstate.isInConflict())
[ + + ]
401 : : {
402 [ - + ][ - - ]: 22863 : Assert(d_qim.hasSentLemma() || e != Theory::EFFORT_LAST_CALL);
[ - + ][ - - ]
403 : 22863 : break;
404 : : }else{
405 [ + + ]: 141037 : if (quant_e == QuantifiersModule::QEFFORT_CONFLICT)
406 : : {
407 : 47025 : d_qstate.incrementInstRoundCounters(e);
408 : : }
409 [ + + ]: 94012 : else if (quant_e == QuantifiersModule::QEFFORT_MODEL)
410 : : {
411 [ + + ]: 28512 : if( e==Theory::EFFORT_LAST_CALL ){
412 : : //sources of incompleteness
413 [ + + ]: 61514 : for (QuantifiersUtil*& util : d_util)
414 : : {
415 [ + + ]: 52823 : if (!util->checkComplete(setModelUnsoundId))
416 : : {
417 [ + - ]: 2 : Trace("quant-engine-debug") << "Set incomplete because utility "
418 [ - + ][ - - ]: 1 : << util->identify().c_str()
419 : 1 : << " was incomplete." << std::endl;
420 : 1 : setModelUnsound = true;
421 : : }
422 : : }
423 [ - + ]: 8691 : if (d_qstate.isInConflict())
424 : : {
425 : : // we reported a conflicting lemma, should return
426 : 0 : setModelUnsound = true;
427 : : }
428 : : //if we have a chance not to set incomplete
429 [ + + ]: 8691 : if (!setModelUnsound)
430 : : {
431 : : //check if we should set the incomplete flag
432 [ + + ]: 58082 : for (QuantifiersModule*& mdl : d_modules)
433 : : {
434 [ + + ]: 49712 : if (!mdl->checkComplete(setModelUnsoundId))
435 : : {
436 [ + - ]: 640 : Trace("quant-engine-debug")
437 : 0 : << "Set incomplete because module "
438 [ - + ][ - - ]: 320 : << mdl->identify().c_str() << " was incomplete."
439 : 320 : << std::endl;
440 : 320 : setModelUnsound = true;
441 : 320 : break;
442 : : }
443 : : }
444 [ + + ]: 8690 : if (!setModelUnsound)
445 : : {
446 : : //look at individual quantified formulas, one module must claim completeness for each one
447 [ + + ]: 10478 : for( unsigned i=0; i<d_model->getNumAssertedQuantifiers(); i++ ){
448 : 9337 : bool hasCompleteM = false;
449 : 9337 : Node q = d_model->getAssertedQuantifier( i );
450 : 9337 : QuantifiersModule* qmd = d_qreg.getOwner(q);
451 [ + + ]: 9337 : if( qmd!=NULL ){
452 : 6891 : hasCompleteM = qmd->checkCompleteFor( q );
453 : : }else{
454 [ + + ]: 12299 : for( unsigned j=0; j<d_modules.size(); j++ ){
455 [ + + ]: 11506 : if( d_modules[j]->checkCompleteFor( q ) ){
456 : 1653 : qmd = d_modules[j];
457 : 1653 : hasCompleteM = true;
458 : 1653 : break;
459 : : }
460 : : }
461 : : }
462 [ + + ]: 9337 : if( !hasCompleteM ){
463 [ + - ]: 7229 : Trace("quant-engine-debug") << "Set incomplete because " << q << " was not fully processed." << std::endl;
464 : 7229 : setModelUnsound = true;
465 : 7229 : break;
466 : : }else{
467 [ - + ][ - + ]: 2108 : Assert(qmd != NULL);
[ - - ]
468 [ + - ][ - + ]: 2108 : Trace("quant-engine-debug2") << "Complete for " << q << " due to " << qmd->identify().c_str() << std::endl;
[ - - ]
469 : : }
470 : : }
471 : : }
472 : : }
473 : : // if setModelUnsound = false, we will answer SAT, otherwise we will
474 : : // run at quant_e QEFFORT_LAST_CALL
475 [ + + ]: 8691 : if (!setModelUnsound)
476 : : {
477 : 1141 : break;
478 : : }
479 : : }
480 : : }
481 : : }
482 : : }
483 [ + - ]: 51020 : Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
484 : : // debug print
485 [ + + ]: 51020 : if (d_qim.hasSentLemma())
486 : : {
487 : 22863 : d_qim.getInstantiate()->notifyEndRound();
488 : 22863 : d_numInstRoundsLemma++;
489 : : }
490 [ - + ]: 51020 : if( TraceIsOn("quant-engine") ){
491 : 0 : double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
492 [ - - ]: 0 : Trace("quant-engine") << "Finished quantifiers engine, total time = " << (clSet2-clSet);
493 [ - - ]: 0 : Trace("quant-engine") << ", sent lemma = " << d_qim.hasSentLemma();
494 [ - - ]: 0 : Trace("quant-engine") << std::endl;
495 : : }
496 : :
497 [ + - ]: 51020 : Trace("quant-engine-debug2") << "Finished quantifiers engine check." << std::endl;
498 : : }else{
499 [ + - ]: 143578 : Trace("quant-engine-debug2") << "Quantifiers Engine does not need check." << std::endl;
500 : : }
501 : :
502 : : //SAT case
503 [ + + ][ + + ]: 194598 : if (e == Theory::EFFORT_LAST_CALL && !d_qim.hasSentLemma())
[ + + ]
504 : : {
505 [ + + ]: 26490 : if (setModelUnsound)
506 : : {
507 [ + - ]: 7216 : Trace("quant-engine") << "Set incomplete flag." << std::endl;
508 : 7216 : d_qim.setModelUnsound(setModelUnsoundId);
509 : : }
510 : : //output debug stats
511 : 26490 : d_qim.getInstantiate()->debugPrintModel();
512 : : }
513 : 194598 : d_qim.clearPending();
514 : : }
515 : :
516 : 43647 : void QuantifiersEngine::notifyCombineTheories() {
517 : : // If allowing theory combination to happen at most once between instantiation
518 : : // rounds, this would reset d_ierCounter to 1 and d_ierCounterLastLc to -1
519 : : // in quantifiers state.
520 : 43647 : }
521 : :
522 : 179014 : bool QuantifiersEngine::reduceQuantifier(Node q)
523 : : {
524 : : // TODO: this can be unified with preregistration: AlphaEquivalence takes
525 : : // ownership of reducable quants
526 : 179014 : BoolMap::const_iterator it = d_quants_red.find(q);
527 [ + + ]: 179014 : if (it == d_quants_red.end())
528 : : {
529 : 54299 : TrustNode tlem;
530 : 54299 : InferenceId id = InferenceId::UNKNOWN;
531 [ + - ]: 54299 : if (d_qmodules->d_alpha_equiv)
532 : : {
533 [ + - ]: 108598 : Trace("quant-engine-red")
534 : 54299 : << "Alpha equivalence " << q << "?" << std::endl;
535 : : // add equivalence with another quantified formula
536 : 54299 : tlem = d_qmodules->d_alpha_equiv->reduceQuantifier(q);
537 : 54299 : id = InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ;
538 [ + + ]: 54299 : if (!tlem.isNull())
539 : : {
540 [ + - ]: 4360 : Trace("quant-engine-red")
541 : 2180 : << "...alpha equivalence success." << std::endl;
542 : 2180 : ++(d_qstate.getStats().d_red_alpha_equiv);
543 : : }
544 : : }
545 [ + + ]: 54299 : if (!tlem.isNull())
546 : : {
547 : 2180 : d_qim.trustedLemma(tlem, id);
548 : : }
549 : 54299 : d_quants_red[q] = !tlem.isNull();
550 : 54299 : return !tlem.isNull();
551 : : }
552 : 124715 : return (*it).second;
553 : : }
554 : :
555 : 144923 : void QuantifiersEngine::registerQuantifierInternal(Node f)
556 : : {
557 : 144923 : std::map< Node, bool >::iterator it = d_quants.find( f );
558 [ + + ]: 144923 : if( it==d_quants.end() ){
559 [ + - ]: 51624 : Trace("quant") << "QuantifiersEngine : Register quantifier ";
560 [ + - ]: 51624 : Trace("quant") << " : " << f << std::endl;
561 : 51624 : size_t prev_lemma_waiting = d_qim.numPendingLemmas();
562 : 51624 : ++(d_qstate.getStats().d_num_quant);
563 [ - + ][ - + ]: 51624 : Assert(f.getKind() == Kind::FORALL);
[ - - ]
564 : : // register with utilities
565 [ + + ]: 373701 : for (unsigned i = 0; i < d_util.size(); i++)
566 : : {
567 : 322077 : d_util[i]->registerQuantifier(f);
568 : : }
569 : :
570 [ + + ]: 346533 : for (QuantifiersModule*& mdl : d_modules)
571 : : {
572 [ + - ][ - + ]: 589818 : Trace("quant-debug") << "check ownership with " << mdl->identify()
[ - - ]
573 : 294909 : << "..." << std::endl;
574 : 294909 : mdl->checkOwnership(f);
575 : : }
576 : 51624 : QuantifiersModule* qm = d_qreg.getOwner(f);
577 : 103248 : Trace("quant") << " Owner : " << (qm == nullptr ? "[none]" : qm->identify())
578 : 51624 : << std::endl;
579 : : // register with each module
580 [ + + ]: 346533 : for (QuantifiersModule*& mdl : d_modules)
581 : : {
582 [ + - ][ - + ]: 589818 : Trace("quant-debug") << "register with " << mdl->identify() << "..."
[ - - ]
583 : 294909 : << std::endl;
584 : 294909 : mdl->registerQuantifier(f);
585 : : // since this is context-independent, we should not add any lemmas during
586 : : // this call
587 [ - + ][ - + ]: 294909 : Assert(d_qim.numPendingLemmas() == prev_lemma_waiting);
[ - - ]
588 : : }
589 [ + - ]: 51624 : Trace("quant-debug") << "...finish." << std::endl;
590 : 51624 : d_quants[f] = true;
591 [ - + ][ - + ]: 51624 : AlwaysAssert(d_qim.numPendingLemmas() == prev_lemma_waiting);
[ - - ]
592 : : }
593 : 144923 : }
594 : :
595 : 60697 : void QuantifiersEngine::preRegisterQuantifier(Node q)
596 : : {
597 : 60697 : NodeSet::const_iterator it = d_quants_prereg.find(q);
598 [ + + ]: 60697 : if (it != d_quants_prereg.end())
599 : : {
600 : 8578 : return;
601 : : }
602 [ + - ]: 54299 : Trace("quant-debug") << "QuantifiersEngine : Pre-register " << q << std::endl;
603 : 54299 : d_quants_prereg.insert(q);
604 : : // try to reduce
605 [ + + ]: 54299 : if (reduceQuantifier(q))
606 : : {
607 : : // if we can reduce it, nothing left to do
608 : 2180 : return;
609 : : }
610 : : // ensure that it is registered
611 : 52119 : registerQuantifierInternal(q);
612 : : // register with each module
613 [ + + ]: 350426 : for (QuantifiersModule*& mdl : d_modules)
614 : : {
615 [ + - ][ - + ]: 596614 : Trace("quant-debug") << "pre-register with " << mdl->identify() << "..."
[ - - ]
616 : 298307 : << std::endl;
617 : 298307 : mdl->preRegisterQuantifier(q);
618 : : }
619 : : // flush the lemmas
620 : 52119 : d_qim.doPending();
621 [ + - ]: 52119 : Trace("quant-debug") << "...finish pre-register " << q << "..." << std::endl;
622 : : }
623 : :
624 : 124715 : void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
625 [ + + ]: 124715 : if (reduceQuantifier(f))
626 : : {
627 : : // if we can reduce it, nothing left to do
628 : 11969 : return;
629 : : }
630 [ + + ]: 112746 : if( !pol ){
631 : : // do skolemization
632 : 19942 : TrustNode lem = d_qim.getSkolemize()->process(f);
633 [ + + ]: 19942 : if (!lem.isNull())
634 : : {
635 [ - + ]: 4867 : if (TraceIsOn("quantifiers-sk-debug"))
636 : : {
637 : 0 : Node slem = rewrite(lem.getNode());
638 [ - - ]: 0 : Trace("quantifiers-sk-debug")
639 : 0 : << "Skolemize lemma : " << slem << std::endl;
640 : : }
641 : 4867 : d_qim.trustedLemma(lem,
642 : : InferenceId::QUANTIFIERS_SKOLEMIZE,
643 : : LemmaProperty::NEEDS_JUSTIFY);
644 : : }
645 : 19942 : return;
646 : : }
647 : : // ensure the quantified formula is registered
648 : 92804 : registerQuantifierInternal(f);
649 : : // assert it to each module
650 : 92804 : d_model->assertQuantifier(f);
651 [ + + ]: 632620 : for (QuantifiersModule*& mdl : d_modules)
652 : : {
653 : 539816 : mdl->assertNode(f);
654 : : }
655 : : // add term to the registry
656 : 92804 : d_treg.addTerm(d_qreg.getInstConstantBody(f), true);
657 : : }
658 : :
659 : 1453240 : void QuantifiersEngine::eqNotifyNewClass(TNode t) { d_treg.addTerm(t); }
660 : :
661 : 0 : void QuantifiersEngine::markRelevant( Node q ) {
662 : 0 : d_model->markRelevant( q );
663 : 0 : }
664 : :
665 : 70 : void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
666 : 70 : d_qim.getInstantiate()->getInstantiationTermVectors(q, tvecs);
667 : 70 : }
668 : :
669 : 69 : void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) {
670 : 69 : d_qim.getInstantiate()->getInstantiationTermVectors(insts);
671 : 69 : }
672 : :
673 : 31 : void QuantifiersEngine::getInstantiations(Node q, std::vector<Node>& insts)
674 : : {
675 : 31 : d_qim.getInstantiate()->getInstantiations(q, insts);
676 : 31 : }
677 : :
678 : 101 : void QuantifiersEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
679 : : {
680 : 101 : d_qim.getInstantiate()->getInstantiatedQuantifiedFormulas(qs);
681 : 101 : }
682 : :
683 : 69 : void QuantifiersEngine::getSkolemTermVectors(
684 : : std::map<Node, std::vector<Node> >& sks) const
685 : : {
686 : 69 : d_qim.getSkolemize()->getSkolemTermVectors(sks);
687 : 69 : }
688 : :
689 : 0 : Node QuantifiersEngine::getNameForQuant(Node q) const
690 : : {
691 : 0 : return d_qreg.getNameForQuant(q);
692 : : }
693 : :
694 : 89 : bool QuantifiersEngine::getNameForQuant(Node q, Node& name, bool req) const
695 : : {
696 : 89 : return d_qreg.getNameForQuant(q, name, req);
697 : : }
698 : :
699 : 3000 : bool QuantifiersEngine::getSynthSolutions(
700 : : std::map<Node, std::map<Node, Node> >& sol_map)
701 : : {
702 : 3000 : return d_qmodules->d_synth_e->getSynthSolutions(sol_map);
703 : : }
704 : 508 : void QuantifiersEngine::declarePool(Node p, const std::vector<Node>& initValue)
705 : : {
706 : 508 : d_treg.declarePool(p, initValue);
707 : 508 : }
708 : :
709 : 654 : void QuantifiersEngine::declareOracleFun(Node f)
710 : : {
711 [ - + ]: 654 : if (d_qmodules->d_oracleEngine.get() == nullptr)
712 : : {
713 : 0 : warning() << "Cannot declare oracle function when oracles are disabled"
714 : 0 : << std::endl;
715 : 0 : return;
716 : : }
717 : 654 : d_qmodules->d_oracleEngine->declareOracleFun(f);
718 : : }
719 : 0 : std::vector<Node> QuantifiersEngine::getOracleFuns() const
720 : : {
721 [ - - ]: 0 : if (d_qmodules->d_oracleEngine.get() == nullptr)
722 : : {
723 : 0 : return {};
724 : : }
725 : 0 : return d_qmodules->d_oracleEngine->getOracleFuns();
726 : : }
727 : :
728 : : } // namespace theory
729 : : } // namespace cvc5::internal
|
