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, 3) dnl version (minor)
6 m4_define(_CVC4_RELEASE, 1) 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)
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])
20 m4_ifdef([AM_SILENT_RULES],[AM_SILENT_RULES([yes])])
22 CVC4_MAJOR=_CVC4_MAJOR
23 CVC4_MINOR=_CVC4_MINOR
24 CVC4_RELEASE=_CVC4_RELEASE
25 CVC4_EXTRAVERSION=_CVC4_EXTRAVERSION
26 CVC4_RELEASE_STRING=_CVC4_RELEASE_STRING
28 # Libtool version numbers for libraries
29 # Version numbers are in the form current:revision:age
32 # increment if interfaces have been added, removed or changed
34 # increment if source code has changed
35 # set to zero if current is incremented
37 # increment if interfaces have been added
38 # set to zero if interfaces have been removed
41 # For more information, see:
42 # http://www.gnu.org/software/libtool/manual/libtool.html#Versioning
43 # For guidance on when to change the version number, refer to the
46 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])])
48 m4_define(_CVC4_LIBRARY_VERSION, library_version([libcvc4]))dnl
49 m4_define(_CVC4_PARSER_LIBRARY_VERSION, library_version([libcvc4parser]))dnl
50 m4_define(_CVC4_COMPAT_LIBRARY_VERSION, library_version([libcvc4compat]))dnl
51 m4_define(_CVC4_BINDINGS_LIBRARY_VERSION, library_version([libcvc4bindings]))dnl
53 m4_define([fatal_error], [m4_errprint(__program__:__file__:__line__[: fatal error: $*
56 m4_ifblank(_CVC4_LIBRARY_VERSION,[fatal_error([no CVC4_LIBRARY_VERSION defined for release version "]_CVC4_RELEASE_STRING[" in library_versions file])])dnl
57 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
58 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
59 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
61 CVC4_LIBRARY_VERSION=_CVC4_LIBRARY_VERSION
62 CVC4_PARSER_LIBRARY_VERSION=_CVC4_PARSER_LIBRARY_VERSION
63 CVC4_COMPAT_LIBRARY_VERSION=_CVC4_COMPAT_LIBRARY_VERSION
64 CVC4_BINDINGS_LIBRARY_VERSION=_CVC4_BINDINGS_LIBRARY_VERSION
66 # Using the AC_CANONICAL_* macros destroy the command line you get
67 # from $@, which we want later for determining the build profile. So
68 # we save it. (We can't do our build profile stuff here, or it's not
69 # included in the output... autoconf overrides us on the orderings of
72 cvc4_config_cmdline="${config_cmdline[[@]]}"
74 # remember if the user set these explicitly (or whether autoconf does)
75 user_specified_enable_or_disable_static=${enable_static+yes}
76 user_specified_enable_or_disable_shared=${enable_shared+yes}
78 if test -e src/include/cvc4_public.h; then
79 CVC4_CONFIGURE_AT_TOP_LEVEL=yes
81 CVC4_CONFIGURE_AT_TOP_LEVEL=no
84 # override autoconf: we don't want it giving us CFLAGS/CXXFLAGS, but we do
85 # want to respect the user's flags
86 if test -z "${CFLAGS+set}"; then CFLAGS=; fi
87 if test -z "${CXXFLAGS+set}"; then CXXFLAGS=; fi
90 AM_MAINTAINER_MODE([enable])
92 # turn off static lib building by default
102 if test "$enable_shared" = no -a "$user_specified_enable_or_disable_shared" = yes; then
106 # Features requested by the user
107 AC_MSG_CHECKING([for requested build profile])
109 [AS_HELP_STRING([--with-build=profile],
110 [for profile in {production,debug,default,competition,personal}])])
112 if test -z "${with_build+set}" -o "$with_build" = default; then
115 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}"; then
116 custom_build_profile=no
118 custom_build_profile=yes
121 if test -n "${enable_optimized+set}"; then
122 if test "$enable_optimized" = yes; then
123 btargs="$btargs optimized"
125 btargs="$btargs nooptimized"
128 if test -n "${enable_static_binary+set}"; then
129 if test "$enable_static_binary" = yes; then
130 btargs="$btargs staticbinary"
132 btargs="$btargs nostaticbinary"
135 if test -n "${enable_debug_symbols+set}"; then
136 if test "$enable_debug_symbols" = yes; then
137 btargs="$btargs debugsymbols"
139 btargs="$btargs nodebugsymbols"
142 if test -n "${enable_assertions+set}"; then
143 if test "$enable_assertions" = yes; then
144 btargs="$btargs assertions"
146 btargs="$btargs noassertions"
149 if test -n "${enable_proof+set}"; then
150 if test "$enable_proof" = yes; then
151 btargs="$btargs proof"
153 btargs="$btargs noproof"
156 if test -n "${enable_tracing+set}"; then
157 if test "$enable_tracing" = yes; then
158 btargs="$btargs tracing"
160 btargs="$btargs notracing"
163 if test -n "${enable_dumping+set}"; then
164 if test "$enable_dumping" = yes; then
165 btargs="$btargs dumping"
167 btargs="$btargs nodumping"
170 if test -n "${enable_muzzle+set}"; then
171 if test "$enable_muzzle" = yes; then
172 btargs="$btargs muzzle"
174 btargs="$btargs nomuzzle"
177 if test -n "${enable_coverage+set}"; then
178 if test "$enable_coverage" = yes; then
179 btargs="$btargs coverage"
181 btargs="$btargs nocoverage"
184 if test -n "${enable_profiling+set}"; then
185 if test "$enable_profiling" = yes; then
186 btargs="$btargs profiling"
188 btargs="$btargs noprofiling"
191 if test -n "${enable_statistics+set}"; then
192 if test "$enable_statistics" = yes; then
193 btargs="$btargs statistics"
195 btargs="$btargs nostatistics"
198 if test -n "${enable_replay+set}"; then
199 if test "$enable_replay" = yes; then
200 btargs="$btargs replay"
202 btargs="$btargs noreplay"
205 if test -n "${with_glpk+set}"; then
206 if test "$with_glpk" = yes; then
207 btargs="$btargs glpk"
210 AC_MSG_RESULT([$with_build])
212 AM_INIT_AUTOMAKE([1.11 no-define tar-pax parallel-tests color-tests subdir-objects])
213 AC_CONFIG_HEADERS([cvc4autoconfig.h])
215 # automake 1.12 changes the test driver mechanism in a way that is
216 # completely incompatible with 1.11. We figure out here which version
217 # we're using in order to set up test makefiles correctly.
218 # See http://lists.gnu.org/archive/html/automake/2012-04/msg00060.html
219 if test -z "$am__api_version"; then
220 AC_MSG_ERROR([Cannot determine automake API version ?!])
222 case "$am__api_version" in
223 1.11*) automake111=true ;;
224 *) automake111=false ;;
226 AM_CONDITIONAL([AUTOMAKE_1_11], [$automake111])
228 # Initialize libtool's configuration options.
229 # we're not DLL-clean yet (i.e., don't properly use dllexport and dllimport)
230 # _LT_SET_OPTION([LT_INIT],[win32-dll])
233 # Checks for programs.
240 # [chris 8/24/2010] The user *must* specify --with-cln to get CLN
241 # (and, thus, opt in to the GPL dependency).
250 [use CLN instead of GMP]
252 [if test "$withval" != no; then
258 # [chris 8/24/2010] --with-gmp has no practical effect, since GMP is
259 # the default. Could be useful if other options are added later.
265 [use GMP instead of CLN (default)]
267 [if test "$withval" = no; then
268 if test $cvc4_use_cln = 0; then
269 AC_MSG_ERROR([You must use either CLN and GMP. Please pick one.])
277 if test $cvc4_use_cln = 1 && test $cvc4_use_gmp = 1; then
279 AC_MSG_ERROR([You cannot use both CLN and GMP. Please pick one.])
282 # try GMP, fail if not found; GMP is required for both CLN and for GMP
284 AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP (libgmp) not found, see http://gmplib.org/])])
286 if test $cvc4_use_cln = 1; then
287 # [mdeters] The PKG_CHECK_MODULES macro isn't customizable and doesn't fail
288 # gracefully. You can only specify it once for a given library name. That
289 # is, even on separate if/else branches, you can't put
290 # PKG_CHECK_MODULES([CLN], ...). That's why things are so convoluted here,
291 # we have to have PKG_CHECK_MODULES _exactly_ once in configure.ac !
292 PKG_CHECK_MODULES([CLN], [cln >= 1.2.2],
295 AC_LINK_IFELSE([AC_LANG_PROGRAM([[#include <cln/cln.h>]], [[cln::cl_F pi = "3.1415926";]])])
298 [if test $cvc4_use_cln = 0; then
300 AC_MSG_NOTICE([CLN not installed (or too old) or pkgconfig missing, will use gmp])
303 AC_MSG_ERROR([CLN not installed (or too old) or pkgconfig missing])
308 if test $cvc4_use_cln = 0; then
309 # try GMPXX, fail if not found
310 AC_CHECK_LIB(gmpxx, __gmpz_init, , [AC_MSG_ERROR([GNU MP C++ library (libgmpxx) not found, see http://gmplib.org/])])
313 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }$CLN_CFLAGS"
314 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }$CLN_CFLAGS"
315 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }$CLN_CFLAGS"
316 LIBS="$CLN_LIBS${LIBS:+ $LIBS}"
320 if test $cvc4_cln_or_gmp = cln; then
321 AC_DEFINE_UNQUOTED(CVC4_CLN_IMP, [], [Defined if using the CLN multi-precision arithmetic library.])
323 AC_DEFINE_UNQUOTED(CVC4_GMP_IMP, [], [Defined if using the GMP multi-precision arithmetic library.])
325 AM_CONDITIONAL([CVC4_CLN_IMP], [test $cvc4_cln_or_gmp = cln])
326 AM_CONDITIONAL([CVC4_GMP_IMP], [test $cvc4_cln_or_gmp = gmp])
328 # construct the build string
329 AC_MSG_CHECKING([for appropriate build string])
330 if test -z "$ac_confdir"; then
333 build_type=`$ac_confdir/config/build-type $with_build $btargs $cvc4_cln_or_gmp`
334 if test "$custom_build_profile" = yes; then
335 if test "$with_build" = default; then
336 build_type=`$ac_confdir/config/build-type custom $btargs $cvc4_cln_or_gmp`
339 AC_MSG_RESULT($build_type)
341 # Require building in target and build-specific build directory:
343 # If the configure script is invoked from the top-level source
344 # directory, it creates a suitable build directory (based on the build
345 # architecture and build profile from $build_type), changes into it,
346 # and reinvokes itself. CVC4_CONFIGURE_IN_BUILDS is an envariable
347 # that breaks any possibility of infinite recursion in this process.
348 AC_MSG_CHECKING([what dir to configure])
349 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
350 AC_MSG_RESULT([this one (in builds/)])
351 elif test "$CVC4_CONFIGURE_AT_TOP_LEVEL" = yes; then
352 AC_MSG_RESULT([builds/$target/$build_type])
354 if test -z "$ac_srcdir"; then
355 mkbuilddir=./config/mkbuilddir
357 mkbuilddir=$ac_srcdir/config/mkbuilddir
359 $as_echo "$mkbuilddir $target $build_type"
360 source $mkbuilddir "$target" "$build_type"
361 $as_echo "cd builds/$target/$build_type"
362 cd "builds/$target/$build_type"
363 CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS
364 echo "$SHELL ../../../configure ${config_cmdline[[@]]}"
365 "$SHELL" "`pwd`/../../../configure" "${config_cmdline[[@]]}"
368 if test $exitval -eq 0; then
369 cat >config.reconfig <<EOF
371 # Generated by configure, `date`
372 # This script is part of CVC4.
374 cd "\`dirname \\"\$0\\"\`"
376 if test -d builds; then :; else echo 'No builds/ directory!' >&2; exit; fi
378 current=(\`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]*\\)/\\(.*\\),\\1 \\2,'\`)
382 echo "reconfiguring in builds/\$arch/\$build..."
383 cd "builds/\$arch/\$build"
384 echo ./config.status "\$@"
385 ./config.status "\$@"]
387 chmod +x config.reconfig
389 ln -sf "$target/$build_type/config.log" "builds/config.log"
392 AC_MSG_RESULT([this one (user-specified)])
397 # Unpack standard build types. Any particular options can be overriden with
398 # --enable/disable-X options
399 case "$with_build" in
400 production) # highly optimized, no assertions, no tracing, dumping
405 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
406 if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=3 ; fi
407 if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
408 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
409 if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
410 if test -z "${enable_replay+set}" ; then enable_replay=no ; fi
411 if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi
412 if test -z "${enable_proof+set}" ; then enable_proof=no ; fi
413 if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi
414 if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
415 if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
417 debug) # unoptimized, debug symbols, assertions, tracing, dumping
418 CVC4CPPFLAGS='-DCVC4_DEBUG'
419 CVC4CXXFLAGS='-fno-inline'
420 CVC4CFLAGS='-fno-inline'
422 FLAG_VISIBILITY_HIDDEN=
423 if test -z "${enable_optimized+set}" ; then enable_optimized=no ; fi
424 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
425 if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
426 if test -z "${enable_replay+set}" ; then enable_replay=yes ; fi
427 if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi
428 if test -z "${enable_proof+set}" ; then enable_proof=no ; fi
429 if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi
430 if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
431 if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
433 default) # moderately optimized, assertions, tracing, dumping
438 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
439 if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=2 ; fi
440 if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
441 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
442 if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
443 if test -z "${enable_replay+set}" ; then enable_replay=yes ; fi
444 if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi
445 if test -z "${enable_proof+set}" ; then enable_proof=no ; fi
446 if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi
447 if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
448 if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
450 competition) # maximally optimized, no assertions, no tracing, no dumping, muzzled
451 CVC4CPPFLAGS='-DCVC4_COMPETITION_MODE'
452 CVC4CXXFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
453 CVC4CFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
455 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
456 if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=9 ; fi
457 if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
458 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no ; fi
459 if test -z "${enable_statistics+set}" ; then enable_statistics=no ; fi
460 if test -z "${enable_replay+set}" ; then enable_replay=no ; fi
461 if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi
462 if test -z "${enable_proof+set}" ; then enable_proof=no ; fi
463 if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi
464 if test -z "${enable_dumping+set}" ; then enable_dumping=no ; fi
465 if test -z "${enable_muzzle+set}" ; then enable_muzzle=yes ; fi
466 if test -z "${user_specified_enable_or_disable_shared}"; then enable_shared=no; fi
467 if test -z "${user_specified_enable_or_disable_static}"; then enable_static=yes; fi
468 if test -z "${enable_static_binary+set}"; then enable_static_binary=yes ; fi
471 AC_MSG_FAILURE([unknown build profile: $with_build])
474 if test -z "${OPTLEVEL+set}"; then OPTLEVEL=3; fi
476 AM_CONDITIONAL([CVC4_BUILD_PROFILE_PRODUCTION], [test "$with_build" = production])
477 AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEBUG], [test "$with_build" = debug])
478 AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEFAULT], [test "$with_build" = default])
479 AM_CONDITIONAL([CVC4_BUILD_PROFILE_COMPETITION], [test "$with_build" = competition])
481 # permit a static binary
482 AC_MSG_CHECKING([whether to build a static binary])
483 AC_ARG_ENABLE([static-binary],
484 [AS_HELP_STRING([--enable-static-binary],
485 [build a fully statically-linked binary [default=no]])])
486 if test -z "${enable_static_binary+set}"; then
487 enable_static_binary=no
489 AC_MSG_RESULT([$enable_static_binary])
490 if test "$enable_static_binary" = yes; then
491 if test "$target_vendor" = apple; then
492 if test -z "$MAC_STATIC_BINARY_MANUAL_OVERRIDE"; then
493 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)]])
495 AC_MSG_WARN([MAC_STATIC_BINARY_MANUAL_OVERRIDE was set!])
496 AC_MSG_WARN([Will make a static binary during this build. Note that it may fail!])
499 if test "$enable_static" != yes; then
501 AC_MSG_WARN([forcing static-library building, --enable-static-binary given])
505 AC_MSG_CHECKING([whether to support proofs in libcvc4])
507 AC_ARG_ENABLE([proof],
508 [AS_HELP_STRING([--enable-proof],
509 [support proof generation])])
510 if test -z "${enable_proof+set}"; then
513 AC_MSG_RESULT([$enable_proof])
515 if test "$enable_proof" = yes; then
516 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROOF"
519 AC_MSG_CHECKING([whether to optimize libcvc4])
521 AC_ARG_ENABLE([optimized],
522 [AS_HELP_STRING([--enable-optimized],
523 [optimize the build])])
525 if test -z "${enable_optimized+set}"; then
529 AC_MSG_RESULT([$enable_optimized])
531 if test "$enable_optimized" = yes; then
532 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O$OPTLEVEL"
533 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O$OPTLEVEL"
535 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O0"
536 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O0"
539 AC_MSG_CHECKING([whether to include debugging symbols in libcvc4])
541 AC_ARG_ENABLE([debug-symbols],
542 [AS_HELP_STRING([--disable-debug-symbols],
543 [do not include debug symbols in libcvc4])])
545 if test -z "${enable_debug_symbols+set}"; then
546 enable_debug_symbols=yes
549 AC_MSG_RESULT([$enable_debug_symbols])
551 if test "$enable_debug_symbols" = yes; then
552 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-ggdb3"
553 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-ggdb3"
556 AC_MSG_CHECKING([whether to include statistics are turned on in libcvc4])
558 AC_ARG_ENABLE([statistics],
559 [AS_HELP_STRING([--disable-statistics],
560 [do not include statistics in libcvc4])])
562 if test -z "${enable_statistics+set}"; then
563 enable_statistics=yes
566 AC_MSG_RESULT([$enable_statistics])
568 if test "$enable_statistics" = yes; then
569 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_STATISTICS_ON"
572 AC_MSG_CHECKING([whether the replay feature should be turned on in libcvc4])
574 AC_ARG_ENABLE([replay],
575 [AS_HELP_STRING([--disable-replay],
576 [turn off the replay feature in libcvc4])])
578 if test -z "${enable_replay+set}"; then
582 AC_MSG_RESULT([$enable_replay])
584 if test "$enable_replay" = yes; then
585 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_REPLAY"
588 AC_MSG_CHECKING([whether to include assertions in build])
590 AC_ARG_ENABLE([assertions],
591 [AS_HELP_STRING([--disable-assertions],
592 [turn off assertions in build])])
594 if test -z "${enable_assertions+set}"; then
595 enable_assertions=yes
598 AC_MSG_RESULT([$enable_assertions])
600 if test "$enable_assertions" = yes; then
601 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_ASSERTIONS"
603 # turn off regular C assert() also
604 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DNDEBUG"
607 AC_MSG_CHECKING([whether to do a traceable build of CVC4])
608 AC_ARG_ENABLE([tracing],
609 [AS_HELP_STRING([--disable-tracing],
610 [remove all tracing code from CVC4])])
612 if test -z "${enable_tracing+set}"; then
616 AC_MSG_RESULT([$enable_tracing])
618 if test "$enable_tracing" = yes; then
619 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_TRACING"
622 AC_MSG_CHECKING([whether to do a dump-capable build of CVC4])
623 AC_ARG_ENABLE([dumping],
624 [AS_HELP_STRING([--disable-dumping],
625 [remove all dumping code from CVC4])])
627 if test -z "${enable_dumping+set}"; then
631 AC_MSG_RESULT([$enable_dumping])
633 if test "$enable_dumping" = yes; then
634 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DUMPING"
637 AC_MSG_CHECKING([whether to do a muzzled build of CVC4])
638 AC_ARG_ENABLE([muzzle],
639 [AS_HELP_STRING([--enable-muzzle],
640 [completely silence CVC4; remove ALL non-result output from build])])
642 if test -z "${enable_muzzle+set}"; then
646 AC_MSG_RESULT([$enable_muzzle])
648 if test "$enable_muzzle" = yes; then
649 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_MUZZLE"
652 AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4])
653 AC_ARG_ENABLE([coverage],
654 [AS_HELP_STRING([--enable-coverage],
655 [build with support for gcov coverage testing])])
657 if test -z "${enable_coverage+set}"; then
661 AC_MSG_RESULT([$enable_coverage])
663 if test "$enable_coverage" = yes; then
664 # For coverage testing, we prefer:
665 # --enable-static --disable-shared --disable-static-binary
666 # If the user didn't specify these, we force them here. If the
667 # user specified them in opposite phase, give warnings that they
668 # shouldn't do that, or bomb out.
669 if test "$user_specified_enable_or_disable_shared" != yes; then
671 AC_MSG_WARN([turning off shared library building due to --enable-coverage])
672 elif test "$enable_shared" = yes; then
674 AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-shared])
675 AC_MSG_WARN([gcov does not support shared libraries, so only your static libraries will be coverage-testable.])
676 AC_MSG_WARN([Your cvc4 driver and testing binaries will not be coverage-testable.])
679 if test "${enable_static_binary+set}" = set -a "$enable_static_binary" = yes; then
681 AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-static-binary])
682 AC_MSG_WARN([Your cvc4 driver and testing binaries will be fully-statically linked and may not be coverage-testable.])
685 if test "$user_specified_enable_or_disable_static" != yes; then
687 AC_MSG_WARN([turning on static library building due to --enable-coverage])
688 elif test "$enable_static" != yes; then
689 AC_MSG_ERROR([--enable-coverage and --disable-static are incompatible; gcov only supports static libraries.])
692 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COVERAGE"
693 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }--coverage"
694 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }--coverage"
695 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }--coverage"
698 AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4])
700 AC_ARG_ENABLE([profiling],
701 [AS_HELP_STRING([--enable-profiling],
702 [build with support for gprof profiling])])
704 if test -z "${enable_profiling+set}"; then
708 AC_MSG_RESULT([$enable_profiling])
710 if test "$enable_profiling" = yes; then
711 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROFILING"
712 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-pg"
713 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-pg"
714 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }-pg"
717 # Check for libglpk (defined in config/glpk.m4)
719 [AS_HELP_STRING([--with-glpk],
720 [use GLPK simplex solver])], [], [with_glpk=])
722 if test $have_libglpk -eq 1; then
723 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_GLPK"
725 AM_CONDITIONAL([CVC4_USE_GLPK], [test $have_libglpk -eq 1])
726 AC_SUBST([GLPK_LIBS])
728 # Check to see if this version/architecture of GNU C++ explicitly
729 # instantiates __gnu_cxx::hash<uint64_t> or not. Some do, some don't.
730 # See src/util/hash.h.
731 AC_MSG_CHECKING([whether __gnu_cxx::hash<uint64_t> is already specialized])
733 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
735 #include <ext/hash_map>
736 namespace __gnu_cxx { template<> struct hash<uint64_t> {}; }])],
737 [AC_MSG_RESULT([no]); CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_NEED_HASH_UINT64_T"],
738 [AC_MSG_RESULT([yes])])
741 # Check whether "long" and "int64_t" are distinct types w.r.t. overloading.
742 # Even if they have the same size, they can be distinct, and some platforms
743 # can have problems with ambiguous function calls when auto-converting
744 # int64_t to long, and others will complain if you overload a function
745 # that takes an int64_t with one that takes a long (giving a redefinition
746 # error). So we have to keep both happy. Probably the same underlying
747 # issue as the hash specialization above, but let's check separately
749 AC_MSG_CHECKING([for the relationship between long and int64_t])
751 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
754 void foo(int64_t) {}])],
755 [AC_MSG_RESULT([no relationship detected]); CVC4_NEED_INT64_T_OVERLOADS=1],
756 [AC_MSG_RESULT([typedef or similar]); CVC4_NEED_INT64_T_OVERLOADS=0])
758 AC_SUBST([CVC4_NEED_INT64_T_OVERLOADS])
760 AC_MSG_CHECKING([for the pb_ds namespace])
762 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
763 #include <ext/pb_ds/priority_queue.hpp>
764 typedef pb_ds::priority_queue<void, void, void> pq;])],
765 [CVC4_PB_DS_NAMESPACE=pb_ds],
766 [AC_COMPILE_IFELSE([AC_LANG_SOURCE([
767 #include <ext/pb_ds/priority_queue.hpp>
768 typedef __gnu_pbds::priority_queue<void, void, void> pq;])],
769 [CVC4_PB_DS_NAMESPACE=__gnu_pbds],
770 [AC_MSG_ERROR([cannot find required priority_queue in either __gnu_pbds or pb_ds namespace.
772 If you're using a non-GCC compiler (such as clang), you may need to explicitly
773 use the GNU standard C++ library by passing:
774 CXXFLAGS='-stdlib=libstdc++' CPPFLAGS='-stdlib=libstdc++'
775 as arguments to this configure script.
776 This is the case on Mac OS Mavericks, for example.])])])
778 AC_MSG_RESULT([$CVC4_PB_DS_NAMESPACE])
779 AC_DEFINE_UNQUOTED(CVC4_PB_DS_NAMESPACE, ${CVC4_PB_DS_NAMESPACE}, [The namespace for pb_ds data structures.])
781 # for information: http://gcc.gnu.org/bugzilla/show_bug.cgi?id=36612
782 AC_MSG_CHECKING([whether pb_ds has bug 36612])
784 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
785 #define __throw_container_error inline __throw_container_error
786 #define __throw_insert_error inline __throw_insert_error
787 #define __throw_join_error inline __throw_join_error
788 #define __throw_resize_error inline __throw_resize_error
789 #include <ext/pb_ds/exception.hpp>
791 [CVC4_GCC_HAS_PB_DS_BUG=1; bugverb=is],
792 [CVC4_GCC_HAS_PB_DS_BUG=0; bugverb="is not"])
794 AC_MSG_RESULT([bug $bugverb present])
795 AC_DEFINE_UNQUOTED(CVC4_GCC_HAS_PB_DS_BUG, ${CVC4_GCC_HAS_PB_DS_BUG}, [Whether libstdc++ has a certain bug; see http://gcc.gnu.org/bugzilla/show_bug.cgi?id=36612])
797 # Check for ANTLR runantlr script (defined in config/antlr.m4)
800 CVC4_CXX_OPTION([-Werror], [WERROR])
801 CVC4_C_OPTION([-Werror], [C_WERROR])
802 CVC4_CXX_OPTION([-Wno-deprecated], [WNO_DEPRECATED])
803 CVC4_C_OPTION([-Wno-deprecated], [C_WNO_DEPRECATED])
804 CVC4_CXX_OPTION([-Wno-conversion-null], [WNO_CONVERSION_NULL])
805 CVC4_CXX_OPTION([-Wno-tautological-compare], [WNO_TAUTOLOGICAL_COMPARE])
806 CVC4_CXX_OPTION([-Wno-parentheses], [WNO_PARENTHESES])
807 CVC4_CXX_OPTION([-Wno-uninitialized], [WNO_UNINITIALIZED])
808 CVC4_CXX_OPTION([-Wno-unused-variable], [WNO_UNUSED_VARIABLE])
809 CVC4_CXX_OPTION([-fno-strict-aliasing], [FNO_STRICT_ALIASING])
811 AC_SUBST([WNO_CONVERSION_NULL])
812 AC_SUBST([WNO_TAUTOLOGICAL_COMPARE])
813 AC_SUBST([WNO_PARENTHESES])
814 AC_SUBST([WNO_UNINITIALIZED])
815 AC_SUBST([WNO_UNUSED_VARIABLE])
816 AC_SUBST([FNO_STRICT_ALIASING])
818 # On Mac, we have to fix the visibility of standard library symbols.
819 # Otherwise, exported template instantiations---even though explicitly
820 # CVC4_PUBLIC, can be generated as symbols with internal-only linkage.
821 # Presumably, Apple is distributing a libstdc++ that is built *without*
822 # --enable-libstdcxx-visibility (?)
823 if test "$target_vendor" = apple; then
824 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-D_GLIBCXX_VISIBILITY_DEFAULT=\"__attribute__((__visibility__(\\\"default\\\")))\""
827 # Tell top-level Makefile to include $(top_srcdir)/personal.mk
828 AC_ARG_ENABLE([personal-make-rules],
829 [AS_HELP_STRING([--enable-personal-make-rules],
830 [include top-level personal.mk (if it exists)])])
831 if test "$enable_personal_make_rules" = yes; then
832 # This allows us to include a personal.mk makefile from every
833 # generated makefile. Named zz_* in order to make sure this
834 # comes last, so it gets other definitions (in particular top_srcdir).
835 zz_cvc4_use_personal_make_rules='yes
837 include $(top_srcdir)/personal.mk
838 $(top_srcdir)/personal.mk:; @touch "$@"'
839 AC_SUBST([zz_cvc4_use_personal_make_rules])
842 # Doxygen configuration
843 AC_ARG_ENABLE([internals-documentation],
844 [AS_HELP_STRING([--enable-internals-documentation],
845 [build Doxygen documentation for static and private member functions])])
846 if test "$enable_internals_documentation" = yes; then
847 DOXYGEN_EXTRACT_PRIVATE=YES
848 DOXYGEN_EXTRACT_STATIC=YES
850 DOXYGEN_EXTRACT_PRIVATE=NO
851 DOXYGEN_EXTRACT_STATIC=NO
853 AC_SUBST([DOXYGEN_EXTRACT_PRIVATE])
854 AC_SUBST([DOXYGEN_EXTRACT_STATIC])
860 DX_INIT_DOXYGEN($PACKAGE_NAME, config/doxygen.cfg, $srcdir/doc/doxygen)
862 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])
863 AC_ARG_VAR(CXXTEST, [path to CxxTest installation])
867 AC_ARG_WITH([cxxtest-dir],
868 [AS_HELP_STRING([--with-cxxtest-dir=DIR], [path to CxxTest installation])],
869 [CXXTEST="$withval"])
871 # In the case of "./configure --with-cxxtest-dir=../cxxtest" (or other
872 # relative path) and having switched the configure directory (see above),
873 # search with respect to the top source dir, not the build dir
874 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes -a -n "$CXXTEST"; then
877 *) CXXTEST="$srcdir/$CXXTEST" ;;
881 AC_ARG_VAR(LFSC, [path to LFSC proof checker])
882 AC_ARG_VAR(LFSCARGS, [arguments to pass to LFSC proof checker])
883 if test -z "$LFSC"; then
884 AC_CHECK_PROGS(LFSC, lfsc, [], [])
886 AC_CHECK_PROG(LFSC, "$LFSC", [], [])
888 AM_CONDITIONAL([PROOF_REGRESSIONS], [test -n "$LFSC" -a "$enable_proof" = yes])
889 if test -n "$LFSC" -a "$enable_proof" = yes; then
890 TESTS_ENVIRONMENT="${TESTS_ENVIRONMENT:+$TESTS_ENVIRONMENT }LFSC=\"$LFSC $LFSCARGS\""
891 RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--proof"
893 AC_SUBST([TESTS_ENVIRONMENT])
894 AC_SUBST([RUN_REGRESSION_ARGS])
895 if test -z "$LFSC"; then
896 support_proof_tests='no, lfsc proof checker unavailable'
897 elif test "$enable_proof" = yes; then
898 support_proof_tests='yes, proof regression tests enabled'
900 support_proof_tests='no, proof generation disabled for this build'
906 AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH])
907 if test -z "$CXXTESTGEN"; then
908 AC_PATH_PROG(CXXTESTGEN, cxxtestgen.py, [], [$CXXTEST:$PATH])
910 if test -z "$CXXTESTGEN"; then
911 AC_PATH_PROG(CXXTESTGEN, cxxtestgen, [], [$CXXTEST:$PATH])
913 if test "$enable_unit_testing" = "no"; then
914 AC_MSG_NOTICE([unit tests disabled by user request.])
917 elif test -z "$CXXTESTGEN"; then
918 AC_MSG_NOTICE([unit tests disabled, could not find cxxtestgen.pl or cxxtestgen.py or cxxtestgen])
919 elif test -z "$CXXTEST"; then
920 CXXTEST=`dirname "$CXXTESTGEN"`
921 AC_MSG_CHECKING([for location of CxxTest headers])
922 if test -e "$CXXTEST/cxxtest/TestRunner.h"; then
923 AC_MSG_RESULT([$CXXTEST])
925 if test -e "/usr/include/cxxtest/TestRunner.h"; then
926 AC_MSG_RESULT([/usr/include])
928 AC_MSG_RESULT([not found])
929 AC_MSG_WARN([unit tests disabled, CxxTest headers not found.])
936 if test "$enable_unit_testing" = yes -a -z "$CXXTESTGEN"; then
937 AC_MSG_ERROR([--enable-unit-testing given but cxxtest not found.])
940 AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"])
942 AC_ARG_VAR(TEST_CPPFLAGS, [CPPFLAGS to use when testing (default=$CPPFLAGS)])
943 AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)])
944 AC_ARG_VAR(TEST_LDFLAGS, [LDFLAGS to use when testing (default=$LDFLAGS)])
946 AC_ARG_VAR(PERL, [PERL interpreter (used when testing)])
948 if test -n "$CXXTEST"; then
949 if test -z "$PERL"; then
950 AC_CHECK_PROGS(PERL, perl, perl, [])
952 AC_CHECK_PROG(PERL, "$PERL", "$PERL", [])
955 if test -z "$PERL"; then
956 AC_MSG_WARN([unit tests disabled, perl not found.])
962 AC_ARG_VAR(PYTHON, [PYTHON interpreter (used for building legacy Java library interface)])
964 if test -z "$PYTHON"; then
965 AC_CHECK_PROGS(PYTHON, python, python, [])
967 AC_CHECK_PROG(PYTHON, "$PYTHON", "$PYTHON", [])
970 if test -z "$PYTHON"; then
971 AC_MSG_WARN([python not found, cannot build libcvc4compat_java (the legacy Java interface).])
976 # Checks for libraries.
978 AC_SEARCH_LIBS([clock_gettime], [rt],
979 [AC_DEFINE([HAVE_CLOCK_GETTIME], [1],
980 [Defined to 1 if clock_gettime() is supported by the platform.])],
981 [AC_LIBOBJ([clock_gettime])])
982 AC_CHECK_FUNC([strtok_r], [AC_DEFINE([HAVE_STRTOK_R], [1],
983 [Defined to 1 if strtok_r() is supported by the platform.])],
984 [AC_LIBOBJ([strtok_r])])
985 AC_CHECK_FUNC([ffs], [AC_DEFINE([HAVE_FFS], [1],
986 [Defined to 1 if ffs() is supported by the platform.])],
989 # Check for antlr C++ runtime (defined in config/antlr.m4)
992 # Check for user preferences for language bindings to build, and for
993 # build support. The arg list is the default set if unspecified by
994 # the user (the actual built set is the subset that appears to be
995 # supported by the build host).
996 CVC4_CHECK_BINDINGS([c java])dnl csharp perl php python ruby tcl ocaml])
998 # Checks for header files and their contents.
999 AC_CHECK_HEADERS([getopt.h unistd.h])
1001 # Checks for typedefs, structures, and compiler characteristics.
1003 # these are bad macros, they clash with system header <stdint.h> !!
1009 # guard against double-inclusion of the autoheader
1010 AH_TOP([#ifndef __CVC4__CVC4AUTOCONFIG_H
1011 #define __CVC4__CVC4AUTOCONFIG_H])
1012 AH_BOTTOM([#endif /* __CVC4__CVC4AUTOCONFIG_H */])
1014 AC_CHECK_DECLS([optreset], [], [], [#include <getopt.h>])
1016 # check with which standard strerror_r() complies
1019 # require boost library
1022 # look for boost threading library
1023 AC_ARG_WITH([portfolio],
1024 AS_HELP_STRING([--with-portfolio], [build the multithreaded portfolio version of CVC4 (pcvc4)]))
1025 cvc4_save_LDFLAGS="$LDFLAGS"
1026 if test "$enable_static_binary" = yes; then
1027 LDFLAGS="-static $LDFLAGS"
1029 cvc4_has_threads=yes
1030 AC_ARG_ENABLE([thread-support],
1031 AS_HELP_STRING([--disable-thread-support], [do not support multithreaded-capable library]))
1032 if test "$enable_thread_support" = no; then
1034 if test "$with_portfolio" = yes; then
1035 AC_MSG_ERROR([user gave both --with-portfolio and --disable-thread-support, which are contradictory])
1038 BOOST_THREADS([], [AC_MSG_WARN([disabling multithreaded support])
1039 cvc4_has_threads=no])
1041 LDFLAGS="$cvc4_save_LDFLAGS"
1042 if test $cvc4_has_threads = no; then
1043 if test "$enable_thread_support" = yes; then
1044 AC_MSG_ERROR([user gave --enable-thread-support but could not build with threads; maybe boost threading library is missing?])
1046 if test "$with_portfolio" = yes; then
1047 AC_MSG_ERROR([user gave --with-portfolio but could not build with threads; maybe boost threading library is missing?])
1051 if test "$with_portfolio" != yes; then
1054 AM_CONDITIONAL([CVC4_BUILD_PCVC4], [test "$with_portfolio" = yes])
1055 if test "$with_portfolio" = yes; then
1056 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PORTFOLIO"
1059 # Check for libreadline (defined in config/readline.m4)
1060 AC_ARG_WITH([readline], [AS_HELP_STRING([--with-readline], [support the readline library])], [], [with_readline=check])
1061 # make the flags as close as possible to the final flags, because the Boost
1062 # flags can bring in a different, incompatible readline library than we'd
1063 # get otherwise (e.g. on Mac, where there are commonly two different readlines,
1064 # one in /usr and one in /opt/local)
1065 cvc4_rlcheck_save_CPPFLAGS="$CPPFLAGS"
1066 cvc4_rlcheck_save_CXXFLAGS="$CXXFLAGS"
1067 cvc4_rlcheck_save_CFLAGS="$CFLAGS"
1068 cvc4_rlcheck_save_LDFLAGS="$LDFLAGS"
1069 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
1070 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS $WNO_DEPRECATED"
1071 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS $C_WNO_DEPRECATED -fexceptions"
1072 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
1073 CVC4_CHECK_FOR_READLINE
1074 CPPFLAGS="$cvc4_rlcheck_save_CPPFLAGS"
1075 CXXFLAGS="$cvc4_rlcheck_save_CXXFLAGS"
1076 CFLAGS="$cvc4_rlcheck_save_CFLAGS"
1077 LDFLAGS="$cvc4_rlcheck_save_LDFLAGS"
1078 AC_DEFINE_UNQUOTED([HAVE_LIBREADLINE], $have_libreadline, [Define to 1 to use libreadline])
1079 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])
1080 AC_SUBST([READLINE_LIBS])
1082 # Whether to build compatibility library
1083 CVC4_BUILD_LIBCOMPAT=yes
1084 AC_ARG_WITH([compat],
1085 AS_HELP_STRING([--with-compat], [build compatibility library (CVC3 API layer)]),
1086 [if test "$withval" = no; then CVC4_BUILD_LIBCOMPAT=no; fi])
1087 AC_MSG_CHECKING([whether to build compatibility library (CVC3 API layer)])
1088 if test "$CVC4_BUILD_LIBCOMPAT" = yes; then
1089 AC_MSG_RESULT([yes])
1091 AC_MSG_RESULT([no, disabled by user])
1093 AC_SUBST(CVC4_BUILD_LIBCOMPAT)
1094 AM_CONDITIONAL([CVC4_BUILD_LIBCOMPAT], [test "$CVC4_BUILD_LIBCOMPAT" = yes])
1096 # Check for availability of TLS support (e.g. __thread storage class)
1097 AC_MSG_CHECKING([whether to use compiler-supported TLS if available])
1098 AC_ARG_ENABLE([tls], AS_HELP_STRING([--disable-tls], [don't use compiler-native TLS]))
1099 if test $cvc4_has_threads = no; then
1100 # We disable TLS entirely by simply telling the build system that
1101 # the empty string is the __thread keyword.
1102 AC_MSG_RESULT([multithreading disabled])
1103 CVC4_TLS_SUPPORTED=1
1105 CVC4_TLS_explanation='disabled (no multithreading support)'
1107 if test -z "${enable_tls+set}" || test "$enable_tls" = "yes"; then
1108 AC_MSG_RESULT([yes])
1109 AX_TLS([CVC4_TLS=$ac_cv_tls], [CVC4_TLS=])
1114 if test -n "$CVC4_TLS"; then
1115 CVC4_TLS_SUPPORTED=1
1116 CVC4_TLS_explanation="$CVC4_TLS"
1118 CVC4_TLS_explanation='pthread_getspecific()'
1119 CVC4_TLS_SUPPORTED=0
1122 AC_SUBST([CVC4_TLS])
1123 AC_SUBST([CVC4_TLS_SUPPORTED])
1125 # Whether to compile with google profiling tools
1126 cvc4_use_google_perftools=0
1130 [--with-google-perftools],
1131 [use Google Performance Tools]
1133 [if test "$withval" != no; then
1134 cvc4_use_google_perftools=1
1138 AC_MSG_CHECKING([whether to link in google perftools libraries])
1139 if test $cvc4_use_google_perftools = 1; then
1140 AC_MSG_RESULT([yes])
1141 AC_CHECK_LIB([tcmalloc], [MallocExtension_GetAllocatedSize], , [AC_MSG_ERROR([cannot link google-perftools test program with -ltcmalloc])], [-lpthread])
1142 AC_CHECK_LIB([profiler], [ProfilerStart], , [AC_MSG_ERROR([cannot link google-perftools test program with -lprofiler])], [-lpthread])
1144 AC_MSG_RESULT([no (user didn't request it)])
1148 AC_ARG_VAR(JAVA, [Java interpreter (used when testing Java interface)])
1149 AC_ARG_VAR(JAVAC, [Java compiler (used when building and testing Java interface)])
1150 AC_ARG_VAR(JAVAH, [Java compiler (used when building and testing Java interface)])
1151 AC_ARG_VAR(JAR, [Jar archiver (used when building Java interface)])
1152 if test "$cvc4_build_java_bindings"; then
1154 if test -z "$JAVA"; then
1155 AC_CHECK_PROGS(JAVA, java, java, [])
1157 AC_CHECK_PROG(JAVA, "$JAVA", "$JAVA", [])
1159 if test -z "$JAVAC"; then
1160 AC_CHECK_PROGS(JAVAC, javac gcj, javac, [])
1161 if test "$JAVAC" = gcj; then JAVAC='gcj -C'; fi
1163 AC_CHECK_PROG(JAVAC, "$JAVAC", "$JAVAC", [])
1165 if test -z "$JAVAH"; then
1166 AC_CHECK_PROGS(JAVAH, javah gcjh, javah, [])
1168 AC_CHECK_PROG(JAVAH, "$JAVAH", "$JAVAH", [])
1170 if test -z "$JAR"; then
1171 AC_CHECK_PROGS(JAR, jar, jar, [])
1173 AC_CHECK_PROG(JAR, "$JAR", "$JAR", [])
1177 # on Mac OS X, Java doesn't like the .so module extension; it wants .dylib
1178 module=no eval CVC4_JAVA_MODULE_EXT="$shrext_cmds"
1179 if test -z "$CVC4_JAVA_MODULE_EXT"; then
1180 CVC4_JAVA_MODULE_EXT=.so
1182 AC_SUBST([CVC4_JAVA_MODULE_EXT])
1184 # Prepare configure output
1186 if test "$enable_shared" = yes; then BUILDING_SHARED=1; else BUILDING_SHARED=0; fi
1187 if test "$enable_static" = yes; then BUILDING_STATIC=1; else BUILDING_STATIC=0; fi
1188 if test "$enable_static_binary" = yes; then STATIC_BINARY=1; else STATIC_BINARY=0; fi
1189 AC_SUBST(BUILDING_SHARED)
1190 AC_SUBST(BUILDING_STATIC)
1191 AC_SUBST(STATIC_BINARY)
1192 AM_CONDITIONAL([STATIC_BINARY], [test "$enable_static_binary" = yes])
1193 AM_CONDITIONAL([COVERAGE_ENABLED], [test "$enable_coverage" = yes])
1195 AM_CONDITIONAL([CVC4_DEBUG], [test "$with_build" = debug])
1196 AM_CONDITIONAL([CVC4_TRACING], [test "$enable_tracing" = yes])
1198 AC_SUBST(CVC4_LIBRARY_VERSION)
1199 AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
1200 AC_SUBST(CVC4_COMPAT_LIBRARY_VERSION)
1201 AC_SUBST(CVC4_BINDINGS_LIBRARY_VERSION)
1203 AC_DEFINE_UNQUOTED(CVC4_MAJOR, ${CVC4_MAJOR}, [Major component of the version of CVC4.])
1204 AC_DEFINE_UNQUOTED(CVC4_MINOR, ${CVC4_MINOR}, [Minor component of the version of CVC4.])
1205 AC_DEFINE_UNQUOTED(CVC4_RELEASE, ${CVC4_RELEASE}, [Release component of the version of CVC4.])
1206 AC_DEFINE_UNQUOTED(CVC4_EXTRAVERSION, ["${CVC4_EXTRAVERSION}"], [Extraversion component of the version of CVC4.])
1207 AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full release string for CVC4.])
1209 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
1210 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
1211 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions"
1212 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
1214 # visibility flag not supported for Windows builds
1215 # also increase default stack size for Windows binaries
1217 (*mingw*) FLAG_VISIBILITY_HIDDEN=
1218 cvc4_LDFLAGS=-Wl,--stack,134217728
1219 pcvc4_LDFLAGS=-Wl,--stack,134217728
1222 AC_SUBST(FLAG_VISIBILITY_HIDDEN)
1223 AC_SUBST(cvc4_LDFLAGS)
1224 AC_SUBST(pcvc4_LDFLAGS)
1226 AM_CONDITIONAL(WHITE_AND_BLACK_TESTS, [test -z "$FLAG_VISIBILITY_HIDDEN"])
1228 # remember the command line used for configure
1229 AC_SUBST(cvc4_config_cmdline)
1233 # When automake scans Makefiles, it complains about non-standard make
1234 # features (including GNU extensions), and breaks GNU Make's
1235 # "if/endif" construct, replacing the "if" with AM_CONDITIONAL if
1236 # constructs. automake even follows "include" and messes with
1237 # included Makefiles.
1239 # CVC4 assumes GNU Make and we want to use GNU Make if/endifs, so we
1240 # have to hide some included Makefiles with GNU extensions. We do
1241 # this by defining mk_include as an autoconf substitution and then
1242 # using "@mk_include@ other_makefile" in Makefile.am to include
1243 # makefiles with GNU extensions; this hides them from automake.
1245 AC_SUBST(mk_include)
1246 # Similar trickery for "if"
1254 # This is used to _always_ comment out rules in automake makefiles, but
1255 # still trigger certain automake behavior; see test/unit/Makefile.am.
1256 AM_CONDITIONAL([CVC4_FALSE], [false])
1258 # set up substitutions for src/util/{rational,integer}.h.in
1259 if test $cvc4_cln_or_gmp = cln; then
1266 AC_SUBST(CVC4_USE_CLN_IMP)
1267 AC_SUBST(CVC4_USE_GMP_IMP)
1269 # month/year for man pages
1270 MAN_DATE=`date '+%B %Y'`
1276 m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | grep -v '^contrib/alttheoryskel/' | sort | sed 's,\.am$,,'])
1279 if test $cvc4_has_threads = yes; then
1280 support_multithreaded='with boost threading library'
1281 AM_CONDITIONAL([CVC4_HAS_THREADS], [true])
1282 AC_SUBST([CVC4_HAS_THREADS], 1)
1284 support_multithreaded='no'
1285 AM_CONDITIONAL([CVC4_HAS_THREADS], [false])
1286 AC_SUBST([CVC4_HAS_THREADS], 0)
1289 AM_CONDITIONAL([CVC4_NEEDS_REPLACEMENT_FUNCTIONS], [test -n "$LIBOBJS"])
1291 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
1292 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
1293 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/tls.h])
1295 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template])
1296 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5])
1297 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3_template])
1298 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc_template])
1299 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc_template])
1300 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3])
1301 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3])
1305 # Final information to the user
1308 if test "$custom_build_profile" = yes; then
1309 if test "$with_build" = default; then
1312 with_build="$with_build (customized)"
1316 support_unit_tests='cxxtest not found; unit tests not supported'
1317 if test -n "$CXXTEST"; then
1318 support_unit_tests='unit testing infrastructure enabled in build directory'
1319 elif test "$enable_unit_testing" = no; then
1320 support_unit_tests='unit testing disabled by user'
1323 if test "$enable_optimized" = yes; then
1324 optimized="yes, at level $OPTLEVEL"
1329 if test $have_libglpk -eq 1; then
1330 licensewarn="${licensewarn}Please note that CVC4 will be built against the GNU Linear Programming
1331 Kit (GLPK). This library is covered under the GPL, so use of this build
1332 of CVC4 will be more restrictive than CVC4's license would normally
1333 suggest. For full details of GLPK and its license, please visit
1334 http://www.gnu.org/software/glpk/
1335 To build CVC4 without GLPK, configure --without-glpk (which is the default).
1340 if test $cvc4_cln_or_gmp = cln; then
1341 mplibrary='cln (GPL)'
1342 licensewarn="${licensewarn}Please note that CVC4 will be built against the Class Library for
1343 Numbers (CLN). This library is covered under the GPL, so use of this
1344 build of CVC4 will be more restrictive than CVC4's license would
1345 normally suggest. For full details of CLN and its license, please visit
1346 http://www.ginac.de/CLN/
1347 To build CVC4 with GMP instead (which is covered under the more permissive
1348 LGPL), configure --without-cln.
1351 if test $with_portfolio = yes; then
1352 licensewarn="${licensewarn}
1353 WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
1354 WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
1356 Note that CLN is UNSAFE FOR USE in parallel contexts!
1357 This build of CVC4 cannot be used safely as a portfolio solver.
1358 since the result of building with CLN will include numerous race
1359 conditions on the refcounts internal to CLN.
1361 WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
1362 WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
1367 mplibrary='gmp (LGPL)'
1370 CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="$CVC4_COMPAT_LIBRARY_VERSION"
1371 CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="$CVC4_BINDINGS_LIBRARY_VERSION"
1372 if test "$CVC4_BUILD_LIBCOMPAT" = no; then
1373 CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="N/A"
1375 if test -z "$CVC4_LANGUAGE_BINDINGS"; then
1376 CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="N/A"
1379 bindings_to_be_built=none
1380 if test -n "$CVC4_LANGUAGE_BINDINGS"; then
1381 bindings_to_be_built="$CVC4_LANGUAGE_BINDINGS"
1382 if test -z "$SWIG"; then
1383 bindings_to_be_built="$bindings_to_be_built (for CVC3 compatibility layer only; SWIG not found)"
1391 Build profile: $with_build
1392 Build ID : $build_type
1393 Optimized : $optimized
1394 Debug symbols: $enable_debug_symbols
1395 Proof : $enable_proof
1396 Statistics : $enable_statistics
1397 Replay : $enable_replay
1398 Assertions : $enable_assertions
1399 Tracing : $enable_tracing
1400 Dumping : $enable_dumping
1401 Muzzle : $enable_muzzle
1403 Unit tests : $support_unit_tests
1404 Proof tests : $support_proof_tests
1405 gcov support : $enable_coverage
1406 gprof support: $enable_profiling
1407 Readline : $with_readline
1409 Static libs : $enable_static
1410 Shared libs : $enable_shared
1411 Static binary: $enable_static_binary
1412 Compat lib : $CVC4_BUILD_LIBCOMPAT
1413 Bindings : $bindings_to_be_built
1415 Multithreaded: $support_multithreaded
1416 TLS support : $CVC4_TLS_explanation
1417 Portfolio : $with_portfolio
1419 MP library : $mplibrary
1422 CPPFLAGS : $CPPFLAGS
1423 CXXFLAGS : $CXXFLAGS
1428 libcvc4 version : $CVC4_LIBRARY_VERSION
1429 libcvc4parser version : $CVC4_PARSER_LIBRARY_VERSION
1430 libcvc4compat version : $CVC4_COMPAT_LIBRARY_VERSION_or_nobuild
1431 libcvc4bindings version: $CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild
1433 Install into : $prefix
1435 ${licensewarn}Now just type make, followed by make check or make install, as you like.
1439 if test -n "$CVC4_UNSUPPORTED_LANGUAGE_BINDINGS"; then
1441 AC_MSG_WARN([You are electing to build unsupported language binding(s): $CVC4_UNSUPPORTED_LANGUAGE_BINDINGS])
1442 AC_MSG_WARN([Please be aware that these bindings may not compile, or work, and the interface to CVC4 via])
1443 AC_MSG_WARN([these bindings may change drastically in upcoming releases of CVC4.])
1447 if test -n "$CVC4_INTEGRITY_WARNING"; then
1449 AC_MSG_WARN($CVC4_INTEGRITY_WARNING)
1450 AC_MSG_WARN([Please run "make check" after building to ensure integrity of the binary and library])