projects / cvc5.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
Fix cached free variable identifiers in sygus term database (#4394)
[cvc5.git] / configure.sh
diff --git a/configure.sh b/configure.sh
index 9bf33ae8a44ed2b0c42d5d35793a778a65bf67f2..070e2c23025762cab92f67652325f1655c1a6c76 100755 (executable)
--- a/configure.sh
+++ b/configure.sh
@@ -1,6 +1,8 @@
-#!/bin/sh
+#!/bin/bash
 #--------------------------------------------------------------------------#
 
+set -e -o pipefail
+
 usage () {
 cat <<EOF
 Usage: $0 [<build type>] [<option> ...]
@@ -10,6 +12,7 @@ Build types:
   debug
   testing
   competition
+  competition-inc
 
 
 General options;
@@ -20,6 +23,7 @@ General options;
   --best                   turn on dependencies known to give best performance
   --gpl                    permit GPL dependencies, if available
   --win64                  cross-compile for Windows 64 bit
+  --ninja                  use Ninja build system
 
 
 Features:
@@ -32,7 +36,6 @@ The following flags enable optional features (disable with --no-<option name>).
   --valgrind               Valgrind instrumentation
   --debug-context-mm       use the debug context memory manager
   --statistics             include statistics
-  --replay                 turn on the replay feature
   --assertions             turn on assertions
   --tracing                include tracing code
   --dumping                include dumping code
@@ -42,6 +45,10 @@ The following flags enable optional features (disable with --no-<option name>).
   --unit-testing           support for unit testing
   --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
+  --asan                   build with ASan instrumentation
+  --ubsan                  build with UBSan instrumentation
+  --tsan                   build with TSan instrumentation
 
 The following options configure parameterized features.
 
@@ -58,8 +65,6 @@ The following flags enable optional packages (disable with --no-<option name>).
   --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
-                           (pcvc4)
   --readline               support the readline library
 
 Optional Path to Optional Packages:
@@ -105,10 +110,13 @@ buildtype=default
 
 abc=default
 asan=default
+ubsan=default
+tsan=default
 assertions=default
 best=default
 cadical=default
 cln=default
+comp_inc=default
 coverage=default
 cryptominisat=default
 debug_symbols=default
@@ -117,13 +125,12 @@ drat2er=default
 dumping=default
 gpl=default
 win64=default
+ninja=default
 glpk=default
 lfsc=default
 muzzle=default
 optimized=default
-portfolio=default
 proofs=default
-replay=default
 shared=default
 static_binary=default
 statistics=default
@@ -132,6 +139,7 @@ tracing=default
 unit_testing=default
 python2=default
 python3=default
+python_bindings=default
 valgrind=default
 profiling=default
 readline=default
@@ -164,6 +172,12 @@ do
     --asan) asan=ON;;
     --no-asan) asan=OFF;;
 
+    --ubsan) ubsan=ON;;
+    --no-ubsan) ubsan=OFF;;
+
+    --tsan) tsan=ON;;
+    --no-tsan) tsan=OFF;;
+
     --assertions) assertions=ON;;
     --no-assertions) assertions=OFF;;
 
@@ -217,6 +231,8 @@ do
     --win64) win64=ON;;
     --no-win64) win64=OFF;;
 
+    --ninja) ninja=ON;;
+
     --glpk) glpk=ON;;
     --no-glpk) glpk=OFF;;
 
@@ -229,15 +245,9 @@ do
     --optimized) optimized=ON;;
     --no-optimized) optimized=OFF;;
 
-    --portfolio) portfolio=ON;;
-    --no-portfolio) portfolio=OFF;;
-
     --proofs) proofs=ON;;
     --no-proofs) proofs=OFF;;
 
-    --replay) replay=ON;;
-    --no-replay) replay=OFF;;
-
     --static) shared=OFF; static_binary=ON;;
     --no-static) shared=ON;;
 
@@ -262,6 +272,9 @@ do
     --python3) python3=ON;;
     --no-python3) python3=OFF;;
 
+    --python-bindings) python_bindings=ON;;
+    --no-python-bindings) python_bindings=OFF;;
+
     --valgrind) valgrind=ON;;
     --no-valgrind) valgrind=OFF;;
 
@@ -321,11 +334,12 @@ do
     -*) die "invalid option '$1' (try -h)";;
 
     *) case $1 in
-         production)  buildtype=Production;;
-         debug)       buildtype=Debug;;
-         testing)     buildtype=Testing;;
-         competition) buildtype=Competition;;
-         *)           die "invalid build type (try -h)";;
+         production)      buildtype=Production;;
+         debug)           buildtype=Debug;;
+         testing)         buildtype=Testing;;
+         competition)     buildtype=Competition;;
+         competition-inc) buildtype=Competition; comp_inc=ON;;
+         *)               die "invalid build type (try -h)";;
        esac
        ;;
   esac
@@ -340,11 +354,17 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DCMAKE_BUILD_TYPE=$buildtype"
 
 [ $asan != default ] \
- && cmake_opts="$cmake_opts -DENABLE_ASAN=$asan"
+  && cmake_opts="$cmake_opts -DENABLE_ASAN=$asan"
+[ $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 ] \
   && cmake_opts="$cmake_opts -DENABLE_COVERAGE=$coverage"
 [ $debug_symbols != default ] \
@@ -357,16 +377,13 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DENABLE_GPL=$gpl"
 [ $win64 != default ] \
   && cmake_opts="$cmake_opts -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-mingw64.cmake"
+[ $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"
-[ $portfolio != default ] \
-  && cmake_opts="$cmake_opts -DENABLE_PORTFOLIO=$portfolio"
 [ $proofs != default ] \
   && cmake_opts="$cmake_opts -DENABLE_PROOFS=$proofs"
-[ $replay != default ] \
-  && cmake_opts="$cmake_opts -DENABLE_REPLAY=$replay"
 [ $shared != default ] \
   && cmake_opts="$cmake_opts -DENABLE_SHARED=$shared"
 [ $static_binary != default ] \
@@ -381,6 +398,8 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DUSE_PYTHON2=$python2"
 [ $python3 != default ] \
   && cmake_opts="$cmake_opts -DUSE_PYTHON3=$python3"
+[ $python_bindings != default ] \
+  && cmake_opts="$cmake_opts -DBUILD_BINDINGS_PYTHON=$python_bindings"
 [ $valgrind != default ] \
   && cmake_opts="$cmake_opts -DENABLE_VALGRIND=$valgrind"
 [ $profiling != default ] \
@@ -405,9 +424,9 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DUSE_SYMFPU=$symfpu"
 
 [ $language_bindings_java != default ] \
-  && cmake_opts="$cmake_opts -DBUILD_BINDINGS_JAVA=$language_bindings_java"
+  && cmake_opts="$cmake_opts -DBUILD_SWIG_BINDINGS_JAVA=$language_bindings_java"
 [ $language_bindings_python != default ] \
-  && cmake_opts="$cmake_opts -DBUILD_BINDINGS_PYTHON=$language_bindings_python"
+  && cmake_opts="$cmake_opts -DBUILD_SWIG_BINDINGS_PYTHON=$language_bindings_python"
 
 [ "$abc_dir" != default ] \
   && cmake_opts="$cmake_opts -DABC_DIR=$abc_dir"
@@ -441,7 +460,7 @@ root_dir=$(pwd)
 [ $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')