diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2018-12-17 15:01:23 -0800 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-12-17 15:01:23 -0800 |
| commit | 6660ab05c399d309208251263faeff3be2964f7b (patch) | |
| tree | ec7ba5d8c9d1ff90611bfce726acb3044be39d6d /CMakeLists.txt | |
| parent | 332357104e9ab1937049f0ea8e53042d8534f966 (diff) | |
Configured for linking against drat2er (#2754)
drat2er is a C/C++ project which includes support for
* Checking DRAT proofs
* Converting DRAT proofs to LRAT proofs
* Converting DRAT proofs to ER proofs
It does the first 2 by using drat-trim under the hood.
I've modified our CMake configuration to allow drat2er to be linked into
CVC4, and I added a contrib script.
Diffstat (limited to 'CMakeLists.txt')
| -rw-r--r-- | CMakeLists.txt | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 099fc00fa..3265830cc 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -93,6 +93,7 @@ cvc4_option(USE_READLINE "Use readline for better interactive support") # > for options where we don't need to detect if set by user (default: OFF) option(USE_CADICAL "Use CaDiCaL SAT solver") option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver") +option(USE_DRAT2ER "Include drat2er for making eager BV proofs") option(USE_LFSC "Use LFSC proof checker") option(USE_SYMFPU "Use SymFPU for floating point support") option(USE_PYTHON2 "Prefer using Python 2 (for Python bindings)") @@ -108,6 +109,7 @@ set(ANTLR_DIR "" CACHE STRING "Set ANTLR3 install directory") set(CADICAL_DIR "" CACHE STRING "Set CaDiCaL install directory") set(CRYPTOMINISAT_DIR "" CACHE STRING "Set CryptoMiniSat install directory") set(CXXTEST_DIR "" CACHE STRING "Set CxxTest install directory") +set(DRAT2ER_DIR "" CACHE STRING "Set drat2er install directory") set(GLPK_DIR "" CACHE STRING "Set GLPK install directory") set(GMP_DIR "" CACHE STRING "Set GMP install directory") set(LFSC_DIR "" CACHE STRING "Set LFSC install directory") @@ -410,6 +412,12 @@ if(USE_CRYPTOMINISAT) add_definitions(-DCVC4_USE_CRYPTOMINISAT) endif() +if(USE_DRAT2ER) + set(Drat2Er_HOME ${DRAT2ER_DIR}) + find_package(Drat2Er REQUIRED) + add_definitions(-DCVC4_USE_DRAT2ER) +endif() + if(USE_GLPK) set(GPL_LIBS "${GPL_LIBS} glpk") set(GLPK_HOME ${GLPK_DIR}) @@ -523,6 +531,7 @@ message("") print_config("ABC :" USE_ABC) print_config("CaDiCaL :" USE_CADICAL) print_config("CryptoMiniSat :" USE_CRYPTOMINISAT) +print_config("drat2er :" USE_DRAT2ER) print_config("GLPK :" USE_GLPK) print_config("LFSC :" USE_LFSC) @@ -546,6 +555,9 @@ endif() if(CRYPTOMINISAT_DIR) message("CRYPTOMINISAT dir : ${CRYPTOMINISAT_DIR}") endif() +if(DRAT2ER_DIR) + message("DRAT2ER dir : ${DRAT2ER_DIR}") +endif() if(GLPK_DIR) message("GLPK dir : ${GLPK_DIR}") endif() |