2 #--------------------------------------------------------------------------#
6 Usage: $0 [<build type>] [<option> ...]
16 -h, --help display this help and exit
17 --prefix=STR install directory
18 --build-prefix=STR prefix build directory with given prefix
19 --name=STR use custom build directory name
20 --best turn on dependences known to give best performance
21 --gpl permit GPL dependences, if available
25 The following flags enable optional features (disable with --no-<option name>).
26 --static build static libraries and binaries [default=no]
27 --proofs support for proof generation
28 --optimized optimize the build
29 --debug-symbols include debug symbols
30 --valgrind Valgrind instrumentation
31 --debug-context-mm use the debug context memory manager
32 --statistics do not include statistics
33 --replay turn off the replay feature
34 --assertions turn off assertions
35 --tracing remove all tracing code
36 --dumping remove all dumping code
37 --muzzle complete silence (no non-result output)
38 --coverage support for gcov coverage testing
39 --profiling support for gprof profiling
40 --unit-testing support for unit testing
41 --python2 prefer using Python 2 (for Python bindings)
43 The following options configure parameterized features.
45 --language-bindings[=java,python,all]
46 specify language bindings to build
49 The following flags enable optional packages (disable with --no-<option name>).
50 --cln use CLN instead of GMP
51 --gmp use GMP instead of CLN
52 --glpk use GLPK simplex solver
53 --abc use the ABC AIG library
54 --cadical use the CaDiCaL SAT solver
55 --cryptominisat use the CRYPTOMINISAT sat solver
56 --lfsc use the LFSC proof checker
57 --symfpu use symfpu for floating point solver
58 --portfolio build the multithreaded portfolio version of CVC4
60 --readline support the readline library
62 Optional Path to Optional Packages:
63 --abc-dir=PATH path to top level of abc source tree
64 --antlr-dir=PATH path to ANTLR C headers and libraries
65 --cadical-dir=PATH path to top level of CaDiCaL source tree
66 --cryptominisat-dir=PATH path to top level of cryptominisat source tree
67 --cxxtest-dir=DIR path to CxxTest installation
68 --glpk-dir=PATH path to top level of glpk installation
69 --lfsc-dir=PATH path to top level of lfsc source tree
70 --symfpu-dir=PATH path to top level of symfpu source tree
72 Report bugs to <cvc4-bugs@cs.stanford.edu>.
77 #--------------------------------------------------------------------------#
80 echo "*** configure.sh: $*" 1>&2
85 echo "[configure.sh] $*"
88 #--------------------------------------------------------------------------#
90 [ ! -e src
/theory
] && die
"$0 not called from CVC4 base directory"
92 #--------------------------------------------------------------------------#
95 install_prefix
=default
99 #--------------------------------------------------------------------------#
110 cryptominisat
=default
111 debug_symbols
=default
112 debug_context_mm
=default
132 language_bindings_java
=default
133 language_bindings_python
=default
138 cryptominisat_dir
=default
143 #--------------------------------------------------------------------------#
155 --no-asan) asan
=OFF
;;
157 --assertions) assertions
=ON
;;
158 --no-assertions) assertions
=OFF
;;
161 --no-best) best
=OFF
;;
163 --prefix) die
"missing argument to $1 (try -h)" ;;
165 install_prefix
=${1##*=}
166 # Check if install_prefix is an absolute path and if not, make it
168 case $install_prefix in
169 /*) ;; # absolute path
170 *) install_prefix
=$
(pwd)/$install_prefix ;; # make absolute path
174 --build-prefix) die
"missing argument to $1 (try -h)" ;;
175 --build-prefix=*) build_prefix
=${1##*=} ;;
177 --name) die
"missing argument to $1 (try -h)" ;;
178 --name=*) build_name
=${1##*=} ;;
180 --cadical) cadical
=ON
;;
181 --no-cadical) cadical
=OFF
;;
186 --coverage) coverage
=ON
;;
187 --no-coverage) coverage
=OFF
;;
189 --cryptominisat) cryptominisat
=ON
;;
190 --no-cryptominisat) cryptominisat
=OFF
;;
192 --debug-symbols) debug_symbols
=ON
;;
193 --no-debug-symbols) debug_symbols
=OFF
;;
195 --debug-context-memory-manager) debug_context_mm
=ON
;;
196 --no-debug-context-memory-manager) debug_context_mm
=OFF
;;
198 --dumping) dumping
=ON
;;
199 --no-dumping) dumping
=OFF
;;
205 --no-glpk) glpk
=OFF
;;
208 --no-lfsc) lfsc
=OFF
;;
210 --muzzle) muzzle
=ON
;;
211 --no-muzzle) muzzle
=OFF
;;
213 --optimized) optimized
=ON
;;
214 --no-optimized) optimized
=OFF
;;
216 --portfolio) portfolio
=ON
;;
217 --no-portfolio) portfolio
=OFF
;;
219 --proofs) proofs
=ON
;;
220 --no-proofs) proofs
=OFF
;;
222 --replay) replay
=ON
;;
223 --no-replay) replay
=OFF
;;
225 --static) shared
=OFF
;;
226 --no-static) shared
=ON
;;
228 --statistics) statistics
=ON
;;
229 --no-statistics) statistics
=OFF
;;
231 --symfpu) symfpu
=ON
;;
232 --no-symfpu) symfpu
=OFF
;;
234 --tracing) tracing
=ON
;;
235 --no-tracing) tracing
=OFF
;;
237 --unit-testing) unit_testing
=ON
;;
238 --no-unit-testing) unit_testing
=OFF
;;
240 --python2) python2
=ON
;;
241 --no-python2) python2
=OFF
;;
243 --valgrind) valgrind
=ON
;;
244 --no-valgrind) valgrind
=OFF
;;
246 --profiling) profiling
=ON
;;
247 --no-profiling) profiling
=OFF
;;
249 --readline) readline
=ON
;;
250 --no-readline) readline
=OFF
;;
252 --language-bindings) die
"missing argument to $1 (try -h)" ;;
253 --language-bindings=*)
258 java
) language_bindings_java
=ON
;;
259 python
) language_bindings_python
=ON
;;
261 language_bindings_python
=ON
262 language_bindings_java
=ON
;;
263 *) die
"invalid language binding '$l' specified (try -h)" ;;
269 --abc-dir) die
"missing argument to $1 (try -h)" ;;
270 --abc-dir=*) abc_dir
=${1##*=} ;;
272 --antlr-dir) die
"missing argument to $1 (try -h)" ;;
273 --antlr-dir=*) antlr_dir
=${1##*=} ;;
275 --cadical-dir) die
"missing argument to $1 (try -h)" ;;
276 --cadical-dir=*) cadical_dir
=${1##*=} ;;
278 --cryptominisat-dir) die
"missing argument to $1 (try -h)" ;;
279 --cryptominisat-dir=*) cryptominisat_dir
=${1##*=} ;;
281 --glpk-dir) die
"missing argument to $1 (try -h)" ;;
282 --glpk-dir=*) glpk_dir
=${1##*=} ;;
284 --lfsc-dir) die
"missing argument to $1 (try -h)" ;;
285 --lfsc-dir=*) lfsc_dir
=${1##*=} ;;
287 --symfpu-dir) die
"missing argument to $1 (try -h)" ;;
288 --symfpu-dir=*) symfpu_dir
=${1##*=} ;;
290 -*) die
"invalid option '$1' (try -h)";;
293 production
) buildtype
=Production
; build_dir
=production
;;
294 debug
) buildtype
=Debug
; build_dir
=debug
;;
295 testing
) buildtype
=Testing
; build_dir
=testing
;;
296 competition
) buildtype
=Competition
; build_dir
=competition
;;
297 *) die
"invalid build type (try -h)";;
304 #--------------------------------------------------------------------------#
308 [ $buildtype != default
] && cmake_opts
="$cmake_opts -DCMAKE_BUILD_TYPE=$buildtype"
310 [ $asan != default
] \
311 && cmake_opts
="$cmake_opts -DENABLE_ASAN=$asan" \
312 && [ $asan = ON
] && build_dir
="$build_dir-asan"
313 [ $assertions != default
] \
314 && cmake_opts
="$cmake_opts -DENABLE_ASSERTIONS=$assertions" \
315 && [ $assertions = ON
] && build_dir
="$build_dir-assertions"
316 [ $best != default
] \
317 && cmake_opts
="$cmake_opts -DENABLE_BEST=$best" \
318 && [ $best = ON
] && build_dir
="$build_dir-best"
319 [ $coverage != default
] \
320 && cmake_opts
="$cmake_opts -DENABLE_COVERAGE=$coverage" \
321 && [ $coverage = ON
] && build_dir
="$build_dir-coverage"
322 [ $debug_symbols != default
] \
323 && cmake_opts
="$cmake_opts -DENABLE_DEBUG_SYMBOLS=$debug_symbols" \
324 && [ $debug_symbols = ON
] && build_dir
="$build_dir-debug_symbols"
325 [ $debug_context_mm != default
] \
326 && cmake_opts
="$cmake_opts -DENABLE_DEBUG_CONTEXT_MM=$debug_context_mm" \
327 && [ $debug_context_mm = ON
] && build_dir
="$build_dir-debug_context_mm"
328 [ $dumping != default
] \
329 && cmake_opts
="$cmake_opts -DENABLE_DUMPING=$dumping" \
330 && [ $dumping = ON
] && build_dir
="$build_dir-dumping"
331 [ $gpl != default
] \
332 && cmake_opts
="$cmake_opts -DENABLE_GPL=$gpl" \
333 && [ $gpl = ON
] && build_dir
="$build_dir-gpl"
334 [ $muzzle != default
] \
335 && cmake_opts
="$cmake_opts -DENABLE_MUZZLE=$muzzle" \
336 && [ $muzzle = ON
] && build_dir
="$build_dir-muzzle"
337 [ $optimized != default
] \
338 && cmake_opts
="$cmake_opts -DENABLE_OPTIMIZED=$optimized" \
339 && [ $optimized = ON
] && build_dir
="$build_dir-optimized"
340 [ $portfolio != default
] \
341 && cmake_opts
="$cmake_opts -DENABLE_PORTFOLIO=$portfolio" \
342 && [ $portfolio = ON
] && build_dir
="$build_dir-portfolio"
343 [ $proofs != default
] \
344 && cmake_opts
="$cmake_opts -DENABLE_PROOFS=$proofs" \
345 && [ $proofs = ON
] && build_dir
="$build_dir-proofs"
346 [ $replay != default
] \
347 && cmake_opts
="$cmake_opts -DENABLE_REPLAY=$replay" \
348 && [ $replay = ON
] && build_dir
="$build_dir-replay"
349 [ $shared != default
] \
350 && cmake_opts
="$cmake_opts -DENABLE_SHARED=$shared" \
351 && [ $shared = OFF
] && build_dir
="$build_dir-static"
352 [ $statistics != default
] \
353 && cmake_opts
="$cmake_opts -DENABLE_STATISTICS=$statistics" \
354 && [ $statistics = ON
] && build_dir
="$build_dir-stastitics"
355 [ $tracing != default
] \
356 && cmake_opts
="$cmake_opts -DENABLE_TRACING=$tracing" \
357 && [ $tracing = ON
] && build_dir
="$build_dir-tracing"
358 [ $unit_testing != default
] \
359 && cmake_opts
="$cmake_opts -DENABLE_UNIT_TESTING=$unit_testing" \
360 && [ $unit_testing = ON
] && build_dir
="$build_dir-unit_testing"
361 [ $python2 != default
] \
362 && cmake_opts
="$cmake_opts -DUSE_PYTHON2=$python2" \
363 && [ $python2 = ON
] && build_dir
="$build_dir-python2"
364 [ $valgrind != default
] \
365 && cmake_opts
="$cmake_opts -DENABLE_VALGRIND=$valgrind" \
366 && [ $valgrind = ON
] && build_dir
="$build_dir-valgrind"
367 [ $profiling != default
] \
368 && cmake_opts
="$cmake_opts -DENABLE_PROFILING=$profiling" \
369 && [ $profiling = ON
] && build_dir
="$build_dir-profiling"
370 [ $readline != default
] \
371 && cmake_opts
="$cmake_opts -DUSE_READLINE=$readline" \
372 && [ $readline = ON
] && build_dir
="$build_dir-readline"
373 [ $abc != default
] \
374 && cmake_opts
="$cmake_opts -DUSE_ABC=$abc" \
375 && [ $abc = ON
] && build_dir
="$build_dir-abc"
376 [ $cadical != default
] \
377 && cmake_opts
="$cmake_opts -DUSE_CADICAL=$cadical" \
378 && [ $cadical = ON
] && build_dir
="$build_dir-cadical"
379 [ $cln != default
] \
380 && cmake_opts
="$cmake_opts -DUSE_CLN=$cln" \
381 && [ $cln = ON
] && build_dir
="$build_dir-cln"
382 [ $cryptominisat != default
] \
383 && cmake_opts
="$cmake_opts -DUSE_CRYPTOMINISAT=$cryptominisat" \
384 && [ $cryptominisat = ON
] && build_dir
="$build_dir-cryptominisat"
385 [ $glpk != default
] \
386 && cmake_opts
="$cmake_opts -DUSE_GLPK=$glpk" \
387 && [ $glpk = ON
] && build_dir
="$build_dir-glpk"
388 [ $lfsc != default
] \
389 && cmake_opts
="$cmake_opts -DUSE_LFSC=$lfsc" \
390 && [ $lfsc = ON
] && build_dir
="$build_dir-lfsc"
391 [ $symfpu != default
] \
392 && cmake_opts
="$cmake_opts -DUSE_SYMFPU=$symfpu" \
393 && [ $symfpu = ON
] && build_dir
="$build_dir-symfpu"
395 [ $language_bindings_java != default
] \
396 && cmake_opts
="$cmake_opts -DBUILD_BINDINGS_JAVA=$language_bindings_java"
397 [ $language_bindings_python != default
] \
398 && cmake_opts
="$cmake_opts -DBUILD_BINDINGS_PYTHON=$language_bindings_python"
400 [ "$abc_dir" != default
] \
401 && cmake_opts
="$cmake_opts -DABC_DIR=$abc_dir"
402 [ "$antlr_dir" != default
] \
403 && cmake_opts
="$cmake_opts -DANTLR_DIR=$antlr_dir"
404 [ "$cadical_dir" != default
] \
405 && cmake_opts
="$cmake_opts -DCADICAL_DIR=$cadical_dir"
406 [ "$cryptominisat_dir" != default
] \
407 && cmake_opts
="$cmake_opts -DCRYPTOMINISAT_DIR=$cryptominisat_dir"
408 [ "$glpk_dir" != default
] \
409 && cmake_opts
="$cmake_opts -DGLPK_DIR=$glpk_dir"
410 [ "$lfsc_dir" != default
] \
411 && cmake_opts
="$cmake_opts -DLFSC_DIR=$lfsc_dir"
412 [ "$symfpu_dir" != default
] \
413 && cmake_opts
="$cmake_opts -DSYMFPU_DIR=$symfpu_dir"
414 [ "$install_prefix" != default
] \
415 && cmake_opts
="$cmake_opts -DCMAKE_INSTALL_PREFIX=$install_prefix"
419 if [ -n "$build_name" ]; then
420 # If a build name is specified just create directory 'build_name' for the
422 build_dir
=$build_name
423 mkdir
-p "$build_name"
425 # If no build name is specified create 'cmake-builds' directory and create
426 # the current build directory. Set symlink 'cmake-builds/build/' to current
428 build_dir
="$build_prefix$build_dir"
429 mkdir
-p "cmake-builds/$build_dir"
430 cd cmake-builds ||
exit 1
431 [ -e build
] && rm build
432 ln -s "$build_dir" build
# link to current build directory
435 cd "$build_dir" ||
exit 1
437 [ -e CMakeCache.txt
] && rm CMakeCache.txt
438 cmake
"$root_dir" $cmake_opts