diff --git a/.travis.yml b/.travis.yml index 50d63e593..81ddefb8b 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 @@ -57,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: diff --git a/README.md b/README.md index 197928877..701556cc8 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 | 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) +| Windows x86 | Windows x64 | Ubuntu x64 | 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) | [![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/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile index 2d16d5394..07504e6b9 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 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=/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 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/README.md b/contrib/ci/README.md index 2e117c8b1..99bbcd7a6 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`) @@ -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. diff --git a/contrib/ci/scripts/ci_defaults.sh b/contrib/ci/scripts/ci_defaults.sh new file mode 100644 index 000000000..d8e9376d8 --- /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 RUN_SYSTEM_TESTS="${RUN_SYSTEM_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}" +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 +# PYTHON_EXECUTABLE +# Z3_SRC_DIR +# Z3_BUILD_DIR +# Z3_SYSTEM_TEST_DIR 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"} 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 diff --git a/contrib/ci/scripts/travis_ci_linux_entry_point.sh b/contrib/ci/scripts/travis_ci_linux_entry_point.sh index 84b2dd400..bd2c9d2d1 100755 --- a/contrib/ci/scripts/travis_ci_linux_entry_point.sh +++ b/contrib/ci/scripts/travis_ci_linux_entry_point.sh @@ -11,16 +11,21 @@ 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 +# 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 diff --git a/contrib/ci/scripts/travis_ci_osx_entry_point.sh b/contrib/ci/scripts/travis_ci_osx_entry_point.sh index c5e8b4c02..ad3b0c7ab 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,12 @@ if [ ! -d "${TRAVIS_BUILD_DIR}" ]; then exit 1 fi +# 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_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}" diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index 234dd670c..ab4d32d39 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -188,7 +188,7 @@ try: if Z3PY_ENABLED: print("Z3Py documentation enabled") - doxygen_config_substitutions['PYTHON_API_FILES'] = 'z3.py' + doxygen_config_substitutions['PYTHON_API_FILES'] = 'z3*.py' else: print("Z3Py documentation disabled") doxygen_config_substitutions['PYTHON_API_FILES'] = '' @@ -288,8 +288,21 @@ try: # Put z3py at the beginning of the search path to try to avoid picking up # an installed copy of Z3py. sys.path.insert(0, os.path.dirname(Z3PY_PACKAGE_PATH)) - pydoc.writedoc('z3') - shutil.move('z3.html', os.path.join(OUTPUT_DIRECTORY, 'html', 'z3.html')) + for modulename in ( + 'z3', + 'z3.z3consts', + 'z3.z3core', + 'z3.z3num', + 'z3.z3poly', + 'z3.z3printer', + 'z3.z3rcf', + 'z3.z3types', + 'z3.z3util', + ): + pydoc.writedoc(modulename) + doc = modulename + '.html' + shutil.move(doc, os.path.join(OUTPUT_DIRECTORY, 'html', doc)) + print("Generated pydoc Z3Py documentation.") if ML_ENABLED: diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index 56b402ad5..62aac110d 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -65,6 +65,15 @@ void throw_z3_error(Z3_context c, Z3_error_code e) longjmp(g_catch_buffer, e); } +/** + \brief Error handling that depends on checking an error code on the context. + +*/ + +void nothrow_z3_error(Z3_context c, Z3_error_code e) { + // no-op +} + /** \brief Create a logical context. @@ -1592,18 +1601,16 @@ void error_code_example1() void error_code_example2() { Z3_config cfg; Z3_context ctx = NULL; - int r; + Z3_error_code e; printf("\nerror_code_example2\n"); LOG_MSG("error_code_example2"); - /* low tech try&catch */ - r = setjmp(g_catch_buffer); - if (r == 0) { + if (1) { Z3_ast x, y, app; cfg = Z3_mk_config(); - ctx = mk_context_custom(cfg, throw_z3_error); + ctx = mk_context_custom(cfg, nothrow_z3_error); Z3_del_config(cfg); x = mk_int_var(ctx, "x"); @@ -1611,11 +1618,14 @@ void error_code_example2() { printf("before Z3_mk_iff\n"); /* the next call will produce an error */ app = Z3_mk_iff(ctx, x, y); + e = Z3_get_error_code(ctx); + if (e != Z3_OK) goto err; unreachable(); Z3_del_context(ctx); } else { - printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, (Z3_error_code)r)); + err: + printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, e)); if (ctx != NULL) { Z3_del_context(ctx); } @@ -1781,15 +1791,14 @@ void parser_example5() { Z3_config cfg; Z3_context ctx = NULL; Z3_solver s = NULL; - int r; + Z3_error_code e; printf("\nparser_example5\n"); LOG_MSG("parser_example5"); - r = setjmp(g_catch_buffer); - if (r == 0) { + if (1) { cfg = Z3_mk_config(); - ctx = mk_context_custom(cfg, throw_z3_error); + ctx = mk_context_custom(cfg, nothrow_z3_error); s = mk_solver(ctx); Z3_del_config(cfg); @@ -1798,12 +1807,15 @@ void parser_example5() { "(benchmark tst :extrafuns ((x Int (y Int)) :formula (> x y) :formula (> x 0))", 0, 0, 0, 0, 0, 0); + e = Z3_get_error_code(ctx); + if (e != Z3_OK) goto err; unreachable(); del_solver(ctx, s); Z3_del_context(ctx); } else { - printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, (Z3_error_code)r)); + err: + printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, e)); if (ctx != NULL) { printf("Error message: '%s'.\n",Z3_get_smtlib_error(ctx)); del_solver(ctx, s); diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 520ba3d91..305395833 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1913,7 +1913,11 @@ class MLComponent(Component): src_dir = self.to_src_dir mk_dir(os.path.join(BUILD_DIR, self.sub_dir)) api_src = get_component(API_COMPONENT).to_src_dir - out.write('CXXFLAGS_OCAML=$(CXXFLAGS:/GL=)\n') # remove /GL; the ocaml tools don't like it. + # remove /GL and -std=c++11; the ocaml tools don't like them. + if IS_WINDOWS: + out.write('CXXFLAGS_OCAML=$(CXXFLAGS:/GL=)\n') + else: + out.write('CXXFLAGS_OCAML=$(subst -std=c++11,,$(CXXFLAGS))\n') if IS_WINDOWS: prefix_lib = '-L' + os.path.abspath(BUILD_DIR).replace('\\', '\\\\') diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index f402f18c9..7641bd7c6 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -57,19 +57,20 @@ extern "C" { Z3_func_decl const decls[]) { Z3_TRY; LOG_Z3_parse_smtlib_string(c, str, num_sorts, sort_names, sorts, num_decls, decl_names, decls); - std::ostringstream outs; + std::ostringstream* outs = alloc(std::ostringstream); bool ok = false; RESET_ERROR_CODE(); init_smtlib_parser(c, num_sorts, sort_names, sorts, num_decls, decl_names, decls); - mk_c(c)->m_smtlib_parser->set_error_stream(outs); + mk_c(c)->m_smtlib_parser->set_error_stream(*outs); try { ok = mk_c(c)->m_smtlib_parser->parse_string(str); } catch (...) { ok = false; } - mk_c(c)->m_smtlib_error_buffer = outs.str(); + mk_c(c)->m_smtlib_error_buffer = outs->str(); + dealloc(outs); if (!ok) { mk_c(c)->reset_parser(); SET_ERROR_CODE(Z3_PARSER_ERROR); @@ -89,16 +90,17 @@ extern "C" { LOG_Z3_parse_smtlib_file(c, file_name, num_sorts, sort_names, types, num_decls, decl_names, decls); bool ok = false; RESET_ERROR_CODE(); - std::ostringstream outs; + std::ostringstream* outs = alloc(std::ostringstream); init_smtlib_parser(c, num_sorts, sort_names, types, num_decls, decl_names, decls); - mk_c(c)->m_smtlib_parser->set_error_stream(outs); + mk_c(c)->m_smtlib_parser->set_error_stream(*outs); try { ok = mk_c(c)->m_smtlib_parser->parse_file(file_name); } catch(...) { ok = false; } - mk_c(c)->m_smtlib_error_buffer = outs.str(); + mk_c(c)->m_smtlib_error_buffer = outs->str(); + dealloc(outs); if (!ok) { mk_c(c)->reset_parser(); SET_ERROR_CODE(Z3_PARSER_ERROR); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index d09129d37..eb38c5fa5 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 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; 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..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; @@ -56,6 +57,13 @@ expr_substitution::~expr_substitution() { reset(); } +std::ostream& expr_substitution::display(std::ostream& out) { + for (auto & kv : m_subst) { + out << mk_pp(kv.m_key, m()) << " |-> " << mk_pp(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/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); diff --git a/src/ast/rewriter/maximize_ac_sharing.cpp b/src/ast/rewriter/maximize_ac_sharing.cpp index b560132db..a838f59fa 100644 --- a/src/ast/rewriter/maximize_ac_sharing.cpp +++ b/src/ast/rewriter/maximize_ac_sharing.cpp @@ -54,13 +54,13 @@ br_status maximize_ac_sharing::reduce_app(func_decl * f, unsigned num_args, expr TRACE("ac_sharing_detail", tout << "args: "; for (unsigned i = 0; i < num_args; i++) tout << mk_pp(_args[i], m) << "\n";); try_to_reuse: if (num_args > 1 && num_args < MAX_NUM_ARGS_FOR_OPT) { - for (unsigned i = 0; i < num_args - 1; i++) { + for (unsigned i = 0; i + 1 < num_args; i++) { for (unsigned j = i + 1; j < num_args; j++) { if (contains(f, _args[i], _args[j])) { TRACE("ac_sharing_detail", tout << "reusing args: " << i << " " << j << "\n";); _args[i] = m.mk_app(f, _args[i], _args[j]); SASSERT(num_args > 1); - for (unsigned w = j; w < num_args - 1; w++) { + for (unsigned w = j; w + 1 < num_args; w++) { _args[w] = _args[w+1]; } num_args--; @@ -144,6 +144,7 @@ void maximize_ac_sharing::restore_entries(unsigned old_lim) { while (i != old_lim) { --i; entry * e = m_entries[i]; + m_cache.remove(e); m.dec_ref(e->m_arg1); m.dec_ref(e->m_arg2); } @@ -151,11 +152,7 @@ void maximize_ac_sharing::restore_entries(unsigned old_lim) { } void maximize_ac_sharing::reset() { - restore_entries(0); - m_entries.reset(); m_cache.reset(); - m_region.reset(); - m_scopes.reset(); } void maximize_bv_sharing::init_core() { diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 260d49174..95c030687 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -870,6 +870,12 @@ void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, s lhs = m().mk_app(f, binding.size(), binding.c_ptr()); eq = m().mk_eq(lhs, e); if (!ids.empty()) { + if (is_var(e)) { + ptr_vector domain; + for (expr* b : binding) domain.push_back(m().get_sort(b)); + insert_macro(f->get_name(), domain.size(), domain.c_ptr(), e); + return; + } if (!is_app(e)) { throw cmd_exception("Z3 only supports recursive definitions that are proper terms (not binders or variables)"); } @@ -1763,6 +1769,7 @@ void cmd_context::validate_model() { continue; } try { + for_each_expr(contains_underspecified, a); for_each_expr(contains_underspecified, r); } catch (contains_underspecified_op_proc::found) { diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index 306807f1f..7314403b0 100755 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -33,9 +33,11 @@ #include #include #include +#include #include "ast/expr_abstract.h" #include "util/params.h" +#include "ast/used_vars.h" using namespace stl_ext; @@ -938,3 +940,30 @@ void iz3mgr::get_bound_substitutes(stl_ext::hash_map &memo, const ast } #endif + +unsigned iz3mgr::num_free_variables(const ast &e){ + used_vars uv; + uv(to_expr(e.raw())); + return uv.get_num_vars(); +} + +iz3mgr::ast iz3mgr::close_universally (ast e){ + used_vars uv; + uv(to_expr(e.raw())); + std::vector bvs; + stl_ext::hash_map subst_memo; + for (unsigned i = 0; i < uv.get_max_found_var_idx_plus_1(); i++){ + if (uv.get(i)) { + std::ostringstream os; + os << "%%" << i; + ast c = make_var(os.str(),uv.get(i)); + ast v = cook(m().mk_var(i,uv.get(i))); + subst_memo[v] = c; + bvs.push_back(c); + } + } + e = subst(subst_memo,e); + for (unsigned i = 0; i < bvs.size(); i++) + e = apply_quant(Forall,bvs[i],e); + return e; +} diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index e6e08f84d..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; } @@ -661,6 +661,12 @@ class iz3mgr { ast apply_quant(opr quantifier, ast var, ast e); + // Universally quantify all the free variables in a formula. + // Makes up names for the quntifiers. + + ast close_universally (ast e); + + unsigned num_free_variables(const ast &e); /** For debugging */ void show(ast); diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index eb7f8e325..fc9d0fac6 100755 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -2968,9 +2968,9 @@ class iz3proof_itp_impl : public iz3proof_itp { ast interpolate(const node &pf){ // proof of false must be a formula, with quantified symbols #ifndef BOGUS_QUANTS - return add_quants(z3_simplify(pf)); + return close_universally(add_quants(z3_simplify(pf))); #else - return z3_simplify(pf); + return close_universally(z3_simplify(pf)); #endif } diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index ebbee46ca..c59dd0178 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -234,6 +234,11 @@ public: } } + // if(!range_is_empty(rng)){ + // if (num_free_variables(con) > 0) + // rng = range_empty(); + // } + if(res == INT_MAX){ if(range_is_empty(rng)) res = -1; diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index f94558097..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) { - m_manager.dec_ref(ec->get_data().m_key); - m_manager.dec_ref(ec->get_data().m_value); + 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(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) { - m_manager.dec_ref(ef->get_data().m_key); - dealloc(ef->get_data().m_value); + 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(k); + dealloc(v); } } diff --git a/src/muz/ddnf/ddnf.cpp b/src/muz/ddnf/ddnf.cpp index 0e2f6b35f..da1f5392b 100644 --- a/src/muz/ddnf/ddnf.cpp +++ b/src/muz/ddnf/ddnf.cpp @@ -192,10 +192,15 @@ namespace datalog { for (unsigned i = 0; i < new_tbvs.size(); ++i) { tbv const& nt = *new_tbvs[i]; IF_VERBOSE(10, m_tbv.display(verbose_stream() << "insert: ", nt); verbose_stream() << "\n";); - if (contains(nt)) continue; - ddnf_node* n = alloc(ddnf_node, *this, m_tbv, nt, m_noderefs.size()); - m_noderefs.push_back(n); - m_nodes.insert(n); + ddnf_node* n; + if (contains(nt)) { + n = find(nt); + } + else { + n = alloc(ddnf_node, *this, m_tbv, nt, m_noderefs.size()); + m_noderefs.push_back(n); + m_nodes.insert(n); + } insert(*m_root, n, new_tbvs); } return find(t); @@ -275,13 +280,17 @@ namespace datalog { void insert(ddnf_node& root, ddnf_node* new_n, ptr_vector& new_intersections) { tbv const& new_tbv = new_n->get_tbv(); + IF_VERBOSE(10, m_tbv.display(verbose_stream() << "root: ", root.get_tbv()); + m_tbv.display(verbose_stream() << " new node ", new_tbv); verbose_stream() << "\n";); SASSERT(m_tbv.contains(root.get_tbv(), new_tbv)); - if (&root == new_n) return; + if (m_eq(&root, new_n)) return; ++m_stats.m_num_inserts; bool inserted = false; for (unsigned i = 0; i < root.num_children(); ++i) { ddnf_node& child = *(root[i]); ++m_stats.m_num_comparisons; + IF_VERBOSE(10, m_tbv.display(verbose_stream() << "child ", child.get_tbv()); + verbose_stream() << " contains: " << m_tbv.contains(child.get_tbv(), new_tbv) << "\n";); if (m_tbv.contains(child.get_tbv(), new_tbv)) { inserted = true; insert(child, new_n, new_intersections); @@ -299,11 +308,13 @@ namespace datalog { // checking for subset if (m_tbv.contains(new_tbv, child.get_tbv())) { subset_children.push_back(&child); + IF_VERBOSE(10, m_tbv.display(verbose_stream() << "contains child", child.get_tbv()); verbose_stream() << "\n";); ++m_stats.m_num_comparisons; } else if (m_tbv.intersect(child.get_tbv(), new_tbv, *intr)) { // this means there is a non-full intersection new_intersections.push_back(intr); + IF_VERBOSE(10, m_tbv.display(verbose_stream() << "intersect child ", child.get_tbv()); verbose_stream() << "\n";); intr = m_tbv.allocate(); m_stats.m_num_comparisons += 2; } diff --git a/src/muz/rel/karr_relation.cpp b/src/muz/rel/karr_relation.cpp index 572d5e8d5..c8a489d69 100644 --- a/src/muz/rel/karr_relation.cpp +++ b/src/muz/rel/karr_relation.cpp @@ -111,8 +111,8 @@ namespace datalog { void filter_interpreted(app* cond) { rational one(1), mone(-1); - expr* e1, *e2, *en; - var* v, *w; + expr* e1 = 0, *e2 = 0, *en = 0; + var* v = 0, *w = 0; rational n1, n2; expr_ref_vector conjs(m); flatten_and(cond, conjs); 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 { diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp index 30505a5e8..7bd35b4ef 100644 --- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp +++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp @@ -398,8 +398,8 @@ namespace datalog { } bool mk_interp_tail_simplifier::propagate_variable_equivalences(rule * r, rule_ref& res) { - if (!m_context.get_params ().xform_tail_simplifier_pve ()) - return false; + if (!m_context.get_params ().xform_tail_simplifier_pve ()) + return false; unsigned u_len = r->get_uninterpreted_tail_size(); unsigned len = r->get_tail_size(); if (u_len == len) { diff --git a/src/parsers/smt2/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp index c1cc40b2b..9a9e69b67 100644 --- a/src/parsers/smt2/smt2scanner.cpp +++ b/src/parsers/smt2/smt2scanner.cpp @@ -124,7 +124,7 @@ namespace smt2 { next(); bool is_float = false; - while (true) { + while (!m_at_eof) { char c = curr(); if ('0' <= c && c <= '9') { m_number = rational(10)*m_number + rational(c - '0'); diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index a4275f804..e0c1b1696 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -218,11 +218,17 @@ namespace sat { bool ba_solver::init_watch(card& c, bool is_true) { clear_watch(c); - if (c.lit() != null_literal && c.lit().sign() == is_true) { + literal root = c.lit(); + if (root != null_literal && root.sign() == is_true) { c.negate(); + root.neg(); } - TRACE("sat", display(tout << "init watch: ", c, true);); - SASSERT(c.lit() == null_literal || value(c.lit()) == l_true); + if (root != null_literal) { + if (!is_watched(root, c)) watch_literal(root, c); + if (!is_watched(~root, c)) watch_literal(~root, c); + } + TRACE("ba", display(tout << "init watch: ", c, true);); + SASSERT(root == null_literal || value(root) == l_true); unsigned j = 0, sz = c.size(), bound = c.k(); // put the non-false literals into the head. @@ -293,7 +299,11 @@ namespace sat { void ba_solver::set_conflict(constraint& c, literal lit) { m_stats.m_num_conflicts++; - TRACE("sat", display(tout, c, true); ); + TRACE("ba", display(tout, c, true); ); + if (!validate_conflict(c)) { + display(std::cout, c, true); + UNREACHABLE(); + } SASSERT(validate_conflict(c)); if (c.is_xor() && value(lit) == l_true) lit.neg(); SASSERT(value(lit) == l_false); @@ -312,7 +322,7 @@ namespace sat { default: m_stats.m_num_propagations++; m_num_propagations_since_pop++; - //TRACE("sat", tout << "#prop: " << m_stats.m_num_propagations << " - " << c.lit() << " => " << lit << "\n";); + //TRACE("ba", tout << "#prop: " << m_stats.m_num_propagations << " - " << c.lit() << " => " << lit << "\n";); SASSERT(validate_unit_propagation(c, lit)); if (get_config().m_drat) { svector ps; @@ -333,25 +343,26 @@ namespace sat { void ba_solver::simplify(pb_base& p) { SASSERT(s().at_base_lvl()); if (p.lit() != null_literal && value(p.lit()) == l_false) { - TRACE("sat", tout << "pb: flip sign " << p << "\n";); + TRACE("ba", tout << "pb: flip sign " << p << "\n";); IF_VERBOSE(0, verbose_stream() << "sign is flipped " << p << "\n";); return; - init_watch(p, !p.lit().sign()); } bool nullify = p.lit() != null_literal && value(p.lit()) == l_true; if (nullify) { + IF_VERBOSE(10, display(verbose_stream() << "nullify tracking literal\n", p, true);); SASSERT(lvl(p.lit()) == 0); nullify_tracking_literal(p); + init_watch(p, true); } - SASSERT(p.lit() == null_literal || value(p.lit()) == l_undef); + SASSERT(p.lit() == null_literal || value(p.lit()) != l_false); unsigned true_val = 0, slack = 0, num_false = 0; for (unsigned i = 0; i < p.size(); ++i) { literal l = p.get_lit(i); if (s().was_eliminated(l.var())) { SASSERT(p.learned()); - remove_constraint(p); + remove_constraint(p, "contains eliminated"); return; } switch (value(l)) { @@ -363,63 +374,71 @@ namespace sat { if (p.k() == 1 && p.lit() == null_literal) { literal_vector lits(p.literals()); s().mk_clause(lits.size(), lits.c_ptr(), p.learned()); - remove_constraint(p); + IF_VERBOSE(10, display(verbose_stream() << "add clause: " << lits << "\n", p, true);); + remove_constraint(p, "implies clause"); } else if (true_val == 0 && num_false == 0) { - if (nullify) { + if (p.lit() == null_literal || value(p.lit()) == l_true) { init_watch(p, true); } } else if (true_val >= p.k()) { if (p.lit() != null_literal) { + IF_VERBOSE(10, display(verbose_stream() << "assign true literal ", p, true);); s().assign(p.lit(), justification()); } - remove_constraint(p); + remove_constraint(p, "is true"); } else if (slack + true_val < p.k()) { if (p.lit() != null_literal) { + IF_VERBOSE(10, display(verbose_stream() << "assign false literal ", p, true);); s().assign(~p.lit(), justification()); } else { IF_VERBOSE(0, verbose_stream() << "unsat during simplification\n";); s().set_conflict(justification()); } - remove_constraint(p); + remove_constraint(p, "is false"); } else if (slack + true_val == p.k()) { - literal_vector lits(p.literals()); + literal_vector lits(p.literals()); assert_unconstrained(p.lit(), lits); - remove_constraint(p); + remove_constraint(p, "is tight"); } else { + unsigned sz = p.size(); clear_watch(p); + unsigned j = 0; for (unsigned i = 0; i < sz; ++i) { literal l = p.get_lit(i); - if (value(l) != l_undef) { - --sz; - p.swap(i, sz); - --i; + if (value(l) == l_undef) { + if (i != j) p.swap(i, j); + ++j; } } + sz = j; + // _bad_id = p.id(); BADLOG(display(verbose_stream() << "simplify ", p, true)); + p.set_size(sz); p.set_k(p.k() - true_val); - BADLOG(display(verbose_stream() << "simplified ", p, true)); - // display(verbose_stream(), c, true); if (p.k() == 1 && p.lit() == null_literal) { - literal_vector lits(p.literals()); - s().mk_clause(lits.size(), lits.c_ptr(), p.learned()); - remove_constraint(p); + literal_vector lits(sz, p.literals().c_ptr()); + s().mk_clause(sz, lits.c_ptr(), p.learned()); + remove_constraint(p, "is clause"); return; } - else if (p.lit() == null_literal) { + else if (p.lit() == null_literal || value(p.lit()) == l_true) { init_watch(p, true); } else { SASSERT(value(p.lit()) == l_undef); } + BADLOG(display(verbose_stream() << "simplified ", p, true); verbose_stream() << "\n"); + // display(verbose_stream(), c, true); + _bad_id = 11111111; SASSERT(p.well_formed()); if (p.is_pb()) simplify2(p.to_pb()); m_simplify_change = true; @@ -492,7 +511,7 @@ namespace sat { // watch a prefix of literals, such that the slack of these is >= k bool ba_solver::init_watch(pb& p, bool is_true) { - clear_watch(p); + clear_watch(p); if (p.lit() != null_literal && p.lit().sign() == is_true) { p.negate(); } @@ -545,9 +564,9 @@ namespace sat { p.set_slack(slack); p.set_num_watch(num_watch); - SASSERT(validate_watch(p)); + SASSERT(validate_watch(p, null_literal)); - TRACE("sat", display(tout << "init watch: ", p, true);); + TRACE("ba", display(tout << "init watch: ", p, true);); // slack is tight: if (slack + slack1 == bound) { @@ -602,9 +621,8 @@ namespace sat { friendly (and the overhead of backtracking has to be taken into account). */ lbool ba_solver::add_assign(pb& p, literal alit) { - BADLOG(display(verbose_stream() << "assign: " << alit << " watch: " << p.num_watch() << " size: " << p.size(), p, true)); - TRACE("sat", display(tout << "assign: " << alit << "\n", p, true);); + TRACE("ba", display(tout << "assign: " << alit << "\n", p, true);); SASSERT(!inconsistent()); unsigned sz = p.size(); unsigned bound = p.k(); @@ -631,12 +649,13 @@ namespace sat { display(verbose_stream(), p, true); verbose_stream() << "alit: " << alit << "\n"; verbose_stream() << "num watch " << num_watch << "\n"); + UNREACHABLE(); exit(0); return l_undef; } - validate_watch(p); - // SASSERT(validate_watch(p)); + SASSERT(validate_watch(p, null_literal)); + // SASSERT(validate_watch(p, null_literal)); SASSERT(index < num_watch); unsigned index1 = index + 1; @@ -658,7 +677,7 @@ namespace sat { watch_literal(p[j], p); p.swap(num_watch, j); add_index(p, num_watch, lit); - BADLOG(verbose_stream() << "add watch: " << lit << " num watch: " << num_watch << "\n"); + BADLOG(verbose_stream() << "add watch: " << lit << " num watch: " << num_watch << " max: " << m_a_max << " slack " << slack << "\n"); ++num_watch; } } @@ -671,10 +690,10 @@ namespace sat { slack += val; p.set_slack(slack); p.set_num_watch(num_watch); - validate_watch(p); + SASSERT(validate_watch(p, null_literal)); BADLOG(display(verbose_stream() << "conflict: " << alit << " watch: " << p.num_watch() << " size: " << p.size(), p, true)); SASSERT(bound <= slack); - TRACE("sat", tout << "conflict " << alit << "\n";); + TRACE("ba", tout << "conflict " << alit << "\n";); set_conflict(p, alit); return l_false; } @@ -696,7 +715,8 @@ namespace sat { // l must be true. // if (slack < bound + m_a_max) { - TRACE("sat", tout << p; for(auto j : m_pb_undef) tout << j << "\n";); + BADLOG(verbose_stream() << "slack " << slack << " " << bound << " " << m_a_max << "\n";); + TRACE("ba", tout << p << "\n"; for(auto j : m_pb_undef) tout << j << " "; tout << "\n";); for (unsigned index1 : m_pb_undef) { if (index1 == num_watch) { index1 = index; @@ -704,16 +724,16 @@ namespace sat { wliteral wl = p[index1]; literal lit = wl.second; SASSERT(value(lit) == l_undef); - BADLOG(verbose_stream() << "Assign " << lit << "\n"); if (slack < bound + wl.first) { + BADLOG(verbose_stream() << "Assign " << lit << " " << wl.first << "\n"); assign(p, lit); } } } - validate_watch(p); + SASSERT(validate_watch(p, alit)); // except that alit is still watched. - TRACE("sat", display(tout << "assign: " << alit << "\n", p, true);); + TRACE("ba", display(tout << "assign: " << alit << "\n", p, true);); BADLOG(verbose_stream() << "unwatch " << alit << " watch: " << p.num_watch() << " size: " << p.size() << " slack: " << p.slack() << " " << inconsistent() << "\n"); @@ -729,6 +749,8 @@ namespace sat { unwatch_literal(p[i].second, p); } p.set_num_watch(0); + + DEBUG_CODE(for (wliteral wl : p) VERIFY(!is_watched(wl.second, p));); } void ba_solver::recompile(pb& p) { @@ -741,14 +763,13 @@ namespace sat { unsigned k = p.k(); unsigned sz = p.size(); bool all_units = true; + unsigned j = 0; for (unsigned i = 0; i < sz && 0 < k; ++i) { literal l = p[i].second; unsigned w1 = m_weights[l.index()]; unsigned w2 = m_weights[(~l).index()]; if (w1 == 0 || w1 < w2) { - p.swap(i, sz - 1); - --sz; - --i; + continue; } else if (k <= w2) { k = 0; @@ -761,16 +782,16 @@ namespace sat { m_weights[l.index()] = 0; m_weights[(~l).index()] = 0; if (w1 == 0) { - p.swap(i, sz - 1); - --sz; - --i; + continue; } else { - p[i] = wliteral(w1, l); + p[j] = wliteral(w1, l); all_units &= w1 == 1; + ++j; } } } + sz = j; // clear weights for (wliteral wl : p) { m_weights[wl.second.index()] = 0; @@ -781,31 +802,32 @@ namespace sat { if (p.lit() != null_literal) { s().assign(p.lit(), justification()); } - remove_constraint(p); + remove_constraint(p, "recompiled to true"); return; } - if (k == 1 && p.lit() == null_literal) { - literal_vector lits(p.literals()); + else if (k == 1 && p.lit() == null_literal) { + literal_vector lits(sz, p.literals().c_ptr()); s().mk_clause(sz, lits.c_ptr(), p.learned()); - remove_constraint(p); + remove_constraint(p, "recompiled to clause"); return; } - if (all_units) { + else if (all_units) { literal_vector lits(sz, p.literals().c_ptr()); add_at_least(p.lit(), lits, k, p.learned()); - remove_constraint(p); + remove_constraint(p, "recompiled to cardinality"); return; } - p.set_size(sz); - p.set_k(k); - SASSERT(p.well_formed()); - - // this could become a cardinality constraint by now. - if (p.lit() == null_literal || value(p.lit()) == l_true) { - init_watch(p, true); + else { + p.set_size(sz); + p.set_k(k); + SASSERT(p.well_formed()); + + if (p.lit() == null_literal || value(p.lit()) == l_true) { + init_watch(p, true); + } } } @@ -816,12 +838,12 @@ namespace sat { literal_vector lits(p.literals()); unsigned k = (p.k() + p[0].first - 1) / p[0].first; add_at_least(p.lit(), lits, k, p.learned()); - remove_constraint(p); + remove_constraint(p, "simplified to cardinality"); } else if (p.lit() == null_literal) { for (wliteral wl : p) { if (p.k() > p.max_sum() - wl.first) { - TRACE("sat", + TRACE("ba", tout << "unit literal " << wl.second << "\n"; display(tout, p, true);); @@ -833,17 +855,21 @@ namespace sat { void ba_solver::display(std::ostream& out, pb const& p, bool values) const { if (p.lit() != null_literal) out << p.lit() << " == "; - if (p.lit() != null_literal && values) { + if (values) { out << "[watch: " << p.num_watch() << ", slack: " << p.slack() << "]"; + } + if (p.lit() != null_literal && values) { out << "@(" << value(p.lit()); if (value(p.lit()) != l_undef) { out << ":" << lvl(p.lit()); } out << "): "; } + unsigned i = 0; for (wliteral wl : p) { literal l = wl.second; unsigned w = wl.first; + if (i++ == p.num_watch()) out << " | "; if (w > 1) out << w << " * "; out << l; if (values) { @@ -888,7 +914,7 @@ namespace sat { if (x.lit() != null_literal && x.lit().sign() == is_true) { x.negate(); } - TRACE("sat", display(tout, x, true);); + TRACE("ba", display(tout, x, true);); unsigned sz = x.size(); unsigned j = 0; for (unsigned i = 0; i < sz && j < 2; ++i) { @@ -930,7 +956,7 @@ namespace sat { lbool ba_solver::add_assign(xor& x, literal alit) { // literal is assigned unsigned sz = x.size(); - TRACE("sat", tout << "assign: " << x.lit() << ": " << ~alit << "@" << lvl(~alit) << "\n";); + TRACE("ba", tout << "assign: " << x.lit() << ": " << ~alit << "@" << lvl(~alit) << "\n";); SASSERT(x.lit() == null_literal || value(x.lit()) == l_true); SASSERT(value(alit) != l_undef); @@ -1055,7 +1081,6 @@ namespace sat { int64 new_bound = m_bound; new_bound += i; if (new_bound < 0) { - // std::cout << "new negative bound " << new_bound << "\n"; m_overflow = true; } else if (new_bound > UINT_MAX) { @@ -1077,6 +1102,8 @@ namespace sat { static literal _debug_consequent = null_literal; static unsigned_vector _debug_var2position; +// #define DEBUG_CODE(_x_) _x_ + lbool ba_solver::resolve_conflict() { if (0 == m_num_propagations_since_pop) { return l_undef; @@ -1087,7 +1114,7 @@ namespace sat { m_bound = 0; literal consequent = s().m_not_l; justification js = s().m_conflict; - TRACE("sat", tout << consequent << " " << js << "\n"; s().display(tout);); + TRACE("ba", tout << consequent << " " << js << "\n";); m_conflict_lvl = s().get_max_lvl(consequent, js); if (consequent != null_literal) { consequent.neg(); @@ -1114,10 +1141,10 @@ namespace sat { } TRACE("sat_verbose", display(tout, m_A);); - TRACE("sat", tout << "process consequent: " << consequent << " : "; s().display_justification(tout, js) << "\n";); + TRACE("ba", tout << "process consequent: " << consequent << " : "; s().display_justification(tout, js) << "\n";); SASSERT(offset > 0); - // DEBUG_CODE(justification2pb(js, consequent, offset, m_B);); + DEBUG_CODE(justification2pb(js, consequent, offset, m_B);); if (_debug_conflict) { IF_VERBOSE(0, @@ -1180,7 +1207,7 @@ namespace sat { inc_bound(offset); inc_coeff(consequent, offset); get_antecedents(consequent, p, m_lemma); - TRACE("sat", display(tout, p, true); tout << m_lemma << "\n";); + TRACE("ba", display(tout, p, true); tout << m_lemma << "\n";); if (_debug_conflict) { verbose_stream() << consequent << " "; verbose_stream() << "antecedents: " << m_lemma << "\n"; @@ -1212,10 +1239,10 @@ namespace sat { DEBUG_CODE( active2pb(m_C); - //SASSERT(validate_resolvent()); + VERIFY(validate_resolvent()); m_A = m_C;); - TRACE("sat", display(tout << "conflict: ", m_A);); + TRACE("ba", display(tout << "conflict: ", m_A);); cut(); @@ -1261,16 +1288,11 @@ namespace sat { if (!create_asserting_lemma()) { goto bail_out; } - active2card(); - if (m_overflow) { - goto bail_out; - } - - SASSERT(validate_conflict(m_lemma, m_A)); + DEBUG_CODE(VERIFY(validate_conflict(m_lemma, m_A));); - TRACE("sat", tout << m_lemma << "\n";); + TRACE("ba", tout << m_lemma << "\n";); if (get_config().m_drat) { svector ps; // TBD fill in @@ -1280,7 +1302,7 @@ namespace sat { s().m_lemma.reset(); s().m_lemma.append(m_lemma); for (unsigned i = 1; i < m_lemma.size(); ++i) { - CTRACE("sat", s().is_marked(m_lemma[i].var()), tout << "marked: " << m_lemma[i] << "\n";); + CTRACE("ba", s().is_marked(m_lemma[i].var()), tout << "marked: " << m_lemma[i] << "\n";); s().mark(m_lemma[i].var()); } @@ -1372,7 +1394,6 @@ namespace sat { IF_VERBOSE(20, verbose_stream() << "(sat.card slack: " << slack << " skipped: " << num_skipped << ")\n";); return false; } - if (m_lemma[0] == null_literal) { if (m_lemma.size() == 1) { @@ -1387,7 +1408,7 @@ namespace sat { IF_VERBOSE(10, verbose_stream() << "(sat.backjump :new-level " << m_conflict_lvl << " :old-level " << old_level << ")\n";); goto adjust_conflict_level; } - return true; + return !m_overflow; } /* @@ -1470,7 +1491,7 @@ namespace sat { TRACE("sat_verbose", tout << "Mark: v" << v << "\n";); ++m_num_marks; if (_debug_conflict && _debug_consequent != null_literal && _debug_var2position[_debug_consequent.var()] < _debug_var2position[l.var()]) { - std::cout << "antecedent " << l << " is above consequent in stack\n"; + IF_VERBOSE(0, verbose_stream() << "antecedent " << l << " is above consequent in stack\n";); } } inc_coeff(l, offset); @@ -1493,7 +1514,7 @@ namespace sat { } ba_solver::ba_solver(): m_solver(0), m_lookahead(0), m_constraint_id(0) { - TRACE("sat", tout << this << "\n";); + TRACE("ba", tout << this << "\n";); } ba_solver::~ba_solver() { @@ -1543,9 +1564,9 @@ namespace sat { init_watch(*c, true); } else { - s().set_external(lit.var()); - get_wlist(lit).push_back(watched(c->index())); - get_wlist(~lit).push_back(watched(c->index())); + if (m_solver) m_solver->set_external(lit.var()); + watch_literal(lit, *c); + watch_literal(~lit, *c); } SASSERT(c->well_formed()); } @@ -1613,8 +1634,8 @@ namespace sat { */ bool ba_solver::propagate(literal l, ext_constraint_idx idx) { SASSERT(value(l) == l_true); - TRACE("sat", tout << l << " " << idx << "\n";); constraint& c = index2constraint(idx); + TRACE("ba", tout << l << "\n";); if (c.lit() != null_literal && l.var() == c.lit().var()) { init_watch(c, !l.sign()); return true; @@ -1709,7 +1730,7 @@ namespace sat { unsigned level = lvl(l); bool_var v = l.var(); SASSERT(js.get_kind() == justification::EXT_JUSTIFICATION); - TRACE("sat", tout << l << ": " << js << "\n"; tout << s().m_trail << "\n";); + TRACE("ba", tout << l << ": " << js << "\n"; tout << s().m_trail << "\n";); unsigned num_marks = 0; unsigned count = 0; @@ -1776,7 +1797,7 @@ namespace sat { reset_parity(lit.var()); } m_parity_trail.reset(); - TRACE("sat", tout << r << "\n";); + TRACE("ba", tout << r << "\n";); } /** @@ -1791,8 +1812,29 @@ namespace sat { Then x is an explanation for l */ + + bool ba_solver::assigned_above(literal above, literal below) { + unsigned l = lvl(above); + SASSERT(l == lvl(below)); + if (l == 0) return false; + unsigned start = s().m_scopes[l-1].m_trail_lim; + literal_vector const& lits = s().m_trail; + +#if 0 + IF_VERBOSE(10, verbose_stream() << "level " << l << " scope level " << s().scope_lvl() << " tail lim start: " + << start << " size of lits: " << lits.size() << " num scopes " << s().m_scopes.size() << "\n";); +#endif + + for (unsigned sz = lits.size(); sz-- > start; ) { + if (lits[sz] == above) return true; + if (lits[sz] == below) return false; + } + UNREACHABLE(); + return false; + } + void ba_solver::get_antecedents(literal l, pb const& p, literal_vector& r) { - TRACE("sat", display(tout, p, true);); + TRACE("ba", display(tout << l << " level: " << s().scope_lvl() << " ", p, true);); SASSERT(p.lit() == null_literal || value(p.lit()) == l_true); if (p.lit() != null_literal) { @@ -1802,8 +1844,8 @@ namespace sat { unsigned k = p.k(); if (_debug_conflict) { - display(std::cout, p, true); - std::cout << "literal: " << l << " value: " << value(l) << " num-watch: " << p.num_watch() << " slack: " << p.slack() << "\n"; + IF_VERBOSE(0, display(verbose_stream(), p, true); + verbose_stream() << "literal: " << l << " value: " << value(l) << " num-watch: " << p.num_watch() << " slack: " << p.slack() << "\n";); } if (value(l) == l_false) { @@ -1830,6 +1872,8 @@ namespace sat { } } else { + // comes from a unit propagation + SASSERT(value(l) == l_true); unsigned coeff = 0, j = 0; for (; j < p.size(); ++j) { if (p[j].second == l) { @@ -1842,21 +1886,29 @@ namespace sat { if (j < p.num_watch()) { j = p.num_watch(); } - CTRACE("sat", coeff == 0, display(tout << l << " coeff: " << coeff << "\n", p, true);); + CTRACE("ba", coeff == 0, display(tout << l << " coeff: " << coeff << "\n", p, true);); if (_debug_conflict) { std::cout << "coeff " << coeff << "\n"; } SASSERT(coeff > 0); - unsigned slack = p.slack() - coeff; - j = std::max(j + 1, p.num_watch()); + unsigned slack = p.max_sum() - coeff; + // we need antecedents to be deeper than alit. for (; j < p.size(); ++j) { literal lit = p[j].second; unsigned w = p[j].first; - SASSERT(l_false == value(lit)); - if (slack + w < k) { + if (l_false != value(lit)) { + // skip + } + else if (lvl(lit) > lvl(l)) { + // skip + } + else if (lvl(lit) == lvl(l) && assigned_above(~lit, l)) { + // skip + } + else if (slack + w < k) { slack += w; } else { @@ -1908,7 +1960,7 @@ namespace sat { void ba_solver::get_antecedents(literal l, xor const& x, literal_vector& r) { if (x.lit() != null_literal) r.push_back(x.lit()); - // TRACE("sat", display(tout << l << " ", x, true);); + // TRACE("ba", display(tout << l << " ", x, true);); SASSERT(x.lit() == null_literal || value(x.lit()) == l_true); SASSERT(x[0].var() == l.var() || x[1].var() == l.var()); if (x[0].var() == l.var()) { @@ -1977,10 +2029,11 @@ namespace sat { } } - void ba_solver::remove_constraint(constraint& c) { + void ba_solver::remove_constraint(constraint& c, char const* reason) { + IF_VERBOSE(21, display(verbose_stream() << "remove " << reason << " ", c, true);); nullify_tracking_literal(c); clear_watch(c); - c.remove(); + c.set_removed(); m_constraint_removed = true; } @@ -2100,16 +2153,11 @@ namespace sat { } bool ba_solver::validate_watched_constraint(constraint const& c) const { - if (c.is_pb() && !validate_watch(c.to_pb())) { + if (c.is_pb() && !validate_watch(c.to_pb(), null_literal)) { return false; } if (c.lit() != null_literal && value(c.lit()) != l_true) return true; - if (c.lit() != null_literal && lvl(c.lit()) != 0) { - if (!is_watched(c.lit(), c) || !is_watched(~c.lit(), c)) { - UNREACHABLE(); - return false; - } - } + SASSERT(c.lit() == null_literal || lvl(c.lit()) == 0 || (is_watched(c.lit(), c) && is_watched(~c.lit(), c))); if (eval(c) == l_true) { return true; } @@ -2136,14 +2184,25 @@ namespace sat { return true; } - bool ba_solver::validate_watch(pb const& p) const { + bool ba_solver::validate_watch(pb const& p, literal alit) const { for (unsigned i = 0; i < p.size(); ++i) { literal l = p[i].second; - if (lvl(l) != 0 && is_watched(l, p) != i < p.num_watch()) { + if (l != alit && lvl(l) != 0 && is_watched(l, p) != i < p.num_watch()) { + IF_VERBOSE(0, display(verbose_stream(), p, true); + verbose_stream() << "literal " << l << " at position " << i << " " << is_watched(l, p) << "\n";); UNREACHABLE(); return false; } } + unsigned slack = 0; + for (unsigned i = 0; i < p.num_watch(); ++i) { + slack += p[i].first; + } + if (slack != p.slack()) { + IF_VERBOSE(0, display(verbose_stream(), p, true);); + UNREACHABLE(); + return false; + } return true; } @@ -2190,14 +2249,14 @@ namespace sat { } void ba_solver::gc_half(char const* st_name) { - TRACE("sat", tout << "gc\n";); + TRACE("ba", tout << "gc\n";); unsigned sz = m_learned.size(); unsigned new_sz = sz/2; unsigned removed = 0; for (unsigned i = new_sz; i < sz; i++) { constraint* c = m_learned[i]; if (!m_constraint_to_reinit.contains(c)) { - remove_constraint(*c); + remove_constraint(*c, "gc"); ++removed; } } @@ -2211,7 +2270,7 @@ namespace sat { // literal is assigned to false. unsigned sz = c.size(); unsigned bound = c.k(); - TRACE("sat", tout << "assign: " << c.lit() << ": " << ~alit << "@" << lvl(~alit) << "\n";); + TRACE("ba", tout << "assign: " << c.lit() << ": " << ~alit << "@" << lvl(~alit) << "\n";); SASSERT(0 < bound && bound <= sz); if (bound == sz) { @@ -2245,12 +2304,12 @@ namespace sat { // conflict if (bound != index && value(c[bound]) == l_false) { - TRACE("sat", tout << "conflict " << c[bound] << " " << alit << "\n";); + TRACE("ba", tout << "conflict " << c[bound] << " " << alit << "\n";); set_conflict(c, alit); return l_false; } - // TRACE("sat", tout << "no swap " << index << " " << alit << "\n";); + // TRACE("ba", tout << "no swap " << index << " " << alit << "\n";); // there are no literals to swap with, // prepare for unit propagation by swapping the false literal into // position bound. Then literals in positions 0..bound-1 have to be @@ -2319,7 +2378,7 @@ namespace sat { } } - void ba_solver::simplify() { + void ba_solver::simplify() { if (!s().at_base_lvl()) s().pop_to_base_level(); unsigned trail_sz; do { @@ -2340,7 +2399,7 @@ namespace sat { } while (m_simplify_change || trail_sz < s().init_trail_size()); - IF_VERBOSE(1, verbose_stream() << "(ba.simplify " + IF_VERBOSE(1, verbose_stream() << "(ba.simplify" << " :vars " << s().num_vars() - trail_sz << " :constraints " << m_constraints.size() << " :lemmas " << m_learned.size() @@ -2506,7 +2565,6 @@ namespace sat { if (m_roots.empty()) return; // validate(); - m_visited.resize(s().num_vars()*2, false); m_constraint_removed = false; for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) @@ -2514,13 +2572,12 @@ namespace sat { for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) flush_roots(*m_learned[i]); cleanup_constraints(); - // validate(); } void ba_solver::recompile(constraint& c) { if (c.id() == _bad_id) { - display(std::cout << "recompile\n", c, true); + IF_VERBOSE(0, display(verbose_stream() << "recompile\n", c, true);); } switch (c.tag()) { case card_t: @@ -2538,6 +2595,9 @@ namespace sat { } void ba_solver::recompile(card& c) { + SASSERT(c.lit() == null_literal || is_watched(c.lit(), c)); + + // pre-condition is that the literals, except c.lit(), in c are unwatched. if (c.id() == _bad_id) std::cout << "recompile: " << c << "\n"; // IF_VERBOSE(0, verbose_stream() << "re: " << c << "\n";); m_weights.resize(2*s().num_vars(), 0); @@ -2548,14 +2608,14 @@ namespace sat { bool all_units = true; unsigned sz = c.size(); unsigned_vector coeffs; + literal_vector lits; + unsigned j = 0; for (unsigned i = 0; i < sz && 0 < k; ++i) { literal l = c[i]; unsigned w = m_weights[l.index()]; unsigned w2 = m_weights[(~l).index()]; if (w == 0 || w < w2) { - c.swap(i, sz - 1); - --sz; - --i; + continue; } else if (k <= w2) { k = 0; @@ -2568,51 +2628,53 @@ namespace sat { m_weights[(~l).index()] = 0; m_weights[l.index()] = 0; if (w == 0) { - c.swap(i, sz - 1); - --sz; - --i; + continue; } else { all_units &= (w == 1); coeffs.push_back(w); + c[j++] = l; } } } + sz = j; + // clear weights for (literal l : c) { m_weights[l.index()] = 0; m_weights[(~l).index()] = 0; } - if (k == 0) { - remove_constraint(c); + if (k == 0 && c.lit() == null_literal) { + remove_constraint(c, "recompiled to true"); return; } - if (k == 1) { - literal_vector lits(c.size(), c.begin()); - s().mk_clause(lits.size(), lits.c_ptr(), c.learned()); - remove_constraint(c); + if (k == 1 && c.lit() == null_literal) { + literal_vector lits(sz, c.literals().c_ptr()); + s().mk_clause(sz, lits.c_ptr(), c.learned()); + remove_constraint(c, "recompiled to clause"); return; } c.set_size(sz); - c.set_k(k); + c.set_k(k); if (!all_units) { - TRACE("sat", tout << "replacing by pb: " << c << "\n";); + TRACE("ba", tout << "replacing by pb: " << c << "\n";); m_wlits.reset(); for (unsigned i = 0; i < sz; ++i) { m_wlits.push_back(wliteral(coeffs[i], c[i])); } literal root = c.lit(); - remove_constraint(c); + remove_constraint(c, "recompiled to pb"); add_pb_ge(root, m_wlits, k, c.learned()); } else { if (c.lit() == null_literal || value(c.lit()) == l_true) { init_watch(c, true); } + SASSERT(c.lit() == null_literal || is_watched(c.lit(), c)); SASSERT(c.well_formed()); } } @@ -2629,6 +2691,11 @@ namespace sat { void ba_solver::flush_roots(constraint& c) { + if (c.lit() != null_literal && !is_watched(c.lit(), c)) { + watch_literal(c.lit(), c); + watch_literal(~c.lit(), c); + } + SASSERT(c.lit() == null_literal || is_watched(c.lit(), c)); bool found = c.lit() != null_literal && m_root_vars[c.lit().var()]; for (unsigned i = 0; !found && i < c.size(); ++i) { found = m_root_vars[c.get_lit(i).var()]; @@ -2643,12 +2710,12 @@ namespace sat { } literal root = c.lit(); - if (c.lit() != null_literal && m_roots[c.lit().index()] != c.lit()) { - root = m_roots[c.lit().index()]; + if (root != null_literal && m_roots[root.index()] != root) { + root = m_roots[root.index()]; nullify_tracking_literal(c); c.update_literal(root); - get_wlist(root).push_back(watched(c.index())); - get_wlist(~root).push_back(watched(c.index())); + watch_literal(root, c); + watch_literal(~root, c); } bool found_dup = false; @@ -2675,7 +2742,7 @@ namespace sat { split_root(c); c.negate(); split_root(c); - remove_constraint(c); + remove_constraint(c, "flush roots"); } else if (found_dup) { recompile(c); @@ -2755,12 +2822,13 @@ namespace sat { switch (c.tag()) { case card_t: case pb_t: { - if (lit != null_literal && + if (lit != null_literal && + value(lit) == l_undef && use_count(lit) == 1 && use_count(~lit) == 1 && get_num_non_learned_bin(lit) == 0 && get_num_non_learned_bin(~lit) == 0) { - remove_constraint(c); + remove_constraint(c, "unused def"); } break; } @@ -2776,8 +2844,9 @@ namespace sat { for (unsigned v = 0; v < s().num_vars(); ++v) { literal lit(v, false); if (s().is_external(v) && - m_cnstr_use_list[lit.index()].size() == 0 && - m_cnstr_use_list[(~lit).index()].size() == 0 && !s().is_assumption(v)) { + m_cnstr_use_list[lit.index()].empty() && + m_cnstr_use_list[(~lit).index()].empty() && + !s().is_assumption(v)) { s().set_non_external(v); ++ext; } @@ -2790,7 +2859,7 @@ namespace sat { for (unsigned i = 0; i < c.size(); ++i) { bool_var v = c.get_lit(i).var(); if (s().was_eliminated(v)) { - remove_constraint(c); + remove_constraint(c, "contains eliminated var"); break; } s().set_external(v); @@ -2801,9 +2870,9 @@ namespace sat { } bool ba_solver::elim_pure(literal lit) { - if (value(lit) != l_undef) return false; - if (!m_cnstr_use_list[lit.index()].empty() && use_count(~lit) == 0 && - get_num_non_learned_bin(~lit) == 0) { + if (value(lit) == l_undef && !m_cnstr_use_list[lit.index()].empty() && + use_count(~lit) == 0 && get_num_non_learned_bin(~lit) == 0) { + IF_VERBOSE(10, verbose_stream() << "pure literal: " << lit << "\n";); s().assign(lit, justification()); return true; } @@ -2855,7 +2924,7 @@ namespace sat { clause_vector::iterator it2 = it; for (; it != end; ++it) { clause* c = *it; - if (c->was_removed()) { + if (c->was_removed() && s().can_delete(*c)) { s().detach_clause(*c); s().del_clause(*c); } @@ -2891,6 +2960,8 @@ namespace sat { for (; it != end; ++it) { constraint& c = *(*it); if (c.was_removed()) { + clear_watch(c); + nullify_tracking_literal(c); m_allocator.deallocate(c.obj_size(), &c); } else if (learned && !c.learned()) { @@ -2994,7 +3065,7 @@ namespace sat { if (s) { ++m_stats.m_num_pb_subsumes; p1.set_learned(false); - remove_constraint(*c); + remove_constraint(*c, "subsumed"); } } } @@ -3023,13 +3094,13 @@ namespace sat { SASSERT(c1.index() != c2.index()); if (subsumes(c1, c2, slit)) { if (slit.empty()) { - TRACE("sat", tout << "subsume cardinality\n" << c1.index() << ":" << c1 << "\n" << c2.index() << ":" << c2 << "\n";); - remove_constraint(c2); + TRACE("ba", tout << "subsume cardinality\n" << c1.index() << ":" << c1 << "\n" << c2.index() << ":" << c2 << "\n";); + remove_constraint(c2, "subsumed"); ++m_stats.m_num_pb_subsumes; c1.set_learned(false); } else { - TRACE("sat", tout << "self subsume cardinality\n";); + TRACE("ba", tout << "self subsume cardinality\n";); IF_VERBOSE(0, verbose_stream() << "self-subsume cardinality is TBD\n"; verbose_stream() << c1 << "\n"; @@ -3059,7 +3130,7 @@ namespace sat { clause& c2 = it.curr(); if (!c2.was_removed() && subsumes(c1, c2, slit)) { if (slit.empty()) { - TRACE("sat", tout << "remove\n" << c1 << "\n" << c2 << "\n";); + TRACE("ba", tout << "remove\n" << c1 << "\n" << c2 << "\n";); removed_clauses.push_back(&c2); ++m_stats.m_num_clause_subsumes; c1.set_learned(false); @@ -3067,7 +3138,7 @@ namespace sat { else { IF_VERBOSE(0, verbose_stream() << "self-subsume clause is TBD\n";); // remove literal slit from c2. - TRACE("sat", tout << "TBD remove literals " << slit << " from " << c2 << "\n";); + TRACE("ba", tout << "TBD remove literals " << slit << " from " << c2 << "\n";); } } it.next(); @@ -3098,9 +3169,7 @@ namespace sat { ++it2; } } - if (it != it2) { - wlist.set_end(it2); - } + wlist.set_end(it2); } void ba_solver::subsumption(card& c1) { @@ -3138,7 +3207,7 @@ namespace sat { for (wliteral l : p1) { m_weights[l.second.index()] = 0; unmark_visited(l.second); - } + } } void ba_solver::clauses_modifed() {} @@ -3174,6 +3243,18 @@ namespace sat { extension* ba_solver::copy(solver* s) { ba_solver* result = alloc(ba_solver); result->set_solver(s); + copy_core(result); + return result; + } + + extension* ba_solver::copy(lookahead* s) { + ba_solver* result = alloc(ba_solver); + result->set_lookahead(s); + copy_core(result); + return result; + } + + void ba_solver::copy_core(ba_solver* result) { literal_vector lits; svector wlits; for (constraint* cp : m_constraints) { @@ -3205,8 +3286,6 @@ namespace sat { UNREACHABLE(); } } - - return result; } void ba_solver::init_use_list(ext_use_list& ul) { @@ -3431,12 +3510,12 @@ namespace sat { } bool ba_solver::validate_unit_propagation(pb const& p, literal alit) const { - if (p.lit() != null_literal && value(p.lit()) != l_true) { + if (p.lit() != null_literal && value(p.lit()) != l_true) { return false; } unsigned sum = 0; - TRACE("sat", display(tout << "validate: " << alit << "\n", p, true);); + TRACE("ba", display(tout << "validate: " << alit << "\n", p, true);); for (wliteral wl : p) { literal lit = wl.second; lbool val = value(lit); @@ -3448,21 +3527,56 @@ namespace sat { } bool ba_solver::validate_unit_propagation(pb const& p, literal_vector const& r, literal alit) const { - unsigned sum = 0; // all elements of r are true, for (literal l : r) { if (value(l) != l_true) { + IF_VERBOSE(0, verbose_stream() << "value of " << l << " is " << value(l) << "\n"; + display(verbose_stream(), p, true);); return false; } + if (value(alit) == l_true && lvl(l) > lvl(alit)) { + IF_VERBOSE(0, + verbose_stream() << "level of premise " << l << " is " << lvl(l) << "\n"; + verbose_stream() << "level of asserting literal " << alit << " is " << lvl(alit) << "\n"; + display(verbose_stream(), p, true);); + return false; + } + // if (value(alit) == l_true && lvl(l) == lvl(alit)) { + // std::cout << "same level " << alit << " " << l << "\n"; + // } } // the sum of elements not in r or alit add up to less than k. + unsigned sum = 0; + // + // a*x + b*alit + c*r >= k + // sum a < k + // val(r) = false + // hence alit has to be true. for (wliteral wl : p) { literal lit = wl.second; - if (lit != alit && value(lit) != l_false && !r.contains(~lit)) { + if (lit != alit && !r.contains(~lit)) { sum += wl.first; } } - return sum < p.k(); + if (sum >= p.k()) { + IF_VERBOSE(0, + verbose_stream() << "sum is " << sum << " >= " << p.k() << "\n"; + display(verbose_stream(), p, true); + verbose_stream() << "id: " << p.id() << "\n"; + sum = 0; + for (wliteral wl : p) sum += wl.first; + verbose_stream() << "overall sum " << sum << "\n"; + verbose_stream() << "asserting literal: " << alit << "\n"; + verbose_stream() << "reason: " << r << "\n";); + return false; + } + for (wliteral wl : p) { + if (alit == wl.second) { + return true; + } + } + IF_VERBOSE(0, verbose_stream() << alit << " not found among literals\n";); + return false; } bool ba_solver::validate_unit_propagation(xor const& x, literal alit) const { @@ -3490,7 +3604,7 @@ namespace sat { val += coeff; } } - CTRACE("sat", val >= 0, active2pb(m_A); display(tout, m_A);); + CTRACE("ba", val >= 0, active2pb(m_A); display(tout, m_A);); return val < 0; } @@ -3627,12 +3741,12 @@ namespace sat { constraint* c = add_at_least(null_literal, lits, k, true); if (c) { + // IF_VERBOSE(0, verbose_stream() << *c << "\n";); lits.reset(); for (wliteral wl : m_wlits) { if (value(wl.second) == l_false) lits.push_back(wl.second); } unsigned glue = s().num_diff_levels(lits.size(), lits.c_ptr()); - c->set_glue(glue); } return c; @@ -3706,6 +3820,7 @@ namespace sat { // validate that m_A & m_B implies m_C bool ba_solver::validate_resolvent() { + return true; u_map coeffs; uint64 k = m_A.m_k + m_B.m_k; for (unsigned i = 0; i < m_A.m_lits.size(); ++i) { @@ -3745,7 +3860,6 @@ namespace sat { uint64 coeff; if (coeffs.find(lit.index(), coeff)) { if (coeff > m_C.m_coeffs[i] && m_C.m_coeffs[i] < m_C.m_k) { - IF_VERBOSE(0, verbose_stream() << i << ": " << m_C.m_coeffs[i] << " " << m_C.m_k << "\n";); goto violated; } coeffs.remove(lit.index()); @@ -3758,6 +3872,23 @@ namespace sat { return true; violated: + // last ditch effort by translating to SAT. + solver s0(s().m_params, s().rlimit()); + u_map translation; + literal l1 = translate_to_sat(s0, translation, m_A); + if (l1 == null_literal) return true; + literal l2 = translate_to_sat(s0, translation, m_B); + if (l2 == null_literal) return true; + ineq notC = negate(m_B); + literal l3 = translate_to_sat(s0, translation, notC); + if (l3 == null_literal) return true; + s0.assign(l1, justification()); + s0.assign(l2, justification()); + s0.assign(l3, justification()); + lbool is_sat = s0.check(); + TRACE("ba", s0.display(tout << "trying sat encoding");); + if (is_sat == l_false) return true; + IF_VERBOSE(0, display(verbose_stream(), m_A); display(verbose_stream(), m_B); @@ -3766,13 +3897,111 @@ namespace sat { verbose_stream() << to_literal(e.m_key) << ": " << e.m_value << "\n"; }); + UNREACHABLE(); return false; } + /** + \brief translate PB inequality to SAT formula. + */ + literal ba_solver::translate_to_sat(solver& s, u_map& translation, ineq const& pb) { + SASSERT(pb.m_k > 0); + if (pb.m_lits.size() > 1) { + ineq a, b; + a.reset(pb.m_k); + b.reset(pb.m_k); + for (unsigned i = 0; i < pb.m_lits.size()/2; ++i) { + a.push(pb.m_lits[i], pb.m_coeffs[i]); + } + for (unsigned i = pb.m_lits.size()/2; i < pb.m_lits.size(); ++i) { + b.push(pb.m_lits[i], pb.m_coeffs[i]); + } + bool_var v = s.mk_var(); + literal lit(v, false); + literal_vector lits; + lits.push_back(~lit); + push_lit(lits, translate_to_sat(s, translation, a)); + push_lit(lits, translate_to_sat(s, translation, b)); + push_lit(lits, translate_to_sat(s, translation, a, b)); + s.mk_clause(lits); + return lit; + } + if (pb.m_coeffs[0] >= pb.m_k) { + return translate_to_sat(s, translation, pb.m_lits[0]); + } + else { + return null_literal; + } + } + + /* + \brief encode the case where Sum(a) >= k-1 & Sum(b) >= 1 \/ ... \/ Sum(a) >= 1 & Sum(b) >= k-1 + */ + literal ba_solver::translate_to_sat(solver& s, u_map& translation, ineq& a, ineq& b) { + uint64 k0 = a.m_k; + literal_vector lits; + for (unsigned k = 1; k < a.m_k - 1; ++k) { + a.m_k = k; b.m_k = k0 - k; + literal lit1 = translate_to_sat(s, translation, a); + literal lit2 = translate_to_sat(s, translation, b); + if (lit1 != null_literal && lit2 != null_literal) { + bool_var v = s.mk_var(); + literal lit(v, false); + s.mk_clause(~lit, lit1); + s.mk_clause(~lit, lit2); + lits.push_back(lit); + } + } + a.m_k = k0; + b.m_k = k0; + switch (lits.size()) { + case 0: return null_literal; + case 1: return lits[0]; + default: { + bool_var v = s.mk_var(); + literal lit(v, false); + lits.push_back(~lit); + s.mk_clause(lits); + return lit; + } + } + } + + literal ba_solver::translate_to_sat(solver& s, u_map& translation, literal lit) { + bool_var v; + if (!translation.find(lit.var(), v)) { + v = s.mk_var(); + translation.insert(lit.var(), v); + } + return literal(v, lit.sign()); + } + + ba_solver::ineq ba_solver::negate(ineq const& a) const { + ineq result; + uint64 sum = 0; + for (unsigned i = 0; i < a.m_lits.size(); ++i) { + result.push(~a.m_lits[i], a.m_coeffs[i]); + sum += a.m_coeffs[i]; + } + SASSERT(sum >= a.m_k + 1); + result.m_k = sum + 1 - a.m_k; + return result; + } + + void ba_solver::push_lit(literal_vector& lits, literal lit) { + if (lit != null_literal) { + lits.push_back(lit); + } + } + bool ba_solver::validate_conflict(literal_vector const& lits, ineq& p) { for (literal l : lits) { if (value(l) != l_false) { - TRACE("sat", tout << "literal " << l << " is not false\n";); + TRACE("ba", tout << "literal " << l << " is not false\n";); + return false; + } + if (!p.m_lits.contains(l)) { + TRACE("ba", tout << "lemma contains literal " << l << " not in inequality\n";); return false; } } @@ -3783,7 +4012,7 @@ namespace sat { value += coeff; } } - CTRACE("sat", value >= p.m_k, tout << "slack: " << value << " bound " << p.m_k << "\n"; + CTRACE("ba", value >= p.m_k, tout << "slack: " << value << " bound " << p.m_k << "\n"; display(tout, p); tout << lits << "\n";); return value < p.m_k; diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h index 88a81701a..3e02d49dc 100644 --- a/src/sat/ba_solver.h +++ b/src/sat/ba_solver.h @@ -79,7 +79,7 @@ namespace sat { void set_size(unsigned sz) { SASSERT(sz <= m_size); m_size = sz; } void update_literal(literal l) { m_lit = l; } bool was_removed() const { return m_removed; } - void remove() { m_removed = true; } + void set_removed() { m_removed = true; } void nullify_literal() { m_lit = null_literal; } unsigned glue() const { return m_glue; } void set_glue(unsigned g) { m_glue = g; } @@ -199,7 +199,7 @@ namespace sat { svector m_coeffs; uint64 m_k; void reset(uint64 k) { m_lits.reset(); m_coeffs.reset(); m_k = k; } - void push(literal l, unsigned c) { m_lits.push_back(l); m_coeffs.push_back(c); } + void push(literal l, uint64 c) { m_lits.push_back(l); m_coeffs.push_back(c); } }; solver* m_solver; @@ -286,7 +286,7 @@ namespace sat { void cleanup_constraints(); void cleanup_constraints(ptr_vector& cs, bool learned); void ensure_external(constraint const& c); - void remove_constraint(constraint& c); + void remove_constraint(constraint& c, char const* reason); // constraints constraint& index2constraint(size_t idx) const { return *reinterpret_cast(idx); } @@ -304,6 +304,7 @@ namespace sat { void nullify_tracking_literal(constraint& c); void set_conflict(constraint& c, literal lit); void assign(constraint& c, literal lit); + bool assigned_above(literal above, literal below); void get_antecedents(literal l, constraint const& c, literal_vector & r); bool validate_conflict(constraint const& c) const; bool validate_unit_propagation(constraint const& c, literal alit) const; @@ -368,7 +369,7 @@ namespace sat { inline watch_list const& get_wlist(literal l) const { return m_lookahead ? m_lookahead->get_wlist(l) : m_solver->get_wlist(l); } inline void assign(literal l, justification j) { if (m_lookahead) m_lookahead->assign(l); else m_solver->assign(l, j); } inline void set_conflict(justification j, literal l) { if (m_lookahead) m_lookahead->set_conflict(); else m_solver->set_conflict(j, l); } - inline config const& get_config() const { return m_solver->get_config(); } + inline config const& get_config() const { return m_lookahead ? m_lookahead->get_config() : m_solver->get_config(); } inline void drat_add(literal_vector const& c, svector const& premises) { m_solver->m_drat.add(c, premises); } @@ -402,8 +403,13 @@ namespace sat { bool validate_watch_literals() const; bool validate_watch_literal(literal lit) const; bool validate_watched_constraint(constraint const& c) const; - bool validate_watch(pb const& p) const; + bool validate_watch(pb const& p, literal alit) const; bool is_watching(literal lit, constraint const& c) const; + literal translate_to_sat(solver& s, u_map& translation, ineq const& pb); + literal translate_to_sat(solver& s, u_map& translation, ineq& a, ineq& b); + literal translate_to_sat(solver& s, u_map& translation, literal lit); + ineq negate(ineq const& a) const; + void push_lit(literal_vector& lits, literal lit); ineq m_A, m_B, m_C; void active2pb(ineq& p); @@ -422,6 +428,7 @@ namespace sat { constraint* add_pb_ge(literal l, svector const& wlits, unsigned k, bool learned); constraint* add_xor(literal l, literal_vector const& lits, bool learned); + void copy_core(ba_solver* result); public: ba_solver(); virtual ~ba_solver(); @@ -447,6 +454,7 @@ namespace sat { virtual std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const; virtual void collect_statistics(statistics& st) const; virtual extension* copy(solver* s); + virtual extension* copy(lookahead* s); virtual void find_mutexes(literal_vector& lits, vector & mutexes); virtual void pop_reinit(); virtual void gc(); diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index 0f1b578f1..d3864fd8b 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -272,7 +272,8 @@ namespace sat { void drat::verify(unsigned n, literal const* c) { if (!is_drup(n, c) && !is_drat(n, c)) { std::cout << "Verification failed\n"; - display(std::cout); + UNREACHABLE(); + //display(std::cout); TRACE("sat", tout << literal_vector(n, c) << "\n"; display(tout); diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp index 8666218c6..7eb307f85 100644 --- a/src/sat/sat_elim_eqs.cpp +++ b/src/sat/sat_elim_eqs.cpp @@ -96,17 +96,18 @@ namespace sat { if (!c.frozen()) m_solver.detach_clause(c); // apply substitution - for (i = 0; i < sz; i++) { - SASSERT(!m_solver.was_eliminated(c[i].var())); + for (i = 0; i < sz; i++) { c[i] = norm(roots, c[i]); + VERIFY(!m_solver.was_eliminated(c[i].var())); } std::sort(c.begin(), c.end()); + for (literal l : c) VERIFY(l == norm(roots, l)); TRACE("sats", tout << "after normalization/sorting: " << c << "\n"; tout.flush();); DEBUG_CODE({ - for (unsigned i = 0; i < sz; i++) { - CTRACE("sats", c[i] != norm(roots, c[i]), tout << c[i] << " " << norm(roots, c[i]) << "\n"; tout.flush();); - SASSERT(c[i] == norm(roots, c[i])); - } }); + for (literal l : c) { + CTRACE("sat", l != norm(roots, l), tout << l << " " << norm(roots, l) << "\n"; tout.flush();); + SASSERT(l == norm(roots, l)); + } }); // remove duplicates, and check if it is a tautology literal l_prev = null_literal; unsigned j = 0; @@ -122,13 +123,11 @@ namespace sat { break; // clause was satisfied if (val == l_false) continue; // skip - if (i != j) { - std::swap(c[i], c[j]); - } + c[j] = l; j++; } if (i < sz) { - // clause is a tautology or was simplified + // clause is a tautology or was simplified to true m_solver.del_clause(c); continue; } @@ -164,10 +163,7 @@ namespace sat { else c.update_approx(); - DEBUG_CODE({ - for (unsigned i = 0; i < j; i++) { - SASSERT(c[i] == norm(roots, c[i])); - } }); + DEBUG_CODE(for (literal l : c) VERIFY(l == norm(roots, l));); *it2 = *it; it2++; @@ -187,7 +183,6 @@ namespace sat { literal r = roots[v]; SASSERT(v != r.var()); if (m_solver.is_external(v) && !m_solver.set_root(l, r)) { - std::cout << "skip: " << l << " == " << r << "\n"; // cannot really eliminate v, since we have to notify extension of future assignments m_solver.mk_bin_clause(~l, r, false); m_solver.mk_bin_clause(l, ~r, false); @@ -199,29 +194,33 @@ namespace sat { mc.insert(e, ~l, r); mc.insert(e, l, ~r); } - m_solver.flush_roots(); } + m_solver.flush_roots(); } - bool elim_eqs::check_clauses(literal_vector const & roots) const { - clause_vector * vs[2] = { &m_solver.m_clauses, &m_solver.m_learned }; - for (unsigned i = 0; i < 2; i++) { - clause_vector & cs = *(vs[i]); - clause_vector::iterator it = cs.begin(); - clause_vector::iterator end = cs.end(); - for (; it != end; ++it) { - clause & c = *(*it); - unsigned sz = c.size(); - for (unsigned i = 0; i < sz; i++) { - CTRACE("elim_eqs_bug", m_solver.was_eliminated(c[i].var()), tout << "lit: " << c[i] << " " << norm(roots, c[i]) << "\n"; - tout << c << "\n";); - SASSERT(!m_solver.was_eliminated(c[i].var())); - } + bool elim_eqs::check_clause(clause const& c, literal_vector const& roots) const { + for (literal l : c) { + CTRACE("elim_eqs_bug", m_solver.was_eliminated(l.var()), tout << "lit: " << l << " " << norm(roots, l) << "\n"; + tout << c << "\n";); + if (m_solver.was_eliminated(l.var())) { + IF_VERBOSE(0, verbose_stream() << c << " contains eliminated literal " << l << " " << norm(roots, l) << "\n";); + UNREACHABLE(); } } return true; } + + bool elim_eqs::check_clauses(literal_vector const & roots) const { + for (clause * cp : m_solver.m_clauses) + if (!check_clause(*cp, roots)) + return false; + for (clause * cp : m_solver.m_learned) + if (!check_clause(*cp, roots)) + return false; + return true; + } + void elim_eqs::operator()(literal_vector const & roots, bool_var_vector const & to_elim) { cleanup_bin_watches(roots); TRACE("elim_eqs", tout << "after bin cleanup\n"; m_solver.display(tout);); diff --git a/src/sat/sat_elim_eqs.h b/src/sat/sat_elim_eqs.h index 0422b60df..15c50097d 100644 --- a/src/sat/sat_elim_eqs.h +++ b/src/sat/sat_elim_eqs.h @@ -30,6 +30,7 @@ namespace sat { void cleanup_clauses(literal_vector const & roots, clause_vector & cs); void cleanup_bin_watches(literal_vector const & roots); bool check_clauses(literal_vector const & roots) const; + bool check_clause(clause const& c, literal_vector const& roots) const; public: elim_eqs(solver & s); void operator()(literal_vector const & roots, bool_var_vector const & to_elim); diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h index 1f747ae50..c2a9197c1 100644 --- a/src/sat/sat_extension.h +++ b/src/sat/sat_extension.h @@ -71,6 +71,7 @@ namespace sat { virtual std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const = 0; virtual void collect_statistics(statistics& st) const = 0; virtual extension* copy(solver* s) = 0; + virtual extension* copy(lookahead* s) = 0; virtual void find_mutexes(literal_vector& lits, vector & mutexes) = 0; virtual void gc() = 0; virtual void pop_reinit() = 0; diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 8f6cba598..cdbbb365b 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -92,7 +92,7 @@ namespace sat { // TRACE("sat", display(tout << "Delete " << to_literal(idx) << "\n");); literal_vector & lits = m_binary[idx]; SASSERT(!lits.empty()); - literal l = lits.back(); + literal l = lits.back(); lits.pop_back(); SASSERT(!m_binary[(~l).index()].empty()); IF_VERBOSE(0, if (m_binary[(~l).index()].back() != ~to_literal(idx)) verbose_stream() << "pop bad literal: " << idx << " " << (~l).index() << "\n";); @@ -112,7 +112,6 @@ namespace sat { } } - void lookahead::inc_bstamp() { ++m_bstamp_id; if (m_bstamp_id == 0) { @@ -120,6 +119,7 @@ namespace sat { m_bstamp.fill(0); } } + void lookahead::inc_istamp() { ++m_istamp_id; if (m_istamp_id == 0) { @@ -204,13 +204,13 @@ namespace sat { void lookahead::pre_select() { + IF_VERBOSE(10, verbose_stream() << "freevars: " << m_freevars.size() << "\n";); m_lookahead.reset(); - for (bool_var x : m_freevars) { // tree lookahead may leave some literals fixed in lower truth levels + for (bool_var x : m_freevars) { // tree lookahead leaves literals fixed in lower truth levels literal l(x, false); set_undef(l); set_undef(~l); } -//printf("m_freevars.size() = %d\n", m_freevars.size()); if (select(scope_lvl())) { get_scc(); if (inconsistent()) return; @@ -276,6 +276,7 @@ namespace sat { sift_down(0, i); } } + SASSERT(validate_heap_sort()); } void lookahead::heapify() { @@ -299,6 +300,17 @@ namespace sat { if (i > j) m_candidates[i] = c; } + /** + * \brief validate that the result of heap sort sorts the candidates + * in descending order of their rating. + */ + bool lookahead::validate_heap_sort() { + for (unsigned i = 0; i + 1 < m_candidates.size(); ++i) + if (m_candidates[i].m_rating < m_candidates[i + 1].m_rating) + return false; + return true; + } + double lookahead::init_candidates(unsigned level, bool newbies) { m_candidates.reset(); double sum = 0; @@ -328,25 +340,14 @@ namespace sat { } bool lookahead::is_unsat() const { - bool all_false = true; - bool first = true; // check if there is a clause whose literals are false. // every clause is terminated by a null-literal. - for (unsigned l_idx : m_nary_literals) { - literal l = to_literal(l_idx); - if (first) { - // skip the first entry, the length indicator. - first = false; - } - else if (l == null_literal) { - // when reaching the end of a clause check if all entries are false - if (all_false) return true; - all_false = true; - first = true; - } - else { + for (nary* n : m_nary_clauses) { + bool all_false = true; + for (literal l : *n) { all_false &= is_false(l); } + if (all_false) return true; } // check if there is a ternary whose literals are false. for (unsigned idx = 0; idx < m_ternary.size(); ++idx) { @@ -382,24 +383,14 @@ namespace sat { } } } - bool no_true = true; - bool first = true; // check if there is a clause whose literals are false. // every clause is terminated by a null-literal. - for (unsigned l_idx : m_nary_literals) { - literal l = to_literal(l_idx); - if (first) { - // skip the first entry, the length indicator. - first = false; - } - else if (l == null_literal) { - if (no_true) return false; - no_true = true; - first = true; - } - else { + for (nary * n : m_nary_clauses) { + bool no_true = true; + for (literal l : *n) { no_true &= !is_true(l); } + if (no_true) return false; } // check if there is a ternary whose literals are false. for (unsigned idx = 0; idx < m_ternary.size(); ++idx) { @@ -476,17 +467,15 @@ namespace sat { sum += (literal_occs(b.m_u) + literal_occs(b.m_v)) / 8.0; } sz = m_nary_count[(~l).index()]; - for (unsigned idx : m_nary[(~l).index()]) { + for (nary * n : m_nary[(~l).index()]) { if (sz-- == 0) break; - literal lit; - unsigned j = idx; double to_add = 0; - while ((lit = to_literal(m_nary_literals[++j])) != null_literal) { + for (literal lit : *n) { if (!is_fixed(lit) && lit != ~l) { to_add += literal_occs(lit); } } - unsigned len = m_nary_literals[idx]; + unsigned len = n->size(); sum += pow(0.5, len) * to_add / len; } return sum; @@ -507,9 +496,9 @@ namespace sat { } sum += 0.25 * m_ternary_count[(~l).index()]; unsigned sz = m_nary_count[(~l).index()]; - for (unsigned cls_idx : m_nary[(~l).index()]) { + for (nary * n : m_nary[(~l).index()]) { if (sz-- == 0) break; - sum += pow(0.5, m_nary_literals[cls_idx]); + sum += pow(0.5, n->size()); } return sum; } @@ -616,18 +605,18 @@ namespace sat { void lookahead::init_arcs(literal l) { literal_vector lits; literal_vector const& succ = m_binary[l.index()]; - for (unsigned i = 0; i < succ.size(); ++i) { - literal u = succ[i]; + for (literal u : succ) { SASSERT(u != l); + // l => u if (u.index() > l.index() && is_stamped(u)) { add_arc(~l, ~u); add_arc( u, l); } } for (auto w : m_watches[l.index()]) { - if (w.is_ext_constraint() && m_s.m_ext->is_extended_binary(w.get_ext_constraint_idx(), lits)) { + if (w.is_ext_constraint() && m_s.m_ext->is_extended_binary(w.get_ext_constraint_idx(), lits)) { for (literal u : lits) { - if (u.index() > l.index() && is_stamped(u)) { + if (u.index() > (~l).index() && is_stamped(u)) { add_arc(~l, ~u); add_arc( u, l); } @@ -901,8 +890,8 @@ namespace sat { m_ternary.push_back(svector()); m_ternary_count.push_back(0); m_ternary_count.push_back(0); - m_nary.push_back(unsigned_vector()); - m_nary.push_back(unsigned_vector()); + m_nary.push_back(ptr_vector()); + m_nary.push_back(ptr_vector()); m_nary_count.push_back(0); m_nary_count.push_back(0); m_bstamp.push_back(0); @@ -958,14 +947,8 @@ namespace sat { } } - // copy externals: - for (unsigned idx = 0; idx < m_s.m_watches.size(); ++idx) { - watch_list const& wl = m_s.m_watches[idx]; - for (watched const& w : wl) { - if (w.is_ext_constraint()) { - m_watches[idx].push_back(w); - } - } + if (m_s.m_ext) { + m_ext = m_s.m_ext->copy(this); } propagate(); m_qhead = m_trail.size(); @@ -1328,17 +1311,14 @@ namespace sat { // new n-ary clause managment void lookahead::add_clause(clause const& c) { - unsigned sz = c.size(); - SASSERT(sz > 3); - unsigned idx = m_nary_literals.size(); - m_nary_literals.push_back(sz); + SASSERT(c.size() > 3); + void * mem = m_allocator.allocate(nary::get_obj_size(c.size())); + nary * n = new (mem) nary(c.size(), c.begin()); + m_nary_clauses.push_back(n); for (literal l : c) { - m_nary_literals.push_back(l.index()); + m_nary[l.index()].push_back(n); m_nary_count[l.index()]++; - m_nary[l.index()].push_back(idx); - SASSERT(m_nary_count[l.index()] == m_nary[l.index()].size()); } - m_nary_literals.push_back(null_literal.index()); } @@ -1347,18 +1327,17 @@ namespace sat { unsigned sz = m_nary_count[(~l).index()]; literal lit; SASSERT(m_search_mode == lookahead_mode::searching); - for (unsigned idx : m_nary[(~l).index()]) { + for (nary * n : m_nary[(~l).index()]) { if (sz-- == 0) break; - unsigned len = --m_nary_literals[idx]; + unsigned len = n->dec_size(); if (m_inconsistent) continue; if (len <= 1) continue; // already processed // find the two unassigned literals, if any if (len == 2) { literal l1 = null_literal; literal l2 = null_literal; - unsigned j = idx; bool found_true = false; - while ((lit = to_literal(m_nary_literals[++j])) != null_literal) { + for (literal lit : *n) { if (!is_fixed(lit)) { if (l1 == null_literal) { l1 = lit; @@ -1370,7 +1349,7 @@ namespace sat { } } else if (is_true(lit)) { - // can't swap with idx. std::swap(m_nary_literals[j], m_nary_literals[idx]); + n->set_head(lit); found_true = true; break; } @@ -1398,9 +1377,9 @@ namespace sat { } // clauses where l is positive: sz = m_nary_count[l.index()]; - for (unsigned idx : m_nary[l.index()]) { + for (nary* n : m_nary[l.index()]) { if (sz-- == 0) break; - remove_clause_at(l, idx); + remove_clause_at(l, *n); } } @@ -1411,14 +1390,17 @@ namespace sat { SASSERT(m_search_mode == lookahead_mode::lookahead1 || m_search_mode == lookahead_mode::lookahead2); - for (unsigned idx : m_nary[(~l).index()]) { + for (nary* n : m_nary[(~l).index()]) { if (sz-- == 0) break; + + if (is_true(n->get_head())) { + continue; + } literal l1 = null_literal; literal l2 = null_literal; - unsigned j = idx; - bool found_true = false; + bool skip_clause = false; unsigned nonfixed = 0; - while ((lit = to_literal(m_nary_literals[++j])) != null_literal) { + for (literal lit : *n) { if (!is_fixed(lit)) { ++nonfixed; if (l1 == null_literal) { @@ -1427,14 +1409,19 @@ namespace sat { else if (l2 == null_literal) { l2 = lit; } + else if (m_search_mode == lookahead_mode::lookahead2) { + skip_clause = true; + break; + } } else if (is_true(lit)) { - found_true = true; + n->set_head(lit); + skip_clause = true; break; } } - if (found_true) { - // skip, the clause will be removed when propagating on 'lit' + if (skip_clause) { + // skip, the clause } else if (l1 == null_literal) { set_conflict(); @@ -1443,20 +1430,16 @@ namespace sat { else if (l2 == null_literal) { propagated(l1); } - else if (m_search_mode == lookahead_mode::lookahead2) { - continue; - } else { SASSERT(nonfixed >= 2); SASSERT(m_search_mode == lookahead_mode::lookahead1); switch (m_config.m_reward_type) { case heule_schur_reward: { - j = idx; double to_add = 0; - while ((lit = to_literal(m_nary_literals[++j])) != null_literal) { + for (literal lit : *n) { if (!is_fixed(lit)) { to_add += literal_occs(lit); - } + } } m_lookahead_reward += pow(0.5, nonfixed) * to_add / nonfixed; break; @@ -1464,9 +1447,6 @@ namespace sat { case heule_unit_reward: m_lookahead_reward += pow(0.5, nonfixed); break; - case march_cu_reward: - m_lookahead_reward += 3.3 * pow(0.5, nonfixed - 2); - break; case ternary_reward: if (nonfixed == 2) { m_lookahead_reward += (*m_heur)[l1.index()] * (*m_heur)[l2.index()]; @@ -1482,23 +1462,20 @@ namespace sat { } } - - void lookahead::remove_clause_at(literal l, unsigned clause_idx) { - unsigned j = clause_idx; - literal lit; - while ((lit = to_literal(m_nary_literals[++j])) != null_literal) { + void lookahead::remove_clause_at(literal l, nary& n) { + for (literal lit : n) { if (lit != l) { - remove_clause(lit, clause_idx); + remove_clause(lit, n); } } } - void lookahead::remove_clause(literal l, unsigned clause_idx) { - unsigned_vector& pclauses = m_nary[l.index()]; + void lookahead::remove_clause(literal l, nary& n) { + ptr_vector& pclauses = m_nary[l.index()]; unsigned sz = m_nary_count[l.index()]--; for (unsigned i = sz; i > 0; ) { --i; - if (clause_idx == pclauses[i]) { + if (&n == pclauses[i]) { std::swap(pclauses[i], pclauses[sz-1]); return; } @@ -1508,33 +1485,29 @@ namespace sat { void lookahead::restore_clauses(literal l) { SASSERT(m_search_mode == lookahead_mode::searching); - // increase the length of clauses where l is negative unsigned sz = m_nary_count[(~l).index()]; - for (unsigned idx : m_nary[(~l).index()]) { + for (nary* n : m_nary[(~l).index()]) { if (sz-- == 0) break; - ++m_nary_literals[idx]; + n->inc_size(); } - // add idx back to clause list where l is positive // add them back in the same order as they were inserted // in this way we can check that the clauses are the same. sz = m_nary_count[l.index()]; - unsigned_vector const& pclauses = m_nary[l.index()]; - for (unsigned i = sz; i > 0; ) { - --i; - unsigned j = pclauses[i]; - literal lit; - while ((lit = to_literal(m_nary_literals[++j])) != null_literal) { + ptr_vector& pclauses = m_nary[l.index()]; + for (unsigned i = sz; i-- > 0; ) { + for (literal lit : *pclauses[i]) { if (lit != l) { SASSERT(m_nary[lit.index()][m_nary_count[lit.index()]] == pclauses[i]); m_nary_count[lit.index()]++; } } - } + } } void lookahead::propagate_clauses(literal l) { + SASSERT(is_true(l)); propagate_ternary(l); switch (m_search_mode) { case lookahead_mode::searching: @@ -1545,9 +1518,7 @@ namespace sat { break; } propagate_external(l); - } - - + } void lookahead::update_binary_clause_reward(literal l1, literal l2) { SASSERT(!is_false(l1)); @@ -1610,7 +1581,6 @@ namespace sat { // FIXME: counts occurences of ~l; misleading double lookahead::literal_occs(literal l) { double result = m_binary[l.index()].size(); - //unsigned_vector const& nclauses = m_nary[(~l).index()]; result += literal_big_occs(l); return result; } @@ -1651,12 +1621,18 @@ namespace sat { TRACE("sat_verbose", display(tout << scope_lvl() << " " << (inconsistent()?"unsat":"sat") << "\n");); } +#define CHECK_FAILED_LITERAL 0 + void lookahead::compute_lookahead_reward() { TRACE("sat", display_lookahead(tout); ); m_delta_decrease = pow(m_config.m_delta_rho, 1.0 / (double)m_lookahead.size()); unsigned base = 2; bool change = true; literal last_changed = null_literal; +#if CHECK_FAILED_LITERAL + unsigned_vector assigns; + literal_vector assigns_lits; +#endif while (change && !inconsistent()) { change = false; for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) { @@ -1677,7 +1653,6 @@ namespace sat { reset_lookahead_reward(lit); unsigned num_units = push_lookahead1(lit, level); update_lookahead_reward(lit, level); - unsigned old_trail_sz = m_trail.size(); unsigned dl_lvl = level; num_units += do_double(lit, dl_lvl); if (dl_lvl > level) { @@ -1688,6 +1663,10 @@ namespace sat { if (unsat) { TRACE("sat", tout << "backtracking and settting " << ~lit << "\n";); lookahead_backtrack(); +#if CHECK_FAILED_LITERAL + assigns.push_back(m_trail.size()); + assigns_lits.push_back(~lit); +#endif assign(~lit); propagate(); change = true; @@ -1701,6 +1680,12 @@ namespace sat { base += 2 * m_lookahead.size(); } lookahead_backtrack(); +#if CHECK_FAILED_LITERAL + for (unsigned i = 0; i < assigns.size(); ++i) { + std::cout << "check trail: " << m_trail[assigns[i]] << " " << assigns_lits[i] << "\n"; + VERIFY(m_trail[assigns[i]] == assigns_lits[i]); + } +#endif TRACE("sat", display_lookahead(tout); ); } @@ -1754,7 +1739,7 @@ namespace sat { return false; #if 0 // no propagations are allowed to reduce clauses. - for (clause * cp : m_full_watches[l.index()]) { + for (nary * cp : m_nary[(~l).index()]) { clause& c = *cp; unsigned sz = c.size(); bool found = false; @@ -1993,8 +1978,10 @@ namespace sat { lbool lookahead::cube() { literal_vector lits; + bool_var_vector vars; + for (bool_var v : m_freevars) vars.push_back(v); while (true) { - lbool result = cube(lits); + lbool result = cube(vars, lits); if (lits.empty() || result != l_undef) { return l_undef; } @@ -2003,8 +1990,13 @@ namespace sat { return l_undef; } - lbool lookahead::cube(literal_vector& lits) { + lbool lookahead::cube(bool_var_vector const& vars, literal_vector& lits) { + scoped_ext _scoped_ext(*this); lits.reset(); + m_select_lookahead_vars.reset(); + for (auto v : vars) { + m_select_lookahead_vars.insert(v); + } bool is_first = m_cube_state.m_first; if (is_first) { init_search(); @@ -2111,20 +2103,9 @@ namespace sat { } } - for (unsigned l_idx : m_nary_literals) { - literal l = to_literal(l_idx); - if (first) { - // the first entry is a length indicator of non-false literals. - out << l_idx << ": "; - first = false; - } - else if (l == null_literal) { - first = true; - out << "\n"; - } - else { - out << l << " "; - } + for (nary * n : m_nary_clauses) { + for (literal l : *n) out << l << " "; + out << "\n"; } return out; @@ -2219,6 +2200,7 @@ namespace sat { \brief simplify set of clauses by extracting units from a lookahead at base level. */ void lookahead::simplify() { + scoped_ext _scoped_ext(*this); SASSERT(m_prefix == 0); SASSERT(m_watches.empty()); m_search_mode = lookahead_mode::searching; diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 56015571d..fce4fd636 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -20,6 +20,7 @@ Notes: #ifndef _SAT_LOOKAHEAD_H_ #define _SAT_LOOKAHEAD_H_ +// #define OLD_NARY 0 #include "sat_elim_eqs.h" @@ -89,8 +90,7 @@ namespace sat { m_min_cutoff = 30; m_preselect = false; m_level_cand = 600; - //m_delta_rho = (double)0.25; - m_delta_rho = (double)0.5; + m_delta_rho = (double)0.25; m_dl_max_iterations = 2; m_tc1_limit = 10000000; m_reward_type = ternary_reward; @@ -132,6 +132,36 @@ namespace sat { literal m_u, m_v; }; + class nary { + unsigned m_size; // number of non-false literals + size_t m_obj_size; // object size (counting all literals) + literal m_head; // head literal + literal m_literals[0]; // list of literals, put any true literal in head. + size_t num_lits() const { + return (m_obj_size - sizeof(nary)) / sizeof(literal); + } + public: + static size_t get_obj_size(unsigned sz) { return sizeof(nary) + sz * sizeof(literal); } + size_t obj_size() const { return m_obj_size; } + nary(unsigned sz, literal const* lits): + m_size(sz), + m_obj_size(get_obj_size(sz)) { + for (unsigned i = 0; i < sz; ++i) m_literals[i] = lits[i]; + m_head = lits[0]; + } + unsigned size() const { return m_size; } + unsigned dec_size() { SASSERT(m_size > 0); return --m_size; } + void inc_size() { SASSERT(m_size < num_lits()); ++m_size; } + literal get_head() const { return m_head; } + void set_head(literal l) { m_head = l; } + + literal operator[](unsigned i) { SASSERT(i < num_lits()); return m_literals[i]; } + literal const* begin() const { return m_literals; } + literal const* end() const { return m_literals + num_lits(); } + // swap the true literal to the head. + // void swap(unsigned i, unsigned j) { SASSERT(i < num_lits() && j < num_lits()); std::swap(m_literals[i], m_literals[j]); } + }; + struct cube_state { bool m_first; svector m_is_decision; @@ -164,10 +194,10 @@ namespace sat { vector> m_ternary; // lit |-> vector of ternary clauses unsigned_vector m_ternary_count; // lit |-> current number of active ternary clauses for lit - vector m_nary; // lit |-> vector of clause_id - unsigned_vector m_nary_count; // lit |-> number of valid clause_id in m_clauses2[lit] - unsigned_vector m_nary_literals; // the actual literals, clauses start at offset clause_id, - // the first entry is the current length, clauses are separated by a null_literal + small_object_allocator m_allocator; + vector> m_nary; // lit |-> vector of nary clauses + ptr_vector m_nary_clauses; // vector of all nary clauses + unsigned_vector m_nary_count; // lit |-> number of valid clause_id in m_nary[lit] unsigned m_num_tc1; unsigned_vector m_num_tc1_lim; @@ -196,6 +226,7 @@ namespace sat { stats m_stats; model m_model; cube_state m_cube_state; + scoped_ptr m_ext; // --------------------------------------- // truth values @@ -293,10 +324,10 @@ namespace sat { double get_rating(bool_var v) const { return m_rating[v]; } double get_rating(literal l) const { return get_rating(l.var()); } bool select(unsigned level); - //void sift_up(unsigned j); void heap_sort(); - void heapify(); + void heapify(); void sift_down(unsigned j, unsigned sz); + bool validate_heap_sort(); double init_candidates(unsigned level, bool newbies); std::ostream& display_candidates(std::ostream& out) const; bool is_unsat() const; @@ -419,15 +450,15 @@ namespace sat { void propagate_clauses_searching(literal l); void propagate_clauses_lookahead(literal l); void restore_clauses(literal l); - void remove_clause(literal l, unsigned clause_idx); - void remove_clause_at(literal l, unsigned clause_idx); - + void remove_clause(literal l, nary& n); + void remove_clause_at(literal l, nary& n); // ------------------------------------ // initialization void init_var(bool_var v); void init(); void copy_clauses(clause_vector const& clauses, bool learned); + nary * copy_clause(clause const& c); // ------------------------------------ // search @@ -510,6 +541,9 @@ namespace sat { ~lookahead() { m_s.rlimit().pop_child(); + for (nary* n : m_nary_clauses) { + m_allocator.deallocate(n->obj_size(), n); + } } @@ -524,9 +558,10 @@ namespace sat { If cut-depth != 0, then it is used to control the depth of cuts. Otherwise, cut-fraction gives an adaptive threshold for creating cuts. */ + lbool cube(); - lbool cube(literal_vector& lits); + lbool cube(bool_var_vector const& vars, literal_vector& lits); literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars); /** @@ -557,6 +592,8 @@ namespace sat { double literal_occs(literal l); double literal_big_occs(literal l); + + sat::config const& get_config() const { return m_s.get_config(); } }; } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index cc79e75ff..8004c9635 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -162,6 +162,7 @@ namespace sat { m_user_scope_literals.append(src.m_user_scope_literals); m_mc = src.m_mc; + m_stats.m_units = init_trail_size(); } // ----------------------- @@ -837,11 +838,11 @@ namespace sat { return lh.select_lookahead(assumptions, vars); } - lbool solver::cube(literal_vector& lits) { + lbool solver::cube(bool_var_vector const& vars, literal_vector& lits) { if (!m_cuber) { m_cuber = alloc(lookahead, *this); } - lbool result = m_cuber->cube(lits); + lbool result = m_cuber->cube(vars, lits); if (result == l_false) { dealloc(m_cuber); m_cuber = nullptr; @@ -858,6 +859,7 @@ namespace sat { lbool solver::check(unsigned num_lits, literal const* lits) { init_reason_unknown(); pop_to_base_level(); + m_stats.m_units = init_trail_size(); IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";); SASSERT(at_base_lvl()); if (m_config.m_dimacs_display) { @@ -1468,11 +1470,14 @@ namespace sat { lh.simplify(); lh.collect_statistics(m_aux_stats); } +#if 0 + // Buggy { lookahead lh(*this); lh.scc(); lh.collect_statistics(m_aux_stats); } +#endif } @@ -2823,6 +2828,7 @@ namespace sat { pop(num_scopes); exchange_par(); reinit_assumptions(); + m_stats.m_units = init_trail_size(); } void solver::pop(unsigned num_scopes) { @@ -3048,7 +3054,6 @@ namespace sat { m_probing.updt_params(p); m_scc.updt_params(p); m_rand.set_seed(m_config.m_random_seed); - m_step_size = m_config.m_step_size_init; } @@ -4032,25 +4037,11 @@ namespace sat { st.update("minimized lits", m_minimized_lits); st.update("dyn subsumption resolution", m_dyn_sub_res); st.update("blocked correction sets", m_blocked_corr_sets); + st.update("units", m_units); } void stats::reset() { - m_mk_var = 0; - m_mk_bin_clause = 0; - m_mk_ter_clause = 0; - m_mk_clause = 0; - m_conflict = 0; - m_propagate = 0; - m_bin_propagate = 0; - m_ter_propagate = 0; - m_decision = 0; - m_restart = 0; - m_gc_clause = 0; - m_del_clause = 0; - m_minimized_lits = 0; - m_dyn_sub_res = 0; - m_non_learned_generation = 0; - m_blocked_corr_sets = 0; + memset(this, 0, sizeof(*this)); } void mk_stat::display(std::ostream & out) const { diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index c115b71bb..020c1dc42 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -67,6 +67,7 @@ namespace sat { unsigned m_dyn_sub_res; unsigned m_non_learned_generation; unsigned m_blocked_corr_sets; + unsigned m_units; stats() { reset(); } void reset(); void collect_statistics(statistics & st) const; @@ -364,7 +365,7 @@ namespace sat { char const* get_reason_unknown() const { return m_reason_unknown.c_str(); } literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars); - lbool cube(literal_vector& lits); + lbool cube(bool_var_vector const& vars, literal_vector& lits); protected: unsigned m_conflicts_since_init; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 908e56da8..53383a7c2 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -353,8 +353,12 @@ public: m_internalized = true; } convert_internalized(); + sat::bool_var_vector vars; + for (auto& kv : m_map) { + vars.push_back(kv.m_value); + } sat::literal_vector lits; - lbool result = m_solver.cube(lits); + lbool result = m_solver.cube(vars, lits); if (result == l_false || lits.empty()) { return expr_ref(m.mk_false(), m); } diff --git a/src/sat/sat_watched.h b/src/sat/sat_watched.h index 2bbf8aa77..d1333c314 100644 --- a/src/sat/sat_watched.h +++ b/src/sat/sat_watched.h @@ -109,10 +109,10 @@ namespace sat { bool operator!=(watched const & w) const { return !operator==(w); } }; - COMPILE_TIME_ASSERT(0 <= watched::BINARY && watched::BINARY <= 3); - COMPILE_TIME_ASSERT(0 <= watched::TERNARY && watched::TERNARY <= 3); - COMPILE_TIME_ASSERT(0 <= watched::CLAUSE && watched::CLAUSE <= 3); - COMPILE_TIME_ASSERT(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 3); + static_assert(0 <= watched::BINARY && watched::BINARY <= 3, ""); + static_assert(0 <= watched::TERNARY && watched::TERNARY <= 3, ""); + static_assert(0 <= watched::CLAUSE && watched::CLAUSE <= 3, ""); + static_assert(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 3, ""); struct watched_lt { bool operator()(watched const & w1, watched const & w2) const { diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 75561ed86..3db2908ed 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -120,7 +120,7 @@ struct goal2sat::imp { sat::bool_var mk_true() { if (m_true == sat::null_bool_var) { // create fake variable to represent true; - m_true = m_solver.mk_var(); + m_true = m_solver.mk_var(false); mk_clause(sat::literal(m_true, false)); // v is true } return m_true; diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 8d2785ac9..55b79ae66 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -170,7 +170,7 @@ void asserted_formulas::get_assertions(ptr_vector & result) const { void asserted_formulas::push_scope() { SASSERT(inconsistent() || m_qhead == m_formulas.size() || m.canceled()); - TRACE("asserted_formulas_scopes", tout << "push:\n"; display(tout);); + TRACE("asserted_formulas_scopes", tout << "before push: " << m_scopes.size() << "\n";); m_scoped_substitution.push(); m_scopes.push_back(scope()); scope & s = m_scopes.back(); @@ -181,10 +181,11 @@ void asserted_formulas::push_scope() { m_bv_sharing.push_scope(); m_macro_manager.push_scope(); commit(); + TRACE("asserted_formulas_scopes", tout << "after push: " << m_scopes.size() << "\n";); } void asserted_formulas::pop_scope(unsigned num_scopes) { - TRACE("asserted_formulas_scopes", tout << "before pop " << num_scopes << "\n"; display(tout);); + TRACE("asserted_formulas_scopes", tout << "before pop " << num_scopes << " of " << m_scopes.size() << "\n";); m_bv_sharing.pop_scope(num_scopes); m_macro_manager.pop_scope(num_scopes); unsigned new_lvl = m_scopes.size() - num_scopes; @@ -196,7 +197,7 @@ void asserted_formulas::pop_scope(unsigned num_scopes) { m_qhead = s.m_formulas_lim; m_scopes.shrink(new_lvl); flush_cache(); - TRACE("asserted_formulas_scopes", tout << "after pop " << num_scopes << "\n"; display(tout);); + TRACE("asserted_formulas_scopes", tout << "after pop " << num_scopes << "\n";); } void asserted_formulas::reset() { diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 011f222f3..8e95e13ac 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -487,6 +487,7 @@ namespace smt { */ void context::add_eq(enode * n1, enode * n2, eq_justification js) { unsigned old_trail_size = m_trail_stack.size(); + scoped_suspend_rlimit _suspend_cancel(m_manager.limit()); try { TRACE("add_eq", tout << "assigning: #" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";); @@ -541,10 +542,14 @@ namespace smt { mark_as_relevant(r1); } + TRACE("add_eq", tout << "to trail\n";); + push_trail(add_eq_trail(r1, n1, r2->get_num_parents())); + TRACE("add_eq", tout << "qmanager add_eq\n";); m_qmanager->add_eq_eh(r1, r2); + TRACE("add_eq", tout << "merge theory_vars\n";); merge_theory_vars(n2, n1, js); // 'Proof' tree @@ -577,6 +582,7 @@ namespace smt { #endif + TRACE("add_eq", tout << "remove_parents_from_cg_table\n";); remove_parents_from_cg_table(r1); enode * curr = r1; @@ -588,8 +594,10 @@ namespace smt { SASSERT(r1->get_root() == r2); + TRACE("add_eq", tout << "reinsert_parents_into_cg_table\n";); reinsert_parents_into_cg_table(r1, r2, n1, n2, js); + TRACE("add_eq", tout << "propagate_bool_enode_assignment\n";); if (n2->is_bool()) propagate_bool_enode_assignment(r1, r2, n1, n2); @@ -604,6 +612,7 @@ namespace smt { catch (...) { // Restore trail size since procedure was interrupted in the middle. // If the add_eq_trail remains on the trail stack, then Z3 may crash when the destructor is invoked. + TRACE("add_eq", tout << "add_eq interrupted. This is unsafe " << m_manager.limit().get_cancel_flag() << "\n";); m_trail_stack.shrink(old_trail_size); throw; } @@ -972,7 +981,7 @@ namespace smt { enode * parent = *it; if (parent->is_cgc_enabled()) { TRACE("add_eq_parents", tout << "removing: #" << parent->get_owner_id() << "\n";); - CTRACE("add_eq", !parent->is_cgr(), + CTRACE("add_eq", !parent->is_cgr() || !m_cg_table.contains_ptr(parent), tout << "old num_parents: " << r2_num_parents << ", num_parents: " << r2->m_parents.size() << ", parent: #" << parent->get_owner_id() << ", parents: \n"; for (unsigned i = 0; i < r2->m_parents.size(); i++) { diff --git a/src/smt/smt_implied_equalities.cpp b/src/smt/smt_implied_equalities.cpp index 7d54e714e..d021708fc 100644 --- a/src/smt/smt_implied_equalities.cpp +++ b/src/smt/smt_implied_equalities.cpp @@ -284,7 +284,7 @@ namespace smt { } lbool reduce_cond(model_ref& model, expr* e) { - expr* e1, *e2; + expr* e1 = 0, *e2 = 0; if (m.is_eq(e, e1, e2) && m_array_util.is_as_array(e1) && m_array_util.is_as_array(e2)) { if (e1 == e2) { return l_true; diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp index 60a7e1c25..f803b6690 100644 --- a/src/smt/smt_model_generator.cpp +++ b/src/smt/smt_model_generator.cpp @@ -54,7 +54,7 @@ namespace smt { ptr_vector::const_iterator it = m_context->begin_theories(); ptr_vector::const_iterator end = m_context->end_theories(); for (; it != end; ++it) { - TRACE("model_generator_bug", tout << "init_model for theory: " << (*it)->get_name() << "\n";); + TRACE("model", tout << "init_model for theory: " << (*it)->get_name() << "\n";); (*it)->init_model(*this); } } @@ -91,7 +91,7 @@ namespace smt { sort * s = m_manager.get_sort(r->get_owner()); model_value_proc * proc = 0; if (m_manager.is_bool(s)) { - CTRACE("func_interp_bug", m_context->get_assignment(r) == l_undef, + CTRACE("model", m_context->get_assignment(r) == l_undef, tout << mk_pp(r->get_owner(), m_manager) << "\n";); SASSERT(m_context->get_assignment(r) != l_undef); if (m_context->get_assignment(r) == l_true) @@ -108,7 +108,7 @@ namespace smt { SASSERT(proc); } else { - TRACE("model_bug", tout << "creating fresh value for #" << r->get_owner_id() << "\n";); + TRACE("model", tout << "creating fresh value for #" << r->get_owner_id() << "\n";); proc = alloc(fresh_value_proc, mk_extra_fresh_value(m_manager.get_sort(r->get_owner()))); } } @@ -130,7 +130,7 @@ namespace smt { if (!m_manager.is_model_value(n)) { sort * s = m_manager.get_sort(r->get_owner()); n = m_model->get_fresh_value(s); - CTRACE("model_generator_bug", n == 0, + CTRACE("model", n == 0, tout << mk_pp(r->get_owner(), m_manager) << "\nsort:\n" << mk_pp(s, m_manager) << "\n"; tout << "is_finite: " << m_model->is_finite(s) << "\n";); } @@ -407,9 +407,11 @@ namespace smt { */ bool model_generator::include_func_interp(func_decl * f) const { family_id fid = f->get_family_id(); + TRACE("model", tout << f->get_name() << " " << fid << "\n";); if (fid == null_family_id) return !m_hidden_ufs.contains(f); if (fid == m_manager.get_basic_family_id()) return false; theory * th = m_context->get_theory(fid); + TRACE("model", tout << th << "\n";); if (!th) return true; return th->include_func_interp(f); } @@ -444,7 +446,7 @@ namespace smt { SASSERT(m_model->has_interpretation(f)); SASSERT(m_model->get_func_interp(f) == fi); // The entry must be new because n->get_cg() == n - TRACE("func_interp_bug", + TRACE("model", tout << "insert new entry for:\n" << mk_ismt2_pp(n->get_owner(), m_manager) << "\nargs: "; for (unsigned i = 0; i < num_args; i++) { tout << "#" << n->get_arg(i)->get_owner_id() << " "; @@ -508,20 +510,20 @@ namespace smt { void model_generator::register_macros() { unsigned num = m_context->get_num_macros(); - TRACE("register_macros", tout << "num. macros: " << num << "\n";); + TRACE("model", tout << "num. macros: " << num << "\n";); expr_ref v(m_manager); for (unsigned i = 0; i < num; i++) { func_decl * f = m_context->get_macro_interpretation(i, v); func_interp * fi = alloc(func_interp, m_manager, f->get_arity()); fi->set_else(v); - TRACE("register_macros", tout << f->get_name() << "\n" << mk_pp(v, m_manager) << "\n";); + TRACE("model", tout << f->get_name() << "\n" << mk_pp(v, m_manager) << "\n";); m_model->register_decl(f, fi); } } proto_model * model_generator::mk_model() { SASSERT(!m_model); - TRACE("func_interp_bug", m_context->display(tout);); + TRACE("model", m_context->display(tout);); init_model(); register_existing_model_values(); mk_bool_model(); diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 858ff2a31..caccb1eef 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -216,6 +216,7 @@ namespace smt { void setup::setup_QF_DT() { setup_QF_UF(); + setup_datatypes(); } void setup::setup_QF_BVRE() { diff --git a/src/smt/smt_theory_var_list.h b/src/smt/smt_theory_var_list.h index d7e246824..aa2816786 100644 --- a/src/smt/smt_theory_var_list.h +++ b/src/smt/smt_theory_var_list.h @@ -67,9 +67,9 @@ namespace smt { }; // 32 bit machine - COMPILE_TIME_ASSERT(sizeof(expr*) != 4 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int)); + static_assert(sizeof(expr*) != 4 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int), "32 bit"); // 64 bit machine - COMPILE_TIME_ASSERT(sizeof(expr*) != 8 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int) + /* a structure must be aligned */ sizeof(int)); + static_assert(sizeof(expr*) != 8 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int) + /* a structure must be aligned */ sizeof(int), "64 bit"); }; #endif /* SMT_THEORY_VAR_LIST_H_ */ diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index a04c34706..230b6de77 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -780,7 +780,7 @@ namespace smt { of a non linear monomial that is not satisfied by the current assignment. if v >= l, then create the case split v >= l+1 else v <= u, then create the case split v <= u-1 - else do nothing and return false. + else create the bound v = 0 and case split on it. */ template bool theory_arith::branch_nl_int_var(theory_var v) { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 0bb76cd90..292d2ab0d 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -689,7 +689,7 @@ namespace smt { SASSERT(!ctx().b_internalized(atom)); bool_var bv = ctx().mk_bool_var(atom); ctx().set_var_theory(bv, get_id()); - expr* n1, *n2; + expr* n1 = 0, *n2 = 0; rational r; lra_lp::bound_kind k; theory_var v = null_theory_var; @@ -721,7 +721,7 @@ namespace smt { SASSERT(!ctx().b_internalized(atom)); bool_var bv = ctx().mk_bool_var(atom); ctx().set_var_theory(bv, get_id()); - expr* n1, *n2; + expr* n1 = 0, *n2 = 0; rational r; lra_lp::bound_kind k; theory_var v = null_theory_var; @@ -862,7 +862,7 @@ namespace smt { void relevant_eh(app* n) { TRACE("arith", tout << mk_pp(n, m) << "\n";); - expr* n1, *n2; + expr* n1 = 0, *n2 = 0; if (a.is_mod(n, n1, n2)) mk_idiv_mod_axioms(n1, n2); else if (a.is_rem(n, n1, n2)) diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 12fddee13..92f66f4b6 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -474,7 +474,6 @@ namespace smt { if (pb.is_aux_bool(atom)) { bool_var abv = ctx.mk_bool_var(atom); ctx.set_var_theory(abv, get_id()); - std::cout << "aux bool " << ctx.get_scope_level() << " " << mk_pp(atom, get_manager()) << " " << literal(abv) << "\n"; return true; } diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index d2cd0d66c..44f920840 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -18,6 +18,7 @@ Author: #include "tactic/bv/bv_bounds_tactic.h" #include "tactic/core/ctx_simplify_tactic.h" +#include "tactic/core/dom_simplify_tactic.h" #include "ast/bv_decl_plugin.h" #include "ast/ast_pp.h" #include @@ -29,507 +30,785 @@ static uint64 uMaxInt(unsigned sz) { namespace { -struct interval { - // l < h: [l, h] - // l > h: [0, h] U [l, UMAX_INT] - uint64 l, h; - unsigned sz; - bool tight; + struct interval { + // l < h: [l, h] + // l > h: [0, h] U [l, UMAX_INT] + uint64 l, h; + unsigned sz; + bool tight; - interval() {} - interval(uint64 l, uint64 h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) { - // canonicalize full set - if (is_wrapped() && l == h + 1) { - this->l = 0; - this->h = uMaxInt(sz); - } - SASSERT(invariant()); - } - - bool invariant() const { - return l <= uMaxInt(sz) && h <= uMaxInt(sz) && - (!is_wrapped() || l != h+1); - } - - bool is_full() const { return l == 0 && h == uMaxInt(sz); } - bool is_wrapped() const { return l > h; } - bool is_singleton() const { return l == h; } - - bool operator==(const interval& b) const { - SASSERT(sz == b.sz); - return l == b.l && h == b.h && tight == b.tight; - } - bool operator!=(const interval& b) const { return !(*this == b); } - - bool implies(const interval& b) const { - if (b.is_full()) - return true; - if (is_full()) - return false; - - if (is_wrapped()) { - // l >= b.l >= b.h >= h - return b.is_wrapped() && h <= b.h && l >= b.l; - } else if (b.is_wrapped()) { - // b.l > b.h >= h >= l - // h >= l >= b.l > b.h - return h <= b.h || l >= b.l; - } else { - // - return l >= b.l && h <= b.h; - } - } - - /// return false if intersection is unsat - bool intersect(const interval& b, interval& result) const { - if (is_full() || *this == b) { - result = b; - return true; - } - if (b.is_full()) { - result = *this; - return true; + interval() {} + interval(uint64 l, uint64 h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) { + // canonicalize full set + if (is_wrapped() && l == h + 1) { + this->l = 0; + this->h = uMaxInt(sz); + } + SASSERT(invariant()); } - if (is_wrapped()) { - if (b.is_wrapped()) { - if (h >= b.l) { - result = b; - } else if (b.h >= l) { - result = *this; + bool invariant() const { + return l <= uMaxInt(sz) && h <= uMaxInt(sz) && + (!is_wrapped() || l != h+1); + } + + bool is_full() const { return l == 0 && h == uMaxInt(sz); } + bool is_wrapped() const { return l > h; } + bool is_singleton() const { return l == h; } + + bool operator==(const interval& b) const { + SASSERT(sz == b.sz); + return l == b.l && h == b.h && tight == b.tight; + } + bool operator!=(const interval& b) const { return !(*this == b); } + + bool implies(const interval& b) const { + if (b.is_full()) + return true; + if (is_full()) + return false; + + if (is_wrapped()) { + // l >= b.l >= b.h >= h + return b.is_wrapped() && h <= b.h && l >= b.l; + } + else if (b.is_wrapped()) { + // b.l > b.h >= h >= l + // h >= l >= b.l > b.h + return h <= b.h || l >= b.l; + } + else { + // + return l >= b.l && h <= b.h; + } + } + + /// return false if intersection is unsat + bool intersect(const interval& b, interval& result) const { + if (is_full() || *this == b) { + result = b; + return true; + } + if (b.is_full()) { + result = *this; + return true; + } + + if (is_wrapped()) { + if (b.is_wrapped()) { + if (h >= b.l) { + result = b; + } else if (b.h >= l) { + result = *this; + } else { + result = interval(std::max(l, b.l), std::min(h, b.h), sz); + } } else { - result = interval(std::max(l, b.l), std::min(h, b.h), sz); + return b.intersect(*this, result); + } + } + else if (b.is_wrapped()) { + // ... b.h ... l ... h ... b.l .. + if (h < b.l && l > b.h) { + return false; + } + // ... l ... b.l ... h ... + if (h >= b.l && l <= b.h) { + result = b; + } else if (h >= b.l) { + result = interval(b.l, h, sz); + } else { + // ... l .. b.h .. h .. b.l ... + SASSERT(l <= b.h); + result = interval(l, std::min(h, b.h), sz); } } else { - return b.intersect(*this, result); - } - } else if (b.is_wrapped()) { - // ... b.h ... l ... h ... b.l .. - if (h < b.l && l > b.h) { - return false; - } - // ... l ... b.l ... h ... - if (h >= b.l && l <= b.h) { - result = b; - } else if (h >= b.l) { - result = interval(b.l, h, sz); - } else { - // ... l .. b.h .. h .. b.l ... - SASSERT(l <= b.h); - result = interval(l, std::min(h, b.h), sz); - } - } else { - if (l > b.h || h < b.l) - return false; + if (l > b.h || h < b.l) + return false; - // 0 .. l.. l' ... h ... h' - result = interval(std::max(l, b.l), std::min(h, b.h), sz, tight && b.tight); - } - return true; - } - - /// return false if negation is empty - bool negate(interval& result) const { - if (!tight) { - result = interval(0, uMaxInt(sz), true); + // 0 .. l.. l' ... h ... h' + result = interval(std::max(l, b.l), std::min(h, b.h), sz, tight && b.tight); + } return true; } - if (is_full()) - return false; - if (l == 0) { - result = interval(h + 1, uMaxInt(sz), sz); - } else if (uMaxInt(sz) == h) { - result = interval(0, l - 1, sz); - } else { - result = interval(h + 1, l - 1, sz); + /// return false if negation is empty + bool negate(interval& result) const { + if (!tight) { + result = interval(0, uMaxInt(sz), true); + return true; + } + + if (is_full()) + return false; + if (l == 0) { + result = interval(h + 1, uMaxInt(sz), sz); + } else if (uMaxInt(sz) == h) { + result = interval(0, l - 1, sz); + } else { + result = interval(h + 1, l - 1, sz); + } + return true; } - return true; - } -}; + }; #ifdef _TRACE -std::ostream& operator<<(std::ostream& o, const interval& I) { - o << "[" << I.l << ", " << I.h << "]"; - return o; -} -#endif - - -struct undo_bound { - expr* e; - interval b; - bool fresh; - undo_bound(expr* e, const interval& b, bool fresh) : e(e), b(b), fresh(fresh) {} -}; - -class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { - typedef obj_map map; - typedef obj_map expr_set; - typedef obj_map expr_cnt; - - ast_manager& m; - params_ref m_params; - bool m_propagate_eq; - bv_util m_bv; - vector m_scopes; - map m_bound; - svector m_expr_vars; - svector m_bound_exprs; - - bool is_number(expr *e, uint64& n, unsigned& sz) const { - rational r; - if (m_bv.is_numeral(e, r, sz) && sz <= 64) { - n = r.get_uint64(); - return true; - } - return false; - } - - bool is_bound(expr *e, expr*& v, interval& b) const { - uint64 n; - expr *lhs, *rhs; - unsigned sz; - - if (m_bv.is_bv_ule(e, lhs, rhs)) { - if (is_number(lhs, n, sz)) { // C ule x <=> x uge C - if (m_bv.is_numeral(rhs)) - return false; - b = interval(n, uMaxInt(sz), sz, true); - v = rhs; - return true; - } - if (is_number(rhs, n, sz)) { // x ule C - b = interval(0, n, sz, true); - v = lhs; - return true; - } - } else if (m_bv.is_bv_sle(e, lhs, rhs)) { - if (is_number(lhs, n, sz)) { // C sle x <=> x sge C - if (m_bv.is_numeral(rhs)) - return false; - b = interval(n, (1ull << (sz-1)) - 1, sz, true); - v = rhs; - return true; - } - if (is_number(rhs, n, sz)) { // x sle C - b = interval(1ull << (sz-1), n, sz, true); - v = lhs; - return true; - } - } else if (m.is_eq(e, lhs, rhs)) { - if (is_number(lhs, n, sz)) { - if (m_bv.is_numeral(rhs)) - return false; - b = interval(n, n, sz, true); - v = rhs; - return true; - } - if (is_number(rhs, n, sz)) { - b = interval(n, n, sz, true); - v = lhs; - return true; - } - } - return false; - } - -#if 0 - expr_set* get_expr_vars(expr* t) { - unsigned id = t->get_id(); - m_expr_vars.reserve(id + 1); - expr_set*& entry = m_expr_vars[id]; - if (entry) - return entry; - - expr_set* set = alloc(expr_set); - entry = set; - - if (!m_bv.is_numeral(t)) - set->insert(t, true); - - if (!is_app(t)) - return set; - - app* a = to_app(t); - for (unsigned i = 0; i < a->get_num_args(); ++i) { - expr_set* set_arg = get_expr_vars(a->get_arg(i)); - for (expr_set::iterator I = set_arg->begin(), E = set_arg->end(); I != E; ++I) { - set->insert(I->m_key, true); - } - } - return set; + std::ostream& operator<<(std::ostream& o, const interval& I) { + o << "[" << I.l << ", " << I.h << "]"; + return o; } #endif -#if 0 - expr_cnt* get_expr_bounds(expr* t) { - unsigned id = t->get_id(); - m_bound_exprs.reserve(id + 1); - expr_cnt*& entry = m_bound_exprs[id]; - if (entry) - return entry; - expr_cnt* set = alloc(expr_cnt); - entry = set; - - if (!is_app(t)) - return set; - - interval b; + struct undo_bound { expr* e; - if (is_bound(t, e, b)) { - set->insert_if_not_there2(e, 0)->get_data().m_value++; + interval b; + bool fresh; + undo_bound(expr* e, const interval& b, bool fresh) : e(e), b(b), fresh(fresh) {} + }; + + class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { + typedef obj_map map; + typedef obj_map expr_set; + typedef obj_map expr_cnt; + + ast_manager& m; + params_ref m_params; + bool m_propagate_eq; + bv_util m_bv; + vector m_scopes; + map m_bound; + svector m_expr_vars; + svector m_bound_exprs; + + bool is_number(expr *e, uint64& n, unsigned& sz) const { + rational r; + if (m_bv.is_numeral(e, r, sz) && sz <= 64) { + n = r.get_uint64(); + return true; + } + return false; } - app* a = to_app(t); - for (unsigned i = 0; i < a->get_num_args(); ++i) { - expr_cnt* set_arg = get_expr_bounds(a->get_arg(i)); - for (expr_cnt::iterator I = set_arg->begin(), E = set_arg->end(); I != E; ++I) { - set->insert_if_not_there2(I->m_key, 0)->get_data().m_value += I->m_value; + bool is_bound(expr *e, expr*& v, interval& b) const { + uint64 n; + expr *lhs = 0, *rhs = 0; + unsigned sz; + + if (m_bv.is_bv_ule(e, lhs, rhs)) { + if (is_number(lhs, n, sz)) { // C ule x <=> x uge C + if (m_bv.is_numeral(rhs)) + return false; + b = interval(n, uMaxInt(sz), sz, true); + v = rhs; + return true; + } + if (is_number(rhs, n, sz)) { // x ule C + b = interval(0, n, sz, true); + v = lhs; + return true; + } + } + else if (m_bv.is_bv_sle(e, lhs, rhs)) { + if (is_number(lhs, n, sz)) { // C sle x <=> x sge C + if (m_bv.is_numeral(rhs)) + return false; + b = interval(n, (1ull << (sz-1)) - 1, sz, true); + v = rhs; + return true; + } + if (is_number(rhs, n, sz)) { // x sle C + b = interval(1ull << (sz-1), n, sz, true); + v = lhs; + return true; + } + } else if (m.is_eq(e, lhs, rhs)) { + if (is_number(lhs, n, sz)) { + if (m_bv.is_numeral(rhs)) + return false; + b = interval(n, n, sz, true); + v = rhs; + return true; + } + if (is_number(rhs, n, sz)) { + b = interval(n, n, sz, true); + v = lhs; + return true; + } } + return false; + } + +#if 0 + expr_set* get_expr_vars(expr* t) { + unsigned id = t->get_id(); + m_expr_vars.reserve(id + 1); + expr_set*& entry = m_expr_vars[id]; + if (entry) + return entry; + + expr_set* set = alloc(expr_set); + entry = set; + + if (!m_bv.is_numeral(t)) + set->insert(t, true); + + if (!is_app(t)) + return set; + + app* a = to_app(t); + for (unsigned i = 0; i < a->get_num_args(); ++i) { + expr_set* set_arg = get_expr_vars(a->get_arg(i)); + for (expr_set::iterator I = set_arg->begin(), E = set_arg->end(); I != E; ++I) { + set->insert(I->m_key, true); + } + } + return set; } - return set; - } #endif -public: - bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) { - updt_params(p); - } +#if 0 + expr_cnt* get_expr_bounds(expr* t) { + unsigned id = t->get_id(); + m_bound_exprs.reserve(id + 1); + expr_cnt*& entry = m_bound_exprs[id]; + if (entry) + return entry; - virtual void updt_params(params_ref const & p) { - m_propagate_eq = p.get_bool("propagate_eq", false); - } + expr_cnt* set = alloc(expr_cnt); + entry = set; - static void get_param_descrs(param_descrs& r) { - r.insert("propagate-eq", CPK_BOOL, "(default: false) propagate equalities from inequalities"); - } + if (!is_app(t)) + return set; - virtual ~bv_bounds_simplifier() { - for (unsigned i = 0, e = m_expr_vars.size(); i < e; ++i) { - dealloc(m_expr_vars[i]); - } - for (unsigned i = 0, e = m_bound_exprs.size(); i < e; ++i) { - dealloc(m_bound_exprs[i]); - } - } - - virtual bool assert_expr(expr * t, bool sign) { - while (m.is_not(t, t)) { - sign = !sign; - } - - interval b; - expr* t1; - if (is_bound(t, t1, b)) { - SASSERT(!m_bv.is_numeral(t1)); - if (sign) - VERIFY(b.negate(b)); - - TRACE("bv", tout << (sign?"(not ":"") << mk_pp(t, m) << (sign ? ")" : "") << ": " << mk_pp(t1, m) << " in " << b << "\n";); - map::obj_map_entry* e = m_bound.find_core(t1); - if (e) { - interval& old = e->get_data().m_value; - interval intr; - if (!old.intersect(b, intr)) - return false; - if (old == intr) - return true; - m_scopes.insert(undo_bound(t1, old, false)); - old = intr; - } else { - m_bound.insert(t1, b); - m_scopes.insert(undo_bound(t1, interval(), true)); - } - } - return true; - } - - virtual bool simplify(expr* t, expr_ref& result) { - expr* t1; - interval b; - - if (m_bound.find(t, b) && b.is_singleton()) { - result = m_bv.mk_numeral(b.l, m_bv.get_bv_size(t)); - return true; - } - - if (!m.is_bool(t)) - return false; - - bool sign = false; - while (m.is_not(t, t)) { - sign = !sign; - } - - if (!is_bound(t, t1, b)) - return false; - - if (sign && b.tight) { - sign = false; - if (!b.negate(b)) { - result = m.mk_false(); - return true; - } - } - - interval ctx, intr; - result = 0; - - if (b.is_full() && b.tight) { - result = m.mk_true(); - } else if (m_bound.find(t1, ctx)) { - if (ctx.implies(b)) { - result = m.mk_true(); - } else if (!b.intersect(ctx, intr)) { - result = m.mk_false(); - } else if (m_propagate_eq && intr.is_singleton()) { - result = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()), - m.get_sort(t1))); - } - } - - CTRACE("bv", result != 0, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << result << "\n";); - if (sign && result != 0) - result = m.mk_not(result); - return result != 0; - } - - // check if t contains v - ptr_vector todo; - bool contains(expr* t, expr* v) { - ast_fast_mark1 mark; - todo.push_back(t); - while (!todo.empty()) { - t = todo.back(); - todo.pop_back(); - if (mark.is_marked(t)) { - continue; - } - if (t == v) { - todo.reset(); - return true; - } - mark.mark(t); - - if (!is_app(t)) { - continue; - } - app* a = to_app(t); - todo.append(a->get_num_args(), a->get_args()); - } - return false; - } - - bool contains_bound(expr* t) { - ast_fast_mark1 mark1; - ast_fast_mark2 mark2; - - todo.push_back(t); - while (!todo.empty()) { - t = todo.back(); - todo.pop_back(); - if (mark1.is_marked(t)) { - continue; - } - mark1.mark(t); - - if (!is_app(t)) { - continue; - } interval b; expr* e; if (is_bound(t, e, b)) { - if (mark2.is_marked(e)) { - todo.reset(); - return true; - } - mark2.mark(e); - if (m_bound.contains(e)) { - todo.reset(); - return true; - } + set->insert_if_not_there2(e, 0)->get_data().m_value++; } app* a = to_app(t); - todo.append(a->get_num_args(), a->get_args()); - } - return false; - } - - virtual bool may_simplify(expr* t) { - if (m_bv.is_numeral(t)) - return false; - - while (m.is_not(t, t)); - - for (auto & v : m_bound) { - if (contains(t, v.m_key)) return true; - } - -#if 0 - expr_set* used_exprs = get_expr_vars(t); - for (map::iterator I = m_bound.begin(), E = m_bound.end(); I != E; ++I) { - if (contains(t, I->m_key)) return true; - if (I->m_value.is_singleton() && used_exprs->contains(I->m_key)) - return true; + for (unsigned i = 0; i < a->get_num_args(); ++i) { + expr_cnt* set_arg = get_expr_bounds(a->get_arg(i)); + for (expr_cnt::iterator I = set_arg->begin(), E = set_arg->end(); I != E; ++I) { + set->insert_if_not_there2(I->m_key, 0)->get_data().m_value += I->m_value; + } + } + return set; } #endif - expr* t1; - interval b; - // skip common case: single bound constraint without any context for simplification - if (is_bound(t, t1, b)) { - return b.is_full() || m_bound.contains(t1); + public: + bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) { + updt_params(p); } - if (contains_bound(t)) { - return true; + virtual void updt_params(params_ref const & p) { + m_propagate_eq = p.get_bool("propagate_eq", false); } -#if 0 - expr_cnt* bounds = get_expr_bounds(t); - for (expr_cnt::iterator I = bounds->begin(), E = bounds->end(); I != E; ++I) { - if (I->m_value > 1 || m_bound.contains(I->m_key)) - return true; - } -#endif - return false; - } - virtual void pop(unsigned num_scopes) { - TRACE("bv", tout << "pop: " << num_scopes << "\n";); - if (m_scopes.empty()) - return; - unsigned target = m_scopes.size() - num_scopes; - if (target == 0) { - m_bound.reset(); - m_scopes.reset(); - return; + static void get_param_descrs(param_descrs& r) { + r.insert("propagate-eq", CPK_BOOL, "(default: false) propagate equalities from inequalities"); } - for (unsigned i = m_scopes.size()-1; i >= target; --i) { - undo_bound& undo = m_scopes[i]; - SASSERT(m_bound.contains(undo.e)); - if (undo.fresh) { - m_bound.erase(undo.e); - } else { - m_bound.insert(undo.e, undo.b); + + virtual ~bv_bounds_simplifier() { + for (unsigned i = 0, e = m_expr_vars.size(); i < e; ++i) { + dealloc(m_expr_vars[i]); + } + for (unsigned i = 0, e = m_bound_exprs.size(); i < e; ++i) { + dealloc(m_bound_exprs[i]); } } - m_scopes.shrink(target); - } - virtual simplifier * translate(ast_manager & m) { - return alloc(bv_bounds_simplifier, m, m_params); - } + virtual bool assert_expr(expr * t, bool sign) { + while (m.is_not(t, t)) { + sign = !sign; + } - virtual unsigned scope_level() const { - return m_scopes.size(); - } -}; + interval b; + expr* t1; + if (is_bound(t, t1, b)) { + SASSERT(!m_bv.is_numeral(t1)); + if (sign) + VERIFY(b.negate(b)); + + TRACE("bv", tout << (sign?"(not ":"") << mk_pp(t, m) << (sign ? ")" : "") << ": " << mk_pp(t1, m) << " in " << b << "\n";); + map::obj_map_entry* e = m_bound.find_core(t1); + if (e) { + interval& old = e->get_data().m_value; + interval intr; + if (!old.intersect(b, intr)) + return false; + if (old == intr) + return true; + m_scopes.insert(undo_bound(t1, old, false)); + old = intr; + } else { + m_bound.insert(t1, b); + m_scopes.insert(undo_bound(t1, interval(), true)); + } + } + return true; + } + + virtual bool simplify(expr* t, expr_ref& result) { + expr* t1; + interval b; + + if (m_bound.find(t, b) && b.is_singleton()) { + result = m_bv.mk_numeral(b.l, m_bv.get_bv_size(t)); + return true; + } + + if (!m.is_bool(t)) + return false; + + bool sign = false; + while (m.is_not(t, t)) { + sign = !sign; + } + + if (!is_bound(t, t1, b)) + return false; + + if (sign && b.tight) { + sign = false; + if (!b.negate(b)) { + result = m.mk_false(); + return true; + } + } + + interval ctx, intr; + result = 0; + + if (b.is_full() && b.tight) { + result = m.mk_true(); + } else if (m_bound.find(t1, ctx)) { + if (ctx.implies(b)) { + result = m.mk_true(); + } else if (!b.intersect(ctx, intr)) { + result = m.mk_false(); + } else if (m_propagate_eq && intr.is_singleton()) { + result = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()), + m.get_sort(t1))); + } + } + + CTRACE("bv", result != 0, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << result << "\n";); + if (sign && result != 0) + result = m.mk_not(result); + return result != 0; + } + + // check if t contains v + ptr_vector todo; + bool contains(expr* t, expr* v) { + ast_fast_mark1 mark; + todo.push_back(t); + while (!todo.empty()) { + t = todo.back(); + todo.pop_back(); + if (mark.is_marked(t)) { + continue; + } + if (t == v) { + todo.reset(); + return true; + } + mark.mark(t); + + if (!is_app(t)) { + continue; + } + app* a = to_app(t); + todo.append(a->get_num_args(), a->get_args()); + } + return false; + } + + bool contains_bound(expr* t) { + ast_fast_mark1 mark1; + ast_fast_mark2 mark2; + + todo.push_back(t); + while (!todo.empty()) { + t = todo.back(); + todo.pop_back(); + if (mark1.is_marked(t)) { + continue; + } + mark1.mark(t); + + if (!is_app(t)) { + continue; + } + interval b; + expr* e; + if (is_bound(t, e, b)) { + if (mark2.is_marked(e)) { + todo.reset(); + return true; + } + mark2.mark(e); + if (m_bound.contains(e)) { + todo.reset(); + return true; + } + } + + app* a = to_app(t); + todo.append(a->get_num_args(), a->get_args()); + } + return false; + } + + virtual bool may_simplify(expr* t) { + if (m_bv.is_numeral(t)) + return false; + + while (m.is_not(t, t)); + + for (auto & v : m_bound) { + if (contains(t, v.m_key)) return true; + } + +#if 0 + expr_set* used_exprs = get_expr_vars(t); + for (map::iterator I = m_bound.begin(), E = m_bound.end(); I != E; ++I) { + if (contains(t, I->m_key)) return true; + if (I->m_value.is_singleton() && used_exprs->contains(I->m_key)) + return true; + } +#endif + + expr* t1; + interval b; + // skip common case: single bound constraint without any context for simplification + if (is_bound(t, t1, b)) { + return b.is_full() || m_bound.contains(t1); + } + + if (contains_bound(t)) { + return true; + } +#if 0 + expr_cnt* bounds = get_expr_bounds(t); + for (expr_cnt::iterator I = bounds->begin(), E = bounds->end(); I != E; ++I) { + if (I->m_value > 1 || m_bound.contains(I->m_key)) + return true; + } +#endif + return false; + } + + virtual void pop(unsigned num_scopes) { + TRACE("bv", tout << "pop: " << num_scopes << "\n";); + if (m_scopes.empty()) + return; + unsigned target = m_scopes.size() - num_scopes; + if (target == 0) { + m_bound.reset(); + m_scopes.reset(); + return; + } + for (unsigned i = m_scopes.size()-1; i >= target; --i) { + undo_bound& undo = m_scopes[i]; + SASSERT(m_bound.contains(undo.e)); + if (undo.fresh) { + m_bound.erase(undo.e); + } else { + m_bound.insert(undo.e, undo.b); + } + } + m_scopes.shrink(target); + } + + virtual simplifier * translate(ast_manager & m) { + return alloc(bv_bounds_simplifier, m, m_params); + } + + virtual unsigned scope_level() const { + return m_scopes.size(); + } + }; + + + class dom_bv_bounds_simplifier : public dom_simplifier { + typedef obj_map map; + typedef obj_map expr_set; + typedef obj_map expr_cnt; + + ast_manager& m; + params_ref m_params; + bool m_propagate_eq; + bv_util m_bv; + vector m_scopes; + map m_bound; + svector m_expr_vars; + svector m_bound_exprs; + + bool is_number(expr *e, uint64& n, unsigned& sz) const { + rational r; + if (m_bv.is_numeral(e, r, sz) && sz <= 64) { + n = r.get_uint64(); + return true; + } + return false; + } + + bool is_bound(expr *e, expr*& v, interval& b) const { + uint64 n; + expr *lhs = 0, *rhs = 0; + unsigned sz = 0; + + if (m_bv.is_bv_ule(e, lhs, rhs)) { + if (is_number(lhs, n, sz)) { // C ule x <=> x uge C + if (m_bv.is_numeral(rhs)) + return false; + b = interval(n, uMaxInt(sz), sz, true); + v = rhs; + return true; + } + if (is_number(rhs, n, sz)) { // x ule C + b = interval(0, n, sz, true); + v = lhs; + return true; + } + } + else if (m_bv.is_bv_sle(e, lhs, rhs)) { + if (is_number(lhs, n, sz)) { // C sle x <=> x sge C + if (m_bv.is_numeral(rhs)) + return false; + b = interval(n, (1ull << (sz-1)) - 1, sz, true); + v = rhs; + return true; + } + if (is_number(rhs, n, sz)) { // x sle C + b = interval(1ull << (sz-1), n, sz, true); + v = lhs; + return true; + } + } else if (m.is_eq(e, lhs, rhs)) { + if (is_number(lhs, n, sz)) { + if (m_bv.is_numeral(rhs)) + return false; + b = interval(n, n, sz, true); + v = rhs; + return true; + } + if (is_number(rhs, n, sz)) { + b = interval(n, n, sz, true); + v = lhs; + return true; + } + } + return false; + } + + + public: + dom_bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) { + updt_params(p); + } + + virtual void updt_params(params_ref const & p) { + m_propagate_eq = p.get_bool("propagate_eq", false); + } + + static void get_param_descrs(param_descrs& r) { + r.insert("propagate-eq", CPK_BOOL, "(default: false) propagate equalities from inequalities"); + } + + virtual ~dom_bv_bounds_simplifier() { + for (unsigned i = 0, e = m_expr_vars.size(); i < e; ++i) { + dealloc(m_expr_vars[i]); + } + for (unsigned i = 0, e = m_bound_exprs.size(); i < e; ++i) { + dealloc(m_bound_exprs[i]); + } + } + + virtual bool assert_expr(expr * t, bool sign) { + while (m.is_not(t, t)) { + sign = !sign; + } + + interval b; + expr* t1; + if (is_bound(t, t1, b)) { + SASSERT(!m_bv.is_numeral(t1)); + if (sign) + VERIFY(b.negate(b)); + + TRACE("bv", tout << (sign?"(not ":"") << mk_pp(t, m) << (sign ? ")" : "") << ": " << mk_pp(t1, m) << " in " << b << "\n";); + map::obj_map_entry* e = m_bound.find_core(t1); + if (e) { + interval& old = e->get_data().m_value; + interval intr; + if (!old.intersect(b, intr)) + return false; + if (old == intr) + return true; + m_scopes.insert(undo_bound(t1, old, false)); + old = intr; + } else { + m_bound.insert(t1, b); + m_scopes.insert(undo_bound(t1, interval(), true)); + } + } + return true; + } + + virtual void operator()(expr_ref& r) { + expr* t1, * t = r; + interval b; + + if (m_bound.find(t, b) && b.is_singleton()) { + r = m_bv.mk_numeral(b.l, m_bv.get_bv_size(t)); + return; + } + + if (!m.is_bool(t)) + return; + + bool sign = false; + while (m.is_not(t, t)) { + sign = !sign; + } + + if (!is_bound(t, t1, b)) + return; + + if (sign && b.tight) { + sign = false; + if (!b.negate(b)) { + r = m.mk_false(); + return; + } + } + + interval ctx, intr; + bool was_updated = true; + if (b.is_full() && b.tight) { + r = m.mk_true(); + } else if (m_bound.find(t1, ctx)) { + if (ctx.implies(b)) { + r = m.mk_true(); + } + else if (!b.intersect(ctx, intr)) { + r = m.mk_false(); + } + else if (m_propagate_eq && intr.is_singleton()) { + r = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()), + m.get_sort(t1))); + } + } + else { + was_updated = false; + } + + CTRACE("bv", was_updated, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << r << "\n";); + if (sign && was_updated) + r = m.mk_not(r); + } + + // check if t contains v + ptr_vector todo; + bool contains(expr* t, expr* v) { + ast_fast_mark1 mark; + todo.push_back(t); + while (!todo.empty()) { + t = todo.back(); + todo.pop_back(); + if (mark.is_marked(t)) { + continue; + } + if (t == v) { + todo.reset(); + return true; + } + mark.mark(t); + + if (!is_app(t)) { + continue; + } + app* a = to_app(t); + todo.append(a->get_num_args(), a->get_args()); + } + return false; + } + + bool contains_bound(expr* t) { + ast_fast_mark1 mark1; + ast_fast_mark2 mark2; + + todo.push_back(t); + while (!todo.empty()) { + t = todo.back(); + todo.pop_back(); + if (mark1.is_marked(t)) { + continue; + } + mark1.mark(t); + + if (!is_app(t)) { + continue; + } + interval b; + expr* e; + if (is_bound(t, e, b)) { + if (mark2.is_marked(e)) { + todo.reset(); + return true; + } + mark2.mark(e); + if (m_bound.contains(e)) { + todo.reset(); + return true; + } + } + + app* a = to_app(t); + todo.append(a->get_num_args(), a->get_args()); + } + return false; + } + + virtual void pop(unsigned num_scopes) { + TRACE("bv", tout << "pop: " << num_scopes << "\n";); + if (m_scopes.empty()) + return; + unsigned target = m_scopes.size() - num_scopes; + if (target == 0) { + m_bound.reset(); + m_scopes.reset(); + return; + } + for (unsigned i = m_scopes.size()-1; i >= target; --i) { + undo_bound& undo = m_scopes[i]; + SASSERT(m_bound.contains(undo.e)); + if (undo.fresh) { + m_bound.erase(undo.e); + } else { + m_bound.insert(undo.e, undo.b); + } + } + m_scopes.shrink(target); + } + + virtual dom_simplifier * translate(ast_manager & m) { + return alloc(dom_bv_bounds_simplifier, m, m_params); + } + + }; } tactic * mk_bv_bounds_tactic(ast_manager & m, params_ref const & p) { return clean(alloc(ctx_simplify_tactic, m, alloc(bv_bounds_simplifier, m, p), p)); } + +tactic * mk_dom_bv_bounds_tactic(ast_manager & m, params_ref const & p) { + return clean(alloc(dom_simplify_tactic, m, alloc(dom_bv_bounds_simplifier, m, p), p)); +} diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt index f192b4fa6..16778d8dd 100644 --- a/src/tactic/core/CMakeLists.txt +++ b/src/tactic/core/CMakeLists.txt @@ -7,6 +7,7 @@ z3_add_component(core_tactics ctx_simplify_tactic.cpp der_tactic.cpp distribute_forall_tactic.cpp + dom_simplify_tactic.cpp elim_term_ite_tactic.cpp elim_uncnstr_tactic.cpp injectivity_tactic.cpp @@ -32,6 +33,7 @@ z3_add_component(core_tactics ctx_simplify_tactic.h der_tactic.h distribute_forall_tactic.h + dom_simplify_tactic.h elim_term_ite_tactic.h elim_uncnstr_tactic.h injectivity_tactic.h diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 595f8f7c6..3a6d55569 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -83,49 +83,66 @@ expr* expr_dominators::intersect(expr* x, expr * y) { return x; } -void expr_dominators::compute_dominators() { +bool expr_dominators::compute_dominators() { expr * e = m_root; SASSERT(m_doms.empty()); m_doms.insert(e, e); bool change = true; + unsigned iterations = 1; while (change) { change = false; - SASSERT(m_post2expr.back() == e); - for (unsigned i = 0; i < m_post2expr.size() - 1; ++i) { + 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 = p[0], * idom2 = 0; - for (unsigned j = 1; j < p.size(); ++j) { - if (m_doms.find(p[j], idom2)) { - new_idom = intersect(new_idom, idom2); + expr * new_idom = 0, *idom2 = 0; + + for (expr * pred : p) { + if (m_doms.contains(pred)) { + new_idom = !new_idom ? pred : intersect(new_idom, pred); } } - if (!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; } } + iterations *= 2; + if (change && iterations > m_post2expr.size()) { + return false; + } } + return true; } void expr_dominators::extract_tree() { for (auto const& kv : m_doms) { add_edge(m_tree, kv.m_value, kv.m_key); } -} +} -void expr_dominators::compile(expr * e) { +bool expr_dominators::compile(expr * e) { reset(); m_root = e; compute_post_order(); - compute_dominators(); + if (!compute_dominators()) return false; extract_tree(); + TRACE("simplify", display(tout);); + return true; } -void expr_dominators::compile(unsigned sz, expr * const* es) { +bool expr_dominators::compile(unsigned sz, expr * const* es) { expr_ref e(m.mk_and(sz, es), m); - compile(e); + return compile(e); } void expr_dominators::reset() { @@ -137,19 +154,39 @@ 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; +} // ----------------------- // 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); } void dom_simplify_tactic::operator()( - goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, + goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { mc = 0; pc = 0; core = 0; @@ -162,33 +199,42 @@ void dom_simplify_tactic::operator()( } void dom_simplify_tactic::cleanup() { - m_trail.reset(); - m_args.reset(); - m_args2.reset(); - m_result.reset(); - m_dominators.reset(); + m_trail.reset(); + m_args.reset(); + m_result.reset(); + m_dominators.reset(); } expr_ref dom_simplify_tactic::simplify_ite(app * ite) { expr_ref r(m); - expr * c = 0, * t = 0, * e = 0; + 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_arg(c); if (m.is_true(new_c)) { - r = simplify(t); - } + r = simplify_arg(t); + } else if (m.is_false(new_c) || !assert_expr(new_c, false)) { - r = simplify(e); - } + r = simplify_arg(e); + } else { - expr_ref new_t = simplify(t); + for (expr * child : tree(ite)) { + if (is_subexpr(child, t) && !is_subexpr(child, e)) { + simplify_rec(child); + } + } pop(scope_level() - old_lvl); + expr_ref new_t = simplify_arg(t); if (!assert_expr(new_c, true)) { return new_t; } - expr_ref new_e = simplify(e); + for (expr * child : tree(ite)) { + if (is_subexpr(child, e) && !is_subexpr(child, t)) { + simplify_rec(child); + } + } pop(scope_level() - old_lvl); + expr_ref new_e = simplify_arg(e); if (c == new_c && t == new_t && e == new_e) { r = ite; } @@ -197,15 +243,28 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) { } else { TRACE("tactic", tout << new_c << "\n" << new_t << "\n" << new_e << "\n";); - r = m.mk_ite(new_c, new_t, new_c); + r = m.mk_ite(new_c, new_t, new_e); } } return r; } -expr_ref dom_simplify_tactic::simplify(expr * e0) { +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; +} + +/** + \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) << "\n";); if (!m_result.find(e0, e)) { e = e0; } @@ -224,17 +283,13 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) { r = simplify_or(to_app(e)); } else { - expr_dominators::tree_t const& t = m_dominators.get_tree(); - if (t.contains(e)) { - ptr_vector const& children = t[e]; - for (expr * child : children) { - simplify(child); - } + for (expr * child : tree(e)) { + simplify_rec(child); } 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? + m_args.push_back(simplify_arg(arg)); } r = m.mk_app(to_app(e)->get_decl(), m_args.size(), m_args.c_ptr()); } @@ -246,45 +301,64 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) { cache(e0, r); TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";); --m_depth; + m_subexpr_cache.reset(); return r; } expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) { expr_ref r(m); unsigned old_lvl = scope_level(); - m_args.reset(); - for (expr * arg : *e) { - r = simplify(arg); - if (!assert_expr(r, !is_and)) { - r = is_and ? m.mk_false() : m.mk_true(); + + auto is_subexpr_arg = [&](expr * child, expr * except) { + if (!is_subexpr(child, except)) + return false; + for (expr * arg : *e) { + if (arg != except && is_subexpr(child, arg)) + return false; } - m_args.push_back(r); + return true; + }; + + expr_ref_vector args(m); + if (m_forward) { + for (expr * arg : *e) { +#define _SIMP_ARG(arg) \ + for (expr * child : tree(arg)) { \ + if (is_subexpr_arg(child, arg)) { \ + simplify_rec(child); \ + } \ + } \ + r = simplify_arg(arg); \ + args.push_back(r); \ + if (!assert_expr(r, !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); + } + args.reverse(); } pop(scope_level() - old_lvl); - m_args.reverse(); - m_args2.reset(); - for (expr * arg : m_args) { - r = simplify(arg); - if (!assert_expr(r, !is_and)) { - r = is_and ? m.mk_false() : m.mk_true(); - } - m_args2.push_back(r); - } - pop(scope_level() - old_lvl); - m_args2.reverse(); - r = is_and ? mk_and(m_args2) : mk_or(m_args2); + r = is_and ? mk_and(args) : mk_or(args); return r; } -void dom_simplify_tactic::init(goal& g) { +bool dom_simplify_tactic::init(goal& g) { expr_ref_vector args(m); unsigned sz = g.size(); for (unsigned i = 0; i < sz; ++i) args.push_back(g.form(i)); expr_ref fml = mk_and(args); m_result.reset(); m_trail.reset(); - m_dominators.compile(fml); + return m_dominators.compile(fml); } void dom_simplify_tactic::simplify_goal(goal& g) { @@ -296,13 +370,15 @@ void dom_simplify_tactic::simplify_goal(goal& g) { change = false; // go forwards - init(g); + m_forward = true; + 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_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(); } + 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()) { @@ -313,15 +389,17 @@ void dom_simplify_tactic::simplify_goal(goal& g) { pop(scope_level()); // go backwards - init(g); + m_forward = false; + if (!init(g)) return; sz = g.size(); for (unsigned i = sz; !g.inconsistent() && i > 0; ) { --i; - expr_ref r = simplify(g.form(i)); + 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(); } 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)); @@ -333,11 +411,41 @@ 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; + + bool r; + if (m_subexpr_cache.find(a, b, r)) + return r; + + if (get_depth(a) >= get_depth(b)) { + 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) { + if (auto p = m_dominators.get_tree().find_core(e)) + return p->get_data().get_value(); + return m_empty; +} + // ---------------------- // expr_substitution_simplifier bool expr_substitution_simplifier::assert_expr(expr * t, bool sign) { + m_scoped_substitution.push(); expr* tt; if (!sign) { update_substitution(t, 0); @@ -389,6 +497,8 @@ void expr_substitution_simplifier::update_substitution(expr* n, proof* pr) { if (is_ground(n) && (m.is_eq(n, lhs, rhs) || m.is_iff(n, lhs, rhs))) { compute_depth(lhs); compute_depth(rhs); + m_trail.push_back(lhs); + m_trail.push_back(rhs); if (is_gt(lhs, rhs)) { TRACE("propagate_values", tout << "insert " << mk_pp(lhs, m) << " -> " << mk_pp(rhs, m) << "\n";); m_scoped_substitution.insert(lhs, rhs, pr); @@ -440,3 +550,7 @@ void expr_substitution_simplifier::compute_depth(expr* e) { m_expr2depth.insert(e, d + 1); } } + +tactic * mk_dom_simplify_tactic(ast_manager & m, params_ref const & p) { + return clean(alloc(dom_simplify_tactic, m, alloc(expr_substitution_simplifier, m), p)); +} diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index 2fa79dd1d..79bc9728c 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -23,6 +23,8 @@ Notes: #include "ast/ast.h" #include "ast/expr_substitution.h" #include "tactic/tactic.h" +#include "tactic/tactical.h" +#include "util/obj_pair_hashtable.h" class expr_dominators { @@ -43,78 +45,92 @@ private: void compute_post_order(); expr* intersect(expr* x, expr * y); - void compute_dominators(); + 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) {} - void compile(expr * e); - void compile(unsigned sz, expr * const* es); + bool compile(expr * e); + 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); +}; + +class dom_simplifier { + public: + dom_simplifier() {} + + virtual ~dom_simplifier() {} + /** + \brief assert_expr performs an implicit push + */ + virtual bool assert_expr(expr * t, bool sign) = 0; + + /** + \brief apply simplification. + */ + virtual void operator()(expr_ref& r) = 0; + + /** + \brief pop scopes accumulated from assertions. + */ + virtual void pop(unsigned num_scopes) = 0; + + virtual dom_simplifier * translate(ast_manager & m) = 0; }; class dom_simplify_tactic : public tactic { -public: - class simplifier { - public: - virtual ~simplifier() {} - /** - \brief assert_expr performs an implicit push - */ - virtual bool assert_expr(expr * t, bool sign) = 0; - - /** - \brief apply simplification. - */ - virtual void operator()(expr_ref& r) = 0; - - /** - \brief pop scopes accumulated from assertions. - */ - virtual void pop(unsigned num_scopes) = 0; - - virtual simplifier * translate(ast_manager & m); - - }; -private: ast_manager& m; - simplifier* m_simplifier; + dom_simplifier* m_simplifier; params_ref m_params; - expr_ref_vector m_trail, m_args, m_args2; + expr_ref_vector m_trail, m_args; obj_map m_result; expr_dominators m_dominators; unsigned m_scope_level; unsigned m_depth; 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_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); } expr_ref simplify_and_or(bool is_and, app * ite); void simplify_goal(goal& g); - expr_ref get_cached(expr* t) { expr* r = 0; if (!m_result.find(r, r)) r = t; return expr_ref(r, m); } + bool is_subexpr(expr * a, expr * b); + + expr_ref get_cached(expr* t) { expr* r = 0; if (!m_result.find(t, r)) r = t; return expr_ref(r, m); } 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); } bool assert_expr(expr* f, bool sign) { m_scope_level++; return m_simplifier->assert_expr(f, sign); } - void init(goal& g); + bool init(goal& g); public: - dom_simplify_tactic(ast_manager & m, simplifier* s, params_ref const & p = params_ref()): + dom_simplify_tactic(ast_manager & m, dom_simplifier* s, params_ref const & p = params_ref()): m(m), m_simplifier(s), m_params(p), - m_trail(m), m_args(m), m_args2(m), + 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() {} + virtual ~dom_simplify_tactic(); virtual tactic * translate(ast_manager & m); virtual void updt_params(params_ref const & p) {} @@ -130,11 +146,12 @@ public: virtual void cleanup(); }; -class expr_substitution_simplifier : public dom_simplify_tactic::simplifier { +class expr_substitution_simplifier : public dom_simplifier { ast_manager& m; expr_substitution m_subst; scoped_expr_substitution m_scoped_substitution; obj_map m_expr2depth; + expr_ref_vector m_trail; // move from asserted_formulas to here.. void compute_depth(expr* e); @@ -142,7 +159,7 @@ class expr_substitution_simplifier : public dom_simplify_tactic::simplifier { unsigned depth(expr* e) { return m_expr2depth[e]; } public: - expr_substitution_simplifier(ast_manager& m): m(m), m_subst(m), m_scoped_substitution(m_subst) {} + expr_substitution_simplifier(ast_manager& m): m(m), m_subst(m), m_scoped_substitution(m_subst), m_trail(m) {} virtual ~expr_substitution_simplifier() {} virtual bool assert_expr(expr * t, bool sign); @@ -152,12 +169,17 @@ public: virtual void pop(unsigned num_scopes) { m_scoped_substitution.pop(num_scopes); } - virtual simplifier * translate(ast_manager & m) { + virtual dom_simplifier * translate(ast_manager & m) { SASSERT(m_subst.empty()); return alloc(expr_substitution_simplifier, m); } - - }; + +tactic * mk_dom_simplify_tactic(ast_manager & m, params_ref const & p = params_ref()); + +/* +ADD_TACTIC("dom-simplify", "apply dominator simplification rules.", "mk_dom_simplify_tactic(m, p)") +*/ + #endif diff --git a/src/tactic/portfolio/CMakeLists.txt b/src/tactic/portfolio/CMakeLists.txt index 570db8f6a..055251467 100644 --- a/src/tactic/portfolio/CMakeLists.txt +++ b/src/tactic/portfolio/CMakeLists.txt @@ -1,11 +1,13 @@ z3_add_component(portfolio SOURCES + bounded_int2bv_solver.cpp default_tactic.cpp enum2bv_solver.cpp - pb2bv_solver.cpp - bounded_int2bv_solver.cpp fd_solver.cpp + parallel_tactic.cpp + pb2bv_solver.cpp smt_strategic_solver.cpp + solver2lookahead.cpp COMPONENT_DEPENDENCIES aig_tactic fp @@ -19,4 +21,5 @@ z3_add_component(portfolio TACTIC_HEADERS default_tactic.h fd_solver.h + parallel_tactic.h ) diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp new file mode 100644 index 000000000..9bacbe6a0 --- /dev/null +++ b/src/tactic/portfolio/parallel_tactic.cpp @@ -0,0 +1,448 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + parallel_tactic.cpp + +Abstract: + + Parallel tactic in the style of Treengeling. + + It assumes a solver that supports good lookaheads. + + +Author: + + Nikolaj Bjorner (nbjorner) 2017-10-9 + +Notes: + +--*/ + +#include "util/scoped_ptr_vector.h" +#include "ast/ast_util.h" +#include "solver/solver.h" +#include "solver/solver2tactic.h" +#include "tactic/tactic.h" +#include "tactic/portfolio/fd_solver.h" + +class parallel_tactic : public tactic { + + class solver_state { + params_ref m_params; + scoped_ptr m_manager; + ref m_solver; + expr_ref_vector m_cube; + unsigned m_units; + public: + solver_state(ast_manager* m, solver* s, params_ref const& p): + m_params(p), + m_manager(m), + m_solver(s), + m_cube(s->get_manager()), + m_units(0) {} + + void update_units() { + m_units = 0; + statistics st; + m_solver->collect_statistics(st); + std::string units("units"); + for (unsigned i = st.size(); i-- > 0; ) { + if (st.get_key(i) == units) { + m_units = st.get_uint_value(i); + std::cout << "value for " << i << " is " << m_units << "\n"; + break; + } + } + } + + expr_ref cube() { return mk_and(m_cube); } + + void add_cube(expr* c) { m_cube.push_back(c); } + + unsigned num_units() const { return m_units; } + + solver& get_solver() { return *m_solver; } + + solver const& get_solver() const { return *m_solver; } + + params_ref const& params() const { return m_params; } + + solver_state* clone(params_ref const& p, expr* cube) { + ast_manager& m = m_solver->get_manager(); + ast_manager* new_m = alloc(ast_manager, m, !m.proof_mode()); + solver* s = m_solver->translate(*new_m, p); + solver_state* st = alloc(solver_state, new_m, s, m_params); + ast_translation translate(m, *new_m); + for (expr* c : m_cube) { + st->m_cube.push_back(translate(c)); + } + expr_ref cube1(translate(cube), *new_m); + st->m_cube.push_back(cube1); + s->assert_expr(cube1); + return st; + } + }; + +public: + bool operator()(solver_state* s1, solver_state* s2) const { + return s1->num_units() > s2->num_units(); + } +private: + + ast_manager& m_manager; + params_ref m_params; + + // parameters + unsigned m_conflicts_lower_bound; + unsigned m_conflicts_upper_bound; + unsigned m_conflicts_growth_rate; + unsigned m_conflicts_decay_rate; + unsigned m_num_threads; + + double m_progress; + unsigned m_max_conflicts; + statistics m_stats; + + vector m_solvers; + + void init() { + m_conflicts_lower_bound = 1000; + m_conflicts_upper_bound = 10000; + m_conflicts_growth_rate = 150; + m_conflicts_decay_rate = 75; + m_max_conflicts = m_conflicts_lower_bound; + m_progress = 0; + m_num_threads = omp_get_num_procs(); // TBD adjust by possible threads used inside each solver. + } + + unsigned get_max_conflicts() { + return m_max_conflicts; + } + + void set_max_conflicts(unsigned c) { + m_max_conflicts = c; + } + + bool should_increase_conflicts() { + return m_progress < 0; + } + + void update_progress(bool b) { + m_progress = 0.9 * m_progress + (b ? 1 : -1); + if (b) { + m_stats.update("closed", 1u); + } + } + + int pick_solvers() { + // order solvers by number of units in descending order + for (solver_state* s : m_solvers) s->update_units(); + std::sort(m_solvers.c_ptr(), m_solvers.c_ptr() + m_solvers.size(), *this); + TRACE("parallel_tactic", display(tout);); + return std::min(m_num_threads, m_solvers.size()); + } + + int max_num_splits() { + if (m_solvers.empty()) { + return m_num_threads; + } + uint64 max_mem = memory::get_max_memory_size(); + uint64 cur_mem = memory::get_allocation_size(); + uint64 sol_sz = cur_mem / m_solvers.size(); + + TRACE("parallel_tactic", tout << "max mem: " << max_mem << " cur mem: " << cur_mem << " num solvers: " << m_solvers.size() << "\n";); + if (max_mem <= cur_mem) { + return 0; + } + if (cur_mem == 0) { + return m_num_threads; + } + uint64 extra_solvers = (max_mem - cur_mem) / (2 * sol_sz); + if (extra_solvers > m_num_threads) { + return m_num_threads; + } + return static_cast(extra_solvers); + } + + void update_max_conflicts() { + if (should_increase_conflicts()) { + set_max_conflicts(std::min(m_conflicts_upper_bound, m_conflicts_growth_rate * get_max_conflicts() / 100)); + } + else { + set_max_conflicts(std::max(m_conflicts_lower_bound, m_conflicts_decay_rate * get_max_conflicts() / 100)); + } + } + + lbool simplify(solver& s) { + params_ref p; + p.copy(m_params); + p.set_uint("max_conflicts", 10); + p.set_bool("lookahead_simplify", true); + s.updt_params(p); + lbool is_sat = s.check_sat(0,0); + p.set_uint("max_conflicts", get_max_conflicts()); + p.set_bool("lookahead_simplify", false); + s.updt_params(p); + return is_sat; + } + + lbool cube(solver_state& s) { + ast_manager& m = s.get_solver().get_manager(); + expr_ref_vector cubes(m); + params_ref p; + p.copy(s.params()); + p.set_uint("lookahead.cube.cutoff", 1); + s.get_solver().updt_params(p); + SASSERT(&m == &cubes.get_manager()); + while (true) { + expr_ref c = s.get_solver().cube(); + VERIFY(c); + if (m.is_false(c)) { + break; + } + if (m.is_true(c)) { + cubes.reset(); + return l_undef; + } + cubes.push_back(c); + } + + IF_VERBOSE(1, verbose_stream() << "cubes: " << cubes << "\n";); + + if (cubes.empty()) { + return l_false; + } + for (unsigned j = 1; j < cubes.size(); ++j) { + solver_state* s1 = s.clone(s.params(), cubes[j].get()); + #pragma omp critical (parallel_tactic) + { + m_solvers.push_back(s1); + } + } + + expr* cube0 = cubes[0].get(); + s.add_cube(cube0); + s.get_solver().assert_expr(cube0); + return l_undef; + } + + lbool solve(solver& s) { + params_ref p; + p.copy(m_params); + p.set_uint("max_conflicts", get_max_conflicts()); + s.updt_params(p); + return s.check_sat(0, 0); + } + + void remove_unsat(svector& unsat) { + std::sort(unsat.begin(), unsat.end()); + unsat.reverse(); + DEBUG_CODE(for (unsigned i = 0; i + 1 < unsat.size(); ++i) SASSERT(unsat[i] > unsat[i+1]);); + for (int i : unsat) { + m_solvers[i]->get_solver().collect_statistics(m_stats); + dealloc(m_solvers[i]); + for (unsigned j = i + 1; j < m_solvers.size(); ++j) { + m_solvers[j - 1] = m_solvers[j]; + } + m_solvers.shrink(m_solvers.size() - 1); + update_progress(true); + } + unsat.reset(); + } + + void get_model(model_ref& mdl, int sat_index) { + SASSERT(sat_index != -1); + m_solvers[sat_index]->get_solver().get_model(mdl); + ast_translation translate(m_solvers[sat_index]->get_solver().get_manager(), m_manager); + mdl = mdl->translate(translate); + } + + lbool solve(model_ref& mdl) { + while (true) { + int sz = pick_solvers(); + + + if (sz == 0) { + return l_false; + } + svector unsat; + int sat_index = -1; + + // Simplify phase. + IF_VERBOSE(1, verbose_stream() << "(solver.parallel :simplify " << sz << ")\n";); + IF_VERBOSE(1, display(verbose_stream()); verbose_stream() << "Number of solvers: " << sz << "\n";); + + #pragma omp parallel for + for (int i = 0; i < sz; ++i) { + lbool is_sat = simplify(m_solvers[i]->get_solver()); + switch (is_sat) { + case l_false: + #pragma omp critical (parallel_tactic) + { + unsat.push_back(i); + } + break; + case l_true: + sat_index = i; + break; + case l_undef: + break; + } + } + if (sat_index != -1) { + get_model(mdl, sat_index); + return l_true; + } + sz -= unsat.size(); + remove_unsat(unsat); + if (sz == 0) continue; + + // Solve phase. + IF_VERBOSE(1, verbose_stream() << "(solver.parallel :solve " << sz << ")\n";); + IF_VERBOSE(1, display(verbose_stream()); verbose_stream() << "Number of solvers: " << sz << "\n";); + + #pragma omp parallel for + for (int i = 0; i < sz; ++i) { + lbool is_sat = solve(m_solvers[i]->get_solver()); + switch (is_sat) { + case l_false: + #pragma omp critical (parallel_tactic) + { + unsat.push_back(i); + } + break; + case l_true: + sat_index = i; + break; + case l_undef: + break; + } + } + if (sat_index != -1) { + get_model(mdl, sat_index); + return l_true; + } + sz -= unsat.size(); + remove_unsat(unsat); + + sz = std::min(max_num_splits(), sz); + if (sz == 0) continue; + + + // Split phase. + IF_VERBOSE(1, verbose_stream() << "(solver.parallel :split " << sz << ")\n";); + IF_VERBOSE(1, display(verbose_stream()); verbose_stream() << "Number of solvers: " << sz << "\n";); + + #pragma omp parallel for + for (int i = 0; i < sz; ++i) { + switch (cube(*m_solvers[i])) { + case l_false: + #pragma omp critical (parallel_tactic) + { + unsat.push_back(i); + } + break; + default: + #pragma omp critical (parallel_tactic) + { + update_progress(false); + } + break; + } + } + + remove_unsat(unsat); + update_max_conflicts(); + } + return l_undef; + } + + std::ostream& display(std::ostream& out) { + for (solver_state* s : m_solvers) { + out << "solver units " << s->num_units() << "\n"; + out << "cube " << s->cube() << "\n"; + } + m_stats.display(out); + return out; + } + + +public: + parallel_tactic(ast_manager& m, params_ref const& p) : + m_manager(m), + m_params(p) { + init(); + } + + void operator ()(const goal_ref & g,goal_ref_buffer & result,model_converter_ref & mc,proof_converter_ref & pc,expr_dependency_ref & dep) { + ast_manager& m = g->m(); + solver* s = mk_fd_solver(m, m_params); + m_solvers.push_back(alloc(solver_state, 0, s, m_params)); + expr_ref_vector clauses(m); + ptr_vector assumptions; + obj_map bool2dep; + ref fmc; + extract_clauses_and_dependencies(g, clauses, assumptions, bool2dep, fmc); + for (expr * clause : clauses) { + s->assert_expr(clause); + } + SASSERT(assumptions.empty()); + model_ref mdl; + lbool is_sat = solve(mdl); + switch (is_sat) { + case l_true: + if (g->models_enabled()) { + mc = model2model_converter(mdl.get()); + mc = concat(fmc.get(), mc.get()); + } + g->reset(); + break; + case l_false: + SASSERT(!g->proofs_enabled()); + SASSERT(!g->unsat_core_enabled()); + g->assert_expr(m.mk_false(), nullptr, nullptr); + break; + case l_undef: + if (m.canceled()) { + throw tactic_exception(Z3_CANCELED_MSG); + } + break; + } + result.push_back(g.get()); + } + + void cleanup() { + for (solver_state * s : m_solvers) dealloc(s); + m_solvers.reset(); + init(); + } + + tactic* translate(ast_manager& m) { + return alloc(parallel_tactic, m, m_params); + } + + virtual void updt_params(params_ref const & p) { + m_params.copy(p); + } + virtual void collect_param_descrs(param_descrs & r) { + // TBD + } + + virtual void collect_statistics(statistics & st) const { + for (solver_state const * s : m_solvers) { + s->get_solver().collect_statistics(st); + } + st.copy(m_stats); + } + virtual void reset_statistics() { + m_stats.reset(); + } + +}; + +tactic * mk_parallel_tactic(ast_manager& m, params_ref const& p) { + return alloc(parallel_tactic, m, p); +} + diff --git a/src/tactic/portfolio/parallel_tactic.h b/src/tactic/portfolio/parallel_tactic.h new file mode 100644 index 000000000..8fd9a29fa --- /dev/null +++ b/src/tactic/portfolio/parallel_tactic.h @@ -0,0 +1,31 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + parallel_tactic.h + +Abstract: + + Parallel tactic in the style of Treengeling. + +Author: + + Nikolaj Bjorner (nbjorner) 2017-10-9 + +Notes: + +--*/ +#ifndef PARALLEL_TACTIC_H_ +#define PARALLEL_TACTIC_H_ + +class solver; +class tactic; + +tactic * mk_parallel_tactic(ast_manager& m, params_ref const& p); + +/* + ADD_TACTIC("qffdp", "builtin strategy for solving QF_FD problems in parallel.", "mk_parallel_tactic(m, p)") +*/ + +#endif diff --git a/src/tactic/portfolio/solver2lookahead.cpp b/src/tactic/portfolio/solver2lookahead.cpp new file mode 100644 index 000000000..0c18ab079 --- /dev/null +++ b/src/tactic/portfolio/solver2lookahead.cpp @@ -0,0 +1,24 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + solver2lookahead.cpp + +Abstract: + + Lookahead wrapper for arbitrary solver. + +Author: + + Nikolaj Bjorner (nbjorner) 2017-10-9 + +Notes: + +--*/ +#include "sat/sat_solver/inc_sat_solver.h" +#include "solver/solver.h" + +solver * mk_solver2lookahead(solver* s) { + return 0; +} diff --git a/src/tactic/portfolio/solver2lookahead.h b/src/tactic/portfolio/solver2lookahead.h new file mode 100644 index 000000000..80d73ddf3 --- /dev/null +++ b/src/tactic/portfolio/solver2lookahead.h @@ -0,0 +1,26 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + solver2lookahead.h + +Abstract: + + Lookahead wrapper for arbitrary solver. + +Author: + + Nikolaj Bjorner (nbjorner) 2017-10-9 + +Notes: + +--*/ +#ifndef SOLVER2LOOKAHEAD_H_ +#define SOLVER2LOOKAHEAD_H_ + +class solver; + +solver * mk_solver2lookahead(solver* s); + +#endif diff --git a/src/test/ddnf.cpp b/src/test/ddnf.cpp index 09f1a4cf9..c9eb6aa08 100644 --- a/src/test/ddnf.cpp +++ b/src/test/ddnf.cpp @@ -214,6 +214,10 @@ void tst_ddnf1() { ddnf.insert(*tX1); ddnf.insert(*t1X); ddnf.display(std::cout); + tbvm.deallocate(tXX); + tbvm.deallocate(t1X); + tbvm.deallocate(tX1); + tbvm.deallocate(t11); } diff --git a/src/util/approx_set.h b/src/util/approx_set.h index e696d52ee..1cb7ae9f2 100644 --- a/src/util/approx_set.h +++ b/src/util/approx_set.h @@ -29,7 +29,7 @@ public: static const unsigned long long zero = 0ull; static const unsigned long long one = 1ull; }; -COMPILE_TIME_ASSERT(sizeof(unsigned long long) == 8); +static_assert(sizeof(unsigned long long) == 8, ""); template <> class approx_set_traits { public: @@ -37,7 +37,7 @@ public: static const unsigned zero = 0; static const unsigned one = 1; }; -COMPILE_TIME_ASSERT(sizeof(unsigned) == 4); +static_assert(sizeof(unsigned) == 4, "unsigned are 4 bytes"); template class approx_set_tpl : private T2U_Proc { diff --git a/src/util/bit_vector.h b/src/util/bit_vector.h index 6a254e399..2d42e35a2 100644 --- a/src/util/bit_vector.h +++ b/src/util/bit_vector.h @@ -24,7 +24,7 @@ Revision History: #include "util/vector.h" #include "util/memory_manager.h" -COMPILE_TIME_ASSERT(sizeof(unsigned) == 4); +static_assert(sizeof(unsigned) == 4, "unsigned are 4 bytes"); #define BV_DEFAULT_CAPACITY 2 class bit_vector { diff --git a/src/util/debug.h b/src/util/debug.h index e0ceb9a64..536df4588 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -90,7 +90,6 @@ bool is_debug_enabled(const char * tag); exit(-1); \ } -#define COMPILE_TIME_ASSERT(expr) static_assert(expr, "") void finalize_debug(); /* diff --git a/src/util/double_manager.h b/src/util/double_manager.h index 33cccf2af..7532a3b8b 100644 --- a/src/util/double_manager.h +++ b/src/util/double_manager.h @@ -97,7 +97,7 @@ public: } }; -COMPILE_TIME_ASSERT(sizeof(uint64) == sizeof(double)); +static_assert(sizeof(uint64) == sizeof(double), ""); #endif /* DOUBLE_MANAGER_H_ */ 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; diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 1ed30bd70..6d2cbea7d 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -417,6 +417,8 @@ public: for (unsigned i : m_rows_with_changed_bounds.m_index) { calculate_implied_bounds_for_row(i, bp); + if (settings().get_cancel_flag()) + return; } m_rows_with_changed_bounds.clear(); if (!use_tableau()) { diff --git a/src/util/lp/lp_primal_core_solver_tableau.h b/src/util/lp/lp_primal_core_solver_tableau.h index 5c7d4d2c2..0c56f0ab9 100644 --- a/src/util/lp/lp_primal_core_solver_tableau.h +++ b/src/util/lp/lp_primal_core_solver_tableau.h @@ -176,25 +176,34 @@ unsigned lp_primal_core_solver::solve_with_tableau() { default: break; // do nothing } - } while (this->get_status() != FLOATING_POINT_ERROR - && - this->get_status() != UNBOUNDED - && - this->get_status() != OPTIMAL - && - this->get_status() != INFEASIBLE - && - this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements - && - this->total_iterations() <= this->m_settings.max_total_number_of_iterations - && - !(this->current_x_is_feasible() && this->m_look_for_feasible_solution_only)); + } while (this->get_status() != FLOATING_POINT_ERROR + && + this->get_status() != UNBOUNDED + && + this->get_status() != OPTIMAL + && + this->get_status() != INFEASIBLE + && + this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements + && + this->total_iterations() <= this->m_settings.max_total_number_of_iterations + && + !(this->current_x_is_feasible() && this->m_look_for_feasible_solution_only) + && + this->m_settings.get_cancel_flag() == false); + + if (this->m_settings.get_cancel_flag()) { + this->set_status(CANCELLED); + } - SASSERT(this->get_status() == FLOATING_POINT_ERROR - || - this->current_x_is_feasible() == false - || - this->calc_current_x_is_feasible_include_non_basis()); + SASSERT( + this->get_status() == FLOATING_POINT_ERROR + || + this->get_status() == CANCELLED + || + this->current_x_is_feasible() == false + || + this->calc_current_x_is_feasible_include_non_basis()); return this->total_iterations(); } diff --git a/src/util/lp/lp_settings.h b/src/util/lp/lp_settings.h index 70a9f1504..a7e6e2665 100644 --- a/src/util/lp/lp_settings.h +++ b/src/util/lp/lp_settings.h @@ -61,7 +61,8 @@ enum lp_status { TIME_EXHAUSTED, ITERATIONS_EXHAUSTED, EMPTY, - UNSTABLE + UNSTABLE, + CANCELLED }; // when the ratio of the vector lenth to domain size to is greater than the return value we switch to solve_By_for_T_indexed_only diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index 0b394b450..35bdce43d 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -58,9 +58,10 @@ static void throw_out_of_memory() { g_memory_out_of_memory = true; } + __assume(0); + if (g_exit_when_out_of_memory) { std::cerr << g_out_of_memory_msg << "\n"; - __assume(0); exit(ERR_MEMOUT); } else { @@ -181,6 +182,23 @@ unsigned long long memory::get_max_used_memory() { return r; } +#if defined(_WINDOWS) +#include "Windows.h" +#endif + +unsigned long long memory::get_max_memory_size() { +#if defined(_WINDOWS) + MEMORYSTATUSEX statex; + statex.dwLength = sizeof (statex); + GlobalMemoryStatusEx (&statex); + return statex.ullTotalPhys; +#else + NOT_IMPLEMENTED_YET(); + // two GB + return 1 << 31; +#endif +} + unsigned long long memory::get_allocation_count() { return g_memory_alloc_count; } diff --git a/src/util/memory_manager.h b/src/util/memory_manager.h index 5aa512018..bbddfa67f 100644 --- a/src/util/memory_manager.h +++ b/src/util/memory_manager.h @@ -67,6 +67,7 @@ public: static unsigned long long get_allocation_size(); static unsigned long long get_max_used_memory(); static unsigned long long get_allocation_count(); + static unsigned long long get_max_memory_size(); // temporary hack to avoid out-of-memory crash in z3.exe static void exit_when_out_of_memory(bool flag, char const * msg); }; diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 5e7233110..3218419a9 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -73,7 +73,7 @@ mpf_manager::~mpf_manager() { } void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, int value) { - COMPILE_TIME_ASSERT(sizeof(int) == 4); + static_assert(sizeof(int) == 4, "assume integers are 4 bytes"); o.sign = false; o.ebits = ebits; @@ -119,7 +119,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, double value) { // double === mpf(11, 53) - COMPILE_TIME_ASSERT(sizeof(double) == 8); + static_assert(sizeof(double) == 8, "doubles are 8 bytes"); uint64 raw; memcpy(&raw, &value, sizeof(double)); @@ -155,7 +155,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, double value) { void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, float value) { // single === mpf(8, 24) - COMPILE_TIME_ASSERT(sizeof(float) == 4); + static_assert(sizeof(float) == 4, "floats are 4 bytes"); unsigned int raw; memcpy(&raw, &value, sizeof(float)); diff --git a/src/util/mpff.cpp b/src/util/mpff.cpp index 459b0691c..eac9cc80c 100644 --- a/src/util/mpff.cpp +++ b/src/util/mpff.cpp @@ -27,8 +27,8 @@ Revision History: #include "util/bit_util.h" #include "util/trace.h" -COMPILE_TIME_ASSERT(sizeof(mpn_digit) == sizeof(unsigned)); -COMPILE_TIME_ASSERT(sizeof(unsigned) == 4); +static_assert(sizeof(mpn_digit) == sizeof(unsigned), ""); +static_assert(sizeof(unsigned) == 4, "unsigned haven't changed size for a while"); // MIN_MSW is an shorthand for 0x8000..00, i.e., the minimal most significand word. #define MIN_MSW (1u << (sizeof(unsigned) * 8 - 1)) diff --git a/src/util/mpn.cpp b/src/util/mpn.cpp index 65223133f..2059ea6fd 100644 --- a/src/util/mpn.cpp +++ b/src/util/mpn.cpp @@ -24,7 +24,7 @@ Revision History: #define max(a,b) (((a) > (b)) ? (a) : (b)) typedef uint64 mpn_double_digit; -COMPILE_TIME_ASSERT(sizeof(mpn_double_digit) == 2 * sizeof(mpn_digit)); +static_assert(sizeof(mpn_double_digit) == 2 * sizeof(mpn_digit), "size alignment"); const mpn_digit mpn_manager::zero = 0; diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 9569ac280..7ad472ef1 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)) { + static_assert(sizeof(a.m_val) == sizeof(int), "size mismatch"); + 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 { @@ -725,7 +724,7 @@ void mpz_manager::gcd(mpz const & a, mpz const & b, mpz & c) { #ifdef LEHMER_GCD // For now, it only works if sizeof(digit_t) == sizeof(unsigned) - COMPILE_TIME_ASSERT(sizeof(digit_t) == sizeof(unsigned)); + static_assert(sizeof(digit_t) == sizeof(unsigned), ""); int64 a_hat, b_hat, A, B, C, D, T, q, a_sz, b_sz; mpz a1, b1, t, r, tmp; @@ -1755,7 +1754,7 @@ void mpz_manager::mul2k(mpz & a, unsigned k) { } #ifndef _MP_GMP -COMPILE_TIME_ASSERT(sizeof(digit_t) == 4 || sizeof(digit_t) == 8); +static_assert(sizeof(digit_t) == 4 || sizeof(digit_t) == 8, ""); #endif template @@ -1822,7 +1821,7 @@ unsigned mpz_manager::log2(mpz const & a) { if (is_small(a)) return ::log2((unsigned)a.m_val); #ifndef _MP_GMP - COMPILE_TIME_ASSERT(sizeof(digit_t) == 8 || sizeof(digit_t) == 4); + static_assert(sizeof(digit_t) == 8 || sizeof(digit_t) == 4, ""); mpz_cell * c = a.m_ptr; unsigned sz = c->m_size; digit_t * ds = c->m_digits; @@ -1844,7 +1843,7 @@ unsigned mpz_manager::mlog2(mpz const & a) { if (is_small(a)) return ::log2((unsigned)-a.m_val); #ifndef _MP_GMP - COMPILE_TIME_ASSERT(sizeof(digit_t) == 8 || sizeof(digit_t) == 4); + static_assert(sizeof(digit_t) == 8 || sizeof(digit_t) == 4, ""); mpz_cell * c = a.m_ptr; unsigned sz = c->m_size; digit_t * ds = c->m_digits; diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp index f3f45c654..e625cab95 100644 --- a/src/util/rlimit.cpp +++ b/src/util/rlimit.cpp @@ -21,6 +21,7 @@ Revision History: reslimit::reslimit(): m_cancel(0), + m_suspend(false), m_count(0), m_limit(0) { } @@ -31,12 +32,12 @@ uint64 reslimit::count() const { bool reslimit::inc() { ++m_count; - return m_cancel == 0 && (m_limit == 0 || m_count <= m_limit); + return (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend; } bool reslimit::inc(unsigned offset) { m_count += offset; - return m_cancel == 0 && (m_limit == 0 || m_count <= m_limit); + return (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend; } void reslimit::push(unsigned delta_limit) { diff --git a/src/util/rlimit.h b/src/util/rlimit.h index 3b278d132..0c81f9449 100644 --- a/src/util/rlimit.h +++ b/src/util/rlimit.h @@ -23,12 +23,14 @@ Revision History: class reslimit { volatile unsigned m_cancel; + bool m_suspend; uint64 m_count; uint64 m_limit; svector m_limits; ptr_vector m_children; void set_cancel(unsigned f); + friend class scoped_suspend_rlimit; public: reslimit(); @@ -42,7 +44,7 @@ public: uint64 count() const; - bool get_cancel_flag() const { return m_cancel > 0; } + bool get_cancel_flag() const { return m_cancel > 0 && !m_suspend; } char const* get_cancel_msg() const; void cancel(); void reset_cancel(); @@ -61,6 +63,17 @@ public: }; +class scoped_suspend_rlimit { + reslimit & m_limit; +public: + scoped_suspend_rlimit(reslimit& r): m_limit(r) { + r.m_suspend = true; + } + ~scoped_suspend_rlimit() { + m_limit.m_suspend = false; + } +}; + struct scoped_limits { reslimit& m_limit; unsigned m_sz; diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h index ade66403d..ab0d69791 100644 --- a/src/util/sorting_network.h +++ b/src/util/sorting_network.h @@ -469,7 +469,9 @@ Notes: } literal mk_ordered_1(bool full, bool is_eq, unsigned n, literal const* xs) { - if (n <= 1 && !is_eq) return ctx.mk_true(); + if (n <= 1 && !is_eq) { + return ctx.mk_true(); + } if (n == 0) { return ctx.mk_false(); } @@ -477,6 +479,8 @@ Notes: return xs[0]; } + SASSERT(n > 1); + // y0 -> y1 // x0 -> y0 // x1 -> y1 diff --git a/src/util/uint_set.h b/src/util/uint_set.h index decaa42ad..0f3715cb1 100644 --- a/src/util/uint_set.h +++ b/src/util/uint_set.h @@ -22,7 +22,6 @@ Revision History: #include "util/util.h" #include "util/vector.h" -COMPILE_TIME_ASSERT(sizeof(unsigned) == 4); class uint_set : unsigned_vector { diff --git a/src/util/util.h b/src/util/util.h index facd5a3cb..9c2bbf7b9 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -34,13 +34,13 @@ Revision History: typedef unsigned long long uint64; #endif -COMPILE_TIME_ASSERT(sizeof(uint64) == 8); +static_assert(sizeof(uint64) == 8, "64 bits please"); #ifndef int64 typedef long long int64; #endif -COMPILE_TIME_ASSERT(sizeof(int64) == 8); +static_assert(sizeof(int64) == 8, "64 bits"); #ifndef INT64_MIN #define INT64_MIN static_cast(0x8000000000000000ull) @@ -112,7 +112,7 @@ inline unsigned next_power_of_two(unsigned v) { unsigned log2(unsigned v); unsigned uint64_log2(uint64 v); -COMPILE_TIME_ASSERT(sizeof(unsigned) == 4); +static_assert(sizeof(unsigned) == 4, "unsigned are 32 bits"); // Return the number of 1 bits in v. static inline unsigned get_num_1bits(unsigned v) { diff --git a/src/util/vector.h b/src/util/vector.h index 2d499a900..2e2640de3 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -72,6 +72,7 @@ class vector { SZ new_capacity = (3 * old_capacity + 1) >> 1; SZ new_capacity_T = sizeof(T) * new_capacity + sizeof(SZ) * 2; if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) { + UNREACHABLE(); throw default_exception("Overflow encountered when expanding vector"); } SZ *mem = (SZ*)memory::reallocate(reinterpret_cast(m_data)-2, new_capacity_T);