mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

[CMake] Move CMake files into their intended location so the

Browse source 
`contrib/cmake/bootstrap.py` script no longer needs to be executed.

The previous location of the CMake files was a compromise proposed
by @agurfinkel in #461. While this has served us well (allowing progress
to be made) over time limitations of this approach have appeared.

The main problem is that doing many git operations (e.g. pull, rebase)
means the CMake files don't get updated unless the user remembers to
run the script. This can lead to broken and confusing build system
behaviour.

This commit only does the file moving and necessary changes to
`.gitignore`. Other changes will be done in subsequent commits.
This commit is contained in:
Dan Liew 2017-06-12 10:21:50 +01:00
parent f0fa439c48
commit 4b517b96df
97 changed files with 0 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

261
src/CMakeLists.txt Normal file
View file

@ -0,0 +1,261 @@
################################################################################
# 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(util/lp)
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})
set_target_properties(libz3 PROPERTIES
# VERSION determines the version in the filename of the shared library.
# SOVERSION determines the value of the DT_SONAME field on ELF platforms.
# On ELF platforms the final compiled filename will be libz3.so.W.X.Y.Z
# but symlinks will be made to this file from libz3.so and also from
# libz3.so.W.X.
# This indicates that no breaking API changes will be made within a single
# minor version.
VERSION ${Z3_VERSION}
SOVERSION ${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR})
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()
# The `PRIVATE` usage requirement is specified so that when building Z3 as a
# shared library the dependent libraries are specified on the link command line
# so that if those are also shared libraries they are referenced by `libz3.so`.
target_link_libraries(libz3 PRIVATE ${Z3_DEPENDENT_LIBS})
# This is currently only for the OpenMP flags. It needs to be set
# via `target_link_libraries()` rather than `z3_append_linker_flag_list_to_target()`
# because when building the `libz3` as a static library when the target is exported
# the link dependencies need to be exported too.
foreach (flag_name ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
target_link_libraries(libz3 PRIVATE ${flag_name})
endforeach()
# 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
EXPORT Z3_EXPORTED_TARGETS
LIBRARY DESTINATION "${CMAKE_INSTALL_LIBDIR}"
ARCHIVE DESTINATION "${CMAKE_INSTALL_LIBDIR}" # On Windows this installs ``libz3.lib`` which CMake calls the "corresponding import library". Do we want this installed?
RUNTIME DESTINATION "${CMAKE_INSTALL_LIBDIR}" # For Windows. DLLs are runtime targets for CMake
PUBLIC_HEADER DESTINATION "${CMAKE_INSTALL_INCLUDEDIR}"
)
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"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
${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)
z3_append_linker_flag_list_to_target(libz3 "/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)
if (NOT BUILD_LIBZ3_SHARED)
message(FATAL_ERROR "The python bindings will not work with a static libz3. "
"You either need to disable BUILD_PYTHON_BINDINGS or enable BUILD_LIBZ3_SHARED")
endif()
add_subdirectory(api/python)
endif()
################################################################################
# .NET bindings
################################################################################
option(BUILD_DOTNET_BINDINGS "Build .NET bindings for Z3" OFF)
if (BUILD_DOTNET_BINDINGS)
if (NOT BUILD_LIBZ3_SHARED)
message(FATAL_ERROR "The .NET bindings will not work with a static libz3. "
"You either need to disable BUILD_DOTNET_BINDINGS or enable BUILD_LIBZ3_SHARED")
endif()
add_subdirectory(api/dotnet)
endif()
################################################################################
# Java bindings
################################################################################
option(BUILD_JAVA_BINDINGS "Build Java bindings for Z3" OFF)
if (BUILD_JAVA_BINDINGS)
if (NOT BUILD_LIBZ3_SHARED)
message(FATAL_ERROR "The Java bindings will not work with a static libz3. "
"You either need to disable BUILD_JAVA_BINDINGS or enable BUILD_LIBZ3_SHARED")
endif()
add_subdirectory(api/java)
endif()
# TODO: Implement support for other bindigns

20
src/ackermannization/CMakeLists.txt Normal file
View file

@ -0,0 +1,20 @@
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
)

74
src/api/CMakeLists.txt Normal file
View file

@ -0,0 +1,74 @@
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"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
# FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency
"${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
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
)

13
src/api/dll/CMakeLists.txt Normal file
View file

@ -0,0 +1,13 @@
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})

291
src/api/dotnet/CMakeLists.txt Normal file
View file

@ -0,0 +1,291 @@
find_package(DotNetToolchain REQUIRED)
# Configure AssemblyInfo.cs
set(VER_MAJOR "${Z3_VERSION_MAJOR}")
set(VER_MINOR "${Z3_VERSION_MINOR}")
set(VER_BUILD "${Z3_VERSION_PATCH}")
set(VER_REVISION "${Z3_VERSION_TWEAK}")
set(Z3_DOTNET_ASSEMBLY_INFO_FILE "${CMAKE_CURRENT_BINARY_DIR}/Properties/AssemblyInfo.cs")
configure_file("Properties/AssemblyInfo.cs.in" "${Z3_DOTNET_ASSEMBLY_INFO_FILE}" @ONLY)
# Generate Native.cs
set(Z3_DOTNET_NATIVE_FILE "${CMAKE_CURRENT_BINARY_DIR}/Native.cs")
add_custom_command(OUTPUT "${Z3_DOTNET_NATIVE_FILE}"
COMMAND "${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/update_api.py"
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"--dotnet-output-dir"
"${CMAKE_CURRENT_BINARY_DIR}"
DEPENDS
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"${CMAKE_SOURCE_DIR}/scripts/update_api.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
# FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency
"${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
COMMENT "Generating ${Z3_DOTNET_NATIVE_FILE}"
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
)
# Generate Enumerations.cs
set(Z3_DOTNET_CONST_FILE "${CMAKE_CURRENT_BINARY_DIR}/Enumerations.cs")
add_custom_command(OUTPUT "${Z3_DOTNET_CONST_FILE}"
COMMAND "${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"--dotnet-output-dir"
"${CMAKE_CURRENT_BINARY_DIR}"
DEPENDS
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
COMMENT "Generating ${Z3_DOTNET_CONST_FILE}"
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
)
set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
AlgebraicNum.cs
ApplyResult.cs
ArithExpr.cs
ArithSort.cs
ArrayExpr.cs
ArraySort.cs
AST.cs
ASTMap.cs
ASTVector.cs
BitVecExpr.cs
BitVecNum.cs
BitVecSort.cs
BoolExpr.cs
BoolSort.cs
Constructor.cs
ConstructorList.cs
Context.cs
DatatypeExpr.cs
DatatypeSort.cs
Deprecated.cs
EnumSort.cs
Expr.cs
FiniteDomainExpr.cs
FiniteDomainNum.cs
FiniteDomainSort.cs
Fixedpoint.cs
FPExpr.cs
FPNum.cs
FPRMExpr.cs
FPRMNum.cs
FPRMSort.cs
FPSort.cs
FuncDecl.cs
FuncInterp.cs
Global.cs
Goal.cs
IDecRefQueue.cs
InterpolationContext.cs
IntExpr.cs
IntNum.cs
IntSort.cs
IntSymbol.cs
ListSort.cs
Log.cs
Model.cs
Optimize.cs
ParamDescrs.cs
Params.cs
Pattern.cs
Probe.cs
Quantifier.cs
RatNum.cs
RealExpr.cs
RealSort.cs
ReExpr.cs
RelationSort.cs
ReSort.cs
SeqExpr.cs
SeqSort.cs
SetSort.cs
Solver.cs
Sort.cs
Statistics.cs
Status.cs
StringSymbol.cs
Symbol.cs
Tactic.cs
TupleSort.cs
UninterpretedSort.cs
Version.cs
Z3Exception.cs
Z3Object.cs
)
set(Z3_DOTNET_ASSEMBLY_SOURCES "")
# Make paths to source files absolute
foreach (csfile ${Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE})
list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES "${CMAKE_CURRENT_SOURCE_DIR}/${csfile}")
endforeach()
# Add generated files
list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES
"${Z3_DOTNET_CONST_FILE}"
"${Z3_DOTNET_NATIVE_FILE}"
"${Z3_DOTNET_ASSEMBLY_INFO_FILE}"
)
# ``csc.exe`` doesn't like UNIX style paths so convert them
# if necessary first to native paths.
set(Z3_DOTNET_ASSEMBLY_SOURCES_NATIVE_PATH "")
foreach (csfile_path ${Z3_DOTNET_ASSEMBLY_SOURCES})
file(TO_NATIVE_PATH "${csfile_path}" csfile_path_native)
list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES_NATIVE_PATH "${csfile_path_native}")
endforeach()
set(CSC_FLAGS "")
if (DOTNET_TOOLCHAIN_IS_WINDOWS)
# FIXME: Why use these flags?
# Note these flags have been copied from the Python build system.
list(APPEND CSC_FLAGS
"/noconfig"
"/nostdlib+"
"/reference:mscorlib.dll"
)
# FIXME: This flag only works when the working directory of csc.exe is
# the directory containing the ``libz3`` target. I can't get this to work
# correctly with multi-configuration generators (i.e. Visual Studio) so
# just don't set the flag for now.
#list(APPEND CSC_FLAGS "/linkresource:$<TARGET_FILE_NAME:libz3>")
elseif (DOTNET_TOOLCHAIN_IS_MONO)
# We need to give the assembly a strong name so that it can be installed
# into the GAC.
list(APPEND CSC_FLAGS
"/keyfile:${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.snk"
)
else()
message(FATAL_ERROR "Unknown .NET toolchain")
endif()
# Common flags
list(APPEND CSC_FLAGS
"/unsafe+"
"/nowarn:1701,1702"
"/errorreport:prompt"
"/warn:4"
"/reference:System.Core.dll"
"/reference:System.dll"
"/reference:System.Numerics.dll"
"/filealign:512" # Why?
"/target:library"
)
# Set the build type flags. The build type for the assembly roughly corresponds
# with the native code build type.
list(APPEND CSC_FLAGS
# Debug flags, expands to nothing if we aren't doing a debug build
"$<$<CONFIG:Debug>:/debug+>"
"$<$<CONFIG:Debug>:/debug:full>"
"$<$<CONFIG:Debug>:/optimize->"
# This has to be quoted otherwise the ``;`` is interpreted as a command separator
"$<$<CONFIG:Debug>:\"/define:DEBUG$<SEMICOLON>TRACE\">"
# Release flags, expands to nothing if we are doing a debug build
"$<$<NOT:$<CONFIG:Debug>>:/optimize+>"
)
# Mono's gacutil crashes when trying to install an assembly if we set the
# platform in some cases, so only set it on Windows. This bug has been
# reported at https://bugzilla.xamarin.com/show_bug.cgi?id=39955 . However mono
# ignores the platform of an assembly when running it (
# http://lists.ximian.com/pipermail/mono-devel-list/2015-November/043370.html )
# so this shouldn't matter in practice.
if (DOTNET_TOOLCHAIN_IS_WINDOWS)
# Set platform for assembly
if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64")
list(APPEND CSC_FLAGS "/platform:x64")
elseif ("${TARGET_ARCHITECTURE}" STREQUAL "i686")
list(APPEND CSC_FLAGS "/platform:x86")
endif()
endif()
# FIXME: Ideally we should emit files into a configuration specific directory
# when using multi-configuration generators so that the files generated by each
# configuration don't clobber each other. Unfortunately the ``get_property()``
# command only works correctly for single configuration generators so we can't
# use it. We also can't use ``$<TARGET_FILE_DIR:libz3>`` because the ``OUTPUT``
# argument to ``add_custom_commands()`` won't accept it.
# See http://public.kitware.com/pipermail/cmake/2016-March/063101.html
#
# For now just output file to the root binary directory like the Python build
# system does and emit a warning when appropriate.
if (DEFINED CMAKE_CONFIGURATION_TYPES)
# Multi-configuration build (e.g. Visual Studio and Xcode).
message(WARNING "You are using a multi-configuration generator. The build rules for"
" the \".NET\" bindings currently do not emit files per configuration so previously"
" generated files for other configurations will be overwritten.")
endif()
set(Z3_DOTNET_ASSEMBLY_OUTPUT_DIR "${CMAKE_BINARY_DIR}")
set(Z3_DOTNET_ASSEMBLY_NAME "Microsoft.Z3.dll")
set(Z3_DOTNET_ASSEMBLY_DLL "${Z3_DOTNET_ASSEMBLY_OUTPUT_DIR}/${Z3_DOTNET_ASSEMBLY_NAME}")
# csc.exe doesn't work with UNIX style paths so convert to native path
file(TO_NATIVE_PATH "${Z3_DOTNET_ASSEMBLY_DLL}" Z3_DOTNET_ASSEMBLY_DLL_NATIVE_PATH)
set(Z3_DOTNET_ASSEMBLY_DLL_DOC "${Z3_DOTNET_ASSEMBLY_OUTPUT_DIR}/Microsoft.Z3.xml")
file(TO_NATIVE_PATH "${Z3_DOTNET_ASSEMBLY_DLL_DOC}" Z3_DOTNET_ASSEMBLY_DLL_DOC_NATIVE_PATH)
add_custom_command(OUTPUT "${Z3_DOTNET_ASSEMBLY_DLL}" "${Z3_DOTNET_ASSEMBLY_DLL_DOC}"
COMMAND
"${DOTNET_CSC_EXECUTABLE}"
${CSC_FLAGS}
"/out:${Z3_DOTNET_ASSEMBLY_DLL_NATIVE_PATH}"
"/doc:${Z3_DOTNET_ASSEMBLY_DLL_DOC_NATIVE_PATH}"
${Z3_DOTNET_ASSEMBLY_SOURCES_NATIVE_PATH}
DEPENDS
${Z3_DOTNET_ASSEMBLY_SOURCES}
libz3
WORKING_DIRECTORY "${Z3_DOTNET_ASSEMBLY_OUTPUT_DIR}"
COMMENT "Building \"${Z3_DOTNET_ASSEMBLY_DLL}\""
)
# Convenient top-level target
add_custom_target(build_z3_dotnet_bindings
ALL
DEPENDS
"${Z3_DOTNET_ASSEMBLY_DLL}"
)
###############################################################################
# Install
###############################################################################
option(INSTALL_DOTNET_BINDINGS "Install .NET bindings when invoking install target" ON)
set(GAC_PKG_NAME "Microsoft.Z3.Sharp")
set(PREFIX "${CMAKE_INSTALL_PREFIX}")
set(VERSION "${Z3_VERSION}")
set(Z3_DOTNET_PKGCONFIG_FILE "${CMAKE_CURRENT_BINARY_DIR}/Microsoft.Z3.Sharp.pc")
configure_file("Microsoft.Z3.Sharp.pc.in" "${Z3_DOTNET_PKGCONFIG_FILE}" @ONLY)
if (DOTNET_TOOLCHAIN_IS_MONO)
message(STATUS "Emitting install rules for .NET bindings")
# Install pkgconfig file for the assembly. This is needed by Monodevelop
# to find the assembly
install(FILES "${Z3_DOTNET_PKGCONFIG_FILE}" DESTINATION "${CMAKE_INSTALL_PKGCONFIGDIR}")
# Configure the install and uninstall scripts.
# Note: If multi-configuration generator support is ever fixed then these
# scripts will be broken.
configure_file(cmake_install_gac.cmake.in cmake_install_gac.cmake @ONLY)
configure_file(cmake_uninstall_gac.cmake.in cmake_uninstall_gac.cmake @ONLY)
# Tell CMake to Invoke a script to install assembly to the GAC during install
install(SCRIPT "${CMAKE_CURRENT_BINARY_DIR}/cmake_install_gac.cmake")
# Add custom target to uninstall the assembly from the GAC
add_custom_target(remove_dotnet_dll_from_gac
COMMAND "${CMAKE_COMMAND}" "-P" "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall_gac.cmake"
COMMENT "Uninstalling ${Z3_DOTNET_ASSEMBLY_NAME} from the GAC"
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
)
add_dependencies(uninstall remove_dotnet_dll_from_gac)
elseif(DOTNET_TOOLCHAIN_IS_WINDOWS)
# Don't install Z3_DOTNET_ASSEMBLY_DLL into the gac. Instead just copy into
# installation directory.
install(FILES "${Z3_DOTNET_ASSEMBLY_DLL}" DESTINATION "${CMAKE_INSTALL_LIBDIR}")
install(FILES "${Z3_DOTNET_ASSEMBLY_DLL_DOC}" DESTINATION "${CMAKE_INSTALL_LIBDIR}")
else()
message(FATAL_ERROR "Unknown .NET toolchain")
endif()

18
src/api/dotnet/cmake_install_gac.cmake.in Normal file
View file

@ -0,0 +1,18 @@
# Install assembly to the GAC
set(GAC_ROOT "$ENV{DESTDIR}@CMAKE_INSTALL_FULL_LIBDIR@")
execute_process(COMMAND
"@DOTNET_GACUTIL_EXECUTABLE@"
"-i"
"@Z3_DOTNET_ASSEMBLY_DLL@"
"-f"
"-package" "@GAC_PKG_NAME@"
"-root" "${GAC_ROOT}"
WORKING_DIRECTORY "@CMAKE_CURRENT_BINARY_DIR@"
RESULT_VARIABLE gacutil_exit_code
)
if ("${gacutil_exit_code}" EQUAL 0)
message(STATUS "Installed \"@Z3_DOTNET_ASSEMBLY_DLL@\" to the GAC")
else()
message(FATAL_ERROR "Failed to install \"@Z3_DOTNET_ASSEMBLY_DLL@\" to the GAC")
endif()

20
src/api/dotnet/cmake_uninstall_gac.cmake.in Normal file
View file

@ -0,0 +1,20 @@
# Uninstall assembly from the GAC
set(GAC_ROOT "$ENV{DESTDIR}@CMAKE_INSTALL_FULL_LIBDIR@")
execute_process(COMMAND
"@DOTNET_GACUTIL_EXECUTABLE@"
# Note ``-us`` takes assembly file name rather than
# ``-u`` which takes an assembly display name
"-us"
"@Z3_DOTNET_ASSEMBLY_NAME@"
"-f"
"-package" "@GAC_PKG_NAME@"
"-root" "${GAC_ROOT}"
WORKING_DIRECTORY "@CMAKE_CURRENT_BINARY_DIR@"
RESULT_VARIABLE gacutil_exit_code
)
if ("${gacutil_exit_code}" EQUAL 0)
message(STATUS "Uninstalled \"@Z3_DOTNET_ASSEMBLY_NAME@\" from the GAC")
else()
message(FATAL_ERROR "Failed to uninstall \"@Z3_DOTNET_ASSEMBLY_NAME@\" from the GAC")
endif()

236
src/api/java/CMakeLists.txt Normal file
View file

@ -0,0 +1,236 @@
find_package(Java REQUIRED)
find_package(JNI REQUIRED)
include(UseJava)
# Sanity check for dirty source tree
foreach (file_name "enumerations" "Native.cpp" "Native.java")
if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/${file_name}")
message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/${file_name}\""
${z3_polluted_tree_msg})
endif()
endforeach()
set(Z3_JAVA_PACKAGE_NAME "com.microsoft.z3")
# Rule to generate ``Native.java`` and ``Native.cpp``
set(Z3_JAVA_NATIVE_JAVA "${CMAKE_CURRENT_BINARY_DIR}/Native.java")
set(Z3_JAVA_NATIVE_CPP "${CMAKE_CURRENT_BINARY_DIR}/Native.cpp")
add_custom_command(OUTPUT "${Z3_JAVA_NATIVE_JAVA}" "${Z3_JAVA_NATIVE_CPP}"
COMMAND "${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/update_api.py"
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"--java-output-dir"
"${CMAKE_CURRENT_BINARY_DIR}"
"--java-package-name"
${Z3_JAVA_PACKAGE_NAME}
DEPENDS
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"${CMAKE_SOURCE_DIR}/scripts/update_api.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
# FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency
"${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
COMMENT "Generating \"${Z3_JAVA_NATIVE_JAVA}\" and \"${Z3_JAVA_NATIVE_CPP}\""
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
)
# Add rule to build native code that provides a bridge between
# ``Native.java`` and libz3's interfac3.
add_library(z3java SHARED ${Z3_JAVA_NATIVE_CPP})
target_link_libraries(z3java PRIVATE libz3)
# FIXME:
# Not sure if using all the flags used by the Z3 components is really necessary
# here. At the bare minimum setting _AMD64_ depending on the target is
# necessary but seeing as the Python build system uses all the flags used for building
# Z3's components to build ``Native.cpp`` lets do the same for now.
target_compile_options(z3java PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
target_compile_definitions(z3java PRIVATE ${Z3_COMPONENT_CXX_DEFINES})
target_include_directories(z3java PRIVATE
"${CMAKE_SOURCE_DIR}/src/api"
"${CMAKE_BINARY_DIR}/src/api"
${JNI_INCLUDE_DIRS}
)
# FIXME: Should this library have SONAME and VERSION set?
# This prevents CMake from automatically defining ``z3java_EXPORTS``
set_property(TARGET z3java PROPERTY DEFINE_SYMBOL "")
# Rule to generate the ``com.microsoft.z3.enumerations`` package
# FIXME: This list of files is fragile
set(Z3_JAVA_ENUMERATION_PACKAGE_FILES
Z3_ast_kind.java
Z3_ast_print_mode.java
Z3_decl_kind.java
Z3_error_code.java
Z3_goal_prec.java
Z3_lbool.java
Z3_param_kind.java
Z3_parameter_kind.java
Z3_sort_kind.java
Z3_symbol_kind.java
)
set(Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH "")
foreach (enum_file ${Z3_JAVA_ENUMERATION_PACKAGE_FILES})
list(APPEND Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH
"${CMAKE_CURRENT_BINARY_DIR}/enumerations/${enum_file}"
)
endforeach()
add_custom_command(OUTPUT ${Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH}
COMMAND "${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"--java-output-dir"
"${CMAKE_CURRENT_BINARY_DIR}"
"--java-package-name"
${Z3_JAVA_PACKAGE_NAME}
DEPENDS
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
COMMENT "Generating ${Z3_JAVA_PACKAGE_NAME}.enumerations package"
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
)
set(Z3_JAVA_JAR_SOURCE_FILES
AlgebraicNum.java
ApplyResultDecRefQueue.java
ApplyResult.java
ArithExpr.java
ArithSort.java
ArrayExpr.java
ArraySort.java
ASTDecRefQueue.java
AST.java
AstMapDecRefQueue.java
ASTMap.java
AstVectorDecRefQueue.java
ASTVector.java
BitVecExpr.java
BitVecNum.java
BitVecSort.java
BoolExpr.java
BoolSort.java
ConstructorDecRefQueue.java
Constructor.java
ConstructorListDecRefQueue.java
ConstructorList.java
Context.java
DatatypeExpr.java
DatatypeSort.java
EnumSort.java
Expr.java
FiniteDomainExpr.java
FiniteDomainNum.java
FiniteDomainSort.java
FixedpointDecRefQueue.java
Fixedpoint.java
FPExpr.java
FPNum.java
FPRMExpr.java
FPRMNum.java
FPRMSort.java
FPSort.java
FuncDecl.java
FuncInterpDecRefQueue.java
FuncInterpEntryDecRefQueue.java
FuncInterp.java
Global.java
GoalDecRefQueue.java
Goal.java
IDecRefQueue.java
InterpolationContext.java
IntExpr.java
IntNum.java
IntSort.java
IntSymbol.java
ListSort.java
Log.java
ModelDecRefQueue.java
Model.java
OptimizeDecRefQueue.java
Optimize.java
ParamDescrsDecRefQueue.java
ParamDescrs.java
ParamsDecRefQueue.java
Params.java
Pattern.java
ProbeDecRefQueue.java
Probe.java
Quantifier.java
RatNum.java
RealExpr.java
RealSort.java
ReExpr.java
RelationSort.java
ReSort.java
SeqExpr.java
SeqSort.java
SetSort.java
SolverDecRefQueue.java
Solver.java
Sort.java
StatisticsDecRefQueue.java
Statistics.java
Status.java
StringSymbol.java
Symbol.java
TacticDecRefQueue.java
Tactic.java
TupleSort.java
UninterpretedSort.java
Version.java
Z3Exception.java
Z3Object.java
)
set(Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH "")
foreach (java_src_file ${Z3_JAVA_JAR_SOURCE_FILES})
list(APPEND Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH "${CMAKE_CURRENT_SOURCE_DIR}/${java_src_file}")
endforeach()
# Add generated files to list
list(APPEND Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH
${Z3_JAVA_NATIVE_JAVA}
${Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH}
)
# Convenient top-level target
add_custom_target(build_z3_java_bindings
ALL
DEPENDS
z3java
z3JavaJar
)
# Rule to build ``com.microsoft.z3.jar``
# TODO: Should we set ``CMAKE_JNI_TARGET`` to ``TRUE``?
add_jar(z3JavaJar
SOURCES ${Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH}
OUTPUT_NAME ${Z3_JAVA_PACKAGE_NAME}
OUTPUT_DIR "${CMAKE_BINARY_DIR}"
VERSION "${Z3_VERSION}"
)
###############################################################################
# Install
###############################################################################
option(INSTALL_JAVA_BINDINGS "Install Java bindings when invoking install target" ON)
if (INSTALL_JAVA_BINDINGS)
# Provide cache variables for the install locations that the user can change.
# This defaults to ``/usr/local/java`` which seems to be the location for ``.jar``
# files on Linux distributions
set(Z3_JAVA_JAR_INSTALLDIR
"${CMAKE_INSTALL_DATAROOTDIR}/java"
CACHE
PATH
"Directory to install Z3 Java jar file relative to install prefix"
)
# FIXME: I don't think this the right installation location
set(Z3_JAVA_JNI_LIB_INSTALLDIR
"${CMAKE_INSTALL_LIBDIR}"
CACHE
PATH
"Directory to install Z3 Java JNI bridge library relative to install prefix"
)
install(TARGETS z3java DESTINATION "${Z3_JAVA_JNI_LIB_INSTALLDIR}")
# Note: Don't use ``DESTINATION`` here as the version of ``UseJava.cmake`` shipped
# with CMake 2.8.12.2 handles that incorrectly.
install_jar(z3JavaJar "${Z3_JAVA_JAR_INSTALLDIR}")
endif()

143
src/api/python/CMakeLists.txt Normal file
View file

@ -0,0 +1,143 @@
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/__init__.py
z3/z3.py
z3/z3num.py
z3/z3poly.py
z3/z3printer.py
z3/z3rcf.py
z3test.py
z3/z3types.py
z3/z3util.py
)
set(z3py_bindings_build_dest "${CMAKE_BINARY_DIR}/python")
file(MAKE_DIRECTORY "${z3py_bindings_build_dest}")
file(MAKE_DIRECTORY "${z3py_bindings_build_dest}/z3")
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}/${z3py_file}"
DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/${z3py_file}"
COMMENT "Copying \"${z3py_file}\" to ${z3py_bindings_build_dest}/${z3py_file}"
)
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}/z3/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"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
# FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency
"${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}/z3/z3core.py")
# Generate z3consts.py
add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/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"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
COMMENT "Generating z3consts.py"
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
)
list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3/z3consts.py")
if (UNIX)
set(LINK_COMMAND "create_symlink")
else()
set(LINK_COMMAND "copy")
endif()
# Link libz3 into the python directory so bindings work out of the box
add_custom_command(OUTPUT "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
COMMAND "${CMAKE_COMMAND}" "-E" "${LINK_COMMAND}"
"${CMAKE_BINARY_DIR}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
"${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
DEPENDS libz3
COMMENT "Linking libz3 into python directory"
)
# Convenient top-level target
add_custom_target(build_z3_python_bindings
ALL
DEPENDS
${build_z3_python_bindings_target_depends}
"${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
)
###############################################################################
# Install
###############################################################################
option(INSTALL_PYTHON_BINDINGS "Install Python bindings when invoking install target" ON)
if (INSTALL_PYTHON_BINDINGS)
message(STATUS "Emitting rules to install Z3 python bindings")
# Try to guess the installation path for the bindings
if (NOT DEFINED CMAKE_INSTALL_PYTHON_PKG_DIR)
message(STATUS "CMAKE_INSTALL_PYTHON_PKG_DIR not set. Trying to guess")
execute_process(
COMMAND "${PYTHON_EXECUTABLE}" "-c"
"import distutils.sysconfig; print(distutils.sysconfig.get_python_lib())"
RESULT_VARIABLE exit_code
OUTPUT_VARIABLE CMAKE_INSTALL_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: \"${CMAKE_INSTALL_PYTHON_PKG_DIR}\"")
# Set a cache variable that the user can modify if needed
set(CMAKE_INSTALL_PYTHON_PKG_DIR
"${CMAKE_INSTALL_PYTHON_PKG_DIR}"
CACHE PATH
"Path to install python bindings. This can be relative or absolute.")
mark_as_advanced(CMAKE_INSTALL_PYTHON_PKG_DIR)
else()
message(STATUS "CMAKE_INSTALL_PYTHON_PKG_DIR already set (\"${CMAKE_INSTALL_PYTHON_PKG_DIR}\")"
". Not trying to guess.")
endif()
# Check if path exists under the install prefix if it is absolute. If the
# path is relative it will be installed under the install prefix so there
# if nothing to check
if (IS_ABSOLUTE "${CMAKE_INSTALL_PYTHON_PKG_DIR}")
string(FIND "${CMAKE_INSTALL_PYTHON_PKG_DIR}" "${CMAKE_INSTALL_PREFIX}" position)
if (NOT ("${position}" EQUAL 0))
message(WARNING "The directory to install the python bindings \"${CMAKE_INSTALL_PYTHON_PKG_DIR}\" "
"is not under the install prefix \"${CMAKE_INSTALL_PREFIX}\"."
" Running the install target may lead to a broken installation. "
"To change the install directory modify the CMAKE_INSTALL_PYTHON_PKG_DIR cache variable."
)
endif()
endif()
# Using DESTDIR still seems to work even if we use an absolute path
message(STATUS "Python bindings will be installed to \"${CMAKE_INSTALL_PYTHON_PKG_DIR}\"")
install(FILES ${build_z3_python_bindings_target_depends}
DESTINATION "${CMAKE_INSTALL_PYTHON_PKG_DIR}/z3"
)
else()
message(STATUS "Not emitting rules to install Z3 python bindings")
endif()

48
src/ast/CMakeLists.txt Normal file
View file

@ -0,0 +1,48 @@
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
)

13
src/ast/fpa/CMakeLists.txt Normal file
View file

@ -0,0 +1,13 @@
z3_add_component(fpa
SOURCES
bv2fpa_converter.cpp
fpa2bv_converter.cpp
fpa2bv_rewriter.cpp
COMPONENT_DEPENDENCIES
ast
simplifier
model
util
PYG_FILES
fpa2bv_rewriter_params.pyg
)

9
src/ast/macros/CMakeLists.txt Normal file
View file

@ -0,0 +1,9 @@
z3_add_component(macros
SOURCES
macro_finder.cpp
macro_manager.cpp
macro_util.cpp
quasi_macros.cpp
COMPONENT_DEPENDENCIES
simplifier
)

11
src/ast/normal_forms/CMakeLists.txt Normal file
View file

@ -0,0 +1,11 @@
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
)

36
src/ast/pattern/CMakeLists.txt Normal file
View file

@ -0,0 +1,36 @@
# 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"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
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
)

6
src/ast/proof_checker/CMakeLists.txt Normal file
View file

@ -0,0 +1,6 @@
z3_add_component(proof_checker
SOURCES
proof_checker.cpp
COMPONENT_DEPENDENCIES
rewriter
)

41
src/ast/rewriter/CMakeLists.txt Normal file
View file

@ -0,0 +1,41 @@
z3_add_component(rewriter
SOURCES
arith_rewriter.cpp
array_rewriter.cpp
ast_counter.cpp
bool_rewriter.cpp
bv_bounds.cpp
bv_rewriter.cpp
datatype_rewriter.cpp
der.cpp
distribute_forall.cpp
dl_rewriter.cpp
enum2bv_rewriter.cpp
expr_replacer.cpp
expr_safe_replace.cpp
factor_rewriter.cpp
fpa_rewriter.cpp
label_rewriter.cpp
mk_simplified_app.cpp
pb_rewriter.cpp
pb2bv_rewriter.cpp
quant_hoist.cpp
rewriter.cpp
seq_rewriter.cpp
th_rewriter.cpp
var_subst.cpp
bv_trailing.cpp
mk_extract_proc.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
)

8
src/ast/rewriter/bit_blaster/CMakeLists.txt Normal file
View file

@ -0,0 +1,8 @@
z3_add_component(bit_blaster
SOURCES
bit_blaster.cpp
bit_blaster_rewriter.cpp
COMPONENT_DEPENDENCIES
rewriter
simplifier
)

29
src/ast/simplifier/CMakeLists.txt Normal file
View file

@ -0,0 +1,29 @@
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
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
)

10
src/ast/substitution/CMakeLists.txt Normal file
View file

@ -0,0 +1,10 @@
z3_add_component(substitution
SOURCES
matcher.cpp
substitution.cpp
substitution_tree.cpp
unifier.cpp
COMPONENT_DEPENDENCIES
ast
rewriter
)

21
src/cmd_context/CMakeLists.txt Normal file
View file

@ -0,0 +1,21 @@
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
)

10
src/cmd_context/extra_cmds/CMakeLists.txt Normal file
View file

@ -0,0 +1,10 @@
z3_add_component(extra_cmds
SOURCES
dbg_cmds.cpp
polynomial_cmds.cpp
subpaving_cmds.cpp
COMPONENT_DEPENDENCIES
arith_tactics
cmd_context
subpaving_tactic
)

11
src/duality/CMakeLists.txt Normal file
View file

@ -0,0 +1,11 @@
z3_add_component(duality
SOURCES
duality_profiling.cpp
duality_rpfp.cpp
duality_solver.cpp
duality_wrapper.cpp
COMPONENT_DEPENDENCIES
interp
qe
smt
)

18
src/interp/CMakeLists.txt Normal file
View file

@ -0,0 +1,18 @@
z3_add_component(interp
SOURCES
iz3base.cpp
iz3checker.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
)

6
src/math/automata/CMakeLists.txt Normal file
View file

@ -0,0 +1,6 @@
z3_add_component(automata
SOURCES
automaton.cpp
COMPONENT_DEPENDENCIES
util
)

6
src/math/euclid/CMakeLists.txt Normal file
View file

@ -0,0 +1,6 @@
z3_add_component(euclid
SOURCES
euclidean_solver.cpp
COMPONENT_DEPENDENCIES
util
)

6
src/math/grobner/CMakeLists.txt Normal file
View file

@ -0,0 +1,6 @@
z3_add_component(grobner
SOURCES
grobner.cpp
COMPONENT_DEPENDENCIES
ast
)

6
src/math/hilbert/CMakeLists.txt Normal file
View file

@ -0,0 +1,6 @@
z3_add_component(hilbert
SOURCES
hilbert_basis.cpp
COMPONENT_DEPENDENCIES
util
)

6
src/math/interval/CMakeLists.txt Normal file
View file

@ -0,0 +1,6 @@
z3_add_component(interval
SOURCES
interval_mpq.cpp
COMPONENT_DEPENDENCIES
util
)

15
src/math/polynomial/CMakeLists.txt Normal file
View file

@ -0,0 +1,15 @@
z3_add_component(polynomial
SOURCES
algebraic_numbers.cpp
polynomial_cache.cpp
polynomial.cpp
rpolynomial.cpp
sexpr2upolynomial.cpp
upolynomial.cpp
upolynomial_factorization.cpp
COMPONENT_DEPENDENCIES
util
PYG_FILES
algebraic_params.pyg
)

9
src/math/realclosure/CMakeLists.txt Normal file
View file

@ -0,0 +1,9 @@
z3_add_component(realclosure
SOURCES
mpz_matrix.cpp
realclosure.cpp
COMPONENT_DEPENDENCIES
interval
PYG_FILES
rcf_params.pyg
)

7
src/math/simplex/CMakeLists.txt Normal file
View file

@ -0,0 +1,7 @@
z3_add_component(simplex
SOURCES
simplex.cpp
model_based_opt.cpp
COMPONENT_DEPENDENCIES
util
)

11
src/math/subpaving/CMakeLists.txt Normal file
View file

@ -0,0 +1,11 @@
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
)

8
src/math/subpaving/tactic/CMakeLists.txt Normal file
View file

@ -0,0 +1,8 @@
z3_add_component(subpaving_tactic
SOURCES
expr2subpaving.cpp
subpaving_tactic.cpp
COMPONENT_DEPENDENCIES
core_tactics
subpaving
)

18
src/model/CMakeLists.txt Normal file
View file

@ -0,0 +1,18 @@
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
)

23
src/muz/base/CMakeLists.txt Normal file
View file

@ -0,0 +1,23 @@
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
)

7
src/muz/bmc/CMakeLists.txt Normal file
View file

@ -0,0 +1,7 @@
z3_add_component(bmc
SOURCES
dl_bmc_engine.cpp
COMPONENT_DEPENDENCIES
muz
transforms
)

7
src/muz/clp/CMakeLists.txt Normal file
View file

@ -0,0 +1,7 @@
z3_add_component(clp
SOURCES
clp_context.cpp
COMPONENT_DEPENDENCIES
muz
transforms
)

6
src/muz/dataflow/CMakeLists.txt Normal file
View file

@ -0,0 +1,6 @@
z3_add_component(dataflow
SOURCES
dataflow.cpp
COMPONENT_DEPENDENCIES
muz
)

8
src/muz/ddnf/CMakeLists.txt Normal file
View file

@ -0,0 +1,8 @@
z3_add_component(ddnf
SOURCES
ddnf.cpp
COMPONENT_DEPENDENCIES
muz
rel
transforms
)

8
src/muz/duality/CMakeLists.txt Normal file
View file

@ -0,0 +1,8 @@
z3_add_component(duality_intf
SOURCES
duality_dl_interface.cpp
COMPONENT_DEPENDENCIES
duality
muz
transforms
)

16
src/muz/fp/CMakeLists.txt Normal file
View file

@ -0,0 +1,16 @@
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
)

20
src/muz/pdr/CMakeLists.txt Normal file
View file

@ -0,0 +1,20 @@
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
)

31
src/muz/rel/CMakeLists.txt Normal file
View file

@ -0,0 +1,31 @@
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_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
)

7
src/muz/tab/CMakeLists.txt Normal file
View file

@ -0,0 +1,7 @@
z3_add_component(tab
SOURCES
tab_context.cpp
COMPONENT_DEPENDENCIES
muz
transforms
)

28
src/muz/transforms/CMakeLists.txt Normal file
View file

@ -0,0 +1,28 @@
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
)

14
src/nlsat/CMakeLists.txt Normal file
View file

@ -0,0 +1,14 @@
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
)

10
src/nlsat/tactic/CMakeLists.txt Normal file
View file

@ -0,0 +1,10 @@
z3_add_component(nlsat_tactic
SOURCES
goal2nlsat.cpp
nlsat_tactic.cpp
qfnra_nlsat_tactic.cpp
COMPONENT_DEPENDENCIES
arith_tactics
nlsat
sat_tactic
)

21
src/opt/CMakeLists.txt Normal file
View file

@ -0,0 +1,21 @@
z3_add_component(opt
SOURCES
maxres.cpp
maxsmt.cpp
mss.cpp
opt_cmds.cpp
opt_context.cpp
opt_pareto.cpp
optsmt.cpp
opt_solver.cpp
pb_sls.cpp
sortmax.cpp
wmax.cpp
COMPONENT_DEPENDENCIES
sat_solver
sls_tactic
smt
smtlogic_tactics
PYG_FILES
opt_params.pyg
)

8
src/parsers/smt/CMakeLists.txt Normal file
View file

@ -0,0 +1,8 @@
z3_add_component(smtparser
SOURCES
smtlib.cpp
smtlib_solver.cpp
smtparser.cpp
COMPONENT_DEPENDENCIES
portfolio
)

8
src/parsers/smt2/CMakeLists.txt Normal file
View file

@ -0,0 +1,8 @@
z3_add_component(smt2parser
SOURCES
smt2parser.cpp
smt2scanner.cpp
COMPONENT_DEPENDENCIES
cmd_context
parser_util
)

11
src/parsers/util/CMakeLists.txt Normal file
View file

@ -0,0 +1,11 @@
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
)

28
src/qe/CMakeLists.txt Normal file
View file

@ -0,0 +1,28 @@
z3_add_component(qe
SOURCES
nlarith_util.cpp
nlqsat.cpp
qe_arith.cpp
qe_arith_plugin.cpp
qe_array_plugin.cpp
qe_arrays.cpp
qe_bool_plugin.cpp
qe_bv_plugin.cpp
qe_cmd.cpp
qe.cpp
qe_datatype_plugin.cpp
qe_datatypes.cpp
qe_dl_plugin.cpp
qe_lite.cpp
qe_mbp.cpp
qe_sat_tactic.cpp
qe_tactic.cpp
qsat.cpp
vsubst_tactic.cpp
COMPONENT_DEPENDENCIES
nlsat_tactic
nlsat
sat
smt
tactic
)

28
src/sat/CMakeLists.txt Normal file
View file

@ -0,0 +1,28 @@
z3_add_component(sat
SOURCES
dimacs.cpp
sat_asymm_branch.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_par.cpp
sat_probing.cpp
sat_scc.cpp
sat_simplifier.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
)

11
src/sat/sat_solver/CMakeLists.txt Normal file
View file

@ -0,0 +1,11 @@
z3_add_component(sat_solver
SOURCES
inc_sat_solver.cpp
COMPONENT_DEPENDENCIES
aig_tactic
arith_tactics
bv_tactics
core_tactics
sat_tactic
solver
)

9
src/sat/tactic/CMakeLists.txt Normal file
View file

@ -0,0 +1,9 @@
z3_add_component(sat_tactic
SOURCES
atom2bool_var.cpp
goal2sat.cpp
sat_tactic.cpp
COMPONENT_DEPENDENCIES
sat
tactic
)

48
src/shell/CMakeLists.txt Normal file
View file

@ -0,0 +1,48 @@
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
lp_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})
z3_append_linker_flag_list_to_target(shell ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
install(TARGETS shell
RUNTIME DESTINATION "${CMAKE_INSTALL_BINDIR}"
)

82
src/smt/CMakeLists.txt Normal file
View file

@ -0,0 +1,82 @@
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_consequences.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
smt2_extra_cmds.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_lra.cpp
theory_opt.cpp
theory_pb.cpp
theory_seq.cpp
theory_str.cpp
theory_utvpi.cpp
theory_wmaxsat.cpp
uses_theory.cpp
watch_list.cpp
COMPONENT_DEPENDENCIES
bit_blaster
cmd_context
euclid
fpa
grobner
lp
macros
normal_forms
parser_util
pattern
proof_checker
proto_model
simplex
substitution
)

19
src/smt/params/CMakeLists.txt Normal file
View file

@ -0,0 +1,19 @@
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
theory_str_params.cpp
COMPONENT_DEPENDENCIES
ast
bit_blaster
pattern
simplifier
PYG_FILES
smt_params_helper.pyg
)

13
src/smt/proto_model/CMakeLists.txt Normal file
View file

@ -0,0 +1,13 @@
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
)

8
src/smt/tactic/CMakeLists.txt Normal file
View file

@ -0,0 +1,8 @@
z3_add_component(smt_tactic
SOURCES
ctx_solver_simplify_tactic.cpp
smt_tactic.cpp
unit_subsumption_tactic.cpp
COMPONENT_DEPENDENCIES
smt
)

16
src/solver/CMakeLists.txt Normal file
View file

@ -0,0 +1,16 @@
z3_add_component(solver
SOURCES
check_sat_result.cpp
combined_solver.cpp
mus.cpp
smt_logics.cpp
solver.cpp
solver_na2as.cpp
solver2tactic.cpp
tactic2solver.cpp
COMPONENT_DEPENDENCIES
model
tactic
PYG_FILES
combined_solver_params.pyg
)

21
src/tactic/CMakeLists.txt Normal file
View file

@ -0,0 +1,21 @@
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
sine_filter.cpp
tactical.cpp
tactic.cpp
COMPONENT_DEPENDENCIES
ast
model
)

7
src/tactic/aig/CMakeLists.txt Normal file
View file

@ -0,0 +1,7 @@
z3_add_component(aig_tactic
SOURCES
aig.cpp
aig_tactic.cpp
COMPONENT_DEPENDENCIES
tactic
)

31
src/tactic/arith/CMakeLists.txt Normal file
View file

@ -0,0 +1,31 @@
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
)

18
src/tactic/bv/CMakeLists.txt Normal file
View file

@ -0,0 +1,18 @@
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_bound_chk_tactic.cpp
bv_bounds_tactic.cpp
bv_size_reduction_tactic.cpp
dt2bv_tactic.cpp
elim_small_bv_tactic.cpp
max_bv_sharing_tactic.cpp
COMPONENT_DEPENDENCIES
bit_blaster
core_tactics
tactic
)

27
src/tactic/core/CMakeLists.txt Normal file
View file

@ -0,0 +1,27 @@
z3_add_component(core_tactics
SOURCES
blast_term_ite_tactic.cpp
cofactor_elim_term_ite.cpp
cofactor_term_ite_tactic.cpp
collect_statistics_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
collect_occs.cpp
COMPONENT_DEPENDENCIES
normal_forms
tactic
)

14
src/tactic/fpa/CMakeLists.txt Normal file
View file

@ -0,0 +1,14 @@
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
)

7
src/tactic/nlsat_smt/CMakeLists.txt Normal file
View file

@ -0,0 +1,7 @@
z3_add_component(nlsat_smt_tactic
SOURCES
nl_purify_tactic.cpp
COMPONENT_DEPENDENCIES
nlsat_tactic
smt_tactic
)

19
src/tactic/portfolio/CMakeLists.txt Normal file
View file

@ -0,0 +1,19 @@
z3_add_component(portfolio
SOURCES
default_tactic.cpp
enum2bv_solver.cpp
pb2bv_solver.cpp
bounded_int2bv_solver.cpp
fd_solver.cpp
smt_strategic_solver.cpp
COMPONENT_DEPENDENCIES
aig_tactic
fp
fpa_tactics
qe
sat_solver
sls_tactic
smtlogic_tactics
subpaving_tactic
ufbv_tactic
)

13
src/tactic/sls/CMakeLists.txt Normal file
View file

@ -0,0 +1,13 @@
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
)

31
src/tactic/smtlogics/CMakeLists.txt Normal file
View file

@ -0,0 +1,31 @@
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
)

14
src/tactic/ufbv/CMakeLists.txt Normal file
View file

@ -0,0 +1,14 @@
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
)

134
src/test/CMakeLists.txt Normal file
View file

@ -0,0 +1,134 @@
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
cnf_backbones.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_consequences.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_based_opt.cpp
model_evaluator.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
pb2bv.cpp
pdr.cpp
permutation.cpp
polynomial.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
lp.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(test-z3 PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS})
z3_append_linker_flag_list_to_target(test-z3 ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
z3_add_component_dependencies_to_target(test-z3 ${z3_test_expanded_deps})

8
src/test/fuzzing/CMakeLists.txt Normal file
View file

@ -0,0 +1,8 @@
z3_add_component(fuzzing
NOT_LIBZ3_COMPONENT # Don't put this component inside libz3
SOURCES
expr_delta.cpp
expr_rand.cpp
COMPONENT_DEPENDENCIES
ast
)

62
src/util/CMakeLists.txt Normal file
View file

@ -0,0 +1,62 @@
if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/version.h")
message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/version.h\""
${z3_polluted_tree_msg}
)
endif()
set(Z3_FULL_VERSION "\"${Z3_FULL_VERSION_STR}\"")
configure_file(version.h.cmake.in ${CMAKE_CURRENT_BINARY_DIR}/version.h)
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
)

35
src/util/lp/CMakeLists.txt Normal file
View file

@ -0,0 +1,35 @@
z3_add_component(lp
SOURCES
lp_utils.cpp
binary_heap_priority_queue_instances.cpp
binary_heap_upair_queue_instances.cpp
bound_propagator.cpp
core_solver_pretty_printer_instances.cpp
dense_matrix_instances.cpp
eta_matrix_instances.cpp
indexed_vector_instances.cpp
lar_core_solver_instances.cpp
lp_core_solver_base_instances.cpp
lp_dual_core_solver_instances.cpp
lp_dual_simplex_instances.cpp
lp_primal_core_solver_instances.cpp
lp_primal_simplex_instances.cpp
lp_settings_instances.cpp
lp_solver_instances.cpp
lu_instances.cpp
matrix_instances.cpp
permutation_matrix_instances.cpp
quick_xplain.cpp
row_eta_matrix_instances.cpp
scaler_instances.cpp
sparse_matrix_instances.cpp
square_dense_submatrix_instances.cpp
static_matrix_instances.cpp
random_updater_instances.cpp
COMPONENT_DEPENDENCIES
util
PYG_FILES
lp_params.pyg
)
include_directories(${src_SOURCE_DIR})