From 8e2c02201d30b5715a095ffe0098dd74a636ac85 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Fri, 3 Sep 2021 05:34:27 -0700 Subject: [PATCH] theory: Have more classes in theory with reference to Env derive from EnvObj. (#7130) --- src/theory/combination_engine.cpp | 4 ++-- src/theory/combination_engine.h | 7 +++---- src/theory/model_manager.cpp | 4 ++-- src/theory/model_manager.h | 5 ++--- src/theory/sort_inference.h | 10 +++++----- src/theory/theory_engine.cpp | 4 ++-- src/theory/theory_engine.h | 8 ++------ src/theory/theory_model.cpp | 2 +- src/theory/theory_model.h | 5 ++--- src/theory/theory_model_builder.cpp | 2 +- src/theory/theory_model_builder.h | 6 ++---- src/theory/theory_state.cpp | 2 +- src/theory/theory_state.h | 5 ++--- 13 files changed, 27 insertions(+), 37 deletions(-) diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp index 609f8d9d6..9352ce95c 100644 --- a/src/theory/combination_engine.cpp +++ b/src/theory/combination_engine.cpp @@ -32,8 +32,8 @@ CombinationEngine::CombinationEngine(TheoryEngine& te, Env& env, const std::vector& paraTheories, ProofNodeManager* pnm) - : d_te(te), - d_env(env), + : EnvObj(env), + d_te(te), d_valuation(&te), d_pnm(pnm), d_logicInfo(te.getLogicInfo()), diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h index 7f04ccd75..f7da01fac 100644 --- a/src/theory/combination_engine.h +++ b/src/theory/combination_engine.h @@ -18,9 +18,10 @@ #ifndef CVC5__THEORY__COMBINATION_ENGINE__H #define CVC5__THEORY__COMBINATION_ENGINE__H -#include #include +#include +#include "smt/env_obj.h" #include "theory/ee_manager.h" #include "theory/valuation.h" @@ -42,7 +43,7 @@ class SharedSolver; * mode, and * (2) Implementing the main combination method (combineTheories). */ -class CombinationEngine +class CombinationEngine : protected EnvObj { public: CombinationEngine(TheoryEngine& te, @@ -107,8 +108,6 @@ class CombinationEngine virtual eq::EqualityEngineNotify* getModelEqualityEngineNotify(); /** Reference to the theory engine */ TheoryEngine& d_te; - /** Reference to the environment */ - Env& d_env; /** Valuation for the engine */ Valuation d_valuation; /** The proof node manager */ diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp index 29c4bf169..2b746cba1 100644 --- a/src/theory/model_manager.cpp +++ b/src/theory/model_manager.cpp @@ -28,8 +28,8 @@ namespace cvc5 { namespace theory { ModelManager::ModelManager(TheoryEngine& te, Env& env, EqEngineManager& eem) - : d_te(te), - d_env(env), + : EnvObj(env), + d_te(te), d_eem(eem), d_modelEqualityEngine(nullptr), d_modelEqualityEngineAlloc(nullptr), diff --git a/src/theory/model_manager.h b/src/theory/model_manager.h index fd8ca6e11..2a62c8be0 100644 --- a/src/theory/model_manager.h +++ b/src/theory/model_manager.h @@ -20,6 +20,7 @@ #include +#include "smt/env_obj.h" #include "theory/ee_manager.h" #include "theory/logic_info.h" @@ -40,7 +41,7 @@ class TheoryModel; * method is a manager-specific way for setting up the equality engine of the * model in preparation for model building. */ -class ModelManager +class ModelManager : protected EnvObj { public: ModelManager(TheoryEngine& te, Env& env, EqEngineManager& eem); @@ -111,8 +112,6 @@ class ModelManager /** Reference to the theory engine */ TheoryEngine& d_te; - /** Reference to the environment */ - Env& d_env; /** The equality engine manager */ EqEngineManager& d_eem; /** diff --git a/src/theory/sort_inference.h b/src/theory/sort_inference.h index 279be5e10..126c94749 100644 --- a/src/theory/sort_inference.h +++ b/src/theory/sort_inference.h @@ -23,6 +23,7 @@ #include "expr/node.h" #include "expr/type_node.h" +#include "smt/env_obj.h" namespace cvc5 { @@ -38,8 +39,9 @@ namespace theory { * "Sort it out with Monotonicity" Claessen 2011 * "Non-Cyclic Sorts for First-Order Satisfiability" Korovin 2013. */ -class SortInference { -private: +class SortInference : protected EnvObj +{ + private: //all subsorts std::vector< int > d_sub_sorts; std::map< int, bool > d_non_monotonic_sorts; @@ -66,8 +68,6 @@ public: }; private: - /** Reference to the env */ - Env& d_env; /** the id count for all subsorts we have allocated */ int d_sortCount; UnionFind d_type_union_find; @@ -111,7 +111,7 @@ private: void reset(); public: - SortInference(Env& env) : d_env(env), d_sortCount(1) {} + SortInference(Env& env) : EnvObj(env), d_sortCount(1) {} ~SortInference(){} /** initialize diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index cd9445bb0..72f3d78ac 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -219,8 +219,8 @@ context::UserContext* TheoryEngine::getUserContext() const } TheoryEngine::TheoryEngine(Env& env) - : d_propEngine(nullptr), - d_env(env), + : EnvObj(env), + d_propEngine(nullptr), d_logicInfo(env.getLogicInfo()), d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager() : nullptr), diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 5c44f8968..496966149 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -26,6 +26,7 @@ #include "expr/node.h" #include "options/theory_options.h" #include "proof/trust_node.h" +#include "smt/env_obj.h" #include "theory/atom_requests.h" #include "theory/engine_output_channel.h" #include "theory/interrupted.h" @@ -98,7 +99,7 @@ class PropEngine; * T-solvers look like a single unit to the propositional part of * cvc5. */ -class TheoryEngine +class TheoryEngine : protected EnvObj { /** Shared terms database can use the internals notify the theories */ friend class SharedTermsDatabase; @@ -528,11 +529,6 @@ class TheoryEngine /** Associated PropEngine engine */ prop::PropEngine* d_propEngine; - /** - * Reference to the environment. - */ - Env& d_env; - /** * A table of from theory IDs to theory pointers. Never use this table * directly, use theoryOf() instead. diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 291cd1905..4cc25a887 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -33,7 +33,7 @@ namespace cvc5 { namespace theory { TheoryModel::TheoryModel(Env& env, std::string name, bool enableFuncModels) - : d_env(env), + : EnvObj(env), d_name(name), d_equalityEngine(nullptr), d_using_model_core(false), diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 6841a11d8..4a6492aaa 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -21,6 +21,7 @@ #include #include +#include "smt/env_obj.h" #include "theory/ee_setup_info.h" #include "theory/rep_set.h" #include "theory/type_enumerator.h" @@ -79,7 +80,7 @@ namespace theory { * above functions such as getRepresentative() when assigning total * interpretations for uninterpreted functions. */ -class TheoryModel +class TheoryModel : protected EnvObj { friend class TheoryEngineModelBuilder; @@ -357,8 +358,6 @@ class TheoryModel std::string debugPrintModelEqc() const; protected: - /** Reference to the environmanet */ - Env& d_env; /** Unique name of this model */ std::string d_name; /** equality engine containing all known equalities/disequalities */ diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 2acbe2388..23a76d273 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -32,7 +32,7 @@ using namespace cvc5::context; namespace cvc5 { namespace theory { -TheoryEngineModelBuilder::TheoryEngineModelBuilder(Env& env) : d_env(env) {} +TheoryEngineModelBuilder::TheoryEngineModelBuilder(Env& env) : EnvObj(env) {} void TheoryEngineModelBuilder::Assigner::initialize( TypeNode tn, TypeEnumeratorProperties* tep, const std::vector& aes) diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h index 71458a913..dd11a3d2e 100644 --- a/src/theory/theory_model_builder.h +++ b/src/theory/theory_model_builder.h @@ -21,6 +21,7 @@ #include #include +#include "smt/env_obj.h" #include "theory/theory_model.h" namespace cvc5 { @@ -42,7 +43,7 @@ namespace theory { * this will set up the data structures in TheoryModel to represent * a model for the current set of assertions. */ -class TheoryEngineModelBuilder +class TheoryEngineModelBuilder : protected EnvObj { typedef std::unordered_map NodeMap; typedef std::unordered_set NodeSet; @@ -315,9 +316,6 @@ class TheoryEngineModelBuilder Node v, std::map& visited); //---------------------------------end for debugging finite model finding - /** Reference to the env */ - Env& d_env; - }; /* class TheoryEngineModelBuilder */ } // namespace theory diff --git a/src/theory/theory_state.cpp b/src/theory/theory_state.cpp index 72ab24a7e..e3655e3ab 100644 --- a/src/theory/theory_state.cpp +++ b/src/theory/theory_state.cpp @@ -21,7 +21,7 @@ namespace cvc5 { namespace theory { TheoryState::TheoryState(Env& env, Valuation val) - : d_env(env), + : EnvObj(env), d_valuation(val), d_ee(nullptr), d_conflict(d_env.getContext(), false) diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h index cc58347bf..9162fdeb6 100644 --- a/src/theory/theory_state.h +++ b/src/theory/theory_state.h @@ -21,6 +21,7 @@ #include "context/cdo.h" #include "expr/node.h" #include "smt/env.h" +#include "smt/env_obj.h" #include "theory/valuation.h" namespace cvc5 { @@ -30,7 +31,7 @@ namespace eq { class EqualityEngine; } -class TheoryState +class TheoryState : protected EnvObj { public: TheoryState(Env& env, @@ -117,8 +118,6 @@ class TheoryState Valuation& getValuation(); protected: - /** Reference to the environment. */ - Env& d_env; /** * The valuation proxy for the Theory to communicate back with the * theory engine (and other theories). -- 2.30.2