DecisionEngine: Use single unique pointer for ITE strategy . (#4078)

Previously, DecisionEngine maintained a vector of ITE strategies.
However, only one was ever created. This uses a single unique_ptr member
for the ITE strategy instead of a vector.

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 63a09ba2c83254a1557b11173d21e14651f37261..e12ae6127ec5f55ec8c2faa557aa75cd160aa91a 100644 (file)
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -26,12 +26,12 @@ using namespace std;
 namespace CVC4 {
 
 DecisionEngine::DecisionEngine(context::Context* sc, context::UserContext* uc)
-    : d_enabledITEStrategies(),
+    : d_enabledITEStrategy(nullptr),
       d_needIteSkolemMap(),
-      d_relevancyStrategy(NULL),
+      d_relevancyStrategy(nullptr),
       d_assertions(uc),
-      d_cnfStream(NULL),
-      d_satSolver(NULL),
+      d_cnfStream(nullptr),
+      d_satSolver(nullptr),
       d_satContext(sc),
       d_userContext(uc),
       d_result(sc, SAT_VALUE_UNKNOWN),
@@ -53,9 +53,9 @@ void DecisionEngine::init()
 
   if (options::decisionMode() == options::DecisionMode::JUSTIFICATION)
   {
-    d_enabledITEStrategies.emplace_back(new decision::JustificationHeuristic(
+    d_enabledITEStrategy.reset(new decision::JustificationHeuristic(
         this, d_userContext, d_satContext));
-    d_needIteSkolemMap.push_back(d_enabledITEStrategies.back().get());
+    d_needIteSkolemMap.push_back(d_enabledITEStrategy.get());
   }
 }
 
@@ -65,18 +65,34 @@ void DecisionEngine::shutdown()
 
   Assert(d_engineState == 1);
   d_engineState = 2;
-
-  d_enabledITEStrategies.clear();
+  d_enabledITEStrategy.reset(nullptr);
   d_needIteSkolemMap.clear();
 }
 
+SatLiteral DecisionEngine::getNext(bool& stopSearch)
+{
+  NodeManager::currentResourceManager()->spendResource(
+      ResourceManager::Resource::DecisionStep);
+  Assert(d_cnfStream != nullptr)
+      << "Forgot to set cnfStream for decision engine?";
+  Assert(d_satSolver != nullptr)
+      << "Forgot to set satSolver for decision engine?";
+
+  return d_enabledITEStrategy == nullptr
+             ? undefSatLiteral
+             : d_enabledITEStrategy->getNext(stopSearch);
+}
+
 bool DecisionEngine::isRelevant(SatVariable var)
 {
   Debug("decision") << "isRelevant(" << var <<")" << std::endl;
-  if(d_relevancyStrategy != NULL) {
+  if (d_relevancyStrategy != nullptr)
+  {
     //Assert(d_cnfStream->hasNode(var));
     return d_relevancyStrategy->isRelevant( d_cnfStream->getNode(SatLiteral(var)) );
-  } else {
+  }
+  else
+  {
     return true;
   }
 }
@@ -84,10 +100,13 @@ bool DecisionEngine::isRelevant(SatVariable var)
 SatValue DecisionEngine::getPolarity(SatVariable var)
 {
   Debug("decision") << "getPolarity(" << var <<")" << std::endl;
-  if(d_relevancyStrategy != NULL) {
+  if (d_relevancyStrategy != nullptr)
+  {
     Assert(isRelevant(var));
     return d_relevancyStrategy->getPolarity( d_cnfStream->getNode(SatLiteral(var)) );
-  } else {
+  }
+  else
+  {
     return SAT_VALUE_UNKNOWN;
   }
 }

diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 28b15c9e0729f423d6cc60142ba3cadaf5269e5e..c4eb29284649db7c47f3850431a7312eae587cf5 100644 (file)
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -38,7 +38,7 @@ using namespace CVC4::decision;
 namespace CVC4 {
 
 class DecisionEngine {
-  vector<std::unique_ptr<ITEDecisionStrategy>> d_enabledITEStrategies;
+  std::unique_ptr<ITEDecisionStrategy> d_enabledITEStrategy;
   vector <ITEDecisionStrategy* > d_needIteSkolemMap;
   RelevancyStrategy* d_relevancyStrategy;
 
@@ -85,7 +85,7 @@ public:
     d_cnfStream = cs;
   }
 
-  /* enables decision stragies based on options */
+  /* Enables decision strategy based on options. */
   void init();
 
   /**
@@ -98,23 +98,7 @@ public:
   // Interface for External World to use our services
 
   /** Gets the next decision based on strategies that are enabled */
-  SatLiteral getNext(bool &stopSearch) {
-    NodeManager::currentResourceManager()->spendResource(
-        ResourceManager::Resource::DecisionStep);
-    Assert(d_cnfStream != NULL)
-        << "Forgot to set cnfStream for decision engine?";
-    Assert(d_satSolver != NULL)
-        << "Forgot to set satSolver for decision engine?";
-
-    SatLiteral ret = undefSatLiteral;
-    for (unsigned i = 0; i < d_enabledITEStrategies.size()
-                         and ret == undefSatLiteral and stopSearch == false;
-         ++i)
-    {
-      ret = d_enabledITEStrategies[i]->getNext(stopSearch);
-    }
-    return ret;
-  }
+  SatLiteral getNext(bool& stopSearch);
 
   /** Is a sat variable relevant */
   bool isRelevant(SatVariable var);