From 4e54aa63e13f551e9c647ce59edd958e1d84ddb1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 30 Sep 2021 11:48:12 -0500 Subject: [PATCH] Make theory engine modules use Env (#7277) This updates several core modules of TheoryEngine to use Env and eliminates some getters from TheoryEngine. --- src/theory/combination_care_graph.cpp | 7 ++---- src/theory/combination_care_graph.h | 7 +++--- src/theory/combination_engine.cpp | 25 ++++++++++---------- src/theory/combination_engine.h | 7 +++--- src/theory/ee_manager.cpp | 4 ++-- src/theory/ee_manager.h | 5 ++-- src/theory/ee_manager_central.cpp | 24 +++++++++---------- src/theory/ee_manager_central.h | 4 +--- src/theory/ee_manager_distributed.cpp | 15 ++++++------ src/theory/ee_manager_distributed.h | 2 +- src/theory/model_manager.cpp | 2 +- src/theory/model_manager.h | 2 +- src/theory/model_manager_distributed.cpp | 6 ++--- src/theory/model_manager_distributed.h | 2 +- src/theory/shared_solver.cpp | 13 +++++----- src/theory/shared_solver.h | 5 ++-- src/theory/shared_solver_distributed.cpp | 5 ++-- src/theory/shared_solver_distributed.h | 2 +- src/theory/shared_terms_database.cpp | 30 +++++++++++------------- src/theory/shared_terms_database.h | 9 +++---- src/theory/theory_engine.cpp | 11 +-------- src/theory/theory_engine.h | 13 ---------- 22 files changed, 85 insertions(+), 115 deletions(-) diff --git a/src/theory/combination_care_graph.cpp b/src/theory/combination_care_graph.cpp index 4b0adf56b..c0d75ceaa 100644 --- a/src/theory/combination_care_graph.cpp +++ b/src/theory/combination_care_graph.cpp @@ -26,11 +26,8 @@ namespace cvc5 { namespace theory { CombinationCareGraph::CombinationCareGraph( - TheoryEngine& te, - Env& env, - const std::vector& paraTheories, - ProofNodeManager* pnm) - : CombinationEngine(te, env, paraTheories, pnm) + Env& env, TheoryEngine& te, const std::vector& paraTheories) + : CombinationEngine(env, te, paraTheories) { } diff --git a/src/theory/combination_care_graph.h b/src/theory/combination_care_graph.h index 971b81d1d..afcf8e3a2 100644 --- a/src/theory/combination_care_graph.h +++ b/src/theory/combination_care_graph.h @@ -35,10 +35,9 @@ namespace theory { class CombinationCareGraph : public CombinationEngine { public: - CombinationCareGraph(TheoryEngine& te, - Env& env, - const std::vector& paraTheories, - ProofNodeManager* pnm); + CombinationCareGraph(Env& env, + TheoryEngine& te, + const std::vector& paraTheories); ~CombinationCareGraph(); bool buildModel() override; diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp index 9352ce95c..dfa6d5da4 100644 --- a/src/theory/combination_engine.cpp +++ b/src/theory/combination_engine.cpp @@ -28,45 +28,44 @@ namespace cvc5 { namespace theory { -CombinationEngine::CombinationEngine(TheoryEngine& te, - Env& env, - const std::vector& paraTheories, - ProofNodeManager* pnm) +CombinationEngine::CombinationEngine(Env& env, + TheoryEngine& te, + const std::vector& paraTheories) : EnvObj(env), d_te(te), d_valuation(&te), - d_pnm(pnm), + d_pnm(env.isTheoryProofProducing() ? env.getProofNodeManager() : nullptr), d_logicInfo(te.getLogicInfo()), d_paraTheories(paraTheories), d_eemanager(nullptr), d_mmanager(nullptr), d_sharedSolver(nullptr), - d_cmbsPg(pnm ? new EagerProofGenerator(pnm, te.getUserContext()) - : nullptr) + d_cmbsPg(d_pnm ? new EagerProofGenerator(d_pnm, env.getUserContext()) + : nullptr) { // create the equality engine, model manager, and shared solver if (options::eeMode() == options::EqEngineMode::DISTRIBUTED) { // use the distributed shared solver - d_sharedSolver.reset(new SharedSolverDistributed(d_te, d_pnm)); + d_sharedSolver.reset(new SharedSolverDistributed(env, d_te)); // make the distributed equality engine manager d_eemanager.reset( - new EqEngineManagerDistributed(d_te, *d_sharedSolver.get())); + new EqEngineManagerDistributed(env, d_te, *d_sharedSolver.get())); // make the distributed model manager d_mmanager.reset( - new ModelManagerDistributed(d_te, d_env, *d_eemanager.get())); + new ModelManagerDistributed(env, d_te, *d_eemanager.get())); } else if (options::eeMode() == options::EqEngineMode::CENTRAL) { // for now, the shared solver is the same in both approaches; use the // distributed one for now - d_sharedSolver.reset(new SharedSolverDistributed(d_te, d_pnm)); + d_sharedSolver.reset(new SharedSolverDistributed(env, d_te)); // make the central equality engine manager d_eemanager.reset( - new EqEngineManagerCentral(d_te, *d_sharedSolver.get(), d_pnm)); + new EqEngineManagerCentral(env, d_te, *d_sharedSolver.get())); // make the distributed model manager d_mmanager.reset( - new ModelManagerDistributed(d_te, d_env, *d_eemanager.get())); + new ModelManagerDistributed(env, d_te, *d_eemanager.get())); } else { diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h index f7da01fac..15f379dc0 100644 --- a/src/theory/combination_engine.h +++ b/src/theory/combination_engine.h @@ -46,10 +46,9 @@ class SharedSolver; class CombinationEngine : protected EnvObj { public: - CombinationEngine(TheoryEngine& te, - Env& env, - const std::vector& paraTheories, - ProofNodeManager* pnm); + CombinationEngine(Env& env, + TheoryEngine& te, + const std::vector& paraTheories); virtual ~CombinationEngine(); /** Finish initialization */ diff --git a/src/theory/ee_manager.cpp b/src/theory/ee_manager.cpp index c02710f77..a91aea94e 100644 --- a/src/theory/ee_manager.cpp +++ b/src/theory/ee_manager.cpp @@ -20,8 +20,8 @@ namespace cvc5 { namespace theory { -EqEngineManager::EqEngineManager(TheoryEngine& te, SharedSolver& shs) - : d_te(te), d_sharedSolver(shs) +EqEngineManager::EqEngineManager(Env& env, TheoryEngine& te, SharedSolver& shs) + : EnvObj(env), d_te(te), d_sharedSolver(shs) { } diff --git a/src/theory/ee_manager.h b/src/theory/ee_manager.h index 51216a614..228c0418a 100644 --- a/src/theory/ee_manager.h +++ b/src/theory/ee_manager.h @@ -21,6 +21,7 @@ #include #include +#include "smt/env_obj.h" #include "theory/ee_setup_info.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -51,7 +52,7 @@ struct EeTheoryInfo }; /** Virtual base class for equality engine managers */ -class EqEngineManager +class EqEngineManager : protected EnvObj { public: /** @@ -59,7 +60,7 @@ class EqEngineManager * @param sharedSolver The shared solver that is being used in combination * with this equality engine manager */ - EqEngineManager(TheoryEngine& te, SharedSolver& shs); + EqEngineManager(Env& env, TheoryEngine& te, SharedSolver& shs); virtual ~EqEngineManager() {} /** * Initialize theories, called during TheoryEngine::finishInit after theory diff --git a/src/theory/ee_manager_central.cpp b/src/theory/ee_manager_central.cpp index 23946512e..0e6610833 100644 --- a/src/theory/ee_manager_central.cpp +++ b/src/theory/ee_manager_central.cpp @@ -15,6 +15,7 @@ #include "theory/ee_manager_central.h" +#include "smt/env.h" #include "theory/quantifiers_engine.h" #include "theory/shared_solver.h" #include "theory/theory_engine.h" @@ -23,15 +24,14 @@ namespace cvc5 { namespace theory { -EqEngineManagerCentral::EqEngineManagerCentral(TheoryEngine& te, - SharedSolver& shs, - ProofNodeManager* pnm) - : EqEngineManager(te, shs), +EqEngineManagerCentral::EqEngineManagerCentral(Env& env, + TheoryEngine& te, + SharedSolver& shs) + : EqEngineManager(env, te, shs), d_masterEENotify(nullptr), d_masterEqualityEngine(nullptr), d_centralEENotify(*this), - d_centralEqualityEngine( - d_centralEENotify, te.getSatContext(), "central::ee", true) + d_centralEqualityEngine(d_centralEENotify, context(), "central::ee", true) { for (TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; @@ -39,12 +39,12 @@ EqEngineManagerCentral::EqEngineManagerCentral(TheoryEngine& te, { d_theoryNotify[theoryId] = nullptr; } - if (pnm != nullptr) + if (env.isTheoryProofProducing()) { - d_centralPfee.reset(new eq::ProofEqEngine(d_te.getSatContext(), - d_te.getUserContext(), + d_centralPfee.reset(new eq::ProofEqEngine(context(), + userContext(), d_centralEqualityEngine, - pnm)); + env.getProofNodeManager())); d_centralEqualityEngine.setProofEqualityEngine(d_centralPfee.get()); } } @@ -53,7 +53,7 @@ EqEngineManagerCentral::~EqEngineManagerCentral() {} void EqEngineManagerCentral::initializeTheories() { - context::Context* c = d_te.getSatContext(); + context::Context* c = context(); // initialize the shared solver EeSetupInfo esis; if (d_sharedSolver.needsEqualityEngine(esis)) @@ -113,7 +113,7 @@ void EqEngineManagerCentral::initializeTheories() if (!masterEqToCentral) { d_masterEqualityEngineAlloc.reset(new eq::EqualityEngine( - *d_masterEENotify.get(), d_te.getSatContext(), "master::ee", false)); + *d_masterEENotify.get(), c, "master::ee", false)); d_masterEqualityEngine = d_masterEqualityEngineAlloc.get(); } else diff --git a/src/theory/ee_manager_central.h b/src/theory/ee_manager_central.h index eb13b7820..f5a34b11e 100644 --- a/src/theory/ee_manager_central.h +++ b/src/theory/ee_manager_central.h @@ -54,9 +54,7 @@ namespace theory { class EqEngineManagerCentral : public EqEngineManager { public: - EqEngineManagerCentral(TheoryEngine& te, - SharedSolver& shs, - ProofNodeManager* pnm); + EqEngineManagerCentral(Env& env, TheoryEngine& te, SharedSolver& shs); ~EqEngineManagerCentral(); /** * Initialize theories. This method allocates unique equality engines diff --git a/src/theory/ee_manager_distributed.cpp b/src/theory/ee_manager_distributed.cpp index 7e4932767..6dee1910b 100644 --- a/src/theory/ee_manager_distributed.cpp +++ b/src/theory/ee_manager_distributed.cpp @@ -23,9 +23,10 @@ namespace cvc5 { namespace theory { -EqEngineManagerDistributed::EqEngineManagerDistributed(TheoryEngine& te, +EqEngineManagerDistributed::EqEngineManagerDistributed(Env& env, + TheoryEngine& te, SharedSolver& shs) - : EqEngineManager(te, shs), d_masterEENotify(nullptr) + : EqEngineManager(env, te, shs), d_masterEENotify(nullptr) { } @@ -35,7 +36,7 @@ EqEngineManagerDistributed::~EqEngineManagerDistributed() void EqEngineManagerDistributed::initializeTheories() { - context::Context* c = d_te.getSatContext(); + context::Context* c = context(); // initialize the shared solver EeSetupInfo esis; if (d_sharedSolver.needsEqualityEngine(esis)) @@ -49,7 +50,7 @@ void EqEngineManagerDistributed::initializeTheories() Unhandled() << "Expected shared solver to use equality engine"; } - const LogicInfo& logicInfo = d_te.getLogicInfo(); + const LogicInfo& logicInfo = d_env.getLogicInfo(); if (logicInfo.isQuantified()) { // construct the master equality engine @@ -57,10 +58,8 @@ void EqEngineManagerDistributed::initializeTheories() QuantifiersEngine* qe = d_te.getQuantifiersEngine(); Assert(qe != nullptr); d_masterEENotify.reset(new quantifiers::MasterNotifyClass(qe)); - d_masterEqualityEngine.reset(new eq::EqualityEngine(*d_masterEENotify.get(), - d_te.getSatContext(), - "theory::master", - false)); + d_masterEqualityEngine.reset(new eq::EqualityEngine( + *d_masterEENotify.get(), c, "theory::master", false)); } // allocate equality engines per theory for (TheoryId theoryId = theory::THEORY_FIRST; diff --git a/src/theory/ee_manager_distributed.h b/src/theory/ee_manager_distributed.h index 8c7bb2618..3aaadbc2e 100644 --- a/src/theory/ee_manager_distributed.h +++ b/src/theory/ee_manager_distributed.h @@ -49,7 +49,7 @@ class EqualityEngine; class EqEngineManagerDistributed : public EqEngineManager { public: - EqEngineManagerDistributed(TheoryEngine& te, SharedSolver& shs); + EqEngineManagerDistributed(Env& env, TheoryEngine& te, SharedSolver& shs); ~EqEngineManagerDistributed(); /** * Initialize theories. This method allocates unique equality engines diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp index dd06d4afd..23cd6430f 100644 --- a/src/theory/model_manager.cpp +++ b/src/theory/model_manager.cpp @@ -27,7 +27,7 @@ namespace cvc5 { namespace theory { -ModelManager::ModelManager(TheoryEngine& te, Env& env, EqEngineManager& eem) +ModelManager::ModelManager(Env& env, TheoryEngine& te, EqEngineManager& eem) : EnvObj(env), d_te(te), d_eem(eem), diff --git a/src/theory/model_manager.h b/src/theory/model_manager.h index 2a62c8be0..4e86b1134 100644 --- a/src/theory/model_manager.h +++ b/src/theory/model_manager.h @@ -44,7 +44,7 @@ class TheoryModel; class ModelManager : protected EnvObj { public: - ModelManager(TheoryEngine& te, Env& env, EqEngineManager& eem); + ModelManager(Env& env, TheoryEngine& te, EqEngineManager& eem); virtual ~ModelManager(); /** * Finish initializing this class, which allocates the model, the model diff --git a/src/theory/model_manager_distributed.cpp b/src/theory/model_manager_distributed.cpp index 91e4cb6d4..f81c39f89 100644 --- a/src/theory/model_manager_distributed.cpp +++ b/src/theory/model_manager_distributed.cpp @@ -23,10 +23,10 @@ namespace cvc5 { namespace theory { -ModelManagerDistributed::ModelManagerDistributed(TheoryEngine& te, - Env& env, +ModelManagerDistributed::ModelManagerDistributed(Env& env, + TheoryEngine& te, EqEngineManager& eem) - : ModelManager(te, env, eem) + : ModelManager(env, te, eem) { } diff --git a/src/theory/model_manager_distributed.h b/src/theory/model_manager_distributed.h index 322e61a98..04aa6788b 100644 --- a/src/theory/model_manager_distributed.h +++ b/src/theory/model_manager_distributed.h @@ -38,7 +38,7 @@ namespace theory { class ModelManagerDistributed : public ModelManager { public: - ModelManagerDistributed(TheoryEngine& te, Env& env, EqEngineManager& eem); + ModelManagerDistributed(Env& env, TheoryEngine& te, EqEngineManager& eem); ~ModelManagerDistributed(); /** Prepare the model, as described above. */ diff --git a/src/theory/shared_solver.cpp b/src/theory/shared_solver.cpp index 95558ead1..a503c5595 100644 --- a/src/theory/shared_solver.cpp +++ b/src/theory/shared_solver.cpp @@ -30,12 +30,13 @@ namespace theory { // In distributed equality engine management, shared terms database also // maintains an equality engine. In central equality engine management, // it does not. -SharedSolver::SharedSolver(TheoryEngine& te, ProofNodeManager* pnm) - : d_te(te), - d_logicInfo(te.getLogicInfo()), - d_sharedTerms(&d_te, d_te.getSatContext(), d_te.getUserContext(), pnm), - d_preRegistrationVisitor(&te, d_te.getSatContext()), - d_sharedTermsVisitor(&te, d_sharedTerms, d_te.getSatContext()), +SharedSolver::SharedSolver(Env& env, TheoryEngine& te) + : EnvObj(env), + d_te(te), + d_logicInfo(logicInfo()), + d_sharedTerms(env, &d_te), + d_preRegistrationVisitor(&te, context()), + d_sharedTermsVisitor(&te, d_sharedTerms, context()), d_im(te.theoryOf(THEORY_BUILTIN)->getInferenceManager()) { } diff --git a/src/theory/shared_solver.h b/src/theory/shared_solver.h index a7f9ceff5..d423b5983 100644 --- a/src/theory/shared_solver.h +++ b/src/theory/shared_solver.h @@ -19,6 +19,7 @@ #define CVC5__THEORY__SHARED_SOLVER__H #include "expr/node.h" +#include "smt/env_obj.h" #include "theory/inference_id.h" #include "theory/shared_terms_database.h" #include "theory/term_registration_visitor.h" @@ -44,10 +45,10 @@ class TheoryInferenceManager; * (2) Be the official interface for equality statuses, * (3) Propagate equalities to TheoryEngine when necessary and explain them. */ -class SharedSolver +class SharedSolver : protected EnvObj { public: - SharedSolver(TheoryEngine& te, ProofNodeManager* pnm); + SharedSolver(Env& env, TheoryEngine& te); virtual ~SharedSolver() {} //------------------------------------- initialization /** diff --git a/src/theory/shared_solver_distributed.cpp b/src/theory/shared_solver_distributed.cpp index 3c78a75f8..1399bac18 100644 --- a/src/theory/shared_solver_distributed.cpp +++ b/src/theory/shared_solver_distributed.cpp @@ -20,9 +20,8 @@ namespace cvc5 { namespace theory { -SharedSolverDistributed::SharedSolverDistributed(TheoryEngine& te, - ProofNodeManager* pnm) - : SharedSolver(te, pnm) +SharedSolverDistributed::SharedSolverDistributed(Env& env, TheoryEngine& te) + : SharedSolver(env, te) { } diff --git a/src/theory/shared_solver_distributed.h b/src/theory/shared_solver_distributed.h index f9a00230b..3e7d81e30 100644 --- a/src/theory/shared_solver_distributed.h +++ b/src/theory/shared_solver_distributed.h @@ -31,7 +31,7 @@ namespace theory { class SharedSolverDistributed : public SharedSolver { public: - SharedSolverDistributed(TheoryEngine& te, ProofNodeManager* pnm); + SharedSolverDistributed(Env& env, TheoryEngine& te); virtual ~SharedSolverDistributed() {} //------------------------------------- initialization /** diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index a4a846e05..e4f1b6fab 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -24,26 +24,23 @@ using namespace cvc5::theory; namespace cvc5 { -SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, - context::Context* context, - context::UserContext* userContext, - ProofNodeManager* pnm) - : ContextNotifyObj(context), +SharedTermsDatabase::SharedTermsDatabase(Env& env, TheoryEngine* theoryEngine) + : ContextNotifyObj(env.getContext()), + d_env(env), d_statSharedTerms( smtStatisticsRegistry().registerInt("theory::shared_terms")), - d_addedSharedTermsSize(context, 0), - d_termsToTheories(context), - d_alreadyNotifiedMap(context), - d_registeredEqualities(context), + d_addedSharedTermsSize(env.getContext(), 0), + d_termsToTheories(env.getContext()), + d_alreadyNotifiedMap(env.getContext()), + d_registeredEqualities(env.getContext()), d_EENotify(*this), d_theoryEngine(theoryEngine), - d_inConflict(context, false), + d_inConflict(env.getContext(), false), d_conflictPolarity(), - d_satContext(context), - d_userContext(userContext), + d_satContext(env.getContext()), + d_userContext(env.getUserContext()), d_equalityEngine(nullptr), - d_pfee(nullptr), - d_pnm(pnm) + d_pfee(nullptr) { } @@ -52,13 +49,14 @@ void SharedTermsDatabase::setEqualityEngine(eq::EqualityEngine* ee) Assert(ee != nullptr); d_equalityEngine = ee; // if proofs are enabled, make the proof equality engine if necessary - if (d_pnm != nullptr) + if (d_env.isTheoryProofProducing()) { d_pfee = d_equalityEngine->getProofEqualityEngine(); if (d_pfee == nullptr) { + ProofNodeManager* pnm = d_env.getProofNodeManager(); d_pfeeAlloc.reset( - new eq::ProofEqEngine(d_satContext, d_userContext, *ee, d_pnm)); + new eq::ProofEqEngine(d_satContext, d_userContext, *ee, pnm)); d_pfee = d_pfeeAlloc.get(); d_equalityEngine->setProofEqualityEngine(d_pfee); } diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index ddb1a4043..3b21c27a8 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -32,6 +32,7 @@ namespace cvc5 { +class Env; class TheoryEngine; class SharedTermsDatabase : public context::ContextNotifyObj { @@ -43,6 +44,9 @@ class SharedTermsDatabase : public context::ContextNotifyObj { typedef shared_terms_list::const_iterator shared_terms_iterator; private: + /** Reference to the env */ + Env& d_env; + /** Some statistics */ IntStat d_statSharedTerms; @@ -158,10 +162,7 @@ class SharedTermsDatabase : public context::ContextNotifyObj { * @param pnm The proof node manager to use, which is non-null if proofs * are enabled. */ - SharedTermsDatabase(TheoryEngine* theoryEngine, - context::Context* context, - context::UserContext* userContext, - ProofNodeManager* pnm); + SharedTermsDatabase(Env& env, TheoryEngine* theoryEngine); //-------------------------------------------- initialization /** Called to set the equality engine. */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 6fbac94e5..13a812bb2 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -147,7 +147,7 @@ void TheoryEngine::finishInit() // Initialize the theory combination architecture if (options::tcMode() == options::TcMode::CARE_GRAPH) { - d_tc.reset(new CombinationCareGraph(*this, d_env, paraTheories, d_pnm)); + d_tc.reset(new CombinationCareGraph(d_env, *this, paraTheories)); } else { @@ -205,15 +205,6 @@ void TheoryEngine::finishInit() Trace("theory") << "End TheoryEngine::finishInit" << std::endl; } -ProofNodeManager* TheoryEngine::getProofNodeManager() const { return d_pnm; } - -context::Context* TheoryEngine::getSatContext() const { return context(); } - -context::UserContext* TheoryEngine::getUserContext() const -{ - return userContext(); -} - TheoryEngine::TheoryEngine(Env& env) : EnvObj(env), d_propEngine(nullptr), diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 4e8beb967..b1ab0a001 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -156,19 +156,6 @@ class TheoryEngine : protected EnvObj */ prop::PropEngine* getPropEngine() const { return d_propEngine; } - /** Get the proof node manager */ - ProofNodeManager* getProofNodeManager() const; - - /** - * Get a pointer to the underlying sat context. - */ - context::Context* getSatContext() const; - - /** - * Get a pointer to the underlying user context. - */ - context::UserContext* getUserContext() const; - /** * Get a pointer to the underlying quantifiers engine. */ -- 2.30.2