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.

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index e12ae6127ec5f55ec8c2faa557aa75cd160aa91a..4ae900e854503c3dd0dd516f62897646c36cffd2 100644 (file)
--- 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 c4eb29284649db7c47f3850431a7312eae587cf5..65ead8d4ce15b6fa22c3de5fc4d302849a6c9da9 100644 (file)
--- 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 b4d638595cbc651f5cd8c9bb7fa51e8d4c943cfa..e18e6f6c6c041ab22450871d8ebcb11e4a5a9807 100644 (file)
--- 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 5b10f66449b71ba4a1041c3fd8dd041ebbaf02a1..33b41210a3d4ac02b0dc1af3e5df55bb7f428cab 100644 (file)
--- 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 aa5bb92d94e99e91e0833803736d7bfb9ab18eb7..73ae5c790016eb688ec661c93c3a43a953a26043 100644 (file)
--- 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 6b528bb81d98979ae4ff3b0ea95baf71bf4d1964..04ec91a68414a4687a30c0b0fca7bcdcd0b9eb4b 100644 (file)
--- 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 89b9191099f649c1145aa2f1216b5541f9e5958f..3ea604f82b49269f01a0778c5a578767b651f481 100644 (file)
--- 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 f1d73fc92bd24e183b4acdf2f0456c938ba39fb5..72ae52134f47445c69aa54cfda30b0296076de68 100644 (file)
--- 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 240533fba06bbaad48ca7dc4e7b5fafb1cab2d6e..990ffd04d77109f02c34258532a3067d81004699 100644 (file)
--- 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 c4e3513bfc2a31059db105f76956b63c6112fee3..bddde4cb76901eb44efc81adb5a54636b302fb8d 100644 (file)
--- 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 06afa126dacc1165226e8af025b261f38eae9f67..463ffae79ee20f02011e67730ab2b10f6b741e17 100644 (file)
--- 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 b08221cf057a3fec6e33ab5b9fd5685c6fa2056a..05daf074ec8f2a502e9cf941965d4ead04199a5f 100644 (file)
--- 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