--arm64 cross-compile for Linux ARM 64 bit
--win64 cross-compile for Windows 64 bit
--ninja use Ninja build system
+ --docs build Api documentation
Features:
--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
- --optimized optimize the build
+ --auto-download automatically download dependencies if necessary
--debug-symbols include debug symbols
--valgrind Valgrind instrumentation
--debug-context-mm use the debug context memory manager
--cln use CLN instead of GMP
--glpk use GLPK simplex solver
--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
+ --poly use the LibPoly library [default=yes]
+ --cocoa use the CoCoA library
--editline support the editline library
Optional Path to Optional Packages:
--abc-dir=PATH path to top level of ABC source tree
- --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
+ --dep-path=PATH path to a dependency installation dir
Build limitations:
--lib-only only build the library, but not the executable or
the parser (default: off)
+CMake Options (Advanced)
+ -DVAR=VALUE manually add CMake options
+
EOF
exit 0
}
abc=default
asan=default
assertions=default
-best=default
-cadical=default
+auto_download=default
cln=default
comp_inc=default
coverage=default
cryptominisat=default
debug_context_mm=default
debug_symbols=default
-drat2er=default
+docs=default
dumping=default
glpk=default
gpl=default
kissat=default
-lfsc=default
-poly=default
+poly=ON
+cocoa=default
muzzle=default
ninja=default
-optimized=default
profiling=default
-proofs=default
python2=default
python_bindings=default
java_bindings=default
shared=default
static_binary=default
statistics=default
-symfpu=default
tracing=default
tsan=default
ubsan=default
werror=default
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
lib_only=default
#--------------------------------------------------------------------------#
+cmake_opts=""
+
while [ $# -gt 0 ]
do
case $1 in
--assertions) assertions=ON;;
--no-assertions) assertions=OFF;;
- --best) best=ON;;
- --no-best) best=OFF;;
+ # Best configuration
+ --best)
+ abc=ON
+ cln=ON
+ cryptominisat=ON
+ glpk=ON
+ editline=ON
+ ;;
--prefix) die "missing argument to $1 (try -h)" ;;
--prefix=*)
--name) die "missing argument to $1 (try -h)" ;;
--name=*) build_dir=${1##*=} ;;
- --cadical) cadical=ON;;
- --no-cadical) cadical=OFF;;
-
--cln) cln=ON;;
--no-cln) cln=OFF;;
--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;;
--ninja) ninja=ON;;
+ --docs) docs=ON;;
+ --no-docs) docs=OFF;;
+
--glpk) glpk=ON;;
--no-glpk) glpk=OFF;;
- --lfsc) lfsc=ON;;
- --no-lfsc) lfsc=OFF;;
-
--poly) poly=ON;;
--no-poly) poly=OFF;;
+ --cocoa) cocoa=ON;;
+ --no-cocoa) cocoa=OFF;;
+
--muzzle) muzzle=ON;;
--no-muzzle) muzzle=OFF;;
- --optimized) optimized=ON;;
- --no-optimized) optimized=OFF;;
-
- --proofs) proofs=ON;;
- --no-proofs) proofs=OFF;;
-
--static) shared=OFF; static_binary=ON;;
--no-static) shared=ON;;
--static-binary) static_binary=ON;;
--no-static-binary) static_binary=OFF;;
+ --auto-download) auto_download=ON;;
+ --no-auto-download) auto_download=OFF;;
+
--statistics) statistics=ON;;
--no-statistics) statistics=OFF;;
- --symfpu) symfpu=ON;;
- --no-symfpu) symfpu=OFF;;
-
--tracing) tracing=ON;;
--no-tracing) tracing=OFF;;
--java-bindings) java_bindings=ON;;
--no-java-bindings) java_bindings=OFF;;
- --all-bindings) python_bindings=ON;;
+ --all-bindings)
+ python_bindings=ON
+ java_bindings=ON;;
--valgrind) valgrind=ON;;
--no-valgrind) valgrind=OFF;;
--abc-dir) die "missing argument to $1 (try -h)" ;;
--abc-dir=*) abc_dir=${1##*=} ;;
- --antlr-dir) die "missing argument to $1 (try -h)" ;;
- --antlr-dir=*) antlr_dir=${1##*=} ;;
-
- --cadical-dir) die "missing argument to $1 (try -h)" ;;
- --cadical-dir=*) cadical_dir=${1##*=} ;;
-
- --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##*=} ;;
- --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##*=} ;;
+ --dep-path) die "missing argument to $1 (try -h)" ;;
+ --dep-path=*) dep_path="${dep_path};${1##*=}" ;;
--lib-only) lib_only=ON ;;
+ -D*) cmake_opts="${cmake_opts} $1" ;;
-*) die "invalid option '$1' (try -h)";;
shift
done
-#--------------------------------------------------------------------------#
-# Automatically set up dependencies based on configure options
-#--------------------------------------------------------------------------#
-
-if [ "$arm64" == "ON" ]; then
- echo "Setting up dependencies for ARM 64-bit build"
- HOST="aarch64-linux-gnu" contrib/get-antlr-3.4 || exit 1
- HOST="aarch64-linux-gnu" contrib/get-gmp-dev || exit 1
-elif [ "$win64" == "ON" ]; then
- echo "Setting up dependencies for Windows 64-bit build"
- HOST="x86_64-w64-mingw32" contrib/get-antlr-3.4 || exit 1
- HOST="x86_64-w64-mingw32" contrib/get-gmp-dev || exit 1
-fi
-
#--------------------------------------------------------------------------#
if [ $werror != default ]; then
export CXXFLAGS=-Werror
fi
-cmake_opts=""
-
[ $buildtype != default ] \
&& cmake_opts="$cmake_opts -DCMAKE_BUILD_TYPE=$buildtype"
[ $asan != default ] \
&& cmake_opts="$cmake_opts -DENABLE_ASAN=$asan"
+[ $auto_download != default ] \
+ && cmake_opts="$cmake_opts -DENABLE_AUTO_DOWNLOAD=$auto_download"
[ $ubsan != default ] \
&& cmake_opts="$cmake_opts -DENABLE_UBSAN=$ubsan"
[ $tsan != default ] \
&& cmake_opts="$cmake_opts -DENABLE_TSAN=$tsan"
[ $assertions != default ] \
&& cmake_opts="$cmake_opts -DENABLE_ASSERTIONS=$assertions"
-[ $best != default ] \
- && cmake_opts="$cmake_opts -DENABLE_BEST=$best"
[ $comp_inc != default ] \
&& cmake_opts="$cmake_opts -DENABLE_COMP_INC_TRACK=$comp_inc"
[ $coverage != default ] \
[ $ninja != default ] && cmake_opts="$cmake_opts -G Ninja"
[ $muzzle != default ] \
&& cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle"
-[ $optimized != default ] \
- && cmake_opts="$cmake_opts -DENABLE_OPTIMIZED=$optimized"
-[ $proofs != default ] \
- && cmake_opts="$cmake_opts -DENABLE_PROOFS=$proofs"
[ $shared != default ] \
&& cmake_opts="$cmake_opts -DENABLE_SHARED=$shared"
[ $static_binary != default ] \
&& cmake_opts="$cmake_opts -DENABLE_UNIT_TESTING=$unit_testing"
[ $python2 != default ] \
&& cmake_opts="$cmake_opts -DUSE_PYTHON2=$python2"
+[ $docs != default ] \
+ && cmake_opts="$cmake_opts -DBUILD_DOCS=$docs"
[ $python_bindings != default ] \
&& cmake_opts="$cmake_opts -DBUILD_BINDINGS_PYTHON=$python_bindings"
[ $java_bindings != default ] \
&& cmake_opts="$cmake_opts -DUSE_EDITLINE=$editline"
[ $abc != default ] \
&& cmake_opts="$cmake_opts -DUSE_ABC=$abc"
-[ $cadical != default ] \
- && cmake_opts="$cmake_opts -DUSE_CADICAL=$cadical"
[ $cln != default ] \
&& 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 ] \
- && cmake_opts="$cmake_opts -DUSE_SYMFPU=$symfpu"
+[ $cocoa != default ] \
+ && cmake_opts="$cmake_opts -DUSE_COCOA=$cocoa"
[ "$abc_dir" != default ] \
&& cmake_opts="$cmake_opts -DABC_DIR=$abc_dir"
-[ "$antlr_dir" != default ] \
- && cmake_opts="$cmake_opts -DANTLR_DIR=$antlr_dir"
-[ "$cadical_dir" != default ] \
- && 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 ] \
- && cmake_opts="$cmake_opts -DSYMFPU_DIR=$symfpu_dir"
+[ "$dep_path" != default ] \
+ && cmake_opts="$cmake_opts -DCMAKE_PREFIX_PATH=$dep_path"
[ "$lib_only" != default ] \
&& cmake_opts="$cmake_opts -DBUILD_LIB_ONLY=$lib_only"
[ "$install_prefix" != default ] \
projects / cvc5.git / blobdiff