diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-09-24 13:14:13 -0700 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-24 15:14:13 -0500 |
| commit | af1eee00a63c01328d02751a4c44914e1fd6efe4 (patch) | |
| tree | 3d71105fb4f66f1ab979b62aede281db750a8228 /src/theory/CMakeLists.txt | |
| parent | 10b73a8778f12ea8d955ad83d8cba3697eb2a168 (diff) | |
cmake: Fix theory order. (#2518)
Diffstat (limited to 'src/theory/CMakeLists.txt')
| -rw-r--r-- | src/theory/CMakeLists.txt | 19 |
1 files changed, 18 insertions, 1 deletions
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) |