summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/decision/decision_engine.cpp10
-rw-r--r--src/decision/decision_engine.h9
-rw-r--r--src/preprocessing/passes/bool_to_bv.cpp3
-rw-r--r--src/preprocessing/passes/bv_to_bool.cpp3
-rw-r--r--src/prop/cnf_stream.cpp13
-rw-r--r--src/prop/cnf_stream.h10
-rw-r--r--src/prop/prop_engine.cpp9
-rw-r--r--src/prop/prop_engine.h3
-rw-r--r--src/smt/smt_engine.cpp12
-rw-r--r--src/theory/bv/bitblast/eager_bitblaster.cpp13
-rw-r--r--src/theory/bv/bitblast/lazy_bitblaster.cpp16
-rw-r--r--test/unit/prop/cnf_stream_white.h3
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback