From a3ee7859234779181facbb2b35dbaa2f5da785e5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 21 Jun 2017 07:29:21 -0700 Subject: [PATCH 01/25] disable dt2bv for quantified variables as enum2bv does not handle them. #1092 Signed-off-by: Nikolaj Bjorner --- src/tactic/bv/dt2bv_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp index 2b9cfb7f3..cac6f1f5d 100644 --- a/src/tactic/bv/dt2bv_tactic.cpp +++ b/src/tactic/bv/dt2bv_tactic.cpp @@ -82,7 +82,7 @@ class dt2bv_tactic : public tactic { void operator()(var * v) { if (m_t.is_fd(v)) { - m_t.m_fd_sorts.insert(get_sort(v)); + m_t.m_non_fd_sorts.insert(get_sort(v)); } } From b516f2254990cd0d56ae81652c260cfdc3e164b6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 21 Jun 2017 08:01:03 -0700 Subject: [PATCH 02/25] refine test for non-fd to be more inclusive while addressing #1092 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.h | 2 ++ src/tactic/bv/dt2bv_tactic.cpp | 31 +++++++++++++++++-------------- 2 files changed, 19 insertions(+), 14 deletions(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index 475e58ac7..f71d5135c 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -667,6 +667,8 @@ public: expr * get_arg(unsigned idx) const { SASSERT(idx < m_num_args); return m_args[idx]; } expr * const * get_args() const { return m_args; } unsigned get_size() const { return get_obj_size(get_num_args()); } + expr * const * begin() const { return m_args; } + expr * const * end() const { return m_args + m_num_args; } unsigned get_depth() const { return flags()->m_depth; } bool is_ground() const { return flags()->m_ground; } diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp index cac6f1f5d..3ae72215f 100644 --- a/src/tactic/bv/dt2bv_tactic.cpp +++ b/src/tactic/bv/dt2bv_tactic.cpp @@ -30,6 +30,7 @@ Revision History: #include "var_subst.h" #include "ast_util.h" #include "enum2bv_rewriter.h" +#include "ast_pp.h" class dt2bv_tactic : public tactic { @@ -53,36 +54,38 @@ class dt2bv_tactic : public tactic { void operator()(app* a) { if (m.is_eq(a)) { - return; + // no-op } - if (m.is_distinct(a)) { - return; + else if (m.is_distinct(a)) { + // no-op } - if (m_t.m_dt.is_recognizer(a->get_decl()) && + else if (m_t.m_dt.is_recognizer(a->get_decl()) && m_t.is_fd(a->get_arg(0))) { m_t.m_fd_sorts.insert(get_sort(a->get_arg(0))); - return; } - - if (m_t.is_fd(a) && a->get_num_args() > 0) { + else if (m_t.is_fd(a) && a->get_num_args() > 0) { m_t.m_non_fd_sorts.insert(get_sort(a)); + args_cannot_be_fd(a); } else if (m_t.is_fd(a)) { m_t.m_fd_sorts.insert(get_sort(a)); } else { - unsigned sz = a->get_num_args(); - for (unsigned i = 0; i < sz; ++i) { - if (m_t.is_fd(a->get_arg(i))) { - m_t.m_non_fd_sorts.insert(get_sort(a->get_arg(i))); - } - } + args_cannot_be_fd(a); + } + } + + void args_cannot_be_fd(app* a) { + for (expr* arg : *a) { + if (m_t.is_fd(arg)) { + m_t.m_non_fd_sorts.insert(get_sort(arg)); + } } } void operator()(var * v) { if (m_t.is_fd(v)) { - m_t.m_non_fd_sorts.insert(get_sort(v)); + m_t.m_fd_sorts.insert(get_sort(v)); } } From 229fd3dc3e6123ef207146161686dd22f9ea76e9 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 21 Jun 2017 18:36:20 +0100 Subject: [PATCH 03/25] [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 ) From 6f48a145aaafe3bc28f1239f3f13325a7d4eeaef Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 21 Jun 2017 22:56:31 +0100 Subject: [PATCH 04/25] [CMake] Fix dependencies for generating `gparams_register_modules.cpp`. Previously CMake was not aware of which headers files the generation of `gparams_register_modules.cpp` depended on. Consequently this could result in broken incremental builds if * Existing headers that declared module description/parameters change. * New headers are added that declare module description/parameters. * `.pyg` files that generate header files that declare module description/parameters change Now the `z3_add_component()` CMake function has been modifed so that * All header files that are generated from `.pyg` files are added as dependencies and are scanned from module description/parameter declarations. This implicit dependency of `gparams_register_modules.cpp` depending on other generated header files seems unnecessary complex. We should revisit this design decision once the Python/Makefile build system is deprecated. * The function now takes an optional `EXTRA_REGISTER_MODULE_HEADERS` argument which allows the headers that declare module description/paramters to be explicitly listed. With this information CMake will now regenerate `gparams_register_modules.cpp` correctly. This required the `mk_gparams_register_modules_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 | 60 +++++++++++++++++++--- scripts/mk_genfile_common.py | 9 +--- scripts/mk_gparams_register_modules_cpp.py | 23 +++++---- scripts/mk_util.py | 3 +- src/ast/normal_forms/CMakeLists.txt | 2 + src/cmd_context/CMakeLists.txt | 2 + src/math/polynomial/CMakeLists.txt | 2 + src/util/CMakeLists.txt | 2 + 8 files changed, 76 insertions(+), 27 deletions(-) diff --git a/cmake/z3_add_component.cmake b/cmake/z3_add_component.cmake index 43a634ae1..489dc3ee2 100644 --- a/cmake/z3_add_component.cmake +++ b/cmake/z3_add_component.cmake @@ -56,6 +56,7 @@ endfunction() # [COMPONENT_DEPENDENCIES component1 [component2...]] # [PYG_FILES pygfile1 [pygfile2...]] # [TACTIC_HEADERS header_file1 [header_file2...]] +# [EXTRA_REGISTER_MODULE_HEADERS header_file1 [header_file2...]] # ) # # Declares a Z3 component (as a CMake "object library") with target name @@ -81,17 +82,28 @@ endfunction() # The optional ``PYG_FILES`` keyword should be followed by a list of one or # more ``.pyg`` files that should used to be generate # ``_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. macro(z3_add_component component_name) - CMAKE_PARSE_ARGUMENTS("Z3_MOD" "NOT_LIBZ3_COMPONENT" "" "SOURCES;COMPONENT_DEPENDENCIES;PYG_FILES;TACTIC_HEADERS" ${ARGN}) + CMAKE_PARSE_ARGUMENTS("Z3_MOD" + "NOT_LIBZ3_COMPONENT" + "" + "SOURCES;COMPONENT_DEPENDENCIES;PYG_FILES;TACTIC_HEADERS;EXTRA_REGISTER_MODULE_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}")) @@ -116,6 +128,18 @@ 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) @@ -136,6 +160,22 @@ macro(z3_add_component component_name) 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) + # 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 @@ -282,23 +322,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() diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 1a2a2dad7..1150b6333 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -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: diff --git a/scripts/mk_gparams_register_modules_cpp.py b/scripts/mk_gparams_register_modules_cpp.py index cf6e8da96..9614768ca 100755 --- a/scripts/mk_gparams_register_modules_cpp.py +++ b/scripts/mk_gparams_register_modules_cpp.py @@ -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)) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index b5924d0d1..165c27745 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2763,7 +2763,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)) diff --git a/src/ast/normal_forms/CMakeLists.txt b/src/ast/normal_forms/CMakeLists.txt index 30702cd8c..69288d92b 100644 --- a/src/ast/normal_forms/CMakeLists.txt +++ b/src/ast/normal_forms/CMakeLists.txt @@ -8,4 +8,6 @@ z3_add_component(normal_forms rewriter PYG_FILES nnf_params.pyg + EXTRA_REGISTER_MODULE_HEADERS + nnf.h ) diff --git a/src/cmd_context/CMakeLists.txt b/src/cmd_context/CMakeLists.txt index 8b2d10eec..f7b888343 100644 --- a/src/cmd_context/CMakeLists.txt +++ b/src/cmd_context/CMakeLists.txt @@ -18,4 +18,6 @@ z3_add_component(cmd_context interp rewriter solver + EXTRA_REGISTER_MODULE_HEADERS + context_params.h ) diff --git a/src/math/polynomial/CMakeLists.txt b/src/math/polynomial/CMakeLists.txt index 1d320d751..8c7d9ec02 100644 --- a/src/math/polynomial/CMakeLists.txt +++ b/src/math/polynomial/CMakeLists.txt @@ -11,5 +11,7 @@ z3_add_component(polynomial util PYG_FILES algebraic_params.pyg + EXTRA_REGISTER_MODULE_HEADERS + polynomial.h ) diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index b76f909d0..4d28fc6ad 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -59,4 +59,6 @@ z3_add_component(util util.cpp warning.cpp z3_exception.cpp + EXTRA_REGISTER_MODULE_HEADERS + env_params.h ) From d00892c9a6ffd927354dd8dd34caf08d2a16ac0f Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 21 Jun 2017 23:43:47 +0100 Subject: [PATCH 05/25] [CMake] Fix dependencies for generating `mem_initializer.cpp`. Previously CMake was not aware of which headers files the generation of `mem_initializer.cpp` depended on. Consequently this could result in broken incremental builds if * Existing headers that declare memory initializers/finalizers change. * New headers are added that declare memory initializers/finalizer. Now the `z3_add_component()` CMake function has been modifed so that it now takes an optional `MEMORY_INIT_FINALIZER_HEADERS` argument which allows the headers that declare memory initializers/finalizers to be explicitly listed. With this information CMake will now regenerate `mem_initializer.cpp` correctly. This required the `mk_mem_initializer_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 | 40 ++++++++++++++++++++++++++++--- scripts/mk_genfile_common.py | 9 ++----- scripts/mk_mem_initializer_cpp.py | 14 +++++------ scripts/mk_util.py | 3 ++- src/util/CMakeLists.txt | 7 ++++++ 5 files changed, 55 insertions(+), 18 deletions(-) diff --git a/cmake/z3_add_component.cmake b/cmake/z3_add_component.cmake index 489dc3ee2..b70838750 100644 --- a/cmake/z3_add_component.cmake +++ b/cmake/z3_add_component.cmake @@ -57,6 +57,7 @@ endfunction() # [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 @@ -93,11 +94,15 @@ endfunction() # 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;TACTIC_HEADERS;EXTRA_REGISTER_MODULE_HEADERS" ${ARGN}) + "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. @@ -176,6 +181,22 @@ macro(z3_add_component component_name) 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 @@ -297,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) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 1150b6333..21771cc04 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -731,7 +731,7 @@ def mk_install_tactic_cpp_internal(h_files_full_path, 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. @@ -745,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 = [] @@ -756,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: diff --git a/scripts/mk_mem_initializer_cpp.py b/scripts/mk_mem_initializer_cpp.py index b56fcbced..238595fa3 100755 --- a/scripts/mk_mem_initializer_cpp.py +++ b/scripts/mk_mem_initializer_cpp.py @@ -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)) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 165c27745..3ce104709 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2745,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)) diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 4d28fc6ad..7ed68c89f 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -61,4 +61,11 @@ z3_add_component(util 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 ) From e62e563e2de3a7ecd39d414feee9153ece150abf Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 21 Jun 2017 20:53:30 -0400 Subject: [PATCH 06/25] (mev) renamed variable to clarify that it is unused --- src/model/model_evaluator.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 61da4b3a0..4d3092cf6 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -202,8 +202,8 @@ struct evaluator_cfg : public default_rewriter_cfg { void expand_value(expr_ref& val) { vector stores; expr_ref else_case(m()); - bool args_are_unique; - if (m_ar.is_array(val) && extract_array_func_interp(val, stores, else_case, args_are_unique)) { + bool _unused; + if (m_ar.is_array(val) && extract_array_func_interp(val, stores, else_case, _unused)) { sort* srt = m().get_sort(val); val = m_ar.mk_const_array(srt, else_case); for (unsigned i = stores.size(); i > 0; ) { From d5ca902bf6240a5527c15e6b0744dec87a7d274b Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 21 Jun 2017 20:54:22 -0400 Subject: [PATCH 07/25] (mev) bug fix in expanding array equalities The stores were processed in the wrong order so that (store (store a x y) x u) was reduced to (store a x y) instead of (store a x u) --- src/model/model_evaluator.cpp | 42 ++++++++++++++++++----------------- 1 file changed, 22 insertions(+), 20 deletions(-) diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 4d3092cf6..f88beba4c 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -213,7 +213,7 @@ struct evaluator_cfg : public default_rewriter_cfg { args.append(stores[i].size(), stores[i].c_ptr()); val = m_ar.mk_store(args.size(), args.c_ptr()); } - } + } } bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) { @@ -291,13 +291,13 @@ struct evaluator_cfg : public default_rewriter_cfg { else { conj.push_back(m().mk_eq(else1, else2)); } - args1.push_back(a); - args2.push_back(b); if (args_are_unique1 && args_are_unique2 && !stores1.empty()) { - return mk_array_eq(stores1, else1, stores2, else2, conj, result); + return mk_array_eq_core(stores1, else1, stores2, else2, conj, result); } // TBD: this is too inefficient. + args1.push_back(a); + args2.push_back(b); stores1.append(stores2); for (unsigned i = 0; i < stores1.size(); ++i) { args1.resize(1); args1.append(stores1[i].size() - 1, stores1[i].c_ptr()); @@ -338,20 +338,22 @@ struct evaluator_cfg : public default_rewriter_cfg { typedef hashtable args_table; - br_status mk_array_eq(vector const& stores1, expr* else1, - vector const& stores2, expr* else2, - expr_ref_vector& conj, expr_ref& result) { + br_status mk_array_eq_core(vector const& stores1, expr* else1, + vector const& stores2, expr* else2, + expr_ref_vector& conj, expr_ref& result) { unsigned arity = stores1[0].size()-1; // TBD: fix arity. args_hash ah(arity); args_eq ae(arity); args_table table1(DEFAULT_HASHTABLE_INITIAL_CAPACITY, ah, ae); args_table table2(DEFAULT_HASHTABLE_INITIAL_CAPACITY, ah, ae); - for (unsigned i = 0; i < stores1.size(); ++i) { - table1.insert(stores1[i].c_ptr()); - } - for (unsigned i = stores2.size(); i > 0; ) { + // stores with smaller index take precedence + for (unsigned i = stores1.size(); i > 0; ) { --i; + table1.insert(stores1[i].c_ptr()); + } + + for (unsigned i = 0, sz = stores2.size(); i < sz; ++i) { if (table2.contains(stores2[i].c_ptr())) { // first insertion takes precedence. continue; @@ -361,7 +363,7 @@ struct evaluator_cfg : public default_rewriter_cfg { expr* val = stores2[i][arity]; if (table1.find(stores2[i].c_ptr(), args)) { switch (compare(args[arity], val)) { - case l_true: table1.remove(stores2[i].c_ptr()); break; + case l_true: table1.remove(args); break; case l_false: result = m().mk_false(); return BR_DONE; default: conj.push_back(m().mk_eq(val, args[arity])); break; } @@ -389,10 +391,10 @@ struct evaluator_cfg : public default_rewriter_cfg { lbool compare(expr* a, expr* b) { if (m().are_equal(a, b)) return l_true; if (m().are_distinct(a, b)) return l_false; - return l_undef; + return l_undef; } - + bool args_are_values(expr_ref_vector const& store, bool& are_unique) { bool are_values = true; for (unsigned j = 0; are_values && j + 1 < store.size(); ++j) { @@ -402,7 +404,7 @@ struct evaluator_cfg : public default_rewriter_cfg { SASSERT(!are_unique || are_values); return are_values; } - + bool extract_array_func_interp(expr* a, vector& stores, expr_ref& else_case, bool& are_unique) { SASSERT(m_ar.is_array(a)); @@ -417,14 +419,14 @@ struct evaluator_cfg : public default_rewriter_cfg { stores.push_back(store); a = to_app(a)->get_arg(0); } - + if (m_ar.is_const(a)) { else_case = to_app(a)->get_arg(0); return true; } - + if (!m_ar.is_as_array(a)) { - TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m()) << "\n";); + TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m()) << "\n";); return false; } @@ -444,7 +446,7 @@ struct evaluator_cfg : public default_rewriter_cfg { } } stores.push_back(store); - } + } else_case = g->get_else(); if (!else_case) { TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m()) << "\n"; @@ -524,7 +526,7 @@ unsigned model_evaluator::get_num_steps() const { void model_evaluator::cleanup(params_ref const & p) { model_core & md = m_imp->cfg().m_model; dealloc(m_imp); - m_imp = alloc(imp, md, p); + m_imp = alloc(imp, md, p); } void model_evaluator::reset(params_ref const & p) { From 493a3a63125230cc567380543d6679c749334e15 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 20 Jun 2017 23:39:38 -0400 Subject: [PATCH 08/25] (mev) call expand_value only at the end There is no need to expand array values throughout evaluation. They are expanded during array equality checking (if requested), and can be expanded at the very end of evaluation (if needed). --- src/model/model_evaluator.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index f88beba4c..279cfde3b 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -125,7 +125,6 @@ struct evaluator_cfg : public default_rewriter_cfg { expr * val = m_model.get_const_interp(f); if (val != 0) { result = val; - expand_value(result); return BR_DONE; } @@ -274,7 +273,6 @@ struct evaluator_cfg : public default_rewriter_cfg { return BR_FAILED; } - // disabled until made more efficient vector stores1, stores2; bool args_are_unique1, args_are_unique2; expr_ref else1(m()), else2(m()); @@ -489,6 +487,10 @@ struct model_evaluator::imp : public rewriter_tpl { m_cfg(md.get_manager(), md, p) { set_cancel_check(false); } + + void expand_value (expr_ref &val) { + m_cfg.expand_value (val); + } }; model_evaluator::model_evaluator(model_core & md, params_ref const & p) { @@ -537,14 +539,12 @@ void model_evaluator::reset(params_ref const & p) { void model_evaluator::operator()(expr * t, expr_ref & result) { TRACE("model_evaluator", tout << mk_ismt2_pp(t, m()) << "\n";); m_imp->operator()(t, result); + m_imp->expand_value(result); } expr_ref model_evaluator::operator()(expr * t) { TRACE("model_evaluator", tout << mk_ismt2_pp(t, m()) << "\n";); expr_ref result(m()); - m_imp->operator()(t, result); + this->operator()(t, result); return result; } - - - From 2d49119d2ab112f43b94b5f561771bed4ca126c6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 21 Jun 2017 18:55:35 -0700 Subject: [PATCH 09/25] add note to Context documentation about scoped uses of contexts #1077 --- src/api/java/Context.java | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/api/java/Context.java b/src/api/java/Context.java index db7a08711..2609dbb29 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -25,6 +25,12 @@ import java.util.Map; /** * The main interaction with Z3 happens via the Context. + * For applications that spawn an unbounded number of contexts, + * the proper use is within a try-with-resources + * scope so that the Context object gets garbage collected in + * a predictable way. Contexts maintain all data-structures + * related to terms and formulas that are created relative + * to them. **/ public class Context implements AutoCloseable { private final long m_ctx; From 972ab6298cde5cdeade5d7f456e9738fe2c8dd6b Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 21 Jun 2017 22:59:52 -0400 Subject: [PATCH 10/25] (mev) only reduce function interpretation --- src/model/model_evaluator.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 279cfde3b..805ed8e5d 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -432,6 +432,7 @@ struct evaluator_cfg : public default_rewriter_cfg { func_interp* g = m_model.get_func_interp(f); unsigned sz = g->num_entries(); unsigned arity = f->get_arity(); + unsigned base_sz = stores.size(); for (unsigned i = 0; i < sz; ++i) { expr_ref_vector store(m()); func_entry const* fe = g->get_entry(i); @@ -456,7 +457,7 @@ struct evaluator_cfg : public default_rewriter_cfg { TRACE("model_evaluator", tout << "non-ground else case " << mk_pp(a, m()) << "\n" << else_case << "\n";); return false; } - for (unsigned i = stores.size(); are_values && i > 0; ) { + for (unsigned i = stores.size(); are_values && i > base_sz; ) { --i; if (m().are_equal(else_case, stores[i].back())) { for (unsigned j = i + 1; j < stores.size(); ++j) { From ed038c2a107854d64d292406b32b34d608818cdd Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 22 Jun 2017 09:42:22 +0100 Subject: [PATCH 11/25] [CMake] Fix CMake warning about CMP0042 on macOS --- CMakeLists.txt | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index 5ed7ee06a..6f39cac13 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -14,6 +14,11 @@ if (POLICY CMP0054) cmake_policy(SET CMP0054 OLD) endif() +if (POLICY CMP0042) + # Enable `MACOSX_RPATH` by default. + cmake_policy(SET CMP0042 NEW) +endif() + set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") project(Z3 CXX) From 2a5f1d6e93d032172f3ea4f505e4f192a8652c5f Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 22 Jun 2017 10:32:35 -0700 Subject: [PATCH 12/25] add a template instantination Signed-off-by: Lev Nachmanson --- src/util/lp/dense_matrix_instances.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/util/lp/dense_matrix_instances.cpp b/src/util/lp/dense_matrix_instances.cpp index 1e931211d..95ba01801 100644 --- a/src/util/lp/dense_matrix_instances.cpp +++ b/src/util/lp/dense_matrix_instances.cpp @@ -11,6 +11,7 @@ template void lean::dense_matrix::apply_from_left(vector template lean::dense_matrix::dense_matrix(lean::matrix const*); template lean::dense_matrix::dense_matrix(unsigned int, unsigned int); template lean::dense_matrix& lean::dense_matrix::operator=(lean::dense_matrix const&); +template lean::dense_matrix::dense_matrix(unsigned int, unsigned int); template lean::dense_matrix >::dense_matrix(lean::matrix > const*); template void lean::dense_matrix >::apply_from_left(vector&); template lean::dense_matrix lean::operator*(lean::matrix&, lean::matrix&); From 7386f2e04535485c92733aab76290e26c3c45741 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 22 Jun 2017 14:18:53 -0700 Subject: [PATCH 13/25] #1101 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 54909939f..0e1c150c0 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1313,17 +1313,18 @@ namespace opt { rational r = n.get_rational(); rational eps = n.get_infinitesimal(); expr_ref_vector args(m); + bool is_int = eps.is_zero() && r.is_int(); if (!inf.is_zero()) { - expr* oo = m.mk_const(symbol("oo"), m_arith.mk_int()); + expr* oo = m.mk_const(symbol("oo"), is_int ? m_arith.mk_int() : m_arith.mk_real()); if (inf.is_one()) { args.push_back(oo); } else { - args.push_back(m_arith.mk_mul(m_arith.mk_numeral(inf, inf.is_int()), oo)); + args.push_back(m_arith.mk_mul(m_arith.mk_numeral(inf, is_int), oo)); } } if (!r.is_zero()) { - args.push_back(m_arith.mk_numeral(r, r.is_int())); + args.push_back(m_arith.mk_numeral(r, is_int)); } if (!eps.is_zero()) { expr* ep = m.mk_const(symbol("epsilon"), m_arith.mk_real()); @@ -1331,7 +1332,7 @@ namespace opt { args.push_back(ep); } else { - args.push_back(m_arith.mk_mul(m_arith.mk_numeral(eps, eps.is_int()), ep)); + args.push_back(m_arith.mk_mul(m_arith.mk_numeral(eps, is_int), ep)); } } switch(args.size()) { From 9874db7458ddcda1375aedb9237a176f95e2c818 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Fri, 23 Jun 2017 09:36:09 -0400 Subject: [PATCH 14/25] [CMake] typos in cmake --- src/api/CMakeLists.txt | 2 +- src/ast/pattern/CMakeLists.txt | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt index 8e796168f..79c5fc1c9 100644 --- a/src/api/CMakeLists.txt +++ b/src/api/CMakeLists.txt @@ -7,7 +7,7 @@ set(generated_files # Sanity check foreach (gen_file ${generated_files}) if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/${gen_file}") - message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/${gen_files}\"" + message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/${gen_file}\"" ${z3_polluted_tree_msg}) endif() endforeach() diff --git a/src/ast/pattern/CMakeLists.txt b/src/ast/pattern/CMakeLists.txt index 59e0545a1..6e8301afc 100644 --- a/src/ast/pattern/CMakeLists.txt +++ b/src/ast/pattern/CMakeLists.txt @@ -2,7 +2,7 @@ # 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\"" + message(FATAL_ERROR "The generated file \"${CMAKE_CURRENT_SOURCE_DIR}/database.h\"" ${z3_polluted_tree_msg}) endif() From 0dead22dca50d07207e0fd816be4b3e441cdb0b1 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Fri, 23 Jun 2017 09:36:44 -0400 Subject: [PATCH 15/25] fix missing initialization --- src/muz/transforms/dl_mk_quantifier_abstraction.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp index 5c0d442df..a22a67416 100644 --- a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp +++ b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp @@ -142,7 +142,8 @@ namespace datalog { m(ctx.get_manager()), m_ctx(ctx), a(m), - m_refs(m) { + m_refs(m), + m_mc(NULL){ } mk_quantifier_abstraction::~mk_quantifier_abstraction() { From c7fbab0c1160b069a2f6458e621a2f04185a7d8a Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Fri, 23 Jun 2017 09:37:19 -0400 Subject: [PATCH 16/25] propagate rule names during xform --- src/muz/rel/dl_mk_similarity_compressor.cpp | 2 +- src/muz/rel/dl_mk_simple_joins.cpp | 2 +- src/muz/transforms/dl_mk_slice.cpp | 2 +- src/muz/transforms/dl_mk_unbound_compressor.cpp | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/muz/rel/dl_mk_similarity_compressor.cpp b/src/muz/rel/dl_mk_similarity_compressor.cpp index 75caba6ae..b65ed455c 100644 --- a/src/muz/rel/dl_mk_similarity_compressor.cpp +++ b/src/muz/rel/dl_mk_similarity_compressor.cpp @@ -426,7 +426,7 @@ namespace datalog { new_negs.push_back(false); rule * new_rule = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(), - new_negs.c_ptr()); + new_negs.c_ptr(), r->name()); m_result_rules.push_back(new_rule); //TODO: allow for a rule to have multiple parent objects diff --git a/src/muz/rel/dl_mk_simple_joins.cpp b/src/muz/rel/dl_mk_simple_joins.cpp index e428fdd2e..a8e54085d 100644 --- a/src/muz/rel/dl_mk_simple_joins.cpp +++ b/src/muz/rel/dl_mk_simple_joins.cpp @@ -726,7 +726,7 @@ namespace datalog { } rule * new_rule = m_context.get_rule_manager().mk(orig_r->get_head(), tail.size(), tail.c_ptr(), - negs.c_ptr()); + negs.c_ptr(), orig_r->name()); new_rule->set_accounting_parent_object(m_context, orig_r); m_context.get_rule_manager().mk_rule_rewrite_proof(*orig_r, *new_rule); diff --git a/src/muz/transforms/dl_mk_slice.cpp b/src/muz/transforms/dl_mk_slice.cpp index aa910002d..cefda74e8 100644 --- a/src/muz/transforms/dl_mk_slice.cpp +++ b/src/muz/transforms/dl_mk_slice.cpp @@ -789,7 +789,7 @@ namespace datalog { tail.push_back(to_app(e)); } - new_rule = rm.mk(head.get(), tail.size(), tail.c_ptr(), (const bool*) 0); + new_rule = rm.mk(head.get(), tail.size(), tail.c_ptr(), (const bool*) 0, r.name()); rm.fix_unbound_vars(new_rule, false); diff --git a/src/muz/transforms/dl_mk_unbound_compressor.cpp b/src/muz/transforms/dl_mk_unbound_compressor.cpp index 41b181450..78133aab7 100644 --- a/src/muz/transforms/dl_mk_unbound_compressor.cpp +++ b/src/muz/transforms/dl_mk_unbound_compressor.cpp @@ -173,7 +173,7 @@ namespace datalog { return l_false; } else { - rule_ref new_rule(m_context.get_rule_manager().mk(r, chead), m_context.get_rule_manager()); + rule_ref new_rule(m_context.get_rule_manager().mk(r, chead, r->name()), m_context.get_rule_manager()); new_rule->set_accounting_parent_object(m_context, r); m_head_occurrence_ctr.dec(m_rules.get(rule_index)->get_decl()); From cd4bb5beaf723f2bf0359aaef5076542b251990d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 23 Jun 2017 11:34:10 -0700 Subject: [PATCH 17/25] another fix for #1101 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index a5a34a079..76e721faa 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2386,16 +2386,16 @@ namespace smt { app_ref mk_obj(theory_var v) { lean::var_index vi = m_theory_var2var_index[v]; + bool is_int = a.is_int(get_enode(v)->get_owner()); if (m_solver->is_term(vi)) { expr_ref_vector args(m); const lean::lar_term& term = m_solver->get_term(vi); for (auto & ti : term.m_coeffs) { theory_var w = m_var_index2theory_var[ti.first]; expr* o = get_enode(w)->get_owner(); - args.push_back(a.mk_mul(a.mk_numeral(ti.second, a.is_int(o)), o)); + args.push_back(a.mk_mul(a.mk_numeral(ti.second, is_int), o)); } - rational r = term.m_v; - args.push_back(a.mk_numeral(r, r.is_int())); + args.push_back(a.mk_numeral(term.m_v, is_int)); return app_ref(a.mk_add(args.size(), args.c_ptr()), m); } else { @@ -2408,11 +2408,12 @@ namespace smt { rational r = val.get_rational(); bool is_strict = val.get_infinitesimal().is_pos(); app_ref b(m); + bool is_int = a.is_int(get_enode(v)->get_owner()); if (is_strict) { - b = a.mk_le(mk_obj(v), a.mk_numeral(r, r.is_int())); + b = a.mk_le(mk_obj(v), a.mk_numeral(r, is_int)); } else { - b = a.mk_ge(mk_obj(v), a.mk_numeral(r, r.is_int())); + b = a.mk_ge(mk_obj(v), a.mk_numeral(r, is_int)); } if (!ctx().b_internalized(b)) { fm.insert(b->get_decl()); From 9d1852343c47ca6abd05752a60650f521bf399e4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 23 Jun 2017 16:34:38 -0700 Subject: [PATCH 18/25] add separate get-objectives command #1107 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 3 +-- src/opt/opt_cmds.cpp | 23 +++++++++++++++++++++++ 2 files changed, 24 insertions(+), 2 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index af16f5796..d252c3629 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1360,7 +1360,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions throw ex; } catch (z3_exception & ex) { - get_opt()->display_assignment(regular_stream()); throw cmd_exception(ex.msg()); } if (m_processing_pareto && r != l_true) { @@ -1398,7 +1397,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions } validate_check_sat_result(r); if (was_opt && r != l_false && !m_processing_pareto) { - get_opt()->display_assignment(regular_stream()); + // get_opt()->display_assignment(regular_stream()); } if (r == l_true && m_params.m_dump_models) { diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index a5c163562..0264a6a24 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -143,12 +143,35 @@ public: } }; +class get_objectives_cmd : public cmd { + opt::context* m_opt; +public: + get_objectives_cmd(opt::context* opt): + cmd("get-objectives"), + m_opt(opt) + {} + + virtual void reset(cmd_context & ctx) { } + virtual char const * get_usage() const { return "(get-objectives)"; } + virtual char const * get_descr(cmd_context & ctx) const { return "retrieve the objective values (after optimization)"; } + virtual unsigned get_arity() const { return 0; } + virtual void prepare(cmd_context & ctx) {} + virtual void failure_cleanup(cmd_context & ctx) { + reset(ctx); + } + + virtual void execute(cmd_context & ctx) { + get_opt(ctx, m_opt).display_assignment(ctx.regular_stream()); + } +}; + void install_opt_cmds(cmd_context & ctx, opt::context* opt) { ctx.insert(alloc(assert_soft_cmd, opt)); ctx.insert(alloc(min_maximize_cmd, true, opt)); ctx.insert(alloc(min_maximize_cmd, false, opt)); + ctx.insert(alloc(get_objectives_cmd, opt)); } From 1681419052d156240b76c4e85b5750b82ecc6a88 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 23 Jun 2017 16:50:33 -0700 Subject: [PATCH 19/25] adding change notes to release notes for a future release Signed-off-by: Nikolaj Bjorner --- RELEASE_NOTES | 10 ++++++++++ src/smt/smt_context.cpp | 8 +++++--- 2 files changed, 15 insertions(+), 3 deletions(-) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 357c17e78..ec05160da 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -1,5 +1,15 @@ RELEASE NOTES +Version 4.5.x +============= +- New features (including): + - A new string solver from University of Waterloo + - A new linear real arithmetic solver + - Changed behavior for optimization commands from the SMT2 command-line interface. + Objective values are no longer printed by default. They can be retrieved by + issuing the command (get-objectives). Pareto front objectives are accessed by + issuing multiple (check-sat) calls until it returns unsat. + Version 4.5.0 ============= diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 0c32f3c76..4e56d3004 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4332,10 +4332,9 @@ namespace smt { ); failure fl = get_last_search_failure(); if (fl == MEMOUT || fl == CANCELED || fl == TIMEOUT || fl == NUM_CONFLICTS || fl == RESOURCE_LIMIT) { - return; + TRACE("get_model", tout << "last search failure: " << fl << "\n";); } - - if (m_fparams.m_model || m_fparams.m_model_on_final_check || m_qmanager->model_based()) { + else if (m_fparams.m_model || m_fparams.m_model_on_final_check || m_qmanager->model_based()) { m_model_generator->reset(); m_proto_model = m_model_generator->mk_model(); m_qmanager->adjust_model(m_proto_model.get()); @@ -4346,6 +4345,9 @@ namespace smt { if (m_fparams.m_model_compact) m_proto_model->compress(); TRACE("mbqi_bug", tout << "after cleanup:\n"; model_pp(tout, *m_proto_model);); + } + else { + } } From 1631a68981d6905c0e0763e4bf143628e0c0b86d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 23 Jun 2017 16:57:50 -0700 Subject: [PATCH 20/25] make the option soup dependencies more user-friendly, #1109 Signed-off-by: Nikolaj Bjorner --- src/smt/tactic/smt_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index 9e3eddafa..64bae0a48 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -253,7 +253,7 @@ public: if (m_ctx->canceled()) { throw tactic_exception(Z3_CANCELED_MSG); } - if (m_fail_if_inconclusive) { + if (m_fail_if_inconclusive && !m_candidate_models) { std::stringstream strm; strm << "smt tactic failed to show goal to be sat/unsat " << m_ctx->last_failure_as_string(); throw tactic_exception(strm.str().c_str()); From ae8a089e254a5820f00aa7dfb611bd3d6c9c7028 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 24 Jun 2017 13:47:51 +0100 Subject: [PATCH 21/25] [CMake] Fix missing sanitization in `z3_add_cxx_flag flag()` function which caused CMake 2.8.12 to hit an error when handling the `-std=c++11` flag. --- cmake/z3_add_cxx_flag.cmake | 1 + 1 file changed, 1 insertion(+) diff --git a/cmake/z3_add_cxx_flag.cmake b/cmake/z3_add_cxx_flag.cmake index 8bffd7de3..6e756d3b9 100644 --- a/cmake/z3_add_cxx_flag.cmake +++ b/cmake/z3_add_cxx_flag.cmake @@ -8,6 +8,7 @@ function(z3_add_cxx_flag flag) string(REPLACE "=" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") string(REPLACE " " "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") string(REPLACE ":" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") + string(REPLACE "+" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") unset(HAS_${SANITIZED_FLAG_NAME}) CHECK_CXX_COMPILER_FLAG("${flag}" HAS_${SANITIZED_FLAG_NAME}) if (z3_add_flag_REQUIRED AND NOT HAS_${SANITIZED_FLAG_NAME}) From 5a8205cb0cc4a8c6f1293b11a5a68b3fa98a2c10 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 24 Jun 2017 14:05:25 +0100 Subject: [PATCH 22/25] [CMake] Unbreak detection of pthreads for CMake versions < 3.4 --- CMakeLists.txt | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index 6f39cac13..971ea9cbd 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -22,6 +22,13 @@ endif() set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") project(Z3 CXX) +if ("${CMAKE_VERSION}" VERSION_LESS "3.4") + # FIXME: Drop this when we upgrade to newer CMake versions. + # HACK: Although we don't need C language support if it is not + # enabled CMake's `FindThreads` module fails in old CMake versions. + enable_language(C) +endif() + ################################################################################ # Project version ################################################################################ From 489077a3eb800b74605c965fa3c152fecf257110 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 24 Jun 2017 14:16:48 +0100 Subject: [PATCH 23/25] [CMake] Remove use of `INSTALL_PREFIX` argument to `configure_package_config_file()`. This argument wasn't available until CMake 3.1 and we don't appear to be really using it anyway. --- CMakeLists.txt | 1 - 1 file changed, 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 971ea9cbd..bf894a5c9 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -540,7 +540,6 @@ configure_package_config_file("${CMAKE_SOURCE_DIR}/cmake/Z3Config.cmake.in" Z3_FIRST_PACKAGE_INCLUDE_DIR Z3_SECOND_PACKAGE_INCLUDE_DIR Z3_CXX_PACKAGE_INCLUDE_DIR - INSTALL_PREFIX "${CMAKE_BINARY_DIR}" ) unset(Z3_FIRST_PACKAGE_INCLUDE_DIR) unset(Z3_SECOND_PACKAGE_INCLUDE_DIR) From 3229bedb36dd8d4ab6f6a809709c2270fbe0d83d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 24 Jun 2017 14:41:33 +0100 Subject: [PATCH 24/25] [CMake] Unbreak the configure step for CMake 2.8.12 --- CMakeLists.txt | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index bf894a5c9..8ed5c7d5e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -524,10 +524,18 @@ add_subdirectory(src) # use Z3 via CMake. ################################################################################ include(CMakePackageConfigHelpers) -export(EXPORT Z3_EXPORTED_TARGETS - NAMESPACE z3:: - FILE "${CMAKE_BINARY_DIR}/Z3Targets.cmake" -) +if ("${CMAKE_VERSION}" VERSION_LESS "3.0") + # FIXME: Remove this once we drop support for CMake 2.8.12 + export(TARGETS libz3 + NAMESPACE z3:: + FILE "${CMAKE_BINARY_DIR}/Z3Targets.cmake" + ) +else() + export(EXPORT Z3_EXPORTED_TARGETS + NAMESPACE z3:: + FILE "${CMAKE_BINARY_DIR}/Z3Targets.cmake" + ) +endif() set(Z3_FIRST_PACKAGE_INCLUDE_DIR "${CMAKE_BINARY_DIR}/src/api") set(Z3_SECOND_PACKAGE_INCLUDE_DIR "${CMAKE_SOURCE_DIR}/src/api") set(Z3_CXX_PACKAGE_INCLUDE_DIR "${CMAKE_SOURCE_DIR}/src/api/c++") From 80c0c4f66362d7815e6062c391be2d68b80a6f11 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 24 Jun 2017 15:15:27 +0100 Subject: [PATCH 25/25] [CMake] Fix detection of git description and hash for CMake 2.8.12 --- CMakeLists.txt | 4 ++-- cmake/git_utils.cmake | 8 ++++++-- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 8ed5c7d5e..c8ecb5295 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -109,7 +109,7 @@ if (EXISTS "${GIT_DIR}") endif() message(STATUS "Using Git hash in version output: ${Z3GITHASH}") # This mimics the behaviour of the old build system. - string(APPEND Z3_FULL_VERSION_STR " ${Z3GITHASH}") + set(Z3_FULL_VERSION_STR "${Z3_FULL_VERSION_STR} ${Z3GITHASH}") else() message(STATUS "Not using Git hash in version output") unset(Z3GITHASH) # Used in configure_file() @@ -122,7 +122,7 @@ if (EXISTS "${GIT_DIR}") endif() message(STATUS "Using Git description in version output: ${Z3_GIT_DESCRIPTION}") # This mimics the behaviour of the old build system. - string(APPEND Z3_FULL_VERSION_STR " ${Z3_GIT_DESCRIPTION}") + set(Z3_FULL_VERSION_STR "${Z3_FULL_VERSION_STR} ${Z3_GIT_DESCRIPTION}") else() message(STATUS "Not including git descrption in version") endif() diff --git a/cmake/git_utils.cmake b/cmake/git_utils.cmake index aa7f38825..f98aca205 100644 --- a/cmake/git_utils.cmake +++ b/cmake/git_utils.cmake @@ -99,7 +99,9 @@ function(get_git_head_hash GIT_DIR OUTPUT_VAR) message(FATAL_ERROR \""${GIT_DIR}\" is not an absolute path") endif() find_package(Git) - if (NOT Git_FOUND) + # NOTE: Use `GIT_FOUND` rather than `Git_FOUND` which was only + # available in CMake >= 3.5 + if (NOT GIT_FOUND) set(${OUTPUT_VAR} "GIT-NOTFOUND" PARENT_SCOPE) return() endif() @@ -146,7 +148,9 @@ function(get_git_head_describe GIT_DIR OUTPUT_VAR) message(FATAL_ERROR \""${GIT_DIR}\" is not an absolute path") endif() find_package(Git) - if (NOT Git_FOUND) + # NOTE: Use `GIT_FOUND` rather than `Git_FOUND` which was only + # available in CMake >= 3.5 + if (NOT GIT_FOUND) set(${OUTPUT_VAR} "GIT-NOTFOUND" PARENT_SCOPE) return() endif()