From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Mon, 13 Aug 2018 21:03:54 +0000 (-0700)
Subject: cmake: Add module finder for CLN.
X-Git-Tag: cvc5-1.0.0~4614
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=013a0fb7fe918d707604690a96ef6c0559af7440;p=cvc5.git

cmake: Add module finder for CLN.
---

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)