mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-10-16 09:07:44 -07:00
commit b36f512879
80 changed files with 751 additions and 310 deletions
Download patch file Download diff file Expand all files Collapse all files

9
.travis.yml
View file

@ -17,6 +17,15 @@ env:
############################################################################### ###############################################################################
# Ubuntu 16.04 LTS # 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 # 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 - 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 # 64-bit Clang 3.9 RelWithDebInfo

1
README-CMake.md
View file

@ -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. * ``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. * ``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. 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. 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.

3
contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile
View file

@ -30,6 +30,7 @@ RUN apt-get update && \
libgomp1 \ libgomp1 \
libomp5 \ libomp5 \
libomp-dev \ libomp-dev \
llvm-3.9 \
make \ make \
mono-devel \ mono-devel \
ninja-build \ ninja-build \
@ -47,4 +48,4 @@ RUN useradd -m user && \
echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
USER user USER user
WORKDIR /home/user WORKDIR /home/user
ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-3.9/bin/llvm-symbolizer

3
contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile
View file

@ -16,6 +16,7 @@ RUN apt-get update && \
libgmp-dev \ libgmp-dev \
libgomp1 \ libgomp1 \
lib32gomp1 \ lib32gomp1 \
llvm-3.9 \
make \ make \
mono-devel \ mono-devel \
ninja-build \ ninja-build \
@ -32,4 +33,4 @@ RUN useradd -m user && \
echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
USER user USER user
WORKDIR /home/user WORKDIR /home/user
ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-3.9/bin/llvm-symbolizer

3
contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile
View file

@ -18,6 +18,7 @@ RUN apt-get update && \
libgomp1 \ libgomp1 \
libomp5 \ libomp5 \
libomp-dev \ libomp-dev \
llvm-3.9 \
make \ make \
mono-devel \ mono-devel \
ninja-build \ ninja-build \
@ -35,4 +36,4 @@ RUN useradd -m user && \
echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
USER user USER user
WORKDIR /home/user WORKDIR /home/user
ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-3.9/bin/llvm-symbolizer

16
contrib/ci/Dockerfiles/z3_build.Dockerfile
View file

@ -5,6 +5,7 @@ FROM ${DOCKER_IMAGE_BASE}
# Build arguments. This can be changed when invoking # Build arguments. This can be changed when invoking
# `docker build`. # `docker build`.
ARG ASAN_BUILD ARG ASAN_BUILD
ARG ASAN_DSO
ARG BUILD_DOCS ARG BUILD_DOCS
ARG CC ARG CC
ARG CXX ARG CXX
@ -13,8 +14,10 @@ ARG JAVA_BINDINGS
ARG NO_SUPPRESS_OUTPUT ARG NO_SUPPRESS_OUTPUT
ARG PYTHON_BINDINGS ARG PYTHON_BINDINGS
ARG PYTHON_EXECUTABLE=/usr/bin/python2.7 ARG PYTHON_EXECUTABLE=/usr/bin/python2.7
ARG RUN_API_EXAMPLES
ARG RUN_SYSTEM_TESTS ARG RUN_SYSTEM_TESTS
ARG RUN_UNIT_TESTS ARG RUN_UNIT_TESTS
ARG SANITIZER_PRINT_SUPPRESSIONS
ARG TARGET_ARCH ARG TARGET_ARCH
ARG TEST_INSTALL ARG TEST_INSTALL
ARG UBSAN_BUILD ARG UBSAN_BUILD
@ -32,6 +35,7 @@ ARG Z3_VERBOSE_BUILD_OUTPUT
ENV \ ENV \
ASAN_BUILD=${ASAN_BUILD} \ ASAN_BUILD=${ASAN_BUILD} \
ASAN_DSO=${ASAN_DSO} \
BUILD_DOCS=${BUILD_DOCS} \ BUILD_DOCS=${BUILD_DOCS} \
CC=${CC} \ CC=${CC} \
CXX=${CXX} \ CXX=${CXX} \
@ -40,6 +44,8 @@ ENV \
NO_SUPPRESS_OUTPUT=${NO_SUPPRESS_OUTPUT} \ NO_SUPPRESS_OUTPUT=${NO_SUPPRESS_OUTPUT} \
PYTHON_BINDINGS=${PYTHON_BINDINGS} \ PYTHON_BINDINGS=${PYTHON_BINDINGS} \
PYTHON_EXECUTABLE=${PYTHON_EXECUTABLE} \ PYTHON_EXECUTABLE=${PYTHON_EXECUTABLE} \
SANITIZER_PRINT_SUPPRESSIONS=${SANITIZER_PRINT_SUPPRESSIONS} \
RUN_API_EXAMPLES=${RUN_API_EXAMPLES} \
RUN_SYSTEM_TESTS=${RUN_SYSTEM_TESTS} \ RUN_SYSTEM_TESTS=${RUN_SYSTEM_TESTS} \
RUN_UNIT_TESTS=${RUN_UNIT_TESTS} \ RUN_UNIT_TESTS=${RUN_UNIT_TESTS} \
TARGET_ARCH=${TARGET_ARCH} \ TARGET_ARCH=${TARGET_ARCH} \
@ -50,6 +56,7 @@ ENV \
USE_OPENMP=${USE_OPENMP} \ USE_OPENMP=${USE_OPENMP} \
Z3_SRC_DIR=${Z3_SRC_DIR} \ Z3_SRC_DIR=${Z3_SRC_DIR} \
Z3_BUILD_DIR=/home/user/z3_build \ Z3_BUILD_DIR=/home/user/z3_build \
Z3_BUILD_TYPE=${Z3_BUILD_TYPE} \
Z3_CMAKE_GENERATOR=${Z3_CMAKE_GENERATOR} \ Z3_CMAKE_GENERATOR=${Z3_CMAKE_GENERATOR} \
Z3_VERBOSE_BUILD_OUTPUT=${Z3_VERBOSE_BUILD_OUTPUT} \ Z3_VERBOSE_BUILD_OUTPUT=${Z3_VERBOSE_BUILD_OUTPUT} \
Z3_STATIC_BUILD=${Z3_STATIC_BUILD} \ Z3_STATIC_BUILD=${Z3_STATIC_BUILD} \
@ -62,7 +69,8 @@ ENV \
# Build Z3 # Build Z3
RUN mkdir -p "${Z3_SRC_DIR}" && \ 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` # Deliberately leave out `contrib`
ADD /cmake ${Z3_SRC_DIR}/cmake/ ADD /cmake ${Z3_SRC_DIR}/cmake/
ADD /doc ${Z3_SRC_DIR}/doc/ ADD /doc ${Z3_SRC_DIR}/doc/
@ -89,7 +97,13 @@ RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_docs.sh
# Test examples # Test examples
ADD \ ADD \
/contrib/ci/scripts/test_z3_examples_cmake.sh \ /contrib/ci/scripts/test_z3_examples_cmake.sh \
/contrib/ci/scripts/sanitizer_env.sh \
${Z3_SRC_DIR}/contrib/ci/scripts/ ${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 ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_examples_cmake.sh
# Run unit tests # Run unit tests

2
contrib/ci/README.md
View file

@ -30,8 +30,10 @@ the future.
* `JAVA_BINDINGS` - Build and test Java API bindings (`0` or `1`) * `JAVA_BINDINGS` - Build and test Java API bindings (`0` or `1`)
* `NO_SUPPRESS_OUTPUT` - Don't suppress output of some commands (`0` or `1`) * `NO_SUPPRESS_OUTPUT` - Don't suppress output of some commands (`0` or `1`)
* `PYTHON_BINDINGS` - Build and test Python API bindings (`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_SYSTEM_TESTS` - Run system tests (`0` or `1`)
* `RUN_UNIT_TESTS` - Run unit tests (`BUILD_ONLY` or `BUILD_AND_RUN` or `SKIP`) * `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`) * `TARGET_ARCH` - Target architecture (`x86_64` or `i686`)
* `TEST_INSTALL` - Test running `install` target (`0` or `1`) * `TEST_INSTALL` - Test running `install` target (`0` or `1`)
* `UBSAN_BUILD` - Do [UndefinedBehaviourSanitizer](https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html) build (`0` or `1`) * `UBSAN_BUILD` - Do [UndefinedBehaviourSanitizer](https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html) build (`0` or `1`)

11
contrib/ci/scripts/build_z3_cmake.sh
View file

@ -22,6 +22,7 @@ set -o pipefail
: ${USE_LTO?"USE_LTO must be specified"} : ${USE_LTO?"USE_LTO must be specified"}
: ${Z3_INSTALL_PREFIX?"Z3_INSTALL_PREFIX must be specified"} : ${Z3_INSTALL_PREFIX?"Z3_INSTALL_PREFIX must be specified"}
: ${Z3_WARNINGS_AS_ERRORS?"Z3_WARNINGS_AS_ERRORS must be specified"} : ${Z3_WARNINGS_AS_ERRORS?"Z3_WARNINGS_AS_ERRORS must be specified"}
: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"}
ADDITIONAL_Z3_OPTS=() ADDITIONAL_Z3_OPTS=()
@ -105,6 +106,16 @@ fi
# Set compiler flags # Set compiler flags
source ${SCRIPT_DIR}/set_compiler_flags.sh 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 # Sanity check
if [ ! -e "${Z3_SRC_DIR}/CMakeLists.txt" ]; then if [ ! -e "${Z3_SRC_DIR}/CMakeLists.txt" ]; then
echo "Z3_SRC_DIR is invalid" echo "Z3_SRC_DIR is invalid"

6
contrib/ci/scripts/ci_defaults.sh
View file

@ -9,8 +9,13 @@ export DOTNET_BINDINGS="${DOTNET_BINDINGS:-1}"
export JAVA_BINDINGS="${JAVA_BINDINGS:-1}" export JAVA_BINDINGS="${JAVA_BINDINGS:-1}"
export NO_SUPPRESS_OUTPUT="${NO_SUPPRESS_OUTPUT:-0}" export NO_SUPPRESS_OUTPUT="${NO_SUPPRESS_OUTPUT:-0}"
export PYTHON_BINDINGS="${PYTHON_BINDINGS:-1}" export PYTHON_BINDINGS="${PYTHON_BINDINGS:-1}"
export RUN_API_EXAMPLES="${RUN_API_EXAMPLES:-1}"
export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}" export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}"
export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-BUILD_AND_RUN}" 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 TARGET_ARCH="${TARGET_ARCH:-x86_64}"
export TEST_INSTALL="${TEST_INSTALL:-1}" export TEST_INSTALL="${TEST_INSTALL:-1}"
export UBSAN_BUILD="${UBSAN_BUILD:-0}" export UBSAN_BUILD="${UBSAN_BUILD:-0}"
@ -49,6 +54,7 @@ unset PLATFORM
# NOTE: The following variables are not set here because # NOTE: The following variables are not set here because
# they are specific to the CI implementation # they are specific to the CI implementation
# PYTHON_EXECUTABLE # PYTHON_EXECUTABLE
# ASAN_DSO
# Z3_SRC_DIR # Z3_SRC_DIR
# Z3_BUILD_DIR # Z3_BUILD_DIR
# Z3_SYSTEM_TEST_DIR # Z3_SYSTEM_TEST_DIR

4
contrib/ci/scripts/run_quiet.sh
View file

@ -34,8 +34,8 @@ function run_quiet() {
fi fi
# Clean up # Clean up
rm "${STDOUT}" "${STDERR}" rm "${STDOUT}" "${STDERR}"
[ $( echo "${OLD_SETTINGS}" | grep -c 'e') -ne 0 ] && set -e [ "$( echo "${OLD_SETTINGS}" | grep -c 'e')" != "0" ] && set -e
[ $( echo "${OLD_SETTINGS}" | grep -c 'x') -ne 0 ] && set -x [ "$( echo "${OLD_SETTINGS}" | grep -c 'x')" != "0" ] && set -x
return ${EXIT_STATUS} return ${EXIT_STATUS}
fi fi
} }

82
contrib/ci/scripts/sanitizer_env.sh Normal file
View file

@ -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

61
contrib/ci/scripts/test_z3_examples_cmake.sh
View file

@ -14,6 +14,13 @@ set -o pipefail
: ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"} : ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"}
: ${DOTNET_BINDINGS?"DOTNET_BINDINGS must be specified"} : ${DOTNET_BINDINGS?"DOTNET_BINDINGS must be specified"}
: ${JAVA_BINDINGS?"JAVA_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 # Set compiler flags
source ${SCRIPT_DIR}/set_compiler_flags.sh source ${SCRIPT_DIR}/set_compiler_flags.sh
@ -21,6 +28,9 @@ source ${SCRIPT_DIR}/set_compiler_flags.sh
# Set CMake generator args # Set CMake generator args
source ${SCRIPT_DIR}/set_generator_args.sh source ${SCRIPT_DIR}/set_generator_args.sh
# Sanitizer environment variables
source ${SCRIPT_DIR}/sanitizer_env.sh
cd "${Z3_BUILD_DIR}" cd "${Z3_BUILD_DIR}"
# Build and run C example # Build and run C example
@ -38,9 +48,21 @@ run_quiet examples/tptp_build_dir/z3_tptp5 -help
# Build an run c_maxsat_example # Build an run c_maxsat_example
cmake --build $(pwd) --target c_maxsat_example "${GENERATOR_ARGS[@]}" cmake --build $(pwd) --target c_maxsat_example "${GENERATOR_ARGS[@]}"
run_quiet \ # FIXME: It is known that the maxsat example leaks memory and the
examples/c_maxsat_example_build_dir/c_maxsat_example \ # the Z3 developers have stated this is "wontfix".
${Z3_SRC_DIR}/examples/maxsat/ex.smt # 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 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 # `all_interval_series.py` produces a lot of output so just throw
# away output. # away output.
# TODO: This example is slow should we remove it from testing? # TODO: This example is slow should we remove it from testing?
run_quiet ${PYTHON_EXECUTABLE} python/all_interval_series.py if [ "X${ASAN_BUILD}" = "X1" -a "X${Z3_BUILD_TYPE}" = "XDebug" ]; then
run_quiet ${PYTHON_EXECUTABLE} python/complex.py # Too slow when doing ASan Debug build
run_quiet ${PYTHON_EXECUTABLE} python/example.py 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. # FIXME: `hamiltonian.py` example is disabled because its too slow.
#${PYTHON_EXECUTABLE} python/hamiltonian.py #${PYTHON_EXECUTABLE} python/hamiltonian.py
run_quiet ${PYTHON_EXECUTABLE} python/marco.py run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/marco.py
run_quiet ${PYTHON_EXECUTABLE} python/mss.py run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/mss.py
run_quiet ${PYTHON_EXECUTABLE} python/socrates.py run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/socrates.py
run_quiet ${PYTHON_EXECUTABLE} python/visitor.py run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/visitor.py
run_quiet ${PYTHON_EXECUTABLE} python/z3test.py run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/z3test.py
fi fi
if [ "X${DOTNET_BINDINGS}" = "X1" ]; then if [ "X${DOTNET_BINDINGS}" = "X1" ]; then
@ -65,7 +92,7 @@ if [ "X${DOTNET_BINDINGS}" = "X1" ]; then
# FIXME: Move compliation step into CMake target # 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 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 .NET example
run_quiet mono ./dotnet_test.exe run_quiet run_non_native_binding mono ./dotnet_test.exe
fi fi
if [ "X${JAVA_BINDINGS}" = "X1" ]; then if [ "X${JAVA_BINDINGS}" = "X1" ]; then
@ -82,6 +109,14 @@ if [ "X${JAVA_BINDINGS}" = "X1" ]; then
# Assume Linux for now # Assume Linux for now
export LD_LIBRARY_PATH=$(pwd):${LD_LIBRARY_PATH} export LD_LIBRARY_PATH=$(pwd):${LD_LIBRARY_PATH}
fi 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 fi

20
contrib/ci/scripts/test_z3_system_tests.sh
View file

@ -10,12 +10,17 @@ set -o pipefail
: ${PYTHON_BINDINGS?"PYTHON_BINDINGS must be specified"} : ${PYTHON_BINDINGS?"PYTHON_BINDINGS must be specified"}
: ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"} : ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"}
: ${Z3_SYSTEM_TEST_DIR?"Z3_SYSTEM_TEST_DIR 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 if [ "X${RUN_SYSTEM_TESTS}" != "X1" ]; then
echo "Skipping system tests" echo "Skipping system tests"
exit 0 exit 0
fi 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_EXE="${Z3_BUILD_DIR}/z3"
Z3_LIB_DIR="${Z3_BUILD_DIR}" 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}" Z3_SYSTEM_TEST_GIT_URL="${Z3_GIT_URL:-https://github.com/Z3Prover/z3test.git}"
# Clone repo to destination # 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}" git clone "${Z3_SYSTEM_TEST_GIT_URL}" "${Z3_SYSTEM_TEST_DIR}"
cd "${Z3_SYSTEM_TEST_DIR}" cd "${Z3_SYSTEM_TEST_DIR}"
@ -48,7 +53,18 @@ fi
if [ "X${PYTHON_BINDINGS}" = "X1" ]; then if [ "X${PYTHON_BINDINGS}" = "X1" ]; then
# Run python binding tests # 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 fi
# FIXME: Run `scripts/test_cs.py` once it has been modified to support mono # FIXME: Run `scripts/test_cs.py` once it has been modified to support mono

3
contrib/ci/scripts/test_z3_unit_tests_cmake.sh
View file

@ -13,6 +13,9 @@ set -o pipefail
# Set CMake generator args # Set CMake generator args
source ${SCRIPT_DIR}/set_generator_args.sh source ${SCRIPT_DIR}/set_generator_args.sh
# Sanitizer environment variables
source ${SCRIPT_DIR}/sanitizer_env.sh
cd "${Z3_BUILD_DIR}" cd "${Z3_BUILD_DIR}"
function build_unit_tests() { function build_unit_tests() {

12
contrib/ci/scripts/travis_ci_linux_entry_point.sh
View file

@ -84,6 +84,14 @@ if [ -n "${ASAN_BUILD}" ]; then
BUILD_OPTS+=("--build-arg" "ASAN_BUILD=${ASAN_BUILD}") BUILD_OPTS+=("--build-arg" "ASAN_BUILD=${ASAN_BUILD}")
fi 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 if [ -n "${UBSAN_BUILD}" ]; then
BUILD_OPTS+=("--build-arg" "UBSAN_BUILD=${UBSAN_BUILD}") BUILD_OPTS+=("--build-arg" "UBSAN_BUILD=${UBSAN_BUILD}")
fi fi
@ -92,6 +100,10 @@ if [ -n "${TEST_INSTALL}" ]; then
BUILD_OPTS+=("--build-arg" "TEST_INSTALL=${TEST_INSTALL}") BUILD_OPTS+=("--build-arg" "TEST_INSTALL=${TEST_INSTALL}")
fi fi
if [ -n "${RUN_API_EXAMPLES}" ]; then
BUILD_OPTS+=("--build-arg" "RUN_API_EXAMPLES=${RUN_API_EXAMPLES}")
fi
if [ -n "${RUN_SYSTEM_TESTS}" ]; then if [ -n "${RUN_SYSTEM_TESTS}" ]; then
BUILD_OPTS+=("--build-arg" "RUN_SYSTEM_TESTS=${RUN_SYSTEM_TESTS}") BUILD_OPTS+=("--build-arg" "RUN_SYSTEM_TESTS=${RUN_SYSTEM_TESTS}")
fi fi

7
contrib/suppressions/README.md Normal file
View file

@ -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.

3
contrib/suppressions/maintainers.txt Normal file
View file

@ -0,0 +1,3 @@
# Maintainers
- Dan Liew (@delcypher)

4
contrib/suppressions/sanitizers/README.md Normal file
View file

@ -0,0 +1,4 @@
# Sanitizer supression files
This directory contains files used to suppress
ASan/LSan/UBSan warnings/errors.

1
contrib/suppressions/sanitizers/asan.txt Normal file
View file

@ -0,0 +1 @@
# AddressSanitizer suppression file

5
contrib/suppressions/sanitizers/lsan.txt Normal file
View file

@ -0,0 +1,5 @@
# LeakSanitizer suppression file
# Ignore Clang OpenMP leaks.
# See https://github.com/Z3Prover/z3/issues/1308
leak:___kmp_allocate

7
contrib/suppressions/sanitizers/ubsan.txt Normal file
View file

@ -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

42
examples/CMakeLists.txt
View file

@ -7,6 +7,30 @@ else()
set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG "") set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG "")
endif() 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 # Build example project using libz3's C API as an external project
################################################################################ ################################################################################
@ -14,7 +38,10 @@ ExternalProject_Add(c_example
DEPENDS libz3 DEPENDS libz3
# Configure step # Configure step
SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/c" 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 # Build step
${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_example_build_dir" BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_example_build_dir"
@ -30,7 +57,10 @@ ExternalProject_Add(c_maxsat_example
DEPENDS libz3 DEPENDS libz3
# Configure step # Configure step
SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/maxsat" 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 # Build step
${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_maxsat_example_build_dir" BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_maxsat_example_build_dir"
@ -47,7 +77,9 @@ ExternalProject_Add(cpp_example
DEPENDS libz3 DEPENDS libz3
# Configure step # Configure step
SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/c++" 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 # Build step
${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/cpp_example_build_dir" BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/cpp_example_build_dir"
@ -63,7 +95,9 @@ ExternalProject_Add(z3_tptp5
DEPENDS libz3 DEPENDS libz3
# Configure step # Configure step
SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/tptp" 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 # Build step
${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/tptp_build_dir" BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/tptp_build_dir"

11
examples/c/CMakeLists.txt
View file

@ -22,6 +22,17 @@ message(STATUS "Found Z3 ${Z3_VERSION_STRING}")
message(STATUS "Z3_DIR: ${Z3_DIR}") message(STATUS "Z3_DIR: ${Z3_DIR}")
add_executable(c_example test_capi.c) 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_include_directories(c_example PRIVATE ${Z3_C_INCLUDE_DIRS})
target_link_libraries(c_example PRIVATE ${Z3_LIBRARIES}) target_link_libraries(c_example PRIVATE ${Z3_LIBRARIES})

10
examples/maxsat/CMakeLists.txt
View file

@ -25,6 +25,16 @@ add_executable(c_maxsat_example maxsat.c)
target_include_directories(c_maxsat_example PRIVATE ${Z3_C_INCLUDE_DIRS}) target_include_directories(c_maxsat_example PRIVATE ${Z3_C_INCLUDE_DIRS})
target_link_libraries(c_maxsat_example PRIVATE ${Z3_LIBRARIES}) 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") if ("${CMAKE_SYSTEM_NAME}" MATCHES "[Ww]indows")
# On Windows we need to copy the Z3 libraries # On Windows we need to copy the Z3 libraries
# into the same directory as the executable # into the same directory as the executable

2
src/ast/ast.cpp
View file

@ -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<func_decl> & cache) { func_decl * basic_decl_plugin::mk_proof_decl(char const * name, basic_op_kind k, unsigned num_parents, ptr_vector<func_decl> & cache) {
if (num_parents >= cache.size()) { if (num_parents >= cache.size()) {
cache.resize(num_parents+1, 0); cache.resize(num_parents+1);
} }
if (cache[num_parents] == 0) { if (cache[num_parents] == 0) {
cache[num_parents] = mk_proof_decl(name, k, num_parents); cache[num_parents] = mk_proof_decl(name, k, num_parents);

14
src/ast/ast.h
View file

@ -121,6 +121,20 @@ public:
explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {} explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {}
parameter(parameter const&); 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();
parameter& operator=(parameter const& other); parameter& operator=(parameter const& other);

3
src/ast/bv_decl_plugin.cpp
View file

@ -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 { app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const {
parameter p1(val); parameter p[2] = { parameter(val), parameter(static_cast<int>(bv_size)) };
parameter p[2] = { p1, parameter(static_cast<int>(bv_size)) };
return m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, 0); return m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, 0);
} }

99
src/ast/normal_forms/nnf.cpp
View file

@ -40,7 +40,7 @@ enum nnf_mode {
transformation will be in skolem normal form. transformation will be in skolem normal form.
If a formula is too expensive to be put into NNF, If a formula is too expensive to be put into NNF,
then nested quantifiers and labels are renamed. then nested quantifiers and labels are renamed.
This mode is sufficient when using E-matching. This mode is sufficient when using E-matching.
*/ */
NNF_QUANT, /* A subformula is put into NNF if it contains 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 quantifier. The result of the transformation will be
in skolem normal form, and the body of quantifiers in skolem normal form, and the body of quantifiers
will be in NNF. If a ground formula is too expensive to 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. are renamed.
This mode is sufficient when using Superposition This mode is sufficient when using Superposition
@ -89,7 +89,7 @@ class skolemizer {
} }
TRACE("skolemizer", tout << "skid: " << q->get_skid() << "\n";); TRACE("skolemizer", tout << "skid: " << q->get_skid() << "\n";);
expr_ref_vector substitution(m()); expr_ref_vector substitution(m());
unsigned num_decls = q->get_num_decls(); unsigned num_decls = q->get_num_decls();
for (unsigned i = num_decls; i > 0; ) { for (unsigned i = num_decls; i > 0; ) {
@ -111,7 +111,7 @@ class skolemizer {
substitution.push_back(0); 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 // are in positions num_decls .. num_decls+sz-1
// //
std::reverse(substitution.c_ptr(), substitution.c_ptr() + substitution.size()); std::reverse(substitution.c_ptr(), substitution.c_ptr() + substitution.size());
@ -139,7 +139,7 @@ class skolemizer {
s(body, substitution.size(), substitution.c_ptr(), r); s(body, substitution.size(), substitution.c_ptr(), r);
p = 0; p = 0;
if (m().proofs_enabled()) { if (m().proofs_enabled()) {
if (q->is_forall()) if (q->is_forall())
p = m().mk_skolemization(m().mk_not(q), m().mk_not(r)); p = m().mk_skolemization(m().mk_not(q), m().mk_not(r));
else else
p = m().mk_skolemization(q, r); p = m().mk_skolemization(q, r);
@ -175,7 +175,7 @@ public:
m_cache_pr.insert(q, p); m_cache_pr.insert(q, p);
} }
} }
bool is_sk_hack(expr * p) const { bool is_sk_hack(expr * p) const {
SASSERT(m().is_pattern(p)); SASSERT(m().is_pattern(p));
if (to_app(p)->get_num_args() != 1) if (to_app(p)->get_num_args() != 1)
@ -204,10 +204,10 @@ struct nnf::imp {
unsigned m_i:28; unsigned m_i:28;
unsigned m_pol:1; // pos/neg polarity unsigned m_pol:1; // pos/neg polarity
unsigned m_in_q:1; // true if m_curr is nested in a quantifier 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_cache_result:1;
unsigned m_spos; // top of the result stack, when the frame was created. 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_curr(n),
m_i(0), m_i(0),
m_pol(pol), m_pol(pol),
@ -223,22 +223,22 @@ struct nnf::imp {
#define POS_NQ_CIDX 1 // positive polarity and not nested in a quantifier #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 NEG_Q_CIDX 2 // negative polarity and nested in a quantifier
#define POS_Q_CIDX 3 // positive polarity and nested in a quantifier #define POS_Q_CIDX 3 // positive polarity and nested in a quantifier
ast_manager & m_manager; ast_manager & m_manager;
vector<frame> m_frame_stack; vector<frame> m_frame_stack;
expr_ref_vector m_result_stack; expr_ref_vector m_result_stack;
typedef act_cache cache; typedef act_cache cache;
cache * m_cache[4]; cache * m_cache[4];
expr_ref_vector m_todo_defs; expr_ref_vector m_todo_defs;
proof_ref_vector m_todo_proofs; proof_ref_vector m_todo_proofs;
// proof generation goodness ---- // proof generation goodness ----
proof_ref_vector m_result_pr_stack; proof_ref_vector m_result_pr_stack;
cache * m_cache_pr[4]; cache * m_cache_pr[4];
// ------------------------------ // ------------------------------
skolemizer m_skolemizer; skolemizer m_skolemizer;
// configuration ---------------- // configuration ----------------
@ -249,7 +249,7 @@ struct nnf::imp {
name_exprs * m_name_nested_formulas; name_exprs * m_name_nested_formulas;
name_exprs * m_name_quant; name_exprs * m_name_quant;
unsigned long long m_max_memory; // in bytes unsigned long long m_max_memory; // in bytes
imp(ast_manager & m, defined_names & n, params_ref const & p): imp(ast_manager & m, defined_names & n, params_ref const & p):
@ -292,9 +292,9 @@ struct nnf::imp {
m_mode = NNF_FULL; m_mode = NNF_FULL;
else if (mode_sym == "quantifiers") else if (mode_sym == "quantifiers")
m_mode = NNF_QUANT; m_mode = NNF_QUANT;
else else
throw nnf_params_exception("invalid NNF mode"); throw nnf_params_exception("invalid NNF mode");
TRACE("nnf", tout << "nnf-mode: " << m_mode << " " << mode_sym << "\n" << _p << "\n";); TRACE("nnf", tout << "nnf-mode: " << m_mode << " " << mode_sym << "\n" << _p << "\n";);
m_ignore_labels = p.ignore_labels(); 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) { void push_frame(expr * t, bool pol, bool in_q, bool cache_res) {
expr_ref tr(t, m()); m_frame_stack.push_back(frame(expr_ref(t, m()), pol, in_q, cache_res, m_result_stack.size()));
m_frame_stack.push_back(frame(tr, pol, in_q, cache_res, m_result_stack.size()));
} }
static unsigned get_cache_idx(bool pol, bool in_q) { static unsigned get_cache_idx(bool pol, bool in_q) {
return static_cast<unsigned>(in_q) * 2 + static_cast<unsigned>(pol); return static_cast<unsigned>(in_q) * 2 + static_cast<unsigned>(pol);
} }
void cache_result(expr * t, bool pol, bool in_q, expr * v, proof * pr) { 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); m_cache_pr[idx]->insert(t, pr);
} }
expr * get_cached(expr * t, bool pol, bool in_q) const { expr * get_cached(expr * t, bool pol, bool in_q) const {
return m_cache[get_cache_idx(pol, in_q)]->find(t); return m_cache[get_cache_idx(pol, in_q)]->find(t);
} }
proof * get_cached_pr(expr * t, bool pol, bool in_q) const { proof * get_cached_pr(expr * t, bool pol, bool in_q) const {
@ -368,12 +367,12 @@ struct nnf::imp {
return false; return false;
} }
void checkpoint() { void checkpoint() {
cooperate("nnf"); cooperate("nnf");
if (memory::get_allocation_size() > m_max_memory) if (memory::get_allocation_size() > m_max_memory)
throw nnf_exception(Z3_MAX_MEMORY_MSG); throw nnf_exception(Z3_MAX_MEMORY_MSG);
if (m().canceled()) if (m().canceled())
throw nnf_exception(m().limit().get_cancel_msg()); throw nnf_exception(m().limit().get_cancel_msg());
} }
@ -382,11 +381,11 @@ struct nnf::imp {
m_frame_stack.back().m_new_child = true; m_frame_stack.back().m_new_child = true;
} }
void set_new_child_flag(expr * old_t, expr * new_t) { void set_new_child_flag(expr * old_t, expr * new_t) {
if (old_t != new_t) if (old_t != new_t)
set_new_child_flag(); set_new_child_flag();
} }
void skip(expr * t, bool pol) { void skip(expr * t, bool pol) {
expr * r = pol ? t : m().mk_not(t); expr * r = pol ? t : m().mk_not(t);
m_result_stack.push_back(r); m_result_stack.push_back(r);
@ -448,10 +447,10 @@ struct nnf::imp {
if (pol) { if (pol) {
if (old_e->get_decl() == new_e->get_decl()) if (old_e->get_decl() == new_e->get_decl())
return m().mk_oeq_congruence(old_e, new_e, num_parents, parents); 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); 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); 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); r = m().mk_and(t->get_num_args(), m_result_stack.c_ptr() + fr.m_spos);
else else
r = m().mk_or(t->get_num_args(), m_result_stack.c_ptr() + fr.m_spos); 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.shrink(fr.m_spos);
m_result_stack.push_back(r); m_result_stack.push_back(r);
if (proofs_enabled()) { if (proofs_enabled()) {
@ -520,7 +519,7 @@ struct nnf::imp {
r = m().mk_or(2, m_result_stack.c_ptr() + fr.m_spos); r = m().mk_or(2, m_result_stack.c_ptr() + fr.m_spos);
else else
r = m().mk_and(2, m_result_stack.c_ptr() + fr.m_spos); r = m().mk_and(2, m_result_stack.c_ptr() + fr.m_spos);
m_result_stack.shrink(fr.m_spos); m_result_stack.shrink(fr.m_spos);
m_result_stack.push_back(r); m_result_stack.push_back(r);
if (proofs_enabled()) { if (proofs_enabled()) {
@ -554,7 +553,7 @@ struct nnf::imp {
default: default:
break; break;
} }
expr * const * rs = m_result_stack.c_ptr() + fr.m_spos; expr * const * rs = m_result_stack.c_ptr() + fr.m_spos;
expr * _cond = rs[0]; expr * _cond = rs[0];
expr * _not_cond = rs[1]; 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 is_eq(app * t) const { return m().is_eq(t) || m().is_iff(t); }
bool process_iff_xor(app * t, frame & fr) { bool process_iff_xor(app * t, frame & fr) {
SASSERT(t->get_num_args() == 2); SASSERT(t->get_num_args() == 2);
switch (fr.m_i) { switch (fr.m_i) {
@ -605,7 +604,7 @@ struct nnf::imp {
expr * not_rhs = rs[3]; expr * not_rhs = rs[3];
app * r; 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)); r = m().mk_and(m().mk_or(not_lhs, rhs), m().mk_or(lhs, not_rhs));
else else
r = m().mk_and(m().mk_or(lhs, rhs), m().mk_or(not_lhs, not_rhs)); r = m().mk_and(m().mk_or(lhs, rhs), m().mk_or(not_lhs, not_rhs));
@ -626,7 +625,7 @@ struct nnf::imp {
else else
return process_default(t, fr); return process_default(t, fr);
} }
bool process_default(app * t, frame & fr) { bool process_default(app * t, frame & fr) {
SASSERT(fr.m_i == 0); SASSERT(fr.m_i == 0);
if (m_mode == NNF_FULL || t->has_quantifiers() || t->has_labels()) { 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); m_name_nested_formulas->operator()(t, m_todo_defs, m_todo_proofs, n2, pr2);
else else
m_name_quant->operator()(t, m_todo_defs, m_todo_proofs, n2, pr2); m_name_quant->operator()(t, m_todo_defs, m_todo_proofs, n2, pr2);
if (!fr.m_pol) if (!fr.m_pol)
n2 = m().mk_not(n2); n2 = m().mk_not(n2);
m_result_stack.push_back(n2); m_result_stack.push_back(n2);
if (proofs_enabled()) { if (proofs_enabled()) {
if (!fr.m_pol) { if (!fr.m_pol) {
@ -666,10 +665,10 @@ struct nnf::imp {
expr * arg = m_result_stack.back(); expr * arg = m_result_stack.back();
proof * arg_pr = proofs_enabled() ? m_result_pr_stack.back() : 0; 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 return true; // the result is already on the stack
buffer<symbol> names; buffer<symbol> names;
bool pos; bool pos;
m().is_label(t, pos, names); 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)), 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))); m().mk_iff_oeq(m().mk_rewrite(aux, r)));
} }
} }
else { else {
r = arg; r = arg;
if (proofs_enabled()) { if (proofs_enabled()) {
@ -692,7 +691,7 @@ struct nnf::imp {
pr = m().mk_transitivity(p1, arg_pr); pr = m().mk_transitivity(p1, arg_pr);
} }
} }
m_result_stack.pop_back(); m_result_stack.pop_back();
m_result_stack.push_back(r); m_result_stack.push_back(r);
if (proofs_enabled()) { if (proofs_enabled()) {
@ -729,7 +728,7 @@ struct nnf::imp {
if (m().is_label(t)) { if (m().is_label(t)) {
return process_label(t, fr); return process_label(t, fr);
} }
return process_default(t, fr); return process_default(t, fr);
} }
@ -737,7 +736,7 @@ struct nnf::imp {
skip(v, fr.m_pol); skip(v, fr.m_pol);
return true; return true;
} }
bool process_quantifier(quantifier * q, frame & fr) { bool process_quantifier(quantifier * q, frame & fr) {
expr_ref r(m()); expr_ref r(m());
proof_ref pr(m()); proof_ref pr(m());
@ -757,7 +756,7 @@ struct nnf::imp {
if (q->is_forall() == fr.m_pol || !m_skolemize) { if (q->is_forall() == fr.m_pol || !m_skolemize) {
expr * new_expr = m_result_stack.back(); expr * new_expr = m_result_stack.back();
proof * new_expr_pr = proofs_enabled() ? m_result_pr_stack.back() : 0; proof * new_expr_pr = proofs_enabled() ? m_result_pr_stack.back() : 0;
ptr_buffer<expr> new_patterns; ptr_buffer<expr> new_patterns;
if (q->is_forall() == fr.m_pol) { if (q->is_forall() == fr.m_pol) {
@ -773,7 +772,7 @@ struct nnf::imp {
// New quantifier has existential force. // New quantifier has existential force.
// So, ignore patterns // So, ignore patterns
} }
quantifier * new_q = 0; quantifier * new_q = 0;
proof * new_q_pr = 0; proof * new_q_pr = 0;
if (fr.m_pol) { if (fr.m_pol) {
@ -786,7 +785,7 @@ struct nnf::imp {
if (proofs_enabled()) if (proofs_enabled())
new_q_pr = m().mk_nnf_neg(q, new_q, 1, &new_expr_pr); new_q_pr = m().mk_nnf_neg(q, new_q, 1, &new_expr_pr);
} }
m_result_stack.pop_back(); m_result_stack.pop_back();
m_result_stack.push_back(new_q); m_result_stack.push_back(new_q);
if (proofs_enabled()) { if (proofs_enabled()) {
@ -809,7 +808,7 @@ struct nnf::imp {
} }
return true; return true;
} }
void recover_result(expr * t, expr_ref & result, proof_ref & result_pr) { void recover_result(expr * t, expr_ref & result, proof_ref & result_pr) {
// recover result from the top of the stack. // recover result from the top of the stack.
result = m_result_stack.back(); result = m_result_stack.back();
@ -873,7 +872,7 @@ struct nnf::imp {
process(n, r, pr); process(n, r, pr);
unsigned old_sz1 = new_defs.size(); unsigned old_sz1 = new_defs.size();
unsigned old_sz2 = new_def_proofs.size(); unsigned old_sz2 = new_def_proofs.size();
for (unsigned i = 0; i < m_todo_defs.size(); i++) { for (unsigned i = 0; i < m_todo_defs.size(); i++) {
expr_ref dr(m()); expr_ref dr(m());
proof_ref dpr(m()); proof_ref dpr(m());
@ -881,7 +880,7 @@ struct nnf::imp {
new_defs.push_back(dr); new_defs.push_back(dr);
if (proofs_enabled()) { if (proofs_enabled()) {
proof * new_pr = m().mk_modus_ponens(m_todo_proofs.get(i), dpr); 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()); 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() { nnf::~nnf() {
dealloc(m_imp); 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) { 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); 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";); TRACE("nnf_result", tout << mk_ismt2_pp(n, m_imp->m()) << "\nNNF result:\n" << mk_ismt2_pp(r, m_imp->m()) << "\n";);

6
src/ast/pattern/expr_pattern_match.cpp
View file

@ -179,11 +179,11 @@ expr_pattern_match::compile(expr* q)
} }
if (m_regs.size() <= max_reg) { 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) { if (m_bound_dom.size() <= num_bound) {
m_bound_dom.resize(num_bound+1, 0); m_bound_dom.resize(num_bound+1);
m_bound_rng.resize(num_bound+1, 0); m_bound_rng.resize(num_bound+1);
} }
instr.m_kind = YIELD; instr.m_kind = YIELD;

2
src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
View file

@ -272,7 +272,7 @@ void bit_blaster_tpl<Cfg>::mk_multiplier(unsigned sz, expr * const * a_bits, exp
zero = m().mk_false(); zero = m().mk_false();
vector< expr_ref_vector > pps; vector< expr_ref_vector > pps;
pps.resize(sz, m()); pps.resize(sz, expr_ref_vector(m()));
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
checkpoint(); checkpoint();

7
src/ast/rewriter/fpa_rewriter.cpp
View file

@ -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 & sm1 = m_fm.m_powers2(sbits - 1);
const mpz & em1 = m_fm.m_powers2(ebits); const mpz & em1 = m_fm.m_powers2(ebits);
scoped_mpq q(mpqm); const mpq & q = r1.to_mpq();
mpqm.set(q, r1.to_mpq()); SASSERT(mpzm.is_one(q.denominator()));
SASSERT(mpzm.is_one(q.get().denominator()));
scoped_mpz z(mpzm); scoped_mpz z(mpzm);
z = q.get().numerator(); z = q.numerator();
mpzm.rem(z, sm1, sig); mpzm.rem(z, sm1, sig);
mpzm.div(z, sm1, z); mpzm.div(z, sm1, z);

4
src/ast/substitution/substitution_tree.cpp
View file

@ -256,7 +256,7 @@ void substitution_tree::insert(expr * new_expr) {
sort * s = to_var(new_expr)->get_sort(); sort * s = to_var(new_expr)->get_sort();
unsigned id = s->get_decl_id(); unsigned id = s->get_decl_id();
if (id >= m_vars.size()) if (id >= m_vars.size())
m_vars.resize(id+1, 0); m_vars.resize(id+1);
if (m_vars[id] == 0) if (m_vars[id] == 0)
m_vars[id] = alloc(var_ref_vector, m_manager); m_vars[id] = alloc(var_ref_vector, m_manager);
var_ref_vector * v = m_vars[id]; var_ref_vector * v = m_vars[id];
@ -277,7 +277,7 @@ void substitution_tree::insert(app * new_expr) {
unsigned id = d->get_decl_id(); unsigned id = d->get_decl_id();
if (id >= m_roots.size()) if (id >= m_roots.size())
m_roots.resize(id+1, 0); m_roots.resize(id+1);
if (!m_roots[id]) { if (!m_roots[id]) {
// there is no tree for the function symbol heading new_expr // there is no tree for the function symbol heading new_expr

2
src/ast/used_vars.cpp
View file

@ -58,7 +58,7 @@ void used_vars::process(expr * n, unsigned delta) {
if (idx >= delta) { if (idx >= delta) {
idx = idx - delta; idx = idx - delta;
if (idx >= m_found_vars.size()) 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(); m_found_vars[idx] = to_var(n)->get_sort();
} }
break; break;

8
src/cmd_context/cmd_context.cpp
View file

@ -1608,7 +1608,9 @@ void cmd_context::validate_check_sat_result(lbool r) {
throw cmd_exception("check annotation that says unsat"); throw cmd_exception("check annotation that says unsat");
#else #else
diagnostic_stream() << "BUG: incompleteness" << std::endl; 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 #endif
} }
break; break;
@ -1618,7 +1620,9 @@ void cmd_context::validate_check_sat_result(lbool r) {
throw cmd_exception("check annotation that says sat"); throw cmd_exception("check annotation that says sat");
#else #else
diagnostic_stream() << "BUG: unsoundness" << std::endl; 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 #endif
} }
break; break;

2
src/math/interval/interval.h
View file

@ -162,7 +162,7 @@ private:
void checkpoint(); void checkpoint();
public: public:
interval_manager(reslimit& lim, C const & c); interval_manager(reslimit& lim, C && c);
~interval_manager(); ~interval_manager();
numeral_manager & m() const { return m_c.m(); } numeral_manager & m() const { return m_c.m(); }

2
src/math/interval/interval_def.h
View file

@ -31,7 +31,7 @@ Revision History:
// #define TRACE_NTH_ROOT // #define TRACE_NTH_ROOT
template<typename C> template<typename C>
interval_manager<C>::interval_manager(reslimit& lim, C const & c): m_limit(lim), m_c(c) { interval_manager<C>::interval_manager(reslimit& lim, C && c): m_limit(lim), m_c(std::move(c)) {
m().set(m_minus_one, -1); m().set(m_minus_one, -1);
m().set(m_one, 1); m().set(m_one, 1);
m_pi_n = 0; m_pi_n = 0;

12
src/math/polynomial/algebraic_numbers.cpp
View file

@ -2632,10 +2632,14 @@ namespace algebraic_numbers {
scoped_mpz neg_n(qm()); scoped_mpz neg_n(qm());
qm().set(neg_n, v.numerator()); qm().set(neg_n, v.numerator());
qm().neg(neg_n); 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 << "("; out << "(";
upm().display(out, 2, coeffs, "#"); upm().display(out, 2, coeffs, "#");
out << ", 1)"; // first root of the polynomial d*# - n out << ", 1)"; // first root of the polynomial d*# - n
zmgr.del(coeffs[0]);
zmgr.del(coeffs[1]);
} }
else { else {
algebraic_cell * c = a.to_algebraic(); algebraic_cell * c = a.to_algebraic();
@ -2678,10 +2682,14 @@ namespace algebraic_numbers {
scoped_mpz neg_n(qm()); scoped_mpz neg_n(qm());
qm().set(neg_n, v.numerator()); qm().set(neg_n, v.numerator());
qm().neg(neg_n); 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 "; out << "(root-obj ";
upm().display_smt2(out, 2, coeffs, "x"); upm().display_smt2(out, 2, coeffs, "x");
out << " 1)"; // first root of the polynomial d*# - n out << " 1)"; // first root of the polynomial d*# - n
zmgr.del(coeffs[0]);
zmgr.del(coeffs[1]);
} }
else { else {
algebraic_cell * c = a.to_algebraic(); algebraic_cell * c = a.to_algebraic();

6
src/math/polynomial/polynomial.cpp
View file

@ -4822,10 +4822,9 @@ namespace polynomial {
polynomial * mk_x_minus_y(var x, var y) { polynomial * mk_x_minus_y(var x, var y) {
numeral zero(0); numeral zero(0);
numeral one(1);
numeral minus_one; // It is not safe to initialize with -1 when numeral_manager is GF_2 numeral minus_one; // It is not safe to initialize with -1 when numeral_manager is GF_2
m_manager.set(minus_one, -1); 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 }; var xs[2] = { x, y };
return mk_linear(2, as, xs, zero); return mk_linear(2, as, xs, zero);
} }
@ -4845,8 +4844,7 @@ namespace polynomial {
polynomial * mk_x_plus_y(var x, var y) { polynomial * mk_x_plus_y(var x, var y) {
numeral zero(0); numeral zero(0);
numeral one(1); numeral as[2] = { numeral(1), numeral(1) };
numeral as[2] = { one, one };
var xs[2] = { x, y }; var xs[2] = { x, y };
return mk_linear(2, as, xs, zero); return mk_linear(2, as, xs, zero);
} }

2
src/math/polynomial/upolynomial_factorization_int.h
View file

@ -45,7 +45,7 @@ namespace upolynomial {
for (unsigned i = 0; i < p.size(); ++ i) { for (unsigned i = 0; i < p.size(); ++ i) {
numeral p_i; // no need to delete, we keep it pushed in zp_p numeral p_i; // no need to delete, we keep it pushed in zp_p
zp_nm.set(p_i, p[i]); 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); zp_upm.trim(zp_p);
} }

4
src/math/simplex/sparse_matrix.h
View file

@ -35,7 +35,7 @@ namespace simplex {
struct row_entry { struct row_entry {
numeral m_coeff; numeral m_coeff;
var_t m_var; 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: private:
@ -61,7 +61,7 @@ namespace simplex {
int m_col_idx; int m_col_idx;
int m_next_free_row_entry_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) {} _row_entry() : row_entry(numeral(), dead_id), m_col_idx(0) {}
bool is_dead() const { return row_entry::m_var == dead_id; } bool is_dead() const { return row_entry::m_var == dead_id; }
}; };

2
src/math/subpaving/subpaving_t_def.h
View file

@ -739,7 +739,7 @@ void context_t<C>::del_sum(polynomial * p) {
template<typename C> template<typename C>
var context_t<C>::mk_sum(numeral const & c, unsigned sz, numeral const * as, var const * xs) { var context_t<C>::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++) { for (unsigned i = 0; i < sz; i++) {
SASSERT(xs[i] < num_vars()); SASSERT(xs[i] < num_vars());
nm().set(m_num_buffer[xs[i]], as[i]); nm().set(m_num_buffer[xs[i]], as[i]);

2
src/model/func_interp.cpp
View file

@ -117,7 +117,7 @@ bool func_interp::is_fi_entry_expr(expr * e, ptr_vector<expr> & args) {
(m_arity > 1 && (!m().is_and(c) || to_app(c)->get_num_args() != m_arity))) (m_arity > 1 && (!m().is_and(c) || to_app(c)->get_num_args() != m_arity)))
return false; return false;
args.resize(m_arity, 0); args.resize(m_arity);
for (unsigned i = 0; i < m_arity; i++) { for (unsigned i = 0; i < m_arity; i++) {
expr * ci = (m_arity == 1 && i == 0) ? c : to_app(c)->get_arg(i); expr * ci = (m_arity == 1 && i == 0) ? c : to_app(c)->get_arg(i);

2
src/muz/rel/dl_instruction.h
View file

@ -128,7 +128,7 @@ namespace datalog {
void set_reg(reg_idx i, reg_type val) { void set_reg(reg_idx i, reg_type val) {
if (i >= m_registers.size()) { if (i >= m_registers.size()) {
check_overflow(i); check_overflow(i);
m_registers.resize(i+1,0); m_registers.resize(i+1);
} }
if (m_registers[i]) { if (m_registers[i]) {
m_registers[i]->deallocate(); m_registers[i]->deallocate();

2
src/muz/rel/dl_mk_explanations.cpp
View file

@ -465,7 +465,7 @@ namespace datalog {
unsigned sz = r.get_signature().size(); unsigned sz = r.get_signature().size();
ptr_vector<expr> subst_arg; ptr_vector<expr> subst_arg;
subst_arg.resize(sz, 0); subst_arg.resize(sz);
unsigned ofs = sz-1; unsigned ofs = sz-1;
for (unsigned i=0; i<sz; i++) { for (unsigned i=0; i<sz; i++) {
SASSERT(!r.is_undefined(i) || !contains_var(m_new_rule, i)); SASSERT(!r.is_undefined(i) || !contains_var(m_new_rule, i));

5
src/parsers/smt2/smt2parser.cpp
View file

@ -444,7 +444,10 @@ namespace smt2 {
m_ctx.regular_stream()<< "line " << line << " column " << pos << ": " << escaped(msg, true) << "\")" << std::endl; m_ctx.regular_stream()<< "line " << line << " column " << pos << ": " << escaped(msg, true) << "\")" << std::endl;
} }
if (m_ctx.exit_on_error()) { if (m_ctx.exit_on_error()) {
exit(1); // WORKAROUND: ASan's LeakSanitizer reports many false positives when
// calling `exit()` so call `_Exit()` instead which avoids invoking leak
// checking.
_Exit(1);
} }
} }

2
src/qe/qe.cpp
View file

@ -1272,7 +1272,7 @@ namespace qe {
family_id fid = p->get_family_id(); family_id fid = p->get_family_id();
SASSERT(fid != null_family_id); SASSERT(fid != null_family_id);
if (static_cast<int>(m_plugins.size()) <= fid) { if (static_cast<int>(m_plugins.size()) <= fid) {
m_plugins.resize(fid+1,0); m_plugins.resize(fid+1);
} }
SASSERT(!m_plugins[fid]); SASSERT(!m_plugins[fid]);
m_plugins[fid] = p; m_plugins[fid] = p;

5
src/sat/sat_simplifier.cpp
View file

@ -1311,7 +1311,6 @@ namespace sat {
clause_use_list & neg_occs = m_use_list.get(neg_l); clause_use_list & neg_occs = m_use_list.get(neg_l);
unsigned num_pos = pos_occs.size() + num_bin_pos; unsigned num_pos = pos_occs.size() + num_bin_pos;
unsigned num_neg = neg_occs.size() + num_bin_neg; 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";); 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(pos_l, m_pos_cls);
collect_clauses(neg_l, m_neg_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";); TRACE("resolution_detail", tout << "collecting number of after_clauses\n";);
unsigned before_clauses = num_pos + num_neg; unsigned before_clauses = num_pos + num_neg;
unsigned after_clauses = 0; unsigned after_clauses = 0;
@ -1376,7 +1373,7 @@ namespace sat {
} }
} }
TRACE("resolution", tout << "found var to eliminate, before: " << before_clauses << " after: " << after_clauses << "\n";); 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 // eliminate variable
model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v); model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);

96
src/smt/asserted_formulas.cpp
View file

@ -38,7 +38,7 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
m_qhead(0), m_qhead(0),
m_macro_manager(m), m_macro_manager(m),
m_bv_sharing(m), m_bv_sharing(m),
m_inconsistent(false), m_inconsistent(false),
m_has_quantifiers(false), m_has_quantifiers(false),
m_reduce_asserted_formulas(*this), m_reduce_asserted_formulas(*this),
m_distribute_forall(*this), m_distribute_forall(*this),
@ -54,8 +54,8 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
m_lift_ite(*this), m_lift_ite(*this),
m_ng_lift_ite(*this), m_ng_lift_ite(*this),
m_find_macros(*this), m_find_macros(*this),
m_propagate_values(*this), m_propagate_values(*this),
m_nnf_cnf(*this), m_nnf_cnf(*this),
m_apply_quasi_macros(*this) { m_apply_quasi_macros(*this) {
m_macro_finder = alloc(macro_finder, m, m_macro_manager); 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() { void asserted_formulas::setup() {
switch (m_params.m_lift_ite) { switch (m_params.m_lift_ite) {
case LI_FULL: case LI_FULL:
m_params.m_ng_lift_ite = LI_NONE; m_params.m_ng_lift_ite = LI_NONE;
break; break;
case LI_CONSERVATIVE: case LI_CONSERVATIVE:
if (m_params.m_ng_lift_ite == LI_CONSERVATIVE) if (m_params.m_ng_lift_ite == LI_CONSERVATIVE)
@ -77,7 +77,7 @@ void asserted_formulas::setup() {
default: default:
break; break;
} }
if (m_params.m_relevancy_lvl == 0) if (m_params.m_relevancy_lvl == 0)
m_params.m_relevancy_lemma = false; m_params.m_relevancy_lemma = false;
} }
@ -93,7 +93,7 @@ void asserted_formulas::push_assertion(expr * e, proof * pr, vector<justified_ex
expr* e1 = 0; expr* e1 = 0;
if (m.is_false(e)) { if (m.is_false(e)) {
result.push_back(justified_expr(m, e, pr)); result.push_back(justified_expr(m, e, pr));
m_inconsistent = true; m_inconsistent = true;
} }
else if (m.is_true(e)) { else if (m.is_true(e)) {
// skip // skip
@ -110,8 +110,8 @@ void asserted_formulas::push_assertion(expr * e, proof * pr, vector<justified_ex
expr* arg = to_app(e1)->get_arg(i); expr* arg = to_app(e1)->get_arg(i);
proof_ref _pr(m.mk_not_or_elim(pr, i), m); proof_ref _pr(m.mk_not_or_elim(pr, i), m);
expr_ref narg(mk_not(m, arg), m); expr_ref narg(mk_not(m, arg), m);
push_assertion(narg, _pr, result); push_assertion(narg, _pr, result);
} }
} }
else { else {
result.push_back(justified_expr(m, e, pr)); 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("eq2ineq", m_params.m_arith_eq2ineq);
p.set_bool("gcd_rounding", true); p.set_bool("gcd_rounding", true);
p.set_bool("expand_select_store", true); p.set_bool("expand_select_store", true);
p.set_bool("bv_sort_ac", true);
m_rewriter.updt_params(p); m_rewriter.updt_params(p);
flush_cache(); 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); proof_ref in_pr(_in_pr, m), pr(_in_pr, m);
expr_ref r(e, m); expr_ref r(e, m);
if (inconsistent()) if (inconsistent())
return; return;
m_has_quantifiers |= ::has_quantifiers(e);
if (m_params.m_preprocess) { if (m_params.m_preprocess) {
TRACE("assert_expr_bug", tout << r << "\n";); TRACE("assert_expr_bug", tout << r << "\n";);
set_eliminate_and(false); // do not eliminate and before nnf. 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";); TRACE("assert_expr_bug", tout << "after...\n" << r << "\n";);
} }
m_has_quantifiers |= ::has_quantifiers(e);
push_assertion(r, pr, m_formulas); push_assertion(r, pr, m_formulas);
TRACE("asserted_formulas_bug", tout << "after assert_expr\n"; display(tout);); TRACE("asserted_formulas_bug", tout << "after assert_expr\n"; display(tout););
} }
@ -183,7 +185,7 @@ void asserted_formulas::push_scope() {
commit(); commit();
TRACE("asserted_formulas_scopes", tout << "after push: " << m_scopes.size() << "\n";); TRACE("asserted_formulas_scopes", tout << "after push: " << m_scopes.size() << "\n";);
} }
void asserted_formulas::pop_scope(unsigned num_scopes) { void asserted_formulas::pop_scope(unsigned num_scopes) {
TRACE("asserted_formulas_scopes", tout << "before pop " << num_scopes << " of " << m_scopes.size() << "\n";); TRACE("asserted_formulas_scopes", tout << "before pop " << num_scopes << " of " << m_scopes.size() << "\n";);
m_bv_sharing.pop_scope(num_scopes); m_bv_sharing.pop_scope(num_scopes);
@ -212,7 +214,7 @@ void asserted_formulas::reset() {
bool asserted_formulas::check_well_sorted() const { bool asserted_formulas::check_well_sorted() const {
for (justified_expr const& je : m_formulas) { 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; return true;
} }
@ -224,20 +226,20 @@ void asserted_formulas::reduce() {
return; return;
if (m_qhead == m_formulas.size()) if (m_qhead == m_formulas.size())
return; return;
if (!m_params.m_preprocess) if (!m_params.m_preprocess)
return; return;
if (m_macro_manager.has_macros()) if (m_macro_manager.has_macros())
invoke(m_find_macros); invoke(m_find_macros);
TRACE("before_reduce", display(tout);); TRACE("before_reduce", display(tout););
CASSERT("well_sorted", check_well_sorted()); CASSERT("well_sorted", check_well_sorted());
set_eliminate_and(false); // do not eliminate and before nnf. set_eliminate_and(false); // do not eliminate and before nnf.
if (!invoke(m_propagate_values)) return; if (!invoke(m_propagate_values)) return;
if (!invoke(m_find_macros)) return; if (!invoke(m_find_macros)) return;
if (!invoke(m_nnf_cnf)) return; if (!invoke(m_nnf_cnf)) return;
set_eliminate_and(true); 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_cheap_ite_trees)) return;
if (!invoke(m_pull_nested_quantifiers)) return; if (!invoke(m_pull_nested_quantifiers)) return;
if (!invoke(m_lift_ite)) 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 (!s.should_apply()) return true;
IF_VERBOSE(10, verbose_stream() << "(smt." << s.id() << ")\n";); IF_VERBOSE(10, verbose_stream() << "(smt." << s.id() << ")\n";);
s(); s();
IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";); IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";);
TRACE("reduce_step_ll", ast_mark visited; display_ll(tout, visited);); TRACE("reduce_step_ll", ast_mark visited; display_ll(tout, visited););
CASSERT("well_sorted",check_well_sorted()); CASSERT("well_sorted",check_well_sorted());
if (inconsistent() || canceled()) { if (inconsistent() || canceled()) {
TRACE("after_reduce", display(tout);); TRACE("after_reduce", display(tout););
TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited);); TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited););
return false; return false;
} }
else { else {
return true; 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 { void asserted_formulas::display_ll(std::ostream & out, ast_mark & pp_visited) const {
if (!m_formulas.empty()) { 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); ast_def_ll_pp(out, m, f.get_fml(), pp_visited, true, false);
out << "asserted formulas:\n"; 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 << "#" << f.get_fml()->get_id() << " ";
out << "\n"; out << "\n";
} }
@ -332,9 +334,9 @@ void asserted_formulas::find_macros_core() {
void asserted_formulas::apply_quasi_macros() { void asserted_formulas::apply_quasi_macros() {
TRACE("before_quasi_macros", display(tout);); TRACE("before_quasi_macros", display(tout););
vector<justified_expr> new_fmls; vector<justified_expr> new_fmls;
quasi_macros proc(m, m_macro_manager); quasi_macros proc(m, m_macro_manager);
while (proc(m_formulas.size() - m_qhead, while (proc(m_formulas.size() - m_qhead,
m_formulas.c_ptr() + m_qhead, m_formulas.c_ptr() + m_qhead,
new_fmls)) { new_fmls)) {
swap_asserted_formulas(new_fmls); swap_asserted_formulas(new_fmls);
new_fmls.reset(); new_fmls.reset();
@ -348,7 +350,7 @@ void asserted_formulas::nnf_cnf() {
vector<justified_expr> new_fmls; vector<justified_expr> new_fmls;
expr_ref_vector push_todo(m); expr_ref_vector push_todo(m);
proof_ref_vector push_todo_prs(m); proof_ref_vector push_todo_prs(m);
unsigned i = m_qhead; unsigned i = m_qhead;
unsigned sz = m_formulas.size(); unsigned sz = m_formulas.size();
TRACE("nnf_bug", tout << "i: " << i << " sz: " << sz << "\n";); 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)); CASSERT("well_sorted",is_well_sorted(m, r1));
if (canceled()) { if (canceled()) {
return; return;
} }
if (m.proofs_enabled()) if (m.proofs_enabled())
pr = m.mk_modus_ponens(push_todo_prs.get(k), pr1); pr = m.mk_modus_ponens(push_todo_prs.get(k), pr1);
push_assertion(r1, pr, new_fmls); push_assertion(r1, pr, new_fmls);
@ -389,8 +391,8 @@ void asserted_formulas::nnf_cnf() {
void asserted_formulas::simplify_fmls::operator()() { void asserted_formulas::simplify_fmls::operator()() {
vector<justified_expr> new_fmls; vector<justified_expr> new_fmls;
unsigned sz = af.m_formulas.size(); unsigned sz = af.m_formulas.size();
for (unsigned i = af.m_qhead; i < sz; i++) { for (unsigned i = af.m_qhead; i < sz; i++) {
auto& j = af.m_formulas[i]; auto& j = af.m_formulas[i];
expr_ref result(m); expr_ref result(m);
proof_ref result_pr(m); proof_ref result_pr(m);
@ -406,8 +408,8 @@ void asserted_formulas::simplify_fmls::operator()() {
af.push_assertion(result, result_pr, new_fmls); af.push_assertion(result, result_pr, new_fmls);
} }
if (af.canceled()) return; if (af.canceled()) return;
} }
af.swap_asserted_formulas(new_fmls); af.swap_asserted_formulas(new_fmls);
TRACE("asserted_formulas", af.display(tout);); TRACE("asserted_formulas", af.display(tout););
post_op(); post_op();
} }
@ -473,12 +475,12 @@ void asserted_formulas::propagate_values() {
unsigned asserted_formulas::propagate_values(unsigned i) { unsigned asserted_formulas::propagate_values(unsigned i) {
expr_ref n(m_formulas[i].get_fml(), m); expr_ref n(m_formulas[i].get_fml(), m);
expr_ref new_n(m); expr_ref new_n(m);
proof_ref new_pr(m); proof_ref new_pr(m);
m_rewriter(n, new_n, new_pr); m_rewriter(n, new_n, new_pr);
if (m.proofs_enabled()) { if (m.proofs_enabled()) {
proof * pr = m_formulas[i].get_proof(); 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); justified_expr j(m, new_n, new_pr);
m_formulas[i] = j; 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";); TRACE("propagate_values", tout << "incompatible " << mk_pp(n, m) << "\n";);
} }
if (m.is_not(n, n1)) { 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 { 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(); UNREACHABLE();
} }
return false; return false;
} }
void asserted_formulas::compute_depth(expr* e) { void asserted_formulas::compute_depth(expr* e) {
ptr_vector<expr> todo; ptr_vector<expr> todo;
todo.push_back(e); todo.push_back(e);
while (!todo.empty()) { while (!todo.empty()) {
e = todo.back(); e = todo.back();
unsigned d = 0; unsigned d = 0;
@ -603,7 +605,7 @@ proof * asserted_formulas::get_inconsistency_proof() const {
return 0; 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(); expr* f = j.get_fml();
if (is_quantifier(f) && simplify_inj_axiom(m, to_quantifier(f), n)) { 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";); TRACE("inj_axiom", tout << "simplifying...\n" << mk_pp(f, m) << "\n" << n << "\n";);

2
src/smt/mam.cpp
View file

@ -1999,7 +1999,7 @@ namespace smt {
m_ast_manager(ctx.get_manager()), m_ast_manager(ctx.get_manager()),
m_mam(m), m_mam(m),
m_use_filters(use_filters) { m_use_filters(use_filters) {
m_args.resize(INIT_ARGS_SIZE, 0); m_args.resize(INIT_ARGS_SIZE);
} }
~interpreter() { ~interpreter() {

2
src/smt/smt_context.cpp
View file

@ -1286,7 +1286,7 @@ namespace smt {
else { else {
if (depth >= m_almost_cg_tables.size()) { if (depth >= m_almost_cg_tables.size()) {
unsigned old_sz = 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++) for (unsigned i = old_sz; i < depth + 1; i++)
m_almost_cg_tables[i] = alloc(almost_cg_table); m_almost_cg_tables[i] = alloc(almost_cg_table);
} }

4
src/smt/theory_array_base.cpp
View file

@ -617,8 +617,8 @@ namespace smt {
m_else_values.reset(); m_else_values.reset();
m_parents.reset(); m_parents.reset();
m_parents.resize(num_vars, -1); m_parents.resize(num_vars, -1);
m_defaults.resize(num_vars, 0); m_defaults.resize(num_vars);
m_else_values.resize(num_vars, 0); m_else_values.resize(num_vars);
if (m_use_unspecified_default) if (m_use_unspecified_default)
return; return;

2
src/smt/theory_datatype.cpp
View file

@ -620,7 +620,7 @@ namespace smt {
sort * s = recognizer->get_decl()->get_domain(0); sort * s = recognizer->get_decl()->get_domain(0);
if (d->m_recognizers.empty()) { if (d->m_recognizers.empty()) {
SASSERT(m_util.is_datatype(s)); 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)); SASSERT(d->m_recognizers.size() == m_util.get_datatype_num_constructors(s));
unsigned c_idx = m_util.get_recognizer_constructor_idx(recognizer->get_decl()); unsigned c_idx = m_util.get_recognizer_constructor_idx(recognizer->get_decl());

9
src/smt/theory_dense_diff_logic_def.h
View file

@ -914,6 +914,8 @@ namespace smt {
} }
verbose_stream() << " + " << m_objective_consts[v] << "\n";); 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_nodes = get_num_vars();
unsigned num_edges = m_edges.size(); unsigned num_edges = m_edges.size();
S.ensure_var(num_nodes + num_edges + m_objectives.size()); S.ensure_var(num_nodes + num_edges + m_objectives.size());
@ -921,8 +923,9 @@ namespace smt {
numeral const& a = m_assignment[i]; numeral const& a = m_assignment[i];
rational fin = a.get_rational().to_rational(); rational fin = a.get_rational().to_rational();
rational inf = a.get_infinitesimal().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); S.set_value(i, q);
inf_mgr.del(q);
} }
for (unsigned i = 0; i < num_nodes; ++i) { for (unsigned i = 0; i < num_nodes; ++i) {
enode * n = get_enode(i); enode * n = get_enode(i);
@ -933,7 +936,6 @@ namespace smt {
} }
} }
svector<unsigned> vars; svector<unsigned> vars;
unsynch_mpq_manager mgr;
scoped_mpq_vector coeffs(mgr); scoped_mpq_vector coeffs(mgr);
coeffs.push_back(mpq(1)); coeffs.push_back(mpq(1));
coeffs.push_back(mpq(-1)); coeffs.push_back(mpq(-1));
@ -954,8 +956,9 @@ namespace smt {
numeral const& w = e.m_offset; numeral const& w = e.m_offset;
rational fin = w.get_rational().to_rational(); rational fin = w.get_rational().to_rational();
rational inf = w.get_infinitesimal().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); S.set_upper(base_var, q);
inf_mgr.del(q);
} }
unsigned w = num_nodes + num_edges + v; unsigned w = num_nodes + num_edges + v;

9
src/smt/theory_diff_logic_def.h
View file

@ -1107,6 +1107,8 @@ unsigned theory_diff_logic<Ext>::simplex2edge(unsigned e) {
template<typename Ext> template<typename Ext>
void theory_diff_logic<Ext>::update_simplex(Simplex& S) { void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
unsynch_mpq_manager mgr;
unsynch_mpq_inf_manager inf_mgr;
unsigned num_nodes = m_graph.get_num_nodes(); unsigned num_nodes = m_graph.get_num_nodes();
vector<dl_edge<GExt> > const& es = m_graph.get_all_edges(); vector<dl_edge<GExt> > const& es = m_graph.get_all_edges();
S.ensure_var(num_simplex_vars()); S.ensure_var(num_simplex_vars());
@ -1114,13 +1116,13 @@ void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
numeral const& a = m_graph.get_assignment(i); numeral const& a = m_graph.get_assignment(i);
rational fin = a.get_rational().to_rational(); rational fin = a.get_rational().to_rational();
rational inf = a.get_infinitesimal().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); S.set_value(node2simplex(i), q);
inf_mgr.del(q);
} }
S.set_lower(node2simplex(get_zero()), mpq_inf(mpq(0), mpq(0))); S.set_lower(node2simplex(get_zero()), mpq_inf(mpq(0), mpq(0)));
S.set_upper(node2simplex(get_zero()), mpq_inf(mpq(0), mpq(0))); S.set_upper(node2simplex(get_zero()), mpq_inf(mpq(0), mpq(0)));
svector<unsigned> vars; svector<unsigned> vars;
unsynch_mpq_manager mgr;
scoped_mpq_vector coeffs(mgr); scoped_mpq_vector coeffs(mgr);
coeffs.push_back(mpq(1)); coeffs.push_back(mpq(1));
coeffs.push_back(mpq(-1)); coeffs.push_back(mpq(-1));
@ -1145,8 +1147,9 @@ void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
numeral const& w = e.get_weight(); numeral const& w = e.get_weight();
rational fin = w.get_rational().to_rational(); rational fin = w.get_rational().to_rational();
rational inf = w.get_infinitesimal().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); S.set_upper(base_var, q);
inf_mgr.del(q);
} }
else { else {
S.unset_upper(base_var); S.unset_upper(base_var);

3
src/smt/theory_pb.cpp
View file

@ -806,8 +806,9 @@ namespace smt {
if (c != 0) { if (c != 0) {
if (m_enable_simplex) { if (m_enable_simplex) {
row_info const& info = m_ineq_row_info.find(v); row_info const& info = m_ineq_row_info.find(v);
unsynch_mpq_manager mgr;
scoped_eps_numeral coeff(m_mpq_inf_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; unsigned slack = info.m_slack;
if (is_true) { if (is_true) {
update_bound(slack, literal(v), true, coeff); update_bound(slack, literal(v), true, coeff);

1
src/smt/theory_pb.h
View file

@ -279,7 +279,6 @@ namespace smt {
// //
void compile_ineq(ineq& c); void compile_ineq(ineq& c);
void inc_propagations(ineq& c); void inc_propagations(ineq& c);
unsigned get_compilation_threshold(ineq& c);
// //
// Conflict resolution, cutting plane derivation. // Conflict resolution, cutting plane derivation.

5
src/smt/theory_str.cpp
View file

@ -315,6 +315,7 @@ namespace smt {
m_trail.push_back(node); m_trail.push_back(node);
if (!cut_var_map.contains(baseNode)) { if (!cut_var_map.contains(baseNode)) {
T_cut * varInfo = alloc(T_cut); T_cut * varInfo = alloc(T_cut);
m_cut_allocs.push_back(varInfo);
varInfo->level = slevel; varInfo->level = slevel;
varInfo->vars[node] = 1; varInfo->vars[node] = 1;
cut_var_map.insert(baseNode, std::stack<T_cut*>()); cut_var_map.insert(baseNode, std::stack<T_cut*>());
@ -323,6 +324,7 @@ namespace smt {
} else { } else {
if (cut_var_map[baseNode].empty()) { if (cut_var_map[baseNode].empty()) {
T_cut * varInfo = alloc(T_cut); T_cut * varInfo = alloc(T_cut);
m_cut_allocs.push_back(varInfo);
varInfo->level = slevel; varInfo->level = slevel;
varInfo->vars[node] = 1; varInfo->vars[node] = 1;
cut_var_map[baseNode].push(varInfo); cut_var_map[baseNode].push(varInfo);
@ -330,6 +332,7 @@ namespace smt {
} else { } else {
if (cut_var_map[baseNode].top()->level < slevel) { if (cut_var_map[baseNode].top()->level < slevel) {
T_cut * varInfo = alloc(T_cut); T_cut * varInfo = alloc(T_cut);
m_cut_allocs.push_back(varInfo);
varInfo->level = slevel; varInfo->level = slevel;
cut_vars_map_copy(varInfo->vars, cut_var_map[baseNode].top()->vars); cut_vars_map_copy(varInfo->vars, cut_var_map[baseNode].top()->vars);
varInfo->vars[node] = 1; varInfo->vars[node] = 1;
@ -359,6 +362,7 @@ namespace smt {
if (!cut_var_map.contains(destNode)) { if (!cut_var_map.contains(destNode)) {
T_cut * varInfo = alloc(T_cut); T_cut * varInfo = alloc(T_cut);
m_cut_allocs.push_back(varInfo);
varInfo->level = slevel; varInfo->level = slevel;
cut_vars_map_copy(varInfo->vars, cut_var_map[srcNode].top()->vars); cut_vars_map_copy(varInfo->vars, cut_var_map[srcNode].top()->vars);
cut_var_map.insert(destNode, std::stack<T_cut*>()); cut_var_map.insert(destNode, std::stack<T_cut*>());
@ -367,6 +371,7 @@ namespace smt {
} else { } else {
if (cut_var_map[destNode].empty() || cut_var_map[destNode].top()->level < slevel) { if (cut_var_map[destNode].empty() || cut_var_map[destNode].top()->level < slevel) {
T_cut * varInfo = alloc(T_cut); T_cut * varInfo = alloc(T_cut);
m_cut_allocs.push_back(varInfo);
varInfo->level = slevel; varInfo->level = slevel;
cut_vars_map_copy(varInfo->vars, cut_var_map[destNode].top()->vars); cut_vars_map_copy(varInfo->vars, cut_var_map[destNode].top()->vars);
cut_vars_map_copy(varInfo->vars, cut_var_map[srcNode].top()->vars); cut_vars_map_copy(varInfo->vars, cut_var_map[srcNode].top()->vars);

6
src/smt/theory_str.h
View file

@ -18,9 +18,12 @@
#define _THEORY_STR_H_ #define _THEORY_STR_H_
#include "util/trail.h" #include "util/trail.h"
#include "util/union_find.h"
#include "util/scoped_ptr_vector.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "ast/arith_decl_plugin.h" #include "ast/arith_decl_plugin.h"
#include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/th_rewriter.h"
#include "ast/seq_decl_plugin.h"
#include "smt/smt_theory.h" #include "smt/smt_theory.h"
#include "smt/params/theory_str_params.h" #include "smt/params/theory_str_params.h"
#include "smt/proto_model/value_factory.h" #include "smt/proto_model/value_factory.h"
@ -29,8 +32,6 @@
#include<stack> #include<stack>
#include<vector> #include<vector>
#include<map> #include<map>
#include "ast/seq_decl_plugin.h"
#include "util/union_find.h"
namespace smt { namespace smt {
@ -292,6 +293,7 @@ protected:
bool avoidLoopCut; bool avoidLoopCut;
bool loopDetected; bool loopDetected;
obj_map<expr, std::stack<T_cut*> > cut_var_map; obj_map<expr, std::stack<T_cut*> > cut_var_map;
scoped_ptr_vector<T_cut> m_cut_allocs;
expr_ref m_theoryStrOverlapAssumption_term; expr_ref m_theoryStrOverlapAssumption_term;
obj_hashtable<expr> variable_set; obj_hashtable<expr> variable_set;

4
src/smt/watch_list.h
View file

@ -85,6 +85,10 @@ namespace smt {
watch_list(): watch_list():
m_data(0) { m_data(0) {
} }
watch_list(watch_list && other) : m_data(0) {
std::swap(m_data, other.m_data);
}
~watch_list() { ~watch_list() {
destroy(); destroy();

2
src/tactic/sls/bvsls_opt_engine.cpp
View file

@ -238,7 +238,7 @@ bool bvsls_opt_engine::what_if(
mpz bvsls_opt_engine::find_best_move( mpz bvsls_opt_engine::find_best_move(
ptr_vector<func_decl> & to_evaluate, ptr_vector<func_decl> & to_evaluate,
mpz score, mpz & score,
unsigned & best_const, unsigned & best_const,
mpz & best_value, mpz & best_value,
unsigned & new_bit, unsigned & new_bit,

2
src/tactic/sls/bvsls_opt_engine.h
View file

@ -61,7 +61,7 @@ protected:
bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp, bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp,
mpz & best_score, unsigned & best_const, mpz & best_value); mpz & best_score, unsigned & best_const, mpz & best_value);
mpz find_best_move(ptr_vector<func_decl> & to_evaluate, mpz score, mpz find_best_move(ptr_vector<func_decl> & to_evaluate, mpz & score,
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move, unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move,
mpz const & max_score, expr * objective); mpz const & max_score, expr * objective);

41
src/tactic/sls/sls_tracker.h
View file

@ -41,7 +41,24 @@ class sls_tracker {
struct value_score { 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() : 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); } ~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; unsynch_mpz_manager * m;
mpz value; mpz value;
double score; double score;
@ -50,15 +67,6 @@ class sls_tracker {
unsigned has_neg_occ; unsigned has_neg_occ;
unsigned distance; // max distance from any root unsigned distance; // max distance from any root
unsigned touched; 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: public:
@ -294,7 +302,7 @@ public:
if (!m_scores.contains(n)) { if (!m_scores.contains(n)) {
value_score vs; value_score vs;
vs.m = & m_mpz_manager; vs.m = & m_mpz_manager;
m_scores.insert(n, vs); m_scores.insert(n, std::move(vs));
} }
// Update uplinks // Update uplinks
@ -539,7 +547,7 @@ public:
rational r_val; rational r_val;
unsigned bv_sz; unsigned bv_sz;
m_bv_util.is_numeral(val, r_val, 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())); SASSERT(m_mpz_manager.is_one(q.denominator()));
set_value(fd, q.numerator()); set_value(fd, q.numerator());
} }
@ -630,7 +638,7 @@ public:
if (m_bv_util.is_bv_sort(s)) if (m_bv_util.is_bv_sort(s))
return get_random_bv(s); return get_random_bv(s);
else if (m_manager.is_bool(s)) else if (m_manager.is_bool(s))
return get_random_bool(); return m_mpz_manager.dup(get_random_bool());
else else
NOT_IMPLEMENTED_YET(); // This only works for bit-vectors for now. 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); ); 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++) { 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, m_zero);
set_value(it->m_value, temp);
m_mpz_manager.del(temp);
} }
} }
@ -931,7 +937,7 @@ public:
rational q; rational q;
if (!m_bv_util.is_numeral(n, q, bv_sz)) if (!m_bv_util.is_numeral(n, q, bv_sz))
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
mpq temp = q.to_mpq(); const mpq& temp = q.to_mpq();
SASSERT(m_mpz_manager.is_one(temp.denominator())); SASSERT(m_mpz_manager.is_one(temp.denominator()));
m_mpz_manager.set(result, temp.numerator()); m_mpz_manager.set(result, temp.numerator());
} }
@ -1039,7 +1045,6 @@ public:
unsigned pos = -1; unsigned pos = -1;
if (m_ucb) if (m_ucb)
{ {
value_score vscore;
double max = -1.0; 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. // 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++) { /* for (unsigned i = 0; i < m_where_false.size(); i++) {
@ -1048,7 +1053,7 @@ public:
expr * e = as[i]; expr * e = as[i];
if (m_mpz_manager.neq(get_value(e), m_one)) 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. // 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);
double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched) + m_ucb_noise * get_random_uint(8); double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched) + m_ucb_noise * get_random_uint(8);

6
src/test/im_float_config.h
View file

@ -63,10 +63,4 @@ public:
numeral_manager & m() const { return const_cast<numeral_manager&>(m_manager); } numeral_manager & m() const { return const_cast<numeral_manager&>(m_manager); }
}; };
template<typename fmanager>
inline void del_f_interval(im_float_config<fmanager> & cfg, typename im_float_config<fmanager>::interval & a) {
cfg.m().del(a.m_lower);
cfg.m().del(a.m_upper);
}
#endif #endif

78
src/test/interval.cpp
View file

@ -125,7 +125,8 @@ static bool mk_interval(im_default_config & cfg, interval & a, bool l_inf, bool
} }
#endif #endif
static void mk_random_interval(im_default_config & cfg, interval & a, unsigned magnitude) { template <typename T>
static void mk_random_interval(T & cfg, interval & a, unsigned magnitude) {
switch (rand()%3) { switch (rand()%3) {
case 0: case 0:
// Neg, Neg // 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 #define BUFFER_SZ 256
static int g_problem_id = 0; static int g_problem_id = 0;
static char g_buffer[BUFFER_SZ]; 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) { \ static void tst_ ## NAME(unsigned N, unsigned magnitude) { \
reslimit rl; \ reslimit rl; \
unsynch_mpq_manager nm; \ unsynch_mpq_manager nm; \
im_default_config imc(nm); \ interval_manager<im_default_config> im(rl, nm); \
interval_manager<im_default_config> im(rl, imc); \
interval a, b, r; \ interval a, b, r; \
\ \
for (unsigned i = 0; i < N; i++) { \ for (unsigned i = 0; i < N; i++) { \
mk_random_interval(imc, a, magnitude); \ mk_random_interval(im, a, magnitude); \
mk_random_interval(imc, b, magnitude); \ mk_random_interval(im, b, magnitude); \
interval_deps deps; \ interval_deps deps; \
im.NAME(a, b, r, deps); \ im.NAME(a, b, r, deps); \
\ \
display_lemmas(nm, RES_TERM, 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)"); MK_BINARY(mul, "(* a b)");
@ -260,56 +255,52 @@ MK_BINARY(sub, "(- a b)");
static void tst_neg(unsigned N, unsigned magnitude) { static void tst_neg(unsigned N, unsigned magnitude) {
reslimit rl; reslimit rl;
unsynch_mpq_manager nm; unsynch_mpq_manager nm;
im_default_config imc(nm); interval_manager<im_default_config> im(rl, nm);
interval_manager<im_default_config> im(rl, imc);
interval a, b, r; interval a, b, r;
for (unsigned i = 0; i < N; i++) { for (unsigned i = 0; i < N; i++) {
mk_random_interval(imc, a, magnitude); mk_random_interval(im, a, magnitude);
interval_deps deps; interval_deps deps;
im.neg(a, r, deps); im.neg(a, r, deps);
display_lemmas(nm, "(- a)", a, b, 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) { static void tst_pw_2(unsigned N, unsigned magnitude) {
reslimit rl; reslimit rl;
unsynch_mpq_manager nm; unsynch_mpq_manager nm;
im_default_config imc(nm); interval_manager<im_default_config> im(rl, nm);
interval_manager<im_default_config> im(rl, imc);
interval a, b, r; interval a, b, r;
for (unsigned i = 0; i < N; i++) { for (unsigned i = 0; i < N; i++) {
mk_random_interval(imc, a, magnitude); mk_random_interval(im, a, magnitude);
interval_deps deps; interval_deps deps;
im.power(a, 2, r, deps); im.power(a, 2, r, deps);
display_lemmas(nm, "(* a a)", a, b, 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) { static void tst_pw_3(unsigned N, unsigned magnitude) {
reslimit rl; reslimit rl;
unsynch_mpq_manager nm; unsynch_mpq_manager nm;
im_default_config imc(nm); interval_manager<im_default_config> im(rl, nm);
interval_manager<im_default_config> im(rl, imc);
interval a, b, r; interval a, b, r;
for (unsigned i = 0; i < N; i++) { for (unsigned i = 0; i < N; i++) {
mk_random_interval(imc, a, magnitude); mk_random_interval(im, a, magnitude);
interval_deps deps; interval_deps deps;
im.power(a, 3, r, deps); im.power(a, 3, r, deps);
display_lemmas(nm, "(* a a a)", a, b, 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) { static void tst_root_2(unsigned N, unsigned magnitude, unsigned precision) {
reslimit rl; reslimit rl;
unsynch_mpq_manager nm; unsynch_mpq_manager nm;
im_default_config imc(nm); interval_manager<im_default_config> im(rl, nm);
interval_manager<im_default_config> im(rl, imc);
interval a, b, r; interval a, b, r;
scoped_mpq p(nm); scoped_mpq p(nm);
p = precision; p = precision;
@ -317,7 +308,7 @@ static void tst_root_2(unsigned N, unsigned magnitude, unsigned precision) {
unsigned i = 0; unsigned i = 0;
while (i < N) { while (i < N) {
mk_random_interval(imc, a, magnitude); mk_random_interval(im, a, magnitude);
if (!im.lower_is_neg(a)) { if (!im.lower_is_neg(a)) {
i++; i++;
interval_deps deps; 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); 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) { static void tst_root_3(unsigned N, unsigned magnitude, unsigned precision) {
reslimit rl; reslimit rl;
unsynch_mpq_manager nm; unsynch_mpq_manager nm;
im_default_config imc(nm); interval_manager<im_default_config> im(rl, nm);
interval_manager<im_default_config> im(rl, imc);
interval a, b, r; interval a, b, r;
scoped_mpq p(nm); scoped_mpq p(nm);
p = precision; p = precision;
@ -340,25 +330,24 @@ static void tst_root_3(unsigned N, unsigned magnitude, unsigned precision) {
unsigned i = 0; unsigned i = 0;
while (i < N) { while (i < N) {
mk_random_interval(imc, a, magnitude); mk_random_interval(im, a, magnitude);
i++; i++;
interval_deps deps; interval_deps deps;
im.nth_root(a, 3, p, r, deps); im.nth_root(a, 3, p, r, deps);
display_lemmas(nm, "(^ a (/ 1.0 3.0))", a, b, 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) { static void tst_inv(unsigned N, unsigned magnitude) {
reslimit rl; reslimit rl;
unsynch_mpq_manager nm; unsynch_mpq_manager nm;
im_default_config imc(nm); interval_manager<im_default_config> im(rl, nm);
interval_manager<im_default_config> im(rl, imc);
interval a, b, r; interval a, b, r;
for (unsigned i = 0; i < N; i++) { for (unsigned i = 0; i < N; i++) {
while (true) { while (true) {
mk_random_interval(imc, a, magnitude); mk_random_interval(im, a, magnitude);
if (!im.contains_zero(a)) if (!im.contains_zero(a))
break; break;
} }
@ -366,20 +355,19 @@ static void tst_inv(unsigned N, unsigned magnitude) {
im.inv(a, r, deps); im.inv(a, r, deps);
display_lemmas(nm, "(/ 1 a)", a, b, 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) { static void tst_div(unsigned N, unsigned magnitude) {
reslimit rl; reslimit rl;
unsynch_mpq_manager nm; unsynch_mpq_manager nm;
im_default_config imc(nm); interval_manager<im_default_config> im(rl, nm);
interval_manager<im_default_config> im(rl, imc);
interval a, b, r; interval a, b, r;
for (unsigned i = 0; i < N; i++) { for (unsigned i = 0; i < N; i++) {
mk_random_interval(imc, a, magnitude); mk_random_interval(im, a, magnitude);
while (true) { while (true) {
mk_random_interval(imc, b, magnitude); mk_random_interval(im, b, magnitude);
if (!im.contains_zero(b)) if (!im.contains_zero(b))
break; break;
} }
@ -387,7 +375,7 @@ static void tst_div(unsigned N, unsigned magnitude) {
im.div(a, b, r, deps); im.div(a, b, r, deps);
display_lemmas(nm, "(/ a b)", 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" #include "test/im_float_config.h"
@ -396,8 +384,7 @@ static void tst_div(unsigned N, unsigned magnitude) {
static void tst_float() { static void tst_float() {
unsynch_mpq_manager qm; unsynch_mpq_manager qm;
mpf_manager fm; mpf_manager fm;
im_float_config<mpf_manager> ifc(fm); interval_manager<im_float_config<mpf_manager> > im(fm);
interval_manager<im_float_config<mpf_manager> > im(ifc);
im_float_config<mpf_manager>::interval a, b, c; im_float_config<mpf_manager>::interval a, b, c;
scoped_mpq minus_one_third(qm), one_third(qm), two_third(qm), minus_two_third(qm); scoped_mpq minus_one_third(qm), one_third(qm), two_third(qm), minus_two_third(qm);
qm.set(minus_one_third, -1, 3); qm.set(minus_one_third, -1, 3);
@ -424,15 +411,14 @@ static void tst_float() {
im.display(std::cout, c); im.display(std::cout, c);
std::cout << "\n"; 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 #endif
void tst_pi() { void tst_pi() {
reslimit rl; reslimit rl;
unsynch_mpq_manager nm; unsynch_mpq_manager nm;
im_default_config imc(nm); interval_manager<im_default_config> im(rl, nm);
interval_manager<im_default_config> im(rl, imc);
interval r; interval r;
for (unsigned i = 0; i < 8; i++) { for (unsigned i = 0; i < 8; i++) {
im.pi(i, r); im.pi(i, r);
@ -440,7 +426,7 @@ void tst_pi() {
nm.display_decimal(std::cout, im.upper(r), 32); std::cout << "\n"; nm.display_decimal(std::cout, im.upper(r), 32); std::cout << "\n";
ENSURE(nm.lt(im.lower(r), im.upper(r))); ENSURE(nm.lt(im.lower(r), im.upper(r)));
} }
del_interval(imc, r); im.del(r);
} }
#if 0 #if 0

6
src/test/main.cpp
View file

@ -10,9 +10,7 @@
#include "util/memory_manager.h" #include "util/memory_manager.h"
#include "util/gparams.h" #include "util/gparams.h"
static void tst_exit_all_tests() {
exit(0);
}
// //
// Unit tests fail by asserting. // Unit tests fail by asserting.
// If they return, we assume the unit test succeeds // If they return, we assume the unit test succeeds
@ -210,7 +208,7 @@ int main(int argc, char ** argv) {
TST(prime_generator); TST(prime_generator);
TST(permutation); TST(permutation);
TST(nlsat); TST(nlsat);
TST(exit_all_tests); if (test_all) return 0;
TST(ext_numeral); TST(ext_numeral);
TST(interval); TST(interval);
TST(f2n); TST(f2n);

17
src/test/trigo.cpp
View file

@ -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) { static void tst_sine(std::ostream & out, unsigned N, unsigned k) {
unsynch_mpq_manager nm; unsynch_mpq_manager nm;
im_default_config imc(nm);
reslimit rl; reslimit rl;
interval_manager<im_default_config> im(rl, imc); interval_manager<im_default_config> im(rl, nm);
scoped_mpq a(nm); scoped_mpq a(nm);
nm.set(a, 0); nm.set(a, 0);
tst_sine_core(out, nm, im, a, 1); 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) { static void tst_cosine(std::ostream & out, unsigned N, unsigned k) {
reslimit rl; reslimit rl;
unsynch_mpq_manager nm; unsynch_mpq_manager nm;
im_default_config imc(nm); interval_manager<im_default_config> im(rl, nm);
interval_manager<im_default_config> im(rl, imc);
scoped_mpq a(nm); scoped_mpq a(nm);
nm.set(a, 0); nm.set(a, 0);
tst_cosine_core(out, nm, im, a, 1); tst_cosine_core(out, nm, im, a, 1);
@ -100,8 +98,7 @@ template<typename fmanager>
static void tst_float_sine(std::ostream & out, unsigned N, unsigned k) { static void tst_float_sine(std::ostream & out, unsigned N, unsigned k) {
reslimit rl; reslimit rl;
fmanager fm; fmanager fm;
im_float_config<fmanager> ifc(fm, EBITS, SBITS); interval_manager<im_float_config<fmanager> > im(rl, { fm, EBITS, SBITS });
interval_manager<im_float_config<fmanager> > im(rl, ifc);
_scoped_numeral<fmanager> a(fm); _scoped_numeral<fmanager> a(fm);
fm.set(a, EBITS, SBITS, static_cast<int>(0)); fm.set(a, EBITS, SBITS, static_cast<int>(0));
tst_float_sine_core(out, fm, im, a, 1); 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) { static void tst_e(std::ostream & out) {
reslimit rl; reslimit rl;
unsynch_mpq_manager nm; unsynch_mpq_manager nm;
im_default_config imc(nm); interval_manager<im_default_config> im(rl, nm);
interval_manager<im_default_config> im(rl, imc);
im_default_config::interval r; im_default_config::interval r;
for (unsigned i = 0; i < 64; i++) { for (unsigned i = 0; i < 64; i++) {
im.e(i, r); im.e(i, r);
@ -152,8 +148,7 @@ static void tst_e_float(std::ostream & out) {
reslimit rl; reslimit rl;
unsynch_mpq_manager qm; unsynch_mpq_manager qm;
mpf_manager fm; mpf_manager fm;
im_float_config<mpf_manager> ifc(fm); interval_manager<im_float_config<mpf_manager> > im(rl, fm);
interval_manager<im_float_config<mpf_manager> > im(rl, ifc);
scoped_mpq q(qm); scoped_mpq q(qm);
im_float_config<mpf_manager>::interval r; im_float_config<mpf_manager>::interval r;
for (unsigned i = 0; i < 64; i++) { 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 << fm.to_rational_string(im.lower(r)) << " <= E\n";
out << "E <= " << fm.to_rational_string(im.upper(r)) << "\n"; out << "E <= " << fm.to_rational_string(im.upper(r)) << "\n";
} }
del_f_interval(ifc, r); im.del(r);
} }
void tst_trigo() { void tst_trigo() {

7
src/util/buffer.h
View file

@ -149,6 +149,13 @@ public:
new (m_buffer + m_pos) T(elem); new (m_buffer + m_pos) T(elem);
m_pos++; 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() { void pop_back() {
if (CallDestructors) { if (CallDestructors) {

3
src/util/f2n.h
View file

@ -46,6 +46,9 @@ public:
m_manager.set(m_one, ebits, sbits, 1); 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() { ~f2n() {
m().del(m_tmp1); m().del(m_tmp1);
m().del(m_one); m().del(m_one);

58
src/util/hashtable.h
View file

@ -54,7 +54,7 @@ public:
bool is_used() const { return m_state == HT_USED; } bool is_used() const { return m_state == HT_USED; }
T & get_data() { return m_data; } T & get_data() { return m_data; }
const T & get_data() const { 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 set_hash(unsigned h) { m_hash = h; }
void mark_as_deleted() { m_state = HT_DELETED; } void mark_as_deleted() { m_state = HT_DELETED; }
void mark_as_free() { m_state = HT_FREE; } 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() { void expand_table() {
unsigned new_capacity = m_capacity << 1; unsigned new_capacity = m_capacity << 1;
entry * new_table = alloc_table(new_capacity); 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(); delete_table();
m_table = new_table; m_table = new_table;
m_capacity = new_capacity; m_capacity = new_capacity;
@ -202,7 +234,7 @@ protected:
if (memory::is_out_of_memory()) if (memory::is_out_of_memory())
return; return;
entry * new_table = alloc_table(m_capacity); 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(); delete_table();
m_table = new_table; m_table = new_table;
m_num_deleted = 0; m_num_deleted = 0;
@ -321,7 +353,7 @@ public:
#define INSERT_LOOP_BODY() { \ #define INSERT_LOOP_BODY() { \
if (curr->is_used()) { \ if (curr->is_used()) { \
if (curr->get_hash() == hash && equals(curr->get_data(), e)) { \ if (curr->get_hash() == hash && equals(curr->get_data(), e)) { \
curr->set_data(e); \ curr->set_data(std::move(e)); \
return; \ return; \
} \ } \
HS_CODE(m_st_collision++;); \ HS_CODE(m_st_collision++;); \
@ -330,7 +362,7 @@ public:
entry * new_entry; \ entry * new_entry; \
if (del_entry) { new_entry = del_entry; m_num_deleted--; } \ if (del_entry) { new_entry = del_entry; m_num_deleted--; } \
else { new_entry = curr; } \ else { new_entry = curr; } \
new_entry->set_data(e); \ new_entry->set_data(std::move(e)); \
new_entry->set_hash(hash); \ new_entry->set_hash(hash); \
m_size++; \ m_size++; \
return; \ return; \
@ -342,7 +374,7 @@ public:
} \ } \
} ((void) 0) } ((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 * 3)) {
// if ((m_size + m_num_deleted) * 2 > (m_capacity)) { // if ((m_size + m_num_deleted) * 2 > (m_capacity)) {
expand_table(); expand_table();
@ -363,6 +395,11 @@ public:
UNREACHABLE(); UNREACHABLE();
} }
void insert(const data & e) {
data tmp(e);
insert(std::move(tmp));
}
#define INSERT_LOOP_CORE_BODY() { \ #define INSERT_LOOP_CORE_BODY() { \
if (curr->is_used()) { \ if (curr->is_used()) { \
if (curr->get_hash() == hash && equals(curr->get_data(), e)) { \ if (curr->get_hash() == hash && equals(curr->get_data(), e)) { \
@ -375,7 +412,7 @@ public:
entry * new_entry; \ entry * new_entry; \
if (del_entry) { new_entry = del_entry; m_num_deleted--; } \ if (del_entry) { new_entry = del_entry; m_num_deleted--; } \
else { new_entry = curr; } \ else { new_entry = curr; } \
new_entry->set_data(e); \ new_entry->set_data(std::move(e)); \
new_entry->set_hash(hash); \ new_entry->set_hash(hash); \
m_size++; \ m_size++; \
et = new_entry; \ et = new_entry; \
@ -393,7 +430,7 @@ public:
Return true if it is a new element, and false otherwise. Return true if it is a new element, and false otherwise.
Store the entry/slot of the table in et. 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 * 3)) {
// if ((m_size + m_num_deleted) * 2 > (m_capacity)) { // if ((m_size + m_num_deleted) * 2 > (m_capacity)) {
expand_table(); expand_table();
@ -415,6 +452,11 @@ public:
return 0; 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. \brief Insert the element e if it is not in the table.
Return a reference to e or to an object identical to e Return a reference to e or to an object identical to e

6
src/util/mpf.cpp
View file

@ -40,12 +40,6 @@ mpf::mpf(unsigned _ebits, unsigned _sbits):
set(ebits, 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() { mpf::~mpf() {
} }

7
src/util/mpf.h
View file

@ -50,7 +50,12 @@ class mpf {
public: public:
mpf(); mpf();
mpf(unsigned ebits, unsigned sbits); 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(); ~mpf();
unsigned get_ebits() const { return ebits; } unsigned get_ebits() const { return ebits; }
unsigned get_sbits() const { return sbits; } unsigned get_sbits() const { return sbits; }

9
src/util/mpq.h
View file

@ -31,11 +31,10 @@ class mpq {
public: public:
mpq(int v):m_num(v), m_den(1) {} mpq(int v):m_num(v), m_den(1) {}
mpq():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); } 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 & numerator() const { return m_num; }
mpz const & denominator() const { return m_den; } mpz const & denominator() const { return m_den; }
double get_double() const;
}; };
inline void swap(mpq & m1, mpq & m2) { m1.swap(m2); } inline void swap(mpq & m1, mpq & m2) { m1.swap(m2); }
@ -745,6 +744,12 @@ public:
reset_denominator(a); reset_denominator(a);
} }
mpq dup(const mpq & source) {
mpq temp;
set(temp, source);
return temp;
}
void swap(mpz & a, mpz & b) { mpz_manager<SYNCH>::swap(a, b); } void swap(mpz & a, mpz & b) { mpz_manager<SYNCH>::swap(a, b); }
void swap(mpq & a, mpq & b) { void swap(mpq & a, mpq & b) {

15
src/util/mpz.h
View file

@ -94,6 +94,9 @@ class mpz {
public: public:
mpz(int v):m_val(v), m_ptr(0) {} mpz(int v):m_val(v), m_ptr(0) {}
mpz():m_val(0), 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) { void swap(mpz & other) {
std::swap(m_val, other.m_val); std::swap(m_val, other.m_val);
std::swap(m_ptr, other.m_ptr); 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) { void set(mpz & a, int val) {
del(a); del(a);
a.m_val = val; a.m_val = val;
@ -700,6 +709,12 @@ public:
void set(mpz & target, unsigned sz, digit_t const * digits); 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) { void reset(mpz & a) {
del(a); del(a);
a.m_val = 0; a.m_val = 0;

10
src/util/obj_hashtable.h
View file

@ -69,6 +69,10 @@ public:
m_key(k), m_key(k),
m_value(v) { 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; } Value const & get_value() const { return m_value; }
Key & get_key () const { return *m_key; } Key & get_key () const { return *m_key; }
unsigned hash() const { return m_key->hash(); } unsigned hash() const { return m_key->hash(); }
@ -86,7 +90,7 @@ public:
bool is_used() const { return m_data.m_key != reinterpret_cast<Key *>(0) && m_data.m_key != reinterpret_cast<Key *>(1); } bool is_used() const { return m_data.m_key != reinterpret_cast<Key *>(0) && m_data.m_key != reinterpret_cast<Key *>(1); }
key_data const & get_data() const { return m_data; } key_data const & get_data() const { return m_data; }
key_data & get_data() { 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 set_hash(unsigned h) { SASSERT(h == m_data.hash()); }
void mark_as_deleted() { m_data.m_key = reinterpret_cast<Key *>(1); } void mark_as_deleted() { m_data.m_key = reinterpret_cast<Key *>(1); }
void mark_as_free() { m_data.m_key = 0; } void mark_as_free() { m_data.m_key = 0; }
@ -137,6 +141,10 @@ public:
void insert(Key * const k, Value const & v) { void insert(Key * const k, Value const & v) {
m_table.insert(key_data(k, 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) { key_data const & insert_if_not_there(Key * k, Value const & v) {
return m_table.insert_if_not_there(key_data(k, v)); return m_table.insert_if_not_there(key_data(k, v));

4
src/util/obj_ref.h
View file

@ -53,6 +53,10 @@ public:
inc_ref(); 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(); } ~obj_ref() { dec_ref(); }
TManager & get_manager() const { return m_manager; } TManager & get_manager() const { return m_manager; }

1
src/util/rational.h
View file

@ -41,6 +41,7 @@ public:
rational() {} rational() {}
rational(rational const & r) { m().set(m_val, r.m_val); } 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); } explicit rational(int n) { m().set(m_val, n); }

10
src/util/ref_vector.h
View file

@ -45,6 +45,10 @@ public:
typedef T * data; typedef T * data;
ref_vector_core(Ref const & r = Ref()):Ref(r) {} 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() { ~ref_vector_core() {
dec_range_ref(m_nodes.begin(), m_nodes.end()); dec_range_ref(m_nodes.begin(), m_nodes.end());
@ -63,7 +67,7 @@ public:
void resize(unsigned sz) { void resize(unsigned sz) {
if (sz < m_nodes.size()) if (sz < m_nodes.size())
dec_range_ref(m_nodes.begin() + sz, m_nodes.end()); 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) { void resize(unsigned sz, T * d) {
@ -80,7 +84,7 @@ public:
void reserve(unsigned sz) { void reserve(unsigned sz) {
if (sz <= m_nodes.size()) if (sz <= m_nodes.size())
return; return;
m_nodes.resize(sz, 0); m_nodes.resize(sz);
} }
void shrink(unsigned sz) { void shrink(unsigned sz) {
@ -207,6 +211,8 @@ public:
this->append(other); this->append(other);
} }
ref_vector(ref_vector && other) : super(std::move(other)) {}
ref_vector(TManager & m, unsigned sz, T * const * data): ref_vector(TManager & m, unsigned sz, T * const * data):
super(ref_manager_wrapper<T, TManager>(m)) { super(ref_manager_wrapper<T, TManager>(m)) {
this->append(sz, data); this->append(sz, data);

3
src/util/scoped_numeral_vector.h
View file

@ -63,8 +63,7 @@ public:
unsigned old_sz = this->size(); unsigned old_sz = this->size();
if (sz <= old_sz) if (sz <= old_sz)
shrink(sz); shrink(sz);
typename Manager::numeral zero(0); svector<typename Manager::numeral>::resize(sz, 0);
svector<typename Manager::numeral>::resize(sz, zero);
} }
}; };

2
src/util/util.h
View file

@ -322,7 +322,7 @@ bool compare_arrays(const T * array1, const T * array2, unsigned size) {
template<typename T> template<typename T>
void force_ptr_array_size(T & v, unsigned sz) { void force_ptr_array_size(T & v, unsigned sz) {
if (sz > v.size()) { if (sz > v.size()) {
v.resize(sz, 0); v.resize(sz);
} }
} }

110
src/util/vector.h
View file

@ -26,6 +26,7 @@ Revision History:
#include "util/debug.h" #include "util/debug.h"
#include<algorithm> #include<algorithm>
#include<type_traits>
#include<memory.h> #include<memory.h>
#include "util/memory_manager.h" #include "util/memory_manager.h"
#include "util/hash.h" #include "util/hash.h"
@ -74,9 +75,27 @@ class vector {
if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) { if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) {
throw default_exception("Overflow encountered when expanding vector"); throw default_exception("Overflow encountered when expanding vector");
} }
SZ *mem = (SZ*)memory::reallocate(reinterpret_cast<SZ*>(m_data)-2, new_capacity_T); SZ *mem, *old_mem = reinterpret_cast<SZ*>(m_data) - 2;
*mem = new_capacity; #if defined(__GNUC__) && !defined(__clang__) && __GNUC__ < 5
m_data = reinterpret_cast<T *>(mem + 2); if (__has_trivial_copy(T)) {
#else
if (std::is_trivially_copyable<T>::value) {
#endif
mem = (SZ*)memory::reallocate(old_mem, new_capacity_T);
m_data = reinterpret_cast<T *>(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<T *>(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()); SASSERT(size() == source.size());
} }
vector(vector&& other) : m_data(0) {
std::swap(m_data, other.m_data);
}
vector(SZ s, T const * data): vector(SZ s, T const * data):
m_data(0) { m_data(0) {
for (SZ i = 0; i < s; i++) { for (SZ i = 0; i < s; i++) {
@ -179,6 +202,16 @@ public:
return *this; 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() { void reset() {
if (m_data) { if (m_data) {
if (CallDestructors) { if (CallDestructors) {
@ -292,6 +325,11 @@ public:
m_data[idx] = val; m_data[idx] = val;
} }
void set(SZ idx, T && val) {
SASSERT(idx < size());
m_data[idx] = std::move(val);
}
T & back() { T & back() {
SASSERT(!empty()); SASSERT(!empty());
return operator[](size() - 1); return operator[](size() - 1);
@ -318,6 +356,14 @@ public:
reinterpret_cast<SZ *>(m_data)[SIZE_IDX]++; reinterpret_cast<SZ *>(m_data)[SIZE_IDX]++;
} }
void push_back(T && elem) {
if (m_data == 0 || reinterpret_cast<SZ *>(m_data)[SIZE_IDX] == reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX]) {
expand_vector();
}
new (m_data + reinterpret_cast<SZ *>(m_data)[SIZE_IDX]) T(std::move(elem));
reinterpret_cast<SZ *>(m_data)[SIZE_IDX]++;
}
void insert(T const & elem) { void insert(T const & elem) {
push_back(elem); push_back(elem);
} }
@ -357,7 +403,8 @@ public:
} }
} }
void resize(SZ s, T const & elem=T()) { template<typename Args>
void resize(SZ s, Args args...) {
SZ sz = size(); SZ sz = size();
if (s <= sz) { shrink(s); return; } if (s <= sz) { shrink(s); return; }
while (s > capacity()) { while (s > capacity()) {
@ -367,8 +414,23 @@ public:
reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = s; reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = s;
iterator it = m_data + sz; iterator it = m_data + sz;
iterator end = m_data + s; iterator end = m_data + s;
for(; it != end; ++it) { for (; it != end; ++it) {
new (it) T(elem); new (it) T(std::forward<Args>(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<SZ *>(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]; return m_data[idx];
} }
void reserve(SZ s, T const & d = T()) { void reserve(SZ s, T const & d) {
if (s > size()) if (s > size())
resize(s, d); resize(s, d);
} }
void reserve(SZ s) {
if (s > size())
resize(s);
}
}; };
template<typename T> template<typename T>
@ -452,7 +519,12 @@ public:
ptr_vector(unsigned s):vector<T *, false>(s) {} ptr_vector(unsigned s):vector<T *, false>(s) {}
ptr_vector(unsigned s, T * elem):vector<T *, false>(s, elem) {} ptr_vector(unsigned s, T * elem):vector<T *, false>(s, elem) {}
ptr_vector(ptr_vector const & source):vector<T *, false>(source) {} ptr_vector(ptr_vector const & source):vector<T *, false>(source) {}
ptr_vector(ptr_vector && other) : vector<T*, false>(std::move(other)) {}
ptr_vector(unsigned s, T * const * data):vector<T *, false>(s, const_cast<T**>(data)) {} ptr_vector(unsigned s, T * const * data):vector<T *, false>(s, const_cast<T**>(data)) {}
ptr_vector & operator=(ptr_vector const & source) {
vector<T *, false>::operator=(source);
return *this;
}
}; };
template<typename T, typename SZ = unsigned> template<typename T, typename SZ = unsigned>
@ -462,7 +534,12 @@ public:
svector(SZ s):vector<T, false, SZ>(s) {} svector(SZ s):vector<T, false, SZ>(s) {}
svector(SZ s, T const & elem):vector<T, false, SZ>(s, elem) {} svector(SZ s, T const & elem):vector<T, false, SZ>(s, elem) {}
svector(svector const & source):vector<T, false, SZ>(source) {} svector(svector const & source):vector<T, false, SZ>(source) {}
svector(svector && other) : vector<T, false, SZ>(std::move(other)) {}
svector(SZ s, T const * data):vector<T, false, SZ>(s, data) {} svector(SZ s, T const * data):vector<T, false, SZ>(s, data) {}
svector & operator=(svector const & source) {
vector<T, false, SZ>::operator=(source);
return *this;
}
}; };
typedef svector<int> int_vector; typedef svector<int> int_vector;
@ -494,23 +571,4 @@ struct vector_hash : public vector_hash_tpl<Hash, vector<typename Hash::data> >
template<typename Hash> template<typename Hash>
struct svector_hash : public vector_hash_tpl<Hash, svector<typename Hash::data> > {}; struct svector_hash : public vector_hash_tpl<Hash, svector<typename Hash::data> > {};
#include <vector>
// Specialize vector<std::string> to be an instance of std::vector instead.
// This will catch any regression of issue #564 and #420.
template <>
class vector<std::string, true, unsigned> : public std::vector<std::string> {
public:
vector(vector<std::string, true, unsigned> const& other): std::vector<std::string>(other) {}
vector(size_t sz, char const* s): std::vector<std::string>(sz, s) {}
vector() {}
void reset() { clear(); }
};
#endif /* VECTOR_H_ */ #endif /* VECTOR_H_ */