From 9054be41a79824bf766413a8d704e5dd14baca40 Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Mon, 13 Aug 2018 17:37:24 -0700
Subject: [PATCH] cmake: Add module finder for CaDiCaL.

---
 CMakeLists.txt          | 45 ++++++++++++++++++++---------------------
 cmake/FindCaDiCaL.cmake | 18 +++++++++++++++++
 2 files changed, 40 insertions(+), 23 deletions(-)
 create mode 100644 cmake/FindCaDiCaL.cmake

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 355a315ff..07bd3ac97 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -107,6 +107,7 @@ message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
 #-----------------------------------------------------------------------------#
 
 option(ENABLE_PROOFS     "Enable proof support" OFF)
+option(USE_CADICAL       "Use CaDiCaL SAT solver" 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)
@@ -123,10 +124,26 @@ find_package(GMP REQUIRED)
 cvc4_link_library(${GMP_LIBRARIES})
 include_directories(${GMP_INCLUDE_DIR})
 
+if(ENABLE_PROOFS)
+  add_definitions(-DCVC4_PROOF)
+endif()
+
+if(USE_CADICAL)
+  find_package(CaDiCaL REQUIRED)
+  cvc4_link_library(${CaDiCaL_LIBRARIES})
+  include_directories(${CaDiCaL_INCLUDE_DIR})
+  add_definitions(-DCVC4_USE_CADICAL)
+endif()
+
 if(USE_CLN)
   find_package(CLN 1.2.2 REQUIRED)
   cvc4_link_library(${CLN_LIBRARIES})
   include_directories(${CLN_INCLUDE_DIR})
+  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()
 
 if(USE_CRYPTOMINISAT)
@@ -139,11 +156,16 @@ if(USE_CRYPTOMINISAT)
   find_package(CryptoMiniSat REQUIRED)
   cvc4_link_library(${CryptoMiniSat_LIBRARIES})
   include_directories(${CryptoMiniSat_INCLUDE_DIR})
+  add_definitions(-DCVC4_USE_CRYPTOMINISAT)
 endif()
 
 if(USE_SYMFPU)
   find_package(SymFPU REQUIRED)
   include_directories(${SymFPU_INCLUDE_DIR})
+  add_definitions(-DCVC4_USE_SYMFPU)
+  set(CVC4_USE_SYMFPU 1)
+else()
+  set(CVC4_USE_SYMFPU 0)
 endif()
 
 #-----------------------------------------------------------------------------#
@@ -253,29 +275,6 @@ set(STRERROR_R_CHAR_P 1)
 configure_file(cvc4autoconfig.new.h.in cvc4autoconfig.h)
 include_directories(${CMAKE_CURRENT_BINARY_DIR})
 
-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()
-
-if(USE_CRYPTOMINISAT)
-  add_definitions(-DCVC4_USE_CRYPTOMINISAT)
-endif()
-
-if(USE_SYMFPU)
-  add_definitions(-DCVC4_USE_SYMFPU)
-  set(CVC4_USE_SYMFPU 1)
-else()
-  set(CVC4_USE_SYMFPU 0)
-endif()
-
-if(ENABLE_PROOFS)
-  add_definitions(-DCVC4_PROOF)
-endif()
-
 #-----------------------------------------------------------------------------#
 
 add_subdirectory(doc)
diff --git a/cmake/FindCaDiCaL.cmake b/cmake/FindCaDiCaL.cmake
new file mode 100644
index 000000000..e3a045911
--- /dev/null
+++ b/cmake/FindCaDiCaL.cmake
@@ -0,0 +1,18 @@
+# Find CaDiCaL
+# CaDiCaL_FOUND - system has CaDiCaL lib
+# CaDiCaL_INCLUDE_DIR - the CaDiCaL include directory
+# CaDiCaL_LIBRARIES - Libraries needed to use CaDiCaL
+
+find_path(CaDiCaL_INCLUDE_DIR
+          NAMES cadical.hpp
+          PATHS "${PROJECT_SOURCE_DIR}/cadical/src")
+find_library(CaDiCaL_LIBRARIES
+             NAMES cadical
+             PATHS "${PROJECT_SOURCE_DIR}/cadical/build")
+
+include(FindPackageHandleStandardArgs)
+find_package_handle_standard_args(CaDiCaL
+  DEFAULT_MSG
+  CaDiCaL_INCLUDE_DIR CaDiCaL_LIBRARIES)
+
+mark_as_advanced(CaDiCaL_INCLUDE_DIR CaDiCaL_LIBRARIES)
-- 
2.30.2