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, 5) 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, [cvc-bugs@cs.nyu.edu])
15 AC_CONFIG_SRCDIR([src/include/cvc4_public.h])
16 AC_CONFIG_AUX_DIR([config])
17 AC_CONFIG_MACRO_DIR([config])
18 AC_CONFIG_LIBOBJ_DIR([src/lib])
19 AC_CONFIG_SUBDIRS([proofs/lfsc_checker])
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 the AC_CANONICAL_* macros destroy the command line you get
68 # from $@, which we want later for determining the build profile. So
69 # we save it. (We can't do our build profile stuff here, or it's not
70 # included in the output... autoconf overrides us on the orderings of
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
103 if test "$enable_shared" = no -a "$user_specified_enable_or_disable_shared" = yes; then
107 # Features requested by the user
108 AC_MSG_CHECKING([for requested build profile])
110 [AS_HELP_STRING([--with-build=profile],
111 [for profile in {production,debug,competition,personal}])])
113 if test -z "${with_build+set}"; then
114 with_build=production
116 if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_dumping+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}" -a -z "${enable_replay+set}" -a -z "${with_gmp+set}" -a -z "${with_cln+set}" -a -z "${with_glpk+set}" -a -z "${with_abc+set}" -a -z "${with_cryptominisat+set}"; then
117 custom_build_profile=no
119 custom_build_profile=yes
122 if test -n "${enable_optimized+set}"; then
123 if test "$enable_optimized" = yes; then
124 btargs="$btargs optimized"
126 btargs="$btargs nooptimized"
129 # --enable-staticbinary is an alias for --enable-static-binary
130 if test -n "${enable_staticbinary+set}"; then
131 enable_static_binary="$enable_staticbinary"
133 if test -n "${enable_static_binary+set}"; then
134 if test "$enable_static_binary" = yes; then
135 btargs="$btargs staticbinary"
137 btargs="$btargs nostaticbinary"
140 if test -n "${enable_debug_symbols+set}"; then
141 if test "$enable_debug_symbols" = yes; then
142 btargs="$btargs debugsymbols"
144 btargs="$btargs nodebugsymbols"
147 if test -n "${enable_assertions+set}"; then
148 if test "$enable_assertions" = yes; then
149 btargs="$btargs assertions"
151 btargs="$btargs noassertions"
154 if test -n "${enable_proof+set}"; then
155 if test "$enable_proof" = yes; then
156 btargs="$btargs proof"
158 btargs="$btargs noproof"
161 if test -n "${enable_tracing+set}"; then
162 if test "$enable_tracing" = yes; then
163 btargs="$btargs tracing"
165 btargs="$btargs notracing"
168 if test -n "${enable_dumping+set}"; then
169 if test "$enable_dumping" = yes; then
170 btargs="$btargs dumping"
172 btargs="$btargs nodumping"
175 if test -n "${enable_muzzle+set}"; then
176 if test "$enable_muzzle" = yes; then
177 btargs="$btargs muzzle"
179 btargs="$btargs nomuzzle"
182 if test -n "${enable_coverage+set}"; then
183 if test "$enable_coverage" = yes; then
184 btargs="$btargs coverage"
186 btargs="$btargs nocoverage"
189 if test -n "${enable_profiling+set}"; then
190 if test "$enable_profiling" = yes; then
191 btargs="$btargs profiling"
193 btargs="$btargs noprofiling"
196 if test -n "${enable_statistics+set}"; then
197 if test "$enable_statistics" = yes; then
198 btargs="$btargs statistics"
200 btargs="$btargs nostatistics"
203 if test -n "${enable_replay+set}"; then
204 if test "$enable_replay" = yes; then
205 btargs="$btargs replay"
207 btargs="$btargs noreplay"
210 if test -n "${with_glpk+set}"; then
211 if test "$with_glpk" = yes; then
212 btargs="$btargs glpk"
215 if test -n "${with_abc+set}"; then
216 if test "$with_abc" = yes; then
220 if test -n "${with_cryptominisat+set}"; then
221 if test "$with_cryptominisat" = yes; then
222 btargs="$btargs cryptominisat"
226 AC_MSG_RESULT([$with_build])
228 AM_INIT_AUTOMAKE([1.11 no-define tar-pax parallel-tests color-tests subdir-objects])
229 AC_CONFIG_HEADERS([cvc4autoconfig.h])
231 # automake 1.12 changes the test driver mechanism in a way that is
232 # completely incompatible with 1.11. We figure out here which version
233 # we're using in order to set up test makefiles correctly.
234 # See http://lists.gnu.org/archive/html/automake/2012-04/msg00060.html
235 if test -z "$am__api_version"; then
236 AC_MSG_ERROR([Cannot determine automake API version ?!])
238 case "$am__api_version" in
239 1.11*) automake111=true ;;
240 *) automake111=false ;;
242 AM_CONDITIONAL([AUTOMAKE_1_11], [$automake111])
244 # Initialize libtool's configuration options.
245 # we're not DLL-clean yet (i.e., don't properly use dllexport and dllimport)
246 # _LT_SET_OPTION([LT_INIT],[win32-dll])
249 # Checks for programs.
263 [use CLN instead of GMP]
266 y|ye|yes|Y|YE|YES) cvc4_use_cln=1 ;;
267 n|no|N|NO) cvc4_use_cln=0 ;;
276 [use GMP instead of CLN]
279 y|ye|yes|Y|YE|YES) cvc4_use_gmp=1 ;;
280 n|no|N|NO) cvc4_use_gmp=0 ;;
285 if test $cvc4_use_cln = 1 -a $cvc4_use_gmp = 1 || test $cvc4_use_cln = 0 -a $cvc4_use_gmp = 0; then
286 AC_MSG_ERROR([You must use either CLN and GMP. Please pick one.])
288 if test $cvc4_use_gmp = 1; then
290 elif test $cvc4_use_gmp = 0; then
292 elif test $cvc4_use_cln = 1; then
294 elif test $cvc4_use_cln = 0; then
298 # try GMP, fail if not found; GMP is required for both CLN and for GMP
300 AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP (libgmp) not found, see http://gmplib.org/])])
302 if test $cvc4_use_cln = 2; then
303 if test "$CVC4_BSD_LICENSED_CODE_ONLY" = 1 -o "$with_portfolio" = yes; then
309 if test $cvc4_use_cln != 0; then
310 # [mdeters] The PKG_CHECK_MODULES macro isn't customizable and doesn't fail
311 # gracefully. You can only specify it once for a given library name. That
312 # is, even on separate if/else branches, you can't put
313 # PKG_CHECK_MODULES([CLN], ...). That's why things are so convoluted here,
314 # we have to have PKG_CHECK_MODULES _exactly_ once in configure.ac !
315 PKG_CHECK_MODULES([CLN], [cln >= 1.2.2],
318 save_CXXFLAGS="$CXXFLAGS"
319 LIBS="$CLN_LIBS $LIBS"
320 CXXFLAGS="$CLN_CFLAGS $CXXFLAGS"
321 AC_LINK_IFELSE([AC_LANG_PROGRAM([[#include <cln/cln.h>]], [[cln::cl_F pi = "3.1415926";]])], [
324 if test $cvc4_use_cln = 1; then
326 AC_MSG_ERROR([CLN installation missing, too old, or not functional for this architecture])
329 AC_MSG_NOTICE([CLN installation missing, too old, or not functional for this architecture, will use gmp instead])
334 CXXFLAGS="$save_CXXFLAGS"
338 [if test $cvc4_use_cln = 1; then
340 AC_MSG_ERROR([CLN not installed (or too old) or pkgconfig missing])
343 AC_MSG_NOTICE([CLN not installed (or too old) or pkgconfig missing, will use gmp])
350 if test $cvc4_use_cln = 0; then
351 # try GMPXX, fail if not found; don't need to link against it, only need its header
353 AC_CHECK_HEADER([gmpxx.h], , [AC_MSG_ERROR([GNU MP C++ library header (gmpxx.h) required but not found, see http://gmplib.org/])])
357 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }$CLN_CFLAGS"
358 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }$CLN_CFLAGS"
359 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }$CLN_CFLAGS"
360 LIBS="$CLN_LIBS${LIBS:+ $LIBS}"
364 if test $cvc4_cln_or_gmp = cln; then
365 AC_DEFINE_UNQUOTED(CVC4_CLN_IMP, [], [Defined if using the CLN multi-precision arithmetic library.])
367 AC_DEFINE_UNQUOTED(CVC4_GMP_IMP, [], [Defined if using the GMP multi-precision arithmetic library.])
369 AM_CONDITIONAL([CVC4_CLN_IMP], [test $cvc4_cln_or_gmp = cln])
370 AM_CONDITIONAL([CVC4_GMP_IMP], [test $cvc4_cln_or_gmp = gmp])
372 # construct the build string
373 AC_MSG_CHECKING([for appropriate build string])
374 if test -z "$ac_confdir"; then
377 build_type=`$ac_confdir/config/build-type $with_build $btargs $cvc4_cln_or_gmp`
378 AC_MSG_RESULT($build_type)
380 # Require building in target and build-specific build directory:
382 # If the configure script is invoked from the top-level source
383 # directory, it creates a suitable build directory (based on the build
384 # architecture and build profile from $build_type), changes into it,
385 # and reinvokes itself. CVC4_CONFIGURE_IN_BUILDS is an envariable
386 # that breaks any possibility of infinite recursion in this process.
387 AC_MSG_CHECKING([what dir to configure])
388 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
389 AC_MSG_RESULT([this one (in builds/)])
390 elif test "$CVC4_CONFIGURE_AT_TOP_LEVEL" = yes; then
391 AC_MSG_RESULT([builds/$target/$build_type])
393 if test -z "$ac_srcdir"; then
394 mkbuilddir=./config/mkbuilddir
396 mkbuilddir=$ac_srcdir/config/mkbuilddir
398 $as_echo "$mkbuilddir $target $build_type"
399 source $mkbuilddir "$target" "$build_type"
400 $as_echo "cd builds/$target/$build_type"
401 cd "builds/$target/$build_type"
402 CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS
403 # Runs the single recursive configure invocation using a relative path.
404 # See https://lists.gnu.org/archive/html/autoconf/2011-04/msg00060.html
405 echo "$SHELL ../../../configure ${config_cmdline[[@]]}"
406 "$SHELL" "../../../configure" "${config_cmdline[[@]]}"
409 if test $exitval -eq 0; then
410 cat >config.reconfig <<EOF
412 # Generated by configure, `date`
413 # This script is part of CVC4.
415 cd "\`dirname \\"\$0\\"\`"
417 if test -d builds; then :; else echo 'No builds/ directory!' >&2; exit; fi
419 current=(\`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]*\\)/\\(.*\\),\\1 \\2,'\`)
423 echo "reconfiguring in builds/\$arch/\$build..."
424 cd "builds/\$arch/\$build"
425 echo ./config.status "\$@"
426 ./config.status "\$@"]
428 chmod +x config.reconfig
430 ln -sf "$target/$build_type/config.log" "builds/config.log"
433 AC_MSG_RESULT([this one (user-specified)])
438 # Unpack standard build types. Any particular options can be overriden with
439 # --enable/disable-X options
440 # Tim: This needs to keep CVC4CPPFLAGS, CVC4CXXFLAGS, etc. set by earlier checks
441 case "$with_build" in
442 production) # highly optimized, no assertions, no tracing, dumping
443 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }"
444 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }"
445 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }"
446 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
447 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
448 if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=3 ; fi
449 if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
450 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
451 if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
452 if test -z "${enable_replay+set}" ; then enable_replay=no ; fi
453 if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi
454 if test -z "${enable_proof+set}" ; then enable_proof=yes ; fi
455 if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi
456 if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
457 if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
459 debug) # unoptimized, debug symbols, assertions, tracing, dumping
460 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DEBUG"
461 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-fno-inline"
462 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-fno-inline"
463 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
464 FLAG_VISIBILITY_HIDDEN=
465 if test -z "${enable_optimized+set}" ; then enable_optimized=no ; fi
466 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
467 if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
468 if test -z "${enable_replay+set}" ; then enable_replay=yes ; fi
469 if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi
470 if test -z "${enable_proof+set}" ; then enable_proof=yes ; fi
471 if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi
472 if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
473 if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
475 default) # moderately optimized, assertions, tracing, dumping
476 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }"
477 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }"
478 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }"
479 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
480 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
481 if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=2 ; fi
482 if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
483 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
484 if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
485 if test -z "${enable_replay+set}" ; then enable_replay=yes ; fi
486 if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi
487 if test -z "${enable_proof+set}" ; then enable_proof=yes ; fi
488 if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi
489 if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi
490 if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
492 competition) # maximally optimized, no assertions, no tracing, no dumping, muzzled
493 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COMPETITION_MODE"
494 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs"
495 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs"
496 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
497 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
498 if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=9 ; fi
499 if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
500 if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no ; fi
501 if test -z "${enable_statistics+set}" ; then enable_statistics=no ; fi
502 if test -z "${enable_replay+set}" ; then enable_replay=no ; fi
503 if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi
504 if test -z "${enable_proof+set}" ; then enable_proof=no ; fi
505 if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi
506 if test -z "${enable_dumping+set}" ; then enable_dumping=no ; fi
507 if test -z "${enable_muzzle+set}" ; then enable_muzzle=yes ; fi
508 if test -z "${user_specified_enable_or_disable_shared}"; then enable_shared=no; fi
509 if test -z "${user_specified_enable_or_disable_static}"; then enable_static=yes; fi
510 if test -z "${enable_static_binary+set}"; then enable_static_binary=yes ; fi
513 AC_MSG_FAILURE([unknown build profile: $with_build])
516 if test -z "${OPTLEVEL+set}"; then OPTLEVEL=3; fi
518 AM_CONDITIONAL([CVC4_BUILD_PROFILE_PRODUCTION], [test "$with_build" = production])
519 AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEBUG], [test "$with_build" = debug])
520 AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEFAULT], [test "$with_build" = default])
521 AM_CONDITIONAL([CVC4_BUILD_PROFILE_COMPETITION], [test "$with_build" = competition])
523 # permit a static binary
524 AC_MSG_CHECKING([whether to build a static binary])
525 AC_ARG_ENABLE([static-binary],
526 [AS_HELP_STRING([--enable-static-binary],
527 [build a fully statically-linked binary [default=no]])])
528 if test -z "${enable_static_binary+set}"; then
529 enable_static_binary=no
531 AC_MSG_RESULT([$enable_static_binary])
532 if test "$enable_static_binary" = yes; then
533 if test "$target_vendor" = apple; then
534 if test -z "$MAC_STATIC_BINARY_MANUAL_OVERRIDE"; then
535 AC_MSG_ERROR([[Statically-linked binaries are not supported on Mac OS. See https://developer.apple.com/library/mac/#qa/qa2001/qa1118.html . (If you ABSOLUTELY insist on this going forward and you know what you are doing, set MAC_STATIC_BINARY_MANUAL_OVERRIDE=1)]])
537 AC_MSG_WARN([MAC_STATIC_BINARY_MANUAL_OVERRIDE was set!])
538 AC_MSG_WARN([Will make a static binary during this build. Note that it may fail!])
541 if test "$enable_static" != yes; then
543 AC_MSG_WARN([forcing static-library building, --enable-static-binary given])
547 AC_MSG_CHECKING([whether to support proofs in libcvc4])
549 AC_ARG_ENABLE([proof],
550 [AS_HELP_STRING([--disable-proof],
551 [do not support proof generation])])
552 if test -z "${enable_proof+set}"; then
555 AC_MSG_RESULT([$enable_proof])
557 if test "$enable_proof" = yes; then
558 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROOF"
560 AM_CONDITIONAL([CVC4_PROOF], [test "$enable_proof" = yes])
562 AC_MSG_CHECKING([whether to optimize libcvc4])
564 AC_ARG_ENABLE([optimized],
565 [AS_HELP_STRING([--enable-optimized],
566 [optimize the build])])
568 if test -z "${enable_optimized+set}"; then
572 AC_MSG_RESULT([$enable_optimized])
574 if test "$enable_optimized" = yes; then
575 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O$OPTLEVEL"
576 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O$OPTLEVEL"
578 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O0"
579 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O0"
582 AC_MSG_CHECKING([whether to include debugging symbols in libcvc4])
584 AC_ARG_ENABLE([debug-symbols],
585 [AS_HELP_STRING([--disable-debug-symbols],
586 [do not include debug symbols in libcvc4])])
588 if test -z "${enable_debug_symbols+set}"; then
589 enable_debug_symbols=yes
592 AC_MSG_RESULT([$enable_debug_symbols])
594 if test "$enable_debug_symbols" = yes; then
595 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-ggdb3"
596 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-ggdb3"
599 AC_MSG_CHECKING([whether to include statistics are turned on in libcvc4])
601 AC_ARG_ENABLE([statistics],
602 [AS_HELP_STRING([--disable-statistics],
603 [do not include statistics in libcvc4])])
605 if test -z "${enable_statistics+set}"; then
606 enable_statistics=yes
609 AC_MSG_RESULT([$enable_statistics])
611 if test "$enable_statistics" = yes; then
612 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_STATISTICS_ON"
615 AC_MSG_CHECKING([whether the replay feature should be turned on in libcvc4])
617 AC_ARG_ENABLE([replay],
618 [AS_HELP_STRING([--disable-replay],
619 [turn off the replay feature in libcvc4])])
621 if test -z "${enable_replay+set}"; then
625 AC_MSG_RESULT([$enable_replay])
627 if test "$enable_replay" = yes; then
628 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_REPLAY"
631 AC_MSG_CHECKING([whether to include assertions in build])
633 AC_ARG_ENABLE([assertions],
634 [AS_HELP_STRING([--disable-assertions],
635 [turn off assertions in build])])
637 if test -z "${enable_assertions+set}"; then
638 enable_assertions=yes
641 AC_MSG_RESULT([$enable_assertions])
643 if test "$enable_assertions" = yes; then
644 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_ASSERTIONS"
646 # turn off regular C assert() also
647 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DNDEBUG"
650 AC_MSG_CHECKING([whether to do a traceable build of CVC4])
651 AC_ARG_ENABLE([tracing],
652 [AS_HELP_STRING([--disable-tracing],
653 [remove all tracing code from CVC4])])
655 if test -z "${enable_tracing+set}"; then
659 AC_MSG_RESULT([$enable_tracing])
661 if test "$enable_tracing" = yes; then
662 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_TRACING"
665 AC_MSG_CHECKING([whether to do a dump-capable build of CVC4])
666 AC_ARG_ENABLE([dumping],
667 [AS_HELP_STRING([--disable-dumping],
668 [remove all dumping code from CVC4])])
670 if test -z "${enable_dumping+set}"; then
674 AC_MSG_RESULT([$enable_dumping])
676 if test "$enable_dumping" = yes; then
677 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DUMPING"
680 AC_MSG_CHECKING([whether to do a muzzled build of CVC4])
681 AC_ARG_ENABLE([muzzle],
682 [AS_HELP_STRING([--enable-muzzle],
683 [completely silence CVC4; remove ALL non-result output from build])])
685 if test -z "${enable_muzzle+set}"; then
689 AC_MSG_RESULT([$enable_muzzle])
691 if test "$enable_muzzle" = yes; then
692 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_MUZZLE"
695 AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4])
696 AC_ARG_ENABLE([coverage],
697 [AS_HELP_STRING([--enable-coverage],
698 [build with support for gcov coverage testing])])
700 if test -z "${enable_coverage+set}"; then
704 AC_MSG_RESULT([$enable_coverage])
706 if test "$enable_coverage" = yes; then
707 # For coverage testing, we prefer:
708 # --enable-static --disable-shared --disable-static-binary
709 # If the user didn't specify these, we force them here. If the
710 # user specified them in opposite phase, give warnings that they
711 # shouldn't do that, or bomb out.
712 if test "$user_specified_enable_or_disable_shared" != yes; then
714 AC_MSG_WARN([turning off shared library building due to --enable-coverage])
715 elif test "$enable_shared" = yes; then
717 AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-shared])
718 AC_MSG_WARN([gcov does not support shared libraries, so only your static libraries will be coverage-testable.])
719 AC_MSG_WARN([Your cvc4 driver and testing binaries will not be coverage-testable.])
722 if test "${enable_static_binary+set}" = set -a "$enable_static_binary" = yes; then
724 AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-static-binary])
725 AC_MSG_WARN([Your cvc4 driver and testing binaries will be fully-statically linked and may not be coverage-testable.])
728 if test "$user_specified_enable_or_disable_static" != yes; then
730 AC_MSG_WARN([turning on static library building due to --enable-coverage])
731 elif test "$enable_static" != yes; then
732 AC_MSG_ERROR([--enable-coverage and --disable-static are incompatible; gcov only supports static libraries.])
735 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COVERAGE"
736 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }--coverage"
737 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }--coverage"
738 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }--coverage"
741 AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4])
743 AC_ARG_ENABLE([profiling],
744 [AS_HELP_STRING([--enable-profiling],
745 [build with support for gprof profiling])])
747 if test -z "${enable_profiling+set}"; then
751 AC_MSG_RESULT([$enable_profiling])
753 if test "$enable_profiling" = yes; then
754 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROFILING"
755 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-pg"
756 CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-pg"
757 CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }-pg"
760 # Check for libglpk (defined in config/glpk.m4)
762 [AS_HELP_STRING([--with-glpk],
763 [use GLPK simplex solver])], [], [with_glpk=])
765 if test $have_libglpk -eq 1; then
766 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_GLPK"
768 AM_CONDITIONAL([CVC4_USE_GLPK], [test $have_libglpk -eq 1])
769 AC_SUBST([GLPK_LDFLAGS])
770 AC_SUBST([GLPK_LIBS])
772 # Build with libabc (defined in config/abc.m4)
774 [AS_HELP_STRING([--with-abc],
775 [use the ABC AIG library])], [], [with_abc=])
777 if test $have_libabc -eq 1; then
778 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_ABC"
780 AM_CONDITIONAL([CVC4_USE_ABC], [test $have_libabc -eq 1])
781 AC_SUBST([ABC_LDFLAGS])
785 # Build with libcryptominisat
786 AC_ARG_WITH([cryptominisat],
787 [AS_HELP_STRING([--with-cryptominisat],
788 [use the CRYPTOMINISAT sat solver])], [], [with_cryptominisat=])
789 CVC4_CHECK_FOR_CRYPTOMINISAT
790 if test $have_libcryptominisat -eq 1; then
791 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_CRYPTOMINISAT"
792 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$CRYPTOMINISAT_HOME/install/include"
794 AM_CONDITIONAL([CVC4_USE_CRYPTOMINISAT], [test $have_libcryptominisat -eq 1])
795 AC_SUBST([CRYPTOMINISAT_LDFLAGS])
796 AC_SUBST([CRYPTOMINISAT_LIBS])
799 # Check to see if this version/architecture of GNU C++ explicitly
800 # instantiates __gnu_cxx::hash<uint64_t> or not. Some do, some don't.
801 # See src/util/hash.h.
802 AC_MSG_CHECKING([whether __gnu_cxx::hash<uint64_t> is already specialized])
804 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
806 #include <ext/hash_map>
807 namespace __gnu_cxx { template<> struct hash<uint64_t> {}; }])],
808 [AC_MSG_RESULT([no]); CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_NEED_HASH_UINT64_T"],
809 [AC_MSG_RESULT([yes])])
812 # Check whether "long" and "int64_t" are distinct types w.r.t. overloading.
813 # Even if they have the same size, they can be distinct, and some platforms
814 # can have problems with ambiguous function calls when auto-converting
815 # int64_t to long, and others will complain if you overload a function
816 # that takes an int64_t with one that takes a long (giving a redefinition
817 # error). So we have to keep both happy. Probably the same underlying
818 # issue as the hash specialization above, but let's check separately
820 AC_MSG_CHECKING([for the relationship between long and int64_t])
822 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
825 void foo(int64_t) {}])],
826 [AC_MSG_RESULT([no relationship detected]); CVC4_NEED_INT64_T_OVERLOADS=1],
827 [AC_MSG_RESULT([typedef or similar]); CVC4_NEED_INT64_T_OVERLOADS=0])
829 AC_SUBST([CVC4_NEED_INT64_T_OVERLOADS])
831 # Check for ANTLR runantlr script (defined in config/antlr.m4)
834 CVC4_CXX_OPTION([-Werror], [WERROR])
835 CVC4_C_OPTION([-Werror], [C_WERROR])
836 CVC4_CXX_OPTION([-Wno-deprecated], [WNO_DEPRECATED])
837 CVC4_C_OPTION([-Wno-deprecated], [C_WNO_DEPRECATED])
838 CVC4_CXX_OPTION([-Wno-conversion-null], [WNO_CONVERSION_NULL])
839 CVC4_CXX_OPTION([-Wno-tautological-compare], [WNO_TAUTOLOGICAL_COMPARE])
840 CVC4_CXX_OPTION([-Wno-parentheses], [WNO_PARENTHESES])
841 CVC4_CXX_OPTION([-Wno-uninitialized], [WNO_UNINITIALIZED])
842 CVC4_CXX_OPTION([-Wno-unused-variable], [WNO_UNUSED_VARIABLE])
843 CVC4_CXX_OPTION([-fno-strict-aliasing], [FNO_STRICT_ALIASING])
845 AC_SUBST([WNO_CONVERSION_NULL])
846 AC_SUBST([WNO_TAUTOLOGICAL_COMPARE])
847 AC_SUBST([WNO_PARENTHESES])
848 AC_SUBST([WNO_UNINITIALIZED])
849 AC_SUBST([WNO_UNUSED_VARIABLE])
850 AC_SUBST([FNO_STRICT_ALIASING])
852 # On Mac, we have to fix the visibility of standard library symbols.
853 # Otherwise, exported template instantiations---even though explicitly
854 # CVC4_PUBLIC, can be generated as symbols with internal-only linkage.
855 # Presumably, Apple is distributing a libstdc++ that is built *without*
856 # --enable-libstdcxx-visibility (?)
857 if test "$target_vendor" = apple; then
858 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-D_GLIBCXX_VISIBILITY_DEFAULT=\"__attribute__((__visibility__(\\\"default\\\")))\""
861 # Tell top-level Makefile to include $(top_srcdir)/personal.mk
862 AC_ARG_ENABLE([personal-make-rules],
863 [AS_HELP_STRING([--enable-personal-make-rules],
864 [include top-level personal.mk (if it exists)])])
865 if test "$enable_personal_make_rules" = yes; then
866 # This allows us to include a personal.mk makefile from every
867 # generated makefile. Named zz_* in order to make sure this
868 # comes last, so it gets other definitions (in particular top_srcdir).
869 zz_cvc4_use_personal_make_rules='yes
872 include $(top_srcdir)/personal.mk
873 $(top_srcdir)/personal.mk:; @touch "$@"'
874 AC_SUBST([zz_cvc4_use_personal_make_rules])
877 # Doxygen configuration
878 AC_ARG_ENABLE([internals-documentation],
879 [AS_HELP_STRING([--enable-internals-documentation],
880 [build Doxygen documentation for static and private member functions])])
881 if test "$enable_internals_documentation" = yes; then
882 DOXYGEN_EXTRACT_PRIVATE=YES
883 DOXYGEN_EXTRACT_STATIC=YES
885 DOXYGEN_EXTRACT_PRIVATE=NO
886 DOXYGEN_EXTRACT_STATIC=NO
888 AC_SUBST([DOXYGEN_EXTRACT_PRIVATE])
889 AC_SUBST([DOXYGEN_EXTRACT_STATIC])
895 DX_INIT_DOXYGEN($PACKAGE_NAME, config/doxygen.cfg, $srcdir/doc/doxygen)
897 AC_ARG_ENABLE([unit-testing], AS_HELP_STRING([--disable-unit-testing], [don't build support for unit testing, even if available]), , [enable_unit_testing=check])
898 AC_ARG_VAR(CXXTEST, [path to CxxTest installation])
902 AC_ARG_WITH([cxxtest-dir],
903 [AS_HELP_STRING([--with-cxxtest-dir=DIR], [path to CxxTest installation])],
904 [CXXTEST="$withval"])
906 # In the case of "./configure --with-cxxtest-dir=../cxxtest" (or other
907 # relative path) and having switched the configure directory (see above),
908 # search with respect to the top source dir, not the build dir
909 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes -a -n "$CXXTEST"; then
912 *) CXXTEST="$srcdir/$CXXTEST" ;;
918 if test "$enable_proof" = yes; then
919 RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--proof"
921 AC_SUBST([TESTS_ENVIRONMENT])
922 AC_SUBST([RUN_REGRESSION_ARGS])
925 AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH])
926 if test -z "$CXXTESTGEN"; then
927 AC_PATH_PROG(CXXTESTGEN, cxxtestgen.py, [], [$CXXTEST:$PATH])
929 if test -z "$CXXTESTGEN"; then
930 AC_PATH_PROG(CXXTESTGEN, cxxtestgen, [], [$CXXTEST:$PATH])
932 # The latest version of cxxtest distributed from the git repository places
933 # cxxtest under <cxxtest-root>/bin/cxxtest
934 if test -z "$CXXTESTGEN"; then
935 AC_PATH_PROG(CXXTESTGEN, cxxtestgen, [], [$CXXTEST/bin:$PATH])
937 if test "$enable_unit_testing" = "no"; then
938 AC_MSG_NOTICE([unit tests disabled by user request.])
941 elif test -z "$CXXTESTGEN"; then
942 AC_MSG_NOTICE([unit tests disabled, could not find cxxtestgen.pl or cxxtestgen.py or cxxtestgen])
943 elif test -z "$CXXTEST"; then
944 CXXTEST=`dirname "$CXXTESTGEN"`
945 AC_MSG_CHECKING([for location of CxxTest headers])
946 if test -e "$CXXTEST/cxxtest/TestRunner.h"; then
947 AC_MSG_RESULT([$CXXTEST])
949 if test -e "/usr/include/cxxtest/TestRunner.h"; then
950 AC_MSG_RESULT([/usr/include])
952 AC_MSG_RESULT([not found])
953 AC_MSG_WARN([unit tests disabled, CxxTest headers not found.])
960 if test "$enable_unit_testing" = yes -a -z "$CXXTESTGEN"; then
961 AC_MSG_ERROR([--enable-unit-testing given but cxxtest not found.])
964 AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"])
966 AC_ARG_VAR(TEST_CPPFLAGS, [CPPFLAGS to use when testing (default=$CPPFLAGS)])
967 AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)])
968 AC_ARG_VAR(TEST_LDFLAGS, [LDFLAGS to use when testing (default=$LDFLAGS)])
970 AC_ARG_VAR(PERL, [PERL interpreter (used when testing)])
972 if test -n "$CXXTEST"; then
973 if test -z "$PERL"; then
974 AC_CHECK_PROGS(PERL, perl, perl, [])
976 AC_CHECK_PROG(PERL, "$PERL", "$PERL", [])
979 if test -z "$PERL"; then
980 AC_MSG_WARN([unit tests disabled, perl not found.])
986 AC_ARG_VAR(PYTHON, [PYTHON interpreter (used for building legacy Java library interface)])
988 if test -z "$PYTHON"; then
989 AC_CHECK_PROGS(PYTHON, python, python, [])
991 AC_CHECK_PROG(PYTHON, "$PYTHON", "$PYTHON", [])
994 if test -z "$PYTHON"; then
995 AC_MSG_WARN([python not found, cannot build libcvc4compat_java (the legacy Java interface).])
1000 # Checks for libraries.
1002 AC_SEARCH_LIBS([clock_gettime], [rt pthread],
1003 [AC_DEFINE([HAVE_CLOCK_GETTIME], [1],
1004 [Defined to 1 if clock_gettime() is supported by the platform.])],
1005 [AC_LIBOBJ([clock_gettime])])
1006 AC_CHECK_FUNC([strtok_r], [AC_DEFINE([HAVE_STRTOK_R], [1],
1007 [Defined to 1 if strtok_r() is supported by the platform.])])
1008 AC_CHECK_FUNC([ffs], [AC_DEFINE([HAVE_FFS], [1],
1009 [Defined to 1 if ffs() is supported by the platform.])])
1011 AC_LIBOBJ([strtok_r ffs])
1013 # Check for antlr C++ runtime (defined in config/antlr.m4)
1016 # Check for user preferences for language bindings to build, and for
1017 # build support. The arg list is the default set if unspecified by
1018 # the user (the actual built set is the subset that appears to be
1019 # supported by the build host).
1020 CVC4_CHECK_BINDINGS([c java])dnl csharp perl php python ruby tcl ocaml])
1022 # Checks for header files and their contents.
1023 AC_CHECK_HEADERS([getopt.h unistd.h ext/stdio_filebuf.h])
1025 # Checks for typedefs, structures, and compiler characteristics.
1027 # these are bad macros, they clash with system header <stdint.h> !!
1033 # guard against double-inclusion of the autoheader
1034 AH_TOP([#ifndef __CVC4__CVC4AUTOCONFIG_H
1035 #define __CVC4__CVC4AUTOCONFIG_H])
1036 AH_BOTTOM([#endif /* __CVC4__CVC4AUTOCONFIG_H */])
1038 AC_CHECK_DECLS([optreset], [], [], [#include <getopt.h>])
1040 # check with which standard strerror_r() complies
1043 # is is_sorted() in std or __gnu_cxx?
1046 # require boost library
1049 # look for boost threading library
1050 AC_ARG_WITH([portfolio],
1051 AS_HELP_STRING([--with-portfolio], [build the multithreaded portfolio version of CVC4 (pcvc4)]))
1052 cvc4_save_LDFLAGS="$LDFLAGS"
1053 if test "$enable_static_binary" = yes; then
1054 LDFLAGS="-static $LDFLAGS"
1056 cvc4_has_threads=yes
1057 AC_ARG_ENABLE([thread-support],
1058 AS_HELP_STRING([--disable-thread-support], [do not support multithreaded-capable library]))
1059 if test "$enable_thread_support" = no; then
1061 if test "$with_portfolio" = yes; then
1062 AC_MSG_ERROR([user gave both --with-portfolio and --disable-thread-support, which are contradictory])
1065 BOOST_THREADS([], [AC_MSG_WARN([disabling multithreaded support])
1066 cvc4_has_threads=no])
1068 LDFLAGS="$cvc4_save_LDFLAGS"
1069 if test $cvc4_has_threads = no; then
1070 if test "$enable_thread_support" = yes; then
1071 AC_MSG_ERROR([user gave --enable-thread-support but could not build with threads; maybe boost threading library is missing?])
1073 if test "$with_portfolio" = yes; then
1074 AC_MSG_ERROR([user gave --with-portfolio but could not build with threads; maybe boost threading library is missing?])
1078 if test "$with_portfolio" != yes; then
1081 AM_CONDITIONAL([CVC4_BUILD_PCVC4], [test "$with_portfolio" = yes])
1082 if test "$with_portfolio" = yes; then
1083 CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PORTFOLIO"
1085 # see if Boost has thread attributes (should be any version >= 1.50.0)
1086 # non-fatal error if not, but we won't support --thread-stack option
1087 AC_MSG_CHECKING([whether Boost threads support thread attrs])
1089 cvc4_save_CPPFLAGS="$CPPFLAGS"
1090 cvc4_save_LIBS="$LIBS"
1091 cvc4_save_LDFLAGS="$LDFLAGS"
1092 CPPFLAGS="$CPPFLAGS $BOOST_CPPFLAGS"
1093 LIBS="$LIBS $BOOST_THREAD_LIBS"
1094 LDFLAGS="$LDFLAGS $BOOST_THREAD_LDFLAGS"
1095 AC_LINK_IFELSE([AC_LANG_PROGRAM([#include <boost/thread.hpp>],
1096 [boost::thread::attributes attrs; attrs.set_stack_size(10 * 1024 * 1024);])],
1097 [cvc4_boost_has_thread_attr=1;
1098 AC_MSG_RESULT([yes])],
1099 [cvc4_boost_has_thread_attr=0;
1100 AC_MSG_RESULT([no])])
1101 CPPFLAGS="$cvc4_save_CPPFLAGS"
1102 LIBS="$cvc4_save_LIBS"
1103 LDFLAGS="$cvc4_save_LDFLAGS"
1106 cvc4_boost_has_thread_attr=0
1108 AC_DEFINE_UNQUOTED([BOOST_HAS_THREAD_ATTR], $cvc4_boost_has_thread_attr, [Define to 1 if Boost threading library has support for thread attributes])
1110 # Check for libreadline (defined in config/readline.m4)
1111 AC_ARG_WITH([readline], [AS_HELP_STRING([--with-readline], [support the readline library])], [], [with_readline=check])
1112 # make the flags as close as possible to the final flags, because the Boost
1113 # flags can bring in a different, incompatible readline library than we'd
1114 # get otherwise (e.g. on Mac, where there are commonly two different readlines,
1115 # one in /usr and one in /opt/local)
1116 cvc4_rlcheck_save_CPPFLAGS="$CPPFLAGS"
1117 cvc4_rlcheck_save_CXXFLAGS="$CXXFLAGS"
1118 cvc4_rlcheck_save_CFLAGS="$CFLAGS"
1119 cvc4_rlcheck_save_LDFLAGS="$LDFLAGS"
1120 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
1121 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS $WNO_DEPRECATED"
1122 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS $C_WNO_DEPRECATED -fexceptions"
1123 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
1124 CVC4_CHECK_FOR_READLINE
1125 CPPFLAGS="$cvc4_rlcheck_save_CPPFLAGS"
1126 CXXFLAGS="$cvc4_rlcheck_save_CXXFLAGS"
1127 CFLAGS="$cvc4_rlcheck_save_CFLAGS"
1128 LDFLAGS="$cvc4_rlcheck_save_LDFLAGS"
1129 AC_DEFINE_UNQUOTED([HAVE_LIBREADLINE], $have_libreadline, [Define to 1 to use libreadline])
1130 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])
1131 AC_SUBST([READLINE_LIBS])
1133 # Whether to build compatibility library
1134 CVC4_BUILD_LIBCOMPAT=yes
1135 AC_ARG_WITH([compat],
1136 AS_HELP_STRING([--with-compat], [build compatibility library (CVC3 API layer)]),
1137 [if test "$withval" = no; then CVC4_BUILD_LIBCOMPAT=no; fi])
1138 AC_MSG_CHECKING([whether to build compatibility library (CVC3 API layer)])
1139 if test "$CVC4_BUILD_LIBCOMPAT" = yes; then
1140 AC_MSG_RESULT([yes])
1142 AC_MSG_RESULT([no, disabled by user])
1144 AC_SUBST(CVC4_BUILD_LIBCOMPAT)
1145 AM_CONDITIONAL([CVC4_BUILD_LIBCOMPAT], [test "$CVC4_BUILD_LIBCOMPAT" = yes])
1147 # Check for availability of TLS support (e.g. __thread storage class)
1148 AC_MSG_CHECKING([whether to use compiler-supported TLS if available])
1149 AC_ARG_ENABLE([tls], AS_HELP_STRING([--disable-tls], [don't use compiler-native TLS]))
1150 if test $cvc4_has_threads = no; then
1151 # We disable TLS entirely by simply telling the build system that
1152 # the empty string is the __thread keyword.
1153 AC_MSG_RESULT([multithreading disabled])
1154 CVC4_TLS_SUPPORTED=1
1156 CVC4_TLS_explanation='disabled (no multithreading support)'
1158 if test -z "${enable_tls+set}" || test "$enable_tls" = "yes"; then
1159 AC_MSG_RESULT([yes])
1160 AX_TLS([CVC4_TLS=$ac_cv_tls], [CVC4_TLS=])
1165 if test -n "$CVC4_TLS"; then
1166 CVC4_TLS_SUPPORTED=1
1167 CVC4_TLS_explanation="$CVC4_TLS"
1169 CVC4_TLS_explanation='pthread_getspecific()'
1170 CVC4_TLS_SUPPORTED=0
1173 AC_SUBST([CVC4_TLS])
1174 AC_SUBST([CVC4_TLS_SUPPORTED])
1176 # Whether to compile with google profiling tools
1177 cvc4_use_google_perftools=0
1181 [--with-google-perftools],
1182 [use Google Performance Tools]
1184 [if test "$withval" != no; then
1185 cvc4_use_google_perftools=1
1189 AC_MSG_CHECKING([whether to link in google perftools libraries])
1190 if test $cvc4_use_google_perftools = 1; then
1191 AC_MSG_RESULT([yes])
1192 AC_CHECK_LIB([tcmalloc], [MallocExtension_GetAllocatedSize], , [AC_MSG_ERROR([cannot link google-perftools test program with -ltcmalloc])], [-lpthread])
1193 AC_CHECK_LIB([profiler], [ProfilerStart], , [AC_MSG_ERROR([cannot link google-perftools test program with -lprofiler])], [-lpthread])
1195 AC_MSG_RESULT([no (user didn't request it)])
1199 AC_ARG_VAR(JAVA, [Java interpreter (used when testing Java interface)])
1200 AC_ARG_VAR(JAVAC, [Java compiler (used when building and testing Java interface)])
1201 AC_ARG_VAR(JAVAH, [Java compiler (used when building and testing Java interface)])
1202 AC_ARG_VAR(JAR, [Jar archiver (used when building Java interface)])
1203 if test "$cvc4_build_java_bindings"; then
1205 if test -z "$JAVA"; then
1206 AC_CHECK_PROGS(JAVA, java, java, [])
1208 AC_CHECK_PROG(JAVA, "$JAVA", "$JAVA", [])
1210 if test -z "$JAVAC"; then
1211 AC_CHECK_PROGS(JAVAC, javac gcj, javac, [])
1212 if test "$JAVAC" = gcj; then JAVAC='gcj -C'; fi
1214 AC_CHECK_PROG(JAVAC, "$JAVAC", "$JAVAC", [])
1216 if test -z "$JAVAH"; then
1217 AC_CHECK_PROGS(JAVAH, javah gcjh, javah, [])
1219 AC_CHECK_PROG(JAVAH, "$JAVAH", "$JAVAH", [])
1221 if test -z "$JAR"; then
1222 AC_CHECK_PROGS(JAR, jar, jar, [])
1224 AC_CHECK_PROG(JAR, "$JAR", "$JAR", [])
1228 # on Mac OS X, Java doesn't like the .so module extension; it wants .dylib
1229 module=no eval CVC4_JAVA_MODULE_EXT="$shrext_cmds"
1230 if test -z "$CVC4_JAVA_MODULE_EXT"; then
1231 CVC4_JAVA_MODULE_EXT=.so
1233 AC_SUBST([CVC4_JAVA_MODULE_EXT])
1235 # Prepare configure output
1237 if test "$enable_shared" = yes; then BUILDING_SHARED=1; else BUILDING_SHARED=0; fi
1238 if test "$enable_static" = yes; then BUILDING_STATIC=1; else BUILDING_STATIC=0; fi
1239 if test "$enable_static_binary" = yes; then STATIC_BINARY=1; else STATIC_BINARY=0; fi
1240 AC_SUBST(BUILDING_SHARED)
1241 AC_SUBST(BUILDING_STATIC)
1242 AC_SUBST(STATIC_BINARY)
1243 AM_CONDITIONAL([STATIC_BINARY], [test "$enable_static_binary" = yes])
1244 AM_CONDITIONAL([COVERAGE_ENABLED], [test "$enable_coverage" = yes])
1246 AM_CONDITIONAL([CVC4_DEBUG], [test "$with_build" = debug])
1247 AM_CONDITIONAL([CVC4_TRACING], [test "$enable_tracing" = yes])
1249 AC_SUBST(CVC4_LIBRARY_VERSION)
1250 AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
1251 AC_SUBST(CVC4_COMPAT_LIBRARY_VERSION)
1252 AC_SUBST(CVC4_BINDINGS_LIBRARY_VERSION)
1254 AC_DEFINE_UNQUOTED(CVC4_MAJOR, ${CVC4_MAJOR}, [Major component of the version of CVC4.])
1255 AC_DEFINE_UNQUOTED(CVC4_MINOR, ${CVC4_MINOR}, [Minor component of the version of CVC4.])
1256 AC_DEFINE_UNQUOTED(CVC4_RELEASE, ${CVC4_RELEASE}, [Release component of the version of CVC4.])
1257 AC_DEFINE_UNQUOTED(CVC4_EXTRAVERSION, ["${CVC4_EXTRAVERSION}"], [Extraversion component of the version of CVC4.])
1258 AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full release string for CVC4.])
1260 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
1261 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
1262 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions"
1263 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
1265 # visibility flag not supported for Windows builds
1266 # also increase default stack size for Windows binaries
1268 (*mingw*) FLAG_VISIBILITY_HIDDEN=
1269 cvc4_LDFLAGS=-Wl,--stack,134217728
1270 pcvc4_LDFLAGS=-Wl,--stack,134217728
1273 AC_SUBST(FLAG_VISIBILITY_HIDDEN)
1274 AC_SUBST(cvc4_LDFLAGS)
1275 AC_SUBST(pcvc4_LDFLAGS)
1277 AM_CONDITIONAL(WHITE_AND_BLACK_TESTS, [test -z "$FLAG_VISIBILITY_HIDDEN"])
1279 # remember the command line used for configure
1280 AC_SUBST(cvc4_config_cmdline)
1284 # When automake scans Makefiles, it complains about non-standard make
1285 # features (including GNU extensions), and breaks GNU Make's
1286 # "if/endif" construct, replacing the "if" with AM_CONDITIONAL if
1287 # constructs. automake even follows "include" and messes with
1288 # included Makefiles.
1290 # CVC4 assumes GNU Make and we want to use GNU Make if/endifs, so we
1291 # have to hide some included Makefiles with GNU extensions. We do
1292 # this by defining mk_include as an autoconf substitution and then
1293 # using "@mk_include@ other_makefile" in Makefile.am to include
1294 # makefiles with GNU extensions; this hides them from automake.
1296 AC_SUBST(mk_include)
1297 # Similar trickery for "if"
1305 # This is used to _always_ comment out rules in automake makefiles, but
1306 # still trigger certain automake behavior; see test/unit/Makefile.am.
1307 AM_CONDITIONAL([CVC4_FALSE], [false])
1309 # set up substitutions for src/util/{rational,integer}.h.in
1310 if test $cvc4_cln_or_gmp = cln; then
1317 AC_SUBST(CVC4_USE_CLN_IMP)
1318 AC_SUBST(CVC4_USE_GMP_IMP)
1320 # month/year for man pages
1321 MAN_DATE=`date '+%B %Y'`
1327 proofs/signatures/Makefile]
1328 m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | grep -v '^contrib/alttheoryskel/' | sort | sed 's,\.am$,,'])
1331 if test $cvc4_has_threads = yes; then
1332 support_multithreaded='with boost threading library'
1333 AM_CONDITIONAL([CVC4_HAS_THREADS], [true])
1334 AC_SUBST([CVC4_HAS_THREADS], 1)
1336 support_multithreaded='no'
1337 AM_CONDITIONAL([CVC4_HAS_THREADS], [false])
1338 AC_SUBST([CVC4_HAS_THREADS], 0)
1341 # Final information to the user
1345 if test "$custom_build_profile" = yes; then
1346 with_build="$with_build (customized)"
1349 support_unit_tests='cxxtest not found; unit tests not supported'
1350 if test -n "$CXXTEST"; then
1351 support_unit_tests='unit testing infrastructure enabled in build directory'
1352 elif test "$enable_unit_testing" = no; then
1353 support_unit_tests='unit testing disabled by user'
1356 if test "$enable_optimized" = yes; then
1357 optimized="yes, at level $OPTLEVEL"
1362 if test $have_libglpk -eq 1; then
1364 gpllibs="${gpllibs} glpk"
1367 if test $have_libreadline -eq 1; then
1369 gpllibs="${gpllibs} readline"
1372 if test $cvc4_cln_or_gmp = cln; then
1373 mplibrary='cln (GPL)'
1375 gpllibs="${gpllibs} cln"
1376 if test $with_portfolio = yes; then
1377 AC_ERROR([Bad configuration detected: cannot build portfolio with CLN.
1378 Please specify only one of --with-portfolio and --with-cln.])
1384 if test "$gpl" = yes; then
1385 if test "$CVC4_BSD_LICENSED_CODE_ONLY" = 1; then
1386 AC_ERROR([Bad configuration detected: BSD-licensed code only, but also requested GPLed libraries:$gpllibs
1387 To permit GPL'ed dependences, use the configure flag --enable-gpl])
1390 licensewarn="${licensewarn}"'****************************************************************************
1391 Please note that CVC4 will be built against the following GPLed libraries:
1393 As these libraries are covered under the GPLv3, so is this build of CVC4.
1394 CVC4 is also available to you under the terms of the (modified) BSD license.
1395 If you prefer to license CVC4 under those terms, please configure with the
1396 option "--bsd", which will disable all optional GPLed library dependences.
1397 ****************************************************************************
1400 license="GPLv3 (due to optional libraries; see below)"
1402 licensewarn="${licensewarn}Please note that this configuration is NOT built against any GPL'ed
1403 libraries, so it is covered by the (modified) BSD license. This is,
1404 however, not the best-performing configuration of CVC4. To build
1405 against GPL'ed libraries which improve CVC4's performance, re-configure
1406 with '--best --enable-gpl'.
1409 license="modified BSD"
1412 if test "$gpl" = yes; then isgpl=1; else isgpl=0; fi
1413 AC_DEFINE_UNQUOTED(CVC4_GPL_DEPS, $isgpl, [Whether CVC4 is built with the (optional) GPLed library dependences.])
1415 CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="$CVC4_COMPAT_LIBRARY_VERSION"
1416 CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="$CVC4_BINDINGS_LIBRARY_VERSION"
1417 if test "$CVC4_BUILD_LIBCOMPAT" = no; then
1418 CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="N/A"
1420 if test -z "$CVC4_LANGUAGE_BINDINGS"; then
1421 CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="N/A"
1424 bindings_to_be_built=none
1425 if test -n "$CVC4_LANGUAGE_BINDINGS"; then
1426 bindings_to_be_built="$CVC4_LANGUAGE_BINDINGS"
1427 if test -z "$SWIG"; then
1428 bindings_to_be_built="$bindings_to_be_built (for CVC3 compatibility layer only; SWIG not found)"
1432 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/base/tls.h])
1433 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
1434 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
1436 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template])
1437 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5])
1438 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3_template])
1439 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc_template])
1440 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc_template])
1441 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3])
1442 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3])
1450 Build profile: $with_build
1451 Build ID : $build_type
1452 Optimized : $optimized
1453 Debug symbols: $enable_debug_symbols
1454 Proofs : $enable_proof
1455 Statistics : $enable_statistics
1456 Replay : $enable_replay
1457 Assertions : $enable_assertions
1458 Tracing : $enable_tracing
1459 Dumping : $enable_dumping
1460 Muzzle : $enable_muzzle
1462 Unit tests : $support_unit_tests
1463 gcov support : $enable_coverage
1464 gprof support: $enable_profiling
1466 Static libs : $enable_static
1467 Shared libs : $enable_shared
1468 Static binary: $enable_static_binary
1469 Compat lib : $CVC4_BUILD_LIBCOMPAT
1470 Bindings : $bindings_to_be_built
1472 Multithreaded: $support_multithreaded
1473 TLS support : $CVC4_TLS_explanation
1474 Portfolio : $with_portfolio
1476 MP library : $mplibrary
1479 Readline : $with_readline
1481 CPPFLAGS : $CPPFLAGS
1482 CXXFLAGS : $CXXFLAGS
1487 libcvc4 version : $CVC4_LIBRARY_VERSION
1488 libcvc4parser version : $CVC4_PARSER_LIBRARY_VERSION
1489 libcvc4compat version : $CVC4_COMPAT_LIBRARY_VERSION_or_nobuild
1490 libcvc4bindings version: $CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild
1492 Install into : $prefix
1494 CVC4 license : $license
1496 ${licensewarn}Now just type make, followed by make check or make install, as you like.
1500 if test -n "$CVC4_UNSUPPORTED_LANGUAGE_BINDINGS"; then
1502 AC_MSG_WARN([You are electing to build unsupported language binding(s):])
1503 AC_MSG_WARN([ $CVC4_UNSUPPORTED_LANGUAGE_BINDINGS])
1504 AC_MSG_WARN([Please be aware that these bindings may not compile, or])
1505 AC_MSG_WARN([work, and the interface to CVC4 via these bindings may])
1506 AC_MSG_WARN([change drastically in upcoming releases of CVC4.])
1510 if test -n "$CVC4_INTEGRITY_WARNING"; then
1512 AC_MSG_WARN($CVC4_INTEGRITY_WARNING)
1513 AC_MSG_WARN([Please run "make check" after building to ensure integrity of the binary and library])