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 /src | |
| 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 'src')
| -rw-r--r-- | src/CMakeLists.txt | 4 | ||||
| -rw-r--r-- | src/base/configuration_private.h | 6 |
2 files changed, 10 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 7ecee2dee..889260045 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -739,6 +739,10 @@ if(USE_CRYPTOMINISAT) target_link_libraries(cvc4 ${CryptoMiniSat_LIBRARIES}) target_include_directories(cvc4 PUBLIC ${CryptoMiniSat_INCLUDE_DIR}) endif() +if(USE_DRAT2ER) + target_link_libraries(cvc4 ${Drat2Er_LIBRARIES}) + target_include_directories(cvc4 PUBLIC ${Drat2Er_INCLUDE_DIR}) +endif() if(USE_GLPK) target_link_libraries(cvc4 ${GLPK_LIBRARIES}) target_include_directories(cvc4 PUBLIC ${GLPK_INCLUDE_DIR}) diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h index 5164d46bc..77f3f5e77 100644 --- a/src/base/configuration_private.h +++ b/src/base/configuration_private.h @@ -126,6 +126,12 @@ namespace CVC4 { # define IS_CRYPTOMINISAT_BUILD false #endif /* CVC4_USE_CRYPTOMINISAT */ +#if CVC4_USE_DRAT2ER +# define IS_DRAT2ER_BUILD true +#else /* CVC4_USE_DRAT2ER */ +# define IS_DRAT2ER_BUILD false +#endif /* CVC4_USE_DRAT2ER */ + #if CVC4_USE_LFSC #define IS_LFSC_BUILD true #else /* CVC4_USE_LFSC */ |