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

cmake: Add module finder for LFSC.
---

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)