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, 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)
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
73 # remember if the user set these explicitly (or whether autoconf does)
74 user_specified_enable_or_disable_static=${enable_static+yes}
75 user_specified_enable_or_disable_shared=${enable_shared+yes}
77 if test -e src/include/cvc4_public.h; then
78 CVC4_CONFIGURE_AT_TOP_LEVEL=yes
80 CVC4_CONFIGURE_AT_TOP_LEVEL=no
83 # override autoconf: we don't want it giving us CFLAGS/CXXFLAGS, but we do
84 # want to respect the user's flags
85 if test -z "${CFLAGS+set}"; then CFLAGS=; fi
86 if test -z "${CXXFLAGS+set}"; then CXXFLAGS=; fi
89 AM_MAINTAINER_MODE([enable])
91 # turn off static lib building by default
101 if test "$enable_shared" = no -a "$user_specified_enable_or_disable_shared" = yes; then
105 # Features requested by the user
106 AC_MSG_CHECKING([for requested build profile])
108 [AS_HELP_STRING([--with-build=profile],
109 [for profile in {production,debug,default,competition}])])
111 if test -z "${with_build+set}" -o "$with_build" = default; then
114 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}"; then
115 custom_build_profile=no
117 custom_build_profile=yes
120 if test -n "${enable_optimized+set}"; then
121 if test "$enable_optimized" = yes; then
122 btargs="$btargs optimized"
124 btargs="$btargs nooptimized"
127 if test -n "${enable_static_binary+set}"; then
128 if test "$enable_static_binary" = yes; then
129 btargs="$btargs staticbinary"
131 btargs="$btargs nostaticbinary"
134 if test -n "${enable_debug_symbols+set}"; then
135 if test "$enable_debug_symbols" = yes; then
136 btargs="$btargs debugsymbols"
138 btargs="$btargs nodebugsymbols"
141 if test -n "${enable_assertions+set}"; then
142 if test "$enable_assertions" = yes; then
143 btargs="$btargs assertions"
145 btargs="$btargs noassertions"
148 if test -n "${enable_proof+set}"; then
149 if test "$enable_proof" = yes; then
150 btargs="$btargs proof"
152 btargs="$btargs noproof"
155 if test -n "${enable_tracing+set}"; then
156 if test "$enable_tracing" = yes; then
157 btargs="$btargs tracing"
159 btargs="$btargs notracing"
162 if test -n "${enable_dumping+set}"; then
163 if test "$enable_dumping" = yes; then
164 btargs="$btargs dumping"
166 btargs="$btargs nodumping"
169 if test -n "${enable_muzzle+set}"; then
170 if test "$enable_muzzle" = yes; then
171 btargs="$btargs muzzle"
173 btargs="$btargs nomuzzle"
176 if test -n "${enable_coverage+set}"; then
177 if test "$enable_coverage" = yes; then
178 btargs="$btargs coverage"
180 btargs="$btargs nocoverage"
183 if test -n "${enable_profiling+set}"; then
184 if test "$enable_profiling" = yes; then
185 btargs="$btargs profiling"
187 btargs="$btargs noprofiling"
190 if test -n "${enable_statistics+set}"; then
191 if test "$enable_statistics" = yes; then
192 btargs="$btargs statistics"
194 btargs="$btargs nostatistics"
197 if test -n "${enable_replay+set}"; then
198 if test "$enable_replay" = yes; then
199 btargs="$btargs replay"
201 btargs="$btargs noreplay"
204 AC_MSG_RESULT([$with_build])
206 AM_INIT_AUTOMAKE([1.11 no-define tar-pax parallel-tests color-tests subdir-objects])
207 AC_CONFIG_HEADERS([cvc4autoconfig.h])
209 # automake 1.12 changes the test driver mechanism in a way that is
210 # completely incompatible with 1.11. We figure out here which version
211 # we're using in order to set up test makefiles correctly.
212 # See http://lists.gnu.org/archive/html/automake/2012-04/msg00060.html
213 if test -z "$am__api_version"; then
214 AC_MSG_ERROR([Cannot determine automake API version ?!])
216 case "$am__api_version" in
217 1.11*) automake111=true ;;
218 *) automake111=false ;;
220 AM_CONDITIONAL([AUTOMAKE_1_11], [$automake111])
222 # Initialize libtool's configuration options.
223 # we're not DLL-clean yet (i.e., don't properly use dllexport and dllimport)
224 # _LT_SET_OPTION([LT_INIT],[win32-dll])
227 # Checks for programs.
234 # [chris 8/24/2010] The user *must* specify --with-cln to get CLN
235 # (and, thus, opt in to the GPL dependency).
244 [use CLN instead of GMP]
246 [if test "$withval" != no; then
252 # [chris 8/24/2010] --with-gmp has no practical effect, since GMP is
253 # the default. Could be useful if other options are added later.
259 [use GMP instead of CLN (default)]
261 [if test "$withval" = no; then
262 if test $cvc4_use_cln = 0; then
263 AC_MSG_ERROR([You must use either CLN and GMP. Please pick one.])
271 if test $cvc4_use_cln = 1 && test $cvc4_use_gmp = 1; then
273 AC_MSG_ERROR([You cannot use both CLN and GMP. Please pick one.])
276 # try GMP, fail if not found; GMP is required for both CLN and for GMP
278 AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP (libgmp) not found, see http://gmplib.org/])])
280 if test $cvc4_use_cln = 1; then
281 # [mdeters] The PKG_CHECK_MODULES macro isn't customizable and doesn't fail
282 # gracefully. You can only specify it once for a given library name. That
283 # is, even on separate if/else branches, you can't put
284 # PKG_CHECK_MODULES([CLN], ...). That's why things are so convoluted here,
285 # we have to have PKG_CHECK_MODULES _exactly_ once in configure.ac !
286 PKG_CHECK_MODULES([CLN], [cln >= 1.2.2],
289 AC_LINK_IFELSE([AC_LANG_PROGRAM([[#include <cln/cln.h>]], [[cln::cl_F pi = "3.1415926";]])])
292 [if test $cvc4_use_cln = 0; then
294 AC_MSG_NOTICE([CLN not installed (or too old) or pkgconfig missing, will use gmp])
297 AC_MSG_ERROR([CLN not installed (or too old) or pkgconfig missing])
302 if test $cvc4_use_cln = 0; then
303 # try GMPXX, fail if not found
304 AC_CHECK_LIB(gmpxx, __gmpz_init, , [AC_MSG_ERROR([GNU MP C++ library (libgmpxx) not found, see http://gmplib.org/])])
307 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }$CLN_CFLAGS"
308 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }$CLN_CFLAGS"
309 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }$CLN_CFLAGS"
310 LIBS="$CLN_LIBS${LIBS:+ $LIBS}"
314 if test $cvc4_cln_or_gmp = cln; then
315 AC_DEFINE_UNQUOTED(CVC4_CLN_IMP, [], [Defined if using the CLN multi-precision arithmetic library.])
317 AC_DEFINE_UNQUOTED(CVC4_GMP_IMP, [], [Defined if using the GMP multi-precision arithmetic library.])
319 AM_CONDITIONAL([CVC4_CLN_IMP], [test $cvc4_cln_or_gmp = cln])
320 AM_CONDITIONAL([CVC4_GMP_IMP], [test $cvc4_cln_or_gmp = gmp])
322 # construct the build string
323 AC_MSG_CHECKING([for appropriate build string])
324 if test -z "$ac_confdir"; then
327 build_type=`$ac_confdir/config/build-type $with_build $btargs $cvc4_cln_or_gmp`
328 if test "$custom_build_profile" = yes; then
329 if test "$with_build" = default; then
330 build_type=`$ac_confdir/config/build-type custom $btargs $cvc4_cln_or_gmp`
333 AC_MSG_RESULT($build_type)
335 # Require building in target and build-specific build directory:
337 # If the configure script is invoked from the top-level source
338 # directory, it creates a suitable build directory (based on the build
339 # architecture and build profile from $build_type), changes into it,
340 # and reinvokes itself. CVC4_CONFIGURE_IN_BUILDS is an envariable
341 # that breaks any possibility of infinite recursion in this process.
342 AC_MSG_CHECKING([what dir to configure])
343 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
344 AC_MSG_RESULT([this one (in builds/)])
345 elif test "$CVC4_CONFIGURE_AT_TOP_LEVEL" = yes; then
346 AC_MSG_RESULT([builds/$target/$build_type])
348 if test -z "$ac_srcdir"; then
349 mkbuilddir=./config/mkbuilddir
351 mkbuilddir=$ac_srcdir/config/mkbuilddir
353 $as_echo "$mkbuilddir $target $build_type"
354 source $mkbuilddir "$target" "$build_type"
355 $as_echo "cd builds/$target/$build_type"
356 cd "builds/$target/$build_type"
357 CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS
358 echo "$SHELL ../../../configure ${config_cmdline[[@]]}"
359 "$SHELL" "`pwd`/../../../configure" "${config_cmdline[[@]]}"
362 if test $exitval -eq 0; then
363 cat >config.reconfig <<EOF
365 # Generated by configure, `date`
366 # This script is part of CVC4.
368 cd "\`dirname \\"\$0\\"\`"
370 if test -d builds; then :; else echo 'No builds/ directory!' >&2; exit; fi
372 current=(\`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]*\\)/\\(.*\\),\\1 \\2,'\`)
376 echo "reconfiguring in builds/\$arch/\$build..."
377 cd "builds/\$arch/\$build"
378 echo ./config.status "\$@"
379 ./config.status "\$@"]
381 chmod +x config.reconfig
383 ln -sf "$target/$build_type/config.log" "builds/config.log"
386 AC_MSG_RESULT([this one (user-specified)])
391 # Unpack standard build types. Any particular options can be overriden with
392 # --enable/disable-X options
393 case "$with_build" in
394 production) # highly optimized, no assertions, no tracing, dumping
399 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
400 if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=3 ; fi
401 if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
402 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
403 if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
404 if test -z "${enable_replay+set}" ; then enable_replay=no ; fi
405 if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi
406 if test -z "${enable_proof+set}" ; then enable_proof=no ; fi
407 if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi
408 if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
409 if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
411 debug) # unoptimized, debug symbols, assertions, tracing, dumping
412 CVC4CPPFLAGS='-DCVC4_DEBUG'
413 CVC4CXXFLAGS='-fno-inline'
414 CVC4CFLAGS='-fno-inline'
416 FLAG_VISIBILITY_HIDDEN=
417 if test -z "${enable_optimized+set}" ; then enable_optimized=no ; fi
418 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
419 if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
420 if test -z "${enable_replay+set}" ; then enable_replay=yes ; fi
421 if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi
422 if test -z "${enable_proof+set}" ; then enable_proof=no ; fi
423 if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi
424 if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
425 if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
427 default) # moderately optimized, assertions, tracing, dumping
432 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
433 if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=2 ; fi
434 if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
435 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
436 if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
437 if test -z "${enable_replay+set}" ; then enable_replay=yes ; fi
438 if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi
439 if test -z "${enable_proof+set}" ; then enable_proof=no ; fi
440 if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi
441 if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
442 if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
444 competition) # maximally optimized, no assertions, no tracing, no dumping, muzzled
445 CVC4CPPFLAGS='-DCVC4_COMPETITION_MODE'
446 CVC4CXXFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
447 CVC4CFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
449 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
450 if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=9 ; fi
451 if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
452 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no ; fi
453 if test -z "${enable_statistics+set}" ; then enable_statistics=no ; fi
454 if test -z "${enable_replay+set}" ; then enable_replay=no ; fi
455 if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi
456 if test -z "${enable_proof+set}" ; then enable_proof=no ; fi
457 if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi
458 if test -z "${enable_dumping+set}" ; then enable_dumping=no ; fi
459 if test -z "${enable_muzzle+set}" ; then enable_muzzle=yes ; fi
460 if test -z "${user_specified_enable_or_disable_shared}"; then enable_shared=no; fi
461 if test -z "${user_specified_enable_or_disable_static}"; then enable_static=yes; fi
462 if test -z "${enable_static_binary+set}"; then enable_static_binary=yes ; fi
465 AC_MSG_FAILURE([unknown build profile: $with_build])
468 if test -z "${OPTLEVEL+set}"; then OPTLEVEL=3; fi
470 AM_CONDITIONAL([CVC4_BUILD_PROFILE_PRODUCTION], [test "$with_build" = production])
471 AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEBUG], [test "$with_build" = debug])
472 AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEFAULT], [test "$with_build" = default])
473 AM_CONDITIONAL([CVC4_BUILD_PROFILE_COMPETITION], [test "$with_build" = competition])
475 # permit a static binary
476 AC_MSG_CHECKING([whether to build a static binary])
477 AC_ARG_ENABLE([static-binary],
478 [AS_HELP_STRING([--enable-static-binary],
479 [build a fully statically-linked binary [default=no]])])
480 if test -z "${enable_static_binary+set}"; then
481 enable_static_binary=no
483 AC_MSG_RESULT([$enable_static_binary])
484 if test "$enable_static_binary" = yes; then
485 if test "$target_vendor" = apple; then
486 if test -z "$MAC_STATIC_BINARY_MANUAL_OVERRIDE"; then
487 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)]])
489 AC_MSG_WARN([MAC_STATIC_BINARY_MANUAL_OVERRIDE was set!])
490 AC_MSG_WARN([Will make a static binary during this build. Note that it may fail!])
493 if test "$enable_static" != yes; then
495 AC_MSG_WARN([forcing static-library building, --enable-static-binary given])
499 AC_MSG_CHECKING([whether to support proofs in libcvc4])
501 AC_ARG_ENABLE([proof],
502 [AS_HELP_STRING([--enable-proof],
503 [support proof generation])])
504 if test -z "${enable_proof+set}"; then
507 AC_MSG_RESULT([$enable_proof])
509 if test "$enable_proof" = yes; then
510 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROOF"
513 AC_MSG_CHECKING([whether to optimize libcvc4])
515 AC_ARG_ENABLE([optimized],
516 [AS_HELP_STRING([--enable-optimized],
517 [optimize the build])])
519 if test -z "${enable_optimized+set}"; then
523 AC_MSG_RESULT([$enable_optimized])
525 if test "$enable_optimized" = yes; then
526 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O$OPTLEVEL"
527 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O$OPTLEVEL"
529 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O0"
530 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O0"
533 AC_MSG_CHECKING([whether to include debugging symbols in libcvc4])
535 AC_ARG_ENABLE([debug-symbols],
536 [AS_HELP_STRING([--disable-debug-symbols],
537 [do not include debug symbols in libcvc4])])
539 if test -z "${enable_debug_symbols+set}"; then
540 enable_debug_symbols=yes
543 AC_MSG_RESULT([$enable_debug_symbols])
545 if test "$enable_debug_symbols" = yes; then
546 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-ggdb3"
547 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-ggdb3"
550 AC_MSG_CHECKING([whether to include statistics are turned on in libcvc4])
552 AC_ARG_ENABLE([statistics],
553 [AS_HELP_STRING([--disable-statistics],
554 [do not include statistics in libcvc4])])
556 if test -z "${enable_statistics+set}"; then
557 enable_statistics=yes
560 AC_MSG_RESULT([$enable_statistics])
562 if test "$enable_statistics" = yes; then
563 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_STATISTICS_ON"
566 AC_MSG_CHECKING([whether the replay feature should be turned on in libcvc4])
568 AC_ARG_ENABLE([replay],
569 [AS_HELP_STRING([--disable-replay],
570 [turn off the replay feature in libcvc4])])
572 if test -z "${enable_replay+set}"; then
576 AC_MSG_RESULT([$enable_replay])
578 if test "$enable_replay" = yes; then
579 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_REPLAY"
582 AC_MSG_CHECKING([whether to include assertions in build])
584 AC_ARG_ENABLE([assertions],
585 [AS_HELP_STRING([--disable-assertions],
586 [turn off assertions in build])])
588 if test -z "${enable_assertions+set}"; then
589 enable_assertions=yes
592 AC_MSG_RESULT([$enable_assertions])
594 if test "$enable_assertions" = yes; then
595 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_ASSERTIONS"
597 # turn off regular C assert() also
598 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DNDEBUG"
601 AC_MSG_CHECKING([whether to do a traceable build of CVC4])
602 AC_ARG_ENABLE([tracing],
603 [AS_HELP_STRING([--disable-tracing],
604 [remove all tracing code from CVC4])])
606 if test -z "${enable_tracing+set}"; then
610 AC_MSG_RESULT([$enable_tracing])
612 if test "$enable_tracing" = yes; then
613 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_TRACING"
616 AC_MSG_CHECKING([whether to do a dump-capable build of CVC4])
617 AC_ARG_ENABLE([dumping],
618 [AS_HELP_STRING([--disable-dumping],
619 [remove all dumping code from CVC4])])
621 if test -z "${enable_dumping+set}"; then
625 AC_MSG_RESULT([$enable_dumping])
627 if test "$enable_dumping" = yes; then
628 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DUMPING"
631 AC_MSG_CHECKING([whether to do a muzzled build of CVC4])
632 AC_ARG_ENABLE([muzzle],
633 [AS_HELP_STRING([--enable-muzzle],
634 [completely silence CVC4; remove ALL non-result output from build])])
636 if test -z "${enable_muzzle+set}"; then
640 AC_MSG_RESULT([$enable_muzzle])
642 if test "$enable_muzzle" = yes; then
643 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_MUZZLE"
646 AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4])
647 AC_ARG_ENABLE([coverage],
648 [AS_HELP_STRING([--enable-coverage],
649 [build with support for gcov coverage testing])])
651 if test -z "${enable_coverage+set}"; then
655 AC_MSG_RESULT([$enable_coverage])
657 if test "$enable_coverage" = yes; then
658 # For coverage testing, we prefer:
659 # --enable-static --disable-shared --disable-static-binary
660 # If the user didn't specify these, we force them here. If the
661 # user specified them in opposite phase, give warnings that they
662 # shouldn't do that, or bomb out.
663 if test "$user_specified_enable_or_disable_shared" != yes; then
665 AC_MSG_WARN([turning off shared library building due to --enable-coverage])
666 elif test "$enable_shared" = yes; then
668 AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-shared])
669 AC_MSG_WARN([gcov does not support shared libraries, so only your static libraries will be coverage-testable.])
670 AC_MSG_WARN([Your cvc4 driver and testing binaries will not be coverage-testable.])
673 if test "${enable_static_binary+set}" = set -a "$enable_static_binary" = yes; then
675 AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-static-binary])
676 AC_MSG_WARN([Your cvc4 driver and testing binaries will be fully-statically linked and may not be coverage-testable.])
679 if test "$user_specified_enable_or_disable_static" != yes; then
681 AC_MSG_WARN([turning on static library building due to --enable-coverage])
682 elif test "$enable_static" != yes; then
683 AC_MSG_ERROR([--enable-coverage and --disable-static are incompatible; gcov only supports static libraries.])
686 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COVERAGE"
687 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }--coverage"
688 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }--coverage"
689 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }--coverage"
692 AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4])
694 AC_ARG_ENABLE([profiling],
695 [AS_HELP_STRING([--enable-profiling],
696 [build with support for gprof profiling])])
698 if test -z "${enable_profiling+set}"; then
702 AC_MSG_RESULT([$enable_profiling])
704 if test "$enable_profiling" = yes; then
705 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROFILING"
706 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-pg"
707 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-pg"
708 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }-pg"
711 # Check for libglpk (defined in config/glpk.m4)
713 [AS_HELP_STRING([--with-glpk],
714 [use GLPK simplex solver])], [], [with_glpk=])
716 if test $have_libglpk -eq 1; then
717 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_GLPK"
719 AM_CONDITIONAL([CVC4_USE_GLPK], [test $have_libglpk -eq 1])
720 AC_SUBST([GLPK_LIBS])
722 # Check to see if this version/architecture of GNU C++ explicitly
723 # instantiates __gnu_cxx::hash<uint64_t> or not. Some do, some don't.
724 # See src/util/hash.h.
725 AC_MSG_CHECKING([whether __gnu_cxx::hash<uint64_t> is already specialized])
727 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
729 #include <ext/hash_map>
730 namespace __gnu_cxx { template<> struct hash<uint64_t> {}; }])],
731 [AC_MSG_RESULT([no]); CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_NEED_HASH_UINT64_T"],
732 [AC_MSG_RESULT([yes])])
735 # Check whether "long" and "int64_t" are distinct types w.r.t. overloading.
736 # Even if they have the same size, they can be distinct, and some platforms
737 # can have problems with ambiguous function calls when auto-converting
738 # int64_t to long, and others will complain if you overload a function
739 # that takes an int64_t with one that takes a long (giving a redefinition
740 # error). So we have to keep both happy. Probably the same underlying
741 # issue as the hash specialization above, but let's check separately
743 AC_MSG_CHECKING([for the relationship between long and int64_t])
745 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
748 void foo(int64_t) {}])],
749 [AC_MSG_RESULT([no relationship detected]); CVC4_NEED_INT64_T_OVERLOADS=1],
750 [AC_MSG_RESULT([typedef or similar]); CVC4_NEED_INT64_T_OVERLOADS=0])
752 AC_SUBST([CVC4_NEED_INT64_T_OVERLOADS])
754 AC_MSG_CHECKING([for the pb_ds namespace])
756 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
757 #include <ext/pb_ds/priority_queue.hpp>
758 typedef pb_ds::priority_queue<void, void, void> pq;])],
759 [CVC4_PB_DS_NAMESPACE=pb_ds],
760 [AC_COMPILE_IFELSE([AC_LANG_SOURCE([
761 #include <ext/pb_ds/priority_queue.hpp>
762 typedef __gnu_pbds::priority_queue<void, void, void> pq;])],
763 [CVC4_PB_DS_NAMESPACE=__gnu_pbds],
764 [AC_MSG_ERROR([cannot find required priority_queue in either __gnu_pbds or pb_ds namespace])])])
766 AC_MSG_RESULT([$CVC4_PB_DS_NAMESPACE])
767 AC_DEFINE_UNQUOTED(CVC4_PB_DS_NAMESPACE, ${CVC4_PB_DS_NAMESPACE}, [The namespace for pb_ds data structures.])
769 # for information: http://gcc.gnu.org/bugzilla/show_bug.cgi?id=36612
770 AC_MSG_CHECKING([whether pb_ds has bug 36612])
772 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
773 #define __throw_container_error inline __throw_container_error
774 #define __throw_insert_error inline __throw_insert_error
775 #define __throw_join_error inline __throw_join_error
776 #define __throw_resize_error inline __throw_resize_error
777 #include <ext/pb_ds/exception.hpp>
779 [CVC4_GCC_HAS_PB_DS_BUG=1; bugverb=is],
780 [CVC4_GCC_HAS_PB_DS_BUG=0; bugverb="is not"])
782 AC_MSG_RESULT([bug $bugverb present])
783 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])
785 # Check for ANTLR runantlr script (defined in config/antlr.m4)
788 CVC4_CXX_OPTION([-Werror], [WERROR])
789 CVC4_C_OPTION([-Werror], [C_WERROR])
790 CVC4_CXX_OPTION([-Wno-deprecated], [WNO_DEPRECATED])
791 CVC4_C_OPTION([-Wno-deprecated], [C_WNO_DEPRECATED])
792 CVC4_CXX_OPTION([-Wno-conversion-null], [WNO_CONVERSION_NULL])
793 CVC4_CXX_OPTION([-Wno-tautological-compare], [WNO_TAUTOLOGICAL_COMPARE])
794 CVC4_CXX_OPTION([-Wno-parentheses], [WNO_PARENTHESES])
795 CVC4_CXX_OPTION([-Wno-uninitialized], [WNO_UNINITIALIZED])
796 CVC4_CXX_OPTION([-Wno-unused-variable], [WNO_UNUSED_VARIABLE])
797 CVC4_CXX_OPTION([-fno-strict-aliasing], [FNO_STRICT_ALIASING])
799 AC_SUBST([WNO_CONVERSION_NULL])
800 AC_SUBST([WNO_TAUTOLOGICAL_COMPARE])
801 AC_SUBST([WNO_PARENTHESES])
802 AC_SUBST([WNO_UNINITIALIZED])
803 AC_SUBST([WNO_UNUSED_VARIABLE])
804 AC_SUBST([FNO_STRICT_ALIASING])
806 # On Mac, we have to fix the visibility of standard library symbols.
807 # Otherwise, exported template instantiations---even though explicitly
808 # CVC4_PUBLIC, can be generated as symbols with internal-only linkage.
809 # Presumably, Apple is distributing a libstdc++ that is built *without*
810 # --enable-libstdcxx-visibility (?)
811 if test "$target_vendor" = apple; then
812 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-D_GLIBCXX_VISIBILITY_DEFAULT=\"__attribute__((__visibility__(\\\"default\\\")))\""
815 # Doxygen configuration
816 AC_ARG_ENABLE([internals-documentation],
817 [AS_HELP_STRING([--enable-internals-documentation],
818 [build Doxygen documentation for static and private member functions])])
819 if test "$enable_internals_documentation" = yes; then
820 DOXYGEN_EXTRACT_PRIVATE=YES
821 DOXYGEN_EXTRACT_STATIC=YES
823 DOXYGEN_EXTRACT_PRIVATE=NO
824 DOXYGEN_EXTRACT_STATIC=NO
826 AC_SUBST([DOXYGEN_EXTRACT_PRIVATE])
827 AC_SUBST([DOXYGEN_EXTRACT_STATIC])
833 DX_INIT_DOXYGEN($PACKAGE_NAME, config/doxygen.cfg, $srcdir/doc/doxygen)
835 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])
836 AC_ARG_VAR(CXXTEST, [path to CxxTest installation])
840 AC_ARG_WITH([cxxtest-dir],
841 [AS_HELP_STRING([--with-cxxtest-dir=DIR], [path to CxxTest installation])],
842 [CXXTEST="$withval"])
844 # In the case of "./configure --with-cxxtest-dir=../cxxtest" (or other
845 # relative path) and having switched the configure directory (see above),
846 # search with respect to the top source dir, not the build dir
847 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes -a -n "$CXXTEST"; then
850 *) CXXTEST="$srcdir/$CXXTEST" ;;
854 AC_ARG_VAR(LFSC, [path to LFSC proof checker])
855 AC_ARG_VAR(LFSCARGS, [arguments to pass to LFSC proof checker])
856 if test -z "$LFSC"; then
857 AC_CHECK_PROGS(LFSC, lfsc, [], [])
859 AC_CHECK_PROG(LFSC, "$LFSC", [], [])
861 AM_CONDITIONAL([PROOF_REGRESSIONS], [test -n "$LFSC" -a "$enable_proof" = yes])
862 if test -n "$LFSC" -a "$enable_proof" = yes; then
863 TESTS_ENVIRONMENT="${TESTS_ENVIRONMENT:+$TESTS_ENVIRONMENT }LFSC=\"$LFSC $LFSCARGS\""
864 RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--proof"
866 AC_SUBST([TESTS_ENVIRONMENT])
867 AC_SUBST([RUN_REGRESSION_ARGS])
868 if test -z "$LFSC"; then
869 support_proof_tests='no, lfsc proof checker unavailable'
870 elif test "$enable_proof" = yes; then
871 support_proof_tests='yes, proof regression tests enabled'
873 support_proof_tests='no, proof generation disabled for this build'
879 AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH])
880 if test -z "$CXXTESTGEN"; then
881 AC_PATH_PROG(CXXTESTGEN, cxxtestgen.py, [], [$CXXTEST:$PATH])
883 if test -z "$CXXTESTGEN"; then
884 AC_PATH_PROG(CXXTESTGEN, cxxtestgen, [], [$CXXTEST:$PATH])
886 if test "$enable_unit_testing" = "no"; then
887 AC_MSG_NOTICE([unit tests disabled by user request.])
890 elif test -z "$CXXTESTGEN"; then
891 AC_MSG_NOTICE([unit tests disabled, could not find cxxtestgen.pl or cxxtestgen.py or cxxtestgen])
892 elif test -z "$CXXTEST"; then
893 CXXTEST=`dirname "$CXXTESTGEN"`
894 AC_MSG_CHECKING([for location of CxxTest headers])
895 if test -e "$CXXTEST/cxxtest/TestRunner.h"; then
896 AC_MSG_RESULT([$CXXTEST])
898 if test -e "/usr/include/cxxtest/TestRunner.h"; then
899 AC_MSG_RESULT([/usr/include])
901 AC_MSG_RESULT([not found])
902 AC_MSG_WARN([unit tests disabled, CxxTest headers not found.])
909 if test "$enable_unit_testing" = yes -a -z "$CXXTESTGEN"; then
910 AC_MSG_ERROR([--enable-unit-testing given but cxxtest not found.])
913 AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"])
915 AC_ARG_VAR(TEST_CPPFLAGS, [CPPFLAGS to use when testing (default=$CPPFLAGS)])
916 AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)])
917 AC_ARG_VAR(TEST_LDFLAGS, [LDFLAGS to use when testing (default=$LDFLAGS)])
919 AC_ARG_VAR(PERL, [PERL interpreter (used when testing)])
921 if test -n "$CXXTEST"; then
922 if test -z "$PERL"; then
923 AC_CHECK_PROGS(PERL, perl, perl, [])
925 AC_CHECK_PROG(PERL, "$PERL", "$PERL", [])
928 if test -z "$PERL"; then
929 AC_MSG_WARN([unit tests disabled, perl not found.])
935 AC_ARG_VAR(PYTHON, [PYTHON interpreter (used for building legacy Java library interface)])
937 if test -z "$PYTHON"; then
938 AC_CHECK_PROGS(PYTHON, python, python, [])
940 AC_CHECK_PROG(PYTHON, "$PYTHON", "$PYTHON", [])
943 if test -z "$PYTHON"; then
944 AC_MSG_WARN([python not found, cannot build libcvc4compat_java (the legacy Java interface).])
949 # Checks for libraries.
951 AC_SEARCH_LIBS([clock_gettime], [rt],
952 [AC_DEFINE([HAVE_CLOCK_GETTIME], [1],
953 [Defined to 1 if clock_gettime() is supported by the platform.])],
954 [AC_LIBOBJ([clock_gettime])])
955 AC_CHECK_FUNC([strtok_r], [AC_DEFINE([HAVE_STRTOK_R], [1],
956 [Defined to 1 if strtok_r() is supported by the platform.])],
957 [AC_LIBOBJ([strtok_r])])
958 AC_CHECK_FUNC([ffs], [AC_DEFINE([HAVE_FFS], [1],
959 [Defined to 1 if ffs() is supported by the platform.])],
962 # Check for antlr C++ runtime (defined in config/antlr.m4)
965 # Check for user preferences for language bindings to build, and for
966 # build support. The arg list is the default set if unspecified by
967 # the user (the actual built set is the subset that appears to be
968 # supported by the build host).
969 CVC4_CHECK_BINDINGS([c java])dnl csharp perl php python ruby tcl ocaml])
971 # Checks for header files and their contents.
972 AC_CHECK_HEADERS([getopt.h unistd.h])
974 # Checks for typedefs, structures, and compiler characteristics.
976 # these are bad macros, they clash with system header <stdint.h> !!
982 # guard against double-inclusion of the autoheader
983 AH_TOP([#ifndef __CVC4__CVC4AUTOCONFIG_H
984 #define __CVC4__CVC4AUTOCONFIG_H])
985 AH_BOTTOM([#endif /* __CVC4__CVC4AUTOCONFIG_H */])
987 AC_CHECK_DECLS([optreset], [], [], [#include <getopt.h>])
989 # check with which standard strerror_r() complies
992 # require boost library
995 # look for boost threading library
996 AC_ARG_WITH([portfolio],
997 AS_HELP_STRING([--with-portfolio], [build the multithreaded portfolio version of CVC4 (pcvc4)]))
998 cvc4_save_LDFLAGS="$LDFLAGS"
999 if test "$enable_static_binary" = yes; then
1000 LDFLAGS="-static $LDFLAGS"
1002 cvc4_has_threads=yes
1003 AC_ARG_ENABLE([thread-support],
1004 AS_HELP_STRING([--disable-thread-support], [do not support multithreaded-capable library]))
1005 if test "$enable_thread_support" = no; then
1007 if test "$with_portfolio" = yes; then
1008 AC_MSG_ERROR([user gave both --with-portfolio and --disable-thread-support, which are contradictory])
1011 BOOST_THREADS([], [AC_MSG_WARN([disabling multithreaded support])
1012 cvc4_has_threads=no])
1014 LDFLAGS="$cvc4_save_LDFLAGS"
1015 if test $cvc4_has_threads = no; then
1016 if test "$enable_thread_support" = yes; then
1017 AC_MSG_ERROR([user gave --enable-thread-support but could not build with threads; maybe boost threading library is missing?])
1019 if test "$with_portfolio" = yes; then
1020 AC_MSG_ERROR([user gave --with-portfolio but could not build with threads; maybe boost threading library is missing?])
1024 if test "$with_portfolio" != yes; then
1027 AM_CONDITIONAL([CVC4_BUILD_PCVC4], [test "$with_portfolio" = yes])
1028 if test "$with_portfolio" = yes; then
1029 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PORTFOLIO"
1032 # Check for libreadline (defined in config/readline.m4)
1033 AC_ARG_WITH([readline], [AS_HELP_STRING([--with-readline], [support the readline library])], [], [with_readline=check])
1034 # make the flags as close as possible to the final flags, because the Boost
1035 # flags can bring in a different, incompatible readline library than we'd
1036 # get otherwise (e.g. on Mac, where there are commonly two different readlines,
1037 # one in /usr and one in /opt/local)
1038 cvc4_rlcheck_save_CPPFLAGS="$CPPFLAGS"
1039 cvc4_rlcheck_save_CXXFLAGS="$CXXFLAGS"
1040 cvc4_rlcheck_save_CFLAGS="$CFLAGS"
1041 cvc4_rlcheck_save_LDFLAGS="$LDFLAGS"
1042 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
1043 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS $WNO_DEPRECATED"
1044 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS $C_WNO_DEPRECATED -fexceptions"
1045 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
1046 CVC4_CHECK_FOR_READLINE
1047 CPPFLAGS="$cvc4_rlcheck_save_CPPFLAGS"
1048 CXXFLAGS="$cvc4_rlcheck_save_CXXFLAGS"
1049 CFLAGS="$cvc4_rlcheck_save_CFLAGS"
1050 LDFLAGS="$cvc4_rlcheck_save_LDFLAGS"
1051 AC_DEFINE_UNQUOTED([HAVE_LIBREADLINE], $have_libreadline, [Define to 1 to use libreadline])
1052 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])
1053 AC_SUBST([READLINE_LIBS])
1055 # Whether to build compatibility library
1056 CVC4_BUILD_LIBCOMPAT=yes
1057 AC_ARG_WITH([compat],
1058 AS_HELP_STRING([--with-compat], [build compatibility library (CVC3 API layer)]),
1059 [if test "$withval" = no; then CVC4_BUILD_LIBCOMPAT=no; fi])
1060 AC_MSG_CHECKING([whether to build compatibility library (CVC3 API layer)])
1061 if test "$CVC4_BUILD_LIBCOMPAT" = yes; then
1062 AC_MSG_RESULT([yes])
1064 AC_MSG_RESULT([no, disabled by user])
1066 AC_SUBST(CVC4_BUILD_LIBCOMPAT)
1067 AM_CONDITIONAL([CVC4_BUILD_LIBCOMPAT], [test "$CVC4_BUILD_LIBCOMPAT" = yes])
1069 # Check for availability of TLS support (e.g. __thread storage class)
1070 AC_MSG_CHECKING([whether to use compiler-supported TLS if available])
1071 AC_ARG_ENABLE([tls], AS_HELP_STRING([--disable-tls], [don't use compiler-native TLS]))
1072 if test $cvc4_has_threads = no; then
1073 # We disable TLS entirely by simply telling the build system that
1074 # the empty string is the __thread keyword.
1075 AC_MSG_RESULT([multithreading disabled])
1076 CVC4_TLS_SUPPORTED=1
1078 CVC4_TLS_explanation='disabled (no multithreading support)'
1080 if test -z "${enable_tls+set}" || test "$enable_tls" = "yes"; then
1081 AC_MSG_RESULT([yes])
1082 AX_TLS([CVC4_TLS=$ac_cv_tls], [CVC4_TLS=])
1087 if test -n "$CVC4_TLS"; then
1088 CVC4_TLS_SUPPORTED=1
1089 CVC4_TLS_explanation="$CVC4_TLS"
1091 CVC4_TLS_explanation='pthread_getspecific()'
1092 CVC4_TLS_SUPPORTED=0
1095 AC_SUBST([CVC4_TLS])
1096 AC_SUBST([CVC4_TLS_SUPPORTED])
1098 # Whether to compile with google profiling tools
1099 cvc4_use_google_perftools=0
1103 [--with-google-perftools],
1104 [use Google Performance Tools]
1106 [if test "$withval" != no; then
1107 cvc4_use_google_perftools=1
1111 AC_MSG_CHECKING([whether to link in google perftools libraries])
1112 if test $cvc4_use_google_perftools = 1; then
1113 AC_MSG_RESULT([yes])
1114 AC_CHECK_LIB([tcmalloc], [MallocExtension_GetAllocatedSize], , [AC_MSG_ERROR([cannot link google-perftools test program with -ltcmalloc])], [-lpthread])
1115 AC_CHECK_LIB([profiler], [ProfilerStart], , [AC_MSG_ERROR([cannot link google-perftools test program with -lprofiler])], [-lpthread])
1117 AC_MSG_RESULT([no (user didn't request it)])
1121 AC_ARG_VAR(JAVA, [Java interpreter (used when testing Java interface)])
1122 AC_ARG_VAR(JAVAC, [Java compiler (used when building and testing Java interface)])
1123 AC_ARG_VAR(JAVAH, [Java compiler (used when building and testing Java interface)])
1124 AC_ARG_VAR(JAR, [Jar archiver (used when building Java interface)])
1125 if test "$cvc4_build_java_bindings"; then
1127 if test -z "$JAVA"; then
1128 AC_CHECK_PROGS(JAVA, java, java, [])
1130 AC_CHECK_PROG(JAVA, "$JAVA", "$JAVA", [])
1132 if test -z "$JAVAC"; then
1133 AC_CHECK_PROGS(JAVAC, javac gcj, javac, [])
1134 if test "$JAVAC" = gcj; then JAVAC='gcj -C'; fi
1136 AC_CHECK_PROG(JAVAC, "$JAVAC", "$JAVAC", [])
1138 if test -z "$JAVAH"; then
1139 AC_CHECK_PROGS(JAVAH, javah gcjh, javah, [])
1141 AC_CHECK_PROG(JAVAH, "$JAVAH", "$JAVAH", [])
1143 if test -z "$JAR"; then
1144 AC_CHECK_PROGS(JAR, jar, jar, [])
1146 AC_CHECK_PROG(JAR, "$JAR", "$JAR", [])
1150 # on Mac OS X, Java doesn't like the .so module extension; it wants .dylib
1151 module=no eval CVC4_JAVA_MODULE_EXT="$shrext_cmds"
1152 if test -z "$CVC4_JAVA_MODULE_EXT"; then
1153 CVC4_JAVA_MODULE_EXT=.so
1155 AC_SUBST([CVC4_JAVA_MODULE_EXT])
1157 # Prepare configure output
1159 if test "$enable_shared" = yes; then BUILDING_SHARED=1; else BUILDING_SHARED=0; fi
1160 if test "$enable_static" = yes; then BUILDING_STATIC=1; else BUILDING_STATIC=0; fi
1161 if test "$enable_static_binary" = yes; then STATIC_BINARY=1; else STATIC_BINARY=0; fi
1162 AC_SUBST(BUILDING_SHARED)
1163 AC_SUBST(BUILDING_STATIC)
1164 AC_SUBST(STATIC_BINARY)
1165 AM_CONDITIONAL([STATIC_BINARY], [test "$enable_static_binary" = yes])
1166 AM_CONDITIONAL([COVERAGE_ENABLED], [test "$enable_coverage" = yes])
1168 AM_CONDITIONAL([CVC4_DEBUG], [test "$with_build" = debug])
1169 AM_CONDITIONAL([CVC4_TRACING], [test "$enable_tracing" = yes])
1171 AC_SUBST(CVC4_LIBRARY_VERSION)
1172 AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
1173 AC_SUBST(CVC4_COMPAT_LIBRARY_VERSION)
1174 AC_SUBST(CVC4_BINDINGS_LIBRARY_VERSION)
1176 AC_DEFINE_UNQUOTED(CVC4_MAJOR, ${CVC4_MAJOR}, [Major component of the version of CVC4.])
1177 AC_DEFINE_UNQUOTED(CVC4_MINOR, ${CVC4_MINOR}, [Minor component of the version of CVC4.])
1178 AC_DEFINE_UNQUOTED(CVC4_RELEASE, ${CVC4_RELEASE}, [Release component of the version of CVC4.])
1179 AC_DEFINE_UNQUOTED(CVC4_EXTRAVERSION, ["${CVC4_EXTRAVERSION}"], [Extraversion component of the version of CVC4.])
1180 AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full release string for CVC4.])
1182 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
1183 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
1184 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions"
1185 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
1187 # visibility flag not supported for Windows builds
1188 # also increase default stack size for Windows binaries
1190 (*mingw*) FLAG_VISIBILITY_HIDDEN=
1191 cvc4_LDFLAGS=-Wl,--stack,134217728
1192 pcvc4_LDFLAGS=-Wl,--stack,134217728
1195 AC_SUBST(FLAG_VISIBILITY_HIDDEN)
1196 AC_SUBST(cvc4_LDFLAGS)
1197 AC_SUBST(pcvc4_LDFLAGS)
1201 # When automake scans Makefiles, it complains about non-standard make
1202 # features (including GNU extensions), and breaks GNU Make's
1203 # "if/endif" construct, replacing the "if" with AM_CONDITIONAL if
1204 # constructs. automake even follows "include" and messes with
1205 # included Makefiles.
1207 # CVC4 assumes GNU Make and we want to use GNU Make if/endifs, so we
1208 # have to hide some included Makefiles with GNU extensions. We do
1209 # this by defining mk_include as an autoconf substitution and then
1210 # using "@mk_include@ other_makefile" in Makefile.am to include
1211 # makefiles with GNU extensions; this hides them from automake.
1213 AC_SUBST(mk_include)
1217 # This is used to _always_ comment out rules in automake makefiles, but
1218 # still trigger certain automake behavior; see test/unit/Makefile.am.
1219 AM_CONDITIONAL([CVC4_FALSE], [false])
1221 # set up substitutions for src/util/{rational,integer}.h.in
1222 if test $cvc4_cln_or_gmp = cln; then
1229 AC_SUBST(CVC4_USE_CLN_IMP)
1230 AC_SUBST(CVC4_USE_GMP_IMP)
1232 # month/year for man pages
1233 MAN_DATE=`date '+%B %Y'`
1239 m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | grep -v '^contrib/alttheoryskel/' | sort | sed 's,\.am$,,'])
1242 if test $cvc4_has_threads = yes; then
1243 support_multithreaded='with boost threading library'
1244 AM_CONDITIONAL([CVC4_HAS_THREADS], [true])
1245 AC_SUBST([CVC4_HAS_THREADS], 1)
1247 support_multithreaded='no'
1248 AM_CONDITIONAL([CVC4_HAS_THREADS], [false])
1249 AC_SUBST([CVC4_HAS_THREADS], 0)
1252 AM_CONDITIONAL([CVC4_NEEDS_REPLACEMENT_FUNCTIONS], [test -n "$LIBOBJS"])
1254 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
1255 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
1256 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/tls.h])
1258 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template])
1259 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5])
1260 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3_template])
1261 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc_template])
1262 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc_template])
1263 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3])
1264 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3])
1268 # Final information to the user
1271 if test "$custom_build_profile" = yes; then
1272 if test "$with_build" = default; then
1275 with_build="$with_build (customized)"
1279 support_unit_tests='cxxtest not found; unit tests not supported'
1280 if test -n "$CXXTEST"; then
1281 support_unit_tests='unit testing infrastructure enabled in build directory'
1282 elif test "$enable_unit_testing" = no; then
1283 support_unit_tests='unit testing disabled by user'
1286 if test "$enable_optimized" = yes; then
1287 optimized="yes, at level $OPTLEVEL"
1292 if test $cvc4_cln_or_gmp = cln; then
1293 mplibrary='cln (GPL)'
1294 licensewarn="${licensewarn}Please note that CVC4 will be built against the Class Library for
1295 Numbers (CLN). This library is covered under the GPL, so use of this
1296 build of CVC4 will be more restrictive than CVC4's license would
1297 normally suggest. For full details of CLN and its license, please visit
1298 http://www.ginac.de/CLN/
1299 To build CVC4 with GMP instead (which is covered under the more permissive
1300 LGPL), configure --without-cln.
1303 if test $with_portfolio = yes; then
1304 licensewarn="${licensewarn}
1305 WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
1306 WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
1308 Note that CLN is UNSAFE FOR USE in parallel contexts!
1309 This build of CVC4 cannot be used safely as a portfolio solver.
1310 since the result of building with CLN will include numerous race
1311 conditions on the refcounts internal to CLN.
1313 WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
1314 WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
1319 mplibrary='gmp (LGPL)'
1322 CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="$CVC4_COMPAT_LIBRARY_VERSION"
1323 CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="$CVC4_BINDINGS_LIBRARY_VERSION"
1324 if test "$CVC4_BUILD_LIBCOMPAT" = no; then
1325 CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="N/A"
1327 if test -z "$CVC4_LANGUAGE_BINDINGS"; then
1328 CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="N/A"
1331 bindings_to_be_built=none
1332 if test -n "$CVC4_LANGUAGE_BINDINGS"; then
1333 bindings_to_be_built="$CVC4_LANGUAGE_BINDINGS"
1334 if test -z "$SWIG"; then
1335 bindings_to_be_built="$bindings_to_be_built (for CVC3 compatibility layer only; SWIG not found)"
1343 Build profile: $with_build
1344 Build ID : $build_type
1345 Optimized : $optimized
1346 Debug symbols: $enable_debug_symbols
1347 Proof : $enable_proof
1348 Statistics : $enable_statistics
1349 Replay : $enable_replay
1350 Assertions : $enable_assertions
1351 Tracing : $enable_tracing
1352 Dumping : $enable_dumping
1353 Muzzle : $enable_muzzle
1355 Unit tests : $support_unit_tests
1356 Proof tests : $support_proof_tests
1357 gcov support : $enable_coverage
1358 gprof support: $enable_profiling
1359 Readline : $with_readline
1361 Static libs : $enable_static
1362 Shared libs : $enable_shared
1363 Static binary: $enable_static_binary
1364 Compat lib : $CVC4_BUILD_LIBCOMPAT
1365 Bindings : $bindings_to_be_built
1367 Multithreaded: $support_multithreaded
1368 TLS support : $CVC4_TLS_explanation
1369 Portfolio : $with_portfolio
1371 MP library : $mplibrary
1374 CPPFLAGS : $CPPFLAGS
1375 CXXFLAGS : $CXXFLAGS
1380 libcvc4 version : $CVC4_LIBRARY_VERSION
1381 libcvc4parser version : $CVC4_PARSER_LIBRARY_VERSION
1382 libcvc4compat version : $CVC4_COMPAT_LIBRARY_VERSION_or_nobuild
1383 libcvc4bindings version: $CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild
1385 Install into : $prefix
1387 ${licensewarn}Now just type make, followed by make check or make install, as you like.
1391 if test -n "$CVC4_UNSUPPORTED_LANGUAGE_BINDINGS"; then
1393 AC_MSG_WARN([You are electing to build unsupported language binding(s): $CVC4_UNSUPPORTED_LANGUAGE_BINDINGS])
1394 AC_MSG_WARN([Please be aware that these bindings may not compile, or work, and the interface to CVC4 via])
1395 AC_MSG_WARN([these bindings may change drastically in upcoming releases of CVC4.])
1399 if test -n "$CVC4_INTEGRITY_WARNING"; then
1401 AC_MSG_WARN($CVC4_INTEGRITY_WARNING)
1402 AC_MSG_WARN([Please run "make check" after building to ensure integrity of the binary and library])