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}}"