diff --git a/CMakeLists.txt b/CMakeLists.txt index 5ed7ee06a..c8ecb5295 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -14,9 +14,21 @@ 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) +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 ################################################################################ @@ -97,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() @@ -110,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() @@ -512,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++") @@ -528,7 +548,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) 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/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() diff --git a/cmake/z3_add_component.cmake b/cmake/z3_add_component.cmake index b90aa2fe7..b70838750 100644 --- a/cmake/z3_add_component.cmake +++ b/cmake/z3_add_component.cmake @@ -55,6 +55,9 @@ endfunction() # SOURCES source1 [source2...] # [COMPONENT_DEPENDENCIES component1 [component2...]] # [PYG_FILES pygfile1 [pygfile2...]] +# [TACTIC_HEADERS header_file1 [header_file2...]] +# [EXTRA_REGISTER_MODULE_HEADERS header_file1 [header_file2...]] +# [MEMORY_INIT_FINALIZER_HEADERS header_file1 [header_file2...]] # ) # # Declares a Z3 component (as a CMake "object library") with target name @@ -80,14 +83,32 @@ endfunction() # The optional ``PYG_FILES`` keyword should be followed by a list of one or # more ``.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. +# +# The optional ``MEMORY_INIT_FINALIZER_HEADERS`` keyword should be followed by a list +# of one or more header files that contain memory initializer/finalizer declarations +# (i.e. ``ADD_INITIALIZER()`` or ``ADD_FINALIZER()``). macro(z3_add_component component_name) - CMAKE_PARSE_ARGUMENTS("Z3_MOD" "NOT_LIBZ3_COMPONENT" "" "SOURCES;COMPONENT_DEPENDENCIES;PYG_FILES" ${ARGN}) + CMAKE_PARSE_ARGUMENTS("Z3_MOD" + "NOT_LIBZ3_COMPONENT" + "" + "SOURCES;COMPONENT_DEPENDENCIES;PYG_FILES;TACTIC_HEADERS;EXTRA_REGISTER_MODULE_HEADERS;MEMORY_INIT_FINALIZER_HEADERS" ${ARGN}) message(STATUS "Adding component ${component_name}") # Note: We don't check the sources exist here because # they might be generated files that don't exist yet. set(_list_generated_headers "") + set_property(GLOBAL PROPERTY Z3_${component_name}_REGISTER_MODULE_HEADERS "") foreach (pyg_file ${Z3_MOD_PYG_FILES}) set(_full_pyg_file_path "${CMAKE_CURRENT_SOURCE_DIR}/${pyg_file}") if (NOT (EXISTS "${_full_pyg_file_path}")) @@ -112,11 +133,70 @@ macro(z3_add_component component_name) VERBATIM ) list(APPEND _list_generated_headers "${_full_output_file_path}") + + # FIXME: This implicit dependency of a generated file depending on + # generated files was inherited from the old build system. + + # Typically generated headers contain `REG_PARAMS()`, `REG_MODULE_PARAMS()` + # and `REG_MODULE_DESCRIPTION()` declarations so add to the list of + # header files to scan. + set_property(GLOBAL + APPEND + PROPERTY Z3_${component_name}_REGISTER_MODULE_HEADERS + "${_full_output_file_path}" + ) endforeach() unset(_full_include_dir_path) unset(_full_output_file_path) unset(_output_file) + # Add tactic/probe headers to global property + set_property(GLOBAL PROPERTY Z3_${component_name}_TACTIC_HEADERS "") + foreach (tactic_header ${Z3_MOD_TACTIC_HEADERS}) + set(_full_tactic_header_file_path "${CMAKE_CURRENT_SOURCE_DIR}/${tactic_header}") + if (NOT (EXISTS "${_full_tactic_header_file_path}")) + message(FATAL_ERROR "\"${_full_tactic_header_file_path}\" does not exist") + endif() + set_property(GLOBAL + APPEND + PROPERTY Z3_${component_name}_TACTIC_HEADERS + "${_full_tactic_header_file_path}" + ) + endforeach() + unset(_full_tactic_header_file_path) + + # Add additional register module headers + foreach (extra_register_module_header ${Z3_MOD_EXTRA_REGISTER_MODULE_HEADERS}) + set(_full_extra_register_module_header_path + "${CMAKE_CURRENT_SOURCE_DIR}/${extra_register_module_header}" + ) + if (NOT (EXISTS "${_full_extra_register_module_header_path}")) + message(FATAL_ERROR "\"${_full_extra_register_module_header_path}\" does not exist") + endif() + set_property(GLOBAL + APPEND + PROPERTY Z3_${component_name}_REGISTER_MODULE_HEADERS + "${_full_extra_register_module_header_path}" + ) + endforeach() + unset(_full_extra_register_module_header) + + # Add memory initializer/finalizer headers to global property + set_property(GLOBAL PROPERTY Z3_${component_name}_MEM_INIT_FINALIZER_HEADERS "") + foreach (memory_init_finalizer_header ${Z3_MOD_MEMORY_INIT_FINALIZER_HEADERS}) + set(_full_memory_init_finalizer_header_path + "${CMAKE_CURRENT_SOURCE_DIR}/${memory_init_finalizer_header}") + if (NOT (EXISTS "${_full_memory_init_finalizer_header_path}")) + message(FATAL_ERROR "\"${_full_memory_init_finalizer_header_path}\" does not exist") + endif() + set_property(GLOBAL + APPEND + PROPERTY Z3_${component_name}_MEM_INIT_FINALIZER_HEADERS + "${_full_memory_init_finalizer_header_path}" + ) + endforeach() + unset(_full_memory_init_finalizer_header_path) + # Using "object" libraries here means we have a convenient # name to refer to a component in CMake but we don't actually # create a static/library from them. This allows us to easily @@ -191,25 +271,33 @@ macro(z3_add_install_tactic_rule) ) endif() z3_expand_dependencies(_expanded_components ${ARGN}) - # Get paths to search - set(_search_paths "") + + # Get header files that declare tactics/probes + set(_tactic_header_files "") foreach (dependency ${_expanded_components}) - get_property(_dep_include_dirs GLOBAL PROPERTY Z3_${dependency}_INCLUDES) - list(APPEND _search_paths ${_dep_include_dirs}) + get_property(_component_tactic_header_files + GLOBAL + PROPERTY Z3_${dependency}_TACTIC_HEADERS + ) + list(APPEND _tactic_header_files ${_component_tactic_header_files}) endforeach() + unset(_component_tactic_header_files) + list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}") add_custom_command(OUTPUT "install_tactic.cpp" COMMAND "${PYTHON_EXECUTABLE}" "${CMAKE_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py" "${CMAKE_CURRENT_BINARY_DIR}" - ${_search_paths} + ${_tactic_header_files} DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py" ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} - ${_expanded_components} + ${_tactic_header_files} COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp\"" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} VERBATIM ) + unset(_expanded_components) + unset(_tactic_header_files) endmacro() macro(z3_add_memory_initializer_rule) @@ -230,18 +318,31 @@ macro(z3_add_memory_initializer_rule) list(APPEND _search_paths ${_dep_include_dirs}) endforeach() list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}") + + # Get header files that declare initializers and finalizers + set(_mem_init_finalize_headers "") + foreach (dependency ${_expanded_components}) + get_property(_dep_mem_init_finalize_headers + GLOBAL + PROPERTY Z3_${dependency}_MEM_INIT_FINALIZER_HEADERS + ) + list(APPEND _mem_init_finalize_headers ${_dep_mem_init_finalize_headers}) + endforeach() + add_custom_command(OUTPUT "mem_initializer.cpp" COMMAND "${PYTHON_EXECUTABLE}" "${CMAKE_SOURCE_DIR}/scripts/mk_mem_initializer_cpp.py" "${CMAKE_CURRENT_BINARY_DIR}" - ${_search_paths} + ${_mem_init_finalize_headers} DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_mem_initializer_cpp.py" ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} - ${_expanded_components} + ${_mem_init_finalize_headers} COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp\"" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} VERBATIM ) + unset(_mem_init_finalize_headers) + unset(_expanded_components) endmacro() macro(z3_add_gparams_register_modules_rule) @@ -255,23 +356,27 @@ macro(z3_add_gparams_register_modules_rule) ) endif() z3_expand_dependencies(_expanded_components ${ARGN}) - # Get paths to search - set(_search_paths "") + + # Get the list of header files to parse + set(_register_module_header_files "") foreach (dependency ${_expanded_components}) - get_property(_dep_include_dirs GLOBAL PROPERTY Z3_${dependency}_INCLUDES) - list(APPEND _search_paths ${_dep_include_dirs}) + get_property(_component_register_module_header_files GLOBAL PROPERTY Z3_${dependency}_REGISTER_MODULE_HEADERS) + list(APPEND _register_module_header_files ${_component_register_module_header_files}) endforeach() - list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}") + unset(_component_register_module_header_files) + add_custom_command(OUTPUT "gparams_register_modules.cpp" COMMAND "${PYTHON_EXECUTABLE}" "${CMAKE_SOURCE_DIR}/scripts/mk_gparams_register_modules_cpp.py" "${CMAKE_CURRENT_BINARY_DIR}" - ${_search_paths} + ${_register_module_header_files} DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_gparams_register_modules_cpp.py" ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} - ${_expanded_components} + ${_register_module_header_files} COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp\"" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} VERBATIM ) + unset(_expanded_components) + unset(_register_module_header_files) endmacro() 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}) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 98346f99f..21771cc04 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: @@ -651,7 +646,7 @@ def mk_gparams_register_modules_internal(component_src_dirs, path): # Functions/data structures for generating ``install_tactics.cpp`` ############################################################################### -def mk_install_tactic_cpp_internal(component_src_dirs, path): +def mk_install_tactic_cpp_internal(h_files_full_path, path): """ Generate a ``install_tactics.cpp`` file in the directory ``path``. Returns the path the generated file. @@ -662,9 +657,10 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path): void install_tactics(tactic_manager & ctx) ``` - It installs all tactics found in the given component directories - ``component_src_dirs`` The procedure looks for ``ADD_TACTIC`` commands - in the ``.h`` and ``.hpp`` files of these components. + It installs all tactics declared in the given header files + ``h_files_full_path`` The procedure looks for ``ADD_TACTIC`` and + ``ADD_PROBE``commands in the ``.h`` and ``.hpp`` files of these + components. """ ADD_TACTIC_DATA = [] ADD_PROBE_DATA = [] @@ -679,7 +675,7 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path): 'ADD_PROBE': ADD_PROBE, } - assert isinstance(component_src_dirs, list) + assert isinstance(h_files_full_path, list) assert check_dir_exists(path) fullname = os.path.join(path, 'install_tactic.cpp') fout = open(fullname, 'w') @@ -689,11 +685,6 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path): fout.write('#include"cmd_context.h"\n') tactic_pat = re.compile('[ \t]*ADD_TACTIC\(.*\)') probe_pat = re.compile('[ \t]*ADD_PROBE\(.*\)') - h_files_full_path = [] - for component_src_dir in sorted(component_src_dirs): - h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir)) - h_files = list(map(lambda p: os.path.join(component_src_dir, p), h_files)) - h_files_full_path.extend(h_files) for h_file in sorted_headers_by_component(h_files_full_path): added_include = False with open(h_file, 'r') as fin: @@ -740,7 +731,7 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path): # Functions for generating ``mem_initializer.cpp`` ############################################################################### -def mk_mem_initializer_cpp_internal(component_src_dirs, path): +def mk_mem_initializer_cpp_internal(h_files_full_path, path): """ Generate a ``mem_initializer.cpp`` file in the directory ``path``. Returns the path to the generated file. @@ -754,7 +745,7 @@ def mk_mem_initializer_cpp_internal(component_src_dirs, path): These procedures are invoked by the Z3 memory_manager """ - assert isinstance(component_src_dirs, list) + assert isinstance(h_files_full_path, list) assert check_dir_exists(path) initializer_cmds = [] finalizer_cmds = [] @@ -765,11 +756,6 @@ def mk_mem_initializer_cpp_internal(component_src_dirs, path): # ADD_INITIALIZER with priority initializer_prio_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)') finalizer_pat = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)') - h_files_full_path = [] - for component_src_dir in sorted(component_src_dirs): - h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir)) - h_files = list(map(lambda p: os.path.join(component_src_dir, p), h_files)) - h_files_full_path.extend(h_files) for h_file in sorted_headers_by_component(h_files_full_path): added_include = False with open(h_file, 'r') as fin: 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_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_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 e7e35817f..3ce104709 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)) @@ -2735,7 +2745,8 @@ def mk_mem_initializer_cpp(cnames, path): for cname in cnames: c = get_component(cname) component_src_dirs.append(c.src_dir) - generated_file = mk_genfile_common.mk_mem_initializer_cpp_internal(component_src_dirs, path) + h_files_full_path = get_header_files_for_components(component_src_dirs) + generated_file = mk_genfile_common.mk_mem_initializer_cpp_internal(h_files_full_path, path) if VERBOSE: print("Generated '{}'".format(generated_file)) @@ -2753,7 +2764,8 @@ def mk_gparams_register_modules(cnames, path): for cname in cnames: c = get_component(cname) component_src_dirs.append(c.src_dir) - generated_file = mk_genfile_common.mk_gparams_register_modules_internal(component_src_dirs, path) + h_files_full_path = get_header_files_for_components(component_src_dirs) + generated_file = mk_genfile_common.mk_gparams_register_modules_internal(h_files_full_path, path) if VERBOSE: print("Generated '{}'".format(generated_file)) 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/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/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; 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/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/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() 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/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/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/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/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 61da4b3a0..805ed8e5d 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; } @@ -202,8 +201,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; ) { @@ -213,7 +212,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) { @@ -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()); @@ -291,13 +289,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 +336,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 +361,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 +389,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 +402,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 +417,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; } @@ -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); @@ -444,7 +445,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"; @@ -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) { @@ -487,6 +488,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) { @@ -524,7 +529,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) { @@ -535,14 +540,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; } - - - 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/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_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() { 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()); 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/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)); } 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()) { 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/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 { + } } 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/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()); 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()); 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/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp index 2b9cfb7f3..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,30 +54,32 @@ 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)); + } } } 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 ) diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index b76f909d0..7ed68c89f 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -59,4 +59,13 @@ z3_add_component(util util.cpp warning.cpp z3_exception.cpp + EXTRA_REGISTER_MODULE_HEADERS + env_params.h + MEMORY_INIT_FINALIZER_HEADERS + debug.h + gparams.h + prime_generator.h + rational.h + symbol.h + trace.h ) 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&);