1 /********************* */
2 /*! \file quantifiers_engine.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Morgan Deters, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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.\endverbatim
12 ** \brief Implementation of quantifiers engine class
15 #include "theory/quantifiers_engine.h"
17 #include "options/quantifiers_options.h"
18 #include "options/uf_options.h"
19 #include "smt/smt_statistics_registry.h"
20 #include "theory/sep/theory_sep.h"
21 #include "theory/theory_engine.h"
22 #include "theory/uf/equality_engine.h"
26 using namespace CVC4::kind
;
27 using namespace CVC4::context
;
28 using namespace CVC4::theory
;
29 using namespace CVC4::theory::inst
;
31 QuantifiersEngine::QuantifiersEngine(context::Context
* c
,
32 context::UserContext
* u
,
35 d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c
, this)),
36 d_eq_inference(nullptr),
38 d_tr_trie(new inst::TriggerTrie
),
45 d_term_util(new quantifiers::TermUtil(this)),
46 d_term_canon(new expr::TermCanonize
),
47 d_term_db(new quantifiers::TermDb(c
, u
, this)),
49 d_quant_attr(new quantifiers::QuantAttributes(this)),
50 d_instantiate(new quantifiers::Instantiate(this, u
)),
51 d_skolemize(new quantifiers::Skolemize(this, u
)),
52 d_term_enum(new quantifiers::TermEnumeration
),
53 d_alpha_equiv(nullptr),
54 d_inst_engine(nullptr),
55 d_model_engine(nullptr),
61 d_lte_part_inst(nullptr),
65 d_anti_skolem(nullptr),
66 d_conflict_c(c
, false),
70 d_lemmas_produced_c(u
),
73 // d_ierCounter_lc(c),
74 // d_ierCounterLastLc(c),
78 d_presolve_cache_wq(u
),
79 d_presolve_cache_wic(u
)
82 d_util
.push_back(d_eq_query
.get());
83 // term util must come before the other utilities
84 d_util
.push_back(d_term_util
.get());
85 d_util
.push_back(d_term_db
.get());
87 if (options::ceGuidedInst()) {
88 d_sygus_tdb
.reset(new quantifiers::TermDbSygus(c
, this));
91 if( options::instPropagate() ){
92 // notice that this option is incompatible with options::qcfAllConflict()
93 d_inst_prop
.reset(new quantifiers::InstPropagator(this));
94 d_util
.push_back(d_inst_prop
.get());
95 d_instantiate
->addNotify(d_inst_prop
->getInstantiationNotify());
98 if( options::inferArithTriggerEq() ){
99 d_eq_inference
.reset(new quantifiers::EqualityInference(c
, false));
102 d_util
.push_back(d_instantiate
.get());
104 d_curr_effort_level
= QuantifiersModule::QEFFORT_NONE
;
106 d_hasAddedLemma
= false;
107 d_useModelEe
= false;
108 //don't add true lemma
109 d_lemmas_produced_c
[d_term_util
->d_true
] = true;
111 Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl
;
112 Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl
;
114 if( options::relevantTriggers() ){
115 d_quant_rel
.reset(new quantifiers::QuantRelevance
);
116 d_util
.push_back(d_quant_rel
.get());
119 if( options::quantEpr() ){
120 Assert( !options::incrementalSolving() );
121 d_qepr
.reset(new quantifiers::QuantEPR
);
125 //allow theory combination to go first, once initially
126 d_ierCounter
= options::instWhenTcFirst() ? 0 : 1;
127 d_ierCounter_c
= d_ierCounter
;
129 d_ierCounterLastLc
= 0;
130 d_inst_when_phase
= 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() );
132 bool needsBuilder
= false;
133 bool needsRelDom
= false;
134 //add quantifiers modules
135 if( options::quantConflictFind() || options::quantRewriteRules() ){
136 d_qcf
.reset(new quantifiers::QuantConflictFind(this, c
));
137 d_modules
.push_back(d_qcf
.get());
139 if( options::conjectureGen() ){
140 d_sg_gen
.reset(new quantifiers::ConjectureGenerator(this, c
));
141 d_modules
.push_back(d_sg_gen
.get());
143 if( !options::finiteModelFind() || options::fmfInstEngine() ){
144 d_inst_engine
.reset(new quantifiers::InstantiationEngine(this));
145 d_modules
.push_back(d_inst_engine
.get());
147 if( options::cbqi() ){
148 d_i_cbqi
.reset(new quantifiers::InstStrategyCegqi(this));
149 d_modules
.push_back(d_i_cbqi
.get());
150 if( options::cbqiBv() ){
151 // if doing instantiation for BV, need the inverter class
152 d_bv_invert
.reset(new quantifiers::BvInverter
);
155 if( options::ceGuidedInst() ){
156 d_synth_e
.reset(new quantifiers::SynthEngine(this, c
));
157 d_modules
.push_back(d_synth_e
.get());
158 //needsBuilder = true;
160 //finite model finding
161 if( options::finiteModelFind() ){
162 if( options::fmfBound() ){
163 d_bint
.reset(new quantifiers::BoundedIntegers(c
, this));
164 d_modules
.push_back(d_bint
.get());
166 d_model_engine
.reset(new quantifiers::ModelEngine(c
, this));
167 d_modules
.push_back(d_model_engine
.get());
168 //finite model finder has special ways of building the model
171 if( options::quantRewriteRules() ){
172 d_rr_engine
.reset(new quantifiers::RewriteEngine(c
, this));
173 d_modules
.push_back(d_rr_engine
.get());
175 if( options::ltePartialInst() ){
176 d_lte_part_inst
.reset(new quantifiers::LtePartialInst(this, c
));
177 d_modules
.push_back(d_lte_part_inst
.get());
179 if( options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE
){
180 d_qsplit
.reset(new quantifiers::QuantDSplit(this, c
));
181 d_modules
.push_back(d_qsplit
.get());
183 if( options::quantAntiSkolem() ){
184 d_anti_skolem
.reset(new quantifiers::QuantAntiSkolem(this));
185 d_modules
.push_back(d_anti_skolem
.get());
187 if( options::quantAlphaEquiv() ){
188 d_alpha_equiv
.reset(new quantifiers::AlphaEquivalence(this));
190 //full saturation : instantiate from relevant domain, then arbitrary terms
191 if( options::fullSaturateQuant() || options::fullSaturateInterleave() ){
192 d_fs
.reset(new quantifiers::InstStrategyEnum(this));
193 d_modules
.push_back(d_fs
.get());
198 d_rel_dom
.reset(new quantifiers::RelevantDomain(this));
199 d_util
.push_back(d_rel_dom
.get());
202 // if we require specialized ways of building the model
204 Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl
;
205 if (options::mbqiMode() == quantifiers::MBQI_FMC
206 || options::mbqiMode() == quantifiers::MBQI_TRUST
207 || options::fmfBound())
209 Trace("quant-engine-debug") << "...make fmc builder." << std::endl
;
210 d_model
.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
211 this, c
, "FirstOrderModelFmc"));
212 d_builder
.reset(new quantifiers::fmcheck::FullModelChecker(c
, this));
214 Trace("quant-engine-debug") << "...make default model builder." << std::endl
;
216 new quantifiers::FirstOrderModel(this, c
, "FirstOrderModel"));
217 d_builder
.reset(new quantifiers::QModelBuilder(c
, this));
220 d_model
.reset(new quantifiers::FirstOrderModel(this, c
, "FirstOrderModel"));
224 QuantifiersEngine::~QuantifiersEngine() {}
226 context::Context
* QuantifiersEngine::getSatContext()
228 return d_te
->theoryOf(THEORY_QUANTIFIERS
)->getSatContext();
231 context::UserContext
* QuantifiersEngine::getUserContext()
233 return d_te
->theoryOf(THEORY_QUANTIFIERS
)->getUserContext();
236 OutputChannel
& QuantifiersEngine::getOutputChannel()
238 return d_te
->theoryOf(THEORY_QUANTIFIERS
)->getOutputChannel();
240 /** get default valuation for the quantifiers engine */
241 Valuation
& QuantifiersEngine::getValuation()
243 return d_te
->theoryOf(THEORY_QUANTIFIERS
)->getValuation();
246 const LogicInfo
& QuantifiersEngine::getLogicInfo() const
248 return d_te
->getLogicInfo();
251 EqualityQuery
* QuantifiersEngine::getEqualityQuery() const
253 return d_eq_query
.get();
255 quantifiers::EqualityInference
* QuantifiersEngine::getEqualityInference() const
257 return d_eq_inference
.get();
259 quantifiers::RelevantDomain
* QuantifiersEngine::getRelevantDomain() const
261 return d_rel_dom
.get();
263 quantifiers::BvInverter
* QuantifiersEngine::getBvInverter() const
265 return d_bv_invert
.get();
267 quantifiers::QuantRelevance
* QuantifiersEngine::getQuantifierRelevance() const
269 return d_quant_rel
.get();
271 quantifiers::QModelBuilder
* QuantifiersEngine::getModelBuilder() const
273 return d_builder
.get();
275 quantifiers::QuantEPR
* QuantifiersEngine::getQuantEPR() const
279 quantifiers::FirstOrderModel
* QuantifiersEngine::getModel() const
281 return d_model
.get();
283 quantifiers::TermDb
* QuantifiersEngine::getTermDatabase() const
285 return d_term_db
.get();
287 quantifiers::TermDbSygus
* QuantifiersEngine::getTermDatabaseSygus() const
289 return d_sygus_tdb
.get();
291 quantifiers::TermUtil
* QuantifiersEngine::getTermUtil() const
293 return d_term_util
.get();
295 expr::TermCanonize
* QuantifiersEngine::getTermCanonize() const
297 return d_term_canon
.get();
299 quantifiers::QuantAttributes
* QuantifiersEngine::getQuantAttributes() const
301 return d_quant_attr
.get();
303 quantifiers::Instantiate
* QuantifiersEngine::getInstantiate() const
305 return d_instantiate
.get();
307 quantifiers::Skolemize
* QuantifiersEngine::getSkolemize() const
309 return d_skolemize
.get();
311 quantifiers::TermEnumeration
* QuantifiersEngine::getTermEnumeration() const
313 return d_term_enum
.get();
315 inst::TriggerTrie
* QuantifiersEngine::getTriggerDatabase() const
317 return d_tr_trie
.get();
320 quantifiers::BoundedIntegers
* QuantifiersEngine::getBoundedIntegers() const
324 quantifiers::QuantConflictFind
* QuantifiersEngine::getConflictFind() const
328 quantifiers::RewriteEngine
* QuantifiersEngine::getRewriteEngine() const
330 return d_rr_engine
.get();
332 quantifiers::SynthEngine
* QuantifiersEngine::getSynthEngine() const
334 return d_synth_e
.get();
336 quantifiers::InstStrategyEnum
* QuantifiersEngine::getInstStrategyEnum() const
340 quantifiers::InstStrategyCegqi
* QuantifiersEngine::getInstStrategyCegqi() const
342 return d_i_cbqi
.get();
345 QuantifiersModule
* QuantifiersEngine::getOwner( Node q
) {
346 std::map
< Node
, QuantifiersModule
* >::iterator it
= d_owner
.find( q
);
347 if( it
==d_owner
.end() ){
354 void QuantifiersEngine::setOwner( Node q
, QuantifiersModule
* m
, int priority
) {
355 QuantifiersModule
* mo
= getOwner( q
);
358 if( priority
<=d_owner_priority
[q
] ){
359 Trace("quant-warn") << "WARNING: setting owner of " << q
<< " to " << ( m
? m
->identify() : "null" ) << ", but already has owner " << mo
->identify() << " with higher priority!" << std::endl
;
364 d_owner_priority
[q
] = priority
;
368 bool QuantifiersEngine::hasOwnership( Node q
, QuantifiersModule
* m
) {
369 QuantifiersModule
* mo
= getOwner( q
);
370 return mo
==m
|| mo
==NULL
;
373 bool QuantifiersEngine::isFiniteBound( Node q
, Node v
) {
374 if( getBoundedIntegers() && getBoundedIntegers()->isBoundVar( q
, v
) ){
377 TypeNode tn
= v
.getType();
378 if( tn
.isSort() && options::finiteModelFind() ){
381 else if (d_term_enum
->mayComplete(tn
))
389 void QuantifiersEngine::presolve() {
390 Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl
;
391 for( unsigned i
=0; i
<d_modules
.size(); i
++ ){
392 d_modules
[i
]->presolve();
394 d_term_db
->presolve();
396 //add all terms to database
397 if( options::incrementalSolving() ){
398 Trace("quant-engine-proc") << "Add presolve cache " << d_presolve_cache
.size() << std::endl
;
399 for( unsigned i
=0; i
<d_presolve_cache
.size(); i
++ ){
400 addTermToDatabase( d_presolve_cache
[i
], d_presolve_cache_wq
[i
], d_presolve_cache_wic
[i
] );
402 Trace("quant-engine-proc") << "Done add presolve cache " << std::endl
;
406 void QuantifiersEngine::ppNotifyAssertions(
407 const std::vector
<Node
>& assertions
) {
408 Trace("quant-engine-proc")
409 << "ppNotifyAssertions in QE, #assertions = " << assertions
.size()
410 << " check epr = " << (d_qepr
!= NULL
) << std::endl
;
411 if ((options::instLevelInputOnly() && options::instMaxLevel() != -1) ||
413 for (unsigned i
= 0; i
< assertions
.size(); i
++) {
414 if (options::instLevelInputOnly() && options::instMaxLevel() != -1) {
415 quantifiers::QuantAttributes::setInstantiationLevelAttr(assertions
[i
],
418 if (d_qepr
!= NULL
) {
419 d_qepr
->registerAssertion(assertions
[i
]);
422 if (d_qepr
!= NULL
) {
423 // must handle sources of other new constants e.g. separation logic
425 sep::TheorySep
* theory_sep
=
426 static_cast<sep::TheorySep
*>(getTheoryEngine()->theoryOf(THEORY_SEP
));
427 theory_sep
->initializeBounds();
428 d_qepr
->finishInit();
433 void QuantifiersEngine::check( Theory::Effort e
){
434 CodeTimer
codeTimer(d_statistics
.d_time
);
435 d_useModelEe
= options::quantModelEe() && ( e
>=Theory::EFFORT_LAST_CALL
);
436 // if we want to use the model's equality engine, build the model now
437 if( d_useModelEe
&& !d_model
->isBuilt() ){
438 Trace("quant-engine-debug") << "Build the model." << std::endl
;
439 if (!d_te
->getModelBuilder()->buildModel(d_model
.get()))
441 //we are done if model building was unsuccessful
443 if( d_hasAddedLemma
){
444 Trace("quant-engine-debug") << "...failed." << std::endl
;
450 if( !getActiveEqualityEngine()->consistent() ){
451 Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl
;
454 if (d_conflict_c
.get())
456 if (e
< Theory::EFFORT_LAST_CALL
)
458 // this can happen in rare cases when quantifiers is the first to realize
459 // there is a quantifier-free conflict, for example, when it discovers
460 // disequal and congruent terms in the master equality engine during
461 // term indexing. In such cases, quantifiers reports a "conflicting lemma"
462 // that is, one that is entailed to be false by the current assignment.
463 // If this lemma is not a SAT conflict, we may get another call to full
464 // effort check and the quantifier-free solvers still haven't realized
465 // there is a conflict. In this case, we return, trusting that theory
466 // combination will do the right thing (split on equalities until there is
467 // a conflict at the quantifier-free level).
468 Trace("quant-engine-debug")
469 << "Conflicting lemma already reported by quantifiers, return."
473 // we reported what we thought was a conflicting lemma, but now we have
474 // gotten a check at LAST_CALL effort, indicating that the lemma we reported
475 // was not conflicting. This should never happen, but in production mode, we
476 // proceed with the check.
479 bool needsCheck
= !d_lemmas_waiting
.empty();
480 QuantifiersModule::QEffort needsModelE
= QuantifiersModule::QEFFORT_NONE
;
481 std::vector
< QuantifiersModule
* > qm
;
482 if( d_model
->checkNeeded() ){
483 needsCheck
= needsCheck
|| e
>=Theory::EFFORT_LAST_CALL
; //always need to check at or above last call
484 for (QuantifiersModule
*& mdl
: d_modules
)
486 if (mdl
->needsCheck(e
))
490 //can only request model at last call since theory combination can find inconsistencies
491 if( e
>=Theory::EFFORT_LAST_CALL
){
492 QuantifiersModule::QEffort me
= mdl
->needsModel(e
);
493 needsModelE
= me
<needsModelE
? me
: needsModelE
;
500 d_hasAddedLemma
= false;
501 bool setIncomplete
= false;
503 Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e
<< ", needsCheck=" << needsCheck
<< std::endl
;
505 //flush previous lemmas (for instance, if was interupted), or other lemmas to process
507 if( d_hasAddedLemma
){
512 if( Trace
.isOn("quant-engine") ){
513 clSet
= double(clock())/double(CLOCKS_PER_SEC
);
514 Trace("quant-engine") << ">>>>> Quantifiers Engine Round, effort = " << e
<< " <<<<<" << std::endl
;
517 if( Trace
.isOn("quant-engine-debug") ){
518 Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e
<< std::endl
;
519 Trace("quant-engine-debug") << " depth : " << d_ierCounter_c
<< std::endl
;
520 Trace("quant-engine-debug") << " modules to check : ";
521 for( unsigned i
=0; i
<qm
.size(); i
++ ){
522 Trace("quant-engine-debug") << qm
[i
]->identify() << " ";
524 Trace("quant-engine-debug") << std::endl
;
525 Trace("quant-engine-debug") << " # quantified formulas = " << d_model
->getNumAssertedQuantifiers() << std::endl
;
526 if( !d_lemmas_waiting
.empty() ){
527 Trace("quant-engine-debug") << " lemmas waiting = " << d_lemmas_waiting
.size() << std::endl
;
529 Trace("quant-engine-debug") << " Theory engine finished : " << !d_te
->needCheck() << std::endl
;
530 Trace("quant-engine-debug") << " Needs model effort : " << needsModelE
<< std::endl
;
532 if( Trace
.isOn("quant-engine-ee-pre") ){
533 Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl
;
534 debugPrintEqualityEngine( "quant-engine-ee-pre" );
536 if( Trace
.isOn("quant-engine-assert") ){
537 Trace("quant-engine-assert") << "Assertions : " << std::endl
;
538 getTheoryEngine()->printAssertions("quant-engine-assert");
542 Trace("quant-engine-debug") << "Resetting all utilities..." << std::endl
;
543 for (QuantifiersUtil
*& util
: d_util
)
545 Trace("quant-engine-debug2") << "Reset " << util
->identify().c_str()
546 << "..." << std::endl
;
550 if( d_hasAddedLemma
){
553 //should only fail reset if added a lemma
559 if( Trace
.isOn("quant-engine-ee") ){
560 Trace("quant-engine-ee") << "Equality engine : " << std::endl
;
561 debugPrintEqualityEngine( "quant-engine-ee" );
565 Trace("quant-engine-debug") << "Reset model..." << std::endl
;
566 d_model
->reset_round();
569 Trace("quant-engine-debug") << "Resetting all modules..." << std::endl
;
570 for (QuantifiersModule
*& mdl
: d_modules
)
572 Trace("quant-engine-debug2") << "Reset " << mdl
->identify().c_str()
576 Trace("quant-engine-debug") << "Done resetting all modules." << std::endl
;
577 //reset may have added lemmas
579 if( d_hasAddedLemma
){
583 if( e
==Theory::EFFORT_LAST_CALL
){
584 ++(d_statistics
.d_instantiation_rounds_lc
);
585 }else if( e
==Theory::EFFORT_FULL
){
586 ++(d_statistics
.d_instantiation_rounds
);
588 Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl
;
589 for (unsigned qef
= QuantifiersModule::QEFFORT_CONFLICT
;
590 qef
<= QuantifiersModule::QEFFORT_LAST_CALL
;
593 QuantifiersModule::QEffort quant_e
=
594 static_cast<QuantifiersModule::QEffort
>(qef
);
595 d_curr_effort_level
= quant_e
;
596 //build the model if any module requested it
597 if (needsModelE
== quant_e
)
599 if (!d_model
->isBuilt())
601 // theory engine's model builder is quantifier engine's builder if it
603 Assert(!getModelBuilder()
604 || getModelBuilder() == d_te
->getModelBuilder());
605 Trace("quant-engine-debug") << "Build model..." << std::endl
;
606 if (!d_te
->getModelBuilder()->buildModel(d_model
.get()))
611 if (!d_model
->isBuiltSuccess())
616 if( !d_hasAddedLemma
){
618 for (QuantifiersModule
*& mdl
: qm
)
620 Trace("quant-engine-debug") << "Check " << mdl
->identify().c_str()
621 << " at effort " << quant_e
<< "..."
623 mdl
->check(e
, quant_e
);
625 Trace("quant-engine-debug") << "...conflict!" << std::endl
;
629 //flush all current lemmas
632 //if we have added one, stop
633 if( d_hasAddedLemma
){
636 Assert( !d_conflict
);
637 if (quant_e
== QuantifiersModule::QEFFORT_CONFLICT
)
639 if( e
==Theory::EFFORT_FULL
){
640 //increment if a last call happened, we are not strictly enforcing interleaving, or already were in phase
641 if( d_ierCounterLastLc
!=d_ierCounter_lc
|| !options::instWhenStrictInterleave() || d_ierCounter
%d_inst_when_phase
!=0 ){
642 d_ierCounter
= d_ierCounter
+ 1;
643 d_ierCounterLastLc
= d_ierCounter_lc
;
644 d_ierCounter_c
= d_ierCounter_c
.get() + 1;
646 }else if( e
==Theory::EFFORT_LAST_CALL
){
647 d_ierCounter_lc
= d_ierCounter_lc
+ 1;
650 else if (quant_e
== QuantifiersModule::QEFFORT_MODEL
)
652 if( e
==Theory::EFFORT_LAST_CALL
){
653 //sources of incompleteness
654 for (QuantifiersUtil
*& util
: d_util
)
656 if (!util
->checkComplete())
658 Trace("quant-engine-debug") << "Set incomplete because utility "
659 << util
->identify().c_str()
660 << " was incomplete." << std::endl
;
661 setIncomplete
= true;
664 if (d_conflict_c
.get())
666 // we reported a conflicting lemma, should return
667 setIncomplete
= true;
669 //if we have a chance not to set incomplete
670 if( !setIncomplete
){
671 //check if we should set the incomplete flag
672 for (QuantifiersModule
*& mdl
: d_modules
)
674 if (!mdl
->checkComplete())
676 Trace("quant-engine-debug")
677 << "Set incomplete because module "
678 << mdl
->identify().c_str() << " was incomplete."
680 setIncomplete
= true;
684 if( !setIncomplete
){
685 //look at individual quantified formulas, one module must claim completeness for each one
686 for( unsigned i
=0; i
<d_model
->getNumAssertedQuantifiers(); i
++ ){
687 bool hasCompleteM
= false;
688 Node q
= d_model
->getAssertedQuantifier( i
);
689 QuantifiersModule
* qmd
= getOwner( q
);
691 hasCompleteM
= qmd
->checkCompleteFor( q
);
693 for( unsigned j
=0; j
<d_modules
.size(); j
++ ){
694 if( d_modules
[j
]->checkCompleteFor( q
) ){
702 Trace("quant-engine-debug") << "Set incomplete because " << q
<< " was not fully processed." << std::endl
;
703 setIncomplete
= true;
707 Trace("quant-engine-debug2") << "Complete for " << q
<< " due to " << qmd
->identify().c_str() << std::endl
;
712 //if setIncomplete = false, we will answer SAT, otherwise we will run at quant_e QEFFORT_LAST_CALL
713 if( !setIncomplete
){
720 d_curr_effort_level
= QuantifiersModule::QEFFORT_NONE
;
721 Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl
;
722 if( d_hasAddedLemma
){
723 d_instantiate
->debugPrint();
725 if( Trace
.isOn("quant-engine") ){
726 double clSet2
= double(clock())/double(CLOCKS_PER_SEC
);
727 Trace("quant-engine") << "Finished quantifiers engine, total time = " << (clSet2
-clSet
);
728 Trace("quant-engine") << ", added lemma = " << d_hasAddedLemma
;
729 Trace("quant-engine") << std::endl
;
732 Trace("quant-engine-debug2") << "Finished quantifiers engine check." << std::endl
;
734 Trace("quant-engine-debug2") << "Quantifiers Engine does not need check." << std::endl
;
738 if( e
==Theory::EFFORT_LAST_CALL
&& !d_hasAddedLemma
){
740 Trace("quant-engine") << "Set incomplete flag." << std::endl
;
741 getOutputChannel().setIncomplete();
744 d_instantiate
->debugPrintModel();
748 void QuantifiersEngine::notifyCombineTheories() {
749 //if allowing theory combination to happen at most once between instantiation rounds
751 //d_ierCounterLastLc = -1;
754 bool QuantifiersEngine::reduceQuantifier( Node q
) {
755 //TODO: this can be unified with preregistration: AlphaEquivalence takes ownership of reducable quants
756 BoolMap::const_iterator it
= d_quants_red
.find( q
);
757 if( it
==d_quants_red
.end() ){
759 std::map
< Node
, Node
>::iterator itr
= d_quants_red_lem
.find( q
);
760 if( itr
==d_quants_red_lem
.end() ){
762 Trace("quant-engine-red") << "Alpha equivalence " << q
<< "?" << std::endl
;
763 //add equivalence with another quantified formula
764 lem
= d_alpha_equiv
->reduceQuantifier( q
);
766 Trace("quant-engine-red") << "...alpha equivalence success." << std::endl
;
767 ++(d_statistics
.d_red_alpha_equiv
);
770 d_quants_red_lem
[q
] = lem
;
775 getOutputChannel().lemma( lem
);
777 d_quants_red
[q
] = !lem
.isNull();
778 return !lem
.isNull();
784 void QuantifiersEngine::registerQuantifierInternal(Node f
)
786 std::map
< Node
, bool >::iterator it
= d_quants
.find( f
);
787 if( it
==d_quants
.end() ){
788 Trace("quant") << "QuantifiersEngine : Register quantifier ";
789 Trace("quant") << " : " << f
<< std::endl
;
790 unsigned prev_lemma_waiting
= d_lemmas_waiting
.size();
791 ++(d_statistics
.d_num_quant
);
792 Assert( f
.getKind()==FORALL
);
793 // register with utilities
794 for (unsigned i
= 0; i
< d_util
.size(); i
++)
796 d_util
[i
]->registerQuantifier(f
);
798 // compute attributes
799 d_quant_attr
->computeAttributes(f
);
801 for (QuantifiersModule
*& mdl
: d_modules
)
803 Trace("quant-debug") << "check ownership with " << mdl
->identify()
804 << "..." << std::endl
;
805 mdl
->checkOwnership(f
);
807 QuantifiersModule
* qm
= getOwner(f
);
808 Trace("quant") << " Owner : " << (qm
== nullptr ? "[none]" : qm
->identify())
810 // register with each module
811 for (QuantifiersModule
*& mdl
: d_modules
)
813 Trace("quant-debug") << "register with " << mdl
->identify() << "..."
815 mdl
->registerQuantifier(f
);
816 // since this is context-independent, we should not add any lemmas during
818 Assert(d_lemmas_waiting
.size() == prev_lemma_waiting
);
820 Trace("quant-debug") << "...finish." << std::endl
;
822 AlwaysAssert(d_lemmas_waiting
.size() == prev_lemma_waiting
);
826 void QuantifiersEngine::preRegisterQuantifier(Node q
)
828 NodeSet::const_iterator it
= d_quants_prereg
.find(q
);
829 if (it
!= d_quants_prereg
.end())
833 Trace("quant-debug") << "QuantifiersEngine : Pre-register " << q
<< std::endl
;
834 d_quants_prereg
.insert(q
);
836 if (reduceQuantifier(q
))
838 // if we can reduce it, nothing left to do
841 // ensure that it is registered
842 registerQuantifierInternal(q
);
843 // register with each module
844 for (QuantifiersModule
*& mdl
: d_modules
)
846 Trace("quant-debug") << "pre-register with " << mdl
->identify() << "..."
848 mdl
->preRegisterQuantifier(q
);
852 Trace("quant-debug") << "...finish pre-register " << q
<< "..." << std::endl
;
855 void QuantifiersEngine::registerPattern( std::vector
<Node
> & pattern
) {
856 for(std::vector
<Node
>::iterator p
= pattern
.begin(); p
!= pattern
.end(); ++p
){
857 std::set
< Node
> added
;
858 getTermDatabase()->addTerm( *p
, added
);
862 void QuantifiersEngine::assertQuantifier( Node f
, bool pol
){
863 if (reduceQuantifier(f
))
865 // if we can reduce it, nothing left to do
870 Node lem
= d_skolemize
->process(f
);
873 if (Trace
.isOn("quantifiers-sk-debug"))
875 Node slem
= Rewriter::rewrite(lem
);
876 Trace("quantifiers-sk-debug")
877 << "Skolemize lemma : " << slem
<< std::endl
;
879 getOutputChannel().lemma(lem
, false, true);
883 // ensure the quantified formula is registered
884 registerQuantifierInternal(f
);
885 // assert it to each module
886 d_model
->assertQuantifier(f
);
887 for (QuantifiersModule
*& mdl
: d_modules
)
891 addTermToDatabase(d_term_util
->getInstConstantBody(f
), true);
894 void QuantifiersEngine::addTermToDatabase( Node n
, bool withinQuant
, bool withinInstClosure
){
895 if( options::incrementalSolving() ){
896 if( d_presolve_in
.find( n
)==d_presolve_in
.end() ){
897 d_presolve_in
.insert( n
);
898 d_presolve_cache
.push_back( n
);
899 d_presolve_cache_wq
.push_back( withinQuant
);
900 d_presolve_cache_wic
.push_back( withinInstClosure
);
903 //only wait if we are doing incremental solving
904 if( !d_presolve
|| !options::incrementalSolving() ){
905 std::set
< Node
> added
;
906 d_term_db
->addTerm(n
, added
, withinQuant
, withinInstClosure
);
912 d_sygus_tdb
->getEvalUnfold()->registerEvalTerm(n
);
918 void QuantifiersEngine::eqNotifyNewClass(TNode t
) {
919 addTermToDatabase( t
);
920 if( d_eq_inference
){
921 d_eq_inference
->eqNotifyNewClass( t
);
925 void QuantifiersEngine::eqNotifyPreMerge(TNode t1
, TNode t2
) {
926 if( d_eq_inference
){
927 d_eq_inference
->eqNotifyMerge( t1
, t2
);
931 void QuantifiersEngine::eqNotifyPostMerge(TNode t1
, TNode t2
) {
935 void QuantifiersEngine::eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
) {
937 // d_qcf->assertDisequal( t1, t2 );
941 bool QuantifiersEngine::addLemma( Node lem
, bool doCache
, bool doRewrite
){
944 lem
= Rewriter::rewrite(lem
);
946 Trace("inst-add-debug") << "Adding lemma : " << lem
<< std::endl
;
947 BoolMap::const_iterator itp
= d_lemmas_produced_c
.find( lem
);
948 if( itp
==d_lemmas_produced_c
.end() || !(*itp
).second
){
949 //d_curr_out->lemma( lem, false, true );
950 d_lemmas_produced_c
[ lem
] = true;
951 d_lemmas_waiting
.push_back( lem
);
952 Trace("inst-add-debug") << "Added lemma" << std::endl
;
955 Trace("inst-add-debug") << "Duplicate." << std::endl
;
959 //do not need to rewrite, will be rewritten after sending
960 d_lemmas_waiting
.push_back( lem
);
965 bool QuantifiersEngine::removeLemma( Node lem
) {
966 std::vector
< Node
>::iterator it
= std::find( d_lemmas_waiting
.begin(), d_lemmas_waiting
.end(), lem
);
967 if( it
!=d_lemmas_waiting
.end() ){
968 d_lemmas_waiting
.erase( it
, it
+ 1 );
969 d_lemmas_produced_c
[ lem
] = false;
976 void QuantifiersEngine::addRequirePhase( Node lit
, bool req
){
977 d_phase_req_waiting
[lit
] = req
;
980 bool QuantifiersEngine::addEPRAxiom( TypeNode tn
) {
982 Assert( !options::incrementalSolving() );
983 if( d_qepr
->isEPR( tn
) && !d_qepr
->hasEPRAxiom( tn
) ){
984 Node lem
= d_qepr
->mkEPRAxiom( tn
);
985 Trace("quant-epr") << "EPR lemma for " << tn
<< " : " << lem
<< std::endl
;
986 getOutputChannel().lemma( lem
);
992 void QuantifiersEngine::markRelevant( Node q
) {
993 d_model
->markRelevant( q
);
996 void QuantifiersEngine::setConflict() {
1001 bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e
) {
1002 Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter
<< ", " << d_ierCounter_lc
<< std::endl
;
1003 //determine if we should perform check, based on instWhenMode
1004 bool performCheck
= false;
1005 if( options::instWhenMode()==quantifiers::INST_WHEN_FULL
){
1006 performCheck
= ( e
>= Theory::EFFORT_FULL
);
1007 }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY
){
1008 performCheck
= ( e
>= Theory::EFFORT_FULL
) && !getTheoryEngine()->needCheck();
1009 }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_LAST_CALL
){
1010 performCheck
= ( ( e
==Theory::EFFORT_FULL
&& d_ierCounter
%d_inst_when_phase
!=0 ) || e
==Theory::EFFORT_LAST_CALL
);
1011 }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY_LAST_CALL
){
1012 performCheck
= ( ( e
==Theory::EFFORT_FULL
&& !getTheoryEngine()->needCheck() && d_ierCounter
%d_inst_when_phase
!=0 ) || e
==Theory::EFFORT_LAST_CALL
);
1013 }else if( options::instWhenMode()==quantifiers::INST_WHEN_LAST_CALL
){
1014 performCheck
= ( e
>= Theory::EFFORT_LAST_CALL
);
1016 performCheck
= true;
1018 if( e
==Theory::EFFORT_LAST_CALL
){
1019 //with bounded integers, skip every other last call,
1020 // since matching loops may occur with infinite quantification
1021 if( d_ierCounter_lc
%2==0 && options::fmfBound() ){
1022 performCheck
= false;
1025 return performCheck
;
1028 quantifiers::UserPatMode
QuantifiersEngine::getInstUserPatMode() {
1029 if( options::userPatternsQuant()==quantifiers::USER_PAT_MODE_INTERLEAVE
){
1030 return d_ierCounter
%2==0 ? quantifiers::USER_PAT_MODE_USE
: quantifiers::USER_PAT_MODE_RESORT
;
1032 return options::userPatternsQuant();
1036 void QuantifiersEngine::flushLemmas(){
1037 if( !d_lemmas_waiting
.empty() ){
1038 //filter based on notify classes
1039 if (d_instantiate
->hasNotify())
1041 unsigned prev_lem_sz
= d_lemmas_waiting
.size();
1042 d_instantiate
->notifyFlushLemmas();
1043 if( prev_lem_sz
!=d_lemmas_waiting
.size() ){
1044 Trace("quant-engine") << "...filtered instances : " << d_lemmas_waiting
.size() << " / " << prev_lem_sz
<< std::endl
;
1047 //take default output channel if none is provided
1048 d_hasAddedLemma
= true;
1049 for( unsigned i
=0; i
<d_lemmas_waiting
.size(); i
++ ){
1050 Trace("qe-lemma") << "Lemma : " << d_lemmas_waiting
[i
] << std::endl
;
1051 getOutputChannel().lemma( d_lemmas_waiting
[i
], false, true );
1053 d_lemmas_waiting
.clear();
1055 if( !d_phase_req_waiting
.empty() ){
1056 for( std::map
< Node
, bool >::iterator it
= d_phase_req_waiting
.begin(); it
!= d_phase_req_waiting
.end(); ++it
){
1057 Trace("qe-lemma") << "Require phase : " << it
->first
<< " -> " << it
->second
<< std::endl
;
1058 getOutputChannel().requirePhase( it
->first
, it
->second
);
1060 d_phase_req_waiting
.clear();
1064 bool QuantifiersEngine::getUnsatCoreLemmas( std::vector
< Node
>& active_lemmas
) {
1065 return d_instantiate
->getUnsatCoreLemmas(active_lemmas
);
1068 bool QuantifiersEngine::getUnsatCoreLemmas( std::vector
< Node
>& active_lemmas
, std::map
< Node
, Node
>& weak_imp
) {
1069 return d_instantiate
->getUnsatCoreLemmas(active_lemmas
, weak_imp
);
1072 void QuantifiersEngine::getInstantiationTermVectors( Node q
, std::vector
< std::vector
< Node
> >& tvecs
) {
1073 d_instantiate
->getInstantiationTermVectors(q
, tvecs
);
1076 void QuantifiersEngine::getInstantiationTermVectors( std::map
< Node
, std::vector
< std::vector
< Node
> > >& insts
) {
1077 d_instantiate
->getInstantiationTermVectors(insts
);
1080 void QuantifiersEngine::getExplanationForInstLemmas(
1081 const std::vector
<Node
>& lems
,
1082 std::map
<Node
, Node
>& quant
,
1083 std::map
<Node
, std::vector
<Node
> >& tvec
)
1085 d_instantiate
->getExplanationForInstLemmas(lems
, quant
, tvec
);
1088 void QuantifiersEngine::printInstantiations( std::ostream
& out
) {
1089 bool printed
= false;
1090 // print the skolemizations
1091 if (d_skolemize
->printSkolemization(out
))
1095 // print the instantiations
1096 if (d_instantiate
->printInstantiations(out
))
1101 out
<< "No instantiations" << std::endl
;
1105 void QuantifiersEngine::printSynthSolution( std::ostream
& out
) {
1108 d_synth_e
->printSynthSolution(out
);
1110 out
<< "Internal error : module for synth solution not found." << std::endl
;
1114 void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector
< Node
>& qs
) {
1115 d_instantiate
->getInstantiatedQuantifiedFormulas(qs
);
1118 void QuantifiersEngine::getInstantiations( std::map
< Node
, std::vector
< Node
> >& insts
) {
1119 d_instantiate
->getInstantiations(insts
);
1122 void QuantifiersEngine::getInstantiations( Node q
, std::vector
< Node
>& insts
) {
1123 d_instantiate
->getInstantiations(q
, insts
);
1126 Node
QuantifiersEngine::getInstantiatedConjunction( Node q
) {
1127 return d_instantiate
->getInstantiatedConjunction(q
);
1130 QuantifiersEngine::Statistics::Statistics()
1131 : d_time("theory::QuantifiersEngine::time"),
1132 d_qcf_time("theory::QuantifiersEngine::time_qcf"),
1133 d_ematching_time("theory::QuantifiersEngine::time_ematching"),
1134 d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
1135 d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
1136 d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
1137 d_triggers("QuantifiersEngine::Triggers", 0),
1138 d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
1139 d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
1140 d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0),
1141 d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0),
1142 d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0),
1143 d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0),
1144 d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0),
1145 d_instantiations_qcf("QuantifiersEngine::Instantiations_Qcf_Conflict", 0),
1146 d_instantiations_qcf_prop("QuantifiersEngine::Instantiations_Qcf_Prop", 0),
1147 d_instantiations_fmf_exh("QuantifiersEngine::Instantiations_Fmf_Exh", 0),
1148 d_instantiations_fmf_mbqi("QuantifiersEngine::Instantiations_Fmf_Mbqi", 0),
1149 d_instantiations_cbqi("QuantifiersEngine::Instantiations_Cbqi", 0),
1150 d_instantiations_rr("QuantifiersEngine::Instantiations_Rewrite_Rules", 0)
1152 smtStatisticsRegistry()->registerStat(&d_time
);
1153 smtStatisticsRegistry()->registerStat(&d_qcf_time
);
1154 smtStatisticsRegistry()->registerStat(&d_ematching_time
);
1155 smtStatisticsRegistry()->registerStat(&d_num_quant
);
1156 smtStatisticsRegistry()->registerStat(&d_instantiation_rounds
);
1157 smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc
);
1158 smtStatisticsRegistry()->registerStat(&d_triggers
);
1159 smtStatisticsRegistry()->registerStat(&d_simple_triggers
);
1160 smtStatisticsRegistry()->registerStat(&d_multi_triggers
);
1161 smtStatisticsRegistry()->registerStat(&d_multi_trigger_instantiations
);
1162 smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv
);
1163 smtStatisticsRegistry()->registerStat(&d_instantiations_user_patterns
);
1164 smtStatisticsRegistry()->registerStat(&d_instantiations_auto_gen
);
1165 smtStatisticsRegistry()->registerStat(&d_instantiations_guess
);
1166 smtStatisticsRegistry()->registerStat(&d_instantiations_qcf
);
1167 smtStatisticsRegistry()->registerStat(&d_instantiations_qcf_prop
);
1168 smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_exh
);
1169 smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_mbqi
);
1170 smtStatisticsRegistry()->registerStat(&d_instantiations_cbqi
);
1171 smtStatisticsRegistry()->registerStat(&d_instantiations_rr
);
1174 QuantifiersEngine::Statistics::~Statistics(){
1175 smtStatisticsRegistry()->unregisterStat(&d_time
);
1176 smtStatisticsRegistry()->unregisterStat(&d_qcf_time
);
1177 smtStatisticsRegistry()->unregisterStat(&d_ematching_time
);
1178 smtStatisticsRegistry()->unregisterStat(&d_num_quant
);
1179 smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds
);
1180 smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc
);
1181 smtStatisticsRegistry()->unregisterStat(&d_triggers
);
1182 smtStatisticsRegistry()->unregisterStat(&d_simple_triggers
);
1183 smtStatisticsRegistry()->unregisterStat(&d_multi_triggers
);
1184 smtStatisticsRegistry()->unregisterStat(&d_multi_trigger_instantiations
);
1185 smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv
);
1186 smtStatisticsRegistry()->unregisterStat(&d_instantiations_user_patterns
);
1187 smtStatisticsRegistry()->unregisterStat(&d_instantiations_auto_gen
);
1188 smtStatisticsRegistry()->unregisterStat(&d_instantiations_guess
);
1189 smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf
);
1190 smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf_prop
);
1191 smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_exh
);
1192 smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_mbqi
);
1193 smtStatisticsRegistry()->unregisterStat(&d_instantiations_cbqi
);
1194 smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr
);
1197 eq::EqualityEngine
* QuantifiersEngine::getMasterEqualityEngine(){
1198 return d_te
->getMasterEqualityEngine();
1201 eq::EqualityEngine
* QuantifiersEngine::getActiveEqualityEngine() {
1203 return d_model
->getEqualityEngine();
1205 return d_te
->getMasterEqualityEngine();
1209 Node
QuantifiersEngine::getInternalRepresentative( Node a
, Node q
, int index
){
1210 bool prevModelEe
= d_useModelEe
;
1211 d_useModelEe
= false;
1212 Node ret
= d_eq_query
->getInternalRepresentative( a
, q
, index
);
1213 d_useModelEe
= prevModelEe
;
1217 void QuantifiersEngine::getSynthSolutions(std::map
<Node
, Node
>& sol_map
)
1219 d_synth_e
->getSynthSolutions(sol_map
);
1222 void QuantifiersEngine::debugPrintEqualityEngine( const char * c
) {
1223 eq::EqualityEngine
* ee
= getActiveEqualityEngine();
1224 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( ee
);
1225 std::map
< TypeNode
, int > typ_num
;
1226 while( !eqcs_i
.isFinished() ){
1227 TNode r
= (*eqcs_i
);
1228 TypeNode tr
= r
.getType();
1229 if( typ_num
.find( tr
)==typ_num
.end() ){
1233 bool firstTime
= true;
1234 Trace(c
) << " " << r
;
1235 Trace(c
) << " : { ";
1236 eq::EqClassIterator eqc_i
= eq::EqClassIterator( r
, ee
);
1237 while( !eqc_i
.isFinished() ){
1241 Trace(c
) << std::endl
;
1244 Trace(c
) << " " << n
<< std::endl
;
1248 if( !firstTime
){ Trace(c
) << " "; }
1249 Trace(c
) << "}" << std::endl
;
1252 Trace(c
) << std::endl
;
1253 for( std::map
< TypeNode
, int >::iterator it
= typ_num
.begin(); it
!= typ_num
.end(); ++it
){
1254 Trace(c
) << "# eqc for " << it
->first
<< " : " << it
->second
<< std::endl
;