Merge branch 'master' into HEAD

Author: arifogel

.gitignore

@@ -43,6 +43,7 @@ bld_dbg/*
 bld_rel/*
 bld_dbg_x64/*
 bld_rel_x64/*
+.vscode
 # Auto generated files.
 config.log
 config.status
@@ -75,3 +76,6 @@ src/api/ml/z3.mllib
 *.bak
 doc/api
 doc/code
+.vs
+examples/**/obj
+CMakeSettings.json

.travis.yml

@@ -17,14 +17,18 @@ env:
 ###############################################################################
 # Ubuntu 16.04 LTS
 ###############################################################################
-    # 64-bit default compilers RelWithDebInfo
-    - LINUX_BASE=ubuntu_16.04 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Release JAVA_BINDINGS=1
+    # 64-bit default compilers Release
+    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Release JAVA_BINDINGS=1
+    # 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 RUN_UNIT_TESTS=BUILD_ONLY
 
 ###############################################################################
 # Ubuntu 14.04 LTS
 ###############################################################################
-    # 64-bit GCC 4.8 RelWithDebInfo java
-    - LINUX_BASE=ubuntu_14.04 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Release JAVA_BINDINGS=1
+    # 64-bit GCC 4.8 Release java
+    - 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=Release JAVA_BINDINGS=1
+    # 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 RUN_UNIT_TESTS=BUILD_ONLY
 
 # macOS (a.k.a OSX) support
 matrix:
@@ -33,11 +37,11 @@ matrix:
     # very slow so we should keep the number of configurations we test on this
     # OS to a minimum.
     - os: osx
-      osx_image: xcode9.2
-      env: Z3_BUILD_TYPE=Release USE_OPENMP=1 JAVA_BINDINGS=1
+      osx_image: xcode10.1
+      env: Z3_BUILD_TYPE=Release USE_OPENMP=1 JAVA_BINDINGS=1 DOTNET_BINDINGS=0
     - os: osx
-      osx_image: xcode9.2
-      env: Z3_BUILD_TYPE=Release USE_OPENMP=0 JAVA_BINDINGS=1
+      osx_image: xcode10.1
+      env: Z3_BUILD_TYPE=Release USE_OPENMP=0 JAVA_BINDINGS=1 DOTNET_BINDINGS=0
 script:
   # Use `travis_wait` when doing LTO builds because this configuration will
   # have long link times during which it will not show any output which

CMakeLists.txt

@@ -33,8 +33,8 @@ endif()
 # Project version
 ################################################################################
 set(Z3_VERSION_MAJOR 4)
-set(Z3_VERSION_MINOR 6)
-set(Z3_VERSION_PATCH 1)
+set(Z3_VERSION_MINOR 8)
+set(Z3_VERSION_PATCH 5)
 set(Z3_VERSION_TWEAK 0)
 set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}")
 set(Z3_FULL_VERSION_STR "${Z3_VERSION}") # Note this might be modified
@@ -99,7 +99,7 @@ set(GIT_DIR "${CMAKE_SOURCE_DIR}/.git")
 if (EXISTS "${GIT_DIR}")
   # Try to make CMake configure depend on the current git HEAD so that
   # a re-configure is triggered when the HEAD changes.
-  add_git_dir_dependency("${GIT_DIR}" ADD_GIT_DEP_SUCCESS)
+  add_git_dir_dependency("${CMAKE_SOURCE_DIR}" ADD_GIT_DEP_SUCCESS)
   if (ADD_GIT_DEP_SUCCESS)
     if (INCLUDE_GIT_HASH)
       get_git_head_hash("${GIT_DIR}" Z3GITHASH)
@@ -205,9 +205,6 @@ message(STATUS "PYTHON_EXECUTABLE: ${PYTHON_EXECUTABLE}")
 include(${CMAKE_SOURCE_DIR}/cmake/target_arch_detect.cmake)
 detect_target_architecture(TARGET_ARCHITECTURE)
 message(STATUS "Detected target architecture: ${TARGET_ARCHITECTURE}")
-if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64")
-  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_AMD64_")
-endif()
 
 
 ################################################################################
@@ -218,12 +215,17 @@ include(${CMAKE_SOURCE_DIR}/cmake/z3_add_cxx_flag.cmake)
 ################################################################################
 # C++ language version
 ################################################################################
-# FIXME: Use CMake's own mechanism for selecting language version
-if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang"))
-  z3_add_cxx_flag("-std=c++11" REQUIRED)
-else()
-  message(AUTHOR_WARNING "Not setting C++ language version for compiler")
-endif()
+if ("${CMAKE_VERSION}" VERSION_LESS "3.1")
+  # FIXME: Drop this when we upgrade to newer CMake versions.
+  if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang"))
+    z3_add_cxx_flag("-std=c++11" REQUIRED)
+  else()
+    message(AUTHOR_WARNING "Not setting C++ language version for compiler")
+  endif()
+else ()
+  set(CMAKE_CXX_STANDARD 11)
+  set(CMAKE_CXX_STANDARD_REQUIRED ON)
+endif ()
 
 ################################################################################
 # Platform detection
@@ -235,11 +237,14 @@ if ("${CMAKE_SYSTEM_NAME}" STREQUAL "Linux")
     list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_USE_THREAD_LOCAL")
   endif()
 elseif ("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin")
-  # Does OSX really not need any special flags?
+  # Does macOS really not need any special flags?
   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_")
@@ -249,6 +254,15 @@ elseif (CYGWIN)
 elseif (WIN32)
   message(STATUS "Platform: Windows")
   list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_WINDOWS")
+elseif (EMSCRIPTEN)
+  message(STATUS "Platform: Emscripten")
+  list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS
+    "-Os"
+    "-s ALLOW_MEMORY_GROWTH=1"
+    "-s ASSERTIONS=0"
+    "-s DISABLE_EXCEPTION_CATCHING=0"
+    "-s ERROR_ON_UNDEFINED_SYMBOLS=1"
+  )
 else()
   message(FATAL_ERROR "Platform \"${CMAKE_SYSTEM_NAME}\" not recognised")
 endif()
@@ -372,9 +386,17 @@ 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"))
+  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")
     # FIXME: Remove "x.." when CMP0054 is set to NEW
+  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 ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
     set(SSE_FLAGS "/arch:SSE2")
   else()
@@ -409,6 +431,29 @@ list(APPEND Z3_DEPENDENT_LIBS ${CMAKE_THREAD_LIBS_INIT})
 ################################################################################
 include(${CMAKE_SOURCE_DIR}/cmake/compiler_warnings.cmake)
 
+################################################################################
+# Save Clang optimization records
+################################################################################
+option(SAVE_CLANG_OPTIMIZATION_RECORDS "Enable saving Clang optimization records." OFF)
+
+if (SAVE_CLANG_OPTIMIZATION_RECORDS)
+  z3_add_cxx_flag("-fsave-optimization-record" REQUIRED)
+endif()
+
+################################################################################
+# If using Ninja, force color output for Clang (and gcc, disabled to check build).
+################################################################################
+if (UNIX AND CMAKE_GENERATOR STREQUAL "Ninja")
+  if (CMAKE_CXX_COMPILER_ID STREQUAL "Clang")
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fcolor-diagnostics")
+    set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -fcolor-diagnostics")
+  endif()
+#  if (CMAKE_CXX_COMPILER_ID STREQUAL "GNU")
+#    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fdiagnostics-color")
+#    set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -fdiagnostics-color")
+#  endif()
+endif()
+
 ################################################################################
 # Option to control what type of library we build
 ################################################################################
@@ -434,7 +479,7 @@ else()
 endif()
 
 ################################################################################
-# Postion independent code
+# Position independent code
 ################################################################################
 # This is required because code built in the components will end up in a shared
 # library. If not building a shared library ``-fPIC`` isn't needed and would add

README.md

@@ -5,16 +5,25 @@ under the [MIT license](LICENSE.txt).
 
 If you are not familiar with Z3, you can start [here](https://github.com/Z3Prover/z3/wiki#background).
 
+Pre-built binaries for releases are available from [here](https://github.com/Z3Prover/z3/releases), 
+and nightly builds from [here](https://github.com/Z3Prover/bin/tree/master/nightly).
+
 Z3 can be built using [Visual Studio][1], a [Makefile][2] or using [CMake][3]. It provides
-[bindings for several programming languages][4].
+[bindings for several programming languages][4]. 
 
 See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z3.
 
 ## Build status
 
+<<<<<<< HEAD
 | Windows x86 | Windows x64 | Ubuntu x64 | 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) | [![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) ![Analytics](https://ga-beacon.appspot.com/UA-100596389-3/open-source/?pixel&useReferer)
+=======
+| Windows x64 | Windows x86 | Windows x64 | Ubuntu x64 | Debian x64 | macOS | TravisCI |
+| ----------- | ----------- | ----------- | ---------- | ---------- | ----- | -------- |
+[![win64-badge](https://z3build.visualstudio.com/_apis/public/build/definitions/2e0aa542-a22c-4b1a-8dcd-3ebae8e12db4/4/badge)](https://z3build.visualstudio.com/Z3Build/_build/index?definitionId=4) | [![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) | [![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) | [![Build status](https://cz3.visualstudio.com/Z3/_apis/build/status/OSX)](https://cz3.visualstudio.com/Z3/_build/latest?definitionId=2) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3)
+>>>>>>> master
 
 [1]: #building-z3-on-windows-using-visual-studio-command-prompt
 [2]: #building-z3-using-make-and-gccclang
@@ -75,7 +84,7 @@ A 32 bit build should work similarly (but is untested); the same is true for 32/
 By default, it will install z3 executable at ``PREFIX/bin``, libraries at
 ``PREFIX/lib``, and include files at ``PREFIX/include``, where ``PREFIX``
 installation prefix if inferred by the ``mk_make.py`` script. It is usually
-``/usr`` for most Linux distros, and ``/usr/local`` for FreeBSD and OSX. Use
+``/usr`` for most Linux distros, and ``/usr/local`` for FreeBSD and macOS. Use
 the ``--prefix=`` command line option to change the install prefix. For example:
 
 ```bash
@@ -189,3 +198,6 @@ python -c 'import z3; print(z3.get_version_string())'
 
 See [``examples/python``](examples/python) for examples.
 
+### ``Web Assembly``
+
+[WebAssembly](https://github.com/cpitclaudel/z3.wasm) bindings are provided by Clément Pit-Claudel.