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, 1) 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 proof 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 to see if this version/architecture of GNU C++ explicitly
712 # instantiates __gnu_cxx::hash<uint64_t> or not. Some do, some don't.
713 # See src/util/hash.h.
714 AC_MSG_CHECKING([whether __gnu_cxx::hash<uint64_t> is already specialized])
716 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
718 #include <ext/hash_map>
719 namespace __gnu_cxx { template<> struct hash<uint64_t> {}; }])],
720 [AC_MSG_RESULT([no]); CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_NEED_HASH_UINT64_T"],
721 [AC_MSG_RESULT([yes])])
724 # Check whether "long" and "int64_t" are distinct types w.r.t. overloading.
725 # Even if they have the same size, they can be distinct, and some platforms
726 # can have problems with ambiguous function calls when auto-converting
727 # int64_t to long, and others will complain if you overload a function
728 # that takes an int64_t with one that takes a long (giving a redefinition
729 # error). So we have to keep both happy. Probably the same underlying
730 # issue as the hash specialization above, but let's check separately
732 AC_MSG_CHECKING([for the relationship between long and int64_t])
734 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
737 void foo(int64_t) {}])],
738 [AC_MSG_RESULT([no relationship detected]); CVC4_NEED_INT64_T_OVERLOADS=1],
739 [AC_MSG_RESULT([typedef or similar]); CVC4_NEED_INT64_T_OVERLOADS=0])
741 AC_SUBST([CVC4_NEED_INT64_T_OVERLOADS])
743 # Check for ANTLR runantlr script (defined in config/antlr.m4)
746 CVC4_CXX_OPTION([-Wno-conversion-null], [WNO_CONVERSION_NULL])
747 CVC4_CXX_OPTION([-Wno-uninitialized], [WNO_UNINITIALIZED])
748 CVC4_CXX_OPTION([-Wno-unused-variable], [WNO_UNUSED_VARIABLE])
749 CVC4_CXX_OPTION([-fno-strict-aliasing], [FNO_STRICT_ALIASING])
750 AC_SUBST([WNO_CONVERSION_NULL])
751 AC_SUBST([WNO_UNINITIALIZED])
752 AC_SUBST([WNO_UNUSED_VARIABLE])
753 AC_SUBST([FNO_STRICT_ALIASING])
755 # On Mac, we have to fix the visibility of standard library symbols.
756 # Otherwise, exported template instantiations---even though explicitly
757 # CVC4_PUBLIC, can be generated as symbols with internal-only linkage.
758 # Presumably, Apple is distributing a libstdc++ that is built *without*
759 # --enable-libstdcxx-visibility (?)
760 if test "$target_vendor" = apple; then
761 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-D_GLIBCXX_VISIBILITY_DEFAULT=\"__attribute__((__visibility__(\\\"default\\\")))\""
764 # Doxygen configuration
765 AC_ARG_ENABLE([internals-documentation],
766 [AS_HELP_STRING([--enable-internals-documentation],
767 [build Doxygen documentation for static and private member functions])])
768 if test "$enable_internals_documentation" = yes; then
769 DOXYGEN_EXTRACT_PRIVATE=YES
770 DOXYGEN_EXTRACT_STATIC=YES
772 DOXYGEN_EXTRACT_PRIVATE=NO
773 DOXYGEN_EXTRACT_STATIC=NO
775 AC_SUBST([DOXYGEN_EXTRACT_PRIVATE])
776 AC_SUBST([DOXYGEN_EXTRACT_STATIC])
782 DX_INIT_DOXYGEN($PACKAGE_NAME, config/doxygen.cfg, $srcdir/doc/doxygen)
784 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])
785 AC_ARG_VAR(CXXTEST, [path to CxxTest installation])
789 AC_ARG_WITH([cxxtest-dir],
790 [AS_HELP_STRING([--with-cxxtest-dir=DIR], [path to CxxTest installation])],
791 [CXXTEST="$withval"])
793 # In the case of "./configure --with-cxxtest-dir=../cxxtest" (or other
794 # relative path) and having switched the configure directory (see above),
795 # search with respect to the top source dir, not the build dir
796 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes -a -n "$CXXTEST"; then
799 *) CXXTEST="$srcdir/$CXXTEST" ;;
803 AC_ARG_VAR(LFSC, [path to LFSC proof checker])
804 AC_ARG_VAR(LFSCARGS, [arguments to pass to LFSC proof checker])
805 if test -z "$LFSC"; then
806 AC_CHECK_PROGS(LFSC, lfsc, [], [])
808 AC_CHECK_PROG(LFSC, "$LFSC", [], [])
810 AM_CONDITIONAL([PROOF_REGRESSIONS], [test -n "$LFSC" -a "$enable_proof" = yes])
811 if test -n "$LFSC" -a "$enable_proof" = yes; then
812 TESTS_ENVIRONMENT="${TESTS_ENVIRONMENT:+$TESTS_ENVIRONMENT }LFSC=\"$LFSC $LFSCARGS\""
813 RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--proof"
815 AC_SUBST([TESTS_ENVIRONMENT])
816 AC_SUBST([RUN_REGRESSION_ARGS])
817 if test -z "$LFSC"; then
818 support_proof_tests='no, lfsc proof checker unavailable'
819 elif test "$enable_proof" = yes; then
820 support_proof_tests='yes, proof regression tests enabled'
822 support_proof_tests='no, proof generation disabled for this build'
828 AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH])
829 if test -z "$CXXTESTGEN"; then
830 AC_PATH_PROG(CXXTESTGEN, cxxtestgen.py, [], [$CXXTEST:$PATH])
832 if test -z "$CXXTESTGEN"; then
833 AC_PATH_PROG(CXXTESTGEN, cxxtestgen, [], [$CXXTEST:$PATH])
835 if test "$enable_unit_testing" = "no"; then
836 AC_MSG_NOTICE([unit tests disabled by user request.])
839 elif test -z "$CXXTESTGEN"; then
840 AC_MSG_NOTICE([unit tests disabled, could not find cxxtestgen.pl or cxxtestgen.py or cxxtestgen])
841 elif test -z "$CXXTEST"; then
842 CXXTEST=`dirname "$CXXTESTGEN"`
843 AC_MSG_CHECKING([for location of CxxTest headers])
844 if test -e "$CXXTEST/cxxtest/TestRunner.h"; then
845 AC_MSG_RESULT([$CXXTEST])
847 if test -e "/usr/include/cxxtest/TestRunner.h"; then
848 AC_MSG_RESULT([/usr/include])
850 AC_MSG_RESULT([not found])
851 AC_MSG_WARN([unit tests disabled, CxxTest headers not found.])
858 if test "$enable_unit_testing" = yes -a -z "$CXXTESTGEN"; then
859 AC_MSG_ERROR([--enable-unit-testing given but cxxtest not found.])
862 AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"])
864 AC_ARG_VAR(TEST_CPPFLAGS, [CPPFLAGS to use when testing (default=$CPPFLAGS)])
865 AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)])
866 AC_ARG_VAR(TEST_LDFLAGS, [LDFLAGS to use when testing (default=$LDFLAGS)])
868 AC_ARG_VAR(PERL, [PERL interpreter (used when testing)])
870 if test -n "$CXXTEST"; then
871 if test -z "$PERL"; then
872 AC_CHECK_PROGS(PERL, perl, perl, [])
874 AC_CHECK_PROG(PERL, "$PERL", "$PERL", [])
877 if test -z "$PERL"; then
878 AC_MSG_WARN([unit tests disabled, perl not found.])
884 AC_ARG_VAR(PYTHON, [PYTHON interpreter (used for building legacy Java library interface)])
886 if test -z "$PYTHON"; then
887 AC_CHECK_PROGS(PYTHON, python, python, [])
889 AC_CHECK_PROG(PYTHON, "$PYTHON", "$PYTHON", [])
892 if test -z "$PYTHON"; then
893 AC_MSG_WARN([python not found, cannot build libcvc4compat_java (the legacy Java interface).])
898 # Checks for libraries.
900 AC_SEARCH_LIBS([clock_gettime], [rt],
901 [AC_DEFINE([HAVE_CLOCK_GETTIME], [1],
902 [Defined to 1 if clock_gettime() is supported by the platform.])],
903 [AC_LIBOBJ([clock_gettime])])
904 AC_CHECK_FUNC([strtok_r], [AC_DEFINE([HAVE_STRTOK_R], [1],
905 [Defined to 1 if strtok_r() is supported by the platform.])],
906 [AC_LIBOBJ([strtok_r])])
907 AC_CHECK_FUNC([ffs], [AC_DEFINE([HAVE_FFS], [1],
908 [Defined to 1 if ffs() is supported by the platform.])],
911 # Check for the presence of CUDD libraries
914 # Check for antlr C++ runtime (defined in config/antlr.m4)
917 # Check for user preferences for language bindings to build, and for
918 # build support. The arg list is the default set if unspecified by
919 # the user (the actual built set is the subset that appears to be
920 # supported by the build host).
921 CVC4_CHECK_BINDINGS([c java])dnl csharp perl php python ruby tcl ocaml])
923 # Checks for header files and their contents.
924 AC_CHECK_HEADERS([getopt.h unistd.h])
926 # Checks for typedefs, structures, and compiler characteristics.
928 # these are bad macros, they clash with system header <stdint.h> !!
934 AC_CHECK_DECLS([optreset], [], [], [#include <getopt.h>])
936 # check with which standard strerror_r() complies
939 # require boost library
942 # look for boost threading library
943 AC_ARG_WITH([portfolio],
944 AS_HELP_STRING([--with-portfolio], [build the multithreaded portfolio version of CVC4 (pcvc4)]))
945 cvc4_save_LDFLAGS="$LDFLAGS"
946 if test "$enable_static_binary" = yes; then
947 LDFLAGS="-static $LDFLAGS"
950 AC_ARG_ENABLE([thread-support],
951 AS_HELP_STRING([--disable-thread-support], [do not support multithreaded-capable library]))
952 if test "$enable_thread_support" = no; then
954 if test "$with_portfolio" = yes; then
955 AC_MSG_ERROR([user gave both --with-portfolio and --disable-thread-support, which are contradictory])
958 BOOST_THREADS([], [AC_MSG_WARN([disabling multithreaded support])
959 cvc4_has_threads=no])
961 LDFLAGS="$cvc4_save_LDFLAGS"
962 if test $cvc4_has_threads = no; then
963 if test "$enable_thread_support" = yes; then
964 AC_MSG_ERROR([user gave --enable-thread-support but could not build with threads; maybe boost threading library is missing?])
966 if test "$with_portfolio" = yes; then
967 AC_MSG_ERROR([user gave --with-portfolio but could not build with threads; maybe boost threading library is missing?])
971 if test "$with_portfolio" != yes; then
974 AM_CONDITIONAL([CVC4_BUILD_PCVC4], [test "$with_portfolio" = yes])
975 if test "$with_portfolio" = yes; then
976 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PORTFOLIO"
979 # Check for libreadline (defined in config/readline.m4)
980 AC_ARG_WITH([readline], [AS_HELP_STRING([--with-readline], [support the readline library])], [], [with_readline=check])
981 # make the flags as close as possible to the final flags, because the Boost
982 # flags can bring in a different, incompatible readline library than we'd
983 # get otherwise (e.g. on Mac, where there are commonly two different readlines,
984 # one in /usr and one in /opt/local)
985 cvc4_rlcheck_save_CPPFLAGS="$CPPFLAGS"
986 cvc4_rlcheck_save_CXXFLAGS="$CXXFLAGS"
987 cvc4_rlcheck_save_CFLAGS="$CFLAGS"
988 cvc4_rlcheck_save_LDFLAGS="$LDFLAGS"
989 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
990 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
991 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions"
992 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
993 CVC4_CHECK_FOR_READLINE
994 CPPFLAGS="$cvc4_rlcheck_save_CPPFLAGS"
995 CXXFLAGS="$cvc4_rlcheck_save_CXXFLAGS"
996 CFLAGS="$cvc4_rlcheck_save_CFLAGS"
997 LDFLAGS="$cvc4_rlcheck_save_LDFLAGS"
998 AC_DEFINE_UNQUOTED([HAVE_LIBREADLINE], $have_libreadline, [Define to 1 to use libreadline])
999 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])
1000 AC_SUBST([READLINE_LIBS])
1002 # Whether to build compatibility library
1003 CVC4_BUILD_LIBCOMPAT=yes
1004 AC_ARG_WITH([compat],
1005 AS_HELP_STRING([--with-compat], [build compatibility library (CVC3 API layer)]),
1006 [if test "$withval" = no; then CVC4_BUILD_LIBCOMPAT=no; fi])
1007 AC_MSG_CHECKING([whether to build compatibility library (CVC3 API layer)])
1008 if test "$CVC4_BUILD_LIBCOMPAT" = yes; then
1009 AC_MSG_RESULT([yes])
1011 AC_MSG_RESULT([no, disabled by user])
1013 AC_SUBST(CVC4_BUILD_LIBCOMPAT)
1014 AM_CONDITIONAL([CVC4_BUILD_LIBCOMPAT], [test "$CVC4_BUILD_LIBCOMPAT" = yes])
1016 # Check for availability of TLS support (e.g. __thread storage class)
1017 AC_MSG_CHECKING([whether to use compiler-supported TLS if available])
1018 AC_ARG_ENABLE([tls], AS_HELP_STRING([--disable-tls], [don't use compiler-native TLS]))
1019 if test $cvc4_has_threads = no; then
1020 # We disable TLS entirely by simply telling the build system that
1021 # the empty string is the __thread keyword.
1022 AC_MSG_RESULT([multithreading disabled])
1023 CVC4_TLS_SUPPORTED=1
1025 CVC4_TLS_explanation='disabled (no multithreading support)'
1027 if test -z "${enable_tls+set}" || test "$enable_tls" = "yes"; then
1028 AC_MSG_RESULT([yes])
1029 AX_TLS([CVC4_TLS=$ac_cv_tls], [CVC4_TLS=])
1034 if test -n "$CVC4_TLS"; then
1035 CVC4_TLS_SUPPORTED=1
1036 CVC4_TLS_explanation="$CVC4_TLS"
1038 CVC4_TLS_explanation='pthread_getspecific()'
1039 CVC4_TLS_SUPPORTED=0
1042 AC_SUBST([CVC4_TLS])
1043 AC_SUBST([CVC4_TLS_SUPPORTED])
1045 # Whether to compile with google profiling tools
1046 cvc4_use_google_perftools=0
1050 [--with-google-perftools],
1051 [use Google Performance Tools]
1053 [if test "$withval" != no; then
1054 cvc4_use_google_perftools=1
1058 AC_MSG_CHECKING([whether to link in google perftools libraries])
1059 if test $cvc4_use_google_perftools = 1; then
1060 AC_MSG_RESULT([yes])
1061 AC_CHECK_LIB([tcmalloc], [MallocExtension_GetAllocatedSize], , [AC_MSG_ERROR([cannot link google-perftools test program with -ltcmalloc])], [-lpthread])
1062 AC_CHECK_LIB([profiler], [ProfilerStart], , [AC_MSG_ERROR([cannot link google-perftools test program with -lprofiler])], [-lpthread])
1064 AC_MSG_RESULT([no (user didn't request it)])
1068 AC_ARG_VAR(JAVA, [Java interpreter (used when testing Java interface)])
1069 AC_ARG_VAR(JAVAC, [Java compiler (used when building and testing Java interface)])
1070 AC_ARG_VAR(JAVAH, [Java compiler (used when building and testing Java interface)])
1071 AC_ARG_VAR(JAR, [Jar archiver (used when building Java interface)])
1072 if test "$cvc4_build_java_bindings"; then
1074 if test -z "$JAVA"; then
1075 AC_CHECK_PROGS(JAVA, java, java, [])
1077 AC_CHECK_PROG(JAVA, "$JAVA", "$JAVA", [])
1079 if test -z "$JAVAC"; then
1080 AC_CHECK_PROGS(JAVAC, javac gcj, javac, [])
1081 if test "$JAVAC" = gcj; then JAVAC='gcj -C'; fi
1083 AC_CHECK_PROG(JAVAC, "$JAVAC", "$JAVAC", [])
1085 if test -z "$JAVAH"; then
1086 AC_CHECK_PROGS(JAVAH, javah gcjh, javah, [])
1088 AC_CHECK_PROG(JAVAH, "$JAVAH", "$JAVAH", [])
1090 if test -z "$JAR"; then
1091 AC_CHECK_PROGS(JAR, jar, jar, [])
1093 AC_CHECK_PROG(JAR, "$JAR", "$JAR", [])
1097 # Prepare configure output
1099 if test "$enable_shared" = yes; then BUILDING_SHARED=1; else BUILDING_SHARED=0; fi
1100 if test "$enable_static" = yes; then BUILDING_STATIC=1; else BUILDING_STATIC=0; fi
1101 if test "$enable_static_binary" = yes; then STATIC_BINARY=1; else STATIC_BINARY=0; fi
1102 AC_SUBST(BUILDING_SHARED)
1103 AC_SUBST(BUILDING_STATIC)
1104 AC_SUBST(STATIC_BINARY)
1105 AM_CONDITIONAL([STATIC_BINARY], [test "$enable_static_binary" = yes])
1106 AM_CONDITIONAL([COVERAGE_ENABLED], [test "$enable_coverage" = yes])
1108 AM_CONDITIONAL([CVC4_DEBUG], [test "$with_build" = debug])
1109 AM_CONDITIONAL([CVC4_TRACING], [test "$enable_tracing" = yes])
1111 AC_SUBST(CVC4_LIBRARY_VERSION)
1112 AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
1113 AC_SUBST(CVC4_COMPAT_LIBRARY_VERSION)
1114 AC_SUBST(CVC4_BINDINGS_LIBRARY_VERSION)
1116 AC_DEFINE_UNQUOTED(CVC4_MAJOR, ${CVC4_MAJOR}, [Major component of the version of CVC4.])
1117 AC_DEFINE_UNQUOTED(CVC4_MINOR, ${CVC4_MINOR}, [Minor component of the version of CVC4.])
1118 AC_DEFINE_UNQUOTED(CVC4_RELEASE, ${CVC4_RELEASE}, [Release component of the version of CVC4.])
1119 AC_DEFINE_UNQUOTED(CVC4_EXTRAVERSION, ["${CVC4_EXTRAVERSION}"], [Extraversion component of the version of CVC4.])
1120 AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full release string for CVC4.])
1122 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
1123 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
1124 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions"
1125 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
1127 # visibility flag not supported for Windows builds
1128 # also increase default stack size for Windows binaries
1130 (*mingw*) FLAG_VISIBILITY_HIDDEN=
1131 cvc4_LDFLAGS=-Wl,--stack,134217728
1132 pcvc4_LDFLAGS=-Wl,--stack,134217728
1135 AC_SUBST(FLAG_VISIBILITY_HIDDEN)
1136 AC_SUBST(cvc4_LDFLAGS)
1137 AC_SUBST(pcvc4_LDFLAGS)
1141 # When automake scans Makefiles, it complains about non-standard make
1142 # features (including GNU extensions), and breaks GNU Make's
1143 # "if/endif" construct, replacing the "if" with AM_CONDITIONAL if
1144 # constructs. automake even follows "include" and messes with
1145 # included Makefiles.
1147 # CVC4 assumes GNU Make and we want to use GNU Make if/endifs, so we
1148 # have to hide some included Makefiles with GNU extensions. We do
1149 # this by defining mk_include as an autoconf substitution and then
1150 # using "@mk_include@ other_makefile" in Makefile.am to include
1151 # makefiles with GNU extensions; this hides them from automake.
1153 AC_SUBST(mk_include)
1157 # This is used to _always_ comment out rules in automake makefiles, but
1158 # still trigger certain automake behavior; see test/unit/Makefile.am.
1159 AM_CONDITIONAL([CVC4_FALSE], [false])
1161 # set up substitutions for src/util/{rational,integer}.h.in
1162 if test $cvc4_cln_or_gmp = cln; then
1169 AC_SUBST(CVC4_USE_CLN_IMP)
1170 AC_SUBST(CVC4_USE_GMP_IMP)
1172 # month/year for man pages
1173 MAN_DATE=`date '+%B %Y'`
1179 m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | grep -v '^src/prop/cryptominisat/' | sort | sed 's,\.am$,,'])
1182 if test $cvc4_has_threads = yes; then
1183 support_multithreaded='with boost threading library'
1184 AM_CONDITIONAL([CVC4_HAS_THREADS], [true])
1185 AC_SUBST([CVC4_HAS_THREADS], 1)
1187 support_multithreaded='no'
1188 AM_CONDITIONAL([CVC4_HAS_THREADS], [false])
1189 AC_SUBST([CVC4_HAS_THREADS], 0)
1192 AM_CONDITIONAL([CVC4_NEEDS_REPLACEMENT_FUNCTIONS], [test -n "$LIBOBJS"])
1194 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
1195 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
1196 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/tls.h])
1198 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template])
1199 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5])
1200 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3_template])
1201 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc_template])
1202 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc_template])
1203 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3])
1204 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3])
1206 # AC_CONFIG_SUBDIRS([src/prop/cryptominisat])
1210 # Final information to the user
1213 if test "$custom_build_profile" = yes; then
1214 if test "$with_build" = default; then
1217 with_build="$with_build (customized)"
1221 support_unit_tests='cxxtest not found; unit tests not supported'
1222 if test -n "$CXXTEST"; then
1223 support_unit_tests='unit testing infrastructure enabled in build directory'
1224 elif test "$enable_unit_testing" = no; then
1225 support_unit_tests='unit testing disabled by user'
1228 if test "$enable_optimized" = yes; then
1229 optimized="yes, at level $OPTLEVEL"
1234 if test $cvc4_cln_or_gmp = cln; then
1235 mplibrary='cln (GPL)'
1236 licensewarn="${licensewarn}Please note that CVC4 will be built against the Class Library for
1237 Numbers (CLN). This library is covered under the GPL, so use of this
1238 build of CVC4 will be more restrictive than CVC4's license would
1239 normally suggest. For full details of CLN and its license, please visit
1240 http://www.ginac.de/CLN/
1241 To build CVC4 with GMP instead (which is covered under the more permissive
1242 LGPL), configure --without-cln.
1245 if test $with_portfolio = yes; then
1246 licensewarn="${licensewarn}
1247 WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
1248 WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
1250 Note that CLN is UNSAFE FOR USE in parallel contexts!
1251 This build of CVC4 cannot be used safely as a portfolio solver.
1252 since the result of building with CLN will include numerous race
1253 conditions on the refcounts internal to CLN.
1255 WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
1256 WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
1261 mplibrary='gmp (LGPL)'
1264 CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="$CVC4_COMPAT_LIBRARY_VERSION"
1265 CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="$CVC4_BINDINGS_LIBRARY_VERSION"
1266 if test "$CVC4_BUILD_LIBCOMPAT" = no; then
1267 CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="N/A"
1269 if test -z "$CVC4_LANGUAGE_BINDINGS"; then
1270 CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="N/A"
1273 bindings_to_be_built=none
1274 if test -n "$CVC4_LANGUAGE_BINDINGS"; then
1275 bindings_to_be_built="$CVC4_LANGUAGE_BINDINGS"
1276 if test -z "$SWIG"; then
1277 bindings_to_be_built="$bindings_to_be_built (for CVC3 compatibility layer only; SWIG not found)"
1285 Build profile: $with_build
1286 Build ID : $build_type
1287 Optimized : $optimized
1288 Debug symbols: $enable_debug_symbols
1289 Proof : $enable_proof
1290 Statistics : $enable_statistics
1291 Replay : $enable_replay
1292 Assertions : $enable_assertions
1293 Tracing : $enable_tracing
1294 Dumping : $enable_dumping
1295 Muzzle : $enable_muzzle
1297 Unit tests : $support_unit_tests
1298 Proof tests : $support_proof_tests
1299 gcov support : $enable_coverage
1300 gprof support: $enable_profiling
1302 Readline : $with_readline
1304 Static libs : $enable_static
1305 Shared libs : $enable_shared
1306 Static binary: $enable_static_binary
1307 Compat lib : $CVC4_BUILD_LIBCOMPAT
1308 Bindings : $bindings_to_be_built
1310 Multithreaded: $support_multithreaded
1311 TLS support : $CVC4_TLS_explanation
1312 Portfolio : $with_portfolio
1314 MP library : $mplibrary
1316 CPPFLAGS : $CPPFLAGS
1317 CXXFLAGS : $CXXFLAGS
1322 libcvc4 version : $CVC4_LIBRARY_VERSION
1323 libcvc4parser version : $CVC4_PARSER_LIBRARY_VERSION
1324 libcvc4compat version : $CVC4_COMPAT_LIBRARY_VERSION_or_nobuild
1325 libcvc4bindings version: $CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild
1327 Install into : $prefix
1329 ${licensewarn}Now just type make, followed by make check or make install, as you like.
1333 if test -n "$CVC4_UNSUPPORTED_LANGUAGE_BINDINGS"; then
1335 AC_MSG_WARN([You are electing to build unsupported language binding(s): $CVC4_UNSUPPORTED_LANGUAGE_BINDINGS])
1336 AC_MSG_WARN([Please be aware that these bindings may not compile, or work, and the interface to CVC4 via])
1337 AC_MSG_WARN([these bindings may change drastically in upcoming releases of CVC4.])
1341 if test -n "$CVC4_INTEGRITY_WARNING"; then
1343 AC_MSG_WARN($CVC4_INTEGRITY_WARNING)
1344 AC_MSG_WARN([Please run "make check" after building to ensure integrity of the binary and library])