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, 7) 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_BINDINGS_LIBRARY_VERSION, library_version([libcvc4bindings]))dnl
53 m4_define([fatal_error], [m4_errprint(__program__:__file__:__line__[: fatal error: $*
56 m4_ifblank(_CVC4_LIBRARY_VERSION,[fatal_error([no CVC4_LIBRARY_VERSION defined for release version "]_CVC4_RELEASE_STRING[" in library_versions file])])dnl
57 m4_ifblank(_CVC4_PARSER_LIBRARY_VERSION,[fatal_error([no CVC4_PARSER_LIBRARY_VERSION defined for release version "]_CVC4_RELEASE_STRING[" in library_versions file])])dnl
58 m4_ifblank(_CVC4_BINDINGS_LIBRARY_VERSION,[fatal_error([no CVC4_BINDINGS_LIBRARY_VERSION defined for release version "]_CVC4_RELEASE_STRING[" in library_versions file])])dnl
60 CVC4_LIBRARY_VERSION=_CVC4_LIBRARY_VERSION
61 CVC4_PARSER_LIBRARY_VERSION=_CVC4_PARSER_LIBRARY_VERSION
62 CVC4_BINDINGS_LIBRARY_VERSION=_CVC4_BINDINGS_LIBRARY_VERSION
64 # Using AX_CXX_COMPILE_STDCXX_11 and the AC_CANONICAL_* macros destroy the
65 # command line you get from $@, which we want later for determining the build
66 # profile. So we save it.
67 # (We can't do our build profile stuff here, or it's not included in the
68 # output... autoconf overrides us on the orderings of some things.)
70 cvc4_config_cmdline="${config_cmdline[[@]]}"
72 # remember if the user set these explicitly (or whether autoconf does)
73 user_specified_enable_or_disable_static=${enable_static+yes}
74 user_specified_enable_or_disable_shared=${enable_shared+yes}
76 if test -e src/include/cvc4_public.h; then
77 CVC4_CONFIGURE_AT_TOP_LEVEL=yes
79 CVC4_CONFIGURE_AT_TOP_LEVEL=no
82 # override autoconf: we don't want it giving us CFLAGS/CXXFLAGS, but we do
83 # want to respect the user's flags
84 if test -z "${CFLAGS+set}"; then CFLAGS=; fi
85 if test -z "${CXXFLAGS+set}"; then CXXFLAGS=; fi
88 AM_MAINTAINER_MODE([enable])
90 # turn off static lib building by default
98 # C++11 support in the compiler is now mandatory. Check for support and add
99 # switches if necessary.
100 AX_CXX_COMPILE_STDCXX_11([ext], [mandatory])
104 if test "$enable_shared" = no -a "$user_specified_enable_or_disable_shared" = yes; then
108 # Features requested by the user
109 AC_MSG_CHECKING([for requested build profile])
111 [AS_HELP_STRING([--with-build=profile],
112 [for profile in {production,debug,competition,testing}])])
114 if test -z "${with_build+set}"; then
115 with_build=production
117 if test -z "${enable_optimized+set}" -a \
118 -z "${enable_debug_symbols+set}" -a \
119 -z "${enable_assertions+set}" -a \
120 -z "${enable_tracing+set}" -a \
121 -z "${enable_dumping+set}" -a \
122 -z "${enable_muzzle+set}" -a \
123 -z "${enable_coverage+set}" -a \
124 -z "${enable_profiling+set}" -a \
125 -z "${enable_statistics+set}" -a \
126 -z "${enable_replay+set}" -a \
127 -z "${with_gmp+set}" -a \
128 -z "${with_cln+set}" -a \
129 -z "${with_glpk+set}" -a \
130 -z "${with_abc+set}" -a \
131 -z "${with_cadical+set}" -a \
132 -z "${with_cryptominisat+set}" -a \
133 -z "${with_lfsc+set}" -a \
134 -z "${with_symfpu+set}"; then
135 custom_build_profile=no
137 custom_build_profile=yes
140 if test -n "${enable_optimized+set}"; then
141 if test "$enable_optimized" = yes; then
142 btargs="$btargs optimized"
144 btargs="$btargs nooptimized"
147 # --enable-staticbinary is an alias for --enable-static-binary
148 if test -n "${enable_staticbinary+set}"; then
149 enable_static_binary="$enable_staticbinary"
151 if test -n "${enable_static_binary+set}"; then
152 if test "$enable_static_binary" = yes; then
153 btargs="$btargs staticbinary"
155 btargs="$btargs nostaticbinary"
158 if test -n "${enable_debug_symbols+set}"; then
159 if test "$enable_debug_symbols" = yes; then
160 btargs="$btargs debugsymbols"
162 btargs="$btargs nodebugsymbols"
165 if test -n "${enable_assertions+set}"; then
166 if test "$enable_assertions" = yes; then
167 btargs="$btargs assertions"
169 btargs="$btargs noassertions"
172 if test -n "${enable_proof+set}"; then
173 if test "$enable_proof" = yes; then
174 btargs="$btargs proof"
176 btargs="$btargs noproof"
179 if test -n "${enable_tracing+set}"; then
180 if test "$enable_tracing" = yes; then
181 btargs="$btargs tracing"
183 btargs="$btargs notracing"
186 if test -n "${enable_dumping+set}"; then
187 if test "$enable_dumping" = yes; then
188 btargs="$btargs dumping"
190 btargs="$btargs nodumping"
193 if test -n "${enable_muzzle+set}"; then
194 if test "$enable_muzzle" = yes; then
195 btargs="$btargs muzzle"
197 btargs="$btargs nomuzzle"
200 if test -n "${enable_coverage+set}"; then
201 if test "$enable_coverage" = yes; then
202 btargs="$btargs coverage"
204 btargs="$btargs nocoverage"
207 if test -n "${enable_profiling+set}"; then
208 if test "$enable_profiling" = yes; then
209 btargs="$btargs profiling"
211 btargs="$btargs noprofiling"
214 if test -n "${enable_statistics+set}"; then
215 if test "$enable_statistics" = yes; then
216 btargs="$btargs statistics"
218 btargs="$btargs nostatistics"
221 if test -n "${enable_replay+set}"; then
222 if test "$enable_replay" = yes; then
223 btargs="$btargs replay"
225 btargs="$btargs noreplay"
228 if test -n "${with_glpk+set}"; then
229 if test "$with_glpk" = yes; then
230 btargs="$btargs glpk"
233 if test -n "${with_abc+set}"; then
234 if test "$with_abc" = yes; then
238 if test -n "${with_cadical+set}"; then
239 if test "$with_cadical" = yes; then
240 btargs="$btargs cadical"
243 if test -n "${with_cryptominisat+set}"; then
244 if test "$with_cryptominisat" = yes; then
245 btargs="$btargs cryptominisat"
248 if test -n "${with_lfsc+set}"; then
249 if test "$with_lfsc" = yes; then
251 btargs="$btargs lfsc"
254 if test -n "${with_symfpu+set}"; then
255 if test "$with_symfpu" = yes; then
256 btargs="$btargs symfpu"
260 AC_MSG_RESULT([$with_build])
262 AM_INIT_AUTOMAKE([1.11 no-define tar-pax parallel-tests color-tests subdir-objects])
263 AC_CONFIG_HEADERS([cvc4autoconfig.h])
265 # automake 1.12 changes the test driver mechanism in a way that is
266 # completely incompatible with 1.11. We figure out here which version
267 # we're using in order to set up test makefiles correctly.
268 # See http://lists.gnu.org/archive/html/automake/2012-04/msg00060.html
269 if test -z "$am__api_version"; then
270 AC_MSG_ERROR([Cannot determine automake API version ?!])
272 case "$am__api_version" in
273 1.11*) automake111=true ;;
274 *) automake111=false ;;
276 AM_CONDITIONAL([AUTOMAKE_1_11], [$automake111])
278 # Initialize libtool's configuration options.
279 # we're not DLL-clean yet (i.e., don't properly use dllexport and dllimport)
280 # _LT_SET_OPTION([LT_INIT],[win32-dll])
283 # Checks for programs.
290 if test $cross_compiling = "no"; then
291 AC_MSG_CHECKING([whether C++ exceptions work])
294 AC_LANG_PROGRAM([#include <exception>], [[
297 throw std::exception();
303 [AC_MSG_RESULT([yes])],
304 [AC_MSG_ERROR([C++ exceptions do not work.])]
308 AC_MSG_WARN([Cross compiling, cannot check whether exceptions work])
318 [use CLN instead of GMP]
321 y|ye|yes|Y|YE|YES) cvc4_use_cln=1 ;;
322 n|no|N|NO) cvc4_use_cln=0 ;;
331 [use GMP instead of CLN]
334 y|ye|yes|Y|YE|YES) cvc4_use_gmp=1 ;;
335 n|no|N|NO) cvc4_use_gmp=0 ;;
340 if test $cvc4_use_cln = 1 -a $cvc4_use_gmp = 1 || test $cvc4_use_cln = 0 -a $cvc4_use_gmp = 0; then
341 AC_MSG_ERROR([You must use either CLN and GMP. Please pick one.])
343 if test $cvc4_use_gmp = 1; then
345 elif test $cvc4_use_gmp = 0; then
347 elif test $cvc4_use_cln = 1; then
349 elif test $cvc4_use_cln = 0; then
353 # try GMP, fail if not found; GMP is required for both CLN and for GMP
355 AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP (libgmp) not found, see http://gmplib.org/])])
357 if test $cvc4_use_cln = 2; then
358 if test "$CVC4_BSD_LICENSED_CODE_ONLY" = 1 -o "$with_portfolio" = yes; then
364 if test $cvc4_use_cln != 0; then
365 # [mdeters] The PKG_CHECK_MODULES macro isn't customizable and doesn't fail
366 # gracefully. You can only specify it once for a given library name. That
367 # is, even on separate if/else branches, you can't put
368 # PKG_CHECK_MODULES([CLN], ...). That's why things are so convoluted here,
369 # we have to have PKG_CHECK_MODULES _exactly_ once in configure.ac !
370 PKG_CHECK_MODULES([CLN], [cln >= 1.2.2],
373 save_CXXFLAGS="$CXXFLAGS"
374 LIBS="$CLN_LIBS $LIBS"
375 CXXFLAGS="$CLN_CFLAGS $CXXFLAGS"
376 AC_LINK_IFELSE([AC_LANG_PROGRAM([[#include <cln/cln.h>]], [[cln::cl_F pi = "3.1415926";]])], [
379 if test $cvc4_use_cln = 1; then
381 AC_MSG_ERROR([CLN installation missing, too old, or not functional for this architecture])
384 AC_MSG_NOTICE([CLN installation missing, too old, or not functional for this architecture, will use gmp instead])
389 CXXFLAGS="$save_CXXFLAGS"
393 [if test $cvc4_use_cln = 1; then
395 AC_MSG_ERROR([CLN not installed (or too old) or pkgconfig missing])
398 AC_MSG_NOTICE([CLN not installed (or too old) or pkgconfig missing, will use gmp])
405 if test $cvc4_use_cln = 0; then
406 # try GMPXX, fail if not found; don't need to link against it, only need its header
408 AC_CHECK_HEADER([gmpxx.h], , [AC_MSG_ERROR([GNU MP C++ library header (gmpxx.h) required but not found, see http://gmplib.org/])])
412 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }$CLN_CFLAGS"
413 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }$CLN_CFLAGS"
414 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }$CLN_CFLAGS"
415 LIBS="$CLN_LIBS${LIBS:+ $LIBS}"
419 if test $cvc4_cln_or_gmp = cln; then
420 AC_DEFINE_UNQUOTED(CVC4_CLN_IMP, [], [Defined if using the CLN multi-precision arithmetic library.])
422 AC_DEFINE_UNQUOTED(CVC4_GMP_IMP, [], [Defined if using the GMP multi-precision arithmetic library.])
424 AM_CONDITIONAL([CVC4_CLN_IMP], [test $cvc4_cln_or_gmp = cln])
425 AM_CONDITIONAL([CVC4_GMP_IMP], [test $cvc4_cln_or_gmp = gmp])
427 # Dumping cannot be used in a portfolio build. Disable dumping by default when
428 # a portfolio build has been requested, throw an error if dumping has been
429 # explicitly requested with a portfolio build.
430 if test "$with_portfolio" = yes; then
431 if test "$enable_dumping" = yes; then
432 AC_MSG_ERROR([Dumping is not supported with a portfolio build])
437 # construct the build string
438 AC_MSG_CHECKING([for appropriate build string])
439 if test -z "$ac_confdir"; then
442 build_type=`$ac_confdir/config/build-type $with_build $btargs $cvc4_cln_or_gmp`
443 AC_MSG_RESULT($build_type)
445 # Require building in target and build-specific build directory:
447 # If the configure script is invoked from the top-level source
448 # directory, it creates a suitable build directory (based on the build
449 # architecture and build profile from $build_type), changes into it,
450 # and reinvokes itself. CVC4_CONFIGURE_IN_BUILDS is an envariable
451 # that breaks any possibility of infinite recursion in this process.
452 AC_MSG_CHECKING([what dir to configure])
453 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
454 AC_MSG_RESULT([this one (in builds/)])
455 elif test "$CVC4_CONFIGURE_AT_TOP_LEVEL" = yes; then
456 AC_MSG_RESULT([builds/$target/$build_type])
458 if test -z "$ac_srcdir"; then
459 mkbuilddir=./config/mkbuilddir
461 mkbuilddir=$ac_srcdir/config/mkbuilddir
463 $as_echo "$mkbuilddir $target $build_type"
464 source $mkbuilddir "$target" "$build_type"
465 $as_echo "cd builds/$target/$build_type"
466 cd "builds/$target/$build_type"
467 CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS
468 # Runs the single recursive configure invocation using a relative path.
469 # See https://lists.gnu.org/archive/html/autoconf/2011-04/msg00060.html
470 echo "$SHELL ../../../configure ${config_cmdline[[@]]}"
471 "$SHELL" "../../../configure" "${config_cmdline[[@]]}"
474 if test $exitval -eq 0; then
475 cat >config.reconfig <<EOF
477 # Generated by configure, `date`
478 # This script is part of CVC4.
480 cd "\`dirname \\"\$0\\"\`"
482 if test -d builds; then :; else echo 'No builds/ directory!' >&2; exit; fi
484 current=(\`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]*\\)/\\(.*\\),\\1 \\2,'\`)
488 echo "reconfiguring in builds/\$arch/\$build..."
489 cd "builds/\$arch/\$build"
490 echo ./config.status "\$@"
491 ./config.status "\$@"]
493 chmod +x config.reconfig
495 ln -sf "$target/$build_type/config.log" "builds/config.log"
498 AC_MSG_RESULT([this one (user-specified)])
503 # Unpack standard build types. Any particular options can be overriden with
504 # --enable/disable-X options
505 # Tim: This needs to keep CVC4CPPFLAGS, CVC4CXXFLAGS, etc. set by earlier checks
506 case "$with_build" in
507 production) # highly optimized, no assertions, no tracing, dumping
508 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }"
509 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }"
510 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }"
511 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
512 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
513 if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=3 ; fi
514 if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
515 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no ; fi
516 if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
517 if test -z "${enable_replay+set}" ; then enable_replay=no ; fi
518 if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi
519 if test -z "${enable_proof+set}" ; then enable_proof=yes ; fi
520 if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi
521 if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
522 if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
523 if test -z "${enable_valgrind+set}" ; then enable_valgrind=no ; fi
525 debug) # unoptimized, debug symbols, assertions, tracing, dumping
526 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DEBUG"
527 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-fno-inline"
528 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-fno-inline"
529 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
530 FLAG_VISIBILITY_HIDDEN=
531 if test -z "${enable_optimized+set}" ; then enable_optimized=no ; fi
532 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
533 if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
534 if test -z "${enable_replay+set}" ; then enable_replay=yes ; fi
535 if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi
536 if test -z "${enable_proof+set}" ; then enable_proof=yes ; fi
537 if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi
538 if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
539 if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
540 if test -z "${enable_valgrind+set}" ; then enable_valgrind=optional ; fi
542 testing) # moderately optimized, assertions, tracing, dumping
543 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }"
544 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }"
545 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }"
546 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
547 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
548 if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=2 ; fi
549 if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
550 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
551 if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
552 if test -z "${enable_replay+set}" ; then enable_replay=yes ; fi
553 if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi
554 if test -z "${enable_proof+set}" ; then enable_proof=yes ; fi
555 if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi
556 if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
557 if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
558 if test -z "${enable_valgrind+set}" ; then enable_valgrind=no ; fi
560 competition) # maximally optimized, no assertions, no tracing, no dumping, muzzled
561 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COMPETITION_MODE"
562 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs"
563 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs"
564 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
565 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
566 if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=9 ; fi
567 if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
568 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no ; fi
569 if test -z "${enable_statistics+set}" ; then enable_statistics=no ; fi
570 if test -z "${enable_replay+set}" ; then enable_replay=no ; fi
571 if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi
572 if test -z "${enable_proof+set}" ; then enable_proof=no ; fi
573 if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi
574 if test -z "${enable_dumping+set}" ; then enable_dumping=no ; fi
575 if test -z "${enable_muzzle+set}" ; then enable_muzzle=yes ; fi
576 if test -z "${enable_valgrind+set}" ; then enable_valgrind=no ; fi
577 if test -z "${user_specified_enable_or_disable_shared}"; then enable_shared=no; fi
578 if test -z "${user_specified_enable_or_disable_static}"; then enable_static=yes; fi
579 if test -z "${enable_static_binary+set}"; then enable_static_binary=yes ; fi
582 AC_MSG_FAILURE([unknown build profile: $with_build])
585 if test -z "${OPTLEVEL+set}"; then OPTLEVEL=3; fi
587 AM_CONDITIONAL([CVC4_BUILD_PROFILE_PRODUCTION], [test "$with_build" = production])
588 AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEBUG], [test "$with_build" = debug])
589 AM_CONDITIONAL([CVC4_BUILD_PROFILE_COMPETITION], [test "$with_build" = competition])
590 AM_CONDITIONAL([CVC4_BUILD_PROFILE_TESTING], [test "$with_build" = testing])
592 # permit a static binary
593 AC_MSG_CHECKING([whether to build a static binary])
594 AC_ARG_ENABLE([static-binary],
595 [AS_HELP_STRING([--enable-static-binary],
596 [build a fully statically-linked binary [default=no]])])
597 if test -z "${enable_static_binary+set}"; then
598 enable_static_binary=no
600 AC_MSG_RESULT([$enable_static_binary])
601 if test "$enable_static_binary" = yes; then
602 if test "$target_vendor" = apple; then
603 if test -z "$MAC_STATIC_BINARY_MANUAL_OVERRIDE"; then
604 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)]])
606 AC_MSG_WARN([MAC_STATIC_BINARY_MANUAL_OVERRIDE was set!])
607 AC_MSG_WARN([Will make a static binary during this build. Note that it may fail!])
610 if test "$enable_static" != yes; then
612 AC_MSG_WARN([forcing static-library building, --enable-static-binary given])
616 AC_MSG_CHECKING([whether to support proofs in libcvc4])
618 AC_ARG_ENABLE([proof],
619 [AS_HELP_STRING([--disable-proof],
620 [do not support proof generation])])
621 if test -z "${enable_proof+set}"; then
624 AC_MSG_RESULT([$enable_proof])
626 if test "$enable_proof" = yes; then
627 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROOF"
629 AM_CONDITIONAL([CVC4_PROOF], [test "$enable_proof" = yes])
631 AC_MSG_CHECKING([whether to optimize libcvc4])
633 AC_ARG_ENABLE([optimized],
634 [AS_HELP_STRING([--enable-optimized],
635 [optimize the build])])
637 if test -z "${enable_optimized+set}"; then
641 AC_MSG_RESULT([$enable_optimized])
643 if test "$enable_optimized" = yes; then
644 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O$OPTLEVEL"
645 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O$OPTLEVEL"
647 # Use -Og if available (optimizations that do not interfere with debugging),
649 debug_optimization_level="-O0"
650 CVC4_CXX_OPTION([-Og], [debug_optimization_level])
651 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }${debug_optimization_level}"
652 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }${debug_optimization_level}"
655 AC_MSG_CHECKING([whether to include debugging symbols in libcvc4])
657 AC_ARG_ENABLE([debug-symbols],
658 [AS_HELP_STRING([--disable-debug-symbols],
659 [do not include debug symbols in libcvc4])])
661 if test -z "${enable_debug_symbols+set}"; then
662 enable_debug_symbols=yes
665 AC_MSG_RESULT([$enable_debug_symbols])
667 if test "$enable_debug_symbols" = yes; then
668 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-ggdb3"
669 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-ggdb3"
672 AC_MSG_CHECKING([whether to enable Valgrind instrumentation])
674 AC_ARG_ENABLE([valgrind],
675 [AS_HELP_STRING([--enable-valgrind],
676 [enable Valgrind instrumentation])])
678 if test -z "${enable_valgrind+set}"; then
682 AC_MSG_RESULT([$enable_valgrind])
684 if test "$enable_valgrind" != no; then
685 # Valgrind instrumentation is either explicitly enabled (enable_valgrind=yes)
686 # or enabled if available (enable_valgrind=optional)
687 AC_CHECK_HEADER([valgrind/memcheck.h],
688 [CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_VALGRIND"],
689 [if test "$enable_valgrind" = yes; then
690 AC_MSG_ERROR([Need valgrind/memcheck.h to enable Valgrind instrumentation])
692 AC_MSG_NOTICE([valgrind/memcheck.h missing, Valgrind instrumentation disabled])
697 AC_MSG_CHECKING([whether to use the debug context memory manager])
699 AC_ARG_ENABLE([debug-context-memory-manager],
700 [AS_HELP_STRING([--enable-debug-context-memory-manager],
701 [use the debug context memory manager])])
703 if test -z "${enable_debug_context_memory_manager+set}"; then
704 enable_debug_context_memory_manager=no
707 AC_MSG_RESULT([$enable_debug_context_memory_manager])
709 if test "$enable_debug_context_memory_manager" = yes; then
710 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DEBUG_CONTEXT_MEMORY_MANAGER"
713 AC_MSG_CHECKING([whether to include statistics are turned on in libcvc4])
715 AC_ARG_ENABLE([statistics],
716 [AS_HELP_STRING([--disable-statistics],
717 [do not include statistics in libcvc4])])
719 if test -z "${enable_statistics+set}"; then
720 enable_statistics=yes
723 AC_MSG_RESULT([$enable_statistics])
725 if test "$enable_statistics" = yes; then
726 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_STATISTICS_ON"
729 AC_MSG_CHECKING([whether the replay feature should be turned on in libcvc4])
731 AC_ARG_ENABLE([replay],
732 [AS_HELP_STRING([--disable-replay],
733 [turn off the replay feature in libcvc4])])
735 if test -z "${enable_replay+set}"; then
739 AC_MSG_RESULT([$enable_replay])
741 if test "$enable_replay" = yes; then
742 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_REPLAY"
745 AC_MSG_CHECKING([whether to include assertions in build])
747 AC_ARG_ENABLE([assertions],
748 [AS_HELP_STRING([--disable-assertions],
749 [turn off assertions in build])])
751 if test -z "${enable_assertions+set}"; then
752 enable_assertions=yes
755 AC_MSG_RESULT([$enable_assertions])
757 if test "$enable_assertions" = yes; then
758 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_ASSERTIONS"
760 # turn off regular C assert() also
761 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DNDEBUG"
764 AC_MSG_CHECKING([whether to do a traceable build of CVC4])
765 AC_ARG_ENABLE([tracing],
766 [AS_HELP_STRING([--disable-tracing],
767 [remove all tracing code from CVC4])])
769 if test -z "${enable_tracing+set}"; then
773 AC_MSG_RESULT([$enable_tracing])
775 if test "$enable_tracing" = yes; then
776 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_TRACING"
779 AC_MSG_CHECKING([whether to do a dump-capable build of CVC4])
780 AC_ARG_ENABLE([dumping],
781 [AS_HELP_STRING([--disable-dumping],
782 [remove all dumping code from CVC4])])
784 if test -z "${enable_dumping+set}"; then
788 AC_MSG_RESULT([$enable_dumping])
790 if test "$enable_dumping" = yes; then
791 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DUMPING"
794 AC_MSG_CHECKING([whether to do a muzzled build of CVC4])
795 AC_ARG_ENABLE([muzzle],
796 [AS_HELP_STRING([--enable-muzzle],
797 [completely silence CVC4; remove ALL non-result output from build])])
799 if test -z "${enable_muzzle+set}"; then
803 AC_MSG_RESULT([$enable_muzzle])
805 if test "$enable_muzzle" = yes; then
806 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_MUZZLE"
809 AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4])
810 AC_ARG_ENABLE([coverage],
811 [AS_HELP_STRING([--enable-coverage],
812 [build with support for gcov coverage testing])])
814 if test -z "${enable_coverage+set}"; then
816 # make COVERAGE_ON the empty string for makefile conditional function
817 # $(if $(COVERAGE_ON), action1, action2)
821 AC_MSG_RESULT([$enable_coverage])
823 if test "$enable_coverage" = yes; then
824 # For coverage testing, we prefer:
825 # --enable-static --disable-shared --disable-static-binary
826 # If the user didn't specify these, we force them here. If the
827 # user specified them in opposite phase, give warnings that they
828 # shouldn't do that, or bomb out.
830 if test "$user_specified_enable_or_disable_shared" != yes; then
832 AC_MSG_WARN([turning off shared library building due to --enable-coverage])
833 elif test "$enable_shared" = yes; then
835 AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-shared])
836 AC_MSG_WARN([gcov does not support shared libraries, so only your static libraries will be coverage-testable.])
837 AC_MSG_WARN([Your cvc4 driver and testing binaries will not be coverage-testable.])
840 if test "${enable_static_binary+set}" = set -a "$enable_static_binary" = yes; then
842 AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-static-binary])
843 AC_MSG_WARN([Your cvc4 driver and testing binaries will be fully-statically linked and may not be coverage-testable.])
846 if test "$user_specified_enable_or_disable_static" != yes; then
848 AC_MSG_WARN([turning on static library building due to --enable-coverage])
849 elif test "$enable_static" != yes; then
850 AC_MSG_ERROR([--enable-coverage and --disable-static are incompatible; gcov only supports static libraries.])
853 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COVERAGE"
854 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }--coverage"
855 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }--coverage"
856 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }--coverage"
859 AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4])
861 AC_ARG_ENABLE([profiling],
862 [AS_HELP_STRING([--enable-profiling],
863 [build with support for gprof profiling])])
865 if test -z "${enable_profiling+set}"; then
869 AC_MSG_RESULT([$enable_profiling])
871 if test "$enable_profiling" = yes; then
872 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROFILING"
873 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-pg"
874 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-pg"
875 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }-pg"
878 # Check for libglpk (defined in config/glpk.m4)
880 [AS_HELP_STRING([--with-glpk],
881 [use GLPK simplex solver])], [], [with_glpk=])
883 if test $have_libglpk -eq 1; then
884 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_GLPK"
886 AM_CONDITIONAL([CVC4_USE_GLPK], [test $have_libglpk -eq 1])
887 AC_SUBST([GLPK_LDFLAGS])
888 AC_SUBST([GLPK_LIBS])
890 # Build with libabc (defined in config/abc.m4)
892 [AS_HELP_STRING([--with-abc],
893 [use the ABC AIG library])], [], [with_abc=])
895 if test $have_libabc -eq 1; then
896 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_ABC"
898 AM_CONDITIONAL([CVC4_USE_ABC], [test $have_libabc -eq 1])
899 AC_SUBST([ABC_LDFLAGS])
903 # Build with libcadical
904 AC_ARG_WITH([cadical],
905 [AS_HELP_STRING([--with-cadical],
906 [use the CaDiCaL SAT solver])], [], [with_cadical=])
907 CVC4_CHECK_FOR_CADICAL
908 if test $have_libcadical -eq 1; then
909 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_CADICAL"
910 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$CADICAL_HOME/src"
912 AM_CONDITIONAL([CVC4_USE_CADICAL], [test $have_libcadical -eq 1])
913 AC_SUBST([CADICAL_LDFLAGS])
914 AC_SUBST([CADICAL_LIBS])
916 # Build with libcryptominisat
917 AC_ARG_WITH([cryptominisat],
918 [AS_HELP_STRING([--with-cryptominisat],
919 [use the CRYPTOMINISAT sat solver])], [], [with_cryptominisat=])
920 CVC4_CHECK_FOR_CRYPTOMINISAT
921 if test $have_libcryptominisat -eq 1; then
922 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_CRYPTOMINISAT"
923 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$CRYPTOMINISAT_HOME/include"
925 AM_CONDITIONAL([CVC4_USE_CRYPTOMINISAT], [test $have_libcryptominisat -eq 1])
926 AC_SUBST([CRYPTOMINISAT_LDFLAGS])
927 AC_SUBST([CRYPTOMINISAT_LIBS])
931 [AS_HELP_STRING([--with-lfsc],
932 [use the LFSC proof checker])], [], [with_lfsc=])
934 if test $have_liblfsc -eq 1; then
935 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_LFSC"
937 AM_CONDITIONAL([CVC4_USE_LFSC], [test $have_liblfsc -eq 1])
938 AC_SUBST([LFSC_LDFLAGS])
939 AC_SUBST([LFSC_LIBS])
942 AC_ARG_WITH([symfpu],
943 [AS_HELP_STRING([--with-symfpu],
944 [use symfpu for floating point solver])], [], [with_symfpu=])
945 CVC4_CHECK_FOR_SYMFPU
946 if test $have_symfpu_headers -eq 1; then
947 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_SYMFPU"
948 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$SYMFPU_HOME"
950 AM_CONDITIONAL([CVC4_USE_SYMFPU], [test $have_symfpu_headers -eq 1])
951 AC_SUBST([CVC4_USE_SYMFPU], [$have_symfpu_headers])
953 # Check to see if this version/architecture of GNU C++ explicitly
954 # instantiates std::hash<uint64_t> or not. Some do, some don't.
955 # See src/util/hash.h.
956 AC_MSG_CHECKING([whether std::hash<uint64_t> is already specialized])
958 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
960 #include <functional>
961 namespace std { template<> struct hash<uint64_t> {}; }])],
962 [AC_MSG_RESULT([no]); CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_NEED_HASH_UINT64_T"],
963 [AC_MSG_RESULT([yes])])
966 # Check whether "long" and "int64_t" are distinct types w.r.t. overloading.
967 # Even if they have the same size, they can be distinct, and some platforms
968 # can have problems with ambiguous function calls when auto-converting
969 # int64_t to long, and others will complain if you overload a function
970 # that takes an int64_t with one that takes a long (giving a redefinition
971 # error). So we have to keep both happy. Probably the same underlying
972 # issue as the hash specialization above, but let's check separately
974 AC_MSG_CHECKING([for the relationship between long and int64_t])
976 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
979 void foo(int64_t) {}])],
980 [AC_MSG_RESULT([no relationship detected]); CVC4_NEED_INT64_T_OVERLOADS=1],
981 [AC_MSG_RESULT([typedef or similar]); CVC4_NEED_INT64_T_OVERLOADS=0])
983 AC_SUBST([CVC4_NEED_INT64_T_OVERLOADS])
985 # Check for ANTLR runantlr script (defined in config/antlr.m4)
988 CVC4_CXX_OPTION([-Werror], [WERROR])
989 CVC4_C_OPTION([-Werror], [C_WERROR])
990 CVC4_CXX_OPTION([-Wno-deprecated], [WNO_DEPRECATED])
991 CVC4_C_OPTION([-Wno-deprecated], [C_WNO_DEPRECATED])
992 CVC4_CXX_OPTION([-Wno-conversion-null], [WNO_CONVERSION_NULL])
993 CVC4_CXX_OPTION([-Wno-tautological-compare], [WNO_TAUTOLOGICAL_COMPARE])
994 CVC4_CXX_OPTION([-Wno-parentheses], [WNO_PARENTHESES])
995 CVC4_CXX_OPTION([-Wno-uninitialized], [WNO_UNINITIALIZED])
996 CVC4_CXX_OPTION([-Wno-unused-variable], [WNO_UNUSED_VARIABLE])
997 CVC4_CXX_OPTION([-Wsuggest-override], [W_SUGGEST_OVERRIDE])
998 CVC4_CXX_OPTION([-Wnon-virtual-dtor], [W_NON_VIRTUAL_DTOR])
999 CVC4_CXX_OPTION([-fno-strict-aliasing], [FNO_STRICT_ALIASING])
1001 AC_SUBST([WNO_CONVERSION_NULL])
1002 AC_SUBST([WNO_TAUTOLOGICAL_COMPARE])
1003 AC_SUBST([WNO_PARENTHESES])
1004 AC_SUBST([WNO_UNINITIALIZED])
1005 AC_SUBST([WNO_UNUSED_VARIABLE])
1006 AC_SUBST([W_SUGGEST_OVERRIDE])
1007 AC_SUBST([W_NON_VIRTUAL_DTOR])
1008 AC_SUBST([FNO_STRICT_ALIASING])
1010 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }${W_SUGGEST_OVERRIDE}"
1011 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }${W_NON_VIRTUAL_DTOR}"
1013 # On Mac, we have to fix the visibility of standard library symbols.
1014 # Otherwise, exported template instantiations---even though explicitly
1015 # CVC4_PUBLIC, can be generated as symbols with internal-only linkage.
1016 # Presumably, Apple is distributing a libstdc++ that is built *without*
1017 # --enable-libstdcxx-visibility (?)
1018 if test "$target_vendor" = apple; then
1019 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-D_GLIBCXX_VISIBILITY_DEFAULT=\"__attribute__((__visibility__(\\\"default\\\")))\""
1022 # Doxygen configuration
1023 AC_ARG_ENABLE([internals-documentation],
1024 [AS_HELP_STRING([--enable-internals-documentation],
1025 [build Doxygen documentation for static and private member functions])])
1026 if test "$enable_internals_documentation" = yes; then
1027 DOXYGEN_EXTRACT_PRIVATE=YES
1028 DOXYGEN_EXTRACT_STATIC=YES
1030 DOXYGEN_EXTRACT_PRIVATE=NO
1031 DOXYGEN_EXTRACT_STATIC=NO
1033 AC_SUBST([DOXYGEN_EXTRACT_PRIVATE])
1034 AC_SUBST([DOXYGEN_EXTRACT_STATIC])
1040 DX_INIT_DOXYGEN($PACKAGE_NAME, config/doxygen.cfg, $srcdir/doc/doxygen)
1042 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])
1043 AC_ARG_VAR(CXXTEST, [path to CxxTest installation])
1044 AC_ARG_WITH([cxxtest-dir],
1045 [AS_HELP_STRING([--with-cxxtest-dir=DIR], [path to CxxTest installation])],
1046 [CXXTEST="$withval"])
1049 RUN_REGRESSION_ARGS=
1050 if test "$with_lfsc" = yes; then
1051 RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--with-lfsc"
1053 if test "$enable_proof" = yes; then
1054 RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--enable-proof"
1056 AC_SUBST([TESTS_ENVIRONMENT])
1057 AC_SUBST([RUN_REGRESSION_ARGS])
1059 AC_ARG_VAR(TEST_CPPFLAGS, [CPPFLAGS to use when testing (default=$CPPFLAGS)])
1060 AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)])
1061 AC_ARG_VAR(TEST_LDFLAGS, [LDFLAGS to use when testing (default=$LDFLAGS)])
1064 if test "$enable_unit_testing" = "no"; then
1065 AC_MSG_NOTICE([unit tests disabled by user request.])
1068 # The latest version of cxxtest distributed from the git repository places
1069 # cxxtest under <cxxtest-root>/bin/cxxtest
1070 AC_PATH_PROGS(CXXTESTGEN,
1071 cxxtestgen.pl cxxtestgen.py cxxtestgen,
1073 [$CXXTEST:$CXXTEST/bin:$PATH])
1075 if test -n "$CXXTESTGEN"; then
1076 if "`basename $CXXTESTGEN`" = "cxxtestgen.pl"; then
1077 if test -z "$PERL"; then
1078 AC_CHECK_PROGS(PERL, perl, perl, [])
1080 AC_CHECK_PROG(PERL, "$PERL", "$PERL", [])
1083 if test -z "$PERL"; then
1084 AC_MSG_WARN([unit tests disabled, perl not found.])
1090 AC_MSG_NOTICE([unit tests disabled, could not find cxxtestgen.pl or cxxtestgen.py or cxxtestgen])
1094 # check if CxxTest headers exist and set include paths accordingly
1095 if test -n "$CXXTESTGEN"; then
1096 AC_MSG_CHECKING([for location of CxxTest headers])
1097 if test -n "$CXXTEST"; then
1098 if test -e "$CXXTEST/cxxtest/TestRunner.h"; then
1099 AC_MSG_RESULT([$CXXTEST])
1100 TEST_CPPFLAGS="${TEST_CPPFLAGS} -I$CXXTEST"
1101 TEST_CXXFLAGS="${TEST_CXXFLAGS} -I$CXXTEST"
1103 AC_MSG_RESULT([not found])
1104 AC_MSG_WARN([unit tests disabled, CxxTest headers not found at $CXXTEST.])
1108 # TODO: use more generic way to find cxxtest/TestRunner.h in system headers
1109 elif test -e "/usr/include/cxxtest/TestRunner.h"; then
1110 CXXTEST=/usr/include
1111 AC_MSG_RESULT([$CXXTEST])
1113 CXXTEST=`dirname "$CXXTESTGEN"`
1114 if test -e "$CXXTEST/cxxtest/TestRunner.h"; then
1115 AC_MSG_RESULT([$CXXTEST])
1116 TEST_CPPFLAGS="${TEST_CPPFLAGS} -I$CXXTEST"
1117 TEST_CXXFLAGS="${TEST_CXXFLAGS} -I$CXXTEST"
1119 AC_MSG_RESULT([not found])
1120 AC_MSG_WARN([unit tests disabled, CxxTest headers not found.])
1128 if test "$enable_unit_testing" = yes -a -z "$CXXTESTGEN"; then
1129 AC_MSG_ERROR([--enable-unit-testing given but cxxtest not found.])
1132 AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"])
1134 AC_ARG_VAR(PERL, [PERL interpreter (used when testing)])
1136 # Python is now a required dependency for generating options code
1137 AM_PATH_PYTHON([2.7],, [
1138 AC_MSG_ERROR([Python not found.])
1141 # Checks for libraries.
1143 AC_SEARCH_LIBS([clock_gettime], [rt pthread],
1144 [AC_DEFINE([HAVE_CLOCK_GETTIME], [1],
1145 [Defined to 1 if clock_gettime() is supported by the platform.])],
1146 [AC_LIBOBJ([clock_gettime])])
1147 AC_CHECK_FUNC([strtok_r], [AC_DEFINE([HAVE_STRTOK_R], [1],
1148 [Defined to 1 if strtok_r() is supported by the platform.])])
1149 AC_CHECK_FUNC([ffs], [AC_DEFINE([HAVE_FFS], [1],
1150 [Defined to 1 if ffs() is supported by the platform.])])
1152 AC_LIBOBJ([strtok_r ffs])
1154 # Check for sigaltstack (missing in emscripten and mingw)
1155 AC_CHECK_FUNC([sigaltstack], [AC_DEFINE([HAVE_SIGALTSTACK], [1],
1156 [Defined to 1 if sigaltstack() is supported by the platform.])])
1158 # Check for antlr C++ runtime (defined in config/antlr.m4)
1161 # Check for user preferences for language bindings to build, and for
1162 # build support. The arg list is the default set if unspecified by
1163 # the user (the actual built set is the subset that appears to be
1164 # supported by the build host).
1165 CVC4_CHECK_BINDINGS([c java])dnl csharp perl php python ruby tcl ocaml])
1167 # Checks for header files and their contents.
1168 AC_CHECK_HEADERS([getopt.h unistd.h ext/stdio_filebuf.h])
1170 # Checks for typedefs, structures, and compiler characteristics.
1172 # these are bad macros, they clash with system header <stdint.h> !!
1178 # guard against double-inclusion of the autoheader
1179 AH_TOP([#ifndef __CVC4__CVC4AUTOCONFIG_H
1180 #define __CVC4__CVC4AUTOCONFIG_H])
1181 AH_BOTTOM([#endif /* __CVC4__CVC4AUTOCONFIG_H */])
1183 AC_CHECK_DECLS([optreset], [], [], [#include <getopt.h>])
1185 # check with which standard strerror_r() complies
1188 # require boost library
1191 # look for boost threading library
1192 AC_ARG_WITH([portfolio],
1193 AS_HELP_STRING([--with-portfolio], [build the multithreaded portfolio version of CVC4 (pcvc4)]))
1194 cvc4_save_LDFLAGS="$LDFLAGS"
1195 if test "$enable_static_binary" = yes; then
1196 LDFLAGS="-static $LDFLAGS"
1198 cvc4_has_threads=yes
1199 AC_ARG_ENABLE([thread-support],
1200 AS_HELP_STRING([--disable-thread-support], [do not support multithreaded-capable library]))
1201 if test "$enable_thread_support" = no; then
1203 if test "$with_portfolio" = yes; then
1204 AC_MSG_ERROR([user gave both --with-portfolio and --disable-thread-support, which are contradictory])
1207 BOOST_THREADS([], [AC_MSG_WARN([disabling multithreaded support])
1208 cvc4_has_threads=no])
1210 LDFLAGS="$cvc4_save_LDFLAGS"
1211 if test $cvc4_has_threads = no; then
1212 if test "$enable_thread_support" = yes; then
1213 AC_MSG_ERROR([user gave --enable-thread-support but could not build with threads; maybe boost threading library is missing?])
1215 if test "$with_portfolio" = yes; then
1216 AC_MSG_ERROR([user gave --with-portfolio but could not build with threads; maybe boost threading library is missing?])
1220 if test "$with_portfolio" != yes; then
1223 AM_CONDITIONAL([CVC4_BUILD_PCVC4], [test "$with_portfolio" = yes])
1224 if test "$with_portfolio" = yes; then
1225 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PORTFOLIO"
1227 # see if Boost has thread attributes (should be any version >= 1.50.0)
1228 # non-fatal error if not, but we won't support --thread-stack option
1229 AC_MSG_CHECKING([whether Boost threads support thread attrs])
1231 cvc4_save_CPPFLAGS="$CPPFLAGS"
1232 cvc4_save_LIBS="$LIBS"
1233 cvc4_save_LDFLAGS="$LDFLAGS"
1234 CPPFLAGS="$CPPFLAGS $BOOST_CPPFLAGS"
1235 LIBS="$LIBS $BOOST_THREAD_LIBS"
1236 LDFLAGS="$LDFLAGS $BOOST_THREAD_LDFLAGS"
1237 AC_LINK_IFELSE([AC_LANG_PROGRAM([#include <boost/thread.hpp>],
1238 [boost::thread::attributes attrs; attrs.set_stack_size(10 * 1024 * 1024);])],
1239 [cvc4_boost_has_thread_attr=1;
1240 AC_MSG_RESULT([yes])],
1241 [cvc4_boost_has_thread_attr=0;
1242 AC_MSG_RESULT([no])])
1243 CPPFLAGS="$cvc4_save_CPPFLAGS"
1244 LIBS="$cvc4_save_LIBS"
1245 LDFLAGS="$cvc4_save_LDFLAGS"
1248 cvc4_boost_has_thread_attr=0
1250 AC_DEFINE_UNQUOTED([BOOST_HAS_THREAD_ATTR], $cvc4_boost_has_thread_attr, [Define to 1 if Boost threading library has support for thread attributes])
1252 # Check for libreadline (defined in config/readline.m4)
1253 AC_ARG_WITH([readline], [AS_HELP_STRING([--with-readline], [support the readline library])], [], [with_readline=check])
1254 # make the flags as close as possible to the final flags, because the Boost
1255 # flags can bring in a different, incompatible readline library than we'd
1256 # get otherwise (e.g. on Mac, where there are commonly two different readlines,
1257 # one in /usr and one in /opt/local)
1258 cvc4_rlcheck_save_CPPFLAGS="$CPPFLAGS"
1259 cvc4_rlcheck_save_CXXFLAGS="$CXXFLAGS"
1260 cvc4_rlcheck_save_CFLAGS="$CFLAGS"
1261 cvc4_rlcheck_save_LDFLAGS="$LDFLAGS"
1262 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
1263 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS $WNO_DEPRECATED"
1264 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS $C_WNO_DEPRECATED -fexceptions"
1265 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
1266 CVC4_CHECK_FOR_READLINE
1267 CPPFLAGS="$cvc4_rlcheck_save_CPPFLAGS"
1268 CXXFLAGS="$cvc4_rlcheck_save_CXXFLAGS"
1269 CFLAGS="$cvc4_rlcheck_save_CFLAGS"
1270 LDFLAGS="$cvc4_rlcheck_save_LDFLAGS"
1271 AC_DEFINE_UNQUOTED([HAVE_LIBREADLINE], $have_libreadline, [Define to 1 to use libreadline])
1272 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])
1273 AC_SUBST([READLINE_LIBS])
1275 # Whether to compile with google profiling tools
1276 cvc4_use_google_perftools=0
1280 [--with-google-perftools],
1281 [use Google Performance Tools]
1283 [if test "$withval" != no; then
1284 cvc4_use_google_perftools=1
1288 AC_MSG_CHECKING([whether to link in google perftools libraries])
1289 if test $cvc4_use_google_perftools = 1; then
1290 AC_MSG_RESULT([yes])
1291 AC_CHECK_LIB([tcmalloc], [MallocExtension_GetAllocatedSize], , [AC_MSG_ERROR([cannot link google-perftools test program with -ltcmalloc])], [-lpthread])
1292 AC_CHECK_LIB([profiler], [ProfilerStart], , [AC_MSG_ERROR([cannot link google-perftools test program with -lprofiler])], [-lpthread])
1294 AC_MSG_RESULT([no (user didn't request it)])
1298 AC_ARG_VAR(JAVA, [Java interpreter (used when testing Java interface)])
1299 AC_ARG_VAR(JAVAC, [Java compiler (used when building and testing Java interface)])
1300 AC_ARG_VAR(JAVAH, [Java compiler (used when building and testing Java interface)])
1301 AC_ARG_VAR(JAR, [Jar archiver (used when building Java interface)])
1302 if test "$cvc4_build_java_bindings"; then
1304 if test -z "$JAVA"; then
1305 AC_CHECK_PROGS(JAVA, java, java, [])
1307 AC_CHECK_PROG(JAVA, "$JAVA", "$JAVA", [])
1309 if test -z "$JAVAC"; then
1310 AC_CHECK_PROGS(JAVAC, javac gcj, javac, [])
1311 if test "$JAVAC" = gcj; then JAVAC='gcj -C'; fi
1313 AC_CHECK_PROG(JAVAC, "$JAVAC", "$JAVAC", [])
1315 if test -z "$JAVAH"; then
1316 AC_CHECK_PROGS(JAVAH, javah gcjh, javah, [])
1318 AC_CHECK_PROG(JAVAH, "$JAVAH", "$JAVAH", [])
1320 if test -z "$JAR"; then
1321 AC_CHECK_PROGS(JAR, jar, jar, [])
1323 AC_CHECK_PROG(JAR, "$JAR", "$JAR", [])
1327 # on Mac OS X, Java doesn't like the .so module extension; it wants .dylib
1328 module=no eval CVC4_JAVA_MODULE_EXT="$shrext_cmds"
1329 if test -z "$CVC4_JAVA_MODULE_EXT"; then
1330 CVC4_JAVA_MODULE_EXT=.so
1332 AC_SUBST([CVC4_JAVA_MODULE_EXT])
1334 # Prepare configure output
1336 if test "$enable_shared" = yes; then BUILDING_SHARED=1; else BUILDING_SHARED=0; fi
1337 if test "$enable_static" = yes; then BUILDING_STATIC=1; else BUILDING_STATIC=0; fi
1338 if test "$enable_static_binary" = yes; then STATIC_BINARY=1; else STATIC_BINARY=0; fi
1339 AC_SUBST(BUILDING_SHARED)
1340 AC_SUBST(BUILDING_STATIC)
1341 AC_SUBST(STATIC_BINARY)
1342 AM_CONDITIONAL([STATIC_BINARY], [test "$enable_static_binary" = yes])
1343 AM_CONDITIONAL([COVERAGE_ENABLED], [test "$enable_coverage" = yes])
1344 AC_SUBST([COVERAGE_ON])
1346 AM_CONDITIONAL([CVC4_DEBUG], [test "$with_build" = debug])
1347 AM_CONDITIONAL([CVC4_TRACING], [test "$enable_tracing" = yes])
1349 AC_SUBST(CVC4_LIBRARY_VERSION)
1350 AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
1351 AC_SUBST(CVC4_BINDINGS_LIBRARY_VERSION)
1353 AC_DEFINE_UNQUOTED(CVC4_MAJOR, ${CVC4_MAJOR}, [Major component of the version of CVC4.])
1354 AC_DEFINE_UNQUOTED(CVC4_MINOR, ${CVC4_MINOR}, [Minor component of the version of CVC4.])
1355 AC_DEFINE_UNQUOTED(CVC4_RELEASE, ${CVC4_RELEASE}, [Release component of the version of CVC4.])
1356 AC_DEFINE_UNQUOTED(CVC4_EXTRAVERSION, ["${CVC4_EXTRAVERSION}"], [Extraversion component of the version of CVC4.])
1357 AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full release string for CVC4.])
1359 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
1360 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
1361 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions"
1362 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
1364 # visibility flag not supported for Windows builds
1365 # also increase default stack size for Windows binaries
1368 (*mingw*) FLAG_VISIBILITY_HIDDEN=
1369 cvc4_LDFLAGS=-Wl,--stack,134217728
1370 pcvc4_LDFLAGS=-Wl,--stack,134217728
1374 AM_CONDITIONAL([CVC4_WINDOWS_BUILD], [test "$windows_build" = "yes"])
1376 AC_SUBST(FLAG_VISIBILITY_HIDDEN)
1377 AC_SUBST(cvc4_LDFLAGS)
1378 AC_SUBST(pcvc4_LDFLAGS)
1380 AM_CONDITIONAL(WHITE_AND_BLACK_TESTS, [test -z "$FLAG_VISIBILITY_HIDDEN"])
1382 # remember the command line used for configure
1383 AC_SUBST(cvc4_config_cmdline)
1387 # When automake scans Makefiles, it complains about non-standard make
1388 # features (including GNU extensions), and breaks GNU Make's
1389 # "if/endif" construct, replacing the "if" with AM_CONDITIONAL if
1390 # constructs. automake even follows "include" and messes with
1391 # included Makefiles.
1393 # CVC4 assumes GNU Make and we want to use GNU Make if/endifs, so we
1394 # have to hide some included Makefiles with GNU extensions. We do
1395 # this by defining mk_include as an autoconf substitution and then
1396 # using "@mk_include@ other_makefile" in Makefile.am to include
1397 # makefiles with GNU extensions; this hides them from automake.
1399 AC_SUBST(mk_include)
1400 # Similar trickery for "if"
1408 # This is used to _always_ comment out rules in automake makefiles, but
1409 # still trigger certain automake behavior; see test/unit/Makefile.am.
1410 AM_CONDITIONAL([CVC4_FALSE], [false])
1412 # set up substitutions for src/util/{rational,integer}.h.in
1413 if test $cvc4_cln_or_gmp = cln; then
1420 AC_SUBST(CVC4_USE_CLN_IMP)
1421 AC_SUBST(CVC4_USE_GMP_IMP)
1423 # month/year for man pages
1424 MAN_DATE=`date '+%B %Y'`
1430 proofs/signatures/Makefile]
1431 m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | grep -v '^contrib/alttheoryskel/' | sort | sed 's,\.am$,,'])
1434 if test $cvc4_has_threads = yes; then
1435 support_multithreaded='with boost threading library'
1436 AM_CONDITIONAL([CVC4_HAS_THREADS], [true])
1437 AC_SUBST([CVC4_HAS_THREADS], 1)
1439 support_multithreaded='no'
1440 AM_CONDITIONAL([CVC4_HAS_THREADS], [false])
1441 AC_SUBST([CVC4_HAS_THREADS], 0)
1444 # Final information to the user
1448 if test "$custom_build_profile" = yes; then
1449 with_build="$with_build (customized)"
1452 support_unit_tests='cxxtest not found; unit tests not supported'
1453 if test -n "$CXXTEST"; then
1454 support_unit_tests='unit testing infrastructure enabled in build directory'
1455 elif test "$enable_unit_testing" = no; then
1456 support_unit_tests='unit testing disabled by user'
1459 if test "$enable_optimized" = yes; then
1460 optimized="yes, at level $OPTLEVEL"
1465 if test $have_libglpk -eq 1; then
1467 gpllibs="${gpllibs} glpk"
1470 if test $have_libreadline -eq 1; then
1472 gpllibs="${gpllibs} readline"
1475 if test $cvc4_cln_or_gmp = cln; then
1476 mplibrary='cln (GPL)'
1478 gpllibs="${gpllibs} cln"
1479 if test $with_portfolio = yes; then
1480 AC_ERROR([Bad configuration detected: cannot build portfolio with CLN.
1481 Please specify only one of --with-portfolio and --with-cln.])
1487 if test "$gpl" = yes; then
1488 if test "$CVC4_BSD_LICENSED_CODE_ONLY" = 1; then
1489 AC_ERROR([Bad configuration detected: BSD-licensed code only, but also requested GPLed libraries:$gpllibs
1490 To permit GPL'ed dependences, use the configure flag --enable-gpl])
1493 licensewarn="${licensewarn}"'****************************************************************************
1494 Please note that CVC4 will be built against the following GPLed libraries:
1496 As these libraries are covered under the GPLv3, so is this build of CVC4.
1497 CVC4 is also available to you under the terms of the (modified) BSD license.
1498 If you prefer to license CVC4 under those terms, please configure with the
1499 option "--bsd", which will disable all optional GPLed library dependences.
1500 ****************************************************************************
1503 license="GPLv3 (due to optional libraries; see below)"
1505 licensewarn="${licensewarn}Please note that this configuration is NOT built against any GPL'ed
1506 libraries, so it is covered by the (modified) BSD license. This is,
1507 however, not the best-performing configuration of CVC4. To build
1508 against GPL'ed libraries which improve CVC4's performance, re-configure
1509 with '--best --enable-gpl'.
1512 license="modified BSD"
1515 if test "$gpl" = yes; then isgpl=1; else isgpl=0; fi
1516 AC_DEFINE_UNQUOTED(CVC4_GPL_DEPS, $isgpl, [Whether CVC4 is built with the (optional) GPLed library dependences.])
1518 CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="$CVC4_BINDINGS_LIBRARY_VERSION"
1519 if test -z "$CVC4_LANGUAGE_BINDINGS"; then
1520 CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="N/A"
1523 bindings_to_be_built=none
1524 if test -n "$CVC4_LANGUAGE_BINDINGS"; then
1525 bindings_to_be_built="$CVC4_LANGUAGE_BINDINGS"
1528 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/floatingpoint.h])
1529 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
1530 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
1532 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template])
1533 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5])
1534 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3])
1535 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc_template])
1536 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc_template])
1537 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3])
1545 Build profile: $with_build
1546 Build ID : $build_type
1547 Optimized : $optimized
1548 Debug symbols: $enable_debug_symbols
1549 Proofs : $enable_proof
1550 Statistics : $enable_statistics
1551 Replay : $enable_replay
1552 Assertions : $enable_assertions
1553 Tracing : $enable_tracing
1554 Dumping : $enable_dumping
1555 Muzzle : $enable_muzzle
1557 Unit tests : $support_unit_tests
1558 gcov support : $enable_coverage
1559 gprof support: $enable_profiling
1561 Static libs : $enable_static
1562 Shared libs : $enable_shared
1563 Static binary: $enable_static_binary
1564 Bindings : $bindings_to_be_built
1566 Multithreaded: $support_multithreaded
1567 Portfolio : $with_portfolio
1570 CaDiCaL : $with_cadical
1571 Cryptominisat: $with_cryptominisat
1574 MP library : $mplibrary
1575 Readline : $with_readline
1576 SymFPU : $with_symfpu
1578 CPPFLAGS : $CPPFLAGS
1579 CXXFLAGS : $CXXFLAGS
1584 libcvc4 version : $CVC4_LIBRARY_VERSION
1585 libcvc4parser version : $CVC4_PARSER_LIBRARY_VERSION
1586 libcvc4bindings version: $CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild
1588 Install into : $prefix
1590 CVC4 license : $license
1592 ${licensewarn}Now just type make, followed by make check or make install, as you like.
1596 if test -n "$CVC4_UNSUPPORTED_LANGUAGE_BINDINGS"; then
1598 AC_MSG_WARN([You are electing to build unsupported language binding(s):])
1599 AC_MSG_WARN([ $CVC4_UNSUPPORTED_LANGUAGE_BINDINGS])
1600 AC_MSG_WARN([Please be aware that these bindings may not compile, or])
1601 AC_MSG_WARN([work, and the interface to CVC4 via these bindings may])
1602 AC_MSG_WARN([change drastically in upcoming releases of CVC4.])
1606 if test -n "$CVC4_INTEGRITY_WARNING"; then
1608 AC_MSG_WARN($CVC4_INTEGRITY_WARNING)
1609 AC_MSG_WARN([Please run "make check" after building to ensure integrity of the binary and library])