diff options
-rw-r--r-- | CMakeLists.txt | 21 | ||||
-rw-r--r-- | cmake/FindReadline.cmake | 4 | ||||
-rw-r--r-- | cmake/Helpers.cmake | 12 | ||||
-rwxr-xr-x | configure.sh | 28 | ||||
-rw-r--r-- | cvc4autoconfig.new.h.in | 10 | ||||
-rw-r--r-- | examples/CMakeLists.txt | 4 | ||||
-rw-r--r-- | 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-<option name>). --debug-symbols include debug symbols --valgrind Valgrind instrumentation --debug-context-mm use the debug context memory manager - --statistics do not include statistics - --replay turn off the replay feature - --assertions turn off assertions - --tracing remove all tracing code - --dumping remove all dumping code + --statistics include statistics + --replay turn on the replay feature + --assertions turn on assertions + --tracing include tracing code + --dumping include dumping code --muzzle complete silence (no non-result output) --coverage support for gcov coverage testing --profiling support for gprof profiling @@ -52,23 +52,23 @@ The following flags enable optional packages (disable with --no-<option name>). --glpk use GLPK simplex solver --abc use the ABC AIG library --cadical use the CaDiCaL SAT solver - --cryptominisat use the CRYPTOMINISAT sat solver + --cryptominisat use the CryptoMiniSat sat solver --lfsc use the LFSC proof checker - --symfpu use symfpu for floating point solver + --symfpu use SymFPU for floating point solver --portfolio build the multithreaded portfolio version of CVC4 (pcvc4) --readline support the readline library Optional Path to Optional Packages: - --abc-dir=PATH path to top level of abc source tree + --abc-dir=PATH path to top level of ABC source tree --antlr-dir=PATH path to ANTLR C headers and libraries --cadical-dir=PATH path to top level of CaDiCaL source tree - --cryptominisat-dir=PATH path to top level of cryptominisat source tree + --cryptominisat-dir=PATH path to top level of CryptoMiniSat source tree --cxxtest-dir=DIR path to CxxTest installation - --glpk-dir=PATH path to top level of glpk installation + --glpk-dir=PATH path to top level of GLPK installation --gmp-dir=PATH path to top level of GMP installation - --lfsc-dir=PATH path to top level of lfsc source tree - --symfpu-dir=PATH path to top level of symfpu source tree + --lfsc-dir=PATH path to top level of LFSC source tree + --symfpu-dir=PATH path to top level of SymFPU source tree Report bugs to <cvc4-bugs@cs.stanford.edu>. EOF diff --git a/cvc4autoconfig.new.h.in b/cvc4autoconfig.new.h.in index 8fafd62e3..ce8aeb5da 100644 --- a/cvc4autoconfig.new.h.in +++ b/cvc4autoconfig.new.h.in @@ -19,7 +19,7 @@ /* Full name of this package. */ #define PACKAGE_NAME "@PACKAGE_NAME@" -/* Define to 1 if CVC4 is built with (optional) GPLed library dependences. */ +/* Define to 1 if CVC4 is built with (optional) GPLed library dependencies. */ #cmakedefine01 CVC4_GPL_DEPS /* Define to use the CLN multi-precision arithmetic library. */ @@ -31,7 +31,7 @@ /* Define to 1 if Boost threading library has support for thread attributes. */ #cmakedefine01 BOOST_HAS_THREAD_ATTR -/* Define to 1 if `clock_gettime' is supported by the platform. */ +/* Define if `clock_gettime' is supported by the platform. */ #cmakedefine HAVE_CLOCK_GETTIME /* Define to 1 if the declaration of `optreset' is available. */ @@ -40,19 +40,19 @@ /* Define to 1 if the <ext/stdio_filebuf.h> header file is available. */ #cmakedefine01 HAVE_EXT_STDIO_FILEBUF_H -/* Define to 1 if `ffs' is supported by the platform. */ +/* Define if `ffs' is supported by the platform. */ #cmakedefine HAVE_FFS /* Define to 1 to use libreadline. */ #cmakedefine01 HAVE_LIBREADLINE -/* Define to 1 if `sigaltstack' is supported by the platform. */ +/* Define if `sigaltstack' is supported by the platform. */ #cmakedefine HAVE_SIGALTSTACK /* Define to 1 if `strerror_r' is supported by the platform. */ #cmakedefine01 HAVE_STRERROR_R -/* Define to 1 if `strtok_r' is supported by the platform. */ +/* Define if `strtok_r' is supported by the platform. */ #cmakedefine HAVE_STRTOK_R /* Define to 1 if the <unistd.h> header file is available. */ diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index a37cb9276..33d341ac8 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -30,8 +30,8 @@ add_custom_target(runexamples # - a list variable: set(<list name> <libs1> <libs2> ...) and pass # as "${<list name>}" # - a string: pass as "lib1 lib2 ..." (alternative: "lib1;lib2;...") -# > ouput_dir: Determines the examples subdirectory and is empty (passed as -# empty string) for the examples root director (this) +# > output_dir: Determines the examples subdirectory and is empty (passed as +# empty string) for the examples root directory (this) # > ARGN: Any additional arguments passed to the macro are interpreted as # as arguments to the test executable. macro(cvc4_add_example name src_files libs output_dir) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4ba64c11a..3e32ab7bf 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -788,29 +788,29 @@ install(FILES DESTINATION include/theory) install(FILES - util/abstract_value.h - util/bitvector.h - util/bool.h - util/cardinality.h - util/channel.h - util/divisible.h - util/gmp_util.h - util/hash.h - util/integer_cln_imp.h - util/integer_gmp_imp.h - util/maybe.h - util/proof.h - util/rational_cln_imp.h - util/rational_gmp_imp.h - util/regexp.h - util/resource_manager.h - util/result.h - util/sexpr.h - util/statistics.h - util/tuple.h - util/unsafe_interrupt_exception.h - ${CMAKE_CURRENT_BINARY_DIR}/util/floatingpoint.h - ${CMAKE_CURRENT_BINARY_DIR}/util/integer.h - ${CMAKE_CURRENT_BINARY_DIR}/util/rational.h + util/abstract_value.h + util/bitvector.h + util/bool.h + util/cardinality.h + util/channel.h + util/divisible.h + util/gmp_util.h + util/hash.h + util/integer_cln_imp.h + util/integer_gmp_imp.h + util/maybe.h + util/proof.h + util/rational_cln_imp.h + util/rational_gmp_imp.h + util/regexp.h + util/resource_manager.h + util/result.h + util/sexpr.h + util/statistics.h + util/tuple.h + util/unsafe_interrupt_exception.h + ${CMAKE_CURRENT_BINARY_DIR}/util/floatingpoint.h + ${CMAKE_CURRENT_BINARY_DIR}/util/integer.h + ${CMAKE_CURRENT_BINARY_DIR}/util/rational.h DESTINATION include/util) |