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

This reverts commit bbba915f44f9e75eaa6238a10ba667643dacb00b.

2 files changed, 7 insertions, 21 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 546567b98..05704c0fa 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -75,12 +75,14 @@ public:
 };
 
 PropEngine::PropEngine(TheoryEngine* te,
+                       DecisionEngine* de,
                        Context* satContext,
-                       UserContext* userContext,
+                       Context* userContext,
                        std::ostream* replayLog,
                        ExprStream* replayStream)
     : d_inCheckSat(false),
       d_theoryEngine(te),
+      d_decisionEngine(de),
       d_context(satContext),
       d_theoryProxy(NULL),
       d_satSolver(NULL),
@@ -92,9 +94,6 @@ 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);
@@ -103,7 +102,7 @@ PropEngine::PropEngine(TheoryEngine* te,
 
   d_theoryProxy = new TheoryProxy(this,
                                   d_theoryEngine,
-                                  d_decisionEngine.get(),
+                                  d_decisionEngine,
                                   d_context,
                                   d_cnfStream,
                                   replayLog,
@@ -119,7 +118,6 @@ PropEngine::PropEngine(TheoryEngine* te,
 
 PropEngine::~PropEngine() {
   Debug("prop") << "Destructing the PropEngine" << endl;
-  d_decisionEngine->shutdown();
   delete d_cnfStream;
   delete d_registrar;
   delete d_satSolver;
@@ -144,12 +142,6 @@ 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;
 
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 707244ff5..061fbbca6 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -27,7 +27,6 @@
 #include "expr/expr_stream.h"
 #include "expr/node.h"
 #include "options/options.h"
-#include "preprocessing/assertion_pipeline.h"
 #include "proof/proof_manager.h"
 #include "util/resource_manager.h"
 #include "util/result.h"
@@ -61,8 +60,9 @@ class PropEngine
    * Create a PropEngine with a particular decision and theory engine.
    */
   PropEngine(TheoryEngine*,
+             DecisionEngine*,
              context::Context* satContext,
-             context::UserContext* userContext,
+             context::Context* userContext,
              std::ostream* replayLog,
              ExprStream* replayStream);
 
@@ -105,12 +105,6 @@ class PropEngine
                    TNode from = TNode::null());
 
   /**
-   * Pass a list of assertions from an AssertionPipeline to the decision engine.
-   */
-  void addAssertionsToDecisionEngine(
-      const preprocessing::AssertionPipeline& assertions);
-
-  /**
    * If ever n is decided upon, it must be in the given phase.  This
    * occurs *globally*, i.e., even if the literal is untranslated by
    * user pop and retranslated, it keeps this phase.  The associated
@@ -229,7 +223,7 @@ class PropEngine
   TheoryEngine* d_theoryEngine;
 
   /** The decision engine we will be using */
-  std::unique_ptr<DecisionEngine> d_decisionEngine;
+  DecisionEngine* d_decisionEngine;
 
   /** The context */
   context::Context* d_context;