diff options
Diffstat (limited to 'src/theory/quantifiers')
19 files changed, 83 insertions, 47 deletions
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 980bc1d4b..118e7023c 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -254,7 +254,7 @@ void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e) { if (quant_e == QEFFORT_STANDARD) { - Assert(!d_quantEngine->inConflict()); + Assert(!d_qstate.isInConflict()); double clSet = 0; if( Trace.isOn("cegqi-engine") ){ clSet = double(clock())/double(CLOCKS_PER_SEC); @@ -269,12 +269,14 @@ void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e) Node q = it->first; Trace("cegqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl; process(q, e, ee); - if (d_quantEngine->inConflict()) + if (d_qstate.isInConflict()) { break; } } - if( d_quantEngine->inConflict() || d_quantEngine->getNumLemmasWaiting()>lastWaiting ){ + if (d_qstate.isInConflict() + || d_quantEngine->getNumLemmasWaiting() > lastWaiting) + { break; } } diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h index 0a4c1b76f..916790d9c 100644 --- a/src/theory/quantifiers/ematching/inst_strategy.h +++ b/src/theory/quantifiers/ematching/inst_strategy.h @@ -28,6 +28,8 @@ class QuantifiersEngine; namespace quantifiers { +class QuantifiersState; + /** A status response to process */ enum class InstStrategyStatus { @@ -43,7 +45,10 @@ enum class InstStrategyStatus class InstStrategy { public: - InstStrategy(QuantifiersEngine* qe) : d_quantEngine(qe) {} + InstStrategy(QuantifiersEngine* qe, QuantifiersState& qs) + : d_quantEngine(qe), d_qstate(qs) + { + } virtual ~InstStrategy() {} /** presolve */ virtual void presolve() {} @@ -57,6 +62,8 @@ class InstStrategy protected: /** reference to the instantiation engine */ QuantifiersEngine* d_quantEngine; + /** The quantifiers state object */ + QuantifiersState& d_qstate; }; /* class InstStrategy */ } // namespace quantifiers diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 8091eded5..362888558 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -58,8 +58,9 @@ struct sortTriggers { }; InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers(QuantifiersEngine* qe, + QuantifiersState& qs, QuantRelevance* qr) - : InstStrategy(qe), d_quant_rel(qr) + : InstStrategy(qe, qs), d_quant_rel(qr) { //how to select trigger terms d_tr_strategy = options::triggerSelMode(); @@ -202,13 +203,12 @@ InstStrategyStatus InstStrategyAutoGenTriggers::process(Node f, { d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst; } - if (d_quantEngine->inConflict()) + if (d_qstate.isInConflict()) { break; } } - if (d_quantEngine->inConflict() - || (hasInst && options::multiTriggerPriority())) + if (d_qstate.isInConflict() || (hasInst && options::multiTriggerPriority())) { break; } diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h index d3c7c2c67..ac3c60ffe 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -85,7 +85,9 @@ class InstStrategyAutoGenTriggers : public InstStrategy std::map<Node, bool> d_hasUserPatterns; public: - InstStrategyAutoGenTriggers(QuantifiersEngine* qe, QuantRelevance* qr); + InstStrategyAutoGenTriggers(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantRelevance* qr); ~InstStrategyAutoGenTriggers() {} /** get auto-generated trigger */ diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp index f7f2531bb..581a29697 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp @@ -23,8 +23,9 @@ namespace CVC4 { namespace theory { namespace quantifiers { -InstStrategyUserPatterns::InstStrategyUserPatterns(QuantifiersEngine* ie) - : InstStrategy(ie) +InstStrategyUserPatterns::InstStrategyUserPatterns(QuantifiersEngine* ie, + QuantifiersState& qs) + : InstStrategy(ie, qs) { } InstStrategyUserPatterns::~InstStrategyUserPatterns() {} @@ -128,7 +129,7 @@ InstStrategyStatus InstStrategyUserPatterns::process(Node q, { d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst; } - if (d_quantEngine->inConflict()) + if (d_qstate.isInConflict()) { // we are already in conflict break; diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h index ed0cd0ac6..3d7ddd97b 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h @@ -33,7 +33,7 @@ namespace quantifiers { class InstStrategyUserPatterns : public InstStrategy { public: - InstStrategyUserPatterns(QuantifiersEngine* qe); + InstStrategyUserPatterns(QuantifiersEngine* qe, QuantifiersState& qs); ~InstStrategyUserPatterns(); /** add pattern */ void addUserPattern(Node q, Node pat); diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index 382cb233f..cd0ab7976 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -53,13 +53,13 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe, // user-provided patterns if (options::userPatternsQuant() != options::UserPatMode::IGNORE) { - d_isup.reset(new InstStrategyUserPatterns(d_quantEngine)); + d_isup.reset(new InstStrategyUserPatterns(d_quantEngine, qs)); d_instStrategies.push_back(d_isup.get()); } // auto-generated patterns d_i_ag.reset( - new InstStrategyAutoGenTriggers(d_quantEngine, d_quant_rel.get())); + new InstStrategyAutoGenTriggers(d_quantEngine, qs, d_quant_rel.get())); d_instStrategies.push_back(d_i_ag.get()); } } diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index effb5938c..b2c7bf704 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -280,7 +280,8 @@ void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) { } } -FullModelChecker::FullModelChecker(QuantifiersEngine* qe) : QModelBuilder(qe) +FullModelChecker::FullModelChecker(QuantifiersEngine* qe, QuantifiersState& qs) + : QModelBuilder(qe, qs) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -593,7 +594,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl; // register the quantifier registerQuantifiedFormula(f); - Assert(!d_qe->inConflict()); + Assert(!d_qstate.isInConflict()); // we do not do model-based quantifier instantiation if the option // disables it, or if the quantified formula has an unhandled type. if (!optUseModel() || !isHandled(f)) @@ -708,7 +709,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i { Trace("fmc-debug-inst") << "** Added instantiation." << std::endl; d_addedLemmas++; - if (d_qe->inConflict() || options::fmfOneInstPerRound()) + if (d_qstate.isInConflict() || options::fmfOneInstPerRound()) { break; } @@ -850,7 +851,8 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No { Trace("fmc-exh-debug") << " ...success."; addedLemmas++; - if( d_qe->inConflict() || options::fmfOneInstPerRound() ){ + if (d_qstate.isInConflict() || options::fmfOneInstPerRound()) + { break; } }else{ diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index 89a472948..76c131369 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -149,7 +149,7 @@ private: Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn ); public: - FullModelChecker(QuantifiersEngine* qe); + FullModelChecker(QuantifiersEngine* qe, QuantifiersState& qs); void debugPrintCond(const char * tr, Node n, bool dispStar = false); void debugPrint(const char * tr, Node n, bool dispStar = false); diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index 4f34c3baa..cdb65f2b2 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -29,11 +29,12 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; -QModelBuilder::QModelBuilder(QuantifiersEngine* qe) +QModelBuilder::QModelBuilder(QuantifiersEngine* qe, QuantifiersState& qs) : TheoryEngineModelBuilder(qe->getTheoryEngine()), d_qe(qe), d_addedLemmas(0), - d_triedLemmas(0) + d_triedLemmas(0), + d_qstate(qs) { } diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index 16e6f2a0b..82f9fa6c3 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -20,6 +20,7 @@ #include "expr/node.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/inst_match.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/theory_model_builder.h" namespace CVC4 { @@ -40,7 +41,7 @@ class QModelBuilder : public TheoryEngineModelBuilder unsigned d_triedLemmas; public: - QModelBuilder(QuantifiersEngine* qe); + QModelBuilder(QuantifiersEngine* qe, QuantifiersState& qs); //do exhaustive instantiation // 0 : failed, but resorting to true exhaustive instantiation may work @@ -56,6 +57,10 @@ class QModelBuilder : public TheoryEngineModelBuilder //statistics unsigned getNumAddedLemmas() { return d_addedLemmas; } unsigned getNumTriedLemmas() { return d_triedLemmas; } + + protected: + /** The quantifiers state object */ + QuantifiersState& d_qstate; }; }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 3849dc2c6..4d74c1697 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -77,7 +77,7 @@ void ModelEngine::check(Theory::Effort e, QEffort quant_e) doCheck = quant_e == QEFFORT_MODEL; } if( doCheck ){ - Assert(!d_quantEngine->inConflict()); + Assert(!d_qstate.isInConflict()); int addedLemmas = 0; //the following will test that the model satisfies all asserted universal quantifiers by @@ -217,7 +217,7 @@ int ModelEngine::checkModel(){ //determine if we should check this quantifier if( d_quantEngine->getModel()->isQuantifierActive( q ) && d_quantEngine->hasOwnership( q, this ) ){ exhaustiveInstantiate( q, e ); - if (d_quantEngine->inConflict()) + if (d_qstate.isInConflict()) { break; } @@ -228,12 +228,13 @@ int ModelEngine::checkModel(){ if( d_addedLemmas>0 ){ break; }else{ - Assert(!d_quantEngine->inConflict()); + Assert(!d_qstate.isInConflict()); } } //print debug information - if( d_quantEngine->inConflict() ){ + if (d_qstate.isInConflict()) + { Trace("model-engine") << "Conflict, added lemmas = "; }else{ Trace("model-engine") << "Added Lemmas = "; @@ -293,7 +294,8 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ if (inst->addInstantiation(f, m, true)) { addedLemmas++; - if( d_quantEngine->inConflict() ){ + if (d_qstate.isInConflict()) + { break; } }else{ diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index 1dff5e000..d1c09a9e8 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -80,7 +80,7 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) } if (options::fullSaturateQuant() && !doCheck) { - if (!d_quantEngine->theoryEngineNeedsCheck()) + if (!d_qstate.getValuation().needCheck()) { doCheck = quant_e == QEFFORT_LAST_CALL; fullEffort = true; @@ -91,7 +91,7 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) { return; } - Assert(!d_quantEngine->inConflict()); + Assert(!d_qstate.isInConflict()); double clSet = 0; if (Trace.isOn("fs-engine")) { @@ -145,13 +145,13 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) // added lemma addedLemmas++; } - if (d_quantEngine->inConflict()) + if (d_qstate.isInConflict()) { break; } } } - if (d_quantEngine->inConflict() + if (d_qstate.isInConflict() || (addedLemmas > 0 && options::fullSaturateStratify())) { // we break if we are in conflict, or if we added any lemma at this @@ -331,7 +331,7 @@ bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd) { index--; } - if (d_quantEngine->inConflict()) + if (d_qstate.isInConflict()) { // could be conflicting for an internal reason (such as term // indices computed in above calls) diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index b123c3e15..ed02c6b32 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -105,7 +105,7 @@ bool Instantiate::addInstantiation( { // For resource-limiting (also does a time check). d_qe->getOutputChannel().safePoint(ResourceManager::Resource::QuantifierStep); - Assert(!d_qe->inConflict()); + Assert(!d_qstate.isInConflict()); Assert(terms.size() == q[0].getNumChildren()); Assert(d_term_db != nullptr); Assert(d_term_util != nullptr); diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 822c9b323..b214f907a 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -637,7 +637,7 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p, } } // spurious if quantifiers engine is in conflict - return p->d_quantEngine->inConflict(); + return p->d_qstate.isInConflict(); } bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) { @@ -1203,27 +1203,27 @@ bool MatchGen::reset_round(QuantConflictFind* p) //} // modified TermDb* tdb = p->getTermDatabase(); - QuantifiersEngine* qe = p->getQuantifiersEngine(); + QuantifiersState& qs = p->getState(); for (unsigned i = 0; i < 2; i++) { if (tdb->isEntailed(d_n, i == 0)) { d_ground_eval[0] = i==0 ? p->d_true : p->d_false; } - if (qe->inConflict()) + if (qs.isInConflict()) { return false; } } }else if( d_type==typ_eq ){ TermDb* tdb = p->getTermDatabase(); - QuantifiersEngine* qe = p->getQuantifiersEngine(); + QuantifiersState& qs = p->getState(); for (unsigned i = 0, size = d_n.getNumChildren(); i < size; i++) { if (!expr::hasBoundVar(d_n[i])) { TNode t = tdb->getEntailedTerm(d_n[i]); - if (qe->inConflict()) + if (qs.isInConflict()) { return false; } @@ -2027,7 +2027,7 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e) { // check this quantified formula checkQuantifiedFormula(q, isConflict, addedLemmas); - if (d_conflict || d_quantEngine->inConflict()) + if (d_conflict || d_qstate.isInConflict()) { break; } @@ -2036,7 +2036,7 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e) // We are done if we added a lemma, or discovered a conflict in another // way. An example of the latter case is when two disequal congruent terms // are discovered during term indexing. - if (addedLemmas > 0 || d_quantEngine->inConflict()) + if (addedLemmas > 0 || d_qstate.isInConflict()) { break; } @@ -2100,7 +2100,7 @@ void QuantConflictFind::checkQuantifiedFormula(Node q, Instantiate* qinst = d_quantEngine->getInstantiate(); while (qi->getNextMatch(this)) { - if (d_quantEngine->inConflict()) + if (d_qstate.isInConflict()) { Trace("qcf-check") << " ... Quantifiers engine discovered conflict, "; Trace("qcf-check") << "probably related to disequal congruent terms in " diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index dcf38eccb..b561b589b 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -71,6 +71,17 @@ quantifiers::TermUtil* QuantifiersModule::getTermUtil() const return d_quantEngine->getTermUtil(); } +quantifiers::QuantifiersState& QuantifiersModule::getState() +{ + return d_qstate; +} + +quantifiers::QuantifiersInferenceManager& +QuantifiersModule::getInferenceManager() +{ + return d_qim; +} + QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){ initialize( n, computeEq ); } diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 5040bd232..16791b130 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -156,6 +156,10 @@ class QuantifiersModule { quantifiers::TermDb* getTermDatabase() const; /** get currently used term utility object */ quantifiers::TermUtil* getTermUtil() const; + /** get the quantifiers state */ + quantifiers::QuantifiersState& getState(); + /** get the quantifiers inference manager */ + quantifiers::QuantifiersInferenceManager& getInferenceManager(); //----------------------------end general queries protected: /** pointer to the quantifiers engine that owns this module */ diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index fc1bda579..43051eb99 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -136,8 +136,7 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e) activeCheckConj.clear(); activeCheckConj = acnext; acnext.clear(); - } while (!activeCheckConj.empty() - && !d_quantEngine->theoryEngineNeedsCheck()); + } while (!activeCheckConj.empty() && !d_qstate.getValuation().needCheck()); Trace("sygus-engine") << "Finished Counterexample Guided Instantiation engine." << std::endl; } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 12cdb1b8c..075ec6ceb 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -410,7 +410,7 @@ void TermDb::computeUfTerms( TNode f ) { { Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " << n << "!!!!" << std::endl; - if (!d_quantEngine->theoryEngineNeedsCheck()) + if (!d_qstate.getValuation().needCheck()) { Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl; @@ -419,7 +419,7 @@ void TermDb::computeUfTerms( TNode f ) { Trace("term-db-lemma") << " add lemma : " << lem << std::endl; } d_quantEngine->addLemma(lem); - d_quantEngine->setConflict(); + d_qstate.notifyInConflict(); d_consistent_ee = false; return; } @@ -1062,7 +1062,7 @@ bool TermDb::reset( Theory::Effort effort ){ Trace("term-db-lemma") << "Purify equality lemma: " << eq << std::endl; d_quantEngine->addLemma(eq); - d_quantEngine->setConflict(); + d_qstate.notifyInConflict(); d_consistent_ee = false; return false; } |