From: Andrew Reynolds Date: Fri, 27 May 2022 20:56:15 +0000 (-0500) Subject: Eliminate static options access for central ee (#8823) X-Git-Tag: cvc5-1.0.1~87 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=17049dc8c6e2f9a9e306fbd7fcfc92a0aff1dd5f;p=cvc5.git Eliminate static options access for central ee (#8823) Also refactors TheoryEngine to not maintain its own reference to logic info and an accessor to it. Towards eliminating option scopes. --- diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp index 9847725c8..07755344f 100644 --- a/src/theory/combination_engine.cpp +++ b/src/theory/combination_engine.cpp @@ -35,7 +35,7 @@ CombinationEngine::CombinationEngine(Env& env, d_te(te), d_valuation(&te), d_pnm(env.isTheoryProofProducing() ? env.getProofNodeManager() : nullptr), - d_logicInfo(te.getLogicInfo()), + d_logicInfo(env.getLogicInfo()), d_paraTheories(paraTheories), d_eemanager(nullptr), d_mmanager(nullptr), diff --git a/src/theory/ee_manager_central.cpp b/src/theory/ee_manager_central.cpp index cef387f3c..02488604e 100644 --- a/src/theory/ee_manager_central.cpp +++ b/src/theory/ee_manager_central.cpp @@ -15,6 +15,8 @@ #include "theory/ee_manager_central.h" +#include "options/arith_options.h" +#include "options/theory_options.h" #include "smt/env.h" #include "theory/quantifiers_engine.h" #include "theory/shared_solver.h" @@ -70,7 +72,7 @@ void EqEngineManagerCentral::initializeTheories() std::map esiMap; // set of theories that need equality engines std::unordered_set eeTheories; - const LogicInfo& logicInfo = d_te.getLogicInfo(); + const LogicInfo& linfo = logicInfo(); for (TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++theoryId) @@ -91,8 +93,8 @@ void EqEngineManagerCentral::initializeTheories() // if the logic has a theory that does not use central equality engine, // we can't use the central equality engine for the master equality // engine - if (theoryId != THEORY_QUANTIFIERS && logicInfo.isTheoryEnabled(theoryId) - && !Theory::usesCentralEqualityEngine(theoryId)) + if (theoryId != THEORY_QUANTIFIERS && linfo.isTheoryEnabled(theoryId) + && !usesCentralEqualityEngine(options(), theoryId)) { Trace("ee-central") << "Must use separate master equality engine due to " << theoryId << std::endl; @@ -102,7 +104,7 @@ void EqEngineManagerCentral::initializeTheories() // initialize the master equality engine, which may be the central equality // engine - if (logicInfo.isQuantified()) + if (linfo.isQuantified()) { // construct the master equality engine Assert(d_masterEqualityEngine == nullptr); @@ -155,12 +157,12 @@ void EqEngineManagerCentral::initializeTheories() eq::EqualityEngineNotify* notify = esi.d_notify; d_theoryNotify[theoryId] = notify; // split on whether integrated, or whether asked for master - if (t->usesCentralEqualityEngine()) + if (usesCentralEqualityEngine(options(), t->getId())) { Trace("ee-central") << "...uses central" << std::endl; // the theory uses the central equality engine eet.d_usedEe = &d_centralEqualityEngine; - if (logicInfo.isTheoryEnabled(theoryId)) + if (linfo.isTheoryEnabled(theoryId)) { // add to vectors for the kinds of notifications if (esi.needsNotifyNewClass()) @@ -196,6 +198,24 @@ void EqEngineManagerCentral::initializeTheories() } } +bool EqEngineManagerCentral::usesCentralEqualityEngine(const Options& opts, + TheoryId id) +{ + Assert(opts.theory.eeMode == options::EqEngineMode::CENTRAL); + if (id == THEORY_BUILTIN) + { + return true; + } + if (id == THEORY_ARITH) + { + // conditional on whether we are using the equality solver + return opts.arith.arithEqSolver; + } + return id == THEORY_UF || id == THEORY_DATATYPES || id == THEORY_BAGS + || id == THEORY_FP || id == THEORY_SETS || id == THEORY_STRINGS + || id == THEORY_SEP || id == THEORY_ARRAYS || id == THEORY_BV; +} + void EqEngineManagerCentral::notifyBuildingModel() {} EqEngineManagerCentral::CentralNotifyClass::CentralNotifyClass( diff --git a/src/theory/ee_manager_central.h b/src/theory/ee_manager_central.h index 2b9677573..536ab1505 100644 --- a/src/theory/ee_manager_central.h +++ b/src/theory/ee_manager_central.h @@ -64,6 +64,12 @@ class EqEngineManagerCentral : public EqEngineManager /** Notify this class that we are building the model. */ void notifyBuildingModel(); + /** + * Return true if the theory with the given id uses central equality engine + * with the given options. + */ + static bool usesCentralEqualityEngine(const Options& opts, TheoryId id); + private: /** * Notify class for central equality engine. This class dispatches diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 5345c5959..81bf7c1c2 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -194,16 +194,9 @@ void PreRegisterVisitor::preRegisterWithTheory(TheoryEngine* te, // guaranteed to be initialized. if (!te->isTheoryEnabled(id)) { - const LogicInfo& l = te->getLogicInfo(); - LogicInfo newLogicInfo = l.getUnlockedCopy(); - newLogicInfo.enableTheory(id); - newLogicInfo.lock(); std::stringstream ss; - ss << "The logic was specified as " << l.getLogicString() - << ", which doesn't include " << id - << ", but found a term in that theory." << std::endl - << "You might want to extend your logic to " - << newLogicInfo.getLogicString() << std::endl; + ss << "The logic doesn't include theory " << id + << ", but found a term in that theory." << std::endl; throw LogicException(ss.str()); } } diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 9ba9ad028..35f2af16b 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -672,34 +672,9 @@ eq::EqualityEngine* Theory::getEqualityEngine() return d_equalityEngine; } -bool Theory::usesCentralEqualityEngine() const -{ - return usesCentralEqualityEngine(d_id); -} - -bool Theory::usesCentralEqualityEngine(TheoryId id) -{ - if (id == THEORY_BUILTIN) - { - return true; - } - if (options::eeMode() == options::EqEngineMode::DISTRIBUTED) - { - return false; - } - if (id == THEORY_ARITH) - { - // conditional on whether we are using the equality solver - return options::arithEqSolver(); - } - return id == THEORY_UF || id == THEORY_DATATYPES || id == THEORY_BAGS - || id == THEORY_FP || id == THEORY_SETS || id == THEORY_STRINGS - || id == THEORY_SEP || id == THEORY_ARRAYS || id == THEORY_BV; -} - bool Theory::expUsingCentralEqualityEngine(TheoryId id) { - return id != THEORY_ARITH && usesCentralEqualityEngine(id); + return id != THEORY_ARITH; } theory::Assertion Theory::get() diff --git a/src/theory/theory.h b/src/theory/theory.h index 1001db7ee..5267e0f53 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -787,11 +787,10 @@ class Theory : protected EnvObj */ virtual std::pair entailmentCheck(TNode lit); - /** Return true if this theory uses central equality engine */ - bool usesCentralEqualityEngine() const; - /** uses central equality engine (static) */ - static bool usesCentralEqualityEngine(TheoryId id); - /** Explains/propagates via central equality engine only */ + /** + * Return true if this theory explains and propagates via central equality + * engine only when the theory uses the central equality engine. + */ static bool expUsingCentralEqualityEngine(TheoryId id); private: diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index fed582cc5..e38839530 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -35,6 +35,7 @@ #include "smt/logic_exception.h" #include "theory/combination_care_graph.h" #include "theory/decision_manager.h" +#include "theory/ee_manager_central.h" #include "theory/partition_generator.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers_engine.h" @@ -136,7 +137,7 @@ void TheoryEngine::finishInit() #endif #define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits::isParametric \ - && d_logicInfo.isTheoryEnabled(THEORY)) \ + && isTheoryEnabled(THEORY)) \ { \ paraTheories.push_back(theoryOf(THEORY)); \ } @@ -161,7 +162,7 @@ void TheoryEngine::finishInit() } // initialize the quantifiers engine - if (d_logicInfo.isQuantified()) + if (logicInfo().isQuantified()) { // get the quantifiers engine, which is initialized by the quantifiers // theory @@ -171,7 +172,7 @@ void TheoryEngine::finishInit() // finish initializing the quantifiers engine, which must come before // initializing theory combination, since quantifiers engine may have a // special model builder object - if (d_logicInfo.isQuantified()) + if (logicInfo().isQuantified()) { d_quantEngine->finishInit(this); } @@ -214,7 +215,6 @@ void TheoryEngine::finishInit() TheoryEngine::TheoryEngine(Env& env) : EnvObj(env), d_propEngine(nullptr), - d_logicInfo(env.getLogicInfo()), d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager() : nullptr), d_lazyProof( @@ -320,7 +320,8 @@ void TheoryEngine::printAssertions(const char* tag) { for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { Theory* theory = d_theoryTable[theoryId]; - if (theory && d_logicInfo.isTheoryEnabled(theoryId)) { + if (theory && isTheoryEnabled(theoryId)) + { Trace(tag) << "--------------------------------------------" << endl; Trace(tag) << "Assertions of " << theory->getId() << ": " << endl; { @@ -341,7 +342,8 @@ void TheoryEngine::printAssertions(const char* tag) { } } - if (d_logicInfo.isSharingEnabled()) { + if (logicInfo().isSharingEnabled()) + { Trace(tag) << "Shared terms of " << theory->getId() << ": " << endl; context::CDList::const_iterator it = theory->shared_terms_begin(), @@ -370,7 +372,7 @@ void TheoryEngine::check(Theory::Effort effort) { #endif #define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits::hasCheck \ - && d_logicInfo.isTheoryEnabled(THEORY)) \ + && isTheoryEnabled(THEORY)) \ { \ theoryOf(THEORY)->check(effort); \ if (d_inConflict) \ @@ -442,7 +444,7 @@ void TheoryEngine::check(Theory::Effort effort) { propagate(effort); // We do combination if all has been processed and we are in fullcheck - if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled() + if (Theory::fullEffort(effort) && logicInfo().isSharingEnabled() && !d_factsAsserted && !needCheck() && !d_inConflict) { // Do the combination @@ -451,7 +453,8 @@ void TheoryEngine::check(Theory::Effort effort) { TimerStat::CodeTimer combineTheoriesTimer(d_combineTheoriesTime); d_tc->combineTheories(); } - if(d_logicInfo.isQuantified()){ + if (logicInfo().isQuantified()) + { d_quantEngine->notifyCombineTheories(); } } @@ -469,7 +472,8 @@ void TheoryEngine::check(Theory::Effort effort) { for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { if( theoryId!=THEORY_QUANTIFIERS ){ Theory* theory = d_theoryTable[theoryId]; - if (theory && d_logicInfo.isTheoryEnabled(theoryId)) { + if (theory && isTheoryEnabled(theoryId)) + { if( theory->needsCheckLastEffort() ){ if (!d_tc->buildModel()) { @@ -482,7 +486,8 @@ void TheoryEngine::check(Theory::Effort effort) { } if (!d_inConflict) { - if(d_logicInfo.isQuantified()) { + if (logicInfo().isQuantified()) + { // quantifiers engine must check at last call effort d_quantEngine->check(Theory::EFFORT_LAST_CALL); } @@ -532,7 +537,7 @@ void TheoryEngine::propagate(Theory::Effort effort) #endif #define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits::hasPropagate \ - && d_logicInfo.isTheoryEnabled(THEORY)) \ + && isTheoryEnabled(THEORY)) \ { \ theoryOf(THEORY)->propagate(effort); \ } @@ -626,6 +631,24 @@ bool TheoryEngine::buildModel() return d_tc->buildModel(); } +bool TheoryEngine::isTheoryEnabled(theory::TheoryId theoryId) const +{ + return logicInfo().isTheoryEnabled(theoryId); +} + +theory::TheoryId TheoryEngine::theoryExpPropagation(theory::TheoryId tid) const +{ + if (options().theory.eeMode == options::EqEngineMode::CENTRAL) + { + if (EqEngineManagerCentral::usesCentralEqualityEngine(options(), tid) + && Theory::expUsingCentralEqualityEngine(tid)) + { + return THEORY_BUILTIN; + } + } + return tid; +} + bool TheoryEngine::presolve() { // Reset the interrupt flag d_interrupted = false; @@ -696,7 +719,7 @@ void TheoryEngine::notifyRestart() { #endif #define CVC5_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits::hasNotifyRestart \ - && d_logicInfo.isTheoryEnabled(THEORY)) \ + && isTheoryEnabled(THEORY)) \ { \ theoryOf(THEORY)->notifyRestart(); \ } @@ -746,10 +769,10 @@ theory::Theory::PPAssertStatus TheoryEngine::solve( Trace("theory::solve") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl; theory::TheoryId tid = d_env.theoryOf(atom); - if (!d_logicInfo.isTheoryEnabled(tid) && tid != THEORY_SAT_SOLVER) + if (!isTheoryEnabled(tid) && tid != THEORY_SAT_SOLVER) { stringstream ss; - ss << "The logic was specified as " << d_logicInfo.getLogicString() + ss << "The logic was specified as " << logicInfo().getLogicString() << ", which doesn't include " << tid << ", but got a preprocessing-time fact for that theory." << endl << "The fact:" << endl @@ -839,10 +862,11 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << originalAssertion << "," << toTheoryId << ", " << fromTheoryId << ")" << endl; Assert(toTheoryId != fromTheoryId); - if(toTheoryId != THEORY_SAT_SOLVER && - ! d_logicInfo.isTheoryEnabled(toTheoryId)) { + if (toTheoryId != THEORY_SAT_SOLVER + && !isTheoryEnabled(toTheoryId)) + { stringstream ss; - ss << "The logic was specified as " << d_logicInfo.getLogicString() + ss << "The logic was specified as " << logicInfo().getLogicString() << ", which doesn't include " << toTheoryId << ", but got an asserted fact to that theory." << endl << "The fact:" << endl @@ -855,7 +879,8 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo } // If sharing is disabled, things are easy - if (!d_logicInfo.isSharingEnabled()) { + if (!logicInfo().isSharingEnabled()) + { Assert(assertion == originalAssertion); if (fromTheoryId == THEORY_SAT_SOLVER) { // Send to the apropriate theory @@ -885,9 +910,7 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo // determine the actual theory that will process/explain the fact, which is // THEORY_BUILTIN if the theory uses the central equality engine - TheoryId toTheoryIdProp = (Theory::expUsingCentralEqualityEngine(toTheoryId)) - ? THEORY_BUILTIN - : toTheoryId; + TheoryId toTheoryIdProp = theoryExpPropagation(toTheoryId); // If sending to the shared solver, it's also simple if (toTheoryId == THEORY_BUILTIN) { if (markPropagation( @@ -998,7 +1021,8 @@ void TheoryEngine::assertFact(TNode literal) bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; - if (d_logicInfo.isSharingEnabled()) { + if (logicInfo().isSharingEnabled()) + { // If any shared terms, it's time to do sharing work d_sharedSolver->preNotifySharedFact(atom); @@ -1035,7 +1059,9 @@ void TheoryEngine::assertFact(TNode literal) /* to */ d_env.theoryOf(atom), /* from */ THEORY_SAT_SOLVER); } - } else { + } + else + { // Assert the fact to the appropriate theory directly assertToTheory(literal, literal, @@ -1057,7 +1083,8 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; - if (d_logicInfo.isSharingEnabled() && atom.getKind() == kind::EQUAL) { + if (logicInfo().isSharingEnabled() && atom.getKind() == kind::EQUAL) + { if (d_propEngine->isSatLiteral(literal)) { // We propagate SAT literals to SAT assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory); @@ -1066,7 +1093,9 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { // Assert to the shared terms database assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ theory); } - } else { + } + else + { // Just send off to the SAT solver Assert(d_propEngine->isSatLiteral(literal)); assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory); @@ -1075,8 +1104,6 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { return !d_inConflict; } -const LogicInfo& TheoryEngine::getLogicInfo() const { return d_logicInfo; } - theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { Assert(a.getType() == b.getType()); @@ -1126,7 +1153,7 @@ TrustNode TheoryEngine::getExplanation(TNode node) TNode atom = polarity ? node : node[0]; // If we're not in shared mode, explanations are simple - if (!d_logicInfo.isSharingEnabled()) + if (!logicInfo().isSharingEnabled()) { Trace("theory::explain") << "TheoryEngine::getExplanation: sharing is NOT enabled. " @@ -1371,7 +1398,8 @@ void TheoryEngine::conflict(TrustNode tconflict, TheoryId theoryId) markInConflict(); // In the multiple-theories case, we need to reconstruct the conflict - if (d_logicInfo.isSharingEnabled()) { + if (logicInfo().isSharingEnabled()) + { // Create the workplace for explanations std::vector vec; vec.push_back( @@ -1454,7 +1482,9 @@ void TheoryEngine::conflict(TrustNode tconflict, TheoryId theoryId) tconf.debugCheckClosed("te-proof-debug", "TheoryEngine::conflict:sharing"); } lemma(tconf, LemmaProperty::REMOVABLE); - } else { + } + else + { // When only one theory, the conflict should need no processing Assert(properConflict(conflict)); // pass the trust node that was sent from the theory @@ -1477,10 +1507,8 @@ TrustNode TheoryEngine::getExplanation( Node conclusion = explanationVector[0].d_node; // if the theory explains using the central equality engine, we always start // with THEORY_BUILTIN. - if (Theory::expUsingCentralEqualityEngine(explanationVector[0].d_theory)) - { - explanationVector[0].d_theory = THEORY_BUILTIN; - } + explanationVector[0].d_theory = + theoryExpPropagation(explanationVector[0].d_theory); std::shared_ptr lcp; if (isProofEnabled()) { @@ -1827,7 +1855,8 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) { } for(TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { Theory* theory = d_theoryTable[theoryId]; - if(theory && d_logicInfo.isTheoryEnabled(theoryId)) { + if (theory && isTheoryEnabled(theoryId)) + { for (context::CDList::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 7391fd60f..3f25eefcd 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -333,12 +333,9 @@ class TheoryEngine : protected EnvObj return d_theoryTable[theoryId]; } - bool isTheoryEnabled(theory::TheoryId theoryId) const - { - return d_logicInfo.isTheoryEnabled(theoryId); - } - /** get the logic info used by this theory engine */ - const LogicInfo& getLogicInfo() const; + bool isTheoryEnabled(theory::TheoryId theoryId) const; + /** return the theory that should explain a propagation from TheoryId */ + theory::TheoryId theoryExpPropagation(theory::TheoryId tid) const; /** * Returns the equality status of the two terms, from the theory @@ -501,15 +498,6 @@ class TheoryEngine : protected EnvObj */ theory::Theory* d_theoryTable[theory::THEORY_LAST]; - /** - * A collection of theories that are "active" for the current run. - * This set is provided by the user (as a logic string, say, in SMT-LIBv2 - * format input), or else by default it's all-inclusive. This is important - * because we can optimize for single-theory runs (no sharing), can reduce - * the cost of walking the DAG on registration, etc. - */ - const LogicInfo& d_logicInfo; - //--------------------------------- new proofs /** Proof node manager used by this theory engine, if proofs are enabled */ ProofNodeManager* d_pnm;