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
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}"; 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 AC_MSG_RESULT([$with_build])
207 AM_INIT_AUTOMAKE([1.11 no-define tar-pax parallel-tests color-tests subdir-objects])
208 AC_CONFIG_HEADERS([cvc4autoconfig.h])
210 # automake 1.12 changes the test driver mechanism in a way that is
211 # completely incompatible with 1.11. We figure out here which version
212 # we're using in order to set up test makefiles correctly.
213 # See http://lists.gnu.org/archive/html/automake/2012-04/msg00060.html
214 if test -z "$am__api_version"; then
215 AC_MSG_ERROR([Cannot determine automake API version ?!])
217 case "$am__api_version" in
218 1.11*) automake111=true ;;
219 *) automake111=false ;;
221 AM_CONDITIONAL([AUTOMAKE_1_11], [$automake111])
223 # Initialize libtool's configuration options.
224 # we're not DLL-clean yet (i.e., don't properly use dllexport and dllimport)
225 # _LT_SET_OPTION([LT_INIT],[win32-dll])
228 # Checks for programs.
235 # [chris 8/24/2010] The user *must* specify --with-cln to get CLN
236 # (and, thus, opt in to the GPL dependency).
245 [use CLN instead of GMP]
247 [if test "$withval" != no; then
253 # [chris 8/24/2010] --with-gmp has no practical effect, since GMP is
254 # the default. Could be useful if other options are added later.
260 [use GMP instead of CLN (default)]
262 [if test "$withval" = no; then
263 if test $cvc4_use_cln = 0; then
264 AC_MSG_ERROR([You must use either CLN and GMP. Please pick one.])
272 if test $cvc4_use_cln = 1 && test $cvc4_use_gmp = 1; then
274 AC_MSG_ERROR([You cannot use both CLN and GMP. Please pick one.])
277 # try GMP, fail if not found; GMP is required for both CLN and for GMP
279 AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP (libgmp) not found, see http://gmplib.org/])])
281 if test $cvc4_use_cln = 1; then
282 # [mdeters] The PKG_CHECK_MODULES macro isn't customizable and doesn't fail
283 # gracefully. You can only specify it once for a given library name. That
284 # is, even on separate if/else branches, you can't put
285 # PKG_CHECK_MODULES([CLN], ...). That's why things are so convoluted here,
286 # we have to have PKG_CHECK_MODULES _exactly_ once in configure.ac !
287 PKG_CHECK_MODULES([CLN], [cln >= 1.2.2],
290 AC_LINK_IFELSE([AC_LANG_PROGRAM([[#include <cln/cln.h>]], [[cln::cl_F pi = "3.1415926";]])])
293 [if test $cvc4_use_cln = 0; then
295 AC_MSG_NOTICE([CLN not installed (or too old) or pkgconfig missing, will use gmp])
298 AC_MSG_ERROR([CLN not installed (or too old) or pkgconfig missing])
303 if test $cvc4_use_cln = 0; then
304 # try GMPXX, fail if not found
305 AC_CHECK_LIB(gmpxx, __gmpz_init, , [AC_MSG_ERROR([GNU MP C++ library (libgmpxx) not found, see http://gmplib.org/])])
308 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }$CLN_CFLAGS"
309 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }$CLN_CFLAGS"
310 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }$CLN_CFLAGS"
311 LIBS="$CLN_LIBS${LIBS:+ $LIBS}"
315 if test $cvc4_cln_or_gmp = cln; then
316 AC_DEFINE_UNQUOTED(CVC4_CLN_IMP, [], [Defined if using the CLN multi-precision arithmetic library.])
318 AC_DEFINE_UNQUOTED(CVC4_GMP_IMP, [], [Defined if using the GMP multi-precision arithmetic library.])
320 AM_CONDITIONAL([CVC4_CLN_IMP], [test $cvc4_cln_or_gmp = cln])
321 AM_CONDITIONAL([CVC4_GMP_IMP], [test $cvc4_cln_or_gmp = gmp])
323 # construct the build string
324 AC_MSG_CHECKING([for appropriate build string])
325 if test -z "$ac_confdir"; then
328 build_type=`$ac_confdir/config/build-type $with_build $btargs $cvc4_cln_or_gmp`
329 if test "$custom_build_profile" = yes; then
330 if test "$with_build" = default; then
331 build_type=`$ac_confdir/config/build-type custom $btargs $cvc4_cln_or_gmp`
334 AC_MSG_RESULT($build_type)
336 # Require building in target and build-specific build directory:
338 # If the configure script is invoked from the top-level source
339 # directory, it creates a suitable build directory (based on the build
340 # architecture and build profile from $build_type), changes into it,
341 # and reinvokes itself. CVC4_CONFIGURE_IN_BUILDS is an envariable
342 # that breaks any possibility of infinite recursion in this process.
343 AC_MSG_CHECKING([what dir to configure])
344 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
345 AC_MSG_RESULT([this one (in builds/)])
346 elif test "$CVC4_CONFIGURE_AT_TOP_LEVEL" = yes; then
347 AC_MSG_RESULT([builds/$target/$build_type])
349 if test -z "$ac_srcdir"; then
350 mkbuilddir=./config/mkbuilddir
352 mkbuilddir=$ac_srcdir/config/mkbuilddir
354 $as_echo "$mkbuilddir $target $build_type"
355 source $mkbuilddir "$target" "$build_type"
356 $as_echo "cd builds/$target/$build_type"
357 cd "builds/$target/$build_type"
358 CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS
359 echo "$SHELL ../../../configure ${config_cmdline[[@]]}"
360 "$SHELL" "`pwd`/../../../configure" "${config_cmdline[[@]]}"
363 if test $exitval -eq 0; then
364 cat >config.reconfig <<EOF
366 # Generated by configure, `date`
367 # This script is part of CVC4.
369 cd "\`dirname \\"\$0\\"\`"
371 if test -d builds; then :; else echo 'No builds/ directory!' >&2; exit; fi
373 current=(\`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]*\\)/\\(.*\\),\\1 \\2,'\`)
377 echo "reconfiguring in builds/\$arch/\$build..."
378 cd "builds/\$arch/\$build"
379 echo ./config.status "\$@"
380 ./config.status "\$@"]
382 chmod +x config.reconfig
384 ln -sf "$target/$build_type/config.log" "builds/config.log"
387 AC_MSG_RESULT([this one (user-specified)])
392 # Unpack standard build types. Any particular options can be overriden with
393 # --enable/disable-X options
394 case "$with_build" in
395 production) # highly optimized, no assertions, no tracing, dumping
400 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
401 if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=3 ; fi
402 if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
403 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
404 if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
405 if test -z "${enable_replay+set}" ; then enable_replay=no ; fi
406 if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi
407 if test -z "${enable_proof+set}" ; then enable_proof=no ; fi
408 if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi
409 if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
410 if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
412 debug) # unoptimized, debug symbols, assertions, tracing, dumping
413 CVC4CPPFLAGS='-DCVC4_DEBUG'
414 CVC4CXXFLAGS='-fno-inline'
415 CVC4CFLAGS='-fno-inline'
417 FLAG_VISIBILITY_HIDDEN=
418 if test -z "${enable_optimized+set}" ; then enable_optimized=no ; fi
419 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
420 if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
421 if test -z "${enable_replay+set}" ; then enable_replay=yes ; fi
422 if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi
423 if test -z "${enable_proof+set}" ; then enable_proof=no ; fi
424 if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi
425 if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
426 if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
428 default) # moderately optimized, assertions, tracing, dumping
433 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
434 if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=2 ; fi
435 if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
436 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
437 if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
438 if test -z "${enable_replay+set}" ; then enable_replay=yes ; fi
439 if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi
440 if test -z "${enable_proof+set}" ; then enable_proof=no ; fi
441 if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi
442 if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
443 if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
445 competition) # maximally optimized, no assertions, no tracing, no dumping, muzzled
446 CVC4CPPFLAGS='-DCVC4_COMPETITION_MODE'
447 CVC4CXXFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
448 CVC4CFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
450 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
451 if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=9 ; fi
452 if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
453 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no ; fi
454 if test -z "${enable_statistics+set}" ; then enable_statistics=no ; fi
455 if test -z "${enable_replay+set}" ; then enable_replay=no ; fi
456 if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi
457 if test -z "${enable_proof+set}" ; then enable_proof=no ; fi
458 if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi
459 if test -z "${enable_dumping+set}" ; then enable_dumping=no ; fi
460 if test -z "${enable_muzzle+set}" ; then enable_muzzle=yes ; fi
461 if test -z "${user_specified_enable_or_disable_shared}"; then enable_shared=no; fi
462 if test -z "${user_specified_enable_or_disable_static}"; then enable_static=yes; fi
463 if test -z "${enable_static_binary+set}"; then enable_static_binary=yes ; fi
466 AC_MSG_FAILURE([unknown build profile: $with_build])
469 if test -z "${OPTLEVEL+set}"; then OPTLEVEL=3; fi
471 AM_CONDITIONAL([CVC4_BUILD_PROFILE_PRODUCTION], [test "$with_build" = production])
472 AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEBUG], [test "$with_build" = debug])
473 AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEFAULT], [test "$with_build" = default])
474 AM_CONDITIONAL([CVC4_BUILD_PROFILE_COMPETITION], [test "$with_build" = competition])
476 # permit a static binary
477 AC_MSG_CHECKING([whether to build a static binary])
478 AC_ARG_ENABLE([static-binary],
479 [AS_HELP_STRING([--enable-static-binary],
480 [build a fully statically-linked binary [default=no]])])
481 if test -z "${enable_static_binary+set}"; then
482 enable_static_binary=no
484 AC_MSG_RESULT([$enable_static_binary])
485 if test "$enable_static_binary" = yes; then
486 if test "$target_vendor" = apple; then
487 if test -z "$MAC_STATIC_BINARY_MANUAL_OVERRIDE"; then
488 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)]])
490 AC_MSG_WARN([MAC_STATIC_BINARY_MANUAL_OVERRIDE was set!])
491 AC_MSG_WARN([Will make a static binary during this build. Note that it may fail!])
494 if test "$enable_static" != yes; then
496 AC_MSG_WARN([forcing static-library building, --enable-static-binary given])
500 AC_MSG_CHECKING([whether to support proofs in libcvc4])
502 AC_ARG_ENABLE([proof],
503 [AS_HELP_STRING([--enable-proof],
504 [support proof generation])])
505 if test -z "${enable_proof+set}"; then
508 AC_MSG_RESULT([$enable_proof])
510 if test "$enable_proof" = yes; then
511 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROOF"
514 AC_MSG_CHECKING([whether to optimize libcvc4])
516 AC_ARG_ENABLE([optimized],
517 [AS_HELP_STRING([--enable-optimized],
518 [optimize the build])])
520 if test -z "${enable_optimized+set}"; then
524 AC_MSG_RESULT([$enable_optimized])
526 if test "$enable_optimized" = yes; then
527 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O$OPTLEVEL"
528 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O$OPTLEVEL"
530 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O0"
531 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O0"
534 AC_MSG_CHECKING([whether to include debugging symbols in libcvc4])
536 AC_ARG_ENABLE([debug-symbols],
537 [AS_HELP_STRING([--disable-debug-symbols],
538 [do not include debug symbols in libcvc4])])
540 if test -z "${enable_debug_symbols+set}"; then
541 enable_debug_symbols=yes
544 AC_MSG_RESULT([$enable_debug_symbols])
546 if test "$enable_debug_symbols" = yes; then
547 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-ggdb3"
548 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-ggdb3"
551 AC_MSG_CHECKING([whether to include statistics are turned on in libcvc4])
553 AC_ARG_ENABLE([statistics],
554 [AS_HELP_STRING([--disable-statistics],
555 [do not include statistics in libcvc4])])
557 if test -z "${enable_statistics+set}"; then
558 enable_statistics=yes
561 AC_MSG_RESULT([$enable_statistics])
563 if test "$enable_statistics" = yes; then
564 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_STATISTICS_ON"
567 AC_MSG_CHECKING([whether the replay feature should be turned on in libcvc4])
569 AC_ARG_ENABLE([replay],
570 [AS_HELP_STRING([--disable-replay],
571 [turn off the replay feature in libcvc4])])
573 if test -z "${enable_replay+set}"; then
577 AC_MSG_RESULT([$enable_replay])
579 if test "$enable_replay" = yes; then
580 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_REPLAY"
583 AC_MSG_CHECKING([whether to include assertions in build])
585 AC_ARG_ENABLE([assertions],
586 [AS_HELP_STRING([--disable-assertions],
587 [turn off assertions in build])])
589 if test -z "${enable_assertions+set}"; then
590 enable_assertions=yes
593 AC_MSG_RESULT([$enable_assertions])
595 if test "$enable_assertions" = yes; then
596 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_ASSERTIONS"
598 # turn off regular C assert() also
599 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DNDEBUG"
602 AC_MSG_CHECKING([whether to do a traceable build of CVC4])
603 AC_ARG_ENABLE([tracing],
604 [AS_HELP_STRING([--disable-tracing],
605 [remove all tracing code from CVC4])])
607 if test -z "${enable_tracing+set}"; then
611 AC_MSG_RESULT([$enable_tracing])
613 if test "$enable_tracing" = yes; then
614 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_TRACING"
617 AC_MSG_CHECKING([whether to do a dump-capable build of CVC4])
618 AC_ARG_ENABLE([dumping],
619 [AS_HELP_STRING([--disable-dumping],
620 [remove all dumping code from CVC4])])
622 if test -z "${enable_dumping+set}"; then
626 AC_MSG_RESULT([$enable_dumping])
628 if test "$enable_dumping" = yes; then
629 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DUMPING"
632 AC_MSG_CHECKING([whether to do a muzzled build of CVC4])
633 AC_ARG_ENABLE([muzzle],
634 [AS_HELP_STRING([--enable-muzzle],
635 [completely silence CVC4; remove ALL non-result output from build])])
637 if test -z "${enable_muzzle+set}"; then
641 AC_MSG_RESULT([$enable_muzzle])
643 if test "$enable_muzzle" = yes; then
644 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_MUZZLE"
647 AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4])
648 AC_ARG_ENABLE([coverage],
649 [AS_HELP_STRING([--enable-coverage],
650 [build with support for gcov coverage testing])])
652 if test -z "${enable_coverage+set}"; then
656 AC_MSG_RESULT([$enable_coverage])
658 if test "$enable_coverage" = yes; then
659 # For coverage testing, we prefer:
660 # --enable-static --disable-shared --disable-static-binary
661 # If the user didn't specify these, we force them here. If the
662 # user specified them in opposite phase, give warnings that they
663 # shouldn't do that, or bomb out.
664 if test "$user_specified_enable_or_disable_shared" != yes; then
666 AC_MSG_WARN([turning off shared library building due to --enable-coverage])
667 elif test "$enable_shared" = yes; then
669 AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-shared])
670 AC_MSG_WARN([gcov does not support shared libraries, so only your static libraries will be coverage-testable.])
671 AC_MSG_WARN([Your cvc4 driver and testing binaries will not be coverage-testable.])
674 if test "${enable_static_binary+set}" = set -a "$enable_static_binary" = yes; then
676 AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-static-binary])
677 AC_MSG_WARN([Your cvc4 driver and testing binaries will be fully-statically linked and may not be coverage-testable.])
680 if test "$user_specified_enable_or_disable_static" != yes; then
682 AC_MSG_WARN([turning on static library building due to --enable-coverage])
683 elif test "$enable_static" != yes; then
684 AC_MSG_ERROR([--enable-coverage and --disable-static are incompatible; gcov only supports static libraries.])
687 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COVERAGE"
688 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }--coverage"
689 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }--coverage"
690 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }--coverage"
693 AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4])
695 AC_ARG_ENABLE([profiling],
696 [AS_HELP_STRING([--enable-profiling],
697 [build with support for gprof profiling])])
699 if test -z "${enable_profiling+set}"; then
703 AC_MSG_RESULT([$enable_profiling])
705 if test "$enable_profiling" = yes; then
706 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROFILING"
707 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-pg"
708 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-pg"
709 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }-pg"
712 # Check for libglpk (defined in config/glpk.m4)
714 [AS_HELP_STRING([--with-glpk],
715 [use GLPK simplex solver])], [], [with_glpk=])
717 if test $have_libglpk -eq 1; then
718 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_GLPK"
720 AM_CONDITIONAL([CVC4_USE_GLPK], [test $have_libglpk -eq 1])
721 AC_SUBST([GLPK_LIBS])
723 # Check to see if this version/architecture of GNU C++ explicitly
724 # instantiates __gnu_cxx::hash<uint64_t> or not. Some do, some don't.
725 # See src/util/hash.h.
726 AC_MSG_CHECKING([whether __gnu_cxx::hash<uint64_t> is already specialized])
728 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
730 #include <ext/hash_map>
731 namespace __gnu_cxx { template<> struct hash<uint64_t> {}; }])],
732 [AC_MSG_RESULT([no]); CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_NEED_HASH_UINT64_T"],
733 [AC_MSG_RESULT([yes])])
736 # Check whether "long" and "int64_t" are distinct types w.r.t. overloading.
737 # Even if they have the same size, they can be distinct, and some platforms
738 # can have problems with ambiguous function calls when auto-converting
739 # int64_t to long, and others will complain if you overload a function
740 # that takes an int64_t with one that takes a long (giving a redefinition
741 # error). So we have to keep both happy. Probably the same underlying
742 # issue as the hash specialization above, but let's check separately
744 AC_MSG_CHECKING([for the relationship between long and int64_t])
746 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
749 void foo(int64_t) {}])],
750 [AC_MSG_RESULT([no relationship detected]); CVC4_NEED_INT64_T_OVERLOADS=1],
751 [AC_MSG_RESULT([typedef or similar]); CVC4_NEED_INT64_T_OVERLOADS=0])
753 AC_SUBST([CVC4_NEED_INT64_T_OVERLOADS])
755 AC_MSG_CHECKING([for the pb_ds namespace])
757 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
758 #include <ext/pb_ds/priority_queue.hpp>
759 typedef pb_ds::priority_queue<void, void, void> pq;])],
760 [CVC4_PB_DS_NAMESPACE=pb_ds],
761 [AC_COMPILE_IFELSE([AC_LANG_SOURCE([
762 #include <ext/pb_ds/priority_queue.hpp>
763 typedef __gnu_pbds::priority_queue<void, void, void> pq;])],
764 [CVC4_PB_DS_NAMESPACE=__gnu_pbds],
765 [AC_MSG_ERROR([cannot find required priority_queue in either __gnu_pbds or pb_ds namespace.
767 If you're using a non-GCC compiler (such as clang), you may need to explicitly
768 use the GNU standard C++ library by passing:
769 CXXFLAGS='-stdlib=libstdc++' CPPFLAGS='-stdlib=libstdc++'
770 as arguments to this configure script.
771 This is the case on Mac OS Mavericks, for example.])])])
773 AC_MSG_RESULT([$CVC4_PB_DS_NAMESPACE])
774 AC_DEFINE_UNQUOTED(CVC4_PB_DS_NAMESPACE, ${CVC4_PB_DS_NAMESPACE}, [The namespace for pb_ds data structures.])
776 # for information: http://gcc.gnu.org/bugzilla/show_bug.cgi?id=36612
777 AC_MSG_CHECKING([whether pb_ds has bug 36612])
779 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
780 #define __throw_container_error inline __throw_container_error
781 #define __throw_insert_error inline __throw_insert_error
782 #define __throw_join_error inline __throw_join_error
783 #define __throw_resize_error inline __throw_resize_error
784 #include <ext/pb_ds/exception.hpp>
786 [CVC4_GCC_HAS_PB_DS_BUG=1; bugverb=is],
787 [CVC4_GCC_HAS_PB_DS_BUG=0; bugverb="is not"])
789 AC_MSG_RESULT([bug $bugverb present])
790 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])
792 # Check for ANTLR runantlr script (defined in config/antlr.m4)
795 CVC4_CXX_OPTION([-Werror], [WERROR])
796 CVC4_C_OPTION([-Werror], [C_WERROR])
797 CVC4_CXX_OPTION([-Wno-deprecated], [WNO_DEPRECATED])
798 CVC4_C_OPTION([-Wno-deprecated], [C_WNO_DEPRECATED])
799 CVC4_CXX_OPTION([-Wno-conversion-null], [WNO_CONVERSION_NULL])
800 CVC4_CXX_OPTION([-Wno-tautological-compare], [WNO_TAUTOLOGICAL_COMPARE])
801 CVC4_CXX_OPTION([-Wno-parentheses], [WNO_PARENTHESES])
802 CVC4_CXX_OPTION([-Wno-uninitialized], [WNO_UNINITIALIZED])
803 CVC4_CXX_OPTION([-Wno-unused-variable], [WNO_UNUSED_VARIABLE])
804 CVC4_CXX_OPTION([-fno-strict-aliasing], [FNO_STRICT_ALIASING])
806 AC_SUBST([WNO_CONVERSION_NULL])
807 AC_SUBST([WNO_TAUTOLOGICAL_COMPARE])
808 AC_SUBST([WNO_PARENTHESES])
809 AC_SUBST([WNO_UNINITIALIZED])
810 AC_SUBST([WNO_UNUSED_VARIABLE])
811 AC_SUBST([FNO_STRICT_ALIASING])
813 # On Mac, we have to fix the visibility of standard library symbols.
814 # Otherwise, exported template instantiations---even though explicitly
815 # CVC4_PUBLIC, can be generated as symbols with internal-only linkage.
816 # Presumably, Apple is distributing a libstdc++ that is built *without*
817 # --enable-libstdcxx-visibility (?)
818 if test "$target_vendor" = apple; then
819 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-D_GLIBCXX_VISIBILITY_DEFAULT=\"__attribute__((__visibility__(\\\"default\\\")))\""
822 # Tell top-level Makefile to include $(top_srcdir)/personal.mk
823 AC_ARG_ENABLE([personal-make-rules],
824 [AS_HELP_STRING([--enable-personal-make-rules],
825 [include top-level personal.mk (if it exists)])])
826 if test "$enable_personal_make_rules" = yes; then
827 # This allows us to include a personal.mk makefile from every
828 # generated makefile. Named zz_* in order to make sure this
829 # comes last, so it gets other definitions (in particular top_srcdir).
830 zz_cvc4_use_personal_make_rules='yes
832 include $(top_srcdir)/personal.mk
833 $(top_srcdir)/personal.mk:; @touch "$@"'
834 AC_SUBST([zz_cvc4_use_personal_make_rules])
837 # Doxygen configuration
838 AC_ARG_ENABLE([internals-documentation],
839 [AS_HELP_STRING([--enable-internals-documentation],
840 [build Doxygen documentation for static and private member functions])])
841 if test "$enable_internals_documentation" = yes; then
842 DOXYGEN_EXTRACT_PRIVATE=YES
843 DOXYGEN_EXTRACT_STATIC=YES
845 DOXYGEN_EXTRACT_PRIVATE=NO
846 DOXYGEN_EXTRACT_STATIC=NO
848 AC_SUBST([DOXYGEN_EXTRACT_PRIVATE])
849 AC_SUBST([DOXYGEN_EXTRACT_STATIC])
855 DX_INIT_DOXYGEN($PACKAGE_NAME, config/doxygen.cfg, $srcdir/doc/doxygen)
857 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])
858 AC_ARG_VAR(CXXTEST, [path to CxxTest installation])
862 AC_ARG_WITH([cxxtest-dir],
863 [AS_HELP_STRING([--with-cxxtest-dir=DIR], [path to CxxTest installation])],
864 [CXXTEST="$withval"])
866 # In the case of "./configure --with-cxxtest-dir=../cxxtest" (or other
867 # relative path) and having switched the configure directory (see above),
868 # search with respect to the top source dir, not the build dir
869 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes -a -n "$CXXTEST"; then
872 *) CXXTEST="$srcdir/$CXXTEST" ;;
876 AC_ARG_VAR(LFSC, [path to LFSC proof checker])
877 AC_ARG_VAR(LFSCARGS, [arguments to pass to LFSC proof checker])
878 if test -z "$LFSC"; then
879 AC_CHECK_PROGS(LFSC, lfsc, [], [])
881 AC_CHECK_PROG(LFSC, "$LFSC", [], [])
883 AM_CONDITIONAL([PROOF_REGRESSIONS], [test -n "$LFSC" -a "$enable_proof" = yes])
884 if test -n "$LFSC" -a "$enable_proof" = yes; then
885 TESTS_ENVIRONMENT="${TESTS_ENVIRONMENT:+$TESTS_ENVIRONMENT }LFSC=\"$LFSC $LFSCARGS\""
886 RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--proof"
888 AC_SUBST([TESTS_ENVIRONMENT])
889 AC_SUBST([RUN_REGRESSION_ARGS])
890 if test -z "$LFSC"; then
891 support_proof_tests='no, lfsc proof checker unavailable'
892 elif test "$enable_proof" = yes; then
893 support_proof_tests='yes, proof regression tests enabled'
895 support_proof_tests='no, proof generation disabled for this build'
901 AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH])
902 if test -z "$CXXTESTGEN"; then
903 AC_PATH_PROG(CXXTESTGEN, cxxtestgen.py, [], [$CXXTEST:$PATH])
905 if test -z "$CXXTESTGEN"; then
906 AC_PATH_PROG(CXXTESTGEN, cxxtestgen, [], [$CXXTEST:$PATH])
908 if test "$enable_unit_testing" = "no"; then
909 AC_MSG_NOTICE([unit tests disabled by user request.])
912 elif test -z "$CXXTESTGEN"; then
913 AC_MSG_NOTICE([unit tests disabled, could not find cxxtestgen.pl or cxxtestgen.py or cxxtestgen])
914 elif test -z "$CXXTEST"; then
915 CXXTEST=`dirname "$CXXTESTGEN"`
916 AC_MSG_CHECKING([for location of CxxTest headers])
917 if test -e "$CXXTEST/cxxtest/TestRunner.h"; then
918 AC_MSG_RESULT([$CXXTEST])
920 if test -e "/usr/include/cxxtest/TestRunner.h"; then
921 AC_MSG_RESULT([/usr/include])
923 AC_MSG_RESULT([not found])
924 AC_MSG_WARN([unit tests disabled, CxxTest headers not found.])
931 if test "$enable_unit_testing" = yes -a -z "$CXXTESTGEN"; then
932 AC_MSG_ERROR([--enable-unit-testing given but cxxtest not found.])
935 AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"])
937 AC_ARG_VAR(TEST_CPPFLAGS, [CPPFLAGS to use when testing (default=$CPPFLAGS)])
938 AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)])
939 AC_ARG_VAR(TEST_LDFLAGS, [LDFLAGS to use when testing (default=$LDFLAGS)])
941 AC_ARG_VAR(PERL, [PERL interpreter (used when testing)])
943 if test -n "$CXXTEST"; then
944 if test -z "$PERL"; then
945 AC_CHECK_PROGS(PERL, perl, perl, [])
947 AC_CHECK_PROG(PERL, "$PERL", "$PERL", [])
950 if test -z "$PERL"; then
951 AC_MSG_WARN([unit tests disabled, perl not found.])
957 AC_ARG_VAR(PYTHON, [PYTHON interpreter (used for building legacy Java library interface)])
959 if test -z "$PYTHON"; then
960 AC_CHECK_PROGS(PYTHON, python, python, [])
962 AC_CHECK_PROG(PYTHON, "$PYTHON", "$PYTHON", [])
965 if test -z "$PYTHON"; then
966 AC_MSG_WARN([python not found, cannot build libcvc4compat_java (the legacy Java interface).])
971 # Checks for libraries.
973 AC_SEARCH_LIBS([clock_gettime], [rt],
974 [AC_DEFINE([HAVE_CLOCK_GETTIME], [1],
975 [Defined to 1 if clock_gettime() is supported by the platform.])],
976 [AC_LIBOBJ([clock_gettime])])
977 AC_CHECK_FUNC([strtok_r], [AC_DEFINE([HAVE_STRTOK_R], [1],
978 [Defined to 1 if strtok_r() is supported by the platform.])],
979 [AC_LIBOBJ([strtok_r])])
980 AC_CHECK_FUNC([ffs], [AC_DEFINE([HAVE_FFS], [1],
981 [Defined to 1 if ffs() is supported by the platform.])],
984 # Check for antlr C++ runtime (defined in config/antlr.m4)
987 # Check for user preferences for language bindings to build, and for
988 # build support. The arg list is the default set if unspecified by
989 # the user (the actual built set is the subset that appears to be
990 # supported by the build host).
991 CVC4_CHECK_BINDINGS([c java])dnl csharp perl php python ruby tcl ocaml])
993 # Checks for header files and their contents.
994 AC_CHECK_HEADERS([getopt.h unistd.h])
996 # Checks for typedefs, structures, and compiler characteristics.
998 # these are bad macros, they clash with system header <stdint.h> !!
1004 # guard against double-inclusion of the autoheader
1005 AH_TOP([#ifndef __CVC4__CVC4AUTOCONFIG_H
1006 #define __CVC4__CVC4AUTOCONFIG_H])
1007 AH_BOTTOM([#endif /* __CVC4__CVC4AUTOCONFIG_H */])
1009 AC_CHECK_DECLS([optreset], [], [], [#include <getopt.h>])
1011 # check with which standard strerror_r() complies
1014 # require boost library
1017 # look for boost threading library
1018 AC_ARG_WITH([portfolio],
1019 AS_HELP_STRING([--with-portfolio], [build the multithreaded portfolio version of CVC4 (pcvc4)]))
1020 cvc4_save_LDFLAGS="$LDFLAGS"
1021 if test "$enable_static_binary" = yes; then
1022 LDFLAGS="-static $LDFLAGS"
1024 cvc4_has_threads=yes
1025 AC_ARG_ENABLE([thread-support],
1026 AS_HELP_STRING([--disable-thread-support], [do not support multithreaded-capable library]))
1027 if test "$enable_thread_support" = no; then
1029 if test "$with_portfolio" = yes; then
1030 AC_MSG_ERROR([user gave both --with-portfolio and --disable-thread-support, which are contradictory])
1033 BOOST_THREADS([], [AC_MSG_WARN([disabling multithreaded support])
1034 cvc4_has_threads=no])
1036 LDFLAGS="$cvc4_save_LDFLAGS"
1037 if test $cvc4_has_threads = no; then
1038 if test "$enable_thread_support" = yes; then
1039 AC_MSG_ERROR([user gave --enable-thread-support but could not build with threads; maybe boost threading library is missing?])
1041 if test "$with_portfolio" = yes; then
1042 AC_MSG_ERROR([user gave --with-portfolio but could not build with threads; maybe boost threading library is missing?])
1046 if test "$with_portfolio" != yes; then
1049 AM_CONDITIONAL([CVC4_BUILD_PCVC4], [test "$with_portfolio" = yes])
1050 if test "$with_portfolio" = yes; then
1051 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PORTFOLIO"
1054 # Check for libreadline (defined in config/readline.m4)
1055 AC_ARG_WITH([readline], [AS_HELP_STRING([--with-readline], [support the readline library])], [], [with_readline=check])
1056 # make the flags as close as possible to the final flags, because the Boost
1057 # flags can bring in a different, incompatible readline library than we'd
1058 # get otherwise (e.g. on Mac, where there are commonly two different readlines,
1059 # one in /usr and one in /opt/local)
1060 cvc4_rlcheck_save_CPPFLAGS="$CPPFLAGS"
1061 cvc4_rlcheck_save_CXXFLAGS="$CXXFLAGS"
1062 cvc4_rlcheck_save_CFLAGS="$CFLAGS"
1063 cvc4_rlcheck_save_LDFLAGS="$LDFLAGS"
1064 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
1065 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS $WNO_DEPRECATED"
1066 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS $C_WNO_DEPRECATED -fexceptions"
1067 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
1068 CVC4_CHECK_FOR_READLINE
1069 CPPFLAGS="$cvc4_rlcheck_save_CPPFLAGS"
1070 CXXFLAGS="$cvc4_rlcheck_save_CXXFLAGS"
1071 CFLAGS="$cvc4_rlcheck_save_CFLAGS"
1072 LDFLAGS="$cvc4_rlcheck_save_LDFLAGS"
1073 AC_DEFINE_UNQUOTED([HAVE_LIBREADLINE], $have_libreadline, [Define to 1 to use libreadline])
1074 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])
1075 AC_SUBST([READLINE_LIBS])
1077 # Whether to build compatibility library
1078 CVC4_BUILD_LIBCOMPAT=yes
1079 AC_ARG_WITH([compat],
1080 AS_HELP_STRING([--with-compat], [build compatibility library (CVC3 API layer)]),
1081 [if test "$withval" = no; then CVC4_BUILD_LIBCOMPAT=no; fi])
1082 AC_MSG_CHECKING([whether to build compatibility library (CVC3 API layer)])
1083 if test "$CVC4_BUILD_LIBCOMPAT" = yes; then
1084 AC_MSG_RESULT([yes])
1086 AC_MSG_RESULT([no, disabled by user])
1088 AC_SUBST(CVC4_BUILD_LIBCOMPAT)
1089 AM_CONDITIONAL([CVC4_BUILD_LIBCOMPAT], [test "$CVC4_BUILD_LIBCOMPAT" = yes])
1091 # Check for availability of TLS support (e.g. __thread storage class)
1092 AC_MSG_CHECKING([whether to use compiler-supported TLS if available])
1093 AC_ARG_ENABLE([tls], AS_HELP_STRING([--disable-tls], [don't use compiler-native TLS]))
1094 if test $cvc4_has_threads = no; then
1095 # We disable TLS entirely by simply telling the build system that
1096 # the empty string is the __thread keyword.
1097 AC_MSG_RESULT([multithreading disabled])
1098 CVC4_TLS_SUPPORTED=1
1100 CVC4_TLS_explanation='disabled (no multithreading support)'
1102 if test -z "${enable_tls+set}" || test "$enable_tls" = "yes"; then
1103 AC_MSG_RESULT([yes])
1104 AX_TLS([CVC4_TLS=$ac_cv_tls], [CVC4_TLS=])
1109 if test -n "$CVC4_TLS"; then
1110 CVC4_TLS_SUPPORTED=1
1111 CVC4_TLS_explanation="$CVC4_TLS"
1113 CVC4_TLS_explanation='pthread_getspecific()'
1114 CVC4_TLS_SUPPORTED=0
1117 AC_SUBST([CVC4_TLS])
1118 AC_SUBST([CVC4_TLS_SUPPORTED])
1120 # Whether to compile with google profiling tools
1121 cvc4_use_google_perftools=0
1125 [--with-google-perftools],
1126 [use Google Performance Tools]
1128 [if test "$withval" != no; then
1129 cvc4_use_google_perftools=1
1133 AC_MSG_CHECKING([whether to link in google perftools libraries])
1134 if test $cvc4_use_google_perftools = 1; then
1135 AC_MSG_RESULT([yes])
1136 AC_CHECK_LIB([tcmalloc], [MallocExtension_GetAllocatedSize], , [AC_MSG_ERROR([cannot link google-perftools test program with -ltcmalloc])], [-lpthread])
1137 AC_CHECK_LIB([profiler], [ProfilerStart], , [AC_MSG_ERROR([cannot link google-perftools test program with -lprofiler])], [-lpthread])
1139 AC_MSG_RESULT([no (user didn't request it)])
1143 AC_ARG_VAR(JAVA, [Java interpreter (used when testing Java interface)])
1144 AC_ARG_VAR(JAVAC, [Java compiler (used when building and testing Java interface)])
1145 AC_ARG_VAR(JAVAH, [Java compiler (used when building and testing Java interface)])
1146 AC_ARG_VAR(JAR, [Jar archiver (used when building Java interface)])
1147 if test "$cvc4_build_java_bindings"; then
1149 if test -z "$JAVA"; then
1150 AC_CHECK_PROGS(JAVA, java, java, [])
1152 AC_CHECK_PROG(JAVA, "$JAVA", "$JAVA", [])
1154 if test -z "$JAVAC"; then
1155 AC_CHECK_PROGS(JAVAC, javac gcj, javac, [])
1156 if test "$JAVAC" = gcj; then JAVAC='gcj -C'; fi
1158 AC_CHECK_PROG(JAVAC, "$JAVAC", "$JAVAC", [])
1160 if test -z "$JAVAH"; then
1161 AC_CHECK_PROGS(JAVAH, javah gcjh, javah, [])
1163 AC_CHECK_PROG(JAVAH, "$JAVAH", "$JAVAH", [])
1165 if test -z "$JAR"; then
1166 AC_CHECK_PROGS(JAR, jar, jar, [])
1168 AC_CHECK_PROG(JAR, "$JAR", "$JAR", [])
1172 # on Mac OS X, Java doesn't like the .so module extension; it wants .dylib
1173 module=no eval CVC4_JAVA_MODULE_EXT="$shrext_cmds"
1174 if test -z "$CVC4_JAVA_MODULE_EXT"; then
1175 CVC4_JAVA_MODULE_EXT=.so
1177 AC_SUBST([CVC4_JAVA_MODULE_EXT])
1179 # Prepare configure output
1181 if test "$enable_shared" = yes; then BUILDING_SHARED=1; else BUILDING_SHARED=0; fi
1182 if test "$enable_static" = yes; then BUILDING_STATIC=1; else BUILDING_STATIC=0; fi
1183 if test "$enable_static_binary" = yes; then STATIC_BINARY=1; else STATIC_BINARY=0; fi
1184 AC_SUBST(BUILDING_SHARED)
1185 AC_SUBST(BUILDING_STATIC)
1186 AC_SUBST(STATIC_BINARY)
1187 AM_CONDITIONAL([STATIC_BINARY], [test "$enable_static_binary" = yes])
1188 AM_CONDITIONAL([COVERAGE_ENABLED], [test "$enable_coverage" = yes])
1190 AM_CONDITIONAL([CVC4_DEBUG], [test "$with_build" = debug])
1191 AM_CONDITIONAL([CVC4_TRACING], [test "$enable_tracing" = yes])
1193 AC_SUBST(CVC4_LIBRARY_VERSION)
1194 AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
1195 AC_SUBST(CVC4_COMPAT_LIBRARY_VERSION)
1196 AC_SUBST(CVC4_BINDINGS_LIBRARY_VERSION)
1198 AC_DEFINE_UNQUOTED(CVC4_MAJOR, ${CVC4_MAJOR}, [Major component of the version of CVC4.])
1199 AC_DEFINE_UNQUOTED(CVC4_MINOR, ${CVC4_MINOR}, [Minor component of the version of CVC4.])
1200 AC_DEFINE_UNQUOTED(CVC4_RELEASE, ${CVC4_RELEASE}, [Release component of the version of CVC4.])
1201 AC_DEFINE_UNQUOTED(CVC4_EXTRAVERSION, ["${CVC4_EXTRAVERSION}"], [Extraversion component of the version of CVC4.])
1202 AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full release string for CVC4.])
1204 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
1205 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
1206 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions"
1207 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
1209 # visibility flag not supported for Windows builds
1210 # also increase default stack size for Windows binaries
1212 (*mingw*) FLAG_VISIBILITY_HIDDEN=
1213 cvc4_LDFLAGS=-Wl,--stack,134217728
1214 pcvc4_LDFLAGS=-Wl,--stack,134217728
1217 AC_SUBST(FLAG_VISIBILITY_HIDDEN)
1218 AC_SUBST(cvc4_LDFLAGS)
1219 AC_SUBST(pcvc4_LDFLAGS)
1221 AM_CONDITIONAL(WHITE_AND_BLACK_TESTS, [test -z "$FLAG_VISIBILITY_HIDDEN"])
1223 # remember the command line used for configure
1224 AC_SUBST(cvc4_config_cmdline)
1228 # When automake scans Makefiles, it complains about non-standard make
1229 # features (including GNU extensions), and breaks GNU Make's
1230 # "if/endif" construct, replacing the "if" with AM_CONDITIONAL if
1231 # constructs. automake even follows "include" and messes with
1232 # included Makefiles.
1234 # CVC4 assumes GNU Make and we want to use GNU Make if/endifs, so we
1235 # have to hide some included Makefiles with GNU extensions. We do
1236 # this by defining mk_include as an autoconf substitution and then
1237 # using "@mk_include@ other_makefile" in Makefile.am to include
1238 # makefiles with GNU extensions; this hides them from automake.
1240 AC_SUBST(mk_include)
1241 # Similar trickery for "if"
1249 # This is used to _always_ comment out rules in automake makefiles, but
1250 # still trigger certain automake behavior; see test/unit/Makefile.am.
1251 AM_CONDITIONAL([CVC4_FALSE], [false])
1253 # set up substitutions for src/util/{rational,integer}.h.in
1254 if test $cvc4_cln_or_gmp = cln; then
1261 AC_SUBST(CVC4_USE_CLN_IMP)
1262 AC_SUBST(CVC4_USE_GMP_IMP)
1264 # month/year for man pages
1265 MAN_DATE=`date '+%B %Y'`
1271 m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | grep -v '^contrib/alttheoryskel/' | sort | sed 's,\.am$,,'])
1274 if test $cvc4_has_threads = yes; then
1275 support_multithreaded='with boost threading library'
1276 AM_CONDITIONAL([CVC4_HAS_THREADS], [true])
1277 AC_SUBST([CVC4_HAS_THREADS], 1)
1279 support_multithreaded='no'
1280 AM_CONDITIONAL([CVC4_HAS_THREADS], [false])
1281 AC_SUBST([CVC4_HAS_THREADS], 0)
1284 AM_CONDITIONAL([CVC4_NEEDS_REPLACEMENT_FUNCTIONS], [test -n "$LIBOBJS"])
1286 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
1287 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
1288 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/tls.h])
1290 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template])
1291 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5])
1292 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3_template])
1293 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc_template])
1294 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc_template])
1295 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3])
1296 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3])
1300 # Final information to the user
1303 if test "$custom_build_profile" = yes; then
1304 if test "$with_build" = default; then
1307 with_build="$with_build (customized)"
1311 support_unit_tests='cxxtest not found; unit tests not supported'
1312 if test -n "$CXXTEST"; then
1313 support_unit_tests='unit testing infrastructure enabled in build directory'
1314 elif test "$enable_unit_testing" = no; then
1315 support_unit_tests='unit testing disabled by user'
1318 if test "$enable_optimized" = yes; then
1319 optimized="yes, at level $OPTLEVEL"
1324 if test $cvc4_cln_or_gmp = cln; then
1325 mplibrary='cln (GPL)'
1326 licensewarn="${licensewarn}Please note that CVC4 will be built against the Class Library for
1327 Numbers (CLN). This library is covered under the GPL, so use of this
1328 build of CVC4 will be more restrictive than CVC4's license would
1329 normally suggest. For full details of CLN and its license, please visit
1330 http://www.ginac.de/CLN/
1331 To build CVC4 with GMP instead (which is covered under the more permissive
1332 LGPL), configure --without-cln.
1335 if test $with_portfolio = yes; then
1336 licensewarn="${licensewarn}
1337 WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
1338 WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
1340 Note that CLN is UNSAFE FOR USE in parallel contexts!
1341 This build of CVC4 cannot be used safely as a portfolio solver.
1342 since the result of building with CLN will include numerous race
1343 conditions on the refcounts internal to CLN.
1345 WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
1346 WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
1351 mplibrary='gmp (LGPL)'
1354 CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="$CVC4_COMPAT_LIBRARY_VERSION"
1355 CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="$CVC4_BINDINGS_LIBRARY_VERSION"
1356 if test "$CVC4_BUILD_LIBCOMPAT" = no; then
1357 CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="N/A"
1359 if test -z "$CVC4_LANGUAGE_BINDINGS"; then
1360 CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="N/A"
1363 bindings_to_be_built=none
1364 if test -n "$CVC4_LANGUAGE_BINDINGS"; then
1365 bindings_to_be_built="$CVC4_LANGUAGE_BINDINGS"
1366 if test -z "$SWIG"; then
1367 bindings_to_be_built="$bindings_to_be_built (for CVC3 compatibility layer only; SWIG not found)"
1375 Build profile: $with_build
1376 Build ID : $build_type
1377 Optimized : $optimized
1378 Debug symbols: $enable_debug_symbols
1379 Proof : $enable_proof
1380 Statistics : $enable_statistics
1381 Replay : $enable_replay
1382 Assertions : $enable_assertions
1383 Tracing : $enable_tracing
1384 Dumping : $enable_dumping
1385 Muzzle : $enable_muzzle
1387 Unit tests : $support_unit_tests
1388 Proof tests : $support_proof_tests
1389 gcov support : $enable_coverage
1390 gprof support: $enable_profiling
1391 Readline : $with_readline
1393 Static libs : $enable_static
1394 Shared libs : $enable_shared
1395 Static binary: $enable_static_binary
1396 Compat lib : $CVC4_BUILD_LIBCOMPAT
1397 Bindings : $bindings_to_be_built
1399 Multithreaded: $support_multithreaded
1400 TLS support : $CVC4_TLS_explanation
1401 Portfolio : $with_portfolio
1403 MP library : $mplibrary
1406 CPPFLAGS : $CPPFLAGS
1407 CXXFLAGS : $CXXFLAGS
1412 libcvc4 version : $CVC4_LIBRARY_VERSION
1413 libcvc4parser version : $CVC4_PARSER_LIBRARY_VERSION
1414 libcvc4compat version : $CVC4_COMPAT_LIBRARY_VERSION_or_nobuild
1415 libcvc4bindings version: $CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild
1417 Install into : $prefix
1419 ${licensewarn}Now just type make, followed by make check or make install, as you like.
1423 if test -n "$CVC4_UNSUPPORTED_LANGUAGE_BINDINGS"; then
1425 AC_MSG_WARN([You are electing to build unsupported language binding(s): $CVC4_UNSUPPORTED_LANGUAGE_BINDINGS])
1426 AC_MSG_WARN([Please be aware that these bindings may not compile, or work, and the interface to CVC4 via])
1427 AC_MSG_WARN([these bindings may change drastically in upcoming releases of CVC4.])
1431 if test -n "$CVC4_INTEGRITY_WARNING"; then
1433 AC_MSG_WARN($CVC4_INTEGRITY_WARNING)
1434 AC_MSG_WARN([Please run "make check" after building to ensure integrity of the binary and library])