From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Mon, 9 Mar 2020 21:54:30 +0000 (-0700)
Subject: DecisionEngine: Use unique_ptr for enabled strategies. (#3984)
X-Git-Tag: cvc5-1.0.0~3542
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=92fad93a38c20852468b1e1d017aee2e8d41467a;p=cvc5.git

DecisionEngine: Use unique_ptr for enabled strategies. (#3984)
---

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 7d31d930f..63a09ba2c 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -25,18 +25,17 @@ using namespace std;
 
 namespace CVC4 {
 
-DecisionEngine::DecisionEngine(context::Context *sc,
-                               context::UserContext *uc) :
-  d_enabledStrategies(),
-  d_needIteSkolemMap(),
-  d_relevancyStrategy(NULL),
-  d_assertions(uc),
-  d_cnfStream(NULL),
-  d_satSolver(NULL),
-  d_satContext(sc),
-  d_userContext(uc),
-  d_result(sc, SAT_VALUE_UNKNOWN),
-  d_engineState(0)
+DecisionEngine::DecisionEngine(context::Context* sc, context::UserContext* uc)
+    : d_enabledITEStrategies(),
+      d_needIteSkolemMap(),
+      d_relevancyStrategy(NULL),
+      d_assertions(uc),
+      d_cnfStream(NULL),
+      d_satSolver(NULL),
+      d_satContext(sc),
+      d_userContext(uc),
+      d_result(sc, SAT_VALUE_UNKNOWN),
+      d_engineState(0)
 {
   Trace("decision") << "Creating decision engine" << std::endl;
 }
@@ -54,10 +53,9 @@ void DecisionEngine::init()
 
   if (options::decisionMode() == options::DecisionMode::JUSTIFICATION)
   {
-    ITEDecisionStrategy* ds =
-      new decision::JustificationHeuristic(this, d_userContext, d_satContext);
-    d_enabledStrategies.push_back(ds);
-    d_needIteSkolemMap.push_back(ds);
+    d_enabledITEStrategies.emplace_back(new decision::JustificationHeuristic(
+        this, d_userContext, d_satContext));
+    d_needIteSkolemMap.push_back(d_enabledITEStrategies.back().get());
   }
 }
 
@@ -68,11 +66,7 @@ void DecisionEngine::shutdown()
   Assert(d_engineState == 1);
   d_engineState = 2;
 
-  for (DecisionStrategy* s : d_enabledStrategies)
-  {
-    delete s;
-  }
-  d_enabledStrategies.clear();
+  d_enabledITEStrategies.clear();
   d_needIteSkolemMap.clear();
 }
 
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index afa306325..28b15c9e0 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -38,8 +38,7 @@ using namespace CVC4::decision;
 namespace CVC4 {
 
 class DecisionEngine {
-
-  vector <DecisionStrategy* > d_enabledStrategies;
+  vector<std::unique_ptr<ITEDecisionStrategy>> d_enabledITEStrategies;
   vector <ITEDecisionStrategy* > d_needIteSkolemMap;
   RelevancyStrategy* d_relevancyStrategy;
 
@@ -72,13 +71,6 @@ public:
     Trace("decision") << "Destroying decision engine" << std::endl;
   }
 
-  // void setPropEngine(PropEngine* pe) {
-  //   // setPropEngine should not be called more than once
-  //   Assert(d_propEngine == NULL);
-  //   Assert(pe != NULL);
-  //   d_propEngine = pe;
-  // }
-
   void setSatSolver(DPLLSatSolverInterface* ss) {
     // setPropEngine should not be called more than once
     Assert(d_satSolver == NULL);
@@ -115,11 +107,11 @@ public:
         << "Forgot to set satSolver for decision engine?";
 
     SatLiteral ret = undefSatLiteral;
-    for(unsigned i = 0;
-        i < d_enabledStrategies.size()
-          and ret == undefSatLiteral
-          and stopSearch == false; ++i) {
-      ret = d_enabledStrategies[i]->getNext(stopSearch);
+    for (unsigned i = 0; i < d_enabledITEStrategies.size()
+                         and ret == undefSatLiteral and stopSearch == false;
+         ++i)
+    {
+      ret = d_enabledITEStrategies[i]->getNext(stopSearch);
     }
     return ret;
   }