summaryrefslogtreecommitdiff
path: root/src/prop/prop_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/prop_engine.cpp')
-rw-r--r--src/prop/prop_engine.cpp9
1 files changed, 5 insertions, 4 deletions
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback