diff options
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, 3 insertions, 31 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3e9b81263..89f3acd56 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -850,7 +850,6 @@ 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), @@ -935,12 +934,8 @@ 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(), @@ -948,7 +943,6 @@ 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(); @@ -1033,9 +1027,6 @@ void SmtEngine::shutdown() { if(d_theoryEngine != NULL) { d_theoryEngine->shutdown(); } - if(d_decisionEngine != NULL) { - d_decisionEngine->shutdown(); - } } SmtEngine::~SmtEngine() @@ -1092,8 +1083,6 @@ SmtEngine::~SmtEngine() d_theoryEngine = NULL; delete d_propEngine; d_propEngine = NULL; - delete d_decisionEngine; - d_decisionEngine = NULL; delete d_stats; d_stats = NULL; @@ -3100,22 +3089,6 @@ 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; @@ -3616,10 +3589,11 @@ 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_decisionEngine->addAssertions(d_assertions); + d_smt.d_propEngine->addAssertionsToDecisionEngine(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 0ef22f353..1424352ef 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -1059,9 +1059,7 @@ 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 */ |