From: Mathias Preiner Date: Mon, 24 Sep 2018 23:23:37 +0000 (-0700) Subject: cmake: Fix theory order #2. (#2522) X-Git-Tag: cvc5-1.0.0~4517 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2772965140024b2bf75e800dea1d9c2e0126f7a0;p=cvc5.git cmake: Fix theory order #2. (#2522) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 96d462d96..9948b0ec9 100644 --- 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 83bd2d585..6a06bc8ed 100644 --- 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 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 )