From 782da6094716b80d3b2b50eb126a0d5fe1cd8c89 Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Mon, 13 Aug 2018 17:49:47 -0700
Subject: [PATCH] cmake: Add module finder for LFSC.

---
 CMakeLists.txt       | 10 ++++++++++
 cmake/FindLFSC.cmake | 18 ++++++++++++++++++
 2 files changed, 28 insertions(+)
 create mode 100644 cmake/FindLFSC.cmake

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 07bd3ac97..c54ddfd87 100644
--- 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
index 000000000..7176b2015
--- /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)
-- 
2.30.2