mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

Merge pull request from delcypher/cmake_fix_generated_cpp_deps

Browse source 
[WIP][CMake] Fix broken regeneration of some .cpp files
This commit is contained in:
Nikolaj Bjorner 2017-06-21 17:47:41 -07:00 committed by GitHub
parent b516f22549 d00892c9a6
commit 1fee5fd94e
28 changed files with 300 additions and 75 deletions

137
cmake/z3_add_component.cmake
View file

@ -55,6 +55,9 @@ endfunction()
# SOURCES source1 [source2...]
# [COMPONENT_DEPENDENCIES component1 [component2...]]
# [PYG_FILES pygfile1 [pygfile2...]]
# [TACTIC_HEADERS header_file1 [header_file2...]]
# [EXTRA_REGISTER_MODULE_HEADERS header_file1 [header_file2...]]
# [MEMORY_INIT_FINALIZER_HEADERS header_file1 [header_file2...]]
# )
#
# Declares a Z3 component (as a CMake "object library") with target name
@ -80,14 +83,32 @@ endfunction()
# The optional ``PYG_FILES`` keyword should be followed by a list of one or
# more ``<NAME>.pyg`` files that should used to be generate
# ``<NAME>_params.hpp`` header files used by the ``component_name``.
# This generated file will automatically be scanned for the register module
# declarations (i.e. ``REG_PARAMS()``, ``REG_MODULE_PARAMS()``, and
# ``REG_MODULE_DESCRIPTION()``).
#
# The optional ``TACTIC_HEADERS`` keyword should be followed by a list of one or
# more header files that declare a tactic and/or a probe that is part of this
# component (see ``ADD_TACTIC()`` and ``ADD_PROBE()``).
#
# The optional ``EXTRA_REGISTER_MODULE_HEADERS`` keyword should be followed by a list
# of one or more header files that contain module registration declarations.
# NOTE: The header files generated from ``.pyg`` files don't need to be included.
#
# The optional ``MEMORY_INIT_FINALIZER_HEADERS`` keyword should be followed by a list
# of one or more header files that contain memory initializer/finalizer declarations
# (i.e. ``ADD_INITIALIZER()`` or ``ADD_FINALIZER()``).
macro(z3_add_component component_name)
CMAKE_PARSE_ARGUMENTS("Z3_MOD" "NOT_LIBZ3_COMPONENT" "" "SOURCES;COMPONENT_DEPENDENCIES;PYG_FILES" ${ARGN})
CMAKE_PARSE_ARGUMENTS("Z3_MOD"
"NOT_LIBZ3_COMPONENT"
""
"SOURCES;COMPONENT_DEPENDENCIES;PYG_FILES;TACTIC_HEADERS;EXTRA_REGISTER_MODULE_HEADERS;MEMORY_INIT_FINALIZER_HEADERS" ${ARGN})
message(STATUS "Adding component ${component_name}")
# Note: We don't check the sources exist here because
# they might be generated files that don't exist yet.
set(_list_generated_headers "")
set_property(GLOBAL PROPERTY Z3_${component_name}_REGISTER_MODULE_HEADERS "")
foreach (pyg_file ${Z3_MOD_PYG_FILES})
set(_full_pyg_file_path "${CMAKE_CURRENT_SOURCE_DIR}/${pyg_file}")
if (NOT (EXISTS "${_full_pyg_file_path}"))
@ -112,11 +133,70 @@ macro(z3_add_component component_name)
VERBATIM
)
list(APPEND _list_generated_headers "${_full_output_file_path}")
# FIXME: This implicit dependency of a generated file depending on
# generated files was inherited from the old build system.
# Typically generated headers contain `REG_PARAMS()`, `REG_MODULE_PARAMS()`
# and `REG_MODULE_DESCRIPTION()` declarations so add to the list of
# header files to scan.
set_property(GLOBAL
APPEND
PROPERTY Z3_${component_name}_REGISTER_MODULE_HEADERS
"${_full_output_file_path}"
)
endforeach()
unset(_full_include_dir_path)
unset(_full_output_file_path)
unset(_output_file)
# Add tactic/probe headers to global property
set_property(GLOBAL PROPERTY Z3_${component_name}_TACTIC_HEADERS "")
foreach (tactic_header ${Z3_MOD_TACTIC_HEADERS})
set(_full_tactic_header_file_path "${CMAKE_CURRENT_SOURCE_DIR}/${tactic_header}")
if (NOT (EXISTS "${_full_tactic_header_file_path}"))
message(FATAL_ERROR "\"${_full_tactic_header_file_path}\" does not exist")
endif()
set_property(GLOBAL
APPEND
PROPERTY Z3_${component_name}_TACTIC_HEADERS
"${_full_tactic_header_file_path}"
)
endforeach()
unset(_full_tactic_header_file_path)
# Add additional register module headers
foreach (extra_register_module_header ${Z3_MOD_EXTRA_REGISTER_MODULE_HEADERS})
set(_full_extra_register_module_header_path
"${CMAKE_CURRENT_SOURCE_DIR}/${extra_register_module_header}"
)
if (NOT (EXISTS "${_full_extra_register_module_header_path}"))
message(FATAL_ERROR "\"${_full_extra_register_module_header_path}\" does not exist")
endif()
set_property(GLOBAL
APPEND
PROPERTY Z3_${component_name}_REGISTER_MODULE_HEADERS
"${_full_extra_register_module_header_path}"
)
endforeach()
unset(_full_extra_register_module_header)
# Add memory initializer/finalizer headers to global property
set_property(GLOBAL PROPERTY Z3_${component_name}_MEM_INIT_FINALIZER_HEADERS "")
foreach (memory_init_finalizer_header ${Z3_MOD_MEMORY_INIT_FINALIZER_HEADERS})
set(_full_memory_init_finalizer_header_path
"${CMAKE_CURRENT_SOURCE_DIR}/${memory_init_finalizer_header}")
if (NOT (EXISTS "${_full_memory_init_finalizer_header_path}"))
message(FATAL_ERROR "\"${_full_memory_init_finalizer_header_path}\" does not exist")
endif()
set_property(GLOBAL
APPEND
PROPERTY Z3_${component_name}_MEM_INIT_FINALIZER_HEADERS
"${_full_memory_init_finalizer_header_path}"
)
endforeach()
unset(_full_memory_init_finalizer_header_path)
# Using "object" libraries here means we have a convenient
# name to refer to a component in CMake but we don't actually
# create a static/library from them. This allows us to easily
@ -191,25 +271,33 @@ macro(z3_add_install_tactic_rule)
)
endif()
z3_expand_dependencies(_expanded_components ${ARGN})
# Get paths to search
set(_search_paths "")
# Get header files that declare tactics/probes
set(_tactic_header_files "")
foreach (dependency ${_expanded_components})
get_property(_dep_include_dirs GLOBAL PROPERTY Z3_${dependency}_INCLUDES)
list(APPEND _search_paths ${_dep_include_dirs})
get_property(_component_tactic_header_files
GLOBAL
PROPERTY Z3_${dependency}_TACTIC_HEADERS
)
list(APPEND _tactic_header_files ${_component_tactic_header_files})
endforeach()
unset(_component_tactic_header_files)
list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}")
add_custom_command(OUTPUT "install_tactic.cpp"
COMMAND "${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py"
"${CMAKE_CURRENT_BINARY_DIR}"
${_search_paths}
${_tactic_header_files}
DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
${_expanded_components}
${_tactic_header_files}
COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp\""
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
VERBATIM
)
unset(_expanded_components)
unset(_tactic_header_files)
endmacro()
macro(z3_add_memory_initializer_rule)
@ -230,18 +318,31 @@ macro(z3_add_memory_initializer_rule)
list(APPEND _search_paths ${_dep_include_dirs})
endforeach()
list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}")
# Get header files that declare initializers and finalizers
set(_mem_init_finalize_headers "")
foreach (dependency ${_expanded_components})
get_property(_dep_mem_init_finalize_headers
GLOBAL
PROPERTY Z3_${dependency}_MEM_INIT_FINALIZER_HEADERS
)
list(APPEND _mem_init_finalize_headers ${_dep_mem_init_finalize_headers})
endforeach()
add_custom_command(OUTPUT "mem_initializer.cpp"
COMMAND "${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/mk_mem_initializer_cpp.py"
"${CMAKE_CURRENT_BINARY_DIR}"
${_search_paths}
${_mem_init_finalize_headers}
DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_mem_initializer_cpp.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
${_expanded_components}
${_mem_init_finalize_headers}
COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp\""
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
VERBATIM
)
unset(_mem_init_finalize_headers)
unset(_expanded_components)
endmacro()
macro(z3_add_gparams_register_modules_rule)
@ -255,23 +356,27 @@ macro(z3_add_gparams_register_modules_rule)
)
endif()
z3_expand_dependencies(_expanded_components ${ARGN})
# Get paths to search
set(_search_paths "")
# Get the list of header files to parse
set(_register_module_header_files "")
foreach (dependency ${_expanded_components})
get_property(_dep_include_dirs GLOBAL PROPERTY Z3_${dependency}_INCLUDES)
list(APPEND _search_paths ${_dep_include_dirs})
get_property(_component_register_module_header_files GLOBAL PROPERTY Z3_${dependency}_REGISTER_MODULE_HEADERS)
list(APPEND _register_module_header_files ${_component_register_module_header_files})
endforeach()
list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}")
unset(_component_register_module_header_files)
add_custom_command(OUTPUT "gparams_register_modules.cpp"
COMMAND "${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/mk_gparams_register_modules_cpp.py"
"${CMAKE_CURRENT_BINARY_DIR}"
${_search_paths}
${_register_module_header_files}
DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_gparams_register_modules_cpp.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
${_expanded_components}
${_register_module_header_files}
COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp\""
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
VERBATIM
)
unset(_expanded_components)
unset(_register_module_header_files)
endmacro()

34
scripts/mk_genfile_common.py
View file

@ -587,7 +587,7 @@ def mk_def_file_internal(defname, dll_name, export_header_files):
###############################################################################
# Functions for generating ``gparams_register_modules.cpp``
###############################################################################
def mk_gparams_register_modules_internal(component_src_dirs, path):
def mk_gparams_register_modules_internal(h_files_full_path, path):
"""
Generate a ``gparams_register_modules.cpp`` file in the directory ``path``.
Returns the path to the generated file.
@ -600,7 +600,7 @@ def mk_gparams_register_modules_internal(component_src_dirs, path):
This procedure is invoked by gparams::init()
"""
assert isinstance(component_src_dirs, list)
assert isinstance(h_files_full_path, list)
assert check_dir_exists(path)
cmds = []
mod_cmds = []
@ -612,11 +612,6 @@ def mk_gparams_register_modules_internal(component_src_dirs, path):
reg_pat = re.compile('[ \t]*REG_PARAMS\(\'([^\']*)\'\)')
reg_mod_pat = re.compile('[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)')
reg_mod_descr_pat = re.compile('[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)')
h_files_full_path = []
for component_src_dir in component_src_dirs:
h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir))
h_files = list(map(lambda p: os.path.join(component_src_dir, p), h_files))
h_files_full_path.extend(h_files)
for h_file in sorted_headers_by_component(h_files_full_path):
added_include = False
with open(h_file, 'r') as fin:
@ -651,7 +646,7 @@ def mk_gparams_register_modules_internal(component_src_dirs, path):
# Functions/data structures for generating ``install_tactics.cpp``
###############################################################################
def mk_install_tactic_cpp_internal(component_src_dirs, path):
def mk_install_tactic_cpp_internal(h_files_full_path, path):
"""
Generate a ``install_tactics.cpp`` file in the directory ``path``.
Returns the path the generated file.
@ -662,9 +657,10 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path):
void install_tactics(tactic_manager & ctx)
```
It installs all tactics found in the given component directories
``component_src_dirs`` The procedure looks for ``ADD_TACTIC`` commands
in the ``.h`` and ``.hpp`` files of these components.
It installs all tactics declared in the given header files
``h_files_full_path`` The procedure looks for ``ADD_TACTIC`` and
``ADD_PROBE``commands in the ``.h`` and ``.hpp`` files of these
components.
"""
ADD_TACTIC_DATA = []
ADD_PROBE_DATA = []
@ -679,7 +675,7 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path):
'ADD_PROBE': ADD_PROBE,
}
assert isinstance(component_src_dirs, list)
assert isinstance(h_files_full_path, list)
assert check_dir_exists(path)
fullname = os.path.join(path, 'install_tactic.cpp')
fout = open(fullname, 'w')
@ -689,11 +685,6 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path):
fout.write('#include"cmd_context.h"\n')
tactic_pat = re.compile('[ \t]*ADD_TACTIC\(.*\)')
probe_pat = re.compile('[ \t]*ADD_PROBE\(.*\)')
h_files_full_path = []
for component_src_dir in sorted(component_src_dirs):
h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir))
h_files = list(map(lambda p: os.path.join(component_src_dir, p), h_files))
h_files_full_path.extend(h_files)
for h_file in sorted_headers_by_component(h_files_full_path):
added_include = False
with open(h_file, 'r') as fin:
@ -740,7 +731,7 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path):
# Functions for generating ``mem_initializer.cpp``
###############################################################################
def mk_mem_initializer_cpp_internal(component_src_dirs, path):
def mk_mem_initializer_cpp_internal(h_files_full_path, path):
"""
Generate a ``mem_initializer.cpp`` file in the directory ``path``.
Returns the path to the generated file.
@ -754,7 +745,7 @@ def mk_mem_initializer_cpp_internal(component_src_dirs, path):
These procedures are invoked by the Z3 memory_manager
"""
assert isinstance(component_src_dirs, list)
assert isinstance(h_files_full_path, list)
assert check_dir_exists(path)
initializer_cmds = []
finalizer_cmds = []
@ -765,11 +756,6 @@ def mk_mem_initializer_cpp_internal(component_src_dirs, path):
# ADD_INITIALIZER with priority
initializer_prio_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)')
finalizer_pat = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)')
h_files_full_path = []
for component_src_dir in sorted(component_src_dirs):
h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir))
h_files = list(map(lambda p: os.path.join(component_src_dir, p), h_files))
h_files_full_path.extend(h_files)
for h_file in sorted_headers_by_component(h_files_full_path):
added_include = False
with open(h_file, 'r') as fin:

23
scripts/mk_gparams_register_modules_cpp.py
View file

@ -1,10 +1,8 @@
#!/usr/bin/env python
"""
Determines the available global parameters
in header files in the list of source directions
and generates a ``gparams_register_modules.cpp`` file in
the destination directory that defines a function
``void gparams_register_modules()``.
Determines the available global parameters from a list of header files and
generates a ``gparams_register_modules.cpp`` file in the destination directory
that defines a function ``void gparams_register_modules()``.
"""
import mk_genfile_common
import argparse
@ -16,19 +14,22 @@ def main(args):
logging.basicConfig(level=logging.INFO)
parser = argparse.ArgumentParser(description=__doc__)
parser.add_argument("destination_dir", help="destination directory")
parser.add_argument("source_dirs", nargs="+",
help="One or more source directories to search")
parser.add_argument("header_files", nargs="+",
help="One or more header files to parse")
pargs = parser.parse_args(args)
if not mk_genfile_common.check_dir_exists(pargs.destination_dir):
return 1
for source_dir in pargs.source_dirs:
if not mk_genfile_common.check_dir_exists(source_dir):
return 1
if not mk_genfile_common.check_files_exist(pargs.header_files):
return 1
h_files_full_path = []
for header_file in pargs.header_files:
h_files_full_path.append(os.path.abspath(header_file))
output = mk_genfile_common.mk_gparams_register_modules_internal(
pargs.source_dirs,
h_files_full_path,
pargs.destination_dir
)
logging.info('Generated "{}"'.format(output))

23
scripts/mk_install_tactic_cpp.py
View file

@ -1,10 +1,8 @@
#!/usr/bin/env python
"""
Determines the available tactics
in header files in the list of source directions
and generates a ``install_tactic.cpp`` file in
the destination directory that defines a function
``void install_tactics(tactic_manager& ctx)``.
Determines the available tactics from a list of header files and generates a
``install_tactic.cpp`` file in the destination directory that defines a
function ``void install_tactics(tactic_manager& ctx)``.
"""
import mk_genfile_common
import argparse
@ -16,19 +14,22 @@ def main(args):
logging.basicConfig(level=logging.INFO)
parser = argparse.ArgumentParser(description=__doc__)
parser.add_argument("destination_dir", help="destination directory")
parser.add_argument("source_dirs", nargs="+",
help="One or more source directories to search")
parser.add_argument("header_files", nargs="+",
help="One or more header files to parse")
pargs = parser.parse_args(args)
if not mk_genfile_common.check_dir_exists(pargs.destination_dir):
return 1
for source_dir in pargs.source_dirs:
if not mk_genfile_common.check_dir_exists(source_dir):
return 1
if not mk_genfile_common.check_files_exist(pargs.header_files):
return 1
h_files_full_path = []
for header_file in pargs.header_files:
h_files_full_path.append(os.path.abspath(header_file))
output = mk_genfile_common.mk_install_tactic_cpp_internal(
pargs.source_dirs,
h_files_full_path,
pargs.destination_dir
)
logging.info('Generated "{}"'.format(output))

14
scripts/mk_mem_initializer_cpp.py
View file

@ -1,6 +1,6 @@
#!/usr/bin/env python
"""
Scans the source directories for
Scans the listed header files for
memory initializers and finalizers and
emits and implementation of
``void mem_initialize()`` and
@ -17,19 +17,19 @@ def main(args):
logging.basicConfig(level=logging.INFO)
parser = argparse.ArgumentParser(description=__doc__)
parser.add_argument("destination_dir", help="destination directory")
parser.add_argument("source_dirs", nargs="+",
help="One or more source directories to search")
parser.add_argument("header_files", nargs="+",
help="One or more header files to parse")
pargs = parser.parse_args(args)
if not mk_genfile_common.check_dir_exists(pargs.destination_dir):
return 1
for source_dir in pargs.source_dirs:
if not mk_genfile_common.check_dir_exists(source_dir):
return 1
h_files_full_path = []
for header_file in pargs.header_files:
h_files_full_path.append(os.path.abspath(header_file))
output = mk_genfile_common.mk_mem_initializer_cpp_internal(
pargs.source_dirs,
h_files_full_path,
pargs.destination_dir
)
logging.info('Generated "{}"'.format(output))

18
scripts/mk_util.py
View file

@ -2712,12 +2712,22 @@ def mk_all_assembly_infos(major, minor, build, revision):
else:
raise MKException("Failed to find assembly template info file '%s'" % assembly_info_template)
def get_header_files_for_components(component_src_dirs):
assert isinstance(component_src_dirs, list)
h_files_full_path = []
for component_src_dir in sorted(component_src_dirs):
h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir))
h_files = list(map(lambda p: os.path.join(component_src_dir, p), h_files))
h_files_full_path.extend(h_files)
return h_files_full_path
def mk_install_tactic_cpp(cnames, path):
component_src_dirs = []
for cname in cnames:
c = get_component(cname)
component_src_dirs.append(c.src_dir)
generated_file = mk_genfile_common.mk_install_tactic_cpp_internal(component_src_dirs, path)
h_files_full_path = get_header_files_for_components(component_src_dirs)
generated_file = mk_genfile_common.mk_install_tactic_cpp_internal(h_files_full_path, path)
if VERBOSE:
print("Generated '{}'".format(generated_file))
@ -2735,7 +2745,8 @@ def mk_mem_initializer_cpp(cnames, path):
for cname in cnames:
c = get_component(cname)
component_src_dirs.append(c.src_dir)
generated_file = mk_genfile_common.mk_mem_initializer_cpp_internal(component_src_dirs, path)
h_files_full_path = get_header_files_for_components(component_src_dirs)
generated_file = mk_genfile_common.mk_mem_initializer_cpp_internal(h_files_full_path, path)
if VERBOSE:
print("Generated '{}'".format(generated_file))
@ -2753,7 +2764,8 @@ def mk_gparams_register_modules(cnames, path):
for cname in cnames:
c = get_component(cname)
component_src_dirs.append(c.src_dir)
generated_file = mk_genfile_common.mk_gparams_register_modules_internal(component_src_dirs, path)
h_files_full_path = get_header_files_for_components(component_src_dirs)
generated_file = mk_genfile_common.mk_gparams_register_modules_internal(h_files_full_path, path)
if VERBOSE:
print("Generated '{}'".format(generated_file))

3
src/ackermannization/CMakeLists.txt
View file

@ -17,4 +17,7 @@ z3_add_component(ackermannization
PYG_FILES
ackermannization_params.pyg
ackermannize_bv_tactic_params.pyg
TACTIC_HEADERS
ackermannize_bv_tactic.h
ackr_bound_probe.h
)

2
src/ast/normal_forms/CMakeLists.txt
View file

@ -8,4 +8,6 @@ z3_add_component(normal_forms
rewriter
PYG_FILES
nnf_params.pyg
EXTRA_REGISTER_MODULE_HEADERS
nnf.h
)

2
src/cmd_context/CMakeLists.txt
View file

@ -18,4 +18,6 @@ z3_add_component(cmd_context
interp
rewriter
solver
EXTRA_REGISTER_MODULE_HEADERS
context_params.h
)

2
src/math/polynomial/CMakeLists.txt
View file

@ -11,5 +11,7 @@ z3_add_component(polynomial
util
PYG_FILES
algebraic_params.pyg
EXTRA_REGISTER_MODULE_HEADERS
polynomial.h
)

2
src/math/subpaving/tactic/CMakeLists.txt
View file

@ -5,4 +5,6 @@ z3_add_component(subpaving_tactic
COMPONENT_DEPENDENCIES
core_tactics
subpaving
TACTIC_HEADERS
subpaving_tactic.h
)

2
src/muz/fp/CMakeLists.txt
View file

@ -13,4 +13,6 @@ z3_add_component(fp
pdr
rel
tab
TACTIC_HEADERS
horn_tactic.h
)

3
src/nlsat/tactic/CMakeLists.txt
View file

@ -7,4 +7,7 @@ z3_add_component(nlsat_tactic
arith_tactics
nlsat
sat_tactic
TACTIC_HEADERS
nlsat_tactic.h
qfnra_nlsat_tactic.h
)

11
src/qe/CMakeLists.txt
View file

@ -23,6 +23,13 @@ z3_add_component(qe
nlsat_tactic
nlsat
sat
smt
tactic
smt
tactic
TACTIC_HEADERS
nlqsat.h
qe_lite.h
qe_sat_tactic.h
qe_tactic.h
qsat.h
vsubst_tactic.h
)

2
src/sat/tactic/CMakeLists.txt
View file

@ -6,4 +6,6 @@ z3_add_component(sat_tactic
COMPONENT_DEPENDENCIES
sat
tactic
TACTIC_HEADERS
sat_tactic.h
)

4
src/smt/tactic/CMakeLists.txt
View file

@ -5,4 +5,8 @@ z3_add_component(smt_tactic
unit_subsumption_tactic.cpp
COMPONENT_DEPENDENCIES
smt
TACTIC_HEADERS
ctx_solver_simplify_tactic.h
smt_tactic.h
unit_subsumption_tactic.h
)

4
src/tactic/CMakeLists.txt
View file

@ -18,4 +18,8 @@ z3_add_component(tactic
COMPONENT_DEPENDENCIES
ast
model
TACTIC_HEADERS
probe.h
sine_filter.h
tactic.h
)

2
src/tactic/aig/CMakeLists.txt
View file

@ -4,4 +4,6 @@ z3_add_component(aig_tactic
aig_tactic.cpp
COMPONENT_DEPENDENCIES
tactic
TACTIC_HEADERS
aig_tactic.h
)

19
src/tactic/arith/CMakeLists.txt
View file

@ -28,4 +28,23 @@ z3_add_component(arith_tactics
COMPONENT_DEPENDENCIES
core_tactics
sat
TACTIC_HEADERS
add_bounds_tactic.h
card2bv_tactic.h
degree_shift_tactic.h
diff_neq_tactic.h
elim01_tactic.h
eq2bv_tactic.h
factor_tactic.h
fix_dl_var_tactic.h
fm_tactic.h
lia2pb_tactic.h
lia2card_tactic.h
nla2bv_tactic.h
normalize_bounds_tactic.h
pb2bv_tactic.h
probe_arith.h
propagate_ineqs_tactic.h
purify_arith_tactic.h
recover_01_tactic.h
)

10
src/tactic/bv/CMakeLists.txt
View file

@ -15,4 +15,14 @@ z3_add_component(bv_tactics
bit_blaster
core_tactics
tactic
TACTIC_HEADERS
bit_blaster_tactic.h
bv1_blaster_tactic.h
bv_bound_chk_tactic.h
bv_bounds_tactic.h
bv_size_reduction_tactic.h
bvarray2uf_tactic.h
dt2bv_tactic.h
elim_small_bv_tactic.h
max_bv_sharing_tactic.h
)

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

@ -3,7 +3,7 @@ z3_add_component(core_tactics
blast_term_ite_tactic.cpp
cofactor_elim_term_ite.cpp
cofactor_term_ite_tactic.cpp
collect_statistics_tactic.cpp
collect_statistics_tactic.cpp
ctx_simplify_tactic.cpp
der_tactic.cpp
distribute_forall_tactic.cpp
@ -23,5 +23,24 @@ z3_add_component(core_tactics
COMPONENT_DEPENDENCIES
normal_forms
tactic
TACTIC_HEADERS
blast_term_ite_tactic.h
cofactor_term_ite_tactic.h
collect_statistics_tactic.h
ctx_simplify_tactic.h
der_tactic.h
distribute_forall_tactic.h
elim_term_ite_tactic.h
elim_uncnstr_tactic.h
nnf_tactic.h
occf_tactic.h
pb_preprocess_tactic.h
propagate_values_tactic.h
reduce_args_tactic.h
simplify_tactic.h
solve_eqs_tactic.h
split_clause_tactic.h
symmetry_reduce_tactic.h
tseitin_cnf_tactic.h
)

3
src/tactic/fpa/CMakeLists.txt
View file

@ -11,4 +11,7 @@ z3_add_component(fpa_tactics
sat_tactic
smtlogic_tactics
smt_tactic
TACTIC_HEADERS
fpa2bv_tactic.h
qffp_tactic.h
)

2
src/tactic/nlsat_smt/CMakeLists.txt
View file

@ -4,4 +4,6 @@ z3_add_component(nlsat_smt_tactic
COMPONENT_DEPENDENCIES
nlsat_tactic
smt_tactic
TACTIC_HEADERS
nl_purify_tactic.h
)

2
src/tactic/portfolio/CMakeLists.txt
View file

@ -16,4 +16,6 @@ z3_add_component(portfolio
smtlogic_tactics
subpaving_tactic
ufbv_tactic
TACTIC_HEADERS
default_tactic.h
)

2
src/tactic/sls/CMakeLists.txt
View file

@ -10,4 +10,6 @@ z3_add_component(sls_tactic
tactic
PYG_FILES
sls_params.pyg
TACTIC_HEADERS
sls_tactic.h
)

14
src/tactic/smtlogics/CMakeLists.txt
View file

@ -28,4 +28,18 @@ z3_add_component(smtlogic_tactics
smt_tactic
PYG_FILES
qfufbv_tactic_params.pyg
TACTIC_HEADERS
nra_tactic.h
qfaufbv_tactic.h
qfauflia_tactic.h
qfbv_tactic.h
qfidl_tactic.h
qflia_tactic.h
qflra_tactic.h
qfnia_tactic.h
qfnra_tactic.h
qfuf_tactic.h
qfufbv_tactic.h
qfufnra_tactic.h
quant_tactics.h
)

5
src/tactic/ufbv/CMakeLists.txt
View file

@ -11,4 +11,9 @@ z3_add_component(ufbv_tactic
normal_forms
rewriter
smt_tactic
TACTIC_HEADERS
macro_finder_tactic.h
quasi_macros_tactic.h
ufbv_rewriter_tactic.h
ufbv_tactic.h
)

9
src/util/CMakeLists.txt
View file

@ -59,4 +59,13 @@ z3_add_component(util
util.cpp
warning.cpp
z3_exception.cpp
EXTRA_REGISTER_MODULE_HEADERS
env_params.h
MEMORY_INIT_FINALIZER_HEADERS
debug.h
gparams.h
prime_generator.h
rational.h
symbol.h
trace.h
)