projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3323571) | patch
Configured for linking against drat2er (#2754)
authorAlex Ozdemir <aozdemir@hmc.edu>
Mon, 17 Dec 2018 23:01:23 +0000 (15:01 -0800)
committerAina Niemetz <aina.niemetz@gmail.com>
Mon, 17 Dec 2018 23:01:23 +0000 (15:01 -0800)
commit6660ab05c399d309208251263faeff3be2964f7b
treeec7ba5d8c9d1ff90611bfce726acb3044be39d6dtree
parent332357104e9ab1937049f0ea8e53042d8534f966commit | 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.
CMakeLists.txt diff | blob | history
cmake/FindDrat2Er.cmake [new file with mode: 0644] blob
configure.sh diff | blob | history
contrib/get-drat2er [new file with mode: 0755] blob
src/CMakeLists.txt diff | blob | history
src/base/configuration_private.h diff | blob | history