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 /contrib | |
| 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 'contrib')
| -rwxr-xr-x | contrib/get-drat2er | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/contrib/get-drat2er b/contrib/get-drat2er new file mode 100755 index 000000000..e465ab3d4 --- /dev/null +++ b/contrib/get-drat2er @@ -0,0 +1,25 @@ +#!/bin/bash +# +source "$(dirname "$0")/get-script-header.sh" +if [ -e drat2er ]; then + echo 'error: file or directory "drat2er" exists; please move it out of the way.' >&2 + exit 1 +fi + +git clone https://github.com/alex-ozdemir/drat2er.git + +cd drat2er + +git checkout api + +mkdir build + +cd build + +cmake .. -DCMAKE_INSTALL_PREFIX=$(pwd)/install + +make install + +echo +echo ===================== Now configure CVC4 with ===================== +echo ./configure.sh --drat2er |