remove deprecated USE_OPENMP, rename API_LOG_SYNC to Z3_API_LOG_SYNC …

…(tiny part of Z3Prover#2709) Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
VeriFIT · Nov 19, 2019 · 3ab9a1c · 3ab9a1c
1 parent 3729458
commit 3ab9a1c
Show file tree

Hide file tree

Showing 8 changed files with 6 additions and 22 deletions.
diff --git a/.travis.yml b/.travis.yml
@@ -54,9 +54,6 @@ env:
     # 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"
 
@@ -83,8 +80,7 @@ matrix:
     # OS to a minimum.
     - os: osx
       osx_image: xcode8.3
-      # Note: Apple Clang does not support OpenMP
-      env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0 DOTNET_BINDINGS=0
+      env: Z3_BUILD_TYPE=RelWithDebInfo 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

diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -259,13 +259,13 @@ endif()
 ################################################################################
 # API Log sync
 ################################################################################
-option(API_LOG_SYNC
+option(Z3_API_LOG_SYNC
   "Use locking when logging Z3 API calls (experimental)"
   OFF
 )
-if (API_LOG_SYNC)
+if (Z3_API_LOG_SYNC)
   list(APPEND Z3_COMPONENT_CXX_DEFINES "-DZ3_LOG_SYNC")
-  message(STATUS "Using API_LOG_SYNC")
+  message(STATUS "Using Z3_API_LOG_SYNC")
 else()
   message(STATUS "Not using API_LOG_SYNC")
 endif()

diff --git a/README-CMake.md b/README-CMake.md
@@ -244,7 +244,6 @@ The following useful options can be passed to CMake whilst configuring.
 * ``ENABLE_TRACING_FOR_NON_DEBUG`` - BOOL. If set to ``TRUE`` enable tracing in non-debug builds, if set to ``FALSE`` disable tracing in non-debug builds. Note in debug builds tracing is always enabled.
 * ``BUILD_LIBZ3_SHARED`` - BOOL. If set to ``TRUE`` build libz3 as a shared library otherwise build as a static library.
 * ``ENABLE_EXAMPLE_TARGETS`` - BOOL. If set to ``TRUE`` add the build targets for building the API examples.
-* ``USE_OPENMP`` - BOOL. If set to ``TRUE`` and OpenMP support is detected build with OpenMP support.
 * ``USE_LIB_GMP`` - BOOL. If set to ``TRUE`` use the GNU multiple precision library. If set to ``FALSE`` use an internal implementation.
 * ``PYTHON_EXECUTABLE`` - STRING. The python executable to use during the build.
 * ``BUILD_PYTHON_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's python bindings will be built.
@@ -267,7 +266,7 @@ The following useful options can be passed to CMake whilst configuring.
 * ``LINK_TIME_OPTIMIZATION`` - BOOL. If set to ``TRUE`` link time optimization will be enabled.
 * ``ENABLE_CFI`` - BOOL. If set to ``TRUE`` will enable Control Flow Integrity security checks. This is only supported by MSVC and Clang and will
     fail on other compilers. This requires LINK_TIME_OPTIMIZATION to also be enabled.
-* ``API_LOG_SYNC`` - BOOL. If set to ``TRUE`` will enable experimental API log sync feature.
+* ``Z3_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.
 * ``Z3_C_EXAMPLES_FORCE_CXX_LINKER`` - BOOL. If set to ``TRUE`` the C API examples will request that the C++ linker is used rather than the C linker.

diff --git a/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile
@@ -23,7 +23,6 @@ ARG TEST_INSTALL
 ARG UBSAN_BUILD
 ARG USE_LIBGMP
 ARG USE_LTO
-ARG USE_OPENMP
 ARG Z3_SRC_DIR=/home/user/z3_src
 ARG Z3_BUILD_TYPE
 ARG Z3_CMAKE_GENERATOR
@@ -53,7 +52,6 @@ ENV \
   UBSAN_BUILD=${UBSAN_BUILD} \
   USE_LIBGMP=${USE_LIBGMP} \
   USE_LTO=${USE_LTO} \
-  USE_OPENMP=${USE_OPENMP} \
   Z3_SRC_DIR=${Z3_SRC_DIR} \
   Z3_BUILD_DIR=/home/user/z3_build \
   Z3_BUILD_TYPE=${Z3_BUILD_TYPE} \

diff --git a/contrib/ci/README.md b/contrib/ci/README.md
@@ -39,7 +39,6 @@ the future.
 * `UBSAN_BUILD` - Do [UndefinedBehaviourSanitizer](https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html) build (`0` or `1`)
 * `USE_LIBGMP` - Use [GNU multiple precision library](https://gmplib.org/) (`0` or `1`)
 * `USE_LTO` - Link binaries using link time optimization (`0` or `1`)
-* `USE_OPENMP` - Use OpenMP (`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`)
@@ -133,16 +132,14 @@ To reproduce a build (e.g. like the one shown below)
 ```yaml
 - os: osx
   osx_image: xcode8.3
-  # Note: Apple Clang does not support OpenMP
-  env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0
+  env: Z3_BUILD_TYPE=RelWithDebInfo 
 ```
 
 Run the following:
 
 ```bash
 TRAVIS_BUILD_DIR=$(pwd) \
 Z3_BUILD_TYPE=RelWithDebInfo \
-USE_OPEN_MP=0 \
 contrib/ci/scripts/travis_ci_osx_entry_point.sh
 ```
 

diff --git a/contrib/ci/scripts/build_z3_cmake.sh b/contrib/ci/scripts/build_z3_cmake.sh
@@ -12,7 +12,6 @@ set -o pipefail
 : ${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"}
-: ${USE_OPENMP?"USE_OPENMP must be specified"}
 : ${USE_LIBGMP?"USE_LIBGMP must be specified"}
 : ${BUILD_DOCS?"BUILD_DOCS must be specified"}
 : ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"}

diff --git a/contrib/ci/scripts/ci_defaults.sh b/contrib/ci/scripts/ci_defaults.sh
@@ -21,7 +21,6 @@ export TEST_INSTALL="${TEST_INSTALL:-1}"
 export UBSAN_BUILD="${UBSAN_BUILD:-0}"
 export USE_LIBGMP="${USE_LIBGMP:-0}"
 export USE_LTO="${USE_LTO:-0}"
-export USE_OPENMP="${USE_OPENMP:-1}"
 
 export Z3_BUILD_TYPE="${Z3_BUILD_TYPE:-RelWithDebInfo}"
 export Z3_CMAKE_GENERATOR="${Z3_CMAKE_GENERATOR:-Ninja}"

diff --git a/contrib/ci/scripts/travis_ci_linux_entry_point.sh b/contrib/ci/scripts/travis_ci_linux_entry_point.sh
@@ -30,10 +30,6 @@ if [ -n "${Z3_CMAKE_GENERATOR}" ]; then
   BUILD_OPTS+=("--build-arg" "Z3_CMAKE_GENERATOR=${Z3_CMAKE_GENERATOR}")
 fi
 
-if [ -n "${USE_OPENMP}" ]; then
-  BUILD_OPTS+=("--build-arg" "USE_OPENMP=${USE_OPENMP}")
-fi
-
 if [ -n "${USE_LIBGMP}" ]; then
   BUILD_OPTS+=("--build-arg" "USE_LIBGMP=${USE_LIBGMP}")
 fi