1 /********************* */
2 /*! \file quantifiers_engine.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Morgan Deters, Mathias Preiner
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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_engine_scope.h"
20 #include "smt/smt_statistics_registry.h"
21 #include "theory/quantifiers/fmf/full_model_check.h"
22 #include "theory/quantifiers/quantifiers_modules.h"
23 #include "theory/quantifiers/quantifiers_rewriter.h"
24 #include "theory/theory_engine.h"
25 #include "theory/uf/equality_engine.h"
28 using namespace CVC4::kind
;
33 QuantifiersEngine::QuantifiersEngine(TheoryEngine
* te
,
35 ProofNodeManager
* pnm
)
37 d_context(te
->getSatContext()),
38 d_userContext(te
->getUserContext()),
40 d_masterEqualityEngine(nullptr),
42 new quantifiers::EqualityQueryQuantifiersEngine(d_context
, this)),
43 d_tr_trie(new inst::TriggerTrie
),
47 d_term_util(new quantifiers::TermUtil(this)),
48 d_term_canon(new expr::TermCanonize
),
49 d_term_db(new quantifiers::TermDb(d_context
, d_userContext
, this)),
51 d_quant_attr(new quantifiers::QuantAttributes(this)),
52 d_instantiate(new quantifiers::Instantiate(this, d_userContext
, pnm
)),
53 d_skolemize(new quantifiers::Skolemize(this, d_userContext
, pnm
)),
54 d_term_enum(new quantifiers::TermEnumeration
),
55 d_conflict_c(d_context
, false),
56 d_quants_prereg(d_userContext
),
57 d_quants_red(d_userContext
),
58 d_lemmas_produced_c(d_userContext
),
59 d_ierCounter_c(d_context
),
60 d_presolve(d_userContext
, true),
61 d_presolve_in(d_userContext
),
62 d_presolve_cache(d_userContext
),
63 d_presolve_cache_wq(d_userContext
),
64 d_presolve_cache_wic(d_userContext
)
67 d_util
.push_back(d_eq_query
.get());
68 // term util must come before the other utilities
69 d_util
.push_back(d_term_util
.get());
70 d_util
.push_back(d_term_db
.get());
72 if (options::sygus() || options::sygusInst())
74 // must be constructed here since it is required for datatypes finistInit
75 d_sygus_tdb
.reset(new quantifiers::TermDbSygus(d_context
, this));
78 d_util
.push_back(d_instantiate
.get());
80 d_curr_effort_level
= QuantifiersModule::QEFFORT_NONE
;
82 d_hasAddedLemma
= false;
83 //don't add true lemma
84 d_lemmas_produced_c
[d_term_util
->d_true
] = true;
86 Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl
;
87 Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl
;
89 if( options::quantEpr() ){
90 Assert(!options::incrementalSolving());
91 d_qepr
.reset(new quantifiers::QuantEPR
);
95 //allow theory combination to go first, once initially
96 d_ierCounter
= options::instWhenTcFirst() ? 0 : 1;
97 d_ierCounter_c
= d_ierCounter
;
99 d_ierCounterLastLc
= 0;
100 d_inst_when_phase
= 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() );
102 // Finite model finding requires specialized ways of building the model.
103 // We require constructing the model and model builder here, since it is
104 // required for initializing the CombinationEngine.
105 if (options::finiteModelFind() || options::fmfBound())
107 Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl
;
108 if (options::mbqiMode() == options::MbqiMode::FMC
109 || options::mbqiMode() == options::MbqiMode::TRUST
110 || options::fmfBound())
112 Trace("quant-engine-debug") << "...make fmc builder." << std::endl
;
113 d_model
.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
114 this, d_context
, "FirstOrderModelFmc"));
116 new quantifiers::fmcheck::FullModelChecker(d_context
, this));
118 Trace("quant-engine-debug") << "...make default model builder." << std::endl
;
120 new quantifiers::FirstOrderModel(this, d_context
, "FirstOrderModel"));
121 d_builder
.reset(new quantifiers::QModelBuilder(d_context
, this));
125 new quantifiers::FirstOrderModel(this, d_context
, "FirstOrderModel"));
129 QuantifiersEngine::~QuantifiersEngine() {}
131 void QuantifiersEngine::finishInit()
133 // Initialize the modules and the utilities here. We delay their
134 // initialization to here, since this is after TheoryQuantifiers finishInit,
135 // which has initialized the state and inference manager of this engine.
136 d_qmodules
.reset(new quantifiers::QuantifiersModules
);
137 d_qmodules
->initialize(this, d_context
, d_modules
);
138 if (d_qmodules
->d_rel_dom
.get())
140 d_util
.push_back(d_qmodules
->d_rel_dom
.get());
144 void QuantifiersEngine::setMasterEqualityEngine(eq::EqualityEngine
* mee
)
146 d_masterEqualityEngine
= mee
;
149 TheoryEngine
* QuantifiersEngine::getTheoryEngine() const { return d_te
; }
151 DecisionManager
* QuantifiersEngine::getDecisionManager()
153 return &d_decManager
;
156 context::Context
* QuantifiersEngine::getSatContext() { return d_context
; }
158 context::UserContext
* QuantifiersEngine::getUserContext()
160 return d_userContext
;
163 OutputChannel
& QuantifiersEngine::getOutputChannel()
165 return d_te
->theoryOf(THEORY_QUANTIFIERS
)->getOutputChannel();
167 /** get default valuation for the quantifiers engine */
168 Valuation
& QuantifiersEngine::getValuation()
170 return d_te
->theoryOf(THEORY_QUANTIFIERS
)->getValuation();
173 const LogicInfo
& QuantifiersEngine::getLogicInfo() const
175 return d_te
->getLogicInfo();
178 EqualityQuery
* QuantifiersEngine::getEqualityQuery() const
180 return d_eq_query
.get();
182 quantifiers::QModelBuilder
* QuantifiersEngine::getModelBuilder() const
184 return d_builder
.get();
186 quantifiers::QuantEPR
* QuantifiersEngine::getQuantEPR() const
190 quantifiers::FirstOrderModel
* QuantifiersEngine::getModel() const
192 return d_model
.get();
194 quantifiers::TermDb
* QuantifiersEngine::getTermDatabase() const
196 return d_term_db
.get();
198 quantifiers::TermDbSygus
* QuantifiersEngine::getTermDatabaseSygus() const
200 return d_sygus_tdb
.get();
202 quantifiers::TermUtil
* QuantifiersEngine::getTermUtil() const
204 return d_term_util
.get();
206 expr::TermCanonize
* QuantifiersEngine::getTermCanonize() const
208 return d_term_canon
.get();
210 quantifiers::QuantAttributes
* QuantifiersEngine::getQuantAttributes() const
212 return d_quant_attr
.get();
214 quantifiers::Instantiate
* QuantifiersEngine::getInstantiate() const
216 return d_instantiate
.get();
218 quantifiers::Skolemize
* QuantifiersEngine::getSkolemize() const
220 return d_skolemize
.get();
222 quantifiers::TermEnumeration
* QuantifiersEngine::getTermEnumeration() const
224 return d_term_enum
.get();
226 inst::TriggerTrie
* QuantifiersEngine::getTriggerDatabase() const
228 return d_tr_trie
.get();
231 QuantifiersModule
* QuantifiersEngine::getOwner( Node q
) {
232 std::map
< Node
, QuantifiersModule
* >::iterator it
= d_owner
.find( q
);
233 if( it
==d_owner
.end() ){
240 void QuantifiersEngine::setOwner( Node q
, QuantifiersModule
* m
, int priority
) {
241 QuantifiersModule
* mo
= getOwner( q
);
244 if( priority
<=d_owner_priority
[q
] ){
245 Trace("quant-warn") << "WARNING: setting owner of " << q
<< " to " << ( m
? m
->identify() : "null" ) << ", but already has owner " << mo
->identify() << " with higher priority!" << std::endl
;
250 d_owner_priority
[q
] = priority
;
254 void QuantifiersEngine::setOwner(Node q
, quantifiers::QAttributes
& qa
)
256 if (qa
.d_sygus
|| (options::sygusRecFun() && !qa
.d_fundef_f
.isNull()))
258 if (d_qmodules
->d_synth_e
.get() == nullptr)
260 Trace("quant-warn") << "WARNING : synth engine is null, and we have : "
263 // set synth engine as owner since this is either a conjecture or a function
264 // definition to be used by sygus
265 setOwner(q
, d_qmodules
->d_synth_e
.get(), 2);
269 bool QuantifiersEngine::hasOwnership( Node q
, QuantifiersModule
* m
) {
270 QuantifiersModule
* mo
= getOwner( q
);
271 return mo
==m
|| mo
==NULL
;
274 bool QuantifiersEngine::isFiniteBound(Node q
, Node v
) const
276 quantifiers::BoundedIntegers
* bi
= d_qmodules
->d_bint
.get();
277 if (bi
&& bi
->isBound(q
, v
))
281 TypeNode tn
= v
.getType();
282 if (tn
.isSort() && options::finiteModelFind())
286 else if (d_term_enum
->mayComplete(tn
))
293 BoundVarType
QuantifiersEngine::getBoundVarType(Node q
, Node v
) const
295 quantifiers::BoundedIntegers
* bi
= d_qmodules
->d_bint
.get();
298 return bi
->getBoundVarType(q
, v
);
300 return isFiniteBound(q
, v
) ? BOUND_FINITE
: BOUND_NONE
;
303 void QuantifiersEngine::getBoundVarIndices(Node q
,
304 std::vector
<unsigned>& indices
) const
306 Assert(indices
.empty());
307 // we take the bounded variables first
308 quantifiers::BoundedIntegers
* bi
= d_qmodules
->d_bint
.get();
311 bi
->getBoundVarIndices(q
, indices
);
313 // then get the remaining ones
314 for (unsigned i
= 0, nvars
= q
[0].getNumChildren(); i
< nvars
; i
++)
316 if (std::find(indices
.begin(), indices
.end(), i
) == indices
.end())
318 indices
.push_back(i
);
323 bool QuantifiersEngine::getBoundElements(RepSetIterator
* rsi
,
327 std::vector
<Node
>& elements
) const
329 quantifiers::BoundedIntegers
* bi
= d_qmodules
->d_bint
.get();
332 return bi
->getBoundElements(rsi
, initial
, q
, v
, elements
);
337 void QuantifiersEngine::presolve() {
338 Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl
;
339 d_lemmas_waiting
.clear();
340 d_phase_req_waiting
.clear();
341 for( unsigned i
=0; i
<d_modules
.size(); i
++ ){
342 d_modules
[i
]->presolve();
344 d_term_db
->presolve();
346 //add all terms to database
347 if( options::incrementalSolving() ){
348 Trace("quant-engine-proc") << "Add presolve cache " << d_presolve_cache
.size() << std::endl
;
349 for( unsigned i
=0; i
<d_presolve_cache
.size(); i
++ ){
350 addTermToDatabase( d_presolve_cache
[i
], d_presolve_cache_wq
[i
], d_presolve_cache_wic
[i
] );
352 Trace("quant-engine-proc") << "Done add presolve cache " << std::endl
;
356 void QuantifiersEngine::ppNotifyAssertions(
357 const std::vector
<Node
>& assertions
) {
358 Trace("quant-engine-proc")
359 << "ppNotifyAssertions in QE, #assertions = " << assertions
.size()
360 << " check epr = " << (d_qepr
!= NULL
) << std::endl
;
361 if (options::instLevelInputOnly() && options::instMaxLevel() != -1)
363 for (const Node
& a
: assertions
)
365 quantifiers::QuantAttributes::setInstantiationLevelAttr(a
, 0);
368 if (options::sygus())
370 quantifiers::SynthEngine
* sye
= d_qmodules
->d_synth_e
.get();
371 for (const Node
& a
: assertions
)
373 sye
->preregisterAssertion(a
);
376 /* The SyGuS instantiation module needs a global view of all available
377 * assertions to collect global terms that get added to each grammar.
379 if (options::sygusInst())
381 quantifiers::SygusInst
* si
= d_qmodules
->d_sygus_inst
.get();
382 si
->ppNotifyAssertions(assertions
);
386 void QuantifiersEngine::check( Theory::Effort e
){
387 CodeTimer
codeTimer(d_statistics
.d_time
);
389 if (!getMasterEqualityEngine()->consistent())
391 Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl
;
394 if (d_conflict_c
.get())
396 if (e
< Theory::EFFORT_LAST_CALL
)
398 // this can happen in rare cases when quantifiers is the first to realize
399 // there is a quantifier-free conflict, for example, when it discovers
400 // disequal and congruent terms in the master equality engine during
401 // term indexing. In such cases, quantifiers reports a "conflicting lemma"
402 // that is, one that is entailed to be false by the current assignment.
403 // If this lemma is not a SAT conflict, we may get another call to full
404 // effort check and the quantifier-free solvers still haven't realized
405 // there is a conflict. In this case, we return, trusting that theory
406 // combination will do the right thing (split on equalities until there is
407 // a conflict at the quantifier-free level).
408 Trace("quant-engine-debug")
409 << "Conflicting lemma already reported by quantifiers, return."
413 // we reported what we thought was a conflicting lemma, but now we have
414 // gotten a check at LAST_CALL effort, indicating that the lemma we reported
415 // was not conflicting. This should never happen, but in production mode, we
416 // proceed with the check.
419 bool needsCheck
= !d_lemmas_waiting
.empty();
420 QuantifiersModule::QEffort needsModelE
= QuantifiersModule::QEFFORT_NONE
;
421 std::vector
< QuantifiersModule
* > qm
;
422 if( d_model
->checkNeeded() ){
423 needsCheck
= needsCheck
|| e
>=Theory::EFFORT_LAST_CALL
; //always need to check at or above last call
424 for (QuantifiersModule
*& mdl
: d_modules
)
426 if (mdl
->needsCheck(e
))
430 //can only request model at last call since theory combination can find inconsistencies
431 if( e
>=Theory::EFFORT_LAST_CALL
){
432 QuantifiersModule::QEffort me
= mdl
->needsModel(e
);
433 needsModelE
= me
<needsModelE
? me
: needsModelE
;
440 d_hasAddedLemma
= false;
441 bool setIncomplete
= false;
443 Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e
<< ", needsCheck=" << needsCheck
<< std::endl
;
445 //flush previous lemmas (for instance, if was interrupted), or other lemmas to process
447 if( d_hasAddedLemma
){
452 if( Trace
.isOn("quant-engine") ){
453 clSet
= double(clock())/double(CLOCKS_PER_SEC
);
454 Trace("quant-engine") << ">>>>> Quantifiers Engine Round, effort = " << e
<< " <<<<<" << std::endl
;
457 if( Trace
.isOn("quant-engine-debug") ){
458 Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e
<< std::endl
;
459 Trace("quant-engine-debug") << " depth : " << d_ierCounter_c
<< std::endl
;
460 Trace("quant-engine-debug") << " modules to check : ";
461 for( unsigned i
=0; i
<qm
.size(); i
++ ){
462 Trace("quant-engine-debug") << qm
[i
]->identify() << " ";
464 Trace("quant-engine-debug") << std::endl
;
465 Trace("quant-engine-debug") << " # quantified formulas = " << d_model
->getNumAssertedQuantifiers() << std::endl
;
466 if( !d_lemmas_waiting
.empty() ){
467 Trace("quant-engine-debug") << " lemmas waiting = " << d_lemmas_waiting
.size() << std::endl
;
469 Trace("quant-engine-debug")
470 << " Theory engine finished : " << !theoryEngineNeedsCheck()
472 Trace("quant-engine-debug") << " Needs model effort : " << needsModelE
<< std::endl
;
473 Trace("quant-engine-debug")
474 << " In conflict : " << d_conflict
<< std::endl
;
476 if( Trace
.isOn("quant-engine-ee-pre") ){
477 Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl
;
478 debugPrintEqualityEngine( "quant-engine-ee-pre" );
480 if( Trace
.isOn("quant-engine-assert") ){
481 Trace("quant-engine-assert") << "Assertions : " << std::endl
;
482 getTheoryEngine()->printAssertions("quant-engine-assert");
486 Trace("quant-engine-debug") << "Resetting all utilities..." << std::endl
;
487 for (QuantifiersUtil
*& util
: d_util
)
489 Trace("quant-engine-debug2") << "Reset " << util
->identify().c_str()
490 << "..." << std::endl
;
494 if( d_hasAddedLemma
){
497 //should only fail reset if added a lemma
503 if( Trace
.isOn("quant-engine-ee") ){
504 Trace("quant-engine-ee") << "Equality engine : " << std::endl
;
505 debugPrintEqualityEngine( "quant-engine-ee" );
509 Trace("quant-engine-debug") << "Reset model..." << std::endl
;
510 d_model
->reset_round();
513 Trace("quant-engine-debug") << "Resetting all modules..." << std::endl
;
514 for (QuantifiersModule
*& mdl
: d_modules
)
516 Trace("quant-engine-debug2") << "Reset " << mdl
->identify().c_str()
520 Trace("quant-engine-debug") << "Done resetting all modules." << std::endl
;
521 //reset may have added lemmas
523 if( d_hasAddedLemma
){
527 if( e
==Theory::EFFORT_LAST_CALL
){
528 ++(d_statistics
.d_instantiation_rounds_lc
);
529 }else if( e
==Theory::EFFORT_FULL
){
530 ++(d_statistics
.d_instantiation_rounds
);
532 Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl
;
533 for (unsigned qef
= QuantifiersModule::QEFFORT_CONFLICT
;
534 qef
<= QuantifiersModule::QEFFORT_LAST_CALL
;
537 QuantifiersModule::QEffort quant_e
=
538 static_cast<QuantifiersModule::QEffort
>(qef
);
539 d_curr_effort_level
= quant_e
;
540 // Force the theory engine to build the model if any module requested it.
541 if (needsModelE
== quant_e
)
543 Trace("quant-engine-debug") << "Build model..." << std::endl
;
544 if (!d_te
->buildModel())
546 // If we failed to build the model, flush all pending lemmas and
552 if( !d_hasAddedLemma
){
554 for (QuantifiersModule
*& mdl
: qm
)
556 Trace("quant-engine-debug") << "Check " << mdl
->identify().c_str()
557 << " at effort " << quant_e
<< "..."
559 mdl
->check(e
, quant_e
);
561 Trace("quant-engine-debug") << "...conflict!" << std::endl
;
565 //flush all current lemmas
568 //if we have added one, stop
569 if( d_hasAddedLemma
){
573 if (quant_e
== QuantifiersModule::QEFFORT_CONFLICT
)
575 if( e
==Theory::EFFORT_FULL
){
576 //increment if a last call happened, we are not strictly enforcing interleaving, or already were in phase
577 if( d_ierCounterLastLc
!=d_ierCounter_lc
|| !options::instWhenStrictInterleave() || d_ierCounter
%d_inst_when_phase
!=0 ){
578 d_ierCounter
= d_ierCounter
+ 1;
579 d_ierCounterLastLc
= d_ierCounter_lc
;
580 d_ierCounter_c
= d_ierCounter_c
.get() + 1;
582 }else if( e
==Theory::EFFORT_LAST_CALL
){
583 d_ierCounter_lc
= d_ierCounter_lc
+ 1;
586 else if (quant_e
== QuantifiersModule::QEFFORT_MODEL
)
588 if( e
==Theory::EFFORT_LAST_CALL
){
589 //sources of incompleteness
590 for (QuantifiersUtil
*& util
: d_util
)
592 if (!util
->checkComplete())
594 Trace("quant-engine-debug") << "Set incomplete because utility "
595 << util
->identify().c_str()
596 << " was incomplete." << std::endl
;
597 setIncomplete
= true;
600 if (d_conflict_c
.get())
602 // we reported a conflicting lemma, should return
603 setIncomplete
= true;
605 //if we have a chance not to set incomplete
606 if( !setIncomplete
){
607 //check if we should set the incomplete flag
608 for (QuantifiersModule
*& mdl
: d_modules
)
610 if (!mdl
->checkComplete())
612 Trace("quant-engine-debug")
613 << "Set incomplete because module "
614 << mdl
->identify().c_str() << " was incomplete."
616 setIncomplete
= true;
620 if( !setIncomplete
){
621 //look at individual quantified formulas, one module must claim completeness for each one
622 for( unsigned i
=0; i
<d_model
->getNumAssertedQuantifiers(); i
++ ){
623 bool hasCompleteM
= false;
624 Node q
= d_model
->getAssertedQuantifier( i
);
625 QuantifiersModule
* qmd
= getOwner( q
);
627 hasCompleteM
= qmd
->checkCompleteFor( q
);
629 for( unsigned j
=0; j
<d_modules
.size(); j
++ ){
630 if( d_modules
[j
]->checkCompleteFor( q
) ){
638 Trace("quant-engine-debug") << "Set incomplete because " << q
<< " was not fully processed." << std::endl
;
639 setIncomplete
= true;
643 Trace("quant-engine-debug2") << "Complete for " << q
<< " due to " << qmd
->identify().c_str() << std::endl
;
648 //if setIncomplete = false, we will answer SAT, otherwise we will run at quant_e QEFFORT_LAST_CALL
649 if( !setIncomplete
){
656 d_curr_effort_level
= QuantifiersModule::QEFFORT_NONE
;
657 Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl
;
661 bool debugInstTrace
= Trace
.isOn("inst-per-quant-round");
662 if (options::debugInst() || debugInstTrace
)
664 Options
& sopts
= smt::currentSmtEngine()->getOptions();
665 std::ostream
& out
= *sopts
.getOut();
666 d_instantiate
->debugPrint(out
);
669 if( Trace
.isOn("quant-engine") ){
670 double clSet2
= double(clock())/double(CLOCKS_PER_SEC
);
671 Trace("quant-engine") << "Finished quantifiers engine, total time = " << (clSet2
-clSet
);
672 Trace("quant-engine") << ", added lemma = " << d_hasAddedLemma
;
673 Trace("quant-engine") << std::endl
;
676 Trace("quant-engine-debug2") << "Finished quantifiers engine check." << std::endl
;
678 Trace("quant-engine-debug2") << "Quantifiers Engine does not need check." << std::endl
;
682 if( e
==Theory::EFFORT_LAST_CALL
&& !d_hasAddedLemma
){
684 Trace("quant-engine") << "Set incomplete flag." << std::endl
;
685 getOutputChannel().setIncomplete();
688 d_instantiate
->debugPrintModel();
692 void QuantifiersEngine::notifyCombineTheories() {
693 //if allowing theory combination to happen at most once between instantiation rounds
695 //d_ierCounterLastLc = -1;
698 bool QuantifiersEngine::reduceQuantifier( Node q
) {
699 //TODO: this can be unified with preregistration: AlphaEquivalence takes ownership of reducable quants
700 BoolMap::const_iterator it
= d_quants_red
.find( q
);
701 if( it
==d_quants_red
.end() ){
703 std::map
< Node
, Node
>::iterator itr
= d_quants_red_lem
.find( q
);
704 if( itr
==d_quants_red_lem
.end() ){
705 if (d_qmodules
->d_alpha_equiv
)
707 Trace("quant-engine-red") << "Alpha equivalence " << q
<< "?" << std::endl
;
708 //add equivalence with another quantified formula
709 lem
= d_qmodules
->d_alpha_equiv
->reduceQuantifier(q
);
711 Trace("quant-engine-red") << "...alpha equivalence success." << std::endl
;
712 ++(d_statistics
.d_red_alpha_equiv
);
715 d_quants_red_lem
[q
] = lem
;
720 getOutputChannel().lemma( lem
);
722 d_quants_red
[q
] = !lem
.isNull();
723 return !lem
.isNull();
729 void QuantifiersEngine::registerQuantifierInternal(Node f
)
731 std::map
< Node
, bool >::iterator it
= d_quants
.find( f
);
732 if( it
==d_quants
.end() ){
733 Trace("quant") << "QuantifiersEngine : Register quantifier ";
734 Trace("quant") << " : " << f
<< std::endl
;
735 unsigned prev_lemma_waiting
= d_lemmas_waiting
.size();
736 ++(d_statistics
.d_num_quant
);
737 Assert(f
.getKind() == FORALL
);
738 // register with utilities
739 for (unsigned i
= 0; i
< d_util
.size(); i
++)
741 d_util
[i
]->registerQuantifier(f
);
743 // compute attributes
744 d_quant_attr
->computeAttributes(f
);
746 for (QuantifiersModule
*& mdl
: d_modules
)
748 Trace("quant-debug") << "check ownership with " << mdl
->identify()
749 << "..." << std::endl
;
750 mdl
->checkOwnership(f
);
752 QuantifiersModule
* qm
= getOwner(f
);
753 Trace("quant") << " Owner : " << (qm
== nullptr ? "[none]" : qm
->identify())
755 // register with each module
756 for (QuantifiersModule
*& mdl
: d_modules
)
758 Trace("quant-debug") << "register with " << mdl
->identify() << "..."
760 mdl
->registerQuantifier(f
);
761 // since this is context-independent, we should not add any lemmas during
763 Assert(d_lemmas_waiting
.size() == prev_lemma_waiting
);
765 Trace("quant-debug") << "...finish." << std::endl
;
767 AlwaysAssert(d_lemmas_waiting
.size() == prev_lemma_waiting
);
771 void QuantifiersEngine::preRegisterQuantifier(Node q
)
773 NodeSet::const_iterator it
= d_quants_prereg
.find(q
);
774 if (it
!= d_quants_prereg
.end())
778 Trace("quant-debug") << "QuantifiersEngine : Pre-register " << q
<< std::endl
;
779 d_quants_prereg
.insert(q
);
781 if (reduceQuantifier(q
))
783 // if we can reduce it, nothing left to do
786 // ensure that it is registered
787 registerQuantifierInternal(q
);
788 // register with each module
789 for (QuantifiersModule
*& mdl
: d_modules
)
791 Trace("quant-debug") << "pre-register with " << mdl
->identify() << "..."
793 mdl
->preRegisterQuantifier(q
);
797 Trace("quant-debug") << "...finish pre-register " << q
<< "..." << std::endl
;
800 void QuantifiersEngine::registerPattern( std::vector
<Node
> & pattern
) {
801 for(std::vector
<Node
>::iterator p
= pattern
.begin(); p
!= pattern
.end(); ++p
){
802 std::set
< Node
> added
;
803 getTermDatabase()->addTerm( *p
, added
);
807 void QuantifiersEngine::assertQuantifier( Node f
, bool pol
){
808 if (reduceQuantifier(f
))
810 // if we can reduce it, nothing left to do
815 TrustNode lem
= d_skolemize
->process(f
);
818 if (Trace
.isOn("quantifiers-sk-debug"))
820 Node slem
= Rewriter::rewrite(lem
.getNode());
821 Trace("quantifiers-sk-debug")
822 << "Skolemize lemma : " << slem
<< std::endl
;
824 getOutputChannel().trustedLemma(
825 lem
, LemmaProperty::PREPROCESS
| LemmaProperty::NEEDS_JUSTIFY
);
829 // ensure the quantified formula is registered
830 registerQuantifierInternal(f
);
831 // assert it to each module
832 d_model
->assertQuantifier(f
);
833 for (QuantifiersModule
*& mdl
: d_modules
)
837 addTermToDatabase(d_term_util
->getInstConstantBody(f
), true);
840 void QuantifiersEngine::addTermToDatabase( Node n
, bool withinQuant
, bool withinInstClosure
){
841 if( options::incrementalSolving() ){
842 if( d_presolve_in
.find( n
)==d_presolve_in
.end() ){
843 d_presolve_in
.insert( n
);
844 d_presolve_cache
.push_back( n
);
845 d_presolve_cache_wq
.push_back( withinQuant
);
846 d_presolve_cache_wic
.push_back( withinInstClosure
);
849 //only wait if we are doing incremental solving
850 if( !d_presolve
|| !options::incrementalSolving() ){
851 std::set
< Node
> added
;
852 d_term_db
->addTerm(n
, added
, withinQuant
, withinInstClosure
);
856 if (d_sygus_tdb
&& options::sygusEvalUnfold())
858 d_sygus_tdb
->getEvalUnfold()->registerEvalTerm(n
);
864 void QuantifiersEngine::eqNotifyNewClass(TNode t
) {
865 addTermToDatabase( t
);
868 bool QuantifiersEngine::addLemma( Node lem
, bool doCache
, bool doRewrite
){
871 lem
= Rewriter::rewrite(lem
);
873 Trace("inst-add-debug") << "Adding lemma : " << lem
<< std::endl
;
874 BoolMap::const_iterator itp
= d_lemmas_produced_c
.find( lem
);
875 if( itp
==d_lemmas_produced_c
.end() || !(*itp
).second
){
876 d_lemmas_produced_c
[ lem
] = true;
877 d_lemmas_waiting
.push_back( lem
);
878 Trace("inst-add-debug") << "Added lemma" << std::endl
;
881 Trace("inst-add-debug") << "Duplicate." << std::endl
;
885 //do not need to rewrite, will be rewritten after sending
886 d_lemmas_waiting
.push_back( lem
);
891 bool QuantifiersEngine::addTrustedLemma(TrustNode tlem
,
895 Node lem
= tlem
.getProven();
896 if (!addLemma(lem
, doCache
, doRewrite
))
900 d_lemmasWaitingPg
[lem
] = tlem
.getGenerator();
904 bool QuantifiersEngine::removeLemma( Node lem
) {
905 std::vector
< Node
>::iterator it
= std::find( d_lemmas_waiting
.begin(), d_lemmas_waiting
.end(), lem
);
906 if( it
!=d_lemmas_waiting
.end() ){
907 d_lemmas_waiting
.erase( it
, it
+ 1 );
908 d_lemmas_produced_c
[ lem
] = false;
915 void QuantifiersEngine::addRequirePhase( Node lit
, bool req
){
916 d_phase_req_waiting
[lit
] = req
;
919 void QuantifiersEngine::markRelevant( Node q
) {
920 d_model
->markRelevant( q
);
922 bool QuantifiersEngine::hasAddedLemma() const
924 return !d_lemmas_waiting
.empty() || d_hasAddedLemma
;
926 bool QuantifiersEngine::theoryEngineNeedsCheck() const
928 return d_te
->needCheck();
931 void QuantifiersEngine::setConflict()
937 bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e
) {
938 Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter
<< ", " << d_ierCounter_lc
<< std::endl
;
939 //determine if we should perform check, based on instWhenMode
940 bool performCheck
= false;
941 if (options::instWhenMode() == options::InstWhenMode::FULL
)
943 performCheck
= ( e
>= Theory::EFFORT_FULL
);
945 else if (options::instWhenMode() == options::InstWhenMode::FULL_DELAY
)
947 performCheck
= (e
>= Theory::EFFORT_FULL
) && !theoryEngineNeedsCheck();
949 else if (options::instWhenMode() == options::InstWhenMode::FULL_LAST_CALL
)
951 performCheck
= ( ( e
==Theory::EFFORT_FULL
&& d_ierCounter
%d_inst_when_phase
!=0 ) || e
==Theory::EFFORT_LAST_CALL
);
953 else if (options::instWhenMode()
954 == options::InstWhenMode::FULL_DELAY_LAST_CALL
)
956 performCheck
= ((e
== Theory::EFFORT_FULL
&& !theoryEngineNeedsCheck()
957 && d_ierCounter
% d_inst_when_phase
!= 0)
958 || e
== Theory::EFFORT_LAST_CALL
);
960 else if (options::instWhenMode() == options::InstWhenMode::LAST_CALL
)
962 performCheck
= ( e
>= Theory::EFFORT_LAST_CALL
);
971 options::UserPatMode
QuantifiersEngine::getInstUserPatMode()
973 if (options::userPatternsQuant() == options::UserPatMode::INTERLEAVE
)
975 return d_ierCounter
% 2 == 0 ? options::UserPatMode::USE
976 : options::UserPatMode::RESORT
;
980 return options::userPatternsQuant();
984 void QuantifiersEngine::flushLemmas(){
985 OutputChannel
& out
= getOutputChannel();
986 if( !d_lemmas_waiting
.empty() ){
987 //take default output channel if none is provided
988 d_hasAddedLemma
= true;
989 std::map
<Node
, ProofGenerator
*>::iterator itp
;
990 // Note: Do not use foreach loop here and do not cache size() call.
991 // New lemmas can be added while iterating over d_lemmas_waiting.
992 for (size_t i
= 0; i
< d_lemmas_waiting
.size(); ++i
)
994 const Node
& lemw
= d_lemmas_waiting
[i
];
995 Trace("qe-lemma") << "Lemma : " << lemw
<< std::endl
;
996 itp
= d_lemmasWaitingPg
.find(lemw
);
997 if (itp
!= d_lemmasWaitingPg
.end())
999 TrustNode tlemw
= TrustNode::mkTrustLemma(lemw
, itp
->second
);
1000 out
.trustedLemma(tlemw
, LemmaProperty::PREPROCESS
);
1004 out
.lemma(lemw
, LemmaProperty::PREPROCESS
);
1007 d_lemmas_waiting
.clear();
1009 if( !d_phase_req_waiting
.empty() ){
1010 for( std::map
< Node
, bool >::iterator it
= d_phase_req_waiting
.begin(); it
!= d_phase_req_waiting
.end(); ++it
){
1011 Trace("qe-lemma") << "Require phase : " << it
->first
<< " -> " << it
->second
<< std::endl
;
1012 out
.requirePhase(it
->first
, it
->second
);
1014 d_phase_req_waiting
.clear();
1018 void QuantifiersEngine::getInstantiationTermVectors( Node q
, std::vector
< std::vector
< Node
> >& tvecs
) {
1019 d_instantiate
->getInstantiationTermVectors(q
, tvecs
);
1022 void QuantifiersEngine::getInstantiationTermVectors( std::map
< Node
, std::vector
< std::vector
< Node
> > >& insts
) {
1023 d_instantiate
->getInstantiationTermVectors(insts
);
1026 void QuantifiersEngine::printInstantiations( std::ostream
& out
) {
1027 bool printed
= false;
1028 // print the skolemizations
1029 if (options::printInstMode() == options::PrintInstMode::LIST
)
1031 if (d_skolemize
->printSkolemization(out
))
1036 // print the instantiations
1037 if (d_instantiate
->printInstantiations(out
))
1042 out
<< "No instantiations" << std::endl
;
1046 void QuantifiersEngine::printSynthSolution( std::ostream
& out
) {
1047 if (d_qmodules
->d_synth_e
)
1049 d_qmodules
->d_synth_e
->printSynthSolution(out
);
1051 out
<< "Internal error : module for synth solution not found." << std::endl
;
1055 void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector
< Node
>& qs
) {
1056 d_instantiate
->getInstantiatedQuantifiedFormulas(qs
);
1059 QuantifiersEngine::Statistics::Statistics()
1060 : d_time("theory::QuantifiersEngine::time"),
1061 d_qcf_time("theory::QuantifiersEngine::time_qcf"),
1062 d_ematching_time("theory::QuantifiersEngine::time_ematching"),
1063 d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
1064 d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
1065 d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
1066 d_triggers("QuantifiersEngine::Triggers", 0),
1067 d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
1068 d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
1069 d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0),
1070 d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0),
1071 d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0),
1072 d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0),
1073 d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0),
1074 d_instantiations_qcf("QuantifiersEngine::Instantiations_Qcf_Conflict", 0),
1075 d_instantiations_qcf_prop("QuantifiersEngine::Instantiations_Qcf_Prop", 0),
1076 d_instantiations_fmf_exh("QuantifiersEngine::Instantiations_Fmf_Exh", 0),
1077 d_instantiations_fmf_mbqi("QuantifiersEngine::Instantiations_Fmf_Mbqi", 0),
1078 d_instantiations_cbqi("QuantifiersEngine::Instantiations_Cbqi", 0),
1079 d_instantiations_rr("QuantifiersEngine::Instantiations_Rewrite_Rules", 0)
1081 smtStatisticsRegistry()->registerStat(&d_time
);
1082 smtStatisticsRegistry()->registerStat(&d_qcf_time
);
1083 smtStatisticsRegistry()->registerStat(&d_ematching_time
);
1084 smtStatisticsRegistry()->registerStat(&d_num_quant
);
1085 smtStatisticsRegistry()->registerStat(&d_instantiation_rounds
);
1086 smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc
);
1087 smtStatisticsRegistry()->registerStat(&d_triggers
);
1088 smtStatisticsRegistry()->registerStat(&d_simple_triggers
);
1089 smtStatisticsRegistry()->registerStat(&d_multi_triggers
);
1090 smtStatisticsRegistry()->registerStat(&d_multi_trigger_instantiations
);
1091 smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv
);
1092 smtStatisticsRegistry()->registerStat(&d_instantiations_user_patterns
);
1093 smtStatisticsRegistry()->registerStat(&d_instantiations_auto_gen
);
1094 smtStatisticsRegistry()->registerStat(&d_instantiations_guess
);
1095 smtStatisticsRegistry()->registerStat(&d_instantiations_qcf
);
1096 smtStatisticsRegistry()->registerStat(&d_instantiations_qcf_prop
);
1097 smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_exh
);
1098 smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_mbqi
);
1099 smtStatisticsRegistry()->registerStat(&d_instantiations_cbqi
);
1100 smtStatisticsRegistry()->registerStat(&d_instantiations_rr
);
1103 QuantifiersEngine::Statistics::~Statistics(){
1104 smtStatisticsRegistry()->unregisterStat(&d_time
);
1105 smtStatisticsRegistry()->unregisterStat(&d_qcf_time
);
1106 smtStatisticsRegistry()->unregisterStat(&d_ematching_time
);
1107 smtStatisticsRegistry()->unregisterStat(&d_num_quant
);
1108 smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds
);
1109 smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc
);
1110 smtStatisticsRegistry()->unregisterStat(&d_triggers
);
1111 smtStatisticsRegistry()->unregisterStat(&d_simple_triggers
);
1112 smtStatisticsRegistry()->unregisterStat(&d_multi_triggers
);
1113 smtStatisticsRegistry()->unregisterStat(&d_multi_trigger_instantiations
);
1114 smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv
);
1115 smtStatisticsRegistry()->unregisterStat(&d_instantiations_user_patterns
);
1116 smtStatisticsRegistry()->unregisterStat(&d_instantiations_auto_gen
);
1117 smtStatisticsRegistry()->unregisterStat(&d_instantiations_guess
);
1118 smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf
);
1119 smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf_prop
);
1120 smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_exh
);
1121 smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_mbqi
);
1122 smtStatisticsRegistry()->unregisterStat(&d_instantiations_cbqi
);
1123 smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr
);
1126 eq::EqualityEngine
* QuantifiersEngine::getMasterEqualityEngine() const
1128 return d_masterEqualityEngine
;
1131 Node
QuantifiersEngine::getInternalRepresentative( Node a
, Node q
, int index
){
1132 return d_eq_query
->getInternalRepresentative(a
, q
, index
);
1135 bool QuantifiersEngine::getSynthSolutions(
1136 std::map
<Node
, std::map
<Node
, Node
> >& sol_map
)
1138 return d_qmodules
->d_synth_e
->getSynthSolutions(sol_map
);
1141 void QuantifiersEngine::debugPrintEqualityEngine( const char * c
) {
1142 eq::EqualityEngine
* ee
= getMasterEqualityEngine();
1143 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( ee
);
1144 std::map
< TypeNode
, int > typ_num
;
1145 while( !eqcs_i
.isFinished() ){
1146 TNode r
= (*eqcs_i
);
1147 TypeNode tr
= r
.getType();
1148 if( typ_num
.find( tr
)==typ_num
.end() ){
1152 bool firstTime
= true;
1153 Trace(c
) << " " << r
;
1154 Trace(c
) << " : { ";
1155 eq::EqClassIterator eqc_i
= eq::EqClassIterator( r
, ee
);
1156 while( !eqc_i
.isFinished() ){
1160 Trace(c
) << std::endl
;
1163 Trace(c
) << " " << n
<< std::endl
;
1167 if( !firstTime
){ Trace(c
) << " "; }
1168 Trace(c
) << "}" << std::endl
;
1171 Trace(c
) << std::endl
;
1172 for( std::map
< TypeNode
, int >::iterator it
= typ_num
.begin(); it
!= typ_num
.end(); ++it
){
1173 Trace(c
) << "# eqc for " << it
->first
<< " : " << it
->second
<< std::endl
;
1177 } // namespace theory