diff options
| -rw-r--r-- | CMakeLists.txt | 27 | ||||
| -rw-r--r-- | cmake/ConfigureCVC4.cmake | 36 | ||||
| -rw-r--r-- | cmake/FindCLN.cmake | 27 | ||||
| -rw-r--r-- | src/util/CMakeLists.txt | 17 |
4 files changed, 89 insertions, 18 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 34281a5f2..9d5e4da54 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -102,13 +102,24 @@ message(STATUS "Building ${CMAKE_BUILD_TYPE} build") #-----------------------------------------------------------------------------# +option(USE_CLN "Use CLN instead of GMP" OFF) + +#-----------------------------------------------------------------------------# + find_package(PythonInterp REQUIRED) find_package(GMP REQUIRED) -message(STATUS "Found GMP headers: ${GMP_INCLUDE_DIR}") set(LIBRARIES ${LIBRARIES} ${GMP_LIBRARIES}) include_directories(${GMP_INCLUDE_DIR}) +if(USE_CLN) + find_package(CLN 1.2.2 REQUIRED) + if(CLN_FOUND) + set(LIBRARIES ${LIBRARIES} ${GMP_LIBRARIES}) + include_directories(${GMP_INCLUDE_DIR}) + endif() +endif() + find_package(ANTLR REQUIRED) message(STATUS "Found ANTLR headers: ${ANTLR_INCLUDE_DIR}") set(LIBRARIES ${LIBRARIES} ${ANTLR_LIBRARIES}) @@ -143,7 +154,7 @@ execute_process( #-----------------------------------------------------------------------------# -# CONFIGURATION (for now manual) +include(ConfigureCVC4) # Define to 1 if Boost threading library has support for thread attributes set(BOOST_HAS_THREAD_ATTR 0) @@ -221,11 +232,13 @@ set(STRERROR_R_CHAR_P 1) configure_file(cvc4autoconfig.new.h.in cvc4autoconfig.h) include_directories(${CMAKE_CURRENT_BINARY_DIR}) -# src/util/rational.h.in -# src/util/integer.h.in -set(CVC4_NEED_INT64_T_OVERLOADS 0) -set(CVC4_USE_CLN_IMP 0) -set(CVC4_USE_GMP_IMP 1) +if(USE_CLN) + set(CVC4_USE_CLN_IMP 1) + set(CVC4_USE_GMP_IMP 0) +else() + set(CVC4_USE_CLN_IMP 0) + set(CVC4_USE_GMP_IMP 1) +endif() set(CVC4_USE_SYMFPU 0) diff --git a/cmake/ConfigureCVC4.cmake b/cmake/ConfigureCVC4.cmake new file mode 100644 index 000000000..bd88a2a1d --- /dev/null +++ b/cmake/ConfigureCVC4.cmake @@ -0,0 +1,36 @@ +include(CheckCXXSourceCompiles) + +# Check whether "long" and "int64_t" are distinct types w.r.t. overloading. +# Even if they have the same size, they can be distinct, and some platforms +# can have problems with ambiguous function calls when auto-converting +# int64_t to long, and others will complain if you overload a function +# that takes an int64_t with one that takes a long (giving a redefinition +# error). So we have to keep both happy. Probably the same underlying +# issue as the hash specialization below, but let's check separately +# for flexibility. + +check_cxx_source_compiles( + "#include <stdint.h> + void foo(long) {} + void foo(int64_t) {} + int main() { return 0; }" + CVC4_NEED_INT64_T_OVERLOADS +) +if(NOT CVC4_NEED_INT64_T_OVERLOADS) + set(CVC4_NEED_INT64_T_OVERLOADS 0) +endif() + +# Check to see if this version/architecture of GNU C++ explicitly +# instantiates std::hash<uint64_t> or not. Some do, some don't. +# See src/util/hash.h. + +check_cxx_source_compiles( + "#include <cstdint> + #include <functional> + namespace std { template<> struct hash<uint64_t> {}; } + int main() { return 0; }" + CVC4_NEED_HASH_UINT64_T_OVERLOAD +) +if(CVC4_NEED_HASH_UINT64_T_OVERLOAD) + add_definitions(-DCVC4_NEED_HASH_UINT64_T) +endif() diff --git a/cmake/FindCLN.cmake b/cmake/FindCLN.cmake new file mode 100644 index 000000000..2cb33eb7e --- /dev/null +++ b/cmake/FindCLN.cmake @@ -0,0 +1,27 @@ +# Find CLN +# CLN_FOUND - system has CLN lib +# CLN_INCLUDE_DIR - the CLN include directory +# CLN_LIBRARIES - Libraries needed to use CLN + +find_path(CLN_INCLUDE_DIR NAMES cln/cln.h) +find_library(CLN_LIBRARIES NAMES cln) + + +if(CLN_INCLUDE_DIR) + file(STRINGS + "${CLN_INCLUDE_DIR}/cln/version.h" version_info + REGEX "^#define[ \t]+CL_VERSION_.*") + string(REGEX REPLACE + "^.*_MAJOR[ \t]+([0-9]+).*" "\\1" version_major "${version_info}") + string(REGEX REPLACE + "^.*_MINOR[ \t]+([0-9]+).*" "\\1" version_minor "${version_info}") + string(REGEX REPLACE + "^.*_PATCHLEVEL[ \t]+([0-9]+).*" "\\1" version_patch "${version_info}") + set(CLN_VERSION ${version_major}.${version_minor}.${version_patch}) + + include(FindPackageHandleStandardArgs) + find_package_handle_standard_args(CLN + REQUIRED_VARS CLN_INCLUDE_DIR CLN_LIBRARIES + VERSION_VAR CLN_VERSION) + mark_as_advanced(CLN_INCLUDE_DIR CLN_LIBRARIES) +endif() diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 0cbdb5d77..54c921371 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -60,18 +60,13 @@ set(util_src_files utility.h ) -#TODO: if CVC4_CLN_IMP -#list(APPEND util_src_files -# rational_cln_imp.cpp -# integer_cln_imp.cpp -#) +if(CVC4_USE_CLN_IMP) + list(APPEND util_src_files rational_cln_imp.cpp integer_cln_imp.cpp) +endif() - -#TODO: if CVC4_GMP_IMP -list(APPEND util_src_files - rational_gmp_imp.cpp - integer_gmp_imp.cpp -) +if(CVC4_USE_GMP_IMP) + list(APPEND util_src_files rational_gmp_imp.cpp integer_gmp_imp.cpp) +endif() add_library(util SHARED ${util_src_files}) set_target_properties(util PROPERTIES COMPILE_DEFINITIONS __BUILDING_CVC4LIB) |