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.

1 files changed, 11 insertions, 5 deletions

diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index f7fd13d4d..f72a0d1b4 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -111,9 +111,12 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a,
       }
     }
   }
-  if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_EE ){
+  if (options::quantRepMode() == options::QuantRepMode::EE)
+  {
     return r;
-  }else{
+  }
+  else
+  {
     TypeNode v_tn = q.isNull() ? a.getType() : q[0][index].getType();
     std::map<Node, Node>& v_int_rep = d_int_rep[v_tn];
     std::map<Node, Node>::const_iterator itir = v_int_rep.find(r);
@@ -239,11 +242,14 @@ int EqualityQueryQuantifiersEngine::getRepScore(Node n,
       return options::instLevelInputOnly() ? -1 : 0;
     }
   }else{
-    if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_FIRST ){
+    if (options::quantRepMode() == options::QuantRepMode::FIRST)
+    {
       //score prefers earliest use of this term as a representative
       return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
-    }else{
-      Assert(options::quantRepMode() == quantifiers::QUANT_REP_MODE_DEPTH);
+    }
+    else
+    {
+      Assert(options::quantRepMode() == options::QuantRepMode::DEPTH);
       return quantifiers::TermUtil::getTermDepth( n );
     }
   }