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, 114 insertions, 72 deletions

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 719239806..a159787f9 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -16,13 +16,14 @@
 
 #include "theory/theory.h"
 
-#include <vector>
-#include <sstream>
 #include <iostream>
+#include <sstream>
 #include <string>
+#include <vector>
 
 #include "base/check.h"
 #include "expr/node_algorithm.h"
+#include "options/theory_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/ext_theory.h"
 #include "theory/quantifiers_engine.h"
@@ -90,87 +91,128 @@ Theory::~Theory() {
   delete d_extTheory;
 }
 
-TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) {
+TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
+{
   TheoryId tid = THEORY_BUILTIN;
   switch(mode) {
-  case THEORY_OF_TYPE_BASED:
-    // Constants, variables, 0-ary constructors
-    if (node.isVar()) {
-      if( node.getKind() == kind::BOOLEAN_TERM_VARIABLE ){
-        tid = THEORY_UF;
-      }else{
-        tid = Theory::theoryOf(node.getType());
-      }
-    }else if (node.isConst()) {
-      tid = Theory::theoryOf(node.getType());
-    } else if (node.getKind() == kind::EQUAL) {
-      // Equality is owned by the theory that owns the domain
-      tid = Theory::theoryOf(node[0].getType());
-    } else {
-      // Regular nodes are owned by the kind
-      tid = kindToTheoryId(node.getKind());
-    }
-    break;
-  case THEORY_OF_TERM_BASED:
-    // Variables
-    if (node.isVar()) {
-      if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL) {
-        // We treat the variables as uninterpreted
-        tid = s_uninterpretedSortOwner;
-      } else {
-        if( node.getKind() == kind::BOOLEAN_TERM_VARIABLE ){
-          //Boolean vars go to UF
+    case options::TheoryOfMode::THEORY_OF_TYPE_BASED:
+      // Constants, variables, 0-ary constructors
+      if (node.isVar())
+      {
+        if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE)
+        {
           tid = THEORY_UF;
-        }else{
-          // Except for the Boolean ones
-          tid = THEORY_BOOL;
         }
+        else
+        {
+          tid = Theory::theoryOf(node.getType());
+        }
+      }
+      else if (node.isConst())
+      {
+        tid = Theory::theoryOf(node.getType());
       }
-    } else if (node.isConst()) {
-      // Constants go to the theory of the type
-      tid = Theory::theoryOf(node.getType());
-    } else if (node.getKind() == kind::EQUAL) { // Equality
-      // If one of them is an ITE, it's irelevant, since they will get replaced out anyhow
-      if (node[0].getKind() == kind::ITE) {
+      else if (node.getKind() == kind::EQUAL)
+      {
+        // Equality is owned by the theory that owns the domain
         tid = Theory::theoryOf(node[0].getType());
-      } else if (node[1].getKind() == kind::ITE) {
-        tid = Theory::theoryOf(node[1].getType());
-      } else {
-        TNode l = node[0];
-        TNode r = node[1];
-        TypeNode ltype = l.getType();
-        TypeNode rtype = r.getType();
-        if( ltype != rtype ){
-          tid = Theory::theoryOf(l.getType());
-        }else {
-          // If both sides belong to the same theory the choice is easy
-          TheoryId T1 = Theory::theoryOf(l);
-          TheoryId T2 = Theory::theoryOf(r);
-          if (T1 == T2) {
-            tid = T1;
-          } else {
-            TheoryId T3 = Theory::theoryOf(ltype);
-            // This is a case of
-            // * x*y = f(z) -> UF
-            // * x = c      -> UF
-            // * f(x) = read(a, y) -> either UF or ARRAY
-            // at least one of the theories has to be parametric, i.e. theory of the type is different
-            // from the theory of the term
-            if (T1 == T3) {
-              tid = T2;
-            } else if (T2 == T3) {
+      }
+      else
+      {
+        // Regular nodes are owned by the kind
+        tid = kindToTheoryId(node.getKind());
+      }
+      break;
+    case options::TheoryOfMode::THEORY_OF_TERM_BASED:
+      // Variables
+      if (node.isVar())
+      {
+        if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL)
+        {
+          // We treat the variables as uninterpreted
+          tid = s_uninterpretedSortOwner;
+        }
+        else
+        {
+          if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE)
+          {
+            // Boolean vars go to UF
+            tid = THEORY_UF;
+          }
+          else
+          {
+            // Except for the Boolean ones
+            tid = THEORY_BOOL;
+          }
+        }
+      }
+      else if (node.isConst())
+      {
+        // Constants go to the theory of the type
+        tid = Theory::theoryOf(node.getType());
+      }
+      else if (node.getKind() == kind::EQUAL)
+      {  // Equality
+        // If one of them is an ITE, it's irelevant, since they will get
+        // replaced out anyhow
+        if (node[0].getKind() == kind::ITE)
+        {
+          tid = Theory::theoryOf(node[0].getType());
+        }
+        else if (node[1].getKind() == kind::ITE)
+        {
+          tid = Theory::theoryOf(node[1].getType());
+        }
+        else
+        {
+          TNode l = node[0];
+          TNode r = node[1];
+          TypeNode ltype = l.getType();
+          TypeNode rtype = r.getType();
+          if (ltype != rtype)
+          {
+            tid = Theory::theoryOf(l.getType());
+          }
+          else
+          {
+            // If both sides belong to the same theory the choice is easy
+            TheoryId T1 = Theory::theoryOf(l);
+            TheoryId T2 = Theory::theoryOf(r);
+            if (T1 == T2)
+            {
               tid = T1;
-            } else {
-              // If both are parametric, we take the smaller one (arbitrary)
-              tid = T1 < T2 ? T1 : T2;
+            }
+            else
+            {
+              TheoryId T3 = Theory::theoryOf(ltype);
+              // This is a case of
+              // * x*y = f(z) -> UF
+              // * x = c      -> UF
+              // * f(x) = read(a, y) -> either UF or ARRAY
+              // at least one of the theories has to be parametric, i.e. theory
+              // of the type is different from the theory of the term
+              if (T1 == T3)
+              {
+                tid = T2;
+              }
+              else if (T2 == T3)
+              {
+                tid = T1;
+              }
+              else
+              {
+                // If both are parametric, we take the smaller one (arbitrary)
+                tid = T1 < T2 ? T1 : T2;
+              }
             }
           }
         }
       }
-    } else {
-      // Regular nodes are owned by the kind
-      tid = kindToTheoryId(node.getKind());
-    }
+      else
+      {
+        // Regular nodes are owned by the kind
+        tid = kindToTheoryId(node.getKind());
+      }
     break;
   default:
     Unreachable();