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

14 files changed, 164 insertions, 77 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 0a6dec216..a24a2e31a 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -682,6 +682,8 @@ libcvc4_add_sources(
   theory/theory.h
   theory/theory_engine.cpp
   theory/theory_engine.h
+  theory/theory_id.cpp
+  theory/theory_id.h
   theory/theory_model.cpp
   theory/theory_model.h
   theory/theory_model_builder.cpp
@@ -717,10 +719,6 @@ include_directories(include)
 include_directories(. ${CMAKE_CURRENT_BINARY_DIR})
 
 #-----------------------------------------------------------------------------#
-# IMPORTANT: The order of the theories is important. It affects the order in
-# which theory solvers are called/initialized internally. For example, strings
-# depends on arith, quantifiers needs to come as the very last.
-# See issue https://github.com/CVC4/CVC4/issues/2517 for more details.
 
 set(KINDS_FILES
   ${PROJECT_SOURCE_DIR}/src/theory/builtin/kinds
@@ -928,6 +926,7 @@ install(FILES
           ${INCLUDE_INSTALL_DIR}/cvc4/smt_util)
 install(FILES
           theory/logic_info.h
+          theory/theory_id.h
         DESTINATION
           ${INCLUDE_INSTALL_DIR}/cvc4/theory)
 install(FILES
diff --git a/src/cvc4.i b/src/cvc4.i
index 166514bc9..69041b277 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -357,6 +357,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %include "smt/command.i"
 %include "smt/logic_exception.i"
 %include "theory/logic_info.i"
+%include "theory/theory_id.i"
 
 // Tim: This should come after "theory/logic_info.i".
 %include "smt/smt_engine.i"
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}}"
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index ffda05d1a..47ac2a11b 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -837,7 +837,8 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
     addTheory(THEORY_SEP);
   }
 
-  Command* cmd = new SetBenchmarkLogicCommand(sygus() ? d_logic.getLogicString() : name);
+  Command* cmd =
+      new SetBenchmarkLogicCommand(sygus() ? d_logic.getLogicString() : name);
   cmd->setMuted(!fromCommand);
   return cmd;
 } /* Smt2::setLogic() */
diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index 456a4b0ea..8a900e1e7 100755
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -41,8 +41,6 @@ template=$1; shift
 theory_traits=
 theory_includes=
 theory_constructors=
-theory_for_each_macro="#define CVC4_FOR_EACH_THEORY \\
-"
 
 type_enumerator_includes=
 mk_type_enumerator_cases=
@@ -105,8 +103,6 @@ function theory {
   theory_header="$3"
   theory_includes="${theory_includes}#include \"$theory_header\"
 "
-  theory_for_each_macro="${theory_for_each_macro} CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::${theory_id}) \\
-"
 }
 
 function alternate {
@@ -412,7 +408,6 @@ nl -ba -s' ' "$template"  | grep '^ *[0-9][0-9]* # *line' |
 text=$(cat "$template")
 for var in \
     theory_traits \
-    theory_for_each_macro \
     theory_includes \
     theory_constructors \
     template \
diff --git a/src/theory/theory.h b/src/theory/theory.h
index b5cc16fc8..f6f1de69c 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -42,6 +42,7 @@
 #include "theory/decision_manager.h"
 #include "theory/logic_info.h"
 #include "theory/output_channel.h"
+#include "theory/theory_id.h"
 #include "theory/valuation.h"
 #include "util/statistics_registry.h"
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 5d185ad9d..ac3c63d55 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -59,6 +59,34 @@ using namespace CVC4::theory;
 
 namespace CVC4 {
 
+/* -------------------------------------------------------------------------- */
+
+namespace theory {
+
+/**
+ * IMPORTANT: The order of the theories is important. For example, strings
+ *            depends on arith, quantifiers needs to come as the very last.
+ *            Do not change this order.
+ */
+
+#define CVC4_FOR_EACH_THEORY                                     \
+  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BUILTIN)   \
+  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BOOL)      \
+  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_UF)        \
+  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_ARITH)     \
+  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BV)        \
+  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_FP)        \
+  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_ARRAYS)    \
+  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_DATATYPES) \
+  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_SEP)       \
+  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_SETS)      \
+  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_STRINGS)   \
+  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_QUANTIFIERS)
+
+}  // namespace theory
+
+/* -------------------------------------------------------------------------- */
+
 inline void flattenAnd(Node n, std::vector<TNode>& out){
   Assert(n.getKind() == kind::AND);
   for(Node::iterator i=n.begin(), i_end=n.end(); i != i_end; ++i){
diff --git a/src/theory/theory_id.cpp b/src/theory/theory_id.cpp
new file mode 100644
index 000000000..260bec418
--- /dev/null
+++ b/src/theory/theory_id.cpp
@@ -0,0 +1,56 @@
+#include "theory/theory_id.h"
+
+namespace CVC4 {
+namespace theory {
+
+TheoryId& operator++(TheoryId& id)
+{
+  return id = static_cast<TheoryId>(static_cast<int>(id) + 1);
+}
+
+std::ostream& operator<<(std::ostream& out, TheoryId theoryId)
+{
+  switch (theoryId)
+  {
+    case THEORY_BUILTIN: out << "THEORY_BUILTIN"; break;
+    case THEORY_BOOL: out << "THEORY_BOOL"; break;
+    case THEORY_UF: out << "THEORY_UF"; break;
+    case THEORY_ARITH: out << "THEORY_ARITH"; break;
+    case THEORY_BV: out << "THEORY_BV"; break;
+    case THEORY_FP: out << "THEORY_FP"; break;
+    case THEORY_ARRAYS: out << "THEORY_ARRAYS"; break;
+    case THEORY_DATATYPES: out << "THEORY_DATATYPES"; break;
+    case THEORY_SEP: out << "THEORY_SEP"; break;
+    case THEORY_SETS: out << "THEORY_SETS"; break;
+    case THEORY_STRINGS: out << "THEORY_STRINGS"; break;
+    case THEORY_QUANTIFIERS: out << "THEORY_QUANTIFIERS"; break;
+
+    default: out << "UNKNOWN_THEORY"; break;
+  }
+  return out;
+}
+
+std::string getStatsPrefix(TheoryId theoryId)
+{
+  switch (theoryId)
+  {
+    case THEORY_BUILTIN: return "theory::builtin"; break;
+    case THEORY_BOOL: return "theory::bool"; break;
+    case THEORY_UF: return "theory::uf"; break;
+    case THEORY_ARITH: return "theory::arith"; break;
+    case THEORY_BV: return "theory::bv"; break;
+    case THEORY_FP: return "theory::fp"; break;
+    case THEORY_ARRAYS: return "theory::arrays"; break;
+    case THEORY_DATATYPES: return "theory::datatypes"; break;
+    case THEORY_SEP: return "theory::sep"; break;
+    case THEORY_SETS: return "theory::sets"; break;
+    case THEORY_STRINGS: return "theory::strings"; break;
+    case THEORY_QUANTIFIERS: return "theory::quantifiers"; break;
+
+    default: break;
+  }
+  return "unknown";
+}
+
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/theory_id.h b/src/theory/theory_id.h
new file mode 100644
index 000000000..7ca5916fa
--- /dev/null
+++ b/src/theory/theory_id.h
@@ -0,0 +1,46 @@
+#include "cvc4_public.h"
+
+#ifndef CVC4__THEORY__THEORY_ID_H
+#define CVC4__THEORY__THEORY_ID_H
+
+#include <iostream>
+
+namespace CVC4 {
+
+namespace theory {
+
+/**
+ * IMPORTANT: The order of the theories is important. For example, strings
+ *            depends on arith, quantifiers needs to come as the very last.
+ *            Do not change this order.
+ */
+enum TheoryId
+{
+  THEORY_BUILTIN,
+  THEORY_BOOL,
+  THEORY_UF,
+  THEORY_ARITH,
+  THEORY_BV,
+  THEORY_FP,
+  THEORY_ARRAYS,
+  THEORY_DATATYPES,
+  THEORY_SEP,
+  THEORY_SETS,
+  THEORY_STRINGS,
+  THEORY_QUANTIFIERS,
+
+  THEORY_LAST
+};
+
+const TheoryId THEORY_FIRST = static_cast<TheoryId>(0);
+const TheoryId THEORY_SAT_SOLVER = THEORY_LAST;
+
+TheoryId& operator++(TheoryId& id) CVC4_PUBLIC;
+
+std::ostream& operator<<(std::ostream& out, TheoryId theoryId);
+
+std::string getStatsPrefix(TheoryId theoryId) CVC4_PUBLIC;
+
+}  // namespace theory
+}  // namespace CVC4
+#endif
diff --git a/src/theory/theory_id.i b/src/theory/theory_id.i
new file mode 100644
index 000000000..afe01d7b2
--- /dev/null
+++ b/src/theory/theory_id.i
@@ -0,0 +1,5 @@
+%{
+#include "theory/theory_id.h"
+%}
+
+%include "theory/theory_id.h"
diff --git a/src/theory/theory_traits_template.h b/src/theory/theory_traits_template.h
index 00ad7656d..564864f19 100644
--- a/src/theory/theory_traits_template.h
+++ b/src/theory/theory_traits_template.h
@@ -34,9 +34,7 @@ struct TheoryTraits;
 
 ${theory_traits}
 
-${theory_for_each_macro}
-
-#line 40 "${template}"
+#line 38 "${template}"
 
 struct TheoryConstructor {
   static void addTheory(TheoryEngine* engine, TheoryId id) {