From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Mon, 24 Sep 2018 20:14:13 +0000 (-0700)
Subject: cmake: Fix theory order. (#2518)
X-Git-Tag: cvc5-1.0.0~4519
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=af1eee00a63c01328d02751a4c44914e1fd6efe4;p=cvc5.git

cmake: Fix theory order. (#2518)
---

diff --git a/src/theory/CMakeLists.txt b/src/theory/CMakeLists.txt
index 3259ce6c0..535c1d5df 100644
--- a/src/theory/CMakeLists.txt
+++ b/src/theory/CMakeLists.txt
@@ -4,7 +4,24 @@ libcvc4_add_sources(GENERATED
   type_enumerator.cpp
 )
 
-file(GLOB kinds_files ${PROJECT_SOURCE_DIR}/src/theory/*/kinds)
+# 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)