Make theory engine modules use Env (#7277)

This updates several core modules of TheoryEngine to use Env and eliminates some getters from TheoryEngine.

diff --git a/src/theory/combination_care_graph.cpp b/src/theory/combination_care_graph.cpp
index 4b0adf56b53ec3b2230b42b0e665a499e417745f..c0d75ceaaa2ecfa51c2b49bdb271f3d4ed9db35e 100644 (file)
--- a/src/theory/combination_care_graph.cpp
+++ b/src/theory/combination_care_graph.cpp
@@ -26,11 +26,8 @@ namespace cvc5 {
 namespace theory {
 
 CombinationCareGraph::CombinationCareGraph(
-    TheoryEngine& te,
-    Env& env,
-    const std::vector<Theory*>& paraTheories,
-    ProofNodeManager* pnm)
-    : CombinationEngine(te, env, paraTheories, pnm)
+    Env& env, TheoryEngine& te, const std::vector<Theory*>& paraTheories)
+    : CombinationEngine(env, te, paraTheories)
 {
 }
 

diff --git a/src/theory/combination_care_graph.h b/src/theory/combination_care_graph.h
index 971b81d1dd864c3fd3a7bcf4e94283105f0fc83b..afcf8e3a22cdedef42dac6b8f8c3141d499b50d1 100644 (file)
--- a/src/theory/combination_care_graph.h
+++ b/src/theory/combination_care_graph.h
@@ -35,10 +35,9 @@ namespace theory {
 class CombinationCareGraph : public CombinationEngine
 {
  public:
-  CombinationCareGraph(TheoryEngine& te,
-                       Env& env,
-                       const std::vector<Theory*>& paraTheories,
-                       ProofNodeManager* pnm);
+  CombinationCareGraph(Env& env,
+                       TheoryEngine& te,
+                       const std::vector<Theory*>& paraTheories);
   ~CombinationCareGraph();
 
   bool buildModel() override;

diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp
index 9352ce95c316335213a8c6c672569ba3b74ba3a1..dfa6d5da4788ec2ee09fef1ec12fc91054ccf9ad 100644 (file)
--- a/src/theory/combination_engine.cpp
+++ b/src/theory/combination_engine.cpp
@@ -28,45 +28,44 @@
 namespace cvc5 {
 namespace theory {
 
-CombinationEngine::CombinationEngine(TheoryEngine& te,
-                                     Env& env,
-                                     const std::vector<Theory*>& paraTheories,
-                                     ProofNodeManager* pnm)
+CombinationEngine::CombinationEngine(Env& env,
+                                     TheoryEngine& te,
+                                     const std::vector<Theory*>& paraTheories)
     : EnvObj(env),
       d_te(te),
       d_valuation(&te),
-      d_pnm(pnm),
+      d_pnm(env.isTheoryProofProducing() ? env.getProofNodeManager() : nullptr),
       d_logicInfo(te.getLogicInfo()),
       d_paraTheories(paraTheories),
       d_eemanager(nullptr),
       d_mmanager(nullptr),
       d_sharedSolver(nullptr),
-      d_cmbsPg(pnm ? new EagerProofGenerator(pnm, te.getUserContext())
-                   : nullptr)
+      d_cmbsPg(d_pnm ? new EagerProofGenerator(d_pnm, env.getUserContext())
+                     : nullptr)
 {
   // create the equality engine, model manager, and shared solver
   if (options::eeMode() == options::EqEngineMode::DISTRIBUTED)
   {
     // use the distributed shared solver
-    d_sharedSolver.reset(new SharedSolverDistributed(d_te, d_pnm));
+    d_sharedSolver.reset(new SharedSolverDistributed(env, d_te));
     // make the distributed equality engine manager
     d_eemanager.reset(
-        new EqEngineManagerDistributed(d_te, *d_sharedSolver.get()));
+        new EqEngineManagerDistributed(env, d_te, *d_sharedSolver.get()));
     // make the distributed model manager
     d_mmanager.reset(
-        new ModelManagerDistributed(d_te, d_env, *d_eemanager.get()));
+        new ModelManagerDistributed(env, d_te, *d_eemanager.get()));
   }
   else if (options::eeMode() == options::EqEngineMode::CENTRAL)
   {
     // for now, the shared solver is the same in both approaches; use the
     // distributed one for now
-    d_sharedSolver.reset(new SharedSolverDistributed(d_te, d_pnm));
+    d_sharedSolver.reset(new SharedSolverDistributed(env, d_te));
     // make the central equality engine manager
     d_eemanager.reset(
-        new EqEngineManagerCentral(d_te, *d_sharedSolver.get(), d_pnm));
+        new EqEngineManagerCentral(env, d_te, *d_sharedSolver.get()));
     // make the distributed model manager
     d_mmanager.reset(
-        new ModelManagerDistributed(d_te, d_env, *d_eemanager.get()));
+        new ModelManagerDistributed(env, d_te, *d_eemanager.get()));
   }
   else
   {

diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h
index f7da01facda2db272446c101bbfbe32f412ebb40..15f379dc0212d5c4a1969ddec862ca790ac5472b 100644 (file)
--- a/src/theory/combination_engine.h
+++ b/src/theory/combination_engine.h
@@ -46,10 +46,9 @@ class SharedSolver;
 class CombinationEngine : protected EnvObj
 {
  public:
-  CombinationEngine(TheoryEngine& te,
-                    Env& env,
-                    const std::vector<Theory*>& paraTheories,
-                    ProofNodeManager* pnm);
+  CombinationEngine(Env& env,
+                    TheoryEngine& te,
+                    const std::vector<Theory*>& paraTheories);
   virtual ~CombinationEngine();
 
   /** Finish initialization */

diff --git a/src/theory/ee_manager.cpp b/src/theory/ee_manager.cpp
index c02710f77776305f3317daa18acf024e645b914c..a91aea94ea27ea44ad4f3a4bd39060c7ec8cf1e5 100644 (file)
--- a/src/theory/ee_manager.cpp
+++ b/src/theory/ee_manager.cpp
@@ -20,8 +20,8 @@
 namespace cvc5 {
 namespace theory {
 
-EqEngineManager::EqEngineManager(TheoryEngine& te, SharedSolver& shs)
-    : d_te(te), d_sharedSolver(shs)
+EqEngineManager::EqEngineManager(Env& env, TheoryEngine& te, SharedSolver& shs)
+    : EnvObj(env), d_te(te), d_sharedSolver(shs)
 {
 }
 

diff --git a/src/theory/ee_manager.h b/src/theory/ee_manager.h
index 51216a614f72a5255f4f8e48697998701f37f41f..228c0418a89cabbd123760375fb494eb4fc4c60c 100644 (file)
--- a/src/theory/ee_manager.h
+++ b/src/theory/ee_manager.h
@@ -21,6 +21,7 @@
 #include <map>
 #include <memory>
 
+#include "smt/env_obj.h"
 #include "theory/ee_setup_info.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
@@ -51,7 +52,7 @@ struct EeTheoryInfo
 };
 
 /** Virtual base class for equality engine managers */
-class EqEngineManager
+class EqEngineManager : protected EnvObj
 {
  public:
    /**
@@ -59,7 +60,7 @@ class EqEngineManager
    * @param sharedSolver The shared solver that is being used in combination
    * with this equality engine manager
     */
-  EqEngineManager(TheoryEngine& te, SharedSolver& shs);
+  EqEngineManager(Env& env, TheoryEngine& te, SharedSolver& shs);
   virtual ~EqEngineManager() {}
   /**
    * Initialize theories, called during TheoryEngine::finishInit after theory

diff --git a/src/theory/ee_manager_central.cpp b/src/theory/ee_manager_central.cpp
index 23946512ef81a378be7f8e288fe757e36d37b085..0e6610833f3da04dc96a16e1bd29ff7fd5e673fb 100644 (file)
--- a/src/theory/ee_manager_central.cpp
+++ b/src/theory/ee_manager_central.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/ee_manager_central.h"
 
+#include "smt/env.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/shared_solver.h"
 #include "theory/theory_engine.h"
@@ -23,15 +24,14 @@
 namespace cvc5 {
 namespace theory {
 
-EqEngineManagerCentral::EqEngineManagerCentral(TheoryEngine& te,
-                                               SharedSolver& shs,
-                                               ProofNodeManager* pnm)
-    : EqEngineManager(te, shs),
+EqEngineManagerCentral::EqEngineManagerCentral(Env& env,
+                                               TheoryEngine& te,
+                                               SharedSolver& shs)
+    : EqEngineManager(env, te, shs),
       d_masterEENotify(nullptr),
       d_masterEqualityEngine(nullptr),
       d_centralEENotify(*this),
-      d_centralEqualityEngine(
-          d_centralEENotify, te.getSatContext(), "central::ee", true)
+      d_centralEqualityEngine(d_centralEENotify, context(), "central::ee", true)
 {
   for (TheoryId theoryId = theory::THEORY_FIRST;
        theoryId != theory::THEORY_LAST;
@@ -39,12 +39,12 @@ EqEngineManagerCentral::EqEngineManagerCentral(TheoryEngine& te,
   {
     d_theoryNotify[theoryId] = nullptr;
   }
-  if (pnm != nullptr)
+  if (env.isTheoryProofProducing())
   {
-    d_centralPfee.reset(new eq::ProofEqEngine(d_te.getSatContext(),
-                                              d_te.getUserContext(),
+    d_centralPfee.reset(new eq::ProofEqEngine(context(),
+                                              userContext(),
                                               d_centralEqualityEngine,
-                                              pnm));
+                                              env.getProofNodeManager()));
     d_centralEqualityEngine.setProofEqualityEngine(d_centralPfee.get());
   }
 }
@@ -53,7 +53,7 @@ EqEngineManagerCentral::~EqEngineManagerCentral() {}
 
 void EqEngineManagerCentral::initializeTheories()
 {
-  context::Context* c = d_te.getSatContext();
+  context::Context* c = context();
   // initialize the shared solver
   EeSetupInfo esis;
   if (d_sharedSolver.needsEqualityEngine(esis))
@@ -113,7 +113,7 @@ void EqEngineManagerCentral::initializeTheories()
     if (!masterEqToCentral)
     {
       d_masterEqualityEngineAlloc.reset(new eq::EqualityEngine(
-          *d_masterEENotify.get(), d_te.getSatContext(), "master::ee", false));
+          *d_masterEENotify.get(), c, "master::ee", false));
       d_masterEqualityEngine = d_masterEqualityEngineAlloc.get();
     }
     else

diff --git a/src/theory/ee_manager_central.h b/src/theory/ee_manager_central.h
index eb13b7820564fff9d59057c3dbf4cb12954c2624..f5a34b11ef894c1674871aef65f3e1a7c0708784 100644 (file)
--- a/src/theory/ee_manager_central.h
+++ b/src/theory/ee_manager_central.h
@@ -54,9 +54,7 @@ namespace theory {
 class EqEngineManagerCentral : public EqEngineManager
 {
  public:
-  EqEngineManagerCentral(TheoryEngine& te,
-                         SharedSolver& shs,
-                         ProofNodeManager* pnm);
+  EqEngineManagerCentral(Env& env, TheoryEngine& te, SharedSolver& shs);
   ~EqEngineManagerCentral();
   /**
    * Initialize theories. This method allocates unique equality engines

diff --git a/src/theory/ee_manager_distributed.cpp b/src/theory/ee_manager_distributed.cpp
index 7e4932767e13d2d346fc4f9cafa9db2026405f73..6dee1910b377e6dc15e5d7cce545f42e8bad3027 100644 (file)
--- a/src/theory/ee_manager_distributed.cpp
+++ b/src/theory/ee_manager_distributed.cpp
@@ -23,9 +23,10 @@
 namespace cvc5 {
 namespace theory {
 
-EqEngineManagerDistributed::EqEngineManagerDistributed(TheoryEngine& te,
+EqEngineManagerDistributed::EqEngineManagerDistributed(Env& env,
+                                                       TheoryEngine& te,
                                                        SharedSolver& shs)
-    : EqEngineManager(te, shs), d_masterEENotify(nullptr)
+    : EqEngineManager(env, te, shs), d_masterEENotify(nullptr)
 {
 }
 
@@ -35,7 +36,7 @@ EqEngineManagerDistributed::~EqEngineManagerDistributed()
 
 void EqEngineManagerDistributed::initializeTheories()
 {
-  context::Context* c = d_te.getSatContext();
+  context::Context* c = context();
   // initialize the shared solver
   EeSetupInfo esis;
   if (d_sharedSolver.needsEqualityEngine(esis))
@@ -49,7 +50,7 @@ void EqEngineManagerDistributed::initializeTheories()
     Unhandled() << "Expected shared solver to use equality engine";
   }
 
-  const LogicInfo& logicInfo = d_te.getLogicInfo();
+  const LogicInfo& logicInfo = d_env.getLogicInfo();
   if (logicInfo.isQuantified())
   {
     // construct the master equality engine
@@ -57,10 +58,8 @@ void EqEngineManagerDistributed::initializeTheories()
     QuantifiersEngine* qe = d_te.getQuantifiersEngine();
     Assert(qe != nullptr);
     d_masterEENotify.reset(new quantifiers::MasterNotifyClass(qe));
-    d_masterEqualityEngine.reset(new eq::EqualityEngine(*d_masterEENotify.get(),
-                                                        d_te.getSatContext(),
-                                                        "theory::master",
-                                                        false));
+    d_masterEqualityEngine.reset(new eq::EqualityEngine(
+        *d_masterEENotify.get(), c, "theory::master", false));
   }
   // allocate equality engines per theory
   for (TheoryId theoryId = theory::THEORY_FIRST;

diff --git a/src/theory/ee_manager_distributed.h b/src/theory/ee_manager_distributed.h
index 8c7bb261802f7b71830270d680c91355f1839ab2..3aaadbc2e27c25fa3252078fc3809eb906e1b5f1 100644 (file)
--- a/src/theory/ee_manager_distributed.h
+++ b/src/theory/ee_manager_distributed.h
@@ -49,7 +49,7 @@ class EqualityEngine;
 class EqEngineManagerDistributed : public EqEngineManager
 {
  public:
-  EqEngineManagerDistributed(TheoryEngine& te, SharedSolver& shs);
+  EqEngineManagerDistributed(Env& env, TheoryEngine& te, SharedSolver& shs);
   ~EqEngineManagerDistributed();
   /**
    * Initialize theories. This method allocates unique equality engines

diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp
index dd06d4afd56845839d0fc4581cdf4c12e04d07d2..23cd6430f0f502d8a8c6cf8123ebe6210e439fc3 100644 (file)
--- a/src/theory/model_manager.cpp
+++ b/src/theory/model_manager.cpp
@@ -27,7 +27,7 @@
 namespace cvc5 {
 namespace theory {
 
-ModelManager::ModelManager(TheoryEngine& te, Env& env, EqEngineManager& eem)
+ModelManager::ModelManager(Env& env, TheoryEngine& te, EqEngineManager& eem)
     : EnvObj(env),
       d_te(te),
       d_eem(eem),

diff --git a/src/theory/model_manager.h b/src/theory/model_manager.h
index 2a62c8be056bd1230149cae81f6126a33f1aa6de..4e86b11346ee38074f60914984bfe6b52c7c8ea9 100644 (file)
--- a/src/theory/model_manager.h
+++ b/src/theory/model_manager.h
@@ -44,7 +44,7 @@ class TheoryModel;
 class ModelManager : protected EnvObj
 {
  public:
-  ModelManager(TheoryEngine& te, Env& env, EqEngineManager& eem);
+  ModelManager(Env& env, TheoryEngine& te, EqEngineManager& eem);
   virtual ~ModelManager();
   /**
    * Finish initializing this class, which allocates the model, the model

diff --git a/src/theory/model_manager_distributed.cpp b/src/theory/model_manager_distributed.cpp
index 91e4cb6d4a7de7ddbdbdf972e3629078ba7204f1..f81c39f898a7572a6c2f07e9db07cd6d14dae668 100644 (file)
--- a/src/theory/model_manager_distributed.cpp
+++ b/src/theory/model_manager_distributed.cpp
@@ -23,10 +23,10 @@
 namespace cvc5 {
 namespace theory {
 
-ModelManagerDistributed::ModelManagerDistributed(TheoryEngine& te,
-                                                 Env& env,
+ModelManagerDistributed::ModelManagerDistributed(Env& env,
+                                                 TheoryEngine& te,
                                                  EqEngineManager& eem)
-    : ModelManager(te, env, eem)
+    : ModelManager(env, te, eem)
 {
 }
 

diff --git a/src/theory/model_manager_distributed.h b/src/theory/model_manager_distributed.h
index 322e61a983b38fd485e93608e9314908d8817355..04aa6788ba21b8f2c3ecf573d364e6b72e2df66c 100644 (file)
--- a/src/theory/model_manager_distributed.h
+++ b/src/theory/model_manager_distributed.h
@@ -38,7 +38,7 @@ namespace theory {
 class ModelManagerDistributed : public ModelManager
 {
  public:
-  ModelManagerDistributed(TheoryEngine& te, Env& env, EqEngineManager& eem);
+  ModelManagerDistributed(Env& env, TheoryEngine& te, EqEngineManager& eem);
   ~ModelManagerDistributed();
 
   /** Prepare the model, as described above. */

diff --git a/src/theory/shared_solver.cpp b/src/theory/shared_solver.cpp
index 95558ead164ea08c1399ead1b0920fa595e1cf96..a503c55954adae09df6f1b873a3764b1099f9205 100644 (file)
--- a/src/theory/shared_solver.cpp
+++ b/src/theory/shared_solver.cpp
@@ -30,12 +30,13 @@ namespace theory {
 // In distributed equality engine management, shared terms database also
 // maintains an equality engine. In central equality engine management,
 // it does not.
-SharedSolver::SharedSolver(TheoryEngine& te, ProofNodeManager* pnm)
-    : d_te(te),
-      d_logicInfo(te.getLogicInfo()),
-      d_sharedTerms(&d_te, d_te.getSatContext(), d_te.getUserContext(), pnm),
-      d_preRegistrationVisitor(&te, d_te.getSatContext()),
-      d_sharedTermsVisitor(&te, d_sharedTerms, d_te.getSatContext()),
+SharedSolver::SharedSolver(Env& env, TheoryEngine& te)
+    : EnvObj(env),
+      d_te(te),
+      d_logicInfo(logicInfo()),
+      d_sharedTerms(env, &d_te),
+      d_preRegistrationVisitor(&te, context()),
+      d_sharedTermsVisitor(&te, d_sharedTerms, context()),
       d_im(te.theoryOf(THEORY_BUILTIN)->getInferenceManager())
 {
 }

diff --git a/src/theory/shared_solver.h b/src/theory/shared_solver.h
index a7f9ceff594fb8978491be69a09bacda00bda017..d423b59832424bef5af76a13b66000df33495c7d 100644 (file)
--- a/src/theory/shared_solver.h
+++ b/src/theory/shared_solver.h
@@ -19,6 +19,7 @@
 #define CVC5__THEORY__SHARED_SOLVER__H
 
 #include "expr/node.h"
+#include "smt/env_obj.h"
 #include "theory/inference_id.h"
 #include "theory/shared_terms_database.h"
 #include "theory/term_registration_visitor.h"
@@ -44,10 +45,10 @@ class TheoryInferenceManager;
  * (2) Be the official interface for equality statuses,
  * (3) Propagate equalities to TheoryEngine when necessary and explain them.
  */
-class SharedSolver
+class SharedSolver : protected EnvObj
 {
  public:
-  SharedSolver(TheoryEngine& te, ProofNodeManager* pnm);
+  SharedSolver(Env& env, TheoryEngine& te);
   virtual ~SharedSolver() {}
   //------------------------------------- initialization
   /**

diff --git a/src/theory/shared_solver_distributed.cpp b/src/theory/shared_solver_distributed.cpp
index 3c78a75f897944c37bf4a09f783948e8114dc7f8..1399bac1816d86790fcdb576cf3c54fbf92157f7 100644 (file)
--- a/src/theory/shared_solver_distributed.cpp
+++ b/src/theory/shared_solver_distributed.cpp
@@ -20,9 +20,8 @@
 namespace cvc5 {
 namespace theory {
 
-SharedSolverDistributed::SharedSolverDistributed(TheoryEngine& te,
-                                                 ProofNodeManager* pnm)
-    : SharedSolver(te, pnm)
+SharedSolverDistributed::SharedSolverDistributed(Env& env, TheoryEngine& te)
+    : SharedSolver(env, te)
 {
 }
 

diff --git a/src/theory/shared_solver_distributed.h b/src/theory/shared_solver_distributed.h
index f9a00230ba16504d3f116b9093940d4e59e45bbc..3e7d81e30976f0d304d0b594f6b2a30cd97ab230 100644 (file)
--- a/src/theory/shared_solver_distributed.h
+++ b/src/theory/shared_solver_distributed.h
@@ -31,7 +31,7 @@ namespace theory {
 class SharedSolverDistributed : public SharedSolver
 {
  public:
-  SharedSolverDistributed(TheoryEngine& te, ProofNodeManager* pnm);
+  SharedSolverDistributed(Env& env, TheoryEngine& te);
   virtual ~SharedSolverDistributed() {}
   //------------------------------------- initialization
   /**

diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index a4a846e053ae63671768b2cdd42e1b6b130a6b9b..e4f1b6fabd014d0a8f3cb0bcfcdf3e43f99a0258 100644 (file)
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -24,26 +24,23 @@ using namespace cvc5::theory;
 
 namespace cvc5 {
 
-SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine,
-                                         context::Context* context,
-                                         context::UserContext* userContext,
-                                         ProofNodeManager* pnm)
-    : ContextNotifyObj(context),
+SharedTermsDatabase::SharedTermsDatabase(Env& env, TheoryEngine* theoryEngine)
+    : ContextNotifyObj(env.getContext()),
+      d_env(env),
       d_statSharedTerms(
           smtStatisticsRegistry().registerInt("theory::shared_terms")),
-      d_addedSharedTermsSize(context, 0),
-      d_termsToTheories(context),
-      d_alreadyNotifiedMap(context),
-      d_registeredEqualities(context),
+      d_addedSharedTermsSize(env.getContext(), 0),
+      d_termsToTheories(env.getContext()),
+      d_alreadyNotifiedMap(env.getContext()),
+      d_registeredEqualities(env.getContext()),
       d_EENotify(*this),
       d_theoryEngine(theoryEngine),
-      d_inConflict(context, false),
+      d_inConflict(env.getContext(), false),
       d_conflictPolarity(),
-      d_satContext(context),
-      d_userContext(userContext),
+      d_satContext(env.getContext()),
+      d_userContext(env.getUserContext()),
       d_equalityEngine(nullptr),
-      d_pfee(nullptr),
-      d_pnm(pnm)
+      d_pfee(nullptr)
 {
 }
 
@@ -52,13 +49,14 @@ void SharedTermsDatabase::setEqualityEngine(eq::EqualityEngine* ee)
   Assert(ee != nullptr);
   d_equalityEngine = ee;
   // if proofs are enabled, make the proof equality engine if necessary
-  if (d_pnm != nullptr)
+  if (d_env.isTheoryProofProducing())
   {
     d_pfee = d_equalityEngine->getProofEqualityEngine();
     if (d_pfee == nullptr)
     {
+      ProofNodeManager* pnm = d_env.getProofNodeManager();
       d_pfeeAlloc.reset(
-          new eq::ProofEqEngine(d_satContext, d_userContext, *ee, d_pnm));
+          new eq::ProofEqEngine(d_satContext, d_userContext, *ee, pnm));
       d_pfee = d_pfeeAlloc.get();
       d_equalityEngine->setProofEqualityEngine(d_pfee);
     }

diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index ddb1a4043bcbc46238ee4e864974f589203a3d44..3b21c27a8dad195a48b30e19463ee1555d33ba1c 100644 (file)
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -32,6 +32,7 @@
 
 namespace cvc5 {
 
+class Env;
 class TheoryEngine;
 
 class SharedTermsDatabase : public context::ContextNotifyObj {
@@ -43,6 +44,9 @@ class SharedTermsDatabase : public context::ContextNotifyObj {
   typedef shared_terms_list::const_iterator shared_terms_iterator;
 
  private:
+  /** Reference to the env */
+  Env& d_env;
+
   /** Some statistics */
   IntStat d_statSharedTerms;
 
@@ -158,10 +162,7 @@ class SharedTermsDatabase : public context::ContextNotifyObj {
    * @param pnm The proof node manager to use, which is non-null if proofs
    * are enabled.
    */
-  SharedTermsDatabase(TheoryEngine* theoryEngine,
-                      context::Context* context,
-                      context::UserContext* userContext,
-                      ProofNodeManager* pnm);
+  SharedTermsDatabase(Env& env, TheoryEngine* theoryEngine);
 
   //-------------------------------------------- initialization
   /** Called to set the equality engine. */

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 6fbac94e5da1fe582d483fd7c4a45f28a50b295e..13a812bb272911ca5288026f62a22980ef4964f9 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -147,7 +147,7 @@ void TheoryEngine::finishInit()
   // Initialize the theory combination architecture
   if (options::tcMode() == options::TcMode::CARE_GRAPH)
   {
-    d_tc.reset(new CombinationCareGraph(*this, d_env, paraTheories, d_pnm));
+    d_tc.reset(new CombinationCareGraph(d_env, *this, paraTheories));
   }
   else
   {
@@ -205,15 +205,6 @@ void TheoryEngine::finishInit()
   Trace("theory") << "End TheoryEngine::finishInit" << std::endl;
 }
 
-ProofNodeManager* TheoryEngine::getProofNodeManager() const { return d_pnm; }
-
-context::Context* TheoryEngine::getSatContext() const { return context(); }
-
-context::UserContext* TheoryEngine::getUserContext() const
-{
-  return userContext();
-}
-
 TheoryEngine::TheoryEngine(Env& env)
     : EnvObj(env),
       d_propEngine(nullptr),

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 4e8beb9673bf7cd1dee0e91fffc947f248b06605..b1ab0a001b47fde1b1d2ece22c1a15915664acc7 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -156,19 +156,6 @@ class TheoryEngine : protected EnvObj
    */
   prop::PropEngine* getPropEngine() const { return d_propEngine; }
 
-  /** Get the proof node manager */
-  ProofNodeManager* getProofNodeManager() const;
-
-  /**
-   * Get a pointer to the underlying sat context.
-   */
-  context::Context* getSatContext() const;
-
-  /**
-   * Get a pointer to the underlying user context.
-   */
-  context::UserContext* getUserContext() const;
-
   /**
    * Get a pointer to the underlying quantifiers engine.
    */