diff --git a/.dockerignore b/.dockerignore new file mode 100644 index 000000000..e85dae524 --- /dev/null +++ b/.dockerignore @@ -0,0 +1,4 @@ +**/*.swp +**/*.pyc +.git +**/*.Dockerfile diff --git a/.travis.yml b/.travis.yml new file mode 100644 index 000000000..e8e207466 --- /dev/null +++ b/.travis.yml @@ -0,0 +1,68 @@ +cache: + # This persistent cache is used to cache the building of + # docker base images. + directories: + - $DOCKER_TRAVIS_CI_CACHE_DIR +sudo: required +language: cpp +services: + - docker +env: + global: + # This environment variable tells the `travis_ci_linux_entry_point.sh` + # script to look for a cached Docker image. + - DOCKER_TRAVIS_CI_CACHE_DIR=$HOME/.cache/docker + # Configurations + matrix: +############################################################################### +# Ubuntu 16.04 LTS +############################################################################### + # 64-bit GCC 5.4 RelWithDebInfo + - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo + # 64-bit Clang 3.9 RelWithDebInfo + - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo + + # 64-bit GCC 5.4 Debug + - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug + # 64-bit Clang Debug + - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug + + # 32-bit GCC 5.4 RelWithDebInfo + - LINUX_BASE=ubuntu32_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=i686 Z3_BUILD_TYPE=RelWithDebInfo + + # Both of the two configurations below build the docs because the current + # implementation uses python as part of the building process. + # TODO: Teach one of the configurations to upload built docs somewhere. + # Test with Python 3 and API docs + - LINUX_BASE=ubuntu_16.04 PYTHON_EXECUTABLE=/usr/bin/python3 BUILD_DOCS=1 + # Test with LibGMP and API docs + - LINUX_BASE=ubuntu_16.04 TARGET_ARCH=x86_64 USE_LIBGMP=1 BUILD_DOCS=1 PYTHON_EXECUTABLE=/usr/bin/python2.7 + + # Test without OpenMP + - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0 + + # Unix Makefile generator build + - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_CMAKE_GENERATOR="Unix Makefiles" + + # LTO build + - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 USE_LTO=1 + + # Static build. Note we have disable building the bindings because they won't work with a static libz3 + - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_STATIC_BUILD=1 DOTNET_BINDINGS=0 JAVA_BINDINGS=0 PYTHON_BINDINGS=0 + +############################################################################### +# Ubuntu 14.04 LTS +############################################################################### + # GCC 4.8 + # 64-bit GCC 4.8 RelWithDebInfo + - LINUX_BASE=ubuntu_14.04 C_COMPILER=/usr/bin/gcc-4.8 CXX_COMPILER=/usr/bin/g++-4.8 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo + # 64-bit GCC 4.8 Debug + - LINUX_BASE=ubuntu_14.04 C_COMPILER=/usr/bin/gcc-4.8 CXX_COMPILER=/usr/bin/g++-4.8 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug + +# TODO: OSX support +#matrix: +# include: +# - os: osx +# osx_image: xcode 8.2 +script: + - contrib/ci/scripts/travis_ci_entry_point.sh diff --git a/README-CMake.md b/README-CMake.md index 7550808fc..715cacad2 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -266,6 +266,8 @@ The following useful options can be passed to CMake whilst configuring. Disabling this is useful for faster incremental builds. The documentation can be manually built by invoking the ``api_docs`` target. * ``LINK_TIME_OPTIMIZATION`` - BOOL. If set to ``TRUE`` link time optimization will be enabled. * ``API_LOG_SYNC`` - BOOL. If set to ``TRUE`` will enable experimental API log sync feature. +* ``WARNINGS_AS_ERRORS`` - STRING. If set to ``TRUE`` compiler warnings will be treated as errors. If set to ``False`` compiler warnings will not be treated as errors. + If set to ``SERIOUS_ONLY`` a subset of compiler warnings will be treated as errors. 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. @@ -381,3 +383,13 @@ It is tempting use file-globbing in ``CMakeLists.txt`` to find a set for files m use them as the sources to build a target. This however is a bad idea because it prevents CMake from knowing when it needs to rerun itself. This is why source file names are explicitly listed in the ``CMakeLists.txt`` so that when changes are made the source files used to build a target automatically triggers a rerun of CMake. Long story short. Don't use file globbing. + +### Serious warning flags + +By default the `WARNINGS_AS_ERRORS` flag is set to `SERIOUS_ONLY` which means +some warnings will be treated as errors. These warnings are controlled by the +relevant `*_WARNINGS_AS_ERRORS` list defined in +`cmake/compiler_warnings.cmake`. + +Additional warnings should only be added here if the warnings has no false +positives. diff --git a/README.md b/README.md index f92a5389a..197928877 100644 --- a/README.md +++ b/README.md @@ -12,9 +12,9 @@ See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z ## Build status -| Windows x86 | Windows x64 | Ubuntu x64 | Ubuntu x86 | Debian x64 | OSX | -| ----------- | ----------- | ---------- | ---------- | ---------- | --- | -![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge) | ![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge) | ![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge) | ![ubuntu-x86-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/6/badge) | ![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge) | ![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge) +| Windows x86 | Windows x64 | Ubuntu x64 | Ubuntu x86 | Debian x64 | OSX | TravisCI | +| ----------- | ----------- | ---------- | ---------- | ---------- | --- | -------- | +[![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=4) | [![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=7) | [![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=3) | [![ubuntu-x86-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/6/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=6) | [![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=5) | [![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3) [1]: #building-z3-on-windows-using-visual-studio-command-prompt [2]: #building-z3-using-make-and-gccclang diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake index e02b28b2c..183f490dd 100644 --- a/cmake/compiler_warnings.cmake +++ b/cmake/compiler_warnings.cmake @@ -1,17 +1,61 @@ +################################################################################ +# Compiler warning flags +################################################################################ +# These are passed to relevant compiler provided they are supported set(GCC_AND_CLANG_WARNINGS - "-Wall" + "-Wall" ) set(GCC_ONLY_WARNINGS "") set(CLANG_ONLY_WARNINGS "") set(MSVC_WARNINGS "/W3") +################################################################################ +# Serious warnings +################################################################################ +# This declares the flags that are passed to the compiler when +# `WARNINGS_AS_ERRORS` is set to `SERIOUS_ONLY`. Only flags that are supported +# by the compiler are used. +# +# In effect this a "whitelist" approach where we explicitly tell the compiler +# which warnings we want to be treated as errors. The alternative would be a +# "blacklist" approach where we ask the compiler to treat all warnings are +# treated as errors but then we explicitly list which warnings which should be +# allowed. +# +# The "whitelist" approach seems simpiler because we can incrementally add +# warnings we "think are serious". + +# TODO: Add more warnings that are considered serious enough that we should +# treat them as errors. +set(GCC_AND_CLANG_WARNINGS_AS_ERRORS + # https://clang.llvm.org/docs/DiagnosticsReference.html#wodr + "-Werror=odr" +) +set(GCC_WARNINGS_AS_ERRORS + "" +) +set(CLANG_WARNINGS_AS_ERRORS + # https://clang.llvm.org/docs/DiagnosticsReference.html#wdelete-non-virtual-dtor + "-Werror=delete-non-virtual-dtor" + # https://clang.llvm.org/docs/DiagnosticsReference.html#woverloaded-virtual + "-Werror=overloaded-virtual" +) + +################################################################################ +# Test warning/error flags +################################################################################ set(WARNING_FLAGS_TO_CHECK "") +set(WARNING_AS_ERROR_FLAGS_TO_CHECK "") if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS}) list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_ONLY_WARNINGS}) + list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_AS_ERRORS}) + list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_WARNINGS_AS_ERRORS}) elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS}) list(APPEND WARNING_FLAGS_TO_CHECK ${CLANG_ONLY_WARNINGS}) + list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_AS_ERRORS}) + list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${CLANG_WARNINGS_AS_ERRORS}) # FIXME: Remove "x.." when CMP0054 is set to NEW elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC") list(APPEND WARNING_FLAGS_TO_CHECK ${MSVC_WARNINGS}) @@ -31,8 +75,40 @@ foreach (flag ${WARNING_FLAGS_TO_CHECK}) z3_add_cxx_flag("${flag}") endforeach() -option(WARNINGS_AS_ERRORS "Treat compiler warnings as errors" OFF) -if (WARNINGS_AS_ERRORS) +# TODO: Remove this eventually. +# Detect legacy `WARNINGS_AS_ERRORS` boolean option and covert to new +# to new option type. +get_property( + WARNINGS_AS_ERRORS_CACHE_VAR_TYPE + CACHE + WARNINGS_AS_ERRORS + PROPERTY + TYPE +) +if ("${WARNINGS_AS_ERRORS_CACHE_VAR_TYPE}" STREQUAL "BOOL") + message(WARNING "Detected legacy WARNINGS_AS_ERRORS option. Upgrading") + set(WARNINGS_AS_ERRORS_DEFAULT "${WARNINGS_AS_ERRORS}") + # Delete old entry + unset(WARNINGS_AS_ERRORS CACHE) +else() + set(WARNINGS_AS_ERRORS_DEFAULT "SERIOUS_ONLY") +endif() + +set(WARNINGS_AS_ERRORS + ${WARNINGS_AS_ERRORS_DEFAULT} + CACHE STRING + "Treat warnings as errors. ON, OFF, or SERIOUS_ONLY" +) + # Set GUI options +set_property( + CACHE + WARNINGS_AS_ERRORS + PROPERTY STRINGS + "ON;OFF;SERIOUS_ONLY" +) + +if ("${WARNINGS_AS_ERRORS}" STREQUAL "ON") + message(STATUS "Treating compiler warnings as errors") if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) list(APPEND Z3_COMPONENT_CXX_FLAGS "-Werror") # FIXME: Remove "x.." when CMP0054 is set to NEW @@ -41,8 +117,14 @@ if (WARNINGS_AS_ERRORS) else() message(AUTHOR_WARNING "Unknown compiler") endif() - message(STATUS "Treating compiler warnings as errors") -else() +elseif ("${WARNINGS_AS_ERRORS}" STREQUAL "SERIOUS_ONLY") + message(STATUS "Treating only serious compiler warnings as errors") + # Loop through the flags + foreach (flag ${WARNING_AS_ERROR_FLAGS_TO_CHECK}) + # Add globally because some flags need to be passed at link time. + z3_add_cxx_flag("${flag}" GLOBAL) + endforeach() +elseif ("${WARNINGS_AS_ERRORS}" STREQUAL "OFF") message(STATUS "Not treating compiler warnings as errors") # FIXME: Remove "x.." when CMP0054 is set to NEW if ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC") @@ -51,4 +133,8 @@ else() # build system. list(APPEND Z3_COMPONENT_CXX_FLAGS "/WX-") endif() +else() + message(FATAL_ERROR + "WARNINGS_AS_ERRORS set to unsupported value \"${WARNINGS_AS_ERRORS}\"" + ) endif() diff --git a/cmake/z3_add_cxx_flag.cmake b/cmake/z3_add_cxx_flag.cmake index 6e756d3b9..d2624d890 100644 --- a/cmake/z3_add_cxx_flag.cmake +++ b/cmake/z3_add_cxx_flag.cmake @@ -2,7 +2,7 @@ include(CheckCXXCompilerFlag) include(CMakeParseArguments) function(z3_add_cxx_flag flag) - CMAKE_PARSE_ARGUMENTS(z3_add_flag "REQUIRED" "" "" ${ARGN}) + CMAKE_PARSE_ARGUMENTS(z3_add_flag "REQUIRED;GLOBAL" "" "" ${ARGN}) string(REPLACE "-" "_" SANITIZED_FLAG_NAME "${flag}") string(REPLACE "/" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") string(REPLACE "=" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") @@ -16,8 +16,13 @@ function(z3_add_cxx_flag flag) endif() if (HAS_${SANITIZED_FLAG_NAME}) message(STATUS "C++ compiler supports ${flag}") - list(APPEND Z3_COMPONENT_CXX_FLAGS "${flag}") - set(Z3_COMPONENT_CXX_FLAGS "${Z3_COMPONENT_CXX_FLAGS}" PARENT_SCOPE) + if (z3_add_flag_GLOBAL) + # Set globally + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${flag} " PARENT_SCOPE) + else() + list(APPEND Z3_COMPONENT_CXX_FLAGS "${flag}") + set(Z3_COMPONENT_CXX_FLAGS "${Z3_COMPONENT_CXX_FLAGS}" PARENT_SCOPE) + endif() else() message(STATUS "C++ compiler does not support ${flag}") endif() diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile new file mode 100644 index 000000000..d8a32edea --- /dev/null +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile @@ -0,0 +1,50 @@ +# This base image is not officially supported by Docker it +# is generated by running +# ``` +# ./update.sh xenial +# ``` +# from git@github.com:daald/docker-brew-ubuntu-core-32bit.git +# at commit 34ea593b40b423755b7d46b6c8c89fc8162ea74b +# +# We could actually store the image generated by this Dockerfile +# rather than just the bare image. However given we have a TravisCI +# cache I'm not sure if it faster to use the TravisCI cache or to +# download from DockerHub everytime. +FROM z3prover/ubuntu32:16.04 + +RUN apt-get update && \ + apt-get -y --no-install-recommends install \ + binutils \ + clang \ + clang-3.9 \ + cmake \ + doxygen \ + default-jdk \ + gcc \ + gcc-5 \ + git \ + graphviz \ + g++ \ + g++ \ + libgmp-dev \ + libgomp1 \ + libomp5 \ + libomp-dev \ + make \ + mono-devel \ + ninja-build \ + python3 \ + python3-setuptools \ + python2.7 \ + python-setuptools \ + sudo + +# Create `user` user for container with password `user`. and give it +# password-less sudo access +RUN useradd -m user && \ + echo user:user | chpasswd && \ + cp /etc/sudoers /etc/sudoers.bak && \ + echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers +USER user +WORKDIR /home/user + diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile new file mode 100644 index 000000000..c28e59e97 --- /dev/null +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile @@ -0,0 +1,35 @@ +FROM ubuntu:14.04 + +RUN apt-get update && \ + apt-get -y --no-install-recommends install \ + binutils \ + clang-3.9 \ + cmake \ + doxygen \ + default-jdk \ + gcc-multilib \ + gcc-4.8-multilib \ + git \ + graphviz \ + g++-multilib \ + g++-4.8-multilib \ + libgmp-dev \ + libgomp1 \ + lib32gomp1 \ + make \ + mono-devel \ + ninja-build \ + python3 \ + python3-setuptools \ + python2.7 \ + python-setuptools + +# Create `user` user for container with password `user`. and give it +# password-less sudo access +RUN useradd -m user && \ + echo user:user | chpasswd && \ + cp /etc/sudoers /etc/sudoers.bak && \ + echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers +USER user +WORKDIR /home/user + diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile new file mode 100644 index 000000000..98a5a3e09 --- /dev/null +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile @@ -0,0 +1,38 @@ +FROM ubuntu:16.04 + +RUN apt-get update && \ + apt-get -y --no-install-recommends install \ + binutils \ + clang \ + clang-3.9 \ + cmake \ + doxygen \ + default-jdk \ + gcc-multilib \ + gcc-5-multilib \ + git \ + graphviz \ + g++-multilib \ + g++-5-multilib \ + libgmp-dev \ + libgomp1 \ + libomp5 \ + libomp-dev \ + make \ + mono-devel \ + ninja-build \ + python3 \ + python3-setuptools \ + python2.7 \ + python-setuptools \ + sudo + +# Create `user` user for container with password `user`. and give it +# password-less sudo access +RUN useradd -m user && \ + echo user:user | chpasswd && \ + cp /etc/sudoers /etc/sudoers.bak && \ + echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers +USER user +WORKDIR /home/user + diff --git a/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile new file mode 100644 index 000000000..2d16d5394 --- /dev/null +++ b/contrib/ci/Dockerfiles/z3_build.Dockerfile @@ -0,0 +1,111 @@ +ARG DOCKER_IMAGE_BASE +FROM ${DOCKER_IMAGE_BASE} + + +# Specify defaults. This can be changed when invoking +# `docker build`. +ARG ASAN_BUILD=0 +ARG BUILD_DOCS=0 +ARG CC=gcc +ARG CXX=g++ +ARG DOTNET_BINDINGS=1 +ARG JAVA_BINDINGS=1 +ARG NO_SUPPRESS_OUTPUT=0 +ARG PYTHON_BINDINGS=1 +ARG PYTHON_EXECUTABLE=/usr/bin/python2.7 +ARG RUN_SYSTEM_TESTS=1 +ARG RUN_UNIT_TESTS=1 +ARG TARGET_ARCH=x86_64 +ARG TEST_INSTALL=1 +ARG UBSAN_BUILD=0 +ARG USE_LIBGMP=0 +ARG USE_LTO=0 +ARG USE_OPENMP=1 +ARG Z3_SRC_DIR=/home/user/z3_src +ARG Z3_BUILD_TYPE=RelWithDebInfo +ARG Z3_CMAKE_GENERATOR=Ninja +ARG Z3_INSTALL_PREFIX=/usr +ARG Z3_STATIC_BUILD=0 +# Blank default indicates use latest. +ARG Z3_SYSTEM_TEST_GIT_REVISION +ARG Z3_WARNINGS_AS_ERRORS=SERIOUS_ONLY +ARG Z3_VERBOSE_BUILD_OUTPUT=0 + +ENV \ + ASAN_BUILD=${ASAN_BUILD} \ + BUILD_DOCS=${BUILD_DOCS} \ + CC=${CC} \ + CXX=${CXX} \ + DOTNET_BINDINGS=${DOTNET_BINDINGS} \ + JAVA_BINDINGS=${JAVA_BINDINGS} \ + NO_SUPPRESS_OUTPUT=${NO_SUPPRESS_OUTPUT} \ + PYTHON_BINDINGS=${PYTHON_BINDINGS} \ + PYTHON_EXECUTABLE=${PYTHON_EXECUTABLE} \ + RUN_SYSTEM_TESTS=${RUN_SYSTEM_TESTS} \ + RUN_UNIT_TESTS=${RUN_UNIT_TESTS} \ + TARGET_ARCH=${TARGET_ARCH} \ + TEST_INSTALL=${TEST_INSTALL} \ + UBSAN_BUILD=${UBSAN_BUILD} \ + USE_LIBGMP=${USE_LIBGMP} \ + USE_LTO=${USE_LTO} \ + USE_OPENMP=${USE_OPENMP} \ + Z3_SRC_DIR=${Z3_SRC_DIR} \ + Z3_BUILD_DIR=/home/user/z3_build \ + Z3_CMAKE_GENERATOR=${Z3_CMAKE_GENERATOR} \ + Z3_VERBOSE_BUILD_OUTPUT=${Z3_VERBOSE_BUILD_OUTPUT} \ + Z3_STATIC_BUILD=${Z3_STATIC_BUILD} \ + Z3_SYSTEM_TEST_DIR=/home/user/z3_system_test \ + Z3_SYSTEM_TEST_GIT_REVISION=${Z3_SYSTEM_TEST_GIT_REVISION} \ + Z3_WARNINGS_AS_ERRORS=${Z3_WARNINGS_AS_ERRORS} \ + Z3_INSTALL_PREFIX=${Z3_INSTALL_PREFIX} + +# We add context across incrementally to maximal cache reuse + +# Build Z3 +RUN mkdir -p "${Z3_SRC_DIR}" && \ + mkdir -p "${Z3_SRC_DIR}/contrib/ci/scripts" +# Deliberately leave out `contrib` +ADD /cmake ${Z3_SRC_DIR}/cmake/ +ADD /doc ${Z3_SRC_DIR}/doc/ +ADD /examples ${Z3_SRC_DIR}/examples/ +ADD /scripts ${Z3_SRC_DIR}/scripts/ +ADD /src ${Z3_SRC_DIR}/src/ +ADD *.txt *.md RELEASE_NOTES ${Z3_SRC_DIR}/ + +ADD \ + /contrib/ci/scripts/build_z3_cmake.sh \ + /contrib/ci/scripts/set_compiler_flags.sh \ + /contrib/ci/scripts/set_generator_args.sh \ + ${Z3_SRC_DIR}/contrib/ci/scripts/ +RUN ${Z3_SRC_DIR}/contrib/ci/scripts/build_z3_cmake.sh + +# Test building docs +ADD \ + /contrib/ci/scripts/test_z3_docs.sh \ + /contrib/ci/scripts/run_quiet.sh \ + ${Z3_SRC_DIR}/contrib/ci/scripts/ +RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_docs.sh + +# Test examples +ADD \ + /contrib/ci/scripts/test_z3_examples_cmake.sh \ + ${Z3_SRC_DIR}/contrib/ci/scripts/ +RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_examples_cmake.sh + +# Run unit tests +ADD \ + /contrib/ci/scripts/test_z3_unit_tests_cmake.sh \ + ${Z3_SRC_DIR}/contrib/ci/scripts/ +RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_unit_tests_cmake.sh + +# Run system tests +ADD \ + /contrib/ci/scripts/test_z3_system_tests.sh \ + ${Z3_SRC_DIR}/contrib/ci/scripts/ +RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_system_tests.sh + +# Test install +ADD \ + /contrib/ci/scripts/test_z3_install_cmake.sh \ + ${Z3_SRC_DIR}/contrib/ci/scripts/ +RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_install_cmake.sh diff --git a/contrib/ci/README.md b/contrib/ci/README.md new file mode 100644 index 000000000..2e117c8b1 --- /dev/null +++ b/contrib/ci/README.md @@ -0,0 +1,114 @@ +# Continous integration scripts + +## TravisCI + +For testing on Linux and macOS we use [TravisCI](https://travis-ci.org/) + +TravisCI consumes the `.travis.yml` file in the root of the repository +to tell it how to build and test Z3. + +However the logic for building and test Z3 is kept out of this file +and instead in a set of scripts in `scripts/`. This avoids +coupling the build to TravisCI tightly so we can migrate to another +service if required in the future. + +The scripts rely on a set of environment variables to control the configuration +of the build. The `.travis.yml` declares a list of configuration with each +configuration setting different environment variables. + +Note that the build scripts currently only support Z3 built with CMake. Support +for building Z3 using the older Python/Makefile build system might be added in +the future. + +### Configuration variables + +* `ASAN_BUILD` - Do [AddressSanitizer](https://github.com/google/sanitizers/wiki/AddressSanitizer) build (`0` or `1`) +* `BUILD_DOCS` - Build API documentation (`0` or `1`) +* `C_COMPILER` - Path to C Compiler +* `CXX_COMPILER` - Path to C++ Compiler +* `DOTNET_BINDINGS` - Build and test .NET API bindings (`0` or `1`) +* `JAVA_BINDINGS` - Build and test Java API bindings (`0` or `1`) +* `NO_SUPPRESS_OUTPUT` - Don't suppress output of some commands (`0` or `1`) +* `PYTHON_BINDINGS` - Build and test Python API bindings (`0` or `1`) +* `RUN_SYSTEM_TESTS` - Run system tests (`0` or `1`) +* `RUN_UNIT_TESTS` - Run unit tests (`0` or `1`) +* `TARGET_ARCH` - Target architecture (`x86_64` or `i686`) +* `TEST_INSTALL` - Test running `install` target (`0` or `1`) +* `UBSAN_BUILD` - Do [UndefinedBehaviourSanitizer](https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html) build (`0` or `1`) +* `USE_LIBGMP` - Use [GNU multiple precision library](https://gmplib.org/) (`0` or `1`) +* `USE_LTO` - Link binaries using link time optimization (`0` or `1`) +* `USE_OPENMP` - Use OpenMP (`0` or `1`) +* `Z3_BUILD_TYPE` - CMake build type (`RelWithDebInfo`, `Release`, `Debug`, or `MinSizeRel`) +* `Z3_CMAKE_GENERATOR` - CMake generator (`Ninja` or `Unix Makefiles`) +* `Z3_VERBOSE_BUILD_OUTPUT` - Show compile commands in CMake builds (`0` or `1`) +* `Z3_STATIC_BUILD` - Build Z3 binaries and libraries statically (`0` or `1`) +* `Z3_SYSTEM_TEST_GIT_REVISION` - Git revision of [z3test](https://github.com/Z3Prover/z3test). If empty lastest revision will be used. +* `Z3_WARNINGS_AS_ERRORS` - Set the `WARNINGS_AS_ERRORS` CMake option pased to Z3 (`OFF`, `ON`, or `SERIOUS_ONLY`) + +### Linux + +For Linux we use Docker to perform the build so that it easily reproducible +on a local machine and so that we can avoid depending on TravisCI's environment +and instead use a Linux distribution of our choice. + +The `scripts/travis_ci_linux_entry_point.sh` script + +1. Creates a base image containing all the dependencies needed to build and test Z3 +2. Builds and tests Z3 using the base image propagating configuration environment + variables (if set) into the build using the `--build-arg` argument of the `docker run` + command. + +If an environemnt variable is not set a defaults value is used which can be +found in `Dockerfiles/z3_build.Dockerfile`. + +#### Linux specific configuration variables + +* `LINUX_BASE` - The base docker image identifier to use (`ubuntu_16.04`, `ubuntu32_16.04`, or `ubuntu_14.04`). + +#### Reproducing a build locally + +A build can be reproduced locally by using the `scripts/travis_ci_linux_entry_point.sh` +script and setting the appropriate environment variable. + +For example lets say we wanted to reproduce the build below. + +```yaml + + - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo +``` + +This can be done by running the command + +```bash +LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo scripts/travis_ci_linux_entry_point.sh +``` + +The `docker build` command which we use internally supports caching. What this +means in practice is that re-running the above command will re-use successfully +completed stages of the build provided they haven't changed. This requires that +the `Dockerfiles/z3_build.Dockerfile` is carefully crafted to avoid invalidating +the cache when unrelated files sent to the build context change. + +#### TravisCI docker image cache + +To improve build times the Z3 base docker images are cached using +[TravisCI's cache directory feature](https://docs.travis-ci.com/user/caching). +If the `DOCKER_TRAVIS_CI_CACHE_DIR` environment variable is set (see `.travis.yml`) +then the directory pointed to by the environment variable is used as a cache +for Docker images. + +The logic for this can be found in `scripts/travis_ci_linux_entry_point.sh`. +The build time improvements are rather modest (~ 2 minutes) and the cache is +rather large due to TravisCI giving each configuration its own cache. So this +feature might be removed in the future. + +It may be better to just build the base image once (outside of TravisCI), upload +it to [DockerHub](https://hub.docker.com/) and have the build pull down the pre-built +image everytime. + +An [organization](https://hub.docker.com/u/z3prover/) has been created on +DockerHub for this. + +### macOS + +Not yet implemented. diff --git a/contrib/ci/maintainers.txt b/contrib/ci/maintainers.txt new file mode 100644 index 000000000..caa6798c6 --- /dev/null +++ b/contrib/ci/maintainers.txt @@ -0,0 +1,3 @@ +# Maintainers + +- Dan Liew (@delcypher) diff --git a/contrib/ci/scripts/build_z3_cmake.sh b/contrib/ci/scripts/build_z3_cmake.sh new file mode 100755 index 000000000..76fd0fb84 --- /dev/null +++ b/contrib/ci/scripts/build_z3_cmake.sh @@ -0,0 +1,130 @@ +#!/bin/bash +# This script builds Z3 + +SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" + +set -x +set -e +set -o pipefail + +: ${Z3_SRC_DIR?"Z3_SRC_DIR must be specified"} +: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"} +: ${Z3_BUILD_TYPE?"Z3_BUILD_TYPE must be specified"} +: ${Z3_CMAKE_GENERATOR?"Z3_CMAKE_GENERATOR must be specified"} +: ${Z3_STATIC_BUILD?"Z3_STATIC_BUILD must be specified"} +: ${USE_OPENMP?"USE_OPENMP must be specified"} +: ${USE_LIBGMP?"USE_LIBGMP must be specified"} +: ${BUILD_DOCS?"BUILD_DOCS must be specified"} +: ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"} +: ${PYTHON_BINDINGS?"PYTHON_BINDINGS must be specified"} +: ${DOTNET_BINDINGS?"DOTNET_BINDINGS must be specified"} +: ${JAVA_BINDINGS?"JAVA_BINDINGS must be specified"} +: ${USE_LTO?"USE_LTO must be specified"} +: ${Z3_INSTALL_PREFIX?"Z3_INSTALL_PREFIX must be specified"} +: ${Z3_WARNINGS_AS_ERRORS?"Z3_WARNINGS_AS_ERRORS must be specified"} + +ADDITIONAL_Z3_OPTS=() + +# Static or dynamic libz3 +if [ "X${Z3_STATIC_BUILD}" = "X1" ]; then + ADDITIONAL_Z3_OPTS+=('-DBUILD_LIBZ3_SHARED=OFF') +else + ADDITIONAL_Z3_OPTS+=('-DBUILD_LIBZ3_SHARED=ON') +fi + +# Use OpenMP? +if [ "X${USE_OPENMP}" = "X1" ]; then + ADDITIONAL_Z3_OPTS+=('-DUSE_OPENMP=ON') +else + ADDITIONAL_Z3_OPTS+=('-DUSE_OPENMP=OFF') +fi + +# Use LibGMP? +if [ "X${USE_LIBGMP}" = "X1" ]; then + ADDITIONAL_Z3_OPTS+=('-DUSE_LIB_GMP=ON') +else + ADDITIONAL_Z3_OPTS+=('-DUSE_LIB_GMP=OFF') +fi + +# Use link time optimziation? +if [ "X${USE_LTO}" = "X1" ]; then + ADDITIONAL_Z3_OPTS+=('-DLINK_TIME_OPTIMIZATION=ON') +else + ADDITIONAL_Z3_OPTS+=('-DLINK_TIME_OPTIMIZATION=OFF') +fi + +# Build API docs? +if [ "X${BUILD_DOCS}" = "X1" ]; then + ADDITIONAL_Z3_OPTS+=( \ + '-DBUILD_DOCUMENTATION=ON' \ + '-DALWAYS_BUILD_DOCS=OFF' \ + ) +else + ADDITIONAL_Z3_OPTS+=('-DBUILD_DOCUMENTATION=OFF') +fi + +# Python bindings? +if [ "X${PYTHON_BINDINGS}" = "X1" ]; then + ADDITIONAL_Z3_OPTS+=( \ + '-DBUILD_PYTHON_BINDINGS=ON' \ + '-DINSTALL_PYTHON_BINDINGS=ON' \ + ) +else + ADDITIONAL_Z3_OPTS+=( \ + '-DBUILD_PYTHON_BINDINGS=OFF' \ + '-DINSTALL_PYTHON_BINDINGS=OFF' \ + ) +fi + +# .NET bindings? +if [ "X${DOTNET_BINDINGS}" = "X1" ]; then + ADDITIONAL_Z3_OPTS+=( \ + '-DBUILD_DOTNET_BINDINGS=ON' \ + '-DINSTALL_DOTNET_BINDINGS=ON' \ + ) +else + ADDITIONAL_Z3_OPTS+=( \ + '-DBUILD_DOTNET_BINDINGS=OFF' \ + '-DINSTALL_DOTNET_BINDINGS=OFF' \ + ) +fi + +# Java bindings? +if [ "X${JAVA_BINDINGS}" = "X1" ]; then + ADDITIONAL_Z3_OPTS+=( \ + '-DBUILD_JAVA_BINDINGS=ON' \ + '-DINSTALL_JAVA_BINDINGS=ON' \ + ) +else + ADDITIONAL_Z3_OPTS+=( \ + '-DBUILD_JAVA_BINDINGS=OFF' \ + '-DINSTALL_JAVA_BINDINGS=OFF' \ + ) +fi + +# Set compiler flags +source ${SCRIPT_DIR}/set_compiler_flags.sh + +# Sanity check +if [ ! -e "${Z3_SRC_DIR}/CMakeLists.txt" ]; then + echo "Z3_SRC_DIR is invalid" + exit 1 +fi + +# Make build tree +mkdir -p "${Z3_BUILD_DIR}" +cd "${Z3_BUILD_DIR}" + +# Configure +cmake \ + -G "${Z3_CMAKE_GENERATOR}" \ + -DCMAKE_BUILD_TYPE=${Z3_BUILD_TYPE} \ + -DPYTHON_EXECUTABLE=${PYTHON_EXECUTABLE} \ + -DCMAKE_INSTALL_PREFIX=${Z3_INSTALL_PREFIX} \ + -DWARNINGS_AS_ERRORS=${Z3_WARNINGS_AS_ERRORS} \ + "${ADDITIONAL_Z3_OPTS[@]}" \ + "${Z3_SRC_DIR}" + +# Build +source ${SCRIPT_DIR}/set_generator_args.sh +cmake --build $(pwd) "${GENERATOR_ARGS[@]}" diff --git a/contrib/ci/scripts/run_quiet.sh b/contrib/ci/scripts/run_quiet.sh new file mode 100644 index 000000000..5abc910e8 --- /dev/null +++ b/contrib/ci/scripts/run_quiet.sh @@ -0,0 +1,41 @@ +# Simple wrapper function that runs a command suppressing +# it's output. However it's output will be shown in the +# case that `NO_SUPPRESS_OUTPUT` is set to `1` or the command +# fails. +# +# The use case for this trying to avoid large logs on TravisCI +function run_quiet() { + if [ "X${NO_SUPPRESS_OUTPUT}" = "X1" ]; then + "${@}" + else + OLD_SETTINGS="$-" + set +x + set +e + TMP_DIR="${TMP_DIR:-/tmp/}" + STDOUT="${TMP_DIR}/$$.stdout" + STDERR="${TMP_DIR}/$$.stderr" + "${@}" > "${STDOUT}" 2> "${STDERR}" + EXIT_STATUS="$?" + if [ "${EXIT_STATUS}" -ne 0 ]; then + echo "Command \"$@\" failed" + echo "EXIT CODE: ${EXIT_STATUS}" + echo "STDOUT" + echo "" + echo "\`\`\`" + cat ${STDOUT} + echo "\`\`\`" + echo "" + echo "STDERR" + echo "" + echo "\`\`\`" + cat ${STDERR} + echo "\`\`\`" + echo "" + fi + # Clean up + rm "${STDOUT}" "${STDERR}" + [ $( echo "${OLD_SETTINGS}" | grep -c 'e') -ne 0 ] && set -e + [ $( echo "${OLD_SETTINGS}" | grep -c 'x') -ne 0 ] && set -x + return ${EXIT_STATUS} + fi +} diff --git a/contrib/ci/scripts/set_compiler_flags.sh b/contrib/ci/scripts/set_compiler_flags.sh new file mode 100644 index 000000000..7efdecdac --- /dev/null +++ b/contrib/ci/scripts/set_compiler_flags.sh @@ -0,0 +1,46 @@ +# This script should is intended to be included by other +# scripts and should not be executed directly + +: ${TARGET_ARCH?"TARGET_ARCH must be specified"} +: ${ASAN_BUILD?"ASAN_BUILD must be specified"} +: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"} +: ${CC?"CC must be specified"} +: ${CXX?"CXX must be specified"} + +case ${TARGET_ARCH} in + x86_64) + CXXFLAGS="${CXXFLAGS} -m64" + CFLAGS="${CFLAGS} -m64" + ;; + i686) + CXXFLAGS="${CXXFLAGS} -m32" + CFLAGS="${CFLAGS} -m32" + ;; + *) + echo "Unknown arch \"${TARGET_ARCH}\"" + exit 1 +esac + +if [ "X${ASAN_BUILD}" = "X1" ]; then + CXXFLAGS="${CXXFLAGS} -fsanitize=address -fno-omit-frame-pointer" + CFLAGS="${CFLAGS} -fsanitize=address -fno-omit-frame-pointer" +fi + +if [ "X${UBSAN_BUILD}" = "X1" ]; then + CXXFLAGS="${CXXFLAGS} -fsanitize=undefined" + CFLAGS="${CFLAGS} -fsanitize=undefined" +fi + +# Report flags +echo "CXXFLAGS: ${CXXFLAGS}" +echo "CFLAGS: ${CFLAGS}" + +# Report compiler +echo "CC: ${CC}" +${CC} --version +echo "CXX: ${CXX}" +${CXX} --version + +# Export the values +export CFLAGS +export CXXFLAGS diff --git a/contrib/ci/scripts/set_generator_args.sh b/contrib/ci/scripts/set_generator_args.sh new file mode 100644 index 000000000..0ef7b76aa --- /dev/null +++ b/contrib/ci/scripts/set_generator_args.sh @@ -0,0 +1,20 @@ +# This script should is intended to be included by other +# scripts and should not be executed directly + +: ${Z3_CMAKE_GENERATOR?"Z3_CMAKE_GENERATOR must be specified"} +: ${Z3_VERBOSE_BUILD_OUTPUT?"Z3_VERBOSE_BUILD_OUTPUT must be specified"} + +GENERATOR_ARGS=('--') +if [ "${Z3_CMAKE_GENERATOR}" = "Unix Makefiles" ]; then + GENERATOR_ARGS+=("-j$(nproc)") + if [ "X${Z3_VERBOSE_BUILD_OUTPUT}" = "X1" ]; then + GENERATOR_ARGS+=("VERBOSE=1") + fi +elif [ "${Z3_CMAKE_GENERATOR}" = "Ninja" ]; then + if [ "X${Z3_VERBOSE_BUILD_OUTPUT}" = "X1" ]; then + GENERATOR_ARGS+=("-v") + fi +else + echo "Unknown CMake generator \"${Z3_CMAKE_GENERATOR}\"" + exit 1 +fi diff --git a/contrib/ci/scripts/test_z3_docs.sh b/contrib/ci/scripts/test_z3_docs.sh new file mode 100755 index 000000000..6a65ffedd --- /dev/null +++ b/contrib/ci/scripts/test_z3_docs.sh @@ -0,0 +1,24 @@ +#!/bin/bash + +SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" +. ${SCRIPT_DIR}/run_quiet.sh + +set -x +set -e +set -o pipefail + +: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"} +: ${BUILD_DOCS?"BUILD_DOCS must be specified"} + +# Set CMake generator args +source ${SCRIPT_DIR}/set_generator_args.sh + +cd "${Z3_BUILD_DIR}" + +# Generate documentation +if [ "X${BUILD_DOCS}" = "X1" ]; then + # TODO: Make quiet once we've fixed the build + run_quiet cmake --build $(pwd) --target api_docs "${GENERATOR_ARGS[@]}" +fi + +# TODO: Test or perhaps deploy the built docs? diff --git a/contrib/ci/scripts/test_z3_examples_cmake.sh b/contrib/ci/scripts/test_z3_examples_cmake.sh new file mode 100755 index 000000000..2eda3de7b --- /dev/null +++ b/contrib/ci/scripts/test_z3_examples_cmake.sh @@ -0,0 +1,87 @@ +#!/bin/bash + +# This script tests Z3 + +SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" +. ${SCRIPT_DIR}/run_quiet.sh + +set -x +set -e +set -o pipefail +: ${Z3_SRC_DIR?"Z3_SRC_DIR must be specified"} +: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"} +: ${PYTHON_BINDINGS?"PYTHON_BINDINGS must be specified"} +: ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"} +: ${DOTNET_BINDINGS?"DOTNET_BINDINGS must be specified"} +: ${JAVA_BINDINGS?"JAVA_BINDINGS must be specified"} + +# Set compiler flags +source ${SCRIPT_DIR}/set_compiler_flags.sh + +# Set CMake generator args +source ${SCRIPT_DIR}/set_generator_args.sh + +cd "${Z3_BUILD_DIR}" + +# Build and run C example +cmake --build $(pwd) --target c_example "${GENERATOR_ARGS[@]}" +run_quiet examples/c_example_build_dir/c_example + +# Build and run C++ example +cmake --build $(pwd) --target cpp_example "${GENERATOR_ARGS[@]}" +run_quiet examples/cpp_example_build_dir/cpp_example + +# Build and run tptp5 example +cmake --build $(pwd) --target z3_tptp5 "${GENERATOR_ARGS[@]}" +# FIXME: Do something more useful with example +run_quiet examples/tptp_build_dir/z3_tptp5 -help + +# Build an run c_maxsat_example +cmake --build $(pwd) --target c_maxsat_example "${GENERATOR_ARGS[@]}" +run_quiet \ + examples/c_maxsat_example_build_dir/c_maxsat_example \ + ${Z3_SRC_DIR}/examples/maxsat/ex.smt + + +if [ "X${PYTHON_BINDINGS}" = "X1" ]; then + # Run python examples + # `all_interval_series.py` produces a lot of output so just throw + # away output. + # TODO: This example is slow should we remove it from testing? + run_quiet ${PYTHON_EXECUTABLE} python/all_interval_series.py + run_quiet ${PYTHON_EXECUTABLE} python/complex.py + run_quiet ${PYTHON_EXECUTABLE} python/example.py + # FIXME: `hamiltonian.py` example is disabled because its too slow. + #${PYTHON_EXECUTABLE} python/hamiltonian.py + run_quiet ${PYTHON_EXECUTABLE} python/marco.py + run_quiet ${PYTHON_EXECUTABLE} python/mss.py + run_quiet ${PYTHON_EXECUTABLE} python/socrates.py + run_quiet ${PYTHON_EXECUTABLE} python/visitor.py + run_quiet ${PYTHON_EXECUTABLE} python/z3test.py +fi + +if [ "X${DOTNET_BINDINGS}" = "X1" ]; then + # Build .NET example + # FIXME: Move compliation step into CMake target + mcs ${Z3_SRC_DIR}/examples/dotnet/Program.cs /target:exe /out:dotnet_test.exe /reference:Microsoft.Z3.dll /r:System.Numerics.dll + # Run .NET example + run_quiet mono ./dotnet_test.exe +fi + +if [ "X${JAVA_BINDINGS}" = "X1" ]; then + # Build Java example + # FIXME: Move compilation step into CMake target + mkdir -p examples/java + cp ${Z3_SRC_DIR}/examples/java/JavaExample.java examples/java/ + javac examples/java/JavaExample.java -classpath com.microsoft.z3.jar + # Run Java example + if [ "$(uname)" = "Darwin" ]; then + # macOS + export DYLD_LIBRARY_PATH=$(pwd):${DYLD_LIBRARY_PATH} + else + # Assume Linux for now + export LD_LIBRARY_PATH=$(pwd):${LD_LIBRARY_PATH} + fi + run_quiet java -cp .:examples/java:com.microsoft.z3.jar JavaExample +fi + diff --git a/contrib/ci/scripts/test_z3_install_cmake.sh b/contrib/ci/scripts/test_z3_install_cmake.sh new file mode 100755 index 000000000..804158f6f --- /dev/null +++ b/contrib/ci/scripts/test_z3_install_cmake.sh @@ -0,0 +1,24 @@ +#!/bin/bash + +SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" + +set -x +set -e +set -o pipefail + +: ${TEST_INSTALL?"TEST_INSTALL must be specified"} +: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"} + +if [ "X${TEST_INSTALL}" != "X1" ]; then + echo "Skipping install" + exit 0 +fi + +# Set CMake generator args +source ${SCRIPT_DIR}/set_generator_args.sh + +cd "${Z3_BUILD_DIR}" + +sudo cmake --build $(pwd) --target install "${GENERATOR_ARGS[@]}" + +# TODO: Test the installed version in some way diff --git a/contrib/ci/scripts/test_z3_system_tests.sh b/contrib/ci/scripts/test_z3_system_tests.sh new file mode 100755 index 000000000..dfb1084a4 --- /dev/null +++ b/contrib/ci/scripts/test_z3_system_tests.sh @@ -0,0 +1,54 @@ +#!/bin/bash + +set -x +set -e +set -o pipefail + +: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"} +: ${Z3_BUILD_TYPE?"Z3_BUILD_TYPE must be specified"} +: ${RUN_SYSTEM_TESTS?"RUN_SYSTEM_TESTS must be speicifed"} +: ${PYTHON_BINDINGS?"PYTHON_BINDINGS must be specified"} +: ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"} +: ${Z3_SYSTEM_TEST_DIR?"Z3_SYSTEM_TEST_DIR must be specified"} + +if [ "X${RUN_SYSTEM_TESTS}" != "X1" ]; then + echo "Skipping system tests" + exit 0 +fi + +Z3_EXE="${Z3_BUILD_DIR}/z3" +Z3_LIB_DIR="${Z3_BUILD_DIR}" + +# Set value if not already defined externally +Z3_SYSTEM_TEST_GIT_URL="${Z3_GIT_URL:-https://github.com/Z3Prover/z3test.git}" + +# Clone repo to destination +mkdir -p "${Z3_SYSTEM_TEST_GIT_URL}" +git clone "${Z3_SYSTEM_TEST_GIT_URL}" "${Z3_SYSTEM_TEST_DIR}" +cd "${Z3_SYSTEM_TEST_DIR}" + +if [ -n "${Z3_SYSTEM_TEST_GIT_REVISION}" ]; then + # If a particular revision is requested then check it out. + # This is useful for reproducible builds + git checkout "${Z3_SYSTEM_TEST_GIT_REVISION}" +fi + +############################################################################### +# Run system tests +############################################################################### + +# SMTLIBv2 tests +${PYTHON_EXECUTABLE} scripts/test_benchmarks.py "${Z3_EXE}" regressions/smt2 + +${PYTHON_EXECUTABLE} scripts/test_benchmarks.py "${Z3_EXE}" regressions/smt2-extra + +if [ "X${Z3_BUILD_TYPE}" = "XDebug" ]; then + ${PYTHON_EXECUTABLE} scripts/test_benchmarks.py "${Z3_EXE}" regressions/smt2-debug +fi + +if [ "X${PYTHON_BINDINGS}" = "X1" ]; then + # Run python binding tests + ${PYTHON_EXECUTABLE} scripts/test_pyscripts.py "${Z3_LIB_DIR}" regressions/python/ +fi + +# FIXME: Run `scripts/test_cs.py` once it has been modified to support mono diff --git a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh new file mode 100755 index 000000000..0d8e59b0f --- /dev/null +++ b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh @@ -0,0 +1,24 @@ +#!/bin/bash + +SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" + +set -x +set -e +set -o pipefail + +: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"} +: ${RUN_UNIT_TESTS?"RUN_UNIT_TESTS must be specified"} + +if [ "X${RUN_UNIT_TESTS}" != "X1" ]; then + echo "Skipping unit tests" + exit 0 +fi + +# Set CMake generator args +source ${SCRIPT_DIR}/set_generator_args.sh + +cd "${Z3_BUILD_DIR}" + +# Build and run internal tests +cmake --build $(pwd) --target test-z3 "${GENERATOR_ARGS[@]}" +./test-z3 diff --git a/contrib/ci/scripts/travis_ci_entry_point.sh b/contrib/ci/scripts/travis_ci_entry_point.sh new file mode 100755 index 000000000..41bde7230 --- /dev/null +++ b/contrib/ci/scripts/travis_ci_entry_point.sh @@ -0,0 +1,18 @@ +#!/bin/bash + +SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" + +set -x +set -e +set -o pipefail + +: ${TRAVIS_OS_NAME?"TRAVIS_OS_NAME should be set"} + +if [ "${TRAVIS_OS_NAME}" = "osx" ]; then + ${SCRIPT_DIR}/travis_ci_osx_entry_point.sh +elif [ "${TRAVIS_OS_NAME}" = "linux" ]; then + ${SCRIPT_DIR}/travis_ci_linux_entry_point.sh +else + echo "Unsupported OS \"${TRAVIS_OS_NAME}\"" + exit 1 +fi diff --git a/contrib/ci/scripts/travis_ci_linux_entry_point.sh b/contrib/ci/scripts/travis_ci_linux_entry_point.sh new file mode 100755 index 000000000..84b2dd400 --- /dev/null +++ b/contrib/ci/scripts/travis_ci_linux_entry_point.sh @@ -0,0 +1,215 @@ +#!/bin/bash + +SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" + +set -x +set -e +set -o pipefail + +DOCKER_FILE_DIR="$(cd ${SCRIPT_DIR}/../Dockerfiles; echo $PWD)" + +: ${LINUX_BASE?"LINUX_BASE must be specified"} + + + +# Sanity check. Current working directory should be repo root +if [ ! -f "./README.md" ]; then + echo "Current working directory should be repo root" + exit 1 +fi + +BUILD_OPTS=() +# Override options if they have been provided. +# Otherwise the defaults in the Docker file will be used +if [ -n "${Z3_CMAKE_GENERATOR}" ]; then + BUILD_OPTS+=("--build-arg" "Z3_CMAKE_GENERATOR=${Z3_CMAKE_GENERATOR}") +fi + +if [ -n "${USE_OPENMP}" ]; then + BUILD_OPTS+=("--build-arg" "USE_OPENMP=${USE_OPENMP}") +fi + +if [ -n "${USE_LIBGMP}" ]; then + BUILD_OPTS+=("--build-arg" "USE_LIBGMP=${USE_LIBGMP}") +fi + +if [ -n "${BUILD_DOCS}" ]; then + BUILD_OPTS+=("--build-arg" "BUILD_DOCS=${BUILD_DOCS}") +fi + +if [ -n "${PYTHON_EXECUTABLE}" ]; then + BUILD_OPTS+=("--build-arg" "PYTHON_EXECUTABLE=${PYTHON_EXECUTABLE}") +fi + +if [ -n "${PYTHON_BINDINGS}" ]; then + BUILD_OPTS+=("--build-arg" "PYTHON_BINDINGS=${PYTHON_BINDINGS}") +fi + +if [ -n "${DOTNET_BINDINGS}" ]; then + BUILD_OPTS+=("--build-arg" "DOTNET_BINDINGS=${DOTNET_BINDINGS}") +fi + +if [ -n "${JAVA_BINDINGS}" ]; then + BUILD_OPTS+=("--build-arg" "JAVA_BINDINGS=${JAVA_BINDINGS}") +fi + +if [ -n "${USE_LTO}" ]; then + BUILD_OPTS+=("--build-arg" "USE_LTO=${USE_LTO}") +fi + +if [ -n "${Z3_INSTALL_PREFIX}" ]; then + BUILD_OPTS+=("--build-arg" "Z3_INSTALL_PREFIX=${Z3_INSTALL_PREFIX}") +fi + +# TravisCI reserves CC for itself so use a different name +if [ -n "${C_COMPILER}" ]; then + BUILD_OPTS+=("--build-arg" "CC=${C_COMPILER}") +fi + +# TravisCI reserves CXX for itself so use a different name +if [ -n "${CXX_COMPILER}" ]; then + BUILD_OPTS+=("--build-arg" "CXX=${CXX_COMPILER}") +fi + +if [ -n "${TARGET_ARCH}" ]; then + BUILD_OPTS+=("--build-arg" "TARGET_ARCH=${TARGET_ARCH}") +fi + +if [ -n "${ASAN_BUILD}" ]; then + BUILD_OPTS+=("--build-arg" "ASAN_BUILD=${ASAN_BUILD}") +fi + +if [ -n "${UBSAN_BUILD}" ]; then + BUILD_OPTS+=("--build-arg" "UBSAN_BUILD=${UBSAN_BUILD}") +fi + +if [ -n "${TEST_INSTALL}" ]; then + BUILD_OPTS+=("--build-arg" "TEST_INSTALL=${TEST_INSTALL}") +fi + +if [ -n "${RUN_SYSTEM_TESTS}" ]; then + BUILD_OPTS+=("--build-arg" "RUN_SYSTEM_TESTS=${RUN_SYSTEM_TESTS}") +fi + +if [ -n "${Z3_SYSTEM_TEST_GIT_REVISION}" ]; then + BUILD_OPTS+=( \ + "--build-arg" \ + "Z3_SYSTEM_TEST_GIT_REVISION=${Z3_SYSTEM_TEST_GIT_REVISION}" \ + ) +fi + +if [ -n "${RUN_UNIT_TESTS}" ]; then + BUILD_OPTS+=("--build-arg" "RUN_UNIT_TESTS=${RUN_UNIT_TESTS}") +fi + +if [ -n "${Z3_VERBOSE_BUILD_OUTPUT}" ]; then + BUILD_OPTS+=( \ + "--build-arg" \ + "Z3_VERBOSE_BUILD_OUTPUT=${Z3_VERBOSE_BUILD_OUTPUT}" \ + ) +fi + +if [ -n "${Z3_STATIC_BUILD}" ]; then + BUILD_OPTS+=("--build-arg" "Z3_STATIC_BUILD=${Z3_STATIC_BUILD}") +fi + +if [ -n "${NO_SUPPRESS_OUTPUT}" ]; then + BUILD_OPTS+=( \ + "--build-arg" \ + "NO_SUPPRESS_OUTPUT=${NO_SUPPRESS_OUTPUT}" \ + ) +fi + +if [ -n "${Z3_WARNINGS_AS_ERRORS}" ]; then + BUILD_OPTS+=( \ + "--build-arg" \ + "Z3_WARNINGS_AS_ERRORS=${Z3_WARNINGS_AS_ERRORS}" \ + ) +fi + +case ${LINUX_BASE} in + ubuntu_14.04) + BASE_DOCKER_FILE="${DOCKER_FILE_DIR}/z3_base_ubuntu_14.04.Dockerfile" + BASE_DOCKER_IMAGE_NAME="z3_base_ubuntu:14.04" + ;; + ubuntu_16.04) + BASE_DOCKER_FILE="${DOCKER_FILE_DIR}/z3_base_ubuntu_16.04.Dockerfile" + BASE_DOCKER_IMAGE_NAME="z3_base_ubuntu:16.04" + ;; + ubuntu32_16.04) + BASE_DOCKER_FILE="${DOCKER_FILE_DIR}/z3_base_ubuntu32_16.04.Dockerfile" + BASE_DOCKER_IMAGE_NAME="z3_base_ubuntu32:16.04" + ;; + *) + echo "Unknown Linux base ${LINUX_BASE}" + exit 1 + ;; +esac + +# Initially assume that we need to build the base Docker image +MUST_BUILD=1 + +# Travis CI persistent cache. +# +# This inspired by http://rundef.com/fast-travis-ci-docker-build . +# The idea is to cache the built image for subsequent builds to +# reduce build time. +if [ -n "${DOCKER_TRAVIS_CI_CACHE_DIR}" ]; then + CHECKSUM_FILE="${DOCKER_TRAVIS_CI_CACHE_DIR}/${BASE_DOCKER_IMAGE_NAME}.chksum" + CACHED_DOCKER_IMAGE="${DOCKER_TRAVIS_CI_CACHE_DIR}/${BASE_DOCKER_IMAGE_NAME}.gz" + if [ -f "${CACHED_DOCKER_IMAGE}" ]; then + # There's a cached image to use. Check the checksums of the Dockerfile + # match. If they don't that implies we need to build a fresh image. + if [ -f "${CHECKSUM_FILE}" ]; then + CURRENT_DOCKERFILE_CHECKSUM=$(sha256sum "${BASE_DOCKER_FILE}" | awk '{ print $1 }') + CACHED_DOCKERFILE_CHECKSUM=$(cat "${CHECKSUM_FILE}") + if [ "X${CURRENT_DOCKERFILE_CHECKSUM}" = "X${CACHED_DOCKERFILE_CHECKSUM}" ]; then + # Load the cached image + MUST_BUILD=0 + gunzip --stdout "${CACHED_DOCKER_IMAGE}" | docker load + fi + fi + fi +fi + +if [ "${MUST_BUILD}" -eq 1 ]; then + # The base image contains all the dependencies we want to build + # Z3. + docker build -t "${BASE_DOCKER_IMAGE_NAME}" - < "${BASE_DOCKER_FILE}" + + if [ -n "${DOCKER_TRAVIS_CI_CACHE_DIR}" ]; then + # Write image and checksum to cache + docker save "${BASE_DOCKER_IMAGE_NAME}" | \ + gzip > "${CACHED_DOCKER_IMAGE}" + sha256sum "${BASE_DOCKER_FILE}" | awk '{ print $1 }' > \ + "${CHECKSUM_FILE}" + fi +fi + + +DOCKER_MAJOR_VERSION=$(docker info --format '{{.ServerVersion}}' | sed 's/^\([0-9]\+\)\.\([0-9]\+\).*$/\1/') +DOCKER_MINOR_VERSION=$(docker info --format '{{.ServerVersion}}' | sed 's/^\([0-9]\+\)\.\([0-9]\+\).*$/\2/') +DOCKER_BUILD_FILE="${DOCKER_FILE_DIR}/z3_build.Dockerfile" + +if [ "${DOCKER_MAJOR_VERSION}${DOCKER_MINOR_VERSION}" -lt 1705 ]; then + # Workaround limitation in older Docker versions where the FROM + # command cannot be parameterized with an ARG. + sed \ + -e '/^ARG DOCKER_IMAGE_BASE/d' \ + -e 's/${DOCKER_IMAGE_BASE}/'"${BASE_DOCKER_IMAGE_NAME}/" \ + "${DOCKER_BUILD_FILE}" > "${DOCKER_BUILD_FILE}.patched" + DOCKER_BUILD_FILE="${DOCKER_BUILD_FILE}.patched" +else + # This feature landed in Docker 17.05 + # See https://github.com/moby/moby/pull/31352 + BUILD_OPTS+=( \ + "--build-arg" \ + "DOCKER_IMAGE_BASE=${BASE_DOCKER_IMAGE_NAME}" \ + ) +fi + +# Now build Z3 and test it using the created base image +docker build \ + -f "${DOCKER_BUILD_FILE}" \ + "${BUILD_OPTS[@]}" \ + . diff --git a/contrib/ci/scripts/travis_ci_osx_entry_point.sh b/contrib/ci/scripts/travis_ci_osx_entry_point.sh new file mode 100755 index 000000000..03be81647 --- /dev/null +++ b/contrib/ci/scripts/travis_ci_osx_entry_point.sh @@ -0,0 +1,10 @@ +#!/bin/bash + +SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" + +set -x +set -e +set -o pipefail + +echo "Not implemented" +exit 1 diff --git a/doc/website.dox.in b/doc/website.dox.in index 17a8552d1..f8659ec0b 100644 --- a/doc/website.dox.in +++ b/doc/website.dox.in @@ -4,9 +4,7 @@ Z3 is a high-performance theorem prover being developed at Microsoft Research. - The Z3 website moved to http://github.com/z3prover.. - - The old Z3 websites can be found here and here. + The Z3 website is at http://github.com/z3prover.. This website hosts the automatically generated documentation for the Z3 APIs. diff --git a/examples/maxsat/maxsat.c b/examples/maxsat/maxsat.c index 45325311e..a312e79ad 100644 --- a/examples/maxsat/maxsat.c +++ b/examples/maxsat/maxsat.c @@ -348,7 +348,15 @@ void assert_at_most_k(Z3_context ctx, Z3_solver s, unsigned n, Z3_ast * lits, un */ void assert_at_most_one(Z3_context ctx, Z3_solver s, unsigned n, Z3_ast * lits) { - assert_at_most_k(ctx, s, n, lits, 1); + assert_at_most_k(ctx, s, n, lits, 1); +} + + +Z3_solver mk_solver(Z3_context ctx) +{ + Z3_solver r = Z3_mk_solver(ctx); + Z3_solver_inc_ref(ctx, r); + return r; } /** @@ -357,8 +365,7 @@ void assert_at_most_one(Z3_context ctx, Z3_solver s, unsigned n, Z3_ast * lits) void tst_at_most_one() { Z3_context ctx = mk_context(); - Z3_solver s = Z3_mk_solver(ctx); - Z3_solver_inc_ref(ctx, s); + Z3_solver s = mk_solver(ctx); Z3_ast k1 = mk_bool_var(ctx, "k1"); Z3_ast k2 = mk_bool_var(ctx, "k2"); Z3_ast k3 = mk_bool_var(ctx, "k3"); @@ -460,7 +467,7 @@ int naive_maxsat(Z3_context ctx, Z3_solver s, unsigned num_hard_cnstrs, Z3_ast * printf("unsat\n"); return num_soft_cnstrs - k - 1; } - m = Z3_solver_get_model(ctx, s); + m = Z3_solver_get_model(ctx, s); Z3_model_inc_ref(ctx, m); num_disabled = get_num_disabled_soft_constraints(ctx, m, num_soft_cnstrs, aux_vars); Z3_model_dec_ref(ctx, m); @@ -523,7 +530,7 @@ int fu_malik_maxsat_step(Z3_context ctx, Z3_solver s, unsigned num_soft_cnstrs, unsigned j; // check whether assumption[i] is in the core or not for (j = 0; j < core_size; j++) { - if (assumptions[i] == Z3_ast_vector_get(ctx, core, j)) + if (assumptions[i] == Z3_ast_vector_get(ctx, core, j)) break; } if (j < core_size) { @@ -607,8 +614,7 @@ int smtlib_maxsat(char * file_name, int approach) Z3_ast * hard_cnstrs, * soft_cnstrs; unsigned result = 0; ctx = mk_context(); - s = Z3_mk_solver(ctx); - Z3_solver_inc_ref(ctx, s); + s = mk_solver(ctx); Z3_parse_smtlib_file(ctx, file_name, 0, 0, 0, 0, 0, 0); hard_cnstrs = get_hard_constraints(ctx, &num_hard_cnstrs); soft_cnstrs = get_soft_constraints(ctx, &num_soft_cnstrs); diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 3ce104709..a5f75fd1c 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -104,6 +104,8 @@ GIT_DESCRIBE=False SLOW_OPTIMIZE=False USE_OMP=True LOG_SYNC=False +GUARD_CF=False +ALWAYS_DYNAMIC_BASE=False FPMATH="Default" FPMATH_FLAGS="-mfpmath=sse -msse -msse2" @@ -623,13 +625,13 @@ def display_help(exit_code): print(" -d, --debug compile Z3 in debug mode.") print(" -t, --trace enable tracing in release mode.") if IS_WINDOWS: + print(" --guardcf enable Control Flow Guard runtime checks.") print(" -x, --x64 create 64 binary when using Visual Studio.") else: print(" --x86 force 32-bit x86 build on x64 systems.") print(" -m, --makefiles generate only makefiles.") if IS_WINDOWS: print(" -v, --vsproj generate Visual Studio Project Files.") - if IS_WINDOWS: print(" --optimize generate optimized code during linking.") print(" --dotnet generate .NET bindings.") print(" --dotnet-key= sign the .NET assembly using the private key in .") @@ -670,10 +672,11 @@ def parse_options(): global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM global DOTNET_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED global LINUX_X64, SLOW_OPTIMIZE, USE_OMP, LOG_SYNC + global GUARD_CF, ALWAYS_DYNAMIC_BASE try: options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:df:sxhmcvtnp:gj', - ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', + ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', 'guardcf', 'trace', 'dotnet', 'dotnet-key=', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof', 'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python', 'staticbin', 'log-sync']) except: @@ -742,6 +745,9 @@ def parse_options(): elif opt in ('--python'): PYTHON_ENABLED = True PYTHON_INSTALL_ENABLED = True + elif opt == '--guardcf': + GUARD_CF = True + ALWAYS_DYNAMIC_BASE = True # /GUARD:CF requires /DYNAMICBASE else: print("ERROR: Invalid command line option '%s'" % opt) display_help(1) @@ -2310,6 +2316,7 @@ def mk_config(): 'SLINK_OUT_FLAG=/Fe\n' 'OS_DEFINES=/D _WINDOWS\n') extra_opt = '' + link_extra_opt = '' HAS_OMP = test_openmp('cl') if HAS_OMP: extra_opt = ' /openmp' @@ -2319,10 +2326,14 @@ def mk_config(): extra_opt = '%s /DZ3_LOG_SYNC' % extra_opt if GIT_HASH: extra_opt = ' %s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH) + if GUARD_CF: + extra_opt = ' %s /guard:cf' % extra_opt + link_extra_opt = ' %s /GUARD:CF' % link_extra_opt if STATIC_BIN: static_opt = '/MT' else: static_opt = '/MD' + maybe_disable_dynamic_base = '/DYNAMICBASE' if ALWAYS_DYNAMIC_BASE else '/DYNAMICBASE:NO' if DEBUG_MODE: static_opt = static_opt + 'd' config.write( @@ -2333,8 +2344,8 @@ def mk_config(): config.write( 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- %s %s\n' % (extra_opt, static_opt)) config.write( - 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' - 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') + 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n' + 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt)) elif VS_ARM: print("ARM on VS is unsupported") exit(1) @@ -2342,8 +2353,8 @@ def mk_config(): config.write( 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2 %s %s\n' % (extra_opt, static_opt)) config.write( - 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' - 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') + 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n' + 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt)) else: # Windows Release mode LTCG=' /LTCG' if SLOW_OPTIMIZE else '' @@ -2358,8 +2369,8 @@ def mk_config(): config.write( 'CXXFLAGS=/c%s /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP %s %s\n' % (GL, extra_opt, static_opt)) config.write( - 'LINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608\n' - 'SLINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n' % (LTCG, LTCG)) + 'LINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 %s\n' + 'SLINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 %s\n' % (LTCG, link_extra_opt, LTCG, link_extra_opt)) elif VS_ARM: print("ARM on VS is unsupported") exit(1) @@ -2367,8 +2378,8 @@ def mk_config(): config.write( 'CXXFLAGS=/nologo /c%s /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2 %s %s\n' % (GL, extra_opt, static_opt)) config.write( - 'LINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' - 'SLINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n' % (LTCG, LTCG)) + 'LINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n' + 'SLINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (LTCG, link_extra_opt, LTCG, maybe_disable_dynamic_base, link_extra_opt)) diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index ad6d5a658..7bb0fda58 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -88,6 +88,7 @@ public class Fixedpoint extends Z3Object /** * Add rule into the fixedpoint solver. * + * @param rule implication (Horn clause) representing rule * @param name Nullable rule name. * @throws Z3Exception **/ @@ -178,6 +179,7 @@ public class Fixedpoint extends Z3Object /** * Update named rule into in the fixedpoint solver. * + * @param rule implication (Horn clause) representing rule * @param name Nullable rule name. * @throws Z3Exception **/ diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 52cc2e858..a16c1b92b 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -12,7 +12,7 @@ Several online tutorials for Z3Py are available at: http://rise4fun.com/Z3Py/tutorial/guide -Please send feedback, comments and/or corrections to leonardo@microsoft.com. Your comments are very valuable. +Please send feedback, comments and/or corrections on the Issue tracker for https://github.com/Z3prover/z3.git. Your comments are very valuable. Small example: @@ -6054,6 +6054,24 @@ class Solver(Z3PPObject): """ Z3_solver_pop(self.ctx.ref(), self.solver, num) + def num_scopes(self): + """Return the current number of backtracking points. + + >>> s = Solver() + >>> s.num_scopes() + 0L + >>> s.push() + >>> s.num_scopes() + 1L + >>> s.push() + >>> s.num_scopes() + 2L + >>> s.pop() + >>> s.num_scopes() + 1L + """ + return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver) + def reset(self): """Remove all asserted constraints and backtracking points created using `push()`. diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 63f1d15ff..8d53c9255 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -396,6 +396,33 @@ typedef enum The meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3) + - Z3_OP_BSMUL_NO_OVFL: a predicate to check that bit-wise signed multiplication does not overflow. + Signed multiplication overflows if the operands have the same sign and the result of multiplication + does not fit within the available bits. \sa Z3_mk_bvmul_no_overflow. + + - Z3_OP_BUMUL_NO_OVFL: check that bit-wise unsigned multiplication does not overflow. + Unsigned multiplication overflows if the result does not fit within the available bits. + \sa Z3_mk_bvmul_no_overflow. + + - Z3_OP_BSMUL_NO_UDFL: check that bit-wise signed multiplication does not underflow. + Signed multiplication underflows if the operands have opposite signs and the result of multiplication + does not fit within the avaialble bits. Z3_mk_bvmul_no_underflow. + + - Z3_OP_BSDIV_I: Binary signed division. + It has the same semantics as Z3_OP_BSDIV, but created in a context where the second operand can be assumed to be non-zero. + + - Z3_OP_BUDIV_I: Binary unsigned division. + It has the same semantics as Z3_OP_BUDIV, but created in a context where the second operand can be assumed to be non-zero. + + - Z3_OP_BSREM_I: Binary signed remainder. + It has the same semantics as Z3_OP_BSREM, but created in a context where the second operand can be assumed to be non-zero. + + - Z3_OP_BUREM_I: Binary unsigned remainder. + It has the same semantics as Z3_OP_BUREM, but created in a context where the second operand can be assumed to be non-zero. + + - Z3_OP_BSMOD_I: Binary signed modulus. + It has the same semantics as Z3_OP_BSMOD, but created in a context where the second operand can be assumed to be non-zero. + - Z3_OP_PR_UNDEF: Undef/Null proof object. - Z3_OP_PR_TRUE: Proof for the expression 'true'. @@ -5349,7 +5376,10 @@ extern "C" { /** \brief Add a new formula \c a to the given goal. - Conjunctions are split into separate formulas. + The formula is split according to the following procedure that is applied + until a fixed-point: + Conjunctions are split into separate formulas. + Negations are distributed over disjunctions, resulting in separate formulas. If the goal is \c false, adding new formulas is a no-op. If the formula \c a is \c true, then nothing is added. If the formula \c a is \c false, then the entire goal is replaced by the formula \c false. diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index beb227c33..6d6da9ed5 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -275,7 +275,9 @@ public: bool is_uminus(expr const * n) const { return is_app_of(n, m_afid, OP_UMINUS); } bool is_mul(expr const * n) const { return is_app_of(n, m_afid, OP_MUL); } bool is_div(expr const * n) const { return is_app_of(n, m_afid, OP_DIV); } + bool is_div0(expr const * n) const { return is_app_of(n, m_afid, OP_DIV_0); } bool is_idiv(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV); } + bool is_idiv0(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV_0); } bool is_mod(expr const * n) const { return is_app_of(n, m_afid, OP_MOD); } bool is_rem(expr const * n) const { return is_app_of(n, m_afid, OP_REM); } bool is_to_real(expr const * n) const { return is_app_of(n, m_afid, OP_TO_REAL); } diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 03b4fe637..321943c72 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -732,7 +732,7 @@ void bv_decl_plugin::get_op_names(svector & op_names, symbol const op_names.push_back(builtin_name("bvudiv_i", OP_BUDIV_I)); op_names.push_back(builtin_name("bvsrem_i", OP_BSREM_I)); op_names.push_back(builtin_name("bvurem_i", OP_BUREM_I)); - op_names.push_back(builtin_name("bvumod_i", OP_BSMOD_I)); + op_names.push_back(builtin_name("bvsmod_i", OP_BSMOD_I)); op_names.push_back(builtin_name("ext_rotate_left",OP_EXT_ROTATE_LEFT)); op_names.push_back(builtin_name("ext_rotate_right",OP_EXT_ROTATE_RIGHT)); diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 2c0ba1ce1..99b8c5ac8 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1632,8 +1632,6 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, res_exp = e_exp; - // Result could overflow into 4.xxx ... - family_id bvfid = m_bv_util.get_fid(); expr_ref res_sgn_c1(m), res_sgn_c2(m), res_sgn_c3(m); expr_ref not_e_sgn(m), not_f_sgn(m), not_sign_bv(m); @@ -1646,11 +1644,34 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 }; res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args); + // Result could have overflown into 4.xxx. + SASSERT(m_bv_util.get_bv_size(sig_abs) == 2 * sbits + 2); + expr_ref ovfl_into_4(m); + ovfl_into_4 = m.mk_eq(m_bv_util.mk_extract(2 * sbits + 1, 2 * sbits, sig_abs), + m_bv_util.mk_numeral(1, 2)); + dbg_decouple("fpa2bv_fma_ovfl_into_4", ovfl_into_4); if (sbits > 5) { - sticky_raw = m_bv_util.mk_extract(sbits - 5, 0, sig_abs); - sticky = m_bv_util.mk_zero_extend(sbits + 3, m.mk_app(bvfid, OP_BREDOR, sticky_raw.get())); - expr * res_or_args[2] = { m_bv_util.mk_extract(2 * sbits - 1, sbits - 4, sig_abs), sticky }; - res_sig = m_bv_util.mk_bv_or(2, res_or_args); + expr_ref sticky_raw(m), sig_upper(m), sticky_redd(m), res_sig_norm(m); + sticky_raw = m_bv_util.mk_extract(sbits - 4, 0, sig_abs); + sig_upper = m_bv_util.mk_extract(2 * sbits, sbits - 3, sig_abs); + SASSERT(m_bv_util.get_bv_size(sig_upper) == sbits + 4); + sticky_redd = m.mk_app(bvfid, OP_BREDOR, sticky_raw.get()); + sticky = m_bv_util.mk_zero_extend(sbits + 3, sticky_redd); + expr * res_or_args[2] = { sig_upper, sticky }; + res_sig_norm = m_bv_util.mk_bv_or(2, res_or_args); + + expr_ref sticky_raw_ovfl(m), sig_upper_ovfl(m), sticky_redd_ovfl(m), sticky_ovfl(m), res_sig_ovfl(m); + sticky_raw_ovfl = m_bv_util.mk_extract(sbits - 4, 0, sig_abs); + sig_upper_ovfl = m_bv_util.mk_extract(2 * sbits, sbits - 3, sig_abs); + SASSERT(m_bv_util.get_bv_size(sig_upper_ovfl) == sbits + 4); + sticky_redd_ovfl = m.mk_app(bvfid, OP_BREDOR, sticky_raw_ovfl.get()); + sticky_ovfl = m_bv_util.mk_zero_extend(sbits + 3, sticky_redd_ovfl); + expr * res_or_args_ovfl[2] = { sig_upper_ovfl, sticky_ovfl }; + res_sig_ovfl = m_bv_util.mk_bv_or(2, res_or_args_ovfl); + + res_sig = m.mk_ite(ovfl_into_4, res_sig_ovfl, res_sig_norm); + res_exp = m.mk_ite(ovfl_into_4, m_bv_util.mk_bv_add(res_exp, m_bv_util.mk_numeral(1, ebits+2)), + res_exp); } else { unsigned too_short = 6 - sbits; @@ -1658,6 +1679,8 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, res_sig = m_bv_util.mk_extract(sbits + 3, 0, sig_abs); } dbg_decouple("fpa2bv_fma_add_sum_sticky", sticky); + dbg_decouple("fpa2bv_fma_sig_abs", sig_abs); + dbg_decouple("fpa2bv_fma_res_sig", res_sig); SASSERT(m_bv_util.get_bv_size(res_sig) == sbits + 4); expr_ref is_zero_sig(m), nil_sbits4(m); diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index fa3d69602..b00e1eb6d 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -1030,7 +1030,7 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) { numeral a; - expr* x; + expr* x = 0; if (m_util.is_numeral(arg, a)) { result = m_util.mk_numeral(floor(a), true); return BR_DONE; diff --git a/src/ast/substitution/substitution.cpp b/src/ast/substitution/substitution.cpp index eea1938a6..f741d3fd4 100644 --- a/src/ast/substitution/substitution.cpp +++ b/src/ast/substitution/substitution.cpp @@ -85,7 +85,7 @@ void substitution::apply(unsigned num_actual_offsets, unsigned const * deltas, e m_state = APPLY; unsigned j; - expr * e; + expr * e = 0; unsigned off; expr_offset n1; bool visited; @@ -214,7 +214,7 @@ void substitution::apply(unsigned num_actual_offsets, unsigned const * deltas, e } } SASSERT(m_apply_cache.contains(n)); - m_apply_cache.find(n, e); + VERIFY(m_apply_cache.find(n, e)); m_new_exprs.push_back(e); result = e; diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index d252c3629..a053fc8e6 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -72,14 +72,22 @@ void func_decls::finalize(ast_manager & m) { m_decls = 0; } +bool func_decls::signatures_collide(func_decl* f, func_decl* g) const { + return f == g; +} + bool func_decls::contains(func_decl * f) const { if (GET_TAG(m_decls) == 0) { - return UNTAG(func_decl*, m_decls) == f; + func_decl* g = UNTAG(func_decl*, m_decls); + return g && signatures_collide(f, g); } else { func_decl_set * fs = UNTAG(func_decl_set *, m_decls); - return fs->contains(f); + for (func_decl* g : *fs) { + if (signatures_collide(f, g)) return true; + } } + return false; } bool func_decls::insert(ast_manager & m, func_decl * f) { diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index b231e3c82..74b2f3fbc 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -42,6 +42,7 @@ Notes: class func_decls { func_decl * m_decls; + bool signatures_collide(func_decl* f, func_decl* g) const; public: func_decls():m_decls(0) {} func_decls(ast_manager & m, func_decl * f); diff --git a/src/muz/base/dl_rule_set.cpp b/src/muz/base/dl_rule_set.cpp index e9b383b56..229db4d27 100644 --- a/src/muz/base/dl_rule_set.cpp +++ b/src/muz/base/dl_rule_set.cpp @@ -668,7 +668,7 @@ namespace datalog { T * el = it->m_key; item_set * out_edges = it->m_value; - unsigned el_comp; + unsigned el_comp = 0; VERIFY( m_component_nums.find(el, el_comp) ); item_set::iterator eit = out_edges->begin(); diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp index 518e848c4..247519d63 100644 --- a/src/muz/base/rule_properties.cpp +++ b/src/muz/base/rule_properties.cpp @@ -51,7 +51,8 @@ void rule_properties::collect(rule_set const& rules) { for (unsigned i = 0; m_inf_sort.empty() && i < r->get_decl()->get_arity(); ++i) { sort* d = r->get_decl()->get_domain(i); sort_size sz = d->get_num_elements(); - if (!sz.is_finite()) { + if (!sz.is_finite() && !m_dl.is_rule_sort(d)) { + TRACE("dl", tout << "sort " << mk_pp(d, m) << " is not finite " << sz << "\n";); m_inf_sort.push_back(m_rule); } } diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp index 74206a1f6..5bb47c5c3 100644 --- a/src/muz/rel/dl_relation_manager.cpp +++ b/src/muz/rel/dl_relation_manager.cpp @@ -36,13 +36,10 @@ namespace datalog { void relation_manager::reset_relations() { - relation_map::iterator it=m_relations.begin(); - relation_map::iterator end=m_relations.end(); - for(;it!=end;++it) { - func_decl * pred = it->m_key; + for (auto const& kv : m_relations) { + func_decl * pred = kv.m_key; get_context().get_manager().dec_ref(pred); //inc_ref in get_relation - relation_base * r=(*it).m_value; - r->deallocate(); + kv.m_value->deallocate(); } m_relations.reset(); } @@ -119,35 +116,25 @@ namespace datalog { } void relation_manager::collect_non_empty_predicates(decl_set & res) const { - relation_map::iterator it = m_relations.begin(); - relation_map::iterator end = m_relations.end(); - for(; it!=end; ++it) { - if(!it->m_value->fast_empty()) { - res.insert(it->m_key); + for (auto const& kv : m_relations) { + if (!kv.m_value->fast_empty()) { + res.insert(kv.m_key); } } } void relation_manager::restrict_predicates(const decl_set & preds) { - typedef ptr_vector fd_vector; - fd_vector to_remove; + ptr_vector to_remove; - relation_map::iterator rit = m_relations.begin(); - relation_map::iterator rend = m_relations.end(); - for(; rit!=rend; ++rit) { - func_decl * pred = rit->m_key; + for (auto const& kv : m_relations) { + func_decl* pred = kv.m_key; if (!preds.contains(pred)) { to_remove.insert(pred); } } - fd_vector::iterator pit = to_remove.begin(); - fd_vector::iterator pend = to_remove.end(); - for(; pit!=pend; ++pit) { - func_decl * pred = *pit; - relation_base * rel; - VERIFY( m_relations.find(pred, rel) ); - rel->deallocate(); + for (func_decl* pred : to_remove) { + m_relations.find(pred)->deallocate(); m_relations.remove(pred); get_context().get_manager().dec_ref(pred); } @@ -283,18 +270,16 @@ namespace datalog { } table_plugin * relation_manager::get_table_plugin(symbol const& k) { - table_plugin_vector::iterator tpit = m_table_plugins.begin(); - table_plugin_vector::iterator tpend = m_table_plugins.end(); - for(; tpit!=tpend; ++tpit) { - if((*tpit)->get_name()==k) { - return *tpit; + for (table_plugin * tp : m_table_plugins) { + if (tp->get_name()==k) { + return tp; } } return 0; } table_relation_plugin & relation_manager::get_table_relation_plugin(table_plugin & tp) { - table_relation_plugin * res; + table_relation_plugin * res = 0; VERIFY( m_table_relation_plugins.find(&tp, res) ); return *res; } @@ -341,10 +326,9 @@ namespace datalog { return res; } - for (unsigned i = 0; i < m_relation_plugins.size(); ++i) { - p = m_relation_plugins[i]; - if (p->can_handle_signature(s)) { - return p->mk_empty(s); + for (relation_plugin* p1 : m_relation_plugins) { + if (p1->can_handle_signature(s)) { + return p1->mk_empty(s); } } diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp index 3c1d1b924..1ed847e89 100644 --- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp +++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp @@ -250,7 +250,7 @@ namespace datalog { bool detect_equivalences(expr_ref_vector& v, bool inside_disjunction) { bool have_pair = false; - unsigned prev_pair_idx; + unsigned prev_pair_idx = 0; arg_pair ap; unsigned read_idx = 0; @@ -296,21 +296,20 @@ namespace datalog { br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { - if (m.is_not(f) && (m.is_and(args[0]) || m.is_or(args[0]))) { - SASSERT(num==1); + SASSERT(num == 1); expr_ref tmp(m); app* a = to_app(args[0]); m_app_args.reset(); - for (unsigned i = 0; i < a->get_num_args(); ++i) { - m_brwr.mk_not(a->get_arg(i), tmp); + for (expr* arg : *a) { + m_brwr.mk_not(arg, tmp); m_app_args.push_back(tmp); } if (m.is_and(args[0])) { - result = m.mk_or(m_app_args.size(), m_app_args.c_ptr()); + result = mk_or(m_app_args); } else { - result = m.mk_and(m_app_args.size(), m_app_args.c_ptr()); + result = mk_and(m_app_args); } return BR_REWRITE2; } diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp index 58d319a63..15b723c8c 100644 --- a/src/opt/wmax.cpp +++ b/src/opt/wmax.cpp @@ -216,7 +216,7 @@ namespace opt { rational remove_negations(smt::theory_wmaxsat& th, expr_ref_vector const& core, ptr_vector& keys, vector& weights) { rational min_weight(-1); for (unsigned i = 0; i < core.size(); ++i) { - expr* e; + expr* e = 0; VERIFY(m.is_not(core[i], e)); keys.push_back(m_keys[e]); rational weight = m_weights[e]; diff --git a/src/qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp index 4281ec909..d8ae75256 100644 --- a/src/qe/qe_arith_plugin.cpp +++ b/src/qe/qe_arith_plugin.cpp @@ -2503,7 +2503,7 @@ public: } virtual void subst(contains_app& x, rational const& vl, expr_ref& fml, expr_ref* def) { - nlarith::branch_conditions *brs; + nlarith::branch_conditions *brs = 0; VERIFY (m_cache.find(x.x(), fml, brs)); SASSERT(vl.is_unsigned()); SASSERT(vl.get_unsigned() < brs->size()); diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index 8901c276f..525d084dc 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -32,7 +32,7 @@ namespace sat { void model_converter::reset() { m_entries.finalize(); } - + void model_converter::operator()(model & m) const { vector::const_iterator begin = m_entries.begin(); vector::const_iterator it = m_entries.end(); @@ -46,7 +46,7 @@ namespace sat { literal_vector::const_iterator it2 = it->m_clauses.begin(); literal_vector::const_iterator end2 = it->m_clauses.end(); for (; it2 != end2; ++it2) { - literal l = *it2; + literal l = *it2; if (l == null_literal) { // end of clause if (!sat) { @@ -56,6 +56,7 @@ namespace sat { sat = false; continue; } + if (sat) continue; bool sign = l.sign(); @@ -125,7 +126,7 @@ namespace sat { } return ok; } - + model_converter::entry & model_converter::mk(kind k, bool_var v) { m_entries.push_back(entry(k, v)); entry & e = m_entries.back(); @@ -218,7 +219,7 @@ namespace sat { out << *it2; } out << ")"; - } + } out << ")\n"; } @@ -237,4 +238,22 @@ namespace sat { } } + unsigned model_converter::max_var(unsigned min) const { + unsigned result = min; + vector::const_iterator it = m_entries.begin(); + vector::const_iterator end = m_entries.end(); + for (; it != end; ++it) { + literal_vector::const_iterator lvit = it->m_clauses.begin(); + literal_vector::const_iterator lvend = it->m_clauses.end(); + for (; lvit != lvend; ++lvit) { + literal l = *lvit; + if (l != null_literal) { + if (l.var() > result) + result = l.var(); + } + } + } + return result; + } + }; diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h index b89e6e784..eb2237707 100644 --- a/src/sat/sat_model_converter.h +++ b/src/sat/sat_model_converter.h @@ -26,7 +26,7 @@ namespace sat { \brief Stores eliminated variables and Blocked clauses. It uses these clauses to extend/patch the model produced for the simplified CNF formula. - + This information may also be used to support incremental solving. If new clauses are asserted into the SAT engine, then we can restore the state by re-asserting all clauses in the model @@ -50,7 +50,7 @@ namespace sat { m_kind(src.m_kind), m_clauses(src.m_clauses) { } - bool_var var() const { return m_var; } + bool_var var() const { return m_var; } kind get_kind() const { return static_cast(m_kind); } }; private: @@ -74,8 +74,9 @@ namespace sat { void copy(model_converter const & src); void collect_vars(bool_var_set & s) const; + unsigned max_var(unsigned min) const; }; - + }; #endif diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 7f2b75830..fbfa0ec6b 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -2628,7 +2628,7 @@ namespace sat { unsigned j = 0; for (unsigned i = 0; i < clauses.size(); ++i) { clause & c = *(clauses[i]); - if (c.contains(lit)) { + if (c.contains(lit) || c.contains(~lit)) { detach_clause(c); del_clause(c); } @@ -2684,6 +2684,7 @@ namespace sat { w = max_var(m_clauses, w); w = max_var(true, w); w = max_var(false, w); + v = m_mc.max_var(w); for (unsigned i = 0; i < m_trail.size(); ++i) { if (m_trail[i].var() > w) w = m_trail[i].var(); } @@ -3150,9 +3151,9 @@ namespace sat { } } } - + // Algorithm 7: Corebased Algorithm with Chunking - + static void back_remove(sat::literal_vector& lits, sat::literal l) { for (unsigned i = lits.size(); i > 0; ) { --i; @@ -3176,7 +3177,7 @@ namespace sat { } } } - + static lbool core_chunking(sat::solver& s, model const& m, sat::bool_var_vector const& vars, sat::literal_vector const& asms, vector& conseq, unsigned K) { sat::literal_vector lambda; for (unsigned i = 0; i < vars.size(); i++) { @@ -3375,7 +3376,7 @@ namespace sat { if (check_inconsistent()) return l_false; unsigned num_iterations = 0; - extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq); + extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq); update_unfixed_literals(unfixed_lits, unfixed_vars); while (!unfixed_lits.empty()) { if (scope_lvl() > 1) { @@ -3390,7 +3391,7 @@ namespace sat { unsigned num_assigned = 0; lbool is_sat = l_true; for (; it != end; ++it) { - literal lit = *it; + literal lit = *it; if (value(lit) != l_undef) { ++num_fixed; if (lvl(lit) <= 1 && value(lit) == l_true) { @@ -3445,8 +3446,8 @@ namespace sat { << " iterations: " << num_iterations << " variables: " << unfixed_lits.size() << " fixed: " << conseq.size() - << " status: " << is_sat - << " pre-assigned: " << num_fixed + << " status: " << is_sat + << " pre-assigned: " << num_fixed << " unfixed: " << lits.size() - conseq.size() - unfixed_lits.size() << ")\n";); diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index b6904ef02..baac9f37b 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -131,7 +131,7 @@ public: } bool is_literal(expr* e) const { - return + return is_uninterp_const(e) || (m.is_not(e, e) && is_uninterp_const(e)); } @@ -153,7 +153,7 @@ public: asm2fml.insert(assumptions[i], assumptions[i]); } } - + TRACE("sat", tout << _assumptions << "\n";); dep2asm_t dep2asm; m_model = 0; @@ -163,7 +163,7 @@ public: if (r != l_true) return r; r = m_solver.check(m_asms.size(), m_asms.c_ptr()); - + switch (r) { case l_true: if (sz > 0) { @@ -280,14 +280,14 @@ public: return r; } - // build map from bound variables to + // build map from bound variables to // the consequences that cover them. u_map bool_var2conseq; for (unsigned i = 0; i < lconseq.size(); ++i) { TRACE("sat", tout << lconseq[i] << "\n";); bool_var2conseq.insert(lconseq[i][0].var(), i); } - + // extract original fixed variables u_map asm2dep; extract_asm2dep(dep2asm, asm2dep); @@ -441,7 +441,7 @@ private: lbool internalize_vars(expr_ref_vector const& vars, sat::bool_var_vector& bvars) { for (unsigned i = 0; i < vars.size(); ++i) { - internalize_var(vars[i], bvars); + internalize_var(vars[i], bvars); } return l_true; } @@ -453,7 +453,7 @@ private: bool internalized = false; if (is_uninterp_const(v) && m.is_bool(v)) { sat::bool_var b = m_map.to_bool_var(v); - + if (b != sat::null_bool_var) { bvars.push_back(b); internalized = true; @@ -479,7 +479,7 @@ private: else if (is_uninterp_const(v) && bvutil.is_bv(v)) { // variable does not occur in assertions, so is unconstrained. } - CTRACE("sat", !internalized, tout << "unhandled variable " << mk_pp(v, m) << "\n";); + CTRACE("sat", !internalized, tout << "unhandled variable " << mk_pp(v, m) << "\n";); return internalized; } @@ -506,7 +506,7 @@ private: } expr_ref val(m); expr_ref_vector conj(m); - internalize_value(value, v, val); + internalize_value(value, v, val); while (!premises.empty()) { expr* e = 0; VERIFY(asm2dep.find(premises.pop().index(), e)); diff --git a/src/smt/cached_var_subst.cpp b/src/smt/cached_var_subst.cpp index 1db3aa0a6..c36eb6dd2 100644 --- a/src/smt/cached_var_subst.cpp +++ b/src/smt/cached_var_subst.cpp @@ -23,7 +23,7 @@ bool cached_var_subst::key_eq_proc::operator()(cached_var_subst::key * k1, cache return false; if (k1->m_num_bindings != k2->m_num_bindings) return false; - for (unsigned i = 0; i < k1->m_num_bindings; i++) + for (unsigned i = 0; i < k1->m_num_bindings; i++) if (k1->m_bindings[i] != k2->m_bindings[i]) return false; return true; @@ -49,9 +49,9 @@ void cached_var_subst::operator()(quantifier * qa, unsigned num_bindings, smt::e new_key->m_qa = qa; new_key->m_num_bindings = num_bindings; - for (unsigned i = 0; i < num_bindings; i++) + for (unsigned i = 0; i < num_bindings; i++) new_key->m_bindings[i] = bindings[i]->get_owner(); - + instances::entry * entry = m_instances.insert_if_not_there2(new_key, 0); if (entry->get_data().m_key != new_key) { SASSERT(entry->get_data().m_value != 0); @@ -60,20 +60,27 @@ void cached_var_subst::operator()(quantifier * qa, unsigned num_bindings, smt::e result = entry->get_data().m_value; return; } - - m_proc(qa->get_expr(), new_key->m_num_bindings, new_key->m_bindings, result); + + SASSERT(entry->get_data().m_value == 0); + try { + m_proc(qa->get_expr(), new_key->m_num_bindings, new_key->m_bindings, result); + } + catch (...) { + // CMW: The var_subst reducer was interrupted and m_instances is + // in an inconsistent state; we need to remove (new_key, 0). + m_instances.remove(new_key); + throw; // Throw on to smt::qi_queue/smt::solver. + } + // cache result entry->get_data().m_value = result; // remove key from cache m_new_keys[num_bindings] = 0; - + // increment reference counters m_refs.push_back(qa); for (unsigned i = 0; i < new_key->m_num_bindings; i++) m_refs.push_back(new_key->m_bindings[i]); m_refs.push_back(result); } - - - diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index 530d0ec88..70a3041d2 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -41,7 +41,7 @@ namespace smt { init_parser_vars(); m_vals.resize(15, 0.0f); } - + qi_queue::~qi_queue() { } @@ -50,7 +50,7 @@ namespace smt { if (!m_parser.parse_string(m_params.m_qi_cost.c_str(), m_cost_function)) { // it is not reasonable to abort here during the creation of smt::context just because an invalid option was provided. // throw default_exception("invalid cost function %s", m_params.m_qi_cost.c_str()); - + // using warning message instead warning_msg("invalid cost function '%s', switching to default one", m_params.m_qi_cost.c_str()); // Trying again with default function @@ -107,7 +107,7 @@ namespace smt { m_vals[SIZE] = static_cast(stat->get_size()); m_vals[DEPTH] = static_cast(stat->get_depth()); m_vals[GENERATION] = static_cast(generation); - m_vals[QUANT_GENERATION] = static_cast(stat->get_generation()); + m_vals[QUANT_GENERATION] = static_cast(stat->get_generation()); m_vals[WEIGHT] = static_cast(q->get_weight()); m_vals[VARS] = static_cast(q->get_num_decls()); m_vals[PATTERN_WIDTH] = pat ? static_cast(pat->get_num_args()) : 1.0f; @@ -118,7 +118,7 @@ namespace smt { TRACE("qi_queue_detail", for (unsigned i = 0; i < m_vals.size(); i++) { tout << m_vals[i] << " "; } tout << "\n";); return stat; } - + float qi_queue::get_cost(quantifier * q, app * pat, unsigned generation, unsigned min_top_generation, unsigned max_top_generation) { quantifier_stat * stat = set_values(q, pat, generation, min_top_generation, max_top_generation, 0); float r = m_evaluator(m_cost_function, m_vals.size(), m_vals.c_ptr()); @@ -132,11 +132,11 @@ namespace smt { float r = m_evaluator(m_new_gen_function, m_vals.size(), m_vals.c_ptr()); return static_cast(r); } - + void qi_queue::insert(fingerprint * f, app * pat, unsigned generation, unsigned min_top_generation, unsigned max_top_generation) { quantifier * q = static_cast(f->get_data()); float cost = get_cost(q, pat, generation, min_top_generation, max_top_generation); - TRACE("qi_queue_detail", + TRACE("qi_queue_detail", tout << "new instance of " << q->get_qid() << ", weight " << q->get_weight() << ", generation: " << generation << ", scope_level: " << m_context.get_scope_level() << ", cost: " << cost << "\n"; for (unsigned i = 0; i < f->get_num_args(); i++) { @@ -157,7 +157,7 @@ namespace smt { quantifier * qa = static_cast(f->get_data()); if (curr.m_cost <= m_eager_cost_threshold) { - instantiate(curr); + instantiate(curr); } else if (m_params.m_qi_promote_unsat && m_checker.is_unsat(qa->get_expr(), f->get_num_args(), f->get_args())) { // do not delay instances that produce a conflict. @@ -193,7 +193,7 @@ namespace smt { // This nasty side-effect may change the behavior of Z3. m_manager.trace_stream() << " #" << bindings[i]->get_owner_id(); } - + #endif if (m_manager.proofs_enabled()) m_manager.trace_stream() << " #" << proof_id; @@ -233,7 +233,7 @@ namespace smt { if (m_manager.is_true(s_instance)) { TRACE("checker", tout << "reduced to true, before:\n" << mk_ll_pp(instance, m_manager);); - if (m_manager.has_trace_stream()) + if (m_manager.has_trace_stream()) m_manager.trace_stream() << "[end-of-instance]\n"; return; @@ -278,7 +278,7 @@ namespace smt { pr1 = m_manager.mk_modus_ponens(qi_pr, rw); } else { - app * bare_s_lemma = m_manager.mk_or(m_manager.mk_not(q), s_instance); + app * bare_s_lemma = m_manager.mk_or(m_manager.mk_not(q), s_instance); proof * prs[1] = { pr.get() }; proof * cg = m_manager.mk_congruence(bare_lemma, bare_s_lemma, 1, prs); proof * rw = m_manager.mk_rewrite(bare_s_lemma, lemma); @@ -331,13 +331,13 @@ namespace smt { s.m_instances_lim = m_instances.size(); s.m_instantiated_trail_lim = m_instantiated_trail.size(); } - + void qi_queue::pop_scope(unsigned num_scopes) { unsigned new_lvl = m_scopes.size() - num_scopes; scope & s = m_scopes[new_lvl]; unsigned old_sz = s.m_instantiated_trail_lim; unsigned sz = m_instantiated_trail.size(); - for (unsigned i = old_sz; i < sz; i++) + for (unsigned i = old_sz; i < sz; i++) m_delayed_entries[m_instantiated_trail[i]].m_instantiated = false; m_instantiated_trail.shrink(old_sz); m_delayed_entries.shrink(s.m_delayed_entries_lim); @@ -359,7 +359,7 @@ namespace smt { } bool qi_queue::final_check_eh() { - TRACE("qi_queue", display_delayed_instances_stats(tout); tout << "lazy threshold: " << m_params.m_qi_lazy_threshold + TRACE("qi_queue", display_delayed_instances_stats(tout); tout << "lazy threshold: " << m_params.m_qi_lazy_threshold << ", scope_level: " << m_context.get_scope_level() << "\n";); if (m_params.m_qi_conservative_final_check) { bool init = false; @@ -379,7 +379,7 @@ namespace smt { entry & e = m_delayed_entries[i]; TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); if (!e.m_instantiated && e.m_cost <= min_cost) { - TRACE("qi_queue", + TRACE("qi_queue", tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(e.m_qb->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";); result = false; m_instantiated_trail.push_back(i); @@ -389,13 +389,13 @@ namespace smt { } return result; } - + bool result = true; for (unsigned i = 0; i < m_delayed_entries.size(); i++) { entry & e = m_delayed_entries[i]; TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); if (!e.m_instantiated && e.m_cost <= m_params.m_qi_lazy_threshold) { - TRACE("qi_queue", + TRACE("qi_queue", tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(e.m_qb->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";); result = false; m_instantiated_trail.push_back(i); @@ -443,7 +443,7 @@ namespace smt { quantifier * qa = *it2; delayed_qa_info info; qa2info.find(qa, info); - out << qa->get_qid() << ": " << info.m_num << " [" << info.m_min_cost << ", " << info.m_max_cost << "]\n"; + out << qa->get_qid() << ": " << info.m_num << " [" << info.m_min_cost << ", " << info.m_max_cost << "]\n"; } } @@ -482,6 +482,6 @@ namespace smt { } #endif } - + }; diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index 65272207e..20813602e 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -103,6 +103,7 @@ namespace smt { void context::justify(literal lit, index_set& s) { ast_manager& m = m_manager; + (void)m; b_justification js = get_justification(lit.var()); switch (js.get_kind()) { case b_justification::CLAUSE: { diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 10e2df988..1c8f94edf 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -135,7 +135,7 @@ namespace smt { m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO m_num_instances++; } - TRACE("quantifier", + TRACE("quantifier", tout << mk_pp(q, m()) << " "; for (unsigned i = 0; i < num_bindings; ++i) { tout << mk_pp(bindings[i]->get_owner(), m()) << " "; @@ -372,7 +372,7 @@ namespace smt { quantifier_manager_plugin * plugin = m_imp->m_plugin->mk_fresh(); m_imp->~imp(); m_imp = new (m_imp) imp(*this, ctx, p, plugin); - plugin->set_manager(*this); + plugin->set_manager(*this); } void quantifier_manager::display(std::ostream & out) const { diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h index 6dcf20583..96af9909a 100644 --- a/src/smt/smt_quantifier.h +++ b/src/smt/smt_quantifier.h @@ -75,7 +75,7 @@ namespace smt { }; bool model_based() const; - bool mbqi_enabled(quantifier *q) const; // can mbqi instantiate this quantifier? + bool mbqi_enabled(quantifier *q) const; // can mbqi instantiate this quantifier? void adjust_model(proto_model * m); check_model_result check_model(proto_model * m, obj_map const & root2value); @@ -167,7 +167,7 @@ namespace smt { virtual void push() = 0; virtual void pop(unsigned num_scopes) = 0; - + }; }; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index c5da28df2..0813e1dcd 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -317,6 +317,9 @@ namespace smt { void found_not_handled(expr* n) { + if (a.is_div0(n)) { + return; + } m_not_handled = n; if (is_app(n) && is_underspecified(to_app(n))) { TRACE("arith", tout << "Unhandled: " << mk_pp(n, m) << "\n";); @@ -785,7 +788,7 @@ namespace smt { } void internalize_eq_eh(app * atom, bool_var) { - expr* lhs, *rhs; + expr* lhs = 0, *rhs = 0; VERIFY(m.is_eq(atom, lhs, rhs)); enode * n1 = get_enode(lhs); enode * n2 = get_enode(rhs); @@ -903,7 +906,7 @@ namespace smt { // to_int (to_real x) = x // to_real(to_int(x)) <= x < to_real(to_int(x)) + 1 void mk_to_int_axiom(app* n) { - expr* x, *y; + expr* x = 0, *y = 0; VERIFY (a.is_to_int(n, x)); if (a.is_to_real(x, y)) { mk_axiom(th.mk_eq(y, n, false)); @@ -919,7 +922,7 @@ namespace smt { // is_int(x) <=> to_real(to_int(x)) = x void mk_is_int_axiom(app* n) { - expr* x; + expr* x = 0; VERIFY(a.is_is_int(n, x)); literal eq = th.mk_eq(a.mk_to_real(a.mk_to_int(x)), x, false); literal is_int = ctx().get_literal(n); @@ -1417,12 +1420,14 @@ namespace smt { return; } int num_of_p = m_solver->settings().st().m_num_of_implied_bounds; + (void)num_of_p; local_bound_propagator bp(*this); m_solver->propagate_bounds_for_touched_rows(bp); if (m.canceled()) { return; } int new_num_of_p = m_solver->settings().st().m_num_of_implied_bounds; + (void)new_num_of_p; CTRACE("arith", new_num_of_p > num_of_p, tout << "found " << new_num_of_p << " implied bounds\n";); if (m_solver->get_status() == lp::lp_status::INFEASIBLE) { set_conflict(); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 4dfff21c2..832995994 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1074,7 +1074,7 @@ expr_ref theory_seq::mk_first(expr* s) { void theory_seq::mk_decompose(expr* e, expr_ref& head, expr_ref& tail) { - expr* e1, *e2; + expr* e1 = 0, *e2 = 0; zstring s; if (m_util.str.is_empty(e)) { head = m_util.str.mk_unit(mk_nth(e, m_autil.mk_int(0))); @@ -1401,7 +1401,7 @@ bool theory_seq::occurs(expr* a, expr* b) { // true if a occurs under an interpreted function or under left/right selector. SASSERT(is_var(a)); SASSERT(m_todo.empty()); - expr* e1, *e2; + expr* e1 = 0, *e2 = 0; m_todo.push_back(b); while (!m_todo.empty()) { b = m_todo.back(); @@ -1990,7 +1990,7 @@ bool theory_seq::solve_nc(unsigned idx) { return true; } - expr* e1, *e2; + expr* e1 = 0, *e2 = 0; if (m.is_eq(c, e1, e2)) { literal eq = mk_eq(e1, e2, false); propagate_lit(deps, 0, 0, ~eq); @@ -2246,10 +2246,7 @@ bool theory_seq::internalize_term(app* term) { return true; } TRACE("seq_verbose", tout << mk_pp(term, m) << "\n";); - unsigned num_args = term->get_num_args(); - expr* arg; - for (unsigned i = 0; i < num_args; i++) { - arg = term->get_arg(i); + for (expr* arg : *term) { mk_var(ensure_enode(arg)); } if (m.is_bool(term)) { @@ -2316,7 +2313,7 @@ bool theory_seq::check_int_string() { bool theory_seq::add_stoi_axiom(expr* e) { context& ctx = get_context(); - expr* n; + expr* n = 0; rational val; TRACE("seq", tout << mk_pp(e, m) << "\n";); VERIFY(m_util.str.is_stoi(e, n)); @@ -2398,7 +2395,7 @@ expr_ref theory_seq::digit2int(expr* ch) { bool theory_seq::add_itos_axiom(expr* e) { context& ctx = get_context(); rational val; - expr* n; + expr* n = 0; TRACE("seq", tout << mk_pp(e, m) << "\n";); VERIFY(m_util.str.is_itos(e, n)); if (get_num_value(n, val)) { @@ -2602,9 +2599,9 @@ void theory_seq::collect_statistics(::statistics & st) const { void theory_seq::init_model(expr_ref_vector const& es) { expr_ref new_s(m); - for (unsigned i = 0; i < es.size(); ++i) { + for (expr* e : es) { dependency* eqs = 0; - expr_ref s = canonize(es[i], eqs); + expr_ref s = canonize(e, eqs); if (is_var(s)) { new_s = m_factory->get_fresh_value(m.get_sort(s)); m_rep.update(s, new_s, eqs); @@ -2615,13 +2612,11 @@ void theory_seq::init_model(expr_ref_vector const& es) { void theory_seq::init_model(model_generator & mg) { m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model()); mg.register_factory(m_factory); - for (unsigned j = 0; j < m_nqs.size(); ++j) { - ne const& n = m_nqs[j]; + for (ne const& n : m_nqs) { m_factory->register_value(n.l()); m_factory->register_value(n.r()); } - for (unsigned j = 0; j < m_nqs.size(); ++j) { - ne const& n = m_nqs[j]; + for (ne const& n : m_nqs) { for (unsigned i = 0; i < n.ls().size(); ++i) { init_model(n.ls(i)); init_model(n.rs(i)); @@ -2863,77 +2858,123 @@ bool theory_seq::canonize(expr_ref_vector const& es, expr_ref_vector& result, de return change; } - -expr_ref theory_seq::expand(expr* e0, dependency*& eqs) { +expr_ref theory_seq::expand(expr* e, dependency*& eqs) { + unsigned sz = m_expand_todo.size(); + m_expand_todo.push_back(e); expr_ref result(m); - dependency* deps = 0; - expr_dep ed; - if (m_rep.find_cache(e0, ed)) { - eqs = m_dm.mk_join(eqs, ed.second); - result = ed.first; - return result; + while (m_expand_todo.size() != sz) { + expr* e = m_expand_todo.back(); + result = expand1(e, eqs); + if (result.get()) m_expand_todo.pop_back(); } + return result; +} + +expr_ref theory_seq::try_expand(expr* e, dependency*& eqs){ + expr_ref result(m); + expr_dep ed; + if (m_rep.find_cache(e, ed)) { + if (e != ed.first) { + eqs = m_dm.mk_join(eqs, ed.second); + } + result = ed.first; + } + else { + m_expand_todo.push_back(e); + } + return result; +} +expr_ref theory_seq::expand1(expr* e0, dependency*& eqs) { + expr_ref result(m); + result = try_expand(e0, eqs); + if (result) return result; + dependency* deps = 0; expr* e = m_rep.find(e0, deps); expr* e1, *e2, *e3; + expr_ref arg1(m), arg2(m); context& ctx = get_context(); if (m_util.str.is_concat(e, e1, e2)) { - result = mk_concat(expand(e1, deps), expand(e2, deps)); + arg1 = try_expand(e1, deps); + arg2 = try_expand(e2, deps); + if (!arg1 || !arg2) return result; + result = mk_concat(arg1, arg2); } else if (m_util.str.is_empty(e) || m_util.str.is_string(e)) { result = e; } else if (m_util.str.is_prefix(e, e1, e2)) { - result = m_util.str.mk_prefix(expand(e1, deps), expand(e2, deps)); + arg1 = try_expand(e1, deps); + arg2 = try_expand(e2, deps); + if (!arg1 || !arg2) return result; + result = m_util.str.mk_prefix(arg1, arg2); } else if (m_util.str.is_suffix(e, e1, e2)) { - result = m_util.str.mk_suffix(expand(e1, deps), expand(e2, deps)); + arg1 = try_expand(e1, deps); + arg2 = try_expand(e2, deps); + if (!arg1 || !arg2) return result; + result = m_util.str.mk_suffix(arg1, arg2); } else if (m_util.str.is_contains(e, e1, e2)) { - result = m_util.str.mk_contains(expand(e1, deps), expand(e2, deps)); + arg1 = try_expand(e1, deps); + arg2 = try_expand(e2, deps); + if (!arg1 || !arg2) return result; + result = m_util.str.mk_contains(arg1, arg2); } else if (m_util.str.is_unit(e, e1)) { - result = m_util.str.mk_unit(expand(e1, deps)); + arg1 = try_expand(e1, deps); + if (!arg1) return result; + result = m_util.str.mk_unit(arg1); } else if (m_util.str.is_index(e, e1, e2)) { - result = m_util.str.mk_index(expand(e1, deps), expand(e2, deps), m_autil.mk_int(0)); + arg1 = try_expand(e1, deps); + arg2 = try_expand(e2, deps); + if (!arg1 || !arg2) return result; + result = m_util.str.mk_index(arg1, arg2, m_autil.mk_int(0)); } else if (m_util.str.is_index(e, e1, e2, e3)) { - result = m_util.str.mk_index(expand(e1, deps), expand(e2, deps), e3); + arg1 = try_expand(e1, deps); + arg2 = try_expand(e2, deps); + if (!arg1 || !arg2) return result; + result = m_util.str.mk_index(arg1, arg2, e3); } else if (m.is_ite(e, e1, e2, e3)) { if (ctx.e_internalized(e) && ctx.e_internalized(e2) && ctx.get_enode(e)->get_root() == ctx.get_enode(e2)->get_root()) { - result = expand(e2, deps); + result = try_expand(e2, deps); + if (!result) return result; add_dependency(deps, ctx.get_enode(e), ctx.get_enode(e2)); } else if (ctx.e_internalized(e) && ctx.e_internalized(e2) && ctx.get_enode(e)->get_root() == ctx.get_enode(e3)->get_root()) { - result = expand(e3, deps); + result = try_expand(e3, deps); + if (!result) return result; add_dependency(deps, ctx.get_enode(e), ctx.get_enode(e3)); } else { - literal lit(mk_literal(e1)); + literal lit(mk_literal(e1)); #if 0 - expr_ref sk_ite = mk_sk_ite(e1, e2, e3); - add_axiom(~lit, mk_eq(e2, sk_ite, false)); - add_axiom( lit, mk_eq(e3, sk_ite, false)); - result = sk_ite; - + expr_ref sk_ite = mk_sk_ite(e1, e2, e3); + add_axiom(~lit, mk_eq(e2, sk_ite, false)); + add_axiom( lit, mk_eq(e3, sk_ite, false)); + result = sk_ite; + #else - switch (ctx.get_assignment(lit)) { - case l_true: - deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(lit))); - result = expand(e2, deps); - break; - case l_false: - deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(~lit))); - result = expand(e3, deps); - break; - case l_undef: - result = e; - m_reset_cache = true; - TRACE("seq", tout << "undef: " << result << "\n"; - tout << lit << "@ level: " << ctx.get_scope_level() << "\n";); - break; - } + switch (ctx.get_assignment(lit)) { + case l_true: + deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(lit))); + result = try_expand(e2, deps); + if (!result) return result; + break; + case l_false: + deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(~lit))); + result = try_expand(e3, deps); + if (!result) return result; + break; + case l_undef: + result = e; + m_reset_cache = true; + TRACE("seq", tout << "undef: " << result << "\n"; + tout << lit << "@ level: " << ctx.get_scope_level() << "\n";); + break; + } #endif } } @@ -3151,7 +3192,7 @@ void theory_seq::add_indexof_axiom(expr* i) { */ void theory_seq::add_replace_axiom(expr* r) { - expr* a, *s, *t; + expr* a = 0, *s = 0, *t = 0; VERIFY(m_util.str.is_replace(r, a, s, t)); expr_ref x = mk_skolem(m_indexof_left, a, s); expr_ref y = mk_skolem(m_indexof_right, a, s); @@ -3284,7 +3325,7 @@ void theory_seq::add_itos_length_axiom(expr* len) { void theory_seq::propagate_in_re(expr* n, bool is_true) { TRACE("seq", tout << mk_pp(n, m) << " <- " << (is_true?"true":"false") << "\n";); - expr* e1, *e2; + expr* e1 = 0, *e2 = 0; VERIFY(m_util.str.is_in_re(n, e1, e2)); expr_ref tmp(n, m); @@ -3416,7 +3457,7 @@ bool theory_seq::get_length(expr* e, rational& val) const { if (!tha) return false; rational val1; expr_ref len(m), len_val(m); - expr* e1, *e2; + expr* e1 = 0, *e2 = 0; ptr_vector todo; todo.push_back(e); val.reset(); @@ -3476,7 +3517,7 @@ bool theory_seq::get_length(expr* e, rational& val) const { */ void theory_seq::add_extract_axiom(expr* e) { - expr* s, *i, *l; + expr* s = 0, *i = 0, *l = 0; VERIFY(m_util.str.is_extract(e, s, i, l)); if (is_tail(s, i, l)) { add_tail_axiom(e, s); @@ -3636,7 +3677,7 @@ void theory_seq::add_at_axiom(expr* e) { */ void theory_seq::propagate_step(literal lit, expr* step) { SASSERT(get_context().get_assignment(lit) == l_true); - expr* re, *acc, *s, *idx, *i, *j; + expr* re = 0, *acc = 0, *s = 0, *idx = 0, *i = 0, *j = 0; VERIFY(is_step(step, s, idx, re, i, j, acc)); TRACE("seq", tout << mk_pp(step, m) << " -> " << mk_pp(acc, m) << "\n";); propagate_lit(0, 1, &lit, mk_literal(acc)); @@ -3797,7 +3838,7 @@ void theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp void theory_seq::assign_eh(bool_var v, bool is_true) { context & ctx = get_context(); expr* e = ctx.bool_var2expr(v); - expr* e1, *e2; + expr* e1 = 0, *e2 = 0; expr_ref f(m); bool change = false; literal lit(v, !is_true); @@ -4145,7 +4186,7 @@ expr_ref theory_seq::mk_step(expr* s, expr* idx, expr* re, unsigned i, unsigned rej(s, idx, re, i) -> len(s) > idx if i is final */ void theory_seq::propagate_acc_rej_length(literal lit, expr* e) { - expr *s, * idx, *re; + expr *s = 0, *idx = 0, *re = 0; unsigned src; eautomaton* aut = 0; bool is_acc; @@ -4174,7 +4215,7 @@ bool theory_seq::add_accept2step(expr* acc, bool& change) { TRACE("seq", tout << mk_pp(acc, m) << "\n";); SASSERT(ctx.get_assignment(acc) == l_true); - expr *e, * idx, *re; + expr *e = 0, *idx = 0, *re = 0; expr_ref step(m); unsigned src; eautomaton* aut = 0; @@ -4253,7 +4294,7 @@ bool theory_seq::add_accept2step(expr* acc, bool& change) { bool theory_seq::add_step2accept(expr* step, bool& change) { context& ctx = get_context(); SASSERT(ctx.get_assignment(step) == l_true); - expr* re, *_acc, *s, *idx, *i, *j; + expr* re = 0, *_acc = 0, *s = 0, *idx = 0, *i = 0, *j = 0; VERIFY(is_step(step, s, idx, re, i, j, _acc)); literal acc1 = mk_accept(s, idx, re, i); switch (ctx.get_assignment(acc1)) { @@ -4302,7 +4343,7 @@ Recall we also have: bool theory_seq::add_reject2reject(expr* rej, bool& change) { context& ctx = get_context(); SASSERT(ctx.get_assignment(rej) == l_true); - expr* s, *idx, *re; + expr* s = 0, *idx = 0, *re = 0; unsigned src; rational r; eautomaton* aut = 0; @@ -4364,7 +4405,7 @@ bool theory_seq::add_reject2reject(expr* rej, bool& change) { void theory_seq::propagate_not_prefix(expr* e) { context& ctx = get_context(); - expr* e1, *e2; + expr* e1 = 0, *e2 = 0; VERIFY(m_util.str.is_prefix(e, e1, e2)); literal lit = ctx.get_literal(e); SASSERT(ctx.get_assignment(lit) == l_false); @@ -4393,7 +4434,7 @@ void theory_seq::propagate_not_prefix(expr* e) { void theory_seq::propagate_not_prefix2(expr* e) { context& ctx = get_context(); - expr* e1, *e2; + expr* e1 = 0, *e2 = 0; VERIFY(m_util.str.is_prefix(e, e1, e2)); literal lit = ctx.get_literal(e); SASSERT(ctx.get_assignment(lit) == l_false); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 5fd31e2ca..f7212e608 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -462,7 +462,10 @@ namespace smt { expr_ref canonize(expr* e, dependency*& eqs); bool canonize(expr* e, expr_ref_vector& es, dependency*& eqs); bool canonize(expr_ref_vector const& es, expr_ref_vector& result, dependency*& eqs); + ptr_vector m_expand_todo; expr_ref expand(expr* e, dependency*& eqs); + expr_ref expand1(expr* e, dependency*& eqs); + expr_ref try_expand(expr* e, dependency*& eqs); void add_dependency(dependency*& dep, enode* a, enode* b); void get_concat(expr* e, ptr_vector& concats); diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 523e087f2..2e928af37 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -21,14 +21,13 @@ #include"ast_pp.h" #include"ast_ll_pp.h" #include -#include #include #include"theory_seq_empty.h" #include"theory_arith.h" #include"ast_util.h" namespace smt { - + theory_str::theory_str(ast_manager & m, theory_str_params const & params): theory(m.mk_family_id("seq")), m_params(params), @@ -99,7 +98,7 @@ namespace smt { if (defaultCharset) { // valid C strings can't contain the null byte ('\0') charSetSize = 255; - char_set.resize(256, 0); + char_set.resize(256, 0); int idx = 0; // small letters for (int i = 97; i < 123; i++) { @@ -233,11 +232,11 @@ namespace smt { for (unsigned i = 0; i < num_args; ++i) { enode * arg = e->get_arg(i); theory_var v_arg = mk_var(arg); - TRACE("str", tout << "arg has theory var #" << v_arg << std::endl;); + TRACE("str", tout << "arg has theory var #" << v_arg << std::endl;); (void)v_arg; } theory_var v = mk_var(e); - TRACE("str", tout << "term has theory var #" << v << std::endl;); + TRACE("str", tout << "term has theory var #" << v << std::endl;); (void)v; if (opt_EagerStringConstantLengthAssertions && u.str.is_string(term)) { TRACE("str", tout << "eagerly asserting length of string term " << mk_pp(term, m) << std::endl;); @@ -258,7 +257,7 @@ namespace smt { void theory_str::refresh_theory_var(expr * e) { enode * en = ensure_enode(e); - theory_var v = mk_var(en); + theory_var v = mk_var(en); (void)v; TRACE("str", tout << "refresh " << mk_pp(e, get_manager()) << ": v#" << v << std::endl;); m_basicstr_axiom_todo.push_back(en); } @@ -488,7 +487,6 @@ namespace smt { app * theory_str::mk_str_var(std::string name) { context & ctx = get_context(); - ast_manager & m = get_manager(); TRACE("str", tout << "creating string variable " << name << " at scope level " << sLevel << std::endl;); @@ -506,7 +504,7 @@ namespace smt { // this might help?? mk_var(ctx.get_enode(a)); m_basicstr_axiom_todo.push_back(ctx.get_enode(a)); - TRACE("str", tout << "add " << mk_pp(a, m) << " to m_basicstr_axiom_todo" << std::endl;); + TRACE("str", tout << "add " << mk_pp(a, get_manager()) << " to m_basicstr_axiom_todo" << std::endl;); variable_set.insert(a); internal_variable_set.insert(a); @@ -517,7 +515,6 @@ namespace smt { app * theory_str::mk_regex_rep_var() { context & ctx = get_context(); - ast_manager & m = get_manager(); sort * string_sort = u.str.mk_string_sort(); app * a = mk_fresh_const("regex", string_sort); @@ -528,7 +525,7 @@ namespace smt { SASSERT(ctx.e_internalized(a)); mk_var(ctx.get_enode(a)); m_basicstr_axiom_todo.push_back(ctx.get_enode(a)); - TRACE("str", tout << "add " << mk_pp(a, m) << " to m_basicstr_axiom_todo" << std::endl;); + TRACE("str", tout << "add " << mk_pp(a, get_manager()) << " to m_basicstr_axiom_todo" << std::endl;); variable_set.insert(a); //internal_variable_set.insert(a); @@ -934,8 +931,7 @@ namespace smt { SASSERT(len_xy); // build RHS: start by extracting x and y from Concat(x, y) - unsigned nArgs = a_cat->get_num_args(); - SASSERT(nArgs == 2); + SASSERT(a_cat->get_num_args() == 2); app * a_x = to_app(a_cat->get_arg(0)); app * a_y = to_app(a_cat->get_arg(1)); @@ -1988,7 +1984,8 @@ namespace smt { return NULL; } - static inline std::string rational_to_string_if_exists(const rational & x, bool x_exists) { + // trace code helper + inline std::string rational_to_string_if_exists(const rational & x, bool x_exists) { if (x_exists) { return x.to_string(); } else { @@ -2055,7 +2052,7 @@ namespace smt { << "* |parent| = " << rational_to_string_if_exists(parentLen, parentLen_exists) << std::endl << "* |arg0| = " << rational_to_string_if_exists(arg0Len, arg0Len_exists) << std::endl << "* |arg1| = " << rational_to_string_if_exists(arg1Len, arg1Len_exists) << std::endl; - ); + ); (void)arg0Len_exists; if (parentLen_exists && !arg1Len_exists) { TRACE("str", tout << "make up len for arg1" << std::endl;); @@ -2126,7 +2123,8 @@ namespace smt { << "* |parent| = " << rational_to_string_if_exists(parentLen, parentLen_exists) << std::endl << "* |arg0| = " << rational_to_string_if_exists(arg0Len, arg0Len_exists) << std::endl << "* |arg1| = " << rational_to_string_if_exists(arg1Len, arg1Len_exists) << std::endl; - ); + ); (void)arg1Len_exists; + if (parentLen_exists && !arg0Len_exists) { TRACE("str", tout << "make up len for arg0" << std::endl;); expr_ref implyL11(m.mk_and(ctx.mk_eq_atom(mk_strlen(a_parent), mk_int(parentLen)), @@ -4497,8 +4495,6 @@ namespace smt { } void theory_str::process_unroll_eq_const_str(expr * unrollFunc, expr * constStr) { - ast_manager & m = get_manager(); - if (!u.re.is_unroll(to_app(unrollFunc))) { return; } @@ -4510,8 +4506,8 @@ namespace smt { zstring strValue; u.str.is_string(constStr, strValue); - TRACE("str", tout << "unrollFunc: " << mk_pp(unrollFunc, m) << std::endl - << "constStr: " << mk_pp(constStr, m) << std::endl;); + TRACE("str", tout << "unrollFunc: " << mk_pp(unrollFunc, get_manager()) << std::endl + << "constStr: " << mk_pp(constStr, get_manager()) << std::endl;); if (strValue == "") { return; @@ -4656,7 +4652,7 @@ namespace smt { } } - bool theory_str::get_value(expr* e, rational& val) const { + bool theory_str::get_arith_value(expr* e, rational& val) const { if (opt_DisableIntegerTheoryIntegration) { TRACE("str", tout << "WARNING: integer theory integration disabled" << std::endl;); return false; @@ -4785,7 +4781,7 @@ namespace smt { } }); - if (ctx.e_internalized(len) && get_value(len, val1)) { + if (ctx.e_internalized(len) && get_arith_value(len, val1)) { val += val1; TRACE("str", tout << "integer theory: subexpression " << mk_ismt2_pp(len, m) << " has length " << val1 << std::endl;); } @@ -4808,17 +4804,16 @@ namespace smt { bool theory_str::in_same_eqc(expr * n1, expr * n2) { if (n1 == n2) return true; context & ctx = get_context(); - ast_manager & m = get_manager(); // similar to get_eqc_value(), make absolutely sure // that we've set this up properly for the context if (!ctx.e_internalized(n1)) { - TRACE("str", tout << "WARNING: expression " << mk_ismt2_pp(n1, m) << " was not internalized" << std::endl;); + TRACE("str", tout << "WARNING: expression " << mk_ismt2_pp(n1, get_manager()) << " was not internalized" << std::endl;); ctx.internalize(n1, false); } if (!ctx.e_internalized(n2)) { - TRACE("str", tout << "WARNING: expression " << mk_ismt2_pp(n2, m) << " was not internalized" << std::endl;); + TRACE("str", tout << "WARNING: expression " << mk_ismt2_pp(n2, get_manager()) << " was not internalized" << std::endl;); ctx.internalize(n2, false); } @@ -4877,7 +4872,7 @@ namespace smt { expr * strAst = itor1->first; expr * substrAst = itor1->second; - expr * boolVar; + expr * boolVar = NULL; if (!contain_pair_bool_map.find(strAst, substrAst, boolVar)) { TRACE("str", tout << "warning: no entry for boolVar in contain_pair_bool_map" << std::endl;); } @@ -5014,7 +5009,7 @@ namespace smt { expr * strAst = itor1->first; expr * substrAst = itor1->second; - expr * boolVar; + expr * boolVar = NULL; if (!contain_pair_bool_map.find(strAst, substrAst, boolVar)) { TRACE("str", tout << "warning: no entry for boolVar in contain_pair_bool_map" << std::endl;); } @@ -5625,8 +5620,7 @@ namespace smt { } void theory_str::print_grounded_concat(expr * node, std::map, std::set > > & groundedMap) { - ast_manager & m = get_manager(); - TRACE("str", tout << mk_pp(node, m) << std::endl;); + TRACE("str", tout << mk_pp(node, get_manager()) << std::endl;); if (groundedMap.find(node) != groundedMap.end()) { std::map, std::set >::iterator itor = groundedMap[node].begin(); for (; itor != groundedMap[node].end(); ++itor) { @@ -5634,13 +5628,13 @@ namespace smt { tout << "\t[grounded] "; std::vector::const_iterator vIt = itor->first.begin(); for (; vIt != itor->first.end(); ++vIt) { - tout << mk_pp(*vIt, m) << ", "; + tout << mk_pp(*vIt, get_manager()) << ", "; } tout << std::endl; tout << "\t[condition] "; std::set::iterator sIt = itor->second.begin(); for (; sIt != itor->second.end(); sIt++) { - tout << mk_pp(*sIt, m) << ", "; + tout << mk_pp(*sIt, get_manager()) << ", "; } tout << std::endl; ); @@ -6936,7 +6930,7 @@ namespace smt { } void theory_str::more_value_tests(expr * valTester, zstring valTesterValue) { - ast_manager & m = get_manager(); + ast_manager & m = get_manager(); (void)m; expr * fVar = valueTester_fvar_map[valTester]; if (m_params.m_UseBinarySearch) { @@ -6991,17 +6985,16 @@ namespace smt { } bool theory_str::free_var_attempt(expr * nn1, expr * nn2) { - ast_manager & m = get_manager(); zstring nn2_str; if (internal_lenTest_vars.contains(nn1) && u.str.is_string(nn2, nn2_str)) { - TRACE("str", tout << "acting on equivalence between length tester var " << mk_ismt2_pp(nn1, m) - << " and constant " << mk_ismt2_pp(nn2, m) << std::endl;); + TRACE("str", tout << "acting on equivalence between length tester var " << mk_pp(nn1, get_manager()) + << " and constant " << mk_pp(nn2, get_manager()) << std::endl;); more_len_tests(nn1, nn2_str); return true; } else if (internal_valTest_vars.contains(nn1) && u.str.is_string(nn2, nn2_str)) { if (nn2_str == "more") { - TRACE("str", tout << "acting on equivalence between value var " << mk_ismt2_pp(nn1, m) - << " and constant " << mk_ismt2_pp(nn2, m) << std::endl;); + TRACE("str", tout << "acting on equivalence between value var " << mk_pp(nn1, get_manager()) + << " and constant " << mk_pp(nn2, get_manager()) << std::endl;); more_value_tests(nn1, nn2_str); } return true; @@ -7302,6 +7295,7 @@ namespace smt { // this might help?? theory_var v = mk_var(n); TRACE("str", tout << "variable " << mk_ismt2_pp(ap, get_manager()) << " is #" << v << std::endl;); + (void)v; } } } else if (ex_sort == bool_sort && !is_quantifier(ex)) { @@ -7388,7 +7382,6 @@ namespace smt { } void theory_str::init_search_eh() { - ast_manager & m = get_manager(); context & ctx = get_context(); TRACE("str", @@ -7396,7 +7389,7 @@ namespace smt { unsigned nFormulas = ctx.get_num_asserted_formulas(); for (unsigned i = 0; i < nFormulas; ++i) { expr * ex = ctx.get_asserted_formula(i); - tout << mk_ismt2_pp(ex, m) << (ctx.is_relevant(ex) ? " (rel)" : " (NOT REL)") << std::endl; + tout << mk_pp(ex, get_manager()) << (ctx.is_relevant(ex) ? " (rel)" : " (NOT REL)") << std::endl; } ); /* @@ -7411,36 +7404,6 @@ namespace smt { set_up_axioms(ex); } - /* - * Similar recursive descent, except over all initially assigned terms. - * This is done to find equalities between terms, etc. that we otherwise - * might not get a chance to see. - */ - - /* - expr_ref_vector assignments(m); - ctx.get_assignments(assignments); - for (expr_ref_vector::iterator i = assignments.begin(); i != assignments.end(); ++i) { - expr * ex = *i; - if (m.is_eq(ex)) { - TRACE("str", tout << "processing assignment " << mk_ismt2_pp(ex, m) << - ": expr is equality" << std::endl;); - app * eq = (app*)ex; - SASSERT(eq->get_num_args() == 2); - expr * lhs = eq->get_arg(0); - expr * rhs = eq->get_arg(1); - - enode * e_lhs = ctx.get_enode(lhs); - enode * e_rhs = ctx.get_enode(rhs); - std::pair eq_pair(e_lhs, e_rhs); - m_str_eq_todo.push_back(eq_pair); - } else { - TRACE("str", tout << "processing assignment " << mk_ismt2_pp(ex, m) - << ": expr ignored" << std::endl;); - } - } - */ - // this might be cheating but we need to make sure that certain maps are populated // before the first call to new_eq_eh() propagate(); @@ -7476,8 +7439,7 @@ namespace smt { } void theory_str::assign_eh(bool_var v, bool is_true) { - context & ctx = get_context(); - TRACE("str", tout << "assert: v" << v << " #" << ctx.bool_var2expr(v)->get_id() << " is_true: " << is_true << std::endl;); + TRACE("str", tout << "assert: v" << v << " #" << get_context().bool_var2expr(v)->get_id() << " is_true: " << is_true << std::endl;); } void theory_str::push_scope_eh() { @@ -7544,7 +7506,6 @@ namespace smt { void theory_str::pop_scope_eh(unsigned num_scopes) { sLevel -= num_scopes; TRACE("str", tout << "pop " << num_scopes << " to " << sLevel << std::endl;); - ast_manager & m = get_manager(); TRACE_CODE(if (is_trace_enabled("t_str_dump_assign_on_scope_change")) { dump_assignments(); }); @@ -7553,10 +7514,9 @@ namespace smt { obj_map >::iterator varItor = cut_var_map.begin(); while (varItor != cut_var_map.end()) { - expr * e = varItor->m_key; std::stack & val = cut_var_map[varItor->m_key]; while ((val.size() > 0) && (val.top()->level != 0) && (val.top()->level >= sLevel)) { - TRACE("str", tout << "remove cut info for " << mk_pp(e, m) << std::endl; print_cut_var(e, tout);); + // TRACE("str", tout << "remove cut info for " << mk_pp(e, get_manager()) << std::endl; print_cut_var(e, tout);); // T_cut * aCut = val.top(); val.pop(); // dealloc(aCut); @@ -7578,8 +7538,7 @@ namespace smt { ptr_vector new_m_basicstr; for (ptr_vector::iterator it = m_basicstr_axiom_todo.begin(); it != m_basicstr_axiom_todo.end(); ++it) { enode * e = *it; - app * a = e->get_owner(); - TRACE("str", tout << "consider deleting " << mk_pp(a, get_manager()) + TRACE("str", tout << "consider deleting " << mk_pp(e->get_owner(), get_manager()) << ", enode scope level is " << e->get_iscope_lvl() << std::endl;); if (e->get_iscope_lvl() <= (unsigned)sLevel) { @@ -8481,7 +8440,7 @@ namespace smt { // check integer theory rational Ival; - bool Ival_exists = get_value(a, Ival); + bool Ival_exists = get_arith_value(a, Ival); if (Ival_exists) { TRACE("str", tout << "integer theory assigns " << mk_pp(a, m) << " = " << Ival.to_string() << std::endl;); // if that value is not -1, we can assert (str.to-int S) = Ival --> S = "Ival" @@ -8652,7 +8611,7 @@ namespace smt { rational lenValue; expr_ref concatlenExpr (mk_strlen(concat), m) ; bool allLeafResolved = true; - if (! get_value(concatlenExpr, lenValue)) { + if (! get_arith_value(concatlenExpr, lenValue)) { // the length fo concat is unresolved yet if (get_len_value(concat, lenValue)) { // but all leaf nodes have length information @@ -8689,7 +8648,7 @@ namespace smt { expr * var = *it; rational lenValue; expr_ref varlen (mk_strlen(var), m) ; - if (! get_value(varlen, lenValue)) { + if (! get_arith_value(varlen, lenValue)) { if (propagate_length_within_eqc(var)) { axiomAdded = true; } @@ -8862,7 +8821,7 @@ namespace smt { continue; } bool hasEqcValue = false; - expr * eqcString = get_eqc_value(itor->first, hasEqcValue); + get_eqc_value(itor->first, hasEqcValue); if (!hasEqcValue) { TRACE("str", tout << "found free variable " << mk_pp(itor->first, m) << std::endl;); needToAssignFreeVars = true; @@ -8870,7 +8829,7 @@ namespace smt { // break; } else { // debug - TRACE("str", tout << "variable " << mk_pp(itor->first, m) << " = " << mk_pp(eqcString, m) << std::endl;); + // TRACE("str", tout << "variable " << mk_pp(itor->first, m) << " = " << mk_pp(eqcString, m) << std::endl;); } } } @@ -9105,7 +9064,6 @@ namespace smt { } void theory_str::print_value_tester_list(svector > & testerList) { - ast_manager & m = get_manager(); TRACE("str", int ss = testerList.size(); tout << "valueTesterList = {"; @@ -9114,7 +9072,7 @@ namespace smt { tout << std::endl; } tout << "(" << testerList[i].first << ", "; - tout << mk_ismt2_pp(testerList[i].second, m); + tout << mk_pp(testerList[i].second, get_manager()); tout << "), "; } tout << std::endl << "}" << std::endl; @@ -9217,8 +9175,8 @@ namespace smt { coverAll = get_next_val_encode(val_range_map[lastestValIndi], base); } - long long l = (tries) * distance; - long long h = l; + size_t l = (tries) * distance; + size_t h = l; for (int i = 0; i < distance; i++) { if (coverAll) break; @@ -9239,10 +9197,10 @@ namespace smt { ); // ---------------------------------------------------------------------------------------- - + expr_ref_vector orList(m), andList(m); - for (long long i = l; i < h; i++) { + for (size_t i = l; i < h; i++) { orList.push_back(m.mk_eq(val_indicator, mk_string(longlong_to_string(i).c_str()) )); if (m_params.m_AggressiveValueTesting) { literal lit = mk_eq(val_indicator, mk_string(longlong_to_string(i).c_str()), false); @@ -9346,8 +9304,7 @@ namespace smt { } bool anEqcHasValue = false; - // Z3_ast anEqc = get_eqc_value(t, aTester, anEqcHasValue); - expr * aTester_eqc_value = get_eqc_value(aTester, anEqcHasValue); + get_eqc_value(aTester, anEqcHasValue); if (!anEqcHasValue) { TRACE("str", tout << "value tester " << mk_ismt2_pp(aTester, m) << " doesn't have an equivalence class value." << std::endl;); @@ -9359,8 +9316,8 @@ namespace smt { << mk_ismt2_pp(makeupAssert, m) << std::endl;); assert_axiom(makeupAssert); } else { - TRACE("str", tout << "value tester " << mk_ismt2_pp(aTester, m) - << " == " << mk_ismt2_pp(aTester_eqc_value, m) << std::endl;); + // TRACE("str", tout << "value tester " << mk_ismt2_pp(aTester, m) + // << " == " << mk_ismt2_pp(aTester_eqc_value, m) << std::endl;); } } @@ -9514,8 +9471,8 @@ namespace smt { items.reset(); rational low, high; - bool low_exists = lower_bound(cntInUnr, low); - bool high_exists = upper_bound(cntInUnr, high); + bool low_exists = lower_bound(cntInUnr, low); (void)low_exists; + bool high_exists = upper_bound(cntInUnr, high); (void)high_exists; TRACE("str", tout << "unroll " << mk_pp(unrFunc, mgr) << std::endl; @@ -9523,7 +9480,7 @@ namespace smt { bool unrLenValue_exists = get_len_value(unrFunc, unrLenValue); tout << "unroll length: " << (unrLenValue_exists ? unrLenValue.to_string() : "?") << std::endl; rational cntInUnrValue; - bool cntHasValue = get_value(cntInUnr, cntInUnrValue); + bool cntHasValue = get_arith_value(cntInUnr, cntInUnrValue); tout << "unroll count: " << (cntHasValue ? cntInUnrValue.to_string() : "?") << " low = " << (low_exists ? low.to_string() : "?") @@ -10266,7 +10223,7 @@ namespace smt { } else { tout << "no eqc string constant"; } - tout << std::endl;); + tout << std::endl;); (void)effectiveInScope; if (effectiveLenInd == lenTesterInCbEq) { effectiveLenIndiStr = lenTesterValue; } else { @@ -10351,7 +10308,6 @@ namespace smt { void theory_str::process_free_var(std::map & freeVar_map) { context & ctx = get_context(); - ast_manager & m = get_manager(); std::set eqcRepSet; std::set leafVarSet; @@ -10378,8 +10334,8 @@ namespace smt { } } if (duplicated && dupVar != NULL) { - TRACE("str", tout << "Duplicated free variable found:" << mk_ismt2_pp(freeVar, m) - << " = " << mk_ismt2_pp(dupVar, m) << " (SKIP)" << std::endl;); + TRACE("str", tout << "Duplicated free variable found:" << mk_pp(freeVar, get_manager()) + << " = " << mk_ismt2_pp(dupVar, get_manager()) << " (SKIP)" << std::endl;); continue; } else { eqcRepSet.insert(freeVar); diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 0bbc44ab8..7f39efa70 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -219,7 +219,7 @@ protected: /* * If DisableIntegerTheoryIntegration is set to true, * ALL calls to the integer theory integration methods - * (get_value, get_len_value, lower_bound, upper_bound) + * (get_arith_value, get_len_value, lower_bound, upper_bound) * will ignore what the arithmetic solver believes about length terms, * and will return no information. * @@ -464,7 +464,7 @@ protected: bool in_same_eqc(expr * n1, expr * n2); expr * collect_eq_nodes(expr * n, expr_ref_vector & eqcSet); - bool get_value(expr* e, rational& val) const; + bool get_arith_value(expr* e, rational& val) const; bool get_len_value(expr* e, rational& val); bool lower_bound(expr* _e, rational& lo); bool upper_bound(expr* _e, rational& hi); diff --git a/src/tactic/arith/elim01_tactic.cpp b/src/tactic/arith/elim01_tactic.cpp index 1aef52d78..e00b1e9c0 100644 --- a/src/tactic/arith/elim01_tactic.cpp +++ b/src/tactic/arith/elim01_tactic.cpp @@ -169,7 +169,7 @@ public: for (; bit != bend; ++bit) { if (!is_app(*bit)) continue; app* x = to_app(*bit); - bool s1, s2; + bool s1 = false, s2 = false; rational lo, hi; if (a.is_int(x) && bounds.has_lower(x, lo, s1) && !s1 && zero <= lo && diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index 4c2e0dead..8f37a8d5e 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -176,7 +176,7 @@ public: bound_manager::iterator bit = bounds.begin(), bend = bounds.end(); for (; bit != bend; ++bit) { expr* x = *bit; - bool s1, s2; + bool s1 = false, s2 = false; rational lo, hi; if (a.is_int(x) && bounds.has_lower(x, lo, s1) && !s1 && lo.is_zero() && diff --git a/src/tactic/core/collect_statistics_tactic.cpp b/src/tactic/core/collect_statistics_tactic.cpp index 8e8879fef..3b820de7a 100644 --- a/src/tactic/core/collect_statistics_tactic.cpp +++ b/src/tactic/core/collect_statistics_tactic.cpp @@ -47,10 +47,10 @@ class collect_statistics_tactic : public tactic { public: collect_statistics_tactic(ast_manager & m, params_ref const & p) : - m(m), + m(m), m_params(p) { - } - + } + virtual ~collect_statistics_tactic() {} virtual tactic * translate(ast_manager & m_) { @@ -60,21 +60,21 @@ public: virtual void updt_params(params_ref const & p) { m_params = p; } - + virtual void collect_param_descrs(param_descrs & r) {} virtual void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, proof_converter_ref & pc, + model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { mc = 0; - tactic_report report("collect-statistics", *g); - + tactic_report report("collect-statistics", *g); + collect_proc cp(m, m_stats); - expr_mark visited; + expr_mark visited; const unsigned sz = g->size(); for (unsigned i = 0; i < sz; i++) for_each_expr(cp, visited, g->form(i)); - + std::cout << "(" << std::endl; stats_type::iterator it = m_stats.begin(); stats_type::iterator end = m_stats.end(); @@ -84,7 +84,7 @@ public: g->inc_depth(); result.push_back(g.get()); - } + } virtual void cleanup() {} @@ -98,11 +98,12 @@ protected: class collect_proc { public: ast_manager & m; - stats_type & m_stats; + stats_type & m_stats; obj_hashtable m_seen_sorts; obj_hashtable m_seen_func_decls; + unsigned m_qdepth; - collect_proc(ast_manager & m, stats_type & s) : m(m), m_stats(s) {} + collect_proc(ast_manager & m, stats_type & s) : m(m), m_stats(s), m_qdepth(0) {} void operator()(var * v) { m_stats["bound-variables"]++; @@ -113,7 +114,18 @@ protected: m_stats["quantifiers"]++; SASSERT(is_app(q->get_expr())); app * body = to_app(q->get_expr()); + if (q->is_forall()) + m_stats["forall-variables"] += q->get_num_decls(); + else + m_stats["exists-variables"] += q->get_num_decls(); + m_stats["patterns"] += q->get_num_patterns(); + m_stats["no-patterns"] += q->get_num_no_patterns(); + m_qdepth++; + if (m_stats.find("max-quantification-depth") == m_stats.end() || + m_stats["max-quantification-depth"] < m_qdepth) + m_stats["max-quantification-depth"] = m_qdepth; this->operator()(body); + m_qdepth--; } void operator()(app * n) { @@ -121,7 +133,7 @@ protected: this->operator()(n->get_decl()); } - void operator()(sort * s) { + void operator()(sort * s) { if (m.is_uninterp(s)) { if (!m_seen_sorts.contains(s)) { m_stats["uninterpreted-sorts"]++; @@ -135,7 +147,7 @@ protected: std::stringstream ss; ss << "(declare-sort " << mk_ismt2_pp(s, m, prms) << ")"; m_stats[ss.str()]++; - + if (s->get_info()->get_num_parameters() > 0) { std::stringstream ssname; ssname << "(declare-sort (_ " << s->get_name() << " *))"; diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp index b14d2676c..a3cac9e2e 100644 --- a/src/tactic/goal.cpp +++ b/src/tactic/goal.cpp @@ -137,7 +137,8 @@ void goal::push_back(expr * f, proof * pr, expr_dependency * d) { } void goal::quick_process(bool save_first, expr_ref& f, expr_dependency * d) { - if (!m().is_and(f) && !(m().is_not(f) && m().is_or(to_app(f)->get_arg(0)))) { + expr* g = 0; + if (!m().is_and(f) && !(m().is_not(f, g) && m().is_or(g))) { if (!save_first) { push_back(f, 0, d); } @@ -170,8 +171,8 @@ void goal::quick_process(bool save_first, expr_ref& f, expr_dependency * d) { todo.push_back(expr_pol(t->get_arg(i), false)); } } - else if (m().is_not(curr)) { - todo.push_back(expr_pol(to_app(curr)->get_arg(0), !pol)); + else if (m().is_not(curr, g)) { + todo.push_back(expr_pol(g, !pol)); } else { if (!pol) { diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp index 83693abba..e293ade17 100644 --- a/src/tactic/portfolio/bounded_int2bv_solver.cpp +++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp @@ -168,7 +168,7 @@ public: // translate bit-vector consequences back to integer values for (unsigned i = 0; i < consequences.size(); ++i) { - expr* a, *b, *u, *v; + expr* a = 0, *b = 0, *u = 0, *v = 0; func_decl* f; rational num; unsigned bvsize; @@ -228,7 +228,7 @@ private: for (; it != end; ++it) { expr* e = *it; rational lo, hi; - bool s1, s2; + bool s1 = false, s2 = false; SASSERT(is_uninterp_const(e)); func_decl* f = to_app(e)->get_decl(); diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp index 35601f374..8c9ff122d 100644 --- a/src/tactic/portfolio/enum2bv_solver.cpp +++ b/src/tactic/portfolio/enum2bv_solver.cpp @@ -116,7 +116,7 @@ public: // translate enumeration constants to bit-vectors. for (unsigned i = 0; i < vars.size(); ++i) { - func_decl* f; + func_decl* f = 0; if (is_app(vars[i]) && is_uninterp_const(vars[i]) && m_rewriter.enum2bv().find(to_app(vars[i])->get_decl(), f)) { bvars.push_back(m.mk_const(f)); } @@ -128,7 +128,7 @@ public: // translate bit-vector consequences back to enumeration types for (unsigned i = 0; i < consequences.size(); ++i) { - expr* a, *b, *u, *v; + expr* a = 0, *b = 0, *u = 0, *v = 0; func_decl* f; rational num; unsigned bvsize; diff --git a/src/test/bit_vector.cpp b/src/test/bit_vector.cpp index 7d3f96ae4..6f83bb328 100644 --- a/src/test/bit_vector.cpp +++ b/src/test/bit_vector.cpp @@ -48,7 +48,7 @@ static void tst1() { SASSERT(v1.size() == v2.size()); if (v1.size() > 0) { unsigned idx = rand()%v1.size(); - SASSERT(v1.get(idx) == v2[idx]); + VERIFY(v1.get(idx) == v2[idx]); } } else if (op <= 5) { diff --git a/src/test/bv_simplifier_plugin.cpp b/src/test/bv_simplifier_plugin.cpp index dc930bb82..69b97a9cc 100644 --- a/src/test/bv_simplifier_plugin.cpp +++ b/src/test/bv_simplifier_plugin.cpp @@ -133,7 +133,7 @@ public: params[0] = parameter(2); ar = m_manager.mk_app(m_fid, OP_REPEAT, 1, params, 1, es); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(((a64 << 32) | a64) == u64(e.get())); + VERIFY(((a64 << 32) | a64) == u64(e.get())); ar = m_manager.mk_app(m_fid, OP_BREDOR, e1.get()); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); @@ -163,11 +163,11 @@ public: ar = m_manager.mk_app(m_fid, OP_BIT0); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(!bit2bool(e.get())); + VERIFY(!bit2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_BIT1); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(bit2bool(e.get())); + VERIFY(bit2bool(e.get())); } @@ -187,113 +187,113 @@ public: ar = m_manager.mk_app(m_fid, OP_BADD, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a + b) == u32(e.get())); + VERIFY((a + b) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BSUB, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a - b) == u32(e.get())); + VERIFY((a - b) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BMUL, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a * b) == u32(e.get())); + VERIFY((a * b) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BAND, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a & b) == u32(e.get())); + VERIFY((a & b) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BOR, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a | b) == u32(e.get())); + VERIFY((a | b) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BNOR, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(~(a | b) == u32(e.get())); + VERIFY(~(a | b) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BXOR, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a ^ b) == u32(e.get())); + VERIFY((a ^ b) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BXNOR, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((~(a ^ b)) == u32(e.get())); + VERIFY((~(a ^ b)) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BNAND, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((~(a & b)) == u32(e.get())); + VERIFY((~(a & b)) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_ULEQ, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a <= b) == ast2bool(e.get())); + VERIFY((a <= b) == ast2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_UGEQ, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a >= b) == ast2bool(e.get())); + VERIFY((a >= b) == ast2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_ULT, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a < b) == ast2bool(e.get())); + VERIFY((a < b) == ast2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_UGT, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a > b) == ast2bool(e.get())); + VERIFY((a > b) == ast2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_SLEQ, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((sa <= sb) == ast2bool(e.get())); + VERIFY((sa <= sb) == ast2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_SGEQ, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((sa >= sb) == ast2bool(e.get())); + VERIFY((sa >= sb) == ast2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_SLT, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((sa < sb) == ast2bool(e.get())); + VERIFY((sa < sb) == ast2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_SGT, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((sa > sb) == ast2bool(e.get())); + VERIFY((sa > sb) == ast2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_BSHL, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(((b>=32)?0:(a << b)) == u32(e.get())); + VERIFY(((b>=32)?0:(a << b)) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BLSHR, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(((b>=32)?0:(a >> b)) == u32(e.get())); + VERIFY(((b>=32)?0:(a >> b)) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BASHR, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); std::cout << "compare: " << sa << " >> " << b << " = " << (sa >> b) << " with " << i32(e.get()) << "\n"; - SASSERT(b >= 32 || ((sa >> b) == i32(e.get()))); + VERIFY(b >= 32 || ((sa >> b) == i32(e.get()))); if (b != 0) { ar = m_manager.mk_app(m_fid, OP_BSDIV, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((sa / sb) == i32(e.get())); + VERIFY((sa / sb) == i32(e.get())); ar = m_manager.mk_app(m_fid, OP_BUDIV, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a / b) == u32(e.get())); + VERIFY((a / b) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BSREM, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - //SASSERT((sa % sb) == i32(e.get())); + //VERIFY((sa % sb) == i32(e.get())); ar = m_manager.mk_app(m_fid, OP_BUREM, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a % b) == u32(e.get())); + VERIFY((a % b) == u32(e.get())); // TBD: BSMOD. } ar = m_manager.mk_app(m_fid, OP_CONCAT, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(((a64 << 32) | b64) == u64(e.get())); + VERIFY(((a64 << 32) | b64) == u64(e.get())); ar = m_manager.mk_app(m_fid, OP_BCOMP, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a == b) == bit2bool(e.get())); + VERIFY((a == b) == bit2bool(e.get())); } void test() { diff --git a/src/test/check_assumptions.cpp b/src/test/check_assumptions.cpp index fa8327cd4..918513ca0 100644 --- a/src/test/check_assumptions.cpp +++ b/src/test/check_assumptions.cpp @@ -38,7 +38,7 @@ void tst_check_assumptions() expr * npE = np.get(); lbool res1 = ctx.check(1, &npE); - SASSERT(res1==l_true); + VERIFY(res1 == l_true); ctx.assert_expr(npE); diff --git a/src/test/cnf_backbones.cpp b/src/test/cnf_backbones.cpp index 14fc594b6..3fdf96f87 100644 --- a/src/test/cnf_backbones.cpp +++ b/src/test/cnf_backbones.cpp @@ -38,6 +38,7 @@ static void STD_CALL on_ctrl_c(int) { raise(SIGINT); } +#if 0 static void display_model(sat::solver const & s) { sat::model const & m = s.get_model(); for (unsigned i = 1; i < m.size(); i++) { @@ -49,6 +50,7 @@ static void display_model(sat::solver const & s) { } std::cout << "\n"; } +#endif static void display_status(lbool r) { switch (r) { diff --git a/src/test/dl_context.cpp b/src/test/dl_context.cpp index ac09722ac..8a62dcb7d 100644 --- a/src/test/dl_context.cpp +++ b/src/test/dl_context.cpp @@ -14,6 +14,36 @@ Copyright (c) 2015 Microsoft Corporation using namespace datalog; +void tst_dl_context() { + + return; + +#if 0 + symbol relations[] = { symbol("tr_skip"), symbol("tr_sparse"), symbol("tr_hashtable"), symbol("smt_relation2") }; + + const unsigned rel_cnt = sizeof(relations)/sizeof(symbol); + const char * test_file = "c:\\tvm\\src\\benchmarks\\datalog\\t0.datalog"; + + params_ref params; + for(unsigned rel_index=0; rel_index=0; eager_checking--) { + params.set_bool("eager_emptiness_checking", eager_checking!=0); + + std::cerr << "Testing " << relations[rel_index] << "\n"; + std::cerr << "Eager emptiness checking " << (eager_checking!=0 ? "on" : "off") << "\n"; + dl_context_simple_query_test(params); + dl_context_saturate_file(params, test_file); + } + } +#endif + +} + + +#if 0 + + static lbool dl_context_eval_unary_predicate(ast_manager & m, context & ctx, char const* problem_text, const char * pred_name) { parser* p = parser::create(ctx,m); @@ -72,29 +102,4 @@ void dl_context_saturate_file(params_ref & params, const char * f) { ctx.get_rel_context()->saturate(); std::cerr << "Done\n"; } - -void tst_dl_context() { - symbol relations[] = { symbol("tr_skip"), symbol("tr_sparse"), symbol("tr_hashtable"), symbol("smt_relation2") }; - const unsigned rel_cnt = sizeof(relations)/sizeof(symbol); - - return; -#if 0 - const char * test_file = "c:\\tvm\\src\\benchmarks\\datalog\\t0.datalog"; - - params_ref params; - for(unsigned rel_index=0; rel_index=0; eager_checking--) { - params.set_bool("eager_emptiness_checking", eager_checking!=0); - - std::cerr << "Testing " << relations[rel_index] << "\n"; - std::cerr << "Eager emptiness checking " << (eager_checking!=0 ? "on" : "off") << "\n"; - dl_context_simple_query_test(params); - dl_context_saturate_file(params, test_file); - } - } #endif -} - - - diff --git a/src/test/dl_query.cpp b/src/test/dl_query.cpp index ae7313e41..e69f1fb13 100644 --- a/src/test/dl_query.cpp +++ b/src/test/dl_query.cpp @@ -40,7 +40,7 @@ void dl_query_ask_for_last_arg(context & ctx, func_decl * pred, relation_fact & lbool is_sat = ctx.query(query); std::cerr << "@@ last arg query should succeed: " << should_be_successful << "\n"; - SASSERT(is_sat != l_undef); + VERIFY(is_sat != l_undef); relation_fact res_fact(m); res_fact.push_back(f.back()); diff --git a/src/test/ext_numeral.cpp b/src/test/ext_numeral.cpp index 0e2b691c9..6f92b1372 100644 --- a/src/test/ext_numeral.cpp +++ b/src/test/ext_numeral.cpp @@ -158,8 +158,7 @@ static void FUN_NAME(int a, ext_numeral_kind ak, int b, ext_numeral_kind bk, boo scoped_mpq _a(m), _b(m); \ m.set(_a, a); \ m.set(_b, b); \ - bool r = OP_NAME(m, _a, ak, _b, bk); \ - SASSERT(r == expected); \ + VERIFY(expected == OP_NAME(m, _a, ak, _b, bk)); \ } #define MK_TST_REL(NAME) MK_TST_REL_CORE(tst_ ## NAME, NAME) diff --git a/src/test/heap.cpp b/src/test/heap.cpp index e745463ff..17f9cfaa0 100644 --- a/src/test/heap.cpp +++ b/src/test/heap.cpp @@ -47,12 +47,13 @@ static void tst1() { for (; it != end; ++it) { SASSERT(h.contains(*it)); } - int last = -1; while (!h.empty()) { int m1 = h.min_value(); int m2 = h.erase_min(); + (void)m1; + (void)m2; SASSERT(m1 == m2); - SASSERT(last < m2); + SASSERT(-1 < m2); } } @@ -76,6 +77,7 @@ static void dump_heap(const int_heap2 & h, std::ostream & out) { } static void tst2() { + (void)dump_heap; int_heap2 h(N); for (int i = 0; i < N * 10; i++) { if (i % 1000 == 0) std::cout << "i: " << i << std::endl; diff --git a/src/test/hwf.cpp b/src/test/hwf.cpp index be32b5400..7a030a452 100644 --- a/src/test/hwf.cpp +++ b/src/test/hwf.cpp @@ -44,19 +44,19 @@ static void bug_to_rational() { unsynch_mpq_manager mq; scoped_mpq r(mq); - double ad, rd; + double ad = 0, rd = 0; m.set(a, 0.0); m.to_rational(a, r); ad = m.to_double(a); rd = mq.get_double(r); - SASSERT(ad == rd); + VERIFY(ad == rd); m.set(a, 1.0); m.to_rational(a, r); ad = m.to_double(a); rd = mq.get_double(r); - SASSERT(ad == rd); + VERIFY(ad == rd); m.set(a, 1.5); m.to_rational(a, r); diff --git a/src/test/karr.cpp b/src/test/karr.cpp index c5581cc66..c69932e22 100644 --- a/src/test/karr.cpp +++ b/src/test/karr.cpp @@ -58,7 +58,7 @@ namespace karr { } lbool is_sat = hb.saturate(); hb.display(std::cout); - SASSERT(is_sat == l_true); + VERIFY(is_sat == l_true); dst.reset(); unsigned basis_size = hb.get_basis_size(); for (unsigned i = 0; i < basis_size; ++i) { @@ -85,7 +85,7 @@ namespace karr { } lbool is_sat = hb.saturate(); hb.display(std::cout); - SASSERT(is_sat == l_true); + VERIFY(is_sat == l_true); dst.reset(); unsigned basis_size = hb.get_basis_size(); bool first_initial = true; diff --git a/src/test/list.cpp b/src/test/list.cpp index 5672f4246..a7ad76972 100644 --- a/src/test/list.cpp +++ b/src/test/list.cpp @@ -35,6 +35,7 @@ static void tst1() { list * l5 = append(r, l4, l2); TRACE("list", display(tout, l5->begin(), l5->end()); tout << "\n";); list * l6 = append(r, l5, l5); + (void) l6; TRACE("list", display(tout, l6->begin(), l6->end()); tout << "\n";); } diff --git a/src/test/model_based_opt.cpp b/src/test/model_based_opt.cpp index 64b2df285..5ee671a4a 100644 --- a/src/test/model_based_opt.cpp +++ b/src/test/model_based_opt.cpp @@ -20,6 +20,7 @@ static void add_ineq(opt::model_based_opt& mbo, mbo.add_constraint(vars, rational(k), rel); } +#if 0 static void add_ineq(opt::model_based_opt& mbo, unsigned x, int a, unsigned y, int b, @@ -31,6 +32,7 @@ static void add_ineq(opt::model_based_opt& mbo, vars.push_back(var(z, rational(c))); mbo.add_constraint(vars, rational(k), rel); } +#endif static void add_random_ineq(opt::model_based_opt& mbo, random_gen& r, @@ -295,7 +297,7 @@ static void test8() { unsigned z = mbo.add_var(rational(4)); unsigned u = mbo.add_var(rational(5)); unsigned v = mbo.add_var(rational(6)); - unsigned w = mbo.add_var(rational(6)); + // unsigned w = mbo.add_var(rational(6)); add_ineq(mbo, x0, 1, y, -1, 0, opt::t_le); add_ineq(mbo, x, 1, y, -1, 0, opt::t_lt); diff --git a/src/test/model_evaluator.cpp b/src/test/model_evaluator.cpp index 0b509fba6..00048b230 100644 --- a/src/test/model_evaluator.cpp +++ b/src/test/model_evaluator.cpp @@ -28,7 +28,6 @@ void tst_model_evaluator() { expr_ref vB2(m.mk_var(2, m.mk_bool_sort()), m); expr* vI0p = vI0.get(); expr* vI1p = vI1.get(); - expr* vB0p = vB0.get(); expr* vB1p = vB1.get(); expr* vB2p = vB2.get(); diff --git a/src/test/mpff.cpp b/src/test/mpff.cpp index 44930f2bd..ca2354b8b 100644 --- a/src/test/mpff.cpp +++ b/src/test/mpff.cpp @@ -435,7 +435,7 @@ static void tst_limits(unsigned prec) { bool overflow = false; try { m.inc(a); } catch (mpff_manager::overflow_exception) { overflow = true; } - SASSERT(overflow); + VERIFY(overflow); m.set_max(a); m.dec(a); SASSERT(m.eq(a, b)); diff --git a/src/test/mpz.cpp b/src/test/mpz.cpp index ee7cf39f1..02627e842 100644 --- a/src/test/mpz.cpp +++ b/src/test/mpz.cpp @@ -147,6 +147,7 @@ void tst_div2k(synch_mpz_manager & m, mpz const & v, unsigned k) { m.power(two, k, pw); m.machine_div(v, pw, y); bool is_eq = m.eq(x, y); + (void)is_eq; CTRACE("mpz_2k", !is_eq, tout << "div: " << m.to_string(v) << ", k: " << k << " r: " << m.to_string(x) << ", expected: " << m.to_string(y) << "\n";); SASSERT(is_eq); m.del(x); @@ -174,6 +175,7 @@ void tst_mul2k(synch_mpz_manager & m, mpz const & v, unsigned k) { m.power(two, k, pw); m.mul(v, pw, y); bool is_eq = m.eq(x, y); + (void)is_eq; CTRACE("mpz_2k", !is_eq, tout << "mul: " << m.to_string(v) << ", k: " << k << " r: " << m.to_string(x) << ", expected: " << m.to_string(y) << "\n";); SASSERT(is_eq); m.del(x); diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index 27a0aa1da..df25db927 100644 --- a/src/test/nlsat.cpp +++ b/src/test/nlsat.cpp @@ -391,7 +391,6 @@ static void tst7() { params_ref ps; reslimit rlim; nlsat::solver s(rlim, ps); - anum_manager & am = s.am(); nlsat::pmanager & pm = s.pm(); nlsat::var x0, x1, x2, a, b, c, d; a = s.mk_var(false); @@ -423,7 +422,7 @@ static void tst7() { nlsat::literal_vector litsv(lits.size(), lits.c_ptr()); lbool res = s.check(litsv); - SASSERT(res == l_false); + VERIFY(res == l_false); for (unsigned i = 0; i < litsv.size(); ++i) { s.display(std::cout, litsv[i]); std::cout << " "; diff --git a/src/test/object_allocator.cpp b/src/test/object_allocator.cpp index 16b9331e2..cca42cf6f 100644 --- a/src/test/object_allocator.cpp +++ b/src/test/object_allocator.cpp @@ -61,6 +61,7 @@ static void tst1() { m.recycle(c1); cell * c3 = m.allocate(); + (void)c3; SASSERT(c3->m_coeff.is_zero()); } diff --git a/src/test/old_interval.cpp b/src/test/old_interval.cpp index 92064c03e..12a45555d 100644 --- a/src/test/old_interval.cpp +++ b/src/test/old_interval.cpp @@ -120,9 +120,9 @@ class interval_tester { interval singleton(int i) { return interval(m, rational(i)); } interval all() { return interval(m); } - interval l(int i, bool o = false, int idx = 0) { return interval(m, rational(i), o, true, idx == 0 ? 0 : m.mk_leaf(reinterpret_cast(idx))); } - interval r(int i, bool o = false, int idx = 0) { return interval(m, rational(i), o, false, idx == 0 ? 0 : m.mk_leaf(reinterpret_cast(idx))); } - interval b(int l, int u, bool lo = false, bool uo = false, int idx_l = 0, int idx_u = 0) { + interval l(int i, bool o = false, size_t idx = 0) { return interval(m, rational(i), o, true, idx == 0 ? 0 : m.mk_leaf(reinterpret_cast(idx))); } + interval r(int i, bool o = false, size_t idx = 0) { return interval(m, rational(i), o, false, idx == 0 ? 0 : m.mk_leaf(reinterpret_cast(idx))); } + interval b(int l, int u, bool lo = false, bool uo = false, size_t idx_l = 0, size_t idx_u = 0) { return interval(m, rational(l), lo, idx_l == 0 ? 0 : m.mk_leaf(reinterpret_cast(idx_l)), rational(u), uo, idx_u == 0 ? 0 : m.mk_leaf(reinterpret_cast(idx_u))); } diff --git a/src/test/pb2bv.cpp b/src/test/pb2bv.cpp index c114997c5..fcc309883 100644 --- a/src/test/pb2bv.cpp +++ b/src/test/pb2bv.cpp @@ -83,10 +83,10 @@ static void test_semantics(ast_manager& m, expr_ref_vector const& vars, vectorcheck_sat(0,0); - SASSERT(res == l_true); + VERIFY(res == l_true); slv->assert_expr(m.is_true(result2) ? m.mk_not(result1) : result1.get()); res = slv->check_sat(0,0); - SASSERT(res == l_false); + VERIFY(res == l_false); } } diff --git a/src/test/polynorm.cpp b/src/test/polynorm.cpp index a8f4ab861..987d8e13b 100644 --- a/src/test/polynorm.cpp +++ b/src/test/polynorm.cpp @@ -88,6 +88,8 @@ private: expr_ref_vector& factors = poly.factors(); expr_ref_vector& coefficients = poly.coefficients(); expr_ref& coefficient = poly.coefficient(); + (void) coefficient; + (void) coefficients; m_rw(term); @@ -170,7 +172,7 @@ static expr_ref mk_mul(arith_util& arith, unsigned num_args, expr* const* args) static void nf(expr_ref& term) { ast_manager& m = term.get_manager(); - expr *e1, *e2; + expr *e1 = 0, *e2 = 0; th_rewriter rw(m); arith_util arith(m); diff --git a/src/test/proof_checker.cpp b/src/test/proof_checker.cpp index 7f9827187..035326b26 100644 --- a/src/test/proof_checker.cpp +++ b/src/test/proof_checker.cpp @@ -11,7 +11,6 @@ void tst_checker1() { ast_manager m(PGM_FINE); expr_ref a(m); proof_ref p1(m), p2(m), p3(m), p4(m); - bool result; expr_ref_vector side_conditions(m); a = m.mk_const(symbol("a"), m.mk_bool_sort()); @@ -26,8 +25,7 @@ void tst_checker1() { proof_checker checker(m); p4 = m.mk_lemma(p3.get(), m.mk_or(a.get(), m.mk_not(a.get()))); ast_ll_pp(std::cout, m, p4.get()); - result = checker.check(p4.get(), side_conditions); - SASSERT(result); + VERIFY(checker.check(p4.get(), side_conditions)); } void tst_proof_checker() { diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp index a73f7ed38..a52c02ecb 100644 --- a/src/test/qe_arith.cpp +++ b/src/test/qe_arith.cpp @@ -163,7 +163,7 @@ static app_ref generate_ineqs(ast_manager& m, sort* s, vector& app* x = vars[0].get(); app* y = vars[1].get(); - app* z = vars[2].get(); + // app* z = vars[2].get(); // // ax <= by, ax < by, not (ax >= by), not (ax > by) // @@ -247,7 +247,7 @@ static void test2(char const *ex) { ctx.push(); ctx.assert_expr(fml); lbool result = ctx.check(); - SASSERT(result == l_true); + VERIFY(result == l_true); ref md; ctx.get_model(md); ctx.pop(1); diff --git a/src/test/rational.cpp b/src/test/rational.cpp index 834aab92f..ac478af98 100644 --- a/src/test/rational.cpp +++ b/src/test/rational.cpp @@ -196,7 +196,7 @@ static void tst2() { // get_int64, get_uint64 uint64 u1 = uint64_max.get_uint64(); uint64 u2 = UINT64_MAX; - SASSERT(u1 == u2); + VERIFY(u1 == u2); std::cout << "int64_max: " << int64_max << ", INT64_MAX: " << INT64_MAX << ", int64_max.get_int64(): " << int64_max.get_int64() << ", int64_max.get_uint64(): " << int64_max.get_uint64() << "\n"; SASSERT(int64_max.get_int64() == INT64_MAX); SASSERT(int64_min.get_int64() == INT64_MIN); diff --git a/src/test/sat_user_scope.cpp b/src/test/sat_user_scope.cpp index aa717f371..a271ce6bb 100644 --- a/src/test/sat_user_scope.cpp +++ b/src/test/sat_user_scope.cpp @@ -34,10 +34,6 @@ static void add_clause(sat::solver& s, random_gen& r, trail_t& t) { s.mk_clause(cls.size(), cls.c_ptr()); } -static void display_state(std::ostream& out, sat::solver& s, trail_t& t) { - s.display(out); -} - static void pop_user_scope(sat::solver& s, trail_t& t) { std::cout << "pop\n"; s.user_pop(1); diff --git a/src/test/simple_parser.cpp b/src/test/simple_parser.cpp index a5d4d8def..934552711 100644 --- a/src/test/simple_parser.cpp +++ b/src/test/simple_parser.cpp @@ -38,6 +38,7 @@ void tst_simple_parser() { TRACE("simple_parser", tout << mk_pp(r, m) << "\n";); p.parse_string("(+ x (* y x) x)", r); float vals[2] = { 2.0f, 3.0f }; + (void)vals; TRACE("simple_parser", tout << mk_pp(r, m) << "\n"; tout << "val: " << eval(r, 2, vals) << "\n";); diff --git a/src/test/small_object_allocator.cpp b/src/test/small_object_allocator.cpp index 1ecf865dd..5ae2836d0 100644 --- a/src/test/small_object_allocator.cpp +++ b/src/test/small_object_allocator.cpp @@ -36,5 +36,14 @@ void tst_small_object_allocator() { r3 = new (soa) char[1]; TRACE("small_object_allocator", tout << "r1: " << (void*)r1 << " r2: " << (void*)r2 << " r3: " << (void*)r3 << " r4: " << (void*)r4 << "\n";); + (void)r1; + (void)r2; + (void)r3; + (void)r4; + (void)q1; + + (void)p1; + (void)p2; + (void)p3; } diff --git a/src/test/sorting_network.cpp b/src/test/sorting_network.cpp index 81340651a..87cc05375 100644 --- a/src/test/sorting_network.cpp +++ b/src/test/sorting_network.cpp @@ -364,15 +364,13 @@ void test_at_most_1(unsigned n, bool full) { for (unsigned i = 0; i < ext.m_clauses.size(); ++i) { solver.assert_expr(ext.m_clauses[i].get()); } - lbool res; if (full) { solver.push(); solver.assert_expr(m.mk_not(m.mk_eq(result1, result2))); std::cout << result1 << "\n"; - res = solver.check(); - SASSERT(res == l_false); + VERIFY(l_false == solver.check()); solver.pop(1); } @@ -390,8 +388,7 @@ void test_at_most_1(unsigned n, bool full) { std::cout << atom << "\n"; if (is_true) ++k; } - res = solver.check(); - SASSERT(res == l_true); + VERIFY(l_false == solver.check()); if (k > 1) { solver.assert_expr(result1); } @@ -402,8 +399,7 @@ void test_at_most_1(unsigned n, bool full) { else { solver.assert_expr(m.mk_not(result1)); } - res = solver.check(); - SASSERT(res == l_false); + VERIFY(l_false == solver.check()); solver.pop(1); } } diff --git a/src/test/substitution.cpp b/src/test/substitution.cpp index cdc7f2080..5609225c6 100644 --- a/src/test/substitution.cpp +++ b/src/test/substitution.cpp @@ -35,6 +35,8 @@ void tst_substitution() bool ok1 = unif(v1.get(), v2.get(), subst, false); bool ok2 = unif(v2.get(), v1.get(), subst, false); + (void)ok1; + (void)ok2; expr_ref res(m); diff --git a/src/test/upolynomial.cpp b/src/test/upolynomial.cpp index e7dcf2719..43aefed99 100644 --- a/src/test/upolynomial.cpp +++ b/src/test/upolynomial.cpp @@ -129,18 +129,18 @@ static void tst_isolate_roots(polynomial_ref const & p, unsigned prec, mpbq_mana tout << "fourier upper: " << um.sign_variations_at(fseq, uppers[i]) << "\n";); unsigned fsv_lower = um.sign_variations_at(fseq, lowers[i]); unsigned fsv_upper = um.sign_variations_at(fseq, uppers[i]); - SASSERT(um.eval_sign_at(q.size(), q.c_ptr(), lowers[i]) == 0 || - um.eval_sign_at(q.size(), q.c_ptr(), uppers[i]) == 0 || + VERIFY(um.eval_sign_at(q.size(), q.c_ptr(), lowers[i]) == 0 || + um.eval_sign_at(q.size(), q.c_ptr(), uppers[i]) == 0 || // fsv_lower - fsv_upper is an upper bound for the number of roots in the interval // fsv_upper - fsv_upper - num_roots is even // Recall that num_roots == 1 in the interval. - (fsv_lower - fsv_upper >= 1 && (fsv_lower - fsv_upper - 1) % 2 == 0)); - + (fsv_lower - fsv_upper >= 1 && (fsv_lower - fsv_upper - 1) % 2 == 0)); + // Double checking using Descartes bounds for the interval // Must use square free component. unsigned dab = um.descartes_bound_a_b(q_sqf.size(), q_sqf.c_ptr(), bqm, lowers[i], uppers[i]); TRACE("upolynomial", tout << "Descartes bound: " << dab << "\n";); - SASSERT(dab == 1); + VERIFY(dab == 1); } } std::cout << "\n"; @@ -164,7 +164,7 @@ static void check_roots(mpbq_vector const & roots, mpbq_vector const & lowers, m for (unsigned j = 0; j < roots.size(); j++) { if (to_rational(roots[j]) == r) { SASSERT(!visited[j]); - SASSERT(!found); + VERIFY(!found); found = true; visited[j] = true; } @@ -172,7 +172,7 @@ static void check_roots(mpbq_vector const & roots, mpbq_vector const & lowers, m for (unsigned j = 0; j < lowers.size(); j++) { unsigned j_prime = j + roots.size(); if (to_rational(lowers[j]) < r && r < to_rational(uppers[j])) { - SASSERT(!found); + VERIFY(!found); SASSERT(!visited[j_prime]); found = true; visited[j_prime] = true; @@ -499,7 +499,7 @@ static void tst_refinable(polynomial_ref const & p, mpbq_manager & bqm, mpbq & a std::cout << "new (" << bqm.to_string(a) << ", " << bqm.to_string(b) << ")\n"; int sign_a = um.eval_sign_at(_p.size(), _p.c_ptr(), a); int sign_b = um.eval_sign_at(_p.size(), _p.c_ptr(), b); - SASSERT(sign_a != 0 && sign_b != 0 && sign_a == -sign_b); + VERIFY(sign_a != 0 && sign_b != 0 && sign_a == -sign_b); } else { std::cout << "new root: " << bqm.to_string(a) << "\n"; diff --git a/src/util/scoped_vector.h b/src/util/scoped_vector.h index bacfbac89..f62fbc8a6 100644 --- a/src/util/scoped_vector.h +++ b/src/util/scoped_vector.h @@ -91,6 +91,31 @@ public: SASSERT(invariant()); } + class iterator { + scoped_vector const& m_vec; + unsigned m_index; + public: + iterator(scoped_vector const& v, unsigned idx): m_vec(v), m_index(idx) {} + + bool operator==(iterator const& other) const { return &other.m_vec == &m_vec && other.m_index == m_index; } + bool operator!=(iterator const& other) const { return &other.m_vec != &m_vec || other.m_index != m_index; } + T const& operator*() { return m_vec[m_index]; } + + iterator & operator++() { + ++m_index; + return *this; + } + + iterator operator++(int) { + iterator r = *this; + ++m_index; + return r; + } + }; + + iterator begin() { return iterator(*this, 0); } + iterator end() { return iterator(*this, m_size); } + void push_back(T const& t) { set_index(m_size, m_elems.size()); m_elems.push_back(t); diff --git a/src/util/total_order.h b/src/util/total_order.h index 7238a5ef9..6fda88110 100644 --- a/src/util/total_order.h +++ b/src/util/total_order.h @@ -79,12 +79,7 @@ class total_order { } cell * to_cell(T const & a) const { - void * r; -#ifdef Z3DEBUG - bool ok = -#endif - m_map.find(a, r); - SASSERT(ok); + void * r = m_map.find(a); return reinterpret_cast(r); } diff --git a/src/util/uint_map.h b/src/util/uint_map.h index 13e0a9db3..0344de322 100644 --- a/src/util/uint_map.h +++ b/src/util/uint_map.h @@ -38,6 +38,11 @@ public: return v != 0; } } + + T * find(unsigned k) const { + SASSERT(k < m_map.size() && m_map[k] != 0); + return m_map[k]; + } void insert(unsigned k, T * v) { m_map.reserve(k+1);