merge

Signed-off-by: Nikolaj Bjorner <[email protected]>

.dockerignore

@@ -0,0 +1,4 @@
+**/*.swp
+**/*.pyc
+.git
+**/*.Dockerfile

.gitignore

@@ -75,14 +75,3 @@ src/api/ml/z3.mllib
 *.bak
 doc/api
 doc/code
-
-# CMake files copied over by the ``contrib/cmake/boostrap.py`` script
-# See #461
-examples/CMakeLists.txt
-examples/*/CMakeLists.txt
-src/CMakeLists.txt
-src/*/CMakeLists.txt
-src/*/*/CMakeLists.txt
-src/*/*/*/CMakeLists.txt
-src/api/dotnet/cmake_install_gac.cmake.in
-src/api/dotnet/cmake_uninstall_gac.cmake.in

.travis.yml

@@ -0,0 +1,68 @@
+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 16.04 LTS
+###############################################################################
+    # 64-bit GCC 5.4 RelWithDebInfo
+    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo
+    # 64-bit Clang 3.9 RelWithDebInfo
+    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo
+
+    # 64-bit GCC 5.4 Debug
+    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug
+    # 64-bit Clang Debug
+    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug
+
+    # 32-bit GCC 5.4 RelWithDebInfo
+    - LINUX_BASE=ubuntu32_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=i686 Z3_BUILD_TYPE=RelWithDebInfo
+
+    # Both of the two configurations below build the docs because the current
+    # implementation uses python as part of the building process.
+    # TODO: Teach one of the configurations to upload built docs somewhere.
+    # Test with Python 3 and API docs
+    - LINUX_BASE=ubuntu_16.04 PYTHON_EXECUTABLE=/usr/bin/python3 BUILD_DOCS=1
+    # Test with LibGMP and API docs
+    - LINUX_BASE=ubuntu_16.04 TARGET_ARCH=x86_64 USE_LIBGMP=1 BUILD_DOCS=1 PYTHON_EXECUTABLE=/usr/bin/python2.7
+
+    # Test without OpenMP
+    - 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 USE_OPENMP=0
+
+    # Unix Makefile generator build
+    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_CMAKE_GENERATOR="Unix Makefiles"
+
+    # LTO build
+    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 USE_LTO=1
+
+    # Static build. Note we have disable building the bindings because they won't work with a static libz3
+    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_STATIC_BUILD=1 DOTNET_BINDINGS=0 JAVA_BINDINGS=0 PYTHON_BINDINGS=0
+
+###############################################################################
+# Ubuntu 14.04 LTS
+###############################################################################
+    # GCC 4.8
+    # 64-bit GCC 4.8 RelWithDebInfo
+    - LINUX_BASE=ubuntu_14.04 C_COMPILER=/usr/bin/gcc-4.8 CXX_COMPILER=/usr/bin/g++-4.8 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo
+    # 64-bit GCC 4.8 Debug
+    - LINUX_BASE=ubuntu_14.04 C_COMPILER=/usr/bin/gcc-4.8 CXX_COMPILER=/usr/bin/g++-4.8 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug
+
+# TODO: OSX support
+#matrix:
+#  include:
+#    - os: osx
+#      osx_image: xcode 8.2
+script:
+  - contrib/ci/scripts/travis_ci_entry_point.sh

CMakeLists.txt

@@ -14,19 +14,21 @@ if (POLICY CMP0054)
   cmake_policy(SET CMP0054 OLD)
 endif()
 
-# Provide a friendly message if the user hasn't run the bootstrap script
-# to copy all the CMake files into their correct location.
-# It is unfortunate that we have to do this, see #461 for the discussion
-# on this.
-if (NOT (EXISTS "${CMAKE_SOURCE_DIR}/src/CMakeLists.txt"))
-  message(FATAL_ERROR "Cannot find \"${CMAKE_SOURCE_DIR}/src/CMakeLists.txt\""
-          ". This probably means you need to run"
-          "``python contrib/cmake/bootstrap.py create``")
+if (POLICY CMP0042)
+  # Enable `MACOSX_RPATH` by default.
+  cmake_policy(SET CMP0042 NEW)
 endif()
 
 set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
 project(Z3 CXX)
 
+if ("${CMAKE_VERSION}" VERSION_LESS "3.4")
+  # FIXME: Drop this when we upgrade to newer CMake versions.
+  # HACK: Although we don't need C language support if it is not
+  # enabled CMake's `FindThreads` module fails in old CMake versions.
+  enable_language(C)
+endif()
+
 ################################################################################
 # Project version
 ################################################################################
@@ -107,7 +109,7 @@ if (EXISTS "${GIT_DIR}")
       endif()
       message(STATUS "Using Git hash in version output: ${Z3GITHASH}")
       # This mimics the behaviour of the old build system.
-      string(APPEND Z3_FULL_VERSION_STR " ${Z3GITHASH}")
+      set(Z3_FULL_VERSION_STR "${Z3_FULL_VERSION_STR} ${Z3GITHASH}")
     else()
       message(STATUS "Not using Git hash in version output")
       unset(Z3GITHASH) # Used in configure_file()
@@ -120,7 +122,7 @@ if (EXISTS "${GIT_DIR}")
       endif()
       message(STATUS "Using Git description in version output: ${Z3_GIT_DESCRIPTION}")
       # This mimics the behaviour of the old build system.
-      string(APPEND Z3_FULL_VERSION_STR " ${Z3_GIT_DESCRIPTION}")
+      set(Z3_FULL_VERSION_STR "${Z3_FULL_VERSION_STR} ${Z3_GIT_DESCRIPTION}")
     else()
       message(STATUS "Not including git descrption in version")
     endif()
@@ -274,18 +276,6 @@ else()
   message(STATUS "Not using libgmp")
 endif()
 
-################################################################################
-# FOCI2 support
-################################################################################
-# FIXME: What is this?
-option(USE_FOCI2 "Use FOCI2" OFF)
-if (USE_FOCI2)
-  message(FATAL_ERROR "TODO")
-  message(STATUS "Using FOCI2")
-else()
-  message(STATUS "Not using FOCI2")
-endif()
-
 ################################################################################
 # OpenMP support
 ################################################################################
@@ -318,6 +308,23 @@ else()
   set(USE_OPENMP OFF CACHE BOOL "Use OpenMP" FORCE)
 endif()
 
+################################################################################
+# API Log sync
+################################################################################
+option(API_LOG_SYNC
+  "Use locking when logging Z3 API calls (experimental)"
+  OFF
+)
+if (API_LOG_SYNC)
+  if (NOT USE_OPENMP)
+    message(FATAL_ERROR "API_LOG_SYNC feature requires OpenMP")
+  endif()
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-DZ3_LOG_SYNC")
+  message(STATUS "Using API_LOG_SYNC")
+else()
+  message(STATUS "Not using API_LOG_SYNC")
+endif()
+
 ################################################################################
 # FP math
 ################################################################################
@@ -517,10 +524,18 @@ add_subdirectory(src)
 # use Z3 via CMake.
 ################################################################################
 include(CMakePackageConfigHelpers)
-export(EXPORT Z3_EXPORTED_TARGETS
-  NAMESPACE z3::
-  FILE "${CMAKE_BINARY_DIR}/Z3Targets.cmake"
-)
+if ("${CMAKE_VERSION}" VERSION_LESS "3.0")
+  # FIXME: Remove this once we drop support for CMake 2.8.12
+  export(TARGETS libz3
+    NAMESPACE z3::
+    FILE "${CMAKE_BINARY_DIR}/Z3Targets.cmake"
+  )
+else()
+  export(EXPORT Z3_EXPORTED_TARGETS
+    NAMESPACE z3::
+    FILE "${CMAKE_BINARY_DIR}/Z3Targets.cmake"
+  )
+endif()
 set(Z3_FIRST_PACKAGE_INCLUDE_DIR "${CMAKE_BINARY_DIR}/src/api")
 set(Z3_SECOND_PACKAGE_INCLUDE_DIR "${CMAKE_SOURCE_DIR}/src/api")
 set(Z3_CXX_PACKAGE_INCLUDE_DIR "${CMAKE_SOURCE_DIR}/src/api/c++")
@@ -533,7 +548,6 @@ configure_package_config_file("${CMAKE_SOURCE_DIR}/cmake/Z3Config.cmake.in"
     Z3_FIRST_PACKAGE_INCLUDE_DIR
     Z3_SECOND_PACKAGE_INCLUDE_DIR
     Z3_CXX_PACKAGE_INCLUDE_DIR
-  INSTALL_PREFIX "${CMAKE_BINARY_DIR}"
 )
 unset(Z3_FIRST_PACKAGE_INCLUDE_DIR)
 unset(Z3_SECOND_PACKAGE_INCLUDE_DIR)

README-CMake.md

@@ -1,4 +1,4 @@
-    # Z3's CMake build system
+# Z3's CMake build system
 
 [CMake](https://cmake.org/) is a "meta build system" that reads a description
 of the project written in the ``CMakeLists.txt`` files and emits a build
@@ -33,34 +33,6 @@ git clean -fx src
 
 which will remove the generated source files.
 
-### Bootstrapping
-
-Most of Z3's CMake files do not live in their correct location. Instead those
-files live in the ``contrib/cmake`` folder and a script is provided that will
-copy (or hard link) the files into their correct location.
-
-To copy the files run
-
-```
-python contrib/cmake/bootstrap.py create
-```
-
-in the root of the repository. Once you have done this you can now build Z3 using CMake.
-Make sure you remember to rerun this command if you pull down new code/rebase/change branch so
-that the copied CMake files are up to date.
-
-To remove the copied files run
-
-```
-python contrib/cmake/bootstrap.py remove
-```
-
-Note if you plan to do development on Z3 you should read the developer
-notes on bootstrapping in this document.
-
-What follows is a brief walk through of how to build Z3 using some
-of the more commonly used CMake generators.
-
 ### Unix Makefiles
 
 Run the following in the top level directory of the Z3 repository.
@@ -293,6 +265,9 @@ The following useful options can be passed to CMake whilst configuring.
 * ``ALWAYS_BUILD_DOCS`` - BOOL. If set to ``TRUE`` and ``BUILD_DOCUMENTATION`` is ``TRUE`` then documentation for API bindings will always be built.
     Disabling this is useful for faster incremental builds. The documentation can be manually built by invoking the ``api_docs`` target.
 * ``LINK_TIME_OPTIMIZATION`` - BOOL. If set to ``TRUE`` link time optimization will be enabled.
+* ``API_LOG_SYNC`` - BOOL. If set to ``TRUE`` will enable experimental API log sync feature.
+* ``WARNINGS_AS_ERRORS`` - STRING. If set to ``TRUE`` compiler warnings will be treated as errors. If set to ``False`` compiler warnings will not be treated as errors.
+    If set to ``SERIOUS_ONLY`` a subset of compiler warnings will be treated as errors.
 
 On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface.
 
@@ -327,44 +302,6 @@ link is not created when building under Windows.
 
 These notes are help developers and packagers of Z3.
 
-### Boostrapping the CMake build
-
-Z3's CMake system is experimental and not officially supported. Consequently
-Z3's developers have decided that they do not want the CMake files in the
-``src/`` and ``examples/`` folders. Instead the ``contrib/cmake/bootstrap.py``
-script copies or hard links them into the correct locations. For context
-on this decision see https://github.com/Z3Prover/z3/pull/461 .
-
-The ``contrib/cmake/bootstrap.py create`` command just copies over files which makes
-development harder because you have to copy your modifications over to the
-files in ``contrib/cmake`` for your changes to committed to git. If you are on a UNIX like
-platform you can create hard links instead by running
-
-```
-contrib/cmake/boostrap.py create --hard-link
-```
-
-Using hard links means that modifying any of the "copied" files also modifies the
-file under version control. Using hard links also means that the file modification time
-will appear correct (i.e. the hard-linked "copies" have the same file modification time
-as the corresponding file under version control) which means CMake will correctly reconfigure
-when invoked. This is why using symbolic links is not an option because the file modification
-time of a symbolic link is not the same as the file modification of the file being pointed to.
-
-Unfortunately a downside to using hard links (or just plain copies) is that if
-you pull down new code (i.e. ``git pull``) then some of the CMake files under
-version control may change but the corresponding hard-linked "copies" will not.
-
-This mean that (regardless of whether or not you use hard links) every time you
-pull down new code or change branch or do an interactive rebase you must run
-(with or without ``--hard-link``):
-
-```
-contrb/cmake/boostrap.py create
-```
-
-in order to be sure that the copied CMake files are not out of date.
-
 ### Install/Uninstall
 
 Install and uninstall targets are supported. Use ``CMAKE_INSTALL_PREFIX`` to
@@ -446,3 +383,13 @@ It is tempting use file-globbing in ``CMakeLists.txt`` to find a set for files m
 use them as the sources to build a target. This however is a bad idea because it prevents CMake from knowing when it needs to rerun itself. This is why source file names are explicitly listed in the ``CMakeLists.txt`` so that when changes are made the source files used to build a target automatically triggers a rerun of CMake.
 
 Long story short. Don't use file globbing.
+
+### Serious warning flags
+
+By default the `WARNINGS_AS_ERRORS` flag is set to `SERIOUS_ONLY` which means
+some warnings will be treated as errors. These warnings are controlled by the
+relevant `*_WARNINGS_AS_ERRORS` list defined in
+`cmake/compiler_warnings.cmake`.
+
+Additional warnings should only be added here if the warnings has no false
+positives.

README.md

@@ -12,9 +12,9 @@ See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z
 
 ## Build status
 
-| Windows x86 | Windows x64 | Ubuntu x64 | Ubuntu x86 | Debian x64 | OSX |
-| ----------- | ----------- | ---------- | ---------- | ---------- | --- |
-![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge) | ![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge) | ![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge) | ![ubuntu-x86-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/6/badge) | ![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge) | ![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge)
+| Windows x86 | Windows x64 | Ubuntu x64 | Ubuntu x86 | Debian x64 | OSX | TravisCI |
+| ----------- | ----------- | ---------- | ---------- | ---------- | --- | -------- |
+[![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=4) | [![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=7) | [![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=3) | [![ubuntu-x86-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/6/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=6) | [![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=5) | [![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3)
 
 [1]: #building-z3-on-windows-using-visual-studio-command-prompt
 [2]: #building-z3-using-make-and-gccclang

RELEASE_NOTES

@@ -1,5 +1,15 @@
 RELEASE NOTES
 
+Version 4.5.x
+=============
+- New features (including):
+  - A new string solver from University of Waterloo
+  - A new linear real arithmetic solver
+  - Changed behavior for optimization commands from the SMT2 command-line interface.
+    Objective values are no longer printed by default. They can be retrieved by
+    issuing the command (get-objectives). Pareto front objectives are accessed by
+    issuing multiple (check-sat) calls until it returns unsat.
+
 Version 4.5.0
 =============