[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 Z3Prover#1030.

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 ``<NAME>.pyg`` files that should used to be generate
 # ``<NAME>_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)

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 ADD_PROBE(name, descr, cmd):
         '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 ADD_PROBE(name, descr, cmd):
     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:

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))

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))
 

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
 )

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
 )

src/muz/fp/CMakeLists.txt

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

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
 )

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
 )

src/sat/tactic/CMakeLists.txt

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

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
 )

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
 )

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
 )

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
 )

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
 )

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
 )
 

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
 )

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
 )

src/tactic/portfolio/CMakeLists.txt

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

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
 )

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
 )