diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-09-24 16:23:37 -0700 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-09-24 16:23:37 -0700 |
| commit | 2772965140024b2bf75e800dea1d9c2e0126f7a0 (patch) | |
| tree | 5137887f9852c666a0f28e03761f04404878cf49 /src/theory/CMakeLists.txt | |
| parent | 2252b50b1393b3c50060a1728f3c10f167f44356 (diff) | |
cmake: Fix theory order #2. (#2522)
Diffstat (limited to 'src/theory/CMakeLists.txt')
| -rw-r--r-- | src/theory/CMakeLists.txt | 25 |
1 files changed, 3 insertions, 22 deletions
diff --git a/src/theory/CMakeLists.txt b/src/theory/CMakeLists.txt index 535c1d5df..028cb3504 100644 --- 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 ) |