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.

1 files changed, 14 insertions, 0 deletions

diff --git a/configure.sh b/configure.sh
index 7fa842f70..e53d8caa7 100755
--- a/configure.sh
+++ b/configure.sh
@@ -55,6 +55,7 @@ The following flags enable optional packages (disable with --no-<option name>).
   --abc                    use the ABC AIG library
   --cadical                use the CaDiCaL SAT solver
   --cryptominisat          use the CryptoMiniSat SAT solver
+  --drat2er                use drat2er (required for eager BV proofs)
   --lfsc                   use the LFSC proof checker
   --symfpu                 use SymFPU for floating point solver
   --portfolio              build the multithreaded portfolio version of CVC4
@@ -66,6 +67,7 @@ Optional Path to Optional Packages:
   --antlr-dir=PATH         path to ANTLR C headers and libraries
   --cadical-dir=PATH       path to top level of CaDiCaL source tree
   --cryptominisat-dir=PATH path to top level of CryptoMiniSat source tree
+  --drat2er-dir=PATH       path to the top level of the drat2er installation
   --cxxtest-dir=PATH       path to CxxTest installation
   --glpk-dir=PATH          path to top level of GLPK installation
   --gmp-dir=PATH           path to top level of GMP installation
@@ -112,6 +114,7 @@ coverage=default
 cryptominisat=default
 debug_symbols=default
 debug_context_mm=default
+drat2er=default
 dumping=default
 gpl=default
 win64=default
@@ -141,6 +144,7 @@ abc_dir=default
 antlr_dir=default
 cadical_dir=default
 cryptominisat_dir=default
+drat2er_dir=default
 cxxtest_dir=default
 glpk_dir=default
 gmp_dir=default
@@ -202,6 +206,9 @@ do
     --debug-context-mm) debug_context_mm=ON;;
     --no-debug-context-mm) debug_context_mm=OFF;;
 
+    --drat2er) drat2er=ON;;
+    --no-drat2er) drat2er=OFF;;
+
     --dumping) dumping=ON;;
     --no-dumping) dumping=OFF;;
 
@@ -297,6 +304,9 @@ do
     --cxxtest-dir) die "missing argument to $1 (try -h)" ;;
     --cxxtest-dir=*) cxxtest_dir=${1##*=} ;;
 
+    --drat2er-dir) die "missing argument to $1 (try -h)" ;;
+    --drat2er-dir=*) drat2er_dir=${1##*=} ;;
+
     --glpk-dir) die "missing argument to $1 (try -h)" ;;
     --glpk-dir=*) glpk_dir=${1##*=} ;;
 
@@ -386,6 +396,8 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DUSE_CLN=$cln"
 [ $cryptominisat != default ] \
   && cmake_opts="$cmake_opts -DUSE_CRYPTOMINISAT=$cryptominisat"
+[ $drat2er != default ] \
+  && cmake_opts="$cmake_opts -DUSE_DRAT2ER=$drat2er"
 [ $glpk != default ] \
   && cmake_opts="$cmake_opts -DUSE_GLPK=$glpk"
 [ $lfsc != default ] \
@@ -408,6 +420,8 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DCRYPTOMINISAT_DIR=$cryptominisat_dir"
 [ "$cxxtest_dir" != default ] \
   && cmake_opts="$cmake_opts -DCXXTEST_DIR=$cxxtest_dir"
+[ "$drat2er_dir" != default ] \
+  && cmake_opts="$cmake_opts -DDRAT2ER_DIR=$drat2er_dir"
 [ "$glpk_dir" != default ] \
   && cmake_opts="$cmake_opts -DGLPK_DIR=$glpk_dir"
 [ "$gmp_dir" != default ] \