Move env into smt solver, theory engine, prop engine (#6486)

This is work towards eliminating singletons.

Also, TheoryModel should use the same substitution map as the preprocessor. This is work towards unifying these things, which will be done in a future PR.

1 files changed, 18 insertions, 14 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 5903c1606..dfd4c4528 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -35,6 +35,7 @@
 #include "prop/sat_solver.h"
 #include "prop/sat_solver_factory.h"
 #include "prop/theory_proxy.h"
+#include "smt/env.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/output_channel.h"
 #include "theory/theory_engine.h"
@@ -65,15 +66,13 @@ public:
 };
 
 PropEngine::PropEngine(TheoryEngine* te,
-                       context::Context* satContext,
-                       context::UserContext* userContext,
-                       ResourceManager* rm,
+                       Env& env,
                        OutputManager& outMgr,
                        ProofNodeManager* pnm)
     : d_inCheckSat(false),
       d_theoryEngine(te),
-      d_context(satContext),
-      d_skdm(new SkolemDefManager(satContext, userContext)),
+      d_env(env),
+      d_skdm(new SkolemDefManager(d_env.getContext(), d_env.getUserContext())),
       d_theoryProxy(nullptr),
       d_satSolver(nullptr),
       d_pnm(pnm),
@@ -81,11 +80,13 @@ PropEngine::PropEngine(TheoryEngine* te,
       d_pfCnfStream(nullptr),
       d_ppm(nullptr),
       d_interrupted(false),
-      d_resourceManager(rm),
       d_outMgr(outMgr),
-      d_assumptions(userContext)
+      d_assumptions(d_env.getUserContext())
 {
   Debug("prop") << "Constructing the PropEngine" << std::endl;
+  context::Context* satContext = d_env.getContext();
+  context::UserContext* userContext = d_env.getUserContext();
+  ResourceManager* rm = d_env.getResourceManager();
 
   d_decisionEngine.reset(new DecisionEngine(satContext, userContext, rm));
   d_decisionEngine->init();  // enable appropriate strategies
@@ -112,9 +113,9 @@ PropEngine::PropEngine(TheoryEngine* te,
   d_theoryProxy->finishInit(d_cnfStream);
   // connect SAT solver
   d_satSolver->initialize(
-      d_context,
+      d_env.getContext(),
       d_theoryProxy,
-      userContext,
+      d_env.getUserContext(),
       options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS
           ? pnm
           : nullptr);
@@ -395,13 +396,16 @@ Result PropEngine::checkSat() {
   }
 
   if( result == SAT_VALUE_UNKNOWN ) {
-
+    ResourceManager* rm = d_env.getResourceManager();
     Result::UnknownExplanation why = Result::INTERRUPTED;
-    if (d_resourceManager->outOfTime())
+    if (rm->outOfTime())
+    {
       why = Result::TIMEOUT;
-    if (d_resourceManager->outOfResources())
+    }
+    if (rm->outOfResources())
+    {
       why = Result::RESOURCEOUT;
-
+    }
     return Result(Result::SAT_UNKNOWN, why);
   }
 
@@ -576,7 +580,7 @@ void PropEngine::interrupt()
 
 void PropEngine::spendResource(Resource r)
 {
-  d_resourceManager->spendResource(r);
+  d_env.getResourceManager()->spendResource(r);
 }
 
 bool PropEngine::properExplanation(TNode node, TNode expl) const