Generate code for options with modes. (#3561)

This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.

2 files changed, 12 insertions, 10 deletions

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 679dd6cc6..dc798626e 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -18,7 +18,6 @@
 #include "decision/decision_attributes.h"
 #include "decision/justification_heuristic.h"
 #include "expr/node.h"
-#include "options/decision_mode.h"
 #include "options/decision_options.h"
 #include "options/smt_options.h"
 
@@ -53,8 +52,8 @@ void DecisionEngine::init()
   Trace("decision-init") << " * options->decisionStopOnly: "
                          << options::decisionStopOnly() << std::endl;
 
-  if(options::decisionMode() == decision::DECISION_STRATEGY_INTERNAL) { }
-  if(options::decisionMode() == decision::DECISION_STRATEGY_JUSTIFICATION) {
+  if (options::decisionMode() == options::DecisionMode::JUSTIFICATION)
+  {
     ITEDecisionStrategy* ds =
       new decision::JustificationHeuristic(this, d_userContext, d_satContext);
     enableStrategy(ds);
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index f7e5b84fc..a6b6cbd8f 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -248,7 +248,9 @@ DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, SatValue satV
 
 DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, bool polarity)
 {
-  if(options::decisionWeightInternal() != DECISION_WEIGHT_INTERNAL_USR1) {
+  if (options::decisionWeightInternal()
+      != options::DecisionWeightInternal::USR1)
+  {
     return getWeight(n);
   }
 
@@ -297,10 +299,11 @@ DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, bool polarity
 
 DecisionWeight JustificationHeuristic::getWeight(TNode n) {
   if(!n.hasAttribute(DecisionWeightAttr()) ) {
+    options::DecisionWeightInternal combiningFn =
+        options::decisionWeightInternal();
 
-    DecisionWeightInternal combiningFn = options::decisionWeightInternal();
-
-    if (combiningFn == DECISION_WEIGHT_INTERNAL_OFF || n.getNumChildren() == 0)
+    if (combiningFn == options::DecisionWeightInternal::OFF
+        || n.getNumChildren() == 0)
     {
       if (options::decisionRandomWeight() != 0)
       {
@@ -308,15 +311,15 @@ DecisionWeight JustificationHeuristic::getWeight(TNode n) {
             Random::getRandom().pick(0, options::decisionRandomWeight()-1));
       }
     }
-    else if (combiningFn == DECISION_WEIGHT_INTERNAL_MAX)
+    else if (combiningFn == options::DecisionWeightInternal::MAX)
     {
       DecisionWeight dW = 0;
       for (TNode::iterator i = n.begin(); i != n.end(); ++i)
         dW = max(dW, getWeight(*i));
       n.setAttribute(DecisionWeightAttr(), dW);
     }
-    else if (combiningFn == DECISION_WEIGHT_INTERNAL_SUM
-             || combiningFn == DECISION_WEIGHT_INTERNAL_USR1)
+    else if (combiningFn == options::DecisionWeightInternal::SUM
+             || combiningFn == options::DecisionWeightInternal::USR1)
     {
       DecisionWeight dW = 0;
       for (TNode::iterator i = n.begin(); i != n.end(); ++i)