From e86a06829491bae68cef1b2156d245874516fd17 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Thu, 20 Sep 2018 13:31:45 -0700 Subject: [PATCH] cmake: Add more documentation, some fixes and cleanup. --- CMakeLists.txt | 21 +++++++++--------- cmake/FindReadline.cmake | 4 ++++ cmake/Helpers.cmake | 12 ++++++++++ configure.sh | 28 +++++++++++------------ cvc4autoconfig.new.h.in | 10 ++++----- examples/CMakeLists.txt | 4 ++-- src/CMakeLists.txt | 48 ++++++++++++++++++++-------------------- 7 files changed, 72 insertions(+), 55 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 54bbc6e12..36d88c12f 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,9 +1,5 @@ cmake_minimum_required(VERSION 3.1) -if(POLICY CMP0075) - cmake_policy(SET CMP0075 NEW) -endif() - #-----------------------------------------------------------------------------# # Project configuration @@ -43,7 +39,7 @@ option(ENABLE_GPL "Enable GPL dependencies") # General build options # -# >> 3-valued: INGORE ON OFF +# >> 3-valued: IGNORE ON OFF # > allows to detect if set by user (default: IGNORE) # > only necessary for options set for build types cvc4_option(ENABLE_ASAN "Enable ASAN build") @@ -69,7 +65,7 @@ option(ENABLE_PROFILING "Enable support for gprof profiling") # Optional dependencies # -# >> 3-valued: INGORE ON OFF +# >> 3-valued: IGNORE ON OFF # > allows to detect if set by user (default: IGNORE) # > only necessary for options set for ENABLE_BEST cvc4_option(USE_ABC "Use ABC for AIG bit-blasting") @@ -160,7 +156,9 @@ cvc4_set_option(ENABLE_SHARED ON) if(ENABLE_BEST) cvc4_set_option(USE_ABC ON) + cvc4_set_option(USE_CADICAL ON) cvc4_set_option(USE_CLN ON) + cvc4_set_option(USE_CRYPTOMINISAT ON) cvc4_set_option(USE_GLPK ON) cvc4_set_option(USE_READLINE ON) endif() @@ -199,9 +197,11 @@ libcvc4_link_libraries(${GMP_LIBRARIES}) libcvc4_include_directories(${GMP_INCLUDE_DIR}) if(ENABLE_ASAN) - set(CMAKE_REQUIRED_LIBRARIES -fsanitize=address) + # -fsanitize=address requires CMAKE_REQUIRED_FLAGS to be explicitely set, + # otherwise the -fsanitize=address check will fail while linking. + set(CMAKE_REQUIRED_FLAGS -fsanitize=address) add_required_c_cxx_flag("-fsanitize=address") - unset(CMAKE_REQUIRED_LIBRARIES) + unset(CMAKE_REQUIRED_FLAGS) add_required_c_cxx_flag("-fno-omit-frame-pointer") add_check_c_cxx_flag("-fsanitize-recover=address") endif() @@ -282,7 +282,7 @@ if(ENABLE_TRACING) endif() if(ENABLE_UNIT_TESTING) - find_package(CxxTest REQUIRED) + find_package(CxxTest REQUIRED) # Force shared libs for unit tests, static libs with unit tests are not # working right now. set(ENABLE_SHARED ON) @@ -363,6 +363,7 @@ if(USE_LFSC) endif() if(USE_READLINE) + set(GPL_LIBS "${GPL_LIBS} readline") find_package(Readline REQUIRED) set(HAVE_LIBREADLINE 1) if(Readline_COMPENTRY_FUNC_RETURNS_CHARPTR) @@ -517,7 +518,7 @@ if(GPL_LIBS) "\n" "If you prefer to license CVC4 under those terms, please configure CVC4 to" "\n" - "disable all optional GPLed library dependences (-DENABLE_BSD_ONLY=ON)." + "disable all optional GPLed library dependencies (-DENABLE_BSD_ONLY=ON)." ) else() message( diff --git a/cmake/FindReadline.cmake b/cmake/FindReadline.cmake index 2448f73cb..16dd72236 100644 --- a/cmake/FindReadline.cmake +++ b/cmake/FindReadline.cmake @@ -2,6 +2,8 @@ # Readline_FOUND - system has Readline lib # Readline_INCLUDE_DIR - the Readline include directory # Readline_LIBRARIES - Libraries needed to use Readline +# Readline_COMPENTRY_FUNC_RETURNS_CHARPTR - Indicates if compentry function +# returns a (char *) find_path(Readline_INCLUDE_DIR NAMES readline/readline.h) find_library(Readline_LIBRARIES NAMES readline) @@ -19,6 +21,8 @@ if(Readline_INCLUDE_DIR) int main() { rl_completion_entry_function = foo; return 0; }" Readline_COMPENTRY_FUNC_RETURNS_CHARPTR ) + unset(CMAKE_REQUIRED_QUIET) + unset(CMAKE_REQUIRED_LIBRARIES) endif() include(FindPackageHandleStandardArgs) diff --git a/cmake/Helpers.cmake b/cmake/Helpers.cmake index 86008e0d2..ec7216452 100644 --- a/cmake/Helpers.cmake +++ b/cmake/Helpers.cmake @@ -1,6 +1,7 @@ include(CheckCCompilerFlag) include(CheckCXXCompilerFlag) +# Add a C flag to the global list of C flags. macro(add_c_flag flag) if(CMAKE_C_FLAGS) set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} ${flag}") @@ -10,6 +11,7 @@ macro(add_c_flag flag) message(STATUS "Configuring with C flag '${flag}'") endmacro() +# Add a CXX flag to the global list of CXX flags. macro(add_cxx_flag flag) if(CMAKE_CXX_FLAGS) set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${flag}") @@ -19,11 +21,13 @@ macro(add_cxx_flag flag) message(STATUS "Configuring with CXX flag '${flag}'") endmacro() +# Add a C and CXX flag to the global list of C/CXX flags. macro(add_c_cxx_flag flag) add_c_flag(${flag}) add_cxx_flag(${flag}) endmacro() +# Check if C flag is supported and add to global list of C flags. macro(add_check_c_flag flag) string(REGEX REPLACE "[-=]" "_" flagname ${flag}) check_c_compiler_flag("${flag}" HAVE_FLAG${flagname}) @@ -32,6 +36,7 @@ macro(add_check_c_flag flag) endif() endmacro() +# Check if CXX flag is supported and add to global list of CXX flags. macro(add_check_cxx_flag flag) string(REGEX REPLACE "[-=]" "_" flagname ${flag}) check_cxx_compiler_flag("${flag}" HAVE_FLAG${flagname}) @@ -40,11 +45,14 @@ macro(add_check_cxx_flag flag) endif() endmacro() +# Check if C/CXX flag is supported and add to global list of C/CXX flags. macro(add_check_c_cxx_flag flag) add_check_c_flag(${flag}) add_check_cxx_flag(${flag}) endmacro() +# Add required CXX flag. Configuration fails if the CXX flag is not supported +# by the compiler. macro(add_required_cxx_flag flag) string(REGEX REPLACE "[-=]" "_" flagnamename ${flag}) check_cxx_compiler_flag("${flag}" HAVE_FLAG${flagname}) @@ -54,6 +62,8 @@ macro(add_required_cxx_flag flag) add_cxx_flag(${flag}) endmacro() +# Add required C flag. Configuration fails if the C flag is not supported by +# the compiler. macro(add_required_c_flag flag) string(REGEX REPLACE "[-=]" "_" flagname ${flag}) check_c_compiler_flag("${flag}" HAVE_FLAG${flagname}) @@ -63,6 +73,8 @@ macro(add_required_c_flag flag) add_c_flag(${flag}) endmacro() +# Add requied C/CXX flag. Configuration fails if the C/CXX flag is not +# supported by the compiler. macro(add_required_c_cxx_flag flag) add_required_c_flag(${flag}) add_required_cxx_flag(${flag}) diff --git a/configure.sh b/configure.sh index e5bf0de4a..f3ba57c82 100755 --- a/configure.sh +++ b/configure.sh @@ -16,8 +16,8 @@ General options; -h, --help display this help and exit --prefix=STR install directory --name=STR use custom build directory name (optionally: +path) - --best turn on dependences known to give best performance - --gpl permit GPL dependences, if available + --best turn on dependencies known to give best performance + --gpl permit GPL dependencies, if available --win64 cross-compile for Windows 64 bit @@ -29,11 +29,11 @@ The following flags enable optional features (disable with --no-