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, 19 insertions, 10 deletions

diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 98e330df4..34952084b 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -480,7 +480,7 @@ SortModel::SortModel(Node n,
 {
   d_cardinality_term = n;
 
-  if (options::ufssMode() == UF_SS_FULL)
+  if (options::ufssMode() == options::UfssMode::FULL)
   {
     // Register the strategy with the decision manager of the theory.
     // We are guaranteed that the decision manager is ready since we
@@ -671,7 +671,7 @@ bool SortModel::areDisequal( Node a, Node b ) {
 
 /** check */
 void SortModel::check( Theory::Effort level, OutputChannel* out ){
-  Assert(options::ufssMode() == UF_SS_FULL);
+  Assert(options::ufssMode() == options::UfssMode::FULL);
   if( level>=Theory::EFFORT_STANDARD && d_hasCard && !d_conflict ){
     Debug("uf-ss") << "CardinalityExtension: Check " << level << " " << d_type
                    << std::endl;
@@ -1314,7 +1314,7 @@ CardinalityExtension::CardinalityExtension(context::Context* c,
       d_min_pos_tn_master_card(c, -1),
       d_rel_eqc(c)
 {
-  if (options::ufssMode() == UF_SS_FULL && options::ufssFairness())
+  if (options::ufssMode() == options::UfssMode::FULL && options::ufssFairness())
   {
     // Register the strategy with the decision manager of the theory.
     // We are guaranteed that the decision manager is ready since we
@@ -1451,7 +1451,8 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
 #endif
   bool polarity = n.getKind() != kind::NOT;
   TNode lit = polarity ? n : n[0];
-  if( options::ufssMode()==UF_SS_FULL ){
+  if (options::ufssMode() == options::UfssMode::FULL)
+  {
     if( lit.getKind()==CARDINALITY_CONSTRAINT ){
       TypeNode tn = lit[0].getType();
       Assert(tn.isSort());
@@ -1532,7 +1533,9 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
         }
       }
     }
-  }else{
+  }
+  else
+  {
     if( lit.getKind()==CARDINALITY_CONSTRAINT || lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){
       // cardinality constraint from user input, set incomplete   
       Trace("uf-ss") << "Literal " << lit << " not handled when uf ss mode is not FULL, set incomplete." << std::endl;
@@ -1566,7 +1569,8 @@ bool CardinalityExtension::areDisequal(Node a, Node b)
 void CardinalityExtension::check(Theory::Effort level)
 {
   if( !d_conflict ){
-    if( options::ufssMode()==UF_SS_FULL ){
+    if (options::ufssMode() == options::UfssMode::FULL)
+    {
       Trace("uf-ss-solver")
           << "CardinalityExtension: check " << level << std::endl;
       if (level == Theory::EFFORT_FULL)
@@ -1593,7 +1597,9 @@ void CardinalityExtension::check(Theory::Effort level)
           break;
         }
       }
-    }else if( options::ufssMode()==UF_SS_NO_MINIMAL ){
+    }
+    else if (options::ufssMode() == options::UfssMode::NO_MINIMAL)
+    {
       if( level==Theory::EFFORT_FULL ){
         // split on an equality between two equivalence classes (at most one per type)
         std::map< TypeNode, std::vector< Node > > eqc_list;
@@ -1625,7 +1631,9 @@ void CardinalityExtension::check(Theory::Effort level)
           ++eqcs_i;
         }
       }
-    }else{
+    }
+    else
+    {
       // unhandled uf ss mode
       Assert(false);
     }
@@ -1664,7 +1672,8 @@ CardinalityExtension::CombinedCardinalityDecisionStrategy::identify() const
 
 void CardinalityExtension::preRegisterTerm(TNode n)
 {
-  if( options::ufssMode()==UF_SS_FULL ){
+  if (options::ufssMode() == options::UfssMode::FULL)
+  {
     //initialize combined cardinality
     initializeCombinedCardinality();
 
@@ -1776,7 +1785,7 @@ void CardinalityExtension::initializeCombinedCardinality()
 /** check */
 void CardinalityExtension::checkCombinedCardinality()
 {
-  Assert(options::ufssMode() == UF_SS_FULL);
+  Assert(options::ufssMode() == options::UfssMode::FULL);
   if( options::ufssFairness() ){
     Trace("uf-ss-com-card-debug") << "Check combined cardinality, get maximum negative cardinalities..." << std::endl;
     int totalCombinedCard = 0;