Towards proper use of resource managers (#4233)

Resource manager will be owned by SmtEngine in the future. This passes the resource manager cached by SmtEnginePrivate to the PropEngine created by SmtEngine instead of using the global pointer. It also makes a few preprocessing passes use the resource manager they already have access to and should use.

1 files changed, 5 insertions, 4 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 89b919109..3ea604f82 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -69,7 +69,8 @@ public:
 
 PropEngine::PropEngine(TheoryEngine* te,
                        Context* satContext,
-                       UserContext* userContext)
+                       UserContext* userContext,
+                       ResourceManager* rm)
     : d_inCheckSat(false),
       d_theoryEngine(te),
       d_context(satContext),
@@ -78,19 +79,19 @@ PropEngine::PropEngine(TheoryEngine* te,
       d_registrar(NULL),
       d_cnfStream(NULL),
       d_interrupted(false),
-      d_resourceManager(NodeManager::currentResourceManager())
+      d_resourceManager(rm)
 {
 
   Debug("prop") << "Constructing the PropEngine" << endl;
 
-  d_decisionEngine.reset(new DecisionEngine(satContext, userContext));
+  d_decisionEngine.reset(new DecisionEngine(satContext, userContext, rm));
   d_decisionEngine->init();  // enable appropriate strategies
 
   d_satSolver = SatSolverFactory::createDPLLMinisat(smtStatisticsRegistry());
 
   d_registrar = new theory::TheoryRegistrar(d_theoryEngine);
   d_cnfStream = new CVC4::prop::TseitinCnfStream(
-      d_satSolver, d_registrar, userContext, true);
+      d_satSolver, d_registrar, userContext, rm, true);
 
   d_theoryProxy = new TheoryProxy(
       this, d_theoryEngine, d_decisionEngine.get(), d_context, d_cnfStream);