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

.github/workflows/android-build.yml

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

.github/workflows/docker-image.yml

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

CMakeLists.txt

@@ -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")
+if (CMAKE_SYSTEM_NAME STREQUAL "Darwin")
-  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 (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
 )
 

README.md

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

RELEASE_NOTES.md

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

cmake/z3_add_component.cmake

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

contrib/.travis.yml

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

contrib/ci/Dockerfiles/z3_base_ubuntu_20.04.Dockerfile

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

contrib/ci/Dockerfiles/z3_build.Dockerfile

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

contrib/ci/README.md

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

contrib/ci/maintainers.txt

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

contrib/ci/scripts/build_z3_cmake.sh

@@ -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[@]}"

contrib/ci/scripts/ci_defaults.sh

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

contrib/ci/scripts/install_deps_osx.sh

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

contrib/ci/scripts/run_quiet.sh

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

contrib/ci/scripts/sanitizer_env.sh

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

contrib/ci/scripts/set_compiler_flags.sh

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

contrib/ci/scripts/set_generator_args.sh

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

contrib/ci/scripts/test_z3_docs.sh

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

contrib/ci/scripts/test_z3_examples_cmake.sh

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

contrib/ci/scripts/test_z3_install_cmake.sh

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

contrib/ci/scripts/test_z3_system_tests.sh

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

contrib/ci/scripts/test_z3_unit_tests_cmake.sh

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

contrib/ci/scripts/travis_ci_entry_point.sh

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

contrib/ci/scripts/travis_ci_linux_entry_point.sh

@@ -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[@]}" \
-  .

contrib/ci/scripts/travis_ci_osx_entry_point.sh

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

contrib/cmake/bootstrap.py

@@ -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:]))

contrib/cmake/maintainers.txt

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

contrib/cmake/src/test/lp/CMakeLists.txt

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

doc/CMakeLists.txt

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

doc/website.dox.in

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

doc/z3api.cfg.in

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

doc/z3code.dox

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

examples/CMakeLists.txt

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

examples/c++/example.cpp

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

examples/python/simplify_formula.py

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

examples/tptp/tptp5.cpp

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

examples/userPropagator/CMakeLists.txt

@@ -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}")

scripts/mk_project.py

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

scripts/mk_unix_dist.py

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

scripts/mk_util.py

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

scripts/nightly.yaml

@@ -1,8 +1,8 @@
 variables:
 
   Major: '4'
-  Minor: '9'
+  Minor: '11'
-  Patch: '2'
+  Patch: '0'
   NightlyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)-$(Build.DefinitionName)
 
 stages:

scripts/release.yml

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

scripts/update_api.py

@@ -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:
+            except Exception as e:
-                raise mk_exec_header.MKException("Failed to process API definition: %s" % line)
+                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

src/CMakeLists.txt

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

src/ackermannization/ackermannize_bv_tactic.cpp

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

src/ackermannization/ackr_model_converter.cpp

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

src/ackermannization/lackr_model_converter_lazy.cpp

@@ -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());

src/api/CMakeLists.txt

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

src/api/api_algebraic.cpp

@@ -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());

src/api/api_ast_vector.h

@@ -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); }

src/api/api_config_params.cpp

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

src/api/api_context.h

@@ -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"));
             }

src/api/api_datalog.cpp

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

src/api/api_goal.h

@@ -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); }

src/api/api_model.h

@@ -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); }

src/api/api_numeral.cpp

@@ -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
+
 };

src/api/api_parsers.cpp

@@ -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); }

src/api/api_solver.cpp

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

src/api/api_solver.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);

src/api/api_stats.h

@@ -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); }

src/api/api_tactic.h

@@ -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); }

src/api/api_util.h

@@ -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();

src/api/c++/z3++.h

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

src/api/dotnet/CMakeLists.txt

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

src/api/dotnet/Context.cs

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

src/api/java/CMakeLists.txt

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

src/api/js/PUBLISHED_README.md

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

src/api/js/scripts/parse-api.ts

@@ -16,7 +16,6 @@ const files = [
 
 const aliases = {
   __proto__: null,
-  Z3_bool: 'boolean',
   Z3_string: 'string',
   bool: 'boolean',
   signed: 'int',

src/api/js/src/high-level/high-level.ts

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

src/api/js/src/jest.ts

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

src/api/julia/z3jl.cpp

@@ -1,4 +1,5 @@
 #include "jlcxx/jlcxx.hpp"
+#include <sstream>
 #include "z3++.h"
 
 using namespace z3;

src/api/python/CMakeLists.txt

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

src/api/python/setup.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:

src/api/python/z3/z3.py

@@ -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)
+    prop = _prop_closures.get(ctx)
-    new_prop = prop.fresh()
+    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.fresh_ctx = ctx
-            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)
         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:
+        if self.fresh_ctx:
-            return self._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):
+    def conflict(self, deps = [], eqs = []):
-        self.propagate(BoolVal(False, self.ctx()), deps, eqs=[])
+        self.propagate(BoolVal(False, self.ctx()), deps, eqs)

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.

src/api/z3_logger.h

@@ -16,6 +16,8 @@ Author:
 Notes:
     
 --*/
+#pragma once
+
 #include "util/symbol.h"
 
 void R();

src/api/z3_macros.h

@@ -3,7 +3,7 @@
 Copyright (c) 2015 Microsoft Corporation
 
 --*/
-
+#pragma once
 
 #ifndef Z3_API
 # ifdef __GNUC__

src/ast/array_decl_plugin.h

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

src/ast/ast.cpp

@@ -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) {
+        for (ast * n : m_ast_table) 
-            if (!mark.is_marked(n)) {
+            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_VERBOSE(1, 
-                if (is_sort(a)) {
+                           verbose_stream() << "Leaked: ";
-                    std::cout << to_sort(a)->get_name() << "\n";
+                           if (is_sort(a)) 
-                }
+                               verbose_stream() << to_sort(a)->get_name() << "\n";
-                else {
+                           else 
-                    std::cout << mk_ll_pp(a, *this, false) << "id: " << a->get_id() << "\n";
+                               verbose_stream() << mk_ll_pp(a, *this, false) << "id: " << a->get_id() << "\n";
-                });
+                           ););
             a->m_ref_count = 0;
             delete_node(a);
         }

src/ast/ast.h

@@ -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();

src/ast/ast_pp_util.cpp

@@ -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);
 }

src/ast/ast_pp_util.h

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

src/ast/ast_printer.cpp

@@ -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); }

src/ast/ast_printer.h

@@ -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();

src/ast/ast_smt2_pp.h

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

src/ast/bv_decl_plugin.h

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

src/ast/datatype_decl_plugin.h

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

src/ast/dl_decl_plugin.h

@@ -101,7 +101,6 @@ namespace datalog {
     public:
 
         dl_decl_plugin();
-        ~dl_decl_plugin() override {}
 
         decl_plugin * mk_fresh() override { return alloc(dl_decl_plugin); }
         

src/ast/expr_functors.h

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

src/ast/format.cpp

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

src/ast/fpa/bv2fpa_converter.cpp

@@ -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);
         }

src/ast/fpa/fpa2bv_converter.h

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

src/ast/macros/quantifier_macro_info.h

@@ -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(); }

src/ast/normal_forms/elim_term_ite.h

@@ -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()); }

src/ast/normal_forms/name_exprs.cpp

@@ -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";);

src/ast/normal_forms/name_exprs.h

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

src/ast/pattern/CMakeLists.txt

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

src/ast/pattern/pattern_inference.cpp

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

src/ast/pattern/pattern_inference.h

@@ -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):
+    smaller_pattern() = default;
-        m(m) {
+
-    }
+    smaller_pattern & operator=(smaller_pattern const &) = delete;
 
     bool operator()(unsigned num_bindings, expr * p1, expr * p2);
 };