2 #--------------------------------------------------------------------------#
8 Usage: $0 [<build type>] [<option> ...]
19 -h, --help display this help and exit
20 --prefix=STR install directory
21 --program-prefix=STR prefix of binaries prepended on make install
22 --name=STR use custom build directory name (optionally: +path)
23 --best turn on dependencies known to give best performance
24 --gpl permit GPL dependencies, if available
25 --win64 cross-compile for Windows 64 bit
26 --ninja use Ninja build system
30 The following flags enable optional features (disable with --no-<option name>).
31 --static build static libraries and binaries [default=no]
32 --static-binary enable/disable static binaries
33 --proofs support for proof generation
34 --optimized optimize the build
35 --debug-symbols include debug symbols
36 --valgrind Valgrind instrumentation
37 --debug-context-mm use the debug context memory manager
38 --statistics include statistics
39 --assertions turn on assertions
40 --tracing include tracing code
41 --dumping include dumping code
42 --muzzle complete silence (no non-result output)
43 --coverage support for gcov coverage testing
44 --profiling support for gprof profiling
45 --unit-testing support for unit testing
46 --python2 prefer using Python 2 (also for Python bindings)
47 --python3 prefer using Python 3 (also for Python bindings)
48 --python-bindings build Python bindings based on new C++ API
49 --java-bindings build Java bindings based on new C++ API
50 --all-bindings build bindings for all supported languages
51 --asan build with ASan instrumentation
52 --ubsan build with UBSan instrumentation
53 --tsan build with TSan instrumentation
56 The following flags enable optional packages (disable with --no-<option name>).
57 --cln use CLN instead of GMP
58 --glpk use GLPK simplex solver
59 --abc use the ABC AIG library
60 --cadical use the CaDiCaL SAT solver
61 --cryptominisat use the CryptoMiniSat SAT solver
62 --drat2er use drat2er (required for eager BV proofs)
63 --kissat use the Kissat SAT solver
64 --lfsc use the LFSC proof checker
65 --poly use the LibPoly library
66 --symfpu use SymFPU for floating point solver
67 --editline support the editline library
69 Optional Path to Optional Packages:
70 --abc-dir=PATH path to top level of ABC source tree
71 --antlr-dir=PATH path to ANTLR C headers and libraries
72 --cadical-dir=PATH path to top level of CaDiCaL source tree
73 --cryptominisat-dir=PATH path to top level of CryptoMiniSat source tree
74 --drat2er-dir=PATH path to the top level of the drat2er installation
75 --cxxtest-dir=PATH path to CxxTest installation
76 --glpk-dir=PATH path to top level of GLPK installation
77 --gmp-dir=PATH path to top level of GMP installation
78 --kissat-dir=PATH path to top level of Kissat source tree
79 --lfsc-dir=PATH path to top level of LFSC source tree
80 --poly-dir=PATH path to top level of LibPoly source tree
81 --symfpu-dir=PATH path to top level of SymFPU source tree
84 --lib-only only build the library, but not the executable or
85 the parser (default: off)
91 #--------------------------------------------------------------------------#
94 echo "*** configure.sh: $*" 1>&2
99 echo "[configure.sh] $*"
102 #--------------------------------------------------------------------------#
104 [ ! -e src
/theory
] && die
"$0 not called from CVC4 base directory"
106 #--------------------------------------------------------------------------#
109 install_prefix
=default
112 #--------------------------------------------------------------------------#
124 cryptominisat
=default
125 debug_context_mm
=default
126 debug_symbols
=default
141 python_bindings
=default
142 java_bindings
=default
145 static_binary
=default
158 cryptominisat_dir
=default
170 #--------------------------------------------------------------------------#
182 --no-asan) asan
=OFF
;;
185 --no-ubsan) ubsan
=OFF
;;
188 --no-tsan) tsan
=OFF
;;
190 --assertions) assertions
=ON
;;
191 --no-assertions) assertions
=OFF
;;
194 --no-best) best
=OFF
;;
196 --prefix) die
"missing argument to $1 (try -h)" ;;
198 install_prefix
=${1##*=}
199 # Check if install_prefix is an absolute path and if not, make it
201 case $install_prefix in
202 /*) ;; # absolute path
203 *) install_prefix
=$
(pwd)/$install_prefix ;; # make absolute path
207 --program-prefix) die
"missing argument to $1 (try -h)" ;;
208 --program-prefix=*) program_prefix
=${1##*=} ;;
210 --name) die
"missing argument to $1 (try -h)" ;;
211 --name=*) build_dir
=${1##*=} ;;
213 --cadical) cadical
=ON
;;
214 --no-cadical) cadical
=OFF
;;
219 --coverage) coverage
=ON
;;
220 --no-coverage) coverage
=OFF
;;
222 --cryptominisat) cryptominisat
=ON
;;
223 --no-cryptominisat) cryptominisat
=OFF
;;
225 --debug-symbols) debug_symbols
=ON
;;
226 --no-debug-symbols) debug_symbols
=OFF
;;
228 --debug-context-mm) debug_context_mm
=ON
;;
229 --no-debug-context-mm) debug_context_mm
=OFF
;;
231 --drat2er) drat2er
=ON
;;
232 --no-drat2er) drat2er
=OFF
;;
234 --dumping) dumping
=ON
;;
235 --no-dumping) dumping
=OFF
;;
240 --kissat) kissat
=ON
;;
241 --no-kissat) kissat
=OFF
;;
244 --no-win64) win64
=OFF
;;
249 --no-glpk) glpk
=OFF
;;
252 --no-lfsc) lfsc
=OFF
;;
255 --no-poly) poly
=OFF
;;
257 --muzzle) muzzle
=ON
;;
258 --no-muzzle) muzzle
=OFF
;;
260 --optimized) optimized
=ON
;;
261 --no-optimized) optimized
=OFF
;;
263 --proofs) proofs
=ON
;;
264 --no-proofs) proofs
=OFF
;;
266 --static) shared
=OFF
; static_binary
=ON
;;
267 --no-static) shared
=ON
;;
269 --static-binary) static_binary
=ON
;;
270 --no-static-binary) static_binary
=OFF
;;
272 --statistics) statistics
=ON
;;
273 --no-statistics) statistics
=OFF
;;
275 --symfpu) symfpu
=ON
;;
276 --no-symfpu) symfpu
=OFF
;;
278 --tracing) tracing
=ON
;;
279 --no-tracing) tracing
=OFF
;;
281 --unit-testing) unit_testing
=ON
;;
282 --no-unit-testing) unit_testing
=OFF
;;
284 --python2) python2
=ON
;;
285 --no-python2) python2
=OFF
;;
287 --python3) python3
=ON
;;
288 --no-python3) python3
=OFF
;;
290 --python-bindings) python_bindings
=ON
;;
291 --no-python-bindings) python_bindings
=OFF
;;
293 --java-bindings) java_bindings
=ON
;;
294 --no-java-bindings) java_bindings
=OFF
;;
296 --all-bindings) python_bindings
=ON
;;
298 --valgrind) valgrind
=ON
;;
299 --no-valgrind) valgrind
=OFF
;;
301 --profiling) profiling
=ON
;;
302 --no-profiling) profiling
=OFF
;;
304 --editline) editline
=ON
;;
305 --no-editline) editline
=OFF
;;
307 --abc-dir) die
"missing argument to $1 (try -h)" ;;
308 --abc-dir=*) abc_dir
=${1##*=} ;;
310 --antlr-dir) die
"missing argument to $1 (try -h)" ;;
311 --antlr-dir=*) antlr_dir
=${1##*=} ;;
313 --cadical-dir) die
"missing argument to $1 (try -h)" ;;
314 --cadical-dir=*) cadical_dir
=${1##*=} ;;
316 --cryptominisat-dir) die
"missing argument to $1 (try -h)" ;;
317 --cryptominisat-dir=*) cryptominisat_dir
=${1##*=} ;;
319 --cxxtest-dir) die
"missing argument to $1 (try -h)" ;;
320 --cxxtest-dir=*) cxxtest_dir
=${1##*=} ;;
322 --drat2er-dir) die
"missing argument to $1 (try -h)" ;;
323 --drat2er-dir=*) drat2er_dir
=${1##*=} ;;
325 --glpk-dir) die
"missing argument to $1 (try -h)" ;;
326 --glpk-dir=*) glpk_dir
=${1##*=} ;;
328 --gmp-dir) die
"missing argument to $1 (try -h)" ;;
329 --gmp-dir=*) gmp_dir
=${1##*=} ;;
331 --kissat-dir) die
"missing argument to $1 (try -h)" ;;
332 --kissat-dir=*) kissat_dir
=${1##*=} ;;
334 --lfsc-dir) die
"missing argument to $1 (try -h)" ;;
335 --lfsc-dir=*) lfsc_dir
=${1##*=} ;;
337 --poly-dir) die
"missing argument to $1 (try -h)" ;;
338 --poly-dir=*) poly_dir
=${1##*=} ;;
340 --symfpu-dir) die
"missing argument to $1 (try -h)" ;;
341 --symfpu-dir=*) symfpu_dir
=${1##*=} ;;
343 --lib-only) lib_only
=ON
;;
345 -*) die
"invalid option '$1' (try -h)";;
348 production
) buildtype
=Production
;;
349 debug
) buildtype
=Debug
;;
350 testing
) buildtype
=Testing
;;
351 competition
) buildtype
=Competition
;;
352 competition-inc
) buildtype
=Competition
; comp_inc
=ON
;;
353 *) die
"invalid build type (try -h)";;
360 #--------------------------------------------------------------------------#
364 [ $buildtype != default
] \
365 && cmake_opts
="$cmake_opts -DCMAKE_BUILD_TYPE=$buildtype"
367 [ $asan != default
] \
368 && cmake_opts
="$cmake_opts -DENABLE_ASAN=$asan"
369 [ $ubsan != default
] \
370 && cmake_opts
="$cmake_opts -DENABLE_UBSAN=$ubsan"
371 [ $tsan != default
] \
372 && cmake_opts
="$cmake_opts -DENABLE_TSAN=$tsan"
373 [ $assertions != default
] \
374 && cmake_opts
="$cmake_opts -DENABLE_ASSERTIONS=$assertions"
375 [ $best != default
] \
376 && cmake_opts
="$cmake_opts -DENABLE_BEST=$best"
377 [ $comp_inc != default
] \
378 && cmake_opts
="$cmake_opts -DENABLE_COMP_INC_TRACK=$comp_inc"
379 [ $coverage != default
] \
380 && cmake_opts
="$cmake_opts -DENABLE_COVERAGE=$coverage"
381 [ $debug_symbols != default
] \
382 && cmake_opts
="$cmake_opts -DENABLE_DEBUG_SYMBOLS=$debug_symbols"
383 [ $debug_context_mm != default
] \
384 && cmake_opts
="$cmake_opts -DENABLE_DEBUG_CONTEXT_MM=$debug_context_mm"
385 [ $dumping != default
] \
386 && cmake_opts
="$cmake_opts -DENABLE_DUMPING=$dumping"
387 [ $gpl != default
] \
388 && cmake_opts
="$cmake_opts -DENABLE_GPL=$gpl"
389 [ $win64 != default
] \
390 && cmake_opts
="$cmake_opts -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-mingw64.cmake"
391 [ $ninja != default
] && cmake_opts
="$cmake_opts -G Ninja"
392 [ $muzzle != default
] \
393 && cmake_opts
="$cmake_opts -DENABLE_MUZZLE=$muzzle"
394 [ $optimized != default
] \
395 && cmake_opts
="$cmake_opts -DENABLE_OPTIMIZED=$optimized"
396 [ $proofs != default
] \
397 && cmake_opts
="$cmake_opts -DENABLE_PROOFS=$proofs"
398 [ $shared != default
] \
399 && cmake_opts
="$cmake_opts -DENABLE_SHARED=$shared"
400 [ $static_binary != default
] \
401 && cmake_opts
="$cmake_opts -DENABLE_STATIC_BINARY=$static_binary"
402 [ $statistics != default
] \
403 && cmake_opts
="$cmake_opts -DENABLE_STATISTICS=$statistics"
404 [ $tracing != default
] \
405 && cmake_opts
="$cmake_opts -DENABLE_TRACING=$tracing"
406 [ $unit_testing != default
] \
407 && cmake_opts
="$cmake_opts -DENABLE_UNIT_TESTING=$unit_testing"
408 [ $python2 != default
] \
409 && cmake_opts
="$cmake_opts -DUSE_PYTHON2=$python2"
410 [ $python3 != default
] \
411 && cmake_opts
="$cmake_opts -DUSE_PYTHON3=$python3"
412 [ $python_bindings != default
] \
413 && cmake_opts
="$cmake_opts -DBUILD_BINDINGS_PYTHON=$python_bindings"
414 [ $java_bindings != default
] \
415 && cmake_opts
="$cmake_opts -DBUILD_BINDINGS_JAVA=$java_bindings"
416 [ $valgrind != default
] \
417 && cmake_opts
="$cmake_opts -DENABLE_VALGRIND=$valgrind"
418 [ $profiling != default
] \
419 && cmake_opts
="$cmake_opts -DENABLE_PROFILING=$profiling"
420 [ $editline != default
] \
421 && cmake_opts
="$cmake_opts -DUSE_EDITLINE=$editline"
422 [ $abc != default
] \
423 && cmake_opts
="$cmake_opts -DUSE_ABC=$abc"
424 [ $cadical != default
] \
425 && cmake_opts
="$cmake_opts -DUSE_CADICAL=$cadical"
426 [ $cln != default
] \
427 && cmake_opts
="$cmake_opts -DUSE_CLN=$cln"
428 [ $cryptominisat != default
] \
429 && cmake_opts
="$cmake_opts -DUSE_CRYPTOMINISAT=$cryptominisat"
430 [ $drat2er != default
] \
431 && cmake_opts
="$cmake_opts -DUSE_DRAT2ER=$drat2er"
432 [ $glpk != default
] \
433 && cmake_opts
="$cmake_opts -DUSE_GLPK=$glpk"
434 [ $kissat != default
] \
435 && cmake_opts
="$cmake_opts -DUSE_KISSAT=$kissat"
436 [ $lfsc != default
] \
437 && cmake_opts
="$cmake_opts -DUSE_LFSC=$lfsc"
438 [ $poly != default
] \
439 && cmake_opts
="$cmake_opts -DUSE_POLY=$poly"
440 [ $symfpu != default
] \
441 && cmake_opts
="$cmake_opts -DUSE_SYMFPU=$symfpu"
442 [ "$abc_dir" != default
] \
443 && cmake_opts
="$cmake_opts -DABC_DIR=$abc_dir"
444 [ "$antlr_dir" != default
] \
445 && cmake_opts
="$cmake_opts -DANTLR_DIR=$antlr_dir"
446 [ "$cadical_dir" != default
] \
447 && cmake_opts
="$cmake_opts -DCADICAL_DIR=$cadical_dir"
448 [ "$cryptominisat_dir" != default
] \
449 && cmake_opts
="$cmake_opts -DCRYPTOMINISAT_DIR=$cryptominisat_dir"
450 [ "$cxxtest_dir" != default
] \
451 && cmake_opts
="$cmake_opts -DCXXTEST_DIR=$cxxtest_dir"
452 [ "$drat2er_dir" != default
] \
453 && cmake_opts
="$cmake_opts -DDRAT2ER_DIR=$drat2er_dir"
454 [ "$glpk_dir" != default
] \
455 && cmake_opts
="$cmake_opts -DGLPK_DIR=$glpk_dir"
456 [ "$gmp_dir" != default
] \
457 && cmake_opts
="$cmake_opts -DGMP_DIR=$gmp_dir"
458 [ "$kissat_dir" != default
] \
459 && cmake_opts
="$cmake_opts -DKISSAT=$kissat_dir"
460 [ "$lfsc_dir" != default
] \
461 && cmake_opts
="$cmake_opts -DLFSC_DIR=$lfsc_dir"
462 [ "$poly_dir" != default
] \
463 && cmake_opts
="$cmake_opts -DPOLY_DIR=$poly_dir"
464 [ "$symfpu_dir" != default
] \
465 && cmake_opts
="$cmake_opts -DSYMFPU_DIR=$symfpu_dir"
466 [ "$lib_only" != default
] \
467 && cmake_opts
="$cmake_opts -DBUILD_LIB_ONLY=$lib_only"
468 [ "$install_prefix" != default
] \
469 && cmake_opts
="$cmake_opts -DCMAKE_INSTALL_PREFIX=$install_prefix"
470 [ -n "$program_prefix" ] \
471 && cmake_opts
="$cmake_opts -DPROGRAM_PREFIX=$program_prefix"
475 # The cmake toolchain can't be changed once it is configured in $build_dir.
476 # Thus, remove $build_dir and create an empty directory.
477 [ $win64 = ON
] && [ -e "$build_dir" ] && rm -r "$build_dir"
478 mkdir
-p "$build_dir"
482 [ -e CMakeCache.txt
] && rm CMakeCache.txt
483 build_dir_escaped
=$
(echo "$build_dir" |
sed 's/\//\\\//g')
484 cmake
"$root_dir" $cmake_opts 2>&1 | \
485 sed "s/^Now just/Now change to '$build_dir_escaped' and/"