2 #--------------------------------------------------------------------------#
6 Usage: $0 [<build type>] [<option> ...]
17 -h, --help display this help and exit
18 --prefix=STR install directory
19 --program-prefix=STR prefix of binaries prepended on make install
20 --name=STR use custom build directory name (optionally: +path)
21 --best turn on dependencies known to give best performance
22 --gpl permit GPL dependencies, if available
23 --win64 cross-compile for Windows 64 bit
24 --ninja use Ninja build system
28 The following flags enable optional features (disable with --no-<option name>).
29 --static build static libraries and binaries [default=no]
30 --static-binary enable/disable static binaries
31 --proofs support for proof generation
32 --optimized optimize the build
33 --debug-symbols include debug symbols
34 --valgrind Valgrind instrumentation
35 --debug-context-mm use the debug context memory manager
36 --statistics include statistics
37 --replay turn on the replay feature
38 --assertions turn on assertions
39 --tracing include tracing code
40 --dumping include dumping code
41 --muzzle complete silence (no non-result output)
42 --coverage support for gcov coverage testing
43 --profiling support for gprof profiling
44 --unit-testing support for unit testing
45 --python2 prefer using Python 2 (also for Python bindings)
46 --python3 prefer using Python 3 (also for Python bindings)
47 --asan build with ASan instrumentation
48 --ubsan build with UBSan instrumentation
49 --tsan build with TSan instrumentation
51 The following options configure parameterized features.
53 --language-bindings[=java,python,all]
54 specify language bindings to build
57 The following flags enable optional packages (disable with --no-<option name>).
58 --cln use CLN instead of GMP
59 --glpk use GLPK simplex solver
60 --abc use the ABC AIG library
61 --cadical use the CaDiCaL SAT solver
62 --cryptominisat use the CryptoMiniSat SAT solver
63 --drat2er use drat2er (required for eager BV proofs)
64 --lfsc use the LFSC proof checker
65 --symfpu use SymFPU for floating point solver
66 --portfolio build the multithreaded portfolio version of CVC4
68 --readline support the readline library
70 Optional Path to Optional Packages:
71 --abc-dir=PATH path to top level of ABC source tree
72 --antlr-dir=PATH path to ANTLR C headers and libraries
73 --cadical-dir=PATH path to top level of CaDiCaL source tree
74 --cryptominisat-dir=PATH path to top level of CryptoMiniSat source tree
75 --drat2er-dir=PATH path to the top level of the drat2er installation
76 --cxxtest-dir=PATH path to CxxTest installation
77 --glpk-dir=PATH path to top level of GLPK installation
78 --gmp-dir=PATH path to top level of GMP installation
79 --lfsc-dir=PATH path to top level of LFSC source tree
80 --symfpu-dir=PATH path to top level of SymFPU source tree
86 #--------------------------------------------------------------------------#
89 echo "*** configure.sh: $*" 1>&2
94 echo "[configure.sh] $*"
97 #--------------------------------------------------------------------------#
99 [ ! -e src
/theory
] && die
"$0 not called from CVC4 base directory"
101 #--------------------------------------------------------------------------#
104 install_prefix
=default
107 #--------------------------------------------------------------------------#
121 cryptominisat
=default
122 debug_symbols
=default
123 debug_context_mm
=default
137 static_binary
=default
148 language_bindings_java
=default
149 language_bindings_python
=default
154 cryptominisat_dir
=default
162 #--------------------------------------------------------------------------#
174 --no-asan) asan
=OFF
;;
177 --no-ubsan) ubsan
=OFF
;;
180 --no-tsan) tsan
=OFF
;;
182 --assertions) assertions
=ON
;;
183 --no-assertions) assertions
=OFF
;;
186 --no-best) best
=OFF
;;
188 --prefix) die
"missing argument to $1 (try -h)" ;;
190 install_prefix
=${1##*=}
191 # Check if install_prefix is an absolute path and if not, make it
193 case $install_prefix in
194 /*) ;; # absolute path
195 *) install_prefix
=$
(pwd)/$install_prefix ;; # make absolute path
199 --program-prefix) die
"missing argument to $1 (try -h)" ;;
200 --program-prefix=*) program_prefix
=${1##*=} ;;
202 --name) die
"missing argument to $1 (try -h)" ;;
203 --name=*) build_dir
=${1##*=} ;;
205 --cadical) cadical
=ON
;;
206 --no-cadical) cadical
=OFF
;;
211 --coverage) coverage
=ON
;;
212 --no-coverage) coverage
=OFF
;;
214 --cryptominisat) cryptominisat
=ON
;;
215 --no-cryptominisat) cryptominisat
=OFF
;;
217 --debug-symbols) debug_symbols
=ON
;;
218 --no-debug-symbols) debug_symbols
=OFF
;;
220 --debug-context-mm) debug_context_mm
=ON
;;
221 --no-debug-context-mm) debug_context_mm
=OFF
;;
223 --drat2er) drat2er
=ON
;;
224 --no-drat2er) drat2er
=OFF
;;
226 --dumping) dumping
=ON
;;
227 --no-dumping) dumping
=OFF
;;
233 --no-win64) win64
=OFF
;;
238 --no-glpk) glpk
=OFF
;;
241 --no-lfsc) lfsc
=OFF
;;
243 --muzzle) muzzle
=ON
;;
244 --no-muzzle) muzzle
=OFF
;;
246 --optimized) optimized
=ON
;;
247 --no-optimized) optimized
=OFF
;;
249 --portfolio) portfolio
=ON
;;
250 --no-portfolio) portfolio
=OFF
;;
252 --proofs) proofs
=ON
;;
253 --no-proofs) proofs
=OFF
;;
255 --replay) replay
=ON
;;
256 --no-replay) replay
=OFF
;;
258 --static) shared
=OFF
; static_binary
=ON
;;
259 --no-static) shared
=ON
;;
261 --static-binary) static_binary
=ON
;;
262 --no-static-binary) static_binary
=OFF
;;
264 --statistics) statistics
=ON
;;
265 --no-statistics) statistics
=OFF
;;
267 --symfpu) symfpu
=ON
;;
268 --no-symfpu) symfpu
=OFF
;;
270 --tracing) tracing
=ON
;;
271 --no-tracing) tracing
=OFF
;;
273 --unit-testing) unit_testing
=ON
;;
274 --no-unit-testing) unit_testing
=OFF
;;
276 --python2) python2
=ON
;;
277 --no-python2) python2
=OFF
;;
279 --python3) python3
=ON
;;
280 --no-python3) python3
=OFF
;;
282 --valgrind) valgrind
=ON
;;
283 --no-valgrind) valgrind
=OFF
;;
285 --profiling) profiling
=ON
;;
286 --no-profiling) profiling
=OFF
;;
288 --readline) readline
=ON
;;
289 --no-readline) readline
=OFF
;;
291 --language-bindings) die
"missing argument to $1 (try -h)" ;;
292 --language-bindings=*)
297 java
) language_bindings_java
=ON
;;
298 python
) language_bindings_python
=ON
;;
300 language_bindings_python
=ON
301 language_bindings_java
=ON
;;
302 *) die
"invalid language binding '$l' specified (try -h)" ;;
308 --abc-dir) die
"missing argument to $1 (try -h)" ;;
309 --abc-dir=*) abc_dir
=${1##*=} ;;
311 --antlr-dir) die
"missing argument to $1 (try -h)" ;;
312 --antlr-dir=*) antlr_dir
=${1##*=} ;;
314 --cadical-dir) die
"missing argument to $1 (try -h)" ;;
315 --cadical-dir=*) cadical_dir
=${1##*=} ;;
317 --cryptominisat-dir) die
"missing argument to $1 (try -h)" ;;
318 --cryptominisat-dir=*) cryptominisat_dir
=${1##*=} ;;
320 --cxxtest-dir) die
"missing argument to $1 (try -h)" ;;
321 --cxxtest-dir=*) cxxtest_dir
=${1##*=} ;;
323 --drat2er-dir) die
"missing argument to $1 (try -h)" ;;
324 --drat2er-dir=*) drat2er_dir
=${1##*=} ;;
326 --glpk-dir) die
"missing argument to $1 (try -h)" ;;
327 --glpk-dir=*) glpk_dir
=${1##*=} ;;
329 --gmp-dir) die
"missing argument to $1 (try -h)" ;;
330 --gmp-dir=*) gmp_dir
=${1##*=} ;;
332 --lfsc-dir) die
"missing argument to $1 (try -h)" ;;
333 --lfsc-dir=*) lfsc_dir
=${1##*=} ;;
335 --symfpu-dir) die
"missing argument to $1 (try -h)" ;;
336 --symfpu-dir=*) symfpu_dir
=${1##*=} ;;
338 -*) die
"invalid option '$1' (try -h)";;
341 production
) buildtype
=Production
;;
342 debug
) buildtype
=Debug
;;
343 testing
) buildtype
=Testing
;;
344 competition
) buildtype
=Competition
;;
345 competition-inc
) buildtype
=Competition
; comp_inc
=ON
;;
346 *) die
"invalid build type (try -h)";;
353 #--------------------------------------------------------------------------#
357 [ $buildtype != default
] \
358 && cmake_opts
="$cmake_opts -DCMAKE_BUILD_TYPE=$buildtype"
360 [ $asan != default
] \
361 && cmake_opts
="$cmake_opts -DENABLE_ASAN=$asan"
362 [ $ubsan != default
] \
363 && cmake_opts
="$cmake_opts -DENABLE_UBSAN=$ubsan"
364 [ $tsan != default
] \
365 && cmake_opts
="$cmake_opts -DENABLE_TSAN=$tsan"
366 [ $assertions != default
] \
367 && cmake_opts
="$cmake_opts -DENABLE_ASSERTIONS=$assertions"
368 [ $best != default
] \
369 && cmake_opts
="$cmake_opts -DENABLE_BEST=$best"
370 [ $comp_inc != default
] \
371 && cmake_opts
="$cmake_opts -DENABLE_COMP_INC_TRACK=$comp_inc"
372 [ $coverage != default
] \
373 && cmake_opts
="$cmake_opts -DENABLE_COVERAGE=$coverage"
374 [ $debug_symbols != default
] \
375 && cmake_opts
="$cmake_opts -DENABLE_DEBUG_SYMBOLS=$debug_symbols"
376 [ $debug_context_mm != default
] \
377 && cmake_opts
="$cmake_opts -DENABLE_DEBUG_CONTEXT_MM=$debug_context_mm"
378 [ $dumping != default
] \
379 && cmake_opts
="$cmake_opts -DENABLE_DUMPING=$dumping"
380 [ $gpl != default
] \
381 && cmake_opts
="$cmake_opts -DENABLE_GPL=$gpl"
382 [ $win64 != default
] \
383 && cmake_opts
="$cmake_opts -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-mingw64.cmake"
384 [ $ninja != default
] && cmake_opts
="$cmake_opts -G Ninja"
385 [ $muzzle != default
] \
386 && cmake_opts
="$cmake_opts -DENABLE_MUZZLE=$muzzle"
387 [ $optimized != default
] \
388 && cmake_opts
="$cmake_opts -DENABLE_OPTIMIZED=$optimized"
389 [ $proofs != default
] \
390 && cmake_opts
="$cmake_opts -DENABLE_PROOFS=$proofs"
391 [ $replay != default
] \
392 && cmake_opts
="$cmake_opts -DENABLE_REPLAY=$replay"
393 [ $shared != default
] \
394 && cmake_opts
="$cmake_opts -DENABLE_SHARED=$shared"
395 [ $static_binary != default
] \
396 && cmake_opts
="$cmake_opts -DENABLE_STATIC_BINARY=$static_binary"
397 [ $statistics != default
] \
398 && cmake_opts
="$cmake_opts -DENABLE_STATISTICS=$statistics"
399 [ $tracing != default
] \
400 && cmake_opts
="$cmake_opts -DENABLE_TRACING=$tracing"
401 [ $unit_testing != default
] \
402 && cmake_opts
="$cmake_opts -DENABLE_UNIT_TESTING=$unit_testing"
403 [ $python2 != default
] \
404 && cmake_opts
="$cmake_opts -DUSE_PYTHON2=$python2"
405 [ $python3 != default
] \
406 && cmake_opts
="$cmake_opts -DUSE_PYTHON3=$python3"
407 [ $valgrind != default
] \
408 && cmake_opts
="$cmake_opts -DENABLE_VALGRIND=$valgrind"
409 [ $profiling != default
] \
410 && cmake_opts
="$cmake_opts -DENABLE_PROFILING=$profiling"
411 [ $readline != default
] \
412 && cmake_opts
="$cmake_opts -DUSE_READLINE=$readline"
413 [ $abc != default
] \
414 && cmake_opts
="$cmake_opts -DUSE_ABC=$abc"
415 [ $cadical != default
] \
416 && cmake_opts
="$cmake_opts -DUSE_CADICAL=$cadical"
417 [ $cln != default
] \
418 && cmake_opts
="$cmake_opts -DUSE_CLN=$cln"
419 [ $cryptominisat != default
] \
420 && cmake_opts
="$cmake_opts -DUSE_CRYPTOMINISAT=$cryptominisat"
421 [ $drat2er != default
] \
422 && cmake_opts
="$cmake_opts -DUSE_DRAT2ER=$drat2er"
423 [ $glpk != default
] \
424 && cmake_opts
="$cmake_opts -DUSE_GLPK=$glpk"
425 [ $lfsc != default
] \
426 && cmake_opts
="$cmake_opts -DUSE_LFSC=$lfsc"
427 [ $symfpu != default
] \
428 && cmake_opts
="$cmake_opts -DUSE_SYMFPU=$symfpu"
430 [ $language_bindings_java != default
] \
431 && cmake_opts
="$cmake_opts -DBUILD_BINDINGS_JAVA=$language_bindings_java"
432 [ $language_bindings_python != default
] \
433 && cmake_opts
="$cmake_opts -DBUILD_BINDINGS_PYTHON=$language_bindings_python"
435 [ "$abc_dir" != default
] \
436 && cmake_opts
="$cmake_opts -DABC_DIR=$abc_dir"
437 [ "$antlr_dir" != default
] \
438 && cmake_opts
="$cmake_opts -DANTLR_DIR=$antlr_dir"
439 [ "$cadical_dir" != default
] \
440 && cmake_opts
="$cmake_opts -DCADICAL_DIR=$cadical_dir"
441 [ "$cryptominisat_dir" != default
] \
442 && cmake_opts
="$cmake_opts -DCRYPTOMINISAT_DIR=$cryptominisat_dir"
443 [ "$cxxtest_dir" != default
] \
444 && cmake_opts
="$cmake_opts -DCXXTEST_DIR=$cxxtest_dir"
445 [ "$drat2er_dir" != default
] \
446 && cmake_opts
="$cmake_opts -DDRAT2ER_DIR=$drat2er_dir"
447 [ "$glpk_dir" != default
] \
448 && cmake_opts
="$cmake_opts -DGLPK_DIR=$glpk_dir"
449 [ "$gmp_dir" != default
] \
450 && cmake_opts
="$cmake_opts -DGMP_DIR=$gmp_dir"
451 [ "$lfsc_dir" != default
] \
452 && cmake_opts
="$cmake_opts -DLFSC_DIR=$lfsc_dir"
453 [ "$symfpu_dir" != default
] \
454 && cmake_opts
="$cmake_opts -DSYMFPU_DIR=$symfpu_dir"
455 [ "$install_prefix" != default
] \
456 && cmake_opts
="$cmake_opts -DCMAKE_INSTALL_PREFIX=$install_prefix"
457 [ -n "$program_prefix" ] \
458 && cmake_opts
="$cmake_opts -DPROGRAM_PREFIX=$program_prefix"
462 # The cmake toolchain can't be changed once it is configured in $build_dir.
463 # Thus, remove $build_dir and create an empty directory.
464 [ $win64 = ON
] && [ -e "$build_dir" ] && rm -r "$build_dir"
465 mkdir
-p "$build_dir"
467 cd "$build_dir" ||
exit 1
469 [ -e CMakeCache.txt
] && rm CMakeCache.txt
470 build_dir_escaped
=$
(echo "$build_dir" |
sed 's/\//\\\//g')
471 cmake
"$root_dir" $cmake_opts 2>&1 | \
472 sed "s/^Now just/Now change to '$build_dir_escaped' and/"