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.

12 files changed, 64 insertions, 40 deletions

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index e12ae6127..4ae900e85 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -25,7 +25,9 @@ using namespace std;
 
 namespace CVC4 {
 
-DecisionEngine::DecisionEngine(context::Context* sc, context::UserContext* uc)
+DecisionEngine::DecisionEngine(context::Context* sc,
+                               context::UserContext* uc,
+                               ResourceManager* rm)
     : d_enabledITEStrategy(nullptr),
       d_needIteSkolemMap(),
       d_relevancyStrategy(nullptr),
@@ -35,7 +37,8 @@ DecisionEngine::DecisionEngine(context::Context* sc, context::UserContext* uc)
       d_satContext(sc),
       d_userContext(uc),
       d_result(sc, SAT_VALUE_UNKNOWN),
-      d_engineState(0)
+      d_engineState(0),
+      d_resourceManager(rm)
 {
   Trace("decision") << "Creating decision engine" << std::endl;
 }
@@ -71,8 +74,7 @@ void DecisionEngine::shutdown()
 
 SatLiteral DecisionEngine::getNext(bool& stopSearch)
 {
-  NodeManager::currentResourceManager()->spendResource(
-      ResourceManager::Resource::DecisionStep);
+  d_resourceManager->spendResource(ResourceManager::Resource::DecisionStep);
   Assert(d_cnfStream != nullptr)
       << "Forgot to set cnfStream for decision engine?";
   Assert(d_satSolver != nullptr)
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index c4eb29284..65ead8d4c 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -60,11 +60,16 @@ class DecisionEngine {
 
   // init/shutdown state
   unsigned d_engineState;    // 0=pre-init; 1=init,pre-shutdown; 2=shutdown
-public:
+  /** Pointer to resource manager for associated SmtEngine */
+  ResourceManager* d_resourceManager;
+
+ public:
   // Necessary functions
 
   /** Constructor */
-  DecisionEngine(context::Context *sc, context::UserContext *uc);
+  DecisionEngine(context::Context* sc,
+                 context::UserContext* uc,
+                 ResourceManager* rm);
 
   /** Destructor, currently does nothing */
   ~DecisionEngine() {
diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp
index b4d638595..e18e6f6c6 100644
--- a/src/preprocessing/passes/bool_to_bv.cpp
+++ b/src/preprocessing/passes/bool_to_bv.cpp
@@ -37,8 +37,7 @@ BoolToBV::BoolToBV(PreprocessingPassContext* preprocContext)
 PreprocessingPassResult BoolToBV::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
-  NodeManager::currentResourceManager()->spendResource(
-      ResourceManager::Resource::PreprocessStep);
+  d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
 
   size_t size = assertionsToPreprocess->size();
 
diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp
index 5b10f6644..33b41210a 100644
--- a/src/preprocessing/passes/bv_to_bool.cpp
+++ b/src/preprocessing/passes/bv_to_bool.cpp
@@ -45,8 +45,7 @@ BVToBool::BVToBool(PreprocessingPassContext* preprocContext)
 PreprocessingPassResult BVToBool::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
-  NodeManager::currentResourceManager()->spendResource(
-      ResourceManager::Resource::PreprocessStep);
+  d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
   std::vector<Node> new_assertions;
   liftBvToBool(assertionsToPreprocess->ref(), new_assertions);
   for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
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.
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 240533fba..990ffd04d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -734,8 +734,10 @@ void SmtEngine::finishInit()
    * are unregistered by the obsolete PropEngine object before registered
    * again by the new PropEngine object */
   d_propEngine.reset(nullptr);
-  d_propEngine.reset(
-      new PropEngine(getTheoryEngine(), getContext(), getUserContext()));
+  d_propEngine.reset(new PropEngine(getTheoryEngine(),
+                                    getContext(),
+                                    getUserContext(),
+                                    d_private->getResourceManager()));
 
   Trace("smt-debug") << "Setting up theory engine..." << std::endl;
   d_theoryEngine->setPropEngine(getPropEngine());
@@ -3418,8 +3420,10 @@ void SmtEngine::resetAssertions()
    * statistics are unregistered by the obsolete PropEngine object before
    * registered again by the new PropEngine object */
   d_propEngine.reset(nullptr);
-  d_propEngine.reset(
-      new PropEngine(getTheoryEngine(), getContext(), getUserContext()));
+  d_propEngine.reset(new PropEngine(getTheoryEngine(),
+                                    getContext(),
+                                    getUserContext(),
+                                    d_private->getResourceManager()));
   d_theoryEngine->setPropEngine(getPropEngine());
 }
 
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index c4e3513bf..bddde4cb7 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -63,12 +63,13 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c)
     default: Unreachable() << "Unknown SAT solver type";
   }
   d_satSolver.reset(solver);
-  d_cnfStream.reset(
-      new prop::TseitinCnfStream(d_satSolver.get(),
-                                 d_bitblastingRegistrar.get(),
-                                 d_nullContext.get(),
-                                 options::proof(),
-                                 "EagerBitblaster"));
+  ResourceManager* rm = NodeManager::currentResourceManager();
+  d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(),
+                                               d_bitblastingRegistrar.get(),
+                                               d_nullContext.get(),
+                                               rm,
+                                               options::proof(),
+                                               "EagerBitblaster"));
 }
 
 EagerBitblaster::~EagerBitblaster() {}
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 06afa126d..463ffae79 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -79,12 +79,13 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c,
   d_satSolver.reset(
       prop::SatSolverFactory::createMinisat(c, smtStatisticsRegistry(), name));
 
-  d_cnfStream.reset(
-      new prop::TseitinCnfStream(d_satSolver.get(),
-                                 d_nullRegistrar.get(),
-                                 d_nullContext.get(),
-                                 options::proof(),
-                                 "LazyBitblaster"));
+  ResourceManager* rm = NodeManager::currentResourceManager();
+  d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(),
+                                               d_nullRegistrar.get(),
+                                               d_nullContext.get(),
+                                               rm,
+                                               options::proof(),
+                                               "LazyBitblaster"));
 
   d_satSolverNotify.reset(
       d_emptyNotify
@@ -578,8 +579,9 @@ void TLazyBitblaster::clearSolver() {
   // recreate sat solver
   d_satSolver.reset(
       prop::SatSolverFactory::createMinisat(d_ctx, smtStatisticsRegistry()));
+  ResourceManager* rm = NodeManager::currentResourceManager();
   d_cnfStream.reset(new prop::TseitinCnfStream(
-      d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get()));
+      d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get(), rm));
   d_satSolverNotify.reset(
       d_emptyNotify
           ? (prop::BVSatSolverNotify*)new MinisatEmptyNotify()
diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index b08221cf0..05daf074e 100644
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -145,8 +145,9 @@ class CnfStreamWhite : public CxxTest::TestSuite {
     d_satSolver = new FakeSatSolver();
     d_cnfContext = new context::Context();
     d_cnfRegistrar = new theory::TheoryRegistrar(d_theoryEngine);
+    ResourceManager * rm = d_nodeManager->getResourceManager();
     d_cnfStream = new CVC4::prop::TseitinCnfStream(
-        d_satSolver, d_cnfRegistrar, d_cnfContext);
+        d_satSolver, d_cnfRegistrar, d_cnfContext, rm);
   }
 
   void tearDown() override