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 /configure.sh | |
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 'configure.sh')
-rwxr-xr-x | configure.sh | 14 |
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 ] \ |