Make order of theories explicit in the source code. (#3379)

Fixes #2517.

This makes the order of theories explicit in the source code rather than relying on the order defined via the build system. Previously, the build system ensured the order of the theories via the KINDS_FILES variable, which is a list of kinds files that is fed to code generation scripts (mkkind, mkmetakind, mkrewriter, mktheorytraits). The generated code critical to the order of theories w.r.t. soundess is the TheoryId enum, and the CVC4_FOR_EACH_THEORY macro. Ideally, we would want to get rid of the latter (ugly and error prone), which is not possible in the current configuration, and to be discussed in the future.

This PR moves the TheoryID enum and related functions to theory/theory_id.h, and the CVC4_FOR_EACH_THEORY macro to theory/theory_engine.cpp, the only place where it is used.

I ran it on whole SMT-LIB (non-incremental and incremental) and did not encounter any soundness issues. The only issue that did occur is not related to these changes, non-critical and known: #2993

4 files changed, 21 insertions, 64 deletions

diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 2c52e5b72..4ca22459b 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -621,7 +621,7 @@ private:
 
 ${getConst_instantiations}
 
-#line 616 "${template}"
+#line 609 "${template}"
 
 inline size_t ExprHashFunction::operator()(CVC4::Expr e) const {
   return (size_t) e.getId();
diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp
index e1a933e7b..d325d24b4 100644
--- a/src/expr/kind_template.cpp
+++ b/src/expr/kind_template.cpp
@@ -74,48 +74,29 @@ ${type_constant_descriptions}
 
 namespace theory {
 
-std::ostream& operator<<(std::ostream& out, TheoryId theoryId) {
-  switch(theoryId) {
-${theory_descriptions}
-#line 81 "${template}"
-  default:
-    out << "UNKNOWN_THEORY";
-    break;
-  }
-  return out;
-}
-
 TheoryId kindToTheoryId(::CVC4::Kind k) {
   switch(k) {
   case kind::UNDEFINED_KIND:
   case kind::NULL_EXPR:
     break;
 ${kind_to_theory_id}
-#line 95 "${template}"
+#line 84 "${template}"
   case kind::LAST_KIND:
     break;
   }
   throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind");
 }
 
-TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) {
-  switch(typeConstant) {
+TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant)
+{
+  switch (typeConstant)
+  {
 ${type_constant_to_theory_id}
-#line 105 "${template}"
-  case LAST_TYPE:
-    break;
-  }
-  throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad type constant");
-}
-
-std::string getStatsPrefix(TheoryId theoryId) {
-  switch(theoryId) {
-${theory_stats_prefixes}
-#line 115 "${template}"
-  default:
-    break;
+#line 94 "${template}"
+    case LAST_TYPE: break;
   }
-  return "unknown";
+  throw IllegalArgumentException(
+      "", "k", __PRETTY_FUNCTION__, "bad type constant");
 }
 
 }/* CVC4::theory namespace */
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 93c37f6cc..0168363d4 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -22,6 +22,7 @@
 #include <iosfwd>
 
 #include "base/exception.h"
+#include "theory/theory_id.h"
 
 namespace CVC4 {
 namespace kind {
@@ -44,7 +45,7 @@ namespace kind {
 
 std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC;
 
-#line 48 "${template}"
+#line 49 "${template}"
 
 /** Returns true if the given kind is associative. This is used by ExprManager to
  * decide whether it's safe to modify big expressions by changing the grouping of
@@ -64,11 +65,12 @@ struct KindHashFunction {
 /**
  * The enumeration for the built-in atomic types.
  */
-enum CVC4_PUBLIC TypeConstant {
-${type_constant_list}
-#line 70 "${template}"
+enum CVC4_PUBLIC TypeConstant
+{
+  ${type_constant_list}
+#line 71 "${template}"
   LAST_TYPE
-};/* enum TypeConstant */
+}; /* enum TypeConstant */
 
 /**
  * We hash the constants with their values.
@@ -83,23 +85,9 @@ std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant);
 
 namespace theory {
 
-enum TheoryId {
-${theory_enum}
-#line 89 "${template}"
-  THEORY_LAST
-};/* enum TheoryId */
-
-const TheoryId THEORY_FIRST = static_cast<TheoryId>(0);
-const TheoryId THEORY_SAT_SOLVER = THEORY_LAST;
-
-CVC4_PUBLIC inline TheoryId& operator++(TheoryId& id) {
-  return id = static_cast<TheoryId>(static_cast<int>(id) + 1);
-}
-
-std::ostream& operator<<(std::ostream& out, TheoryId theoryId);
-TheoryId kindToTheoryId(::CVC4::Kind k) CVC4_PUBLIC;
-TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) CVC4_PUBLIC;
-std::string getStatsPrefix(TheoryId theoryId) CVC4_PUBLIC;
+::CVC4::theory::TheoryId kindToTheoryId(::CVC4::Kind k) CVC4_PUBLIC;
+::CVC4::theory::TheoryId typeConstantToTheoryId(
+    ::CVC4::TypeConstant typeConstant) CVC4_PUBLIC;
 
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/expr/mkkind b/src/expr/mkkind
index 5e5be7c45..a8a74b5a6 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -73,9 +73,6 @@ type_properties_includes=
 seen_theory=false
 seen_theory_builtin=false
 
-theory_enum=
-theory_descriptions=
-theory_stats_prefixes=
 
 function theory {
   # theory ID T header
@@ -88,7 +85,7 @@ function theory {
   fi
 
   # this script doesn't care about the theory class information, but
-  # makes does make sure it's there
+  # makes sure it's there
   seen_theory=true
   if [ "$1" = THEORY_BUILTIN ]; then
     if $seen_theory_builtin; then
@@ -106,13 +103,7 @@ function theory {
   fi
 
   theory_id="$1"
-  theory_enum="${theory_enum}  $1,
-"
-  theory_descriptions="${theory_descriptions}  case ${theory_id}: out << \"${theory_id}\"; break;
-"
   prefix=$(echo "$theory_id" | tr '[:upper:]' '[:lower:]')
-  theory_stats_prefixes="${theory_stats_prefixes}  case ${theory_id}: return \"theory::${prefix#theory_}\"; break;
-"
 }
 
 function alternate {
@@ -408,7 +399,6 @@ for var in \
     kind_decls \
     kind_printers \
     kind_to_theory_id \
-    theory_enum \
     type_constant_list \
     type_constant_descriptions \
     type_constant_to_theory_id \
@@ -419,8 +409,6 @@ for var in \
     type_groundterms \
     type_constant_groundterms \
     type_properties_includes \
-    theory_descriptions \
-    theory_stats_prefixes \
     template \
     ; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"