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, 6) 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, [cvc4-bugs@cs.stanford.edu])
15 AC_CONFIG_SRCDIR([src/include/cvc4_public.h])
16 AC_CONFIG_AUX_DIR([config])
17 AC_REQUIRE_AUX_FILE([tap-driver.sh])
18 AC_CONFIG_MACRO_DIR([config])
19 AC_CONFIG_LIBOBJ_DIR([src/lib])
21 m4_ifdef([AM_SILENT_RULES],[AM_SILENT_RULES([yes])])
23 CVC4_MAJOR=_CVC4_MAJOR
24 CVC4_MINOR=_CVC4_MINOR
25 CVC4_RELEASE=_CVC4_RELEASE
26 CVC4_EXTRAVERSION=_CVC4_EXTRAVERSION
27 CVC4_RELEASE_STRING=_CVC4_RELEASE_STRING
29 # Libtool version numbers for libraries
30 # Version numbers are in the form current:revision:age
33 # increment if interfaces have been added, removed or changed
35 # increment if source code has changed
36 # set to zero if current is incremented
38 # increment if interfaces have been added
39 # set to zero if interfaces have been removed
42 # For more information, see:
43 # http://www.gnu.org/software/libtool/manual/libtool.html#Versioning
44 # For guidance on when to change the version number, refer to the
47 m4_define([library_version], [m4_esyscmd([grep -F "$(grep -v '^#' library_versions | awk '{print$][1}' | sed 's,\\,\\\\\\,g' | (while read r; do if echo "]_CVC4_RELEASE_STRING[" | grep -q "^$r\$"; then echo "$r"; exit; fi; done; echo NO_MATCH_FOUND)) " library_versions | awk 'BEGIN {FS=":";OFS=":";RS=" "} /^$1:/ {print$][2,$][3,$][4}' | head -1])])
49 m4_define(_CVC4_LIBRARY_VERSION, library_version([libcvc4]))dnl
50 m4_define(_CVC4_PARSER_LIBRARY_VERSION, library_version([libcvc4parser]))dnl
51 m4_define(_CVC4_COMPAT_LIBRARY_VERSION, library_version([libcvc4compat]))dnl
52 m4_define(_CVC4_BINDINGS_LIBRARY_VERSION, library_version([libcvc4bindings]))dnl
54 m4_define([fatal_error], [m4_errprint(__program__:__file__:__line__[: fatal error: $*
57 m4_ifblank(_CVC4_LIBRARY_VERSION,[fatal_error([no CVC4_LIBRARY_VERSION defined for release version "]_CVC4_RELEASE_STRING[" in library_versions file])])dnl
58 m4_ifblank(_CVC4_PARSER_LIBRARY_VERSION,[fatal_error([no CVC4_PARSER_LIBRARY_VERSION defined for release version "]_CVC4_RELEASE_STRING[" in library_versions file])])dnl
59 m4_ifblank(_CVC4_COMPAT_LIBRARY_VERSION,[fatal_error([no CVC4_COMPAT_LIBRARY_VERSION defined for release version "]_CVC4_RELEASE_STRING[" in library_versions file])])dnl
60 m4_ifblank(_CVC4_BINDINGS_LIBRARY_VERSION,[fatal_error([no CVC4_BINDINGS_LIBRARY_VERSION defined for release version "]_CVC4_RELEASE_STRING[" in library_versions file])])dnl
62 CVC4_LIBRARY_VERSION=_CVC4_LIBRARY_VERSION
63 CVC4_PARSER_LIBRARY_VERSION=_CVC4_PARSER_LIBRARY_VERSION
64 CVC4_COMPAT_LIBRARY_VERSION=_CVC4_COMPAT_LIBRARY_VERSION
65 CVC4_BINDINGS_LIBRARY_VERSION=_CVC4_BINDINGS_LIBRARY_VERSION
67 # Using AX_CXX_COMPILE_STDCXX_11 and the AC_CANONICAL_* macros destroy the
68 # command line you get from $@, which we want later for determining the build
69 # profile. So we save it.
70 # (We can't do our build profile stuff here, or it's not included in the
71 # output... autoconf overrides us on the orderings of some things.)
73 cvc4_config_cmdline="${config_cmdline[[@]]}"
75 # remember if the user set these explicitly (or whether autoconf does)
76 user_specified_enable_or_disable_static=${enable_static+yes}
77 user_specified_enable_or_disable_shared=${enable_shared+yes}
79 if test -e src/include/cvc4_public.h; then
80 CVC4_CONFIGURE_AT_TOP_LEVEL=yes
82 CVC4_CONFIGURE_AT_TOP_LEVEL=no
85 # override autoconf: we don't want it giving us CFLAGS/CXXFLAGS, but we do
86 # want to respect the user's flags
87 if test -z "${CFLAGS+set}"; then CFLAGS=; fi
88 if test -z "${CXXFLAGS+set}"; then CXXFLAGS=; fi
91 AM_MAINTAINER_MODE([enable])
93 # turn off static lib building by default
101 # C++11 support in the compiler is now mandatory. Check for support and add
102 # switches if necessary.
103 AX_CXX_COMPILE_STDCXX_11([ext], [mandatory])
107 if test "$enable_shared" = no -a "$user_specified_enable_or_disable_shared" = yes; then
111 # Features requested by the user
112 AC_MSG_CHECKING([for requested build profile])
114 [AS_HELP_STRING([--with-build=profile],
115 [for profile in {production,debug,competition,personal}])])
117 if test -z "${with_build+set}"; then
118 with_build=production
120 if test -z "${enable_optimized+set}" -a \
121 -z "${enable_debug_symbols+set}" -a \
122 -z "${enable_assertions+set}" -a \
123 -z "${enable_tracing+set}" -a \
124 -z "${enable_dumping+set}" -a \
125 -z "${enable_muzzle+set}" -a \
126 -z "${enable_coverage+set}" -a \
127 -z "${enable_profiling+set}" -a \
128 -z "${enable_statistics+set}" -a \
129 -z "${enable_replay+set}" -a \
130 -z "${with_gmp+set}" -a \
131 -z "${with_cln+set}" -a \
132 -z "${with_glpk+set}" -a \
133 -z "${with_abc+set}" -a \
134 -z "${with_cadical+set}" -a \
135 -z "${with_cryptominisat+set}" -a \
136 -z "${with_lfsc+set}" -a \
137 -z "${with_symfpu+set}"; then
138 custom_build_profile=no
140 custom_build_profile=yes
143 if test -n "${enable_optimized+set}"; then
144 if test "$enable_optimized" = yes; then
145 btargs="$btargs optimized"
147 btargs="$btargs nooptimized"
150 # --enable-staticbinary is an alias for --enable-static-binary
151 if test -n "${enable_staticbinary+set}"; then
152 enable_static_binary="$enable_staticbinary"
154 if test -n "${enable_static_binary+set}"; then
155 if test "$enable_static_binary" = yes; then
156 btargs="$btargs staticbinary"
158 btargs="$btargs nostaticbinary"
161 if test -n "${enable_debug_symbols+set}"; then
162 if test "$enable_debug_symbols" = yes; then
163 btargs="$btargs debugsymbols"
165 btargs="$btargs nodebugsymbols"
168 if test -n "${enable_assertions+set}"; then
169 if test "$enable_assertions" = yes; then
170 btargs="$btargs assertions"
172 btargs="$btargs noassertions"
175 if test -n "${enable_proof+set}"; then
176 if test "$enable_proof" = yes; then
177 btargs="$btargs proof"
179 btargs="$btargs noproof"
182 if test -n "${enable_tracing+set}"; then
183 if test "$enable_tracing" = yes; then
184 btargs="$btargs tracing"
186 btargs="$btargs notracing"
189 if test -n "${enable_dumping+set}"; then
190 if test "$enable_dumping" = yes; then
191 btargs="$btargs dumping"
193 btargs="$btargs nodumping"
196 if test -n "${enable_muzzle+set}"; then
197 if test "$enable_muzzle" = yes; then
198 btargs="$btargs muzzle"
200 btargs="$btargs nomuzzle"
203 if test -n "${enable_coverage+set}"; then
204 if test "$enable_coverage" = yes; then
205 btargs="$btargs coverage"
207 btargs="$btargs nocoverage"
210 if test -n "${enable_profiling+set}"; then
211 if test "$enable_profiling" = yes; then
212 btargs="$btargs profiling"
214 btargs="$btargs noprofiling"
217 if test -n "${enable_statistics+set}"; then
218 if test "$enable_statistics" = yes; then
219 btargs="$btargs statistics"
221 btargs="$btargs nostatistics"
224 if test -n "${enable_replay+set}"; then
225 if test "$enable_replay" = yes; then
226 btargs="$btargs replay"
228 btargs="$btargs noreplay"
231 if test -n "${with_glpk+set}"; then
232 if test "$with_glpk" = yes; then
233 btargs="$btargs glpk"
236 if test -n "${with_abc+set}"; then
237 if test "$with_abc" = yes; then
241 if test -n "${with_cadical+set}"; then
242 if test "$with_cadical" = yes; then
243 btargs="$btargs cadical"
246 if test -n "${with_cryptominisat+set}"; then
247 if test "$with_cryptominisat" = yes; then
248 btargs="$btargs cryptominisat"
251 if test -n "${with_lfsc+set}"; then
252 if test "$with_lfsc" = yes; then
254 btargs="$btargs lfsc"
257 if test -n "${with_symfpu+set}"; then
258 if test "$with_symfpu" = yes; then
259 btargs="$btargs symfpu"
263 AC_MSG_RESULT([$with_build])
265 AM_INIT_AUTOMAKE([1.11 no-define tar-pax parallel-tests color-tests subdir-objects])
266 AC_CONFIG_HEADERS([cvc4autoconfig.h])
268 # automake 1.12 changes the test driver mechanism in a way that is
269 # completely incompatible with 1.11. We figure out here which version
270 # we're using in order to set up test makefiles correctly.
271 # See http://lists.gnu.org/archive/html/automake/2012-04/msg00060.html
272 if test -z "$am__api_version"; then
273 AC_MSG_ERROR([Cannot determine automake API version ?!])
275 case "$am__api_version" in
276 1.11*) automake111=true ;;
277 *) automake111=false ;;
279 AM_CONDITIONAL([AUTOMAKE_1_11], [$automake111])
281 # Initialize libtool's configuration options.
282 # we're not DLL-clean yet (i.e., don't properly use dllexport and dllimport)
283 # _LT_SET_OPTION([LT_INIT],[win32-dll])
286 # Checks for programs.
293 if test $cross_compiling = "no"; then
294 AC_MSG_CHECKING([whether C++ exceptions work])
297 AC_LANG_PROGRAM([#include <exception>], [[
300 throw std::exception();
306 [AC_MSG_RESULT([yes])],
307 [AC_MSG_ERROR([C++ exceptions do not work.])]
311 AC_MSG_WARN([Cross compiling, cannot check whether exceptions work])
321 [use CLN instead of GMP]
324 y|ye|yes|Y|YE|YES) cvc4_use_cln=1 ;;
325 n|no|N|NO) cvc4_use_cln=0 ;;
334 [use GMP instead of CLN]
337 y|ye|yes|Y|YE|YES) cvc4_use_gmp=1 ;;
338 n|no|N|NO) cvc4_use_gmp=0 ;;
343 if test $cvc4_use_cln = 1 -a $cvc4_use_gmp = 1 || test $cvc4_use_cln = 0 -a $cvc4_use_gmp = 0; then
344 AC_MSG_ERROR([You must use either CLN and GMP. Please pick one.])
346 if test $cvc4_use_gmp = 1; then
348 elif test $cvc4_use_gmp = 0; then
350 elif test $cvc4_use_cln = 1; then
352 elif test $cvc4_use_cln = 0; then
356 # try GMP, fail if not found; GMP is required for both CLN and for GMP
358 AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP (libgmp) not found, see http://gmplib.org/])])
360 if test $cvc4_use_cln = 2; then
361 if test "$CVC4_BSD_LICENSED_CODE_ONLY" = 1 -o "$with_portfolio" = yes; then
367 if test $cvc4_use_cln != 0; then
368 # [mdeters] The PKG_CHECK_MODULES macro isn't customizable and doesn't fail
369 # gracefully. You can only specify it once for a given library name. That
370 # is, even on separate if/else branches, you can't put
371 # PKG_CHECK_MODULES([CLN], ...). That's why things are so convoluted here,
372 # we have to have PKG_CHECK_MODULES _exactly_ once in configure.ac !
373 PKG_CHECK_MODULES([CLN], [cln >= 1.2.2],
376 save_CXXFLAGS="$CXXFLAGS"
377 LIBS="$CLN_LIBS $LIBS"
378 CXXFLAGS="$CLN_CFLAGS $CXXFLAGS"
379 AC_LINK_IFELSE([AC_LANG_PROGRAM([[#include <cln/cln.h>]], [[cln::cl_F pi = "3.1415926";]])], [
382 if test $cvc4_use_cln = 1; then
384 AC_MSG_ERROR([CLN installation missing, too old, or not functional for this architecture])
387 AC_MSG_NOTICE([CLN installation missing, too old, or not functional for this architecture, will use gmp instead])
392 CXXFLAGS="$save_CXXFLAGS"
396 [if test $cvc4_use_cln = 1; then
398 AC_MSG_ERROR([CLN not installed (or too old) or pkgconfig missing])
401 AC_MSG_NOTICE([CLN not installed (or too old) or pkgconfig missing, will use gmp])
408 if test $cvc4_use_cln = 0; then
409 # try GMPXX, fail if not found; don't need to link against it, only need its header
411 AC_CHECK_HEADER([gmpxx.h], , [AC_MSG_ERROR([GNU MP C++ library header (gmpxx.h) required but not found, see http://gmplib.org/])])
415 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }$CLN_CFLAGS"
416 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }$CLN_CFLAGS"
417 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }$CLN_CFLAGS"
418 LIBS="$CLN_LIBS${LIBS:+ $LIBS}"
422 if test $cvc4_cln_or_gmp = cln; then
423 AC_DEFINE_UNQUOTED(CVC4_CLN_IMP, [], [Defined if using the CLN multi-precision arithmetic library.])
425 AC_DEFINE_UNQUOTED(CVC4_GMP_IMP, [], [Defined if using the GMP multi-precision arithmetic library.])
427 AM_CONDITIONAL([CVC4_CLN_IMP], [test $cvc4_cln_or_gmp = cln])
428 AM_CONDITIONAL([CVC4_GMP_IMP], [test $cvc4_cln_or_gmp = gmp])
430 # construct the build string
431 AC_MSG_CHECKING([for appropriate build string])
432 if test -z "$ac_confdir"; then
435 build_type=`$ac_confdir/config/build-type $with_build $btargs $cvc4_cln_or_gmp`
436 AC_MSG_RESULT($build_type)
438 # Require building in target and build-specific build directory:
440 # If the configure script is invoked from the top-level source
441 # directory, it creates a suitable build directory (based on the build
442 # architecture and build profile from $build_type), changes into it,
443 # and reinvokes itself. CVC4_CONFIGURE_IN_BUILDS is an envariable
444 # that breaks any possibility of infinite recursion in this process.
445 AC_MSG_CHECKING([what dir to configure])
446 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
447 AC_MSG_RESULT([this one (in builds/)])
448 elif test "$CVC4_CONFIGURE_AT_TOP_LEVEL" = yes; then
449 AC_MSG_RESULT([builds/$target/$build_type])
451 if test -z "$ac_srcdir"; then
452 mkbuilddir=./config/mkbuilddir
454 mkbuilddir=$ac_srcdir/config/mkbuilddir
456 $as_echo "$mkbuilddir $target $build_type"
457 source $mkbuilddir "$target" "$build_type"
458 $as_echo "cd builds/$target/$build_type"
459 cd "builds/$target/$build_type"
460 CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS
461 # Runs the single recursive configure invocation using a relative path.
462 # See https://lists.gnu.org/archive/html/autoconf/2011-04/msg00060.html
463 echo "$SHELL ../../../configure ${config_cmdline[[@]]}"
464 "$SHELL" "../../../configure" "${config_cmdline[[@]]}"
467 if test $exitval -eq 0; then
468 cat >config.reconfig <<EOF
470 # Generated by configure, `date`
471 # This script is part of CVC4.
473 cd "\`dirname \\"\$0\\"\`"
475 if test -d builds; then :; else echo 'No builds/ directory!' >&2; exit; fi
477 current=(\`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]*\\)/\\(.*\\),\\1 \\2,'\`)
481 echo "reconfiguring in builds/\$arch/\$build..."
482 cd "builds/\$arch/\$build"
483 echo ./config.status "\$@"
484 ./config.status "\$@"]
486 chmod +x config.reconfig
488 ln -sf "$target/$build_type/config.log" "builds/config.log"
491 AC_MSG_RESULT([this one (user-specified)])
496 # Unpack standard build types. Any particular options can be overriden with
497 # --enable/disable-X options
498 # Tim: This needs to keep CVC4CPPFLAGS, CVC4CXXFLAGS, etc. set by earlier checks
499 case "$with_build" in
500 production) # highly optimized, no assertions, no tracing, dumping
501 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }"
502 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }"
503 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }"
504 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
505 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
506 if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=3 ; fi
507 if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
508 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no ; fi
509 if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
510 if test -z "${enable_replay+set}" ; then enable_replay=no ; fi
511 if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi
512 if test -z "${enable_proof+set}" ; then enable_proof=yes ; fi
513 if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi
514 if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
515 if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
516 if test -z "${enable_valgrind+set}" ; then enable_valgrind=no ; fi
518 debug) # unoptimized, debug symbols, assertions, tracing, dumping
519 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DEBUG"
520 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-fno-inline"
521 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-fno-inline"
522 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
523 FLAG_VISIBILITY_HIDDEN=
524 if test -z "${enable_optimized+set}" ; then enable_optimized=no ; fi
525 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
526 if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
527 if test -z "${enable_replay+set}" ; then enable_replay=yes ; fi
528 if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi
529 if test -z "${enable_proof+set}" ; then enable_proof=yes ; fi
530 if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi
531 if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
532 if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
533 if test -z "${enable_valgrind+set}" ; then enable_valgrind=optional ; fi
535 default) # moderately optimized, assertions, tracing, dumping
536 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }"
537 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }"
538 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }"
539 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
540 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
541 if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=2 ; fi
542 if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
543 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
544 if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
545 if test -z "${enable_replay+set}" ; then enable_replay=yes ; fi
546 if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi
547 if test -z "${enable_proof+set}" ; then enable_proof=yes ; fi
548 if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi
549 if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
550 if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
551 if test -z "${enable_valgrind+set}" ; then enable_valgrind=no ; fi
553 competition) # maximally optimized, no assertions, no tracing, no dumping, muzzled
554 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COMPETITION_MODE"
555 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs"
556 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs"
557 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
558 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
559 if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=9 ; fi
560 if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
561 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no ; fi
562 if test -z "${enable_statistics+set}" ; then enable_statistics=no ; fi
563 if test -z "${enable_replay+set}" ; then enable_replay=no ; fi
564 if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi
565 if test -z "${enable_proof+set}" ; then enable_proof=no ; fi
566 if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi
567 if test -z "${enable_dumping+set}" ; then enable_dumping=no ; fi
568 if test -z "${enable_muzzle+set}" ; then enable_muzzle=yes ; fi
569 if test -z "${enable_valgrind+set}" ; then enable_valgrind=no ; fi
570 if test -z "${user_specified_enable_or_disable_shared}"; then enable_shared=no; fi
571 if test -z "${user_specified_enable_or_disable_static}"; then enable_static=yes; fi
572 if test -z "${enable_static_binary+set}"; then enable_static_binary=yes ; fi
575 AC_MSG_FAILURE([unknown build profile: $with_build])
578 if test -z "${OPTLEVEL+set}"; then OPTLEVEL=3; fi
580 AM_CONDITIONAL([CVC4_BUILD_PROFILE_PRODUCTION], [test "$with_build" = production])
581 AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEBUG], [test "$with_build" = debug])
582 AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEFAULT], [test "$with_build" = default])
583 AM_CONDITIONAL([CVC4_BUILD_PROFILE_COMPETITION], [test "$with_build" = competition])
585 # permit a static binary
586 AC_MSG_CHECKING([whether to build a static binary])
587 AC_ARG_ENABLE([static-binary],
588 [AS_HELP_STRING([--enable-static-binary],
589 [build a fully statically-linked binary [default=no]])])
590 if test -z "${enable_static_binary+set}"; then
591 enable_static_binary=no
593 AC_MSG_RESULT([$enable_static_binary])
594 if test "$enable_static_binary" = yes; then
595 if test "$target_vendor" = apple; then
596 if test -z "$MAC_STATIC_BINARY_MANUAL_OVERRIDE"; then
597 AC_MSG_ERROR([[Statically-linked binaries are not supported on macOS. See https://developer.apple.com/library/content/qa/qa1118/_index.html . (If you ABSOLUTELY insist on this going forward and you know what you are doing, set MAC_STATIC_BINARY_MANUAL_OVERRIDE=1)]])
599 AC_MSG_WARN([MAC_STATIC_BINARY_MANUAL_OVERRIDE was set!])
600 AC_MSG_WARN([Will make a static binary during this build. Note that it may fail!])
603 if test "$enable_static" != yes; then
605 AC_MSG_WARN([forcing static-library building, --enable-static-binary given])
609 AC_MSG_CHECKING([whether to support proofs in libcvc4])
611 AC_ARG_ENABLE([proof],
612 [AS_HELP_STRING([--disable-proof],
613 [do not support proof generation])])
614 if test -z "${enable_proof+set}"; then
617 AC_MSG_RESULT([$enable_proof])
619 if test "$enable_proof" = yes; then
620 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROOF"
622 AM_CONDITIONAL([CVC4_PROOF], [test "$enable_proof" = yes])
624 AC_MSG_CHECKING([whether to optimize libcvc4])
626 AC_ARG_ENABLE([optimized],
627 [AS_HELP_STRING([--enable-optimized],
628 [optimize the build])])
630 if test -z "${enable_optimized+set}"; then
634 AC_MSG_RESULT([$enable_optimized])
636 if test "$enable_optimized" = yes; then
637 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O$OPTLEVEL"
638 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O$OPTLEVEL"
640 # Use -Og if available (optimizations that do not interfere with debugging),
642 debug_optimization_level="-O0"
643 CVC4_CXX_OPTION([-Og], [debug_optimization_level])
644 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }${debug_optimization_level}"
645 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }${debug_optimization_level}"
648 AC_MSG_CHECKING([whether to include debugging symbols in libcvc4])
650 AC_ARG_ENABLE([debug-symbols],
651 [AS_HELP_STRING([--disable-debug-symbols],
652 [do not include debug symbols in libcvc4])])
654 if test -z "${enable_debug_symbols+set}"; then
655 enable_debug_symbols=yes
658 AC_MSG_RESULT([$enable_debug_symbols])
660 if test "$enable_debug_symbols" = yes; then
661 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-ggdb3"
662 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-ggdb3"
665 AC_MSG_CHECKING([whether to enable Valgrind instrumentation])
667 AC_ARG_ENABLE([valgrind],
668 [AS_HELP_STRING([--enable-valgrind],
669 [enable Valgrind instrumentation])])
671 if test -z "${enable_valgrind+set}"; then
675 AC_MSG_RESULT([$enable_valgrind])
677 if test "$enable_valgrind" != no; then
678 # Valgrind instrumentation is either explicitly enabled (enable_valgrind=yes)
679 # or enabled if available (enable_valgrind=optional)
680 AC_CHECK_HEADER([valgrind/memcheck.h],
681 [CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_VALGRIND"],
682 [if test "$enable_valgrind" = yes; then
683 AC_MSG_ERROR([Need valgrind/memcheck.h to enable Valgrind instrumentation])
685 AC_MSG_NOTICE([valgrind/memcheck.h missing, Valgrind instrumentation disabled])
690 AC_MSG_CHECKING([whether to use the debug context memory manager])
692 AC_ARG_ENABLE([debug-context-memory-manager],
693 [AS_HELP_STRING([--enable-debug-context-memory-manager],
694 [use the debug context memory manager])])
696 if test -z "${enable_debug_context_memory_manager+set}"; then
697 enable_debug_context_memory_manager=no
700 AC_MSG_RESULT([$enable_debug_context_memory_manager])
702 if test "$enable_debug_context_memory_manager" = yes; then
703 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DEBUG_CONTEXT_MEMORY_MANAGER"
706 AC_MSG_CHECKING([whether to include statistics are turned on in libcvc4])
708 AC_ARG_ENABLE([statistics],
709 [AS_HELP_STRING([--disable-statistics],
710 [do not include statistics in libcvc4])])
712 if test -z "${enable_statistics+set}"; then
713 enable_statistics=yes
716 AC_MSG_RESULT([$enable_statistics])
718 if test "$enable_statistics" = yes; then
719 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_STATISTICS_ON"
722 AC_MSG_CHECKING([whether the replay feature should be turned on in libcvc4])
724 AC_ARG_ENABLE([replay],
725 [AS_HELP_STRING([--disable-replay],
726 [turn off the replay feature in libcvc4])])
728 if test -z "${enable_replay+set}"; then
732 AC_MSG_RESULT([$enable_replay])
734 if test "$enable_replay" = yes; then
735 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_REPLAY"
738 AC_MSG_CHECKING([whether to include assertions in build])
740 AC_ARG_ENABLE([assertions],
741 [AS_HELP_STRING([--disable-assertions],
742 [turn off assertions in build])])
744 if test -z "${enable_assertions+set}"; then
745 enable_assertions=yes
748 AC_MSG_RESULT([$enable_assertions])
750 if test "$enable_assertions" = yes; then
751 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_ASSERTIONS"
753 # turn off regular C assert() also
754 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DNDEBUG"
757 AC_MSG_CHECKING([whether to do a traceable build of CVC4])
758 AC_ARG_ENABLE([tracing],
759 [AS_HELP_STRING([--disable-tracing],
760 [remove all tracing code from CVC4])])
762 if test -z "${enable_tracing+set}"; then
766 AC_MSG_RESULT([$enable_tracing])
768 if test "$enable_tracing" = yes; then
769 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_TRACING"
772 AC_MSG_CHECKING([whether to do a dump-capable build of CVC4])
773 AC_ARG_ENABLE([dumping],
774 [AS_HELP_STRING([--disable-dumping],
775 [remove all dumping code from CVC4])])
777 if test -z "${enable_dumping+set}"; then
781 AC_MSG_RESULT([$enable_dumping])
783 if test "$enable_dumping" = yes; then
784 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DUMPING"
787 AC_MSG_CHECKING([whether to do a muzzled build of CVC4])
788 AC_ARG_ENABLE([muzzle],
789 [AS_HELP_STRING([--enable-muzzle],
790 [completely silence CVC4; remove ALL non-result output from build])])
792 if test -z "${enable_muzzle+set}"; then
796 AC_MSG_RESULT([$enable_muzzle])
798 if test "$enable_muzzle" = yes; then
799 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_MUZZLE"
802 AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4])
803 AC_ARG_ENABLE([coverage],
804 [AS_HELP_STRING([--enable-coverage],
805 [build with support for gcov coverage testing])])
807 if test -z "${enable_coverage+set}"; then
809 # make COVERAGE_ON the empty string for makefile conditional function
810 # $(if $(COVERAGE_ON), action1, action2)
814 AC_MSG_RESULT([$enable_coverage])
816 if test "$enable_coverage" = yes; then
817 # For coverage testing, we prefer:
818 # --enable-static --disable-shared --disable-static-binary
819 # If the user didn't specify these, we force them here. If the
820 # user specified them in opposite phase, give warnings that they
821 # shouldn't do that, or bomb out.
823 if test "$user_specified_enable_or_disable_shared" != yes; then
825 AC_MSG_WARN([turning off shared library building due to --enable-coverage])
826 elif test "$enable_shared" = yes; then
828 AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-shared])
829 AC_MSG_WARN([gcov does not support shared libraries, so only your static libraries will be coverage-testable.])
830 AC_MSG_WARN([Your cvc4 driver and testing binaries will not be coverage-testable.])
833 if test "${enable_static_binary+set}" = set -a "$enable_static_binary" = yes; then
835 AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-static-binary])
836 AC_MSG_WARN([Your cvc4 driver and testing binaries will be fully-statically linked and may not be coverage-testable.])
839 if test "$user_specified_enable_or_disable_static" != yes; then
841 AC_MSG_WARN([turning on static library building due to --enable-coverage])
842 elif test "$enable_static" != yes; then
843 AC_MSG_ERROR([--enable-coverage and --disable-static are incompatible; gcov only supports static libraries.])
846 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COVERAGE"
847 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }--coverage"
848 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }--coverage"
849 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }--coverage"
852 AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4])
854 AC_ARG_ENABLE([profiling],
855 [AS_HELP_STRING([--enable-profiling],
856 [build with support for gprof profiling])])
858 if test -z "${enable_profiling+set}"; then
862 AC_MSG_RESULT([$enable_profiling])
864 if test "$enable_profiling" = yes; then
865 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROFILING"
866 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-pg"
867 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-pg"
868 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }-pg"
871 # Check for libglpk (defined in config/glpk.m4)
873 [AS_HELP_STRING([--with-glpk],
874 [use GLPK simplex solver])], [], [with_glpk=])
876 if test $have_libglpk -eq 1; then
877 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_GLPK"
879 AM_CONDITIONAL([CVC4_USE_GLPK], [test $have_libglpk -eq 1])
880 AC_SUBST([GLPK_LDFLAGS])
881 AC_SUBST([GLPK_LIBS])
883 # Build with libabc (defined in config/abc.m4)
885 [AS_HELP_STRING([--with-abc],
886 [use the ABC AIG library])], [], [with_abc=])
888 if test $have_libabc -eq 1; then
889 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_ABC"
891 AM_CONDITIONAL([CVC4_USE_ABC], [test $have_libabc -eq 1])
892 AC_SUBST([ABC_LDFLAGS])
896 # Build with libcadical
897 AC_ARG_WITH([cadical],
898 [AS_HELP_STRING([--with-cadical],
899 [use the CaDiCaL SAT solver])], [], [with_cadical=])
900 CVC4_CHECK_FOR_CADICAL
901 if test $have_libcadical -eq 1; then
902 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_CADICAL"
903 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$CADICAL_HOME/src"
905 AM_CONDITIONAL([CVC4_USE_CADICAL], [test $have_libcadical -eq 1])
906 AC_SUBST([CADICAL_LDFLAGS])
907 AC_SUBST([CADICAL_LIBS])
909 # Build with libcryptominisat
910 AC_ARG_WITH([cryptominisat],
911 [AS_HELP_STRING([--with-cryptominisat],
912 [use the CRYPTOMINISAT sat solver])], [], [with_cryptominisat=])
913 CVC4_CHECK_FOR_CRYPTOMINISAT
914 if test $have_libcryptominisat -eq 1; then
915 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_CRYPTOMINISAT"
916 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$CRYPTOMINISAT_HOME/install/include"
918 AM_CONDITIONAL([CVC4_USE_CRYPTOMINISAT], [test $have_libcryptominisat -eq 1])
919 AC_SUBST([CRYPTOMINISAT_LDFLAGS])
920 AC_SUBST([CRYPTOMINISAT_LIBS])
924 [AS_HELP_STRING([--with-lfsc],
925 [use the LFSC proof checker])], [], [with_lfsc=])
927 if test $have_liblfsc -eq 1; then
928 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_LFSC"
930 AM_CONDITIONAL([CVC4_USE_LFSC], [test $have_liblfsc -eq 1])
931 AC_SUBST([LFSC_LDFLAGS])
932 AC_SUBST([LFSC_LIBS])
935 AC_ARG_WITH([symfpu],
936 [AS_HELP_STRING([--with-symfpu],
937 [use symfpu for floating point solver])], [], [with_symfpu=])
938 CVC4_CHECK_FOR_SYMFPU
939 if test $have_symfpu_headers -eq 1; then
940 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_SYMFPU"
941 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$SYMFPU_HOME"
943 AM_CONDITIONAL([CVC4_USE_SYMFPU], [test $have_symfpu_headers -eq 1])
945 # Check to see if this version/architecture of GNU C++ explicitly
946 # instantiates std::hash<uint64_t> or not. Some do, some don't.
947 # See src/util/hash.h.
948 AC_MSG_CHECKING([whether std::hash<uint64_t> is already specialized])
950 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
952 #include <functional>
953 namespace std { template<> struct hash<uint64_t> {}; }])],
954 [AC_MSG_RESULT([no]); CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_NEED_HASH_UINT64_T"],
955 [AC_MSG_RESULT([yes])])
958 # Check whether "long" and "int64_t" are distinct types w.r.t. overloading.
959 # Even if they have the same size, they can be distinct, and some platforms
960 # can have problems with ambiguous function calls when auto-converting
961 # int64_t to long, and others will complain if you overload a function
962 # that takes an int64_t with one that takes a long (giving a redefinition
963 # error). So we have to keep both happy. Probably the same underlying
964 # issue as the hash specialization above, but let's check separately
966 AC_MSG_CHECKING([for the relationship between long and int64_t])
968 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
971 void foo(int64_t) {}])],
972 [AC_MSG_RESULT([no relationship detected]); CVC4_NEED_INT64_T_OVERLOADS=1],
973 [AC_MSG_RESULT([typedef or similar]); CVC4_NEED_INT64_T_OVERLOADS=0])
975 AC_SUBST([CVC4_NEED_INT64_T_OVERLOADS])
977 # Check for ANTLR runantlr script (defined in config/antlr.m4)
980 CVC4_CXX_OPTION([-Werror], [WERROR])
981 CVC4_C_OPTION([-Werror], [C_WERROR])
982 CVC4_CXX_OPTION([-Wno-deprecated], [WNO_DEPRECATED])
983 CVC4_C_OPTION([-Wno-deprecated], [C_WNO_DEPRECATED])
984 CVC4_CXX_OPTION([-Wno-conversion-null], [WNO_CONVERSION_NULL])
985 CVC4_CXX_OPTION([-Wno-tautological-compare], [WNO_TAUTOLOGICAL_COMPARE])
986 CVC4_CXX_OPTION([-Wno-parentheses], [WNO_PARENTHESES])
987 CVC4_CXX_OPTION([-Wno-uninitialized], [WNO_UNINITIALIZED])
988 CVC4_CXX_OPTION([-Wno-unused-variable], [WNO_UNUSED_VARIABLE])
989 CVC4_CXX_OPTION([-Wsuggest-override], [W_SUGGEST_OVERRIDE])
990 CVC4_CXX_OPTION([-fno-strict-aliasing], [FNO_STRICT_ALIASING])
992 AC_SUBST([WNO_CONVERSION_NULL])
993 AC_SUBST([WNO_TAUTOLOGICAL_COMPARE])
994 AC_SUBST([WNO_PARENTHESES])
995 AC_SUBST([WNO_UNINITIALIZED])
996 AC_SUBST([WNO_UNUSED_VARIABLE])
997 AC_SUBST([W_SUGGEST_OVERRIDE])
998 AC_SUBST([FNO_STRICT_ALIASING])
1000 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }${W_SUGGEST_OVERRIDE}"
1002 # On Mac, we have to fix the visibility of standard library symbols.
1003 # Otherwise, exported template instantiations---even though explicitly
1004 # CVC4_PUBLIC, can be generated as symbols with internal-only linkage.
1005 # Presumably, Apple is distributing a libstdc++ that is built *without*
1006 # --enable-libstdcxx-visibility (?)
1007 if test "$target_vendor" = apple; then
1008 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-D_GLIBCXX_VISIBILITY_DEFAULT=\"__attribute__((__visibility__(\\\"default\\\")))\""
1011 # Tell top-level Makefile to include $(top_srcdir)/personal.mk
1012 AC_ARG_ENABLE([personal-make-rules],
1013 [AS_HELP_STRING([--enable-personal-make-rules],
1014 [include top-level personal.mk (if it exists)])])
1015 if test "$enable_personal_make_rules" = yes; then
1016 # This allows us to include a personal.mk makefile from every
1017 # generated makefile. Named zz_* in order to make sure this
1018 # comes last, so it gets other definitions (in particular top_srcdir).
1019 zz_cvc4_use_personal_make_rules='yes
1022 include $(top_srcdir)/personal.mk
1023 $(top_srcdir)/personal.mk:; @touch "$@"'
1024 AC_SUBST([zz_cvc4_use_personal_make_rules])
1027 # Doxygen configuration
1028 AC_ARG_ENABLE([internals-documentation],
1029 [AS_HELP_STRING([--enable-internals-documentation],
1030 [build Doxygen documentation for static and private member functions])])
1031 if test "$enable_internals_documentation" = yes; then
1032 DOXYGEN_EXTRACT_PRIVATE=YES
1033 DOXYGEN_EXTRACT_STATIC=YES
1035 DOXYGEN_EXTRACT_PRIVATE=NO
1036 DOXYGEN_EXTRACT_STATIC=NO
1038 AC_SUBST([DOXYGEN_EXTRACT_PRIVATE])
1039 AC_SUBST([DOXYGEN_EXTRACT_STATIC])
1045 DX_INIT_DOXYGEN($PACKAGE_NAME, config/doxygen.cfg, $srcdir/doc/doxygen)
1047 AC_ARG_ENABLE([unit-testing], AS_HELP_STRING([--disable-unit-testing], [do not build support for unit testing, even if available]), , [enable_unit_testing=check])
1048 AC_ARG_VAR(CXXTEST, [path to CxxTest installation])
1049 AC_ARG_WITH([cxxtest-dir],
1050 [AS_HELP_STRING([--with-cxxtest-dir=DIR], [path to CxxTest installation])],
1051 [CXXTEST="$withval"])
1054 RUN_REGRESSION_ARGS=
1055 # FIXME currently, unsat core regressions are disabled without LFSC
1056 if test "$with_lfsc" = yes; then
1057 RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--proof"
1059 AC_SUBST([TESTS_ENVIRONMENT])
1060 AC_SUBST([RUN_REGRESSION_ARGS])
1062 AC_ARG_VAR(TEST_CPPFLAGS, [CPPFLAGS to use when testing (default=$CPPFLAGS)])
1063 AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)])
1064 AC_ARG_VAR(TEST_LDFLAGS, [LDFLAGS to use when testing (default=$LDFLAGS)])
1067 if test "$enable_unit_testing" = "no"; then
1068 AC_MSG_NOTICE([unit tests disabled by user request.])
1071 # The latest version of cxxtest distributed from the git repository places
1072 # cxxtest under <cxxtest-root>/bin/cxxtest
1073 AC_PATH_PROGS(CXXTESTGEN,
1074 cxxtestgen.pl cxxtestgen.py cxxtestgen,
1076 AC_MSG_NOTICE([unit tests disabled, \
1077 could not find cxxtestgen.pl or \
1078 cxxtestgen.py or cxxtestgen])
1081 [$CXXTEST:$CXXTEST/bin:$PATH])
1083 if test -n "$CXXTESTGEN" -a "`basename $CXXTESTGEN`" = "cxxtestgen.pl"; then
1084 if test -z "$PERL"; then
1085 AC_CHECK_PROGS(PERL, perl, perl, [])
1087 AC_CHECK_PROG(PERL, "$PERL", "$PERL", [])
1090 if test -z "$PERL"; then
1091 AC_MSG_WARN([unit tests disabled, perl not found.])
1097 # check if CxxTest headers exist and set include paths accordingly
1098 if test -n "$CXXTESTGEN"; then
1099 AC_MSG_CHECKING([for location of CxxTest headers])
1100 if test -n "$CXXTEST"; then
1101 if test -e "$CXXTEST/cxxtest/TestRunner.h"; then
1102 AC_MSG_RESULT([$CXXTEST])
1103 TEST_CPPFLAGS="${TEST_CPPFLAGS} -I$CXXTEST"
1104 TEST_CXXFLAGS="${TEST_CXXFLAGS} -I$CXXTEST"
1106 AC_MSG_RESULT([not found])
1107 AC_MSG_WARN([unit tests disabled, CxxTest headers not found at $CXXTEST.])
1111 # TODO: use more generic way to find cxxtest/TestRunner.h in system headers
1112 elif test -e "/usr/include/cxxtest/TestRunner.h"; then
1113 CXXTEST=/usr/include
1114 AC_MSG_RESULT([$CXXTEST])
1116 CXXTEST=`dirname "$CXXTESTGEN"`
1117 if test -e "$CXXTEST/cxxtest/TestRunner.h"; then
1118 AC_MSG_RESULT([$CXXTEST])
1119 TEST_CPPFLAGS="${TEST_CPPFLAGS} -I$CXXTEST"
1120 TEST_CXXFLAGS="${TEST_CXXFLAGS} -I$CXXTEST"
1122 AC_MSG_RESULT([not found])
1123 AC_MSG_WARN([unit tests disabled, CxxTest headers not found.])
1131 if test "$enable_unit_testing" = yes -a -z "$CXXTESTGEN"; then
1132 AC_MSG_ERROR([--enable-unit-testing given but cxxtest not found.])
1135 AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"])
1137 AC_ARG_VAR(PERL, [PERL interpreter (used when testing)])
1139 AC_ARG_VAR(PYTHON, [PYTHON interpreter (used for building legacy Java library interface)])
1141 if test -z "$PYTHON"; then
1142 AC_CHECK_PROGS(PYTHON, python, python, [])
1144 AC_CHECK_PROG(PYTHON, "$PYTHON", "$PYTHON", [])
1147 if test -z "$PYTHON"; then
1148 AC_MSG_WARN([python not found, cannot build libcvc4compat_java (the legacy Java interface).])
1153 # Checks for libraries.
1155 AC_SEARCH_LIBS([clock_gettime], [rt pthread],
1156 [AC_DEFINE([HAVE_CLOCK_GETTIME], [1],
1157 [Defined to 1 if clock_gettime() is supported by the platform.])],
1158 [AC_LIBOBJ([clock_gettime])])
1159 AC_CHECK_FUNC([strtok_r], [AC_DEFINE([HAVE_STRTOK_R], [1],
1160 [Defined to 1 if strtok_r() is supported by the platform.])])
1161 AC_CHECK_FUNC([ffs], [AC_DEFINE([HAVE_FFS], [1],
1162 [Defined to 1 if ffs() is supported by the platform.])])
1164 AC_LIBOBJ([strtok_r ffs])
1166 # Check for sigaltstack (missing in emscripten and mingw)
1167 AC_CHECK_FUNC([sigaltstack], [AC_DEFINE([HAVE_SIGALTSTACK], [1],
1168 [Defined to 1 if sigaltstack() is supported by the platform.])])
1170 # Check for antlr C++ runtime (defined in config/antlr.m4)
1173 # Check for user preferences for language bindings to build, and for
1174 # build support. The arg list is the default set if unspecified by
1175 # the user (the actual built set is the subset that appears to be
1176 # supported by the build host).
1177 CVC4_CHECK_BINDINGS([c java])dnl csharp perl php python ruby tcl ocaml])
1179 # Checks for header files and their contents.
1180 AC_CHECK_HEADERS([getopt.h unistd.h ext/stdio_filebuf.h])
1182 # Checks for typedefs, structures, and compiler characteristics.
1184 # these are bad macros, they clash with system header <stdint.h> !!
1190 # guard against double-inclusion of the autoheader
1191 AH_TOP([#ifndef __CVC4__CVC4AUTOCONFIG_H
1192 #define __CVC4__CVC4AUTOCONFIG_H])
1193 AH_BOTTOM([#endif /* __CVC4__CVC4AUTOCONFIG_H */])
1195 AC_CHECK_DECLS([optreset], [], [], [#include <getopt.h>])
1197 # check with which standard strerror_r() complies
1200 # require boost library
1203 # look for boost threading library
1204 AC_ARG_WITH([portfolio],
1205 AS_HELP_STRING([--with-portfolio], [build the multithreaded portfolio version of CVC4 (pcvc4)]))
1206 cvc4_save_LDFLAGS="$LDFLAGS"
1207 if test "$enable_static_binary" = yes; then
1208 LDFLAGS="-static $LDFLAGS"
1210 cvc4_has_threads=yes
1211 AC_ARG_ENABLE([thread-support],
1212 AS_HELP_STRING([--disable-thread-support], [do not support multithreaded-capable library]))
1213 if test "$enable_thread_support" = no; then
1215 if test "$with_portfolio" = yes; then
1216 AC_MSG_ERROR([user gave both --with-portfolio and --disable-thread-support, which are contradictory])
1219 BOOST_THREADS([], [AC_MSG_WARN([disabling multithreaded support])
1220 cvc4_has_threads=no])
1222 LDFLAGS="$cvc4_save_LDFLAGS"
1223 if test $cvc4_has_threads = no; then
1224 if test "$enable_thread_support" = yes; then
1225 AC_MSG_ERROR([user gave --enable-thread-support but could not build with threads; maybe boost threading library is missing?])
1227 if test "$with_portfolio" = yes; then
1228 AC_MSG_ERROR([user gave --with-portfolio but could not build with threads; maybe boost threading library is missing?])
1232 if test "$with_portfolio" != yes; then
1235 AM_CONDITIONAL([CVC4_BUILD_PCVC4], [test "$with_portfolio" = yes])
1236 if test "$with_portfolio" = yes; then
1237 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PORTFOLIO"
1239 # see if Boost has thread attributes (should be any version >= 1.50.0)
1240 # non-fatal error if not, but we won't support --thread-stack option
1241 AC_MSG_CHECKING([whether Boost threads support thread attrs])
1243 cvc4_save_CPPFLAGS="$CPPFLAGS"
1244 cvc4_save_LIBS="$LIBS"
1245 cvc4_save_LDFLAGS="$LDFLAGS"
1246 CPPFLAGS="$CPPFLAGS $BOOST_CPPFLAGS"
1247 LIBS="$LIBS $BOOST_THREAD_LIBS"
1248 LDFLAGS="$LDFLAGS $BOOST_THREAD_LDFLAGS"
1249 AC_LINK_IFELSE([AC_LANG_PROGRAM([#include <boost/thread.hpp>],
1250 [boost::thread::attributes attrs; attrs.set_stack_size(10 * 1024 * 1024);])],
1251 [cvc4_boost_has_thread_attr=1;
1252 AC_MSG_RESULT([yes])],
1253 [cvc4_boost_has_thread_attr=0;
1254 AC_MSG_RESULT([no])])
1255 CPPFLAGS="$cvc4_save_CPPFLAGS"
1256 LIBS="$cvc4_save_LIBS"
1257 LDFLAGS="$cvc4_save_LDFLAGS"
1260 cvc4_boost_has_thread_attr=0
1262 AC_DEFINE_UNQUOTED([BOOST_HAS_THREAD_ATTR], $cvc4_boost_has_thread_attr, [Define to 1 if Boost threading library has support for thread attributes])
1264 # Check for libreadline (defined in config/readline.m4)
1265 AC_ARG_WITH([readline], [AS_HELP_STRING([--with-readline], [support the readline library])], [], [with_readline=check])
1266 # make the flags as close as possible to the final flags, because the Boost
1267 # flags can bring in a different, incompatible readline library than we'd
1268 # get otherwise (e.g. on Mac, where there are commonly two different readlines,
1269 # one in /usr and one in /opt/local)
1270 cvc4_rlcheck_save_CPPFLAGS="$CPPFLAGS"
1271 cvc4_rlcheck_save_CXXFLAGS="$CXXFLAGS"
1272 cvc4_rlcheck_save_CFLAGS="$CFLAGS"
1273 cvc4_rlcheck_save_LDFLAGS="$LDFLAGS"
1274 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
1275 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS $WNO_DEPRECATED"
1276 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS $C_WNO_DEPRECATED -fexceptions"
1277 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
1278 CVC4_CHECK_FOR_READLINE
1279 CPPFLAGS="$cvc4_rlcheck_save_CPPFLAGS"
1280 CXXFLAGS="$cvc4_rlcheck_save_CXXFLAGS"
1281 CFLAGS="$cvc4_rlcheck_save_CFLAGS"
1282 LDFLAGS="$cvc4_rlcheck_save_LDFLAGS"
1283 AC_DEFINE_UNQUOTED([HAVE_LIBREADLINE], $have_libreadline, [Define to 1 to use libreadline])
1284 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])
1285 AC_SUBST([READLINE_LIBS])
1287 # Whether to build compatibility library
1288 CVC4_BUILD_LIBCOMPAT=yes
1289 AC_ARG_WITH([compat],
1290 AS_HELP_STRING([--with-compat], [build compatibility library (CVC3 API layer)]),
1291 [if test "$withval" = no; then CVC4_BUILD_LIBCOMPAT=no; fi])
1292 AC_MSG_CHECKING([whether to build compatibility library (CVC3 API layer)])
1293 if test "$CVC4_BUILD_LIBCOMPAT" = yes; then
1294 AC_MSG_RESULT([yes])
1296 AC_MSG_RESULT([no, disabled by user])
1298 AC_SUBST(CVC4_BUILD_LIBCOMPAT)
1299 AM_CONDITIONAL([CVC4_BUILD_LIBCOMPAT], [test "$CVC4_BUILD_LIBCOMPAT" = yes])
1301 # Whether to compile with google profiling tools
1302 cvc4_use_google_perftools=0
1306 [--with-google-perftools],
1307 [use Google Performance Tools]
1309 [if test "$withval" != no; then
1310 cvc4_use_google_perftools=1
1314 AC_MSG_CHECKING([whether to link in google perftools libraries])
1315 if test $cvc4_use_google_perftools = 1; then
1316 AC_MSG_RESULT([yes])
1317 AC_CHECK_LIB([tcmalloc], [MallocExtension_GetAllocatedSize], , [AC_MSG_ERROR([cannot link google-perftools test program with -ltcmalloc])], [-lpthread])
1318 AC_CHECK_LIB([profiler], [ProfilerStart], , [AC_MSG_ERROR([cannot link google-perftools test program with -lprofiler])], [-lpthread])
1320 AC_MSG_RESULT([no (user didn't request it)])
1324 AC_ARG_VAR(JAVA, [Java interpreter (used when testing Java interface)])
1325 AC_ARG_VAR(JAVAC, [Java compiler (used when building and testing Java interface)])
1326 AC_ARG_VAR(JAVAH, [Java compiler (used when building and testing Java interface)])
1327 AC_ARG_VAR(JAR, [Jar archiver (used when building Java interface)])
1328 if test "$cvc4_build_java_bindings"; then
1330 if test -z "$JAVA"; then
1331 AC_CHECK_PROGS(JAVA, java, java, [])
1333 AC_CHECK_PROG(JAVA, "$JAVA", "$JAVA", [])
1335 if test -z "$JAVAC"; then
1336 AC_CHECK_PROGS(JAVAC, javac gcj, javac, [])
1337 if test "$JAVAC" = gcj; then JAVAC='gcj -C'; fi
1339 AC_CHECK_PROG(JAVAC, "$JAVAC", "$JAVAC", [])
1341 if test -z "$JAVAH"; then
1342 AC_CHECK_PROGS(JAVAH, javah gcjh, javah, [])
1344 AC_CHECK_PROG(JAVAH, "$JAVAH", "$JAVAH", [])
1346 if test -z "$JAR"; then
1347 AC_CHECK_PROGS(JAR, jar, jar, [])
1349 AC_CHECK_PROG(JAR, "$JAR", "$JAR", [])
1353 # on Mac OS X, Java doesn't like the .so module extension; it wants .dylib
1354 module=no eval CVC4_JAVA_MODULE_EXT="$shrext_cmds"
1355 if test -z "$CVC4_JAVA_MODULE_EXT"; then
1356 CVC4_JAVA_MODULE_EXT=.so
1358 AC_SUBST([CVC4_JAVA_MODULE_EXT])
1360 # Prepare configure output
1362 if test "$enable_shared" = yes; then BUILDING_SHARED=1; else BUILDING_SHARED=0; fi
1363 if test "$enable_static" = yes; then BUILDING_STATIC=1; else BUILDING_STATIC=0; fi
1364 if test "$enable_static_binary" = yes; then STATIC_BINARY=1; else STATIC_BINARY=0; fi
1365 AC_SUBST(BUILDING_SHARED)
1366 AC_SUBST(BUILDING_STATIC)
1367 AC_SUBST(STATIC_BINARY)
1368 AM_CONDITIONAL([STATIC_BINARY], [test "$enable_static_binary" = yes])
1369 AM_CONDITIONAL([COVERAGE_ENABLED], [test "$enable_coverage" = yes])
1370 AC_SUBST([COVERAGE_ON])
1372 AM_CONDITIONAL([CVC4_DEBUG], [test "$with_build" = debug])
1373 AM_CONDITIONAL([CVC4_TRACING], [test "$enable_tracing" = yes])
1375 AC_SUBST(CVC4_LIBRARY_VERSION)
1376 AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
1377 AC_SUBST(CVC4_COMPAT_LIBRARY_VERSION)
1378 AC_SUBST(CVC4_BINDINGS_LIBRARY_VERSION)
1380 AC_DEFINE_UNQUOTED(CVC4_MAJOR, ${CVC4_MAJOR}, [Major component of the version of CVC4.])
1381 AC_DEFINE_UNQUOTED(CVC4_MINOR, ${CVC4_MINOR}, [Minor component of the version of CVC4.])
1382 AC_DEFINE_UNQUOTED(CVC4_RELEASE, ${CVC4_RELEASE}, [Release component of the version of CVC4.])
1383 AC_DEFINE_UNQUOTED(CVC4_EXTRAVERSION, ["${CVC4_EXTRAVERSION}"], [Extraversion component of the version of CVC4.])
1384 AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full release string for CVC4.])
1386 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
1387 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
1388 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions"
1389 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
1391 # visibility flag not supported for Windows builds
1392 # also increase default stack size for Windows binaries
1395 (*mingw*) FLAG_VISIBILITY_HIDDEN=
1396 cvc4_LDFLAGS=-Wl,--stack,134217728
1397 pcvc4_LDFLAGS=-Wl,--stack,134217728
1401 AM_CONDITIONAL([CVC4_WINDOWS_BUILD], [test "$windows_build" = "yes"])
1403 AC_SUBST(FLAG_VISIBILITY_HIDDEN)
1404 AC_SUBST(cvc4_LDFLAGS)
1405 AC_SUBST(pcvc4_LDFLAGS)
1407 AM_CONDITIONAL(WHITE_AND_BLACK_TESTS, [test -z "$FLAG_VISIBILITY_HIDDEN"])
1409 # remember the command line used for configure
1410 AC_SUBST(cvc4_config_cmdline)
1414 # When automake scans Makefiles, it complains about non-standard make
1415 # features (including GNU extensions), and breaks GNU Make's
1416 # "if/endif" construct, replacing the "if" with AM_CONDITIONAL if
1417 # constructs. automake even follows "include" and messes with
1418 # included Makefiles.
1420 # CVC4 assumes GNU Make and we want to use GNU Make if/endifs, so we
1421 # have to hide some included Makefiles with GNU extensions. We do
1422 # this by defining mk_include as an autoconf substitution and then
1423 # using "@mk_include@ other_makefile" in Makefile.am to include
1424 # makefiles with GNU extensions; this hides them from automake.
1426 AC_SUBST(mk_include)
1427 # Similar trickery for "if"
1435 # This is used to _always_ comment out rules in automake makefiles, but
1436 # still trigger certain automake behavior; see test/unit/Makefile.am.
1437 AM_CONDITIONAL([CVC4_FALSE], [false])
1439 # set up substitutions for src/util/{rational,integer}.h.in
1440 if test $cvc4_cln_or_gmp = cln; then
1447 AC_SUBST(CVC4_USE_CLN_IMP)
1448 AC_SUBST(CVC4_USE_GMP_IMP)
1450 # month/year for man pages
1451 MAN_DATE=`date '+%B %Y'`
1457 proofs/signatures/Makefile]
1458 m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | grep -v '^contrib/alttheoryskel/' | sort | sed 's,\.am$,,'])
1461 if test $cvc4_has_threads = yes; then
1462 support_multithreaded='with boost threading library'
1463 AM_CONDITIONAL([CVC4_HAS_THREADS], [true])
1464 AC_SUBST([CVC4_HAS_THREADS], 1)
1466 support_multithreaded='no'
1467 AM_CONDITIONAL([CVC4_HAS_THREADS], [false])
1468 AC_SUBST([CVC4_HAS_THREADS], 0)
1471 # Final information to the user
1475 if test "$custom_build_profile" = yes; then
1476 with_build="$with_build (customized)"
1479 support_unit_tests='cxxtest not found; unit tests not supported'
1480 if test -n "$CXXTEST"; then
1481 support_unit_tests='unit testing infrastructure enabled in build directory'
1482 elif test "$enable_unit_testing" = no; then
1483 support_unit_tests='unit testing disabled by user'
1486 if test "$enable_optimized" = yes; then
1487 optimized="yes, at level $OPTLEVEL"
1492 if test $have_libglpk -eq 1; then
1494 gpllibs="${gpllibs} glpk"
1497 if test $have_libreadline -eq 1; then
1499 gpllibs="${gpllibs} readline"
1502 if test $cvc4_cln_or_gmp = cln; then
1503 mplibrary='cln (GPL)'
1505 gpllibs="${gpllibs} cln"
1506 if test $with_portfolio = yes; then
1507 AC_ERROR([Bad configuration detected: cannot build portfolio with CLN.
1508 Please specify only one of --with-portfolio and --with-cln.])
1514 if test "$gpl" = yes; then
1515 if test "$CVC4_BSD_LICENSED_CODE_ONLY" = 1; then
1516 AC_ERROR([Bad configuration detected: BSD-licensed code only, but also requested GPLed libraries:$gpllibs
1517 To permit GPL'ed dependences, use the configure flag --enable-gpl])
1520 licensewarn="${licensewarn}"'****************************************************************************
1521 Please note that CVC4 will be built against the following GPLed libraries:
1523 As these libraries are covered under the GPLv3, so is this build of CVC4.
1524 CVC4 is also available to you under the terms of the (modified) BSD license.
1525 If you prefer to license CVC4 under those terms, please configure with the
1526 option "--bsd", which will disable all optional GPLed library dependences.
1527 ****************************************************************************
1530 license="GPLv3 (due to optional libraries; see below)"
1532 licensewarn="${licensewarn}Please note that this configuration is NOT built against any GPL'ed
1533 libraries, so it is covered by the (modified) BSD license. This is,
1534 however, not the best-performing configuration of CVC4. To build
1535 against GPL'ed libraries which improve CVC4's performance, re-configure
1536 with '--best --enable-gpl'.
1539 license="modified BSD"
1542 if test "$gpl" = yes; then isgpl=1; else isgpl=0; fi
1543 AC_DEFINE_UNQUOTED(CVC4_GPL_DEPS, $isgpl, [Whether CVC4 is built with the (optional) GPLed library dependences.])
1545 CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="$CVC4_COMPAT_LIBRARY_VERSION"
1546 CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="$CVC4_BINDINGS_LIBRARY_VERSION"
1547 if test "$CVC4_BUILD_LIBCOMPAT" = no; then
1548 CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="N/A"
1550 if test -z "$CVC4_LANGUAGE_BINDINGS"; then
1551 CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="N/A"
1554 bindings_to_be_built=none
1555 if test -n "$CVC4_LANGUAGE_BINDINGS"; then
1556 bindings_to_be_built="$CVC4_LANGUAGE_BINDINGS"
1557 if test -z "$SWIG"; then
1558 bindings_to_be_built="$bindings_to_be_built (for CVC3 compatibility layer only; SWIG not found)"
1562 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
1563 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
1565 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template])
1566 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5])
1567 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3])
1568 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc_template])
1569 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc_template])
1570 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3])
1571 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3])
1579 Build profile: $with_build
1580 Build ID : $build_type
1581 Optimized : $optimized
1582 Debug symbols: $enable_debug_symbols
1583 Proofs : $enable_proof
1584 Statistics : $enable_statistics
1585 Replay : $enable_replay
1586 Assertions : $enable_assertions
1587 Tracing : $enable_tracing
1588 Dumping : $enable_dumping
1589 Muzzle : $enable_muzzle
1591 Unit tests : $support_unit_tests
1592 gcov support : $enable_coverage
1593 gprof support: $enable_profiling
1595 Static libs : $enable_static
1596 Shared libs : $enable_shared
1597 Static binary: $enable_static_binary
1598 Compat lib : $CVC4_BUILD_LIBCOMPAT
1599 Bindings : $bindings_to_be_built
1601 Multithreaded: $support_multithreaded
1602 Portfolio : $with_portfolio
1605 CaDiCaL : $with_cadical
1606 Cryptominisat: $with_cryptominisat
1609 MP library : $mplibrary
1610 Readline : $with_readline
1611 SymFPU : $with_symfpu
1613 CPPFLAGS : $CPPFLAGS
1614 CXXFLAGS : $CXXFLAGS
1619 libcvc4 version : $CVC4_LIBRARY_VERSION
1620 libcvc4parser version : $CVC4_PARSER_LIBRARY_VERSION
1621 libcvc4compat version : $CVC4_COMPAT_LIBRARY_VERSION_or_nobuild
1622 libcvc4bindings version: $CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild
1624 Install into : $prefix
1626 CVC4 license : $license
1628 ${licensewarn}Now just type make, followed by make check or make install, as you like.
1632 if test -n "$CVC4_UNSUPPORTED_LANGUAGE_BINDINGS"; then
1634 AC_MSG_WARN([You are electing to build unsupported language binding(s):])
1635 AC_MSG_WARN([ $CVC4_UNSUPPORTED_LANGUAGE_BINDINGS])
1636 AC_MSG_WARN([Please be aware that these bindings may not compile, or])
1637 AC_MSG_WARN([work, and the interface to CVC4 via these bindings may])
1638 AC_MSG_WARN([change drastically in upcoming releases of CVC4.])
1642 if test -n "$CVC4_INTEGRITY_WARNING"; then
1644 AC_MSG_WARN($CVC4_INTEGRITY_WARNING)
1645 AC_MSG_WARN([Please run "make check" after building to ensure integrity of the binary and library])