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

This reverts commit bbba915f44f9e75eaa6238a10ba667643dacb00b.

1 files changed, 24 insertions, 1 deletions

diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index afa306325..5ebcda8fe 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -96,12 +96,22 @@ public:
   /* enables decision stragies based on options */
   void init();
 
+  /* clears all of the strategies */
+  void clearStrategies();
+
+
   /**
    * This is called by SmtEngine, at shutdown time, just before
    * destruction.  It is important because there are destruction
    * ordering issues between some parts of the system.
    */
-  void shutdown();
+  void shutdown() {
+    Assert(d_engineState == 1);
+    d_engineState = 2;
+
+    Trace("decision") << "Shutting down decision engine" << std::endl;
+    clearStrategies();
+  }
 
   // Interface for External World to use our services
 
@@ -160,6 +170,11 @@ public:
 
   // External World helping us help the Strategies
 
+  /** If one of the enabled strategies needs them  */
+  /* bool needIteSkolemMap() { */
+  /*   return d_needIteSkolemMap.size() > 0; */
+  /* } */
+
   /**
    * Add a list of assertions from an AssertionPipeline.
    */
@@ -193,6 +208,14 @@ public:
   Node getNode(SatLiteral l) {
     return d_cnfStream->getNode(l);
   }
+
+private:
+  /**
+   * Enable a particular decision strategy, also updating
+   * corresponding vector<DecisionStrategy*>-s is the engine
+   */
+  void enableStrategy(DecisionStrategy* ds);
+
 };/* DecisionEngine class */
 
 }/* CVC4 namespace */