From 229fd3dc3e6123ef207146161686dd22f9ea76e9 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 21 Jun 2017 18:36:20 +0100 Subject: [PATCH] [CMake] Fix dependencies for generating `install_tactic.cpp`. Previously CMake was not aware of which headers files the generation of `install_tactic.cpp` depended on. Consequently this could result in broken incremental builds if * Existing headers that declared tactics/probes changed. * New tactics/probes were added to new header files. Now the `z3_add_component()` CMake function has been modifed to take an optional `TACTIC_HEADERS` argument which allows the headers that declare tactics/probes to be explicitly listed. The necessary component declarations have been modified to declare their tactic/probe header files. With this information CMake will now regenerate `install_tactic.cpp` correctly. This required the `mk_install_tactic_cpp_internal()` function to be changed to take a list of header files rather than a list of component source directories. The two consumers (CMake and Python/Makefile build systems) of this function have been modified to work with this change. This partially fixes #1030. --- cmake/z3_add_component.cmake | 41 ++++++++++++++++++++---- scripts/mk_genfile_common.py | 16 ++++----- scripts/mk_install_tactic_cpp.py | 23 ++++++------- scripts/mk_util.py | 12 ++++++- src/ackermannization/CMakeLists.txt | 3 ++ src/math/subpaving/tactic/CMakeLists.txt | 2 ++ src/muz/fp/CMakeLists.txt | 2 ++ src/nlsat/tactic/CMakeLists.txt | 3 ++ src/qe/CMakeLists.txt | 11 +++++-- src/sat/tactic/CMakeLists.txt | 2 ++ src/smt/tactic/CMakeLists.txt | 4 +++ src/tactic/CMakeLists.txt | 4 +++ src/tactic/aig/CMakeLists.txt | 2 ++ src/tactic/arith/CMakeLists.txt | 19 +++++++++++ src/tactic/bv/CMakeLists.txt | 10 ++++++ src/tactic/core/CMakeLists.txt | 21 +++++++++++- src/tactic/fpa/CMakeLists.txt | 3 ++ src/tactic/nlsat_smt/CMakeLists.txt | 2 ++ src/tactic/portfolio/CMakeLists.txt | 2 ++ src/tactic/sls/CMakeLists.txt | 2 ++ src/tactic/smtlogics/CMakeLists.txt | 14 ++++++++ src/tactic/ufbv/CMakeLists.txt | 5 +++ 22 files changed, 171 insertions(+), 32 deletions(-) diff --git a/cmake/z3_add_component.cmake b/cmake/z3_add_component.cmake index b90aa2fe7..43a634ae1 100644 --- a/cmake/z3_add_component.cmake +++ b/cmake/z3_add_component.cmake @@ -55,6 +55,7 @@ endfunction() # SOURCES source1 [source2...] # [COMPONENT_DEPENDENCIES component1 [component2...]] # [PYG_FILES pygfile1 [pygfile2...]] +# [TACTIC_HEADERS header_file1 [header_file2...]] # ) # # Declares a Z3 component (as a CMake "object library") with target name @@ -81,8 +82,11 @@ endfunction() # more ``.pyg`` files that should used to be generate # ``_params.hpp`` header files used by the ``component_name``. # +# 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()``). 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" ${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. @@ -117,6 +121,21 @@ macro(z3_add_component component_name) 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) + # 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 +210,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) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 98346f99f..1a2a2dad7 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -651,7 +651,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 +662,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 +680,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 +690,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: diff --git a/scripts/mk_install_tactic_cpp.py b/scripts/mk_install_tactic_cpp.py index 21e66b3ab..a152eff14 100755 --- a/scripts/mk_install_tactic_cpp.py +++ b/scripts/mk_install_tactic_cpp.py @@ -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)) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index e7e35817f..b5924d0d1 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -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)) diff --git a/src/ackermannization/CMakeLists.txt b/src/ackermannization/CMakeLists.txt index 93529ae12..3ce7f97cc 100644 --- a/src/ackermannization/CMakeLists.txt +++ b/src/ackermannization/CMakeLists.txt @@ -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 ) diff --git a/src/math/subpaving/tactic/CMakeLists.txt b/src/math/subpaving/tactic/CMakeLists.txt index eedb0ed4d..8873a1021 100644 --- a/src/math/subpaving/tactic/CMakeLists.txt +++ b/src/math/subpaving/tactic/CMakeLists.txt @@ -5,4 +5,6 @@ z3_add_component(subpaving_tactic COMPONENT_DEPENDENCIES core_tactics subpaving + TACTIC_HEADERS + subpaving_tactic.h ) diff --git a/src/muz/fp/CMakeLists.txt b/src/muz/fp/CMakeLists.txt index 239c4df12..4a7c4d018 100644 --- a/src/muz/fp/CMakeLists.txt +++ b/src/muz/fp/CMakeLists.txt @@ -13,4 +13,6 @@ z3_add_component(fp pdr rel tab + TACTIC_HEADERS + horn_tactic.h ) diff --git a/src/nlsat/tactic/CMakeLists.txt b/src/nlsat/tactic/CMakeLists.txt index 9ea26a0c5..3be3bcfb7 100644 --- a/src/nlsat/tactic/CMakeLists.txt +++ b/src/nlsat/tactic/CMakeLists.txt @@ -7,4 +7,7 @@ z3_add_component(nlsat_tactic arith_tactics nlsat sat_tactic + TACTIC_HEADERS + nlsat_tactic.h + qfnra_nlsat_tactic.h ) diff --git a/src/qe/CMakeLists.txt b/src/qe/CMakeLists.txt index 6e82e2c96..2d2cf9579 100644 --- a/src/qe/CMakeLists.txt +++ b/src/qe/CMakeLists.txt @@ -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 ) diff --git a/src/sat/tactic/CMakeLists.txt b/src/sat/tactic/CMakeLists.txt index 74aeba8b9..fed6a89c8 100644 --- a/src/sat/tactic/CMakeLists.txt +++ b/src/sat/tactic/CMakeLists.txt @@ -6,4 +6,6 @@ z3_add_component(sat_tactic COMPONENT_DEPENDENCIES sat tactic + TACTIC_HEADERS + sat_tactic.h ) diff --git a/src/smt/tactic/CMakeLists.txt b/src/smt/tactic/CMakeLists.txt index b7525bda8..6187f9c18 100644 --- a/src/smt/tactic/CMakeLists.txt +++ b/src/smt/tactic/CMakeLists.txt @@ -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 ) diff --git a/src/tactic/CMakeLists.txt b/src/tactic/CMakeLists.txt index 324d8089b..e7cfdb644 100644 --- a/src/tactic/CMakeLists.txt +++ b/src/tactic/CMakeLists.txt @@ -18,4 +18,8 @@ z3_add_component(tactic COMPONENT_DEPENDENCIES ast model + TACTIC_HEADERS + probe.h + sine_filter.h + tactic.h ) diff --git a/src/tactic/aig/CMakeLists.txt b/src/tactic/aig/CMakeLists.txt index 1e1a0d266..51ea9b6d3 100644 --- a/src/tactic/aig/CMakeLists.txt +++ b/src/tactic/aig/CMakeLists.txt @@ -4,4 +4,6 @@ z3_add_component(aig_tactic aig_tactic.cpp COMPONENT_DEPENDENCIES tactic + TACTIC_HEADERS + aig_tactic.h ) diff --git a/src/tactic/arith/CMakeLists.txt b/src/tactic/arith/CMakeLists.txt index cdc42367a..335020838 100644 --- a/src/tactic/arith/CMakeLists.txt +++ b/src/tactic/arith/CMakeLists.txt @@ -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 ) diff --git a/src/tactic/bv/CMakeLists.txt b/src/tactic/bv/CMakeLists.txt index 90ed65e3f..e9f0927d5 100644 --- a/src/tactic/bv/CMakeLists.txt +++ b/src/tactic/bv/CMakeLists.txt @@ -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 ) diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt index fcd26bd84..1f766bd47 100644 --- a/src/tactic/core/CMakeLists.txt +++ b/src/tactic/core/CMakeLists.txt @@ -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 ) diff --git a/src/tactic/fpa/CMakeLists.txt b/src/tactic/fpa/CMakeLists.txt index d93cd5b82..a54212235 100644 --- a/src/tactic/fpa/CMakeLists.txt +++ b/src/tactic/fpa/CMakeLists.txt @@ -11,4 +11,7 @@ z3_add_component(fpa_tactics sat_tactic smtlogic_tactics smt_tactic + TACTIC_HEADERS + fpa2bv_tactic.h + qffp_tactic.h ) diff --git a/src/tactic/nlsat_smt/CMakeLists.txt b/src/tactic/nlsat_smt/CMakeLists.txt index e28b11966..ccfc0e3ef 100644 --- a/src/tactic/nlsat_smt/CMakeLists.txt +++ b/src/tactic/nlsat_smt/CMakeLists.txt @@ -4,4 +4,6 @@ z3_add_component(nlsat_smt_tactic COMPONENT_DEPENDENCIES nlsat_tactic smt_tactic + TACTIC_HEADERS + nl_purify_tactic.h ) diff --git a/src/tactic/portfolio/CMakeLists.txt b/src/tactic/portfolio/CMakeLists.txt index c6f621f25..a8a9b2bba 100644 --- a/src/tactic/portfolio/CMakeLists.txt +++ b/src/tactic/portfolio/CMakeLists.txt @@ -16,4 +16,6 @@ z3_add_component(portfolio smtlogic_tactics subpaving_tactic ufbv_tactic + TACTIC_HEADERS + default_tactic.h ) diff --git a/src/tactic/sls/CMakeLists.txt b/src/tactic/sls/CMakeLists.txt index 8b720b333..436b1742f 100644 --- a/src/tactic/sls/CMakeLists.txt +++ b/src/tactic/sls/CMakeLists.txt @@ -10,4 +10,6 @@ z3_add_component(sls_tactic tactic PYG_FILES sls_params.pyg + TACTIC_HEADERS + sls_tactic.h ) diff --git a/src/tactic/smtlogics/CMakeLists.txt b/src/tactic/smtlogics/CMakeLists.txt index 840dd008a..c90fd7468 100644 --- a/src/tactic/smtlogics/CMakeLists.txt +++ b/src/tactic/smtlogics/CMakeLists.txt @@ -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 ) diff --git a/src/tactic/ufbv/CMakeLists.txt b/src/tactic/ufbv/CMakeLists.txt index c1d6daaaa..511dc2b2d 100644 --- a/src/tactic/ufbv/CMakeLists.txt +++ b/src/tactic/ufbv/CMakeLists.txt @@ -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 )