mirror of
https://github.com/Z3Prover/z3
synced 2025-04-05 17:14:07 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
Christoph M. Wintersteiger
commit
2fceac04d4
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
=============
|
||||
|
||||
|
|
|
|||
|
|
@ -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()
|
||||
|
|
|
|||
|
|
@ -55,6 +55,9 @@ endfunction()
|
|||
# SOURCES source1 [source2...]
|
||||
# [COMPONENT_DEPENDENCIES component1 [component2...]]
|
||||
# [PYG_FILES pygfile1 [pygfile2...]]
|
||||
# [TACTIC_HEADERS header_file1 [header_file2...]]
|
||||
# [EXTRA_REGISTER_MODULE_HEADERS header_file1 [header_file2...]]
|
||||
# [MEMORY_INIT_FINALIZER_HEADERS header_file1 [header_file2...]]
|
||||
# )
|
||||
#
|
||||
# Declares a Z3 component (as a CMake "object library") with target name
|
||||
|
|
@ -80,14 +83,32 @@ endfunction()
|
|||
# The optional ``PYG_FILES`` keyword should be followed by a list of one or
|
||||
# more ``<NAME>.pyg`` files that should used to be generate
|
||||
# ``<NAME>_params.hpp`` header files used by the ``component_name``.
|
||||
# This generated file will automatically be scanned for the register module
|
||||
# declarations (i.e. ``REG_PARAMS()``, ``REG_MODULE_PARAMS()``, and
|
||||
# ``REG_MODULE_DESCRIPTION()``).
|
||||
#
|
||||
# The optional ``TACTIC_HEADERS`` keyword should be followed by a list of one or
|
||||
# more header files that declare a tactic and/or a probe that is part of this
|
||||
# component (see ``ADD_TACTIC()`` and ``ADD_PROBE()``).
|
||||
#
|
||||
# The optional ``EXTRA_REGISTER_MODULE_HEADERS`` keyword should be followed by a list
|
||||
# of one or more header files that contain module registration declarations.
|
||||
# NOTE: The header files generated from ``.pyg`` files don't need to be included.
|
||||
#
|
||||
# The optional ``MEMORY_INIT_FINALIZER_HEADERS`` keyword should be followed by a list
|
||||
# of one or more header files that contain memory initializer/finalizer declarations
|
||||
# (i.e. ``ADD_INITIALIZER()`` or ``ADD_FINALIZER()``).
|
||||
macro(z3_add_component component_name)
|
||||
CMAKE_PARSE_ARGUMENTS("Z3_MOD" "NOT_LIBZ3_COMPONENT" "" "SOURCES;COMPONENT_DEPENDENCIES;PYG_FILES" ${ARGN})
|
||||
CMAKE_PARSE_ARGUMENTS("Z3_MOD"
|
||||
"NOT_LIBZ3_COMPONENT"
|
||||
""
|
||||
"SOURCES;COMPONENT_DEPENDENCIES;PYG_FILES;TACTIC_HEADERS;EXTRA_REGISTER_MODULE_HEADERS;MEMORY_INIT_FINALIZER_HEADERS" ${ARGN})
|
||||
message(STATUS "Adding component ${component_name}")
|
||||
# Note: We don't check the sources exist here because
|
||||
# they might be generated files that don't exist yet.
|
||||
|
||||
set(_list_generated_headers "")
|
||||
set_property(GLOBAL PROPERTY Z3_${component_name}_REGISTER_MODULE_HEADERS "")
|
||||
foreach (pyg_file ${Z3_MOD_PYG_FILES})
|
||||
set(_full_pyg_file_path "${CMAKE_CURRENT_SOURCE_DIR}/${pyg_file}")
|
||||
if (NOT (EXISTS "${_full_pyg_file_path}"))
|
||||
|
|
@ -112,11 +133,70 @@ macro(z3_add_component component_name)
|
|||
VERBATIM
|
||||
)
|
||||
list(APPEND _list_generated_headers "${_full_output_file_path}")
|
||||
|
||||
# FIXME: This implicit dependency of a generated file depending on
|
||||
# generated files was inherited from the old build system.
|
||||
|
||||
# Typically generated headers contain `REG_PARAMS()`, `REG_MODULE_PARAMS()`
|
||||
# and `REG_MODULE_DESCRIPTION()` declarations so add to the list of
|
||||
# header files to scan.
|
||||
set_property(GLOBAL
|
||||
APPEND
|
||||
PROPERTY Z3_${component_name}_REGISTER_MODULE_HEADERS
|
||||
"${_full_output_file_path}"
|
||||
)
|
||||
endforeach()
|
||||
unset(_full_include_dir_path)
|
||||
unset(_full_output_file_path)
|
||||
unset(_output_file)
|
||||
|
||||
# Add tactic/probe headers to global property
|
||||
set_property(GLOBAL PROPERTY Z3_${component_name}_TACTIC_HEADERS "")
|
||||
foreach (tactic_header ${Z3_MOD_TACTIC_HEADERS})
|
||||
set(_full_tactic_header_file_path "${CMAKE_CURRENT_SOURCE_DIR}/${tactic_header}")
|
||||
if (NOT (EXISTS "${_full_tactic_header_file_path}"))
|
||||
message(FATAL_ERROR "\"${_full_tactic_header_file_path}\" does not exist")
|
||||
endif()
|
||||
set_property(GLOBAL
|
||||
APPEND
|
||||
PROPERTY Z3_${component_name}_TACTIC_HEADERS
|
||||
"${_full_tactic_header_file_path}"
|
||||
)
|
||||
endforeach()
|
||||
unset(_full_tactic_header_file_path)
|
||||
|
||||
# Add additional register module headers
|
||||
foreach (extra_register_module_header ${Z3_MOD_EXTRA_REGISTER_MODULE_HEADERS})
|
||||
set(_full_extra_register_module_header_path
|
||||
"${CMAKE_CURRENT_SOURCE_DIR}/${extra_register_module_header}"
|
||||
)
|
||||
if (NOT (EXISTS "${_full_extra_register_module_header_path}"))
|
||||
message(FATAL_ERROR "\"${_full_extra_register_module_header_path}\" does not exist")
|
||||
endif()
|
||||
set_property(GLOBAL
|
||||
APPEND
|
||||
PROPERTY Z3_${component_name}_REGISTER_MODULE_HEADERS
|
||||
"${_full_extra_register_module_header_path}"
|
||||
)
|
||||
endforeach()
|
||||
unset(_full_extra_register_module_header)
|
||||
|
||||
# Add memory initializer/finalizer headers to global property
|
||||
set_property(GLOBAL PROPERTY Z3_${component_name}_MEM_INIT_FINALIZER_HEADERS "")
|
||||
foreach (memory_init_finalizer_header ${Z3_MOD_MEMORY_INIT_FINALIZER_HEADERS})
|
||||
set(_full_memory_init_finalizer_header_path
|
||||
"${CMAKE_CURRENT_SOURCE_DIR}/${memory_init_finalizer_header}")
|
||||
if (NOT (EXISTS "${_full_memory_init_finalizer_header_path}"))
|
||||
message(FATAL_ERROR "\"${_full_memory_init_finalizer_header_path}\" does not exist")
|
||||
endif()
|
||||
set_property(GLOBAL
|
||||
APPEND
|
||||
PROPERTY Z3_${component_name}_MEM_INIT_FINALIZER_HEADERS
|
||||
"${_full_memory_init_finalizer_header_path}"
|
||||
)
|
||||
endforeach()
|
||||
unset(_full_memory_init_finalizer_header_path)
|
||||
|
||||
# Using "object" libraries here means we have a convenient
|
||||
# name to refer to a component in CMake but we don't actually
|
||||
# create a static/library from them. This allows us to easily
|
||||
|
|
@ -191,25 +271,33 @@ macro(z3_add_install_tactic_rule)
|
|||
)
|
||||
endif()
|
||||
z3_expand_dependencies(_expanded_components ${ARGN})
|
||||
# Get paths to search
|
||||
set(_search_paths "")
|
||||
|
||||
# Get header files that declare tactics/probes
|
||||
set(_tactic_header_files "")
|
||||
foreach (dependency ${_expanded_components})
|
||||
get_property(_dep_include_dirs GLOBAL PROPERTY Z3_${dependency}_INCLUDES)
|
||||
list(APPEND _search_paths ${_dep_include_dirs})
|
||||
get_property(_component_tactic_header_files
|
||||
GLOBAL
|
||||
PROPERTY Z3_${dependency}_TACTIC_HEADERS
|
||||
)
|
||||
list(APPEND _tactic_header_files ${_component_tactic_header_files})
|
||||
endforeach()
|
||||
unset(_component_tactic_header_files)
|
||||
|
||||
list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}")
|
||||
add_custom_command(OUTPUT "install_tactic.cpp"
|
||||
COMMAND "${PYTHON_EXECUTABLE}"
|
||||
"${CMAKE_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py"
|
||||
"${CMAKE_CURRENT_BINARY_DIR}"
|
||||
${_search_paths}
|
||||
${_tactic_header_files}
|
||||
DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py"
|
||||
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
|
||||
${_expanded_components}
|
||||
${_tactic_header_files}
|
||||
COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp\""
|
||||
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
|
||||
VERBATIM
|
||||
)
|
||||
unset(_expanded_components)
|
||||
unset(_tactic_header_files)
|
||||
endmacro()
|
||||
|
||||
macro(z3_add_memory_initializer_rule)
|
||||
|
|
@ -230,18 +318,31 @@ macro(z3_add_memory_initializer_rule)
|
|||
list(APPEND _search_paths ${_dep_include_dirs})
|
||||
endforeach()
|
||||
list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}")
|
||||
|
||||
# Get header files that declare initializers and finalizers
|
||||
set(_mem_init_finalize_headers "")
|
||||
foreach (dependency ${_expanded_components})
|
||||
get_property(_dep_mem_init_finalize_headers
|
||||
GLOBAL
|
||||
PROPERTY Z3_${dependency}_MEM_INIT_FINALIZER_HEADERS
|
||||
)
|
||||
list(APPEND _mem_init_finalize_headers ${_dep_mem_init_finalize_headers})
|
||||
endforeach()
|
||||
|
||||
add_custom_command(OUTPUT "mem_initializer.cpp"
|
||||
COMMAND "${PYTHON_EXECUTABLE}"
|
||||
"${CMAKE_SOURCE_DIR}/scripts/mk_mem_initializer_cpp.py"
|
||||
"${CMAKE_CURRENT_BINARY_DIR}"
|
||||
${_search_paths}
|
||||
${_mem_init_finalize_headers}
|
||||
DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_mem_initializer_cpp.py"
|
||||
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
|
||||
${_expanded_components}
|
||||
${_mem_init_finalize_headers}
|
||||
COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp\""
|
||||
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
|
||||
VERBATIM
|
||||
)
|
||||
unset(_mem_init_finalize_headers)
|
||||
unset(_expanded_components)
|
||||
endmacro()
|
||||
|
||||
macro(z3_add_gparams_register_modules_rule)
|
||||
|
|
@ -255,23 +356,27 @@ macro(z3_add_gparams_register_modules_rule)
|
|||
)
|
||||
endif()
|
||||
z3_expand_dependencies(_expanded_components ${ARGN})
|
||||
# Get paths to search
|
||||
set(_search_paths "")
|
||||
|
||||
# Get the list of header files to parse
|
||||
set(_register_module_header_files "")
|
||||
foreach (dependency ${_expanded_components})
|
||||
get_property(_dep_include_dirs GLOBAL PROPERTY Z3_${dependency}_INCLUDES)
|
||||
list(APPEND _search_paths ${_dep_include_dirs})
|
||||
get_property(_component_register_module_header_files GLOBAL PROPERTY Z3_${dependency}_REGISTER_MODULE_HEADERS)
|
||||
list(APPEND _register_module_header_files ${_component_register_module_header_files})
|
||||
endforeach()
|
||||
list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}")
|
||||
unset(_component_register_module_header_files)
|
||||
|
||||
add_custom_command(OUTPUT "gparams_register_modules.cpp"
|
||||
COMMAND "${PYTHON_EXECUTABLE}"
|
||||
"${CMAKE_SOURCE_DIR}/scripts/mk_gparams_register_modules_cpp.py"
|
||||
"${CMAKE_CURRENT_BINARY_DIR}"
|
||||
${_search_paths}
|
||||
${_register_module_header_files}
|
||||
DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_gparams_register_modules_cpp.py"
|
||||
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
|
||||
${_expanded_components}
|
||||
${_register_module_header_files}
|
||||
COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp\""
|
||||
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
|
||||
VERBATIM
|
||||
)
|
||||
unset(_expanded_components)
|
||||
unset(_register_module_header_files)
|
||||
endmacro()
|
||||
|
|
|
|||
|
|
@ -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})
|
||||
|
|
|
|||
|
|
@ -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:
|
||||
|
|
|
|||
|
|
@ -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))
|
||||
|
|
|
|||
|
|
@ -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))
|
||||
|
|
|
|||
|
|
@ -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))
|
||||
|
|
|
|||
|
|
@ -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))
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
)
|
||||
|
|
|
|||
|
|
@ -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()
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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; }
|
||||
|
|
|
|||
|
|
@ -8,4 +8,6 @@ z3_add_component(normal_forms
|
|||
rewriter
|
||||
PYG_FILES
|
||||
nnf_params.pyg
|
||||
EXTRA_REGISTER_MODULE_HEADERS
|
||||
nnf.h
|
||||
)
|
||||
|
|
|
|||
|
|
@ -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()
|
||||
|
||||
|
|
|
|||
|
|
@ -18,4 +18,6 @@ z3_add_component(cmd_context
|
|||
interp
|
||||
rewriter
|
||||
solver
|
||||
EXTRA_REGISTER_MODULE_HEADERS
|
||||
context_params.h
|
||||
)
|
||||
|
|
|
|||
|
|
@ -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) {
|
||||
|
|
|
|||
|
|
@ -11,5 +11,7 @@ z3_add_component(polynomial
|
|||
util
|
||||
PYG_FILES
|
||||
algebraic_params.pyg
|
||||
EXTRA_REGISTER_MODULE_HEADERS
|
||||
polynomial.h
|
||||
)
|
||||
|
||||
|
|
|
|||
|
|
@ -5,4 +5,6 @@ z3_add_component(subpaving_tactic
|
|||
COMPONENT_DEPENDENCIES
|
||||
core_tactics
|
||||
subpaving
|
||||
TACTIC_HEADERS
|
||||
subpaving_tactic.h
|
||||
)
|
||||
|
|
|
|||
|
|
@ -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<expr_ref_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<expr_ref_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<expr*const*, args_hash, args_eq> args_table;
|
||||
|
||||
br_status mk_array_eq(vector<expr_ref_vector> const& stores1, expr* else1,
|
||||
vector<expr_ref_vector> const& stores2, expr* else2,
|
||||
expr_ref_vector& conj, expr_ref& result) {
|
||||
br_status mk_array_eq_core(vector<expr_ref_vector> const& stores1, expr* else1,
|
||||
vector<expr_ref_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<expr_ref_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<evaluator_cfg> {
|
|||
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;
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -13,4 +13,6 @@ z3_add_component(fp
|
|||
pdr
|
||||
rel
|
||||
tab
|
||||
TACTIC_HEADERS
|
||||
horn_tactic.h
|
||||
)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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() {
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
||||
|
|
|
|||
|
|
@ -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());
|
||||
|
|
|
|||
|
|
@ -7,4 +7,7 @@ z3_add_component(nlsat_tactic
|
|||
arith_tactics
|
||||
nlsat
|
||||
sat_tactic
|
||||
TACTIC_HEADERS
|
||||
nlsat_tactic.h
|
||||
qfnra_nlsat_tactic.h
|
||||
)
|
||||
|
|
|
|||
|
|
@ -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));
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -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()) {
|
||||
|
|
|
|||
|
|
@ -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
|
||||
)
|
||||
|
|
|
|||
|
|
@ -6,4 +6,6 @@ z3_add_component(sat_tactic
|
|||
COMPONENT_DEPENDENCIES
|
||||
sat
|
||||
tactic
|
||||
TACTIC_HEADERS
|
||||
sat_tactic.h
|
||||
)
|
||||
|
|
|
|||
|
|
@ -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 {
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
)
|
||||
|
|
|
|||
|
|
@ -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());
|
||||
|
|
|
|||
|
|
@ -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());
|
||||
|
|
|
|||
|
|
@ -18,4 +18,8 @@ z3_add_component(tactic
|
|||
COMPONENT_DEPENDENCIES
|
||||
ast
|
||||
model
|
||||
TACTIC_HEADERS
|
||||
probe.h
|
||||
sine_filter.h
|
||||
tactic.h
|
||||
)
|
||||
|
|
|
|||
|
|
@ -4,4 +4,6 @@ z3_add_component(aig_tactic
|
|||
aig_tactic.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
tactic
|
||||
TACTIC_HEADERS
|
||||
aig_tactic.h
|
||||
)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
)
|
||||
|
|
|
|||
|
|
@ -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));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
)
|
||||
|
||||
|
|
|
|||
|
|
@ -11,4 +11,7 @@ z3_add_component(fpa_tactics
|
|||
sat_tactic
|
||||
smtlogic_tactics
|
||||
smt_tactic
|
||||
TACTIC_HEADERS
|
||||
fpa2bv_tactic.h
|
||||
qffp_tactic.h
|
||||
)
|
||||
|
|
|
|||
|
|
@ -4,4 +4,6 @@ z3_add_component(nlsat_smt_tactic
|
|||
COMPONENT_DEPENDENCIES
|
||||
nlsat_tactic
|
||||
smt_tactic
|
||||
TACTIC_HEADERS
|
||||
nl_purify_tactic.h
|
||||
)
|
||||
|
|
|
|||
|
|
@ -16,4 +16,6 @@ z3_add_component(portfolio
|
|||
smtlogic_tactics
|
||||
subpaving_tactic
|
||||
ufbv_tactic
|
||||
TACTIC_HEADERS
|
||||
default_tactic.h
|
||||
)
|
||||
|
|
|
|||
|
|
@ -10,4 +10,6 @@ z3_add_component(sls_tactic
|
|||
tactic
|
||||
PYG_FILES
|
||||
sls_params.pyg
|
||||
TACTIC_HEADERS
|
||||
sls_tactic.h
|
||||
)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
)
|
||||
|
|
|
|||
|
|
@ -11,6 +11,7 @@ template void lean::dense_matrix<double, double>::apply_from_left(vector<double>
|
|||
template lean::dense_matrix<double, double>::dense_matrix(lean::matrix<double, double> const*);
|
||||
template lean::dense_matrix<double, double>::dense_matrix(unsigned int, unsigned int);
|
||||
template lean::dense_matrix<double, double>& lean::dense_matrix<double, double>::operator=(lean::dense_matrix<double, double> const&);
|
||||
template lean::dense_matrix<lean::mpq, lean::mpq>::dense_matrix(unsigned int, unsigned int);
|
||||
template lean::dense_matrix<lean::mpq, lean::numeric_pair<lean::mpq> >::dense_matrix(lean::matrix<lean::mpq, lean::numeric_pair<lean::mpq> > const*);
|
||||
template void lean::dense_matrix<lean::mpq, lean::numeric_pair<lean::mpq> >::apply_from_left(vector<lean::mpq>&);
|
||||
template lean::dense_matrix<lean::mpq, lean::mpq> lean::operator*<lean::mpq, lean::mpq>(lean::matrix<lean::mpq, lean::mpq>&, lean::matrix<lean::mpq, lean::mpq>&);
|
||||
|
|
|
|||
Loading…
Reference in a new issue