Make Theory class use Env (#7011)

This PR changes the Theory base class and the constructors of all theories to use the Env class to access contexts, logic information and the proof node manager.

1 files changed, 13 insertions, 20 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 41f35601b..a857931a8 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -29,6 +29,7 @@
 #include "expr/node.h"
 #include "options/theory_options.h"
 #include "proof/trust_node.h"
+#include "smt/env.h"
 #include "theory/assertion.h"
 #include "theory/care_graph.h"
 #include "theory/logic_info.h"
@@ -105,14 +106,8 @@ class Theory {
   /** An integer identifying the type of the theory. */
   TheoryId d_id;
 
-  /** The SAT search context for the Theory. */
-  context::Context* d_satContext;
-
-  /** The user level assertion context for the Theory. */
-  context::UserContext* d_userContext;
-
-  /** Information about the logic we're operating within. */
-  const LogicInfo& d_logicInfo;
+  /** The environment class */
+  Env& d_env;
 
   /**
    * The assertFact() queue.
@@ -169,12 +164,9 @@ class Theory {
    * w.r.t. the SmtEngine.
    */
   Theory(TheoryId id,
-         context::Context* satContext,
-         context::UserContext* userContext,
+         Env& env,
          OutputChannel& out,
          Valuation valuation,
-         const LogicInfo& logicInfo,
-         ProofNodeManager* pnm,
          std::string instance = "");  // taking : No default.
 
   /**
@@ -241,9 +233,7 @@ class Theory {
    */
   inline Assertion get();
 
-  const LogicInfo& getLogicInfo() const {
-    return d_logicInfo;
-  }
+  const LogicInfo& getLogicInfo() const { return d_env.getLogicInfo(); }
 
   /**
    * Set separation logic heap. This is called when the location and data
@@ -455,17 +445,20 @@ class Theory {
   }
 
   /**
+   * Get a reference to the environment.
+   */
+  Env& getEnv() const { return d_env; }
+
+  /**
    * Get the SAT context associated to this Theory.
    */
-  context::Context* getSatContext() const {
-    return d_satContext;
-  }
+  context::Context* getSatContext() const { return d_env.getContext(); }
 
   /**
    * Get the context associated to this Theory.
    */
   context::UserContext* getUserContext() const {
-    return d_userContext;
+    return d_env.getUserContext();
   }
 
   /**
@@ -512,7 +505,7 @@ class Theory {
    */
   void assertFact(TNode assertion, bool isPreregistered) {
     Trace("theory") << "Theory<" << getId() << ">::assertFact["
-                    << d_satContext->getLevel() << "](" << assertion << ", "
+                    << getSatContext()->getLevel() << "](" << assertion << ", "
                     << (isPreregistered ? "true" : "false") << ")" << std::endl;
     d_facts.push_back(Assertion(assertion, isPreregistered));
   }