cmake: Add module finder for LFSC.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 07bd3ac97d4f97b5f02888dcec5faeeb73497c03..c54ddfd87e741c176d76dc2af8f5ef7e17be440e 100644 (file)
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -110,6 +110,7 @@ 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_LFSC          "Use LFSC proof checker" OFF)
 option(USE_SYMFPU        "Use SymFPU for floating point support" OFF)
 
 #-----------------------------------------------------------------------------#
@@ -159,6 +160,15 @@ if(USE_CRYPTOMINISAT)
   add_definitions(-DCVC4_USE_CRYPTOMINISAT)
 endif()
 
+if(USE_LFSC)
+  find_package(LFSC REQUIRED)
+  include_directories(${LFSC_INCLUDE_DIR})
+  add_definitions(-DCVC4_USE_LFSC)
+  set(CVC4_USE_LFSC 1)
+else()
+  set(CVC4_USE_LFSC 0)
+endif()
+
 if(USE_SYMFPU)
   find_package(SymFPU REQUIRED)
   include_directories(${SymFPU_INCLUDE_DIR})

diff --git a/cmake/FindLFSC.cmake b/cmake/FindLFSC.cmake
new file mode 100644 (file)
index 0000000..7176b20
--- /dev/null
+++ b/cmake/FindLFSC.cmake
@@ -0,0 +1,18 @@
+# Find LFSC
+# LFSC_FOUND - system has LFSC lib
+# LFSC_INCLUDE_DIR - the LFSC include directory
+# LFSC_LIBRARIES - Libraries needed to use LFSC
+
+find_path(LFSC_INCLUDE_DIR
+          NAMES lfscc.h
+          PATHS "${PROJECT_SOURCE_DIR}/lfsc-checker/install/include")
+find_library(LFSC_LIBRARIES
+             NAMES lfscc
+             PATHS "${PROJECT_SOURCE_DIR}/lfsc-checker/install/lib")
+
+include(FindPackageHandleStandardArgs)
+find_package_handle_standard_args(LFSC
+  DEFAULT_MSG
+  LFSC_INCLUDE_DIR LFSC_LIBRARIES)
+
+mark_as_advanced(LFSC_INCLUDE_DIR LFSC_LIBRARIES)