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.

2 files changed, 5 insertions, 15 deletions

diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index 1db03d22b..f12d2caf9 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -25,15 +25,10 @@ namespace cvc5 {
 namespace theory {
 namespace builtin {
 
-TheoryBuiltin::TheoryBuiltin(context::Context* c,
-                             context::UserContext* u,
-                             OutputChannel& out,
-                             Valuation valuation,
-                             const LogicInfo& logicInfo,
-                             ProofNodeManager* pnm)
-    : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo, pnm),
-      d_state(c, u, valuation),
-      d_im(*this, d_state, pnm, "theory::builtin::")
+TheoryBuiltin::TheoryBuiltin(Env& env, OutputChannel& out, Valuation valuation)
+    : Theory(THEORY_BUILTIN, env, out, valuation),
+      d_state(getSatContext(), getUserContext(), valuation),
+      d_im(*this, d_state, d_pnm, "theory::builtin::")
 {
   // indicate we are using the default theory state and inference managers
   d_theoryState = &d_state;
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index 72485f0ea..29a3cfb36 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -31,12 +31,7 @@ namespace builtin {
 class TheoryBuiltin : public Theory
 {
  public:
-  TheoryBuiltin(context::Context* c,
-                context::UserContext* u,
-                OutputChannel& out,
-                Valuation valuation,
-                const LogicInfo& logicInfo,
-                ProofNodeManager* pnm = nullptr);
+  TheoryBuiltin(Env& env, OutputChannel& out, Valuation valuation);
 
   /** get the official theory rewriter of this theory */
   TheoryRewriter* getTheoryRewriter() override;