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/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 'src/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 4 |
1 files changed, 4 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}) |