diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-03-05 13:17:55 -0800 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2020-03-05 13:17:55 -0800 |
commit | a4151cb6755b9267cb90f7facc0ffd367aa7f0f2 (patch) | |
tree | d8d5511eeb12ecace73845785546df95e8f67f1f /src/smt | |
parent | bbba915f44f9e75eaa6238a10ba667643dacb00b (diff) |
Revert "Move ownership of DecisionEngine into PropEngine. (#3850)"
This reverts commit bbba915f44f9e75eaa6238a10ba667643dacb00b.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 32 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 2 |
2 files changed, 31 insertions, 3 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 89f3acd56..3e9b81263 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -850,6 +850,7 @@ SmtEngine::SmtEngine(ExprManager* em) d_userLevels(), d_exprManager(em), d_nodeManager(d_exprManager->getNodeManager()), + d_decisionEngine(NULL), d_theoryEngine(NULL), d_propEngine(NULL), d_proofManager(NULL), @@ -934,8 +935,12 @@ void SmtEngine::finishInit() Trace("smt-debug") << "Making decision engine..." << std::endl; + d_decisionEngine = new DecisionEngine(d_context, d_userContext); + d_decisionEngine->init(); // enable appropriate strategies + Trace("smt-debug") << "Making prop engine..." << std::endl; d_propEngine = new PropEngine(d_theoryEngine, + d_decisionEngine, d_context, d_userContext, d_private->getReplayLog(), @@ -943,6 +948,7 @@ void SmtEngine::finishInit() Trace("smt-debug") << "Setting up theory engine..." << std::endl; d_theoryEngine->setPropEngine(d_propEngine); + d_theoryEngine->setDecisionEngine(d_decisionEngine); Trace("smt-debug") << "Finishing init for theory engine..." << std::endl; d_theoryEngine->finishInit(); @@ -1027,6 +1033,9 @@ void SmtEngine::shutdown() { if(d_theoryEngine != NULL) { d_theoryEngine->shutdown(); } + if(d_decisionEngine != NULL) { + d_decisionEngine->shutdown(); + } } SmtEngine::~SmtEngine() @@ -1083,6 +1092,8 @@ SmtEngine::~SmtEngine() d_theoryEngine = NULL; delete d_propEngine; d_propEngine = NULL; + delete d_decisionEngine; + d_decisionEngine = NULL; delete d_stats; d_stats = NULL; @@ -3089,6 +3100,22 @@ Result SmtEngine::check() { d_private->processAssertions(); Trace("smt") << "SmtEngine::check(): done processing assertions" << endl; + // Turn off stop only for QF_LRA + // TODO: Bring up in a meeting where to put this + if(options::decisionStopOnly() && !options::decisionMode.wasSetByUser() ){ + if( // QF_LRA + (not d_logic.isQuantified() && + d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() && !d_logic.areIntegersUsed() + )){ + if (d_private->getIteSkolemMap().empty()) + { + options::decisionStopOnly.set(false); + d_decisionEngine->clearStrategies(); + Trace("smt") << "SmtEngine::check(): turning off stop only" << endl; + } + } + } + TimerStat::CodeTimer solveTimer(d_stats->d_solveTime); Chat() << "solving..." << endl; @@ -3589,11 +3616,10 @@ void SmtEnginePrivate::processAssertions() { d_smt.d_theoryEngine->notifyPreprocessedAssertions( d_assertions.ref() ); // Push the formula to decision engine - if (noConflict) - { + if(noConflict) { Chat() << "pushing to decision engine..." << endl; Assert(iteRewriteAssertionsEnd == d_assertions.size()); - d_smt.d_propEngine->addAssertionsToDecisionEngine(d_assertions); + d_smt.d_decisionEngine->addAssertions(d_assertions); } // end: INVARIANT to maintain: no reordering of assertions or diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 1424352ef..0ef22f353 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -1059,7 +1059,9 @@ class CVC4_PUBLIC SmtEngine ExprManager* d_exprManager; /** Our internal expression/node manager */ NodeManager* d_nodeManager; + /** The decision engine */ + DecisionEngine* d_decisionEngine; /** The theory engine */ TheoryEngine* d_theoryEngine; /** The propositional engine */ |