From 53fc6ac11b25593e3827c943f5d61ce9f28da7ca Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 5 Oct 2017 14:27:56 +0100 Subject: [PATCH 01/27] [TravisCI] Refactor as many CI default options as possible so that the Docker and "TravisCI macOS" builds share most of the same defaults by sourcing the `ci_defaults.sh` file. --- contrib/ci/Dockerfiles/z3_build.Dockerfile | 50 ++++++++--------- contrib/ci/scripts/ci_defaults.sh | 54 +++++++++++++++++++ .../ci/scripts/travis_ci_linux_entry_point.sh | 4 +- .../ci/scripts/travis_ci_osx_entry_point.sh | 30 ++--------- 4 files changed, 86 insertions(+), 52 deletions(-) create mode 100644 contrib/ci/scripts/ci_defaults.sh diff --git a/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile index 2d16d5394..5f7608cf4 100644 --- a/contrib/ci/Dockerfiles/z3_build.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_build.Dockerfile @@ -2,34 +2,33 @@ ARG DOCKER_IMAGE_BASE FROM ${DOCKER_IMAGE_BASE} -# Specify defaults. This can be changed when invoking +# Build arguments. 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 ASAN_BUILD +ARG BUILD_DOCS +ARG CC +ARG CXX +ARG DOTNET_BINDINGS +ARG JAVA_BINDINGS +ARG NO_SUPPRESS_OUTPUT +ARG PYTHON_BINDINGS +ARG PYTHON_EXECUTABLE +ARG RUN_SYSTEM_TESTS +ARG RUN_UNIT_TESTS +ARG TARGET_ARCH +ARG TEST_INSTALL +ARG UBSAN_BUILD +ARG USE_LIBGMP +ARG USE_LTO +ARG USE_OPENMP 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_BUILD_TYPE +ARG Z3_CMAKE_GENERATOR +ARG Z3_INSTALL_PREFIX +ARG Z3_STATIC_BUILD ARG Z3_SYSTEM_TEST_GIT_REVISION -ARG Z3_WARNINGS_AS_ERRORS=SERIOUS_ONLY -ARG Z3_VERBOSE_BUILD_OUTPUT=0 +ARG Z3_WARNINGS_AS_ERRORS +ARG Z3_VERBOSE_BUILD_OUTPUT ENV \ ASAN_BUILD=${ASAN_BUILD} \ @@ -74,6 +73,7 @@ ADD *.txt *.md RELEASE_NOTES ${Z3_SRC_DIR}/ ADD \ /contrib/ci/scripts/build_z3_cmake.sh \ + /contrib/ci/scripts/ci_defaults.sh \ /contrib/ci/scripts/set_compiler_flags.sh \ /contrib/ci/scripts/set_generator_args.sh \ ${Z3_SRC_DIR}/contrib/ci/scripts/ diff --git a/contrib/ci/scripts/ci_defaults.sh b/contrib/ci/scripts/ci_defaults.sh new file mode 100644 index 000000000..354ea95b7 --- /dev/null +++ b/contrib/ci/scripts/ci_defaults.sh @@ -0,0 +1,54 @@ +# This file should be sourced by other scripts +# and not executed directly + +# Set CI build defaults + +export ASAN_BUILD="${ASAN_BUILD:-0}" +export BUILD_DOCS="${BUILD_DOCS:-0}" +export DOTNET_BINDINGS="${DOTNET_BINDINGS:-1}" +export JAVA_BINDINGS="${JAVA_BINDINGS:-1}" +export NO_SUPPRESS_OUTPUT="${NO_SUPPRESS_OUTPUT:-0}" +export PYTHON_BINDINGS="${PYTHON_BINDINGS:-1}" +export PYTHON_EXECUTABLE="${PYTHON_EXECUTABLE:-$(which python)}" +export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}" +export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-1}" +export TARGET_ARCH="${TARGET_ARCH:-x86_64}" +export TEST_INSTALL="${TEST_INSTALL:-1}" +export UBSAN_BUILD="${UBSAN_BUILD:-0}" +export USE_LIBGMP="${USE_LIBGMP:-0}" +export USE_LTO="${USE_LTO:-0}" +export USE_OPENMP="${USE_OPENMP:-1}" + +export Z3_BUILD_TYPE="${Z3_BUILD_TYPE:-RelWithDebInfo}" +export Z3_CMAKE_GENERATOR="${Z3_CMAKE_GENERATOR:-Ninja}" +export Z3_STATIC_BUILD="${Z3_STATIC_BUILD:-0}" +# Default is blank which means get latest revision +export Z3_SYSTEM_TEST_GIT_REVISION="${Z3_SYSTEM_TEST_GIT_REVISION:-}" +export Z3_WARNINGS_AS_ERRORS="${Z3_WARNINGS_AS_ERRORS:-SERIOUS_ONLY}" +export Z3_VERBOSE_BUILD_OUTPUT="${Z3_VERBOSE_BUILD_OUTPUT:-0}" + +# Platform specific defaults +PLATFORM="$(uname -s)" +case "${PLATFORM}" in + Linux*) + export C_COMPILER="${C_COMPILER:-gcc}" + export CXX_COMPILER="${CXX_COMPILER:-g++}" + export Z3_INSTALL_PREFIX="${Z3_INSTALL_PREFIX:-/usr}" + ;; + Darwin*) + export C_COMPILER="${C_COMPILER:-clang}" + export CXX_COMPILER="${CXX_COMPILER:-clang++}" + export Z3_INSTALL_PREFIX="${Z3_INSTALL_PREFIX:-/usr/local}" + ;; + *) + echo "Unknown platform \"${PLATFORM}\"" + exit 1 + ;; +esac +unset PLATFORM + +# NOTE: The following variables are not set here because +# they are specific to the CI implementation +# Z3_SRC_DIR +# Z3_BUILD_DIR +# Z3_SYSTEM_TEST_DIR diff --git a/contrib/ci/scripts/travis_ci_linux_entry_point.sh b/contrib/ci/scripts/travis_ci_linux_entry_point.sh index 84b2dd400..c0f856faa 100755 --- a/contrib/ci/scripts/travis_ci_linux_entry_point.sh +++ b/contrib/ci/scripts/travis_ci_linux_entry_point.sh @@ -11,13 +11,15 @@ 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 +# Get defaults +source "${SCRIPT_DIR}/ci_defaults.sh" + BUILD_OPTS=() # Override options if they have been provided. # Otherwise the defaults in the Docker file will be used diff --git a/contrib/ci/scripts/travis_ci_osx_entry_point.sh b/contrib/ci/scripts/travis_ci_osx_entry_point.sh index c5e8b4c02..7dd566877 100755 --- a/contrib/ci/scripts/travis_ci_osx_entry_point.sh +++ b/contrib/ci/scripts/travis_ci_osx_entry_point.sh @@ -6,26 +6,8 @@ set -x set -e set -o pipefail -# Set defaults -# FIXME: Refactor this so we don't need to stay in sync with -# `z3_build.Dockerfile`. -export ASAN_BUILD="${ASAN_BUILD:-0}" -export BUILD_DOCS="${BUILD_DOCS:-0}" -export C_COMPILER="${C_COMPILER:-clang}" -export CXX_COMPILER="${CXX_COMPILER:-clang++}" -export DOTNET_BINDINGS="${DOTNET_BINDINGS:-1}" -export JAVA_BINDINGS="${JAVA_BINDINGS:-1}" -export NO_SUPPRESS_OUTPUT="${NO_SUPPRESS_OUTPUT:-0}" -export PYTHON_BINDINGS="${PYTHON_BINDINGS:-1}" -export PYTHON_EXECUTABLE="$(which python)" -export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}" -export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-1}" -export TARGET_ARCH="${TARGET_ARCH:-x86_64}" -export TEST_INSTALL="${TEST_INSTALL:-1}" -export UBSAN_BUILD="${UBSAN_BUILD:-0}" -export USE_LIBGMP="${USE_LIBGMP:-0}" -export USE_LTO="${USE_LTO:-0}" -export USE_OPENMP="${USE_OPENMP:-1}" +# Get defaults +source "${SCRIPT_DIR}/ci_defaults.sh" if [ -z "${TRAVIS_BUILD_DIR}" ]; then echo "TRAVIS_BUILD_DIR must be set to root of Z3 repository" @@ -37,15 +19,11 @@ if [ ! -d "${TRAVIS_BUILD_DIR}" ]; then exit 1 fi +# These three variables are specific to the macOS TravisCI +# implementation and are not set in `ci_defaults.sh`. export Z3_SRC_DIR="${TRAVIS_BUILD_DIR}" export Z3_BUILD_DIR="${Z3_SRC_DIR}/build" -export Z3_BUILD_TYPE="${Z3_BUILD_TYPE:-RelWithDebInfo}" -export Z3_CMAKE_GENERATOR="${Z3_CMAKE_GENERATOR:-Ninja}" -export Z3_INSTALL_PREFIX="${Z3_INSTALL_PREFIX:-/usr/local}" -export Z3_STATIC_BUILD="${Z3_STATIC_BUILD:-0}" export Z3_SYSTEM_TEST_DIR="${Z3_SRC_DIR}/z3_system_test" -export Z3_WARNINGS_AS_ERRORS="${Z3_WARNINGS_AS_ERRORS:-SERIOUS_ONLY}" -export Z3_VERBOSE_BUILD_OUTPUT="${Z3_VERBOSE_BUILD_OUTPUT:-0}" # Overwrite whatever what set in TravisCI export CC="${C_COMPILER}" From eb975a49d606bcdb076b523d0506bf855ef8d267 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 5 Oct 2017 14:44:41 +0100 Subject: [PATCH 02/27] [TravisCI] Fix bug where `Z3_BUILD_TYPE` was not being passed as a Docker build argument. Also update an out of date comment. --- contrib/ci/scripts/travis_ci_linux_entry_point.sh | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/contrib/ci/scripts/travis_ci_linux_entry_point.sh b/contrib/ci/scripts/travis_ci_linux_entry_point.sh index c0f856faa..bd2c9d2d1 100755 --- a/contrib/ci/scripts/travis_ci_linux_entry_point.sh +++ b/contrib/ci/scripts/travis_ci_linux_entry_point.sh @@ -21,8 +21,11 @@ fi source "${SCRIPT_DIR}/ci_defaults.sh" BUILD_OPTS=() -# Override options if they have been provided. -# Otherwise the defaults in the Docker file will be used +# Pass Docker build arguments +if [ -n "${Z3_BUILD_TYPE}" ]; then + BUILD_OPTS+=("--build-arg" "Z3_BUILD_TYPE=${Z3_BUILD_TYPE}") +fi + if [ -n "${Z3_CMAKE_GENERATOR}" ]; then BUILD_OPTS+=("--build-arg" "Z3_CMAKE_GENERATOR=${Z3_CMAKE_GENERATOR}") fi From 0633d5819f8b996b3300f177efe6b1406a1285a5 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 5 Oct 2017 15:09:16 +0100 Subject: [PATCH 03/27] [TravisCI] Fix bug. `PYTHON_EXECUTABLE` should not be in common defaults. The location is dependent on the implementation. This triggered a build failure on TravisCI because the location of the default Python binary is different to what is in the Docker container. --- contrib/ci/Dockerfiles/z3_build.Dockerfile | 2 +- contrib/ci/scripts/ci_defaults.sh | 2 +- contrib/ci/scripts/travis_ci_osx_entry_point.sh | 3 ++- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile index 5f7608cf4..07504e6b9 100644 --- a/contrib/ci/Dockerfiles/z3_build.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_build.Dockerfile @@ -12,7 +12,7 @@ ARG DOTNET_BINDINGS ARG JAVA_BINDINGS ARG NO_SUPPRESS_OUTPUT ARG PYTHON_BINDINGS -ARG PYTHON_EXECUTABLE +ARG PYTHON_EXECUTABLE=/usr/bin/python2.7 ARG RUN_SYSTEM_TESTS ARG RUN_UNIT_TESTS ARG TARGET_ARCH diff --git a/contrib/ci/scripts/ci_defaults.sh b/contrib/ci/scripts/ci_defaults.sh index 354ea95b7..2fb3fa52a 100644 --- a/contrib/ci/scripts/ci_defaults.sh +++ b/contrib/ci/scripts/ci_defaults.sh @@ -9,7 +9,6 @@ export DOTNET_BINDINGS="${DOTNET_BINDINGS:-1}" export JAVA_BINDINGS="${JAVA_BINDINGS:-1}" export NO_SUPPRESS_OUTPUT="${NO_SUPPRESS_OUTPUT:-0}" export PYTHON_BINDINGS="${PYTHON_BINDINGS:-1}" -export PYTHON_EXECUTABLE="${PYTHON_EXECUTABLE:-$(which python)}" export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}" export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-1}" export TARGET_ARCH="${TARGET_ARCH:-x86_64}" @@ -49,6 +48,7 @@ unset PLATFORM # NOTE: The following variables are not set here because # they are specific to the CI implementation +# PYTHON_EXECUTABLE # Z3_SRC_DIR # Z3_BUILD_DIR # Z3_SYSTEM_TEST_DIR diff --git a/contrib/ci/scripts/travis_ci_osx_entry_point.sh b/contrib/ci/scripts/travis_ci_osx_entry_point.sh index 7dd566877..ad3b0c7ab 100755 --- a/contrib/ci/scripts/travis_ci_osx_entry_point.sh +++ b/contrib/ci/scripts/travis_ci_osx_entry_point.sh @@ -19,8 +19,9 @@ if [ ! -d "${TRAVIS_BUILD_DIR}" ]; then exit 1 fi -# These three variables are specific to the macOS TravisCI +# These variables are specific to the macOS TravisCI # implementation and are not set in `ci_defaults.sh`. +export PYTHON_EXECUTABLE="${PYTHON_EXECUTABLE:-$(which python)}" export Z3_SRC_DIR="${TRAVIS_BUILD_DIR}" export Z3_BUILD_DIR="${Z3_SRC_DIR}/build" export Z3_SYSTEM_TEST_DIR="${Z3_SRC_DIR}/z3_system_test" From d47aea398730634444bd31172fd2a04739a9efa7 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 6 Oct 2017 11:23:44 +0100 Subject: [PATCH 04/27] [TravisCI] Workaround slow unit test execution for Debug builds. Unit tests execute very slowly in Debug (i.e. unoptimized) builds. This causes TravisCI to terminate the job due to no console output being seen. To workaround this for the debug builds the tests are just compiled but not executed. To implement this the `RUN_UNIT_TESTS` environment variable now can take on the values `BUILD_ONLY`, `BUILD_AND_RUN`, and `SKIP` rather than `0` or `1`. --- .travis.yml | 11 ++++-- contrib/ci/README.md | 2 +- contrib/ci/scripts/ci_defaults.sh | 2 +- .../ci/scripts/test_z3_unit_tests_cmake.sh | 36 ++++++++++++++----- 4 files changed, 38 insertions(+), 13 deletions(-) diff --git a/.travis.yml b/.travis.yml index 50d63e593..ac00ef918 100644 --- a/.travis.yml +++ b/.travis.yml @@ -22,10 +22,17 @@ env: # 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 + # Debug builds + # + # Note the unit tests for the debug builds are compiled but **not** + # executed. This is because the debug build of unit tests takes a large + # amount of time to execute compared to the optimized builds. The hope is + # that just running the optimized unit tests is sufficient. + # # 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 + - 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 RUN_UNIT_TESTS=BUILD_ONLY # 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 + - 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 RUN_UNIT_TESTS=BUILD_ONLY # 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 diff --git a/contrib/ci/README.md b/contrib/ci/README.md index 2e117c8b1..e4c9aecfd 100644 --- a/contrib/ci/README.md +++ b/contrib/ci/README.md @@ -31,7 +31,7 @@ the future. * `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`) +* `RUN_UNIT_TESTS` - Run unit tests (`BUILD_ONLY` or `BUILD_AND_RUN` or `SKIP`) * `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`) diff --git a/contrib/ci/scripts/ci_defaults.sh b/contrib/ci/scripts/ci_defaults.sh index 2fb3fa52a..d8e9376d8 100644 --- a/contrib/ci/scripts/ci_defaults.sh +++ b/contrib/ci/scripts/ci_defaults.sh @@ -10,7 +10,7 @@ export JAVA_BINDINGS="${JAVA_BINDINGS:-1}" export NO_SUPPRESS_OUTPUT="${NO_SUPPRESS_OUTPUT:-0}" export PYTHON_BINDINGS="${PYTHON_BINDINGS:-1}" export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}" -export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-1}" +export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-BUILD_AND_RUN}" export TARGET_ARCH="${TARGET_ARCH:-x86_64}" export TEST_INSTALL="${TEST_INSTALL:-1}" export UBSAN_BUILD="${UBSAN_BUILD:-0}" diff --git a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh index 666673328..e1c927f58 100755 --- a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh +++ b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh @@ -10,17 +10,35 @@ 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[@]}" -# Run all tests that don't require arguments -run_quiet ./test-z3 /a +function build_unit_tests() { + # Build internal tests + cmake --build $(pwd) --target test-z3 "${GENERATOR_ARGS[@]}" +} + +function run_unit_tests() { + # Run all tests that don't require arguments + run_quiet ./test-z3 /a +} + +case "${RUN_UNIT_TESTS}" in + BUILD_AND_RUN) + build_unit_tests + run_unit_tests + ;; + BUILD_ONLY) + build_unit_tests + ;; + SKIP) + echo "RUN_UNIT_TESTS set to \"${RUN_UNIT_TESTS}\" so skipping build and run" + exit 0 + ;; + *) + echo "Error: RUN_UNIT_TESTS set to unhandled value \"${RUN_UNIT_TESTS}\"" + exit 1 + ;; +esac From 2519719d3f452eb2cbbaf0db822e58b671e4e74f Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 6 Oct 2017 11:30:06 +0100 Subject: [PATCH 05/27] Fix typo --- contrib/ci/scripts/set_generator_args.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/contrib/ci/scripts/set_generator_args.sh b/contrib/ci/scripts/set_generator_args.sh index 0ef7b76aa..a704c518b 100644 --- a/contrib/ci/scripts/set_generator_args.sh +++ b/contrib/ci/scripts/set_generator_args.sh @@ -1,4 +1,4 @@ -# This script should is intended to be included by other +# This script is intended to be included by other # scripts and should not be executed directly : ${Z3_CMAKE_GENERATOR?"Z3_CMAKE_GENERATOR must be specified"} From 0be28b66fe3319be01492a0391514727e099916c Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 6 Oct 2017 11:48:20 +0100 Subject: [PATCH 06/27] [TravisCI] Update out of date `README.md` file. --- contrib/ci/README.md | 46 ++++++++++++++++++++++++++++++++++++++------ 1 file changed, 40 insertions(+), 6 deletions(-) diff --git a/contrib/ci/README.md b/contrib/ci/README.md index e4c9aecfd..99bbcd7a6 100644 --- a/contrib/ci/README.md +++ b/contrib/ci/README.md @@ -58,8 +58,9 @@ The `scripts/travis_ci_linux_entry_point.sh` script 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`. +The default values of the configuration environment variables +can be found in +[`scripts/ci_defaults.sh`](scripts/ci_defaults.sh). #### Linux specific configuration variables @@ -67,8 +68,9 @@ found in `Dockerfiles/z3_build.Dockerfile`. #### 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. +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. @@ -104,11 +106,43 @@ 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. +image every time. An [organization](https://hub.docker.com/u/z3prover/) has been created on DockerHub for this. ### macOS -Not yet implemented. +For macOS we execute directly on TravisCI's macOS environment. The entry point +for the TravisCI builds is the +[`scripts/travis_ci_osx_entry_point.sh`](scripts/travis_ci_osx_entry_point.sh) +scripts. + +#### macOS specific configuration variables + +* `MACOS_SKIP_DEPS_UPDATE` - If set to `1` installing the necessary build dependencies + is skipped. This is useful for local testing if the dependencies are already installed. +* `MACOS_UPDATE_CMAKE` - If set to `1` the installed version of CMake will be upgraded. + +#### Reproducing a build locally + +To reproduce a build (e.g. like the one shown below) + +```yaml +- os: osx + osx_image: xcode8.3 + # Note: Apple Clang does not support OpenMP + env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0 +``` + +Run the following: + +```bash +TRAVIS_BUILD_DIR=$(pwd) \ +Z3_BUILD_TYPE=RelWithDebInfo \ +USE_OPEN_MP=0 \ +contrib/ci/scripts/travis_ci_osx_entry_point.sh +``` + +Note this assumes that the current working directory is the root of the Z3 +git repository. From 50042ab6388f5bd4bb7b8ba23622b96b7ef59131 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 6 Oct 2017 13:00:09 +0100 Subject: [PATCH 07/27] removed unused variables --- src/ast/fpa/fpa2bv_converter.cpp | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index f09ddcd42..13a7599a9 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1180,8 +1180,6 @@ void fpa2bv_converter::mk_abs(sort * s, expr_ref & x, expr_ref & result) { void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); - unsigned ebits = m_util.get_ebits(f->get_range()); - unsigned sbits = m_util.get_sbits(f->get_range()); expr * x = args[0], * y = args[1]; @@ -1227,8 +1225,6 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); - unsigned ebits = m_util.get_ebits(f->get_range()); - unsigned sbits = m_util.get_sbits(f->get_range()); expr * x = args[0], *y = args[1]; @@ -3081,8 +3077,6 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * mk_is_nan(x, x_is_nan); sort * fp_srt = m.get_sort(x); - unsigned ebits = m_util.get_ebits(fp_srt); - unsigned sbits = m_util.get_sbits(fp_srt); expr_ref unspec(m); mk_to_ieee_bv_unspecified(f, num, args, unspec); From 2634be01aa0c615e3b8b1362ce317f783b7109fc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Oct 2017 13:43:01 +0100 Subject: [PATCH 08/27] adding backwards pass Signed-off-by: Nikolaj Bjorner --- src/tactic/core/dom_simplify_tactic.cpp | 35 +++++++++++++++++-------- src/tactic/core/dom_simplify_tactic.h | 3 ++- 2 files changed, 26 insertions(+), 12 deletions(-) diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index d38324db9..da704bd0b 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -281,17 +281,28 @@ expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) { }; expr_ref_vector args(m); - for (expr * arg : *e) { - for (expr * child : tree(arg)) { - if (is_subexpr_arg(child, arg)) { - simplify(child); - } - } - r = simplify(arg); - args.push_back(r); - if (!assert_expr(simplify(arg), !is_and)) { - r = is_and ? m.mk_false() : m.mk_true(); - return r; + if (m_forward) { + for (expr * arg : *e) { +#define _SIMP_ARG(arg) \ + for (expr * child : tree(arg)) { \ + if (is_subexpr_arg(child, arg)) { \ + simplify(child); \ + } \ + } \ + r = simplify(arg); \ + args.push_back(r); \ + if (!assert_expr(simplify(arg), !is_and)) { \ + r = is_and ? m.mk_false() : m.mk_true(); \ + return r; \ + } + _SIMP_ARG(arg); + } + } + else { + for (unsigned i = e->get_num_args(); i > 0; ) { + --i; + expr* arg = e->get_arg(i); + _SIMP_ARG(arg); } } pop(scope_level() - old_lvl); @@ -319,6 +330,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) { change = false; // go forwards + m_forward = true; if (!init(g)) return; unsigned sz = g.size(); for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) { @@ -336,6 +348,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) { pop(scope_level()); // go backwards + m_forward = false; if (!init(g)) return; sz = g.size(); for (unsigned i = sz; !g.inconsistent() && i > 0; ) { diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index 6e5833cdb..581d40cd0 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -96,6 +96,7 @@ private: unsigned m_max_depth; ptr_vector m_empty; obj_pair_map m_subexpr_cache; + bool m_forward; expr_ref simplify(expr* t); expr_ref simplify_ite(app * ite); @@ -122,7 +123,7 @@ public: m(m), m_simplifier(s), m_params(p), m_trail(m), m_args(m), m_dominators(m), - m_scope_level(0), m_depth(0), m_max_depth(1024) {} + m_scope_level(0), m_depth(0), m_max_depth(1024), m_forward(true) {} virtual ~dom_simplify_tactic() {} From 9aa6386be94e96651b5c12065cb95a9e4dea74b8 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 6 Oct 2017 15:27:16 +0100 Subject: [PATCH 09/27] fix debug build --- src/util/lp/indexed_vector_instances.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/util/lp/indexed_vector_instances.cpp b/src/util/lp/indexed_vector_instances.cpp index ee078f021..79c3ee1a1 100644 --- a/src/util/lp/indexed_vector_instances.cpp +++ b/src/util/lp/indexed_vector_instances.cpp @@ -33,6 +33,7 @@ template void indexed_vector::resize(unsigned int); template void indexed_vector::set_value(const mpq&, unsigned int); template void indexed_vector::set_value(const unsigned&, unsigned int); #ifdef Z3DEBUG +template bool indexed_vector::is_OK() const; template bool indexed_vector::is_OK() const; template bool indexed_vector::is_OK() const; template bool indexed_vector >::is_OK() const; From ba8bff76ae9a68bef78c88913cbc2c62a193b299 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 6 Oct 2017 15:52:01 +0100 Subject: [PATCH 10/27] [TravisCI] Modify Debug configuration that I forgot to change with `RUN_UNIT_TESTS=BUILD_ONLY`. --- .travis.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index ac00ef918..81ddefb8b 100644 --- a/.travis.yml +++ b/.travis.yml @@ -64,7 +64,7 @@ env: # 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 + - 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 RUN_UNIT_TESTS=BUILD_ONLY # macOS (a.k.a OSX) support matrix: From c3f615dbfcf1436a142d1112598f358ed6c27bbd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Oct 2017 16:03:43 +0100 Subject: [PATCH 11/27] reverse arguments Signed-off-by: Nikolaj Bjorner --- src/tactic/core/dom_simplify_tactic.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index da704bd0b..67b039814 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -291,7 +291,7 @@ expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) { } \ r = simplify(arg); \ args.push_back(r); \ - if (!assert_expr(simplify(arg), !is_and)) { \ + if (!assert_expr(r, !is_and)) { \ r = is_and ? m.mk_false() : m.mk_true(); \ return r; \ } @@ -304,6 +304,7 @@ expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) { expr* arg = e->get_arg(i); _SIMP_ARG(arg); } + args.reverse(); } pop(scope_level() - old_lvl); r = is_and ? mk_and(args) : mk_or(args); @@ -338,6 +339,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) { if (i < sz - 1 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !g.proofs_enabled() && !assert_expr(r, false)) { r = m.mk_false(); } + CTRACE("simplify", r != g.form(i), tout << r << " " << mk_pp(g.form(i), m) << "\n";); change |= r != g.form(i); proof* new_pr = 0; if (g.proofs_enabled()) { @@ -358,6 +360,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) { r = m.mk_false(); } change |= r != g.form(i); + CTRACE("simplify", r != g.form(i), tout << r << " " << mk_pp(g.form(i), m) << "\n";); proof* new_pr = 0; if (g.proofs_enabled()) { new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(g.form(i), r, 0, 0)); From 31c6b3eb5b94053c8c40f2939ad429c31471edaa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Oct 2017 16:07:25 +0100 Subject: [PATCH 12/27] fix leak Signed-off-by: Nikolaj Bjorner --- src/tactic/core/dom_simplify_tactic.cpp | 4 ++++ src/tactic/core/dom_simplify_tactic.h | 4 +--- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 67b039814..99f83799b 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -152,6 +152,10 @@ void expr_dominators::reset() { // ----------------------- // dom_simplify_tactic +dom_simplify_tactic::~dom_simplify_tactic() { + dealloc(m_simplifier); +} + tactic * dom_simplify_tactic::translate(ast_manager & m) { return alloc(dom_simplify_tactic, m, m_simplifier->translate(m), m_params); } diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index 581d40cd0..c1660a941 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -83,8 +83,6 @@ class dom_simplifier { }; class dom_simplify_tactic : public tactic { -public: -private: ast_manager& m; dom_simplifier* m_simplifier; params_ref m_params; @@ -126,7 +124,7 @@ public: m_scope_level(0), m_depth(0), m_max_depth(1024), m_forward(true) {} - virtual ~dom_simplify_tactic() {} + virtual ~dom_simplify_tactic(); virtual tactic * translate(ast_manager & m); virtual void updt_params(params_ref const & p) {} From 1d12a9c86de07feafe1261fa52b8248fe1d494ef Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 6 Oct 2017 18:19:37 +0100 Subject: [PATCH 13/27] dom_simplifier: fix dominator computation --- src/tactic/core/dom_simplify_tactic.cpp | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 99f83799b..16d8500a4 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -95,17 +95,17 @@ bool expr_dominators::compute_dominators() { for (unsigned i = 0; i + 1 < m_post2expr.size(); ++i) { expr * child = m_post2expr[i]; ptr_vector const& p = m_parents[child]; - SASSERT(!p.empty()); expr * new_idom = 0, *idom2 = 0; - for (unsigned j = 0; j < p.size(); ++j) { - if (!new_idom) { - m_doms.find(p[j], new_idom); - } - else if (m_doms.find(p[j], idom2)) { - new_idom = intersect(new_idom, idom2); + for (auto& pred : p) { + if (m_doms.contains(pred)) { + new_idom = !new_idom ? pred : intersect(new_idom, pred); } } - if (new_idom && (!m_doms.find(child, idom2) || idom2 != new_idom)) { + if (!new_idom) { + m_doms.insert(child, p[0]); + change = true; + } + else if (!m_doms.find(child, idom2) || idom2 != new_idom) { m_doms.insert(child, new_idom); change = true; } From a18236bc7f2a9037ccd1d7d078cb54c132328474 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 7 Oct 2017 00:07:53 +0100 Subject: [PATCH 14/27] have quantifier equality take names into account Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 3 ++ src/ast/expr_abstract.cpp | 9 ++++ src/ast/expr_substitution.cpp | 7 +++ src/ast/expr_substitution.h | 3 ++ src/tactic/core/dom_simplify_tactic.cpp | 65 ++++++++++++++++++++----- src/tactic/core/dom_simplify_tactic.h | 5 +- 6 files changed, 78 insertions(+), 14 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index c98307ee0..cac12413e 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -471,6 +471,9 @@ bool compare_nodes(ast const * n1, ast const * n2) { compare_arrays(to_quantifier(n1)->get_decl_sorts(), to_quantifier(n2)->get_decl_sorts(), to_quantifier(n1)->get_num_decls()) && + compare_arrays(to_quantifier(n1)->get_decl_names(), + to_quantifier(n2)->get_decl_names(), + to_quantifier(n1)->get_num_decls()) && to_quantifier(n1)->get_expr() == to_quantifier(n2)->get_expr() && to_quantifier(n1)->get_weight() == to_quantifier(n2)->get_weight() && to_quantifier(n1)->get_num_patterns() == to_quantifier(n2)->get_num_patterns() && diff --git a/src/ast/expr_abstract.cpp b/src/ast/expr_abstract.cpp index 46682eed6..43035e203 100644 --- a/src/ast/expr_abstract.cpp +++ b/src/ast/expr_abstract.cpp @@ -19,6 +19,7 @@ Notes: #include "ast/expr_abstract.h" #include "util/map.h" +#include "ast/ast_pp.h" void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result) { @@ -109,6 +110,9 @@ void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const* void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result) { expr_abstractor abs(m); abs(base, num_bound, bound, n, result); + TRACE("expr_abstract", + tout << expr_ref(n, m) << "\n"; + tout << result << "\n";); } expr_ref mk_quantifier(bool is_forall, ast_manager& m, unsigned num_bound, app* const* bound, expr* n) { @@ -123,6 +127,11 @@ expr_ref mk_quantifier(bool is_forall, ast_manager& m, unsigned num_bound, app* } result = m.mk_quantifier(is_forall, num_bound, sorts.c_ptr(), names.c_ptr(), result); } + TRACE("expr_abstract", + tout << expr_ref(n, m) << "\n"; + for (unsigned i = 0; i < num_bound; ++i) tout << expr_ref(bound[i], m) << " "; + tout << "\n"; + tout << result << "\n";); return result; } diff --git a/src/ast/expr_substitution.cpp b/src/ast/expr_substitution.cpp index 149a59ce5..3ce038250 100644 --- a/src/ast/expr_substitution.cpp +++ b/src/ast/expr_substitution.cpp @@ -56,6 +56,13 @@ expr_substitution::~expr_substitution() { reset(); } +std::ostream& expr_substitution::display(std::ostream& out) { + for (auto & kv : m_subst) { + out << expr_ref(kv.m_key, m()) << " |-> " << expr_ref(kv.m_value, m()) << "\n"; + } + return out; +} + void expr_substitution::insert(expr * c, expr * def, proof * def_pr, expr_dependency * def_dep) { obj_map::obj_map_entry * entry = m_subst.insert_if_not_there2(c, 0); if (entry->get_data().m_value == 0) { diff --git a/src/ast/expr_substitution.h b/src/ast/expr_substitution.h index d360356eb..90154d163 100644 --- a/src/ast/expr_substitution.h +++ b/src/ast/expr_substitution.h @@ -50,6 +50,8 @@ public: bool contains(expr * s); void reset(); void cleanup(); + + std::ostream& display(std::ostream& out); }; class scoped_expr_substitution { @@ -84,6 +86,7 @@ public: bool find(expr * s, expr * & def, proof * & def_pr, expr_dependency * & def_dep) { return m_subst.find(s, def, def_pr, def_dep); } bool contains(expr * s) { return m_subst.contains(s); } void cleanup() { m_subst.cleanup(); } + std::ostream& display(std::ostream& out) { return m_subst.display(out); } }; #endif diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 99f83799b..60207e823 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -91,23 +91,42 @@ bool expr_dominators::compute_dominators() { unsigned iterations = 1; while (change) { change = false; + TRACE("simplify", + for (auto & kv : m_doms) { + tout << expr_ref(kv.m_key, m) << " |-> " << expr_ref(kv.m_value, m) << "\n"; + }); + SASSERT(m_post2expr.empty() || m_post2expr.back() == e); for (unsigned i = 0; i + 1 < m_post2expr.size(); ++i) { expr * child = m_post2expr[i]; ptr_vector const& p = m_parents[child]; SASSERT(!p.empty()); - expr * new_idom = 0, *idom2 = 0; - for (unsigned j = 0; j < p.size(); ++j) { - if (!new_idom) { - m_doms.find(p[j], new_idom); - } - else if (m_doms.find(p[j], idom2)) { - new_idom = intersect(new_idom, idom2); - } + if (p.size() == 1) { + if (!m_doms.contains(child)) { + m_doms.insert(child, p[0]); + change = true; + } } - if (new_idom && (!m_doms.find(child, idom2) || idom2 != new_idom)) { - m_doms.insert(child, new_idom); - change = true; + else { + expr * new_idom = 0, *idom2 = 0; + for (unsigned j = 0; j < p.size(); ++j) { + if (!new_idom) { + m_doms.find(p[j], new_idom); + } + else if (m_doms.find(p[j], idom2)) { + new_idom = intersect(new_idom, idom2); + } + } + if (!new_idom) { + m_doms.insert(child, p[0]); + TRACE("simplify", tout << expr_ref(child, m) << " |-> " << expr_ref(p[0], m) << "\n";); + change = true; + } + else if (!m_doms.find(child, idom2) || idom2 != new_idom) { + m_doms.insert(child, new_idom); + TRACE("simplify", tout << expr_ref(child, m) << " |-> " << expr_ref(new_idom, m) << "\n";); + change = true; + } } } iterations *= 2; @@ -130,6 +149,7 @@ bool expr_dominators::compile(expr * e) { compute_post_order(); if (!compute_dominators()) return false; extract_tree(); + TRACE("simplify", display(tout);); return true; } @@ -147,6 +167,22 @@ void expr_dominators::reset() { m_root.reset(); } +std::ostream& expr_dominators::display(std::ostream& out) { + return display(out, 0, m_root); +} + +std::ostream& expr_dominators::display(std::ostream& out, unsigned indent, expr* r) { + for (unsigned i = 0; i < indent; ++i) out << " "; + out << expr_ref(r, m); + if (m_tree.contains(r)) { + for (expr* child : m_tree[r]) { + if (child != r) + display(out, indent + 1, child); + } + } + out << "\n"; + return out; +} // ----------------------- @@ -200,7 +236,6 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) { simplify(child); } } - pop(scope_level() - old_lvl); expr_ref new_t = simplify(t); if (!assert_expr(new_c, true)) { @@ -230,6 +265,8 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) { expr_ref dom_simplify_tactic::simplify(expr * e0) { expr_ref r(m); expr* e = 0; + + TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";); if (!m_result.find(e0, e)) { e = e0; } @@ -254,7 +291,9 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) { if (is_app(e)) { m_args.reset(); for (expr* arg : *to_app(e)) { - m_args.push_back(get_cached(arg)); // TBD is cache really applied to all sub-terms? + r = get_cached(arg); + (*m_simplifier)(r); + m_args.push_back(r); } r = m.mk_app(to_app(e)->get_decl(), m_args.size(), m_args.c_ptr()); } diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index c1660a941..d99f799b4 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -48,6 +48,8 @@ private: bool compute_dominators(); void extract_tree(); + std::ostream& display(std::ostream& out, unsigned indent, expr* r); + public: expr_dominators(ast_manager& m): m(m), m_root(m) {} @@ -55,7 +57,8 @@ public: bool compile(unsigned sz, expr * const* es); tree_t const& get_tree() { return m_tree; } void reset(); - + + std::ostream& display(std::ostream& out); }; class dom_simplifier { From 76c309a595639cbbde974f8efe2b42f24a9d7e8f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 7 Oct 2017 00:20:58 +0100 Subject: [PATCH 15/27] disable caching of simplifier when applied to direct arguments of terms. Caching is only valid when applied to dominator children Signed-off-by: Nikolaj Bjorner --- src/tactic/core/dom_simplify_tactic.cpp | 31 +++++++++++++------------ src/tactic/core/dom_simplify_tactic.h | 2 +- 2 files changed, 17 insertions(+), 16 deletions(-) diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 830d44c7a..1bd685bb1 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -101,7 +101,8 @@ bool expr_dominators::compute_dominators() { expr * child = m_post2expr[i]; ptr_vector const& p = m_parents[child]; expr * new_idom = 0, *idom2 = 0; - for (auto& pred : p) { + + for (expr * pred : p) { if (m_doms.contains(pred)) { new_idom = !new_idom ? pred : intersect(new_idom, pred); } @@ -209,31 +210,31 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) { expr * c = 0, *t = 0, *e = 0; VERIFY(m.is_ite(ite, c, t, e)); unsigned old_lvl = scope_level(); - expr_ref new_c = simplify(c); + expr_ref new_c = simplify(c, false); if (m.is_true(new_c)) { - r = simplify(t); + r = simplify(t, false); } else if (m.is_false(new_c) || !assert_expr(new_c, false)) { - r = simplify(e); + r = simplify(e, false); } else { for (expr * child : tree(ite)) { if (is_subexpr(child, t) && !is_subexpr(child, e)) { - simplify(child); + simplify(child, true); } } pop(scope_level() - old_lvl); - expr_ref new_t = simplify(t); + expr_ref new_t = simplify(t, false); if (!assert_expr(new_c, true)) { return new_t; } for (expr * child : tree(ite)) { if (is_subexpr(child, e) && !is_subexpr(child, t)) { - simplify(child); + simplify(child, true); } } pop(scope_level() - old_lvl); - expr_ref new_e = simplify(e); + expr_ref new_e = simplify(e, false); if (c == new_c && t == new_t && e == new_e) { r = ite; } @@ -248,7 +249,7 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) { return r; } -expr_ref dom_simplify_tactic::simplify(expr * e0) { +expr_ref dom_simplify_tactic::simplify(expr * e0, bool cache_result) { expr_ref r(m); expr* e = 0; @@ -272,7 +273,7 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) { } else { for (expr * child : tree(e)) { - simplify(child); + simplify(child, true); } if (is_app(e)) { m_args.reset(); @@ -288,7 +289,7 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) { } } (*m_simplifier)(r); - cache(e0, r); + if (cache_result) cache(e0, r); TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";); --m_depth; m_subexpr_cache.reset(); @@ -315,10 +316,10 @@ expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) { #define _SIMP_ARG(arg) \ for (expr * child : tree(arg)) { \ if (is_subexpr_arg(child, arg)) { \ - simplify(child); \ + simplify(child, true); \ } \ } \ - r = simplify(arg); \ + r = simplify(arg, false); \ args.push_back(r); \ if (!assert_expr(r, !is_and)) { \ r = is_and ? m.mk_false() : m.mk_true(); \ @@ -364,7 +365,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) { if (!init(g)) return; unsigned sz = g.size(); for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) { - expr_ref r = simplify(g.form(i)); + expr_ref r = simplify(g.form(i), true); if (i < sz - 1 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !g.proofs_enabled() && !assert_expr(r, false)) { r = m.mk_false(); } @@ -384,7 +385,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) { sz = g.size(); for (unsigned i = sz; !g.inconsistent() && i > 0; ) { --i; - expr_ref r = simplify(g.form(i)); + expr_ref r = simplify(g.form(i), true); if (i > 0 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !g.proofs_enabled() && !assert_expr(r, false)) { r = m.mk_false(); } diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index d99f799b4..e79777215 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -99,7 +99,7 @@ class dom_simplify_tactic : public tactic { obj_pair_map m_subexpr_cache; bool m_forward; - expr_ref simplify(expr* t); + expr_ref simplify(expr* t, bool cache); expr_ref simplify_ite(app * ite); expr_ref simplify_and(app * ite) { return simplify_and_or(true, ite); } expr_ref simplify_or(app * ite) { return simplify_and_or(false, ite); } From 7e4f5322023ddf5d1a4ae485d710c4f8c59a65f6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 7 Oct 2017 00:37:44 +0100 Subject: [PATCH 16/27] fix build by including mk_pp Signed-off-by: Nikolaj Bjorner --- src/ast/expr_substitution.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/ast/expr_substitution.cpp b/src/ast/expr_substitution.cpp index 3ce038250..f9333c443 100644 --- a/src/ast/expr_substitution.cpp +++ b/src/ast/expr_substitution.cpp @@ -16,8 +16,9 @@ Author: Notes: --*/ -#include "ast/expr_substitution.h" #include "util/ref_util.h" +#include "ast/expr_substitution.h" +#include "ast/ast_pp.h" typedef obj_map expr2proof; typedef obj_map expr2expr_dependency; @@ -58,7 +59,7 @@ expr_substitution::~expr_substitution() { std::ostream& expr_substitution::display(std::ostream& out) { for (auto & kv : m_subst) { - out << expr_ref(kv.m_key, m()) << " |-> " << expr_ref(kv.m_value, m()) << "\n"; + out << mk_pp(kv.m_key, m()) << " |-> " << mk_pp(kv.m_value, m()) << "\n"; } return out; } From b898b077953c8e4a18d9b49567af37952e889eb8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 7 Oct 2017 11:12:09 +0100 Subject: [PATCH 17/27] distinguish simplify_rec from simplify immediate argument Signed-off-by: Nikolaj Bjorner --- src/tactic/core/dom_simplify_tactic.cpp | 40 ++++++++++++++----------- src/tactic/core/dom_simplify_tactic.h | 3 +- 2 files changed, 25 insertions(+), 18 deletions(-) diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 1bd685bb1..366e1edb0 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -210,31 +210,31 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) { expr * c = 0, *t = 0, *e = 0; VERIFY(m.is_ite(ite, c, t, e)); unsigned old_lvl = scope_level(); - expr_ref new_c = simplify(c, false); + expr_ref new_c = simplify_arg(c); if (m.is_true(new_c)) { - r = simplify(t, false); + r = simplify_arg(t); } else if (m.is_false(new_c) || !assert_expr(new_c, false)) { - r = simplify(e, false); + r = simplify_arg(e); } else { for (expr * child : tree(ite)) { if (is_subexpr(child, t) && !is_subexpr(child, e)) { - simplify(child, true); + simplify_rec(child); } } pop(scope_level() - old_lvl); - expr_ref new_t = simplify(t, false); + expr_ref new_t = simplify_arg(t); if (!assert_expr(new_c, true)) { return new_t; } for (expr * child : tree(ite)) { if (is_subexpr(child, e) && !is_subexpr(child, t)) { - simplify(child, true); + simplify_rec(child); } } pop(scope_level() - old_lvl); - expr_ref new_e = simplify(e, false); + expr_ref new_e = simplify_arg(e); if (c == new_c && t == new_t && e == new_e) { r = ite; } @@ -249,7 +249,15 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) { return r; } -expr_ref dom_simplify_tactic::simplify(expr * e0, bool cache_result) { +expr_ref dom_simplify_tactic::simplify_arg(expr * e) { + expr_ref r(m); + r = get_cached(e); + (*m_simplifier)(r); + TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e, m) << " -> " << r << "\n";); + return r; +} + +expr_ref dom_simplify_tactic::simplify_rec(expr * e0) { expr_ref r(m); expr* e = 0; @@ -273,14 +281,12 @@ expr_ref dom_simplify_tactic::simplify(expr * e0, bool cache_result) { } else { for (expr * child : tree(e)) { - simplify(child, true); + simplify_rec(child); } if (is_app(e)) { m_args.reset(); for (expr* arg : *to_app(e)) { - r = get_cached(arg); - (*m_simplifier)(r); - m_args.push_back(r); + m_args.push_back(simplify_arg(arg)); } r = m.mk_app(to_app(e)->get_decl(), m_args.size(), m_args.c_ptr()); } @@ -289,7 +295,7 @@ expr_ref dom_simplify_tactic::simplify(expr * e0, bool cache_result) { } } (*m_simplifier)(r); - if (cache_result) cache(e0, r); + cache(e0, r); TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";); --m_depth; m_subexpr_cache.reset(); @@ -316,10 +322,10 @@ expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) { #define _SIMP_ARG(arg) \ for (expr * child : tree(arg)) { \ if (is_subexpr_arg(child, arg)) { \ - simplify(child, true); \ + simplify_rec(child); \ } \ } \ - r = simplify(arg, false); \ + r = simplify_arg(arg); \ args.push_back(r); \ if (!assert_expr(r, !is_and)) { \ r = is_and ? m.mk_false() : m.mk_true(); \ @@ -365,7 +371,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) { if (!init(g)) return; unsigned sz = g.size(); for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) { - expr_ref r = simplify(g.form(i), true); + expr_ref r = simplify_rec(g.form(i)); if (i < sz - 1 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !g.proofs_enabled() && !assert_expr(r, false)) { r = m.mk_false(); } @@ -385,7 +391,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) { sz = g.size(); for (unsigned i = sz; !g.inconsistent() && i > 0; ) { --i; - expr_ref r = simplify(g.form(i), true); + expr_ref r = simplify_rec(g.form(i)); if (i > 0 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !g.proofs_enabled() && !assert_expr(r, false)) { r = m.mk_false(); } diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index e79777215..4f9851514 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -99,7 +99,8 @@ class dom_simplify_tactic : public tactic { obj_pair_map m_subexpr_cache; bool m_forward; - expr_ref simplify(expr* t, bool cache); + expr_ref simplify_rec(expr* t); + expr_ref simplify_arg(expr* t); expr_ref simplify_ite(app * ite); expr_ref simplify_and(app * ite) { return simplify_and_or(true, ite); } expr_ref simplify_or(app * ite) { return simplify_and_or(false, ite); } From deba7d4d6e74c2896b2f75aeeacc205618157f05 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 7 Oct 2017 14:35:44 +0100 Subject: [PATCH 18/27] use idom for checking dominator relationships Signed-off-by: Nikolaj Bjorner --- src/tactic/core/dom_simplify_tactic.cpp | 24 ++++++++++++++++-------- src/tactic/core/dom_simplify_tactic.h | 2 ++ 2 files changed, 18 insertions(+), 8 deletions(-) diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 366e1edb0..3a6d55569 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -257,11 +257,14 @@ expr_ref dom_simplify_tactic::simplify_arg(expr * e) { return r; } +/** + \brief simplify e recursively. +*/ expr_ref dom_simplify_tactic::simplify_rec(expr * e0) { expr_ref r(m); expr* e = 0; - TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";); + TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << "\n";); if (!m_result.find(e0, e)) { e = e0; } @@ -408,6 +411,12 @@ void dom_simplify_tactic::simplify_goal(goal& g) { SASSERT(scope_level() == 0); } +/** + \brief determine if a is dominated by b. + Walk the immediate dominators of a upwards until hitting b or a term that is deeper than b. + Save intermediary results in a cache to avoid recomputations. +*/ + bool dom_simplify_tactic::is_subexpr(expr * a, expr * b) { if (a == b) return true; @@ -416,14 +425,13 @@ bool dom_simplify_tactic::is_subexpr(expr * a, expr * b) { if (m_subexpr_cache.find(a, b, r)) return r; - for (expr * e : tree(b)) { - if (is_subexpr(a, e)) { - m_subexpr_cache.insert(a, b, true); - return true; - } + if (get_depth(a) >= get_depth(b)) { + return false; } - m_subexpr_cache.insert(a, b, false); - return false; + SASSERT(a != idom(a) && get_depth(idom(a)) > get_depth(a)); + r = is_subexpr(idom(a), b); + m_subexpr_cache.insert(a, b, r); + return r; } ptr_vector const & dom_simplify_tactic::tree(expr * e) { diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index 4f9851514..79bc9728c 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -57,6 +57,7 @@ public: bool compile(unsigned sz, expr * const* es); tree_t const& get_tree() { return m_tree; } void reset(); + expr* idom(expr *e) const { return m_doms[e]; } std::ostream& display(std::ostream& out); }; @@ -113,6 +114,7 @@ class dom_simplify_tactic : public tactic { void cache(expr *t, expr* r) { m_result.insert(t, r); m_trail.push_back(r); } ptr_vector const & tree(expr * e); + expr* idom(expr *e) const { return m_dominators.idom(e); } unsigned scope_level() { return m_scope_level; } void pop(unsigned n) { SASSERT(n <= m_scope_level); m_scope_level -= n; m_simplifier->pop(n); } From a5ecf87ab82c86b01eef01646b70fdcbb30b1f5d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Oct 2017 10:32:38 +0100 Subject: [PATCH 19/27] fix #1288 Signed-off-by: Nikolaj Bjorner --- src/muz/rel/tbv.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp index 7475750db..69cc4819a 100644 --- a/src/muz/rel/tbv.cpp +++ b/src/muz/rel/tbv.cpp @@ -74,8 +74,7 @@ tbv* tbv_manager::allocate(tbv const& bv) { } tbv* tbv_manager::allocate(uint64 val) { tbv* v = allocate0(); - for (unsigned bit = num_tbits(); bit > 0;) { - --bit; + for (unsigned bit = std::min(64u, num_tbits()); bit-- > 0;) { if (val & (1ULL << bit)) { set(*v, bit, BIT_1); } else { From 6f7f957a266d8a22f628aaee29303ac650529f73 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Oct 2017 10:38:02 +0100 Subject: [PATCH 20/27] likely fix for #1287 Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 8938fb1b5..41f3f0e06 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -140,7 +140,7 @@ namespace z3 { class context { bool m_enable_exceptions; Z3_context m_ctx; - static void error_handler(Z3_context /*c*/, Z3_error_code /*e*/) { /* do nothing */ } + static void __cdecl error_handler(Z3_context /*c*/, Z3_error_code /*e*/) { /* do nothing */ } void init(config & c) { m_ctx = Z3_mk_context_rc(c); m_enable_exceptions = true; From c72b3356c16778fe21223f374f7679c1c0664e65 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Oct 2017 10:41:02 +0100 Subject: [PATCH 21/27] fix #1286 Signed-off-by: Nikolaj Bjorner --- src/interp/iz3mgr.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 6ca8fae34..e4c294059 100755 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -96,7 +96,7 @@ class ast_r : public ast_i { ast_r(const ast_r &other) : ast_i(other) { _m = other._m; - _m->inc_ref(_ast); + if (_m) _m->inc_ref(_ast); } ast_r &operator=(const ast_r &other) { @@ -104,7 +104,7 @@ class ast_r : public ast_i { _m->dec_ref(_ast); _ast = other._ast; _m = other._m; - _m->inc_ref(_ast); + if (_m) _m->inc_ref(_ast); return *this; } From 52217f0600aaa2b2961f971d8648b8e3c7bf4f2f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Oct 2017 10:56:05 +0100 Subject: [PATCH 22/27] fix #1290 Signed-off-by: Nikolaj Bjorner --- src/model/model_core.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index f94558097..4290700d4 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -86,18 +86,18 @@ void model_core::register_decl(func_decl * d, func_interp * fi) { void model_core::unregister_decl(func_decl * d) { decl2expr::obj_map_entry * ec = m_interp.find_core(d); if (ec && ec->get_data().m_value != 0) { - m_manager.dec_ref(ec->get_data().m_key); - m_manager.dec_ref(ec->get_data().m_value); m_interp.remove(d); m_const_decls.erase(d); + m_manager.dec_ref(ec->get_data().m_key); + m_manager.dec_ref(ec->get_data().m_value); return; } decl2finterp::obj_map_entry * ef = m_finterp.find_core(d); if (ef && ef->get_data().m_value != 0) { - m_manager.dec_ref(ef->get_data().m_key); - dealloc(ef->get_data().m_value); m_finterp.remove(d); m_func_decls.erase(d); + m_manager.dec_ref(ef->get_data().m_key); + dealloc(ef->get_data().m_value); } } From 1371caace28097b8d86ba4cd47be22492d419784 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Oct 2017 11:05:57 +0100 Subject: [PATCH 23/27] fix #1287, again Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 41f3f0e06..2200874d3 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -140,7 +140,7 @@ namespace z3 { class context { bool m_enable_exceptions; Z3_context m_ctx; - static void __cdecl error_handler(Z3_context /*c*/, Z3_error_code /*e*/) { /* do nothing */ } + static void Z3_API error_handler(Z3_context /*c*/, Z3_error_code /*e*/) { /* do nothing */ } void init(config & c) { m_ctx = Z3_mk_context_rc(c); m_enable_exceptions = true; From 22fa108ffd91834eb5b4a98a3e14434750b7b8f5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Oct 2017 11:07:22 +0100 Subject: [PATCH 24/27] fix #1288, again Signed-off-by: Nikolaj Bjorner --- src/muz/rel/tbv.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp index 69cc4819a..5ef15303e 100644 --- a/src/muz/rel/tbv.cpp +++ b/src/muz/rel/tbv.cpp @@ -74,7 +74,7 @@ tbv* tbv_manager::allocate(tbv const& bv) { } tbv* tbv_manager::allocate(uint64 val) { tbv* v = allocate0(); - for (unsigned bit = std::min(64u, num_tbits()); bit-- > 0;) { + for (unsigned bit = std::min(63u, num_tbits()); bit-- > 0;) { if (val & (1ULL << bit)) { set(*v, bit, BIT_1); } else { From 06d75a616f6246eaa717ca34bb2719726d6858d7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Oct 2017 11:40:17 +0100 Subject: [PATCH 25/27] fix #1288, again Signed-off-by: Nikolaj Bjorner --- src/muz/rel/tbv.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp index 5ef15303e..69cc4819a 100644 --- a/src/muz/rel/tbv.cpp +++ b/src/muz/rel/tbv.cpp @@ -74,7 +74,7 @@ tbv* tbv_manager::allocate(tbv const& bv) { } tbv* tbv_manager::allocate(uint64 val) { tbv* v = allocate0(); - for (unsigned bit = std::min(63u, num_tbits()); bit-- > 0;) { + for (unsigned bit = std::min(64u, num_tbits()); bit-- > 0;) { if (val & (1ULL << bit)) { set(*v, bit, BIT_1); } else { From d2ec927844120a4c26236e80b9bd8ae302de51f3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Oct 2017 12:34:08 +0100 Subject: [PATCH 26/27] fix build break Signed-off-by: Nikolaj Bjorner --- src/model/model_core.cpp | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index 4290700d4..833c254c3 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -86,18 +86,22 @@ void model_core::register_decl(func_decl * d, func_interp * fi) { void model_core::unregister_decl(func_decl * d) { decl2expr::obj_map_entry * ec = m_interp.find_core(d); if (ec && ec->get_data().m_value != 0) { + auto k = ec->get_data().m_key; + auto v = ec->get_data().m_value; m_interp.remove(d); m_const_decls.erase(d); - m_manager.dec_ref(ec->get_data().m_key); - m_manager.dec_ref(ec->get_data().m_value); + m_manager.dec_ref(k); + m_manager.dec_ref(v); return; } decl2finterp::obj_map_entry * ef = m_finterp.find_core(d); if (ef && ef->get_data().m_value != 0) { + auto k = ef->get_data().m_key; + auto v = ef->get_data().m_value; m_finterp.remove(d); m_func_decls.erase(d); - m_manager.dec_ref(ef->get_data().m_key); - dealloc(ef->get_data().m_value); + m_manager.dec_ref(k); + dealloc(v); } } From f359f238851d8c1a5db11a95d4ded3639813db9a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Oct 2017 15:47:06 -0700 Subject: [PATCH 27/27] another fix for #1288 Signed-off-by: Nikolaj Bjorner --- src/util/mpz.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 9569ac280..7cf87b24b 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -558,14 +558,13 @@ void mpz_manager::big_rem(mpz const & a, mpz const & b, mpz & c) { template void mpz_manager::gcd(mpz const & a, mpz const & b, mpz & c) { - if (is_small(a) && is_small(b)) { + COMPILE_TIME_ASSERT(sizeof(a.m_val) == sizeof(int)); + if (is_small(a) && is_small(b) && a.m_val != INT_MIN && b.m_val != INT_MIN) { int _a = a.m_val; int _b = b.m_val; if (_a < 0) _a = -_a; if (_b < 0) _b = -_b; unsigned r = u_gcd(_a, _b); - // Remark: r is (INT_MAX + 1) - // If a == b == INT_MIN set(c, r); } else {