Removing unused build options and deprecated proof compile flag (#6195)

1 files changed, 0 insertions, 35 deletions

diff --git a/configure.sh b/configure.sh
index d57bcd5d5..43925a504 100755
--- a/configure.sh
+++ b/configure.sh
@@ -32,7 +32,6 @@ The following flags enable optional features (disable with --no-<option name>).
   --static                 build static libraries and binaries [default=no]
   --static-binary          statically link against system libraries
                            (must be disabled for static macOS builds) [default=yes]
-  --proofs                 support for proof generation
   --debug-symbols          include debug symbols
   --valgrind               Valgrind instrumentation
   --debug-context-mm       use the debug context memory manager
@@ -60,9 +59,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)
   --kissat                 use the Kissat SAT solver
-  --lfsc                   use the LFSC proof checker
   --poly                   use the LibPoly library
   --symfpu                 use SymFPU for floating point solver
   --editline               support the editline library
@@ -72,11 +69,9 @@ 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
   --glpk-dir=PATH          path to top level of GLPK installation
   --gmp-dir=PATH           path to top level of GMP installation
   --kissat-dir=PATH        path to top level of Kissat source tree
-  --lfsc-dir=PATH          path to top level of LFSC source tree
   --poly-dir=PATH          path to top level of LibPoly source tree
   --symfpu-dir=PATH        path to top level of SymFPU source tree
 
@@ -123,17 +118,14 @@ coverage=default
 cryptominisat=default
 debug_context_mm=default
 debug_symbols=default
-drat2er=default
 dumping=default
 glpk=default
 gpl=default
 kissat=default
-lfsc=default
 poly=default
 muzzle=default
 ninja=default
 profiling=default
-proofs=default
 python2=default
 python_bindings=default
 java_bindings=default
@@ -155,11 +147,9 @@ abc_dir=default
 antlr_dir=default
 cadical_dir=default
 cryptominisat_dir=default
-drat2er_dir=default
 glpk_dir=default
 gmp_dir=default
 kissat_dir=default
-lfsc_dir=default
 poly_dir=default
 symfpu_dir=default
 
@@ -235,9 +225,6 @@ 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;;
 
@@ -256,18 +243,12 @@ do
     --glpk) glpk=ON;;
     --no-glpk) glpk=OFF;;
 
-    --lfsc) lfsc=ON;;
-    --no-lfsc) lfsc=OFF;;
-
     --poly) poly=ON;;
     --no-poly) poly=OFF;;
 
     --muzzle) muzzle=ON;;
     --no-muzzle) muzzle=OFF;;
 
-    --proofs) proofs=ON;;
-    --no-proofs) proofs=OFF;;
-
     --static) shared=OFF; static_binary=ON;;
     --no-static) shared=ON;;
 
@@ -320,9 +301,6 @@ do
     --cryptominisat-dir) die "missing argument to $1 (try -h)" ;;
     --cryptominisat-dir=*) cryptominisat_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##*=} ;;
 
@@ -332,9 +310,6 @@ do
     --kissat-dir) die "missing argument to $1 (try -h)" ;;
     --kissat-dir=*) kissat_dir=${1##*=} ;;
 
-    --lfsc-dir) die "missing argument to $1 (try -h)" ;;
-    --lfsc-dir=*) lfsc_dir=${1##*=} ;;
-
     --poly-dir) die "missing argument to $1 (try -h)" ;;
     --poly-dir=*) poly_dir=${1##*=} ;;
 
@@ -411,8 +386,6 @@ cmake_opts=""
 [ $ninja != default ] && cmake_opts="$cmake_opts -G Ninja"
 [ $muzzle != default ] \
   && cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle"
-[ $proofs != default ] \
-  && cmake_opts="$cmake_opts -DENABLE_PROOFS=$proofs"
 [ $shared != default ] \
   && cmake_opts="$cmake_opts -DENABLE_SHARED=$shared"
 [ $static_binary != default ] \
@@ -443,14 +416,10 @@ 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"
 [ $kissat != default ] \
   && cmake_opts="$cmake_opts -DUSE_KISSAT=$kissat"
-[ $lfsc != default ] \
-  && cmake_opts="$cmake_opts -DUSE_LFSC=$lfsc"
 [ $poly != default ] \
   && cmake_opts="$cmake_opts -DUSE_POLY=$poly"
 [ $symfpu != default ] \
@@ -463,16 +432,12 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DCADICAL_DIR=$cadical_dir"
 [ "$cryptominisat_dir" != default ] \
   && cmake_opts="$cmake_opts -DCRYPTOMINISAT_DIR=$cryptominisat_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 ] \
   && cmake_opts="$cmake_opts -DGMP_DIR=$gmp_dir"
 [ "$kissat_dir" != default ] \
   && cmake_opts="$cmake_opts -DKISSAT=$kissat_dir"
-[ "$lfsc_dir" != default ] \
-  && cmake_opts="$cmake_opts -DLFSC_DIR=$lfsc_dir"
 [ "$poly_dir" != default ] \
   && cmake_opts="$cmake_opts -DPOLY_DIR=$poly_dir"
 [ "$symfpu_dir" != default ] \