From 91acac585b0b2bc5a3fab4466d887cfbafa35f77 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 10 Oct 2019 18:52:46 -0700
Subject: 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
---
 src/expr/kind_template.h | 32 ++++++++++----------------------
 1 file changed, 10 insertions(+), 22 deletions(-)

(limited to 'src/expr/kind_template.h')

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 */
-- 
cgit v1.2.3