cmake: Fix theory order #2. (#2522)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 96d462d96f342d8885c061dbd3d708e424b206d6..9948b0ec96407ac607d3f9f330a0cca8104f6b5f 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -655,6 +655,27 @@ libcvc4_add_sources(
 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
+  ${PROJECT_SOURCE_DIR}/src/theory/booleans/kinds
+  ${PROJECT_SOURCE_DIR}/src/theory/uf/kinds
+  ${PROJECT_SOURCE_DIR}/src/theory/arith/kinds
+  ${PROJECT_SOURCE_DIR}/src/theory/bv/kinds
+  ${PROJECT_SOURCE_DIR}/src/theory/fp/kinds
+  ${PROJECT_SOURCE_DIR}/src/theory/arrays/kinds
+  ${PROJECT_SOURCE_DIR}/src/theory/datatypes/kinds
+  ${PROJECT_SOURCE_DIR}/src/theory/sep/kinds
+  ${PROJECT_SOURCE_DIR}/src/theory/sets/kinds
+  ${PROJECT_SOURCE_DIR}/src/theory/strings/kinds
+  ${PROJECT_SOURCE_DIR}/src/theory/quantifiers/kinds
+  ${PROJECT_SOURCE_DIR}/src/theory/idl/kinds)
+
 #-----------------------------------------------------------------------------#
 # Add subdirectories
 

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 83bd2d585a882e8d6ff05d2b38de8b3f1b7b8182..6a06bc8ed24a7768d571ce8bd6ca143bb8068894 100644 (file)
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -65,7 +65,6 @@ libcvc4_add_sources(GENERATED
 #
 # Generate code for kinds.
 #
-file(GLOB kinds_files ${PROJECT_SOURCE_DIR}/src/theory/*/kinds)
 
 set(mkkind_script ${CMAKE_CURRENT_LIST_DIR}/mkkind)
 set(mkmetakind_script ${CMAKE_CURRENT_LIST_DIR}/mkmetakind)
@@ -76,7 +75,7 @@ add_custom_command(
   COMMAND
     ${mkkind_script}
     ${CMAKE_CURRENT_LIST_DIR}/kind_template.h
-    ${kinds_files}
+    ${KINDS_FILES}
     > ${CMAKE_CURRENT_BINARY_DIR}/kind.h
   DEPENDS mkkind kind_template.h
 )
@@ -86,7 +85,7 @@ add_custom_command(
   COMMAND
     ${mkkind_script}
     ${CMAKE_CURRENT_LIST_DIR}/kind_template.cpp
-    ${kinds_files}
+    ${KINDS_FILES}
     > ${CMAKE_CURRENT_BINARY_DIR}/kind.cpp
   DEPENDS mkkind kind_template.cpp kind.h
 )
@@ -96,7 +95,7 @@ add_custom_command(
   COMMAND
     ${mkkind_script}
     ${CMAKE_CURRENT_LIST_DIR}/type_properties_template.h
-    ${kinds_files}
+    ${KINDS_FILES}
     > ${CMAKE_CURRENT_BINARY_DIR}/type_properties.h
   DEPENDS mkkind type_properties_template.h
 )
@@ -106,7 +105,7 @@ add_custom_command(
   COMMAND
     ${mkmetakind_script}
     ${CMAKE_CURRENT_LIST_DIR}/metakind_template.h
-    ${kinds_files}
+    ${KINDS_FILES}
     > ${CMAKE_CURRENT_BINARY_DIR}/metakind.h
   DEPENDS mkmetakind metakind_template.h
 )
@@ -116,7 +115,7 @@ add_custom_command(
   COMMAND
     ${mkmetakind_script}
     ${CMAKE_CURRENT_LIST_DIR}/metakind_template.cpp
-    ${kinds_files}
+    ${KINDS_FILES}
     > ${CMAKE_CURRENT_BINARY_DIR}/metakind.cpp
   DEPENDS mkmetakind metakind_template.cpp metakind.h
 )
@@ -126,7 +125,7 @@ add_custom_command(
   COMMAND
     ${mkexpr_script}
     ${CMAKE_CURRENT_LIST_DIR}/expr_template.h
-    ${kinds_files}
+    ${KINDS_FILES}
     > ${CMAKE_CURRENT_BINARY_DIR}/expr.h
   DEPENDS mkexpr expr_template.h kind.h
 )
@@ -136,7 +135,7 @@ add_custom_command(
   COMMAND
     ${mkexpr_script}
     ${CMAKE_CURRENT_LIST_DIR}/expr_template.cpp
-    ${kinds_files}
+    ${KINDS_FILES}
     > ${CMAKE_CURRENT_BINARY_DIR}/expr.cpp
   DEPENDS mkexpr expr_template.cpp expr.h
 )
@@ -146,7 +145,7 @@ add_custom_command(
   COMMAND
     ${mkexpr_script}
     ${CMAKE_CURRENT_LIST_DIR}/expr_manager_template.h
-    ${kinds_files}
+    ${KINDS_FILES}
     > ${CMAKE_CURRENT_BINARY_DIR}/expr_manager.h
   DEPENDS mkexpr expr_manager_template.h expr.h
 )
@@ -156,7 +155,7 @@ add_custom_command(
   COMMAND
     ${mkexpr_script}
     ${CMAKE_CURRENT_LIST_DIR}/expr_manager_template.cpp
-    ${kinds_files}
+    ${KINDS_FILES}
     > ${CMAKE_CURRENT_BINARY_DIR}/expr_manager.cpp
   DEPENDS mkexpr expr_manager_template.cpp expr_manager.h
 )
@@ -166,7 +165,7 @@ add_custom_command(
   COMMAND
     ${mkexpr_script}
     ${CMAKE_CURRENT_LIST_DIR}/type_checker_template.cpp
-    ${kinds_files}
+    ${KINDS_FILES}
     > ${CMAKE_CURRENT_BINARY_DIR}/type_checker.cpp
   DEPENDS mkexpr type_checker_template.cpp
 )

diff --git a/src/theory/CMakeLists.txt b/src/theory/CMakeLists.txt
index 535c1d5dfa99e93da3b5d96bce51d1e0c982b3fc..028cb35040ba135fac356172064a9cf46b94e077 100644 (file)
--- a/src/theory/CMakeLists.txt
+++ b/src/theory/CMakeLists.txt
@@ -4,25 +4,6 @@ libcvc4_add_sources(GENERATED
   type_enumerator.cpp
 )
 
-# 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
-  ${PROJECT_SOURCE_DIR}/src/theory/booleans/kinds
-  ${PROJECT_SOURCE_DIR}/src/theory/uf/kinds
-  ${PROJECT_SOURCE_DIR}/src/theory/arith/kinds
-  ${PROJECT_SOURCE_DIR}/src/theory/bv/kinds
-  ${PROJECT_SOURCE_DIR}/src/theory/fp/kinds
-  ${PROJECT_SOURCE_DIR}/src/theory/arrays/kinds
-  ${PROJECT_SOURCE_DIR}/src/theory/datatypes/kinds
-  ${PROJECT_SOURCE_DIR}/src/theory/sep/kinds
-  ${PROJECT_SOURCE_DIR}/src/theory/sets/kinds
-  ${PROJECT_SOURCE_DIR}/src/theory/strings/kinds
-  ${PROJECT_SOURCE_DIR}/src/theory/quantifiers/kinds
-  ${PROJECT_SOURCE_DIR}/src/theory/idl/kinds)
-
 set(mktheorytraits_script ${CMAKE_CURRENT_LIST_DIR}/mktheorytraits)
 set(mkrewriter_script ${CMAKE_CURRENT_LIST_DIR}/mkrewriter)
 
@@ -31,7 +12,7 @@ add_custom_command(
   COMMAND
     ${mkrewriter_script}
     ${CMAKE_CURRENT_LIST_DIR}/rewriter_tables_template.h
-    ${kinds_files}
+    ${KINDS_FILES}
     > ${CMAKE_CURRENT_BINARY_DIR}/rewriter_tables.h
   DEPENDS mkrewriter rewriter_tables_template.h
 )
@@ -41,7 +22,7 @@ add_custom_command(
   COMMAND
     ${mktheorytraits_script}
     ${CMAKE_CURRENT_LIST_DIR}/theory_traits_template.h
-    ${kinds_files}
+    ${KINDS_FILES}
     > ${CMAKE_CURRENT_BINARY_DIR}/theory_traits.h
   DEPENDS mktheorytraits theory_traits_template.h
 )
@@ -51,7 +32,7 @@ add_custom_command(
   COMMAND
     ${mktheorytraits_script}
     ${CMAKE_CURRENT_LIST_DIR}/type_enumerator_template.cpp
-    ${kinds_files}
+    ${KINDS_FILES}
     > ${CMAKE_CURRENT_BINARY_DIR}/type_enumerator.cpp
   DEPENDS mktheorytraits type_enumerator_template.cpp
 )