Remove static access to options in decision folder (#7527)

This PR replaces static accesses to options (options::foo()) by using the options object provided via the environment.

diff --git a/src/decision/decision_engine_old.cpp b/src/decision/decision_engine_old.cpp
index 120fc730be8bbee152770a785be22a389cbabcd2..261d78fdf2f930586035d2742b99642cc12b3238 100644 (file)
--- a/src/decision/decision_engine_old.cpp
+++ b/src/decision/decision_engine_old.cpp
@@ -30,7 +30,7 @@ DecisionEngineOld::DecisionEngineOld(Env& env)
       d_result(context(), SAT_VALUE_UNKNOWN),
       d_engineState(0),
       d_enabledITEStrategy(nullptr),
-      d_decisionStopOnly(options::decisionMode()
+      d_decisionStopOnly(options().decision.decisionMode
                          == options::DecisionMode::STOPONLY_OLD)
 {
   Trace("decision") << "Creating decision engine" << std::endl;
@@ -39,11 +39,11 @@ DecisionEngineOld::DecisionEngineOld(Env& env)
 
   Trace("decision-init") << "DecisionEngineOld::init()" << std::endl;
   Trace("decision-init") << " * options->decisionMode: "
-                         << options::decisionMode() << std::endl;
+                         << options().decision.decisionMode << std::endl;
   Trace("decision-init") << " * decisionStopOnly: " << d_decisionStopOnly
                          << std::endl;
 
-  if (options::decisionMode() == options::DecisionMode::JUSTIFICATION)
+  if (options().decision.decisionMode == options::DecisionMode::JUSTIFICATION)
   {
     d_enabledITEStrategy.reset(new decision::JustificationHeuristic(env, this));
   }

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index e04de9ce1c9b33d96b33112b258d5426f02d4ae3..cadb107c3e7e671c6c3a4fe49458f9d00726427e 100644 (file)
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -62,10 +62,11 @@ JustificationHeuristic::~JustificationHeuristic() {}
 
 cvc5::prop::SatLiteral JustificationHeuristic::getNext(bool& stopSearch)
 {
-  if(options::decisionThreshold() > 0) {
+  if (options().decision.decisionThreshold > 0)
+  {
     bool stopSearchTmp = false;
     prop::SatLiteral lit =
-        getNextThresh(stopSearchTmp, options::decisionThreshold());
+        getNextThresh(stopSearchTmp, options().decision.decisionThreshold);
     if (lit != prop::undefSatLiteral)
     {
       Assert(stopSearchTmp == false);
@@ -252,7 +253,7 @@ DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, SatValue satV
 
 DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, bool polarity)
 {
-  if (options::decisionWeightInternal()
+  if (options().decision.decisionWeightInternal
       != options::DecisionWeightInternal::USR1)
   {
     return getWeight(n);
@@ -304,15 +305,16 @@ DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, bool polarity
 DecisionWeight JustificationHeuristic::getWeight(TNode n) {
   if(!n.hasAttribute(DecisionWeightAttr()) ) {
     options::DecisionWeightInternal combiningFn =
-        options::decisionWeightInternal();
+        options().decision.decisionWeightInternal;
 
     if (combiningFn == options::DecisionWeightInternal::OFF
         || n.getNumChildren() == 0)
     {
-      if (options::decisionRandomWeight() != 0)
+      if (options().decision.decisionRandomWeight != 0)
       {
         n.setAttribute(DecisionWeightAttr(),
-            Random::getRandom().pick(0, options::decisionRandomWeight()-1));
+                       Random::getRandom().pick(
+                           0, options().decision.decisionRandomWeight - 1));
       }
     }
     else if (combiningFn == options::DecisionWeightInternal::MAX)
@@ -340,7 +342,8 @@ DecisionWeight JustificationHeuristic::getWeight(TNode n) {
 
 typedef std::vector<TNode> ChildList;
 TNode JustificationHeuristic::getChildByWeight(TNode n, int i, bool polarity) {
-  if(options::decisionUseWeight()) {
+  if (options().decision.decisionUseWeight)
+  {
     // TODO: Optimize storing & access
     if(d_childCache.find(n) == d_childCache.end()) {
       ChildList list0(n.begin(), n.end()), list1(n.begin(), n.end());
@@ -349,7 +352,9 @@ TNode JustificationHeuristic::getChildByWeight(TNode n, int i, bool polarity) {
       d_childCache[n] = make_pair(list0, list1);
     }
     return polarity ? d_childCache[n].get().second[i] : d_childCache[n].get().first[i];
-  } else {
+  }
+  else
+  {
     return n[i];
   }
 }
@@ -612,8 +617,10 @@ JustificationHeuristic::SearchResult JustificationHeuristic::handleBinaryEasy(TN
                                               TNode node2,
                                               SatValue desiredVal2)
 {
-  if(options::decisionUseWeight() &&
-     getWeightPolarized(node1, desiredVal1) > getWeightPolarized(node2, desiredVal2)) {
+  if (options().decision.decisionUseWeight
+      && getWeightPolarized(node1, desiredVal1)
+             > getWeightPolarized(node2, desiredVal2))
+  {
     std::swap(node1, node2);
     std::swap(desiredVal1, desiredVal2);
   }
@@ -637,8 +644,10 @@ JustificationHeuristic::SearchResult JustificationHeuristic::handleBinaryHard(TN
                                               TNode node2,
                                               SatValue desiredVal2)
 {
-  if(options::decisionUseWeight() &&
-     getWeightPolarized(node1, desiredVal1) > getWeightPolarized(node2, desiredVal2)) {
+  if (options().decision.decisionUseWeight
+      && getWeightPolarized(node1, desiredVal1)
+             > getWeightPolarized(node2, desiredVal2))
+  {
     std::swap(node1, node2);
     std::swap(desiredVal1, desiredVal2);
   }
@@ -673,13 +682,17 @@ JustificationHeuristic::SearchResult JustificationHeuristic::handleITE(TNode nod
 
     if(trueChildVal == desiredVal || falseChildVal == invertValue(desiredVal)) {
       ifDesiredVal = SAT_VALUE_TRUE;
-    } else if(trueChildVal == invertValue(desiredVal) ||
-              falseChildVal == desiredVal ||
-              (options::decisionUseWeight() &&
-               getWeightPolarized(node[1], true) > getWeightPolarized(node[2], false))
-              ) {
+    }
+    else if (trueChildVal == invertValue(desiredVal)
+             || falseChildVal == desiredVal
+             || (options().decision.decisionUseWeight
+                 && getWeightPolarized(node[1], true)
+                        > getWeightPolarized(node[2], false)))
+    {
       ifDesiredVal = SAT_VALUE_FALSE;
-    } else {
+    }
+    else
+    {
       ifDesiredVal = SAT_VALUE_TRUE;
     }
 

diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index 303f1a63bca9180b7fb841b8a9b1a2fdbd3a3256..fbba2e33a677904fea6d4a4c8044170e33641d01 100644 (file)
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -150,7 +150,7 @@ private:
  int getPrvsIndex();
  DecisionWeight getWeightPolarized(TNode n, bool polarity);
  DecisionWeight getWeightPolarized(TNode n, prop::SatValue);
- static DecisionWeight getWeight(TNode);
+ DecisionWeight getWeight(TNode);
  bool compareByWeightFalse(TNode, TNode);
  bool compareByWeightTrue(TNode, TNode);
  TNode getChildByWeight(TNode n, int i, bool polarity);

diff --git a/src/decision/justification_strategy.cpp b/src/decision/justification_strategy.cpp
index d659369642a97dc19c83d203ddf6e2ade3a77c71..bced3d662c2bf8186f3a594621f1027e627ee6f4 100644 (file)
--- a/src/decision/justification_strategy.cpp
+++ b/src/decision/justification_strategy.cpp
@@ -28,18 +28,19 @@ JustificationStrategy::JustificationStrategy(Env& env)
       d_assertions(
           userContext(),
           context(),
-          options::jhRlvOrder()),  // assertions are user-context dependent
+          options()
+              .decision.jhRlvOrder),  // assertions are user-context dependent
       d_skolemAssertions(
           context(), context()),  // skolem assertions are SAT-context dependent
       d_justified(context()),
       d_stack(context()),
       d_lastDecisionLit(context()),
       d_currStatusDec(false),
-      d_useRlvOrder(options::jhRlvOrder()),
-      d_decisionStopOnly(options::decisionMode()
+      d_useRlvOrder(options().decision.jhRlvOrder),
+      d_decisionStopOnly(options().decision.decisionMode
                          == options::DecisionMode::STOPONLY),
-      d_jhSkMode(options::jhSkolemMode()),
-      d_jhSkRlvMode(options::jhSkolemRlvMode())
+      d_jhSkMode(options().decision.jhSkolemMode),
+      d_jhSkRlvMode(options().decision.jhSkolemRlvMode)
 {
 }