diff --git a/.travis.yml b/.travis.yml index 81ddefb8b..a3ffb221e 100644 --- a/.travis.yml +++ b/.travis.yml @@ -17,6 +17,15 @@ env: ############################################################################### # Ubuntu 16.04 LTS ############################################################################### + # 64-bit UBSan Debug build + - 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 UBSAN_BUILD=1 RUN_UNIT_TESTS=SKIP + # 64-bit ASan Debug build + - 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 ASAN_BUILD=1 RUN_UNIT_TESTS=SKIP ASAN_DSO=/usr/lib/clang/3.9/lib/linux/libclang_rt.asan-x86_64.so + # Build for running unit tests under ASan/UBSan + # FIXME: We should really be doing a debug build but the unit tests run too + # slowly when we do that. + - 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 ASAN_BUILD=1 RUN_UNIT_TESTS=BUILD_AND_RUN ASAN_DSO=/usr/lib/clang/3.9/lib/linux/libclang_rt.asan-x86_64.so UBSAN_BUILD=1 RUN_API_EXAMPLES=0 RUN_SYSTEM_TESTS=0 DOTNET_BINDINGS=0 JAVA_BINDINGS=0 PYTHON_BINDINGS=0 + # 64-bit GCC 5.4 RelWithDebInfo - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo # 64-bit Clang 3.9 RelWithDebInfo diff --git a/README-CMake.md b/README-CMake.md index 605c14818..0d323e08f 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -270,6 +270,7 @@ The following useful options can be passed to CMake whilst configuring. * ``API_LOG_SYNC`` - BOOL. If set to ``TRUE`` will enable experimental API log sync feature. * ``WARNINGS_AS_ERRORS`` - STRING. If set to ``TRUE`` compiler warnings will be treated as errors. If set to ``False`` compiler warnings will not be treated as errors. If set to ``SERIOUS_ONLY`` a subset of compiler warnings will be treated as errors. +* ``Z3_C_EXAMPLES_FORCE_CXX_LINKER`` - BOOL. If set to ``TRUE`` the C API examples will request that the C++ linker is used rather than the C linker. On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface. diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile index d8a32edea..87e3c8d67 100644 --- a/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile @@ -30,6 +30,7 @@ RUN apt-get update && \ libgomp1 \ libomp5 \ libomp-dev \ + llvm-3.9 \ make \ mono-devel \ ninja-build \ @@ -47,4 +48,4 @@ RUN useradd -m user && \ echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers USER user WORKDIR /home/user - +ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-3.9/bin/llvm-symbolizer diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile index c28e59e97..c963ce255 100644 --- a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile @@ -16,6 +16,7 @@ RUN apt-get update && \ libgmp-dev \ libgomp1 \ lib32gomp1 \ + llvm-3.9 \ make \ mono-devel \ ninja-build \ @@ -32,4 +33,4 @@ RUN useradd -m user && \ echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers USER user WORKDIR /home/user - +ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-3.9/bin/llvm-symbolizer diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile index 98a5a3e09..08686e275 100644 --- a/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile @@ -18,6 +18,7 @@ RUN apt-get update && \ libgomp1 \ libomp5 \ libomp-dev \ + llvm-3.9 \ make \ mono-devel \ ninja-build \ @@ -35,4 +36,4 @@ RUN useradd -m user && \ echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers USER user WORKDIR /home/user - +ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-3.9/bin/llvm-symbolizer diff --git a/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile index 07504e6b9..eb2e03a43 100644 --- a/contrib/ci/Dockerfiles/z3_build.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_build.Dockerfile @@ -5,6 +5,7 @@ FROM ${DOCKER_IMAGE_BASE} # Build arguments. This can be changed when invoking # `docker build`. ARG ASAN_BUILD +ARG ASAN_DSO ARG BUILD_DOCS ARG CC ARG CXX @@ -13,8 +14,10 @@ ARG JAVA_BINDINGS ARG NO_SUPPRESS_OUTPUT ARG PYTHON_BINDINGS ARG PYTHON_EXECUTABLE=/usr/bin/python2.7 +ARG RUN_API_EXAMPLES ARG RUN_SYSTEM_TESTS ARG RUN_UNIT_TESTS +ARG SANITIZER_PRINT_SUPPRESSIONS ARG TARGET_ARCH ARG TEST_INSTALL ARG UBSAN_BUILD @@ -32,6 +35,7 @@ ARG Z3_VERBOSE_BUILD_OUTPUT ENV \ ASAN_BUILD=${ASAN_BUILD} \ + ASAN_DSO=${ASAN_DSO} \ BUILD_DOCS=${BUILD_DOCS} \ CC=${CC} \ CXX=${CXX} \ @@ -40,6 +44,8 @@ ENV \ NO_SUPPRESS_OUTPUT=${NO_SUPPRESS_OUTPUT} \ PYTHON_BINDINGS=${PYTHON_BINDINGS} \ PYTHON_EXECUTABLE=${PYTHON_EXECUTABLE} \ + SANITIZER_PRINT_SUPPRESSIONS=${SANITIZER_PRINT_SUPPRESSIONS} \ + RUN_API_EXAMPLES=${RUN_API_EXAMPLES} \ RUN_SYSTEM_TESTS=${RUN_SYSTEM_TESTS} \ RUN_UNIT_TESTS=${RUN_UNIT_TESTS} \ TARGET_ARCH=${TARGET_ARCH} \ @@ -50,6 +56,7 @@ ENV \ USE_OPENMP=${USE_OPENMP} \ Z3_SRC_DIR=${Z3_SRC_DIR} \ Z3_BUILD_DIR=/home/user/z3_build \ + Z3_BUILD_TYPE=${Z3_BUILD_TYPE} \ Z3_CMAKE_GENERATOR=${Z3_CMAKE_GENERATOR} \ Z3_VERBOSE_BUILD_OUTPUT=${Z3_VERBOSE_BUILD_OUTPUT} \ Z3_STATIC_BUILD=${Z3_STATIC_BUILD} \ @@ -62,7 +69,8 @@ ENV \ # Build Z3 RUN mkdir -p "${Z3_SRC_DIR}" && \ - mkdir -p "${Z3_SRC_DIR}/contrib/ci/scripts" + mkdir -p "${Z3_SRC_DIR}/contrib/ci/scripts" && \ + mkdir -p "${Z3_SRC_DIR}/contrib/suppressions/sanitizers" # Deliberately leave out `contrib` ADD /cmake ${Z3_SRC_DIR}/cmake/ ADD /doc ${Z3_SRC_DIR}/doc/ @@ -89,7 +97,13 @@ RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_docs.sh # Test examples ADD \ /contrib/ci/scripts/test_z3_examples_cmake.sh \ + /contrib/ci/scripts/sanitizer_env.sh \ ${Z3_SRC_DIR}/contrib/ci/scripts/ +ADD \ + /contrib/suppressions/sanitizers/asan.txt \ + /contrib/suppressions/sanitizers/lsan.txt \ + /contrib/suppressions/sanitizers/ubsan.txt \ + ${Z3_SRC_DIR}/contrib/suppressions/sanitizers/ RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_examples_cmake.sh # Run unit tests diff --git a/contrib/ci/README.md b/contrib/ci/README.md index 99bbcd7a6..bd1c52792 100644 --- a/contrib/ci/README.md +++ b/contrib/ci/README.md @@ -30,8 +30,10 @@ the future. * `JAVA_BINDINGS` - Build and test Java API bindings (`0` or `1`) * `NO_SUPPRESS_OUTPUT` - Don't suppress output of some commands (`0` or `1`) * `PYTHON_BINDINGS` - Build and test Python API bindings (`0` or `1`) +* `RUN_API_EXAMPLES` - Build and run API examples (`0` or `1`) * `RUN_SYSTEM_TESTS` - Run system tests (`0` or `1`) * `RUN_UNIT_TESTS` - Run unit tests (`BUILD_ONLY` or `BUILD_AND_RUN` or `SKIP`) +* `SANITIZER_PRINT_SUPPRESSIONS` - Show ASan/UBSan suppressions (`0` or `1`) * `TARGET_ARCH` - Target architecture (`x86_64` or `i686`) * `TEST_INSTALL` - Test running `install` target (`0` or `1`) * `UBSAN_BUILD` - Do [UndefinedBehaviourSanitizer](https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html) build (`0` or `1`) diff --git a/contrib/ci/scripts/build_z3_cmake.sh b/contrib/ci/scripts/build_z3_cmake.sh index 76fd0fb84..c1014d5d5 100755 --- a/contrib/ci/scripts/build_z3_cmake.sh +++ b/contrib/ci/scripts/build_z3_cmake.sh @@ -22,6 +22,7 @@ set -o pipefail : ${USE_LTO?"USE_LTO must be specified"} : ${Z3_INSTALL_PREFIX?"Z3_INSTALL_PREFIX must be specified"} : ${Z3_WARNINGS_AS_ERRORS?"Z3_WARNINGS_AS_ERRORS must be specified"} +: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"} ADDITIONAL_Z3_OPTS=() @@ -105,6 +106,16 @@ fi # Set compiler flags source ${SCRIPT_DIR}/set_compiler_flags.sh +if [ "X${UBSAN_BUILD}" = "X1" ]; then + # HACK: When building with UBSan the C++ linker + # must be used to avoid the following linker errors. + # undefined reference to `__ubsan_vptr_type_cache' + # undefined reference to `__ubsan_handle_dynamic_type_cache_miss' + ADDITIONAL_Z3_OPTS+=( \ + '-DZ3_C_EXAMPLES_FORCE_CXX_LINKER=ON' \ + ) +fi + # Sanity check if [ ! -e "${Z3_SRC_DIR}/CMakeLists.txt" ]; then echo "Z3_SRC_DIR is invalid" diff --git a/contrib/ci/scripts/ci_defaults.sh b/contrib/ci/scripts/ci_defaults.sh index d8e9376d8..7a4434bd5 100644 --- a/contrib/ci/scripts/ci_defaults.sh +++ b/contrib/ci/scripts/ci_defaults.sh @@ -9,8 +9,13 @@ 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_API_EXAMPLES="${RUN_API_EXAMPLES:-1}" export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}" export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-BUILD_AND_RUN}" +# Don't print suppressions by default because that breaks the Z3 +# regression tests because they don't expect them to appear in Z3's +# output. +export SANITIZER_PRINT_SUPPRESSIONS="${SANITIZER_PRINT_SUPPRESSIONS:-0}" export TARGET_ARCH="${TARGET_ARCH:-x86_64}" export TEST_INSTALL="${TEST_INSTALL:-1}" export UBSAN_BUILD="${UBSAN_BUILD:-0}" @@ -49,6 +54,7 @@ unset PLATFORM # NOTE: The following variables are not set here because # they are specific to the CI implementation # PYTHON_EXECUTABLE +# ASAN_DSO # Z3_SRC_DIR # Z3_BUILD_DIR # Z3_SYSTEM_TEST_DIR diff --git a/contrib/ci/scripts/run_quiet.sh b/contrib/ci/scripts/run_quiet.sh index 5abc910e8..0f49da3be 100644 --- a/contrib/ci/scripts/run_quiet.sh +++ b/contrib/ci/scripts/run_quiet.sh @@ -34,8 +34,8 @@ function run_quiet() { fi # Clean up rm "${STDOUT}" "${STDERR}" - [ $( echo "${OLD_SETTINGS}" | grep -c 'e') -ne 0 ] && set -e - [ $( echo "${OLD_SETTINGS}" | grep -c 'x') -ne 0 ] && set -x + [ "$( echo "${OLD_SETTINGS}" | grep -c 'e')" != "0" ] && set -e + [ "$( echo "${OLD_SETTINGS}" | grep -c 'x')" != "0" ] && set -x return ${EXIT_STATUS} fi } diff --git a/contrib/ci/scripts/sanitizer_env.sh b/contrib/ci/scripts/sanitizer_env.sh new file mode 100644 index 000000000..f1fa87442 --- /dev/null +++ b/contrib/ci/scripts/sanitizer_env.sh @@ -0,0 +1,82 @@ +# This script is intended to be included by other +# scripts and should not be executed directly + +: ${Z3_SRC_DIR?"Z3_SRC_DIR must be specified"} +: ${ASAN_BUILD?"ASAN_BUILD must be specified"} +: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"} + +if [ "X${ASAN_BUILD}" = "X1" ]; then + # Use suppression files + export LSAN_OPTIONS="suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/lsan.txt" + # NOTE: If you get bad stacktraces try using `fast_unwind_on_malloc=0` + # NOTE: `malloc_context_size` controls size of recorded stacktrace for allocations. + # If the reported stacktraces appear incomplete try increasing the value. + export ASAN_OPTIONS="malloc_context_size=100,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/asan.txt" + + : ${SANITIZER_PRINT_SUPPRESSIONS?"SANITIZER_PRINT_SUPPRESSIONS must be specified"} + if [ "X${SANITIZER_PRINT_SUPPRESSIONS}" = "X1" ]; then + export LSAN_OPTIONS="${LSAN_OPTIONS},print_suppressions=1" + export ASAN_OPTIONS="${ASAN_OPTIONS},print_suppressions=1" + else + export LSAN_OPTIONS="${LSAN_OPTIONS},print_suppressions=0" + export ASAN_OPTIONS="${ASAN_OPTIONS},print_suppressions=0" + fi + + : ${ASAN_SYMBOLIZER_PATH?"ASAN_SYMBOLIZER_PATH must be specified"} + + # Run command without checking for leaks + function run_no_lsan() { + ASAN_OPTIONS="${ASAN_OPTIONS},detect_leaks=0" "${@}" + } + + # Check path to ASan DSO + : ${ASAN_DSO?"ASAN_DSO must be specified"} + if [ ! -e "${ASAN_DSO}" ]; then + echo "ASAN_DSO (${ASAN_DSO}) does not exist" + exit 1 + fi + # FIXME: We'll need to refactor this when we can do UBSan builds + # against a UBSan DSO. + function run_non_native_binding() { + # We need to preload the ASan DSO that libz3 + # will have undefined references to. + # Don't run leak checking because we get lots reported leaks + # in the language runtime (e.g. python). + PLATFORM="$(uname -s)" + case "${PLATFORM}" in + Linux*) + LD_PRELOAD="${ASAN_DSO}" run_no_lsan "${@}" + ;; + Darwin*) + DYLD_INSERT_LIBRARIES="${ASAN_DSO}" run_no_lsan "${@}" + ;; + *) + echo "Unknown platform \"${PLATFORM}\"" + exit 1 + ;; + esac + unset PLATFORM + } +else + # In non-ASan build just run directly + function run_no_lsan() { + "${@}" + } + function run_non_native_binding() { + "${@}" + } +fi + +if [ "X${UBSAN_BUILD}" = "X1" ]; then + # `halt_on_error=1,abort_on_error=1` means that on the first UBSan error + # the program will terminate by calling `abort(). Without this UBSan will + # allow execution to continue. We also use a suppression file. + export UBSAN_OPTIONS="halt_on_error=1,abort_on_error=1,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/ubsan.txt" + + : ${SANITIZER_PRINT_SUPPRESSIONS?"SANITIZER_PRINT_SUPPRESSIONS must be specified"} + if [ "X${SANITIZER_PRINT_SUPPRESSIONS}" = "X1" ]; then + export UBSAN_OPTIONS="${UBSAN_OPTIONS},print_suppressions=1" + else + export UBSAN_OPTIONS="${UBSAN_OPTIONS},print_suppressions=0" + fi +fi diff --git a/contrib/ci/scripts/test_z3_examples_cmake.sh b/contrib/ci/scripts/test_z3_examples_cmake.sh index 2eda3de7b..687efebb4 100755 --- a/contrib/ci/scripts/test_z3_examples_cmake.sh +++ b/contrib/ci/scripts/test_z3_examples_cmake.sh @@ -14,6 +14,13 @@ set -o pipefail : ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"} : ${DOTNET_BINDINGS?"DOTNET_BINDINGS must be specified"} : ${JAVA_BINDINGS?"JAVA_BINDINGS must be specified"} +: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"} +: ${RUN_API_EXAMPLES?"RUN_API_EXAMPLES must be specified"} + +if [ "X${RUN_API_EXAMPLES}" = "X0" ]; then + echo "Skipping run of API examples" + exit 0 +fi # Set compiler flags source ${SCRIPT_DIR}/set_compiler_flags.sh @@ -21,6 +28,9 @@ source ${SCRIPT_DIR}/set_compiler_flags.sh # Set CMake generator args source ${SCRIPT_DIR}/set_generator_args.sh +# Sanitizer environment variables +source ${SCRIPT_DIR}/sanitizer_env.sh + cd "${Z3_BUILD_DIR}" # Build and run C example @@ -38,9 +48,21 @@ run_quiet examples/tptp_build_dir/z3_tptp5 -help # Build an run c_maxsat_example cmake --build $(pwd) --target c_maxsat_example "${GENERATOR_ARGS[@]}" -run_quiet \ - examples/c_maxsat_example_build_dir/c_maxsat_example \ - ${Z3_SRC_DIR}/examples/maxsat/ex.smt +# FIXME: It is known that the maxsat example leaks memory and the +# the Z3 developers have stated this is "wontfix". +# See https://github.com/Z3Prover/z3/issues/1299 +run_no_lsan \ + run_quiet \ + examples/c_maxsat_example_build_dir/c_maxsat_example \ + ${Z3_SRC_DIR}/examples/maxsat/ex.smt + +if [ "X${UBSAN_BUILD}" = "X1" ]; then + # FIXME: We really need libz3 to link against a shared UBSan runtime. + # Right now we link against the static runtime which breaks all the + # non-native language bindings. + echo "FIXME: Can't run other examples when building with UBSan" + exit 0 +fi if [ "X${PYTHON_BINDINGS}" = "X1" ]; then @@ -48,16 +70,21 @@ if [ "X${PYTHON_BINDINGS}" = "X1" ]; then # `all_interval_series.py` produces a lot of output so just throw # away output. # TODO: This example is slow should we remove it from testing? - run_quiet ${PYTHON_EXECUTABLE} python/all_interval_series.py - run_quiet ${PYTHON_EXECUTABLE} python/complex.py - run_quiet ${PYTHON_EXECUTABLE} python/example.py + if [ "X${ASAN_BUILD}" = "X1" -a "X${Z3_BUILD_TYPE}" = "XDebug" ]; then + # Too slow when doing ASan Debug build + echo "Skipping all_interval_series.py under ASan Debug build" + else + run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/all_interval_series.py + fi + run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/complex.py + run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/example.py # FIXME: `hamiltonian.py` example is disabled because its too slow. #${PYTHON_EXECUTABLE} python/hamiltonian.py - run_quiet ${PYTHON_EXECUTABLE} python/marco.py - run_quiet ${PYTHON_EXECUTABLE} python/mss.py - run_quiet ${PYTHON_EXECUTABLE} python/socrates.py - run_quiet ${PYTHON_EXECUTABLE} python/visitor.py - run_quiet ${PYTHON_EXECUTABLE} python/z3test.py + run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/marco.py + run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/mss.py + run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/socrates.py + run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/visitor.py + run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/z3test.py fi if [ "X${DOTNET_BINDINGS}" = "X1" ]; then @@ -65,7 +92,7 @@ if [ "X${DOTNET_BINDINGS}" = "X1" ]; then # FIXME: Move compliation step into CMake target mcs ${Z3_SRC_DIR}/examples/dotnet/Program.cs /target:exe /out:dotnet_test.exe /reference:Microsoft.Z3.dll /r:System.Numerics.dll # Run .NET example - run_quiet mono ./dotnet_test.exe + run_quiet run_non_native_binding mono ./dotnet_test.exe fi if [ "X${JAVA_BINDINGS}" = "X1" ]; then @@ -82,6 +109,14 @@ if [ "X${JAVA_BINDINGS}" = "X1" ]; then # Assume Linux for now export LD_LIBRARY_PATH=$(pwd):${LD_LIBRARY_PATH} fi - run_quiet java -cp .:examples/java:com.microsoft.z3.jar JavaExample + if [ "X${ASAN_BUILD}" = "X1" ]; then + # The JVM seems to crash (SEGV) if we pre-load ASan + # so don't run it for now. + echo "Skipping JavaExample under ASan build" + else + run_quiet \ + run_non_native_binding \ + java -cp .:examples/java:com.microsoft.z3.jar JavaExample + fi fi diff --git a/contrib/ci/scripts/test_z3_system_tests.sh b/contrib/ci/scripts/test_z3_system_tests.sh index dfb1084a4..19c179268 100755 --- a/contrib/ci/scripts/test_z3_system_tests.sh +++ b/contrib/ci/scripts/test_z3_system_tests.sh @@ -10,12 +10,17 @@ set -o pipefail : ${PYTHON_BINDINGS?"PYTHON_BINDINGS must be specified"} : ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"} : ${Z3_SYSTEM_TEST_DIR?"Z3_SYSTEM_TEST_DIR must be specified"} +: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"} if [ "X${RUN_SYSTEM_TESTS}" != "X1" ]; then echo "Skipping system tests" exit 0 fi +# Sanitizer environment variables +SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" +source ${SCRIPT_DIR}/sanitizer_env.sh + Z3_EXE="${Z3_BUILD_DIR}/z3" Z3_LIB_DIR="${Z3_BUILD_DIR}" @@ -23,7 +28,7 @@ Z3_LIB_DIR="${Z3_BUILD_DIR}" Z3_SYSTEM_TEST_GIT_URL="${Z3_GIT_URL:-https://github.com/Z3Prover/z3test.git}" # Clone repo to destination -mkdir -p "${Z3_SYSTEM_TEST_GIT_URL}" +mkdir -p "${Z3_SYSTEM_TEST_DIR}" git clone "${Z3_SYSTEM_TEST_GIT_URL}" "${Z3_SYSTEM_TEST_DIR}" cd "${Z3_SYSTEM_TEST_DIR}" @@ -48,7 +53,18 @@ fi if [ "X${PYTHON_BINDINGS}" = "X1" ]; then # Run python binding tests - ${PYTHON_EXECUTABLE} scripts/test_pyscripts.py "${Z3_LIB_DIR}" regressions/python/ + if [ "X${UBSAN_BUILD}" = "X1" ]; then + # FIXME: We need to build libz3 with a shared UBSan runtime for the bindings + # to work. + echo "FIXME: Skipping python binding tests when building with UBSan" + elif [ "X${ASAN_BUILD}" = "X1" ]; then + # FIXME: The `test_pyscripts.py` doesn't propagate LD_PRELOAD + # so under ASan the tests fail to run + # to work. + echo "FIXME: Skipping python binding tests when building with ASan" + else + run_non_native_binding ${PYTHON_EXECUTABLE} scripts/test_pyscripts.py "${Z3_LIB_DIR}" regressions/python/ + fi fi # FIXME: Run `scripts/test_cs.py` once it has been modified to support mono diff --git a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh index e1c927f58..60c29556b 100755 --- a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh +++ b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh @@ -13,6 +13,9 @@ set -o pipefail # Set CMake generator args source ${SCRIPT_DIR}/set_generator_args.sh +# Sanitizer environment variables +source ${SCRIPT_DIR}/sanitizer_env.sh + cd "${Z3_BUILD_DIR}" function build_unit_tests() { diff --git a/contrib/ci/scripts/travis_ci_linux_entry_point.sh b/contrib/ci/scripts/travis_ci_linux_entry_point.sh index bd2c9d2d1..731ea9ff0 100755 --- a/contrib/ci/scripts/travis_ci_linux_entry_point.sh +++ b/contrib/ci/scripts/travis_ci_linux_entry_point.sh @@ -84,6 +84,14 @@ if [ -n "${ASAN_BUILD}" ]; then BUILD_OPTS+=("--build-arg" "ASAN_BUILD=${ASAN_BUILD}") fi +if [ -n "${ASAN_DSO}" ]; then + BUILD_OPTS+=("--build-arg" "ASAN_DSO=${ASAN_DSO}") +fi + +if [ -n "${SANITIZER_PRINT_SUPPRESSIONS}" ]; then + BUILD_OPTS+=("--build-arg" "SANITIZER_PRINT_SUPPRESSIONS=${SANITIZER_PRINT_SUPPRESSIONS}") +fi + if [ -n "${UBSAN_BUILD}" ]; then BUILD_OPTS+=("--build-arg" "UBSAN_BUILD=${UBSAN_BUILD}") fi @@ -92,6 +100,10 @@ if [ -n "${TEST_INSTALL}" ]; then BUILD_OPTS+=("--build-arg" "TEST_INSTALL=${TEST_INSTALL}") fi +if [ -n "${RUN_API_EXAMPLES}" ]; then + BUILD_OPTS+=("--build-arg" "RUN_API_EXAMPLES=${RUN_API_EXAMPLES}") +fi + if [ -n "${RUN_SYSTEM_TESTS}" ]; then BUILD_OPTS+=("--build-arg" "RUN_SYSTEM_TESTS=${RUN_SYSTEM_TESTS}") fi diff --git a/contrib/suppressions/README.md b/contrib/suppressions/README.md new file mode 100644 index 000000000..90df39084 --- /dev/null +++ b/contrib/suppressions/README.md @@ -0,0 +1,7 @@ +# Suppression files + +This directory contains suppression files used by various +program analysis tools. + +Suppression files tell a program analysis tool to suppress +various warnings/errors. diff --git a/contrib/suppressions/maintainers.txt b/contrib/suppressions/maintainers.txt new file mode 100644 index 000000000..caa6798c6 --- /dev/null +++ b/contrib/suppressions/maintainers.txt @@ -0,0 +1,3 @@ +# Maintainers + +- Dan Liew (@delcypher) diff --git a/contrib/suppressions/sanitizers/README.md b/contrib/suppressions/sanitizers/README.md new file mode 100644 index 000000000..f76f920b2 --- /dev/null +++ b/contrib/suppressions/sanitizers/README.md @@ -0,0 +1,4 @@ +# Sanitizer supression files + +This directory contains files used to suppress +ASan/LSan/UBSan warnings/errors. diff --git a/contrib/suppressions/sanitizers/asan.txt b/contrib/suppressions/sanitizers/asan.txt new file mode 100644 index 000000000..f058adfe2 --- /dev/null +++ b/contrib/suppressions/sanitizers/asan.txt @@ -0,0 +1 @@ +# AddressSanitizer suppression file diff --git a/contrib/suppressions/sanitizers/lsan.txt b/contrib/suppressions/sanitizers/lsan.txt new file mode 100644 index 000000000..1480b7c09 --- /dev/null +++ b/contrib/suppressions/sanitizers/lsan.txt @@ -0,0 +1,5 @@ +# LeakSanitizer suppression file + +# Ignore Clang OpenMP leaks. +# See https://github.com/Z3Prover/z3/issues/1308 +leak:___kmp_allocate diff --git a/contrib/suppressions/sanitizers/ubsan.txt b/contrib/suppressions/sanitizers/ubsan.txt new file mode 100644 index 000000000..4d19e40be --- /dev/null +++ b/contrib/suppressions/sanitizers/ubsan.txt @@ -0,0 +1,7 @@ +# UndefinedBehavior sanitizer suppression file +# FIXME: UBSan doesn't usually have false positives so we need to fix all of these! + +# Occurs when running tptp example +# See https://github.com/Z3Prover/z3/issues/964 +null:rational.h +null:mpq.h diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index ba7f6ee59..6c50320ed 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -7,6 +7,30 @@ else() set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG "") endif() +option(Z3_C_EXAMPLES_FORCE_CXX_LINKER + "Force C++ linker when building C example projects" OFF) + +if (Z3_C_EXAMPLES_FORCE_CXX_LINKER) + # HACK: This is a workaround for UBSan. + message(STATUS "Forcing C++ linker to be used when building example C projects") + set(EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG + "-DFORCE_CXX_LINKER=ON" + ) +else() + set(EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG "") +endif() + +if (DEFINED CMAKE_CONFIGURATION_TYPES) + message(WARNING + "Cannot set built type of external project when building with a " + "multi-configuration generator") + set(EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG "") +else() + set(EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG + "-DCMAKE_BUILD_TYPE:STRING=${CMAKE_BUILD_TYPE}" + ) +endif() + ################################################################################ # Build example project using libz3's C API as an external project ################################################################################ @@ -14,7 +38,10 @@ ExternalProject_Add(c_example DEPENDS libz3 # Configure step SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/c" - CMAKE_ARGS "-DZ3_DIR=${CMAKE_BINARY_DIR}" + CMAKE_ARGS + "-DZ3_DIR=${CMAKE_BINARY_DIR}" + "${EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG}" + "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}" # Build step ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_example_build_dir" @@ -30,7 +57,10 @@ ExternalProject_Add(c_maxsat_example DEPENDS libz3 # Configure step SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/maxsat" - CMAKE_ARGS "-DZ3_DIR=${CMAKE_BINARY_DIR}" + CMAKE_ARGS + "-DZ3_DIR=${CMAKE_BINARY_DIR}" + "${EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG}" + "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}" # Build step ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_maxsat_example_build_dir" @@ -47,7 +77,9 @@ ExternalProject_Add(cpp_example DEPENDS libz3 # Configure step SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/c++" - CMAKE_ARGS "-DZ3_DIR=${CMAKE_BINARY_DIR}" + CMAKE_ARGS + "-DZ3_DIR=${CMAKE_BINARY_DIR}" + "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}" # Build step ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/cpp_example_build_dir" @@ -63,7 +95,9 @@ ExternalProject_Add(z3_tptp5 DEPENDS libz3 # Configure step SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/tptp" - CMAKE_ARGS "-DZ3_DIR=${CMAKE_BINARY_DIR}" + CMAKE_ARGS + "-DZ3_DIR=${CMAKE_BINARY_DIR}" + "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}" # Build step ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/tptp_build_dir" diff --git a/examples/c/CMakeLists.txt b/examples/c/CMakeLists.txt index dd8fa6328..bac08e460 100644 --- a/examples/c/CMakeLists.txt +++ b/examples/c/CMakeLists.txt @@ -22,6 +22,17 @@ message(STATUS "Found Z3 ${Z3_VERSION_STRING}") message(STATUS "Z3_DIR: ${Z3_DIR}") add_executable(c_example test_capi.c) + +option(FORCE_CXX_LINKER "Force linker with C++ linker" OFF) +if (FORCE_CXX_LINKER) + # This is a hack for avoiding UBSan linking errors + message(STATUS "Forcing use of C++ linker") + set_target_properties(c_example + PROPERTIES + LINKER_LANGUAGE CXX + ) +endif() + target_include_directories(c_example PRIVATE ${Z3_C_INCLUDE_DIRS}) target_link_libraries(c_example PRIVATE ${Z3_LIBRARIES}) diff --git a/examples/maxsat/CMakeLists.txt b/examples/maxsat/CMakeLists.txt index b48e167ea..019243ecf 100644 --- a/examples/maxsat/CMakeLists.txt +++ b/examples/maxsat/CMakeLists.txt @@ -25,6 +25,16 @@ add_executable(c_maxsat_example maxsat.c) target_include_directories(c_maxsat_example PRIVATE ${Z3_C_INCLUDE_DIRS}) target_link_libraries(c_maxsat_example PRIVATE ${Z3_LIBRARIES}) +option(FORCE_CXX_LINKER "Force linker with C++ linker" OFF) +if (FORCE_CXX_LINKER) + # This is a hack for avoiding UBSan linking errors + message(STATUS "Forcing use of C++ linker") + set_target_properties(c_maxsat_example + PROPERTIES + LINKER_LANGUAGE CXX + ) +endif() + if ("${CMAKE_SYSTEM_NAME}" MATCHES "[Ww]indows") # On Windows we need to copy the Z3 libraries # into the same directory as the executable diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index cac12413e..9116c5d95 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -768,7 +768,7 @@ func_decl * basic_decl_plugin::mk_compressed_proof_decl(char const * name, basic func_decl * basic_decl_plugin::mk_proof_decl(char const * name, basic_op_kind k, unsigned num_parents, ptr_vector & cache) { if (num_parents >= cache.size()) { - cache.resize(num_parents+1, 0); + cache.resize(num_parents+1); } if (cache[num_parents] == 0) { cache[num_parents] = mk_proof_decl(name, k, num_parents); diff --git a/src/ast/ast.h b/src/ast/ast.h index 4eb43d30b..7e1645753 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -121,6 +121,20 @@ public: explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {} parameter(parameter const&); + parameter(parameter && other) : m_kind(other.m_kind) { + switch (other.m_kind) { + case PARAM_INT: m_int = other.get_int(); break; + case PARAM_AST: m_ast = other.get_ast(); break; + case PARAM_SYMBOL: m_symbol = other.m_symbol; break; + case PARAM_RATIONAL: m_rational = 0; std::swap(m_rational, other.m_rational); break; + case PARAM_DOUBLE: m_dval = other.m_dval; break; + case PARAM_EXTERNAL: m_ext_id = other.m_ext_id; break; + default: + UNREACHABLE(); + break; + } + } + ~parameter(); parameter& operator=(parameter const& other); diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index fcf9a9f8f..093d0f548 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -863,8 +863,7 @@ app * bv_util::mk_numeral(rational const & val, sort* s) const { } app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const { - parameter p1(val); - parameter p[2] = { p1, parameter(static_cast(bv_size)) }; + parameter p[2] = { parameter(val), parameter(static_cast(bv_size)) }; return m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, 0); } diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index 247e9dea1..7368d7935 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/src/ast/normal_forms/nnf.cpp @@ -40,7 +40,7 @@ enum nnf_mode { transformation will be in skolem normal form. If a formula is too expensive to be put into NNF, then nested quantifiers and labels are renamed. - + This mode is sufficient when using E-matching. */ NNF_QUANT, /* A subformula is put into NNF if it contains @@ -48,7 +48,7 @@ enum nnf_mode { quantifier. The result of the transformation will be in skolem normal form, and the body of quantifiers will be in NNF. If a ground formula is too expensive to - be put into NNF, then nested quantifiers and labels + be put into NNF, then nested quantifiers and labels are renamed. This mode is sufficient when using Superposition @@ -89,7 +89,7 @@ class skolemizer { } TRACE("skolemizer", tout << "skid: " << q->get_skid() << "\n";); - + expr_ref_vector substitution(m()); unsigned num_decls = q->get_num_decls(); for (unsigned i = num_decls; i > 0; ) { @@ -111,7 +111,7 @@ class skolemizer { substitution.push_back(0); } // - // (VAR num_decls) ... (VAR num_decls+sz-1) + // (VAR num_decls) ... (VAR num_decls+sz-1) // are in positions num_decls .. num_decls+sz-1 // std::reverse(substitution.c_ptr(), substitution.c_ptr() + substitution.size()); @@ -139,7 +139,7 @@ class skolemizer { s(body, substitution.size(), substitution.c_ptr(), r); p = 0; if (m().proofs_enabled()) { - if (q->is_forall()) + if (q->is_forall()) p = m().mk_skolemization(m().mk_not(q), m().mk_not(r)); else p = m().mk_skolemization(q, r); @@ -175,7 +175,7 @@ public: m_cache_pr.insert(q, p); } } - + bool is_sk_hack(expr * p) const { SASSERT(m().is_pattern(p)); if (to_app(p)->get_num_args() != 1) @@ -204,10 +204,10 @@ struct nnf::imp { unsigned m_i:28; unsigned m_pol:1; // pos/neg polarity unsigned m_in_q:1; // true if m_curr is nested in a quantifier - unsigned m_new_child:1; + unsigned m_new_child:1; unsigned m_cache_result:1; unsigned m_spos; // top of the result stack, when the frame was created. - frame(expr_ref& n, bool pol, bool in_q, bool cache_res, unsigned spos): + frame(expr_ref & n, bool pol, bool in_q, bool cache_res, unsigned spos): m_curr(n), m_i(0), m_pol(pol), @@ -223,22 +223,22 @@ struct nnf::imp { #define POS_NQ_CIDX 1 // positive polarity and not nested in a quantifier #define NEG_Q_CIDX 2 // negative polarity and nested in a quantifier #define POS_Q_CIDX 3 // positive polarity and nested in a quantifier - + ast_manager & m_manager; vector m_frame_stack; expr_ref_vector m_result_stack; - + typedef act_cache cache; cache * m_cache[4]; expr_ref_vector m_todo_defs; proof_ref_vector m_todo_proofs; - + // proof generation goodness ---- proof_ref_vector m_result_pr_stack; cache * m_cache_pr[4]; // ------------------------------ - + skolemizer m_skolemizer; // configuration ---------------- @@ -249,7 +249,7 @@ struct nnf::imp { name_exprs * m_name_nested_formulas; name_exprs * m_name_quant; - + unsigned long long m_max_memory; // in bytes imp(ast_manager & m, defined_names & n, params_ref const & p): @@ -292,9 +292,9 @@ struct nnf::imp { m_mode = NNF_FULL; else if (mode_sym == "quantifiers") m_mode = NNF_QUANT; - else + else throw nnf_params_exception("invalid NNF mode"); - + TRACE("nnf", tout << "nnf-mode: " << m_mode << " " << mode_sym << "\n" << _p << "\n";); m_ignore_labels = p.ignore_labels(); @@ -324,12 +324,11 @@ struct nnf::imp { } void push_frame(expr * t, bool pol, bool in_q, bool cache_res) { - expr_ref tr(t, m()); - m_frame_stack.push_back(frame(tr, pol, in_q, cache_res, m_result_stack.size())); + m_frame_stack.push_back(frame(expr_ref(t, m()), pol, in_q, cache_res, m_result_stack.size())); } - static unsigned get_cache_idx(bool pol, bool in_q) { - return static_cast(in_q) * 2 + static_cast(pol); + static unsigned get_cache_idx(bool pol, bool in_q) { + return static_cast(in_q) * 2 + static_cast(pol); } void cache_result(expr * t, bool pol, bool in_q, expr * v, proof * pr) { @@ -339,8 +338,8 @@ struct nnf::imp { m_cache_pr[idx]->insert(t, pr); } - expr * get_cached(expr * t, bool pol, bool in_q) const { - return m_cache[get_cache_idx(pol, in_q)]->find(t); + expr * get_cached(expr * t, bool pol, bool in_q) const { + return m_cache[get_cache_idx(pol, in_q)]->find(t); } proof * get_cached_pr(expr * t, bool pol, bool in_q) const { @@ -368,12 +367,12 @@ struct nnf::imp { return false; } - + void checkpoint() { cooperate("nnf"); if (memory::get_allocation_size() > m_max_memory) throw nnf_exception(Z3_MAX_MEMORY_MSG); - if (m().canceled()) + if (m().canceled()) throw nnf_exception(m().limit().get_cancel_msg()); } @@ -382,11 +381,11 @@ struct nnf::imp { m_frame_stack.back().m_new_child = true; } - void set_new_child_flag(expr * old_t, expr * new_t) { - if (old_t != new_t) - set_new_child_flag(); + void set_new_child_flag(expr * old_t, expr * new_t) { + if (old_t != new_t) + set_new_child_flag(); } - + void skip(expr * t, bool pol) { expr * r = pol ? t : m().mk_not(t); m_result_stack.push_back(r); @@ -448,10 +447,10 @@ struct nnf::imp { if (pol) { if (old_e->get_decl() == new_e->get_decl()) return m().mk_oeq_congruence(old_e, new_e, num_parents, parents); - else + else return m().mk_nnf_pos(old_e, new_e, num_parents, parents); } - else + else return m().mk_nnf_neg(old_e, new_e, num_parents, parents); } @@ -468,7 +467,7 @@ struct nnf::imp { r = m().mk_and(t->get_num_args(), m_result_stack.c_ptr() + fr.m_spos); else r = m().mk_or(t->get_num_args(), m_result_stack.c_ptr() + fr.m_spos); - + m_result_stack.shrink(fr.m_spos); m_result_stack.push_back(r); if (proofs_enabled()) { @@ -520,7 +519,7 @@ struct nnf::imp { r = m().mk_or(2, m_result_stack.c_ptr() + fr.m_spos); else r = m().mk_and(2, m_result_stack.c_ptr() + fr.m_spos); - + m_result_stack.shrink(fr.m_spos); m_result_stack.push_back(r); if (proofs_enabled()) { @@ -554,7 +553,7 @@ struct nnf::imp { default: break; } - + expr * const * rs = m_result_stack.c_ptr() + fr.m_spos; expr * _cond = rs[0]; expr * _not_cond = rs[1]; @@ -574,7 +573,7 @@ struct nnf::imp { } bool is_eq(app * t) const { return m().is_eq(t) || m().is_iff(t); } - + bool process_iff_xor(app * t, frame & fr) { SASSERT(t->get_num_args() == 2); switch (fr.m_i) { @@ -605,7 +604,7 @@ struct nnf::imp { expr * not_rhs = rs[3]; app * r; - if (is_eq(t) == fr.m_pol) + if (is_eq(t) == fr.m_pol) r = m().mk_and(m().mk_or(not_lhs, rhs), m().mk_or(lhs, not_rhs)); else r = m().mk_and(m().mk_or(lhs, rhs), m().mk_or(not_lhs, not_rhs)); @@ -626,7 +625,7 @@ struct nnf::imp { else return process_default(t, fr); } - + bool process_default(app * t, frame & fr) { SASSERT(fr.m_i == 0); if (m_mode == NNF_FULL || t->has_quantifiers() || t->has_labels()) { @@ -636,10 +635,10 @@ struct nnf::imp { m_name_nested_formulas->operator()(t, m_todo_defs, m_todo_proofs, n2, pr2); else m_name_quant->operator()(t, m_todo_defs, m_todo_proofs, n2, pr2); - + if (!fr.m_pol) n2 = m().mk_not(n2); - + m_result_stack.push_back(n2); if (proofs_enabled()) { if (!fr.m_pol) { @@ -666,10 +665,10 @@ struct nnf::imp { expr * arg = m_result_stack.back(); proof * arg_pr = proofs_enabled() ? m_result_pr_stack.back() : 0; - if (m_ignore_labels && !proofs_enabled()) + if (m_ignore_labels && !proofs_enabled()) return true; // the result is already on the stack - + buffer names; bool pos; m().is_label(t, pos, names); @@ -684,7 +683,7 @@ struct nnf::imp { pr = m().mk_transitivity(mk_proof(fr.m_pol, 1, &arg_pr, t, to_app(aux)), m().mk_iff_oeq(m().mk_rewrite(aux, r))); } - } + } else { r = arg; if (proofs_enabled()) { @@ -692,7 +691,7 @@ struct nnf::imp { pr = m().mk_transitivity(p1, arg_pr); } } - + m_result_stack.pop_back(); m_result_stack.push_back(r); if (proofs_enabled()) { @@ -729,7 +728,7 @@ struct nnf::imp { if (m().is_label(t)) { return process_label(t, fr); } - + return process_default(t, fr); } @@ -737,7 +736,7 @@ struct nnf::imp { skip(v, fr.m_pol); return true; } - + bool process_quantifier(quantifier * q, frame & fr) { expr_ref r(m()); proof_ref pr(m()); @@ -757,7 +756,7 @@ struct nnf::imp { if (q->is_forall() == fr.m_pol || !m_skolemize) { expr * new_expr = m_result_stack.back(); proof * new_expr_pr = proofs_enabled() ? m_result_pr_stack.back() : 0; - + ptr_buffer new_patterns; if (q->is_forall() == fr.m_pol) { @@ -773,7 +772,7 @@ struct nnf::imp { // New quantifier has existential force. // So, ignore patterns } - + quantifier * new_q = 0; proof * new_q_pr = 0; if (fr.m_pol) { @@ -786,7 +785,7 @@ struct nnf::imp { if (proofs_enabled()) new_q_pr = m().mk_nnf_neg(q, new_q, 1, &new_expr_pr); } - + m_result_stack.pop_back(); m_result_stack.push_back(new_q); if (proofs_enabled()) { @@ -809,7 +808,7 @@ struct nnf::imp { } return true; } - + void recover_result(expr * t, expr_ref & result, proof_ref & result_pr) { // recover result from the top of the stack. result = m_result_stack.back(); @@ -873,7 +872,7 @@ struct nnf::imp { process(n, r, pr); unsigned old_sz1 = new_defs.size(); unsigned old_sz2 = new_def_proofs.size(); - + for (unsigned i = 0; i < m_todo_defs.size(); i++) { expr_ref dr(m()); proof_ref dpr(m()); @@ -881,7 +880,7 @@ struct nnf::imp { new_defs.push_back(dr); if (proofs_enabled()) { proof * new_pr = m().mk_modus_ponens(m_todo_proofs.get(i), dpr); - new_def_proofs.push_back(new_pr); + new_def_proofs.push_back(new_pr); } } std::reverse(new_defs.c_ptr() + old_sz1, new_defs.c_ptr() + new_defs.size()); @@ -898,7 +897,7 @@ nnf::nnf(ast_manager & m, defined_names & n, params_ref const & p) { nnf::~nnf() { dealloc(m_imp); } - + void nnf::operator()(expr * n, expr_ref_vector & new_defs, proof_ref_vector & new_def_proofs, expr_ref & r, proof_ref & p) { m_imp->operator()(n, new_defs, new_def_proofs, r, p); TRACE("nnf_result", tout << mk_ismt2_pp(n, m_imp->m()) << "\nNNF result:\n" << mk_ismt2_pp(r, m_imp->m()) << "\n";); diff --git a/src/ast/pattern/expr_pattern_match.cpp b/src/ast/pattern/expr_pattern_match.cpp index 770832d1f..628c777d3 100644 --- a/src/ast/pattern/expr_pattern_match.cpp +++ b/src/ast/pattern/expr_pattern_match.cpp @@ -179,11 +179,11 @@ expr_pattern_match::compile(expr* q) } if (m_regs.size() <= max_reg) { - m_regs.resize(max_reg+1, 0); + m_regs.resize(max_reg+1); } if (m_bound_dom.size() <= num_bound) { - m_bound_dom.resize(num_bound+1, 0); - m_bound_rng.resize(num_bound+1, 0); + m_bound_dom.resize(num_bound+1); + m_bound_rng.resize(num_bound+1); } instr.m_kind = YIELD; diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index cd66a5124..a80994f6c 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -272,7 +272,7 @@ void bit_blaster_tpl::mk_multiplier(unsigned sz, expr * const * a_bits, exp zero = m().mk_false(); vector< expr_ref_vector > pps; - pps.resize(sz, m()); + pps.resize(sz, expr_ref_vector(m())); for (unsigned i = 0; i < sz; i++) { checkpoint(); diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 818336c75..ce14349b2 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -125,11 +125,10 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const const mpz & sm1 = m_fm.m_powers2(sbits - 1); const mpz & em1 = m_fm.m_powers2(ebits); - scoped_mpq q(mpqm); - mpqm.set(q, r1.to_mpq()); - SASSERT(mpzm.is_one(q.get().denominator())); + const mpq & q = r1.to_mpq(); + SASSERT(mpzm.is_one(q.denominator())); scoped_mpz z(mpzm); - z = q.get().numerator(); + z = q.numerator(); mpzm.rem(z, sm1, sig); mpzm.div(z, sm1, z); diff --git a/src/ast/substitution/substitution_tree.cpp b/src/ast/substitution/substitution_tree.cpp index 9befb582f..20d5f1590 100644 --- a/src/ast/substitution/substitution_tree.cpp +++ b/src/ast/substitution/substitution_tree.cpp @@ -256,7 +256,7 @@ void substitution_tree::insert(expr * new_expr) { sort * s = to_var(new_expr)->get_sort(); unsigned id = s->get_decl_id(); if (id >= m_vars.size()) - m_vars.resize(id+1, 0); + m_vars.resize(id+1); if (m_vars[id] == 0) m_vars[id] = alloc(var_ref_vector, m_manager); var_ref_vector * v = m_vars[id]; @@ -277,7 +277,7 @@ void substitution_tree::insert(app * new_expr) { unsigned id = d->get_decl_id(); if (id >= m_roots.size()) - m_roots.resize(id+1, 0); + m_roots.resize(id+1); if (!m_roots[id]) { // there is no tree for the function symbol heading new_expr diff --git a/src/ast/used_vars.cpp b/src/ast/used_vars.cpp index a1cd65feb..a3030f087 100644 --- a/src/ast/used_vars.cpp +++ b/src/ast/used_vars.cpp @@ -58,7 +58,7 @@ void used_vars::process(expr * n, unsigned delta) { if (idx >= delta) { idx = idx - delta; if (idx >= m_found_vars.size()) - m_found_vars.resize(idx + 1, 0); + m_found_vars.resize(idx + 1); m_found_vars[idx] = to_var(n)->get_sort(); } break; diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 95c030687..9615e86ce 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1608,7 +1608,9 @@ void cmd_context::validate_check_sat_result(lbool r) { throw cmd_exception("check annotation that says unsat"); #else diagnostic_stream() << "BUG: incompleteness" << std::endl; - exit(ERR_INCOMPLETENESS); + // WORKAROUND: `exit()` causes LSan to be invoked and produce + // many false positives. + _Exit(ERR_INCOMPLETENESS); #endif } break; @@ -1618,7 +1620,9 @@ void cmd_context::validate_check_sat_result(lbool r) { throw cmd_exception("check annotation that says sat"); #else diagnostic_stream() << "BUG: unsoundness" << std::endl; - exit(ERR_UNSOUNDNESS); + // WORKAROUND: `exit()` causes LSan to be invoked and produce + // many false positives. + _Exit(ERR_UNSOUNDNESS); #endif } break; diff --git a/src/math/interval/interval.h b/src/math/interval/interval.h index bae644fac..db3c5a850 100644 --- a/src/math/interval/interval.h +++ b/src/math/interval/interval.h @@ -162,7 +162,7 @@ private: void checkpoint(); public: - interval_manager(reslimit& lim, C const & c); + interval_manager(reslimit& lim, C && c); ~interval_manager(); numeral_manager & m() const { return m_c.m(); } diff --git a/src/math/interval/interval_def.h b/src/math/interval/interval_def.h index e18d9edda..de3a5fa19 100644 --- a/src/math/interval/interval_def.h +++ b/src/math/interval/interval_def.h @@ -31,7 +31,7 @@ Revision History: // #define TRACE_NTH_ROOT template -interval_manager::interval_manager(reslimit& lim, C const & c): m_limit(lim), m_c(c) { +interval_manager::interval_manager(reslimit& lim, C && c): m_limit(lim), m_c(std::move(c)) { m().set(m_minus_one, -1); m().set(m_one, 1); m_pi_n = 0; diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp index 22b50326b..9484c3c83 100644 --- a/src/math/polynomial/algebraic_numbers.cpp +++ b/src/math/polynomial/algebraic_numbers.cpp @@ -2632,10 +2632,14 @@ namespace algebraic_numbers { scoped_mpz neg_n(qm()); qm().set(neg_n, v.numerator()); qm().neg(neg_n); - mpz const coeffs[2] = { neg_n.get(), v.denominator() }; + unsynch_mpz_manager zmgr; + // FIXME: remove these copies + mpz coeffs[2] = { zmgr.dup(neg_n.get()), zmgr.dup(v.denominator()) }; out << "("; upm().display(out, 2, coeffs, "#"); out << ", 1)"; // first root of the polynomial d*# - n + zmgr.del(coeffs[0]); + zmgr.del(coeffs[1]); } else { algebraic_cell * c = a.to_algebraic(); @@ -2678,10 +2682,14 @@ namespace algebraic_numbers { scoped_mpz neg_n(qm()); qm().set(neg_n, v.numerator()); qm().neg(neg_n); - mpz const coeffs[2] = { neg_n.get(), v.denominator() }; + unsynch_mpz_manager zmgr; + // FIXME: remove these copies + mpz coeffs[2] = { zmgr.dup(neg_n.get()), zmgr.dup(v.denominator()) }; out << "(root-obj "; upm().display_smt2(out, 2, coeffs, "x"); out << " 1)"; // first root of the polynomial d*# - n + zmgr.del(coeffs[0]); + zmgr.del(coeffs[1]); } else { algebraic_cell * c = a.to_algebraic(); diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 7adaf9adb..d6d392148 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -4822,10 +4822,9 @@ namespace polynomial { polynomial * mk_x_minus_y(var x, var y) { numeral zero(0); - numeral one(1); numeral minus_one; // It is not safe to initialize with -1 when numeral_manager is GF_2 m_manager.set(minus_one, -1); - numeral as[2] = { one, minus_one }; + numeral as[2] = { numeral(1), std::move(minus_one) }; var xs[2] = { x, y }; return mk_linear(2, as, xs, zero); } @@ -4845,8 +4844,7 @@ namespace polynomial { polynomial * mk_x_plus_y(var x, var y) { numeral zero(0); - numeral one(1); - numeral as[2] = { one, one }; + numeral as[2] = { numeral(1), numeral(1) }; var xs[2] = { x, y }; return mk_linear(2, as, xs, zero); } diff --git a/src/math/polynomial/upolynomial_factorization_int.h b/src/math/polynomial/upolynomial_factorization_int.h index 640c5ad5c..ea2b51d8f 100644 --- a/src/math/polynomial/upolynomial_factorization_int.h +++ b/src/math/polynomial/upolynomial_factorization_int.h @@ -45,7 +45,7 @@ namespace upolynomial { for (unsigned i = 0; i < p.size(); ++ i) { numeral p_i; // no need to delete, we keep it pushed in zp_p zp_nm.set(p_i, p[i]); - zp_p.push_back(p_i); + zp_p.push_back(std::move(p_i)); } zp_upm.trim(zp_p); } diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h index dc4ce8695..4edbb2b9d 100644 --- a/src/math/simplex/sparse_matrix.h +++ b/src/math/simplex/sparse_matrix.h @@ -35,7 +35,7 @@ namespace simplex { struct row_entry { numeral m_coeff; var_t m_var; - row_entry(numeral const& c, var_t v): m_coeff(c), m_var(v) {} + row_entry(numeral && c, var_t v) : m_coeff(std::move(c)), m_var(v) {} }; private: @@ -61,7 +61,7 @@ namespace simplex { int m_col_idx; int m_next_free_row_entry_idx; }; - _row_entry(numeral const & c, var_t v): row_entry(c, v), m_col_idx(0) {} + _row_entry(numeral && c, var_t v) : row_entry(std::move(c), v), m_col_idx(0) {} _row_entry() : row_entry(numeral(), dead_id), m_col_idx(0) {} bool is_dead() const { return row_entry::m_var == dead_id; } }; diff --git a/src/math/subpaving/subpaving_t_def.h b/src/math/subpaving/subpaving_t_def.h index 108b6aac3..3574787d8 100644 --- a/src/math/subpaving/subpaving_t_def.h +++ b/src/math/subpaving/subpaving_t_def.h @@ -739,7 +739,7 @@ void context_t::del_sum(polynomial * p) { template var context_t::mk_sum(numeral const & c, unsigned sz, numeral const * as, var const * xs) { - m_num_buffer.reserve(num_vars(), numeral()); + m_num_buffer.reserve(num_vars()); for (unsigned i = 0; i < sz; i++) { SASSERT(xs[i] < num_vars()); nm().set(m_num_buffer[xs[i]], as[i]); diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp index 6699ef0e2..e458cc4b0 100644 --- a/src/model/func_interp.cpp +++ b/src/model/func_interp.cpp @@ -117,7 +117,7 @@ bool func_interp::is_fi_entry_expr(expr * e, ptr_vector & args) { (m_arity > 1 && (!m().is_and(c) || to_app(c)->get_num_args() != m_arity))) return false; - args.resize(m_arity, 0); + args.resize(m_arity); for (unsigned i = 0; i < m_arity; i++) { expr * ci = (m_arity == 1 && i == 0) ? c : to_app(c)->get_arg(i); diff --git a/src/muz/rel/dl_instruction.h b/src/muz/rel/dl_instruction.h index c29681f37..56dd249a5 100644 --- a/src/muz/rel/dl_instruction.h +++ b/src/muz/rel/dl_instruction.h @@ -128,7 +128,7 @@ namespace datalog { void set_reg(reg_idx i, reg_type val) { if (i >= m_registers.size()) { check_overflow(i); - m_registers.resize(i+1,0); + m_registers.resize(i+1); } if (m_registers[i]) { m_registers[i]->deallocate(); diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp index fd13978d2..c4fb57eeb 100644 --- a/src/muz/rel/dl_mk_explanations.cpp +++ b/src/muz/rel/dl_mk_explanations.cpp @@ -465,7 +465,7 @@ namespace datalog { unsigned sz = r.get_signature().size(); ptr_vector subst_arg; - subst_arg.resize(sz, 0); + subst_arg.resize(sz); unsigned ofs = sz-1; for (unsigned i=0; iget_family_id(); SASSERT(fid != null_family_id); if (static_cast(m_plugins.size()) <= fid) { - m_plugins.resize(fid+1,0); + m_plugins.resize(fid+1); } SASSERT(!m_plugins[fid]); m_plugins[fid] = p; diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 67101b4d8..84534bf3f 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1311,7 +1311,6 @@ namespace sat { clause_use_list & neg_occs = m_use_list.get(neg_l); unsigned num_pos = pos_occs.size() + num_bin_pos; unsigned num_neg = neg_occs.size() + num_bin_neg; - m_elim_counter -= num_pos + num_neg; TRACE("resolution", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << "\n";); @@ -1352,8 +1351,6 @@ namespace sat { collect_clauses(pos_l, m_pos_cls); collect_clauses(neg_l, m_neg_cls); - m_elim_counter -= num_pos * num_neg + before_lits; - TRACE("resolution_detail", tout << "collecting number of after_clauses\n";); unsigned before_clauses = num_pos + num_neg; unsigned after_clauses = 0; @@ -1376,7 +1373,7 @@ namespace sat { } } TRACE("resolution", tout << "found var to eliminate, before: " << before_clauses << " after: " << after_clauses << "\n";); - + m_elim_counter -= num_pos * num_neg + before_lits; // eliminate variable model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v); diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 11cc846b8..1ed5f2fe1 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -38,7 +38,7 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p): m_qhead(0), m_macro_manager(m), m_bv_sharing(m), - m_inconsistent(false), + m_inconsistent(false), m_has_quantifiers(false), m_reduce_asserted_formulas(*this), m_distribute_forall(*this), @@ -54,8 +54,8 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p): m_lift_ite(*this), m_ng_lift_ite(*this), m_find_macros(*this), - m_propagate_values(*this), - m_nnf_cnf(*this), + m_propagate_values(*this), + m_nnf_cnf(*this), m_apply_quasi_macros(*this) { m_macro_finder = alloc(macro_finder, m, m_macro_manager); @@ -68,7 +68,7 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p): void asserted_formulas::setup() { switch (m_params.m_lift_ite) { case LI_FULL: - m_params.m_ng_lift_ite = LI_NONE; + m_params.m_ng_lift_ite = LI_NONE; break; case LI_CONSERVATIVE: if (m_params.m_ng_lift_ite == LI_CONSERVATIVE) @@ -77,7 +77,7 @@ void asserted_formulas::setup() { default: break; } - + if (m_params.m_relevancy_lvl == 0) m_params.m_relevancy_lemma = false; } @@ -93,7 +93,7 @@ void asserted_formulas::push_assertion(expr * e, proof * pr, vectorget_arg(i); proof_ref _pr(m.mk_not_or_elim(pr, i), m); expr_ref narg(mk_not(m, arg), m); - push_assertion(narg, _pr, result); - } + push_assertion(narg, _pr, result); + } } else { result.push_back(justified_expr(m, e, pr)); @@ -130,6 +130,7 @@ void asserted_formulas::set_eliminate_and(bool flag) { p.set_bool("eq2ineq", m_params.m_arith_eq2ineq); p.set_bool("gcd_rounding", true); p.set_bool("expand_select_store", true); + p.set_bool("bv_sort_ac", true); m_rewriter.updt_params(p); flush_cache(); } @@ -139,11 +140,9 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) { proof_ref in_pr(_in_pr, m), pr(_in_pr, m); expr_ref r(e, m); - if (inconsistent()) + if (inconsistent()) return; - m_has_quantifiers |= ::has_quantifiers(e); - if (m_params.m_preprocess) { TRACE("assert_expr_bug", tout << r << "\n";); set_eliminate_and(false); // do not eliminate and before nnf. @@ -156,6 +155,9 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) { } TRACE("assert_expr_bug", tout << "after...\n" << r << "\n";); } + + m_has_quantifiers |= ::has_quantifiers(e); + push_assertion(r, pr, m_formulas); TRACE("asserted_formulas_bug", tout << "after assert_expr\n"; display(tout);); } @@ -183,7 +185,7 @@ void asserted_formulas::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 << " of " << m_scopes.size() << "\n";); m_bv_sharing.pop_scope(num_scopes); @@ -212,7 +214,7 @@ void asserted_formulas::reset() { bool asserted_formulas::check_well_sorted() const { for (justified_expr const& je : m_formulas) { - if (!is_well_sorted(m, je.get_fml())) return false; + if (!is_well_sorted(m, je.get_fml())) return false; } return true; } @@ -224,20 +226,20 @@ void asserted_formulas::reduce() { return; if (m_qhead == m_formulas.size()) return; - if (!m_params.m_preprocess) - return; - if (m_macro_manager.has_macros()) + if (!m_params.m_preprocess) + return; + if (m_macro_manager.has_macros()) invoke(m_find_macros); - + TRACE("before_reduce", display(tout);); CASSERT("well_sorted", check_well_sorted()); - + set_eliminate_and(false); // do not eliminate and before nnf. if (!invoke(m_propagate_values)) return; if (!invoke(m_find_macros)) return; if (!invoke(m_nnf_cnf)) return; set_eliminate_and(true); - if (!invoke(m_reduce_asserted_formulas)) return; + if (!invoke(m_reduce_asserted_formulas)) return; if (!invoke(m_pull_cheap_ite_trees)) return; if (!invoke(m_pull_nested_quantifiers)) return; if (!invoke(m_lift_ite)) return; @@ -276,14 +278,14 @@ bool asserted_formulas::invoke(simplify_fmls& s) { if (!s.should_apply()) return true; IF_VERBOSE(10, verbose_stream() << "(smt." << s.id() << ")\n";); s(); - IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";); - TRACE("reduce_step_ll", ast_mark visited; display_ll(tout, visited);); - CASSERT("well_sorted",check_well_sorted()); - if (inconsistent() || canceled()) { - TRACE("after_reduce", display(tout);); - TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited);); + IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";); + TRACE("reduce_step_ll", ast_mark visited; display_ll(tout, visited);); + CASSERT("well_sorted",check_well_sorted()); + if (inconsistent() || canceled()) { + TRACE("after_reduce", display(tout);); + TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited);); return false; - } + } else { return true; } @@ -301,10 +303,10 @@ void asserted_formulas::display(std::ostream & out) const { void asserted_formulas::display_ll(std::ostream & out, ast_mark & pp_visited) const { if (!m_formulas.empty()) { - for (justified_expr const& f : m_formulas) + for (justified_expr const& f : m_formulas) ast_def_ll_pp(out, m, f.get_fml(), pp_visited, true, false); out << "asserted formulas:\n"; - for (justified_expr const& f : m_formulas) + for (justified_expr const& f : m_formulas) out << "#" << f.get_fml()->get_id() << " "; out << "\n"; } @@ -332,9 +334,9 @@ void asserted_formulas::find_macros_core() { void asserted_formulas::apply_quasi_macros() { TRACE("before_quasi_macros", display(tout);); vector new_fmls; - quasi_macros proc(m, m_macro_manager); - while (proc(m_formulas.size() - m_qhead, - m_formulas.c_ptr() + m_qhead, + quasi_macros proc(m, m_macro_manager); + while (proc(m_formulas.size() - m_qhead, + m_formulas.c_ptr() + m_qhead, new_fmls)) { swap_asserted_formulas(new_fmls); new_fmls.reset(); @@ -348,7 +350,7 @@ void asserted_formulas::nnf_cnf() { vector new_fmls; expr_ref_vector push_todo(m); proof_ref_vector push_todo_prs(m); - + unsigned i = m_qhead; unsigned sz = m_formulas.size(); TRACE("nnf_bug", tout << "i: " << i << " sz: " << sz << "\n";); @@ -378,7 +380,7 @@ void asserted_formulas::nnf_cnf() { CASSERT("well_sorted",is_well_sorted(m, r1)); if (canceled()) { return; - } + } if (m.proofs_enabled()) pr = m.mk_modus_ponens(push_todo_prs.get(k), pr1); push_assertion(r1, pr, new_fmls); @@ -389,8 +391,8 @@ void asserted_formulas::nnf_cnf() { void asserted_formulas::simplify_fmls::operator()() { vector new_fmls; - unsigned sz = af.m_formulas.size(); - for (unsigned i = af.m_qhead; i < sz; i++) { + unsigned sz = af.m_formulas.size(); + for (unsigned i = af.m_qhead; i < sz; i++) { auto& j = af.m_formulas[i]; expr_ref result(m); proof_ref result_pr(m); @@ -406,8 +408,8 @@ void asserted_formulas::simplify_fmls::operator()() { af.push_assertion(result, result_pr, new_fmls); } if (af.canceled()) return; - } - af.swap_asserted_formulas(new_fmls); + } + af.swap_asserted_formulas(new_fmls); TRACE("asserted_formulas", af.display(tout);); post_op(); } @@ -473,12 +475,12 @@ void asserted_formulas::propagate_values() { unsigned asserted_formulas::propagate_values(unsigned i) { expr_ref n(m_formulas[i].get_fml(), m); - expr_ref new_n(m); - proof_ref new_pr(m); - m_rewriter(n, new_n, new_pr); - if (m.proofs_enabled()) { + expr_ref new_n(m); + proof_ref new_pr(m); + m_rewriter(n, new_n, new_pr); + if (m.proofs_enabled()) { proof * pr = m_formulas[i].get_proof(); - new_pr = m.mk_modus_ponens(pr, new_pr); + new_pr = m.mk_modus_ponens(pr, new_pr); } justified_expr j(m, new_n, new_pr); m_formulas[i] = j; @@ -510,10 +512,10 @@ void asserted_formulas::update_substitution(expr* n, proof* pr) { TRACE("propagate_values", tout << "incompatible " << mk_pp(n, m) << "\n";); } if (m.is_not(n, n1)) { - m_scoped_substitution.insert(n1, m.mk_false(), m.mk_iff_false(pr)); + m_scoped_substitution.insert(n1, m.mk_false(), m.mk_iff_false(pr)); } else { - m_scoped_substitution.insert(n, m.mk_true(), m.mk_iff_true(pr)); + m_scoped_substitution.insert(n, m.mk_true(), m.mk_iff_true(pr)); } } @@ -554,13 +556,13 @@ bool asserted_formulas::is_gt(expr* lhs, expr* rhs) { } UNREACHABLE(); } - + return false; } void asserted_formulas::compute_depth(expr* e) { ptr_vector todo; - todo.push_back(e); + todo.push_back(e); while (!todo.empty()) { e = todo.back(); unsigned d = 0; @@ -603,7 +605,7 @@ proof * asserted_formulas::get_inconsistency_proof() const { return 0; } -void asserted_formulas::refine_inj_axiom_fn::simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { +void asserted_formulas::refine_inj_axiom_fn::simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { expr* f = j.get_fml(); if (is_quantifier(f) && simplify_inj_axiom(m, to_quantifier(f), n)) { TRACE("inj_axiom", tout << "simplifying...\n" << mk_pp(f, m) << "\n" << n << "\n";); diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 497aab8db..96334e3ce 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -1999,7 +1999,7 @@ namespace smt { m_ast_manager(ctx.get_manager()), m_mam(m), m_use_filters(use_filters) { - m_args.resize(INIT_ARGS_SIZE, 0); + m_args.resize(INIT_ARGS_SIZE); } ~interpreter() { diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index ac7b1f44b..48d02da26 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1286,7 +1286,7 @@ namespace smt { else { if (depth >= m_almost_cg_tables.size()) { unsigned old_sz = m_almost_cg_tables.size(); - m_almost_cg_tables.resize(depth+1, 0); + m_almost_cg_tables.resize(depth+1); for (unsigned i = old_sz; i < depth + 1; i++) m_almost_cg_tables[i] = alloc(almost_cg_table); } diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 1f519dfda..21df02c76 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -617,8 +617,8 @@ namespace smt { m_else_values.reset(); m_parents.reset(); m_parents.resize(num_vars, -1); - m_defaults.resize(num_vars, 0); - m_else_values.resize(num_vars, 0); + m_defaults.resize(num_vars); + m_else_values.resize(num_vars); if (m_use_unspecified_default) return; diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 616314117..bbed6840d 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -620,7 +620,7 @@ namespace smt { sort * s = recognizer->get_decl()->get_domain(0); if (d->m_recognizers.empty()) { SASSERT(m_util.is_datatype(s)); - d->m_recognizers.resize(m_util.get_datatype_num_constructors(s), 0); + d->m_recognizers.resize(m_util.get_datatype_num_constructors(s)); } SASSERT(d->m_recognizers.size() == m_util.get_datatype_num_constructors(s)); unsigned c_idx = m_util.get_recognizer_constructor_idx(recognizer->get_decl()); diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index 064bdd433..78fb4d03d 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -914,6 +914,8 @@ namespace smt { } verbose_stream() << " + " << m_objective_consts[v] << "\n";); + unsynch_mpq_manager mgr; + unsynch_mpq_inf_manager inf_mgr; unsigned num_nodes = get_num_vars(); unsigned num_edges = m_edges.size(); S.ensure_var(num_nodes + num_edges + m_objectives.size()); @@ -921,8 +923,9 @@ namespace smt { numeral const& a = m_assignment[i]; rational fin = a.get_rational().to_rational(); rational inf = a.get_infinitesimal().to_rational(); - mpq_inf q(fin.to_mpq(), inf.to_mpq()); + mpq_inf q(mgr.dup(fin.to_mpq()), mgr.dup(inf.to_mpq())); S.set_value(i, q); + inf_mgr.del(q); } for (unsigned i = 0; i < num_nodes; ++i) { enode * n = get_enode(i); @@ -933,7 +936,6 @@ namespace smt { } } svector vars; - unsynch_mpq_manager mgr; scoped_mpq_vector coeffs(mgr); coeffs.push_back(mpq(1)); coeffs.push_back(mpq(-1)); @@ -954,8 +956,9 @@ namespace smt { numeral const& w = e.m_offset; rational fin = w.get_rational().to_rational(); rational inf = w.get_infinitesimal().to_rational(); - mpq_inf q(fin.to_mpq(),inf.to_mpq()); + mpq_inf q(mgr.dup(fin.to_mpq()), mgr.dup(inf.to_mpq())); S.set_upper(base_var, q); + inf_mgr.del(q); } unsigned w = num_nodes + num_edges + v; diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index a7153234c..203dd24d2 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -1107,6 +1107,8 @@ unsigned theory_diff_logic::simplex2edge(unsigned e) { template void theory_diff_logic::update_simplex(Simplex& S) { + unsynch_mpq_manager mgr; + unsynch_mpq_inf_manager inf_mgr; unsigned num_nodes = m_graph.get_num_nodes(); vector > const& es = m_graph.get_all_edges(); S.ensure_var(num_simplex_vars()); @@ -1114,13 +1116,13 @@ void theory_diff_logic::update_simplex(Simplex& S) { numeral const& a = m_graph.get_assignment(i); rational fin = a.get_rational().to_rational(); rational inf = a.get_infinitesimal().to_rational(); - mpq_inf q(fin.to_mpq(), inf.to_mpq()); + mpq_inf q(mgr.dup(fin.to_mpq()), mgr.dup(inf.to_mpq())); S.set_value(node2simplex(i), q); + inf_mgr.del(q); } S.set_lower(node2simplex(get_zero()), mpq_inf(mpq(0), mpq(0))); S.set_upper(node2simplex(get_zero()), mpq_inf(mpq(0), mpq(0))); svector vars; - unsynch_mpq_manager mgr; scoped_mpq_vector coeffs(mgr); coeffs.push_back(mpq(1)); coeffs.push_back(mpq(-1)); @@ -1145,8 +1147,9 @@ void theory_diff_logic::update_simplex(Simplex& S) { numeral const& w = e.get_weight(); rational fin = w.get_rational().to_rational(); rational inf = w.get_infinitesimal().to_rational(); - mpq_inf q(fin.to_mpq(),inf.to_mpq()); + mpq_inf q(mgr.dup(fin.to_mpq()), mgr.dup(inf.to_mpq())); S.set_upper(base_var, q); + inf_mgr.del(q); } else { S.unset_upper(base_var); diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 4b52d7950..9d2059f55 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -806,8 +806,9 @@ namespace smt { if (c != 0) { if (m_enable_simplex) { row_info const& info = m_ineq_row_info.find(v); + unsynch_mpq_manager mgr; scoped_eps_numeral coeff(m_mpq_inf_mgr); - coeff = std::make_pair(info.m_bound.to_mpq(), mpq(0)); + coeff = std::make_pair(mgr.dup(info.m_bound.to_mpq()), mpq(0)); unsigned slack = info.m_slack; if (is_true) { update_bound(slack, literal(v), true, coeff); diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index 7f530e5b0..662378bdf 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -279,7 +279,6 @@ namespace smt { // void compile_ineq(ineq& c); void inc_propagations(ineq& c); - unsigned get_compilation_threshold(ineq& c); // // Conflict resolution, cutting plane derivation. diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 8a141665c..97c8db125 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -315,6 +315,7 @@ namespace smt { m_trail.push_back(node); if (!cut_var_map.contains(baseNode)) { T_cut * varInfo = alloc(T_cut); + m_cut_allocs.push_back(varInfo); varInfo->level = slevel; varInfo->vars[node] = 1; cut_var_map.insert(baseNode, std::stack()); @@ -323,6 +324,7 @@ namespace smt { } else { if (cut_var_map[baseNode].empty()) { T_cut * varInfo = alloc(T_cut); + m_cut_allocs.push_back(varInfo); varInfo->level = slevel; varInfo->vars[node] = 1; cut_var_map[baseNode].push(varInfo); @@ -330,6 +332,7 @@ namespace smt { } else { if (cut_var_map[baseNode].top()->level < slevel) { T_cut * varInfo = alloc(T_cut); + m_cut_allocs.push_back(varInfo); varInfo->level = slevel; cut_vars_map_copy(varInfo->vars, cut_var_map[baseNode].top()->vars); varInfo->vars[node] = 1; @@ -359,6 +362,7 @@ namespace smt { if (!cut_var_map.contains(destNode)) { T_cut * varInfo = alloc(T_cut); + m_cut_allocs.push_back(varInfo); varInfo->level = slevel; cut_vars_map_copy(varInfo->vars, cut_var_map[srcNode].top()->vars); cut_var_map.insert(destNode, std::stack()); @@ -367,6 +371,7 @@ namespace smt { } else { if (cut_var_map[destNode].empty() || cut_var_map[destNode].top()->level < slevel) { T_cut * varInfo = alloc(T_cut); + m_cut_allocs.push_back(varInfo); varInfo->level = slevel; cut_vars_map_copy(varInfo->vars, cut_var_map[destNode].top()->vars); cut_vars_map_copy(varInfo->vars, cut_var_map[srcNode].top()->vars); diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 686fcdd57..acac8cad1 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -18,9 +18,12 @@ #define _THEORY_STR_H_ #include "util/trail.h" +#include "util/union_find.h" +#include "util/scoped_ptr_vector.h" #include "ast/ast_pp.h" #include "ast/arith_decl_plugin.h" #include "ast/rewriter/th_rewriter.h" +#include "ast/seq_decl_plugin.h" #include "smt/smt_theory.h" #include "smt/params/theory_str_params.h" #include "smt/proto_model/value_factory.h" @@ -29,8 +32,6 @@ #include #include #include -#include "ast/seq_decl_plugin.h" -#include "util/union_find.h" namespace smt { @@ -292,6 +293,7 @@ protected: bool avoidLoopCut; bool loopDetected; obj_map > cut_var_map; + scoped_ptr_vector m_cut_allocs; expr_ref m_theoryStrOverlapAssumption_term; obj_hashtable variable_set; diff --git a/src/smt/watch_list.h b/src/smt/watch_list.h index 19d3f20a8..1cc29da5a 100644 --- a/src/smt/watch_list.h +++ b/src/smt/watch_list.h @@ -85,6 +85,10 @@ namespace smt { watch_list(): m_data(0) { } + + watch_list(watch_list && other) : m_data(0) { + std::swap(m_data, other.m_data); + } ~watch_list() { destroy(); diff --git a/src/tactic/sls/bvsls_opt_engine.cpp b/src/tactic/sls/bvsls_opt_engine.cpp index e8547fdfd..502bcbde6 100644 --- a/src/tactic/sls/bvsls_opt_engine.cpp +++ b/src/tactic/sls/bvsls_opt_engine.cpp @@ -238,7 +238,7 @@ bool bvsls_opt_engine::what_if( mpz bvsls_opt_engine::find_best_move( ptr_vector & to_evaluate, - mpz score, + mpz & score, unsigned & best_const, mpz & best_value, unsigned & new_bit, diff --git a/src/tactic/sls/bvsls_opt_engine.h b/src/tactic/sls/bvsls_opt_engine.h index 67d9a5d02..9487130d3 100644 --- a/src/tactic/sls/bvsls_opt_engine.h +++ b/src/tactic/sls/bvsls_opt_engine.h @@ -61,7 +61,7 @@ protected: bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp, mpz & best_score, unsigned & best_const, mpz & best_value); - mpz find_best_move(ptr_vector & to_evaluate, mpz score, + mpz find_best_move(ptr_vector & to_evaluate, mpz & score, unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move, mpz const & max_score, expr * objective); diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h index 4ad5c65f4..15f06f096 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -41,7 +41,24 @@ class sls_tracker { struct value_score { value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), score_prune(0.0), has_pos_occ(0), has_neg_occ(0), distance(0), touched(1) {}; + value_score(value_score && other) : + m(other.m), + value(std::move(other.value)), + score(other.score), + score_prune(other.score_prune), + has_pos_occ(other.has_pos_occ), + has_neg_occ(other.has_neg_occ), + distance(other.distance), + touched(other.touched) {} ~value_score() { if (m) m->del(value); } + void operator=(value_score && other) { + this->~value_score(); + new (this) value_score(std::move(other)); + } + value_score& operator=(value_score& other) { + UNREACHABLE(); + return *this; + } unsynch_mpz_manager * m; mpz value; double score; @@ -50,15 +67,6 @@ class sls_tracker { unsigned has_neg_occ; unsigned distance; // max distance from any root unsigned touched; - value_score & operator=(const value_score & other) { - SASSERT(m == 0 || m == other.m); - if (m) m->set(value, 0); else m = other.m; - m->set(value, other.value); - score = other.score; - distance = other.distance; - touched = other.touched; - return *this; - } }; public: @@ -294,7 +302,7 @@ public: if (!m_scores.contains(n)) { value_score vs; vs.m = & m_mpz_manager; - m_scores.insert(n, vs); + m_scores.insert(n, std::move(vs)); } // Update uplinks @@ -539,7 +547,7 @@ public: rational r_val; unsigned bv_sz; m_bv_util.is_numeral(val, r_val, bv_sz); - mpq q = r_val.to_mpq(); + const mpq& q = r_val.to_mpq(); SASSERT(m_mpz_manager.is_one(q.denominator())); set_value(fd, q.numerator()); } @@ -630,7 +638,7 @@ public: if (m_bv_util.is_bv_sort(s)) return get_random_bv(s); else if (m_manager.is_bool(s)) - return get_random_bool(); + return m_mpz_manager.dup(get_random_bool()); else NOT_IMPLEMENTED_YET(); // This only works for bit-vectors for now. } @@ -653,9 +661,7 @@ public: TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); ); for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) { - mpz temp = m_zero; - set_value(it->m_value, temp); - m_mpz_manager.del(temp); + set_value(it->m_value, m_zero); } } @@ -931,7 +937,7 @@ public: rational q; if (!m_bv_util.is_numeral(n, q, bv_sz)) NOT_IMPLEMENTED_YET(); - mpq temp = q.to_mpq(); + const mpq& temp = q.to_mpq(); SASSERT(m_mpz_manager.is_one(temp.denominator())); m_mpz_manager.set(result, temp.numerator()); } @@ -1039,7 +1045,6 @@ public: unsigned pos = -1; if (m_ucb) { - value_score vscore; double max = -1.0; // Andreas: Commented things here might be used for track_unsat data structures as done in SLS for SAT. But seems to have no benefit. /* for (unsigned i = 0; i < m_where_false.size(); i++) { @@ -1048,7 +1053,7 @@ public: expr * e = as[i]; if (m_mpz_manager.neq(get_value(e), m_one)) { - vscore = m_scores.find(e); + value_score & vscore = m_scores.find(e); // Andreas: Select the assertion with the greatest ucb score. Potentially add some noise. // double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched); double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched) + m_ucb_noise * get_random_uint(8); diff --git a/src/test/im_float_config.h b/src/test/im_float_config.h index 436d9ecaf..3905358ea 100644 --- a/src/test/im_float_config.h +++ b/src/test/im_float_config.h @@ -63,10 +63,4 @@ public: numeral_manager & m() const { return const_cast(m_manager); } }; -template -inline void del_f_interval(im_float_config & cfg, typename im_float_config::interval & a) { - cfg.m().del(a.m_lower); - cfg.m().del(a.m_upper); -} - #endif diff --git a/src/test/interval.cpp b/src/test/interval.cpp index ba218c010..21b25a9be 100644 --- a/src/test/interval.cpp +++ b/src/test/interval.cpp @@ -125,7 +125,8 @@ static bool mk_interval(im_default_config & cfg, interval & a, bool l_inf, bool } #endif -static void mk_random_interval(im_default_config & cfg, interval & a, unsigned magnitude) { +template +static void mk_random_interval(T & cfg, interval & a, unsigned magnitude) { switch (rand()%3) { case 0: // Neg, Neg @@ -195,11 +196,6 @@ static void mk_random_interval(im_default_config & cfg, interval & a, unsigned m } } -static void del_interval(im_default_config & cfg, interval & a) { - cfg.m().del(a.m_lower); - cfg.m().del(a.m_upper); -} - #define BUFFER_SZ 256 static int g_problem_id = 0; static char g_buffer[BUFFER_SZ]; @@ -238,19 +234,18 @@ static void display_lemmas(unsynch_mpq_manager & nm, char const * result_term, static void tst_ ## NAME(unsigned N, unsigned magnitude) { \ reslimit rl; \ unsynch_mpq_manager nm; \ - im_default_config imc(nm); \ - interval_manager im(rl, imc); \ + interval_manager im(rl, nm); \ interval a, b, r; \ \ for (unsigned i = 0; i < N; i++) { \ - mk_random_interval(imc, a, magnitude); \ - mk_random_interval(imc, b, magnitude); \ + mk_random_interval(im, a, magnitude); \ + mk_random_interval(im, b, magnitude); \ interval_deps deps; \ im.NAME(a, b, r, deps); \ \ display_lemmas(nm, RES_TERM, a, b, r, deps); \ } \ - del_interval(imc, a); del_interval(imc, b); del_interval(imc, r); \ + im.del(a); im.del(b); im.del(r); \ } MK_BINARY(mul, "(* a b)"); @@ -260,56 +255,52 @@ MK_BINARY(sub, "(- a b)"); static void tst_neg(unsigned N, unsigned magnitude) { reslimit rl; unsynch_mpq_manager nm; - im_default_config imc(nm); - interval_manager im(rl, imc); + interval_manager im(rl, nm); interval a, b, r; for (unsigned i = 0; i < N; i++) { - mk_random_interval(imc, a, magnitude); + mk_random_interval(im, a, magnitude); interval_deps deps; im.neg(a, r, deps); display_lemmas(nm, "(- a)", a, b, r, deps); } - del_interval(imc, a); del_interval(imc, b); del_interval(imc, r); + im.del(a); im.del(b); im.del(r); } static void tst_pw_2(unsigned N, unsigned magnitude) { reslimit rl; unsynch_mpq_manager nm; - im_default_config imc(nm); - interval_manager im(rl, imc); + interval_manager im(rl, nm); interval a, b, r; for (unsigned i = 0; i < N; i++) { - mk_random_interval(imc, a, magnitude); + mk_random_interval(im, a, magnitude); interval_deps deps; im.power(a, 2, r, deps); display_lemmas(nm, "(* a a)", a, b, r, deps); } - del_interval(imc, a); del_interval(imc, b); del_interval(imc, r); + im.del(a); im.del(b); im.del(r); } static void tst_pw_3(unsigned N, unsigned magnitude) { reslimit rl; unsynch_mpq_manager nm; - im_default_config imc(nm); - interval_manager im(rl, imc); + interval_manager im(rl, nm); interval a, b, r; for (unsigned i = 0; i < N; i++) { - mk_random_interval(imc, a, magnitude); + mk_random_interval(im, a, magnitude); interval_deps deps; im.power(a, 3, r, deps); display_lemmas(nm, "(* a a a)", a, b, r, deps); } - del_interval(imc, a); del_interval(imc, b); del_interval(imc, r); + im.del(a); im.del(b); im.del(r); } static void tst_root_2(unsigned N, unsigned magnitude, unsigned precision) { reslimit rl; unsynch_mpq_manager nm; - im_default_config imc(nm); - interval_manager im(rl, imc); + interval_manager im(rl, nm); interval a, b, r; scoped_mpq p(nm); p = precision; @@ -317,7 +308,7 @@ static void tst_root_2(unsigned N, unsigned magnitude, unsigned precision) { unsigned i = 0; while (i < N) { - mk_random_interval(imc, a, magnitude); + mk_random_interval(im, a, magnitude); if (!im.lower_is_neg(a)) { i++; interval_deps deps; @@ -325,14 +316,13 @@ static void tst_root_2(unsigned N, unsigned magnitude, unsigned precision) { display_lemmas(nm, "(^ a (/ 1.0 2.0))", a, b, r, deps); } } - del_interval(imc, a); del_interval(imc, b); del_interval(imc, r); + im.del(a); im.del(b); im.del(r); } static void tst_root_3(unsigned N, unsigned magnitude, unsigned precision) { reslimit rl; unsynch_mpq_manager nm; - im_default_config imc(nm); - interval_manager im(rl, imc); + interval_manager im(rl, nm); interval a, b, r; scoped_mpq p(nm); p = precision; @@ -340,25 +330,24 @@ static void tst_root_3(unsigned N, unsigned magnitude, unsigned precision) { unsigned i = 0; while (i < N) { - mk_random_interval(imc, a, magnitude); + mk_random_interval(im, a, magnitude); i++; interval_deps deps; im.nth_root(a, 3, p, r, deps); display_lemmas(nm, "(^ a (/ 1.0 3.0))", a, b, r, deps); } - del_interval(imc, a); del_interval(imc, b); del_interval(imc, r); + im.del(a); im.del(b); im.del(r); } static void tst_inv(unsigned N, unsigned magnitude) { reslimit rl; unsynch_mpq_manager nm; - im_default_config imc(nm); - interval_manager im(rl, imc); + interval_manager im(rl, nm); interval a, b, r; for (unsigned i = 0; i < N; i++) { while (true) { - mk_random_interval(imc, a, magnitude); + mk_random_interval(im, a, magnitude); if (!im.contains_zero(a)) break; } @@ -366,20 +355,19 @@ static void tst_inv(unsigned N, unsigned magnitude) { im.inv(a, r, deps); display_lemmas(nm, "(/ 1 a)", a, b, r, deps); } - del_interval(imc, a); del_interval(imc, b); del_interval(imc, r); + im.del(a); im.del(b); im.del(r); } static void tst_div(unsigned N, unsigned magnitude) { reslimit rl; unsynch_mpq_manager nm; - im_default_config imc(nm); - interval_manager im(rl, imc); + interval_manager im(rl, nm); interval a, b, r; for (unsigned i = 0; i < N; i++) { - mk_random_interval(imc, a, magnitude); + mk_random_interval(im, a, magnitude); while (true) { - mk_random_interval(imc, b, magnitude); + mk_random_interval(im, b, magnitude); if (!im.contains_zero(b)) break; } @@ -387,7 +375,7 @@ static void tst_div(unsigned N, unsigned magnitude) { im.div(a, b, r, deps); display_lemmas(nm, "(/ a b)", a, b, r, deps); } - del_interval(imc, a); del_interval(imc, b); del_interval(imc, r); + im.del(a); im.del(b); im.del(r); } #include "test/im_float_config.h" @@ -396,8 +384,7 @@ static void tst_div(unsigned N, unsigned magnitude) { static void tst_float() { unsynch_mpq_manager qm; mpf_manager fm; - im_float_config ifc(fm); - interval_manager > im(ifc); + interval_manager > im(fm); im_float_config::interval a, b, c; scoped_mpq minus_one_third(qm), one_third(qm), two_third(qm), minus_two_third(qm); qm.set(minus_one_third, -1, 3); @@ -424,15 +411,14 @@ static void tst_float() { im.display(std::cout, c); std::cout << "\n"; - del_f_interval(ifc, a); del_f_interval(ifc, b); del_f_interval(ifc, c); + im.del(a); im.del(b); im.del(r); } #endif void tst_pi() { reslimit rl; unsynch_mpq_manager nm; - im_default_config imc(nm); - interval_manager im(rl, imc); + interval_manager im(rl, nm); interval r; for (unsigned i = 0; i < 8; i++) { im.pi(i, r); @@ -440,7 +426,7 @@ void tst_pi() { nm.display_decimal(std::cout, im.upper(r), 32); std::cout << "\n"; ENSURE(nm.lt(im.lower(r), im.upper(r))); } - del_interval(imc, r); + im.del(r); } #if 0 diff --git a/src/test/main.cpp b/src/test/main.cpp index cdc06404c..98be722e3 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -10,9 +10,7 @@ #include "util/memory_manager.h" #include "util/gparams.h" -static void tst_exit_all_tests() { - exit(0); -} + // // Unit tests fail by asserting. // If they return, we assume the unit test succeeds @@ -210,7 +208,7 @@ int main(int argc, char ** argv) { TST(prime_generator); TST(permutation); TST(nlsat); - TST(exit_all_tests); + if (test_all) return 0; TST(ext_numeral); TST(interval); TST(f2n); diff --git a/src/test/trigo.cpp b/src/test/trigo.cpp index c1b73c423..d1b75c7fb 100644 --- a/src/test/trigo.cpp +++ b/src/test/trigo.cpp @@ -39,9 +39,8 @@ static void tst_sine_core(std::ostream & out, unsynch_mpq_manager & nm, interval static void tst_sine(std::ostream & out, unsigned N, unsigned k) { unsynch_mpq_manager nm; - im_default_config imc(nm); reslimit rl; - interval_manager im(rl, imc); + interval_manager im(rl, nm); scoped_mpq a(nm); nm.set(a, 0); tst_sine_core(out, nm, im, a, 1); @@ -67,8 +66,7 @@ static void tst_cosine_core(std::ostream & out, unsynch_mpq_manager & nm, interv static void tst_cosine(std::ostream & out, unsigned N, unsigned k) { reslimit rl; unsynch_mpq_manager nm; - im_default_config imc(nm); - interval_manager im(rl, imc); + interval_manager im(rl, nm); scoped_mpq a(nm); nm.set(a, 0); tst_cosine_core(out, nm, im, a, 1); @@ -100,8 +98,7 @@ template static void tst_float_sine(std::ostream & out, unsigned N, unsigned k) { reslimit rl; fmanager fm; - im_float_config ifc(fm, EBITS, SBITS); - interval_manager > im(rl, ifc); + interval_manager > im(rl, { fm, EBITS, SBITS }); _scoped_numeral a(fm); fm.set(a, EBITS, SBITS, static_cast(0)); tst_float_sine_core(out, fm, im, a, 1); @@ -136,8 +133,7 @@ static void tst_mpf_bug() { static void tst_e(std::ostream & out) { reslimit rl; unsynch_mpq_manager nm; - im_default_config imc(nm); - interval_manager im(rl, imc); + interval_manager im(rl, nm); im_default_config::interval r; for (unsigned i = 0; i < 64; i++) { im.e(i, r); @@ -152,8 +148,7 @@ static void tst_e_float(std::ostream & out) { reslimit rl; unsynch_mpq_manager qm; mpf_manager fm; - im_float_config ifc(fm); - interval_manager > im(rl, ifc); + interval_manager > im(rl, fm); scoped_mpq q(qm); im_float_config::interval r; for (unsigned i = 0; i < 64; i++) { @@ -161,7 +156,7 @@ static void tst_e_float(std::ostream & out) { out << fm.to_rational_string(im.lower(r)) << " <= E\n"; out << "E <= " << fm.to_rational_string(im.upper(r)) << "\n"; } - del_f_interval(ifc, r); + im.del(r); } void tst_trigo() { diff --git a/src/util/buffer.h b/src/util/buffer.h index 503788fa0..c64e23d8b 100644 --- a/src/util/buffer.h +++ b/src/util/buffer.h @@ -149,6 +149,13 @@ public: new (m_buffer + m_pos) T(elem); m_pos++; } + + void push_back(T && elem) { + if (m_pos >= m_capacity) + expand(); + new (m_buffer + m_pos) T(std::move(elem)); + m_pos++; + } void pop_back() { if (CallDestructors) { diff --git a/src/util/f2n.h b/src/util/f2n.h index e5e84f6f0..d55b21d3d 100644 --- a/src/util/f2n.h +++ b/src/util/f2n.h @@ -46,6 +46,9 @@ public: m_manager.set(m_one, ebits, sbits, 1); } + f2n(f2n && other) : m_manager(other.m_manager), m_mode(other.m_mode), m_ebits(other.m_ebits), m_sbits(other.m_sbits), + m_tmp1(std::move(other.m_tmp1)), m_one(std::move(other.m_one)) {} + ~f2n() { m().del(m_tmp1); m().del(m_one); diff --git a/src/util/hashtable.h b/src/util/hashtable.h index 020c47b2b..fa9fef180 100644 --- a/src/util/hashtable.h +++ b/src/util/hashtable.h @@ -54,7 +54,7 @@ public: bool is_used() const { return m_state == HT_USED; } T & get_data() { return m_data; } const T & get_data() const { return m_data; } - void set_data(const T & d) { m_data = d; m_state = HT_USED; } + void set_data(T && d) { m_data = std::move(d); m_state = HT_USED; } void set_hash(unsigned h) { m_hash = h; } void mark_as_deleted() { m_state = HT_DELETED; } void mark_as_free() { m_state = HT_FREE; } @@ -187,10 +187,42 @@ protected: } } + static void move_table(entry * source, unsigned source_capacity, entry * target, unsigned target_capacity) { + SASSERT(target_capacity >= source_capacity); + unsigned target_mask = target_capacity - 1; + entry * source_end = source + source_capacity; + entry * target_end = target + target_capacity; + for (entry * source_curr = source; source_curr != source_end; ++source_curr) { + if (source_curr->is_used()) { + unsigned hash = source_curr->get_hash(); + unsigned idx = hash & target_mask; + entry * target_begin = target + idx; + entry * target_curr = target_begin; + for (; target_curr != target_end; ++target_curr) { + SASSERT(!target_curr->is_deleted()); + if (target_curr->is_free()) { + *target_curr = std::move(*source_curr); + goto end; + } + } + for (target_curr = target; target_curr != target_begin; ++target_curr) { + SASSERT(!target_curr->is_deleted()); + if (target_curr->is_free()) { + *target_curr = std::move(*source_curr); + goto end; + } + } + UNREACHABLE(); + end: + ; + } + } + } + void expand_table() { unsigned new_capacity = m_capacity << 1; entry * new_table = alloc_table(new_capacity); - copy_table(m_table, m_capacity, new_table, new_capacity); + move_table(m_table, m_capacity, new_table, new_capacity); delete_table(); m_table = new_table; m_capacity = new_capacity; @@ -202,7 +234,7 @@ protected: if (memory::is_out_of_memory()) return; entry * new_table = alloc_table(m_capacity); - copy_table(m_table, m_capacity, new_table, m_capacity); + move_table(m_table, m_capacity, new_table, m_capacity); delete_table(); m_table = new_table; m_num_deleted = 0; @@ -321,7 +353,7 @@ public: #define INSERT_LOOP_BODY() { \ if (curr->is_used()) { \ if (curr->get_hash() == hash && equals(curr->get_data(), e)) { \ - curr->set_data(e); \ + curr->set_data(std::move(e)); \ return; \ } \ HS_CODE(m_st_collision++;); \ @@ -330,7 +362,7 @@ public: entry * new_entry; \ if (del_entry) { new_entry = del_entry; m_num_deleted--; } \ else { new_entry = curr; } \ - new_entry->set_data(e); \ + new_entry->set_data(std::move(e)); \ new_entry->set_hash(hash); \ m_size++; \ return; \ @@ -342,7 +374,7 @@ public: } \ } ((void) 0) - void insert(data const & e) { + void insert(data && e) { if ((m_size + m_num_deleted) << 2 > (m_capacity * 3)) { // if ((m_size + m_num_deleted) * 2 > (m_capacity)) { expand_table(); @@ -363,6 +395,11 @@ public: UNREACHABLE(); } + void insert(const data & e) { + data tmp(e); + insert(std::move(tmp)); + } + #define INSERT_LOOP_CORE_BODY() { \ if (curr->is_used()) { \ if (curr->get_hash() == hash && equals(curr->get_data(), e)) { \ @@ -375,7 +412,7 @@ public: entry * new_entry; \ if (del_entry) { new_entry = del_entry; m_num_deleted--; } \ else { new_entry = curr; } \ - new_entry->set_data(e); \ + new_entry->set_data(std::move(e)); \ new_entry->set_hash(hash); \ m_size++; \ et = new_entry; \ @@ -393,7 +430,7 @@ public: Return true if it is a new element, and false otherwise. Store the entry/slot of the table in et. */ - bool insert_if_not_there_core(data const & e, entry * & et) { + bool insert_if_not_there_core(data && e, entry * & et) { if ((m_size + m_num_deleted) << 2 > (m_capacity * 3)) { // if ((m_size + m_num_deleted) * 2 > (m_capacity)) { expand_table(); @@ -415,6 +452,11 @@ public: return 0; } + bool insert_if_not_there_core(const data & e, entry * & et) { + data temp(e); + return insert_if_not_there_core(std::move(temp), et); + } + /** \brief Insert the element e if it is not in the table. Return a reference to e or to an object identical to e diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 3218419a9..9e309a726 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -40,12 +40,6 @@ mpf::mpf(unsigned _ebits, unsigned _sbits): set(ebits, sbits); } -mpf::mpf(mpf const & other) { - // It is safe if the mpz numbers are small. - // I need it for resize method in vector. - // UNREACHABLE(); -} - mpf::~mpf() { } diff --git a/src/util/mpf.h b/src/util/mpf.h index 8070768b2..e679be558 100644 --- a/src/util/mpf.h +++ b/src/util/mpf.h @@ -50,7 +50,12 @@ class mpf { public: mpf(); mpf(unsigned ebits, unsigned sbits); - mpf(mpf const & other); + mpf(mpf && other) : + ebits(other.ebits), + sbits(other.sbits), + sign(other.sign), + significand(std::move(other.significand)), + exponent(other.exponent) {} ~mpf(); unsigned get_ebits() const { return ebits; } unsigned get_sbits() const { return sbits; } diff --git a/src/util/mpq.h b/src/util/mpq.h index 5aa3ca083..fd0ae13d4 100644 --- a/src/util/mpq.h +++ b/src/util/mpq.h @@ -31,11 +31,10 @@ class mpq { public: mpq(int v):m_num(v), m_den(1) {} mpq():m_den(1) {} + mpq(mpq && other) : m_num(std::move(other.m_num)), m_den(std::move(other.m_den)) {} void swap(mpq & other) { m_num.swap(other.m_num); m_den.swap(other.m_den); } mpz const & numerator() const { return m_num; } mpz const & denominator() const { return m_den; } - - double get_double() const; }; inline void swap(mpq & m1, mpq & m2) { m1.swap(m2); } @@ -745,6 +744,12 @@ public: reset_denominator(a); } + mpq dup(const mpq & source) { + mpq temp; + set(temp, source); + return temp; + } + void swap(mpz & a, mpz & b) { mpz_manager::swap(a, b); } void swap(mpq & a, mpq & b) { diff --git a/src/util/mpz.h b/src/util/mpz.h index 7001b9a42..f04430e17 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -94,6 +94,9 @@ class mpz { public: mpz(int v):m_val(v), m_ptr(0) {} mpz():m_val(0), m_ptr(0) {} + mpz(mpz && other) : m_val(other.m_val), m_ptr(0) { + std::swap(m_ptr, other.m_ptr); + } void swap(mpz & other) { std::swap(m_val, other.m_val); std::swap(m_ptr, other.m_ptr); @@ -668,6 +671,12 @@ public: } } + void set(mpz & target, mpz && source) { + del(target); + target.m_val = source.m_val; + std::swap(target.m_ptr, source.m_ptr); + } + void set(mpz & a, int val) { del(a); a.m_val = val; @@ -700,6 +709,12 @@ public: void set(mpz & target, unsigned sz, digit_t const * digits); + mpz dup(const mpz & source) { + mpz temp; + set(temp, source); + return temp; + } + void reset(mpz & a) { del(a); a.m_val = 0; diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index 189d1e1a0..df279383b 100644 --- a/src/util/obj_hashtable.h +++ b/src/util/obj_hashtable.h @@ -69,6 +69,10 @@ public: m_key(k), m_value(v) { } + key_data(Key * k, Value && v) : + m_key(k), + m_value(std::move(v)) { + } Value const & get_value() const { return m_value; } Key & get_key () const { return *m_key; } unsigned hash() const { return m_key->hash(); } @@ -86,7 +90,7 @@ public: bool is_used() const { return m_data.m_key != reinterpret_cast(0) && m_data.m_key != reinterpret_cast(1); } key_data const & get_data() const { return m_data; } key_data & get_data() { return m_data; } - void set_data(key_data const & d) { m_data = d; } + void set_data(key_data && d) { m_data = std::move(d); } void set_hash(unsigned h) { SASSERT(h == m_data.hash()); } void mark_as_deleted() { m_data.m_key = reinterpret_cast(1); } void mark_as_free() { m_data.m_key = 0; } @@ -137,6 +141,10 @@ public: void insert(Key * const k, Value const & v) { m_table.insert(key_data(k, v)); } + + void insert(Key * const k, Value && v) { + m_table.insert(key_data(k, std::move(v))); + } key_data const & insert_if_not_there(Key * k, Value const & v) { return m_table.insert_if_not_there(key_data(k, v)); diff --git a/src/util/obj_ref.h b/src/util/obj_ref.h index 1aa562a8f..72762ea5b 100644 --- a/src/util/obj_ref.h +++ b/src/util/obj_ref.h @@ -53,6 +53,10 @@ public: inc_ref(); } + obj_ref(obj_ref && other) : m_obj(0), m_manager(other.m_manager) { + std::swap(m_obj, other.m_obj); + } + ~obj_ref() { dec_ref(); } TManager & get_manager() const { return m_manager; } diff --git a/src/util/rational.h b/src/util/rational.h index 803c562ad..392a1982b 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -41,6 +41,7 @@ public: rational() {} rational(rational const & r) { m().set(m_val, r.m_val); } + rational(rational && r) : m_val(std::move(r.m_val)) {} explicit rational(int n) { m().set(m_val, n); } diff --git a/src/util/ref_vector.h b/src/util/ref_vector.h index 469183b76..f340d8886 100644 --- a/src/util/ref_vector.h +++ b/src/util/ref_vector.h @@ -45,6 +45,10 @@ public: typedef T * data; ref_vector_core(Ref const & r = Ref()):Ref(r) {} + + ref_vector_core(ref_vector_core && other) : + Ref(std::move(other)), + m_nodes(std::move(other.m_nodes)) {} ~ref_vector_core() { dec_range_ref(m_nodes.begin(), m_nodes.end()); @@ -63,7 +67,7 @@ public: void resize(unsigned sz) { if (sz < m_nodes.size()) dec_range_ref(m_nodes.begin() + sz, m_nodes.end()); - m_nodes.resize(sz, 0); + m_nodes.resize(sz); } void resize(unsigned sz, T * d) { @@ -80,7 +84,7 @@ public: void reserve(unsigned sz) { if (sz <= m_nodes.size()) return; - m_nodes.resize(sz, 0); + m_nodes.resize(sz); } void shrink(unsigned sz) { @@ -207,6 +211,8 @@ public: this->append(other); } + ref_vector(ref_vector && other) : super(std::move(other)) {} + ref_vector(TManager & m, unsigned sz, T * const * data): super(ref_manager_wrapper(m)) { this->append(sz, data); diff --git a/src/util/scoped_numeral_vector.h b/src/util/scoped_numeral_vector.h index fdf63bf35..cb9a6b4fd 100644 --- a/src/util/scoped_numeral_vector.h +++ b/src/util/scoped_numeral_vector.h @@ -63,8 +63,7 @@ public: unsigned old_sz = this->size(); if (sz <= old_sz) shrink(sz); - typename Manager::numeral zero(0); - svector::resize(sz, zero); + svector::resize(sz, 0); } }; diff --git a/src/util/util.h b/src/util/util.h index 1f753099c..f8c464197 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -322,7 +322,7 @@ bool compare_arrays(const T * array1, const T * array2, unsigned size) { template void force_ptr_array_size(T & v, unsigned sz) { if (sz > v.size()) { - v.resize(sz, 0); + v.resize(sz); } } diff --git a/src/util/vector.h b/src/util/vector.h index 2d499a900..f5792a5d3 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -26,6 +26,7 @@ Revision History: #include "util/debug.h" #include +#include #include #include "util/memory_manager.h" #include "util/hash.h" @@ -74,9 +75,27 @@ class vector { if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) { throw default_exception("Overflow encountered when expanding vector"); } - SZ *mem = (SZ*)memory::reallocate(reinterpret_cast(m_data)-2, new_capacity_T); - *mem = new_capacity; - m_data = reinterpret_cast(mem + 2); + SZ *mem, *old_mem = reinterpret_cast(m_data) - 2; +#if defined(__GNUC__) && !defined(__clang__) && __GNUC__ < 5 + if (__has_trivial_copy(T)) { +#else + if (std::is_trivially_copyable::value) { +#endif + mem = (SZ*)memory::reallocate(old_mem, new_capacity_T); + m_data = reinterpret_cast(mem + 2); + } else { + mem = (SZ*)memory::allocate(new_capacity_T); + auto old_data = m_data; + auto old_size = size(); + mem[1] = old_size; + m_data = reinterpret_cast(mem + 2); + for (unsigned i = 0; i < old_size; ++i) { + new (&m_data[i]) T(std::move(old_data[i])); + old_data[i].~T(); + } + memory::deallocate(old_mem); + } + *mem = new_capacity; } } @@ -148,6 +167,10 @@ public: SASSERT(size() == source.size()); } + vector(vector&& other) : m_data(0) { + std::swap(m_data, other.m_data); + } + vector(SZ s, T const * data): m_data(0) { for (SZ i = 0; i < s; i++) { @@ -179,6 +202,16 @@ public: return *this; } + vector & operator=(vector && source) { + if (this == &source) { + return *this; + } + destroy(); + m_data = 0; + std::swap(m_data, source.m_data); + return *this; + } + void reset() { if (m_data) { if (CallDestructors) { @@ -292,6 +325,11 @@ public: m_data[idx] = val; } + void set(SZ idx, T && val) { + SASSERT(idx < size()); + m_data[idx] = std::move(val); + } + T & back() { SASSERT(!empty()); return operator[](size() - 1); @@ -318,6 +356,14 @@ public: reinterpret_cast(m_data)[SIZE_IDX]++; } + void push_back(T && elem) { + if (m_data == 0 || reinterpret_cast(m_data)[SIZE_IDX] == reinterpret_cast(m_data)[CAPACITY_IDX]) { + expand_vector(); + } + new (m_data + reinterpret_cast(m_data)[SIZE_IDX]) T(std::move(elem)); + reinterpret_cast(m_data)[SIZE_IDX]++; + } + void insert(T const & elem) { push_back(elem); } @@ -357,7 +403,8 @@ public: } } - void resize(SZ s, T const & elem=T()) { + template + void resize(SZ s, Args args...) { SZ sz = size(); if (s <= sz) { shrink(s); return; } while (s > capacity()) { @@ -367,8 +414,23 @@ public: reinterpret_cast(m_data)[SIZE_IDX] = s; iterator it = m_data + sz; iterator end = m_data + s; - for(; it != end; ++it) { - new (it) T(elem); + for (; it != end; ++it) { + new (it) T(std::forward(args)); + } + } + + void resize(SZ s) { + SZ sz = size(); + if (s <= sz) { shrink(s); return; } + while (s > capacity()) { + expand_vector(); + } + SASSERT(m_data != 0); + reinterpret_cast(m_data)[SIZE_IDX] = s; + iterator it = m_data + sz; + iterator end = m_data + s; + for (; it != end; ++it) { + new (it) T(); } } @@ -439,10 +501,15 @@ public: return m_data[idx]; } - void reserve(SZ s, T const & d = T()) { + void reserve(SZ s, T const & d) { if (s > size()) resize(s, d); } + + void reserve(SZ s) { + if (s > size()) + resize(s); + } }; template @@ -452,7 +519,12 @@ public: ptr_vector(unsigned s):vector(s) {} ptr_vector(unsigned s, T * elem):vector(s, elem) {} ptr_vector(ptr_vector const & source):vector(source) {} + ptr_vector(ptr_vector && other) : vector(std::move(other)) {} ptr_vector(unsigned s, T * const * data):vector(s, const_cast(data)) {} + ptr_vector & operator=(ptr_vector const & source) { + vector::operator=(source); + return *this; + } }; template @@ -462,7 +534,12 @@ public: svector(SZ s):vector(s) {} svector(SZ s, T const & elem):vector(s, elem) {} svector(svector const & source):vector(source) {} + svector(svector && other) : vector(std::move(other)) {} svector(SZ s, T const * data):vector(s, data) {} + svector & operator=(svector const & source) { + vector::operator=(source); + return *this; + } }; typedef svector int_vector; @@ -494,23 +571,4 @@ struct vector_hash : public vector_hash_tpl > template struct svector_hash : public vector_hash_tpl > {}; -#include -// Specialize vector to be an instance of std::vector instead. -// This will catch any regression of issue #564 and #420. - -template <> -class vector : public std::vector { -public: - vector(vector const& other): std::vector(other) {} - vector(size_t sz, char const* s): std::vector(sz, s) {} - vector() {} - - void reset() { clear(); } - - -}; - - - #endif /* VECTOR_H_ */ -