1 /********************* */
2 /*! \file quantifiers_engine.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Tim King, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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/arrays/theory_arrays.h"
21 #include "theory/datatypes/theory_datatypes.h"
22 #include "theory/quantifiers/alpha_equivalence.h"
23 #include "theory/quantifiers/anti_skolem.h"
24 #include "theory/quantifiers/cegqi/ceg_t_instantiator.h"
25 #include "theory/quantifiers/cegqi/inst_strategy_cbqi.h"
26 #include "theory/quantifiers/conjecture_generator.h"
27 #include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
28 #include "theory/quantifiers/ematching/instantiation_engine.h"
29 #include "theory/quantifiers/ematching/trigger.h"
30 #include "theory/quantifiers/equality_infer.h"
31 #include "theory/quantifiers/equality_query.h"
32 #include "theory/quantifiers/first_order_model.h"
33 #include "theory/quantifiers/fmf/ambqi_builder.h"
34 #include "theory/quantifiers/fmf/bounded_integers.h"
35 #include "theory/quantifiers/fmf/full_model_check.h"
36 #include "theory/quantifiers/fmf/model_engine.h"
37 #include "theory/quantifiers/inst_propagator.h"
38 #include "theory/quantifiers/inst_strategy_enumerative.h"
39 #include "theory/quantifiers/instantiate.h"
40 #include "theory/quantifiers/local_theory_ext.h"
41 #include "theory/quantifiers/quant_conflict_find.h"
42 #include "theory/quantifiers/quant_epr.h"
43 #include "theory/quantifiers/quant_relevance.h"
44 #include "theory/quantifiers/quant_split.h"
45 #include "theory/quantifiers/quantifiers_attributes.h"
46 #include "theory/quantifiers/quantifiers_rewriter.h"
47 #include "theory/quantifiers/relevant_domain.h"
48 #include "theory/quantifiers/rewrite_engine.h"
49 #include "theory/quantifiers/skolemize.h"
50 #include "theory/quantifiers/sygus/ce_guided_instantiation.h"
51 #include "theory/quantifiers/sygus/sygus_eval_unfold.h"
52 #include "theory/quantifiers/sygus/term_database_sygus.h"
53 #include "theory/quantifiers/term_database.h"
54 #include "theory/quantifiers/term_enumeration.h"
55 #include "theory/quantifiers/term_util.h"
56 #include "theory/sep/theory_sep.h"
57 #include "theory/theory_engine.h"
58 #include "theory/uf/equality_engine.h"
59 #include "theory/uf/theory_uf.h"
60 #include "theory/uf/theory_uf_strong_solver.h"
64 using namespace CVC4::kind
;
65 using namespace CVC4::context
;
66 using namespace CVC4::theory
;
67 using namespace CVC4::theory::inst
;
69 QuantifiersEngine::QuantifiersEngine(context::Context
* c
,
70 context::UserContext
* u
,
73 d_quant_attr(new quantifiers::QuantAttributes(this)),
74 d_instantiate(new quantifiers::Instantiate(this, u
)),
75 d_skolemize(new quantifiers::Skolemize(this, u
)),
76 d_term_enum(new quantifiers::TermEnumeration
),
77 d_conflict_c(c
, false),
81 d_lemmas_produced_c(u
),
84 // d_ierCounter_lc(c),
85 // d_ierCounterLastLc(c),
89 d_presolve_cache_wq(u
),
90 d_presolve_cache_wic(u
)
93 d_eq_query
= new quantifiers::EqualityQueryQuantifiersEngine( c
, this );
94 d_util
.push_back( d_eq_query
);
96 // term util must come first
97 d_term_util
= new quantifiers::TermUtil(this);
98 d_util
.push_back(d_term_util
);
100 d_term_db
= new quantifiers::TermDb( c
, u
, this );
101 d_util
.push_back( d_term_db
);
103 if (options::ceGuidedInst()) {
104 d_sygus_tdb
= new quantifiers::TermDbSygus(c
, this);
109 if( options::instPropagate() ){
110 // notice that this option is incompatible with options::qcfAllConflict()
111 d_inst_prop
= new quantifiers::InstPropagator( this );
112 d_util
.push_back( d_inst_prop
);
113 d_instantiate
->addNotify(d_inst_prop
->getInstantiationNotify());
118 if( options::inferArithTriggerEq() ){
119 d_eq_inference
= new quantifiers::EqualityInference( c
, options::inferArithTriggerEqExp() );
121 d_eq_inference
= NULL
;
124 d_util
.push_back(d_instantiate
.get());
126 d_tr_trie
= new inst::TriggerTrie
;
127 d_curr_effort_level
= QuantifiersModule::QEFFORT_NONE
;
129 d_hasAddedLemma
= false;
130 d_useModelEe
= false;
131 //don't add true lemma
132 d_lemmas_produced_c
[d_term_util
->d_true
] = true;
134 Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl
;
135 Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl
;
137 if( options::relevantTriggers() ){
138 d_quant_rel
= new quantifiers::QuantRelevance(false);
139 d_util
.push_back(d_quant_rel
);
144 if( options::quantEpr() ){
145 Assert( !options::incrementalSolving() );
146 d_qepr
= new quantifiers::QuantEPR
;
154 d_inst_engine
= NULL
;
157 d_anti_skolem
= NULL
;
159 d_model_engine
= NULL
;
163 d_lte_part_inst
= NULL
;
164 d_alpha_equiv
= NULL
;
170 //allow theory combination to go first, once initially
171 d_ierCounter
= options::instWhenTcFirst() ? 0 : 1;
172 d_ierCounter_c
= d_ierCounter
;
174 d_ierCounterLastLc
= 0;
175 d_inst_when_phase
= 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() );
177 bool needsBuilder
= false;
178 bool needsRelDom
= false;
179 //add quantifiers modules
180 if( options::quantConflictFind() || options::quantRewriteRules() ){
181 d_qcf
= new quantifiers::QuantConflictFind( this, c
);
182 d_modules
.push_back( d_qcf
);
184 if( options::conjectureGen() ){
185 d_sg_gen
= new quantifiers::ConjectureGenerator( this, c
);
186 d_modules
.push_back( d_sg_gen
);
188 if( !options::finiteModelFind() || options::fmfInstEngine() ){
189 d_inst_engine
= new quantifiers::InstantiationEngine( this );
190 d_modules
.push_back( d_inst_engine
);
192 if( options::cbqi() ){
193 d_i_cbqi
= new quantifiers::InstStrategyCegqi( this );
194 d_modules
.push_back( d_i_cbqi
);
195 if( options::cbqiBv() ){
196 // if doing instantiation for BV, need the inverter class
197 d_bv_invert
= new quantifiers::BvInverter
;
200 if( options::ceGuidedInst() ){
201 d_ceg_inst
= new quantifiers::CegInstantiation( this, c
);
202 d_modules
.push_back( d_ceg_inst
);
203 //needsBuilder = true;
205 //finite model finding
206 if( options::finiteModelFind() ){
207 if( options::fmfBound() ){
208 d_bint
= new quantifiers::BoundedIntegers( c
, this );
209 d_modules
.push_back( d_bint
);
211 d_model_engine
= new quantifiers::ModelEngine( c
, this );
212 d_modules
.push_back( d_model_engine
);
213 //finite model finder has special ways of building the model
216 if( options::quantRewriteRules() ){
217 d_rr_engine
= new quantifiers::RewriteEngine( c
, this );
218 d_modules
.push_back(d_rr_engine
);
220 if( options::ltePartialInst() ){
221 d_lte_part_inst
= new quantifiers::LtePartialInst( this, c
);
222 d_modules
.push_back( d_lte_part_inst
);
224 if( options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE
){
225 d_qsplit
= new quantifiers::QuantDSplit( this, c
);
226 d_modules
.push_back( d_qsplit
);
228 if( options::quantAntiSkolem() ){
229 d_anti_skolem
= new quantifiers::QuantAntiSkolem( this );
230 d_modules
.push_back( d_anti_skolem
);
232 if( options::quantAlphaEquiv() ){
233 d_alpha_equiv
= new quantifiers::AlphaEquivalence( this );
235 //full saturation : instantiate from relevant domain, then arbitrary terms
236 if( options::fullSaturateQuant() || options::fullSaturateInterleave() ){
237 d_fs
= new quantifiers::InstStrategyEnum(this);
238 d_modules
.push_back( d_fs
);
243 d_rel_dom
= new quantifiers::RelevantDomain( this );
244 d_util
.push_back( d_rel_dom
);
247 // if we require specialized ways of building the model
249 Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl
;
250 if( options::mbqiMode()==quantifiers::MBQI_FMC
|| options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL
||
251 options::mbqiMode()==quantifiers::MBQI_TRUST
|| options::fmfBound() ){
252 Trace("quant-engine-debug") << "...make fmc builder." << std::endl
;
253 d_model
= new quantifiers::fmcheck::FirstOrderModelFmc( this, c
, "FirstOrderModelFmc" );
254 d_builder
= new quantifiers::fmcheck::FullModelChecker( c
, this );
255 }else if( options::mbqiMode()==quantifiers::MBQI_ABS
){
256 Trace("quant-engine-debug") << "...make abs mbqi builder." << std::endl
;
257 d_model
= new quantifiers::FirstOrderModelAbs( this, c
, "FirstOrderModelAbs" );
258 d_builder
= new quantifiers::AbsMbqiBuilder( c
, this );
260 Trace("quant-engine-debug") << "...make default model builder." << std::endl
;
261 d_model
= new quantifiers::FirstOrderModelIG( this, c
, "FirstOrderModelIG" );
262 d_builder
= new quantifiers::QModelBuilderDefault( c
, this );
265 d_model
= new quantifiers::FirstOrderModelIG( this, c
, "FirstOrderModelIG" );
269 QuantifiersEngine::~QuantifiersEngine()
271 delete d_alpha_equiv
;
276 delete d_model_engine
;
277 delete d_inst_engine
;
287 delete d_eq_inference
;
291 delete d_lte_part_inst
;
295 delete d_anti_skolem
;
299 EqualityQuery
* QuantifiersEngine::getEqualityQuery() { return d_eq_query
; }
301 context::Context
* QuantifiersEngine::getSatContext()
303 return d_te
->theoryOf(THEORY_QUANTIFIERS
)->getSatContext();
306 context::UserContext
* QuantifiersEngine::getUserContext()
308 return d_te
->theoryOf(THEORY_QUANTIFIERS
)->getUserContext();
311 OutputChannel
& QuantifiersEngine::getOutputChannel()
313 return d_te
->theoryOf(THEORY_QUANTIFIERS
)->getOutputChannel();
315 /** get default valuation for the quantifiers engine */
316 Valuation
& QuantifiersEngine::getValuation()
318 return d_te
->theoryOf(THEORY_QUANTIFIERS
)->getValuation();
321 const LogicInfo
& QuantifiersEngine::getLogicInfo() const
323 return d_te
->getLogicInfo();
326 QuantifiersModule
* QuantifiersEngine::getOwner( Node q
) {
327 std::map
< Node
, QuantifiersModule
* >::iterator it
= d_owner
.find( q
);
328 if( it
==d_owner
.end() ){
335 void QuantifiersEngine::setOwner( Node q
, QuantifiersModule
* m
, int priority
) {
336 QuantifiersModule
* mo
= getOwner( q
);
339 if( priority
<=d_owner_priority
[q
] ){
340 Trace("quant-warn") << "WARNING: setting owner of " << q
<< " to " << ( m
? m
->identify() : "null" ) << ", but already has owner " << mo
->identify() << " with higher priority!" << std::endl
;
345 d_owner_priority
[q
] = priority
;
349 bool QuantifiersEngine::hasOwnership( Node q
, QuantifiersModule
* m
) {
350 QuantifiersModule
* mo
= getOwner( q
);
351 return mo
==m
|| mo
==NULL
;
354 bool QuantifiersEngine::isFiniteBound( Node q
, Node v
) {
355 if( getBoundedIntegers() && getBoundedIntegers()->isBoundVar( q
, v
) ){
358 TypeNode tn
= v
.getType();
359 if( tn
.isSort() && options::finiteModelFind() ){
362 else if (d_term_enum
->mayComplete(tn
))
370 void QuantifiersEngine::presolve() {
371 Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl
;
372 for( unsigned i
=0; i
<d_modules
.size(); i
++ ){
373 d_modules
[i
]->presolve();
375 d_term_db
->presolve();
377 //add all terms to database
378 if( options::incrementalSolving() ){
379 Trace("quant-engine-proc") << "Add presolve cache " << d_presolve_cache
.size() << std::endl
;
380 for( unsigned i
=0; i
<d_presolve_cache
.size(); i
++ ){
381 addTermToDatabase( d_presolve_cache
[i
], d_presolve_cache_wq
[i
], d_presolve_cache_wic
[i
] );
383 Trace("quant-engine-proc") << "Done add presolve cache " << std::endl
;
387 void QuantifiersEngine::ppNotifyAssertions(
388 const std::vector
<Node
>& assertions
) {
389 Trace("quant-engine-proc")
390 << "ppNotifyAssertions in QE, #assertions = " << assertions
.size()
391 << " check epr = " << (d_qepr
!= NULL
) << std::endl
;
392 if ((options::instLevelInputOnly() && options::instMaxLevel() != -1) ||
394 for (unsigned i
= 0; i
< assertions
.size(); i
++) {
395 if (options::instLevelInputOnly() && options::instMaxLevel() != -1) {
396 quantifiers::QuantAttributes::setInstantiationLevelAttr(assertions
[i
],
399 if (d_qepr
!= NULL
) {
400 d_qepr
->registerAssertion(assertions
[i
]);
403 if (d_qepr
!= NULL
) {
404 // must handle sources of other new constants e.g. separation logic
406 sep::TheorySep
* theory_sep
=
407 static_cast<sep::TheorySep
*>(getTheoryEngine()->theoryOf(THEORY_SEP
));
408 theory_sep
->initializeBounds();
409 d_qepr
->finishInit();
414 void QuantifiersEngine::check( Theory::Effort e
){
415 CodeTimer
codeTimer(d_statistics
.d_time
);
416 d_useModelEe
= options::quantModelEe() && ( e
>=Theory::EFFORT_LAST_CALL
);
417 // if we want to use the model's equality engine, build the model now
418 if( d_useModelEe
&& !d_model
->isBuilt() ){
419 Trace("quant-engine-debug") << "Build the model." << std::endl
;
420 if( !d_te
->getModelBuilder()->buildModel( d_model
) ){
421 //we are done if model building was unsuccessful
423 if( d_hasAddedLemma
){
424 Trace("quant-engine-debug") << "...failed." << std::endl
;
430 if( !getActiveEqualityEngine()->consistent() ){
431 Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl
;
434 bool needsCheck
= !d_lemmas_waiting
.empty();
435 QuantifiersModule::QEffort needsModelE
= QuantifiersModule::QEFFORT_NONE
;
436 std::vector
< QuantifiersModule
* > qm
;
437 if( d_model
->checkNeeded() ){
438 needsCheck
= needsCheck
|| e
>=Theory::EFFORT_LAST_CALL
; //always need to check at or above last call
439 for (QuantifiersModule
*& mdl
: d_modules
)
441 if (mdl
->needsCheck(e
))
445 //can only request model at last call since theory combination can find inconsistencies
446 if( e
>=Theory::EFFORT_LAST_CALL
){
447 QuantifiersModule::QEffort me
= mdl
->needsModel(e
);
448 needsModelE
= me
<needsModelE
? me
: needsModelE
;
455 d_hasAddedLemma
= false;
456 bool setIncomplete
= false;
458 Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e
<< ", needsCheck=" << needsCheck
<< std::endl
;
460 //this will fail if a set of instances is marked as a conflict, but is not
461 Assert( !d_conflict_c
.get() );
462 //flush previous lemmas (for instance, if was interupted), or other lemmas to process
464 if( d_hasAddedLemma
){
469 if( Trace
.isOn("quant-engine") ){
470 clSet
= double(clock())/double(CLOCKS_PER_SEC
);
471 Trace("quant-engine") << ">>>>> Quantifiers Engine Round, effort = " << e
<< " <<<<<" << std::endl
;
474 if( Trace
.isOn("quant-engine-debug") ){
475 Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e
<< std::endl
;
476 Trace("quant-engine-debug") << " depth : " << d_ierCounter_c
<< std::endl
;
477 Trace("quant-engine-debug") << " modules to check : ";
478 for( unsigned i
=0; i
<qm
.size(); i
++ ){
479 Trace("quant-engine-debug") << qm
[i
]->identify() << " ";
481 Trace("quant-engine-debug") << std::endl
;
482 Trace("quant-engine-debug") << " # quantified formulas = " << d_model
->getNumAssertedQuantifiers() << std::endl
;
483 if( !d_lemmas_waiting
.empty() ){
484 Trace("quant-engine-debug") << " lemmas waiting = " << d_lemmas_waiting
.size() << std::endl
;
486 Trace("quant-engine-debug") << " Theory engine finished : " << !d_te
->needCheck() << std::endl
;
487 Trace("quant-engine-debug") << " Needs model effort : " << needsModelE
<< std::endl
;
489 if( Trace
.isOn("quant-engine-ee-pre") ){
490 Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl
;
491 debugPrintEqualityEngine( "quant-engine-ee-pre" );
493 if( Trace
.isOn("quant-engine-assert") ){
494 Trace("quant-engine-assert") << "Assertions : " << std::endl
;
495 getTheoryEngine()->printAssertions("quant-engine-assert");
499 Trace("quant-engine-debug") << "Resetting all utilities..." << std::endl
;
500 for (QuantifiersUtil
*& util
: d_util
)
502 Trace("quant-engine-debug2") << "Reset " << util
->identify().c_str()
503 << "..." << std::endl
;
507 if( d_hasAddedLemma
){
510 //should only fail reset if added a lemma
516 if( Trace
.isOn("quant-engine-ee") ){
517 Trace("quant-engine-ee") << "Equality engine : " << std::endl
;
518 debugPrintEqualityEngine( "quant-engine-ee" );
522 Trace("quant-engine-debug") << "Reset model..." << std::endl
;
523 d_model
->reset_round();
526 Trace("quant-engine-debug") << "Resetting all modules..." << std::endl
;
527 for (QuantifiersModule
*& mdl
: d_modules
)
529 Trace("quant-engine-debug2") << "Reset " << mdl
->identify().c_str()
533 Trace("quant-engine-debug") << "Done resetting all modules." << std::endl
;
534 //reset may have added lemmas
536 if( d_hasAddedLemma
){
540 if( e
==Theory::EFFORT_LAST_CALL
){
541 //if effort is last call, try to minimize model first
542 //uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver();
543 //if( ufss && !ufss->minimize() ){ return; }
544 ++(d_statistics
.d_instantiation_rounds_lc
);
545 }else if( e
==Theory::EFFORT_FULL
){
546 ++(d_statistics
.d_instantiation_rounds
);
548 Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl
;
549 for (unsigned qef
= QuantifiersModule::QEFFORT_CONFLICT
;
550 qef
<= QuantifiersModule::QEFFORT_LAST_CALL
;
553 QuantifiersModule::QEffort quant_e
=
554 static_cast<QuantifiersModule::QEffort
>(qef
);
555 d_curr_effort_level
= quant_e
;
556 //build the model if any module requested it
557 if (needsModelE
== quant_e
)
559 if (!d_model
->isBuilt())
561 // theory engine's model builder is quantifier engine's builder if it
563 Assert(!d_builder
|| d_builder
== d_te
->getModelBuilder());
564 Trace("quant-engine-debug") << "Build model..." << std::endl
;
565 if (!d_te
->getModelBuilder()->buildModel(d_model
))
570 if (!d_model
->isBuiltSuccess())
575 if( !d_hasAddedLemma
){
577 for (QuantifiersModule
*& mdl
: qm
)
579 Trace("quant-engine-debug") << "Check " << mdl
->identify().c_str()
580 << " at effort " << quant_e
<< "..."
582 mdl
->check(e
, quant_e
);
584 Trace("quant-engine-debug") << "...conflict!" << std::endl
;
588 //flush all current lemmas
591 //if we have added one, stop
592 if( d_hasAddedLemma
){
595 Assert( !d_conflict
);
596 if (quant_e
== QuantifiersModule::QEFFORT_CONFLICT
)
598 if( e
==Theory::EFFORT_FULL
){
599 //increment if a last call happened, we are not strictly enforcing interleaving, or already were in phase
600 if( d_ierCounterLastLc
!=d_ierCounter_lc
|| !options::instWhenStrictInterleave() || d_ierCounter
%d_inst_when_phase
!=0 ){
601 d_ierCounter
= d_ierCounter
+ 1;
602 d_ierCounterLastLc
= d_ierCounter_lc
;
603 d_ierCounter_c
= d_ierCounter_c
.get() + 1;
605 }else if( e
==Theory::EFFORT_LAST_CALL
){
606 d_ierCounter_lc
= d_ierCounter_lc
+ 1;
609 else if (quant_e
== QuantifiersModule::QEFFORT_MODEL
)
611 if( e
==Theory::EFFORT_LAST_CALL
){
612 //sources of incompleteness
613 for (QuantifiersUtil
*& util
: d_util
)
615 if (!util
->checkComplete())
617 Trace("quant-engine-debug") << "Set incomplete because utility "
618 << util
->identify().c_str()
619 << " was incomplete." << std::endl
;
620 setIncomplete
= true;
623 //if we have a chance not to set incomplete
624 if( !setIncomplete
){
625 //check if we should set the incomplete flag
626 for (QuantifiersModule
*& mdl
: d_modules
)
628 if (!mdl
->checkComplete())
630 Trace("quant-engine-debug")
631 << "Set incomplete because module "
632 << mdl
->identify().c_str() << " was incomplete."
634 setIncomplete
= true;
638 if( !setIncomplete
){
639 //look at individual quantified formulas, one module must claim completeness for each one
640 for( unsigned i
=0; i
<d_model
->getNumAssertedQuantifiers(); i
++ ){
641 bool hasCompleteM
= false;
642 Node q
= d_model
->getAssertedQuantifier( i
);
643 QuantifiersModule
* qmd
= getOwner( q
);
645 hasCompleteM
= qmd
->checkCompleteFor( q
);
647 for( unsigned j
=0; j
<d_modules
.size(); j
++ ){
648 if( d_modules
[j
]->checkCompleteFor( q
) ){
656 Trace("quant-engine-debug") << "Set incomplete because " << q
<< " was not fully processed." << std::endl
;
657 setIncomplete
= true;
661 Trace("quant-engine-debug2") << "Complete for " << q
<< " due to " << qmd
->identify().c_str() << std::endl
;
666 //if setIncomplete = false, we will answer SAT, otherwise we will run at quant_e QEFFORT_LAST_CALL
667 if( !setIncomplete
){
674 d_curr_effort_level
= QuantifiersModule::QEFFORT_NONE
;
675 Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl
;
676 if( d_hasAddedLemma
){
677 d_instantiate
->debugPrint();
679 if( Trace
.isOn("quant-engine") ){
680 double clSet2
= double(clock())/double(CLOCKS_PER_SEC
);
681 Trace("quant-engine") << "Finished quantifiers engine, total time = " << (clSet2
-clSet
);
682 Trace("quant-engine") << ", added lemma = " << d_hasAddedLemma
;
683 Trace("quant-engine") << std::endl
;
686 Trace("quant-engine-debug2") << "Finished quantifiers engine check." << std::endl
;
688 Trace("quant-engine-debug2") << "Quantifiers Engine does not need check." << std::endl
;
692 if( e
==Theory::EFFORT_LAST_CALL
&& !d_hasAddedLemma
){
694 Trace("quant-engine") << "Set incomplete flag." << std::endl
;
695 getOutputChannel().setIncomplete();
698 d_instantiate
->debugPrintModel();
702 void QuantifiersEngine::notifyCombineTheories() {
703 //if allowing theory combination to happen at most once between instantiation rounds
705 //d_ierCounterLastLc = -1;
708 bool QuantifiersEngine::reduceQuantifier( Node q
) {
709 //TODO: this can be unified with preregistration: AlphaEquivalence takes ownership of reducable quants
710 BoolMap::const_iterator it
= d_quants_red
.find( q
);
711 if( it
==d_quants_red
.end() ){
713 std::map
< Node
, Node
>::iterator itr
= d_quants_red_lem
.find( q
);
714 if( itr
==d_quants_red_lem
.end() ){
716 Trace("quant-engine-red") << "Alpha equivalence " << q
<< "?" << std::endl
;
717 //add equivalence with another quantified formula
718 lem
= d_alpha_equiv
->reduceQuantifier( q
);
720 Trace("quant-engine-red") << "...alpha equivalence success." << std::endl
;
721 ++(d_statistics
.d_red_alpha_equiv
);
724 d_quants_red_lem
[q
] = lem
;
729 getOutputChannel().lemma( lem
);
731 d_quants_red
[q
] = !lem
.isNull();
732 return !lem
.isNull();
738 void QuantifiersEngine::registerQuantifierInternal(Node f
)
740 std::map
< Node
, bool >::iterator it
= d_quants
.find( f
);
741 if( it
==d_quants
.end() ){
742 Trace("quant") << "QuantifiersEngine : Register quantifier ";
743 Trace("quant") << " : " << f
<< std::endl
;
744 unsigned prev_lemma_waiting
= d_lemmas_waiting
.size();
745 ++(d_statistics
.d_num_quant
);
746 Assert( f
.getKind()==FORALL
);
747 // register with utilities
748 for (unsigned i
= 0; i
< d_util
.size(); i
++)
750 d_util
[i
]->registerQuantifier(f
);
752 // compute attributes
753 d_quant_attr
->computeAttributes(f
);
755 for (QuantifiersModule
*& mdl
: d_modules
)
757 Trace("quant-debug") << "check ownership with " << mdl
->identify()
758 << "..." << std::endl
;
759 mdl
->checkOwnership(f
);
761 QuantifiersModule
* qm
= getOwner(f
);
762 Trace("quant") << " Owner : " << (qm
== nullptr ? "[none]" : qm
->identify())
764 // register with each module
765 for (QuantifiersModule
*& mdl
: d_modules
)
767 Trace("quant-debug") << "register with " << mdl
->identify() << "..."
769 mdl
->registerQuantifier(f
);
770 // since this is context-independent, we should not add any lemmas during
772 Assert(d_lemmas_waiting
.size() == prev_lemma_waiting
);
774 // TODO (#2020): remove this
775 Node ceBody
= d_term_util
->getInstConstantBody(f
);
776 Trace("quant-debug") << "...finish." << std::endl
;
778 AlwaysAssert(d_lemmas_waiting
.size() == prev_lemma_waiting
);
782 void QuantifiersEngine::preRegisterQuantifier(Node q
)
784 NodeSet::const_iterator it
= d_quants_prereg
.find(q
);
785 if (it
!= d_quants_prereg
.end())
789 Trace("quant-debug") << "QuantifiersEngine : Pre-register " << q
<< std::endl
;
790 d_quants_prereg
.insert(q
);
791 // ensure that it is registered
792 registerQuantifierInternal(q
);
793 // register with each module
794 for (QuantifiersModule
*& mdl
: d_modules
)
796 Trace("quant-debug") << "pre-register with " << mdl
->identify() << "..."
798 mdl
->preRegisterQuantifier(q
);
802 Trace("quant-debug") << "...finish pre-register " << q
<< "..." << std::endl
;
805 void QuantifiersEngine::registerPattern( std::vector
<Node
> & pattern
) {
806 for(std::vector
<Node
>::iterator p
= pattern
.begin(); p
!= pattern
.end(); ++p
){
807 std::set
< Node
> added
;
808 getTermDatabase()->addTerm( *p
, added
);
812 void QuantifiersEngine::assertQuantifier( Node f
, bool pol
){
813 if (reduceQuantifier(f
))
815 // if we can reduce it, nothing left to do
820 Node lem
= d_skolemize
->process(f
);
823 if (Trace
.isOn("quantifiers-sk-debug"))
825 Node slem
= Rewriter::rewrite(lem
);
826 Trace("quantifiers-sk-debug")
827 << "Skolemize lemma : " << slem
<< std::endl
;
829 getOutputChannel().lemma(lem
, false, true);
833 // ensure the quantified formula is registered
834 registerQuantifierInternal(f
);
835 // assert it to each module
836 d_model
->assertQuantifier(f
);
837 for (QuantifiersModule
*& mdl
: d_modules
)
841 addTermToDatabase(d_term_util
->getInstConstantBody(f
), true);
844 void QuantifiersEngine::propagate( Theory::Effort level
){
845 CodeTimer
codeTimer(d_statistics
.d_time
);
849 Node
QuantifiersEngine::getNextDecisionRequest( unsigned& priority
){
850 unsigned min_priority
= 0;
852 for( unsigned i
=0; i
<d_modules
.size(); i
++ ){
853 Node n
= d_modules
[i
]->getNextDecisionRequest( priority
);
854 if( !n
.isNull() && ( dec
.isNull() || priority
<min_priority
) ){
856 min_priority
= priority
;
862 void QuantifiersEngine::addTermToDatabase( Node n
, bool withinQuant
, bool withinInstClosure
){
863 if( options::incrementalSolving() ){
864 if( d_presolve_in
.find( n
)==d_presolve_in
.end() ){
865 d_presolve_in
.insert( n
);
866 d_presolve_cache
.push_back( n
);
867 d_presolve_cache_wq
.push_back( withinQuant
);
868 d_presolve_cache_wic
.push_back( withinInstClosure
);
871 //only wait if we are doing incremental solving
872 if( !d_presolve
|| !options::incrementalSolving() ){
873 std::set
< Node
> added
;
874 d_term_db
->addTerm(n
, added
, withinQuant
, withinInstClosure
);
880 d_sygus_tdb
->getEvalUnfold()->registerEvalTerm(n
);
883 // added contains also the Node that just have been asserted in this
887 for (std::set
<Node
>::iterator i
= added
.begin(), end
= added
.end();
891 d_quant_rel
->setRelevance( i
->getOperator(), 0 );
898 void QuantifiersEngine::eqNotifyNewClass(TNode t
) {
899 addTermToDatabase( t
);
900 if( d_eq_inference
){
901 d_eq_inference
->eqNotifyNewClass( t
);
905 void QuantifiersEngine::eqNotifyPreMerge(TNode t1
, TNode t2
) {
906 if( d_eq_inference
){
907 d_eq_inference
->eqNotifyMerge( t1
, t2
);
911 void QuantifiersEngine::eqNotifyPostMerge(TNode t1
, TNode t2
) {
915 void QuantifiersEngine::eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
) {
917 // d_qcf->assertDisequal( t1, t2 );
921 bool QuantifiersEngine::addLemma( Node lem
, bool doCache
, bool doRewrite
){
924 lem
= Rewriter::rewrite(lem
);
926 Trace("inst-add-debug") << "Adding lemma : " << lem
<< std::endl
;
927 BoolMap::const_iterator itp
= d_lemmas_produced_c
.find( lem
);
928 if( itp
==d_lemmas_produced_c
.end() || !(*itp
).second
){
929 //d_curr_out->lemma( lem, false, true );
930 d_lemmas_produced_c
[ lem
] = true;
931 d_lemmas_waiting
.push_back( lem
);
932 Trace("inst-add-debug") << "Added lemma" << std::endl
;
935 Trace("inst-add-debug") << "Duplicate." << std::endl
;
939 //do not need to rewrite, will be rewritten after sending
940 d_lemmas_waiting
.push_back( lem
);
945 bool QuantifiersEngine::removeLemma( Node lem
) {
946 std::vector
< Node
>::iterator it
= std::find( d_lemmas_waiting
.begin(), d_lemmas_waiting
.end(), lem
);
947 if( it
!=d_lemmas_waiting
.end() ){
948 d_lemmas_waiting
.erase( it
, it
+ 1 );
949 d_lemmas_produced_c
[ lem
] = false;
956 void QuantifiersEngine::addRequirePhase( Node lit
, bool req
){
957 d_phase_req_waiting
[lit
] = req
;
960 bool QuantifiersEngine::addSplit( Node n
, bool reqPhase
, bool reqPhasePol
){
961 n
= Rewriter::rewrite( n
);
962 Node lem
= NodeManager::currentNM()->mkNode( OR
, n
, n
.notNode() );
963 if( addLemma( lem
) ){
964 Debug("inst") << "*** Add split " << n
<< std::endl
;
970 bool QuantifiersEngine::addSplitEquality( Node n1
, Node n2
, bool reqPhase
, bool reqPhasePol
){
971 //Assert( !areEqual( n1, n2 ) );
972 //Assert( !areDisequal( n1, n2 ) );
973 Node fm
= NodeManager::currentNM()->mkNode( EQUAL
, n1
, n2
);
974 return addSplit( fm
);
977 bool QuantifiersEngine::addEPRAxiom( TypeNode tn
) {
979 Assert( !options::incrementalSolving() );
980 if( d_qepr
->isEPR( tn
) && !d_qepr
->hasEPRAxiom( tn
) ){
981 Node lem
= d_qepr
->mkEPRAxiom( tn
);
982 Trace("quant-epr") << "EPR lemma for " << tn
<< " : " << lem
<< std::endl
;
983 getOutputChannel().lemma( lem
);
989 void QuantifiersEngine::markRelevant( Node q
) {
990 d_model
->markRelevant( q
);
993 void QuantifiersEngine::setConflict() {
998 bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e
) {
999 Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter
<< ", " << d_ierCounter_lc
<< std::endl
;
1000 //determine if we should perform check, based on instWhenMode
1001 bool performCheck
= false;
1002 if( options::instWhenMode()==quantifiers::INST_WHEN_FULL
){
1003 performCheck
= ( e
>= Theory::EFFORT_FULL
);
1004 }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY
){
1005 performCheck
= ( e
>= Theory::EFFORT_FULL
) && !getTheoryEngine()->needCheck();
1006 }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_LAST_CALL
){
1007 performCheck
= ( ( e
==Theory::EFFORT_FULL
&& d_ierCounter
%d_inst_when_phase
!=0 ) || e
==Theory::EFFORT_LAST_CALL
);
1008 }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY_LAST_CALL
){
1009 performCheck
= ( ( e
==Theory::EFFORT_FULL
&& !getTheoryEngine()->needCheck() && d_ierCounter
%d_inst_when_phase
!=0 ) || e
==Theory::EFFORT_LAST_CALL
);
1010 }else if( options::instWhenMode()==quantifiers::INST_WHEN_LAST_CALL
){
1011 performCheck
= ( e
>= Theory::EFFORT_LAST_CALL
);
1013 performCheck
= true;
1015 if( e
==Theory::EFFORT_LAST_CALL
){
1016 //with bounded integers, skip every other last call,
1017 // since matching loops may occur with infinite quantification
1018 if( d_ierCounter_lc
%2==0 && options::fmfBound() ){
1019 performCheck
= false;
1022 return performCheck
;
1025 quantifiers::UserPatMode
QuantifiersEngine::getInstUserPatMode() {
1026 if( options::userPatternsQuant()==quantifiers::USER_PAT_MODE_INTERLEAVE
){
1027 return d_ierCounter
%2==0 ? quantifiers::USER_PAT_MODE_USE
: quantifiers::USER_PAT_MODE_RESORT
;
1029 return options::userPatternsQuant();
1033 void QuantifiersEngine::flushLemmas(){
1034 if( !d_lemmas_waiting
.empty() ){
1035 //filter based on notify classes
1036 if (d_instantiate
->hasNotify())
1038 unsigned prev_lem_sz
= d_lemmas_waiting
.size();
1039 d_instantiate
->notifyFlushLemmas();
1040 if( prev_lem_sz
!=d_lemmas_waiting
.size() ){
1041 Trace("quant-engine") << "...filtered instances : " << d_lemmas_waiting
.size() << " / " << prev_lem_sz
<< std::endl
;
1044 //take default output channel if none is provided
1045 d_hasAddedLemma
= true;
1046 for( unsigned i
=0; i
<d_lemmas_waiting
.size(); i
++ ){
1047 Trace("qe-lemma") << "Lemma : " << d_lemmas_waiting
[i
] << std::endl
;
1048 getOutputChannel().lemma( d_lemmas_waiting
[i
], false, true );
1050 d_lemmas_waiting
.clear();
1052 if( !d_phase_req_waiting
.empty() ){
1053 for( std::map
< Node
, bool >::iterator it
= d_phase_req_waiting
.begin(); it
!= d_phase_req_waiting
.end(); ++it
){
1054 Trace("qe-lemma") << "Require phase : " << it
->first
<< " -> " << it
->second
<< std::endl
;
1055 getOutputChannel().requirePhase( it
->first
, it
->second
);
1057 d_phase_req_waiting
.clear();
1061 bool QuantifiersEngine::getUnsatCoreLemmas( std::vector
< Node
>& active_lemmas
) {
1062 return d_instantiate
->getUnsatCoreLemmas(active_lemmas
);
1065 bool QuantifiersEngine::getUnsatCoreLemmas( std::vector
< Node
>& active_lemmas
, std::map
< Node
, Node
>& weak_imp
) {
1066 return d_instantiate
->getUnsatCoreLemmas(active_lemmas
, weak_imp
);
1069 void QuantifiersEngine::getInstantiationTermVectors( Node q
, std::vector
< std::vector
< Node
> >& tvecs
) {
1070 d_instantiate
->getInstantiationTermVectors(q
, tvecs
);
1073 void QuantifiersEngine::getInstantiationTermVectors( std::map
< Node
, std::vector
< std::vector
< Node
> > >& insts
) {
1074 d_instantiate
->getInstantiationTermVectors(insts
);
1077 void QuantifiersEngine::getExplanationForInstLemmas(
1078 const std::vector
<Node
>& lems
,
1079 std::map
<Node
, Node
>& quant
,
1080 std::map
<Node
, std::vector
<Node
> >& tvec
)
1082 d_instantiate
->getExplanationForInstLemmas(lems
, quant
, tvec
);
1085 void QuantifiersEngine::printInstantiations( std::ostream
& out
) {
1086 bool printed
= false;
1087 // print the skolemizations
1088 if (d_skolemize
->printSkolemization(out
))
1092 // print the instantiations
1093 if (d_instantiate
->printInstantiations(out
))
1098 out
<< "No instantiations" << std::endl
;
1102 void QuantifiersEngine::printSynthSolution( std::ostream
& out
) {
1104 d_ceg_inst
->printSynthSolution( out
);
1106 out
<< "Internal error : module for synth solution not found." << std::endl
;
1110 void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector
< Node
>& qs
) {
1111 d_instantiate
->getInstantiatedQuantifiedFormulas(qs
);
1114 void QuantifiersEngine::getInstantiations( std::map
< Node
, std::vector
< Node
> >& insts
) {
1115 d_instantiate
->getInstantiations(insts
);
1118 void QuantifiersEngine::getInstantiations( Node q
, std::vector
< Node
>& insts
) {
1119 d_instantiate
->getInstantiations(q
, insts
);
1122 Node
QuantifiersEngine::getInstantiatedConjunction( Node q
) {
1123 return d_instantiate
->getInstantiatedConjunction(q
);
1126 QuantifiersEngine::Statistics::Statistics()
1127 : d_time("theory::QuantifiersEngine::time"),
1128 d_qcf_time("theory::QuantifiersEngine::time_qcf"),
1129 d_ematching_time("theory::QuantifiersEngine::time_ematching"),
1130 d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
1131 d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
1132 d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
1133 d_triggers("QuantifiersEngine::Triggers", 0),
1134 d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
1135 d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
1136 d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0),
1137 d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0),
1138 d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0),
1139 d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0),
1140 d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0),
1141 d_instantiations_qcf("QuantifiersEngine::Instantiations_Qcf_Conflict", 0),
1142 d_instantiations_qcf_prop("QuantifiersEngine::Instantiations_Qcf_Prop", 0),
1143 d_instantiations_fmf_exh("QuantifiersEngine::Instantiations_Fmf_Exh", 0),
1144 d_instantiations_fmf_mbqi("QuantifiersEngine::Instantiations_Fmf_Mbqi", 0),
1145 d_instantiations_cbqi("QuantifiersEngine::Instantiations_Cbqi", 0),
1146 d_instantiations_rr("QuantifiersEngine::Instantiations_Rewrite_Rules", 0)
1148 smtStatisticsRegistry()->registerStat(&d_time
);
1149 smtStatisticsRegistry()->registerStat(&d_qcf_time
);
1150 smtStatisticsRegistry()->registerStat(&d_ematching_time
);
1151 smtStatisticsRegistry()->registerStat(&d_num_quant
);
1152 smtStatisticsRegistry()->registerStat(&d_instantiation_rounds
);
1153 smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc
);
1154 smtStatisticsRegistry()->registerStat(&d_triggers
);
1155 smtStatisticsRegistry()->registerStat(&d_simple_triggers
);
1156 smtStatisticsRegistry()->registerStat(&d_multi_triggers
);
1157 smtStatisticsRegistry()->registerStat(&d_multi_trigger_instantiations
);
1158 smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv
);
1159 smtStatisticsRegistry()->registerStat(&d_instantiations_user_patterns
);
1160 smtStatisticsRegistry()->registerStat(&d_instantiations_auto_gen
);
1161 smtStatisticsRegistry()->registerStat(&d_instantiations_guess
);
1162 smtStatisticsRegistry()->registerStat(&d_instantiations_qcf
);
1163 smtStatisticsRegistry()->registerStat(&d_instantiations_qcf_prop
);
1164 smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_exh
);
1165 smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_mbqi
);
1166 smtStatisticsRegistry()->registerStat(&d_instantiations_cbqi
);
1167 smtStatisticsRegistry()->registerStat(&d_instantiations_rr
);
1170 QuantifiersEngine::Statistics::~Statistics(){
1171 smtStatisticsRegistry()->unregisterStat(&d_time
);
1172 smtStatisticsRegistry()->unregisterStat(&d_qcf_time
);
1173 smtStatisticsRegistry()->unregisterStat(&d_ematching_time
);
1174 smtStatisticsRegistry()->unregisterStat(&d_num_quant
);
1175 smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds
);
1176 smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc
);
1177 smtStatisticsRegistry()->unregisterStat(&d_triggers
);
1178 smtStatisticsRegistry()->unregisterStat(&d_simple_triggers
);
1179 smtStatisticsRegistry()->unregisterStat(&d_multi_triggers
);
1180 smtStatisticsRegistry()->unregisterStat(&d_multi_trigger_instantiations
);
1181 smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv
);
1182 smtStatisticsRegistry()->unregisterStat(&d_instantiations_user_patterns
);
1183 smtStatisticsRegistry()->unregisterStat(&d_instantiations_auto_gen
);
1184 smtStatisticsRegistry()->unregisterStat(&d_instantiations_guess
);
1185 smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf
);
1186 smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf_prop
);
1187 smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_exh
);
1188 smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_mbqi
);
1189 smtStatisticsRegistry()->unregisterStat(&d_instantiations_cbqi
);
1190 smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr
);
1193 eq::EqualityEngine
* QuantifiersEngine::getMasterEqualityEngine(){
1194 return d_te
->getMasterEqualityEngine();
1197 eq::EqualityEngine
* QuantifiersEngine::getActiveEqualityEngine() {
1199 return d_model
->getEqualityEngine();
1201 return d_te
->getMasterEqualityEngine();
1205 Node
QuantifiersEngine::getInternalRepresentative( Node a
, Node q
, int index
){
1206 bool prevModelEe
= d_useModelEe
;
1207 d_useModelEe
= false;
1208 Node ret
= d_eq_query
->getInternalRepresentative( a
, q
, index
);
1209 d_useModelEe
= prevModelEe
;
1213 void QuantifiersEngine::getSynthSolutions(std::map
<Node
, Node
>& sol_map
)
1215 d_ceg_inst
->getSynthSolutions(sol_map
);
1218 void QuantifiersEngine::debugPrintEqualityEngine( const char * c
) {
1219 eq::EqualityEngine
* ee
= getActiveEqualityEngine();
1220 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( ee
);
1221 std::map
< TypeNode
, int > typ_num
;
1222 while( !eqcs_i
.isFinished() ){
1223 TNode r
= (*eqcs_i
);
1224 TypeNode tr
= r
.getType();
1225 if( typ_num
.find( tr
)==typ_num
.end() ){
1229 bool firstTime
= true;
1230 Trace(c
) << " " << r
;
1231 Trace(c
) << " : { ";
1232 eq::EqClassIterator eqc_i
= eq::EqClassIterator( r
, ee
);
1233 while( !eqc_i
.isFinished() ){
1237 Trace(c
) << std::endl
;
1240 Trace(c
) << " " << n
<< std::endl
;
1244 if( !firstTime
){ Trace(c
) << " "; }
1245 Trace(c
) << "}" << std::endl
;
1248 Trace(c
) << std::endl
;
1249 for( std::map
< TypeNode
, int >::iterator it
= typ_num
.begin(); it
!= typ_num
.end(); ++it
){
1250 Trace(c
) << "# eqc for " << it
->first
<< " : " << it
->second
<< std::endl
;