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.

1 files changed, 3 insertions, 29 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