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, 9 insertions, 14 deletions

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 547d24b23..1976177b7 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -30,35 +30,33 @@ namespace cvc5 {
 namespace theory {
 namespace bv {
 
-TheoryBV::TheoryBV(context::Context* c,
-                   context::UserContext* u,
+TheoryBV::TheoryBV(Env& env,
                    OutputChannel& out,
                    Valuation valuation,
-                   const LogicInfo& logicInfo,
-                   ProofNodeManager* pnm,
                    std::string name)
-    : Theory(THEORY_BV, c, u, out, valuation, logicInfo, pnm, name),
+    : Theory(THEORY_BV, env, out, valuation, name),
       d_internal(nullptr),
       d_rewriter(),
-      d_state(c, u, valuation),
+      d_state(getSatContext(), getUserContext(), valuation),
       d_im(*this, d_state, nullptr, "theory::bv::"),
       d_notify(d_im),
-      d_invalidateModelCache(c, true),
+      d_invalidateModelCache(getSatContext(), true),
       d_stats("theory::bv::")
 {
   switch (options::bvSolver())
   {
     case options::BVSolver::BITBLAST:
-      d_internal.reset(new BVSolverBitblast(&d_state, d_im, pnm));
+      d_internal.reset(new BVSolverBitblast(&d_state, d_im, d_pnm));
       break;
 
     case options::BVSolver::LAYERED:
-      d_internal.reset(new BVSolverLayered(*this, c, u, pnm, name));
+      d_internal.reset(new BVSolverLayered(
+          *this, getSatContext(), getUserContext(), d_pnm, name));
       break;
 
     default:
       AlwaysAssert(options::bvSolver() == options::BVSolver::BITBLAST_INTERNAL);
-      d_internal.reset(new BVSolverBitblastInternal(&d_state, d_im, pnm));
+      d_internal.reset(new BVSolverBitblastInternal(&d_state, d_im, d_pnm));
   }
   d_theoryState = &d_state;
   d_inferManager = &d_im;
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index da44d7022..b4afb5f5d 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -39,12 +39,9 @@ class TheoryBV : public Theory
   friend class BVSolverLayered;
 
  public:
-  TheoryBV(context::Context* c,
-           context::UserContext* u,
+  TheoryBV(Env& env,
            OutputChannel& out,
            Valuation valuation,
-           const LogicInfo& logicInfo,
-           ProofNodeManager* pnm = nullptr,
            std::string name = "");
 
   ~TheoryBV();