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.

4 files changed, 23 insertions, 12 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index aa5bb92d9..73ae5c790 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -57,10 +57,14 @@ CnfStream::CnfStream(SatSolver* satSolver, Registrar* registrar,
       d_removable(false) {
 }
 
-TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar,
+TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver,
+                                   Registrar* registrar,
                                    context::Context* context,
-                                   bool fullLitToNodeMap, std::string name)
-  : CnfStream(satSolver, registrar, context, fullLitToNodeMap, name)
+                                   ResourceManager* rm,
+                                   bool fullLitToNodeMap,
+                                   std::string name)
+    : CnfStream(satSolver, registrar, context, fullLitToNodeMap, name),
+      d_resourceManager(rm)
 {}
 
 void CnfStream::assertClause(TNode node, SatClause& c) {
@@ -722,8 +726,7 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
                << ", negated = " << (negated ? "true" : "false") << ")" << endl;
 
   if (d_convertAndAssertCounter % ResourceManager::getFrequencyCount() == 0) {
-    NodeManager::currentResourceManager()->spendResource(
-        ResourceManager::Resource::CnfStep);
+    d_resourceManager->spendResource(ResourceManager::Resource::CnfStep);
     d_convertAndAssertCounter = 0;
   }
   ++d_convertAndAssertCounter;
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 6b528bb81..04ec91a68 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -253,11 +253,15 @@ class TseitinCnfStream : public CnfStream {
    * @param satSolver the sat solver to use
    * @param registrar the entity that takes care of pre-registration of Nodes
    * @param context the context that the CNF should respect.
+   * @param rm the resource manager of the CNF stream
    * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
    * even for non-theory literals
    */
-  TseitinCnfStream(SatSolver* satSolver, Registrar* registrar,
-                   context::Context* context, bool fullLitToNodeMap = false,
+  TseitinCnfStream(SatSolver* satSolver,
+                   Registrar* registrar,
+                   context::Context* context,
+                   ResourceManager* rm,
+                   bool fullLitToNodeMap = false,
                    std::string name = "");
 
   /**
@@ -313,6 +317,8 @@ class TseitinCnfStream : public CnfStream {
 
   void ensureLiteral(TNode n, bool noPreregistration = false) override;
 
+  /** Pointer to resource manager for associated SmtEngine */
+  ResourceManager* d_resourceManager;
 }; /* class TseitinCnfStream */
 
 } /* CVC4::prop namespace */
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);
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index f1d73fc92..72ae52134 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -61,7 +61,8 @@ class PropEngine
    */
   PropEngine(TheoryEngine*,
              context::Context* satContext,
-             context::UserContext* userContext);
+             context::UserContext* userContext,
+             ResourceManager* rm);
 
   /**
    * Destructor.