diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-05-22 06:41:50 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-05-22 08:41:50 -0500 |
commit | c531152e6a707b66b885e508ea61e2a67e195ccc (patch) | |
tree | a18a2d342b03db1700a963470f2064cf3ac8d086 /configure.sh | |
parent | ae33f11d0f4156b4d21b9e77f6df59ec0f9e8184 (diff) |
Add support for SAT solver Kissat. (#4514)
Diffstat (limited to 'configure.sh')
-rwxr-xr-x | configure.sh | 36 |
1 files changed, 25 insertions, 11 deletions
diff --git a/configure.sh b/configure.sh index 070e2c230..21a444082 100755 --- a/configure.sh +++ b/configure.sh @@ -63,6 +63,7 @@ The following flags enable optional packages (disable with --no-<option name>). --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 --symfpu use SymFPU for floating point solver --readline support the readline library @@ -76,6 +77,7 @@ Optional Path to Optional Packages: --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 + --kissat-dir=PATH path to top level of Kissat source tree --lfsc-dir=PATH path to top level of LFSC source tree --symfpu-dir=PATH path to top level of SymFPU source tree @@ -110,8 +112,6 @@ buildtype=default abc=default asan=default -ubsan=default -tsan=default assertions=default best=default cadical=default @@ -119,30 +119,33 @@ cln=default comp_inc=default coverage=default cryptominisat=default -debug_symbols=default debug_context_mm=default +debug_symbols=default drat2er=default dumping=default -gpl=default -win64=default -ninja=default glpk=default +gpl=default +kissat=default lfsc=default muzzle=default +ninja=default optimized=default +profiling=default proofs=default +python2=default +python3=default +python_bindings=default +readline=default shared=default static_binary=default statistics=default symfpu=default tracing=default +tsan=default +ubsan=default unit_testing=default -python2=default -python3=default -python_bindings=default valgrind=default -profiling=default -readline=default +win64=default language_bindings_java=default language_bindings_python=default @@ -155,6 +158,7 @@ drat2er_dir=default cxxtest_dir=default glpk_dir=default gmp_dir=default +kissat_dir=default lfsc_dir=default symfpu_dir=default @@ -228,6 +232,9 @@ do --gpl) gpl=ON;; --no-gpl) gpl=OFF;; + --kissat) kissat=ON;; + --no-kissat) kissat=OFF;; + --win64) win64=ON;; --no-win64) win64=OFF;; @@ -325,6 +332,9 @@ do --gmp-dir) die "missing argument to $1 (try -h)" ;; --gmp-dir=*) gmp_dir=${1##*=} ;; + --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##*=} ;; @@ -418,6 +428,8 @@ cmake_opts="" && 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" [ $symfpu != default ] \ @@ -444,6 +456,8 @@ cmake_opts="" && 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" [ "$symfpu_dir" != default ] \ |