theory: Have more classes in theory with reference to Env derive from EnvObj. (#7130)

diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp
index 609f8d9d627d65c8152283f48baad18626e64aed..9352ce95c316335213a8c6c672569ba3b74ba3a1 100644 (file)
--- 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<Theory*>& 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 7f04ccd7529e9332c378396273fc6f9881b05592..f7da01facda2db272446c101bbfbe32f412ebb40 100644 (file)
--- 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 <vector>
 #include <memory>
+#include <vector>
 
+#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 29c4bf1699602e4cf4245ee0a2f2fe3129982fac..2b746cba14352bfd62542bc98dc985bbf8c0640f 100644 (file)
--- 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 fd8ca6e11462a5d615993bf7fbb2ac17c8159cf0..2a62c8be056bd1230149cae81f6126a33f1aa6de 100644 (file)
--- a/src/theory/model_manager.h
+++ b/src/theory/model_manager.h
@@ -20,6 +20,7 @@
 
 #include <memory>
 
+#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 279be5e10b691c696ba2e31ff32de3bd9132d282..126c94749e94a41492efab415665d845b9c98ecb 100644 (file)
--- 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 cd9445bb0a7131b165fb294a90eb21574bcbe033..72f3d78ac2b7453637b0b08b4bffcf0d228dcef3 100644 (file)
--- 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 5c44f896899c92f7038f37f130645fa9c01c393f..4969661496cd8b23d621991460991e278dfb0af8 100644 (file)
--- 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 291cd1905b1a861a53cf304af4d839956db656e5..4cc25a887f1f829bce2c31e20248b04b302fce58 100644 (file)
--- 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 6841a11d857fa9ae511ccdf2199a0fbef1e855e9..4a6492aaa115785297d72acf138344a3de1800e4 100644 (file)
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -21,6 +21,7 @@
 #include <unordered_map>
 #include <unordered_set>
 
+#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 2acbe2388c29a635ac40936cd0e8c613b1bb9f0e..23a76d2732c60af01e9f2c0311f974dde551e4fe 100644 (file)
--- 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<Node>& aes)

diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h
index 71458a913df24ccf845fccc5f7e1c36775d71353..dd11a3d2ec5de1991f5d08bad546f630c326d7be 100644 (file)
--- a/src/theory/theory_model_builder.h
+++ b/src/theory/theory_model_builder.h
@@ -21,6 +21,7 @@
 #include <unordered_map>
 #include <unordered_set>
 
+#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<Node, Node> NodeMap;
   typedef std::unordered_set<Node> NodeSet;
@@ -315,9 +316,6 @@ class TheoryEngineModelBuilder
                             Node v,
                             std::map<Node, bool>& 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 72ab24a7edb2280c4dcabbee7375ca08e9b2e311..e3655e3ab7261963bec579a9c9357c17e77c1bb2 100644 (file)
--- 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 cc58347bf1141cfa77d3e255065035cc9837e21d..9162fdeb6277b2f9ee928c9058be2ad216f61a99 100644 (file)
--- 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).