mirror of
https://github.com/Z3Prover/z3
synced 2025-04-18 14:49:01 +00:00
Merge branch 'master' into jfleisher/devIntellitest
This commit is contained in:
jofleish
commit
7321e88764
6
.github/workflows/android-build.yml
vendored
6
.github/workflows/android-build.yml
vendored
|
|
@ -13,7 +13,7 @@ permissions:
|
|||
jobs:
|
||||
build:
|
||||
runs-on: ubuntu-latest
|
||||
|
||||
|
||||
strategy:
|
||||
fail-fast: false
|
||||
matrix:
|
||||
|
|
@ -27,10 +27,10 @@ jobs:
|
|||
run: |
|
||||
mkdir build
|
||||
cd build
|
||||
cmake -DCMAKE_BUILD_TYPE=${{ env.BUILD_TYPE }} -DCMAKE_SYSTEM_NAME=Android -DCMAKE_SYSTEM_VERSION=21 -DCMAKE_ANDROID_ARCH_ABI=${{ matrix.android-abi }} -DCMAKE_ANDROID_NDK=$ANDROID_NDK_HOME -DZ3_BUILD_JAVA_BINDINGS=TRUE -G "Unix Makefiles" -DJAVA_AWT_LIBRARY=NotNeeded -DJAVA_JVM_LIBRARY=NotNeeded -DJAVA_INCLUDE_PATH2=NotNeeded -DJAVA_AWT_INCLUDE_PATH=NotNeeded ../
|
||||
cmake -DCMAKE_BUILD_TYPE=${{ env.BUILD_TYPE }} -DCMAKE_SYSTEM_NAME=Android -DCMAKE_SYSTEM_VERSION=21 -DCMAKE_ANDROID_ARCH_ABI=${{ matrix.android-abi }} "-DCMAKE_ANDROID_NDK=$ANDROID_NDK_LATEST_HOME" -DZ3_BUILD_JAVA_BINDINGS=TRUE -G "Unix Makefiles" -DJAVA_AWT_LIBRARY=NotNeeded -DJAVA_JVM_LIBRARY=NotNeeded -DJAVA_INCLUDE_PATH2=NotNeeded -DJAVA_AWT_INCLUDE_PATH=NotNeeded ../
|
||||
make -j $(nproc)
|
||||
tar -cvf z3-build-${{ matrix.android-abi }}.tar *.jar *.so
|
||||
|
||||
|
||||
- name: Archive production artifacts
|
||||
uses: actions/upload-artifact@v3
|
||||
with:
|
||||
|
|
|
|||
2
.github/workflows/docker-image.yml
vendored
2
.github/workflows/docker-image.yml
vendored
|
|
@ -41,7 +41,7 @@ jobs:
|
|||
type=edge
|
||||
type=sha,prefix=ubuntu-20.04-bare-z3-sha-
|
||||
- name: Build and push Bare Z3 Docker Image
|
||||
uses: docker/build-push-action@v3.0.0
|
||||
uses: docker/build-push-action@v3.1.0
|
||||
with:
|
||||
context: .
|
||||
push: true
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@
|
|||
cmake_minimum_required(VERSION 3.4)
|
||||
|
||||
set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
|
||||
project(Z3 VERSION 4.9.2.0 LANGUAGES CXX)
|
||||
project(Z3 VERSION 4.11.0.0 LANGUAGES CXX)
|
||||
|
||||
################################################################################
|
||||
# Project version
|
||||
|
|
@ -10,13 +10,6 @@ project(Z3 VERSION 4.9.2.0 LANGUAGES CXX)
|
|||
set(Z3_FULL_VERSION_STR "${Z3_VERSION}") # Note this might be modified
|
||||
message(STATUS "Z3 version ${Z3_VERSION}")
|
||||
|
||||
################################################################################
|
||||
# Set various useful variables depending on CMake version
|
||||
################################################################################
|
||||
|
||||
set(ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG "USES_TERMINAL")
|
||||
set(ADD_CUSTOM_TARGET_USES_TERMINAL_ARG "USES_TERMINAL")
|
||||
|
||||
################################################################################
|
||||
# Message for polluted source tree sanity checks
|
||||
################################################################################
|
||||
|
|
@ -185,35 +178,10 @@ set(CMAKE_CXX_STANDARD_REQUIRED ON)
|
|||
################################################################################
|
||||
# Platform detection
|
||||
################################################################################
|
||||
if (CMAKE_SYSTEM_NAME STREQUAL "Linux")
|
||||
message(STATUS "Platform: Linux")
|
||||
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_LINUX_")
|
||||
if (TARGET_ARCHITECTURE STREQUAL "x86_64")
|
||||
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_USE_THREAD_LOCAL")
|
||||
endif()
|
||||
elseif (CMAKE_SYSTEM_NAME STREQUAL "Android")
|
||||
message(STATUS "Platform: Android")
|
||||
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_ANDROID_")
|
||||
elseif (CMAKE_SYSTEM_NAME MATCHES "GNU")
|
||||
message(STATUS "Platform: GNU/Hurd")
|
||||
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_HURD_")
|
||||
elseif (CMAKE_SYSTEM_NAME STREQUAL "Darwin")
|
||||
if (CMAKE_SYSTEM_NAME STREQUAL "Darwin")
|
||||
if (TARGET_ARCHITECTURE STREQUAL "arm64")
|
||||
set(CMAKE_OSX_ARCHITECTURES "arm64")
|
||||
endif()
|
||||
message(STATUS "Platform: Darwin")
|
||||
elseif (CMAKE_SYSTEM_NAME MATCHES "FreeBSD")
|
||||
message(STATUS "Platform: FreeBSD")
|
||||
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_FREEBSD_")
|
||||
elseif (CMAKE_SYSTEM_NAME MATCHES "NetBSD")
|
||||
message(STATUS "Platform: NetBSD")
|
||||
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_NetBSD_")
|
||||
elseif (CMAKE_SYSTEM_NAME MATCHES "OpenBSD")
|
||||
message(STATUS "Platform: OpenBSD")
|
||||
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_OPENBSD_")
|
||||
elseif (CYGWIN)
|
||||
message(STATUS "Platform: Cygwin")
|
||||
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_CYGWIN")
|
||||
elseif (WIN32)
|
||||
message(STATUS "Platform: Windows")
|
||||
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_WINDOWS")
|
||||
|
|
@ -226,8 +194,6 @@ elseif (EMSCRIPTEN)
|
|||
"-s DISABLE_EXCEPTION_CATCHING=0"
|
||||
"-s ERROR_ON_UNDEFINED_SYMBOLS=1"
|
||||
)
|
||||
else()
|
||||
message(FATAL_ERROR "Platform \"${CMAKE_SYSTEM_NAME}\" not recognised")
|
||||
endif()
|
||||
|
||||
list(APPEND Z3_COMPONENT_EXTRA_INCLUDE_DIRS
|
||||
|
|
@ -286,15 +252,7 @@ endif()
|
|||
# FIXME: Support ARM "-mfpu=vfp -mfloat-abi=hard"
|
||||
if ((TARGET_ARCHITECTURE STREQUAL "x86_64") OR (TARGET_ARCHITECTURE STREQUAL "i686"))
|
||||
if ((CMAKE_CXX_COMPILER_ID MATCHES "GNU") OR (CMAKE_CXX_COMPILER_ID MATCHES "Clang") OR (CMAKE_CXX_COMPILER_ID MATCHES "Intel"))
|
||||
if (CMAKE_CXX_COMPILER_ID MATCHES "Intel")
|
||||
# Intel's compiler requires linking with libiomp5
|
||||
list(APPEND Z3_DEPENDENT_LIBS "iomp5")
|
||||
endif()
|
||||
set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2")
|
||||
elseif (CMAKE_CXX_COMPILER_ID MATCHES "Intel")
|
||||
set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2")
|
||||
# Intel's compiler requires linking with libiomp5
|
||||
list(APPEND Z3_DEPENDENT_LIBS "iomp5")
|
||||
elseif (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
|
||||
set(SSE_FLAGS "/arch:SSE2")
|
||||
else()
|
||||
|
|
@ -348,14 +306,6 @@ endif()
|
|||
option(Z3_BUILD_LIBZ3_SHARED "Build libz3 as a shared library if true, otherwise build a static library" ON)
|
||||
|
||||
|
||||
################################################################################
|
||||
# Symbol visibility
|
||||
################################################################################
|
||||
if (NOT MSVC)
|
||||
z3_add_cxx_flag("-fvisibility=hidden" REQUIRED)
|
||||
z3_add_cxx_flag("-fvisibility-inlines-hidden" REQUIRED)
|
||||
endif()
|
||||
|
||||
################################################################################
|
||||
# Tracing
|
||||
################################################################################
|
||||
|
|
@ -367,20 +317,6 @@ else()
|
|||
list(APPEND Z3_COMPONENT_CXX_DEFINES $<$<CONFIG:Debug>:_TRACE>)
|
||||
endif()
|
||||
|
||||
################################################################################
|
||||
# Position independent code
|
||||
################################################################################
|
||||
# This is required because code built in the components will end up in a shared
|
||||
# library.
|
||||
|
||||
# Avoid adding -fPIC compiler switch if we compile with MSVC (which does not
|
||||
# support the flag) or if we target Windows, which generally does not use
|
||||
# position independent code for native code shared libraries (DLLs).
|
||||
if (NOT (MSVC OR MINGW OR WIN32))
|
||||
z3_add_cxx_flag("-fPIC" REQUIRED)
|
||||
endif()
|
||||
|
||||
|
||||
################################################################################
|
||||
# Link time optimization
|
||||
################################################################################
|
||||
|
|
@ -507,7 +443,7 @@ add_custom_target(uninstall
|
|||
COMMAND
|
||||
"${CMAKE_COMMAND}" -P "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake"
|
||||
COMMENT "Uninstalling..."
|
||||
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
|
||||
USES_TERMINAL
|
||||
VERBATIM
|
||||
)
|
||||
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ Pre-built binaries for stable and nightly releases are available from [here](htt
|
|||
Z3 can be built using [Visual Studio][1], a [Makefile][2] or using [CMake][3]. It provides
|
||||
[bindings for several programming languages][4].
|
||||
|
||||
See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z3.
|
||||
See the [release notes](RELEASE_NOTES.md) for notes on various stable releases of Z3.
|
||||
|
||||
## Build status
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
RELEASE NOTES
|
||||
|
||||
Version 4.9.next
|
||||
Version 4.next
|
||||
================
|
||||
- Planned features
|
||||
- sat.euf
|
||||
|
|
@ -10,6 +10,57 @@ Version 4.9.next
|
|||
- native word level bit-vector solving.
|
||||
- introduction of simple induction lemmas to handle a limited repertoire of induction proofs.
|
||||
|
||||
Version 4.11.0
|
||||
==============
|
||||
- remove `Z3_bool`, `Z3_TRUE`, `Z3_FALSE` from the API. Use `bool`, `true`, `false` instead.
|
||||
- z3++.h no longer includes `<sstream>` as it did not use it.
|
||||
- add solver.axioms2files
|
||||
- prints negated theory axioms to files. Each file should be unsat
|
||||
- add solver.lemmas2console
|
||||
- prints lemmas to the console.
|
||||
- remove option smt.arith.dump_lemmas. It is replaced by solver.axioms2files
|
||||
|
||||
Version 4.10.2
|
||||
==============
|
||||
- fix regression #6194. It broke mod/rem/div reasoning.
|
||||
- fix user propagator scope management for equality callbacks.
|
||||
|
||||
Version 4.10.1
|
||||
==============
|
||||
- fix implementation of mk_fresh in user propagator for Python API
|
||||
|
||||
Version 4.10.0
|
||||
==============
|
||||
- Added API Z3_enable_concurrent_dec_ref to be set by interfaces that
|
||||
use concurrent GC to manage reference counts. This feature is integrated
|
||||
with the OCaml bindings and fixes a regression introduced when OCaml
|
||||
transitioned to concurrent GC. Use of this feature for .Net and Java
|
||||
bindings is not integrated for this release. They use external queues
|
||||
that are unnecessarily complicated.
|
||||
- Added pre-declared abstract datatype declarations to the context so
|
||||
that Z3_eval_smtlib2_string works with List examples.
|
||||
- Fixed Java linking for MacOS Arm64.
|
||||
- Added missing callback handlers in tactics for user-propagator,
|
||||
Thanks to Clemens Eisenhofer
|
||||
- Tuning to Grobner arithmetic reasoning for smt.arith.solver=6
|
||||
(currently the default in most cases). The check for consistency
|
||||
modulo multiplication was updated in the following way:
|
||||
- polynomial equalities are extracted from Simplex tableau rows using
|
||||
a cone of influence algorithm. Rows where the basic variables were
|
||||
unbounded were previously included. Following the legacy implementation
|
||||
such rows are not included when building polynomial equations.
|
||||
- equations are pre-solved if they are linear and can be split
|
||||
into two groups one containing a single variable that has a
|
||||
lower (upper) bound, the other with more than two variables
|
||||
with upper (lower) bounds. This avoids losing bounds information
|
||||
during completion.
|
||||
- After (partial) completion, perform constant propagation for equalities
|
||||
of the form x = 0
|
||||
- After (partial) completion, perform factorization for factors of the
|
||||
form x*y*p = 0 where x, are variables, p is linear.
|
||||
- Added support for declaring algebraic datatypes from the C++ interface.
|
||||
|
||||
|
||||
Version 4.9.1
|
||||
=============
|
||||
- Bugfix release to ensure npm package works
|
||||
|
|
|
|||
|
|
@ -122,7 +122,7 @@ macro(z3_add_component component_name)
|
|||
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
|
||||
COMMENT "Generating \"${_full_output_file_path}\" from \"${pyg_file}\""
|
||||
WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}"
|
||||
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
|
||||
USES_TERMINAL
|
||||
VERBATIM
|
||||
)
|
||||
list(APPEND _list_generated_headers "${_full_output_file_path}")
|
||||
|
|
@ -206,6 +206,12 @@ macro(z3_add_component component_name)
|
|||
foreach (flag ${Z3_COMPONENT_CXX_FLAGS})
|
||||
target_compile_options(${component_name} PRIVATE ${flag})
|
||||
endforeach()
|
||||
set_target_properties(${component_name} PROPERTIES
|
||||
# Position independent code needed in shared libraries
|
||||
POSITION_INDEPENDENT_CODE ON
|
||||
# Symbol visibility
|
||||
CXX_VISIBILITY_PRESET hidden
|
||||
VISIBILITY_INLINES_HIDDEN ON)
|
||||
|
||||
# It's unfortunate that we have to manage dependencies ourselves.
|
||||
#
|
||||
|
|
@ -277,7 +283,7 @@ macro(z3_add_install_tactic_rule)
|
|||
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
|
||||
"${CMAKE_CURRENT_BINARY_DIR}/install_tactic.deps"
|
||||
COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp\""
|
||||
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
|
||||
USES_TERMINAL
|
||||
VERBATIM
|
||||
)
|
||||
unset(_expanded_components)
|
||||
|
|
@ -315,7 +321,7 @@ macro(z3_add_memory_initializer_rule)
|
|||
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
|
||||
${_mem_init_finalize_headers}
|
||||
COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp\""
|
||||
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
|
||||
USES_TERMINAL
|
||||
VERBATIM
|
||||
)
|
||||
unset(_mem_init_finalize_headers)
|
||||
|
|
@ -351,7 +357,7 @@ macro(z3_add_gparams_register_modules_rule)
|
|||
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
|
||||
${_register_module_header_files}
|
||||
COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp\""
|
||||
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
|
||||
USES_TERMINAL
|
||||
VERBATIM
|
||||
)
|
||||
unset(_expanded_components)
|
||||
|
|
|
|||
|
|
@ -1,53 +0,0 @@
|
|||
cache:
|
||||
# This persistent cache is used to cache the building of
|
||||
# docker base images.
|
||||
directories:
|
||||
- $DOCKER_TRAVIS_CI_CACHE_DIR
|
||||
sudo: required
|
||||
language: cpp
|
||||
services:
|
||||
- docker
|
||||
env:
|
||||
global:
|
||||
# This environment variable tells the `travis_ci_linux_entry_point.sh`
|
||||
# script to look for a cached Docker image.
|
||||
- DOCKER_TRAVIS_CI_CACHE_DIR=$HOME/.cache/docker
|
||||
# Configurations
|
||||
matrix:
|
||||
###############################################################################
|
||||
# Ubuntu 20.04 LTS
|
||||
###############################################################################
|
||||
# Note the unit tests for the debug builds are compiled but **not**
|
||||
# executed. This is because the debug build of unit tests takes a large
|
||||
# amount of time to execute compared to the optimized builds.
|
||||
|
||||
# clang
|
||||
- LINUX_BASE=ubuntu_20.04 C_COMPILER=clang CXX_COMPILER=clang++ TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug
|
||||
- LINUX_BASE=ubuntu_20.04 C_COMPILER=clang CXX_COMPILER=clang++ TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Release UBSAN_BUILD=1
|
||||
- LINUX_BASE=ubuntu_20.04 C_COMPILER=clang CXX_COMPILER=clang++ TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Release ASAN_BUILD=1 DOTNET_BINDINGS=0 JAVA_BINDINGS=0 PYTHON_BINDINGS=0
|
||||
|
||||
# gcc
|
||||
# ubsan/msan builds too slow
|
||||
- LINUX_BASE=ubuntu_20.04 C_COMPILER=gcc CXX_COMPILER=g++ TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Release BUILD_DOCS=1
|
||||
- LINUX_BASE=ubuntu_20.04 C_COMPILER=gcc CXX_COMPILER=g++ TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug
|
||||
|
||||
# GMP library
|
||||
- LINUX_BASE=ubuntu_20.04 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Release USE_LIBGMP=1
|
||||
- LINUX_BASE=ubuntu_20.04 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug USE_LIBGMP=1
|
||||
|
||||
# Unix Makefile generator build
|
||||
- LINUX_BASE=ubuntu_20.04 TARGET_ARCH=x86_64 Z3_CMAKE_GENERATOR="Unix Makefiles"
|
||||
|
||||
# LTO build
|
||||
# too slow
|
||||
#- LINUX_BASE=ubuntu_20.04 C_COMPILER=gcc CXX_COMPILER=g++ TARGET_ARCH=x86_64 USE_LTO=1 RUN_UNIT_TESTS=BUILD_ONLY RUN_SYSTEM_TESTS=0
|
||||
#- LINUX_BASE=ubuntu_20.04 C_COMPILER=clang CXX_COMPILER=clang++ TARGET_ARCH=x86_64 USE_LTO=1 RUN_UNIT_TESTS=BUILD_ONLY RUN_SYSTEM_TESTS=0
|
||||
|
||||
# Static build. Note we have disable building the bindings because they won't work with a static libz3
|
||||
- LINUX_BASE=ubuntu_20.04 TARGET_ARCH=x86_64 Z3_STATIC_BUILD=1 DOTNET_BINDINGS=0 JAVA_BINDINGS=0 PYTHON_BINDINGS=0
|
||||
|
||||
|
||||
script:
|
||||
# Use `travis_wait` when building because some configurations don't produce an
|
||||
# output for a long time (linking & testing)
|
||||
- travis_wait 55 contrib/ci/scripts/travis_ci_entry_point.sh || exit 1;
|
||||
|
|
@ -1,34 +0,0 @@
|
|||
FROM ubuntu:20.04
|
||||
|
||||
ARG DEBIAN_FRONTEND=noninteractive
|
||||
RUN apt-get update && \
|
||||
apt-get -y --no-install-recommends install \
|
||||
cmake \
|
||||
make \
|
||||
ninja-build \
|
||||
clang \
|
||||
g++ \
|
||||
curl \
|
||||
doxygen \
|
||||
default-jdk \
|
||||
git \
|
||||
graphviz \
|
||||
python3 \
|
||||
python3-setuptools \
|
||||
python-is-python3 \
|
||||
sudo
|
||||
|
||||
RUN curl -SL https://packages.microsoft.com/config/ubuntu/20.04/packages-microsoft-prod.deb --output packages-microsoft-prod.deb && \
|
||||
dpkg -i packages-microsoft-prod.deb && \
|
||||
apt-get update && \
|
||||
apt-get -y --no-install-recommends install dotnet-sdk-2.1
|
||||
|
||||
# Create `user` user for container with password `user`. and give it
|
||||
# password-less sudo access
|
||||
RUN useradd -m user && \
|
||||
echo user:user | chpasswd && \
|
||||
cp /etc/sudoers /etc/sudoers.bak && \
|
||||
echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
|
||||
USER user
|
||||
WORKDIR /home/user
|
||||
#ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-7/bin/llvm-symbolizer
|
||||
|
|
@ -1,121 +0,0 @@
|
|||
ARG DOCKER_IMAGE_BASE
|
||||
FROM ${DOCKER_IMAGE_BASE}
|
||||
|
||||
|
||||
# Build arguments. This can be changed when invoking
|
||||
# `docker build`.
|
||||
ARG ASAN_BUILD
|
||||
ARG BUILD_DOCS
|
||||
ARG CC
|
||||
ARG CXX
|
||||
ARG DOTNET_BINDINGS
|
||||
ARG JAVA_BINDINGS
|
||||
ARG NO_SUPPRESS_OUTPUT
|
||||
ARG PYTHON_BINDINGS
|
||||
ARG PYTHON_EXECUTABLE=/usr/bin/python
|
||||
ARG RUN_API_EXAMPLES
|
||||
ARG RUN_SYSTEM_TESTS
|
||||
ARG RUN_UNIT_TESTS
|
||||
ARG SANITIZER_PRINT_SUPPRESSIONS
|
||||
ARG TARGET_ARCH
|
||||
ARG TEST_INSTALL
|
||||
ARG UBSAN_BUILD
|
||||
ARG Z3_USE_LIBGMP
|
||||
ARG USE_LTO
|
||||
ARG Z3_SRC_DIR=/home/user/z3_src
|
||||
ARG Z3_BUILD_TYPE
|
||||
ARG Z3_CMAKE_GENERATOR
|
||||
ARG Z3_INSTALL_PREFIX
|
||||
ARG Z3_STATIC_BUILD
|
||||
ARG Z3_SYSTEM_TEST_GIT_REVISION
|
||||
ARG Z3_WARNINGS_AS_ERRORS
|
||||
ARG Z3_VERBOSE_BUILD_OUTPUT
|
||||
|
||||
ENV \
|
||||
ASAN_BUILD=${ASAN_BUILD} \
|
||||
BUILD_DOCS=${BUILD_DOCS} \
|
||||
CC=${CC} \
|
||||
CXX=${CXX} \
|
||||
DOTNET_BINDINGS=${DOTNET_BINDINGS} \
|
||||
JAVA_BINDINGS=${JAVA_BINDINGS} \
|
||||
NO_SUPPRESS_OUTPUT=${NO_SUPPRESS_OUTPUT} \
|
||||
PYTHON_BINDINGS=${PYTHON_BINDINGS} \
|
||||
PYTHON_EXECUTABLE=${PYTHON_EXECUTABLE} \
|
||||
SANITIZER_PRINT_SUPPRESSIONS=${SANITIZER_PRINT_SUPPRESSIONS} \
|
||||
RUN_API_EXAMPLES=${RUN_API_EXAMPLES} \
|
||||
RUN_SYSTEM_TESTS=${RUN_SYSTEM_TESTS} \
|
||||
RUN_UNIT_TESTS=${RUN_UNIT_TESTS} \
|
||||
TARGET_ARCH=${TARGET_ARCH} \
|
||||
TEST_INSTALL=${TEST_INSTALL} \
|
||||
UBSAN_BUILD=${UBSAN_BUILD} \
|
||||
Z3_USE_LIBGMP=${Z3_USE_LIBGMP} \
|
||||
USE_LTO=${USE_LTO} \
|
||||
Z3_SRC_DIR=${Z3_SRC_DIR} \
|
||||
Z3_BUILD_DIR=/home/user/z3_build \
|
||||
Z3_BUILD_TYPE=${Z3_BUILD_TYPE} \
|
||||
Z3_CMAKE_GENERATOR=${Z3_CMAKE_GENERATOR} \
|
||||
Z3_VERBOSE_BUILD_OUTPUT=${Z3_VERBOSE_BUILD_OUTPUT} \
|
||||
Z3_STATIC_BUILD=${Z3_STATIC_BUILD} \
|
||||
Z3_SYSTEM_TEST_DIR=/home/user/z3_system_test \
|
||||
Z3_SYSTEM_TEST_GIT_REVISION=${Z3_SYSTEM_TEST_GIT_REVISION} \
|
||||
Z3_WARNINGS_AS_ERRORS=${Z3_WARNINGS_AS_ERRORS} \
|
||||
Z3_INSTALL_PREFIX=${Z3_INSTALL_PREFIX}
|
||||
|
||||
# We add context across incrementally to maximal cache reuse
|
||||
|
||||
# Build Z3
|
||||
RUN mkdir -p "${Z3_SRC_DIR}" && \
|
||||
mkdir -p "${Z3_SRC_DIR}/contrib/ci/scripts" && \
|
||||
mkdir -p "${Z3_SRC_DIR}/contrib/suppressions/sanitizers"
|
||||
# Deliberately leave out `contrib`
|
||||
ADD /cmake ${Z3_SRC_DIR}/cmake/
|
||||
ADD /doc ${Z3_SRC_DIR}/doc/
|
||||
ADD /examples ${Z3_SRC_DIR}/examples/
|
||||
ADD /scripts ${Z3_SRC_DIR}/scripts/
|
||||
ADD /src ${Z3_SRC_DIR}/src/
|
||||
ADD *.txt *.md *.cmake.in RELEASE_NOTES ${Z3_SRC_DIR}/
|
||||
|
||||
ADD \
|
||||
/contrib/ci/scripts/build_z3_cmake.sh \
|
||||
/contrib/ci/scripts/ci_defaults.sh \
|
||||
/contrib/ci/scripts/set_compiler_flags.sh \
|
||||
/contrib/ci/scripts/set_generator_args.sh \
|
||||
${Z3_SRC_DIR}/contrib/ci/scripts/
|
||||
RUN ${Z3_SRC_DIR}/contrib/ci/scripts/build_z3_cmake.sh
|
||||
|
||||
# Test building docs
|
||||
ADD \
|
||||
/contrib/ci/scripts/test_z3_docs.sh \
|
||||
/contrib/ci/scripts/run_quiet.sh \
|
||||
${Z3_SRC_DIR}/contrib/ci/scripts/
|
||||
RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_docs.sh
|
||||
|
||||
# Test examples
|
||||
ADD \
|
||||
/contrib/ci/scripts/test_z3_examples_cmake.sh \
|
||||
/contrib/ci/scripts/sanitizer_env.sh \
|
||||
${Z3_SRC_DIR}/contrib/ci/scripts/
|
||||
ADD \
|
||||
/contrib/suppressions/sanitizers/asan.txt \
|
||||
/contrib/suppressions/sanitizers/lsan.txt \
|
||||
/contrib/suppressions/sanitizers/ubsan.txt \
|
||||
${Z3_SRC_DIR}/contrib/suppressions/sanitizers/
|
||||
RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_examples_cmake.sh
|
||||
|
||||
# Run unit tests
|
||||
ADD \
|
||||
/contrib/ci/scripts/test_z3_unit_tests_cmake.sh \
|
||||
${Z3_SRC_DIR}/contrib/ci/scripts/
|
||||
RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_unit_tests_cmake.sh
|
||||
|
||||
# Run system tests
|
||||
ADD \
|
||||
/contrib/ci/scripts/test_z3_system_tests.sh \
|
||||
${Z3_SRC_DIR}/contrib/ci/scripts/
|
||||
RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_system_tests.sh
|
||||
|
||||
# Test install
|
||||
ADD \
|
||||
/contrib/ci/scripts/test_z3_install_cmake.sh \
|
||||
${Z3_SRC_DIR}/contrib/ci/scripts/
|
||||
RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_install_cmake.sh
|
||||
|
|
@ -1,147 +0,0 @@
|
|||
# Continuous integration scripts
|
||||
|
||||
## TravisCI
|
||||
|
||||
For testing on Linux and macOS we use [TravisCI](https://travis-ci.org/)
|
||||
|
||||
TravisCI consumes the `.travis.yml` file in the root of the repository
|
||||
to tell it how to build and test Z3.
|
||||
|
||||
However the logic for building and test Z3 is kept out of this file
|
||||
and instead in a set of scripts in `scripts/`. This avoids
|
||||
coupling the build to TravisCI tightly so we can migrate to another
|
||||
service if required in the future.
|
||||
|
||||
The scripts rely on a set of environment variables to control the configuration
|
||||
of the build. The `.travis.yml` declares a list of configuration with each
|
||||
configuration setting different environment variables.
|
||||
|
||||
Note that the build scripts currently only support Z3 built with CMake. Support
|
||||
for building Z3 using the older Python/Makefile build system might be added in
|
||||
the future.
|
||||
|
||||
### Configuration variables
|
||||
|
||||
* `ASAN_BUILD` - Do [AddressSanitizer](https://github.com/google/sanitizers/wiki/AddressSanitizer) build (`0` or `1`)
|
||||
* `BUILD_DOCS` - Build API documentation (`0` or `1`)
|
||||
* `C_COMPILER` - Path to C Compiler
|
||||
* `CXX_COMPILER` - Path to C++ Compiler
|
||||
* `DOTNET_BINDINGS` - Build and test .NET API bindings (`0` or `1`)
|
||||
* `JAVA_BINDINGS` - Build and test Java API bindings (`0` or `1`)
|
||||
* `NO_SUPPRESS_OUTPUT` - Don't suppress output of some commands (`0` or `1`)
|
||||
* `PYTHON_BINDINGS` - Build and test Python API bindings (`0` or `1`)
|
||||
* `RUN_API_EXAMPLES` - Build and run API examples (`0` or `1`)
|
||||
* `RUN_SYSTEM_TESTS` - Run system tests (`0` or `1`)
|
||||
* `RUN_UNIT_TESTS` - Run unit tests (`BUILD_ONLY` or `BUILD_AND_RUN` or `SKIP`)
|
||||
* `SANITIZER_PRINT_SUPPRESSIONS` - Show ASan/UBSan suppressions (`0` or `1`)
|
||||
* `TARGET_ARCH` - Target architecture (`x86_64` or `i686`)
|
||||
* `TEST_INSTALL` - Test running `install` target (`0` or `1`)
|
||||
* `UBSAN_BUILD` - Do [UndefinedBehaviourSanitizer](https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html) build (`0` or `1`)
|
||||
* `Z3_USE_LIBGMP` - Use [GNU multiple precision library](https://gmplib.org/) (`0` or `1`)
|
||||
* `USE_LTO` - Link binaries using link time optimization (`0` or `1`)
|
||||
* `Z3_BUILD_TYPE` - CMake build type (`RelWithDebInfo`, `Release`, `Debug`, or `MinSizeRel`)
|
||||
* `Z3_CMAKE_GENERATOR` - CMake generator (`Ninja` or `Unix Makefiles`)
|
||||
* `Z3_VERBOSE_BUILD_OUTPUT` - Show compile commands in CMake builds (`0` or `1`)
|
||||
* `Z3_BUILD_LIBZ3_SHARED` - Build Z3 binaries and libraries dynamically/statically (`0` or `1`)
|
||||
* `Z3_SYSTEM_TEST_GIT_REVISION` - Git revision of [z3test](https://github.com/Z3Prover/z3test). If empty latest revision will be used.
|
||||
* `Z3_WARNINGS_AS_ERRORS` - Set the `WARNINGS_AS_ERRORS` CMake option passed to Z3 (`OFF`, `ON`, or `SERIOUS_ONLY`)
|
||||
|
||||
### Linux
|
||||
|
||||
For Linux we use Docker to perform the build so that it easily reproducible
|
||||
on a local machine and so that we can avoid depending on TravisCI's environment
|
||||
and instead use a Linux distribution of our choice.
|
||||
|
||||
The `scripts/travis_ci_linux_entry_point.sh` script
|
||||
|
||||
1. Creates a base image containing all the dependencies needed to build and test Z3
|
||||
2. Builds and tests Z3 using the base image propagating configuration environment
|
||||
variables (if set) into the build using the `--build-arg` argument of the `docker run`
|
||||
command.
|
||||
|
||||
The default values of the configuration environment variables
|
||||
can be found in
|
||||
[`scripts/ci_defaults.sh`](scripts/ci_defaults.sh).
|
||||
|
||||
#### Linux specific configuration variables
|
||||
|
||||
* `LINUX_BASE` - The base docker image identifier to use (`ubuntu_16.04`, `ubuntu32_16.04`, or `ubuntu_14.04`).
|
||||
|
||||
#### Reproducing a build locally
|
||||
|
||||
A build can be reproduced locally by using the
|
||||
`scripts/travis_ci_linux_entry_point.sh` script and setting the appropriate
|
||||
environment variable.
|
||||
|
||||
For example lets say we wanted to reproduce the build below.
|
||||
|
||||
```yaml
|
||||
|
||||
- LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo
|
||||
```
|
||||
|
||||
This can be done by running the command
|
||||
|
||||
```bash
|
||||
LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo scripts/travis_ci_linux_entry_point.sh
|
||||
```
|
||||
|
||||
The `docker build` command which we use internally supports caching. What this
|
||||
means in practice is that re-running the above command will re-use successfully
|
||||
completed stages of the build provided they haven't changed. This requires that
|
||||
the `Dockerfiles/z3_build.Dockerfile` is carefully crafted to avoid invalidating
|
||||
the cache when unrelated files sent to the build context change.
|
||||
|
||||
#### TravisCI docker image cache
|
||||
|
||||
To improve build times the Z3 base docker images are cached using
|
||||
[TravisCI's cache directory feature](https://docs.travis-ci.com/user/caching).
|
||||
If the `DOCKER_TRAVIS_CI_CACHE_DIR` environment variable is set (see `.travis.yml`)
|
||||
then the directory pointed to by the environment variable is used as a cache
|
||||
for Docker images.
|
||||
|
||||
The logic for this can be found in `scripts/travis_ci_linux_entry_point.sh`.
|
||||
The build time improvements are rather modest (~ 2 minutes) and the cache is
|
||||
rather large due to TravisCI giving each configuration its own cache. So this
|
||||
feature might be removed in the future.
|
||||
|
||||
It may be better to just build the base image once (outside of TravisCI), upload
|
||||
it to [DockerHub](https://hub.docker.com/) and have the build pull down the pre-built
|
||||
image every time.
|
||||
|
||||
An [organization](https://hub.docker.com/u/z3prover/) has been created on
|
||||
DockerHub for this.
|
||||
|
||||
### macOS
|
||||
|
||||
For macOS we execute directly on TravisCI's macOS environment. The entry point
|
||||
for the TravisCI builds is the
|
||||
[`scripts/travis_ci_osx_entry_point.sh`](scripts/travis_ci_osx_entry_point.sh)
|
||||
scripts.
|
||||
|
||||
#### macOS specific configuration variables
|
||||
|
||||
* `MACOS_SKIP_DEPS_UPDATE` - If set to `1` installing the necessary build dependencies
|
||||
is skipped. This is useful for local testing if the dependencies are already installed.
|
||||
* `MACOS_UPDATE_CMAKE` - If set to `1` the installed version of CMake will be upgraded.
|
||||
|
||||
#### Reproducing a build locally
|
||||
|
||||
To reproduce a build (e.g. like the one shown below)
|
||||
|
||||
```yaml
|
||||
- os: osx
|
||||
osx_image: xcode8.3
|
||||
env: Z3_BUILD_TYPE=RelWithDebInfo
|
||||
```
|
||||
|
||||
Run the following:
|
||||
|
||||
```bash
|
||||
TRAVIS_BUILD_DIR=$(pwd) \
|
||||
Z3_BUILD_TYPE=RelWithDebInfo \
|
||||
contrib/ci/scripts/travis_ci_osx_entry_point.sh
|
||||
```
|
||||
|
||||
Note this assumes that the current working directory is the root of the Z3
|
||||
git repository.
|
||||
|
|
@ -1,3 +0,0 @@
|
|||
# Maintainers
|
||||
|
||||
- Dan Liew (@delcypher)
|
||||
|
|
@ -1,133 +0,0 @@
|
|||
#!/bin/bash
|
||||
# This script builds Z3
|
||||
|
||||
SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
|
||||
|
||||
set -x
|
||||
set -e
|
||||
set -o pipefail
|
||||
|
||||
: ${Z3_SRC_DIR?"Z3_SRC_DIR must be specified"}
|
||||
: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"}
|
||||
: ${Z3_BUILD_TYPE?"Z3_BUILD_TYPE must be specified"}
|
||||
: ${Z3_CMAKE_GENERATOR?"Z3_CMAKE_GENERATOR must be specified"}
|
||||
: ${Z3_STATIC_BUILD?"Z3_STATIC_BUILD must be specified"}
|
||||
: ${Z3_USE_LIBGMP?"Z3_USE_LIBGMP must be specified"}
|
||||
: ${BUILD_DOCS?"BUILD_DOCS must be specified"}
|
||||
: ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"}
|
||||
: ${PYTHON_BINDINGS?"PYTHON_BINDINGS must be specified"}
|
||||
: ${DOTNET_BINDINGS?"DOTNET_BINDINGS must be specified"}
|
||||
: ${JAVA_BINDINGS?"JAVA_BINDINGS must be specified"}
|
||||
: ${USE_LTO?"USE_LTO must be specified"}
|
||||
: ${Z3_INSTALL_PREFIX?"Z3_INSTALL_PREFIX must be specified"}
|
||||
: ${Z3_WARNINGS_AS_ERRORS?"Z3_WARNINGS_AS_ERRORS must be specified"}
|
||||
: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"}
|
||||
|
||||
ADDITIONAL_Z3_OPTS=()
|
||||
|
||||
# Static or dynamic libz3
|
||||
if [ "X${Z3_STATIC_BUILD}" = "X1" ]; then
|
||||
ADDITIONAL_Z3_OPTS+=('-DZ3_BUILD_LIBZ3_SHARED=OFF')
|
||||
else
|
||||
ADDITIONAL_Z3_OPTS+=('-DZ3_BUILD_LIBZ3_SHARED=ON')
|
||||
fi
|
||||
|
||||
# Use LibGMP?
|
||||
if [ "X${Z3_USE_LIBGMP}" = "X1" ]; then
|
||||
ADDITIONAL_Z3_OPTS+=('-DZ3_USE_LIB_GMP=ON')
|
||||
else
|
||||
ADDITIONAL_Z3_OPTS+=('-DZ3_USE_LIB_GMP=OFF')
|
||||
fi
|
||||
|
||||
# Use link time optimziation?
|
||||
if [ "X${USE_LTO}" = "X1" ]; then
|
||||
ADDITIONAL_Z3_OPTS+=('-DZ3_LINK_TIME_OPTIMIZATION=ON')
|
||||
else
|
||||
ADDITIONAL_Z3_OPTS+=('-DZ3_LINK_TIME_OPTIMIZATION=OFF')
|
||||
fi
|
||||
|
||||
# Build API docs?
|
||||
if [ "X${BUILD_DOCS}" = "X1" ]; then
|
||||
ADDITIONAL_Z3_OPTS+=( \
|
||||
'-DZ3_BUILD_DOCUMENTATION=ON' \
|
||||
'-DZ3_ALWAYS_BUILD_DOCS=OFF' \
|
||||
)
|
||||
else
|
||||
ADDITIONAL_Z3_OPTS+=('-DZ3_BUILD_DOCUMENTATION=OFF')
|
||||
fi
|
||||
|
||||
# Python bindings?
|
||||
if [ "X${PYTHON_BINDINGS}" = "X1" ]; then
|
||||
ADDITIONAL_Z3_OPTS+=( \
|
||||
'-DZ3_BUILD_PYTHON_BINDINGS=ON' \
|
||||
'-DZ3_INSTALL_PYTHON_BINDINGS=ON' \
|
||||
)
|
||||
else
|
||||
ADDITIONAL_Z3_OPTS+=( \
|
||||
'-DZ3_BUILD_PYTHON_BINDINGS=OFF' \
|
||||
'-DZ3_INSTALL_PYTHON_BINDINGS=OFF' \
|
||||
)
|
||||
fi
|
||||
|
||||
# .NET bindings?
|
||||
if [ "X${DOTNET_BINDINGS}" = "X1" ]; then
|
||||
ADDITIONAL_Z3_OPTS+=( \
|
||||
'-DZ3_BUILD_DOTNET_BINDINGS=ON' \
|
||||
'-DZ3_INSTALL_DOTNET_BINDINGS=ON' \
|
||||
)
|
||||
else
|
||||
ADDITIONAL_Z3_OPTS+=( \
|
||||
'-DZ3_BUILD_DOTNET_BINDINGS=OFF' \
|
||||
'-DZ3_INSTALL_DOTNET_BINDINGS=OFF' \
|
||||
)
|
||||
fi
|
||||
|
||||
# Java bindings?
|
||||
if [ "X${JAVA_BINDINGS}" = "X1" ]; then
|
||||
ADDITIONAL_Z3_OPTS+=( \
|
||||
'-DZ3_BUILD_JAVA_BINDINGS=ON' \
|
||||
'-DZ3_INSTALL_JAVA_BINDINGS=ON' \
|
||||
)
|
||||
else
|
||||
ADDITIONAL_Z3_OPTS+=( \
|
||||
'-DZ3_BUILD_JAVA_BINDINGS=OFF' \
|
||||
'-DZ3_INSTALL_JAVA_BINDINGS=OFF' \
|
||||
)
|
||||
fi
|
||||
|
||||
# Set compiler flags
|
||||
source ${SCRIPT_DIR}/set_compiler_flags.sh
|
||||
|
||||
if [ "X${UBSAN_BUILD}" = "X1" ]; then
|
||||
# HACK: When building with UBSan the C++ linker
|
||||
# must be used to avoid the following linker errors.
|
||||
# undefined reference to `__ubsan_vptr_type_cache'
|
||||
# undefined reference to `__ubsan_handle_dynamic_type_cache_miss'
|
||||
ADDITIONAL_Z3_OPTS+=( \
|
||||
'-DZ3_C_EXAMPLES_FORCE_CXX_LINKER=ON' \
|
||||
)
|
||||
fi
|
||||
|
||||
# Sanity check
|
||||
if [ ! -e "${Z3_SRC_DIR}/CMakeLists.txt" ]; then
|
||||
echo "Z3_SRC_DIR is invalid"
|
||||
exit 1
|
||||
fi
|
||||
|
||||
# Make build tree
|
||||
mkdir -p "${Z3_BUILD_DIR}"
|
||||
cd "${Z3_BUILD_DIR}"
|
||||
|
||||
# Configure
|
||||
cmake \
|
||||
-G "${Z3_CMAKE_GENERATOR}" \
|
||||
-DCMAKE_BUILD_TYPE=${Z3_BUILD_TYPE} \
|
||||
-DPYTHON_EXECUTABLE=${PYTHON_EXECUTABLE} \
|
||||
-DCMAKE_INSTALL_PREFIX=${Z3_INSTALL_PREFIX} \
|
||||
-DWARNINGS_AS_ERRORS=${Z3_WARNINGS_AS_ERRORS} \
|
||||
"${ADDITIONAL_Z3_OPTS[@]}" \
|
||||
"${Z3_SRC_DIR}"
|
||||
|
||||
# Build
|
||||
source ${SCRIPT_DIR}/set_generator_args.sh
|
||||
cmake --build $(pwd) "${GENERATOR_ARGS[@]}"
|
||||
|
|
@ -1,59 +0,0 @@
|
|||
# This file should be sourced by other scripts
|
||||
# and not executed directly
|
||||
|
||||
# Set CI build defaults
|
||||
|
||||
export ASAN_BUILD="${ASAN_BUILD:-0}"
|
||||
export BUILD_DOCS="${BUILD_DOCS:-0}"
|
||||
export DOTNET_BINDINGS="${DOTNET_BINDINGS:-1}"
|
||||
export JAVA_BINDINGS="${JAVA_BINDINGS:-1}"
|
||||
export NO_SUPPRESS_OUTPUT="${NO_SUPPRESS_OUTPUT:-0}"
|
||||
export PYTHON_BINDINGS="${PYTHON_BINDINGS:-1}"
|
||||
export RUN_API_EXAMPLES="${RUN_API_EXAMPLES:-1}"
|
||||
export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}"
|
||||
export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-BUILD_AND_RUN}"
|
||||
# Don't print suppressions by default because that breaks the Z3
|
||||
# regression tests because they don't expect them to appear in Z3's
|
||||
# output.
|
||||
export SANITIZER_PRINT_SUPPRESSIONS="${SANITIZER_PRINT_SUPPRESSIONS:-0}"
|
||||
export TARGET_ARCH="${TARGET_ARCH:-x86_64}"
|
||||
export TEST_INSTALL="${TEST_INSTALL:-1}"
|
||||
export UBSAN_BUILD="${UBSAN_BUILD:-0}"
|
||||
export Z3_USE_LIBGMP="${Z3_USE_LIBGMP:-0}"
|
||||
export USE_LTO="${USE_LTO:-0}"
|
||||
|
||||
export Z3_BUILD_TYPE="${Z3_BUILD_TYPE:-RelWithDebInfo}"
|
||||
export Z3_CMAKE_GENERATOR="${Z3_CMAKE_GENERATOR:-Ninja}"
|
||||
export Z3_STATIC_BUILD="${Z3_STATIC_BUILD:-0}"
|
||||
# Default is blank which means get latest revision
|
||||
export Z3_SYSTEM_TEST_GIT_REVISION="${Z3_SYSTEM_TEST_GIT_REVISION:-}"
|
||||
export Z3_WARNINGS_AS_ERRORS="${Z3_WARNINGS_AS_ERRORS:-SERIOUS_ONLY}"
|
||||
export Z3_VERBOSE_BUILD_OUTPUT="${Z3_VERBOSE_BUILD_OUTPUT:-0}"
|
||||
|
||||
# Platform specific defaults
|
||||
PLATFORM="$(uname -s)"
|
||||
case "${PLATFORM}" in
|
||||
Linux*)
|
||||
export C_COMPILER="${C_COMPILER:-gcc}"
|
||||
export CXX_COMPILER="${CXX_COMPILER:-g++}"
|
||||
export Z3_INSTALL_PREFIX="${Z3_INSTALL_PREFIX:-/usr}"
|
||||
;;
|
||||
Darwin*)
|
||||
export C_COMPILER="${C_COMPILER:-clang}"
|
||||
export CXX_COMPILER="${CXX_COMPILER:-clang++}"
|
||||
export Z3_INSTALL_PREFIX="${Z3_INSTALL_PREFIX:-/usr/local}"
|
||||
;;
|
||||
*)
|
||||
echo "Unknown platform \"${PLATFORM}\""
|
||||
exit 1
|
||||
;;
|
||||
esac
|
||||
unset PLATFORM
|
||||
|
||||
# NOTE: The following variables are not set here because
|
||||
# they are specific to the CI implementation
|
||||
# PYTHON_EXECUTABLE
|
||||
# ASAN_DSO
|
||||
# Z3_SRC_DIR
|
||||
# Z3_BUILD_DIR
|
||||
# Z3_SYSTEM_TEST_DIR
|
||||
|
|
@ -1,47 +0,0 @@
|
|||
#!/bin/bash
|
||||
|
||||
SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
|
||||
. ${SCRIPT_DIR}/run_quiet.sh
|
||||
|
||||
set -x
|
||||
set -e
|
||||
set -o pipefail
|
||||
|
||||
run_quiet brew update
|
||||
export HOMEBREW_NO_AUTO_UPDATE=1
|
||||
|
||||
function brew_install_or_upgrade() {
|
||||
if brew ls --versions "$1" > /dev/null 2>&1 ; then
|
||||
brew upgrade "$1"
|
||||
else
|
||||
brew install "$1"
|
||||
fi
|
||||
}
|
||||
|
||||
# FIXME: We should fix the versions of dependencies used
|
||||
# so that we have reproducible builds.
|
||||
|
||||
# HACK: Just use CMake version in TravisCI for now
|
||||
if [ "X${MACOS_UPDATE_CMAKE}" = "X1" ]; then
|
||||
brew_install_or_upgrade cmake
|
||||
fi
|
||||
|
||||
if [ "X${Z3_CMAKE_GENERATOR}" = "XNinja" ]; then
|
||||
brew_install_or_upgrade ninja
|
||||
fi
|
||||
|
||||
if [ "X${Z3_USE_LIBGMP}" = "X1" ]; then
|
||||
brew_install_or_upgrade gmp
|
||||
fi
|
||||
|
||||
if [ "X${BUILD_DOCS}" = "X1" ]; then
|
||||
brew_install_or_upgrade doxygen
|
||||
fi
|
||||
|
||||
if [ "X${DOTNET_BINDINGS}" = "X1" ]; then
|
||||
brew_install_or_upgrade mono
|
||||
fi
|
||||
|
||||
if [ "X${JAVA_BINDINGS}" = "X1" ]; then
|
||||
brew cask install java
|
||||
fi
|
||||
|
|
@ -1,41 +0,0 @@
|
|||
# Simple wrapper function that runs a command suppressing
|
||||
# it's output. However it's output will be shown in the
|
||||
# case that `NO_SUPPRESS_OUTPUT` is set to `1` or the command
|
||||
# fails.
|
||||
#
|
||||
# The use case for this trying to avoid large logs on TravisCI
|
||||
function run_quiet() {
|
||||
if [ "X${NO_SUPPRESS_OUTPUT}" = "X1" ]; then
|
||||
"${@}"
|
||||
else
|
||||
OLD_SETTINGS="$-"
|
||||
set +x
|
||||
set +e
|
||||
TMP_DIR="${TMP_DIR:-/tmp/}"
|
||||
STDOUT="${TMP_DIR}/$$.stdout"
|
||||
STDERR="${TMP_DIR}/$$.stderr"
|
||||
"${@}" > "${STDOUT}" 2> "${STDERR}"
|
||||
EXIT_STATUS="$?"
|
||||
if [ "${EXIT_STATUS}" -ne 0 ]; then
|
||||
echo "Command \"$@\" failed"
|
||||
echo "EXIT CODE: ${EXIT_STATUS}"
|
||||
echo "STDOUT"
|
||||
echo ""
|
||||
echo "\`\`\`"
|
||||
cat ${STDOUT}
|
||||
echo "\`\`\`"
|
||||
echo ""
|
||||
echo "STDERR"
|
||||
echo ""
|
||||
echo "\`\`\`"
|
||||
cat ${STDERR}
|
||||
echo "\`\`\`"
|
||||
echo ""
|
||||
fi
|
||||
# Clean up
|
||||
rm "${STDOUT}" "${STDERR}"
|
||||
[ "$( echo "${OLD_SETTINGS}" | grep -c 'e')" != "0" ] && set -e
|
||||
[ "$( echo "${OLD_SETTINGS}" | grep -c 'x')" != "0" ] && set -x
|
||||
return ${EXIT_STATUS}
|
||||
fi
|
||||
}
|
||||
|
|
@ -1,58 +0,0 @@
|
|||
# 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.
|
||||
# leak checking disabled because it doesn't work on unpriviledged docker
|
||||
export ASAN_OPTIONS="malloc_context_size=100,detect_leaks=0,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" "${@}"
|
||||
}
|
||||
|
||||
function run_non_native_binding() {
|
||||
"${@}"
|
||||
}
|
||||
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
|
||||
|
|
@ -1,46 +0,0 @@
|
|||
# This script should is intended to be included by other
|
||||
# scripts and should not be executed directly
|
||||
|
||||
: ${TARGET_ARCH?"TARGET_ARCH must be specified"}
|
||||
: ${ASAN_BUILD?"ASAN_BUILD must be specified"}
|
||||
: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"}
|
||||
: ${CC?"CC must be specified"}
|
||||
: ${CXX?"CXX must be specified"}
|
||||
|
||||
case ${TARGET_ARCH} in
|
||||
x86_64)
|
||||
CXXFLAGS="${CXXFLAGS} -m64"
|
||||
CFLAGS="${CFLAGS} -m64"
|
||||
;;
|
||||
i686)
|
||||
CXXFLAGS="${CXXFLAGS} -m32"
|
||||
CFLAGS="${CFLAGS} -m32"
|
||||
;;
|
||||
*)
|
||||
echo "Unknown arch \"${TARGET_ARCH}\""
|
||||
exit 1
|
||||
esac
|
||||
|
||||
if [ "X${ASAN_BUILD}" = "X1" ]; then
|
||||
CXXFLAGS="${CXXFLAGS} -fsanitize=address -fno-omit-frame-pointer"
|
||||
CFLAGS="${CFLAGS} -fsanitize=address -fno-omit-frame-pointer"
|
||||
fi
|
||||
|
||||
if [ "X${UBSAN_BUILD}" = "X1" ]; then
|
||||
CXXFLAGS="${CXXFLAGS} -fsanitize=undefined"
|
||||
CFLAGS="${CFLAGS} -fsanitize=undefined"
|
||||
fi
|
||||
|
||||
# Report flags
|
||||
echo "CXXFLAGS: ${CXXFLAGS}"
|
||||
echo "CFLAGS: ${CFLAGS}"
|
||||
|
||||
# Report compiler
|
||||
echo "CC: ${CC}"
|
||||
${CC} --version
|
||||
echo "CXX: ${CXX}"
|
||||
${CXX} --version
|
||||
|
||||
# Export the values
|
||||
export CFLAGS
|
||||
export CXXFLAGS
|
||||
|
|
@ -1,20 +0,0 @@
|
|||
# This script is intended to be included by other
|
||||
# scripts and should not be executed directly
|
||||
|
||||
: ${Z3_CMAKE_GENERATOR?"Z3_CMAKE_GENERATOR must be specified"}
|
||||
: ${Z3_VERBOSE_BUILD_OUTPUT?"Z3_VERBOSE_BUILD_OUTPUT must be specified"}
|
||||
|
||||
GENERATOR_ARGS=('--')
|
||||
if [ "${Z3_CMAKE_GENERATOR}" = "Unix Makefiles" ]; then
|
||||
GENERATOR_ARGS+=("-j$(nproc)")
|
||||
if [ "X${Z3_VERBOSE_BUILD_OUTPUT}" = "X1" ]; then
|
||||
GENERATOR_ARGS+=("VERBOSE=1")
|
||||
fi
|
||||
elif [ "${Z3_CMAKE_GENERATOR}" = "Ninja" ]; then
|
||||
if [ "X${Z3_VERBOSE_BUILD_OUTPUT}" = "X1" ]; then
|
||||
GENERATOR_ARGS+=("-v")
|
||||
fi
|
||||
else
|
||||
echo "Unknown CMake generator \"${Z3_CMAKE_GENERATOR}\""
|
||||
exit 1
|
||||
fi
|
||||
|
|
@ -1,24 +0,0 @@
|
|||
#!/bin/bash
|
||||
|
||||
SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
|
||||
. ${SCRIPT_DIR}/run_quiet.sh
|
||||
|
||||
set -x
|
||||
set -e
|
||||
set -o pipefail
|
||||
|
||||
: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"}
|
||||
: ${BUILD_DOCS?"BUILD_DOCS must be specified"}
|
||||
|
||||
# Set CMake generator args
|
||||
source ${SCRIPT_DIR}/set_generator_args.sh
|
||||
|
||||
cd "${Z3_BUILD_DIR}"
|
||||
|
||||
# Generate documentation
|
||||
if [ "X${BUILD_DOCS}" = "X1" ]; then
|
||||
# TODO: Make quiet once we've fixed the build
|
||||
run_quiet cmake --build $(pwd) --target api_docs "${GENERATOR_ARGS[@]}"
|
||||
fi
|
||||
|
||||
# TODO: Test or perhaps deploy the built docs?
|
||||
|
|
@ -1,125 +0,0 @@
|
|||
#!/bin/bash
|
||||
|
||||
# This script tests Z3
|
||||
|
||||
SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
|
||||
. ${SCRIPT_DIR}/run_quiet.sh
|
||||
|
||||
set -x
|
||||
set -e
|
||||
set -o pipefail
|
||||
: ${Z3_SRC_DIR?"Z3_SRC_DIR must be specified"}
|
||||
: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"}
|
||||
: ${PYTHON_BINDINGS?"PYTHON_BINDINGS must be specified"}
|
||||
: ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"}
|
||||
: ${DOTNET_BINDINGS?"DOTNET_BINDINGS must be specified"}
|
||||
: ${JAVA_BINDINGS?"JAVA_BINDINGS must be specified"}
|
||||
: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"}
|
||||
: ${RUN_API_EXAMPLES?"RUN_API_EXAMPLES must be specified"}
|
||||
|
||||
if [ "X${RUN_API_EXAMPLES}" = "X0" ]; then
|
||||
echo "Skipping run of API examples"
|
||||
exit 0
|
||||
fi
|
||||
|
||||
# Set compiler flags
|
||||
source ${SCRIPT_DIR}/set_compiler_flags.sh
|
||||
|
||||
# Set CMake generator args
|
||||
source ${SCRIPT_DIR}/set_generator_args.sh
|
||||
|
||||
# Sanitizer environment variables
|
||||
source ${SCRIPT_DIR}/sanitizer_env.sh
|
||||
|
||||
cd "${Z3_BUILD_DIR}"
|
||||
|
||||
# Build and run C example
|
||||
cmake --build $(pwd) --target c_example "${GENERATOR_ARGS[@]}"
|
||||
run_quiet examples/c_example_build_dir/c_example
|
||||
|
||||
# Build and run C++ example
|
||||
cmake --build $(pwd) --target cpp_example "${GENERATOR_ARGS[@]}"
|
||||
run_quiet examples/cpp_example_build_dir/cpp_example
|
||||
|
||||
# Build and run tptp5 example
|
||||
cmake --build $(pwd) --target z3_tptp5 "${GENERATOR_ARGS[@]}"
|
||||
# FIXME: Do something more useful with example
|
||||
run_quiet examples/tptp_build_dir/z3_tptp5 -help
|
||||
|
||||
# Build an run c_maxsat_example
|
||||
cmake --build $(pwd) --target c_maxsat_example "${GENERATOR_ARGS[@]}"
|
||||
# FIXME: It is known that the maxsat example leaks memory and the
|
||||
# the Z3 developers have stated this is "wontfix".
|
||||
# See https://github.com/Z3Prover/z3/issues/1299
|
||||
run_no_lsan \
|
||||
run_quiet \
|
||||
examples/c_maxsat_example_build_dir/c_maxsat_example \
|
||||
${Z3_SRC_DIR}/examples/maxsat/ex.smt
|
||||
|
||||
if [ "X${UBSAN_BUILD}" = "X1" ]; then
|
||||
# FIXME: We really need libz3 to link against a shared UBSan runtime.
|
||||
# Right now we link against the static runtime which breaks all the
|
||||
# non-native language bindings.
|
||||
echo "FIXME: Can't run other examples when building with UBSan"
|
||||
exit 0
|
||||
fi
|
||||
|
||||
|
||||
if [ "X${PYTHON_BINDINGS}" = "X1" ]; then
|
||||
# Run python examples
|
||||
# `all_interval_series.py` produces a lot of output so just throw
|
||||
# away output.
|
||||
# TODO: This example is slow should we remove it from testing?
|
||||
if [ "X${ASAN_BUILD}" = "X1" -a "X${Z3_BUILD_TYPE}" = "XDebug" ]; then
|
||||
# Too slow when doing ASan Debug build
|
||||
echo "Skipping all_interval_series.py under ASan Debug build"
|
||||
else
|
||||
run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/all_interval_series.py
|
||||
fi
|
||||
run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/complex.py
|
||||
run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/example.py
|
||||
# FIXME: `hamiltonian.py` example is disabled because its too slow.
|
||||
#${PYTHON_EXECUTABLE} python/hamiltonian.py
|
||||
run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/marco.py
|
||||
run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/mss.py
|
||||
run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/socrates.py
|
||||
run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/visitor.py
|
||||
run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/z3test.py
|
||||
fi
|
||||
|
||||
if [ "X${DOTNET_BINDINGS}" = "X1" ]; then
|
||||
# Run .NET example
|
||||
if [ "X${ASAN_BUILD}" = "X1" ]; then
|
||||
# The dotnet test get stuck on ASAN
|
||||
# so don't run it for now.
|
||||
echo "Skipping .NET example under ASan build"
|
||||
else
|
||||
run_quiet run_non_native_binding dotnet ${Z3_BUILD_DIR}/dotnet/netcoreapp2.0/dotnet.dll
|
||||
fi
|
||||
fi
|
||||
|
||||
if [ "X${JAVA_BINDINGS}" = "X1" ]; then
|
||||
# Build Java example
|
||||
# FIXME: Move compilation step into CMake target
|
||||
mkdir -p examples/java
|
||||
cp ${Z3_SRC_DIR}/examples/java/JavaExample.java examples/java/
|
||||
javac examples/java/JavaExample.java -classpath com.microsoft.z3.jar
|
||||
# Run Java example
|
||||
if [ "$(uname)" = "Darwin" ]; then
|
||||
# macOS
|
||||
export DYLD_LIBRARY_PATH=$(pwd):${DYLD_LIBRARY_PATH}
|
||||
else
|
||||
# Assume Linux for now
|
||||
export LD_LIBRARY_PATH=$(pwd):${LD_LIBRARY_PATH}
|
||||
fi
|
||||
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
|
||||
|
||||
|
|
@ -1,24 +0,0 @@
|
|||
#!/bin/bash
|
||||
|
||||
SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
|
||||
|
||||
set -x
|
||||
set -e
|
||||
set -o pipefail
|
||||
|
||||
: ${TEST_INSTALL?"TEST_INSTALL must be specified"}
|
||||
: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"}
|
||||
|
||||
if [ "X${TEST_INSTALL}" != "X1" ]; then
|
||||
echo "Skipping install"
|
||||
exit 0
|
||||
fi
|
||||
|
||||
# Set CMake generator args
|
||||
source ${SCRIPT_DIR}/set_generator_args.sh
|
||||
|
||||
cd "${Z3_BUILD_DIR}"
|
||||
|
||||
sudo cmake --build $(pwd) --target install "${GENERATOR_ARGS[@]}"
|
||||
|
||||
# TODO: Test the installed version in some way
|
||||
|
|
@ -1,70 +0,0 @@
|
|||
#!/bin/bash
|
||||
|
||||
set -x
|
||||
set -e
|
||||
set -o pipefail
|
||||
|
||||
: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"}
|
||||
: ${Z3_BUILD_TYPE?"Z3_BUILD_TYPE must be specified"}
|
||||
: ${RUN_SYSTEM_TESTS?"RUN_SYSTEM_TESTS must be speicifed"}
|
||||
: ${PYTHON_BINDINGS?"PYTHON_BINDINGS must be specified"}
|
||||
: ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"}
|
||||
: ${Z3_SYSTEM_TEST_DIR?"Z3_SYSTEM_TEST_DIR must be specified"}
|
||||
: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"}
|
||||
|
||||
if [ "X${RUN_SYSTEM_TESTS}" != "X1" ]; then
|
||||
echo "Skipping system tests"
|
||||
exit 0
|
||||
fi
|
||||
|
||||
# Sanitizer environment variables
|
||||
SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
|
||||
source ${SCRIPT_DIR}/sanitizer_env.sh
|
||||
|
||||
Z3_EXE="${Z3_BUILD_DIR}/z3"
|
||||
Z3_LIB_DIR="${Z3_BUILD_DIR}"
|
||||
|
||||
# Set value if not already defined externally
|
||||
Z3_SYSTEM_TEST_GIT_URL="${Z3_GIT_URL:-https://github.com/Z3Prover/z3test.git}"
|
||||
|
||||
# Clone repo to destination
|
||||
mkdir -p "${Z3_SYSTEM_TEST_DIR}"
|
||||
git clone "${Z3_SYSTEM_TEST_GIT_URL}" "${Z3_SYSTEM_TEST_DIR}"
|
||||
cd "${Z3_SYSTEM_TEST_DIR}"
|
||||
|
||||
if [ -n "${Z3_SYSTEM_TEST_GIT_REVISION}" ]; then
|
||||
# If a particular revision is requested then check it out.
|
||||
# This is useful for reproducible builds
|
||||
git checkout "${Z3_SYSTEM_TEST_GIT_REVISION}"
|
||||
fi
|
||||
|
||||
###############################################################################
|
||||
# Run system tests
|
||||
###############################################################################
|
||||
|
||||
# SMTLIBv2 tests
|
||||
${PYTHON_EXECUTABLE} scripts/test_benchmarks.py "${Z3_EXE}" regressions/smt2
|
||||
|
||||
${PYTHON_EXECUTABLE} scripts/test_benchmarks.py "${Z3_EXE}" regressions/smt2-extra
|
||||
|
||||
if [ "X${Z3_BUILD_TYPE}" = "XDebug" ]; then
|
||||
${PYTHON_EXECUTABLE} scripts/test_benchmarks.py "${Z3_EXE}" regressions/smt2-debug
|
||||
fi
|
||||
|
||||
if [ "X${PYTHON_BINDINGS}" = "X1" ]; then
|
||||
# Run python binding tests
|
||||
if [ "X${UBSAN_BUILD}" = "X1" ]; then
|
||||
# FIXME: We need to build libz3 with a shared UBSan runtime for the bindings
|
||||
# to work.
|
||||
echo "FIXME: Skipping python binding tests when building with UBSan"
|
||||
elif [ "X${ASAN_BUILD}" = "X1" ]; then
|
||||
# FIXME: The `test_pyscripts.py` doesn't propagate LD_PRELOAD
|
||||
# so under ASan the tests fail to run
|
||||
# to work.
|
||||
echo "FIXME: Skipping python binding tests when building with ASan"
|
||||
else
|
||||
run_non_native_binding ${PYTHON_EXECUTABLE} scripts/test_pyscripts.py "${Z3_LIB_DIR}" regressions/python/
|
||||
fi
|
||||
fi
|
||||
|
||||
# FIXME: Run `scripts/test_cs.py` once it has been modified to support mono
|
||||
|
|
@ -1,47 +0,0 @@
|
|||
#!/bin/bash
|
||||
|
||||
SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
|
||||
. ${SCRIPT_DIR}/run_quiet.sh
|
||||
|
||||
set -x
|
||||
set -e
|
||||
set -o pipefail
|
||||
|
||||
: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"}
|
||||
: ${RUN_UNIT_TESTS?"RUN_UNIT_TESTS must be specified"}
|
||||
|
||||
# Set CMake generator args
|
||||
source ${SCRIPT_DIR}/set_generator_args.sh
|
||||
|
||||
# Sanitizer environment variables
|
||||
source ${SCRIPT_DIR}/sanitizer_env.sh
|
||||
|
||||
cd "${Z3_BUILD_DIR}"
|
||||
|
||||
function build_unit_tests() {
|
||||
# Build internal tests
|
||||
cmake --build $(pwd) --target test-z3 "${GENERATOR_ARGS[@]}"
|
||||
}
|
||||
|
||||
function run_unit_tests() {
|
||||
# Run all tests that don't require arguments
|
||||
run_quiet ./test-z3 /a
|
||||
}
|
||||
|
||||
case "${RUN_UNIT_TESTS}" in
|
||||
BUILD_AND_RUN)
|
||||
build_unit_tests
|
||||
run_unit_tests
|
||||
;;
|
||||
BUILD_ONLY)
|
||||
build_unit_tests
|
||||
;;
|
||||
SKIP)
|
||||
echo "RUN_UNIT_TESTS set to \"${RUN_UNIT_TESTS}\" so skipping build and run"
|
||||
exit 0
|
||||
;;
|
||||
*)
|
||||
echo "Error: RUN_UNIT_TESTS set to unhandled value \"${RUN_UNIT_TESTS}\""
|
||||
exit 1
|
||||
;;
|
||||
esac
|
||||
|
|
@ -1,18 +0,0 @@
|
|||
#!/bin/bash
|
||||
|
||||
SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
|
||||
|
||||
set -x
|
||||
set -e
|
||||
set -o pipefail
|
||||
|
||||
: ${TRAVIS_OS_NAME?"TRAVIS_OS_NAME should be set"}
|
||||
|
||||
if [ "${TRAVIS_OS_NAME}" = "osx" ]; then
|
||||
${SCRIPT_DIR}/travis_ci_osx_entry_point.sh
|
||||
elif [ "${TRAVIS_OS_NAME}" = "linux" ]; then
|
||||
${SCRIPT_DIR}/travis_ci_linux_entry_point.sh
|
||||
else
|
||||
echo "Unsupported OS \"${TRAVIS_OS_NAME}\""
|
||||
exit 1
|
||||
fi
|
||||
|
|
@ -1,220 +0,0 @@
|
|||
#!/bin/bash
|
||||
|
||||
SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
|
||||
|
||||
set -x
|
||||
set -e
|
||||
set -o pipefail
|
||||
|
||||
DOCKER_FILE_DIR="$(cd ${SCRIPT_DIR}/../Dockerfiles; echo $PWD)"
|
||||
|
||||
: ${LINUX_BASE?"LINUX_BASE must be specified"}
|
||||
|
||||
|
||||
# Sanity check. Current working directory should be repo root
|
||||
if [ ! -f "./README.md" ]; then
|
||||
echo "Current working directory should be repo root"
|
||||
exit 1
|
||||
fi
|
||||
|
||||
# Get defaults
|
||||
source "${SCRIPT_DIR}/ci_defaults.sh"
|
||||
|
||||
BUILD_OPTS=()
|
||||
# Pass Docker build arguments
|
||||
if [ -n "${Z3_BUILD_TYPE}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "Z3_BUILD_TYPE=${Z3_BUILD_TYPE}")
|
||||
fi
|
||||
|
||||
if [ -n "${Z3_CMAKE_GENERATOR}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "Z3_CMAKE_GENERATOR=${Z3_CMAKE_GENERATOR}")
|
||||
fi
|
||||
|
||||
if [ -n "${Z3_USE_LIBGMP}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "Z3_USE_LIBGMP=${Z3_USE_LIBGMP}")
|
||||
fi
|
||||
|
||||
if [ -n "${BUILD_DOCS}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "BUILD_DOCS=${BUILD_DOCS}")
|
||||
fi
|
||||
|
||||
if [ -n "${PYTHON_EXECUTABLE}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "PYTHON_EXECUTABLE=${PYTHON_EXECUTABLE}")
|
||||
fi
|
||||
|
||||
if [ -n "${PYTHON_BINDINGS}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "PYTHON_BINDINGS=${PYTHON_BINDINGS}")
|
||||
fi
|
||||
|
||||
if [ -n "${DOTNET_BINDINGS}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "DOTNET_BINDINGS=${DOTNET_BINDINGS}")
|
||||
fi
|
||||
|
||||
if [ -n "${JAVA_BINDINGS}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "JAVA_BINDINGS=${JAVA_BINDINGS}")
|
||||
fi
|
||||
|
||||
if [ -n "${USE_LTO}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "USE_LTO=${USE_LTO}")
|
||||
fi
|
||||
|
||||
if [ -n "${Z3_INSTALL_PREFIX}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "Z3_INSTALL_PREFIX=${Z3_INSTALL_PREFIX}")
|
||||
fi
|
||||
|
||||
# TravisCI reserves CC for itself so use a different name
|
||||
if [ -n "${C_COMPILER}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "CC=${C_COMPILER}")
|
||||
fi
|
||||
|
||||
# TravisCI reserves CXX for itself so use a different name
|
||||
if [ -n "${CXX_COMPILER}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "CXX=${CXX_COMPILER}")
|
||||
fi
|
||||
|
||||
if [ -n "${TARGET_ARCH}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "TARGET_ARCH=${TARGET_ARCH}")
|
||||
fi
|
||||
|
||||
if [ -n "${ASAN_BUILD}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "ASAN_BUILD=${ASAN_BUILD}")
|
||||
fi
|
||||
|
||||
if [ -n "${ASAN_DSO}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "ASAN_DSO=${ASAN_DSO}")
|
||||
fi
|
||||
|
||||
if [ -n "${SANITIZER_PRINT_SUPPRESSIONS}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "SANITIZER_PRINT_SUPPRESSIONS=${SANITIZER_PRINT_SUPPRESSIONS}")
|
||||
fi
|
||||
|
||||
if [ -n "${UBSAN_BUILD}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "UBSAN_BUILD=${UBSAN_BUILD}")
|
||||
fi
|
||||
|
||||
if [ -n "${TEST_INSTALL}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "TEST_INSTALL=${TEST_INSTALL}")
|
||||
fi
|
||||
|
||||
if [ -n "${RUN_API_EXAMPLES}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "RUN_API_EXAMPLES=${RUN_API_EXAMPLES}")
|
||||
fi
|
||||
|
||||
if [ -n "${RUN_SYSTEM_TESTS}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "RUN_SYSTEM_TESTS=${RUN_SYSTEM_TESTS}")
|
||||
fi
|
||||
|
||||
if [ -n "${Z3_SYSTEM_TEST_GIT_REVISION}" ]; then
|
||||
BUILD_OPTS+=( \
|
||||
"--build-arg" \
|
||||
"Z3_SYSTEM_TEST_GIT_REVISION=${Z3_SYSTEM_TEST_GIT_REVISION}" \
|
||||
)
|
||||
fi
|
||||
|
||||
if [ -n "${RUN_UNIT_TESTS}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "RUN_UNIT_TESTS=${RUN_UNIT_TESTS}")
|
||||
fi
|
||||
|
||||
if [ -n "${Z3_VERBOSE_BUILD_OUTPUT}" ]; then
|
||||
BUILD_OPTS+=( \
|
||||
"--build-arg" \
|
||||
"Z3_VERBOSE_BUILD_OUTPUT=${Z3_VERBOSE_BUILD_OUTPUT}" \
|
||||
)
|
||||
fi
|
||||
|
||||
if [ -n "${Z3_STATIC_BUILD}" ]; then
|
||||
BUILD_OPTS+=("--build-arg" "Z3_STATIC_BUILD=${Z3_STATIC_BUILD}")
|
||||
fi
|
||||
|
||||
if [ -n "${NO_SUPPRESS_OUTPUT}" ]; then
|
||||
BUILD_OPTS+=( \
|
||||
"--build-arg" \
|
||||
"NO_SUPPRESS_OUTPUT=${NO_SUPPRESS_OUTPUT}" \
|
||||
)
|
||||
fi
|
||||
|
||||
if [ -n "${Z3_WARNINGS_AS_ERRORS}" ]; then
|
||||
BUILD_OPTS+=( \
|
||||
"--build-arg" \
|
||||
"Z3_WARNINGS_AS_ERRORS=${Z3_WARNINGS_AS_ERRORS}" \
|
||||
)
|
||||
fi
|
||||
|
||||
case ${LINUX_BASE} in
|
||||
ubuntu_20.04)
|
||||
BASE_DOCKER_FILE="${DOCKER_FILE_DIR}/z3_base_ubuntu_20.04.Dockerfile"
|
||||
BASE_DOCKER_IMAGE_NAME="z3_base_ubuntu:20.04"
|
||||
;;
|
||||
*)
|
||||
echo "Unknown Linux base ${LINUX_BASE}"
|
||||
exit 1
|
||||
;;
|
||||
esac
|
||||
|
||||
# Initially assume that we need to build the base Docker image
|
||||
MUST_BUILD=1
|
||||
|
||||
# Travis CI persistent cache.
|
||||
#
|
||||
# This inspired by http://rundef.com/fast-travis-ci-docker-build .
|
||||
# The idea is to cache the built image for subsequent builds to
|
||||
# reduce build time.
|
||||
if [ -n "${DOCKER_TRAVIS_CI_CACHE_DIR}" ]; then
|
||||
CHECKSUM_FILE="${DOCKER_TRAVIS_CI_CACHE_DIR}/${BASE_DOCKER_IMAGE_NAME}.chksum"
|
||||
CACHED_DOCKER_IMAGE="${DOCKER_TRAVIS_CI_CACHE_DIR}/${BASE_DOCKER_IMAGE_NAME}.gz"
|
||||
if [ -f "${CACHED_DOCKER_IMAGE}" ]; then
|
||||
# There's a cached image to use. Check the checksums of the Dockerfile
|
||||
# match. If they don't that implies we need to build a fresh image.
|
||||
if [ -f "${CHECKSUM_FILE}" ]; then
|
||||
CURRENT_DOCKERFILE_CHECKSUM=$(sha256sum "${BASE_DOCKER_FILE}" | awk '{ print $1 }')
|
||||
CACHED_DOCKERFILE_CHECKSUM=$(cat "${CHECKSUM_FILE}")
|
||||
if [ "X${CURRENT_DOCKERFILE_CHECKSUM}" = "X${CACHED_DOCKERFILE_CHECKSUM}" ]; then
|
||||
# Load the cached image
|
||||
MUST_BUILD=0
|
||||
gunzip --stdout "${CACHED_DOCKER_IMAGE}" | docker load
|
||||
fi
|
||||
fi
|
||||
fi
|
||||
fi
|
||||
|
||||
if [ "${MUST_BUILD}" -eq 1 ]; then
|
||||
# The base image contains all the dependencies we want to build
|
||||
# Z3.
|
||||
docker build -t "${BASE_DOCKER_IMAGE_NAME}" - < "${BASE_DOCKER_FILE}"
|
||||
|
||||
if [ -n "${DOCKER_TRAVIS_CI_CACHE_DIR}" ]; then
|
||||
# Write image and checksum to cache
|
||||
docker save "${BASE_DOCKER_IMAGE_NAME}" | \
|
||||
gzip > "${CACHED_DOCKER_IMAGE}"
|
||||
sha256sum "${BASE_DOCKER_FILE}" | awk '{ print $1 }' > \
|
||||
"${CHECKSUM_FILE}"
|
||||
fi
|
||||
fi
|
||||
|
||||
|
||||
DOCKER_MAJOR_VERSION=$(docker info --format '{{.ServerVersion}}' | sed 's/^\([0-9]\+\)\.\([0-9]\+\).*$/\1/')
|
||||
DOCKER_MINOR_VERSION=$(docker info --format '{{.ServerVersion}}' | sed 's/^\([0-9]\+\)\.\([0-9]\+\).*$/\2/')
|
||||
DOCKER_BUILD_FILE="${DOCKER_FILE_DIR}/z3_build.Dockerfile"
|
||||
|
||||
if [ "${DOCKER_MAJOR_VERSION}${DOCKER_MINOR_VERSION}" -lt 1705 ]; then
|
||||
# Workaround limitation in older Docker versions where the FROM
|
||||
# command cannot be parameterized with an ARG.
|
||||
sed \
|
||||
-e '/^ARG DOCKER_IMAGE_BASE/d' \
|
||||
-e 's/${DOCKER_IMAGE_BASE}/'"${BASE_DOCKER_IMAGE_NAME}/" \
|
||||
"${DOCKER_BUILD_FILE}" > "${DOCKER_BUILD_FILE}.patched"
|
||||
DOCKER_BUILD_FILE="${DOCKER_BUILD_FILE}.patched"
|
||||
else
|
||||
# This feature landed in Docker 17.05
|
||||
# See https://github.com/moby/moby/pull/31352
|
||||
BUILD_OPTS+=( \
|
||||
"--build-arg" \
|
||||
"DOCKER_IMAGE_BASE=${BASE_DOCKER_IMAGE_NAME}" \
|
||||
)
|
||||
fi
|
||||
|
||||
# Now build Z3 and test it using the created base image
|
||||
docker build \
|
||||
-f "${DOCKER_BUILD_FILE}" \
|
||||
"${BUILD_OPTS[@]}" \
|
||||
.
|
||||
|
|
@ -1,51 +0,0 @@
|
|||
#!/bin/bash
|
||||
|
||||
SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
|
||||
|
||||
set -x
|
||||
set -e
|
||||
set -o pipefail
|
||||
|
||||
# Get defaults
|
||||
source "${SCRIPT_DIR}/ci_defaults.sh"
|
||||
|
||||
if [ -z "${TRAVIS_BUILD_DIR}" ]; then
|
||||
echo "TRAVIS_BUILD_DIR must be set to root of Z3 repository"
|
||||
exit 1
|
||||
fi
|
||||
|
||||
if [ ! -d "${TRAVIS_BUILD_DIR}" ]; then
|
||||
echo "TRAVIS_BUILD_DIR must be a directory"
|
||||
exit 1
|
||||
fi
|
||||
|
||||
# These variables are specific to the macOS TravisCI
|
||||
# implementation and are not set in `ci_defaults.sh`.
|
||||
export PYTHON_EXECUTABLE="${PYTHON_EXECUTABLE:-$(which python)}"
|
||||
export Z3_SRC_DIR="${TRAVIS_BUILD_DIR}"
|
||||
export Z3_BUILD_DIR="${Z3_SRC_DIR}/build"
|
||||
export Z3_SYSTEM_TEST_DIR="${Z3_SRC_DIR}/z3_system_test"
|
||||
|
||||
# Overwrite whatever what set in TravisCI
|
||||
export CC="${C_COMPILER}"
|
||||
export CXX="${CXX_COMPILER}"
|
||||
|
||||
if [ "X${MACOS_SKIP_DEPS_UPDATE}" = "X1" ]; then
|
||||
# This is just for local testing to avoid updating
|
||||
echo "Skipping dependency update"
|
||||
else
|
||||
"${SCRIPT_DIR}/install_deps_osx.sh"
|
||||
fi
|
||||
|
||||
# Build Z3
|
||||
"${SCRIPT_DIR}/build_z3_cmake.sh"
|
||||
# Test building docs
|
||||
"${SCRIPT_DIR}/test_z3_docs.sh"
|
||||
# Test examples
|
||||
"${SCRIPT_DIR}/test_z3_examples_cmake.sh"
|
||||
# Run unit tests
|
||||
"${SCRIPT_DIR}/test_z3_unit_tests_cmake.sh"
|
||||
# Run system tests
|
||||
"${SCRIPT_DIR}/test_z3_system_tests.sh"
|
||||
# Test install
|
||||
"${SCRIPT_DIR}/test_z3_install_cmake.sh"
|
||||
|
|
@ -1,48 +0,0 @@
|
|||
#!/usr/bin/env python
|
||||
"""
|
||||
This script is an artifact of compromise that was
|
||||
made when the CMake build system was first introduced
|
||||
(see #461).
|
||||
|
||||
This script now does nothing. It remains only to not
|
||||
break out-of-tree scripts that build Z3 using CMake.
|
||||
|
||||
Eventually this script will be removed.
|
||||
"""
|
||||
import argparse
|
||||
import logging
|
||||
import os
|
||||
import pprint
|
||||
import shutil
|
||||
import sys
|
||||
|
||||
def main(args):
|
||||
logging.basicConfig(level=logging.INFO)
|
||||
parser = argparse.ArgumentParser(description=__doc__)
|
||||
parser.add_argument('mode',
|
||||
choices=['create', 'remove'],
|
||||
help='The mode to use')
|
||||
parser.add_argument("-l","--log-level",
|
||||
type=str,
|
||||
default="info",
|
||||
dest="log_level",
|
||||
choices=['debug','info','warning','error']
|
||||
)
|
||||
parser.add_argument("-H", "--hard-link",
|
||||
action='store_true',
|
||||
default=False,
|
||||
dest='hard_link',
|
||||
help='When using the create mode create hard links instead of copies'
|
||||
)
|
||||
pargs = parser.parse_args(args)
|
||||
|
||||
logLevel = getattr(logging, pargs.log_level.upper(),None)
|
||||
logging.basicConfig(level=logLevel)
|
||||
logging.warning('Use of this script is deprecated. The script will be removed in the future')
|
||||
logging.warning('Action "{}" ignored'.format(pargs.mode))
|
||||
if pargs.hard_link:
|
||||
logging.warning('Hard link option ignored')
|
||||
return 0
|
||||
|
||||
if __name__ == '__main__':
|
||||
sys.exit(main(sys.argv[1:]))
|
||||
|
|
@ -1,3 +0,0 @@
|
|||
# Maintainers
|
||||
|
||||
- Dan Liew (@delcypher)
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
add_executable(lp_tst lp_main.cpp lp.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:polynomial> $<TARGET_OBJECTS:nlsat> $<TARGET_OBJECTS:lp> )
|
||||
target_compile_definitions(lp_tst PRIVATE ${Z3_COMPONENT_CXX_DEFINES})
|
||||
target_compile_options(lp_tst PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
|
||||
target_include_directories(lp_tst PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS})
|
||||
target_link_libraries(lp_tst PRIVATE ${Z3_DEPENDENT_LIBS})
|
||||
z3_append_linker_flag_list_to_target(lp_tst ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
|
||||
|
|
@ -69,7 +69,7 @@ add_custom_target(api_docs ${ALWAYS_BUILD_DOCS_ARG}
|
|||
DEPENDS
|
||||
${DOC_EXTRA_DEPENDS}
|
||||
COMMENT "Generating documentation"
|
||||
${ADD_CUSTOM_TARGET_USES_TERMINAL_ARG}
|
||||
USES_TERMINAL
|
||||
)
|
||||
|
||||
# Remove generated documentation when running `clean` target.
|
||||
|
|
|
|||
|
|
@ -8,5 +8,5 @@
|
|||
|
||||
This website hosts the automatically generated documentation for the Z3 APIs.
|
||||
|
||||
- \ref @C_API@ @CPP_API@ @DOTNET_API@ @JAVA_API@ @PYTHON_API@ @OCAML_API@ @JS_API@
|
||||
@C_API@ @CPP_API@ @DOTNET_API@ @JAVA_API@ @PYTHON_API@ @OCAML_API@ @JS_API@
|
||||
*/
|
||||
|
|
|
|||
|
|
@ -2171,7 +2171,6 @@ INCLUDE_FILE_PATTERNS =
|
|||
# This tag requires that the tag ENABLE_PREPROCESSING is set to YES.
|
||||
|
||||
PREDEFINED = Z3_ast_opt:=Z3_ast \
|
||||
Z3_bool_opt:=Z3_bool \
|
||||
Z3_func_interp_opt:=Z3_func_interp \
|
||||
Z3_model_opt:=Z3_model \
|
||||
__out_opt:=__out
|
||||
|
|
|
|||
|
|
@ -816,7 +816,7 @@ INCLUDE_FILE_PATTERNS =
|
|||
# undefined via #undef or recursively expanded use the := operator
|
||||
# instead of the = operator.
|
||||
|
||||
PREDEFINED =Z3_ast_opt:=Z3_ast Z3_bool_opt:=Z3_bool Z3_func_interp_opt:=Z3_func_interp Z3_model_opt:=Z3_model __out_opt:=__out
|
||||
PREDEFINED =Z3_ast_opt:=Z3_ast Z3_func_interp_opt:=Z3_func_interp Z3_model_opt:=Z3_model __out_opt:=__out
|
||||
|
||||
# If the MACRO_EXPANSION and EXPAND_ONLY_PREDEF tags are set to YES then
|
||||
# this tag can be used to specify a list of macro names that should be expanded.
|
||||
|
|
@ -825,7 +825,7 @@ PREDEFINED =Z3_ast_opt:=Z3_ast Z3_bool_opt:=Z3_bool Z3_func_interp_o
|
|||
|
||||
EXPAND_AS_DEFINED =
|
||||
|
||||
# Z3_ast_opt Z3_bool_opt Z3_func_interp_opt Z3_model_opt __out_opt
|
||||
# Z3_ast_opt Z3_func_interp_opt Z3_model_opt __out_opt
|
||||
|
||||
# If the SKIP_FUNCTION_MACROS tag is set to YES (the default) then
|
||||
# doxygen's preprocessor will remove all function-like macros that are alone
|
||||
|
|
|
|||
|
|
@ -1,11 +1,4 @@
|
|||
include(ExternalProject)
|
||||
# Unfortunately `BUILD_ALWAYS` only seems to be supported with the version of ExternalProject
|
||||
# that shipped with CMake >= 3.1.
|
||||
if (("${CMAKE_VERSION}" VERSION_EQUAL "3.1") OR ("${CMAKE_VERSION}" VERSION_GREATER "3.1"))
|
||||
set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG BUILD_ALWAYS 1)
|
||||
else()
|
||||
set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG "")
|
||||
endif()
|
||||
|
||||
option(Z3_C_EXAMPLES_FORCE_CXX_LINKER
|
||||
"Force C++ linker when building C example projects" OFF)
|
||||
|
|
@ -43,7 +36,7 @@ ExternalProject_Add(c_example
|
|||
"${EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG}"
|
||||
"${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}"
|
||||
# Build step
|
||||
${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
|
||||
BUILD_ALWAYS ON
|
||||
BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_example_build_dir"
|
||||
# Install Step
|
||||
INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command
|
||||
|
|
@ -62,7 +55,7 @@ ExternalProject_Add(c_maxsat_example
|
|||
"${EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG}"
|
||||
"${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}"
|
||||
# Build step
|
||||
${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
|
||||
BUILD_ALWAYS ON
|
||||
BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_maxsat_example_build_dir"
|
||||
# Install Step
|
||||
INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command
|
||||
|
|
@ -81,7 +74,7 @@ ExternalProject_Add(cpp_example
|
|||
"-DZ3_DIR=${PROJECT_BINARY_DIR}"
|
||||
"${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}"
|
||||
# Build step
|
||||
${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
|
||||
BUILD_ALWAYS ON
|
||||
BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/cpp_example_build_dir"
|
||||
# Install Step
|
||||
INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command
|
||||
|
|
@ -99,7 +92,7 @@ ExternalProject_Add(z3_tptp5
|
|||
"-DZ3_DIR=${PROJECT_BINARY_DIR}"
|
||||
"${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}"
|
||||
# Build step
|
||||
${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
|
||||
BUILD_ALWAYS ON
|
||||
BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/tptp_build_dir"
|
||||
# Install Step
|
||||
INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command
|
||||
|
|
@ -117,7 +110,7 @@ ExternalProject_Add(userPropagator
|
|||
"-DZ3_DIR=${PROJECT_BINARY_DIR}"
|
||||
"${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}"
|
||||
# Build step
|
||||
${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
|
||||
BUILD_ALWAYS ON
|
||||
BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/userPropagator_build_dir"
|
||||
# Install Step
|
||||
INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command
|
||||
|
|
|
|||
|
|
@ -5,6 +5,7 @@ Copyright (c) 2015 Microsoft Corporation
|
|||
--*/
|
||||
|
||||
#include <iostream>
|
||||
#include <sstream>
|
||||
#include<vector>
|
||||
#include"z3++.h"
|
||||
|
||||
|
|
@ -956,6 +957,55 @@ void tuple_example() {
|
|||
std::cout << pair2 << "\n";
|
||||
}
|
||||
|
||||
void datatype_example() {
|
||||
std::cout << "datatype example\n";
|
||||
context ctx;
|
||||
constructors cs(ctx);
|
||||
symbol ilist = ctx.str_symbol("ilist");
|
||||
symbol accs[2] = { ctx.str_symbol("hd"), ctx.str_symbol("tl") };
|
||||
sort sorts[2] = { ctx.int_sort(), ctx.datatype_sort(ilist) };
|
||||
cs.add(ctx.str_symbol("nil"), ctx.str_symbol("is-nil"), 0, nullptr, nullptr);
|
||||
cs.add(ctx.str_symbol("cons"), ctx.str_symbol("is-cons"), 2, accs, sorts);
|
||||
sort ls = ctx.datatype(ilist, cs);
|
||||
std::cout << ls << "\n";
|
||||
func_decl nil(ctx), is_nil(ctx);
|
||||
func_decl_vector nil_acc(ctx);
|
||||
cs.query(0, nil, is_nil, nil_acc);
|
||||
func_decl cons(ctx), is_cons(ctx);
|
||||
func_decl_vector cons_acc(ctx);
|
||||
cs.query(1, cons, is_cons, cons_acc);
|
||||
std::cout << nil << " " << is_nil << " " << nil_acc << "\n";
|
||||
std::cout << cons << " " << is_cons << " " << cons_acc << "\n";
|
||||
|
||||
symbol tree = ctx.str_symbol("tree");
|
||||
symbol tlist = ctx.str_symbol("tree_list");
|
||||
symbol accs1[2] = { ctx.str_symbol("left"), ctx.str_symbol("right") };
|
||||
symbol accs2[2] = { ctx.str_symbol("hd"), ctx.str_symbol("tail") };
|
||||
sort sorts1[2] = { ctx.datatype_sort(tlist), ctx.datatype_sort(tlist) };
|
||||
sort sorts2[2] = { ctx.int_sort(), ctx.datatype_sort(tree) };
|
||||
constructors cs1(ctx), cs2(ctx);
|
||||
cs1.add(ctx.str_symbol("tnil"), ctx.str_symbol("is-tnil"), 0, nullptr, nullptr);
|
||||
cs1.add(ctx.str_symbol("tnode"), ctx.str_symbol("is-tnode"), 2, accs1, sorts1);
|
||||
constructor_list cl1(cs1);
|
||||
cs2.add(ctx.str_symbol("lnil"), ctx.str_symbol("is-lnil"), 0, nullptr, nullptr);
|
||||
cs2.add(ctx.str_symbol("lcons"), ctx.str_symbol("is-lcons"), 2, accs2, sorts2);
|
||||
constructor_list cl2(cs2);
|
||||
symbol names[2] = { tree, tlist };
|
||||
constructor_list* cl[2] = { &cl1, &cl2 };
|
||||
sort_vector dsorts = ctx.datatypes(2, names, cl);
|
||||
std::cout << dsorts << "\n";
|
||||
cs1.query(0, nil, is_nil, nil_acc);
|
||||
cs1.query(1, cons, is_cons, cons_acc);
|
||||
std::cout << nil << " " << is_nil << " " << nil_acc << "\n";
|
||||
std::cout << cons << " " << is_cons << " " << cons_acc << "\n";
|
||||
|
||||
cs2.query(0, nil, is_nil, nil_acc);
|
||||
cs2.query(1, cons, is_cons, cons_acc);
|
||||
std::cout << nil << " " << is_nil << " " << nil_acc << "\n";
|
||||
std::cout << cons << " " << is_cons << " " << cons_acc << "\n";
|
||||
|
||||
}
|
||||
|
||||
void expr_vector_example() {
|
||||
std::cout << "expr_vector example\n";
|
||||
context c;
|
||||
|
|
@ -1343,6 +1393,7 @@ int main() {
|
|||
incremental_example3(); std::cout << "\n";
|
||||
enum_sort_example(); std::cout << "\n";
|
||||
tuple_example(); std::cout << "\n";
|
||||
datatype_example(); std::cout << "\n";
|
||||
expr_vector_example(); std::cout << "\n";
|
||||
exists_expr_vector_example(); std::cout << "\n";
|
||||
substitute_example(); std::cout << "\n";
|
||||
|
|
|
|||
83
examples/python/simplify_formula.py
Normal file
83
examples/python/simplify_formula.py
Normal file
|
|
@ -0,0 +1,83 @@
|
|||
from z3 import *
|
||||
|
||||
def is_atom(t):
|
||||
if not is_bool(t):
|
||||
return False
|
||||
if not is_app(t):
|
||||
return False
|
||||
k = t.decl().kind()
|
||||
if k == Z3_OP_AND or k == Z3_OP_OR or k == Z3_OP_IMPLIES:
|
||||
return False
|
||||
if k == Z3_OP_EQ and t.arg(0).is_bool():
|
||||
return False
|
||||
if k == Z3_OP_TRUE or k == Z3_OP_FALSE or k == Z3_OP_XOR or k == Z3_OP_NOT:
|
||||
return False
|
||||
return True
|
||||
|
||||
def atoms(fml):
|
||||
visited = set([])
|
||||
atms = set([])
|
||||
def atoms_rec(t, visited, atms):
|
||||
if t in visited:
|
||||
return
|
||||
visited |= { t }
|
||||
if is_atom(t):
|
||||
atms |= { t }
|
||||
for s in t.children():
|
||||
atoms_rec(s, visited, atms)
|
||||
atoms_rec(fml, visited, atms)
|
||||
return atms
|
||||
|
||||
def atom2literal(m, a):
|
||||
if is_true(m.eval(a)):
|
||||
return a
|
||||
return Not(a)
|
||||
|
||||
# Extract subset of atoms used to satisfy the negation
|
||||
# of a formula.
|
||||
# snot is a solver for Not(fml)
|
||||
# s is a solver for fml
|
||||
# m is a model for Not(fml)
|
||||
# evaluate each atom in fml using m and create
|
||||
# literals corresponding to the sign of the evaluation.
|
||||
# If the model evaluates atoms to false, the literal is
|
||||
# negated.
|
||||
#
|
||||
#
|
||||
def implicant(atoms, s, snot):
|
||||
m = snot.model()
|
||||
lits = [atom2literal(m, a) for a in atoms]
|
||||
is_sat = s.check(lits)
|
||||
assert is_sat == unsat
|
||||
core = s.unsat_core()
|
||||
return Or([mk_not(c) for c in core])
|
||||
|
||||
#
|
||||
# Extract a CNF representation of fml
|
||||
# The procedure uses two solvers
|
||||
# Enumerate models for Not(fml)
|
||||
# Use the enumerated model to identify literals
|
||||
# that imply Not(fml)
|
||||
# The CNF of fml is a conjunction of the
|
||||
# negation of these literals.
|
||||
#
|
||||
|
||||
def to_cnf(fml):
|
||||
atms = atoms(fml)
|
||||
s = Solver()
|
||||
snot = Solver()
|
||||
snot.add(Not(fml))
|
||||
s.add(fml)
|
||||
|
||||
while sat == snot.check():
|
||||
clause = implicant(atms, s, snot)
|
||||
yield clause
|
||||
snot.add(clause)
|
||||
|
||||
|
||||
a, b, c, = Bools('a b c')
|
||||
fml = Or(And(a, b), And(Not(a), c))
|
||||
|
||||
for clause in to_cnf(fml):
|
||||
print(clause)
|
||||
|
||||
|
|
@ -15,6 +15,7 @@ Copyright (c) 2015 Microsoft Corporation
|
|||
#include <iostream>
|
||||
#include <fstream>
|
||||
#include <limits>
|
||||
#include <sstream>
|
||||
#include <string.h>
|
||||
#include <cstdlib>
|
||||
#include "z3++.h"
|
||||
|
|
|
|||
|
|
@ -15,9 +15,9 @@ find_package(Z3
|
|||
)
|
||||
|
||||
################################################################################
|
||||
# Z3 C++ API bindings require C++11
|
||||
# Z3 C++ API bindings require C++11, but this code needs later.
|
||||
################################################################################
|
||||
set(CMAKE_CXX_STANDARD 11)
|
||||
set(CMAKE_CXX_STANDARD 20)
|
||||
set(CMAKE_CXX_STANDARD_REQUIRED ON)
|
||||
|
||||
message(STATUS "Z3_FOUND: ${Z3_FOUND}")
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@
|
|||
from mk_util import *
|
||||
|
||||
def init_version():
|
||||
set_version(4, 9, 2, 0)
|
||||
set_version(4, 11, 0, 0)
|
||||
|
||||
# Z3 Project definition
|
||||
def init_project_def():
|
||||
|
|
@ -38,7 +38,7 @@ def init_project_def():
|
|||
add_lib('substitution', ['ast', 'rewriter'], 'ast/substitution')
|
||||
add_lib('parser_util', ['ast'], 'parsers/util')
|
||||
add_lib('proofs', ['rewriter', 'util'], 'ast/proofs')
|
||||
add_lib('solver', ['model', 'tactic', 'proofs'])
|
||||
add_lib('solver', ['params', 'model', 'tactic', 'proofs'])
|
||||
add_lib('cmd_context', ['solver', 'rewriter', 'params'])
|
||||
add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2')
|
||||
add_lib('pattern', ['normal_forms', 'smt2parser', 'rewriter'], 'ast/pattern')
|
||||
|
|
|
|||
|
|
@ -66,7 +66,7 @@ def display_help():
|
|||
|
||||
# Parse configuration option for mk_make script
|
||||
def parse_options():
|
||||
global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, OS_NAME
|
||||
global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, PYTHON_ENABLED, OS_NAME
|
||||
path = BUILD_DIR
|
||||
options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=',
|
||||
'help',
|
||||
|
|
|
|||
|
|
@ -1830,8 +1830,11 @@ class JavaDLLComponent(Component):
|
|||
if IS_WINDOWS: # On Windows, CL creates a .lib file to link against.
|
||||
out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(LIB_EXT)\n' %
|
||||
os.path.join('api', 'java', 'Native'))
|
||||
elif IS_OSX and IS_ARCH_ARM64:
|
||||
out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) -arch arm64 %s$(OBJ_EXT) libz3$(SO_EXT)\n' %
|
||||
os.path.join('api', 'java', 'Native'))
|
||||
else:
|
||||
out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) $(SLINK_EXTRA_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' %
|
||||
out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' %
|
||||
os.path.join('api', 'java', 'Native'))
|
||||
out.write('%s.jar: libz3java$(SO_EXT) ' % self.package_name)
|
||||
deps = ''
|
||||
|
|
@ -2591,46 +2594,30 @@ def mk_config():
|
|||
SO_EXT = '.dylib'
|
||||
SLIBFLAGS = '-dynamiclib'
|
||||
elif sysname == 'Linux':
|
||||
CXXFLAGS = '%s -D_LINUX_' % CXXFLAGS
|
||||
OS_DEFINES = '-D_LINUX_'
|
||||
SO_EXT = '.so'
|
||||
SLIBFLAGS = '-shared'
|
||||
SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so' % SLIBEXTRAFLAGS
|
||||
elif sysname == 'GNU':
|
||||
CXXFLAGS = '%s -D_HURD_' % CXXFLAGS
|
||||
OS_DEFINES = '-D_HURD_'
|
||||
SO_EXT = '.so'
|
||||
SLIBFLAGS = '-shared'
|
||||
elif sysname == 'FreeBSD':
|
||||
CXXFLAGS = '%s -D_FREEBSD_' % CXXFLAGS
|
||||
OS_DEFINES = '-D_FREEBSD_'
|
||||
SO_EXT = '.so'
|
||||
SLIBFLAGS = '-shared'
|
||||
SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so' % SLIBEXTRAFLAGS
|
||||
elif sysname == 'NetBSD':
|
||||
CXXFLAGS = '%s -D_NETBSD_' % CXXFLAGS
|
||||
OS_DEFINES = '-D_NETBSD_'
|
||||
SO_EXT = '.so'
|
||||
SLIBFLAGS = '-shared'
|
||||
elif sysname == 'OpenBSD':
|
||||
CXXFLAGS = '%s -D_OPENBSD_' % CXXFLAGS
|
||||
OS_DEFINES = '-D_OPENBSD_'
|
||||
SO_EXT = '.so'
|
||||
SLIBFLAGS = '-shared'
|
||||
elif sysname == 'SunOS':
|
||||
CXXFLAGS = '%s -D_SUNOS_' % CXXFLAGS
|
||||
OS_DEFINES = '-D_SUNOS_'
|
||||
SO_EXT = '.so'
|
||||
SLIBFLAGS = '-shared'
|
||||
SLIBEXTRAFLAGS = '%s -mimpure-text' % SLIBEXTRAFLAGS
|
||||
elif sysname.startswith('CYGWIN'):
|
||||
CXXFLAGS = '%s -D_CYGWIN' % CXXFLAGS
|
||||
OS_DEFINES = '-D_CYGWIN'
|
||||
SO_EXT = '.dll'
|
||||
SLIBFLAGS = '-shared'
|
||||
elif sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'):
|
||||
CXXFLAGS = '%s -D_MINGW' % CXXFLAGS
|
||||
OS_DEFINES = '-D_MINGW'
|
||||
SO_EXT = '.dll'
|
||||
SLIBFLAGS = '-shared'
|
||||
EXE_EXT = '.exe'
|
||||
|
|
@ -2640,8 +2627,6 @@ def mk_config():
|
|||
if is64():
|
||||
if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'):
|
||||
CXXFLAGS = '%s -fPIC' % CXXFLAGS
|
||||
if sysname == 'Linux' or sysname == 'FreeBSD':
|
||||
CPPFLAGS = '%s -D_USE_THREAD_LOCAL' % CPPFLAGS
|
||||
elif not LINUX_X64:
|
||||
CXXFLAGS = '%s -m32' % CXXFLAGS
|
||||
LDFLAGS = '%s -m32' % LDFLAGS
|
||||
|
|
|
|||
|
|
@ -1,8 +1,8 @@
|
|||
variables:
|
||||
|
||||
Major: '4'
|
||||
Minor: '9'
|
||||
Patch: '2'
|
||||
Minor: '11'
|
||||
Patch: '0'
|
||||
NightlyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)-$(Build.DefinitionName)
|
||||
|
||||
stages:
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@
|
|||
trigger: none
|
||||
|
||||
variables:
|
||||
ReleaseVersion: '4.9.2'
|
||||
ReleaseVersion: '4.11.0'
|
||||
|
||||
stages:
|
||||
|
||||
|
|
@ -516,8 +516,9 @@ stages:
|
|||
inputs:
|
||||
command: push
|
||||
nuGetFeedType: External
|
||||
publishFeedCredentials: Z3Nuget
|
||||
publishFeedCredentials: $(NugetZ3)
|
||||
packagesToPush: $(Agent.TempDirectory)/*.nupkg
|
||||
|
||||
|
||||
# Enable on release:
|
||||
- job: PyPIPublish
|
||||
|
|
|
|||
|
|
@ -16,7 +16,6 @@ emit some of the files required for Z3's different
|
|||
language bindings.
|
||||
"""
|
||||
|
||||
import mk_exception
|
||||
import argparse
|
||||
import logging
|
||||
import re
|
||||
|
|
@ -1700,8 +1699,8 @@ def def_APIs(api_files):
|
|||
m = pat2.match(line)
|
||||
if m:
|
||||
eval(line)
|
||||
except Exception:
|
||||
raise mk_exec_header.MKException("Failed to process API definition: %s" % line)
|
||||
except Exception as e:
|
||||
error('ERROR: While processing: %s: %s\n' % (e, line))
|
||||
|
||||
def write_log_h_preamble(log_h):
|
||||
log_h.write('// Automatically generated file\n')
|
||||
|
|
@ -1854,6 +1853,7 @@ _lib.Z3_solver_propagate_final.restype = None
|
|||
_lib.Z3_solver_propagate_fixed.restype = None
|
||||
_lib.Z3_solver_propagate_eq.restype = None
|
||||
_lib.Z3_solver_propagate_diseq.restype = None
|
||||
_lib.Z3_solver_propagate_decide.restype = None
|
||||
|
||||
on_model_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p)
|
||||
_lib.Z3_optimize_register_model_eh.restype = None
|
||||
|
|
|
|||
|
|
@ -204,7 +204,7 @@ if (MSVC)
|
|||
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
|
||||
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
|
||||
COMMENT "Generating \"${dll_module_exports_file}\""
|
||||
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
|
||||
USES_TERMINAL
|
||||
VERBATIM
|
||||
)
|
||||
add_custom_target(libz3_extra_depends
|
||||
|
|
|
|||
|
|
@ -29,8 +29,6 @@ public:
|
|||
updt_params(p);
|
||||
}
|
||||
|
||||
~ackermannize_bv_tactic() override { }
|
||||
|
||||
char const* name() const override { return "ackermannize_bv"; }
|
||||
|
||||
void operator()(goal_ref const & g, goal_ref_buffer & result) override {
|
||||
|
|
|
|||
|
|
@ -40,8 +40,6 @@ public:
|
|||
fixed_model(false)
|
||||
{ }
|
||||
|
||||
~ackr_model_converter() override { }
|
||||
|
||||
void get_units(obj_map<expr, bool>& units) override { units.reset(); }
|
||||
|
||||
void operator()(model_ref & md) override {
|
||||
|
|
|
|||
|
|
@ -28,8 +28,6 @@ public:
|
|||
, model_constructor(lmc)
|
||||
{ }
|
||||
|
||||
~lackr_model_converter_lazy() override { }
|
||||
|
||||
void operator()(model_ref & md) override {
|
||||
SASSERT(md.get() == 0 || (!md->get_num_constants() && !md->get_num_functions()));
|
||||
SASSERT(model_constructor.get());
|
||||
|
|
|
|||
|
|
@ -26,10 +26,8 @@ add_custom_command(OUTPUT ${generated_files}
|
|||
DEPENDS "${PROJECT_SOURCE_DIR}/scripts/update_api.py"
|
||||
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
|
||||
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
|
||||
# FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency
|
||||
"${PROJECT_SOURCE_DIR}/scripts/mk_util.py"
|
||||
COMMENT "Generating ${generated_files}"
|
||||
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
|
||||
USES_TERMINAL
|
||||
VERBATIM
|
||||
)
|
||||
|
||||
|
|
|
|||
|
|
@ -344,7 +344,6 @@ extern "C" {
|
|||
scoped_anum_vector const & m_as;
|
||||
public:
|
||||
vector_var2anum(scoped_anum_vector & as):m_as(as) {}
|
||||
virtual ~vector_var2anum() {}
|
||||
algebraic_numbers::manager & m() const override { return m_as.m(); }
|
||||
bool contains(polynomial::var x) const override { return static_cast<unsigned>(x) < m_as.size(); }
|
||||
algebraic_numbers::anum const & operator()(polynomial::var x) const override { return m_as.get(x); }
|
||||
|
|
@ -422,7 +421,7 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_algebraic_get_poly(c, a);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_IS_ALGEBRAIC(a, 0);
|
||||
CHECK_IS_ALGEBRAIC(a, nullptr);
|
||||
algebraic_numbers::manager & _am = am(c);
|
||||
algebraic_numbers::anum const & av = get_irrational(c, a);
|
||||
scoped_mpz_vector coeffs(_am.qm());
|
||||
|
|
|
|||
|
|
@ -26,7 +26,6 @@ namespace api {
|
|||
struct Z3_ast_vector_ref : public api::object {
|
||||
ast_ref_vector m_ast_vector;
|
||||
Z3_ast_vector_ref(api::context& c, ast_manager & m): api::object(c), m_ast_vector(m) {}
|
||||
~Z3_ast_vector_ref() override {}
|
||||
};
|
||||
|
||||
inline Z3_ast_vector_ref * to_ast_vector(Z3_ast_vector v) { return reinterpret_cast<Z3_ast_vector_ref *>(v); }
|
||||
|
|
|
|||
|
|
@ -47,7 +47,7 @@ extern "C" {
|
|||
env_params::updt_params();
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value) {
|
||||
bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value) {
|
||||
memory::initialize(UINT_MAX);
|
||||
LOG_Z3_global_param_get(param_id, param_value);
|
||||
*param_value = nullptr;
|
||||
|
|
|
|||
|
|
@ -58,7 +58,7 @@ namespace api {
|
|||
solver_ref s;
|
||||
public:
|
||||
seq_expr_solver(ast_manager& m, params_ref const& p): m(m), p(p) {}
|
||||
lbool check_sat(expr* e) {
|
||||
lbool check_sat(expr* e) override {
|
||||
if (!s) {
|
||||
s = mk_smt_solver(m, p, symbol("ALL"));
|
||||
}
|
||||
|
|
|
|||
|
|
@ -52,7 +52,6 @@ namespace api {
|
|||
m_context(m, m_register_engine, p),
|
||||
m_trail(m) {}
|
||||
|
||||
~fixedpoint_context() override {}
|
||||
family_id get_family_id() const override { return const_cast<datalog::context&>(m_context).get_decl_util().get_family_id(); }
|
||||
void set_state(void* state) {
|
||||
SASSERT(!m_state);
|
||||
|
|
|
|||
|
|
@ -23,7 +23,6 @@ Revision History:
|
|||
struct Z3_goal_ref : public api::object {
|
||||
goal_ref m_goal;
|
||||
Z3_goal_ref(api::context& c) : api::object(c) {}
|
||||
~Z3_goal_ref() override {}
|
||||
};
|
||||
|
||||
inline Z3_goal_ref * to_goal(Z3_goal g) { return reinterpret_cast<Z3_goal_ref *>(g); }
|
||||
|
|
|
|||
|
|
@ -23,7 +23,6 @@ Revision History:
|
|||
struct Z3_model_ref : public api::object {
|
||||
model_ref m_model;
|
||||
Z3_model_ref(api::context& c): api::object(c) {}
|
||||
~Z3_model_ref() override {}
|
||||
};
|
||||
|
||||
inline Z3_model_ref * to_model(Z3_model s) { return reinterpret_cast<Z3_model_ref *>(s); }
|
||||
|
|
@ -34,7 +33,6 @@ struct Z3_func_interp_ref : public api::object {
|
|||
model_ref m_model; // must have it to prevent reference to m_func_interp to be killed.
|
||||
func_interp * m_func_interp;
|
||||
Z3_func_interp_ref(api::context& c, model * m): api::object(c), m_model(m), m_func_interp(nullptr) {}
|
||||
~Z3_func_interp_ref() override {}
|
||||
};
|
||||
|
||||
inline Z3_func_interp_ref * to_func_interp(Z3_func_interp s) { return reinterpret_cast<Z3_func_interp_ref *>(s); }
|
||||
|
|
@ -46,7 +44,6 @@ struct Z3_func_entry_ref : public api::object {
|
|||
func_interp * m_func_interp;
|
||||
func_entry const * m_func_entry;
|
||||
Z3_func_entry_ref(api::context& c, model * m):api::object(c), m_model(m), m_func_interp(nullptr), m_func_entry(nullptr) {}
|
||||
~Z3_func_entry_ref() override {}
|
||||
};
|
||||
|
||||
inline Z3_func_entry_ref * to_func_entry(Z3_func_entry s) { return reinterpret_cast<Z3_func_entry_ref *>(s); }
|
||||
|
|
|
|||
|
|
@ -459,4 +459,33 @@ extern "C" {
|
|||
Z3_CATCH_RETURN(nullptr);
|
||||
}
|
||||
|
||||
#if 0
|
||||
Z3_ast Z3_API Z3_mk_mpz_numeral(Z3_context c, bool sign, unsigned n, unsigned const nums[], Z3_sort* srt) {
|
||||
LOG_TRY;
|
||||
LOG_Z3_mk_mpz_numeral(c, sign, n, nums, srt);
|
||||
RESET_ERROR_CODE();
|
||||
rational z;
|
||||
|
||||
// todo fill in z
|
||||
if (!z.size())
|
||||
z.neg();
|
||||
arith_util & a = mk_c(c)->autil();
|
||||
auto* a = mk_c(c)->mk_numeral_core(r, a.mk_int_sort());
|
||||
Z3_CATCH_RETURN(nullptr);
|
||||
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_mk_mpq_numeral1(Z3_context c, bool sign, unsigned n, unsigned const nums[], unsigned d, unsigned const dens[]) {
|
||||
LOG_TRY;
|
||||
LOG_Z3_mk_mpq_numeral(c, sign, n, nums, d, dens);
|
||||
RESET_ERROR_CODE();
|
||||
rational q;
|
||||
|
||||
if (!sign)
|
||||
q.neg();
|
||||
|
||||
Z3_CATCH_RETURN(nullptr);
|
||||
}
|
||||
#endif
|
||||
|
||||
};
|
||||
|
|
|
|||
|
|
@ -47,8 +47,6 @@ extern "C" {
|
|||
ctx->register_plist();
|
||||
ctx->set_ignore_check(true);
|
||||
}
|
||||
|
||||
~Z3_parser_context_ref() override {}
|
||||
};
|
||||
|
||||
inline Z3_parser_context_ref * to_parser_context(Z3_parser_context pc) { return reinterpret_cast<Z3_parser_context_ref*>(pc); }
|
||||
|
|
|
|||
|
|
@ -36,7 +36,7 @@ Revision History:
|
|||
#include "smt/smt_implied_equalities.h"
|
||||
#include "solver/smt_logics.h"
|
||||
#include "solver/tactic2solver.h"
|
||||
#include "solver/solver_params.hpp"
|
||||
#include "params/solver_params.hpp"
|
||||
#include "cmd_context/cmd_context.h"
|
||||
#include "parsers/smt2/smt2parser.h"
|
||||
#include "sat/dimacs.h"
|
||||
|
|
|
|||
|
|
@ -51,7 +51,6 @@ struct Z3_solver_ref : public api::object {
|
|||
|
||||
Z3_solver_ref(api::context& c, solver_factory * f):
|
||||
api::object(c), m_solver_factory(f), m_solver(nullptr), m_logic(symbol::null), m_eh(nullptr) {}
|
||||
~Z3_solver_ref() override {}
|
||||
|
||||
void assert_expr(expr* e);
|
||||
void assert_expr(expr* e, expr* t);
|
||||
|
|
|
|||
|
|
@ -23,7 +23,6 @@ Revision History:
|
|||
struct Z3_stats_ref : public api::object {
|
||||
statistics m_stats;
|
||||
Z3_stats_ref(api::context& c): api::object(c) {}
|
||||
~Z3_stats_ref() override {}
|
||||
};
|
||||
|
||||
inline Z3_stats_ref * to_stats(Z3_stats s) { return reinterpret_cast<Z3_stats_ref *>(s); }
|
||||
|
|
|
|||
|
|
@ -28,13 +28,11 @@ namespace api {
|
|||
struct Z3_tactic_ref : public api::object {
|
||||
tactic_ref m_tactic;
|
||||
Z3_tactic_ref(api::context& c): api::object(c) {}
|
||||
~Z3_tactic_ref() override {}
|
||||
};
|
||||
|
||||
struct Z3_probe_ref : public api::object {
|
||||
probe_ref m_probe;
|
||||
Z3_probe_ref(api::context& c):api::object(c) {}
|
||||
~Z3_probe_ref() override {}
|
||||
};
|
||||
|
||||
inline Z3_tactic_ref * to_tactic(Z3_tactic g) { return reinterpret_cast<Z3_tactic_ref *>(g); }
|
||||
|
|
@ -50,7 +48,6 @@ struct Z3_apply_result_ref : public api::object {
|
|||
model_converter_ref m_mc;
|
||||
proof_converter_ref m_pc;
|
||||
Z3_apply_result_ref(api::context& c, ast_manager & m);
|
||||
~Z3_apply_result_ref() override {}
|
||||
};
|
||||
|
||||
inline Z3_apply_result_ref * to_apply_result(Z3_apply_result g) { return reinterpret_cast<Z3_apply_result_ref *>(g); }
|
||||
|
|
|
|||
|
|
@ -40,7 +40,7 @@ namespace api {
|
|||
context& m_context;
|
||||
public:
|
||||
object(context& c);
|
||||
virtual ~object() {}
|
||||
virtual ~object() = default;
|
||||
unsigned ref_count() const { return m_ref_count; }
|
||||
unsigned id() const { return m_id; }
|
||||
void inc_ref();
|
||||
|
|
|
|||
|
|
@ -23,7 +23,6 @@ Notes:
|
|||
#include<cassert>
|
||||
#include<ostream>
|
||||
#include<string>
|
||||
#include<sstream>
|
||||
#include<memory>
|
||||
#include<vector>
|
||||
#include<z3.h>
|
||||
|
|
@ -57,6 +56,8 @@ namespace z3 {
|
|||
class param_descrs;
|
||||
class ast;
|
||||
class sort;
|
||||
class constructors;
|
||||
class constructor_list;
|
||||
class func_decl;
|
||||
class expr;
|
||||
class solver;
|
||||
|
|
@ -86,7 +87,7 @@ namespace z3 {
|
|||
class exception : public std::exception {
|
||||
std::string m_msg;
|
||||
public:
|
||||
virtual ~exception() throw() {}
|
||||
virtual ~exception() throw() = default;
|
||||
exception(char const * msg):m_msg(msg) {}
|
||||
char const * msg() const { return m_msg.c_str(); }
|
||||
char const * what() const throw() { return m_msg.c_str(); }
|
||||
|
|
@ -313,6 +314,34 @@ namespace z3 {
|
|||
*/
|
||||
func_decl tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs);
|
||||
|
||||
|
||||
/**
|
||||
\brief Create a recursive datatype over a single sort.
|
||||
\c name is the name of the recursive datatype
|
||||
\c n - the numer of constructors of the datatype
|
||||
\c cs - the \c n constructors used to define the datatype
|
||||
|
||||
References to the datatype can be created using \ref datatype_sort.
|
||||
*/
|
||||
sort datatype(symbol const& name, constructors const& cs);
|
||||
|
||||
/**
|
||||
\brief Create a set of mutually recursive datatypes.
|
||||
\c n - number of recursive datatypes
|
||||
\c names - array of names of length n
|
||||
\c cons - array of constructor lists of length n
|
||||
*/
|
||||
sort_vector datatypes(unsigned n, symbol const* names,
|
||||
constructor_list *const* cons);
|
||||
|
||||
|
||||
/**
|
||||
\brief a reference to a recursively defined datatype.
|
||||
Expect that it gets defined as a \ref datatype.
|
||||
*/
|
||||
sort datatype_sort(symbol const& name);
|
||||
|
||||
|
||||
/**
|
||||
\brief create an uninterpreted sort with the name given by the string or symbol.
|
||||
*/
|
||||
|
|
@ -3330,6 +3359,98 @@ namespace z3 {
|
|||
return func_decl(*this, tuple);
|
||||
}
|
||||
|
||||
class constructor_list {
|
||||
context& ctx;
|
||||
Z3_constructor_list clist;
|
||||
public:
|
||||
constructor_list(constructors const& cs);
|
||||
~constructor_list() { Z3_del_constructor_list(ctx, clist); }
|
||||
operator Z3_constructor_list() const { return clist; }
|
||||
};
|
||||
|
||||
class constructors {
|
||||
friend class constructor_list;
|
||||
context& ctx;
|
||||
std::vector<Z3_constructor> cons;
|
||||
std::vector<unsigned> num_fields;
|
||||
public:
|
||||
constructors(context& ctx): ctx(ctx) {}
|
||||
|
||||
~constructors() {
|
||||
for (auto con : cons)
|
||||
Z3_del_constructor(ctx, con);
|
||||
}
|
||||
|
||||
void add(symbol const& name, symbol const& rec, unsigned n, symbol const* names, sort const* fields) {
|
||||
array<unsigned> sort_refs(n);
|
||||
array<Z3_sort> sorts(n);
|
||||
array<Z3_symbol> _names(n);
|
||||
for (unsigned i = 0; i < n; ++i) sorts[i] = fields[i], _names[i] = names[i];
|
||||
cons.push_back(Z3_mk_constructor(ctx, name, rec, n, _names.ptr(), sorts.ptr(), sort_refs.ptr()));
|
||||
num_fields.push_back(n);
|
||||
}
|
||||
|
||||
Z3_constructor operator[](unsigned i) const { return cons[i]; }
|
||||
|
||||
unsigned size() const { return (unsigned)cons.size(); }
|
||||
|
||||
void query(unsigned i, func_decl& constructor, func_decl& test, func_decl_vector& accs) {
|
||||
Z3_func_decl _constructor;
|
||||
Z3_func_decl _test;
|
||||
array<Z3_func_decl> accessors(num_fields[i]);
|
||||
accs.resize(0);
|
||||
Z3_query_constructor(ctx,
|
||||
cons[i],
|
||||
num_fields[i],
|
||||
&_constructor,
|
||||
&_test,
|
||||
accessors.ptr());
|
||||
constructor = func_decl(ctx, _constructor);
|
||||
|
||||
test = func_decl(ctx, _test);
|
||||
for (unsigned j = 0; j < num_fields[i]; ++j)
|
||||
accs.push_back(func_decl(ctx, accessors[j]));
|
||||
}
|
||||
};
|
||||
|
||||
inline constructor_list::constructor_list(constructors const& cs): ctx(cs.ctx) {
|
||||
array<Z3_constructor> cons(cs.size());
|
||||
for (unsigned i = 0; i < cs.size(); ++i)
|
||||
cons[i] = cs[i];
|
||||
clist = Z3_mk_constructor_list(ctx, cs.size(), cons.ptr());
|
||||
}
|
||||
|
||||
inline sort context::datatype(symbol const& name, constructors const& cs) {
|
||||
array<Z3_constructor> _cs(cs.size());
|
||||
for (unsigned i = 0; i < cs.size(); ++i) _cs[i] = cs[i];
|
||||
Z3_sort s = Z3_mk_datatype(*this, name, cs.size(), _cs.ptr());
|
||||
check_error();
|
||||
return sort(*this, s);
|
||||
}
|
||||
|
||||
inline sort_vector context::datatypes(
|
||||
unsigned n, symbol const* names,
|
||||
constructor_list *const* cons) {
|
||||
sort_vector result(*this);
|
||||
array<Z3_symbol> _names(n);
|
||||
array<Z3_sort> _sorts(n);
|
||||
array<Z3_constructor_list> _cons(n);
|
||||
for (unsigned i = 0; i < n; ++i)
|
||||
_names[i] = names[i], _cons[i] = *cons[i];
|
||||
Z3_mk_datatypes(*this, n, _names.ptr(), _sorts.ptr(), _cons.ptr());
|
||||
for (unsigned i = 0; i < n; ++i)
|
||||
result.push_back(sort(*this, _sorts[i]));
|
||||
return result;
|
||||
}
|
||||
|
||||
|
||||
inline sort context::datatype_sort(symbol const& name) {
|
||||
Z3_sort s = Z3_mk_datatype_sort(*this, name);
|
||||
check_error();
|
||||
return sort(*this, s);
|
||||
}
|
||||
|
||||
|
||||
inline sort context::uninterpreted_sort(char const* name) {
|
||||
Z3_symbol _name = Z3_mk_string_symbol(*this, name);
|
||||
return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
|
||||
|
|
|
|||
|
|
@ -19,7 +19,7 @@ add_custom_command(OUTPUT "${Z3_DOTNET_NATIVE_FILE}"
|
|||
"${PROJECT_SOURCE_DIR}/scripts/update_api.py"
|
||||
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
|
||||
COMMENT "Generating ${Z3_DOTNET_NATIVE_FILE}"
|
||||
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
|
||||
USES_TERMINAL
|
||||
)
|
||||
|
||||
# Generate Enumerations.cs
|
||||
|
|
@ -35,7 +35,7 @@ add_custom_command(OUTPUT "${Z3_DOTNET_CONST_FILE}"
|
|||
"${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py"
|
||||
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
|
||||
COMMENT "Generating ${Z3_DOTNET_CONST_FILE}"
|
||||
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
|
||||
USES_TERMINAL
|
||||
)
|
||||
|
||||
set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
|
||||
|
|
|
|||
|
|
@ -938,6 +938,15 @@ namespace Microsoft.Z3
|
|||
return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Creates a <c>distinct</c> term.
|
||||
/// </summary>
|
||||
public BoolExpr MkDistinct(IEnumerable<Expr> args)
|
||||
{
|
||||
Debug.Assert(args != null);
|
||||
return MkDistinct(args.ToArray());
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Mk an expression representing <c>not(a)</c>.
|
||||
/// </summary>
|
||||
|
|
|
|||
|
|
@ -29,10 +29,8 @@ add_custom_command(OUTPUT "${Z3_JAVA_NATIVE_JAVA}" "${Z3_JAVA_NATIVE_CPP}"
|
|||
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
|
||||
"${PROJECT_SOURCE_DIR}/scripts/update_api.py"
|
||||
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
|
||||
# FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency
|
||||
"${PROJECT_SOURCE_DIR}/scripts/mk_util.py"
|
||||
COMMENT "Generating \"${Z3_JAVA_NATIVE_JAVA}\" and \"${Z3_JAVA_NATIVE_CPP}\""
|
||||
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
|
||||
USES_TERMINAL
|
||||
)
|
||||
|
||||
# Add rule to build native code that provides a bridge between
|
||||
|
|
@ -88,7 +86,7 @@ add_custom_command(OUTPUT ${Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH}
|
|||
"${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py"
|
||||
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
|
||||
COMMENT "Generating ${Z3_JAVA_PACKAGE_NAME}.enumerations package"
|
||||
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
|
||||
USES_TERMINAL
|
||||
)
|
||||
|
||||
set(Z3_JAVA_JAR_SOURCE_FILES
|
||||
|
|
|
|||
|
|
@ -103,7 +103,7 @@ function rcf_get_numerator_denominator(c: Z3_context, a: Z3_rcf_num): { n: Z3_rc
|
|||
When there is only a single out parameter, and the return value is not otherwise of interest, the parameter is not wrapped. For example, the C declaration
|
||||
|
||||
```c
|
||||
Z3_bool Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v);
|
||||
bool Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v);
|
||||
```
|
||||
|
||||
is represented in the TS bindings as
|
||||
|
|
|
|||
|
|
@ -16,7 +16,6 @@ const files = [
|
|||
|
||||
const aliases = {
|
||||
__proto__: null,
|
||||
Z3_bool: 'boolean',
|
||||
Z3_string: 'string',
|
||||
bool: 'boolean',
|
||||
signed: 'int',
|
||||
|
|
|
|||
|
|
@ -498,6 +498,15 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
|
|||
return result;
|
||||
}
|
||||
|
||||
///////////////////////////////
|
||||
// expression simplification //
|
||||
///////////////////////////////
|
||||
|
||||
async function simplify(e : Expr<Name>) {
|
||||
const result = await Z3.simplify(contextPtr, e.ast)
|
||||
return _toExpr(check(result));
|
||||
}
|
||||
|
||||
/////////////
|
||||
// Objects //
|
||||
/////////////
|
||||
|
|
@ -1050,6 +1059,10 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
|
|||
return check(Z3.model_to_string(contextPtr, this.ptr));
|
||||
}
|
||||
|
||||
toString() {
|
||||
return this.sexpr();
|
||||
}
|
||||
|
||||
eval(expr: Bool<Name>, modelCompletion?: boolean): Bool<Name>;
|
||||
eval(expr: Arith<Name>, modelCompletion?: boolean): Arith<Name>;
|
||||
eval(expr: Expr<Name>, modelCompletion: boolean = false) {
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@
|
|||
// @ts-ignore no-implicit-any
|
||||
import { createApi, Z3HighLevel } from './high-level';
|
||||
import { init as initWrapper, Z3LowLevel } from './low-level';
|
||||
import initModule = require('../z3-built');
|
||||
import initModule = require('../build/z3-built');
|
||||
|
||||
export * from './high-level/types';
|
||||
export { Z3Core, Z3LowLevel } from './low-level';
|
||||
|
|
|
|||
|
|
@ -1,4 +1,5 @@
|
|||
#include "jlcxx/jlcxx.hpp"
|
||||
#include <sstream>
|
||||
#include "z3++.h"
|
||||
|
||||
using namespace z3;
|
||||
|
|
|
|||
|
|
@ -43,7 +43,7 @@ add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/z3core.py"
|
|||
"${PROJECT_SOURCE_DIR}/scripts/update_api.py"
|
||||
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
|
||||
COMMENT "Generating z3core.py"
|
||||
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
|
||||
USES_TERMINAL
|
||||
)
|
||||
list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3/z3core.py")
|
||||
|
||||
|
|
@ -59,7 +59,7 @@ add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/z3consts.py"
|
|||
"${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py"
|
||||
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
|
||||
COMMENT "Generating z3consts.py"
|
||||
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
|
||||
USES_TERMINAL
|
||||
)
|
||||
list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3/z3consts.py")
|
||||
|
||||
|
|
|
|||
|
|
@ -129,6 +129,15 @@ def _configure_z3():
|
|||
for key, val in cmake_options.items():
|
||||
if type(val) is bool:
|
||||
cmake_options[key] = str(val).upper()
|
||||
|
||||
# Allow command-line arguments to add and override Z3_ options
|
||||
for i in range(len(sys.argv) - 1):
|
||||
key = sys.argv[i]
|
||||
if key.startswith("Z3_"):
|
||||
val = sys.argv[i + 1].upper()
|
||||
if val == "TRUE" or val == "FALSE":
|
||||
cmake_options[key] = val
|
||||
|
||||
cmake_args = [ '-D' + key + '=' + value for key,value in cmake_options.items() ]
|
||||
args = [ 'cmake', *cmake_args, SRC_DIR ]
|
||||
if subprocess.call(args, env=build_env, cwd=BUILD_DIR) != 0:
|
||||
|
|
|
|||
|
|
@ -204,12 +204,13 @@ class Context:
|
|||
Z3_set_param_value(conf, str(prev), _to_param_value(a))
|
||||
prev = None
|
||||
self.ctx = Z3_mk_context_rc(conf)
|
||||
self.owner = True
|
||||
self.eh = Z3_set_error_handler(self.ctx, z3_error_handler)
|
||||
Z3_set_ast_print_mode(self.ctx, Z3_PRINT_SMTLIB2_COMPLIANT)
|
||||
Z3_del_config(conf)
|
||||
|
||||
def __del__(self):
|
||||
if Z3_del_context is not None:
|
||||
if Z3_del_context is not None and self.owner:
|
||||
Z3_del_context(self.ctx)
|
||||
self.ctx = None
|
||||
self.eh = None
|
||||
|
|
@ -5345,6 +5346,10 @@ class DatatypeRef(ExprRef):
|
|||
"""Return the datatype sort of the datatype expression `self`."""
|
||||
return DatatypeSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
|
||||
|
||||
def DatatypeSort(name, ctx = None):
|
||||
"""Create a reference to a sort that was declared, or will be declared, as a recursive datatype"""
|
||||
ctx = _get_ctx(ctx)
|
||||
return DatatypeSortRef(Z3_mk_datatype_sort(ctx.ref(), to_symbol(name, ctx)), ctx)
|
||||
|
||||
def TupleSort(name, sorts, ctx=None):
|
||||
"""Create a named tuple sort base on a set of underlying sorts
|
||||
|
|
@ -11353,13 +11358,24 @@ def user_prop_pop(ctx, cb, num_scopes):
|
|||
prop.cb = cb
|
||||
prop.pop(num_scopes)
|
||||
|
||||
def to_ContextObj(ptr,):
|
||||
ctx = ContextObj(ptr)
|
||||
super(ctypes.c_void_p, ctx).__init__(ptr)
|
||||
return ctx
|
||||
|
||||
def user_prop_fresh(id, ctx):
|
||||
|
||||
def user_prop_fresh(ctx, _new_ctx):
|
||||
_prop_closures.set_threaded()
|
||||
prop = _prop_closures.get(id)
|
||||
new_prop = prop.fresh()
|
||||
prop = _prop_closures.get(ctx)
|
||||
nctx = Context()
|
||||
Z3_del_context(nctx.ctx)
|
||||
new_ctx = to_ContextObj(_new_ctx)
|
||||
nctx.ctx = new_ctx
|
||||
nctx.eh = Z3_set_error_handler(new_ctx, z3_error_handler)
|
||||
nctx.owner = False
|
||||
new_prop = prop.fresh(nctx)
|
||||
_prop_closures.set(new_prop.id, new_prop)
|
||||
return ctypes.c_void_p(new_prop.id)
|
||||
return new_prop.id
|
||||
|
||||
def to_Ast(ptr,):
|
||||
ast = Ast(ptr)
|
||||
|
|
@ -11374,6 +11390,13 @@ def user_prop_fixed(ctx, cb, id, value):
|
|||
prop.fixed(id, value)
|
||||
prop.cb = None
|
||||
|
||||
def user_prop_created(ctx, cb, id):
|
||||
prop = _prop_closures.get(ctx)
|
||||
prop.cb = cb
|
||||
id = _to_expr_ref(to_Ast(id), prop.ctx())
|
||||
prop.created(id)
|
||||
prop.cb = None
|
||||
|
||||
def user_prop_final(ctx, cb):
|
||||
prop = _prop_closures.get(ctx)
|
||||
prop.cb = cb
|
||||
|
|
@ -11396,15 +11419,50 @@ def user_prop_diseq(ctx, cb, x, y):
|
|||
prop.diseq(x, y)
|
||||
prop.cb = None
|
||||
|
||||
# TODO The decision callback is not fully implemented.
|
||||
# It needs to handle the ast*, unsigned* idx, and Z3_lbool*
|
||||
def user_prop_decide(ctx, cb, t_ref, idx_ref, phase_ref):
|
||||
prop = _prop_closures.get(ctx)
|
||||
prop.cb = cb
|
||||
t = _to_expr_ref(to_Ast(t_ref), prop.ctx())
|
||||
t, idx, phase = prop.decide(t, idx, phase)
|
||||
t_ref = t
|
||||
idx_ref = idx
|
||||
phase_ref = phase
|
||||
prop.cb = None
|
||||
|
||||
|
||||
_user_prop_push = Z3_push_eh(user_prop_push)
|
||||
_user_prop_pop = Z3_pop_eh(user_prop_pop)
|
||||
_user_prop_fresh = Z3_fresh_eh(user_prop_fresh)
|
||||
_user_prop_fixed = Z3_fixed_eh(user_prop_fixed)
|
||||
_user_prop_created = Z3_created_eh(user_prop_created)
|
||||
_user_prop_final = Z3_final_eh(user_prop_final)
|
||||
_user_prop_eq = Z3_eq_eh(user_prop_eq)
|
||||
_user_prop_diseq = Z3_eq_eh(user_prop_diseq)
|
||||
_user_prop_decide = Z3_decide_eh(user_prop_decide)
|
||||
|
||||
def PropagateFunction(name, *sig):
|
||||
"""Create a function that gets tracked by user propagator.
|
||||
Every term headed by this function symbol is tracked.
|
||||
If a term is fixed and the fixed callback is registered a
|
||||
callback is invoked that the term headed by this function is fixed.
|
||||
"""
|
||||
sig = _get_args(sig)
|
||||
if z3_debug():
|
||||
_z3_assert(len(sig) > 0, "At least two arguments expected")
|
||||
arity = len(sig) - 1
|
||||
rng = sig[arity]
|
||||
if z3_debug():
|
||||
_z3_assert(is_sort(rng), "Z3 sort expected")
|
||||
dom = (Sort * arity)()
|
||||
for i in range(arity):
|
||||
if z3_debug():
|
||||
_z3_assert(is_sort(sig[i]), "Z3 sort expected")
|
||||
dom[i] = sig[i].ast
|
||||
ctx = rng.ctx
|
||||
return FuncDeclRef(Z3_solver_propagate_declare(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx)
|
||||
|
||||
|
||||
class UserPropagateBase:
|
||||
|
||||
|
|
@ -11420,19 +11478,16 @@ class UserPropagateBase:
|
|||
ensure_prop_closures()
|
||||
self.solver = s
|
||||
self._ctx = None
|
||||
self.fresh_ctx = None
|
||||
self.cb = None
|
||||
self.id = _prop_closures.insert(self)
|
||||
self.fixed = None
|
||||
self.final = None
|
||||
self.eq = None
|
||||
self.diseq = None
|
||||
self.created = None
|
||||
if ctx:
|
||||
# TBD fresh is broken: ctx is not of the right type when we reach here.
|
||||
self._ctx = Context()
|
||||
#Z3_del_context(self._ctx.ctx)
|
||||
#self._ctx.ctx = ctx
|
||||
#self._ctx.eh = Z3_set_error_handler(ctx, z3_error_handler)
|
||||
#Z3_set_ast_print_mode(ctx, Z3_PRINT_SMTLIB2_COMPLIANT)
|
||||
self.fresh_ctx = ctx
|
||||
if s:
|
||||
Z3_solver_propagate_init(self.ctx_ref(),
|
||||
s.solver,
|
||||
|
|
@ -11446,8 +11501,8 @@ class UserPropagateBase:
|
|||
self._ctx.ctx = None
|
||||
|
||||
def ctx(self):
|
||||
if self._ctx:
|
||||
return self._ctx
|
||||
if self.fresh_ctx:
|
||||
return self.fresh_ctx
|
||||
else:
|
||||
return self.solver.ctx
|
||||
|
||||
|
|
@ -11457,41 +11512,69 @@ class UserPropagateBase:
|
|||
def add_fixed(self, fixed):
|
||||
assert not self.fixed
|
||||
assert not self._ctx
|
||||
Z3_solver_propagate_fixed(self.ctx_ref(), self.solver.solver, _user_prop_fixed)
|
||||
if self.solver:
|
||||
Z3_solver_propagate_fixed(self.ctx_ref(), self.solver.solver, _user_prop_fixed)
|
||||
self.fixed = fixed
|
||||
|
||||
def add_created(self, created):
|
||||
assert not self.created
|
||||
assert not self._ctx
|
||||
if self.solver:
|
||||
Z3_solver_propagate_created(self.ctx_ref(), self.solver.solver, _user_prop_created)
|
||||
self.created = created
|
||||
|
||||
def add_final(self, final):
|
||||
assert not self.final
|
||||
assert not self._ctx
|
||||
Z3_solver_propagate_final(self.ctx_ref(), self.solver.solver, _user_prop_final)
|
||||
if self.solver:
|
||||
Z3_solver_propagate_final(self.ctx_ref(), self.solver.solver, _user_prop_final)
|
||||
self.final = final
|
||||
|
||||
def add_eq(self, eq):
|
||||
assert not self.eq
|
||||
assert not self._ctx
|
||||
Z3_solver_propagate_eq(self.ctx_ref(), self.solver.solver, _user_prop_eq)
|
||||
if self.solver:
|
||||
Z3_solver_propagate_eq(self.ctx_ref(), self.solver.solver, _user_prop_eq)
|
||||
self.eq = eq
|
||||
|
||||
def add_diseq(self, diseq):
|
||||
assert not self.diseq
|
||||
assert not self._ctx
|
||||
Z3_solver_propagate_diseq(self.ctx_ref(), self.solver.solver, _user_prop_diseq)
|
||||
if self.solver:
|
||||
Z3_solver_propagate_diseq(self.ctx_ref(), self.solver.solver, _user_prop_diseq)
|
||||
self.diseq = diseq
|
||||
|
||||
def add_decide(self, decide):
|
||||
assert not self.decide
|
||||
assert not self._ctx
|
||||
if self.solver:
|
||||
Z3_solver_propagate_decide(self.ctx_ref(), self.solver.solver, _user_prop_decide)
|
||||
self.decide = decide
|
||||
|
||||
def push(self):
|
||||
raise Z3Exception("push needs to be overwritten")
|
||||
|
||||
def pop(self, num_scopes):
|
||||
raise Z3Exception("pop needs to be overwritten")
|
||||
|
||||
def fresh(self):
|
||||
def fresh(self, new_ctx):
|
||||
raise Z3Exception("fresh needs to be overwritten")
|
||||
|
||||
def add(self, e):
|
||||
assert self.solver
|
||||
assert not self._ctx
|
||||
Z3_solver_propagate_register(self.ctx_ref(), self.solver.solver, e.ast)
|
||||
|
||||
if self.solver:
|
||||
Z3_solver_propagate_register(self.ctx_ref(), self.solver.solver, e.ast)
|
||||
else:
|
||||
Z3_solver_propagate_register_cb(self.ctx_ref(), ctypes.c_void_p(self.cb), e.ast)
|
||||
|
||||
#
|
||||
# Tell the solver to perform the next split on a given term
|
||||
# If the term is a bit-vector the index idx specifies the index of the Boolean variable being
|
||||
# split on. A phase of true = 1/false = -1/undef = 0 = let solver decide is the last argument.
|
||||
#
|
||||
def next_split(self, t, idx, phase):
|
||||
Z3_solver_next_split(self.ctx_ref(), ctypes.c_void_p(self.cb), t.ast, idx, phase)
|
||||
|
||||
#
|
||||
# Propagation can only be invoked as during a fixed or final callback.
|
||||
#
|
||||
|
|
@ -11503,5 +11586,5 @@ class UserPropagateBase:
|
|||
Z3_solver_propagate_consequence(e.ctx.ref(), ctypes.c_void_p(
|
||||
self.cb), num_fixed, _ids, num_eqs, _lhs, _rhs, e.ast)
|
||||
|
||||
def conflict(self, deps):
|
||||
self.propagate(BoolVal(False, self.ctx()), deps, eqs=[])
|
||||
def conflict(self, deps = [], eqs = []):
|
||||
self.propagate(BoolVal(False, self.ctx()), deps, eqs)
|
||||
|
|
|
|||
110
src/api/z3_api.h
110
src/api/z3_api.h
|
|
@ -75,11 +75,6 @@ DEFINE_TYPE(Z3_rcf_num);
|
|||
- \c Z3_stats: statistical data for a solver.
|
||||
*/
|
||||
|
||||
/**
|
||||
\brief Z3 Boolean type. It is just an alias for \c bool.
|
||||
*/
|
||||
typedef bool Z3_bool;
|
||||
|
||||
/**
|
||||
\brief Z3 string type. It is just an alias for \ccode{const char *}.
|
||||
*/
|
||||
|
|
@ -87,16 +82,6 @@ typedef const char * Z3_string;
|
|||
typedef char const* Z3_char_ptr;
|
||||
typedef Z3_string * Z3_string_ptr;
|
||||
|
||||
/**
|
||||
\brief True value. It is just an alias for \c true.
|
||||
*/
|
||||
#define Z3_TRUE true
|
||||
|
||||
/**
|
||||
\brief False value. It is just an alias for \c false.
|
||||
*/
|
||||
#define Z3_FALSE false
|
||||
|
||||
/**
|
||||
\brief Lifted Boolean type: \c false, \c undefined, \c true.
|
||||
*/
|
||||
|
|
@ -1528,7 +1513,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_global_param_get', BOOL, (_in(STRING), _out(STRING)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value);
|
||||
bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value);
|
||||
|
||||
/**@}*/
|
||||
|
||||
|
|
@ -3387,6 +3372,39 @@ extern "C" {
|
|||
*/
|
||||
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty);
|
||||
|
||||
#if 0
|
||||
/**
|
||||
\brief Create an integer numeral from a vector of unsigned numerals.
|
||||
|
||||
\param c - context
|
||||
\param sign - true if positive, false if negative
|
||||
\param n - length of array of numerals
|
||||
\param nums - array of numerals
|
||||
\param s - sort of numeral (int, real, bit-vector).
|
||||
|
||||
future_('Z3_mk_mpz_numeral', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in_array(2, UINT), _in(SORT)))
|
||||
*/
|
||||
|
||||
Z3_ast Z3_mk_mpz_numeral(Z3_context c, bool sign, unsigned n, unsigned const nums[], Z3_sort s);
|
||||
|
||||
/**
|
||||
\brief Create a rational numeral from a vector of unsigned numerals.
|
||||
|
||||
\param c - context
|
||||
\param sign - true if positive, false if negative
|
||||
\param n - length of array of nominator numerals
|
||||
\param nums - array of numerator numerals
|
||||
\param d - length of array of denominator numerals
|
||||
\param dens - array of denominator numerals
|
||||
|
||||
The sort of returned numeral is Real.
|
||||
|
||||
future_('Z3_mk_mpq_numeral', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in_array(2, UINT), _in(UINT), _in_array(4, UINT)))
|
||||
*/
|
||||
|
||||
Z3_ast Z3_mk_mpq_numeral(Z3_context c, bool sign, unsigned n, unsigned const nums[], unsigned d, unsigned const dens[]);
|
||||
#endif
|
||||
|
||||
/**
|
||||
\brief Create a real from a fraction.
|
||||
|
||||
|
|
@ -4407,7 +4425,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_get_finite_domain_sort_size', BOOL, (_in(CONTEXT), _in(SORT), _out(UINT64)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t* r);
|
||||
bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t* r);
|
||||
|
||||
/**
|
||||
\brief Return the domain of the given array sort.
|
||||
|
|
@ -4822,6 +4840,8 @@ extern "C" {
|
|||
\brief Return the number of argument of an application. If \c t
|
||||
is an constant, then the number of arguments is 0.
|
||||
|
||||
\sa Z3_get_app_arg
|
||||
|
||||
def_API('Z3_get_app_num_args', UINT, (_in(CONTEXT), _in(APP)))
|
||||
*/
|
||||
unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a);
|
||||
|
|
@ -4831,6 +4851,8 @@ extern "C" {
|
|||
|
||||
\pre i < Z3_get_app_num_args(c, a)
|
||||
|
||||
\sa Z3_get_app_num_args
|
||||
|
||||
def_API('Z3_get_app_arg', AST, (_in(CONTEXT), _in(APP), _in(UINT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i);
|
||||
|
|
@ -5376,7 +5398,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_model_eval', BOOL, (_in(CONTEXT), _in(MODEL), _in(AST), _in(BOOL), _out(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v);
|
||||
bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v);
|
||||
|
||||
/**
|
||||
\brief Return the interpretation (i.e., assignment) of constant \c a in the model \c m.
|
||||
|
|
@ -5425,6 +5447,7 @@ extern "C" {
|
|||
\pre i < Z3_model_get_num_consts(c, m)
|
||||
|
||||
\sa Z3_model_eval
|
||||
\sa Z3_model_get_num_consts
|
||||
|
||||
def_API('Z3_model_get_const_decl', FUNC_DECL, (_in(CONTEXT), _in(MODEL), _in(UINT)))
|
||||
*/
|
||||
|
|
@ -5436,6 +5459,8 @@ extern "C" {
|
|||
A function interpretation is represented as a finite map and an 'else' value.
|
||||
Each entry in the finite map represents the value of a function given a set of arguments.
|
||||
|
||||
\sa Z3_model_get_func_decl
|
||||
|
||||
def_API('Z3_model_get_num_funcs', UINT, (_in(CONTEXT), _in(MODEL)))
|
||||
*/
|
||||
unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m);
|
||||
|
|
@ -5561,6 +5586,8 @@ extern "C" {
|
|||
Each entry in the finite map represents the value of a function given a set of arguments.
|
||||
This procedure return the number of element in the finite map of \c f.
|
||||
|
||||
\sa Z3_func_interp_get_entry
|
||||
|
||||
def_API('Z3_func_interp_get_num_entries', UINT, (_in(CONTEXT), _in(FUNC_INTERP)))
|
||||
*/
|
||||
unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f);
|
||||
|
|
@ -5649,6 +5676,7 @@ extern "C" {
|
|||
/**
|
||||
\brief Return the number of arguments in a \c Z3_func_entry object.
|
||||
|
||||
\sa Z3_func_entry_get_arg
|
||||
\sa Z3_func_interp_get_entry
|
||||
|
||||
def_API('Z3_func_entry_get_num_args', UINT, (_in(CONTEXT), _in(FUNC_ENTRY)))
|
||||
|
|
@ -5660,6 +5688,7 @@ extern "C" {
|
|||
|
||||
\pre i < Z3_func_entry_get_num_args(c, e)
|
||||
|
||||
\sa Z3_func_entry_get_num_args
|
||||
\sa Z3_func_interp_get_entry
|
||||
|
||||
def_API('Z3_func_entry_get_arg', AST, (_in(CONTEXT), _in(FUNC_ENTRY), _in(UINT)))
|
||||
|
|
@ -5672,6 +5701,9 @@ extern "C" {
|
|||
/**
|
||||
\brief Log interaction to a file.
|
||||
|
||||
\sa Z3_append_log
|
||||
\sa Z3_close_log
|
||||
|
||||
extra_API('Z3_open_log', INT, (_in(STRING),))
|
||||
*/
|
||||
bool Z3_API Z3_open_log(Z3_string filename);
|
||||
|
|
@ -5679,10 +5711,13 @@ extern "C" {
|
|||
/**
|
||||
\brief Append user-defined string to interaction log.
|
||||
|
||||
The interaction log is opened using Z3_open_log.
|
||||
The interaction log is opened using #Z3_open_log.
|
||||
It contains the formulas that are checked using Z3.
|
||||
You can use this command to append comments, for instance.
|
||||
|
||||
\sa Z3_open_log
|
||||
\sa Z3_close_log
|
||||
|
||||
extra_API('Z3_append_log', VOID, (_in(STRING),))
|
||||
*/
|
||||
void Z3_API Z3_append_log(Z3_string string);
|
||||
|
|
@ -5690,6 +5725,9 @@ extern "C" {
|
|||
/**
|
||||
\brief Close interaction log.
|
||||
|
||||
\sa Z3_open_log
|
||||
\sa Z3_append_log
|
||||
|
||||
extra_API('Z3_close_log', VOID, ())
|
||||
*/
|
||||
void Z3_API Z3_close_log(void);
|
||||
|
|
@ -6388,6 +6426,8 @@ extern "C" {
|
|||
/**
|
||||
\brief Return the number of builtin tactics available in Z3.
|
||||
|
||||
\sa Z3_get_tactic_name
|
||||
|
||||
def_API('Z3_get_num_tactics', UINT, (_in(CONTEXT),))
|
||||
*/
|
||||
unsigned Z3_API Z3_get_num_tactics(Z3_context c);
|
||||
|
|
@ -6397,6 +6437,8 @@ extern "C" {
|
|||
|
||||
\pre i < Z3_get_num_tactics(c)
|
||||
|
||||
\sa Z3_get_num_tactics
|
||||
|
||||
def_API('Z3_get_tactic_name', STRING, (_in(CONTEXT), _in(UINT)))
|
||||
*/
|
||||
Z3_string Z3_API Z3_get_tactic_name(Z3_context c, unsigned i);
|
||||
|
|
@ -6404,6 +6446,8 @@ extern "C" {
|
|||
/**
|
||||
\brief Return the number of builtin probes available in Z3.
|
||||
|
||||
\sa Z3_get_probe_name
|
||||
|
||||
def_API('Z3_get_num_probes', UINT, (_in(CONTEXT),))
|
||||
*/
|
||||
unsigned Z3_API Z3_get_num_probes(Z3_context c);
|
||||
|
|
@ -6413,6 +6457,8 @@ extern "C" {
|
|||
|
||||
\pre i < Z3_get_num_probes(c)
|
||||
|
||||
\sa Z3_get_num_probes
|
||||
|
||||
def_API('Z3_get_probe_name', STRING, (_in(CONTEXT), _in(UINT)))
|
||||
*/
|
||||
Z3_string Z3_API Z3_get_probe_name(Z3_context c, unsigned i);
|
||||
|
|
@ -6456,6 +6502,8 @@ extern "C" {
|
|||
/**
|
||||
\brief Apply tactic \c t to the goal \c g.
|
||||
|
||||
\sa Z3_tactic_apply_ex
|
||||
|
||||
def_API('Z3_tactic_apply', APPLY_RESULT, (_in(CONTEXT), _in(TACTIC), _in(GOAL)))
|
||||
*/
|
||||
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g);
|
||||
|
|
@ -6463,6 +6511,8 @@ extern "C" {
|
|||
/**
|
||||
\brief Apply tactic \c t to the goal \c g using the parameter set \c p.
|
||||
|
||||
\sa Z3_tactic_apply
|
||||
|
||||
def_API('Z3_tactic_apply_ex', APPLY_RESULT, (_in(CONTEXT), _in(TACTIC), _in(GOAL), _in(PARAMS)))
|
||||
*/
|
||||
Z3_apply_result Z3_API Z3_tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p);
|
||||
|
|
@ -6491,6 +6541,8 @@ extern "C" {
|
|||
/**
|
||||
\brief Return the number of subgoals in the \c Z3_apply_result object returned by #Z3_tactic_apply.
|
||||
|
||||
\sa Z3_apply_result_get_subgoal
|
||||
|
||||
def_API('Z3_apply_result_get_num_subgoals', UINT, (_in(CONTEXT), _in(APPLY_RESULT)))
|
||||
*/
|
||||
unsigned Z3_API Z3_apply_result_get_num_subgoals(Z3_context c, Z3_apply_result r);
|
||||
|
|
@ -6500,6 +6552,8 @@ extern "C" {
|
|||
|
||||
\pre i < Z3_apply_result_get_num_subgoals(c, r)
|
||||
|
||||
\sa Z3_apply_result_get_num_subgoals
|
||||
|
||||
def_API('Z3_apply_result_get_subgoal', GOAL, (_in(CONTEXT), _in(APPLY_RESULT), _in(UINT)))
|
||||
*/
|
||||
Z3_goal Z3_API Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, unsigned i);
|
||||
|
|
@ -6542,6 +6596,10 @@ extern "C" {
|
|||
\remark User must use #Z3_solver_inc_ref and #Z3_solver_dec_ref to manage solver objects.
|
||||
Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc.
|
||||
|
||||
\sa Z3_mk_simple_solver
|
||||
\sa Z3_mk_solver_for_logic
|
||||
\sa Z3_mk_solver_from_tactic
|
||||
|
||||
def_API('Z3_mk_solver', SOLVER, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_solver Z3_API Z3_mk_solver(Z3_context c);
|
||||
|
|
@ -6569,6 +6627,10 @@ extern "C" {
|
|||
\remark User must use #Z3_solver_inc_ref and #Z3_solver_dec_ref to manage solver objects.
|
||||
Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc.
|
||||
|
||||
\sa Z3_mk_solver
|
||||
\sa Z3_mk_solver_for_logic
|
||||
\sa Z3_mk_solver_from_tactic
|
||||
|
||||
def_API('Z3_mk_simple_solver', SOLVER, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c);
|
||||
|
|
@ -6580,6 +6642,10 @@ extern "C" {
|
|||
\remark User must use #Z3_solver_inc_ref and #Z3_solver_dec_ref to manage solver objects.
|
||||
Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc.
|
||||
|
||||
\sa Z3_mk_solver
|
||||
\sa Z3_mk_simple_solver
|
||||
\sa Z3_mk_solver_from_tactic
|
||||
|
||||
def_API('Z3_mk_solver_for_logic', SOLVER, (_in(CONTEXT), _in(SYMBOL)))
|
||||
*/
|
||||
Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic);
|
||||
|
|
@ -6592,6 +6658,10 @@ extern "C" {
|
|||
\remark User must use #Z3_solver_inc_ref and #Z3_solver_dec_ref to manage solver objects.
|
||||
Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc.
|
||||
|
||||
\sa Z3_mk_solver
|
||||
\sa Z3_mk_simple_solver
|
||||
\sa Z3_mk_solver_for_logic
|
||||
|
||||
def_API('Z3_mk_solver_from_tactic', SOLVER, (_in(CONTEXT), _in(TACTIC)))
|
||||
*/
|
||||
Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t);
|
||||
|
|
@ -6899,7 +6969,7 @@ extern "C" {
|
|||
/**
|
||||
Create uninterpreted function declaration for the user propagator.
|
||||
When expressions using the function are created by the solver invoke a callback
|
||||
to \ref \Z3_solver_propagate_created with arguments
|
||||
to \ref Z3_solver_propagate_created with arguments
|
||||
1. context and callback solve
|
||||
2. declared_expr: expression using function that was used as the top-level symbol
|
||||
3. declared_id: a unique identifier (unique within the current scope) to track the expression.
|
||||
|
|
|
|||
|
|
@ -16,6 +16,8 @@ Author:
|
|||
Notes:
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
|
||||
#include "util/symbol.h"
|
||||
|
||||
void R();
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@
|
|||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
#pragma once
|
||||
|
||||
#ifndef Z3_API
|
||||
# ifdef __GNUC__
|
||||
|
|
|
|||
|
|
@ -107,7 +107,6 @@ class array_decl_plugin : public decl_plugin {
|
|||
bool is_array_sort(sort* s) const;
|
||||
public:
|
||||
array_decl_plugin();
|
||||
~array_decl_plugin() override {}
|
||||
|
||||
decl_plugin * mk_fresh() override {
|
||||
return alloc(array_decl_plugin);
|
||||
|
|
|
|||
|
|
@ -1429,7 +1429,7 @@ ast_manager::~ast_manager() {
|
|||
}
|
||||
m_plugins.reset();
|
||||
while (!m_ast_table.empty()) {
|
||||
DEBUG_CODE(IF_VERBOSE(0, verbose_stream() << "ast_manager LEAKED: " << m_ast_table.size() << std::endl););
|
||||
DEBUG_CODE(IF_VERBOSE(1, verbose_stream() << "ast_manager LEAKED: " << m_ast_table.size() << std::endl););
|
||||
ptr_vector<ast> roots;
|
||||
ast_mark mark;
|
||||
for (ast * n : m_ast_table) {
|
||||
|
|
@ -1465,22 +1465,21 @@ ast_manager::~ast_manager() {
|
|||
break;
|
||||
}
|
||||
}
|
||||
for (ast * n : m_ast_table) {
|
||||
if (!mark.is_marked(n)) {
|
||||
for (ast * n : m_ast_table)
|
||||
if (!mark.is_marked(n))
|
||||
roots.push_back(n);
|
||||
}
|
||||
}
|
||||
|
||||
SASSERT(!roots.empty());
|
||||
for (unsigned i = 0; i < roots.size(); ++i) {
|
||||
ast* a = roots[i];
|
||||
DEBUG_CODE(
|
||||
std::cout << "Leaked: ";
|
||||
if (is_sort(a)) {
|
||||
std::cout << to_sort(a)->get_name() << "\n";
|
||||
}
|
||||
else {
|
||||
std::cout << mk_ll_pp(a, *this, false) << "id: " << a->get_id() << "\n";
|
||||
});
|
||||
IF_VERBOSE(1,
|
||||
verbose_stream() << "Leaked: ";
|
||||
if (is_sort(a))
|
||||
verbose_stream() << to_sort(a)->get_name() << "\n";
|
||||
else
|
||||
verbose_stream() << mk_ll_pp(a, *this, false) << "id: " << a->get_id() << "\n";
|
||||
););
|
||||
a->m_ref_count = 0;
|
||||
delete_node(a);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1024,7 +1024,7 @@ protected:
|
|||
friend class ast_manager;
|
||||
|
||||
public:
|
||||
virtual ~decl_plugin() {}
|
||||
virtual ~decl_plugin() = default;
|
||||
virtual void finalize() {}
|
||||
|
||||
|
||||
|
|
@ -2582,7 +2582,7 @@ class ast_mark {
|
|||
obj_mark<expr> m_expr_marks;
|
||||
obj_mark<decl, bit_vector, decl2uint> m_decl_marks;
|
||||
public:
|
||||
virtual ~ast_mark() {}
|
||||
virtual ~ast_mark() = default;
|
||||
bool is_marked(ast * n) const;
|
||||
virtual void mark(ast * n, bool flag);
|
||||
virtual void reset();
|
||||
|
|
|
|||
|
|
@ -64,6 +64,17 @@ void ast_pp_util::display_decls(std::ostream& out) {
|
|||
m_rec_decls = n;
|
||||
}
|
||||
|
||||
void ast_pp_util::display_skolem_decls(std::ostream& out) {
|
||||
ast_smt_pp pp(m);
|
||||
unsigned n = coll.get_num_decls();
|
||||
for (unsigned i = m_decls; i < n; ++i) {
|
||||
func_decl* f = coll.get_func_decls()[i];
|
||||
if (f->get_family_id() == null_family_id && !m_removed.contains(f) && f->is_skolem())
|
||||
ast_smt2_pp(out, f, m_env) << "\n";
|
||||
}
|
||||
m_decls = n;
|
||||
}
|
||||
|
||||
void ast_pp_util::remove_decl(func_decl* f) {
|
||||
m_removed.insert(f);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -50,6 +50,8 @@ class ast_pp_util {
|
|||
|
||||
void display_decls(std::ostream& out);
|
||||
|
||||
void display_skolem_decls(std::ostream& out);
|
||||
|
||||
void display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat = true);
|
||||
|
||||
void display_assert(std::ostream& out, expr* f, bool neat = true);
|
||||
|
|
|
|||
|
|
@ -26,7 +26,6 @@ class simple_ast_printer_context : public ast_printer_context {
|
|||
smt2_pp_environment_dbg & env() const { return *(m_env.get()); }
|
||||
public:
|
||||
simple_ast_printer_context(ast_manager & m):m_manager(m) { m_env = alloc(smt2_pp_environment_dbg, m); }
|
||||
~simple_ast_printer_context() override {}
|
||||
ast_manager & m() const { return m_manager; }
|
||||
ast_manager & get_ast_manager() override { return m_manager; }
|
||||
void display(std::ostream & out, sort * s, unsigned indent = 0) const override { out << mk_ismt2_pp(s, m(), indent); }
|
||||
|
|
|
|||
|
|
@ -24,7 +24,7 @@ Revision History:
|
|||
|
||||
class ast_printer {
|
||||
public:
|
||||
virtual ~ast_printer() {}
|
||||
virtual ~ast_printer() = default;
|
||||
virtual void pp(sort * s, format_ns::format_ref & r) const { UNREACHABLE(); }
|
||||
virtual void pp(func_decl * f, format_ns::format_ref & r) const { UNREACHABLE(); }
|
||||
virtual void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer<symbol> & var_names) const { UNREACHABLE(); }
|
||||
|
|
@ -45,7 +45,6 @@ public:
|
|||
|
||||
class ast_printer_context : public ast_printer {
|
||||
public:
|
||||
~ast_printer_context() override {}
|
||||
virtual ast_manager & get_ast_manager() = 0;
|
||||
virtual std::ostream & regular_stream();
|
||||
virtual std::ostream & diagnostic_stream();
|
||||
|
|
|
|||
|
|
@ -46,7 +46,7 @@ protected:
|
|||
format_ns::format * pp_as(format_ns::format * fname, sort * s);
|
||||
format_ns::format * pp_signature(format_ns::format * f_name, func_decl * f);
|
||||
public:
|
||||
virtual ~smt2_pp_environment() {}
|
||||
virtual ~smt2_pp_environment() = default;
|
||||
virtual ast_manager & get_manager() const = 0;
|
||||
virtual arith_util & get_autil() = 0;
|
||||
virtual bv_util & get_bvutil() = 0;
|
||||
|
|
|
|||
|
|
@ -241,7 +241,6 @@ protected:
|
|||
public:
|
||||
bv_decl_plugin();
|
||||
|
||||
~bv_decl_plugin() override {}
|
||||
void finalize() override;
|
||||
|
||||
decl_plugin * mk_fresh() override { return alloc(bv_decl_plugin); }
|
||||
|
|
@ -343,6 +342,14 @@ public:
|
|||
bool is_bv_not(expr const * e) const { return is_app_of(e, get_fid(), OP_BNOT); }
|
||||
bool is_bv_ule(expr const * e) const { return is_app_of(e, get_fid(), OP_ULEQ); }
|
||||
bool is_bv_sle(expr const * e) const { return is_app_of(e, get_fid(), OP_SLEQ); }
|
||||
bool is_ule(expr const * e) const { return is_app_of(e, get_fid(), OP_ULEQ); }
|
||||
bool is_sle(expr const * e) const { return is_app_of(e, get_fid(), OP_SLEQ); }
|
||||
bool is_ult(expr const * e) const { return is_app_of(e, get_fid(), OP_ULT); }
|
||||
bool is_slt(expr const * e) const { return is_app_of(e, get_fid(), OP_SLT); }
|
||||
bool is_ugt(expr const * e) const { return is_app_of(e, get_fid(), OP_UGT); }
|
||||
bool is_sgt(expr const * e) const { return is_app_of(e, get_fid(), OP_SGT); }
|
||||
bool is_uge(expr const * e) const { return is_app_of(e, get_fid(), OP_UGEQ); }
|
||||
bool is_sge(expr const * e) const { return is_app_of(e, get_fid(), OP_SGEQ); }
|
||||
bool is_bit2bool(expr const * e) const { return is_app_of(e, get_fid(), OP_BIT2BOOL); }
|
||||
bool is_bv2int(expr const* e) const { return is_app_of(e, get_fid(), OP_BV2INT); }
|
||||
bool is_int2bv(expr const* e) const { return is_app_of(e, get_fid(), OP_INT2BV); }
|
||||
|
|
@ -356,9 +363,19 @@ public:
|
|||
MATCH_UNARY(is_bv_not);
|
||||
|
||||
MATCH_BINARY(is_bv_add);
|
||||
MATCH_BINARY(is_bv_sub);
|
||||
MATCH_BINARY(is_bv_mul);
|
||||
MATCH_BINARY(is_bv_sle);
|
||||
MATCH_BINARY(is_bv_ule);
|
||||
MATCH_BINARY(is_ule);
|
||||
MATCH_BINARY(is_sle);
|
||||
MATCH_BINARY(is_ult);
|
||||
MATCH_BINARY(is_slt);
|
||||
MATCH_BINARY(is_uge);
|
||||
MATCH_BINARY(is_sge);
|
||||
MATCH_BINARY(is_ugt);
|
||||
MATCH_BINARY(is_sgt);
|
||||
MATCH_BINARY(is_bv_umul_no_ovfl);
|
||||
MATCH_BINARY(is_bv_ashr);
|
||||
MATCH_BINARY(is_bv_lshr);
|
||||
MATCH_BINARY(is_bv_shl);
|
||||
|
|
|
|||
|
|
@ -105,7 +105,7 @@ namespace datatype {
|
|||
class size {
|
||||
unsigned m_ref{ 0 };
|
||||
public:
|
||||
virtual ~size() { }
|
||||
virtual ~size() = default;
|
||||
void inc_ref() { ++m_ref; }
|
||||
void dec_ref();
|
||||
static size* mk_offset(sort_size const& s);
|
||||
|
|
|
|||
|
|
@ -101,7 +101,6 @@ namespace datalog {
|
|||
public:
|
||||
|
||||
dl_decl_plugin();
|
||||
~dl_decl_plugin() override {}
|
||||
|
||||
decl_plugin * mk_fresh() override { return alloc(dl_decl_plugin); }
|
||||
|
||||
|
|
|
|||
|
|
@ -27,14 +27,14 @@ Revision History:
|
|||
class i_expr_pred {
|
||||
public:
|
||||
virtual bool operator()(expr* e) = 0;
|
||||
virtual ~i_expr_pred() {}
|
||||
virtual ~i_expr_pred() = default;
|
||||
};
|
||||
|
||||
|
||||
class i_sort_pred {
|
||||
public:
|
||||
virtual bool operator()(sort* s) = 0;
|
||||
virtual ~i_sort_pred() {}
|
||||
virtual ~i_sort_pred() = default;
|
||||
};
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -52,8 +52,6 @@ namespace format_ns {
|
|||
m_line_break_ext("cr++") {
|
||||
}
|
||||
|
||||
~format_decl_plugin() override {}
|
||||
|
||||
void finalize() override {
|
||||
if (m_format_sort)
|
||||
m_manager->dec_ref(m_format_sort);
|
||||
|
|
|
|||
|
|
@ -326,12 +326,12 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl *
|
|||
}
|
||||
else if (m_fpa_util.is_to_real(f)) {
|
||||
expr_ref_vector dom(m);
|
||||
func_decl_ref to_real_i(m.mk_func_decl(fid, OP_FPA_TO_REAL_I, 0, NULL, dom.size(), dom.data()), m);
|
||||
func_decl_ref to_real_i(m.mk_func_decl(fid, OP_FPA_TO_REAL_I, 0, nullptr, dom.size(), dom.data()), m);
|
||||
expr_ref else_value(m.mk_app(to_real_i, dom.size(), dom.data()), m);
|
||||
result->set_else(else_value);
|
||||
}
|
||||
else if (m_fpa_util.is_to_ieee_bv(f)) {
|
||||
func_decl_ref to_ieee_bv_i(m.mk_func_decl(fid, OP_FPA_TO_IEEE_BV_I, 0, NULL, dom.size(), dom.data()), m);
|
||||
func_decl_ref to_ieee_bv_i(m.mk_func_decl(fid, OP_FPA_TO_IEEE_BV_I, 0, nullptr, dom.size(), dom.data()), m);
|
||||
expr_ref else_value(m.mk_app(to_ieee_bv_i, dom.size(), dom.data()), m);
|
||||
result->set_else(else_value);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -239,7 +239,6 @@ class fpa2bv_converter_wrapped : public fpa2bv_converter {
|
|||
fpa2bv_converter_wrapped(ast_manager & m, th_rewriter& rw) :
|
||||
fpa2bv_converter(m),
|
||||
m_rw(rw) {}
|
||||
virtual ~fpa2bv_converter_wrapped() {}
|
||||
void mk_const(func_decl * f, expr_ref & result) override;
|
||||
void mk_rm_const(func_decl * f, expr_ref & result) override;
|
||||
app_ref wrap(expr * e);
|
||||
|
|
|
|||
|
|
@ -39,7 +39,7 @@ protected:
|
|||
void collect_macro_candidates(quantifier* q);
|
||||
public:
|
||||
quantifier_macro_info(ast_manager& m, quantifier* q);
|
||||
virtual ~quantifier_macro_info() {}
|
||||
virtual ~quantifier_macro_info() = default;
|
||||
bool is_auf() const { return m_is_auf; }
|
||||
quantifier* get_flat_q() const { return m_flat_q; }
|
||||
bool has_cond_macros() const { return !m_cond_macros.empty(); }
|
||||
|
|
|
|||
|
|
@ -31,7 +31,7 @@ public:
|
|||
elim_term_ite_cfg(ast_manager & m, defined_names & d): m(m), m_defined_names(d) {
|
||||
// TBD enable_ac_support(false);
|
||||
}
|
||||
virtual ~elim_term_ite_cfg() {}
|
||||
virtual ~elim_term_ite_cfg() = default;
|
||||
vector<justified_expr> const& new_defs() const { return m_new_defs; }
|
||||
br_status reduce_app(func_decl* f, unsigned n, expr *const* args, expr_ref& result, proof_ref& result_pr);
|
||||
void push() { m_lim.push_back(m_new_defs.size()); }
|
||||
|
|
|
|||
|
|
@ -77,9 +77,6 @@ public:
|
|||
m_rw(m, m.proofs_enabled(), m_cfg) {
|
||||
}
|
||||
|
||||
~name_exprs_core() override {
|
||||
}
|
||||
|
||||
void operator()(expr * n, expr_ref_vector & new_defs, proof_ref_vector & new_def_proofs, expr_ref & r, proof_ref & p) override {
|
||||
m_cfg.m_def_exprs = &new_defs;
|
||||
m_cfg.m_def_proofs = &new_def_proofs;
|
||||
|
|
@ -113,9 +110,6 @@ public:
|
|||
name_exprs_core(m, n, m_pred),
|
||||
m_pred(m) {
|
||||
}
|
||||
|
||||
~name_quantifier_labels() override {
|
||||
}
|
||||
};
|
||||
|
||||
name_exprs * mk_quantifier_label_namer(ast_manager & m, defined_names & n) {
|
||||
|
|
@ -145,9 +139,6 @@ public:
|
|||
m_pred(m) {
|
||||
}
|
||||
|
||||
~name_nested_formulas() override {
|
||||
}
|
||||
|
||||
void operator()(expr * n, expr_ref_vector & new_defs, proof_ref_vector & new_def_proofs, expr_ref & r, proof_ref & p) override {
|
||||
m_pred.m_root = n;
|
||||
TRACE("name_exprs", tout << "operator()\n";);
|
||||
|
|
|
|||
|
|
@ -29,7 +29,7 @@ public:
|
|||
|
||||
class name_exprs {
|
||||
public:
|
||||
virtual ~name_exprs() {}
|
||||
virtual ~name_exprs() = default;
|
||||
virtual void operator()(expr * n, // [IN] expression that contain the sub-expressions to be named
|
||||
expr_ref_vector & new_defs, // [OUT] new definitions
|
||||
proof_ref_vector & new_def_proofs, // [OUT] proofs of the new definitions
|
||||
|
|
|
|||
|
|
@ -15,7 +15,7 @@ add_custom_command(OUTPUT "database.h"
|
|||
DEPENDS "${PROJECT_SOURCE_DIR}/scripts/mk_pat_db.py"
|
||||
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
|
||||
COMMENT "Generating \"database.h\""
|
||||
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
|
||||
USES_TERMINAL
|
||||
VERBATIM
|
||||
)
|
||||
|
||||
|
|
|
|||
|
|
@ -106,7 +106,7 @@ pattern_inference_cfg::pattern_inference_cfg(ast_manager & m, pattern_inference_
|
|||
m_params(params),
|
||||
m_bfid(m.get_basic_family_id()),
|
||||
m_afid(m.mk_family_id("arith")),
|
||||
m_le(m),
|
||||
m_le(),
|
||||
m_nested_arith_only(true),
|
||||
m_block_loop_patterns(params.m_pi_block_loop_patterns),
|
||||
m_candidates(m),
|
||||
|
|
|
|||
|
|
@ -37,7 +37,6 @@ Revision History:
|
|||
every instance of f(g(X)) is also an instance of f(X).
|
||||
*/
|
||||
class smaller_pattern {
|
||||
ast_manager & m;
|
||||
ptr_vector<expr> m_bindings;
|
||||
|
||||
typedef std::pair<expr *, expr *> expr_pair;
|
||||
|
|
@ -48,13 +47,11 @@ class smaller_pattern {
|
|||
void save(expr * p1, expr * p2);
|
||||
bool process(expr * p1, expr * p2);
|
||||
|
||||
smaller_pattern & operator=(smaller_pattern const &);
|
||||
|
||||
public:
|
||||
|
||||
smaller_pattern(ast_manager & m):
|
||||
m(m) {
|
||||
}
|
||||
smaller_pattern() = default;
|
||||
|
||||
smaller_pattern & operator=(smaller_pattern const &) = delete;
|
||||
|
||||
bool operator()(unsigned num_bindings, expr * p1, expr * p2);
|
||||
};
|
||||
|
|
|
|||
Some files were not shown because too many files have changed in this diff Show more
Loading…
Reference in a new issue