diff options
-rw-r--r-- | src/decision/decision_engine.cpp | 10 | ||||
-rw-r--r-- | src/decision/decision_engine.h | 9 | ||||
-rw-r--r-- | src/preprocessing/passes/bool_to_bv.cpp | 3 | ||||
-rw-r--r-- | src/preprocessing/passes/bv_to_bool.cpp | 3 | ||||
-rw-r--r-- | src/prop/cnf_stream.cpp | 13 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 10 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 9 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 3 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 12 | ||||
-rw-r--r-- | src/theory/bv/bitblast/eager_bitblaster.cpp | 13 | ||||
-rw-r--r-- | src/theory/bv/bitblast/lazy_bitblaster.cpp | 16 | ||||
-rw-r--r-- | test/unit/prop/cnf_stream_white.h | 3 |
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 |