diff --git a/CMakeLists.txt b/CMakeLists.txt index 87bd07f31..cf46e7012 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -35,8 +35,8 @@ set(Z3_VERSION_MAJOR 4) set(Z3_VERSION_MINOR 5) set(Z3_VERSION_PATCH 1) set(Z3_VERSION_TWEAK 0) -set(Z3_FULL_VERSION 0) set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}") +set(Z3_FULL_VERSION_STR "${Z3_VERSION}") # Note this might be modified message(STATUS "Z3 version ${Z3_VERSION}") ################################################################################ @@ -75,6 +75,64 @@ endif() ################################################################################ list(APPEND CMAKE_MODULE_PATH "${CMAKE_SOURCE_DIR}/cmake/modules") +################################################################################ +# Handle git hash and description +################################################################################ +include(${CMAKE_SOURCE_DIR}/cmake/git_utils.cmake) +macro(disable_git_describe) + message(WARNING "Disabling INCLUDE_GIT_DESCRIBE") + set(INCLUDE_GIT_DESCRIBE OFF CACHE BOOL "Include git describe output in version output" FORCE) +endmacro() +macro(disable_git_hash) + message(WARNING "Disabling INCLUDE_GIT_HASH") + set(INCLUDE_GIT_HASH OFF CACHE BOOL "Include git hash in version output" FORCE) + unset(Z3GITHASH) # Used in configure_file() +endmacro() +option(INCLUDE_GIT_HASH "Include git hash in version output" ON) +option(INCLUDE_GIT_DESCRIBE "Include git describe output in version output" ON) + +set(GIT_DIR "${CMAKE_SOURCE_DIR}/.git") +if (EXISTS "${GIT_DIR}") + # Try to make CMake configure depend on the current git HEAD so that + # a re-configure is triggered when the HEAD changes. + add_git_dir_dependency("${GIT_DIR}" ADD_GIT_DEP_SUCCESS) + if (ADD_GIT_DEP_SUCCESS) + if (INCLUDE_GIT_HASH) + get_git_head_hash("${GIT_DIR}" Z3GITHASH) + if (NOT Z3GITHASH) + message(WARNING "Failed to get Git hash") + disable_git_hash() + 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}") + else() + message(STATUS "Not using Git hash in version output") + unset(Z3GITHASH) # Used in configure_file() + endif() + if (INCLUDE_GIT_DESCRIBE) + get_git_head_describe("${GIT_DIR}" Z3_GIT_DESCRIPTION) + if (NOT Z3_GIT_DESCRIPTION) + message(WARNING "Failed to get Git description") + disable_git_describe() + 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}") + else() + message(STATUS "Not including git descrption in version") + endif() + else() + message(WARNING "Failed to add git dependency.") + disable_git_describe() + disable_git_hash() + endif() +else() + message(STATUS "Failed to find git directory.") + disable_git_describe() + disable_git_hash() +endif() + ################################################################################ # Useful CMake functions/Macros ################################################################################ @@ -89,7 +147,6 @@ set(Z3_COMPONENT_CXX_FLAGS "") set(Z3_COMPONENT_EXTRA_INCLUDE_DIRS "") set(Z3_DEPENDENT_LIBS "") set(Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS "") -set(Z3_DEPENDENT_EXTRA_C_LINK_FLAGS "") ################################################################################ # Build type @@ -236,11 +293,7 @@ if (OPENMP_FOUND) # flag by MSVC and breaks the build if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) - list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS ${OpenMP_C_FLAGS}) - endif() - if (("${CMAKE_C_COMPILER_ID}" MATCHES "Clang") OR - ("${CMAKE_C_COMPILER_ID}" MATCHES "GNU")) - list(APPEND Z3_DEPENDENT_EXTRA_C_LINK_FLAGS ${OpenMP_CXX_FLAGS}) + list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS ${OpenMP_CXX_FLAGS}) endif() unset(CMAKE_REQUIRED_FLAGS) message(STATUS "Using OpenMP") @@ -328,7 +381,6 @@ message(STATUS "Z3_COMPONENT_CXX_FLAGS: ${Z3_COMPONENT_CXX_FLAGS}") message(STATUS "Z3_DEPENDENT_LIBS: ${Z3_DEPENDENT_LIBS}") message(STATUS "Z3_COMPONENT_EXTRA_INCLUDE_DIRS: ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS}") message(STATUS "Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS: ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}") -message(STATUS "Z3_DEPENDENT_EXTRA_C_LINK_FLAGS: ${Z3_DEPENDENT_EXTRA_C_LINK_FLAGS}") ################################################################################ # Z3 installation locations @@ -340,10 +392,18 @@ set(CMAKE_INSTALL_PKGCONFIGDIR PATH "Directory to install pkgconfig files" ) + +set(CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR + "${CMAKE_INSTALL_LIBDIR}/cmake/z3" + CACHE + PATH + "Directory to install Z3 CMake package files" +) message(STATUS "CMAKE_INSTALL_LIBDIR: \"${CMAKE_INSTALL_LIBDIR}\"") message(STATUS "CMAKE_INSTALL_BINDIR: \"${CMAKE_INSTALL_BINDIR}\"") message(STATUS "CMAKE_INSTALL_INCLUDEDIR: \"${CMAKE_INSTALL_INCLUDEDIR}\"") message(STATUS "CMAKE_INSTALL_PKGCONFIGDIR: \"${CMAKE_INSTALL_PKGCONFIGDIR}\"") +message(STATUS "CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR: \"${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}\"") ################################################################################ # Uninstall rule @@ -391,6 +451,76 @@ include(${CMAKE_SOURCE_DIR}/cmake/z3_add_component.cmake) include(${CMAKE_SOURCE_DIR}/cmake/z3_append_linker_flag_list_to_target.cmake) add_subdirectory(src) +################################################################################ +# Create `Z3Config.cmake` and related files for the build tree so clients can +# use Z3 via CMake. +################################################################################ +include(CMakePackageConfigHelpers) +export(EXPORT Z3_EXPORTED_TARGETS + NAMESPACE z3:: + FILE "${CMAKE_BINARY_DIR}/Z3Targets.cmake" +) +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++") +set(AUTO_GEN_MSG "Automatically generated. DO NOT EDIT") +set(CONFIG_FILE_TYPE "build tree") +configure_package_config_file("${CMAKE_SOURCE_DIR}/cmake/Z3Config.cmake.in" + "Z3Config.cmake" + INSTALL_DESTINATION "${CMAKE_BINARY_DIR}" + PATH_VARS + 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) +unset(Z3_CXX_PACKAGE_INCLUDE_DIR) +unset(AUTO_GEN_MSG) +unset(CONFIG_FILE_TYPE) +# TODO: Provide a `Z3Version.cmake` file so that clients can specify the version +# of Z3 they want. + +################################################################################ +# Create `Z3Config.cmake` and related files for install tree so clients can use +# Z3 via CMake. +################################################################################ +install(EXPORT + Z3_EXPORTED_TARGETS + FILE "Z3Targets.cmake" + NAMESPACE z3:: + DESTINATION "${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}" +) +set(Z3_INSTALL_TREE_CMAKE_CONFIG_FILE "${CMAKE_BINARY_DIR}/cmake/Z3Config.cmake") +set(Z3_FIRST_PACKAGE_INCLUDE_DIR "${CMAKE_INSTALL_INCLUDEDIR}") +set(Z3_SECOND_INCLUDE_DIR "") +set(Z3_CXX_PACKAGE_INCLUDE_DIR "") +set(AUTO_GEN_MSG "Automatically generated. DO NOT EDIT") +set(CONFIG_FILE_TYPE "install tree") +# We use `configure_package_config_file()` to try and create CMake files +# that are re-locatable so that it doesn't matter if the files aren't placed +# in the original install prefix. +configure_package_config_file("${CMAKE_SOURCE_DIR}/cmake/Z3Config.cmake.in" + "${Z3_INSTALL_TREE_CMAKE_CONFIG_FILE}" + INSTALL_DESTINATION "${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}" + PATH_VARS Z3_FIRST_PACKAGE_INCLUDE_DIR +) +unset(Z3_FIRST_PACKAGE_INCLUDE_DIR) +unset(Z3_SECOND_PACKAGE_INCLUDE_DIR) +unset(Z3_CXX_PACKAGE_INCLUDE_DIR) +unset(AUTO_GEN_MSG) +unset(CONFIG_FILE_TYPE) + +# Add install rule to install ${Z3_INSTALL_TREE_CMAKE_CONFIG_FILE} +install( + FILES "${Z3_INSTALL_TREE_CMAKE_CONFIG_FILE}" + DESTINATION "${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}" +) + +# TODO: Provide a `Z3Version.cmake` file so that clients can specify the version +# of Z3 they want. + ################################################################################ # Examples ################################################################################ diff --git a/README-CMake.md b/README-CMake.md index 0943e7a7d..6a78b5d4c 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -267,6 +267,7 @@ The following useful options can be passed to CMake whilst configuring. * ``CMAKE_INSTALL_PREFIX`` - STRING. The install prefix to use (e.g. ``/usr/local/``). * ``CMAKE_INSTALL_PKGCONFIGDIR`` - STRING. The path to install pkgconfig files. * ``CMAKE_INSTALL_PYTHON_PKG_DIR`` - STRING. The path to install the z3 python bindings. This can be relative (to ``CMAKE_INSTALL_PREFIX``) or absolute. +* ``CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR`` - STRING. The path to install CMake package files (e.g. ``/usr/lib/cmake/z3``). * ``ENABLE_TRACING_FOR_NON_DEBUG`` - BOOL. If set to ``TRUE`` enable tracing in non-debug builds, if set to ``FALSE`` disable tracing in non-debug builds. Note in debug builds tracing is always enabled. * ``BUILD_LIBZ3_SHARED`` - BOOL. If set to ``TRUE`` build libz3 as a shared library otherwise build as a static library. * ``ENABLE_EXAMPLE_TARGETS`` - BOOL. If set to ``TRUE`` add the build targets for building the API examples. @@ -283,6 +284,8 @@ The following useful options can be passed to CMake whilst configuring. * ``INSTALL_JAVA_BINDINGS`` - BOOL. If set to ``TRUE`` and ``BUILD_JAVA_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's Java bindings. * ``Z3_JAVA_JAR_INSTALLDIR`` - STRING. The path to directory to install the Z3 Java ``.jar`` file. This path should be relative to ``CMAKE_INSTALL_PREFIX``. * ``Z3_JAVA_JNI_LIB_INSTALLDIRR`` - STRING. The path to directory to install the Z3 Java JNI bridge library. This path should be relative to ``CMAKE_INSTALL_PREFIX``. +* ``INCLUDE_GIT_DESCRIBE`` - BOOL. If set to ``TRUE`` and the source tree of Z3 is a git repository then the output of ``git describe`` will be included in the build. +* ``INCLUDE_GIT_HASH`` - BOOL. If set to ``TRUE`` and the source tree of Z3 is a git repository then the git hash will be included in the build. On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface. diff --git a/README.md b/README.md index e0821ac79..f4c6dd012 100644 --- a/README.md +++ b/README.md @@ -168,7 +168,10 @@ python scripts/mk_make.py --prefix=/home/leo --python --pypkgdir=/home/leo/lib/p If you do need to install to a non standard prefix a better approach is to use a [Python virtual environment](https://virtualenv.readthedocs.org/en/latest/) -and install Z3 there. +and install Z3 there. Python packages also work for Python3. +Under Windows, recall to build inside the Visual C++ native command build environment. +Note that the buit/python/z3 directory should be accessible from where python is used with Z3 +and it depends on libz3.dll to be in the path. ```bash virtualenv venv @@ -185,3 +188,4 @@ python -c 'import z3; print(z3.get_version_string())' ``` See [``examples/python``](examples/python) for examples. + diff --git a/contrib/cmake/cmake/Z3Config.cmake.in b/contrib/cmake/cmake/Z3Config.cmake.in new file mode 100644 index 000000000..e7f604591 --- /dev/null +++ b/contrib/cmake/cmake/Z3Config.cmake.in @@ -0,0 +1,30 @@ +################################################################################ +# @AUTO_GEN_MSG@ +# +# This file is intended to be consumed by clients who wish to use Z3 from CMake. +# It can be use by doing `find_package(Z3 config)` from within a +# `CMakeLists.txt` file. If CMake doesn't find this package automatically you +# can give it a hint by passing `-DZ3_DIR=` to the CMake invocation where +# `` is the path to the directory containing this file. +# +# This file was built for the @CONFIG_FILE_TYPE@. +################################################################################ + +# Exported targets +include("${CMAKE_CURRENT_LIST_DIR}/Z3Targets.cmake") + +@PACKAGE_INIT@ + +# Version information +set(Z3_VERSION_MAJOR @Z3_VERSION_MAJOR@) +set(Z3_VERSION_MINOR @Z3_VERSION_MINOR@) +set(Z3_VERSION_PATCH @Z3_VERSION_PATCH@) +set(Z3_VERSION_TWEAK @Z3_VERSION_TWEAK@) +set(Z3_VERSION_STRING "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}") + +# NOTE: We can't use `set_and_check()` here because this a list of paths. +# List of include directories +set(Z3_C_INCLUDE_DIRS @PACKAGE_Z3_FIRST_PACKAGE_INCLUDE_DIR@ @PACKAGE_Z3_SECOND_PACKAGE_INCLUDE_DIR@) +set(Z3_CXX_INCLUDE_DIRS @PACKAGE_Z3_CXX_PACKAGE_INCLUDE_DIR@ ${Z3_C_INCLUDE_DIRS}) +# List of libraries to link against +set(Z3_LIBRARIES "z3::libz3") diff --git a/contrib/cmake/cmake/git_utils.cmake b/contrib/cmake/cmake/git_utils.cmake new file mode 100644 index 000000000..aa7f38825 --- /dev/null +++ b/contrib/cmake/cmake/git_utils.cmake @@ -0,0 +1,173 @@ +# add_git_dir_dependency(GIT_DIR SUCCESS_VAR) +# +# Adds a configure time dependency on the git directory such that if the HEAD +# of the git directory changes CMake will be forced to re-run. This useful +# for fetching the current git hash and including it in the build. +# +# `GIT_DIR` is the path to the git directory (i.e. the `.git` directory) +# `SUCCESS_VAR` is the name of the variable to set. It will be set to TRUE +# if the dependency was successfully added and FALSE otherwise. +function(add_git_dir_dependency GIT_DIR SUCCESS_VAR) + if (NOT "${ARGC}" EQUAL 2) + message(FATAL_ERROR "Invalid number (${ARGC}) of arguments") + endif() + + if (NOT IS_ABSOLUTE "${GIT_DIR}") + message(FATAL_ERROR "GIT_DIR (\"${GIT_DIR}\") is not an absolute path") + endif() + + if (NOT IS_DIRECTORY "${GIT_DIR}") + message(FATAL_ERROR "GIT_DIR (\"${GIT_DIR}\") is not a directory") + endif() + + set(GIT_HEAD_FILE "${GIT_DIR}/HEAD") + if (NOT EXISTS "${GIT_HEAD_FILE}") + message(AUTHOR_WARNING "Git head file \"${GIT_HEAD_FILE}\" cannot be found") + set(${SUCCESS_VAR} FALSE PARENT_SCOPE) + return() + endif() + + # List of files in the git tree that CMake configuration should depend on + set(GIT_FILE_DEPS "${GIT_HEAD_FILE}") + + # Examine the HEAD and workout what additional dependencies there are. + file(READ "${GIT_HEAD_FILE}" GIT_HEAD_DATA LIMIT 128) + string(STRIP "${GIT_HEAD_DATA}" GIT_HEAD_DATA_STRIPPED) + + if ("${GIT_HEAD_DATA_STRIPPED}" MATCHES "^ref:[ ]*(.+)$") + # HEAD points at a reference. + set(GIT_REF "${CMAKE_MATCH_1}") + if (EXISTS "${GIT_DIR}/${GIT_REF}") + # Unpacked reference. The file contains the commit hash + # so add a dependency on this file so that if we stay on this + # reference (i.e. branch) but change commit CMake will be forced + # to reconfigure. + list(APPEND GIT_FILE_DEPS "${GIT_DIR}/${GIT_REF}") + elseif(EXISTS "${GIT_DIR}/packed-refs") + # The ref must be packed (see `man git-pack-refs`). + list(APPEND GIT_FILE_DEPS "${GIT_DIR}/packed-refs") + else() + # Fail + message(AUTHOR_WARNING "Unhandled git reference") + set(${SUCCESS_VAR} FALSE PARENT_SCOPE) + return() + endif() + else() + # Detached HEAD. + # No other dependencies needed + endif() + + # FIXME: + # This is the directory we will copy (via `configure_file()`) git files + # into. This is a hack. It would be better to use the + # `CMAKE_CONFIGURE_DEPENDS` directory property but that feature is not + # available in CMake 2.8.12. So we use `configure_file()` to effectively + # do the same thing. When the source file to `configure_file()` changes + # it will trigger a re-run of CMake. + set(GIT_CMAKE_FILES_DIR "${CMAKE_CURRENT_BINARY_DIR}/git_cmake_files") + file(MAKE_DIRECTORY "${GIT_CMAKE_FILES_DIR}") + + foreach (git_dependency ${GIT_FILE_DEPS}) + message(STATUS "Adding git dependency \"${git_dependency}\"") + configure_file( + "${git_dependency}" + "${GIT_CMAKE_FILES_DIR}" + COPYONLY + ) + endforeach() + + set(${SUCCESS_VAR} TRUE PARENT_SCOPE) +endfunction() + +# get_git_head_hash(GIT_DIR OUTPUT_VAR) +# +# Retrieve the current commit hash for a git working directory where `GIT_DIR` +# is the `.git` directory in the root of the git working directory. +# +# `OUTPUT_VAR` should be the name of the variable to put the result in. If this +# function fails then either a fatal error will be raised or `OUTPUT_VAR` will +# contain a string with the suffix `NOTFOUND` which can be used in CMake `if()` +# commands. +function(get_git_head_hash GIT_DIR OUTPUT_VAR) + if (NOT "${ARGC}" EQUAL 2) + message(FATAL_ERROR "Invalid number of arguments") + endif() + if (NOT IS_DIRECTORY "${GIT_DIR}") + message(FATAL_ERROR "\"${GIT_DIR}\" is not a directory") + endif() + if (NOT IS_ABSOLUTE "${GIT_DIR}") + message(FATAL_ERROR \""${GIT_DIR}\" is not an absolute path") + endif() + find_package(Git) + if (NOT Git_FOUND) + set(${OUTPUT_VAR} "GIT-NOTFOUND" PARENT_SCOPE) + return() + endif() + get_filename_component(GIT_WORKING_DIR "${GIT_DIR}" DIRECTORY) + execute_process( + COMMAND + "${GIT_EXECUTABLE}" + "rev-parse" + "-q" # Quiet + "HEAD" + WORKING_DIRECTORY + "${GIT_WORKING_DIR}" + RESULT_VARIABLE + GIT_EXIT_CODE + OUTPUT_VARIABLE + Z3_GIT_HASH + OUTPUT_STRIP_TRAILING_WHITESPACE + ) + if (NOT "${GIT_EXIT_CODE}" EQUAL 0) + message(WARNING "Failed to execute git") + set(${OUTPUT_VAR} NOTFOUND PARENT_SCOPE) + return() + endif() + set(${OUTPUT_VAR} "${Z3_GIT_HASH}" PARENT_SCOPE) +endfunction() + +# get_git_head_describe(GIT_DIR OUTPUT_VAR) +# +# Retrieve the output of `git describe` for a git working directory where +# `GIT_DIR` is the `.git` directory in the root of the git working directory. +# +# `OUTPUT_VAR` should be the name of the variable to put the result in. If this +# function fails then either a fatal error will be raised or `OUTPUT_VAR` will +# contain a string with the suffix `NOTFOUND` which can be used in CMake `if()` +# commands. +function(get_git_head_describe GIT_DIR OUTPUT_VAR) + if (NOT "${ARGC}" EQUAL 2) + message(FATAL_ERROR "Invalid number of arguments") + endif() + if (NOT IS_DIRECTORY "${GIT_DIR}") + message(FATAL_ERROR "\"${GIT_DIR}\" is not a directory") + endif() + if (NOT IS_ABSOLUTE "${GIT_DIR}") + message(FATAL_ERROR \""${GIT_DIR}\" is not an absolute path") + endif() + find_package(Git) + if (NOT Git_FOUND) + set(${OUTPUT_VAR} "GIT-NOTFOUND" PARENT_SCOPE) + return() + endif() + get_filename_component(GIT_WORKING_DIR "${GIT_DIR}" DIRECTORY) + execute_process( + COMMAND + "${GIT_EXECUTABLE}" + "describe" + "--long" + WORKING_DIRECTORY + "${GIT_WORKING_DIR}" + RESULT_VARIABLE + GIT_EXIT_CODE + OUTPUT_VARIABLE + Z3_GIT_DESCRIPTION + OUTPUT_STRIP_TRAILING_WHITESPACE + ) + if (NOT "${GIT_EXIT_CODE}" EQUAL 0) + message(WARNING "Failed to execute git") + set(${OUTPUT_VAR} NOTFOUND PARENT_SCOPE) + return() + endif() + set(${OUTPUT_VAR} "${Z3_GIT_DESCRIPTION}" PARENT_SCOPE) +endfunction() diff --git a/contrib/cmake/examples/CMakeLists.txt b/contrib/cmake/examples/CMakeLists.txt index e596ed3dd..3fa49f9e0 100644 --- a/contrib/cmake/examples/CMakeLists.txt +++ b/contrib/cmake/examples/CMakeLists.txt @@ -1,4 +1,64 @@ -add_subdirectory(c) -add_subdirectory(c++) -add_subdirectory(tptp) -add_subdirectory(python) +include(ExternalProject) +# Unfortunately `BUILD_ALWAYS` only seems to be supported with the version of ExternalProject +# that shipped with CMake >= 3.1. +if (("${CMAKE_VERSION}" VERSION_EQUAL "3.1") OR ("${CMAKE_VERSION}" VERSION_GREATER "3.1")) + set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG BUILD_ALWAYS 1) +else() + set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG "") +endif() + +################################################################################ +# Build example project using libz3's C API as an external project +################################################################################ +ExternalProject_Add(c_example + DEPENDS libz3 + # Configure step + SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/c" + CMAKE_ARGS "-DZ3_DIR=${CMAKE_BINARY_DIR}" + # Build step + ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} + BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_example_build_dir" + # Install Step + INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command +) +set_target_properties(c_example PROPERTIES EXCLUDE_FROM_ALL TRUE) + + +################################################################################ +# Build example project using libz3's C++ API as an external project +################################################################################ +ExternalProject_Add(cpp_example + DEPENDS libz3 + # Configure step + SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/c++" + CMAKE_ARGS "-DZ3_DIR=${CMAKE_BINARY_DIR}" + # Build step + ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} + BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/cpp_example_build_dir" + # Install Step + INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command +) +set_target_properties(cpp_example PROPERTIES EXCLUDE_FROM_ALL TRUE) + +################################################################################ +# Build example tptp5 project using libz3's C++ API as an external project +################################################################################ +ExternalProject_Add(z3_tptp5 + DEPENDS libz3 + # Configure step + SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/tptp" + CMAKE_ARGS "-DZ3_DIR=${CMAKE_BINARY_DIR}" + # Build step + ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} + BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/tptp_build_dir" + # Install Step + INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command +) +set_target_properties(z3_tptp5 PROPERTIES EXCLUDE_FROM_ALL TRUE) + +################################################################################ +# Build Python examples +################################################################################ +if (BUILD_PYTHON_BINDINGS) + add_subdirectory(python) +endif() diff --git a/contrib/cmake/examples/c++/CMakeLists.txt b/contrib/cmake/examples/c++/CMakeLists.txt index fdc5cf387..d60604924 100644 --- a/contrib/cmake/examples/c++/CMakeLists.txt +++ b/contrib/cmake/examples/c++/CMakeLists.txt @@ -1,9 +1,38 @@ -# FIXME: We should build this as an external project and consume -# Z3 as `find_package(z3 CONFIG)`. -add_executable(cpp_example EXCLUDE_FROM_ALL example.cpp) -target_link_libraries(cpp_example PRIVATE libz3) -target_include_directories(cpp_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api") -target_include_directories(cpp_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api/c++") -if (NOT BUILD_LIBZ3_SHARED) - z3_append_linker_flag_list_to_target(cpp_example ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) +################################################################################ +# Example C++ project +################################################################################ +project(Z3_C_EXAMPLE CXX) +cmake_minimum_required(VERSION 2.8.12) +find_package(Z3 + REQUIRED + CONFIG + # `NO_DEFAULT_PATH` is set so that -DZ3_DIR has to be passed to find Z3. + # This should prevent us from accidently picking up an installed + # copy of Z3. This is here to benefit Z3's build sytem when building + # this project. When making your own project you probably shouldn't + # use this option. + NO_DEFAULT_PATH +) +message(STATUS "Z3_FOUND: ${Z3_FOUND}") +message(STATUS "Found Z3 ${Z3_VERSION_STRING}") +message(STATUS "Z3_DIR: ${Z3_DIR}") + +add_executable(cpp_example example.cpp) +target_include_directories(cpp_example PRIVATE ${Z3_CXX_INCLUDE_DIRS}) +target_link_libraries(cpp_example PRIVATE ${Z3_LIBRARIES}) + +if ("${CMAKE_SYSTEM_NAME}" MATCHES "[Ww]indows") + # On Windows we need to copy the Z3 libraries + # into the same directory as the executable + # so that they can be found. + foreach (z3_lib ${Z3_LIBRARIES}) + message(STATUS "Adding copy rule for ${z3_lib}") + add_custom_command(TARGET cpp_example + POST_BUILD + COMMAND + ${CMAKE_COMMAND} -E copy_if_different + $ + $ + ) + endforeach() endif() diff --git a/contrib/cmake/examples/c/CMakeLists.txt b/contrib/cmake/examples/c/CMakeLists.txt index fc6eaee18..dd8fa6328 100644 --- a/contrib/cmake/examples/c/CMakeLists.txt +++ b/contrib/cmake/examples/c/CMakeLists.txt @@ -1,9 +1,42 @@ -# FIXME: We should build this as an external project and consume -# Z3 as `find_package(z3 CONFIG)`. -add_executable(c_example EXCLUDE_FROM_ALL test_capi.c) -target_link_libraries(c_example PRIVATE libz3) -target_include_directories(c_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api") -# This is needed for when libz3 is built as a static library -if (NOT BUILD_LIBZ3_SHARED) - z3_append_linker_flag_list_to_target(c_example ${Z3_DEPENDENT_EXTRA_C_LINK_FLAGS}) +################################################################################ +# Example C project +################################################################################ +# NOTE: Even though this is a C project, libz3 uses C++. When using libz3 +# as a static library if we don't configure this project to also support +# C++ we will use the C linker rather than the C++ linker and will not link +# the C++ standard library in resulting in a link failure. +project(Z3_C_EXAMPLE C CXX) +cmake_minimum_required(VERSION 2.8.12) +find_package(Z3 + REQUIRED + CONFIG + # `NO_DEFAULT_PATH` is set so that -DZ3_DIR has to be passed to find Z3. + # This should prevent us from accidently picking up an installed + # copy of Z3. This is here to benefit Z3's build sytem when building + # this project. When making your own project you probably shouldn't + # use this option. + NO_DEFAULT_PATH +) +message(STATUS "Z3_FOUND: ${Z3_FOUND}") +message(STATUS "Found Z3 ${Z3_VERSION_STRING}") +message(STATUS "Z3_DIR: ${Z3_DIR}") + +add_executable(c_example test_capi.c) +target_include_directories(c_example PRIVATE ${Z3_C_INCLUDE_DIRS}) +target_link_libraries(c_example PRIVATE ${Z3_LIBRARIES}) + +if ("${CMAKE_SYSTEM_NAME}" MATCHES "[Ww]indows") + # On Windows we need to copy the Z3 libraries + # into the same directory as the executable + # so that they can be found. + foreach (z3_lib ${Z3_LIBRARIES}) + message(STATUS "Adding copy rule for ${z3_lib}") + add_custom_command(TARGET c_example + POST_BUILD + COMMAND + ${CMAKE_COMMAND} -E copy_if_different + $ + $ + ) + endforeach() endif() diff --git a/contrib/cmake/examples/tptp/CMakeLists.txt b/contrib/cmake/examples/tptp/CMakeLists.txt index 41fa9cc65..8e8dfb8ea 100644 --- a/contrib/cmake/examples/tptp/CMakeLists.txt +++ b/contrib/cmake/examples/tptp/CMakeLists.txt @@ -1,4 +1,39 @@ -add_executable(z3_tptp5 EXCLUDE_FROM_ALL tptp5.cpp tptp5.lex.cpp) -target_link_libraries(z3_tptp5 PRIVATE libz3) -target_include_directories(z3_tptp5 PRIVATE "${CMAKE_SOURCE_DIR}/src/api") -target_include_directories(z3_tptp5 PRIVATE "${CMAKE_SOURCE_DIR}/src/api/c++") +################################################################################ +# TPTP example +################################################################################ +project(Z3_TPTP5 CXX) +cmake_minimum_required(VERSION 2.8.12) +find_package(Z3 + REQUIRED + CONFIG + # `NO_DEFAULT_PATH` is set so that -DZ3_DIR has to be passed to find Z3. + # This should prevent us from accidently picking up an installed + # copy of Z3. This is here to benefit Z3's build sytem when building + # this project. When making your own project you probably shouldn't + # use this option. + NO_DEFAULT_PATH +) +message(STATUS "Z3_FOUND: ${Z3_FOUND}") +message(STATUS "Found Z3 ${Z3_VERSION_STRING}") +message(STATUS "Z3_DIR: ${Z3_DIR}") + +add_executable(z3_tptp5 tptp5.cpp tptp5.lex.cpp) +target_include_directories(z3_tptp5 PRIVATE ${Z3_CXX_INCLUDE_DIRS}) +target_link_libraries(z3_tptp5 PRIVATE ${Z3_LIBRARIES}) + +if ("${CMAKE_SYSTEM_NAME}" MATCHES "[Ww]indows") + # On Windows we need to copy the Z3 libraries + # into the same directory as the executable + # so that they can be found. + foreach (z3_lib ${Z3_LIBRARIES}) + message(STATUS "Adding copy rule for ${z3_lib}") + add_custom_command(TARGET z3_tptp5 + POST_BUILD + COMMAND + ${CMAKE_COMMAND} -E copy_if_different + $ + $ + ) + endforeach() +endif() + diff --git a/contrib/cmake/src/CMakeLists.txt b/contrib/cmake/src/CMakeLists.txt index 65eef8094..66e34790a 100644 --- a/contrib/cmake/src/CMakeLists.txt +++ b/contrib/cmake/src/CMakeLists.txt @@ -143,7 +143,13 @@ endif() # so that if those are also shared libraries they are referenced by `libz3.so`. target_link_libraries(libz3 PRIVATE ${Z3_DEPENDENT_LIBS}) -z3_append_linker_flag_list_to_target(libz3 ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) +# This is currently only for the OpenMP flags. It needs to be set +# via `target_link_libraries()` rather than `z3_append_linker_flag_list_to_target()` +# because when building the `libz3` as a static library when the target is exported +# the link dependencies need to be exported too. +foreach (flag_name ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) + target_link_libraries(libz3 PRIVATE ${flag_name}) +endforeach() # Declare which header file are the public header files of libz3 # these will automatically installed when the libz3 target is installed @@ -168,6 +174,7 @@ foreach (header ${libz3_public_headers}) endforeach() install(TARGETS libz3 + EXPORT Z3_EXPORTED_TARGETS LIBRARY DESTINATION "${CMAKE_INSTALL_LIBDIR}" ARCHIVE DESTINATION "${CMAKE_INSTALL_LIBDIR}" # On Windows this installs ``libz3.lib`` which CMake calls the "corresponding import library". Do we want this installed? RUNTIME DESTINATION "${CMAKE_INSTALL_LIBDIR}" # For Windows. DLLs are runtime targets for CMake diff --git a/contrib/cmake/src/api/java/CMakeLists.txt b/contrib/cmake/src/api/java/CMakeLists.txt index b34277266..dce2bc4ea 100644 --- a/contrib/cmake/src/api/java/CMakeLists.txt +++ b/contrib/cmake/src/api/java/CMakeLists.txt @@ -44,7 +44,6 @@ target_link_libraries(z3java PRIVATE libz3) # Z3's components to build ``Native.cpp`` lets do the same for now. target_compile_options(z3java PRIVATE ${Z3_COMPONENT_CXX_FLAGS}) target_compile_definitions(z3java PRIVATE ${Z3_COMPONENT_CXX_DEFINES}) -z3_append_linker_flag_list_to_target(z3java ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) target_include_directories(z3java PRIVATE "${CMAKE_SOURCE_DIR}/src/api" "${CMAKE_BINARY_DIR}/src/api" diff --git a/contrib/cmake/src/util/CMakeLists.txt b/contrib/cmake/src/util/CMakeLists.txt index c85076531..b76f909d0 100644 --- a/contrib/cmake/src/util/CMakeLists.txt +++ b/contrib/cmake/src/util/CMakeLists.txt @@ -3,7 +3,9 @@ if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/version.h") ${z3_polluted_tree_msg} ) endif() -configure_file(version.h.in ${CMAKE_CURRENT_BINARY_DIR}/version.h @ONLY) + +set(Z3_FULL_VERSION "\"${Z3_FULL_VERSION_STR}\"") +configure_file(version.h.cmake.in ${CMAKE_CURRENT_BINARY_DIR}/version.h) z3_add_component(util SOURCES diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 21a3fedf4..bfd4eb2c4 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2175,6 +2175,50 @@ namespace z3 { }; inline std::ostream & operator<<(std::ostream & out, optimize const & s) { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; } + class fixedpoint : public object { + Z3_fixedpoint m_fp; + public: + fixedpoint(context& c):object(c) { m_fp = Z3_mk_fixedpoint(c); Z3_fixedpoint_inc_ref(c, m_fp); } + ~fixedpoint() { Z3_fixedpoint_dec_ref(ctx(), m_fp); } + operator Z3_fixedpoint() const { return m_fp; } + void from_string(char const* s) { Z3_fixedpoint_from_string(ctx(), m_fp, s); check_error(); } + void from_file(char const* s) { Z3_fixedpoint_from_file(ctx(), m_fp, s); check_error(); } + void add_rule(expr& rule, symbol const& name) { Z3_fixedpoint_add_rule(ctx(), m_fp, rule, name); check_error(); } + void add_fact(func_decl& f, unsigned * args) { Z3_fixedpoint_add_fact(ctx(), m_fp, f, f.arity(), args); check_error(); } + check_result query(expr& q) { Z3_lbool r = Z3_fixedpoint_query(ctx(), m_fp, q); check_error(); to_check_result(r); } + check_result query(func_decl_vector& relations) { + array rs(relations); + Z3_lbool r = Z3_fixedpoint_query_relations(ctx(), m_fp, rs.size(), rs.ptr()); + check_error(); + return to_check_result(r); + } + expr get_answer() { Z3_ast r = Z3_fixedpoint_get_answer(ctx(), m_fp); check_error(); return expr(ctx(), r); } + std::string reason_unknown() { return Z3_fixedpoint_get_reason_unknown(ctx(), m_fp); } + void update_rule(expr& rule, symbol const& name) { Z3_fixedpoint_update_rule(ctx(), m_fp, rule, name); check_error(); } + unsigned get_num_levels(func_decl& p) { unsigned r = Z3_fixedpoint_get_num_levels(ctx(), m_fp, p); check_error(); return r; } + expr get_cover_delta(int level, func_decl& p) { + Z3_ast r = Z3_fixedpoint_get_cover_delta(ctx(), m_fp, level, p); + check_error(); + return expr(ctx(), r); + } + void add_cover(int level, func_decl& p, expr& property) { Z3_fixedpoint_add_cover(ctx(), m_fp, level, p, property); check_error(); } + stats statistics() const { Z3_stats r = Z3_fixedpoint_get_statistics(ctx(), m_fp); check_error(); return stats(ctx(), r); } + void register_relation(func_decl& p) { Z3_fixedpoint_register_relation(ctx(), m_fp, p); } + expr_vector assertions() const { Z3_ast_vector r = Z3_fixedpoint_get_assertions(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); } + expr_vector rules() const { Z3_ast_vector r = Z3_fixedpoint_get_rules(ctx(), m_fp); check_error(); return expr_vector(ctx(), r); } + void set(params const & p) { Z3_fixedpoint_set_params(ctx(), m_fp, p); check_error(); } + std::string help() const { return Z3_fixedpoint_get_help(ctx(), m_fp); } + param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_fixedpoint_get_param_descrs(ctx(), m_fp)); } + std::string to_string() { return Z3_fixedpoint_to_string(ctx(), m_fp, 0, 0); } + std::string to_string(expr_vector const& queries) { + array qs(queries); + return Z3_fixedpoint_to_string(ctx(), m_fp, qs.size(), qs.ptr()); + } + void push() { Z3_fixedpoint_push(ctx(), m_fp); check_error(); } + void pop() { Z3_fixedpoint_pop(ctx(), m_fp); check_error(); } + }; + inline std::ostream & operator<<(std::ostream & out, fixedpoint const & f) { return out << Z3_fixedpoint_to_string(f.ctx(), f, 0, 0); } + inline tactic fail_if(probe const & p) { Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p); p.check_error(); diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index a0aba95d6..16d7fbb5f 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -7204,7 +7204,7 @@ def With(t, *args, **keys): >>> t((x + 1)*(y + 2) == 0) [[2*x + y + x*y == -2]] """ - ctx = keys.get('ctx', None) + ctx = keys.pop('ctx', None) t = _to_tactic(t, ctx) p = args2params(args, keys, t.ctx) return Tactic(Z3_tactic_using_params(t.ctx.ref(), t.tactic, p.params), t.ctx) diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index d8bf70e80..e039bcbd9 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -836,7 +836,7 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, return mk_to_ieee_bv(k, num_parameters, parameters, arity, domain, range); case OP_FPA_INTERNAL_BVWRAP: - return mk_internal_bv_wrap(k, num_parameters, parameters, arity, domain, range); + return mk_internal_bv_wrap(k, num_parameters, parameters, arity, domain, range); case OP_FPA_INTERNAL_BV2RM: return mk_internal_bv2rm(k, num_parameters, parameters, arity, domain, range); @@ -915,7 +915,7 @@ void fpa_decl_plugin::get_op_names(svector & op_names, symbol cons op_names.push_back(builtin_name("to_fp_unsigned", OP_FPA_TO_FP_UNSIGNED)); /* Extensions */ - op_names.push_back(builtin_name("to_ieee_bv", OP_FPA_TO_IEEE_BV)); + op_names.push_back(builtin_name("to_ieee_bv", OP_FPA_TO_IEEE_BV)); op_names.push_back(builtin_name("fp.to_ieee_bv", OP_FPA_TO_IEEE_BV)); } diff --git a/src/ast/rewriter/rewriter.h b/src/ast/rewriter/rewriter.h index fc596cabd..2b4f4b14e 100644 --- a/src/ast/rewriter/rewriter.h +++ b/src/ast/rewriter/rewriter.h @@ -315,6 +315,8 @@ protected: template void process_app(app * t, frame & fr); + bool constant_fold(app* t, frame& fr); + template void process_quantifier(quantifier * q, frame & fr); diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 61d177809..aecc1c93a 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -174,6 +174,38 @@ bool rewriter_tpl::visit(expr * t, unsigned max_depth) { } } +template +bool rewriter_tpl::constant_fold(app * t, frame & fr) { + if (fr.m_i == 1 && m().is_ite(t)) { + expr * cond = result_stack()[fr.m_spos].get(); + expr* arg = 0; + if (m().is_true(cond)) { + arg = t->get_arg(1); + } + else if (m().is_false(cond)) { + arg = t->get_arg(2); + } + if (arg) { + result_stack().shrink(fr.m_spos); + result_stack().push_back(arg); + fr.m_state = REWRITE_BUILTIN; + unsigned max_depth = fr.m_max_depth; + if (visit(arg, fr.m_max_depth)) { + m_r = result_stack().back(); + result_stack().pop_back(); + result_stack().pop_back(); + result_stack().push_back(m_r); + cache_result(t, m_r, m_pr, fr.m_cache_result); + frame_stack().pop_back(); + set_new_child_flag(t); + } + m_r = 0; + return true; + } + } + return false; +} + template template void rewriter_tpl::process_app(app * t, frame & fr) { @@ -183,10 +215,15 @@ void rewriter_tpl::process_app(app * t, frame & fr) { case PROCESS_CHILDREN: { unsigned num_args = t->get_num_args(); while (fr.m_i < num_args) { + if (!ProofGen && constant_fold(t, fr)) { + return; + } expr * arg = t->get_arg(fr.m_i); fr.m_i++; if (!visit(arg, fr.m_max_depth)) return; + + } func_decl * f = t->get_decl(); diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 4efb4b9d7..5ab4a695c 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -632,14 +632,25 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) { return BR_FAILED; } +/* + * (str.at s i), constants s/i, i < 0 or i >= |s| ==> (str.at s i) = "" + */ br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) { zstring c; rational r; - if (m_util.str.is_string(a, c) && m_autil.is_numeral(b, r) && r.is_unsigned()) { - unsigned j = r.get_unsigned(); - if (j < c.length()) { - result = m_util.str.mk_string(c.extract(j, 1)); + if (m_util.str.is_string(a, c) && m_autil.is_numeral(b, r)) { + if (r.is_neg()) { + result = m_util.str.mk_string(symbol("")); return BR_DONE; + } else if (r.is_unsigned()) { + unsigned j = r.get_unsigned(); + if (j < c.length()) { + result = m_util.str.mk_string(c.extract(j, 1)); + return BR_DONE; + } else { + result = m_util.str.mk_string(symbol("")); + return BR_DONE; + } } } return BR_FAILED; diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index b387e8810..091d5f402 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1554,6 +1554,7 @@ void cmd_context::validate_model() { p.set_uint("sort_store", true); p.set_bool("completion", true); model_evaluator evaluator(*(md.get()), p); + evaluator.set_expand_array_equalities(false); contains_array_op_proc contains_array(m()); { scoped_rlimit _rlimit(m().limit(), 0); diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index af2253801..61da4b3a0 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -50,6 +50,7 @@ struct evaluator_cfg : public default_rewriter_cfg { unsigned m_max_steps; bool m_model_completion; bool m_cache; + bool m_array_equalities; evaluator_cfg(ast_manager & m, model_core & md, params_ref const & p): m_model(md), @@ -81,6 +82,7 @@ struct evaluator_cfg : public default_rewriter_cfg { m_max_steps = p.max_steps(); m_model_completion = p.completion(); m_cache = p.cache(); + m_array_equalities = p.array_equalities(); } ast_manager & m() const { return m_model.get_manager(); } @@ -264,11 +266,14 @@ struct evaluator_cfg : public default_rewriter_cfg { br_status mk_array_eq(expr* a, expr* b, expr_ref& result) { - return BR_FAILED; if (a == b) { result = m().mk_true(); return BR_DONE; } + if (!m_array_equalities) { + return BR_FAILED; + } + // disabled until made more efficient vector stores1, stores2; bool args_are_unique1, args_are_unique2; @@ -508,6 +513,10 @@ void model_evaluator::set_model_completion(bool f) { m_imp->cfg().m_model_completion = f; } +void model_evaluator::set_expand_array_equalities(bool f) { + m_imp->cfg().m_array_equalities = f; +} + unsigned model_evaluator::get_num_steps() const { return m_imp->get_num_steps(); } diff --git a/src/model/model_evaluator.h b/src/model/model_evaluator.h index 3f4da5c96..ba55e96ba 100644 --- a/src/model/model_evaluator.h +++ b/src/model/model_evaluator.h @@ -35,6 +35,7 @@ public: ast_manager & m () const; void set_model_completion(bool f); + void set_expand_array_equalities(bool f); void updt_params(params_ref const & p); static void get_param_descrs(param_descrs & r); diff --git a/src/model/model_evaluator_params.pyg b/src/model/model_evaluator_params.pyg index b68d5c3ad..b6417f7fc 100644 --- a/src/model/model_evaluator_params.pyg +++ b/src/model/model_evaluator_params.pyg @@ -3,6 +3,7 @@ def_module_params('model_evaluator', params=(max_memory_param(), max_steps_param(), ('completion', BOOL, False, 'assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model'), - ('cache', BOOL, True, 'cache intermediate results in the model evaluator') + ('cache', BOOL, True, 'cache intermediate results in the model evaluator'), + ('array_equalities', BOOL, True, 'evaluate array equalities') )) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index ebe56381a..cd40944b2 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1002,7 +1002,8 @@ namespace opt { TRACE("opt", tout << "Term does not evaluate " << term << "\n";); return false; } - if (!m_arith.is_numeral(val, r)) { + unsigned bvsz; + if (!m_arith.is_numeral(val, r) && !m_bv.is_numeral(val, r, bvsz)) { TRACE("opt", tout << "model does not evaluate objective to a value\n";); return false; } diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 5d03a3563..ba9f970a2 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -3942,7 +3942,7 @@ namespace smt { #endif virtual void on_match(quantifier * qa, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, ptr_vector & used_enodes) { - TRACE("trigger_bug", tout << "found match\n";); + TRACE("trigger_bug", tout << "found match " << mk_pp(qa, m_ast_manager) << "\n";); #ifdef Z3DEBUG if (m_check_missing_instances) { if (!m_context.slow_contains_instance(qa, num_bindings, bindings)) { diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index a7875e99e..129bed87e 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -93,6 +93,7 @@ bool proto_model::is_select_of_model_value(expr* e) const { bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { m_eval.set_model_completion(model_completion); + m_eval.set_expand_array_equalities(false); try { m_eval(e, result); #if 0 diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 29321ecf7..f0eea7ea8 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -306,7 +306,6 @@ namespace smt { TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " "; display_literal_verbose(tout, l); tout << " level: " << m_scope_lvl << "\n"; display(tout, j);); - SASSERT(l.var() < static_cast(m_b_internalized_stack.size())); m_assigned_literals.push_back(l); m_assignment[l.index()] = l_true; m_assignment[(~l).index()] = l_false; @@ -321,14 +320,23 @@ namespace smt { d.m_phase_available = true; d.m_phase = !l.sign(); TRACE("phase_selection", tout << "saving phase, is_pos: " << d.m_phase << " l: " << l << "\n";); + TRACE("relevancy", - tout << "is_atom: " << d.is_atom() << " is relevant: " << is_relevant_core(bool_var2expr(l.var())) << "\n";); - if (d.is_atom() && (m_fparams.m_relevancy_lvl == 0 || (m_fparams.m_relevancy_lvl == 1 && !d.is_quantifier()) || is_relevant_core(bool_var2expr(l.var())))) + tout << "is_atom: " << d.is_atom() << " is relevant: " << is_relevant_core(l) << "\n";); + if (d.is_atom() && (m_fparams.m_relevancy_lvl == 0 || (m_fparams.m_relevancy_lvl == 1 && !d.is_quantifier()) || is_relevant_core(l))) m_atom_propagation_queue.push_back(l); if (m_manager.has_trace_stream()) trace_assign(l, j, decision); m_case_split_queue->assign_lit_eh(l); + + // a unit is asserted at search level. Mark it as relevant. + // this addresses bug... where a literal becomes fixed to true (false) + // as a conflict gets assigned misses relevancy (and quantifier instantiation). + // + if (false && !decision && relevancy() && at_search_level() && !is_relevant_core(l)) { + mark_as_relevant(l); + } } bool context::bcp() { @@ -1637,7 +1645,7 @@ namespace smt { m_atom_propagation_queue.push_back(literal(v, val == l_false)); } } - TRACE("propagate_relevancy", tout << "marking as relevant:\n" << mk_bounded_pp(n, m_manager) << "\n";); + TRACE("propagate_relevancy", tout << "marking as relevant:\n" << mk_bounded_pp(n, m_manager) << " " << m_scope_lvl << "\n";); #ifndef SMTCOMP m_case_split_queue->relevant_eh(n); #endif @@ -3895,6 +3903,7 @@ namespace smt { // I invoke pop_scope_core instead of pop_scope because I don't want // to reset cached generations... I need them to rebuild the literals // of the new conflict clause. + if (relevancy()) record_relevancy(num_lits, lits); unsigned num_bool_vars = pop_scope_core(m_scope_lvl - new_lvl); SASSERT(m_scope_lvl == new_lvl); // the logical context may still be in conflict after @@ -3926,6 +3935,7 @@ namespace smt { } } } + if (relevancy()) restore_relevancy(num_lits, lits); // Resetting the cache manually because I did not invoke pop_scope, but pop_scope_core reset_cache_generation(); TRACE("resolve_conflict_bug", @@ -4008,6 +4018,28 @@ namespace smt { } return false; } + + /* + \brief we record and restore relevancy information for literals in conflict clauses. + A literal may have been marked relevant within the scope that gets popped during + conflict resolution. In this case, the literal is no longer marked as relevant after + the pop. This can cause quantifier instantiation to miss relevant triggers and thereby + cause incmpleteness. + */ + void context::record_relevancy(unsigned n, literal const* lits) { + m_relevant_conflict_literals.reset(); + for (unsigned i = 0; i < n; ++i) { + m_relevant_conflict_literals.push_back(is_relevant(lits[i])); + } + } + + void context::restore_relevancy(unsigned n, literal const* lits) { + for (unsigned i = 0; i < n; ++i) { + if (m_relevant_conflict_literals[i] && !is_relevant(lits[i])) { + mark_as_relevant(lits[i]); + } + } + } void context::get_relevant_labels(expr* cnstr, buffer & result) { if (m_fparams.m_check_at_labels) { @@ -4281,6 +4313,7 @@ namespace smt { if (fcs == FC_DONE) { mk_proto_model(l_true); m_model = m_proto_model->mk_model(); + add_rec_funs_to_model(); } return fcs == FC_DONE; @@ -4333,8 +4366,51 @@ namespace smt { return m_last_search_failure; } + void context::add_rec_funs_to_model() { + ast_manager& m = m_manager; + SASSERT(m_model); + for (unsigned i = 0; i < m_asserted_formulas.get_num_formulas(); ++i) { + expr* e = m_asserted_formulas.get_formula(i); + if (is_quantifier(e)) { + quantifier* q = to_quantifier(e); + if (!m.is_rec_fun_def(q)) continue; + SASSERT(q->get_num_patterns() == 1); + expr* fn = to_app(q->get_pattern(0))->get_arg(0); + SASSERT(is_app(fn)); + func_decl* f = to_app(fn)->get_decl(); + expr* eq = q->get_expr(); + expr_ref body(m); + if (is_fun_def(fn, q->get_expr(), body)) { + func_interp* fi = alloc(func_interp, m, f->get_arity()); + fi->set_else(body); + m_model->register_decl(f, fi); + } + } + } + } + + bool context::is_fun_def(expr* f, expr* body, expr_ref& result) { + expr* t1, *t2, *t3; + if (m_manager.is_eq(body, t1, t2) || m_manager.is_iff(body, t1, t2)) { + if (t1 == f) return result = t2, true; + if (t2 == f) return result = t1, true; + return false; + } + if (m_manager.is_ite(body, t1, t2, t3)) { + expr_ref body1(m_manager), body2(m_manager); + if (is_fun_def(f, t2, body1) && is_fun_def(f, t3, body2)) { + // f is not free in t1 + result = m_manager.mk_ite(t1, body1, body2); + return true; + } + } + return false; + } + + }; + #ifdef Z3DEBUG void pp(smt::context & c) { c.display(std::cout); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index e23ecaf43..9532c806f 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -209,6 +209,7 @@ namespace smt { ~scoped_mk_model() { if (m_ctx.m_proto_model.get() != 0) { m_ctx.m_model = m_ctx.m_proto_model->mk_model(); + m_ctx.add_rec_funs_to_model(); m_ctx.m_proto_model = 0; // proto_model is not needed anymore. } } @@ -1132,6 +1133,10 @@ namespace smt { bool is_relevant_core(expr * n) const { return m_relevancy_propagator->is_relevant(n); } + svector m_relevant_conflict_literals; + void record_relevancy(unsigned n, literal const* lits); + void restore_relevancy(unsigned n, literal const* lits); + public: // event handler for relevancy_propagator class void relevant_eh(expr * n); @@ -1153,6 +1158,10 @@ namespace smt { return is_relevant(l.var()); } + bool is_relevant_core(literal l) const { + return is_relevant_core(bool_var2expr(l.var())); + } + void mark_as_relevant(expr * n) { m_relevancy_propagator->mark_as_relevant(n); m_relevancy_propagator->propagate(); } void mark_as_relevant(enode * n) { mark_as_relevant(n->get_owner()); } @@ -1186,6 +1195,10 @@ namespace smt { bool propagate(); + void add_rec_funs_to_model(); + + bool is_fun_def(expr* f, expr* q, expr_ref& body); + public: bool can_propagate() const; diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 5329cd80f..093d215b6 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -290,7 +290,7 @@ namespace smt { while (true) { lbool r = m_aux_context->check(); - TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";); + TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";); if (r != l_true) break; model_ref cex; @@ -300,7 +300,7 @@ namespace smt { } num_new_instances++; if (num_new_instances >= m_max_cexs || !add_blocking_clause(cex.get(), sks)) { - TRACE("model_checker", tout << "Add blocking clause failed\n";); + TRACE("model_checker", tout << "Add blocking clause failed new-instances: " << num_new_instances << " max-cex: " << m_max_cexs << "\n";); // add_blocking_clause failed... stop the search for new counter-examples... break; } @@ -407,6 +407,7 @@ namespace smt { found_relevant = true; if (m.is_rec_fun_def(q)) { if (!check_rec_fun(q)) { + TRACE("model_checker", tout << "checking recursive function failed\n";); num_failures++; } } @@ -414,6 +415,7 @@ namespace smt { if (m_params.m_mbqi_trace || get_verbosity_level() >= 5) { verbose_stream() << "(smt.mbqi :failed " << q->get_qid() << ")\n"; } + TRACE("model_checker", tout << "checking quantifier " << mk_pp(q, m) << " failed\n";); num_failures++; } } @@ -452,6 +454,7 @@ namespace smt { } bool model_checker::has_new_instances() { + TRACE("model_checker", tout << "instances: " << m_new_instances.size() << "\n";); return !m_new_instances.empty(); } diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 2a56168f2..bad788f5d 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -52,8 +52,9 @@ namespace smt { m_qi_queue.setup(); } - bool has_trace_stream() const { return m_context.get_manager().has_trace_stream(); } - std::ostream & trace_stream() { return m_context.get_manager().trace_stream(); } + ast_manager& m() const { return m_context.get_manager(); } + bool has_trace_stream() const { return m().has_trace_stream(); } + std::ostream & trace_stream() { return m().trace_stream(); } quantifier_stat * get_stat(quantifier * q) const { return m_quantifier_stat.find(q); @@ -110,8 +111,9 @@ namespace smt { unsigned max_top_generation, ptr_vector & used_enodes) { max_generation = std::max(max_generation, get_generation(q)); - if (m_num_instances > m_params.m_qi_max_instances) + if (m_num_instances > m_params.m_qi_max_instances) { return false; + } get_stat(q)->update_max_generation(max_generation); fingerprint * f = m_context.add_fingerprint(q, q->get_id(), num_bindings, bindings); if (f) { @@ -132,9 +134,17 @@ namespace smt { } m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO m_num_instances++; - return true; } - return false; + TRACE("quantifier", + tout << mk_pp(q, m()) << " "; + for (unsigned i = 0; i < num_bindings; ++i) { + tout << mk_pp(bindings[i]->get_owner(), m()) << " "; + } + tout << "\n"; + tout << "inserted: " << (f != 0) << "\n"; + ); + + return f != 0; } void init_search_eh() { @@ -186,7 +196,7 @@ namespace smt { } bool check_quantifier(quantifier* q) { - return m_context.is_relevant(q) && m_context.get_assignment(q) == l_true; // && !m_context.get_manager().is_rec_fun_def(q); + return m_context.is_relevant(q) && m_context.get_assignment(q) == l_true; // && !m().is_rec_fun_def(q); } bool quick_check_quantifiers() { @@ -501,13 +511,13 @@ namespace smt { SASSERT(m_context->get_manager().is_pattern(mp)); bool unary = (mp->get_num_args() == 1); if (!unary && j >= num_eager_multi_patterns) { - TRACE("assign_quantifier", tout << "delaying (too many multipatterns):\n" << mk_ismt2_pp(mp, m_context->get_manager()) << "\n" + TRACE("quantifier", tout << "delaying (too many multipatterns):\n" << mk_ismt2_pp(mp, m_context->get_manager()) << "\n" << "j: " << j << " unary: " << unary << " m_params.m_qi_max_eager_multipatterns: " << m_fparams->m_qi_max_eager_multipatterns << " num_eager_multi_patterns: " << num_eager_multi_patterns << "\n";); m_lazy_mam->add_pattern(q, mp); } else { - TRACE("assign_quantifier", tout << "adding:\n" << mk_ismt2_pp(mp, m_context->get_manager()) << "\n";); + TRACE("quantifier", tout << "adding:\n" << mk_ismt2_pp(mp, m_context->get_manager()) << "\n";); m_mam->add_pattern(q, mp); } if (!unary) diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h index bc731bf9c..bc249ed1a 100644 --- a/src/smt/smt_quantifier.h +++ b/src/smt/smt_quantifier.h @@ -165,6 +165,8 @@ namespace smt { virtual void push() = 0; virtual void pop(unsigned num_scopes) = 0; + + }; }; diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index 1eb6be08e..d67643edf 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -228,7 +228,7 @@ public: if (m_inc_timeout == UINT_MAX) { IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 2 (without a timeout)\")\n";); lbool r = m_solver2->check_sat(num_assumptions, assumptions); - if (r != l_undef || !use_solver1_when_undef()) { + if (r != l_undef || !use_solver1_when_undef() || get_manager().canceled()) { return r; } } @@ -285,10 +285,9 @@ public: } virtual void collect_statistics(statistics & st) const { + m_solver2->collect_statistics(st); if (m_use_solver1_results) m_solver1->collect_statistics(st); - else - m_solver2->collect_statistics(st); } virtual void get_unsat_core(ptr_vector & r) { diff --git a/src/tactic/extension_model_converter.cpp b/src/tactic/extension_model_converter.cpp index ee6b8f691..18b5b6288 100644 --- a/src/tactic/extension_model_converter.cpp +++ b/src/tactic/extension_model_converter.cpp @@ -49,6 +49,7 @@ void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) { TRACE("extension_mc", model_v2_pp(tout, *md); display_decls_info(tout, md);); model_evaluator ev(*(md.get())); ev.set_model_completion(true); + ev.set_expand_array_equalities(false); expr_ref val(m()); unsigned i = m_vars.size(); while (i > 0) { diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp index 044511c33..7d428b369 100644 --- a/src/tactic/smtlogics/quant_tactics.cpp +++ b/src/tactic/smtlogics/quant_tactics.cpp @@ -28,6 +28,7 @@ Revision History: #include"ctx_simplify_tactic.h" #include"smt_tactic.h" #include"elim_term_ite_tactic.h" +#include"probe_arith.h" static tactic * mk_quant_preprocessor(ast_manager & m, bool disable_gaussian = false) { params_ref pull_ite_p; @@ -107,8 +108,10 @@ tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) { tactic * st = and_then(mk_quant_preprocessor(m), mk_qe_lite_tactic(m, p), cond(mk_has_quantifier_probe(), - or_else(mk_qsat_tactic(m, p), - and_then(mk_qe_tactic(m), mk_smt_tactic())), + cond(mk_is_lira_probe(), + or_else(mk_qsat_tactic(m, p), + and_then(mk_qe_tactic(m), mk_smt_tactic())), + mk_smt_tactic()), mk_smt_tactic())); st->updt_params(p); return st; diff --git a/src/util/vector.h b/src/util/vector.h index 03c1d6019..7ffee2535 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -374,6 +374,11 @@ public: } } + void fill(unsigned sz, T const & elem) { + resize(sz); + fill(sz, elem); + } + bool contains(T const & elem) const { const_iterator it = begin(); const_iterator e = end(); diff --git a/src/util/version.h.cmake.in b/src/util/version.h.cmake.in new file mode 100644 index 000000000..af3a652a6 --- /dev/null +++ b/src/util/version.h.cmake.in @@ -0,0 +1,8 @@ +// automatically generated file. +#define Z3_MAJOR_VERSION @Z3_VERSION_MAJOR@ +#define Z3_MINOR_VERSION @Z3_VERSION_MINOR@ +#define Z3_BUILD_NUMBER @Z3_VERSION_PATCH@ +#define Z3_REVISION_NUMBER @Z3_VERSION_TWEAK@ + +#define Z3_FULL_VERSION @Z3_FULL_VERSION@ +#cmakedefine Z3GITHASH @Z3GITHASH@