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

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 0a6dec2164ebc9ca2b001c0f2ec6f02ddcce6688..a24a2e31a4caae7506171e85eec0e4ae7d5212f5 100644 (file)
--- 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 166514bc9ff78955b773a2411569d05850fb7f54..69041b2779e0fbfd7cbc5298770243edb886cc31 100644 (file)
--- 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 2c52e5b7237a1a6cb0d6efe30f0bec36e6b61956..4ca22459b9459e304906f40bc3ec1a644ff675a1 100644 (file)
--- 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 e1a933e7b39c9bc6c12e483fc625c265e84afcf6..d325d24b45381f3ce5b1d8af3f9ee0cf5a797e0d 100644 (file)
--- 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 93c37f6cc1e302ae8909b4697ce69eebc5606e21..0168363d438084c973e48650b35820a0eff1bbe2 100644 (file)
--- 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 5e5be7c4532cce097db81bb41ef763a12099e33d..a8a74b5a693c5ca98c25d3c02d8649f8bc174c97 100755 (executable)
--- 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 ffda05d1a715507581f241f5bb44192f50470a36..47ac2a11bf3cc5f9fba1652b11d33078d2c72e50 100644 (file)
--- 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 456a4b0ea410e14ad3aec9fd0a5053c24ebce9e7..8a900e1e7e0163266842e11b65ac952318e61f85 100755 (executable)
--- 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=
@@ -104,8 +102,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}) \\
 "
 }
 
@@ -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 b5cc16fc86f0f51fa6a52959d1d02e9a0eee0734..f6f1de69c6156aa6c9ded2358460935450185439 100644 (file)
--- 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 5d185ad9da17070664bc15fd246a7827df201483..ac3c63d55e7b7f091ce0cdfab205e5f775ce42ff 100644 (file)
--- 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 (file)
index 0000000..260bec4
--- /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 (file)
index 0000000..7ca5916
--- /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 (file)
index 0000000..afe01d7
--- /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 00ad7656d5040ea9fe3eb1e2c80aa3e0ce997be3..564864f19b747e6ec79a63125a31e80c7d9780b0 100644 (file)
--- 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) {