-#!/bin/sh
+#!/bin/bash
#--------------------------------------------------------------------------#
+set -e -o pipefail
+
usage () {
cat <<EOF
Usage: $0 [<build type>] [<option> ...]
--python2 prefer using Python 2 (also for Python bindings)
--python3 prefer using Python 3 (also for Python bindings)
--python-bindings build Python bindings based on new C++ API
+ --java-bindings build Java bindings based on new C++ API
+ --all-bindings build bindings for all supported languages
--asan build with ASan instrumentation
--ubsan build with UBSan instrumentation
--tsan build with TSan instrumentation
-The following options configure parameterized features.
-
- --language-bindings[=java,python,all]
- specify language bindings to build
-
Optional Packages:
The following flags enable optional packages (disable with --no-<option name>).
--cln use CLN instead of GMP
--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
- --readline support the readline library
+ --editline support the editline library
Optional Path to Optional Packages:
--abc-dir=PATH path to top level of ABC source tree
--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
+ --poly-dir=PATH path to top level of LibPoly source tree
--symfpu-dir=PATH path to top level of SymFPU source tree
+Build limitations:
+ --lib-only only build the library, but not the executable or
+ the parser (default: off)
+
EOF
exit 0
}
abc=default
asan=default
-ubsan=default
-tsan=default
assertions=default
best=default
cadical=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
+poly=default
muzzle=default
+ninja=default
optimized=default
+profiling=default
proofs=default
+python2=default
+python3=default
+python_bindings=default
+java_bindings=default
+editline=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
-
-language_bindings_java=default
-language_bindings_python=default
+win64=default
abc_dir=default
antlr_dir=default
cxxtest_dir=default
glpk_dir=default
gmp_dir=default
+kissat_dir=default
lfsc_dir=default
+poly_dir=default
symfpu_dir=default
+lib_only=default
+
#--------------------------------------------------------------------------#
while [ $# -gt 0 ]
--gpl) gpl=ON;;
--no-gpl) gpl=OFF;;
+ --kissat) kissat=ON;;
+ --no-kissat) kissat=OFF;;
+
--win64) win64=ON;;
--no-win64) win64=OFF;;
--lfsc) lfsc=ON;;
--no-lfsc) lfsc=OFF;;
+ --poly) poly=ON;;
+ --no-poly) poly=OFF;;
+
--muzzle) muzzle=ON;;
--no-muzzle) muzzle=OFF;;
--python-bindings) python_bindings=ON;;
--no-python-bindings) python_bindings=OFF;;
+ --java-bindings) java_bindings=ON;;
+ --no-java-bindings) java_bindings=OFF;;
+
+ --all-bindings) python_bindings=ON;;
+
--valgrind) valgrind=ON;;
--no-valgrind) valgrind=OFF;;
--profiling) profiling=ON;;
--no-profiling) profiling=OFF;;
- --readline) readline=ON;;
- --no-readline) readline=OFF;;
-
- --language-bindings) die "missing argument to $1 (try -h)" ;;
- --language-bindings=*)
- lang="${1##*=}"
- IFS=','
- for l in $lang; do
- case $l in
- java) language_bindings_java=ON ;;
- python) language_bindings_python=ON ;;
- all)
- language_bindings_python=ON
- language_bindings_java=ON ;;
- *) die "invalid language binding '$l' specified (try -h)" ;;
- esac
- done
- unset IFS
- ;;
+ --editline) editline=ON;;
+ --no-editline) editline=OFF;;
--abc-dir) die "missing argument to $1 (try -h)" ;;
--abc-dir=*) abc_dir=${1##*=} ;;
--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##*=} ;;
+ --poly-dir) die "missing argument to $1 (try -h)" ;;
+ --poly-dir=*) poly_dir=${1##*=} ;;
+
--symfpu-dir) die "missing argument to $1 (try -h)" ;;
--symfpu-dir=*) symfpu_dir=${1##*=} ;;
+ --lib-only) lib_only=ON ;;
+
-*) die "invalid option '$1' (try -h)";;
*) case $1 in
&& cmake_opts="$cmake_opts -DUSE_PYTHON3=$python3"
[ $python_bindings != default ] \
&& cmake_opts="$cmake_opts -DBUILD_BINDINGS_PYTHON=$python_bindings"
+[ $java_bindings != default ] \
+ && cmake_opts="$cmake_opts -DBUILD_BINDINGS_JAVA=$java_bindings"
[ $valgrind != default ] \
&& cmake_opts="$cmake_opts -DENABLE_VALGRIND=$valgrind"
[ $profiling != default ] \
&& cmake_opts="$cmake_opts -DENABLE_PROFILING=$profiling"
-[ $readline != default ] \
- && cmake_opts="$cmake_opts -DUSE_READLINE=$readline"
+[ $editline != default ] \
+ && cmake_opts="$cmake_opts -DUSE_EDITLINE=$editline"
[ $abc != default ] \
&& cmake_opts="$cmake_opts -DUSE_ABC=$abc"
[ $cadical != 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 ] \
&& cmake_opts="$cmake_opts -DUSE_SYMFPU=$symfpu"
-
-[ $language_bindings_java != default ] \
- && cmake_opts="$cmake_opts -DBUILD_SWIG_BINDINGS_JAVA=$language_bindings_java"
-[ $language_bindings_python != default ] \
- && cmake_opts="$cmake_opts -DBUILD_SWIG_BINDINGS_PYTHON=$language_bindings_python"
-
[ "$abc_dir" != default ] \
&& cmake_opts="$cmake_opts -DABC_DIR=$abc_dir"
[ "$antlr_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 ] \
&& cmake_opts="$cmake_opts -DSYMFPU_DIR=$symfpu_dir"
+[ "$lib_only" != default ] \
+ && cmake_opts="$cmake_opts -DBUILD_LIB_ONLY=$lib_only"
[ "$install_prefix" != default ] \
&& cmake_opts="$cmake_opts -DCMAKE_INSTALL_PREFIX=$install_prefix"
[ -n "$program_prefix" ] \
[ $win64 = ON ] && [ -e "$build_dir" ] && rm -r "$build_dir"
mkdir -p "$build_dir"
-cd "$build_dir" || exit 1
+cd "$build_dir"
[ -e CMakeCache.txt ] && rm CMakeCache.txt
build_dir_escaped=$(echo "$build_dir" | sed 's/\//\\\//g')
projects / cvc5.git / blobdiff