mirror of
https://github.com/Z3Prover/z3
synced 2025-11-19 12:20:49 +00:00
Move CMakeLists.txt files (other than the one in the repository root)
and the cmake directory into a new directory ``contrib/cmake`` that mirrors the directory structure of the root. This is a comprimise between me and Christoph Wintersteiger that was suggested by Arie Gurfinkel that allows the CMake build system to live in the Z3 repository but not impact the Z3 developers that want to avoid the CMake build system. The build system will not work in its new location and a bootstrap script will soon be provided that allows a developer to copy the files back to their correct location.
This commit is contained in:
Dan Liew
parent
d54d6b50f0
commit
a3e0eae9ec
82 changed files with 0 additions and 0 deletions
|
|
@ -1,223 +0,0 @@
|
|||
################################################################################
|
||||
# API header files
|
||||
################################################################################
|
||||
# This lists the API header files that are scanned by
|
||||
# some of the build rules to generate some files needed
|
||||
# by the build
|
||||
set(Z3_API_HEADER_FILES_TO_SCAN
|
||||
z3_api.h
|
||||
z3_ast_containers.h
|
||||
z3_algebraic.h
|
||||
z3_polynomial.h
|
||||
z3_rcf.h
|
||||
z3_fixedpoint.h
|
||||
z3_optimization.h
|
||||
z3_interp.h
|
||||
z3_fpa.h
|
||||
)
|
||||
set(Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN "")
|
||||
foreach (header_file ${Z3_API_HEADER_FILES_TO_SCAN})
|
||||
set(full_path_api_header_file "${CMAKE_CURRENT_SOURCE_DIR}/api/${header_file}")
|
||||
list(APPEND Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN "${full_path_api_header_file}")
|
||||
if (NOT EXISTS "${full_path_api_header_file}")
|
||||
message(FATAL_ERROR "API header file \"${full_path_api_header_file}\" does not exist")
|
||||
endif()
|
||||
endforeach()
|
||||
|
||||
################################################################################
|
||||
# Traverse directories each adding a Z3 component
|
||||
################################################################################
|
||||
# I'm duplicating the order in ``mk_project.py`` for now to help us keep
|
||||
# the build systems in sync.
|
||||
#
|
||||
# The components in these directory explicitly declare their dependencies so
|
||||
# you may be able to re-order some of these directories but an error will be
|
||||
# raised if you try to declare a component is dependent on another component
|
||||
# that has not yet been declared.
|
||||
add_subdirectory(util)
|
||||
add_subdirectory(math/polynomial)
|
||||
add_subdirectory(sat)
|
||||
add_subdirectory(nlsat)
|
||||
add_subdirectory(math/hilbert)
|
||||
add_subdirectory(math/simplex)
|
||||
add_subdirectory(math/automata)
|
||||
add_subdirectory(math/interval)
|
||||
add_subdirectory(math/realclosure)
|
||||
add_subdirectory(math/subpaving)
|
||||
add_subdirectory(ast)
|
||||
add_subdirectory(ast/rewriter)
|
||||
add_subdirectory(ast/normal_forms)
|
||||
add_subdirectory(model)
|
||||
add_subdirectory(tactic)
|
||||
add_subdirectory(ast/substitution)
|
||||
add_subdirectory(parsers/util)
|
||||
add_subdirectory(math/grobner)
|
||||
add_subdirectory(math/euclid)
|
||||
add_subdirectory(tactic/core)
|
||||
add_subdirectory(sat/tactic)
|
||||
add_subdirectory(tactic/arith)
|
||||
add_subdirectory(nlsat/tactic)
|
||||
add_subdirectory(math/subpaving/tactic)
|
||||
add_subdirectory(tactic/aig)
|
||||
add_subdirectory(solver)
|
||||
add_subdirectory(ackermannization)
|
||||
add_subdirectory(interp)
|
||||
add_subdirectory(cmd_context)
|
||||
add_subdirectory(cmd_context/extra_cmds)
|
||||
add_subdirectory(parsers/smt2)
|
||||
add_subdirectory(ast/proof_checker)
|
||||
## Simplifier module will be deleted in the future.
|
||||
## It has been replaced with rewriter component.
|
||||
add_subdirectory(ast/simplifier)
|
||||
add_subdirectory(ast/fpa)
|
||||
add_subdirectory(ast/macros)
|
||||
add_subdirectory(ast/pattern)
|
||||
add_subdirectory(ast/rewriter/bit_blaster)
|
||||
add_subdirectory(smt/params)
|
||||
add_subdirectory(smt/proto_model)
|
||||
add_subdirectory(smt)
|
||||
add_subdirectory(tactic/bv)
|
||||
add_subdirectory(smt/tactic)
|
||||
add_subdirectory(tactic/sls)
|
||||
add_subdirectory(qe)
|
||||
add_subdirectory(duality)
|
||||
add_subdirectory(muz/base)
|
||||
add_subdirectory(muz/dataflow)
|
||||
add_subdirectory(muz/transforms)
|
||||
add_subdirectory(muz/rel)
|
||||
add_subdirectory(muz/pdr)
|
||||
add_subdirectory(muz/clp)
|
||||
add_subdirectory(muz/tab)
|
||||
add_subdirectory(muz/bmc)
|
||||
add_subdirectory(muz/ddnf)
|
||||
add_subdirectory(muz/duality)
|
||||
add_subdirectory(muz/fp)
|
||||
add_subdirectory(tactic/nlsat_smt)
|
||||
add_subdirectory(tactic/ufbv)
|
||||
add_subdirectory(sat/sat_solver)
|
||||
add_subdirectory(tactic/smtlogics)
|
||||
add_subdirectory(tactic/fpa)
|
||||
add_subdirectory(tactic/portfolio)
|
||||
add_subdirectory(parsers/smt)
|
||||
add_subdirectory(opt)
|
||||
add_subdirectory(api)
|
||||
add_subdirectory(api/dll)
|
||||
|
||||
################################################################################
|
||||
# libz3
|
||||
################################################################################
|
||||
get_property(Z3_LIBZ3_COMPONENTS_LIST GLOBAL PROPERTY Z3_LIBZ3_COMPONENTS)
|
||||
set (object_files "")
|
||||
foreach (component ${Z3_LIBZ3_COMPONENTS_LIST})
|
||||
list(APPEND object_files $<TARGET_OBJECTS:${component}>)
|
||||
endforeach()
|
||||
if (BUILD_LIBZ3_SHARED)
|
||||
set(lib_type "SHARED")
|
||||
else()
|
||||
set(lib_type "STATIC")
|
||||
endif()
|
||||
add_library(libz3 ${lib_type} ${object_files})
|
||||
# FIXME: Set "VERSION" and "SOVERSION" properly
|
||||
set_target_properties(libz3 PROPERTIES
|
||||
# FIXME: Should we be using ${Z3_VERSION} here?
|
||||
# VERSION: Sets up symlinks, does it do anything else?
|
||||
VERSION ${Z3_VERSION}
|
||||
# SOVERSION: On platforms that use ELF this sets the API version
|
||||
# and should be incremented everytime the API changes
|
||||
SOVERSION ${Z3_VERSION})
|
||||
|
||||
if (NOT MSVC)
|
||||
# On UNIX like platforms if we don't change the OUTPUT_NAME
|
||||
# the library gets a name like ``liblibz3.so`` so we change it
|
||||
# here. We don't do a rename with MSVC because we get file naming
|
||||
# conflicts (the z3 executable also has this OUTPUT_NAME) with
|
||||
# ``.ilk``, ``.pdb``, ``.lib`` and ``.exp`` files sharing the same
|
||||
# prefix.
|
||||
set_target_properties(libz3 PROPERTIES OUTPUT_NAME z3)
|
||||
endif()
|
||||
|
||||
# Using INTERFACE means that targets that try link against libz3 will
|
||||
# automatically link against the libs in Z3_DEPENDENT_LIBS
|
||||
target_link_libraries(libz3 INTERFACE ${Z3_DEPENDENT_LIBS})
|
||||
|
||||
set_property(TARGET libz3 APPEND PROPERTY LINK_FLAGS ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
|
||||
|
||||
# Declare which header file are the public header files of libz3
|
||||
# these will automatically installed when the libz3 target is installed
|
||||
set (libz3_public_headers
|
||||
z3_algebraic.h
|
||||
z3_api.h
|
||||
z3_ast_containers.h
|
||||
z3_fixedpoint.h
|
||||
z3_fpa.h
|
||||
z3.h
|
||||
c++/z3++.h
|
||||
z3_interp.h
|
||||
z3_macros.h
|
||||
z3_optimization.h
|
||||
z3_polynomial.h
|
||||
z3_rcf.h
|
||||
z3_v1.h
|
||||
)
|
||||
foreach (header ${libz3_public_headers})
|
||||
set_property(TARGET libz3 APPEND PROPERTY
|
||||
PUBLIC_HEADER "${CMAKE_SOURCE_DIR}/src/api/${header}")
|
||||
endforeach()
|
||||
|
||||
install(TARGETS libz3
|
||||
LIBRARY DESTINATION "${Z3_INSTALL_LIB_DIR}"
|
||||
ARCHIVE DESTINATION "${Z3_INSTALL_LIB_DIR}"
|
||||
PUBLIC_HEADER DESTINATION "${Z3_INSTALL_INCLUDE_DIR}"
|
||||
)
|
||||
|
||||
if (MSVC)
|
||||
# Handle settings dll exports when using MSVC
|
||||
# FIXME: This seems unnecessarily complicated but I'm doing
|
||||
# this because this is what the python build system does.
|
||||
# CMake has a much more elegant (see ``GenerateExportHeader.cmake``)
|
||||
# way of handling this.
|
||||
set(dll_module_exports_file "${CMAKE_CURRENT_BINARY_DIR}/api_dll.def")
|
||||
add_custom_command(OUTPUT "${dll_module_exports_file}"
|
||||
COMMAND
|
||||
"${PYTHON_EXECUTABLE}"
|
||||
"${CMAKE_SOURCE_DIR}/scripts/mk_def_file.py"
|
||||
"${dll_module_exports_file}"
|
||||
"libz3"
|
||||
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
|
||||
DEPENDS
|
||||
"${CMAKE_SOURCE_DIR}/scripts/mk_def_file.py"
|
||||
"${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
|
||||
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
|
||||
COMMENT "Generating \"${dll_module_exports_file}\""
|
||||
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
|
||||
VERBATIM
|
||||
)
|
||||
add_custom_target(libz3_extra_depends
|
||||
DEPENDS "${dll_module_exports_file}"
|
||||
)
|
||||
add_dependencies(libz3 libz3_extra_depends)
|
||||
set_property(TARGET libz3 APPEND PROPERTY LINK_FLAGS
|
||||
"/DEF:${dll_module_exports_file}"
|
||||
)
|
||||
endif()
|
||||
|
||||
################################################################################
|
||||
# Z3 executable
|
||||
################################################################################
|
||||
add_subdirectory(shell)
|
||||
|
||||
################################################################################
|
||||
# z3-test
|
||||
################################################################################
|
||||
add_subdirectory(test)
|
||||
|
||||
|
||||
################################################################################
|
||||
# Z3 API bindings
|
||||
################################################################################
|
||||
option(BUILD_PYTHON_BINDINGS "Build Python bindings for Z3" OFF)
|
||||
if (BUILD_PYTHON_BINDINGS)
|
||||
add_subdirectory(api/python)
|
||||
endif()
|
||||
|
||||
# TODO: Implement support for other bindigns
|
||||
|
|
@ -1,20 +0,0 @@
|
|||
z3_add_component(ackermannization
|
||||
SOURCES
|
||||
ackermannize_bv_model_converter.cpp
|
||||
ackermannize_bv_tactic.cpp
|
||||
ackr_bound_probe.cpp
|
||||
ackr_helper.cpp
|
||||
ackr_model_converter.cpp
|
||||
lackr.cpp
|
||||
lackr_model_constructor.cpp
|
||||
lackr_model_converter_lazy.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
ast
|
||||
model
|
||||
rewriter
|
||||
solver
|
||||
tactic
|
||||
PYG_FILES
|
||||
ackermannization_params.pyg
|
||||
ackermannize_bv_tactic_params.pyg
|
||||
)
|
||||
|
|
@ -1,72 +0,0 @@
|
|||
set(generated_files
|
||||
api_commands.cpp
|
||||
api_log_macros.cpp
|
||||
api_log_macros.h
|
||||
)
|
||||
|
||||
# Sanity check
|
||||
foreach (gen_file ${generated_files})
|
||||
if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/${gen_file}")
|
||||
message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/${gen_files}\""
|
||||
${z3_polluted_tree_msg})
|
||||
endif()
|
||||
endforeach()
|
||||
|
||||
set(full_path_generated_files "")
|
||||
foreach (gen_file ${generated_files})
|
||||
list(APPEND full_path_generated_files "${CMAKE_CURRENT_BINARY_DIR}/${gen_file}")
|
||||
endforeach()
|
||||
|
||||
add_custom_command(OUTPUT ${generated_files}
|
||||
COMMAND "${PYTHON_EXECUTABLE}"
|
||||
"${CMAKE_SOURCE_DIR}/scripts/update_api.py"
|
||||
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
|
||||
"--api_output_dir"
|
||||
"${CMAKE_CURRENT_BINARY_DIR}"
|
||||
DEPENDS "${CMAKE_SOURCE_DIR}/scripts/update_api.py"
|
||||
"${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
|
||||
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
|
||||
COMMENT "Generating ${generated_files}"
|
||||
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
|
||||
VERBATIM
|
||||
)
|
||||
|
||||
z3_add_component(api
|
||||
SOURCES
|
||||
api_algebraic.cpp
|
||||
api_arith.cpp
|
||||
api_array.cpp
|
||||
api_ast.cpp
|
||||
api_ast_map.cpp
|
||||
api_ast_vector.cpp
|
||||
api_bv.cpp
|
||||
api_config_params.cpp
|
||||
api_context.cpp
|
||||
api_datalog.cpp
|
||||
api_datatype.cpp
|
||||
api_fpa.cpp
|
||||
api_goal.cpp
|
||||
api_interp.cpp
|
||||
api_log.cpp
|
||||
api_model.cpp
|
||||
api_numeral.cpp
|
||||
api_opt.cpp
|
||||
api_params.cpp
|
||||
api_parsers.cpp
|
||||
api_pb.cpp
|
||||
api_polynomial.cpp
|
||||
api_quant.cpp
|
||||
api_rcf.cpp
|
||||
api_seq.cpp
|
||||
api_solver.cpp
|
||||
api_stats.cpp
|
||||
api_tactic.cpp
|
||||
z3_replayer.cpp
|
||||
${full_path_generated_files}
|
||||
COMPONENT_DEPENDENCIES
|
||||
interp
|
||||
opt
|
||||
portfolio
|
||||
realclosure
|
||||
smtparser
|
||||
)
|
||||
|
|
@ -1,13 +0,0 @@
|
|||
set(api_dll_deps api extra_cmds sat)
|
||||
z3_add_component(api_dll
|
||||
SOURCES
|
||||
dll.cpp
|
||||
"${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp"
|
||||
"${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp"
|
||||
"${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp"
|
||||
COMPONENT_DEPENDENCIES
|
||||
${api_dll_deps}
|
||||
)
|
||||
z3_add_install_tactic_rule(${api_dll_deps})
|
||||
z3_add_memory_initializer_rule(${api_dll_deps})
|
||||
z3_add_gparams_register_modules_rule(${api_dll_deps})
|
||||
|
|
@ -1,107 +0,0 @@
|
|||
message(STATUS "Emitting rules to build Z3 python bindings")
|
||||
###############################################################################
|
||||
# Add target to build python bindings for the build directory
|
||||
###############################################################################
|
||||
# This allows the python bindings to be used directly from the build directory
|
||||
set(z3py_files
|
||||
z3.py
|
||||
z3num.py
|
||||
z3poly.py
|
||||
z3printer.py
|
||||
z3rcf.py
|
||||
z3test.py
|
||||
z3types.py
|
||||
z3util.py
|
||||
)
|
||||
|
||||
set(z3py_bindings_build_dest "${CMAKE_BINARY_DIR}")
|
||||
|
||||
set(build_z3_python_bindings_target_depends "")
|
||||
foreach (z3py_file ${z3py_files})
|
||||
add_custom_command(OUTPUT "${z3py_bindings_build_dest}/${z3py_file}"
|
||||
COMMAND "${CMAKE_COMMAND}" "-E" "copy"
|
||||
"${CMAKE_CURRENT_SOURCE_DIR}/${z3py_file}"
|
||||
"${z3py_bindings_build_dest}"
|
||||
DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/${z3py_file}"
|
||||
COMMENT "Copying \"${z3py_file}\" to ${z3py_bindings_build_dest}"
|
||||
)
|
||||
list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/${z3py_file}")
|
||||
endforeach()
|
||||
|
||||
# Generate z3core.py
|
||||
add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3core.py"
|
||||
COMMAND "${PYTHON_EXECUTABLE}"
|
||||
"${CMAKE_SOURCE_DIR}/scripts/update_api.py"
|
||||
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
|
||||
"--z3py-output-dir"
|
||||
"${z3py_bindings_build_dest}"
|
||||
DEPENDS
|
||||
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
|
||||
"${CMAKE_SOURCE_DIR}/scripts/update_api.py"
|
||||
"${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
|
||||
COMMENT "Generating z3core.py"
|
||||
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
|
||||
)
|
||||
list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3core.py")
|
||||
|
||||
# Generate z3consts.py
|
||||
add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3consts.py"
|
||||
COMMAND "${PYTHON_EXECUTABLE}"
|
||||
"${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
|
||||
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
|
||||
"--z3py-output-dir"
|
||||
"${z3py_bindings_build_dest}"
|
||||
DEPENDS
|
||||
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
|
||||
"${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
|
||||
"${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
|
||||
COMMENT "Generating z3consts.py"
|
||||
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
|
||||
)
|
||||
list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3consts.py")
|
||||
|
||||
# Convenient top-level target
|
||||
add_custom_target(build_z3_python_bindings
|
||||
ALL
|
||||
DEPENDS
|
||||
${build_z3_python_bindings_target_depends}
|
||||
)
|
||||
|
||||
###############################################################################
|
||||
# Install
|
||||
###############################################################################
|
||||
option(INSTALL_PYTHON_BINDINGS "Install Python bindings when invoking install target" ON)
|
||||
if (INSTALL_PYTHON_BINDINGS)
|
||||
# Determine the installation path for the bindings
|
||||
message(STATUS "Emitting rules to install Z3 python bindings")
|
||||
execute_process(
|
||||
COMMAND "${PYTHON_EXECUTABLE}" "-c"
|
||||
"import distutils.sysconfig; print(distutils.sysconfig.get_python_lib())"
|
||||
RESULT_VARIABLE exit_code
|
||||
OUTPUT_VARIABLE python_pkg_dir
|
||||
OUTPUT_STRIP_TRAILING_WHITESPACE
|
||||
)
|
||||
|
||||
if (NOT ("${exit_code}" EQUAL 0))
|
||||
message(FATAL_ERROR "Failed to determine your Python package directory")
|
||||
endif()
|
||||
message(STATUS "Detected Python package directory: \"${python_pkg_dir}\"")
|
||||
|
||||
# Check if path exists under the install prefix
|
||||
set(python_install_dir "")
|
||||
string(FIND "${python_pkg_dir}" "${CMAKE_INSTALL_PREFIX}" position)
|
||||
if (NOT ("${position}" EQUAL 0))
|
||||
message(WARNING "The detected Python package directory \"${python_pkg_dir}\" "
|
||||
"does not exist under the install prefix \"${CMAKE_INSTALL_PREFIX}\"."
|
||||
" Running the install target may lead to a broken installation."
|
||||
)
|
||||
endif()
|
||||
# Using DESTDIR still seems to work even if we use an absolute path
|
||||
set(python_install_dir "${python_pkg_dir}")
|
||||
message(STATUS "Python bindings will be installed to \"${python_install_dir}\"")
|
||||
install(FILES ${build_z3_python_bindings_target_depends}
|
||||
DESTINATION "${python_install_dir}"
|
||||
)
|
||||
else()
|
||||
message(STATUS "Not emitting rules to install Z3 python bindings")
|
||||
endif()
|
||||
|
|
@ -1,48 +0,0 @@
|
|||
z3_add_component(ast
|
||||
SOURCES
|
||||
act_cache.cpp
|
||||
arith_decl_plugin.cpp
|
||||
array_decl_plugin.cpp
|
||||
ast.cpp
|
||||
ast_ll_pp.cpp
|
||||
ast_lt.cpp
|
||||
ast_pp_util.cpp
|
||||
ast_printer.cpp
|
||||
ast_smt2_pp.cpp
|
||||
ast_smt_pp.cpp
|
||||
ast_translation.cpp
|
||||
ast_util.cpp
|
||||
bv_decl_plugin.cpp
|
||||
datatype_decl_plugin.cpp
|
||||
decl_collector.cpp
|
||||
dl_decl_plugin.cpp
|
||||
expr2polynomial.cpp
|
||||
expr2var.cpp
|
||||
expr_abstract.cpp
|
||||
expr_functors.cpp
|
||||
expr_map.cpp
|
||||
expr_stat.cpp
|
||||
expr_substitution.cpp
|
||||
for_each_ast.cpp
|
||||
for_each_expr.cpp
|
||||
format.cpp
|
||||
fpa_decl_plugin.cpp
|
||||
func_decl_dependencies.cpp
|
||||
has_free_vars.cpp
|
||||
macro_substitution.cpp
|
||||
num_occurs.cpp
|
||||
occurs.cpp
|
||||
pb_decl_plugin.cpp
|
||||
pp.cpp
|
||||
reg_decl_plugins.cpp
|
||||
seq_decl_plugin.cpp
|
||||
shared_occs.cpp
|
||||
static_features.cpp
|
||||
used_vars.cpp
|
||||
well_sorted.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
polynomial
|
||||
util # Unnecessary? polynomial already depends on util
|
||||
PYG_FILES
|
||||
pp_params.pyg
|
||||
)
|
||||
|
|
@ -1,10 +0,0 @@
|
|||
z3_add_component(fpa
|
||||
SOURCES
|
||||
fpa2bv_converter.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
ast
|
||||
simplifier
|
||||
util
|
||||
PYG_FILES
|
||||
fpa2bv_rewriter_params.pyg
|
||||
)
|
||||
|
|
@ -1,9 +0,0 @@
|
|||
z3_add_component(macros
|
||||
SOURCES
|
||||
macro_finder.cpp
|
||||
macro_manager.cpp
|
||||
macro_util.cpp
|
||||
quasi_macros.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
simplifier
|
||||
)
|
||||
|
|
@ -1,11 +0,0 @@
|
|||
z3_add_component(normal_forms
|
||||
SOURCES
|
||||
defined_names.cpp
|
||||
name_exprs.cpp
|
||||
nnf.cpp
|
||||
pull_quant.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
rewriter
|
||||
PYG_FILES
|
||||
nnf_params.pyg
|
||||
)
|
||||
|
|
@ -1,36 +0,0 @@
|
|||
# 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 \"database.h\""
|
||||
${z3_polluted_tree_msg})
|
||||
endif()
|
||||
|
||||
add_custom_command(OUTPUT "database.h"
|
||||
COMMAND "${PYTHON_EXECUTABLE}"
|
||||
"${CMAKE_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 "${CMAKE_SOURCE_DIR}/scripts/mk_pat_db.py"
|
||||
"${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
|
||||
COMMENT "Generating \"database.h\""
|
||||
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
|
||||
VERBATIM
|
||||
)
|
||||
|
||||
z3_add_component(pattern
|
||||
SOURCES
|
||||
expr_pattern_match.cpp
|
||||
pattern_inference.cpp
|
||||
pattern_inference_params.cpp
|
||||
# Let CMake know this target depends on this generated
|
||||
# header file
|
||||
${CMAKE_CURRENT_BINARY_DIR}/database.h
|
||||
COMPONENT_DEPENDENCIES
|
||||
normal_forms
|
||||
simplifier
|
||||
smt2parser
|
||||
PYG_FILES
|
||||
pattern_inference_params_helper.pyg
|
||||
)
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
z3_add_component(proof_checker
|
||||
SOURCES
|
||||
proof_checker.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
rewriter
|
||||
)
|
||||
|
|
@ -1,34 +0,0 @@
|
|||
z3_add_component(rewriter
|
||||
SOURCES
|
||||
arith_rewriter.cpp
|
||||
array_rewriter.cpp
|
||||
ast_counter.cpp
|
||||
bool_rewriter.cpp
|
||||
bv_rewriter.cpp
|
||||
datatype_rewriter.cpp
|
||||
der.cpp
|
||||
dl_rewriter.cpp
|
||||
expr_replacer.cpp
|
||||
expr_safe_replace.cpp
|
||||
factor_rewriter.cpp
|
||||
fpa_rewriter.cpp
|
||||
mk_simplified_app.cpp
|
||||
pb_rewriter.cpp
|
||||
quant_hoist.cpp
|
||||
rewriter.cpp
|
||||
seq_rewriter.cpp
|
||||
th_rewriter.cpp
|
||||
var_subst.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
ast
|
||||
automata
|
||||
polynomial
|
||||
PYG_FILES
|
||||
arith_rewriter_params.pyg
|
||||
array_rewriter_params.pyg
|
||||
bool_rewriter_params.pyg
|
||||
bv_rewriter_params.pyg
|
||||
fpa_rewriter_params.pyg
|
||||
poly_rewriter_params.pyg
|
||||
rewriter_params.pyg
|
||||
)
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
z3_add_component(bit_blaster
|
||||
SOURCES
|
||||
bit_blaster.cpp
|
||||
bit_blaster_rewriter.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
rewriter
|
||||
simplifier
|
||||
)
|
||||
|
|
@ -1,30 +0,0 @@
|
|||
z3_add_component(simplifier
|
||||
SOURCES
|
||||
arith_simplifier_params.cpp
|
||||
arith_simplifier_plugin.cpp
|
||||
array_simplifier_params.cpp
|
||||
array_simplifier_plugin.cpp
|
||||
basic_simplifier_plugin.cpp
|
||||
bit2int.cpp
|
||||
bv_elim.cpp
|
||||
bv_simplifier_params.cpp
|
||||
bv_simplifier_plugin.cpp
|
||||
datatype_simplifier_plugin.cpp
|
||||
distribute_forall.cpp
|
||||
elim_bounds.cpp
|
||||
fpa_simplifier_plugin.cpp
|
||||
inj_axiom.cpp
|
||||
maximise_ac_sharing.cpp
|
||||
poly_simplifier_plugin.cpp
|
||||
pull_ite_tree.cpp
|
||||
push_app_ite.cpp
|
||||
seq_simplifier_plugin.cpp
|
||||
simplifier.cpp
|
||||
simplifier_plugin.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
rewriter
|
||||
PYG_FILES
|
||||
arith_simplifier_params_helper.pyg
|
||||
array_simplifier_params_helper.pyg
|
||||
bv_simplifier_params_helper.pyg
|
||||
)
|
||||
|
|
@ -1,10 +0,0 @@
|
|||
z3_add_component(substitution
|
||||
SOURCES
|
||||
matcher.cpp
|
||||
substitution.cpp
|
||||
substitution_tree.cpp
|
||||
unifier.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
ast
|
||||
rewriter
|
||||
)
|
||||
|
|
@ -1,21 +0,0 @@
|
|||
z3_add_component(cmd_context
|
||||
SOURCES
|
||||
basic_cmds.cpp
|
||||
check_logic.cpp
|
||||
cmd_context.cpp
|
||||
cmd_context_to_goal.cpp
|
||||
cmd_util.cpp
|
||||
context_params.cpp
|
||||
echo_tactic.cpp
|
||||
eval_cmd.cpp
|
||||
interpolant_cmds.cpp
|
||||
parametric_cmd.cpp
|
||||
pdecl.cpp
|
||||
simplify_cmd.cpp
|
||||
tactic_cmds.cpp
|
||||
tactic_manager.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
interp
|
||||
rewriter
|
||||
solver
|
||||
)
|
||||
|
|
@ -1,10 +0,0 @@
|
|||
z3_add_component(extra_cmds
|
||||
SOURCES
|
||||
dbg_cmds.cpp
|
||||
polynomial_cmds.cpp
|
||||
subpaving_cmds.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
arith_tactics
|
||||
cmd_context
|
||||
subpaving_tactic
|
||||
)
|
||||
|
|
@ -1,11 +0,0 @@
|
|||
z3_add_component(duality
|
||||
SOURCES
|
||||
duality_profiling.cpp
|
||||
duality_rpfp.cpp
|
||||
duality_solver.cpp
|
||||
duality_wrapper.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
interp
|
||||
qe
|
||||
smt
|
||||
)
|
||||
|
|
@ -1,19 +0,0 @@
|
|||
z3_add_component(interp
|
||||
SOURCES
|
||||
iz3base.cpp
|
||||
iz3checker.cpp
|
||||
iz3foci.cpp
|
||||
iz3interp.cpp
|
||||
iz3mgr.cpp
|
||||
iz3pp.cpp
|
||||
iz3profiling.cpp
|
||||
iz3proof.cpp
|
||||
iz3proof_itp.cpp
|
||||
iz3scopes.cpp
|
||||
iz3translate.cpp
|
||||
iz3translate_direct.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
solver
|
||||
PYG_FILES
|
||||
interp_params.pyg
|
||||
)
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
z3_add_component(automata
|
||||
SOURCES
|
||||
automaton.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
util
|
||||
)
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
z3_add_component(euclid
|
||||
SOURCES
|
||||
euclidean_solver.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
util
|
||||
)
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
z3_add_component(grobner
|
||||
SOURCES
|
||||
grobner.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
ast
|
||||
)
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
z3_add_component(hilbert
|
||||
SOURCES
|
||||
hilbert_basis.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
util
|
||||
)
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
z3_add_component(interval
|
||||
SOURCES
|
||||
interval_mpq.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
util
|
||||
)
|
||||
|
|
@ -1,16 +0,0 @@
|
|||
z3_add_component(polynomial
|
||||
SOURCES
|
||||
algebraic_numbers.cpp
|
||||
polynomial_cache.cpp
|
||||
polynomial.cpp
|
||||
polynomial_factorization.cpp
|
||||
rpolynomial.cpp
|
||||
sexpr2upolynomial.cpp
|
||||
upolynomial.cpp
|
||||
upolynomial_factorization.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
util
|
||||
PYG_FILES
|
||||
algebraic_params.pyg
|
||||
)
|
||||
|
||||
|
|
@ -1,9 +0,0 @@
|
|||
z3_add_component(realclosure
|
||||
SOURCES
|
||||
mpz_matrix.cpp
|
||||
realclosure.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
interval
|
||||
PYG_FILES
|
||||
rcf_params.pyg
|
||||
)
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
z3_add_component(simplex
|
||||
SOURCES
|
||||
simplex.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
util
|
||||
)
|
||||
|
|
@ -1,11 +0,0 @@
|
|||
z3_add_component(subpaving
|
||||
SOURCES
|
||||
subpaving.cpp
|
||||
subpaving_hwf.cpp
|
||||
subpaving_mpf.cpp
|
||||
subpaving_mpff.cpp
|
||||
subpaving_mpfx.cpp
|
||||
subpaving_mpq.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
interval
|
||||
)
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
z3_add_component(subpaving_tactic
|
||||
SOURCES
|
||||
expr2subpaving.cpp
|
||||
subpaving_tactic.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
core_tactics
|
||||
subpaving
|
||||
)
|
||||
|
|
@ -1,18 +0,0 @@
|
|||
z3_add_component(model
|
||||
SOURCES
|
||||
func_interp.cpp
|
||||
model2expr.cpp
|
||||
model_core.cpp
|
||||
model.cpp
|
||||
model_evaluator.cpp
|
||||
model_implicant.cpp
|
||||
model_pp.cpp
|
||||
model_smt2_pp.cpp
|
||||
model_v2_pp.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
rewriter
|
||||
PYG_FILES
|
||||
model_evaluator_params.pyg
|
||||
model_params.pyg
|
||||
)
|
||||
|
||||
|
|
@ -1,23 +0,0 @@
|
|||
z3_add_component(muz
|
||||
SOURCES
|
||||
bind_variables.cpp
|
||||
dl_boogie_proof.cpp
|
||||
dl_context.cpp
|
||||
dl_costs.cpp
|
||||
dl_rule.cpp
|
||||
dl_rule_set.cpp
|
||||
dl_rule_subsumption_index.cpp
|
||||
dl_rule_transformer.cpp
|
||||
dl_util.cpp
|
||||
hnf.cpp
|
||||
proof_utils.cpp
|
||||
rule_properties.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
aig_tactic
|
||||
qe
|
||||
sat
|
||||
smt
|
||||
smt2parser
|
||||
PYG_FILES
|
||||
fixedpoint_params.pyg
|
||||
)
|
||||
|
|
@ -1,7 +0,0 @@
|
|||
z3_add_component(bmc
|
||||
SOURCES
|
||||
dl_bmc_engine.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
muz
|
||||
transforms
|
||||
)
|
||||
|
|
@ -1,7 +0,0 @@
|
|||
z3_add_component(clp
|
||||
SOURCES
|
||||
clp_context.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
muz
|
||||
transforms
|
||||
)
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
z3_add_component(dataflow
|
||||
SOURCES
|
||||
dataflow.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
muz
|
||||
)
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
z3_add_component(ddnf
|
||||
SOURCES
|
||||
ddnf.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
muz
|
||||
rel
|
||||
transforms
|
||||
)
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
z3_add_component(duality_intf
|
||||
SOURCES
|
||||
duality_dl_interface.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
duality
|
||||
muz
|
||||
transforms
|
||||
)
|
||||
|
|
@ -1,16 +0,0 @@
|
|||
z3_add_component(fp
|
||||
SOURCES
|
||||
datalog_parser.cpp
|
||||
dl_cmds.cpp
|
||||
dl_register_engine.cpp
|
||||
horn_tactic.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
bmc
|
||||
clp
|
||||
ddnf
|
||||
duality_intf
|
||||
muz
|
||||
pdr
|
||||
rel
|
||||
tab
|
||||
)
|
||||
|
|
@ -1,20 +0,0 @@
|
|||
z3_add_component(pdr
|
||||
SOURCES
|
||||
pdr_closure.cpp
|
||||
pdr_context.cpp
|
||||
pdr_dl_interface.cpp
|
||||
pdr_farkas_learner.cpp
|
||||
pdr_generalizers.cpp
|
||||
pdr_manager.cpp
|
||||
pdr_prop_solver.cpp
|
||||
pdr_reachable_cache.cpp
|
||||
pdr_smt_context_manager.cpp
|
||||
pdr_sym_mux.cpp
|
||||
pdr_util.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
arith_tactics
|
||||
core_tactics
|
||||
muz
|
||||
smt_tactic
|
||||
transforms
|
||||
)
|
||||
|
|
@ -1,32 +0,0 @@
|
|||
z3_add_component(rel
|
||||
SOURCES
|
||||
aig_exporter.cpp
|
||||
check_relation.cpp
|
||||
dl_base.cpp
|
||||
dl_bound_relation.cpp
|
||||
dl_check_table.cpp
|
||||
dl_compiler.cpp
|
||||
dl_external_relation.cpp
|
||||
dl_finite_product_relation.cpp
|
||||
dl_instruction.cpp
|
||||
dl_interval_relation.cpp
|
||||
dl_lazy_table.cpp
|
||||
dl_mk_explanations.cpp
|
||||
dl_mk_partial_equiv.cpp
|
||||
dl_mk_similarity_compressor.cpp
|
||||
dl_mk_simple_joins.cpp
|
||||
dl_product_relation.cpp
|
||||
dl_relation_manager.cpp
|
||||
dl_sieve_relation.cpp
|
||||
dl_sparse_table.cpp
|
||||
dl_table.cpp
|
||||
dl_table_relation.cpp
|
||||
doc.cpp
|
||||
karr_relation.cpp
|
||||
rel_context.cpp
|
||||
tbv.cpp
|
||||
udoc_relation.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
muz
|
||||
transforms
|
||||
)
|
||||
|
|
@ -1,7 +0,0 @@
|
|||
z3_add_component(tab
|
||||
SOURCES
|
||||
tab_context.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
muz
|
||||
transforms
|
||||
)
|
||||
|
|
@ -1,28 +0,0 @@
|
|||
z3_add_component(transforms
|
||||
SOURCES
|
||||
dl_mk_array_blast.cpp
|
||||
dl_mk_backwards.cpp
|
||||
dl_mk_bit_blast.cpp
|
||||
dl_mk_coalesce.cpp
|
||||
dl_mk_coi_filter.cpp
|
||||
dl_mk_filter_rules.cpp
|
||||
dl_mk_interp_tail_simplifier.cpp
|
||||
dl_mk_karr_invariants.cpp
|
||||
dl_mk_loop_counter.cpp
|
||||
dl_mk_magic_sets.cpp
|
||||
dl_mk_magic_symbolic.cpp
|
||||
dl_mk_quantifier_abstraction.cpp
|
||||
dl_mk_quantifier_instantiation.cpp
|
||||
dl_mk_rule_inliner.cpp
|
||||
dl_mk_scale.cpp
|
||||
dl_mk_separate_negated_tails.cpp
|
||||
dl_mk_slice.cpp
|
||||
dl_mk_subsumption_checker.cpp
|
||||
dl_mk_unbound_compressor.cpp
|
||||
dl_mk_unfold.cpp
|
||||
dl_transforms.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
dataflow
|
||||
hilbert
|
||||
muz
|
||||
)
|
||||
|
|
@ -1,14 +0,0 @@
|
|||
z3_add_component(nlsat
|
||||
SOURCES
|
||||
nlsat_clause.cpp
|
||||
nlsat_evaluator.cpp
|
||||
nlsat_explain.cpp
|
||||
nlsat_interval_set.cpp
|
||||
nlsat_solver.cpp
|
||||
nlsat_types.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
polynomial
|
||||
sat
|
||||
PYG_FILES
|
||||
nlsat_params.pyg
|
||||
)
|
||||
|
|
@ -1,10 +0,0 @@
|
|||
z3_add_component(nlsat_tactic
|
||||
SOURCES
|
||||
goal2nlsat.cpp
|
||||
nlsat_tactic.cpp
|
||||
qfnra_nlsat_tactic.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
arith_tactics
|
||||
nlsat
|
||||
sat_tactic
|
||||
)
|
||||
|
|
@ -1,26 +0,0 @@
|
|||
z3_add_component(opt
|
||||
SOURCES
|
||||
bcd2.cpp
|
||||
fu_malik.cpp
|
||||
hitting_sets.cpp
|
||||
maxhs.cpp
|
||||
maxres.cpp
|
||||
maxsls.cpp
|
||||
maxsmt.cpp
|
||||
mss.cpp
|
||||
mus.cpp
|
||||
opt_cmds.cpp
|
||||
opt_context.cpp
|
||||
opt_pareto.cpp
|
||||
optsmt.cpp
|
||||
opt_solver.cpp
|
||||
pb_sls.cpp
|
||||
wmax.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
sat_solver
|
||||
sls_tactic
|
||||
smt
|
||||
smtlogic_tactics
|
||||
PYG_FILES
|
||||
opt_params.pyg
|
||||
)
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
z3_add_component(smtparser
|
||||
SOURCES
|
||||
smtlib.cpp
|
||||
smtlib_solver.cpp
|
||||
smtparser.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
portfolio
|
||||
)
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
z3_add_component(smt2parser
|
||||
SOURCES
|
||||
smt2parser.cpp
|
||||
smt2scanner.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
cmd_context
|
||||
parser_util
|
||||
)
|
||||
|
|
@ -1,11 +0,0 @@
|
|||
z3_add_component(parser_util
|
||||
SOURCES
|
||||
cost_parser.cpp
|
||||
pattern_validation.cpp
|
||||
scanner.cpp
|
||||
simple_parser.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
ast
|
||||
PYG_FILES
|
||||
parser_params.pyg
|
||||
)
|
||||
|
|
@ -1,21 +0,0 @@
|
|||
z3_add_component(qe
|
||||
SOURCES
|
||||
nlarith_util.cpp
|
||||
qe_arith.cpp
|
||||
qe_arith_plugin.cpp
|
||||
qe_array_plugin.cpp
|
||||
qe_bool_plugin.cpp
|
||||
qe_bv_plugin.cpp
|
||||
qe_cmd.cpp
|
||||
qe.cpp
|
||||
qe_datatype_plugin.cpp
|
||||
qe_dl_plugin.cpp
|
||||
qe_lite.cpp
|
||||
qe_sat_tactic.cpp
|
||||
qe_tactic.cpp
|
||||
qe_util.cpp
|
||||
vsubst_tactic.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
sat
|
||||
smt
|
||||
)
|
||||
|
|
@ -1,29 +0,0 @@
|
|||
z3_add_component(sat
|
||||
SOURCES
|
||||
dimacs.cpp
|
||||
sat_asymm_branch.cpp
|
||||
sat_bceq.cpp
|
||||
sat_clause.cpp
|
||||
sat_clause_set.cpp
|
||||
sat_clause_use_list.cpp
|
||||
sat_cleaner.cpp
|
||||
sat_config.cpp
|
||||
sat_elim_eqs.cpp
|
||||
sat_iff3_finder.cpp
|
||||
sat_integrity_checker.cpp
|
||||
sat_model_converter.cpp
|
||||
sat_mus.cpp
|
||||
sat_probing.cpp
|
||||
sat_scc.cpp
|
||||
sat_simplifier.cpp
|
||||
sat_sls.cpp
|
||||
sat_solver.cpp
|
||||
sat_watched.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
util
|
||||
PYG_FILES
|
||||
sat_asymm_branch_params.pyg
|
||||
sat_params.pyg
|
||||
sat_scc_params.pyg
|
||||
sat_simplifier_params.pyg
|
||||
)
|
||||
|
|
@ -1,11 +0,0 @@
|
|||
z3_add_component(sat_solver
|
||||
SOURCES
|
||||
inc_sat_solver.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
aig_tactic
|
||||
arith_tactics
|
||||
bv_tactics
|
||||
core_tactics
|
||||
sat_tactic
|
||||
solver
|
||||
)
|
||||
|
|
@ -1,9 +0,0 @@
|
|||
z3_add_component(sat_tactic
|
||||
SOURCES
|
||||
atom2bool_var.cpp
|
||||
goal2sat.cpp
|
||||
sat_tactic.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
sat
|
||||
tactic
|
||||
)
|
||||
|
|
@ -1,47 +0,0 @@
|
|||
set (shell_object_files "")
|
||||
# FIXME: z3 should really link against libz3 and not the
|
||||
# individual components. Several things prevent us from
|
||||
# doing this
|
||||
# * The api_dll component in libz3 shouldn't be used the
|
||||
# the z3 executable.
|
||||
# * The z3 executable uses symbols that are hidden in libz3
|
||||
|
||||
# We are only using these dependencies to enforce a build
|
||||
# order. We don't use this list for actual linking.
|
||||
set(shell_deps api extra_cmds opt sat)
|
||||
z3_expand_dependencies(shell_expanded_deps ${shell_deps})
|
||||
get_property(Z3_LIBZ3_COMPONENTS_LIST GLOBAL PROPERTY Z3_LIBZ3_COMPONENTS)
|
||||
foreach (component ${Z3_LIBZ3_COMPONENTS_LIST})
|
||||
if (NOT ("${component}" STREQUAL "api_dll"))
|
||||
# We don't use the api_dll component in the Z3 executable
|
||||
list(APPEND shell_object_files $<TARGET_OBJECTS:${component}>)
|
||||
endif()
|
||||
endforeach()
|
||||
add_executable(shell
|
||||
datalog_frontend.cpp
|
||||
dimacs_frontend.cpp
|
||||
"${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp"
|
||||
"${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp"
|
||||
main.cpp
|
||||
"${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp"
|
||||
opt_frontend.cpp
|
||||
smtlib_frontend.cpp
|
||||
z3_log_frontend.cpp
|
||||
# FIXME: shell should really link against libz3 but it can't due to requiring
|
||||
# use of some hidden symbols. Also libz3 has the ``api_dll`` component which
|
||||
# we don't want (I think).
|
||||
${shell_object_files}
|
||||
)
|
||||
z3_add_install_tactic_rule(${shell_deps})
|
||||
z3_add_memory_initializer_rule(${shell_deps})
|
||||
z3_add_gparams_register_modules_rule(${shell_deps})
|
||||
set_target_properties(shell PROPERTIES OUTPUT_NAME z3)
|
||||
target_compile_definitions(shell PRIVATE ${Z3_COMPONENT_CXX_DEFINES})
|
||||
target_compile_options(shell PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
|
||||
target_include_directories(shell PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS})
|
||||
target_link_libraries(shell PRIVATE ${Z3_DEPENDENT_LIBS})
|
||||
z3_add_component_dependencies_to_target(shell ${shell_expanded_deps})
|
||||
set_property(TARGET shell APPEND PROPERTY LINK_FLAGS ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
|
||||
install(TARGETS shell
|
||||
RUNTIME DESTINATION "${Z3_INSTALL_BIN_DIR}"
|
||||
)
|
||||
|
|
@ -1,77 +0,0 @@
|
|||
z3_add_component(smt
|
||||
SOURCES
|
||||
arith_eq_adapter.cpp
|
||||
arith_eq_solver.cpp
|
||||
asserted_formulas.cpp
|
||||
cached_var_subst.cpp
|
||||
cost_evaluator.cpp
|
||||
dyn_ack.cpp
|
||||
elim_term_ite.cpp
|
||||
expr_context_simplifier.cpp
|
||||
fingerprints.cpp
|
||||
mam.cpp
|
||||
old_interval.cpp
|
||||
qi_queue.cpp
|
||||
smt_almost_cg_table.cpp
|
||||
smt_case_split_queue.cpp
|
||||
smt_cg_table.cpp
|
||||
smt_checker.cpp
|
||||
smt_clause.cpp
|
||||
smt_conflict_resolution.cpp
|
||||
smt_context.cpp
|
||||
smt_context_inv.cpp
|
||||
smt_context_pp.cpp
|
||||
smt_context_stat.cpp
|
||||
smt_enode.cpp
|
||||
smt_farkas_util.cpp
|
||||
smt_for_each_relevant_expr.cpp
|
||||
smt_implied_equalities.cpp
|
||||
smt_internalizer.cpp
|
||||
smt_justification.cpp
|
||||
smt_kernel.cpp
|
||||
smt_literal.cpp
|
||||
smt_model_checker.cpp
|
||||
smt_model_finder.cpp
|
||||
smt_model_generator.cpp
|
||||
smt_quantifier.cpp
|
||||
smt_quantifier_stat.cpp
|
||||
smt_quick_checker.cpp
|
||||
smt_relevancy.cpp
|
||||
smt_setup.cpp
|
||||
smt_solver.cpp
|
||||
smt_statistics.cpp
|
||||
smt_theory.cpp
|
||||
smt_value_sort.cpp
|
||||
theory_arith.cpp
|
||||
theory_array_base.cpp
|
||||
theory_array.cpp
|
||||
theory_array_full.cpp
|
||||
theory_bv.cpp
|
||||
theory_datatype.cpp
|
||||
theory_dense_diff_logic.cpp
|
||||
theory_diff_logic.cpp
|
||||
theory_dl.cpp
|
||||
theory_dummy.cpp
|
||||
theory_fpa.cpp
|
||||
theory_opt.cpp
|
||||
theory_pb.cpp
|
||||
theory_seq.cpp
|
||||
theory_utvpi.cpp
|
||||
theory_wmaxsat.cpp
|
||||
uses_theory.cpp
|
||||
watch_list.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
bit_blaster
|
||||
cmd_context
|
||||
euclid
|
||||
fpa
|
||||
grobner
|
||||
macros
|
||||
normal_forms
|
||||
parser_util
|
||||
pattern
|
||||
proof_checker
|
||||
proto_model
|
||||
simplex
|
||||
substitution
|
||||
)
|
||||
|
|
@ -1,18 +0,0 @@
|
|||
z3_add_component(smt_params
|
||||
SOURCES
|
||||
dyn_ack_params.cpp
|
||||
preprocessor_params.cpp
|
||||
qi_params.cpp
|
||||
smt_params.cpp
|
||||
theory_arith_params.cpp
|
||||
theory_array_params.cpp
|
||||
theory_bv_params.cpp
|
||||
theory_pb_params.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
ast
|
||||
bit_blaster
|
||||
pattern
|
||||
simplifier
|
||||
PYG_FILES
|
||||
smt_params_helper.pyg
|
||||
)
|
||||
|
|
@ -1,13 +0,0 @@
|
|||
z3_add_component(proto_model
|
||||
SOURCES
|
||||
array_factory.cpp
|
||||
datatype_factory.cpp
|
||||
numeral_factory.cpp
|
||||
proto_model.cpp
|
||||
struct_factory.cpp
|
||||
value_factory.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
model
|
||||
simplifier
|
||||
smt_params
|
||||
)
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
z3_add_component(smt_tactic
|
||||
SOURCES
|
||||
ctx_solver_simplify_tactic.cpp
|
||||
smt_tactic.cpp
|
||||
unit_subsumption_tactic.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
smt
|
||||
)
|
||||
|
|
@ -1,13 +0,0 @@
|
|||
z3_add_component(solver
|
||||
SOURCES
|
||||
check_sat_result.cpp
|
||||
combined_solver.cpp
|
||||
solver.cpp
|
||||
solver_na2as.cpp
|
||||
tactic2solver.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
model
|
||||
tactic
|
||||
PYG_FILES
|
||||
combined_solver_params.pyg
|
||||
)
|
||||
|
|
@ -1,20 +0,0 @@
|
|||
z3_add_component(tactic
|
||||
SOURCES
|
||||
equiv_proof_converter.cpp
|
||||
extension_model_converter.cpp
|
||||
filter_model_converter.cpp
|
||||
goal.cpp
|
||||
goal_num_occurs.cpp
|
||||
goal_shared_occs.cpp
|
||||
goal_util.cpp
|
||||
horn_subsume_model_converter.cpp
|
||||
model_converter.cpp
|
||||
probe.cpp
|
||||
proof_converter.cpp
|
||||
replace_proof_converter.cpp
|
||||
tactical.cpp
|
||||
tactic.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
ast
|
||||
model
|
||||
)
|
||||
|
|
@ -1,7 +0,0 @@
|
|||
z3_add_component(aig_tactic
|
||||
SOURCES
|
||||
aig.cpp
|
||||
aig_tactic.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
tactic
|
||||
)
|
||||
|
|
@ -1,31 +0,0 @@
|
|||
z3_add_component(arith_tactics
|
||||
SOURCES
|
||||
add_bounds_tactic.cpp
|
||||
arith_bounds_tactic.cpp
|
||||
bound_manager.cpp
|
||||
bound_propagator.cpp
|
||||
bv2int_rewriter.cpp
|
||||
bv2real_rewriter.cpp
|
||||
card2bv_tactic.cpp
|
||||
degree_shift_tactic.cpp
|
||||
diff_neq_tactic.cpp
|
||||
elim01_tactic.cpp
|
||||
eq2bv_tactic.cpp
|
||||
factor_tactic.cpp
|
||||
fix_dl_var_tactic.cpp
|
||||
fm_tactic.cpp
|
||||
lia2card_tactic.cpp
|
||||
lia2pb_tactic.cpp
|
||||
linear_equation.cpp
|
||||
nla2bv_tactic.cpp
|
||||
normalize_bounds_tactic.cpp
|
||||
pb2bv_model_converter.cpp
|
||||
pb2bv_tactic.cpp
|
||||
probe_arith.cpp
|
||||
propagate_ineqs_tactic.cpp
|
||||
purify_arith_tactic.cpp
|
||||
recover_01_tactic.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
core_tactics
|
||||
sat
|
||||
)
|
||||
|
|
@ -1,16 +0,0 @@
|
|||
z3_add_component(bv_tactics
|
||||
SOURCES
|
||||
bit_blaster_model_converter.cpp
|
||||
bit_blaster_tactic.cpp
|
||||
bv1_blaster_tactic.cpp
|
||||
bvarray2uf_rewriter.cpp
|
||||
bvarray2uf_tactic.cpp
|
||||
bv_bounds_tactic.cpp
|
||||
bv_size_reduction_tactic.cpp
|
||||
elim_small_bv_tactic.cpp
|
||||
max_bv_sharing_tactic.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
bit_blaster
|
||||
core_tactics
|
||||
tactic
|
||||
)
|
||||
|
|
@ -1,25 +0,0 @@
|
|||
z3_add_component(core_tactics
|
||||
SOURCES
|
||||
blast_term_ite_tactic.cpp
|
||||
cofactor_elim_term_ite.cpp
|
||||
cofactor_term_ite_tactic.cpp
|
||||
ctx_simplify_tactic.cpp
|
||||
der_tactic.cpp
|
||||
distribute_forall_tactic.cpp
|
||||
elim_term_ite_tactic.cpp
|
||||
elim_uncnstr_tactic.cpp
|
||||
nnf_tactic.cpp
|
||||
occf_tactic.cpp
|
||||
pb_preprocess_tactic.cpp
|
||||
propagate_values_tactic.cpp
|
||||
reduce_args_tactic.cpp
|
||||
simplify_tactic.cpp
|
||||
solve_eqs_tactic.cpp
|
||||
split_clause_tactic.cpp
|
||||
symmetry_reduce_tactic.cpp
|
||||
tseitin_cnf_tactic.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
normal_forms
|
||||
tactic
|
||||
)
|
||||
|
||||
|
|
@ -1,14 +0,0 @@
|
|||
z3_add_component(fpa_tactics
|
||||
SOURCES
|
||||
fpa2bv_model_converter.cpp
|
||||
fpa2bv_tactic.cpp
|
||||
qffp_tactic.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
arith_tactics
|
||||
bv_tactics
|
||||
core_tactics
|
||||
fpa
|
||||
sat_tactic
|
||||
smtlogic_tactics
|
||||
smt_tactic
|
||||
)
|
||||
|
|
@ -1,7 +0,0 @@
|
|||
z3_add_component(nlsat_smt_tactic
|
||||
SOURCES
|
||||
nl_purify_tactic.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
nlsat_tactic
|
||||
smt_tactic
|
||||
)
|
||||
|
|
@ -1,15 +0,0 @@
|
|||
z3_add_component(portfolio
|
||||
SOURCES
|
||||
default_tactic.cpp
|
||||
smt_strategic_solver.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
aig_tactic
|
||||
fp
|
||||
fpa_tactics
|
||||
qe
|
||||
sat_solver
|
||||
sls_tactic
|
||||
smtlogic_tactics
|
||||
subpaving_tactic
|
||||
ufbv_tactic
|
||||
)
|
||||
|
|
@ -1,13 +0,0 @@
|
|||
z3_add_component(sls_tactic
|
||||
SOURCES
|
||||
bvsls_opt_engine.cpp
|
||||
sls_engine.cpp
|
||||
sls_tactic.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
bv_tactics
|
||||
core_tactics
|
||||
normal_forms
|
||||
tactic
|
||||
PYG_FILES
|
||||
sls_params.pyg
|
||||
)
|
||||
|
|
@ -1,31 +0,0 @@
|
|||
z3_add_component(smtlogic_tactics
|
||||
SOURCES
|
||||
nra_tactic.cpp
|
||||
qfaufbv_tactic.cpp
|
||||
qfauflia_tactic.cpp
|
||||
qfbv_tactic.cpp
|
||||
qfidl_tactic.cpp
|
||||
qflia_tactic.cpp
|
||||
qflra_tactic.cpp
|
||||
qfnia_tactic.cpp
|
||||
qfnra_tactic.cpp
|
||||
qfufbv_ackr_model_converter.cpp
|
||||
qfufbv_tactic.cpp
|
||||
qfufnra_tactic.cpp
|
||||
qfuf_tactic.cpp
|
||||
quant_tactics.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
ackermannization
|
||||
aig_tactic
|
||||
arith_tactics
|
||||
bv_tactics
|
||||
fp
|
||||
muz
|
||||
nlsat_tactic
|
||||
nlsat_smt_tactic
|
||||
qe
|
||||
sat_solver
|
||||
smt_tactic
|
||||
PYG_FILES
|
||||
qfufbv_tactic_params.pyg
|
||||
)
|
||||
|
|
@ -1,14 +0,0 @@
|
|||
z3_add_component(ufbv_tactic
|
||||
SOURCES
|
||||
macro_finder_tactic.cpp
|
||||
quasi_macros_tactic.cpp
|
||||
ufbv_rewriter.cpp
|
||||
ufbv_rewriter_tactic.cpp
|
||||
ufbv_tactic.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
core_tactics
|
||||
macros
|
||||
normal_forms
|
||||
rewriter
|
||||
smt_tactic
|
||||
)
|
||||
|
|
@ -1,126 +0,0 @@
|
|||
add_subdirectory(fuzzing)
|
||||
################################################################################
|
||||
# z3-test executable
|
||||
################################################################################
|
||||
set(z3_test_deps api fuzzing simplex)
|
||||
z3_expand_dependencies(z3_test_expanded_deps ${z3_test_deps})
|
||||
set (z3_test_extra_object_files "")
|
||||
foreach (component ${z3_test_expanded_deps})
|
||||
list(APPEND z3_test_extra_object_files $<TARGET_OBJECTS:${component}>)
|
||||
endforeach()
|
||||
add_executable(test-z3
|
||||
EXCLUDE_FROM_ALL
|
||||
algebraic.cpp
|
||||
api_bug.cpp
|
||||
api.cpp
|
||||
arith_rewriter.cpp
|
||||
arith_simplifier_plugin.cpp
|
||||
ast.cpp
|
||||
bit_blaster.cpp
|
||||
bits.cpp
|
||||
bit_vector.cpp
|
||||
buffer.cpp
|
||||
bv_simplifier_plugin.cpp
|
||||
chashtable.cpp
|
||||
check_assumptions.cpp
|
||||
datalog_parser.cpp
|
||||
ddnf.cpp
|
||||
diff_logic.cpp
|
||||
dl_context.cpp
|
||||
dl_product_relation.cpp
|
||||
dl_query.cpp
|
||||
dl_relation.cpp
|
||||
dl_table.cpp
|
||||
dl_util.cpp
|
||||
doc.cpp
|
||||
escaped.cpp
|
||||
ex.cpp
|
||||
expr_rand.cpp
|
||||
expr_substitution.cpp
|
||||
ext_numeral.cpp
|
||||
f2n.cpp
|
||||
factor_rewriter.cpp
|
||||
fixed_bit_vector.cpp
|
||||
for_each_file.cpp
|
||||
get_implied_equalities.cpp
|
||||
"${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp"
|
||||
hashtable.cpp
|
||||
heap.cpp
|
||||
heap_trie.cpp
|
||||
hilbert_basis.cpp
|
||||
horn_subsume_model_converter.cpp
|
||||
hwf.cpp
|
||||
inf_rational.cpp
|
||||
"${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp"
|
||||
interval.cpp
|
||||
karr.cpp
|
||||
list.cpp
|
||||
main.cpp
|
||||
map.cpp
|
||||
matcher.cpp
|
||||
"${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp"
|
||||
memory.cpp
|
||||
model2expr.cpp
|
||||
model_retrieval.cpp
|
||||
mpbq.cpp
|
||||
mpf.cpp
|
||||
mpff.cpp
|
||||
mpfx.cpp
|
||||
mpq.cpp
|
||||
mpz.cpp
|
||||
nlarith_util.cpp
|
||||
nlsat.cpp
|
||||
no_overflow.cpp
|
||||
object_allocator.cpp
|
||||
old_interval.cpp
|
||||
optional.cpp
|
||||
parray.cpp
|
||||
pdr.cpp
|
||||
permutation.cpp
|
||||
polynomial.cpp
|
||||
polynomial_factorization.cpp
|
||||
polynorm.cpp
|
||||
prime_generator.cpp
|
||||
proof_checker.cpp
|
||||
qe_arith.cpp
|
||||
quant_elim.cpp
|
||||
quant_solve.cpp
|
||||
random.cpp
|
||||
rational.cpp
|
||||
rcf.cpp
|
||||
region.cpp
|
||||
sat_user_scope.cpp
|
||||
simple_parser.cpp
|
||||
simplex.cpp
|
||||
simplifier.cpp
|
||||
small_object_allocator.cpp
|
||||
smt2print_parse.cpp
|
||||
smt_context.cpp
|
||||
sorting_network.cpp
|
||||
stack.cpp
|
||||
string_buffer.cpp
|
||||
substitution.cpp
|
||||
symbol.cpp
|
||||
symbol_table.cpp
|
||||
tbv.cpp
|
||||
theory_dl.cpp
|
||||
theory_pb.cpp
|
||||
timeout.cpp
|
||||
total_order.cpp
|
||||
trigo.cpp
|
||||
udoc_relation.cpp
|
||||
uint_set.cpp
|
||||
upolynomial.cpp
|
||||
var_subst.cpp
|
||||
vector.cpp
|
||||
${z3_test_extra_object_files}
|
||||
)
|
||||
z3_add_install_tactic_rule(${z3_test_deps})
|
||||
z3_add_memory_initializer_rule(${z3_test_deps})
|
||||
z3_add_gparams_register_modules_rule(${z3_test_deps})
|
||||
target_compile_definitions(test-z3 PRIVATE ${Z3_COMPONENT_CXX_DEFINES})
|
||||
target_compile_options(test-z3 PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
|
||||
target_link_libraries(test-z3 PRIVATE ${Z3_DEPENDENT_LIBS})
|
||||
target_include_directories(shell PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS})
|
||||
set_property(TARGET test-z3 APPEND PROPERTY LINK_FLAGS ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
|
||||
z3_add_component_dependencies_to_target(test-z3 ${z3_test_expanded_deps})
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
z3_add_component(fuzzing
|
||||
NOT_LIBZ3_COMPONENT # Don't put this component inside libz3
|
||||
SOURCES
|
||||
expr_delta.cpp
|
||||
expr_rand.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
ast
|
||||
)
|
||||
|
|
@ -1,60 +0,0 @@
|
|||
if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/version.h")
|
||||
message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/version.h\""
|
||||
${z3_polluted_tree_msg}
|
||||
)
|
||||
endif()
|
||||
configure_file(version.h.in ${CMAKE_CURRENT_BINARY_DIR}/version.h @ONLY)
|
||||
|
||||
z3_add_component(util
|
||||
SOURCES
|
||||
approx_nat.cpp
|
||||
approx_set.cpp
|
||||
bit_util.cpp
|
||||
bit_vector.cpp
|
||||
cmd_context_types.cpp
|
||||
common_msgs.cpp
|
||||
cooperate.cpp
|
||||
debug.cpp
|
||||
env_params.cpp
|
||||
fixed_bit_vector.cpp
|
||||
gparams.cpp
|
||||
hash.cpp
|
||||
hwf.cpp
|
||||
inf_int_rational.cpp
|
||||
inf_rational.cpp
|
||||
inf_s_integer.cpp
|
||||
lbool.cpp
|
||||
luby.cpp
|
||||
memory_manager.cpp
|
||||
mpbq.cpp
|
||||
mpf.cpp
|
||||
mpff.cpp
|
||||
mpfx.cpp
|
||||
mpn.cpp
|
||||
mpq.cpp
|
||||
mpq_inf.cpp
|
||||
mpz.cpp
|
||||
page.cpp
|
||||
params.cpp
|
||||
permutation.cpp
|
||||
prime_generator.cpp
|
||||
rational.cpp
|
||||
region.cpp
|
||||
rlimit.cpp
|
||||
scoped_ctrl_c.cpp
|
||||
scoped_timer.cpp
|
||||
sexpr.cpp
|
||||
s_integer.cpp
|
||||
small_object_allocator.cpp
|
||||
smt2_util.cpp
|
||||
stack.cpp
|
||||
statistics.cpp
|
||||
symbol.cpp
|
||||
timeit.cpp
|
||||
timeout.cpp
|
||||
timer.cpp
|
||||
trace.cpp
|
||||
util.cpp
|
||||
warning.cpp
|
||||
z3_exception.cpp
|
||||
)
|
||||
Loading…
Add table
Add a link
Reference in a new issue