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}"; then
137 custom_build_profile=no
139 custom_build_profile=yes
142 if test -n "${enable_optimized+set}"; then
143 if test "$enable_optimized" = yes; then
144 btargs="$btargs optimized"
146 btargs="$btargs nooptimized"
149 # --enable-staticbinary is an alias for --enable-static-binary
150 if test -n "${enable_staticbinary+set}"; then
151 enable_static_binary="$enable_staticbinary"
153 if test -n "${enable_static_binary+set}"; then
154 if test "$enable_static_binary" = yes; then
155 btargs="$btargs staticbinary"
157 btargs="$btargs nostaticbinary"
160 if test -n "${enable_debug_symbols+set}"; then
161 if test "$enable_debug_symbols" = yes; then
162 btargs="$btargs debugsymbols"
164 btargs="$btargs nodebugsymbols"
167 if test -n "${enable_assertions+set}"; then
168 if test "$enable_assertions" = yes; then
169 btargs="$btargs assertions"
171 btargs="$btargs noassertions"
174 if test -n "${enable_proof+set}"; then
175 if test "$enable_proof" = yes; then
176 btargs="$btargs proof"
178 btargs="$btargs noproof"
181 if test -n "${enable_tracing+set}"; then
182 if test "$enable_tracing" = yes; then
183 btargs="$btargs tracing"
185 btargs="$btargs notracing"
188 if test -n "${enable_dumping+set}"; then
189 if test "$enable_dumping" = yes; then
190 btargs="$btargs dumping"
192 btargs="$btargs nodumping"
195 if test -n "${enable_muzzle+set}"; then
196 if test "$enable_muzzle" = yes; then
197 btargs="$btargs muzzle"
199 btargs="$btargs nomuzzle"
202 if test -n "${enable_coverage+set}"; then
203 if test "$enable_coverage" = yes; then
204 btargs="$btargs coverage"
206 btargs="$btargs nocoverage"
209 if test -n "${enable_profiling+set}"; then
210 if test "$enable_profiling" = yes; then
211 btargs="$btargs profiling"
213 btargs="$btargs noprofiling"
216 if test -n "${enable_statistics+set}"; then
217 if test "$enable_statistics" = yes; then
218 btargs="$btargs statistics"
220 btargs="$btargs nostatistics"
223 if test -n "${enable_replay+set}"; then
224 if test "$enable_replay" = yes; then
225 btargs="$btargs replay"
227 btargs="$btargs noreplay"
230 if test -n "${with_glpk+set}"; then
231 if test "$with_glpk" = yes; then
232 btargs="$btargs glpk"
235 if test -n "${with_abc+set}"; then
236 if test "$with_abc" = yes; then
240 if test -n "${with_cadical+set}"; then
241 if test "$with_cadical" = yes; then
242 btargs="$btargs cadical"
245 if test -n "${with_cryptominisat+set}"; then
246 if test "$with_cryptominisat" = yes; then
247 btargs="$btargs cryptominisat"
250 if test -n "${with_lfsc+set}"; then
251 if test "$with_lfsc" = yes; then
253 btargs="$btargs lfsc"
257 AC_MSG_RESULT([$with_build])
259 AM_INIT_AUTOMAKE([1.11 no-define tar-pax parallel-tests color-tests subdir-objects])
260 AC_CONFIG_HEADERS([cvc4autoconfig.h])
262 # automake 1.12 changes the test driver mechanism in a way that is
263 # completely incompatible with 1.11. We figure out here which version
264 # we're using in order to set up test makefiles correctly.
265 # See http://lists.gnu.org/archive/html/automake/2012-04/msg00060.html
266 if test -z "$am__api_version"; then
267 AC_MSG_ERROR([Cannot determine automake API version ?!])
269 case "$am__api_version" in
270 1.11*) automake111=true ;;
271 *) automake111=false ;;
273 AM_CONDITIONAL([AUTOMAKE_1_11], [$automake111])
275 # Initialize libtool's configuration options.
276 # we're not DLL-clean yet (i.e., don't properly use dllexport and dllimport)
277 # _LT_SET_OPTION([LT_INIT],[win32-dll])
280 # Checks for programs.
287 if test $cross_compiling = "no"; then
288 AC_MSG_CHECKING([whether C++ exceptions work])
291 AC_LANG_PROGRAM([#include <exception>], [[
294 throw std::exception();
300 [AC_MSG_RESULT([yes])],
301 [AC_MSG_ERROR([C++ exceptions do not work.])]
305 AC_MSG_WARN([Cross compiling, cannot check whether exceptions work])
315 [use CLN instead of GMP]
318 y|ye|yes|Y|YE|YES) cvc4_use_cln=1 ;;
319 n|no|N|NO) cvc4_use_cln=0 ;;
328 [use GMP instead of CLN]
331 y|ye|yes|Y|YE|YES) cvc4_use_gmp=1 ;;
332 n|no|N|NO) cvc4_use_gmp=0 ;;
337 if test $cvc4_use_cln = 1 -a $cvc4_use_gmp = 1 || test $cvc4_use_cln = 0 -a $cvc4_use_gmp = 0; then
338 AC_MSG_ERROR([You must use either CLN and GMP. Please pick one.])
340 if test $cvc4_use_gmp = 1; then
342 elif test $cvc4_use_gmp = 0; then
344 elif test $cvc4_use_cln = 1; then
346 elif test $cvc4_use_cln = 0; then
350 # try GMP, fail if not found; GMP is required for both CLN and for GMP
352 AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP (libgmp) not found, see http://gmplib.org/])])
354 if test $cvc4_use_cln = 2; then
355 if test "$CVC4_BSD_LICENSED_CODE_ONLY" = 1 -o "$with_portfolio" = yes; then
361 if test $cvc4_use_cln != 0; then
362 # [mdeters] The PKG_CHECK_MODULES macro isn't customizable and doesn't fail
363 # gracefully. You can only specify it once for a given library name. That
364 # is, even on separate if/else branches, you can't put
365 # PKG_CHECK_MODULES([CLN], ...). That's why things are so convoluted here,
366 # we have to have PKG_CHECK_MODULES _exactly_ once in configure.ac !
367 PKG_CHECK_MODULES([CLN], [cln >= 1.2.2],
370 save_CXXFLAGS="$CXXFLAGS"
371 LIBS="$CLN_LIBS $LIBS"
372 CXXFLAGS="$CLN_CFLAGS $CXXFLAGS"
373 AC_LINK_IFELSE([AC_LANG_PROGRAM([[#include <cln/cln.h>]], [[cln::cl_F pi = "3.1415926";]])], [
376 if test $cvc4_use_cln = 1; then
378 AC_MSG_ERROR([CLN installation missing, too old, or not functional for this architecture])
381 AC_MSG_NOTICE([CLN installation missing, too old, or not functional for this architecture, will use gmp instead])
386 CXXFLAGS="$save_CXXFLAGS"
390 [if test $cvc4_use_cln = 1; then
392 AC_MSG_ERROR([CLN not installed (or too old) or pkgconfig missing])
395 AC_MSG_NOTICE([CLN not installed (or too old) or pkgconfig missing, will use gmp])
402 if test $cvc4_use_cln = 0; then
403 # try GMPXX, fail if not found; don't need to link against it, only need its header
405 AC_CHECK_HEADER([gmpxx.h], , [AC_MSG_ERROR([GNU MP C++ library header (gmpxx.h) required but not found, see http://gmplib.org/])])
409 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }$CLN_CFLAGS"
410 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }$CLN_CFLAGS"
411 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }$CLN_CFLAGS"
412 LIBS="$CLN_LIBS${LIBS:+ $LIBS}"
416 if test $cvc4_cln_or_gmp = cln; then
417 AC_DEFINE_UNQUOTED(CVC4_CLN_IMP, [], [Defined if using the CLN multi-precision arithmetic library.])
419 AC_DEFINE_UNQUOTED(CVC4_GMP_IMP, [], [Defined if using the GMP multi-precision arithmetic library.])
421 AM_CONDITIONAL([CVC4_CLN_IMP], [test $cvc4_cln_or_gmp = cln])
422 AM_CONDITIONAL([CVC4_GMP_IMP], [test $cvc4_cln_or_gmp = gmp])
424 # construct the build string
425 AC_MSG_CHECKING([for appropriate build string])
426 if test -z "$ac_confdir"; then
429 build_type=`$ac_confdir/config/build-type $with_build $btargs $cvc4_cln_or_gmp`
430 AC_MSG_RESULT($build_type)
432 # Require building in target and build-specific build directory:
434 # If the configure script is invoked from the top-level source
435 # directory, it creates a suitable build directory (based on the build
436 # architecture and build profile from $build_type), changes into it,
437 # and reinvokes itself. CVC4_CONFIGURE_IN_BUILDS is an envariable
438 # that breaks any possibility of infinite recursion in this process.
439 AC_MSG_CHECKING([what dir to configure])
440 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
441 AC_MSG_RESULT([this one (in builds/)])
442 elif test "$CVC4_CONFIGURE_AT_TOP_LEVEL" = yes; then
443 AC_MSG_RESULT([builds/$target/$build_type])
445 if test -z "$ac_srcdir"; then
446 mkbuilddir=./config/mkbuilddir
448 mkbuilddir=$ac_srcdir/config/mkbuilddir
450 $as_echo "$mkbuilddir $target $build_type"
451 source $mkbuilddir "$target" "$build_type"
452 $as_echo "cd builds/$target/$build_type"
453 cd "builds/$target/$build_type"
454 CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS
455 # Runs the single recursive configure invocation using a relative path.
456 # See https://lists.gnu.org/archive/html/autoconf/2011-04/msg00060.html
457 echo "$SHELL ../../../configure ${config_cmdline[[@]]}"
458 "$SHELL" "../../../configure" "${config_cmdline[[@]]}"
461 if test $exitval -eq 0; then
462 cat >config.reconfig <<EOF
464 # Generated by configure, `date`
465 # This script is part of CVC4.
467 cd "\`dirname \\"\$0\\"\`"
469 if test -d builds; then :; else echo 'No builds/ directory!' >&2; exit; fi
471 current=(\`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]*\\)/\\(.*\\),\\1 \\2,'\`)
475 echo "reconfiguring in builds/\$arch/\$build..."
476 cd "builds/\$arch/\$build"
477 echo ./config.status "\$@"
478 ./config.status "\$@"]
480 chmod +x config.reconfig
482 ln -sf "$target/$build_type/config.log" "builds/config.log"
485 AC_MSG_RESULT([this one (user-specified)])
490 # Unpack standard build types. Any particular options can be overriden with
491 # --enable/disable-X options
492 # Tim: This needs to keep CVC4CPPFLAGS, CVC4CXXFLAGS, etc. set by earlier checks
493 case "$with_build" in
494 production) # highly optimized, no assertions, no tracing, dumping
495 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }"
496 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }"
497 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }"
498 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
499 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
500 if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=3 ; fi
501 if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
502 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no ; fi
503 if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
504 if test -z "${enable_replay+set}" ; then enable_replay=no ; fi
505 if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi
506 if test -z "${enable_proof+set}" ; then enable_proof=yes ; fi
507 if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi
508 if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
509 if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
510 if test -z "${enable_valgrind+set}" ; then enable_valgrind=no ; fi
512 debug) # unoptimized, debug symbols, assertions, tracing, dumping
513 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DEBUG"
514 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-fno-inline"
515 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-fno-inline"
516 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
517 FLAG_VISIBILITY_HIDDEN=
518 if test -z "${enable_optimized+set}" ; then enable_optimized=no ; fi
519 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
520 if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
521 if test -z "${enable_replay+set}" ; then enable_replay=yes ; fi
522 if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi
523 if test -z "${enable_proof+set}" ; then enable_proof=yes ; fi
524 if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi
525 if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
526 if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
527 if test -z "${enable_valgrind+set}" ; then enable_valgrind=optional ; fi
529 default) # moderately optimized, assertions, tracing, dumping
530 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }"
531 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }"
532 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }"
533 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
534 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
535 if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=2 ; fi
536 if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
537 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
538 if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
539 if test -z "${enable_replay+set}" ; then enable_replay=yes ; fi
540 if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi
541 if test -z "${enable_proof+set}" ; then enable_proof=yes ; fi
542 if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi
543 if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
544 if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
545 if test -z "${enable_valgrind+set}" ; then enable_valgrind=no ; fi
547 competition) # maximally optimized, no assertions, no tracing, no dumping, muzzled
548 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COMPETITION_MODE"
549 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs"
550 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs"
551 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
552 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
553 if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=9 ; fi
554 if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
555 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no ; fi
556 if test -z "${enable_statistics+set}" ; then enable_statistics=no ; fi
557 if test -z "${enable_replay+set}" ; then enable_replay=no ; fi
558 if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi
559 if test -z "${enable_proof+set}" ; then enable_proof=no ; fi
560 if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi
561 if test -z "${enable_dumping+set}" ; then enable_dumping=no ; fi
562 if test -z "${enable_muzzle+set}" ; then enable_muzzle=yes ; fi
563 if test -z "${enable_valgrind+set}" ; then enable_valgrind=no ; fi
564 if test -z "${user_specified_enable_or_disable_shared}"; then enable_shared=no; fi
565 if test -z "${user_specified_enable_or_disable_static}"; then enable_static=yes; fi
566 if test -z "${enable_static_binary+set}"; then enable_static_binary=yes ; fi
569 AC_MSG_FAILURE([unknown build profile: $with_build])
572 if test -z "${OPTLEVEL+set}"; then OPTLEVEL=3; fi
574 AM_CONDITIONAL([CVC4_BUILD_PROFILE_PRODUCTION], [test "$with_build" = production])
575 AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEBUG], [test "$with_build" = debug])
576 AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEFAULT], [test "$with_build" = default])
577 AM_CONDITIONAL([CVC4_BUILD_PROFILE_COMPETITION], [test "$with_build" = competition])
579 # permit a static binary
580 AC_MSG_CHECKING([whether to build a static binary])
581 AC_ARG_ENABLE([static-binary],
582 [AS_HELP_STRING([--enable-static-binary],
583 [build a fully statically-linked binary [default=no]])])
584 if test -z "${enable_static_binary+set}"; then
585 enable_static_binary=no
587 AC_MSG_RESULT([$enable_static_binary])
588 if test "$enable_static_binary" = yes; then
589 if test "$target_vendor" = apple; then
590 if test -z "$MAC_STATIC_BINARY_MANUAL_OVERRIDE"; then
591 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)]])
593 AC_MSG_WARN([MAC_STATIC_BINARY_MANUAL_OVERRIDE was set!])
594 AC_MSG_WARN([Will make a static binary during this build. Note that it may fail!])
597 if test "$enable_static" != yes; then
599 AC_MSG_WARN([forcing static-library building, --enable-static-binary given])
603 AC_MSG_CHECKING([whether to support proofs in libcvc4])
605 AC_ARG_ENABLE([proof],
606 [AS_HELP_STRING([--disable-proof],
607 [do not support proof generation])])
608 if test -z "${enable_proof+set}"; then
611 AC_MSG_RESULT([$enable_proof])
613 if test "$enable_proof" = yes; then
614 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROOF"
616 AM_CONDITIONAL([CVC4_PROOF], [test "$enable_proof" = yes])
618 AC_MSG_CHECKING([whether to optimize libcvc4])
620 AC_ARG_ENABLE([optimized],
621 [AS_HELP_STRING([--enable-optimized],
622 [optimize the build])])
624 if test -z "${enable_optimized+set}"; then
628 AC_MSG_RESULT([$enable_optimized])
630 if test "$enable_optimized" = yes; then
631 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O$OPTLEVEL"
632 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O$OPTLEVEL"
634 # Use -Og if available (optimizations that do not interfere with debugging),
636 debug_optimization_level="-O0"
637 CVC4_CXX_OPTION([-Og], [debug_optimization_level])
638 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }${debug_optimization_level}"
639 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }${debug_optimization_level}"
642 AC_MSG_CHECKING([whether to include debugging symbols in libcvc4])
644 AC_ARG_ENABLE([debug-symbols],
645 [AS_HELP_STRING([--disable-debug-symbols],
646 [do not include debug symbols in libcvc4])])
648 if test -z "${enable_debug_symbols+set}"; then
649 enable_debug_symbols=yes
652 AC_MSG_RESULT([$enable_debug_symbols])
654 if test "$enable_debug_symbols" = yes; then
655 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-ggdb3"
656 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-ggdb3"
659 AC_MSG_CHECKING([whether to enable Valgrind instrumentation])
661 AC_ARG_ENABLE([valgrind],
662 [AS_HELP_STRING([--enable-valgrind],
663 [enable Valgrind instrumentation])])
665 if test -z "${enable_valgrind+set}"; then
669 AC_MSG_RESULT([$enable_valgrind])
671 if test "$enable_valgrind" != no; then
672 # Valgrind instrumentation is either explicitly enabled (enable_valgrind=yes)
673 # or enabled if available (enable_valgrind=optional)
674 AC_CHECK_HEADER([valgrind/memcheck.h],
675 [CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_VALGRIND"],
676 [if test "$enable_valgrind" = yes; then
677 AC_MSG_ERROR([Need valgrind/memcheck.h to enable Valgrind instrumentation])
679 AC_MSG_NOTICE([valgrind/memcheck.h missing, Valgrind instrumentation disabled])
684 AC_MSG_CHECKING([whether to use the debug context memory manager])
686 AC_ARG_ENABLE([debug-context-memory-manager],
687 [AS_HELP_STRING([--enable-debug-context-memory-manager],
688 [use the debug context memory manager])])
690 if test -z "${enable_debug_context_memory_manager+set}"; then
691 enable_debug_context_memory_manager=no
694 AC_MSG_RESULT([$enable_debug_context_memory_manager])
696 if test "$enable_debug_context_memory_manager" = yes; then
697 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DEBUG_CONTEXT_MEMORY_MANAGER"
700 AC_MSG_CHECKING([whether to include statistics are turned on in libcvc4])
702 AC_ARG_ENABLE([statistics],
703 [AS_HELP_STRING([--disable-statistics],
704 [do not include statistics in libcvc4])])
706 if test -z "${enable_statistics+set}"; then
707 enable_statistics=yes
710 AC_MSG_RESULT([$enable_statistics])
712 if test "$enable_statistics" = yes; then
713 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_STATISTICS_ON"
716 AC_MSG_CHECKING([whether the replay feature should be turned on in libcvc4])
718 AC_ARG_ENABLE([replay],
719 [AS_HELP_STRING([--disable-replay],
720 [turn off the replay feature in libcvc4])])
722 if test -z "${enable_replay+set}"; then
726 AC_MSG_RESULT([$enable_replay])
728 if test "$enable_replay" = yes; then
729 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_REPLAY"
732 AC_MSG_CHECKING([whether to include assertions in build])
734 AC_ARG_ENABLE([assertions],
735 [AS_HELP_STRING([--disable-assertions],
736 [turn off assertions in build])])
738 if test -z "${enable_assertions+set}"; then
739 enable_assertions=yes
742 AC_MSG_RESULT([$enable_assertions])
744 if test "$enable_assertions" = yes; then
745 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_ASSERTIONS"
747 # turn off regular C assert() also
748 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DNDEBUG"
751 AC_MSG_CHECKING([whether to do a traceable build of CVC4])
752 AC_ARG_ENABLE([tracing],
753 [AS_HELP_STRING([--disable-tracing],
754 [remove all tracing code from CVC4])])
756 if test -z "${enable_tracing+set}"; then
760 AC_MSG_RESULT([$enable_tracing])
762 if test "$enable_tracing" = yes; then
763 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_TRACING"
766 AC_MSG_CHECKING([whether to do a dump-capable build of CVC4])
767 AC_ARG_ENABLE([dumping],
768 [AS_HELP_STRING([--disable-dumping],
769 [remove all dumping code from CVC4])])
771 if test -z "${enable_dumping+set}"; then
775 AC_MSG_RESULT([$enable_dumping])
777 if test "$enable_dumping" = yes; then
778 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DUMPING"
781 AC_MSG_CHECKING([whether to do a muzzled build of CVC4])
782 AC_ARG_ENABLE([muzzle],
783 [AS_HELP_STRING([--enable-muzzle],
784 [completely silence CVC4; remove ALL non-result output from build])])
786 if test -z "${enable_muzzle+set}"; then
790 AC_MSG_RESULT([$enable_muzzle])
792 if test "$enable_muzzle" = yes; then
793 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_MUZZLE"
796 AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4])
797 AC_ARG_ENABLE([coverage],
798 [AS_HELP_STRING([--enable-coverage],
799 [build with support for gcov coverage testing])])
801 if test -z "${enable_coverage+set}"; then
803 # make COVERAGE_ON the empty string for makefile conditional function
804 # $(if $(COVERAGE_ON), action1, action2)
808 AC_MSG_RESULT([$enable_coverage])
810 if test "$enable_coverage" = yes; then
811 # For coverage testing, we prefer:
812 # --enable-static --disable-shared --disable-static-binary
813 # If the user didn't specify these, we force them here. If the
814 # user specified them in opposite phase, give warnings that they
815 # shouldn't do that, or bomb out.
817 if test "$user_specified_enable_or_disable_shared" != yes; then
819 AC_MSG_WARN([turning off shared library building due to --enable-coverage])
820 elif test "$enable_shared" = yes; then
822 AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-shared])
823 AC_MSG_WARN([gcov does not support shared libraries, so only your static libraries will be coverage-testable.])
824 AC_MSG_WARN([Your cvc4 driver and testing binaries will not be coverage-testable.])
827 if test "${enable_static_binary+set}" = set -a "$enable_static_binary" = yes; then
829 AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-static-binary])
830 AC_MSG_WARN([Your cvc4 driver and testing binaries will be fully-statically linked and may not be coverage-testable.])
833 if test "$user_specified_enable_or_disable_static" != yes; then
835 AC_MSG_WARN([turning on static library building due to --enable-coverage])
836 elif test "$enable_static" != yes; then
837 AC_MSG_ERROR([--enable-coverage and --disable-static are incompatible; gcov only supports static libraries.])
840 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COVERAGE"
841 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }--coverage"
842 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }--coverage"
843 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }--coverage"
846 AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4])
848 AC_ARG_ENABLE([profiling],
849 [AS_HELP_STRING([--enable-profiling],
850 [build with support for gprof profiling])])
852 if test -z "${enable_profiling+set}"; then
856 AC_MSG_RESULT([$enable_profiling])
858 if test "$enable_profiling" = yes; then
859 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROFILING"
860 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-pg"
861 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-pg"
862 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }-pg"
865 # Check for libglpk (defined in config/glpk.m4)
867 [AS_HELP_STRING([--with-glpk],
868 [use GLPK simplex solver])], [], [with_glpk=])
870 if test $have_libglpk -eq 1; then
871 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_GLPK"
873 AM_CONDITIONAL([CVC4_USE_GLPK], [test $have_libglpk -eq 1])
874 AC_SUBST([GLPK_LDFLAGS])
875 AC_SUBST([GLPK_LIBS])
877 # Build with libabc (defined in config/abc.m4)
879 [AS_HELP_STRING([--with-abc],
880 [use the ABC AIG library])], [], [with_abc=])
882 if test $have_libabc -eq 1; then
883 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_ABC"
885 AM_CONDITIONAL([CVC4_USE_ABC], [test $have_libabc -eq 1])
886 AC_SUBST([ABC_LDFLAGS])
890 # Build with libcadical
891 AC_ARG_WITH([cadical],
892 [AS_HELP_STRING([--with-cadical],
893 [use the CaDiCaL SAT solver])], [], [with_cadical=])
894 CVC4_CHECK_FOR_CADICAL
895 if test $have_libcadical -eq 1; then
896 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_CADICAL"
897 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$CADICAL_HOME/src"
899 AM_CONDITIONAL([CVC4_USE_CADICAL], [test $have_libcadical -eq 1])
900 AC_SUBST([CADICAL_LDFLAGS])
901 AC_SUBST([CADICAL_LIBS])
903 # Build with libcryptominisat
904 AC_ARG_WITH([cryptominisat],
905 [AS_HELP_STRING([--with-cryptominisat],
906 [use the CRYPTOMINISAT sat solver])], [], [with_cryptominisat=])
907 CVC4_CHECK_FOR_CRYPTOMINISAT
908 if test $have_libcryptominisat -eq 1; then
909 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_CRYPTOMINISAT"
910 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$CRYPTOMINISAT_HOME/install/include"
912 AM_CONDITIONAL([CVC4_USE_CRYPTOMINISAT], [test $have_libcryptominisat -eq 1])
913 AC_SUBST([CRYPTOMINISAT_LDFLAGS])
914 AC_SUBST([CRYPTOMINISAT_LIBS])
918 [AS_HELP_STRING([--with-lfsc],
919 [use the LFSC proof checker])], [], [with_lfsc=])
921 if test $have_liblfsc -eq 1; then
922 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_LFSC"
924 AM_CONDITIONAL([CVC4_USE_LFSC], [test $have_liblfsc -eq 1])
925 AC_SUBST([LFSC_LDFLAGS])
926 AC_SUBST([LFSC_LIBS])
929 # Check to see if this version/architecture of GNU C++ explicitly
930 # instantiates std::hash<uint64_t> or not. Some do, some don't.
931 # See src/util/hash.h.
932 AC_MSG_CHECKING([whether std::hash<uint64_t> is already specialized])
934 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
936 #include <functional>
937 namespace std { template<> struct hash<uint64_t> {}; }])],
938 [AC_MSG_RESULT([no]); CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_NEED_HASH_UINT64_T"],
939 [AC_MSG_RESULT([yes])])
942 # Check whether "long" and "int64_t" are distinct types w.r.t. overloading.
943 # Even if they have the same size, they can be distinct, and some platforms
944 # can have problems with ambiguous function calls when auto-converting
945 # int64_t to long, and others will complain if you overload a function
946 # that takes an int64_t with one that takes a long (giving a redefinition
947 # error). So we have to keep both happy. Probably the same underlying
948 # issue as the hash specialization above, but let's check separately
950 AC_MSG_CHECKING([for the relationship between long and int64_t])
952 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
955 void foo(int64_t) {}])],
956 [AC_MSG_RESULT([no relationship detected]); CVC4_NEED_INT64_T_OVERLOADS=1],
957 [AC_MSG_RESULT([typedef or similar]); CVC4_NEED_INT64_T_OVERLOADS=0])
959 AC_SUBST([CVC4_NEED_INT64_T_OVERLOADS])
961 # Check for ANTLR runantlr script (defined in config/antlr.m4)
964 CVC4_CXX_OPTION([-Werror], [WERROR])
965 CVC4_C_OPTION([-Werror], [C_WERROR])
966 CVC4_CXX_OPTION([-Wno-deprecated], [WNO_DEPRECATED])
967 CVC4_C_OPTION([-Wno-deprecated], [C_WNO_DEPRECATED])
968 CVC4_CXX_OPTION([-Wno-conversion-null], [WNO_CONVERSION_NULL])
969 CVC4_CXX_OPTION([-Wno-tautological-compare], [WNO_TAUTOLOGICAL_COMPARE])
970 CVC4_CXX_OPTION([-Wno-parentheses], [WNO_PARENTHESES])
971 CVC4_CXX_OPTION([-Wno-uninitialized], [WNO_UNINITIALIZED])
972 CVC4_CXX_OPTION([-Wno-unused-variable], [WNO_UNUSED_VARIABLE])
973 CVC4_CXX_OPTION([-Wsuggest-override], [W_SUGGEST_OVERRIDE])
974 CVC4_CXX_OPTION([-fno-strict-aliasing], [FNO_STRICT_ALIASING])
976 AC_SUBST([WNO_CONVERSION_NULL])
977 AC_SUBST([WNO_TAUTOLOGICAL_COMPARE])
978 AC_SUBST([WNO_PARENTHESES])
979 AC_SUBST([WNO_UNINITIALIZED])
980 AC_SUBST([WNO_UNUSED_VARIABLE])
981 AC_SUBST([W_SUGGEST_OVERRIDE])
982 AC_SUBST([FNO_STRICT_ALIASING])
984 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }${W_SUGGEST_OVERRIDE}"
986 # On Mac, we have to fix the visibility of standard library symbols.
987 # Otherwise, exported template instantiations---even though explicitly
988 # CVC4_PUBLIC, can be generated as symbols with internal-only linkage.
989 # Presumably, Apple is distributing a libstdc++ that is built *without*
990 # --enable-libstdcxx-visibility (?)
991 if test "$target_vendor" = apple; then
992 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-D_GLIBCXX_VISIBILITY_DEFAULT=\"__attribute__((__visibility__(\\\"default\\\")))\""
995 # Tell top-level Makefile to include $(top_srcdir)/personal.mk
996 AC_ARG_ENABLE([personal-make-rules],
997 [AS_HELP_STRING([--enable-personal-make-rules],
998 [include top-level personal.mk (if it exists)])])
999 if test "$enable_personal_make_rules" = yes; then
1000 # This allows us to include a personal.mk makefile from every
1001 # generated makefile. Named zz_* in order to make sure this
1002 # comes last, so it gets other definitions (in particular top_srcdir).
1003 zz_cvc4_use_personal_make_rules='yes
1006 include $(top_srcdir)/personal.mk
1007 $(top_srcdir)/personal.mk:; @touch "$@"'
1008 AC_SUBST([zz_cvc4_use_personal_make_rules])
1011 # Doxygen configuration
1012 AC_ARG_ENABLE([internals-documentation],
1013 [AS_HELP_STRING([--enable-internals-documentation],
1014 [build Doxygen documentation for static and private member functions])])
1015 if test "$enable_internals_documentation" = yes; then
1016 DOXYGEN_EXTRACT_PRIVATE=YES
1017 DOXYGEN_EXTRACT_STATIC=YES
1019 DOXYGEN_EXTRACT_PRIVATE=NO
1020 DOXYGEN_EXTRACT_STATIC=NO
1022 AC_SUBST([DOXYGEN_EXTRACT_PRIVATE])
1023 AC_SUBST([DOXYGEN_EXTRACT_STATIC])
1029 DX_INIT_DOXYGEN($PACKAGE_NAME, config/doxygen.cfg, $srcdir/doc/doxygen)
1031 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])
1032 AC_ARG_VAR(CXXTEST, [path to CxxTest installation])
1033 AC_ARG_WITH([cxxtest-dir],
1034 [AS_HELP_STRING([--with-cxxtest-dir=DIR], [path to CxxTest installation])],
1035 [CXXTEST="$withval"])
1038 RUN_REGRESSION_ARGS=
1039 # FIXME currently, unsat core regressions are disabled without LFSC
1040 if test "$with_lfsc" = yes; then
1041 RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--proof"
1043 AC_SUBST([TESTS_ENVIRONMENT])
1044 AC_SUBST([RUN_REGRESSION_ARGS])
1046 AC_ARG_VAR(TEST_CPPFLAGS, [CPPFLAGS to use when testing (default=$CPPFLAGS)])
1047 AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)])
1048 AC_ARG_VAR(TEST_LDFLAGS, [LDFLAGS to use when testing (default=$LDFLAGS)])
1051 if test "$enable_unit_testing" = "no"; then
1052 AC_MSG_NOTICE([unit tests disabled by user request.])
1055 # The latest version of cxxtest distributed from the git repository places
1056 # cxxtest under <cxxtest-root>/bin/cxxtest
1057 AC_PATH_PROGS(CXXTESTGEN,
1058 cxxtestgen.pl cxxtestgen.py cxxtestgen,
1060 AC_MSG_NOTICE([unit tests disabled, \
1061 could not find cxxtestgen.pl or \
1062 cxxtestgen.py or cxxtestgen])
1065 [$CXXTEST:$CXXTEST/bin:$PATH])
1067 if test -n "$CXXTESTGEN" -a "`basename $CXXTESTGEN`" = "cxxtestgen.pl"; then
1068 if test -z "$PERL"; then
1069 AC_CHECK_PROGS(PERL, perl, perl, [])
1071 AC_CHECK_PROG(PERL, "$PERL", "$PERL", [])
1074 if test -z "$PERL"; then
1075 AC_MSG_WARN([unit tests disabled, perl not found.])
1081 # check if CxxTest headers exist and set include paths accordingly
1082 if test -n "$CXXTESTGEN"; then
1083 AC_MSG_CHECKING([for location of CxxTest headers])
1084 if test -n "$CXXTEST"; then
1085 if test -e "$CXXTEST/cxxtest/TestRunner.h"; then
1086 AC_MSG_RESULT([$CXXTEST])
1087 TEST_CPPFLAGS="${TEST_CPPFLAGS} -I$CXXTEST"
1088 TEST_CXXFLAGS="${TEST_CXXFLAGS} -I$CXXTEST"
1090 AC_MSG_RESULT([not found])
1091 AC_MSG_WARN([unit tests disabled, CxxTest headers not found at $CXXTEST.])
1095 # TODO: use more generic way to find cxxtest/TestRunner.h in system headers
1096 elif test -e "/usr/include/cxxtest/TestRunner.h"; then
1097 CXXTEST=/usr/include
1098 AC_MSG_RESULT([$CXXTEST])
1100 CXXTEST=`dirname "$CXXTESTGEN"`
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.])
1115 if test "$enable_unit_testing" = yes -a -z "$CXXTESTGEN"; then
1116 AC_MSG_ERROR([--enable-unit-testing given but cxxtest not found.])
1119 AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"])
1121 AC_ARG_VAR(PERL, [PERL interpreter (used when testing)])
1123 AC_ARG_VAR(PYTHON, [PYTHON interpreter (used for building legacy Java library interface)])
1125 if test -z "$PYTHON"; then
1126 AC_CHECK_PROGS(PYTHON, python, python, [])
1128 AC_CHECK_PROG(PYTHON, "$PYTHON", "$PYTHON", [])
1131 if test -z "$PYTHON"; then
1132 AC_MSG_WARN([python not found, cannot build libcvc4compat_java (the legacy Java interface).])
1137 # Checks for libraries.
1139 AC_SEARCH_LIBS([clock_gettime], [rt pthread],
1140 [AC_DEFINE([HAVE_CLOCK_GETTIME], [1],
1141 [Defined to 1 if clock_gettime() is supported by the platform.])],
1142 [AC_LIBOBJ([clock_gettime])])
1143 AC_CHECK_FUNC([strtok_r], [AC_DEFINE([HAVE_STRTOK_R], [1],
1144 [Defined to 1 if strtok_r() is supported by the platform.])])
1145 AC_CHECK_FUNC([ffs], [AC_DEFINE([HAVE_FFS], [1],
1146 [Defined to 1 if ffs() is supported by the platform.])])
1148 AC_LIBOBJ([strtok_r ffs])
1150 # Check for sigaltstack (missing in emscripten and mingw)
1151 AC_CHECK_FUNC([sigaltstack], [AC_DEFINE([HAVE_SIGALTSTACK], [1],
1152 [Defined to 1 if sigaltstack() is supported by the platform.])])
1154 # Check for antlr C++ runtime (defined in config/antlr.m4)
1157 # Check for user preferences for language bindings to build, and for
1158 # build support. The arg list is the default set if unspecified by
1159 # the user (the actual built set is the subset that appears to be
1160 # supported by the build host).
1161 CVC4_CHECK_BINDINGS([c java])dnl csharp perl php python ruby tcl ocaml])
1163 # Checks for header files and their contents.
1164 AC_CHECK_HEADERS([getopt.h unistd.h ext/stdio_filebuf.h])
1166 # Checks for typedefs, structures, and compiler characteristics.
1168 # these are bad macros, they clash with system header <stdint.h> !!
1174 # guard against double-inclusion of the autoheader
1175 AH_TOP([#ifndef __CVC4__CVC4AUTOCONFIG_H
1176 #define __CVC4__CVC4AUTOCONFIG_H])
1177 AH_BOTTOM([#endif /* __CVC4__CVC4AUTOCONFIG_H */])
1179 AC_CHECK_DECLS([optreset], [], [], [#include <getopt.h>])
1181 # check with which standard strerror_r() complies
1184 # require boost library
1187 # look for boost threading library
1188 AC_ARG_WITH([portfolio],
1189 AS_HELP_STRING([--with-portfolio], [build the multithreaded portfolio version of CVC4 (pcvc4)]))
1190 cvc4_save_LDFLAGS="$LDFLAGS"
1191 if test "$enable_static_binary" = yes; then
1192 LDFLAGS="-static $LDFLAGS"
1194 cvc4_has_threads=yes
1195 AC_ARG_ENABLE([thread-support],
1196 AS_HELP_STRING([--disable-thread-support], [do not support multithreaded-capable library]))
1197 if test "$enable_thread_support" = no; then
1199 if test "$with_portfolio" = yes; then
1200 AC_MSG_ERROR([user gave both --with-portfolio and --disable-thread-support, which are contradictory])
1203 BOOST_THREADS([], [AC_MSG_WARN([disabling multithreaded support])
1204 cvc4_has_threads=no])
1206 LDFLAGS="$cvc4_save_LDFLAGS"
1207 if test $cvc4_has_threads = no; then
1208 if test "$enable_thread_support" = yes; then
1209 AC_MSG_ERROR([user gave --enable-thread-support but could not build with threads; maybe boost threading library is missing?])
1211 if test "$with_portfolio" = yes; then
1212 AC_MSG_ERROR([user gave --with-portfolio but could not build with threads; maybe boost threading library is missing?])
1216 if test "$with_portfolio" != yes; then
1219 AM_CONDITIONAL([CVC4_BUILD_PCVC4], [test "$with_portfolio" = yes])
1220 if test "$with_portfolio" = yes; then
1221 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PORTFOLIO"
1223 # see if Boost has thread attributes (should be any version >= 1.50.0)
1224 # non-fatal error if not, but we won't support --thread-stack option
1225 AC_MSG_CHECKING([whether Boost threads support thread attrs])
1227 cvc4_save_CPPFLAGS="$CPPFLAGS"
1228 cvc4_save_LIBS="$LIBS"
1229 cvc4_save_LDFLAGS="$LDFLAGS"
1230 CPPFLAGS="$CPPFLAGS $BOOST_CPPFLAGS"
1231 LIBS="$LIBS $BOOST_THREAD_LIBS"
1232 LDFLAGS="$LDFLAGS $BOOST_THREAD_LDFLAGS"
1233 AC_LINK_IFELSE([AC_LANG_PROGRAM([#include <boost/thread.hpp>],
1234 [boost::thread::attributes attrs; attrs.set_stack_size(10 * 1024 * 1024);])],
1235 [cvc4_boost_has_thread_attr=1;
1236 AC_MSG_RESULT([yes])],
1237 [cvc4_boost_has_thread_attr=0;
1238 AC_MSG_RESULT([no])])
1239 CPPFLAGS="$cvc4_save_CPPFLAGS"
1240 LIBS="$cvc4_save_LIBS"
1241 LDFLAGS="$cvc4_save_LDFLAGS"
1244 cvc4_boost_has_thread_attr=0
1246 AC_DEFINE_UNQUOTED([BOOST_HAS_THREAD_ATTR], $cvc4_boost_has_thread_attr, [Define to 1 if Boost threading library has support for thread attributes])
1248 # Check for libreadline (defined in config/readline.m4)
1249 AC_ARG_WITH([readline], [AS_HELP_STRING([--with-readline], [support the readline library])], [], [with_readline=check])
1250 # make the flags as close as possible to the final flags, because the Boost
1251 # flags can bring in a different, incompatible readline library than we'd
1252 # get otherwise (e.g. on Mac, where there are commonly two different readlines,
1253 # one in /usr and one in /opt/local)
1254 cvc4_rlcheck_save_CPPFLAGS="$CPPFLAGS"
1255 cvc4_rlcheck_save_CXXFLAGS="$CXXFLAGS"
1256 cvc4_rlcheck_save_CFLAGS="$CFLAGS"
1257 cvc4_rlcheck_save_LDFLAGS="$LDFLAGS"
1258 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
1259 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS $WNO_DEPRECATED"
1260 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS $C_WNO_DEPRECATED -fexceptions"
1261 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
1262 CVC4_CHECK_FOR_READLINE
1263 CPPFLAGS="$cvc4_rlcheck_save_CPPFLAGS"
1264 CXXFLAGS="$cvc4_rlcheck_save_CXXFLAGS"
1265 CFLAGS="$cvc4_rlcheck_save_CFLAGS"
1266 LDFLAGS="$cvc4_rlcheck_save_LDFLAGS"
1267 AC_DEFINE_UNQUOTED([HAVE_LIBREADLINE], $have_libreadline, [Define to 1 to use libreadline])
1268 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])
1269 AC_SUBST([READLINE_LIBS])
1271 # Whether to build compatibility library
1272 CVC4_BUILD_LIBCOMPAT=yes
1273 AC_ARG_WITH([compat],
1274 AS_HELP_STRING([--with-compat], [build compatibility library (CVC3 API layer)]),
1275 [if test "$withval" = no; then CVC4_BUILD_LIBCOMPAT=no; fi])
1276 AC_MSG_CHECKING([whether to build compatibility library (CVC3 API layer)])
1277 if test "$CVC4_BUILD_LIBCOMPAT" = yes; then
1278 AC_MSG_RESULT([yes])
1280 AC_MSG_RESULT([no, disabled by user])
1282 AC_SUBST(CVC4_BUILD_LIBCOMPAT)
1283 AM_CONDITIONAL([CVC4_BUILD_LIBCOMPAT], [test "$CVC4_BUILD_LIBCOMPAT" = yes])
1285 # Whether to compile with google profiling tools
1286 cvc4_use_google_perftools=0
1290 [--with-google-perftools],
1291 [use Google Performance Tools]
1293 [if test "$withval" != no; then
1294 cvc4_use_google_perftools=1
1298 AC_MSG_CHECKING([whether to link in google perftools libraries])
1299 if test $cvc4_use_google_perftools = 1; then
1300 AC_MSG_RESULT([yes])
1301 AC_CHECK_LIB([tcmalloc], [MallocExtension_GetAllocatedSize], , [AC_MSG_ERROR([cannot link google-perftools test program with -ltcmalloc])], [-lpthread])
1302 AC_CHECK_LIB([profiler], [ProfilerStart], , [AC_MSG_ERROR([cannot link google-perftools test program with -lprofiler])], [-lpthread])
1304 AC_MSG_RESULT([no (user didn't request it)])
1308 AC_ARG_VAR(JAVA, [Java interpreter (used when testing Java interface)])
1309 AC_ARG_VAR(JAVAC, [Java compiler (used when building and testing Java interface)])
1310 AC_ARG_VAR(JAVAH, [Java compiler (used when building and testing Java interface)])
1311 AC_ARG_VAR(JAR, [Jar archiver (used when building Java interface)])
1312 if test "$cvc4_build_java_bindings"; then
1314 if test -z "$JAVA"; then
1315 AC_CHECK_PROGS(JAVA, java, java, [])
1317 AC_CHECK_PROG(JAVA, "$JAVA", "$JAVA", [])
1319 if test -z "$JAVAC"; then
1320 AC_CHECK_PROGS(JAVAC, javac gcj, javac, [])
1321 if test "$JAVAC" = gcj; then JAVAC='gcj -C'; fi
1323 AC_CHECK_PROG(JAVAC, "$JAVAC", "$JAVAC", [])
1325 if test -z "$JAVAH"; then
1326 AC_CHECK_PROGS(JAVAH, javah gcjh, javah, [])
1328 AC_CHECK_PROG(JAVAH, "$JAVAH", "$JAVAH", [])
1330 if test -z "$JAR"; then
1331 AC_CHECK_PROGS(JAR, jar, jar, [])
1333 AC_CHECK_PROG(JAR, "$JAR", "$JAR", [])
1337 # on Mac OS X, Java doesn't like the .so module extension; it wants .dylib
1338 module=no eval CVC4_JAVA_MODULE_EXT="$shrext_cmds"
1339 if test -z "$CVC4_JAVA_MODULE_EXT"; then
1340 CVC4_JAVA_MODULE_EXT=.so
1342 AC_SUBST([CVC4_JAVA_MODULE_EXT])
1344 # Prepare configure output
1346 if test "$enable_shared" = yes; then BUILDING_SHARED=1; else BUILDING_SHARED=0; fi
1347 if test "$enable_static" = yes; then BUILDING_STATIC=1; else BUILDING_STATIC=0; fi
1348 if test "$enable_static_binary" = yes; then STATIC_BINARY=1; else STATIC_BINARY=0; fi
1349 AC_SUBST(BUILDING_SHARED)
1350 AC_SUBST(BUILDING_STATIC)
1351 AC_SUBST(STATIC_BINARY)
1352 AM_CONDITIONAL([STATIC_BINARY], [test "$enable_static_binary" = yes])
1353 AM_CONDITIONAL([COVERAGE_ENABLED], [test "$enable_coverage" = yes])
1354 AC_SUBST([COVERAGE_ON])
1356 AM_CONDITIONAL([CVC4_DEBUG], [test "$with_build" = debug])
1357 AM_CONDITIONAL([CVC4_TRACING], [test "$enable_tracing" = yes])
1359 AC_SUBST(CVC4_LIBRARY_VERSION)
1360 AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
1361 AC_SUBST(CVC4_COMPAT_LIBRARY_VERSION)
1362 AC_SUBST(CVC4_BINDINGS_LIBRARY_VERSION)
1364 AC_DEFINE_UNQUOTED(CVC4_MAJOR, ${CVC4_MAJOR}, [Major component of the version of CVC4.])
1365 AC_DEFINE_UNQUOTED(CVC4_MINOR, ${CVC4_MINOR}, [Minor component of the version of CVC4.])
1366 AC_DEFINE_UNQUOTED(CVC4_RELEASE, ${CVC4_RELEASE}, [Release component of the version of CVC4.])
1367 AC_DEFINE_UNQUOTED(CVC4_EXTRAVERSION, ["${CVC4_EXTRAVERSION}"], [Extraversion component of the version of CVC4.])
1368 AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full release string for CVC4.])
1370 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
1371 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
1372 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions"
1373 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
1375 # visibility flag not supported for Windows builds
1376 # also increase default stack size for Windows binaries
1379 (*mingw*) FLAG_VISIBILITY_HIDDEN=
1380 cvc4_LDFLAGS=-Wl,--stack,134217728
1381 pcvc4_LDFLAGS=-Wl,--stack,134217728
1385 AM_CONDITIONAL([CVC4_WINDOWS_BUILD], [test "$windows_build" = "yes"])
1387 AC_SUBST(FLAG_VISIBILITY_HIDDEN)
1388 AC_SUBST(cvc4_LDFLAGS)
1389 AC_SUBST(pcvc4_LDFLAGS)
1391 AM_CONDITIONAL(WHITE_AND_BLACK_TESTS, [test -z "$FLAG_VISIBILITY_HIDDEN"])
1393 # remember the command line used for configure
1394 AC_SUBST(cvc4_config_cmdline)
1398 # When automake scans Makefiles, it complains about non-standard make
1399 # features (including GNU extensions), and breaks GNU Make's
1400 # "if/endif" construct, replacing the "if" with AM_CONDITIONAL if
1401 # constructs. automake even follows "include" and messes with
1402 # included Makefiles.
1404 # CVC4 assumes GNU Make and we want to use GNU Make if/endifs, so we
1405 # have to hide some included Makefiles with GNU extensions. We do
1406 # this by defining mk_include as an autoconf substitution and then
1407 # using "@mk_include@ other_makefile" in Makefile.am to include
1408 # makefiles with GNU extensions; this hides them from automake.
1410 AC_SUBST(mk_include)
1411 # Similar trickery for "if"
1419 # This is used to _always_ comment out rules in automake makefiles, but
1420 # still trigger certain automake behavior; see test/unit/Makefile.am.
1421 AM_CONDITIONAL([CVC4_FALSE], [false])
1423 # set up substitutions for src/util/{rational,integer}.h.in
1424 if test $cvc4_cln_or_gmp = cln; then
1431 AC_SUBST(CVC4_USE_CLN_IMP)
1432 AC_SUBST(CVC4_USE_GMP_IMP)
1434 # month/year for man pages
1435 MAN_DATE=`date '+%B %Y'`
1441 proofs/signatures/Makefile]
1442 m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | grep -v '^contrib/alttheoryskel/' | sort | sed 's,\.am$,,'])
1445 if test $cvc4_has_threads = yes; then
1446 support_multithreaded='with boost threading library'
1447 AM_CONDITIONAL([CVC4_HAS_THREADS], [true])
1448 AC_SUBST([CVC4_HAS_THREADS], 1)
1450 support_multithreaded='no'
1451 AM_CONDITIONAL([CVC4_HAS_THREADS], [false])
1452 AC_SUBST([CVC4_HAS_THREADS], 0)
1455 # Final information to the user
1459 if test "$custom_build_profile" = yes; then
1460 with_build="$with_build (customized)"
1463 support_unit_tests='cxxtest not found; unit tests not supported'
1464 if test -n "$CXXTEST"; then
1465 support_unit_tests='unit testing infrastructure enabled in build directory'
1466 elif test "$enable_unit_testing" = no; then
1467 support_unit_tests='unit testing disabled by user'
1470 if test "$enable_optimized" = yes; then
1471 optimized="yes, at level $OPTLEVEL"
1476 if test $have_libglpk -eq 1; then
1478 gpllibs="${gpllibs} glpk"
1481 if test $have_libreadline -eq 1; then
1483 gpllibs="${gpllibs} readline"
1486 if test $cvc4_cln_or_gmp = cln; then
1487 mplibrary='cln (GPL)'
1489 gpllibs="${gpllibs} cln"
1490 if test $with_portfolio = yes; then
1491 AC_ERROR([Bad configuration detected: cannot build portfolio with CLN.
1492 Please specify only one of --with-portfolio and --with-cln.])
1498 if test "$gpl" = yes; then
1499 if test "$CVC4_BSD_LICENSED_CODE_ONLY" = 1; then
1500 AC_ERROR([Bad configuration detected: BSD-licensed code only, but also requested GPLed libraries:$gpllibs
1501 To permit GPL'ed dependences, use the configure flag --enable-gpl])
1504 licensewarn="${licensewarn}"'****************************************************************************
1505 Please note that CVC4 will be built against the following GPLed libraries:
1507 As these libraries are covered under the GPLv3, so is this build of CVC4.
1508 CVC4 is also available to you under the terms of the (modified) BSD license.
1509 If you prefer to license CVC4 under those terms, please configure with the
1510 option "--bsd", which will disable all optional GPLed library dependences.
1511 ****************************************************************************
1514 license="GPLv3 (due to optional libraries; see below)"
1516 licensewarn="${licensewarn}Please note that this configuration is NOT built against any GPL'ed
1517 libraries, so it is covered by the (modified) BSD license. This is,
1518 however, not the best-performing configuration of CVC4. To build
1519 against GPL'ed libraries which improve CVC4's performance, re-configure
1520 with '--best --enable-gpl'.
1523 license="modified BSD"
1526 if test "$gpl" = yes; then isgpl=1; else isgpl=0; fi
1527 AC_DEFINE_UNQUOTED(CVC4_GPL_DEPS, $isgpl, [Whether CVC4 is built with the (optional) GPLed library dependences.])
1529 CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="$CVC4_COMPAT_LIBRARY_VERSION"
1530 CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="$CVC4_BINDINGS_LIBRARY_VERSION"
1531 if test "$CVC4_BUILD_LIBCOMPAT" = no; then
1532 CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="N/A"
1534 if test -z "$CVC4_LANGUAGE_BINDINGS"; then
1535 CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="N/A"
1538 bindings_to_be_built=none
1539 if test -n "$CVC4_LANGUAGE_BINDINGS"; then
1540 bindings_to_be_built="$CVC4_LANGUAGE_BINDINGS"
1541 if test -z "$SWIG"; then
1542 bindings_to_be_built="$bindings_to_be_built (for CVC3 compatibility layer only; SWIG not found)"
1546 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
1547 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
1549 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template])
1550 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5])
1551 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3])
1552 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc_template])
1553 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc_template])
1554 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3])
1555 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3])
1563 Build profile: $with_build
1564 Build ID : $build_type
1565 Optimized : $optimized
1566 Debug symbols: $enable_debug_symbols
1567 Proofs : $enable_proof
1568 Statistics : $enable_statistics
1569 Replay : $enable_replay
1570 Assertions : $enable_assertions
1571 Tracing : $enable_tracing
1572 Dumping : $enable_dumping
1573 Muzzle : $enable_muzzle
1575 Unit tests : $support_unit_tests
1576 gcov support : $enable_coverage
1577 gprof support: $enable_profiling
1579 Static libs : $enable_static
1580 Shared libs : $enable_shared
1581 Static binary: $enable_static_binary
1582 Compat lib : $CVC4_BUILD_LIBCOMPAT
1583 Bindings : $bindings_to_be_built
1585 Multithreaded: $support_multithreaded
1586 Portfolio : $with_portfolio
1589 CaDiCaL : $with_cadical
1590 Cryptominisat: $with_cryptominisat
1593 MP library : $mplibrary
1594 Readline : $with_readline
1596 CPPFLAGS : $CPPFLAGS
1597 CXXFLAGS : $CXXFLAGS
1602 libcvc4 version : $CVC4_LIBRARY_VERSION
1603 libcvc4parser version : $CVC4_PARSER_LIBRARY_VERSION
1604 libcvc4compat version : $CVC4_COMPAT_LIBRARY_VERSION_or_nobuild
1605 libcvc4bindings version: $CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild
1607 Install into : $prefix
1609 CVC4 license : $license
1611 ${licensewarn}Now just type make, followed by make check or make install, as you like.
1615 if test -n "$CVC4_UNSUPPORTED_LANGUAGE_BINDINGS"; then
1617 AC_MSG_WARN([You are electing to build unsupported language binding(s):])
1618 AC_MSG_WARN([ $CVC4_UNSUPPORTED_LANGUAGE_BINDINGS])
1619 AC_MSG_WARN([Please be aware that these bindings may not compile, or])
1620 AC_MSG_WARN([work, and the interface to CVC4 via these bindings may])
1621 AC_MSG_WARN([change drastically in upcoming releases of CVC4.])
1625 if test -n "$CVC4_INTEGRITY_WARNING"; then
1627 AC_MSG_WARN($CVC4_INTEGRITY_WARNING)
1628 AC_MSG_WARN([Please run "make check" after building to ensure integrity of the binary and library])