diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-03-05 13:21:43 -0800 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2020-03-05 13:21:43 -0800 |
commit | 50f82fac417bc5b27ecaeb34d4e8034339c5982f (patch) | |
tree | 981c352e9aae8c96539374e98065101ee3835b28 /src/prop/prop_engine.cpp | |
parent | a4151cb6755b9267cb90f7facc0ffd367aa7f0f2 (diff) |
Move ownership of DecisionEngine into PropEngine. (#3850)
This is in preparation of fixing the issue we currently have with
reset-assertions. This also removes a competition hack for QF_LRA.
Diffstat (limited to 'src/prop/prop_engine.cpp')
-rw-r--r-- | src/prop/prop_engine.cpp | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 05704c0fa..546567b98 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -75,14 +75,12 @@ public: }; PropEngine::PropEngine(TheoryEngine* te, - DecisionEngine* de, Context* satContext, - Context* userContext, + UserContext* userContext, std::ostream* replayLog, ExprStream* replayStream) : d_inCheckSat(false), d_theoryEngine(te), - d_decisionEngine(de), d_context(satContext), d_theoryProxy(NULL), d_satSolver(NULL), @@ -94,6 +92,9 @@ PropEngine::PropEngine(TheoryEngine* te, Debug("prop") << "Constructing the PropEngine" << endl; + d_decisionEngine.reset(new DecisionEngine(satContext, userContext)); + d_decisionEngine->init(); // enable appropriate strategies + d_satSolver = SatSolverFactory::createDPLLMinisat(smtStatisticsRegistry()); d_registrar = new theory::TheoryRegistrar(d_theoryEngine); @@ -102,7 +103,7 @@ PropEngine::PropEngine(TheoryEngine* te, d_theoryProxy = new TheoryProxy(this, d_theoryEngine, - d_decisionEngine, + d_decisionEngine.get(), d_context, d_cnfStream, replayLog, @@ -118,6 +119,7 @@ PropEngine::PropEngine(TheoryEngine* te, PropEngine::~PropEngine() { Debug("prop") << "Destructing the PropEngine" << endl; + d_decisionEngine->shutdown(); delete d_cnfStream; delete d_registrar; delete d_satSolver; @@ -142,6 +144,12 @@ void PropEngine::assertLemma(TNode node, bool negated, d_cnfStream->convertAndAssert(node, removable, negated, rule, from); } +void PropEngine::addAssertionsToDecisionEngine( + const preprocessing::AssertionPipeline& assertions) +{ + d_decisionEngine->addAssertions(assertions); +} + void PropEngine::requirePhase(TNode n, bool phase) { Debug("prop") << "requirePhase(" << n << ", " << phase << ")" << endl; |