cmake: Add module finder for CryptoMiniSat.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 624644fc4aafd7aef13d383dad4a4002a54d79ed..355a315ffe9aca9b65ff63f8e257b727e7c02ffc 100644 (file)
--- 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 (file)
index 0000000..1706efb
--- /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)