mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

clean up CMake code (#5182)

Browse source 
* CMake: simplify FindGMP.cmake

Remove printing of all the different variables, and let FPHSA output the library
name. Add an imported target, which bundles the library and the include
directories for easier usage.

* fix build: vector::c_ptr() now is vector::data()

* CMake: use Threads::Threads imported module

Otherwise the setting of THREADS_PREFER_PTHREAD_FLAG has no effect.

* CMake: remove needless policy setting

The minimum required version is CMake 3.4, where these policies are already set
to new because they were introduced earlier.

* CMake: remove needless variable expansion
This commit is contained in:
Rolf Eike Beer 2021-04-14 19:29:15 +02:00 committed by GitHub
parent ce96182746
commit 7f8e2a9f75
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
13 changed files with 69 additions and 94 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

48
CMakeLists.txt
View file

@ -1,15 +1,6 @@
# Enforce some CMake policies # Enforce some CMake policies
cmake_minimum_required(VERSION 3.4) cmake_minimum_required(VERSION 3.4)
if (POLICY CMP0054)
cmake_policy(SET CMP0054 NEW)
endif()
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") set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
project(Z3 VERSION 4.8.11.0 LANGUAGES CXX) project(Z3 VERSION 4.8.11.0 LANGUAGES CXX)
@ -42,7 +33,7 @@ set(z3_polluted_tree_msg
################################################################################ ################################################################################
# Sanity check - Disallow building in source # Sanity check - Disallow building in source
################################################################################ ################################################################################
if ("${PROJECT_SOURCE_DIR}" STREQUAL "${PROJECT_BINARY_DIR}") if (PROJECT_SOURCE_DIR STREQUAL PROJECT_BINARY_DIR)
message(FATAL_ERROR "In source builds are not allowed. You should invoke " message(FATAL_ERROR "In source builds are not allowed. You should invoke "
"CMake from a different directory.") "CMake from a different directory.")
endif() endif()
@ -194,28 +185,28 @@ set(CMAKE_CXX_STANDARD_REQUIRED ON)
################################################################################ ################################################################################
# Platform detection # Platform detection
################################################################################ ################################################################################
if ("${CMAKE_SYSTEM_NAME}" STREQUAL "Linux") if (CMAKE_SYSTEM_NAME STREQUAL "Linux")
message(STATUS "Platform: Linux") message(STATUS "Platform: Linux")
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_LINUX_") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_LINUX_")
if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") if (TARGET_ARCHITECTURE STREQUAL "x86_64")
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_USE_THREAD_LOCAL") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_USE_THREAD_LOCAL")
endif() endif()
elseif ("${CMAKE_SYSTEM_NAME}" STREQUAL "Android") elseif (CMAKE_SYSTEM_NAME STREQUAL "Android")
message(STATUS "Platform: Android") message(STATUS "Platform: Android")
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_ANDROID_") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_ANDROID_")
elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "GNU") elseif (CMAKE_SYSTEM_NAME MATCHES "GNU")
message(STATUS "Platform: GNU/Hurd") message(STATUS "Platform: GNU/Hurd")
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_HURD_") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_HURD_")
elseif ("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin") elseif (CMAKE_SYSTEM_NAME STREQUAL "Darwin")
# Does macOS really not need any special flags? # Does macOS really not need any special flags?
message(STATUS "Platform: Darwin") message(STATUS "Platform: Darwin")
elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "FreeBSD") elseif (CMAKE_SYSTEM_NAME MATCHES "FreeBSD")
message(STATUS "Platform: FreeBSD") message(STATUS "Platform: FreeBSD")
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_FREEBSD_") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_FREEBSD_")
elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "NetBSD") elseif (CMAKE_SYSTEM_NAME MATCHES "NetBSD")
message(STATUS "Platform: NetBSD") message(STATUS "Platform: NetBSD")
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_NetBSD_") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_NetBSD_")
elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "OpenBSD") elseif (CMAKE_SYSTEM_NAME MATCHES "OpenBSD")
message(STATUS "Platform: OpenBSD") message(STATUS "Platform: OpenBSD")
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_OPENBSD_") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_OPENBSD_")
elseif (CYGWIN) elseif (CYGWIN)
@ -251,8 +242,7 @@ if (Z3_USE_LIB_GMP)
# can't be found # can't be found
find_package(GMP REQUIRED) find_package(GMP REQUIRED)
message(STATUS "Using libgmp") message(STATUS "Using libgmp")
list(APPEND Z3_DEPENDENT_LIBS ${GMP_C_LIBRARIES}) list(APPEND Z3_DEPENDENT_LIBS GMP::GMP)
list(APPEND Z3_COMPONENT_EXTRA_INCLUDE_DIRS ${GMP_INCLUDE_DIRS})
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_MP_GMP") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_MP_GMP")
else() else()
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_MP_INTERNAL") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_MP_INTERNAL")
@ -292,18 +282,18 @@ endif()
# FP math # FP math
################################################################################ ################################################################################
# FIXME: Support ARM "-mfpu=vfp -mfloat-abi=hard" # FIXME: Support ARM "-mfpu=vfp -mfloat-abi=hard"
if (("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") OR ("${TARGET_ARCHITECTURE}" STREQUAL "i686")) 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 "GNU") OR (CMAKE_CXX_COMPILER_ID MATCHES "Clang") OR (CMAKE_CXX_COMPILER_ID MATCHES "Intel"))
if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Intel") if (CMAKE_CXX_COMPILER_ID MATCHES "Intel")
# Intel's compiler requires linking with libiomp5 # Intel's compiler requires linking with libiomp5
list(APPEND Z3_DEPENDENT_LIBS "iomp5") list(APPEND Z3_DEPENDENT_LIBS "iomp5")
endif() endif()
set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2") set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2")
elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Intel") elseif (CMAKE_CXX_COMPILER_ID MATCHES "Intel")
set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2") set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2")
# Intel's compiler requires linking with libiomp5 # Intel's compiler requires linking with libiomp5
list(APPEND Z3_DEPENDENT_LIBS "iomp5") list(APPEND Z3_DEPENDENT_LIBS "iomp5")
elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC") elseif (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
set(SSE_FLAGS "/arch:SSE2") set(SSE_FLAGS "/arch:SSE2")
else() else()
message(FATAL_ERROR "Unknown compiler ${CMAKE_CXX_COMPILER_ID}") message(FATAL_ERROR "Unknown compiler ${CMAKE_CXX_COMPILER_ID}")
@ -320,7 +310,7 @@ endif()
################################################################################ ################################################################################
set(THREADS_PREFER_PTHREAD_FLAG TRUE) set(THREADS_PREFER_PTHREAD_FLAG TRUE)
find_package(Threads) find_package(Threads)
list(APPEND Z3_DEPENDENT_LIBS ${CMAKE_THREAD_LIBS_INIT}) list(APPEND Z3_DEPENDENT_LIBS Threads::Threads)
################################################################################ ################################################################################
# Compiler warnings # Compiler warnings
@ -411,7 +401,7 @@ if (Z3_ENABLE_CFI)
if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")
z3_add_cxx_flag("-fsanitize=cfi" REQUIRED) z3_add_cxx_flag("-fsanitize=cfi" REQUIRED)
z3_add_cxx_flag("-fsanitize-cfi-cross-dso" REQUIRED) z3_add_cxx_flag("-fsanitize-cfi-cross-dso" REQUIRED)
elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC") elseif (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
z3_add_cxx_flag("/guard:cf" REQUIRED) z3_add_cxx_flag("/guard:cf" REQUIRED)
message(STATUS "Enabling CFI for MSVC") message(STATUS "Enabling CFI for MSVC")
foreach (_build_type ${build_types_with_cfi}) foreach (_build_type ${build_types_with_cfi})
@ -428,14 +418,14 @@ endif()
################################################################################ ################################################################################
# MSVC specific flags inherited from old build system # MSVC specific flags inherited from old build system
################################################################################ ################################################################################
if ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC") if (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
include(${PROJECT_SOURCE_DIR}/cmake/msvc_legacy_quirks.cmake) include(${PROJECT_SOURCE_DIR}/cmake/msvc_legacy_quirks.cmake)
endif() endif()
################################################################################ ################################################################################
# Pass /RELEASE to the linker so that checksums in PE files are calculated. # Pass /RELEASE to the linker so that checksums in PE files are calculated.
################################################################################ ################################################################################
if ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC") if (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
string(APPEND CMAKE_EXE_LINKER_FLAGS " /RELEASE") string(APPEND CMAKE_EXE_LINKER_FLAGS " /RELEASE")
string(APPEND CMAKE_SHARED_LINKER_FLAGS " /RELEASE") string(APPEND CMAKE_SHARED_LINKER_FLAGS " /RELEASE")
endif() endif()

6
cmake/compiler_lto.cmake
View file

@ -18,11 +18,11 @@ if (Z3_LINK_TIME_OPTIMIZATION)
set(_lto_compiler_flag "") set(_lto_compiler_flag "")
set(_lto_linker_flag "") set(_lto_linker_flag "")
if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR if ((CMAKE_CXX_COMPILER_ID MATCHES "Clang") OR
("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) (CMAKE_CXX_COMPILER_ID MATCHES "GNU"))
set(_lto_compiler_flag "-flto") set(_lto_compiler_flag "-flto")
set(_lto_linker_flag "-flto") set(_lto_linker_flag "-flto")
elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC") elseif (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
set(_lto_compiler_flag "/GL") set(_lto_compiler_flag "/GL")
set(_lto_linker_flag "/LTCG") set(_lto_linker_flag "/LTCG")
else() else()

22
cmake/compiler_warnings.cmake
View file

@ -46,22 +46,22 @@ set(CLANG_WARNINGS_AS_ERRORS
################################################################################ ################################################################################
set(WARNING_FLAGS_TO_CHECK "") set(WARNING_FLAGS_TO_CHECK "")
set(WARNING_AS_ERROR_FLAGS_TO_CHECK "") set(WARNING_AS_ERROR_FLAGS_TO_CHECK "")
if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") if (CMAKE_CXX_COMPILER_ID MATCHES "GNU")
list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS}) list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS})
list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_ONLY_WARNINGS}) list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_ONLY_WARNINGS})
list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_AS_ERRORS}) list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_AS_ERRORS})
list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_WARNINGS_AS_ERRORS}) list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_WARNINGS_AS_ERRORS})
elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") elseif (CMAKE_CXX_COMPILER_ID MATCHES "Clang")
list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS}) list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS})
list(APPEND WARNING_FLAGS_TO_CHECK ${CLANG_ONLY_WARNINGS}) list(APPEND WARNING_FLAGS_TO_CHECK ${CLANG_ONLY_WARNINGS})
list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_AS_ERRORS}) list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_AS_ERRORS})
list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${CLANG_WARNINGS_AS_ERRORS}) list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${CLANG_WARNINGS_AS_ERRORS})
elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC") elseif (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
list(APPEND WARNING_FLAGS_TO_CHECK ${MSVC_WARNINGS}) list(APPEND WARNING_FLAGS_TO_CHECK ${MSVC_WARNINGS})
# CMake's default flags include /W3 already so remove them if # CMake's default flags include /W3 already so remove them if
# they already exist. # they already exist.
if ("${CMAKE_CXX_FLAGS}" MATCHES "/W3") if (CMAKE_CXX_FLAGS MATCHES "/W3")
string(REPLACE "/W3" "" _cmake_cxx_flags_remove_w3 "${CMAKE_CXX_FLAGS}") string(REPLACE "/W3" "" _cmake_cxx_flags_remove_w3 "${CMAKE_CXX_FLAGS}")
set(CMAKE_CXX_FLAGS "${_cmake_cxx_flags_remove_w3}" CACHE STRING "" FORCE) set(CMAKE_CXX_FLAGS "${_cmake_cxx_flags_remove_w3}" CACHE STRING "" FORCE)
endif() endif()
@ -84,7 +84,7 @@ get_property(
PROPERTY PROPERTY
TYPE TYPE
) )
if ("${WARNINGS_AS_ERRORS_CACHE_VAR_TYPE}" STREQUAL "BOOL") if (WARNINGS_AS_ERRORS_CACHE_VAR_TYPE STREQUAL "BOOL")
message(WARNING "Detected legacy WARNINGS_AS_ERRORS option. Upgrading") message(WARNING "Detected legacy WARNINGS_AS_ERRORS option. Upgrading")
set(WARNINGS_AS_ERRORS_DEFAULT "${WARNINGS_AS_ERRORS}") set(WARNINGS_AS_ERRORS_DEFAULT "${WARNINGS_AS_ERRORS}")
# Delete old entry # Delete old entry
@ -106,25 +106,25 @@ set_property(
"ON;OFF;SERIOUS_ONLY" "ON;OFF;SERIOUS_ONLY"
) )
if ("${WARNINGS_AS_ERRORS}" STREQUAL "ON") if (WARNINGS_AS_ERRORS STREQUAL "ON")
message(STATUS "Treating compiler warnings as errors") message(STATUS "Treating compiler warnings as errors")
if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) if ((CMAKE_CXX_COMPILER_ID MATCHES "Clang") OR (CMAKE_CXX_COMPILER_ID MATCHES "GNU"))
list(APPEND Z3_COMPONENT_CXX_FLAGS "-Werror") list(APPEND Z3_COMPONENT_CXX_FLAGS "-Werror")
elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC") elseif (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
list(APPEND Z3_COMPONENT_CXX_FLAGS "/WX") list(APPEND Z3_COMPONENT_CXX_FLAGS "/WX")
else() else()
message(AUTHOR_WARNING "Unknown compiler") message(AUTHOR_WARNING "Unknown compiler")
endif() endif()
elseif ("${WARNINGS_AS_ERRORS}" STREQUAL "SERIOUS_ONLY") elseif (WARNINGS_AS_ERRORS STREQUAL "SERIOUS_ONLY")
message(STATUS "Treating only serious compiler warnings as errors") message(STATUS "Treating only serious compiler warnings as errors")
# Loop through the flags # Loop through the flags
foreach (flag ${WARNING_AS_ERROR_FLAGS_TO_CHECK}) foreach (flag ${WARNING_AS_ERROR_FLAGS_TO_CHECK})
# Add globally because some flags need to be passed at link time. # Add globally because some flags need to be passed at link time.
z3_add_cxx_flag("${flag}" GLOBAL) z3_add_cxx_flag("${flag}" GLOBAL)
endforeach() endforeach()
elseif ("${WARNINGS_AS_ERRORS}" STREQUAL "OFF") elseif (WARNINGS_AS_ERRORS STREQUAL "OFF")
message(STATUS "Not treating compiler warnings as errors") message(STATUS "Not treating compiler warnings as errors")
if ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC") if (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
# Warnings as errors is off by default for MSVC so setting this # Warnings as errors is off by default for MSVC so setting this
# is not necessary but this duplicates the behaviour of the old # is not necessary but this duplicates the behaviour of the old
# build system. # build system.

4
cmake/git_utils.cmake
View file

@ -26,7 +26,7 @@ function(add_git_dir_dependency GIT_DOT_FILE SUCCESS_VAR)
# git directory # git directory
file(READ "${GIT_DOT_FILE}" GIT_DOT_FILE_DATA LIMIT 512) file(READ "${GIT_DOT_FILE}" GIT_DOT_FILE_DATA LIMIT 512)
string(STRIP "${GIT_DOT_FILE_DATA}" GIT_DOT_FILE_DATA_STRIPPED) string(STRIP "${GIT_DOT_FILE_DATA}" GIT_DOT_FILE_DATA_STRIPPED)
if ("${GIT_DOT_FILE_DATA_STRIPPED}" MATCHES "^gitdir:[ ]*(.+)$") if (GIT_DOT_FILE_DATA_STRIPPED MATCHES "^gitdir:[ ]*(.+)$")
# Git worktree # Git worktree
message(STATUS "Found git worktree") message(STATUS "Found git worktree")
set(GIT_WORKTREE_DIR "${CMAKE_MATCH_1}") set(GIT_WORKTREE_DIR "${CMAKE_MATCH_1}")
@ -75,7 +75,7 @@ function(add_git_dir_dependency GIT_DOT_FILE SUCCESS_VAR)
file(READ "${GIT_HEAD_FILE}" GIT_HEAD_DATA LIMIT 128) file(READ "${GIT_HEAD_FILE}" GIT_HEAD_DATA LIMIT 128)
string(STRIP "${GIT_HEAD_DATA}" GIT_HEAD_DATA_STRIPPED) string(STRIP "${GIT_HEAD_DATA}" GIT_HEAD_DATA_STRIPPED)
if ("${GIT_HEAD_DATA_STRIPPED}" MATCHES "^ref:[ ]*(.+)$") if (GIT_HEAD_DATA_STRIPPED MATCHES "^ref:[ ]*(.+)$")
# HEAD points at a reference. # HEAD points at a reference.
set(GIT_REF "${CMAKE_MATCH_1}") set(GIT_REF "${CMAKE_MATCH_1}")
if (EXISTS "${GIT_DIR}/${GIT_REF}") if (EXISTS "${GIT_DIR}/${GIT_REF}")

43
cmake/modules/FindGMP.cmake
View file

@ -13,52 +13,37 @@ find_library(GMP_C_LIBRARIES
NAMES gmp NAMES gmp
DOC "GMP C libraries" DOC "GMP C libraries"
) )
if (GMP_C_LIBRARIES)
message(STATUS "Found GMP C library: \"${GMP_C_LIBRARIES}\"")
else()
message(STATUS "Could not find GMP C library")
endif()
find_library(GMP_CXX_LIBRARIES find_library(GMP_CXX_LIBRARIES
NAMES gmpxx NAMES gmpxx
DOC "GMP C++ libraries" DOC "GMP C++ libraries"
) )
if (GMP_CXX_LIBRARIES)
message(STATUS "Found GMP C++ library: \"${GMP_CXX_LIBRARIES}\"")
else()
message(STATUS "Could not find GMP C++ library")
endif()
# Try to find headers # Try to find headers
find_path(GMP_C_INCLUDES find_path(GMP_C_INCLUDES
NAMES gmp.h NAMES gmp.h
DOC "GMP C header" DOC "GMP C header"
) )
if (GMP_C_INCLUDES)
message(STATUS "Found GMP C include path: \"${GMP_C_INCLUDES}\"")
else()
message(STATUS "Could not find GMP C include path")
endif()
find_path(GMP_CXX_INCLUDES find_path(GMP_CXX_INCLUDES
NAMES gmpxx.h NAMES gmpxx.h
DOC "GMP C++ header" DOC "GMP C++ header"
) )
if (GMP_CXX_INCLUDES)
message(STATUS "Found GMP C++ include path: \"${GMP_CXX_INCLUDES}\"")
else()
message(STATUS "Could not find GMP C++ include path")
endif()
if (GMP_C_LIBRARIES AND GMP_CXX_LIBRARIES AND GMP_C_INCLUDES AND GMP_CXX_INCLUDES)
set(GMP_INCLUDE_DIRS "${GMP_C_INCLUDES}" "${GMP_CXX_INCLUDES}")
list(REMOVE_DUPLICATES GMP_INCLUDE_DIRS)
message(STATUS "Found GMP")
else()
message(STATUS "Could not find GMP")
endif()
# TODO: We should check we can link some simple code against libgmp and libgmpxx # TODO: We should check we can link some simple code against libgmp and libgmpxx
# Handle QUIET and REQUIRED and check the necessary variables were set and if so # Handle QUIET and REQUIRED and check the necessary variables were set and if so
# set ``GMP_FOUND`` # set ``GMP_FOUND``
find_package_handle_standard_args(GMP DEFAULT_MSG GMP_INCLUDE_DIRS GMP_C_LIBRARIES GMP_CXX_LIBRARIES) find_package_handle_standard_args(GMP
REQUIRED_VARS GMP_C_LIBRARIES GMP_C_INCLUDES GMP_CXX_LIBRARIES GMP_CXX_INCLUDES)
if (GMP_FOUND)
set(GMP_INCLUDE_DIRS "${GMP_C_INCLUDES}" "${GMP_CXX_INCLUDES}")
list(REMOVE_DUPLICATES GMP_INCLUDE_DIRS)
if (NOT TARGET GMP::GMP)
add_library(GMP::GMP UNKNOWN IMPORTED)
set_target_properties(GMP::GMP PROPERTIES
INTERFACE_INCLUDE_DIRECTORIES "${GMP_C_INCLUDES}"
IMPORTED_LOCATION "${GMP_C_LIBRARIES}")
endif()
endif()

16
cmake/msvc_legacy_quirks.cmake
View file

@ -22,7 +22,7 @@ set(Z3_MSVC_LEGACY_DEFINES
_UNICODE _UNICODE
) )
if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") if (TARGET_ARCHITECTURE STREQUAL "x86_64")
list(APPEND Z3_MSVC_LEGACY_DEFINES "" list(APPEND Z3_MSVC_LEGACY_DEFINES ""
# Don't set `_LIB`. The old build system sets this for x86_64 release # Don't set `_LIB`. The old build system sets this for x86_64 release
# build. This flag doesn't seem to be documented but a stackoverflow # build. This flag doesn't seem to be documented but a stackoverflow
@ -57,10 +57,10 @@ endif()
# Note we don't set WIN32 or _WINDOWS because # Note we don't set WIN32 or _WINDOWS because
# CMake provides that for us. As a sanity check make sure the option # CMake provides that for us. As a sanity check make sure the option
# is present. # is present.
if (NOT "${CMAKE_CXX_FLAGS}" MATCHES "[-/]D[ ]*WIN32") if (NOT CMAKE_CXX_FLAGS MATCHES "[-/]D[ ]*WIN32")
message(FATAL_ERROR "\"/D WIN32\" is missing") message(FATAL_ERROR "\"/D WIN32\" is missing")
endif() endif()
if (NOT "${CMAKE_CXX_FLAGS}" MATCHES "[-/]D[ ]*_WINDOWS") if (NOT CMAKE_CXX_FLAGS MATCHES "[-/]D[ ]*_WINDOWS")
message(FATAL_ERROR "\"/D _WINDOWS\" is missing") message(FATAL_ERROR "\"/D _WINDOWS\" is missing")
endif() endif()
@ -82,7 +82,7 @@ endif()
# build system kept the frame pointer for all configurations # build system kept the frame pointer for all configurations
# except x86_64 release (I don't know why the frame pointer # except x86_64 release (I don't know why the frame pointer
# is kept for i686 release). # is kept for i686 release).
if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") if (TARGET_ARCHITECTURE STREQUAL "x86_64")
list(APPEND Z3_COMPONENT_CXX_FLAGS list(APPEND Z3_COMPONENT_CXX_FLAGS
$<$<CONFIG:Debug>:${NO_OMIT_FRAME_POINTER_MSVC_FLAG}> $<$<CONFIG:Debug>:${NO_OMIT_FRAME_POINTER_MSVC_FLAG}>
$<$<CONFIG:MinSizeRel>:${NO_OMIT_FRAME_POINTER_MSVC_FLAG}> $<$<CONFIG:MinSizeRel>:${NO_OMIT_FRAME_POINTER_MSVC_FLAG}>
@ -91,7 +91,7 @@ else()
list(APPEND Z3_COMPONENT_CXX_FLAGS ${NO_OMIT_FRAME_POINTER_MSVC_FLAG}) list(APPEND Z3_COMPONENT_CXX_FLAGS ${NO_OMIT_FRAME_POINTER_MSVC_FLAG})
endif() endif()
if (("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") OR ("${TARGET_ARCHITECTURE}" STREQUAL "i686")) if ((TARGET_ARCHITECTURE STREQUAL "x86_64") OR (TARGET_ARCHITECTURE STREQUAL "i686"))
# Use __cdecl calling convention. Apparently this is MSVC's default # Use __cdecl calling convention. Apparently this is MSVC's default
# but the old build system set it so for completeness set it too. # but the old build system set it so for completeness set it too.
# See https://msdn.microsoft.com/en-us/library/46t77ak2.aspx # See https://msdn.microsoft.com/en-us/library/46t77ak2.aspx
@ -153,9 +153,9 @@ string(APPEND CMAKE_SHARED_LINKER_FLAGS " /SUBSYSTEM:WINDOWS")
# in the old build system except release x86_64. We try to emulate this here but # in the old build system except release x86_64. We try to emulate this here but
# this is likely the wrong thing to do. # this is likely the wrong thing to do.
foreach (_build_type ${_build_types_as_upper}) foreach (_build_type ${_build_types_as_upper})
if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64" AND if (TARGET_ARCHITECTURE STREQUAL "x86_64" AND
("${_build_type}" STREQUAL "RELEASE" OR (_build_type STREQUAL "RELEASE" OR
"${_build_type}" STREQUAL "RELWITHDEBINFO") _build_type STREQUAL "RELWITHDEBINFO")
) )
message(AUTHOR_WARNING "Skipping legacy linker MSVC options for x86_64 ${_build_type}") message(AUTHOR_WARNING "Skipping legacy linker MSVC options for x86_64 ${_build_type}")
else() else()

2
examples/c++/CMakeLists.txt
View file

@ -28,7 +28,7 @@ add_executable(cpp_example example.cpp)
target_include_directories(cpp_example PRIVATE ${Z3_CXX_INCLUDE_DIRS}) target_include_directories(cpp_example PRIVATE ${Z3_CXX_INCLUDE_DIRS})
target_link_libraries(cpp_example PRIVATE ${Z3_LIBRARIES}) target_link_libraries(cpp_example PRIVATE ${Z3_LIBRARIES})
if ("${CMAKE_SYSTEM_NAME}" MATCHES "[Ww]indows") if (CMAKE_SYSTEM_NAME MATCHES "[Ww]indows")
# On Windows we need to copy the Z3 libraries # On Windows we need to copy the Z3 libraries
# into the same directory as the executable # into the same directory as the executable
# so that they can be found. # so that they can be found.

2
examples/c/CMakeLists.txt
View file

@ -40,7 +40,7 @@ endif()
target_include_directories(c_example PRIVATE ${Z3_C_INCLUDE_DIRS}) target_include_directories(c_example PRIVATE ${Z3_C_INCLUDE_DIRS})
target_link_libraries(c_example PRIVATE ${Z3_LIBRARIES}) target_link_libraries(c_example PRIVATE ${Z3_LIBRARIES})
if ("${CMAKE_SYSTEM_NAME}" MATCHES "[Ww]indows") if (CMAKE_SYSTEM_NAME MATCHES "[Ww]indows")
# On Windows we need to copy the Z3 libraries # On Windows we need to copy the Z3 libraries
# into the same directory as the executable # into the same directory as the executable
# so that they can be found. # so that they can be found.

2
examples/dotnet/CMakeLists.txt
View file

@ -1,6 +1,6 @@
find_package(Dotnet REQUIRED) find_package(Dotnet REQUIRED)
if("${TARGET_ARCHITECTURE}" STREQUAL "i686") if(TARGET_ARCHITECTURE STREQUAL "i686")
set(Z3_DOTNET_PLATFORM "x86") set(Z3_DOTNET_PLATFORM "x86")
else() else()
set(Z3_DOTNET_PLATFORM "AnyCPU") set(Z3_DOTNET_PLATFORM "AnyCPU")

2
examples/maxsat/CMakeLists.txt
View file

@ -35,7 +35,7 @@ if (FORCE_CXX_LINKER)
) )
endif() endif()
if ("${CMAKE_SYSTEM_NAME}" MATCHES "[Ww]indows") if (CMAKE_SYSTEM_NAME MATCHES "[Ww]indows")
# On Windows we need to copy the Z3 libraries # On Windows we need to copy the Z3 libraries
# into the same directory as the executable # into the same directory as the executable
# so that they can be found. # so that they can be found.

2
examples/tptp/CMakeLists.txt
View file

@ -28,7 +28,7 @@ add_executable(z3_tptp5 tptp5.cpp tptp5.lex.cpp)
target_include_directories(z3_tptp5 PRIVATE ${Z3_CXX_INCLUDE_DIRS}) target_include_directories(z3_tptp5 PRIVATE ${Z3_CXX_INCLUDE_DIRS})
target_link_libraries(z3_tptp5 PRIVATE ${Z3_LIBRARIES}) target_link_libraries(z3_tptp5 PRIVATE ${Z3_LIBRARIES})
if ("${CMAKE_SYSTEM_NAME}" MATCHES "[Ww]indows") if (CMAKE_SYSTEM_NAME MATCHES "[Ww]indows")
# On Windows we need to copy the Z3 libraries # On Windows we need to copy the Z3 libraries
# into the same directory as the executable # into the same directory as the executable
# so that they can be found. # so that they can be found.

2
src/api/dotnet/CMakeLists.txt
View file

@ -140,7 +140,7 @@ endforeach()
# Note, nuget package file names do not have the ${VER_REV} part. # Note, nuget package file names do not have the ${VER_REV} part.
set(Z3_DOTNET_NUPKG_VERSION "${VER_MAJOR}.${VER_MINOR}.${VER_BUILD}") set(Z3_DOTNET_NUPKG_VERSION "${VER_MAJOR}.${VER_MINOR}.${VER_BUILD}")
if("${TARGET_ARCHITECTURE}" STREQUAL "i686") if(TARGET_ARCHITECTURE STREQUAL "i686")
set(Z3_DOTNET_PLATFORM "x86") set(Z3_DOTNET_PLATFORM "x86")
else() else()
set(Z3_DOTNET_PLATFORM "AnyCPU") set(Z3_DOTNET_PLATFORM "AnyCPU")

12
src/util/mpz.cpp
View file

@ -1716,8 +1716,8 @@ void mpz_manager<SYNCH>::display(std::ostream & out, mpz const & a) const {
// GMP version // GMP version
size_t sz = mpz_sizeinbase(*a.m_ptr, 10) + 2; size_t sz = mpz_sizeinbase(*a.m_ptr, 10) + 2;
sbuffer<char, 1024> buffer(sz, 0); sbuffer<char, 1024> buffer(sz, 0);
mpz_get_str(buffer.c_ptr(), 10, *a.m_ptr); mpz_get_str(buffer.data(), 10, *a.m_ptr);
out << buffer.c_ptr(); out << buffer.data();
#endif #endif
} }
} }
@ -1776,11 +1776,11 @@ void mpz_manager<SYNCH>::display_hex(std::ostream & out, mpz const & a, unsigned
unsigned requiredLength = num_bits / 4; unsigned requiredLength = num_bits / 4;
unsigned padding = requiredLength > sz ? requiredLength - sz : 0; unsigned padding = requiredLength > sz ? requiredLength - sz : 0;
sbuffer<char, 1024> buffer(sz, 0); sbuffer<char, 1024> buffer(sz, 0);
mpz_get_str(buffer.c_ptr(), 16, *(a.m_ptr)); mpz_get_str(buffer.data(), 16, *(a.m_ptr));
for (unsigned i = 0; i < padding; ++i) { for (unsigned i = 0; i < padding; ++i) {
out << "0"; out << "0";
} }
out << buffer.c_ptr() + (sz > requiredLength ? sz - requiredLength : 0); out << buffer.data() + (sz > requiredLength ? sz - requiredLength : 0);
#endif #endif
} }
out.copyfmt(fmt); out.copyfmt(fmt);
@ -1830,11 +1830,11 @@ void mpz_manager<SYNCH>::display_bin(std::ostream & out, mpz const & a, unsigned
size_t sz = mpz_sizeinbase(*(a.m_ptr), 2); size_t sz = mpz_sizeinbase(*(a.m_ptr), 2);
unsigned padding = num_bits > sz ? num_bits - sz : 0; unsigned padding = num_bits > sz ? num_bits - sz : 0;
sbuffer<char, 1024> buffer(sz, 0); sbuffer<char, 1024> buffer(sz, 0);
mpz_get_str(buffer.c_ptr(), 2, *(a.m_ptr)); mpz_get_str(buffer.data(), 2, *(a.m_ptr));
for (unsigned i = 0; i < padding; ++i) { for (unsigned i = 0; i < padding; ++i) {
out << "0"; out << "0";
} }
out << buffer.c_ptr() + (sz > num_bits ? sz - num_bits : 0); out << buffer.data() + (sz > num_bits ? sz - num_bits : 0);
#endif #endif
} }
} }