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.

2 files changed, 13 insertions, 6 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() {