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.

2 files changed, 10 insertions, 32 deletions

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index dc798626e..7d31d930f 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -56,20 +56,21 @@ void DecisionEngine::init()
   {
     ITEDecisionStrategy* ds =
       new decision::JustificationHeuristic(this, d_userContext, d_satContext);
-    enableStrategy(ds);
+    d_enabledStrategies.push_back(ds);
     d_needIteSkolemMap.push_back(ds);
   }
 }
 
-
-void DecisionEngine::enableStrategy(DecisionStrategy* ds)
+void DecisionEngine::shutdown()
 {
-  d_enabledStrategies.push_back(ds);
-}
+  Trace("decision") << "Shutting down decision engine" << std::endl;
 
-void DecisionEngine::clearStrategies(){
-  for(unsigned i = 0; i < d_enabledStrategies.size(); ++i){
-    delete d_enabledStrategies[i];
+  Assert(d_engineState == 1);
+  d_engineState = 2;
+
+  for (DecisionStrategy* s : d_enabledStrategies)
+  {
+    delete s;
   }
   d_enabledStrategies.clear();
   d_needIteSkolemMap.clear();
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 5ebcda8fe..afa306325 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -96,22 +96,12 @@ 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() {
-    Assert(d_engineState == 1);
-    d_engineState = 2;
-
-    Trace("decision") << "Shutting down decision engine" << std::endl;
-    clearStrategies();
-  }
+  void shutdown();
 
   // Interface for External World to use our services
 
@@ -170,11 +160,6 @@ 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.
    */
@@ -208,14 +193,6 @@ 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 */