From: Andrew Reynolds Date: Wed, 27 Jan 2021 01:24:58 +0000 (-0600) Subject: Use standard conflict mechanism in quantifiers state (#5822) X-Git-Tag: cvc5-1.0.0~2351 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=524c2d9f44a7c4297422dd1356fe3dc377166180;p=cvc5.git Use standard conflict mechanism in quantifiers state (#5822) Work towards eliminating dependencies on quantifiers engine, this updates quantifiers module to use the standard SAT-context dependent flag in quantifiers state instead of the one in QuantifiersEngine. It also eliminates the use of a custom call to theoryEngineNeedsCheck. --- 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 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; } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index fa7e50e1c..83aafe33a 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -51,7 +51,6 @@ QuantifiersEngine::QuantifiersEngine( d_instantiate(new quantifiers::Instantiate(this, qstate, pnm)), d_skolemize(new quantifiers::Skolemize(this, qstate, pnm)), d_term_enum(new quantifiers::TermEnumeration), - d_conflict_c(qstate.getSatContext(), false), d_quants_prereg(qstate.getUserContext()), d_quants_red(qstate.getUserContext()), d_lemmas_produced_c(qstate.getUserContext()), @@ -77,7 +76,6 @@ QuantifiersEngine::QuantifiersEngine( d_util.push_back(d_instantiate.get()); d_curr_effort_level = QuantifiersModule::QEFFORT_NONE; - d_conflict = false; d_hasAddedLemma = false; //don't add true lemma d_lemmas_produced_c[d_term_util->d_true] = true; @@ -107,12 +105,12 @@ QuantifiersEngine::QuantifiersEngine( Trace("quant-engine-debug") << "...make fmc builder." << std::endl; d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc( this, qstate, "FirstOrderModelFmc")); - d_builder.reset(new quantifiers::fmcheck::FullModelChecker(this)); + d_builder.reset(new quantifiers::fmcheck::FullModelChecker(this, qstate)); }else{ Trace("quant-engine-debug") << "...make default model builder." << std::endl; d_model.reset( new quantifiers::FirstOrderModel(this, qstate, "FirstOrderModel")); - d_builder.reset(new quantifiers::QModelBuilder(this)); + d_builder.reset(new quantifiers::QModelBuilder(this, qstate)); } }else{ d_model.reset( @@ -150,10 +148,7 @@ OutputChannel& QuantifiersEngine::getOutputChannel() return d_te->theoryOf(THEORY_QUANTIFIERS)->getOutputChannel(); } /** get default valuation for the quantifiers engine */ -Valuation& QuantifiersEngine::getValuation() -{ - return d_te->theoryOf(THEORY_QUANTIFIERS)->getValuation(); -} +Valuation& QuantifiersEngine::getValuation() { return d_qstate.getValuation(); } const LogicInfo& QuantifiersEngine::getLogicInfo() const { @@ -372,7 +367,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl; return; } - if (d_conflict_c.get()) + if (d_qstate.isInConflict()) { if (e < Theory::EFFORT_LAST_CALL) { @@ -417,7 +412,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } - d_conflict = false; d_hasAddedLemma = false; bool setIncomplete = false; @@ -448,11 +442,11 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine-debug") << " lemmas waiting = " << d_lemmas_waiting.size() << std::endl; } Trace("quant-engine-debug") - << " Theory engine finished : " << !theoryEngineNeedsCheck() - << std::endl; + << " Theory engine finished : " + << !d_qstate.getValuation().needCheck() << std::endl; Trace("quant-engine-debug") << " Needs model effort : " << needsModelE << std::endl; Trace("quant-engine-debug") - << " In conflict : " << d_conflict << std::endl; + << " In conflict : " << d_qstate.isInConflict() << std::endl; } if( Trace.isOn("quant-engine-ee-pre") ){ Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl; @@ -538,7 +532,8 @@ void QuantifiersEngine::check( Theory::Effort e ){ << " at effort " << quant_e << "..." << std::endl; mdl->check(e, quant_e); - if( d_conflict ){ + if (d_qstate.isInConflict()) + { Trace("quant-engine-debug") << "...conflict!" << std::endl; break; } @@ -550,7 +545,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ if( d_hasAddedLemma ){ break; }else{ - Assert(!d_conflict); + Assert(!d_qstate.isInConflict()); if (quant_e == QuantifiersModule::QEFFORT_CONFLICT) { if( e==Theory::EFFORT_FULL ){ @@ -578,7 +573,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ setIncomplete = true; } } - if (d_conflict_c.get()) + if (d_qstate.isInConflict()) { // we reported a conflicting lemma, should return setIncomplete = true; @@ -900,20 +895,13 @@ void QuantifiersEngine::addRequirePhase( Node lit, bool req ){ void QuantifiersEngine::markRelevant( Node q ) { d_model->markRelevant( q ); } + bool QuantifiersEngine::hasAddedLemma() const { return !d_lemmas_waiting.empty() || d_hasAddedLemma; } -bool QuantifiersEngine::theoryEngineNeedsCheck() const -{ - return d_te->needCheck(); -} -void QuantifiersEngine::setConflict() -{ - d_conflict = true; - d_conflict_c = true; -} +bool QuantifiersEngine::inConflict() const { return d_qstate.isInConflict(); } bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) { Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl; @@ -925,7 +913,8 @@ bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) { } else if (options::instWhenMode() == options::InstWhenMode::FULL_DELAY) { - performCheck = (e >= Theory::EFFORT_FULL) && !theoryEngineNeedsCheck(); + performCheck = + (e >= Theory::EFFORT_FULL) && !d_qstate.getValuation().needCheck(); } else if (options::instWhenMode() == options::InstWhenMode::FULL_LAST_CALL) { @@ -934,9 +923,10 @@ bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) { else if (options::instWhenMode() == options::InstWhenMode::FULL_DELAY_LAST_CALL) { - performCheck = ((e == Theory::EFFORT_FULL && !theoryEngineNeedsCheck() - && d_ierCounter % d_inst_when_phase != 0) - || e == Theory::EFFORT_LAST_CALL); + performCheck = + ((e == Theory::EFFORT_FULL && !d_qstate.getValuation().needCheck() + && d_ierCounter % d_inst_when_phase != 0) + || e == Theory::EFFORT_LAST_CALL); } else if (options::instWhenMode() == options::InstWhenMode::LAST_CALL) { diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 5a371ff09..2790ad11a 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -234,17 +234,8 @@ public: void markRelevant(Node q); /** has added lemma */ bool hasAddedLemma() const; - /** theory engine needs check - * - * This is true if the theory engine has more constraints to process. When - * it is false, we are tentatively going to terminate solving with - * sat/unknown. For details, see TheoryEngine::needCheck. - */ - bool theoryEngineNeedsCheck() const; /** is in conflict */ - bool inConflict() { return d_conflict; } - /** set conflict */ - void setConflict(); + bool inConflict() const; /** get current q effort */ QuantifiersModule::QEffort getCurrentQEffort() { return d_curr_effort_level; } /** get number of waiting lemmas */ @@ -384,9 +375,6 @@ public: //------------- temporary information during check /** current effort level */ QuantifiersModule::QEffort d_curr_effort_level; - /** are we in conflict */ - bool d_conflict; - context::CDO d_conflict_c; /** has added lemma this round */ bool d_hasAddedLemma; //------------- end temporary information during check diff --git a/src/theory/theory_state.cpp b/src/theory/theory_state.cpp index 95a96808e..47528e1a6 100644 --- a/src/theory/theory_state.cpp +++ b/src/theory/theory_state.cpp @@ -137,5 +137,7 @@ bool TheoryState::hasSatValue(TNode n, bool& value) const return d_valuation.hasSatValue(n, value); } +Valuation& TheoryState::getValuation() { return d_valuation; } + } // namespace theory } // namespace CVC4 diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h index 187d586a1..7c2a044bf 100644 --- a/src/theory/theory_state.h +++ b/src/theory/theory_state.h @@ -83,6 +83,9 @@ class TheoryState /** Returns true if n has a current SAT assignment and stores it in value. */ virtual bool hasSatValue(TNode n, bool& value) const; + /** Get the underlying valuation class */ + Valuation& getValuation(); + protected: /** Pointer to the SAT context object used by the theory. */ context::Context* d_context;