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, 15 insertions, 6 deletions

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 79279eb41..524c440ba 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -16,10 +16,11 @@
 
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
+#include "options/theory_options.h"
 #include "options/uf_options.h"
+#include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
 
@@ -672,7 +673,8 @@ Node TermDb::evaluateTerm2(TNode n,
             for (unsigned j = 0; j < 2; j++)
             {
               std::pair<bool, Node> et = te->entailmentCheck(
-                  THEORY_OF_TYPE_BASED, j == 0 ? ret : ret.negate());
+                  options::TheoryOfMode::THEORY_OF_TYPE_BASED,
+                  j == 0 ? ret : ret.negate());
               if (et.first)
               {
                 ret = j == 0 ? d_true : d_false;
@@ -905,11 +907,16 @@ bool TermDb::hasTermCurrent( Node n, bool useMode ) {
     return d_has_map.find( n )!=d_has_map.end();
   }else{
     //return d_quantEngine->getActiveEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE
-    if( options::termDbMode()==TERM_DB_ALL ){
+    if (options::termDbMode() == options::TermDbMode::ALL)
+    {
       return true;
-    }else if( options::termDbMode()==TERM_DB_RELEVANT ){
+    }
+    else if (options::termDbMode() == options::TermDbMode::RELEVANT)
+    {
       return d_has_map.find( n )!=d_has_map.end();
-    }else{
+    }
+    else
+    {
       Assert(false);
       return false;
     }
@@ -1061,7 +1068,9 @@ bool TermDb::reset( Theory::Effort effort ){
   }
 
   //compute has map
-  if( options::termDbMode()==TERM_DB_RELEVANT || options::lteRestrictInstClosure() ){
+  if (options::termDbMode() == options::TermDbMode::RELEVANT
+      || options::lteRestrictInstClosure())
+  {
     d_has_map.clear();
     d_term_elig_eqc.clear();
     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );