diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-08-13 17:49:47 -0700 |
|---|---|---|
| committer | Mathias Preiner <mathias.preiner@gmail.com> | 2018-09-22 16:30:59 -0700 |
| commit | 782da6094716b80d3b2b50eb126a0d5fe1cd8c89 (patch) | |
| tree | 877d1645cb9a5b50d6f9ffe327beaf1a9ba9f9fb /CMakeLists.txt | |
| parent | 9054be41a79824bf766413a8d704e5dd14baca40 (diff) | |
cmake: Add module finder for LFSC.
Diffstat (limited to 'CMakeLists.txt')
| -rw-r--r-- | CMakeLists.txt | 10 |
1 files changed, 10 insertions, 0 deletions
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}) |