Revert "Move ownership of DecisionEngine into PropEngine. (#3850)"

This reverts commit bbba915f44f9e75eaa6238a10ba667643dacb00b.

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 */