2 # Process this file with autoconf to produce a configure script.
4 m4_define(_CVC4_MAJOR, 1) dnl version (major)
5 m4_define(_CVC4_MINOR, 5) dnl version (minor)
6 m4_define(_CVC4_RELEASE, 0) dnl version (alpha)
7 m4_define(_CVC4_EXTRAVERSION, [-prerelease]) dnl version (extra)
8 m4_define(_CVC4_RELEASE_STRING, _CVC4_MAJOR[.]_CVC4_MINOR[]m4_if(_CVC4_RELEASE,[0],,[.]_CVC4_RELEASE)_CVC4_EXTRAVERSION) dnl version string
10 dnl Preprocess CL args. Defined in config/cvc4.m4
14 AC_INIT([cvc4], _CVC4_RELEASE_STRING, [cvc-bugs@cs.nyu.edu])
15 AC_CONFIG_SRCDIR([src/include/cvc4_public.h])
16 AC_CONFIG_AUX_DIR([config])
17 AC_CONFIG_MACRO_DIR([config])
18 AC_CONFIG_LIBOBJ_DIR([src/lib])
19 AC_CONFIG_SUBDIRS([proofs/lfsc_checker])
21 m4_ifdef([AM_SILENT_RULES],[AM_SILENT_RULES([yes])])
23 CVC4_MAJOR=_CVC4_MAJOR
24 CVC4_MINOR=_CVC4_MINOR
25 CVC4_RELEASE=_CVC4_RELEASE
26 CVC4_EXTRAVERSION=_CVC4_EXTRAVERSION
27 CVC4_RELEASE_STRING=_CVC4_RELEASE_STRING
29 # Libtool version numbers for libraries
30 # Version numbers are in the form current:revision:age
33 # increment if interfaces have been added, removed or changed
35 # increment if source code has changed
36 # set to zero if current is incremented
38 # increment if interfaces have been added
39 # set to zero if interfaces have been removed
42 # For more information, see:
43 # http://www.gnu.org/software/libtool/manual/libtool.html#Versioning
44 # For guidance on when to change the version number, refer to the
47 m4_define([library_version], [m4_esyscmd([grep -F "$(grep -v '^#' library_versions | awk '{print$][1}' | sed 's,\\,\\\\\\,g' | (while read r; do if echo "]_CVC4_RELEASE_STRING[" | grep -q "^$r\$"; then echo "$r"; exit; fi; done; echo NO_MATCH_FOUND)) " library_versions | awk 'BEGIN {FS=":";OFS=":";RS=" "} /^$1:/ {print$][2,$][3,$][4}' | head -1])])
49 m4_define(_CVC4_LIBRARY_VERSION, library_version([libcvc4]))dnl
50 m4_define(_CVC4_PARSER_LIBRARY_VERSION, library_version([libcvc4parser]))dnl
51 m4_define(_CVC4_COMPAT_LIBRARY_VERSION, library_version([libcvc4compat]))dnl
52 m4_define(_CVC4_BINDINGS_LIBRARY_VERSION, library_version([libcvc4bindings]))dnl
54 m4_define([fatal_error], [m4_errprint(__program__:__file__:__line__[: fatal error: $*
57 m4_ifblank(_CVC4_LIBRARY_VERSION,[fatal_error([no CVC4_LIBRARY_VERSION defined for release version "]_CVC4_RELEASE_STRING[" in library_versions file])])dnl
58 m4_ifblank(_CVC4_PARSER_LIBRARY_VERSION,[fatal_error([no CVC4_PARSER_LIBRARY_VERSION defined for release version "]_CVC4_RELEASE_STRING[" in library_versions file])])dnl
59 m4_ifblank(_CVC4_COMPAT_LIBRARY_VERSION,[fatal_error([no CVC4_COMPAT_LIBRARY_VERSION defined for release version "]_CVC4_RELEASE_STRING[" in library_versions file])])dnl
60 m4_ifblank(_CVC4_BINDINGS_LIBRARY_VERSION,[fatal_error([no CVC4_BINDINGS_LIBRARY_VERSION defined for release version "]_CVC4_RELEASE_STRING[" in library_versions file])])dnl
62 CVC4_LIBRARY_VERSION=_CVC4_LIBRARY_VERSION
63 CVC4_PARSER_LIBRARY_VERSION=_CVC4_PARSER_LIBRARY_VERSION
64 CVC4_COMPAT_LIBRARY_VERSION=_CVC4_COMPAT_LIBRARY_VERSION
65 CVC4_BINDINGS_LIBRARY_VERSION=_CVC4_BINDINGS_LIBRARY_VERSION
67 # Using the AC_CANONICAL_* macros destroy the command line you get
68 # from $@, which we want later for determining the build profile. So
69 # we save it. (We can't do our build profile stuff here, or it's not
70 # included in the output... autoconf overrides us on the orderings of
73 cvc4_config_cmdline="${config_cmdline[[@]]}"
75 # remember if the user set these explicitly (or whether autoconf does)
76 user_specified_enable_or_disable_static=${enable_static+yes}
77 user_specified_enable_or_disable_shared=${enable_shared+yes}
79 if test -e src/include/cvc4_public.h; then
80 CVC4_CONFIGURE_AT_TOP_LEVEL=yes
82 CVC4_CONFIGURE_AT_TOP_LEVEL=no
85 # override autoconf: we don't want it giving us CFLAGS/CXXFLAGS, but we do
86 # want to respect the user's flags
87 if test -z "${CFLAGS+set}"; then CFLAGS=; fi
88 if test -z "${CXXFLAGS+set}"; then CXXFLAGS=; fi
91 AM_MAINTAINER_MODE([enable])
93 # turn off static lib building by default
103 if test "$enable_shared" = no -a "$user_specified_enable_or_disable_shared" = yes; then
107 # Features requested by the user
108 AC_MSG_CHECKING([for requested build profile])
110 [AS_HELP_STRING([--with-build=profile],
111 [for profile in {production,debug,competition,personal}])])
113 if test -z "${with_build+set}"; then
114 with_build=production
116 if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_dumping+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}" -a -z "${enable_replay+set}" -a -z "${with_gmp+set}" -a -z "${with_cln+set}" -a -z "${with_glpk+set}" -a -z "${with_abc+set}"; then
117 custom_build_profile=no
119 custom_build_profile=yes
122 if test -n "${enable_optimized+set}"; then
123 if test "$enable_optimized" = yes; then
124 btargs="$btargs optimized"
126 btargs="$btargs nooptimized"
129 # --enable-staticbinary is an alias for --enable-static-binary
130 if test -n "${enable_staticbinary+set}"; then
131 enable_static_binary="$enable_staticbinary"
133 if test -n "${enable_static_binary+set}"; then
134 if test "$enable_static_binary" = yes; then
135 btargs="$btargs staticbinary"
137 btargs="$btargs nostaticbinary"
140 if test -n "${enable_debug_symbols+set}"; then
141 if test "$enable_debug_symbols" = yes; then
142 btargs="$btargs debugsymbols"
144 btargs="$btargs nodebugsymbols"
147 if test -n "${enable_assertions+set}"; then
148 if test "$enable_assertions" = yes; then
149 btargs="$btargs assertions"
151 btargs="$btargs noassertions"
154 if test -n "${enable_proof+set}"; then
155 if test "$enable_proof" = yes; then
156 btargs="$btargs proof"
158 btargs="$btargs noproof"
161 if test -n "${enable_tracing+set}"; then
162 if test "$enable_tracing" = yes; then
163 btargs="$btargs tracing"
165 btargs="$btargs notracing"
168 if test -n "${enable_dumping+set}"; then
169 if test "$enable_dumping" = yes; then
170 btargs="$btargs dumping"
172 btargs="$btargs nodumping"
175 if test -n "${enable_muzzle+set}"; then
176 if test "$enable_muzzle" = yes; then
177 btargs="$btargs muzzle"
179 btargs="$btargs nomuzzle"
182 if test -n "${enable_coverage+set}"; then
183 if test "$enable_coverage" = yes; then
184 btargs="$btargs coverage"
186 btargs="$btargs nocoverage"
189 if test -n "${enable_profiling+set}"; then
190 if test "$enable_profiling" = yes; then
191 btargs="$btargs profiling"
193 btargs="$btargs noprofiling"
196 if test -n "${enable_statistics+set}"; then
197 if test "$enable_statistics" = yes; then
198 btargs="$btargs statistics"
200 btargs="$btargs nostatistics"
203 if test -n "${enable_replay+set}"; then
204 if test "$enable_replay" = yes; then
205 btargs="$btargs replay"
207 btargs="$btargs noreplay"
210 if test -n "${with_glpk+set}"; then
211 if test "$with_glpk" = yes; then
212 btargs="$btargs glpk"
215 if test -n "${with_abc+set}"; then
216 if test "$with_abc" = yes; then
220 AC_MSG_RESULT([$with_build])
222 AM_INIT_AUTOMAKE([1.11 no-define tar-pax parallel-tests color-tests subdir-objects])
223 AC_CONFIG_HEADERS([cvc4autoconfig.h])
225 # automake 1.12 changes the test driver mechanism in a way that is
226 # completely incompatible with 1.11. We figure out here which version
227 # we're using in order to set up test makefiles correctly.
228 # See http://lists.gnu.org/archive/html/automake/2012-04/msg00060.html
229 if test -z "$am__api_version"; then
230 AC_MSG_ERROR([Cannot determine automake API version ?!])
232 case "$am__api_version" in
233 1.11*) automake111=true ;;
234 *) automake111=false ;;
236 AM_CONDITIONAL([AUTOMAKE_1_11], [$automake111])
238 # Initialize libtool's configuration options.
239 # we're not DLL-clean yet (i.e., don't properly use dllexport and dllimport)
240 # _LT_SET_OPTION([LT_INIT],[win32-dll])
243 # Checks for programs.
257 [use CLN instead of GMP]
260 y|ye|yes|Y|YE|YES) cvc4_use_cln=1 ;;
261 n|no|N|NO) cvc4_use_cln=0 ;;
270 [use GMP instead of CLN]
273 y|ye|yes|Y|YE|YES) cvc4_use_gmp=1 ;;
274 n|no|N|NO) cvc4_use_gmp=0 ;;
279 if test $cvc4_use_cln = 1 -a $cvc4_use_gmp = 1 || test $cvc4_use_cln = 0 -a $cvc4_use_gmp = 0; then
280 AC_MSG_ERROR([You must use either CLN and GMP. Please pick one.])
282 if test $cvc4_use_gmp = 1; then
284 elif test $cvc4_use_gmp = 0; then
286 elif test $cvc4_use_cln = 1; then
288 elif test $cvc4_use_cln = 0; then
292 # try GMP, fail if not found; GMP is required for both CLN and for GMP
294 AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP (libgmp) not found, see http://gmplib.org/])])
296 if test $cvc4_use_cln = 2; then
297 if test "$CVC4_BSD_LICENSED_CODE_ONLY" = 1 -o "$with_portfolio" = yes; then
303 if test $cvc4_use_cln != 0; then
304 # [mdeters] The PKG_CHECK_MODULES macro isn't customizable and doesn't fail
305 # gracefully. You can only specify it once for a given library name. That
306 # is, even on separate if/else branches, you can't put
307 # PKG_CHECK_MODULES([CLN], ...). That's why things are so convoluted here,
308 # we have to have PKG_CHECK_MODULES _exactly_ once in configure.ac !
309 PKG_CHECK_MODULES([CLN], [cln >= 1.2.2],
312 save_CXXFLAGS="$CXXFLAGS"
313 LIBS="$CLN_LIBS $LIBS"
314 CXXFLAGS="$CLN_CFLAGS $CXXFLAGS"
315 AC_LINK_IFELSE([AC_LANG_PROGRAM([[#include <cln/cln.h>]], [[cln::cl_F pi = "3.1415926";]])], [
318 if test $cvc4_use_cln = 1; then
320 AC_MSG_ERROR([CLN installation missing, too old, or not functional for this architecture])
323 AC_MSG_NOTICE([CLN installation missing, too old, or not functional for this architecture, will use gmp instead])
328 CXXFLAGS="$save_CXXFLAGS"
332 [if test $cvc4_use_cln = 1; then
334 AC_MSG_ERROR([CLN not installed (or too old) or pkgconfig missing])
337 AC_MSG_NOTICE([CLN not installed (or too old) or pkgconfig missing, will use gmp])
344 if test $cvc4_use_cln = 0; then
345 # try GMPXX, fail if not found; don't need to link against it, only need its header
347 AC_CHECK_HEADER([gmpxx.h], , [AC_MSG_ERROR([GNU MP C++ library header (gmpxx.h) required but not found, see http://gmplib.org/])])
351 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }$CLN_CFLAGS"
352 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }$CLN_CFLAGS"
353 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }$CLN_CFLAGS"
354 LIBS="$CLN_LIBS${LIBS:+ $LIBS}"
358 if test $cvc4_cln_or_gmp = cln; then
359 AC_DEFINE_UNQUOTED(CVC4_CLN_IMP, [], [Defined if using the CLN multi-precision arithmetic library.])
361 AC_DEFINE_UNQUOTED(CVC4_GMP_IMP, [], [Defined if using the GMP multi-precision arithmetic library.])
363 AM_CONDITIONAL([CVC4_CLN_IMP], [test $cvc4_cln_or_gmp = cln])
364 AM_CONDITIONAL([CVC4_GMP_IMP], [test $cvc4_cln_or_gmp = gmp])
366 # construct the build string
367 AC_MSG_CHECKING([for appropriate build string])
368 if test -z "$ac_confdir"; then
371 build_type=`$ac_confdir/config/build-type $with_build $btargs $cvc4_cln_or_gmp`
372 AC_MSG_RESULT($build_type)
374 # Require building in target and build-specific build directory:
376 # If the configure script is invoked from the top-level source
377 # directory, it creates a suitable build directory (based on the build
378 # architecture and build profile from $build_type), changes into it,
379 # and reinvokes itself. CVC4_CONFIGURE_IN_BUILDS is an envariable
380 # that breaks any possibility of infinite recursion in this process.
381 AC_MSG_CHECKING([what dir to configure])
382 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
383 AC_MSG_RESULT([this one (in builds/)])
384 elif test "$CVC4_CONFIGURE_AT_TOP_LEVEL" = yes; then
385 AC_MSG_RESULT([builds/$target/$build_type])
387 if test -z "$ac_srcdir"; then
388 mkbuilddir=./config/mkbuilddir
390 mkbuilddir=$ac_srcdir/config/mkbuilddir
392 $as_echo "$mkbuilddir $target $build_type"
393 source $mkbuilddir "$target" "$build_type"
394 $as_echo "cd builds/$target/$build_type"
395 cd "builds/$target/$build_type"
396 CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS
397 # Runs the single recursive configure invocation using a relative path.
398 # See https://lists.gnu.org/archive/html/autoconf/2011-04/msg00060.html
399 echo "$SHELL ../../../configure ${config_cmdline[[@]]}"
400 "$SHELL" "../../../configure" "${config_cmdline[[@]]}"
403 if test $exitval -eq 0; then
404 cat >config.reconfig <<EOF
406 # Generated by configure, `date`
407 # This script is part of CVC4.
409 cd "\`dirname \\"\$0\\"\`"
411 if test -d builds; then :; else echo 'No builds/ directory!' >&2; exit; fi
413 current=(\`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]*\\)/\\(.*\\),\\1 \\2,'\`)
417 echo "reconfiguring in builds/\$arch/\$build..."
418 cd "builds/\$arch/\$build"
419 echo ./config.status "\$@"
420 ./config.status "\$@"]
422 chmod +x config.reconfig
424 ln -sf "$target/$build_type/config.log" "builds/config.log"
427 AC_MSG_RESULT([this one (user-specified)])
432 # Unpack standard build types. Any particular options can be overriden with
433 # --enable/disable-X options
434 # Tim: This needs to keep CVC4CPPFLAGS, CVC4CXXFLAGS, etc. set by earlier checks
435 case "$with_build" in
436 production) # highly optimized, no assertions, no tracing, dumping
437 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }"
438 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }"
439 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }"
440 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
441 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
442 if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=3 ; fi
443 if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
444 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
445 if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
446 if test -z "${enable_replay+set}" ; then enable_replay=no ; fi
447 if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi
448 if test -z "${enable_proof+set}" ; then enable_proof=yes ; fi
449 if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi
450 if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
451 if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
453 debug) # unoptimized, debug symbols, assertions, tracing, dumping
454 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DEBUG"
455 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-fno-inline"
456 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-fno-inline"
457 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
458 FLAG_VISIBILITY_HIDDEN=
459 if test -z "${enable_optimized+set}" ; then enable_optimized=no ; fi
460 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
461 if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
462 if test -z "${enable_replay+set}" ; then enable_replay=yes ; fi
463 if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi
464 if test -z "${enable_proof+set}" ; then enable_proof=yes ; fi
465 if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi
466 if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
467 if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
469 default) # moderately optimized, assertions, tracing, dumping
470 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }"
471 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }"
472 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }"
473 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
474 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
475 if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=2 ; fi
476 if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
477 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
478 if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
479 if test -z "${enable_replay+set}" ; then enable_replay=yes ; fi
480 if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi
481 if test -z "${enable_proof+set}" ; then enable_proof=yes ; fi
482 if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi
483 if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
484 if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
486 competition) # maximally optimized, no assertions, no tracing, no dumping, muzzled
487 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COMPETITION_MODE"
488 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs"
489 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs"
490 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
491 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
492 if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=9 ; fi
493 if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
494 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no ; fi
495 if test -z "${enable_statistics+set}" ; then enable_statistics=no ; fi
496 if test -z "${enable_replay+set}" ; then enable_replay=no ; fi
497 if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi
498 if test -z "${enable_proof+set}" ; then enable_proof=no ; fi
499 if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi
500 if test -z "${enable_dumping+set}" ; then enable_dumping=no ; fi
501 if test -z "${enable_muzzle+set}" ; then enable_muzzle=yes ; fi
502 if test -z "${user_specified_enable_or_disable_shared}"; then enable_shared=no; fi
503 if test -z "${user_specified_enable_or_disable_static}"; then enable_static=yes; fi
504 if test -z "${enable_static_binary+set}"; then enable_static_binary=yes ; fi
507 AC_MSG_FAILURE([unknown build profile: $with_build])
510 if test -z "${OPTLEVEL+set}"; then OPTLEVEL=3; fi
512 AM_CONDITIONAL([CVC4_BUILD_PROFILE_PRODUCTION], [test "$with_build" = production])
513 AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEBUG], [test "$with_build" = debug])
514 AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEFAULT], [test "$with_build" = default])
515 AM_CONDITIONAL([CVC4_BUILD_PROFILE_COMPETITION], [test "$with_build" = competition])
517 # permit a static binary
518 AC_MSG_CHECKING([whether to build a static binary])
519 AC_ARG_ENABLE([static-binary],
520 [AS_HELP_STRING([--enable-static-binary],
521 [build a fully statically-linked binary [default=no]])])
522 if test -z "${enable_static_binary+set}"; then
523 enable_static_binary=no
525 AC_MSG_RESULT([$enable_static_binary])
526 if test "$enable_static_binary" = yes; then
527 if test "$target_vendor" = apple; then
528 if test -z "$MAC_STATIC_BINARY_MANUAL_OVERRIDE"; then
529 AC_MSG_ERROR([[Statically-linked binaries are not supported on Mac OS. See https://developer.apple.com/library/mac/#qa/qa2001/qa1118.html . (If you ABSOLUTELY insist on this going forward and you know what you are doing, set MAC_STATIC_BINARY_MANUAL_OVERRIDE=1)]])
531 AC_MSG_WARN([MAC_STATIC_BINARY_MANUAL_OVERRIDE was set!])
532 AC_MSG_WARN([Will make a static binary during this build. Note that it may fail!])
535 if test "$enable_static" != yes; then
537 AC_MSG_WARN([forcing static-library building, --enable-static-binary given])
541 AC_MSG_CHECKING([whether to support proofs in libcvc4])
543 AC_ARG_ENABLE([proof],
544 [AS_HELP_STRING([--disable-proof],
545 [do not support proof generation])])
546 if test -z "${enable_proof+set}"; then
549 AC_MSG_RESULT([$enable_proof])
551 if test "$enable_proof" = yes; then
552 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROOF"
554 AM_CONDITIONAL([CVC4_PROOF], [test "$enable_proof" = yes])
556 AC_MSG_CHECKING([whether to optimize libcvc4])
558 AC_ARG_ENABLE([optimized],
559 [AS_HELP_STRING([--enable-optimized],
560 [optimize the build])])
562 if test -z "${enable_optimized+set}"; then
566 AC_MSG_RESULT([$enable_optimized])
568 if test "$enable_optimized" = yes; then
569 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O$OPTLEVEL"
570 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O$OPTLEVEL"
572 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O0"
573 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O0"
576 AC_MSG_CHECKING([whether to include debugging symbols in libcvc4])
578 AC_ARG_ENABLE([debug-symbols],
579 [AS_HELP_STRING([--disable-debug-symbols],
580 [do not include debug symbols in libcvc4])])
582 if test -z "${enable_debug_symbols+set}"; then
583 enable_debug_symbols=yes
586 AC_MSG_RESULT([$enable_debug_symbols])
588 if test "$enable_debug_symbols" = yes; then
589 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-ggdb3"
590 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-ggdb3"
593 AC_MSG_CHECKING([whether to include statistics are turned on in libcvc4])
595 AC_ARG_ENABLE([statistics],
596 [AS_HELP_STRING([--disable-statistics],
597 [do not include statistics in libcvc4])])
599 if test -z "${enable_statistics+set}"; then
600 enable_statistics=yes
603 AC_MSG_RESULT([$enable_statistics])
605 if test "$enable_statistics" = yes; then
606 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_STATISTICS_ON"
609 AC_MSG_CHECKING([whether the replay feature should be turned on in libcvc4])
611 AC_ARG_ENABLE([replay],
612 [AS_HELP_STRING([--disable-replay],
613 [turn off the replay feature in libcvc4])])
615 if test -z "${enable_replay+set}"; then
619 AC_MSG_RESULT([$enable_replay])
621 if test "$enable_replay" = yes; then
622 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_REPLAY"
625 AC_MSG_CHECKING([whether to include assertions in build])
627 AC_ARG_ENABLE([assertions],
628 [AS_HELP_STRING([--disable-assertions],
629 [turn off assertions in build])])
631 if test -z "${enable_assertions+set}"; then
632 enable_assertions=yes
635 AC_MSG_RESULT([$enable_assertions])
637 if test "$enable_assertions" = yes; then
638 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_ASSERTIONS"
640 # turn off regular C assert() also
641 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DNDEBUG"
644 AC_MSG_CHECKING([whether to do a traceable build of CVC4])
645 AC_ARG_ENABLE([tracing],
646 [AS_HELP_STRING([--disable-tracing],
647 [remove all tracing code from CVC4])])
649 if test -z "${enable_tracing+set}"; then
653 AC_MSG_RESULT([$enable_tracing])
655 if test "$enable_tracing" = yes; then
656 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_TRACING"
659 AC_MSG_CHECKING([whether to do a dump-capable build of CVC4])
660 AC_ARG_ENABLE([dumping],
661 [AS_HELP_STRING([--disable-dumping],
662 [remove all dumping code from CVC4])])
664 if test -z "${enable_dumping+set}"; then
668 AC_MSG_RESULT([$enable_dumping])
670 if test "$enable_dumping" = yes; then
671 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DUMPING"
674 AC_MSG_CHECKING([whether to do a muzzled build of CVC4])
675 AC_ARG_ENABLE([muzzle],
676 [AS_HELP_STRING([--enable-muzzle],
677 [completely silence CVC4; remove ALL non-result output from build])])
679 if test -z "${enable_muzzle+set}"; then
683 AC_MSG_RESULT([$enable_muzzle])
685 if test "$enable_muzzle" = yes; then
686 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_MUZZLE"
689 AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4])
690 AC_ARG_ENABLE([coverage],
691 [AS_HELP_STRING([--enable-coverage],
692 [build with support for gcov coverage testing])])
694 if test -z "${enable_coverage+set}"; then
698 AC_MSG_RESULT([$enable_coverage])
700 if test "$enable_coverage" = yes; then
701 # For coverage testing, we prefer:
702 # --enable-static --disable-shared --disable-static-binary
703 # If the user didn't specify these, we force them here. If the
704 # user specified them in opposite phase, give warnings that they
705 # shouldn't do that, or bomb out.
706 if test "$user_specified_enable_or_disable_shared" != yes; then
708 AC_MSG_WARN([turning off shared library building due to --enable-coverage])
709 elif test "$enable_shared" = yes; then
711 AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-shared])
712 AC_MSG_WARN([gcov does not support shared libraries, so only your static libraries will be coverage-testable.])
713 AC_MSG_WARN([Your cvc4 driver and testing binaries will not be coverage-testable.])
716 if test "${enable_static_binary+set}" = set -a "$enable_static_binary" = yes; then
718 AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-static-binary])
719 AC_MSG_WARN([Your cvc4 driver and testing binaries will be fully-statically linked and may not be coverage-testable.])
722 if test "$user_specified_enable_or_disable_static" != yes; then
724 AC_MSG_WARN([turning on static library building due to --enable-coverage])
725 elif test "$enable_static" != yes; then
726 AC_MSG_ERROR([--enable-coverage and --disable-static are incompatible; gcov only supports static libraries.])
729 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COVERAGE"
730 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }--coverage"
731 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }--coverage"
732 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }--coverage"
735 AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4])
737 AC_ARG_ENABLE([profiling],
738 [AS_HELP_STRING([--enable-profiling],
739 [build with support for gprof profiling])])
741 if test -z "${enable_profiling+set}"; then
745 AC_MSG_RESULT([$enable_profiling])
747 if test "$enable_profiling" = yes; then
748 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROFILING"
749 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-pg"
750 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-pg"
751 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }-pg"
754 # Check for libglpk (defined in config/glpk.m4)
756 [AS_HELP_STRING([--with-glpk],
757 [use GLPK simplex solver])], [], [with_glpk=])
759 if test $have_libglpk -eq 1; then
760 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_GLPK"
762 AM_CONDITIONAL([CVC4_USE_GLPK], [test $have_libglpk -eq 1])
763 AC_SUBST([GLPK_LDFLAGS])
764 AC_SUBST([GLPK_LIBS])
766 # Build with libabc (defined in config/abc.m4)
768 [AS_HELP_STRING([--with-abc],
769 [use the ABC AIG library])], [], [with_abc=])
771 if test $have_libabc -eq 1; then
772 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_ABC"
774 AM_CONDITIONAL([CVC4_USE_ABC], [test $have_libabc -eq 1])
775 AC_SUBST([ABC_LDFLAGS])
778 # Check to see if this version/architecture of GNU C++ explicitly
779 # instantiates __gnu_cxx::hash<uint64_t> or not. Some do, some don't.
780 # See src/util/hash.h.
781 AC_MSG_CHECKING([whether __gnu_cxx::hash<uint64_t> is already specialized])
783 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
785 #include <ext/hash_map>
786 namespace __gnu_cxx { template<> struct hash<uint64_t> {}; }])],
787 [AC_MSG_RESULT([no]); CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_NEED_HASH_UINT64_T"],
788 [AC_MSG_RESULT([yes])])
791 # Check whether "long" and "int64_t" are distinct types w.r.t. overloading.
792 # Even if they have the same size, they can be distinct, and some platforms
793 # can have problems with ambiguous function calls when auto-converting
794 # int64_t to long, and others will complain if you overload a function
795 # that takes an int64_t with one that takes a long (giving a redefinition
796 # error). So we have to keep both happy. Probably the same underlying
797 # issue as the hash specialization above, but let's check separately
799 AC_MSG_CHECKING([for the relationship between long and int64_t])
801 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
804 void foo(int64_t) {}])],
805 [AC_MSG_RESULT([no relationship detected]); CVC4_NEED_INT64_T_OVERLOADS=1],
806 [AC_MSG_RESULT([typedef or similar]); CVC4_NEED_INT64_T_OVERLOADS=0])
808 AC_SUBST([CVC4_NEED_INT64_T_OVERLOADS])
810 # Check for ANTLR runantlr script (defined in config/antlr.m4)
813 CVC4_CXX_OPTION([-Werror], [WERROR])
814 CVC4_C_OPTION([-Werror], [C_WERROR])
815 CVC4_CXX_OPTION([-Wno-deprecated], [WNO_DEPRECATED])
816 CVC4_C_OPTION([-Wno-deprecated], [C_WNO_DEPRECATED])
817 CVC4_CXX_OPTION([-Wno-conversion-null], [WNO_CONVERSION_NULL])
818 CVC4_CXX_OPTION([-Wno-tautological-compare], [WNO_TAUTOLOGICAL_COMPARE])
819 CVC4_CXX_OPTION([-Wno-parentheses], [WNO_PARENTHESES])
820 CVC4_CXX_OPTION([-Wno-uninitialized], [WNO_UNINITIALIZED])
821 CVC4_CXX_OPTION([-Wno-unused-variable], [WNO_UNUSED_VARIABLE])
822 CVC4_CXX_OPTION([-fno-strict-aliasing], [FNO_STRICT_ALIASING])
824 AC_SUBST([WNO_CONVERSION_NULL])
825 AC_SUBST([WNO_TAUTOLOGICAL_COMPARE])
826 AC_SUBST([WNO_PARENTHESES])
827 AC_SUBST([WNO_UNINITIALIZED])
828 AC_SUBST([WNO_UNUSED_VARIABLE])
829 AC_SUBST([FNO_STRICT_ALIASING])
831 # On Mac, we have to fix the visibility of standard library symbols.
832 # Otherwise, exported template instantiations---even though explicitly
833 # CVC4_PUBLIC, can be generated as symbols with internal-only linkage.
834 # Presumably, Apple is distributing a libstdc++ that is built *without*
835 # --enable-libstdcxx-visibility (?)
836 if test "$target_vendor" = apple; then
837 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-D_GLIBCXX_VISIBILITY_DEFAULT=\"__attribute__((__visibility__(\\\"default\\\")))\""
840 # Tell top-level Makefile to include $(top_srcdir)/personal.mk
841 AC_ARG_ENABLE([personal-make-rules],
842 [AS_HELP_STRING([--enable-personal-make-rules],
843 [include top-level personal.mk (if it exists)])])
844 if test "$enable_personal_make_rules" = yes; then
845 # This allows us to include a personal.mk makefile from every
846 # generated makefile. Named zz_* in order to make sure this
847 # comes last, so it gets other definitions (in particular top_srcdir).
848 zz_cvc4_use_personal_make_rules='yes
851 include $(top_srcdir)/personal.mk
852 $(top_srcdir)/personal.mk:; @touch "$@"'
853 AC_SUBST([zz_cvc4_use_personal_make_rules])
856 # Doxygen configuration
857 AC_ARG_ENABLE([internals-documentation],
858 [AS_HELP_STRING([--enable-internals-documentation],
859 [build Doxygen documentation for static and private member functions])])
860 if test "$enable_internals_documentation" = yes; then
861 DOXYGEN_EXTRACT_PRIVATE=YES
862 DOXYGEN_EXTRACT_STATIC=YES
864 DOXYGEN_EXTRACT_PRIVATE=NO
865 DOXYGEN_EXTRACT_STATIC=NO
867 AC_SUBST([DOXYGEN_EXTRACT_PRIVATE])
868 AC_SUBST([DOXYGEN_EXTRACT_STATIC])
874 DX_INIT_DOXYGEN($PACKAGE_NAME, config/doxygen.cfg, $srcdir/doc/doxygen)
876 AC_ARG_ENABLE([unit-testing], AS_HELP_STRING([--disable-unit-testing], [don't build support for unit testing, even if available]), , [enable_unit_testing=check])
877 AC_ARG_VAR(CXXTEST, [path to CxxTest installation])
881 AC_ARG_WITH([cxxtest-dir],
882 [AS_HELP_STRING([--with-cxxtest-dir=DIR], [path to CxxTest installation])],
883 [CXXTEST="$withval"])
885 # In the case of "./configure --with-cxxtest-dir=../cxxtest" (or other
886 # relative path) and having switched the configure directory (see above),
887 # search with respect to the top source dir, not the build dir
888 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes -a -n "$CXXTEST"; then
891 *) CXXTEST="$srcdir/$CXXTEST" ;;
897 if test "$enable_proof" = yes; then
898 RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--proof"
900 AC_SUBST([TESTS_ENVIRONMENT])
901 AC_SUBST([RUN_REGRESSION_ARGS])
904 AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH])
905 if test -z "$CXXTESTGEN"; then
906 AC_PATH_PROG(CXXTESTGEN, cxxtestgen.py, [], [$CXXTEST:$PATH])
908 if test -z "$CXXTESTGEN"; then
909 AC_PATH_PROG(CXXTESTGEN, cxxtestgen, [], [$CXXTEST:$PATH])
911 # The latest version of cxxtest distributed from the git repository places
912 # cxxtest under <cxxtest-root>/bin/cxxtest
913 if test -z "$CXXTESTGEN"; then
914 AC_PATH_PROG(CXXTESTGEN, cxxtestgen, [], [$CXXTEST/bin:$PATH])
916 if test "$enable_unit_testing" = "no"; then
917 AC_MSG_NOTICE([unit tests disabled by user request.])
920 elif test -z "$CXXTESTGEN"; then
921 AC_MSG_NOTICE([unit tests disabled, could not find cxxtestgen.pl or cxxtestgen.py or cxxtestgen])
922 elif test -z "$CXXTEST"; then
923 CXXTEST=`dirname "$CXXTESTGEN"`
924 AC_MSG_CHECKING([for location of CxxTest headers])
925 if test -e "$CXXTEST/cxxtest/TestRunner.h"; then
926 AC_MSG_RESULT([$CXXTEST])
928 if test -e "/usr/include/cxxtest/TestRunner.h"; then
929 AC_MSG_RESULT([/usr/include])
931 AC_MSG_RESULT([not found])
932 AC_MSG_WARN([unit tests disabled, CxxTest headers not found.])
939 if test "$enable_unit_testing" = yes -a -z "$CXXTESTGEN"; then
940 AC_MSG_ERROR([--enable-unit-testing given but cxxtest not found.])
943 AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"])
945 AC_ARG_VAR(TEST_CPPFLAGS, [CPPFLAGS to use when testing (default=$CPPFLAGS)])
946 AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)])
947 AC_ARG_VAR(TEST_LDFLAGS, [LDFLAGS to use when testing (default=$LDFLAGS)])
949 AC_ARG_VAR(PERL, [PERL interpreter (used when testing)])
951 if test -n "$CXXTEST"; then
952 if test -z "$PERL"; then
953 AC_CHECK_PROGS(PERL, perl, perl, [])
955 AC_CHECK_PROG(PERL, "$PERL", "$PERL", [])
958 if test -z "$PERL"; then
959 AC_MSG_WARN([unit tests disabled, perl not found.])
965 AC_ARG_VAR(PYTHON, [PYTHON interpreter (used for building legacy Java library interface)])
967 if test -z "$PYTHON"; then
968 AC_CHECK_PROGS(PYTHON, python, python, [])
970 AC_CHECK_PROG(PYTHON, "$PYTHON", "$PYTHON", [])
973 if test -z "$PYTHON"; then
974 AC_MSG_WARN([python not found, cannot build libcvc4compat_java (the legacy Java interface).])
979 # Checks for libraries.
981 AC_SEARCH_LIBS([clock_gettime], [rt],
982 [AC_DEFINE([HAVE_CLOCK_GETTIME], [1],
983 [Defined to 1 if clock_gettime() is supported by the platform.])],
984 [AC_LIBOBJ([clock_gettime])])
985 AC_CHECK_FUNC([strtok_r], [AC_DEFINE([HAVE_STRTOK_R], [1],
986 [Defined to 1 if strtok_r() is supported by the platform.])],
987 [AC_LIBOBJ([strtok_r])])
988 AC_CHECK_FUNC([ffs], [AC_DEFINE([HAVE_FFS], [1],
989 [Defined to 1 if ffs() is supported by the platform.])],
992 # Check for antlr C++ runtime (defined in config/antlr.m4)
995 # Check for user preferences for language bindings to build, and for
996 # build support. The arg list is the default set if unspecified by
997 # the user (the actual built set is the subset that appears to be
998 # supported by the build host).
999 CVC4_CHECK_BINDINGS([c java])dnl csharp perl php python ruby tcl ocaml])
1001 # Checks for header files and their contents.
1002 AC_CHECK_HEADERS([getopt.h unistd.h ext/stdio_filebuf.h])
1004 # Checks for typedefs, structures, and compiler characteristics.
1006 # these are bad macros, they clash with system header <stdint.h> !!
1012 # guard against double-inclusion of the autoheader
1013 AH_TOP([#ifndef __CVC4__CVC4AUTOCONFIG_H
1014 #define __CVC4__CVC4AUTOCONFIG_H])
1015 AH_BOTTOM([#endif /* __CVC4__CVC4AUTOCONFIG_H */])
1017 AC_CHECK_DECLS([optreset], [], [], [#include <getopt.h>])
1019 # check with which standard strerror_r() complies
1022 # is is_sorted() in std or __gnu_cxx?
1025 # require boost library
1028 # look for boost threading library
1029 AC_ARG_WITH([portfolio],
1030 AS_HELP_STRING([--with-portfolio], [build the multithreaded portfolio version of CVC4 (pcvc4)]))
1031 cvc4_save_LDFLAGS="$LDFLAGS"
1032 if test "$enable_static_binary" = yes; then
1033 LDFLAGS="-static $LDFLAGS"
1035 cvc4_has_threads=yes
1036 AC_ARG_ENABLE([thread-support],
1037 AS_HELP_STRING([--disable-thread-support], [do not support multithreaded-capable library]))
1038 if test "$enable_thread_support" = no; then
1040 if test "$with_portfolio" = yes; then
1041 AC_MSG_ERROR([user gave both --with-portfolio and --disable-thread-support, which are contradictory])
1044 BOOST_THREADS([], [AC_MSG_WARN([disabling multithreaded support])
1045 cvc4_has_threads=no])
1047 LDFLAGS="$cvc4_save_LDFLAGS"
1048 if test $cvc4_has_threads = no; then
1049 if test "$enable_thread_support" = yes; then
1050 AC_MSG_ERROR([user gave --enable-thread-support but could not build with threads; maybe boost threading library is missing?])
1052 if test "$with_portfolio" = yes; then
1053 AC_MSG_ERROR([user gave --with-portfolio but could not build with threads; maybe boost threading library is missing?])
1057 if test "$with_portfolio" != yes; then
1060 AM_CONDITIONAL([CVC4_BUILD_PCVC4], [test "$with_portfolio" = yes])
1061 if test "$with_portfolio" = yes; then
1062 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PORTFOLIO"
1064 # see if Boost has thread attributes (should be any version >= 1.50.0)
1065 # non-fatal error if not, but we won't support --thread-stack option
1066 AC_MSG_CHECKING([whether Boost threads support thread attrs])
1068 cvc4_save_CPPFLAGS="$CPPFLAGS"
1069 cvc4_save_LIBS="$LIBS"
1070 cvc4_save_LDFLAGS="$LDFLAGS"
1071 CPPFLAGS="$CPPFLAGS $BOOST_CPPFLAGS"
1072 LIBS="$LIBS $BOOST_THREAD_LIBS"
1073 LDFLAGS="$LDFLAGS $BOOST_THREAD_LDFLAGS"
1074 AC_LINK_IFELSE([AC_LANG_PROGRAM([#include <boost/thread.hpp>],
1075 [boost::thread::attributes attrs; attrs.set_stack_size(10 * 1024 * 1024);])],
1076 [cvc4_boost_has_thread_attr=1;
1077 AC_MSG_RESULT([yes])],
1078 [cvc4_boost_has_thread_attr=0;
1079 AC_MSG_RESULT([no])])
1080 CPPFLAGS="$cvc4_save_CPPFLAGS"
1081 LIBS="$cvc4_save_LIBS"
1082 LDFLAGS="$cvc4_save_LDFLAGS"
1085 cvc4_boost_has_thread_attr=0
1087 AC_DEFINE_UNQUOTED([BOOST_HAS_THREAD_ATTR], $cvc4_boost_has_thread_attr, [Define to 1 if Boost threading library has support for thread attributes])
1089 # Check for libreadline (defined in config/readline.m4)
1090 AC_ARG_WITH([readline], [AS_HELP_STRING([--with-readline], [support the readline library])], [], [with_readline=check])
1091 # make the flags as close as possible to the final flags, because the Boost
1092 # flags can bring in a different, incompatible readline library than we'd
1093 # get otherwise (e.g. on Mac, where there are commonly two different readlines,
1094 # one in /usr and one in /opt/local)
1095 cvc4_rlcheck_save_CPPFLAGS="$CPPFLAGS"
1096 cvc4_rlcheck_save_CXXFLAGS="$CXXFLAGS"
1097 cvc4_rlcheck_save_CFLAGS="$CFLAGS"
1098 cvc4_rlcheck_save_LDFLAGS="$LDFLAGS"
1099 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
1100 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS $WNO_DEPRECATED"
1101 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS $C_WNO_DEPRECATED -fexceptions"
1102 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
1103 CVC4_CHECK_FOR_READLINE
1104 CPPFLAGS="$cvc4_rlcheck_save_CPPFLAGS"
1105 CXXFLAGS="$cvc4_rlcheck_save_CXXFLAGS"
1106 CFLAGS="$cvc4_rlcheck_save_CFLAGS"
1107 LDFLAGS="$cvc4_rlcheck_save_LDFLAGS"
1108 AC_DEFINE_UNQUOTED([HAVE_LIBREADLINE], $have_libreadline, [Define to 1 to use libreadline])
1109 AC_DEFINE_UNQUOTED([READLINE_COMPENTRY_FUNC_RETURNS_CHARP], $readline_compentry_func_returns_charp, [Define to 1 if rl_completion_entry_function is declared to return pointer to char])
1110 AC_SUBST([READLINE_LIBS])
1112 # Whether to build compatibility library
1113 CVC4_BUILD_LIBCOMPAT=yes
1114 AC_ARG_WITH([compat],
1115 AS_HELP_STRING([--with-compat], [build compatibility library (CVC3 API layer)]),
1116 [if test "$withval" = no; then CVC4_BUILD_LIBCOMPAT=no; fi])
1117 AC_MSG_CHECKING([whether to build compatibility library (CVC3 API layer)])
1118 if test "$CVC4_BUILD_LIBCOMPAT" = yes; then
1119 AC_MSG_RESULT([yes])
1121 AC_MSG_RESULT([no, disabled by user])
1123 AC_SUBST(CVC4_BUILD_LIBCOMPAT)
1124 AM_CONDITIONAL([CVC4_BUILD_LIBCOMPAT], [test "$CVC4_BUILD_LIBCOMPAT" = yes])
1126 # Check for availability of TLS support (e.g. __thread storage class)
1127 AC_MSG_CHECKING([whether to use compiler-supported TLS if available])
1128 AC_ARG_ENABLE([tls], AS_HELP_STRING([--disable-tls], [don't use compiler-native TLS]))
1129 if test $cvc4_has_threads = no; then
1130 # We disable TLS entirely by simply telling the build system that
1131 # the empty string is the __thread keyword.
1132 AC_MSG_RESULT([multithreading disabled])
1133 CVC4_TLS_SUPPORTED=1
1135 CVC4_TLS_explanation='disabled (no multithreading support)'
1137 if test -z "${enable_tls+set}" || test "$enable_tls" = "yes"; then
1138 AC_MSG_RESULT([yes])
1139 AX_TLS([CVC4_TLS=$ac_cv_tls], [CVC4_TLS=])
1144 if test -n "$CVC4_TLS"; then
1145 CVC4_TLS_SUPPORTED=1
1146 CVC4_TLS_explanation="$CVC4_TLS"
1148 CVC4_TLS_explanation='pthread_getspecific()'
1149 CVC4_TLS_SUPPORTED=0
1152 AC_SUBST([CVC4_TLS])
1153 AC_SUBST([CVC4_TLS_SUPPORTED])
1155 # Whether to compile with google profiling tools
1156 cvc4_use_google_perftools=0
1160 [--with-google-perftools],
1161 [use Google Performance Tools]
1163 [if test "$withval" != no; then
1164 cvc4_use_google_perftools=1
1168 AC_MSG_CHECKING([whether to link in google perftools libraries])
1169 if test $cvc4_use_google_perftools = 1; then
1170 AC_MSG_RESULT([yes])
1171 AC_CHECK_LIB([tcmalloc], [MallocExtension_GetAllocatedSize], , [AC_MSG_ERROR([cannot link google-perftools test program with -ltcmalloc])], [-lpthread])
1172 AC_CHECK_LIB([profiler], [ProfilerStart], , [AC_MSG_ERROR([cannot link google-perftools test program with -lprofiler])], [-lpthread])
1174 AC_MSG_RESULT([no (user didn't request it)])
1178 AC_ARG_VAR(JAVA, [Java interpreter (used when testing Java interface)])
1179 AC_ARG_VAR(JAVAC, [Java compiler (used when building and testing Java interface)])
1180 AC_ARG_VAR(JAVAH, [Java compiler (used when building and testing Java interface)])
1181 AC_ARG_VAR(JAR, [Jar archiver (used when building Java interface)])
1182 if test "$cvc4_build_java_bindings"; then
1184 if test -z "$JAVA"; then
1185 AC_CHECK_PROGS(JAVA, java, java, [])
1187 AC_CHECK_PROG(JAVA, "$JAVA", "$JAVA", [])
1189 if test -z "$JAVAC"; then
1190 AC_CHECK_PROGS(JAVAC, javac gcj, javac, [])
1191 if test "$JAVAC" = gcj; then JAVAC='gcj -C'; fi
1193 AC_CHECK_PROG(JAVAC, "$JAVAC", "$JAVAC", [])
1195 if test -z "$JAVAH"; then
1196 AC_CHECK_PROGS(JAVAH, javah gcjh, javah, [])
1198 AC_CHECK_PROG(JAVAH, "$JAVAH", "$JAVAH", [])
1200 if test -z "$JAR"; then
1201 AC_CHECK_PROGS(JAR, jar, jar, [])
1203 AC_CHECK_PROG(JAR, "$JAR", "$JAR", [])
1207 # on Mac OS X, Java doesn't like the .so module extension; it wants .dylib
1208 module=no eval CVC4_JAVA_MODULE_EXT="$shrext_cmds"
1209 if test -z "$CVC4_JAVA_MODULE_EXT"; then
1210 CVC4_JAVA_MODULE_EXT=.so
1212 AC_SUBST([CVC4_JAVA_MODULE_EXT])
1214 # Prepare configure output
1216 if test "$enable_shared" = yes; then BUILDING_SHARED=1; else BUILDING_SHARED=0; fi
1217 if test "$enable_static" = yes; then BUILDING_STATIC=1; else BUILDING_STATIC=0; fi
1218 if test "$enable_static_binary" = yes; then STATIC_BINARY=1; else STATIC_BINARY=0; fi
1219 AC_SUBST(BUILDING_SHARED)
1220 AC_SUBST(BUILDING_STATIC)
1221 AC_SUBST(STATIC_BINARY)
1222 AM_CONDITIONAL([STATIC_BINARY], [test "$enable_static_binary" = yes])
1223 AM_CONDITIONAL([COVERAGE_ENABLED], [test "$enable_coverage" = yes])
1225 AM_CONDITIONAL([CVC4_DEBUG], [test "$with_build" = debug])
1226 AM_CONDITIONAL([CVC4_TRACING], [test "$enable_tracing" = yes])
1228 AC_SUBST(CVC4_LIBRARY_VERSION)
1229 AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
1230 AC_SUBST(CVC4_COMPAT_LIBRARY_VERSION)
1231 AC_SUBST(CVC4_BINDINGS_LIBRARY_VERSION)
1233 AC_DEFINE_UNQUOTED(CVC4_MAJOR, ${CVC4_MAJOR}, [Major component of the version of CVC4.])
1234 AC_DEFINE_UNQUOTED(CVC4_MINOR, ${CVC4_MINOR}, [Minor component of the version of CVC4.])
1235 AC_DEFINE_UNQUOTED(CVC4_RELEASE, ${CVC4_RELEASE}, [Release component of the version of CVC4.])
1236 AC_DEFINE_UNQUOTED(CVC4_EXTRAVERSION, ["${CVC4_EXTRAVERSION}"], [Extraversion component of the version of CVC4.])
1237 AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full release string for CVC4.])
1239 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
1240 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
1241 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions"
1242 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
1244 # visibility flag not supported for Windows builds
1245 # also increase default stack size for Windows binaries
1247 (*mingw*) FLAG_VISIBILITY_HIDDEN=
1248 cvc4_LDFLAGS=-Wl,--stack,134217728
1249 pcvc4_LDFLAGS=-Wl,--stack,134217728
1252 AC_SUBST(FLAG_VISIBILITY_HIDDEN)
1253 AC_SUBST(cvc4_LDFLAGS)
1254 AC_SUBST(pcvc4_LDFLAGS)
1256 AM_CONDITIONAL(WHITE_AND_BLACK_TESTS, [test -z "$FLAG_VISIBILITY_HIDDEN"])
1258 # remember the command line used for configure
1259 AC_SUBST(cvc4_config_cmdline)
1263 # When automake scans Makefiles, it complains about non-standard make
1264 # features (including GNU extensions), and breaks GNU Make's
1265 # "if/endif" construct, replacing the "if" with AM_CONDITIONAL if
1266 # constructs. automake even follows "include" and messes with
1267 # included Makefiles.
1269 # CVC4 assumes GNU Make and we want to use GNU Make if/endifs, so we
1270 # have to hide some included Makefiles with GNU extensions. We do
1271 # this by defining mk_include as an autoconf substitution and then
1272 # using "@mk_include@ other_makefile" in Makefile.am to include
1273 # makefiles with GNU extensions; this hides them from automake.
1275 AC_SUBST(mk_include)
1276 # Similar trickery for "if"
1284 # This is used to _always_ comment out rules in automake makefiles, but
1285 # still trigger certain automake behavior; see test/unit/Makefile.am.
1286 AM_CONDITIONAL([CVC4_FALSE], [false])
1288 # set up substitutions for src/util/{rational,integer}.h.in
1289 if test $cvc4_cln_or_gmp = cln; then
1296 AC_SUBST(CVC4_USE_CLN_IMP)
1297 AC_SUBST(CVC4_USE_GMP_IMP)
1299 # month/year for man pages
1300 MAN_DATE=`date '+%B %Y'`
1306 proofs/signatures/Makefile]
1307 m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | grep -v '^contrib/alttheoryskel/' | sort | sed 's,\.am$,,'])
1310 if test $cvc4_has_threads = yes; then
1311 support_multithreaded='with boost threading library'
1312 AM_CONDITIONAL([CVC4_HAS_THREADS], [true])
1313 AC_SUBST([CVC4_HAS_THREADS], 1)
1315 support_multithreaded='no'
1316 AM_CONDITIONAL([CVC4_HAS_THREADS], [false])
1317 AC_SUBST([CVC4_HAS_THREADS], 0)
1320 AM_CONDITIONAL([CVC4_NEEDS_REPLACEMENT_FUNCTIONS], [test -n "$LIBOBJS"])
1322 # Final information to the user
1326 if test "$custom_build_profile" = yes; then
1327 with_build="$with_build (customized)"
1330 support_unit_tests='cxxtest not found; unit tests not supported'
1331 if test -n "$CXXTEST"; then
1332 support_unit_tests='unit testing infrastructure enabled in build directory'
1333 elif test "$enable_unit_testing" = no; then
1334 support_unit_tests='unit testing disabled by user'
1337 if test "$enable_optimized" = yes; then
1338 optimized="yes, at level $OPTLEVEL"
1343 if test $have_libglpk -eq 1; then
1345 gpllibs="${gpllibs} glpk"
1348 if test $have_libreadline -eq 1; then
1350 gpllibs="${gpllibs} readline"
1353 if test $cvc4_cln_or_gmp = cln; then
1354 mplibrary='cln (GPL)'
1356 gpllibs="${gpllibs} cln"
1357 if test $with_portfolio = yes; then
1358 AC_ERROR([Bad configuration detected: cannot build portfolio with CLN.
1359 Please specify only one of --with-portfolio and --with-cln.])
1365 if test "$gpl" = yes; then
1366 if test "$CVC4_BSD_LICENSED_CODE_ONLY" = 1; then
1367 AC_ERROR([Bad configuration detected: BSD-licensed code only, but also requested GPLed libraries:$gpllibs
1368 To permit GPL'ed dependences, use the configure flag --enable-gpl])
1371 licensewarn="${licensewarn}"'****************************************************************************
1372 Please note that CVC4 will be built against the following GPLed libraries:
1374 As these libraries are covered under the GPLv3, so is this build of CVC4.
1375 CVC4 is also available to you under the terms of the (modified) BSD license.
1376 If you prefer to license CVC4 under those terms, please configure with the
1377 option "--bsd", which will disable all optional GPLed library dependences.
1378 ****************************************************************************
1381 license="GPLv3 (due to optional libraries; see below)"
1383 licensewarn="${licensewarn}Please note that this configuration is NOT built against any GPL'ed
1384 libraries, so it is covered by the (modified) BSD license. This is,
1385 however, not the best-performing configuration of CVC4. To build
1386 against GPL'ed libraries which improve CVC4's performance, re-configure
1387 with '--best --enable-gpl'.
1390 license="modified BSD"
1393 if test "$gpl" = yes; then isgpl=1; else isgpl=0; fi
1394 AC_DEFINE_UNQUOTED(CVC4_GPL_DEPS, $isgpl, [Whether CVC4 is built with the (optional) GPLed library dependences.])
1396 CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="$CVC4_COMPAT_LIBRARY_VERSION"
1397 CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="$CVC4_BINDINGS_LIBRARY_VERSION"
1398 if test "$CVC4_BUILD_LIBCOMPAT" = no; then
1399 CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="N/A"
1401 if test -z "$CVC4_LANGUAGE_BINDINGS"; then
1402 CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="N/A"
1405 bindings_to_be_built=none
1406 if test -n "$CVC4_LANGUAGE_BINDINGS"; then
1407 bindings_to_be_built="$CVC4_LANGUAGE_BINDINGS"
1408 if test -z "$SWIG"; then
1409 bindings_to_be_built="$bindings_to_be_built (for CVC3 compatibility layer only; SWIG not found)"
1413 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/base/tls.h])
1414 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
1415 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
1417 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template])
1418 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5])
1419 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3_template])
1420 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc_template])
1421 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc_template])
1422 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3])
1423 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3])
1431 Build profile: $with_build
1432 Build ID : $build_type
1433 Optimized : $optimized
1434 Debug symbols: $enable_debug_symbols
1435 Proofs : $enable_proof
1436 Statistics : $enable_statistics
1437 Replay : $enable_replay
1438 Assertions : $enable_assertions
1439 Tracing : $enable_tracing
1440 Dumping : $enable_dumping
1441 Muzzle : $enable_muzzle
1443 Unit tests : $support_unit_tests
1444 gcov support : $enable_coverage
1445 gprof support: $enable_profiling
1447 Static libs : $enable_static
1448 Shared libs : $enable_shared
1449 Static binary: $enable_static_binary
1450 Compat lib : $CVC4_BUILD_LIBCOMPAT
1451 Bindings : $bindings_to_be_built
1453 Multithreaded: $support_multithreaded
1454 TLS support : $CVC4_TLS_explanation
1455 Portfolio : $with_portfolio
1457 MP library : $mplibrary
1460 Readline : $with_readline
1462 CPPFLAGS : $CPPFLAGS
1463 CXXFLAGS : $CXXFLAGS
1468 libcvc4 version : $CVC4_LIBRARY_VERSION
1469 libcvc4parser version : $CVC4_PARSER_LIBRARY_VERSION
1470 libcvc4compat version : $CVC4_COMPAT_LIBRARY_VERSION_or_nobuild
1471 libcvc4bindings version: $CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild
1473 Install into : $prefix
1475 CVC4 license : $license
1477 ${licensewarn}Now just type make, followed by make check or make install, as you like.
1481 if test -n "$CVC4_UNSUPPORTED_LANGUAGE_BINDINGS"; then
1483 AC_MSG_WARN([You are electing to build unsupported language binding(s):])
1484 AC_MSG_WARN([ $CVC4_UNSUPPORTED_LANGUAGE_BINDINGS])
1485 AC_MSG_WARN([Please be aware that these bindings may not compile, or])
1486 AC_MSG_WARN([work, and the interface to CVC4 via these bindings may])
1487 AC_MSG_WARN([change drastically in upcoming releases of CVC4.])
1491 if test -n "$CVC4_INTEGRITY_WARNING"; then
1493 AC_MSG_WARN($CVC4_INTEGRITY_WARNING)
1494 AC_MSG_WARN([Please run "make check" after building to ensure integrity of the binary and library])