mirror of
https://github.com/Z3Prover/z3
synced 2026-03-06 21:34:53 +00:00
42f5047463
In older versions, this was dependent upon the version of cmake, but when it was updated for newer cmake, these remnants were left.
33 lines
1.1 KiB
CMake
33 lines
1.1 KiB
CMake
# If this code for adding the rule to generate the database file is ever needed
|
|
# for other components then we should refactor this code into
|
|
# z3_add_component()
|
|
if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/database.h")
|
|
message(FATAL_ERROR "The generated file \"${CMAKE_CURRENT_SOURCE_DIR}/database.h\""
|
|
${z3_polluted_tree_msg})
|
|
endif()
|
|
|
|
add_custom_command(OUTPUT "database.h"
|
|
COMMAND "${PYTHON_EXECUTABLE}"
|
|
"${PROJECT_SOURCE_DIR}/scripts/mk_pat_db.py"
|
|
"${CMAKE_CURRENT_SOURCE_DIR}/database.smt2"
|
|
"${CMAKE_CURRENT_BINARY_DIR}/database.h"
|
|
MAIN_DEPENDENCY "${CMAKE_CURRENT_SOURCE_DIR}/database.smt2"
|
|
DEPENDS "${PROJECT_SOURCE_DIR}/scripts/mk_pat_db.py"
|
|
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
|
|
COMMENT "Generating \"database.h\""
|
|
USES_TERMINAL
|
|
VERBATIM
|
|
)
|
|
|
|
z3_add_component(pattern
|
|
SOURCES
|
|
expr_pattern_match.cpp
|
|
pattern_inference.cpp
|
|
# Let CMake know this target depends on this generated
|
|
# header file
|
|
${CMAKE_CURRENT_BINARY_DIR}/database.h
|
|
COMPONENT_DEPENDENCIES
|
|
normal_forms
|
|
rewriter
|
|
smt2parser
|
|
)
|