From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Fri, 3 Sep 2021 12:34:27 +0000 (-0700)
Subject: theory: Have more classes in theory with reference to Env derive from EnvObj. (#7130)
X-Git-Tag: cvc5-1.0.0~1278
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8e2c02201d30b5715a095ffe0098dd74a636ac85;p=cvc5.git

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 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<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 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 <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 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 <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 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 <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 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<Node>& 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 <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 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).