From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Tue, 14 Aug 2018 00:21:13 +0000 (-0700)
Subject: cmake: Add module finder for CryptoMiniSat.
X-Git-Tag: cvc5-1.0.0~4612
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d45041a10431c39162b3e990eb88705e4c2ab179;p=cvc5.git

cmake: Add module finder for CryptoMiniSat.
---

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 624644fc4..355a315ff 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -106,14 +106,19 @@ message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
 
 #-----------------------------------------------------------------------------#
 
-option(USE_CLN         "Use CLN instead of GMP" OFF)
-option(ENABLE_PROOFS   "Enable proof support" OFF)
-option(USE_SYMFPU      "Use SymFPU for floating point support" OFF)
+option(ENABLE_PROOFS     "Enable proof support" OFF)
+option(USE_CLN           "Use CLN instead of GMP" OFF)
+option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver" OFF)
+option(USE_SYMFPU        "Use SymFPU for floating point support" OFF)
 
 #-----------------------------------------------------------------------------#
 
 find_package(PythonInterp REQUIRED)
 
+find_package(ANTLR REQUIRED)
+cvc4_link_library(${ANTLR_LIBRARIES})
+include_directories(${ANTLR_INCLUDE_DIR})
+
 find_package(GMP REQUIRED)
 cvc4_link_library(${GMP_LIBRARIES})
 include_directories(${GMP_INCLUDE_DIR})
@@ -124,15 +129,23 @@ if(USE_CLN)
   include_directories(${CLN_INCLUDE_DIR})
 endif()
 
+if(USE_CRYPTOMINISAT)
+  # CryptoMiniSat requires pthreads support
+  set(THREADS_PREFER_PTHREAD_FLAG ON)
+  find_package(Threads REQUIRED)
+  if(THREADS_HAVE_PTHREAD_ARG)
+    add_c_cxx_flag(-pthread)
+  endif()
+  find_package(CryptoMiniSat REQUIRED)
+  cvc4_link_library(${CryptoMiniSat_LIBRARIES})
+  include_directories(${CryptoMiniSat_INCLUDE_DIR})
+endif()
+
 if(USE_SYMFPU)
   find_package(SymFPU REQUIRED)
   include_directories(${SymFPU_INCLUDE_DIR})
 endif()
 
-find_package(ANTLR REQUIRED)
-cvc4_link_library(${ANTLR_LIBRARIES})
-include_directories(${ANTLR_INCLUDE_DIR})
-
 #-----------------------------------------------------------------------------#
 
 add_check_c_flag("-fexceptions")
@@ -248,6 +261,10 @@ else()
   set(CVC4_USE_GMP_IMP 1)
 endif()
 
+if(USE_CRYPTOMINISAT)
+  add_definitions(-DCVC4_USE_CRYPTOMINISAT)
+endif()
+
 if(USE_SYMFPU)
   add_definitions(-DCVC4_USE_SYMFPU)
   set(CVC4_USE_SYMFPU 1)
diff --git a/cmake/FindCryptoMiniSat.cmake b/cmake/FindCryptoMiniSat.cmake
new file mode 100644
index 000000000..1706efb9c
--- /dev/null
+++ b/cmake/FindCryptoMiniSat.cmake
@@ -0,0 +1,18 @@
+# Find CryptoMiniSat
+# CryptoMiniSat_FOUND - system has CryptoMiniSat lib
+# CryptoMiniSat_INCLUDE_DIR - the CryptoMiniSat include directory
+# CryptoMiniSat_LIBRARIES - Libraries needed to use CryptoMiniSat
+
+find_path(CryptoMiniSat_INCLUDE_DIR
+          NAMES cryptominisat5/cryptominisat.h
+          PATHS "${PROJECT_SOURCE_DIR}/cryptominisat5/install/include")
+find_library(CryptoMiniSat_LIBRARIES
+             NAMES cryptominisat5
+             PATHS "${PROJECT_SOURCE_DIR}/cryptominisat5/install/lib")
+
+include(FindPackageHandleStandardArgs)
+find_package_handle_standard_args(CryptoMiniSat
+  DEFAULT_MSG
+  CryptoMiniSat_INCLUDE_DIR CryptoMiniSat_LIBRARIES)
+
+mark_as_advanced(CryptoMiniSat_INCLUDE_DIR CryptoMiniSat_LIBRARIES)