configure.ac

   1 #                                               -*- Autoconf -*-
   2 # Process this file with autoconf to produce a configure script.
   3
   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
   9
  10 dnl Preprocess CL args. Defined in config/cvc4.m4
  11 CVC4_AC_INIT
  12
  13 AC_PREREQ([2.61])
  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])
  20
  21 m4_ifdef([AM_SILENT_RULES],[AM_SILENT_RULES([yes])])
  22
  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
  28
  29 # Libtool version numbers for libraries
  30 # Version numbers are in the form current:revision:age
  31 #
  32 # current -
  33 #   increment if interfaces have been added, removed or changed
  34 # revision -
  35 #   increment if source code has changed
  36 #   set to zero if current is incremented
  37 # age -
  38 #   increment if interfaces have been added
  39 #   set to zero if interfaces have been removed
  40 #   or changed
  41 #
  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
  45 # developer's guide.
  46
  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])])
  48
  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
  53
  54 m4_define([fatal_error], [m4_errprint(__program__:__file__:__line__[: fatal error: $*
  55 ])m4_exit(1)])dnl
  56
  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
  61
  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
  66
  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
  71 # some things.)
  72 config_cmdline=("$@")
  73 cvc4_config_cmdline="${config_cmdline[[@]]}"
  74
  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}
  78
  79 if test -e src/include/cvc4_public.h; then
  80   CVC4_CONFIGURE_AT_TOP_LEVEL=yes
  81 else
  82   CVC4_CONFIGURE_AT_TOP_LEVEL=no
  83 fi
  84
  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
  89
  90 # on by default
  91 AM_MAINTAINER_MODE([enable])
  92
  93 # turn off static lib building by default
  94 AC_ENABLE_SHARED
  95 AC_DISABLE_STATIC
  96
  97 AC_CANONICAL_BUILD
  98 AC_CANONICAL_HOST
  99 AC_CANONICAL_TARGET
 100
 101 as_me=configure
 102
 103 if test "$enable_shared" = no -a "$user_specified_enable_or_disable_shared" = yes; then
 104   enable_static=yes
 105 fi
 106
 107 # Features requested by the user
 108 AC_MSG_CHECKING([for requested build profile])
 109 AC_ARG_WITH([build],
 110   [AS_HELP_STRING([--with-build=profile],
 111      [for profile in {production,debug,competition,personal}])])
 112
 113 if test -z "${with_build+set}"; then
 114   with_build=production
 115 fi
 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}"; then
 117   custom_build_profile=no
 118 else
 119   custom_build_profile=yes
 120 fi
 121 btargs=
 122 if test -n "${enable_optimized+set}"; then
 123   if test "$enable_optimized" = yes; then
 124     btargs="$btargs optimized"
 125   else
 126     btargs="$btargs nooptimized"
 127   fi
 128 fi
 129 # --enable-staticbinary is an alias for --enable-static-binary
 130 if test -n "${enable_staticbinary+set}"; then
 131   enable_static_binary="$enable_staticbinary"
 132 fi
 133 if test -n "${enable_static_binary+set}"; then
 134   if test "$enable_static_binary" = yes; then
 135     btargs="$btargs staticbinary"
 136   else
 137     btargs="$btargs nostaticbinary"
 138   fi
 139 fi
 140 if test -n "${enable_debug_symbols+set}"; then
 141   if test "$enable_debug_symbols" = yes; then
 142     btargs="$btargs debugsymbols"
 143   else
 144     btargs="$btargs nodebugsymbols"
 145   fi
 146 fi
 147 if test -n "${enable_assertions+set}"; then
 148   if test "$enable_assertions" = yes; then
 149     btargs="$btargs assertions"
 150   else
 151     btargs="$btargs noassertions"
 152   fi
 153 fi
 154 if test -n "${enable_proof+set}"; then
 155   if test "$enable_proof" = yes; then
 156     btargs="$btargs proof"
 157   else
 158     btargs="$btargs noproof"
 159   fi
 160 fi
 161 if test -n "${enable_tracing+set}"; then
 162   if test "$enable_tracing" = yes; then
 163     btargs="$btargs tracing"
 164   else
 165     btargs="$btargs notracing"
 166   fi
 167 fi
 168 if test -n "${enable_dumping+set}"; then
 169   if test "$enable_dumping" = yes; then
 170     btargs="$btargs dumping"
 171   else
 172     btargs="$btargs nodumping"
 173   fi
 174 fi
 175 if test -n "${enable_muzzle+set}"; then
 176   if test "$enable_muzzle" = yes; then
 177     btargs="$btargs muzzle"
 178   else
 179     btargs="$btargs nomuzzle"
 180   fi
 181 fi
 182 if test -n "${enable_coverage+set}"; then
 183   if test "$enable_coverage" = yes; then
 184     btargs="$btargs coverage"
 185   else
 186     btargs="$btargs nocoverage"
 187   fi
 188 fi
 189 if test -n "${enable_profiling+set}"; then
 190   if test "$enable_profiling" = yes; then
 191     btargs="$btargs profiling"
 192   else
 193     btargs="$btargs noprofiling"
 194   fi
 195 fi
 196 if test -n "${enable_statistics+set}"; then
 197   if test "$enable_statistics" = yes; then
 198     btargs="$btargs statistics"
 199   else
 200     btargs="$btargs nostatistics"
 201   fi
 202 fi
 203 if test -n "${enable_replay+set}"; then
 204   if test "$enable_replay" = yes; then
 205     btargs="$btargs replay"
 206   else
 207     btargs="$btargs noreplay"
 208   fi
 209 fi
 210 if test -n "${with_glpk+set}"; then
 211   if test "$with_glpk" = yes; then
 212     btargs="$btargs glpk"
 213   fi
 214 fi
 215 if test -n "${with_abc+set}"; then
 216   if test "$with_abc" = yes; then
 217     btargs="$btargs abc"
 218   fi
 219 fi
 220 AC_MSG_RESULT([$with_build])
 221
 222 AM_INIT_AUTOMAKE([1.11 no-define tar-pax parallel-tests color-tests subdir-objects])
 223 AC_CONFIG_HEADERS([cvc4autoconfig.h])
 224
 225 # automake 1.12 changes the test driver mechanism in a way that is
 226 # completely incompatible with 1.11.  We figure out here which version
 227 # we're using in order to set up test makefiles correctly.
 228 # See http://lists.gnu.org/archive/html/automake/2012-04/msg00060.html
 229 if test -z "$am__api_version"; then
 230   AC_MSG_ERROR([Cannot determine automake API version ?!])
 231 fi
 232 case "$am__api_version" in
 233   1.11*) automake111=true ;;
 234   *) automake111=false ;;
 235 esac
 236 AM_CONDITIONAL([AUTOMAKE_1_11], [$automake111])
 237
 238 # Initialize libtool's configuration options.
 239 # we're not DLL-clean yet (i.e., don't properly use dllexport and dllimport)
 240 # _LT_SET_OPTION([LT_INIT],[win32-dll])
 241 LT_INIT
 242
 243 # Checks for programs.
 244 AC_PROG_CC
 245 AC_PROG_CXX
 246 AC_PROG_INSTALL
 247
 248 CVC4_GCC_VERSION
 249
 250 cvc4_use_gmp=2
 251 cvc4_use_cln=2
 252
 253 AC_ARG_WITH(
 254   [cln],
 255   AS_HELP_STRING(
 256     [--with-cln],
 257     [use CLN instead of GMP]
 258   ),
 259   [case "$withval" in
 260    y|ye|yes|Y|YE|YES) cvc4_use_cln=1 ;;
 261    n|no|N|NO) cvc4_use_cln=0 ;;
 262    esac
 263   ]
 264 )
 265
 266 AC_ARG_WITH(
 267   [gmp],
 268   AS_HELP_STRING(
 269     [--with-gmp],
 270     [use GMP instead of CLN]
 271   ),
 272   [case "$withval" in
 273    y|ye|yes|Y|YE|YES) cvc4_use_gmp=1 ;;
 274    n|no|N|NO) cvc4_use_gmp=0 ;;
 275    esac
 276   ]
 277 )
 278
 279 if test $cvc4_use_cln = 1 -a $cvc4_use_gmp = 1 || test $cvc4_use_cln = 0 -a $cvc4_use_gmp = 0; then
 280   AC_MSG_ERROR([You must use either CLN and GMP.  Please pick one.])
 281 fi
 282 if test $cvc4_use_gmp = 1; then
 283   cvc4_use_cln=0
 284 elif test $cvc4_use_gmp = 0; then
 285   cvc4_use_cln=1
 286 elif test $cvc4_use_cln = 1; then
 287   cvc4_use_gmp=0
 288 elif test $cvc4_use_cln = 0; then
 289   cvc4_use_gmp=1
 290 fi
 291
 292 # try GMP, fail if not found; GMP is required for both CLN and for GMP
 293 # versions of CVC4
 294 AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP (libgmp) not found, see http://gmplib.org/])])
 295
 296 if test $cvc4_use_cln = 2; then
 297   if test "$CVC4_BSD_LICENSED_CODE_ONLY" = 1 -o "$with_portfolio" = yes; then
 298     cvc4_use_cln=0
 299     cvc4_use_gmp=1
 300   fi
 301 fi
 302
 303 if test $cvc4_use_cln != 0; then
 304   # [mdeters] The PKG_CHECK_MODULES macro isn't customizable and doesn't fail
 305   # gracefully.  You can only specify it once for a given library name.  That
 306   # is, even on separate if/else branches, you can't put
 307   # PKG_CHECK_MODULES([CLN], ...).  That's why things are so convoluted here,
 308   # we have to have PKG_CHECK_MODULES _exactly_ once in configure.ac !
 309   PKG_CHECK_MODULES([CLN], [cln >= 1.2.2],
 310     [AC_LANG_PUSH([C++])
 311      save_LIBS="$LIBS"
 312      save_CXXFLAGS="$CXXFLAGS"
 313      LIBS="$CLN_LIBS $LIBS"
 314      CXXFLAGS="$CLN_CFLAGS $CXXFLAGS"
 315      AC_LINK_IFELSE([AC_LANG_PROGRAM([[#include <cln/cln.h>]], [[cln::cl_F pi = "3.1415926";]])], [
 316        cvc4_use_cln=1
 317      ], [
 318        if test $cvc4_use_cln = 1; then
 319          # fail
 320          AC_MSG_ERROR([CLN installation missing, too old, or not functional for this architecture])
 321        else
 322          # fall back to GMP
 323          AC_MSG_NOTICE([CLN installation missing, too old, or not functional for this architecture, will use gmp instead])
 324          cvc4_use_cln=0
 325          cvc4_use_gmp=1
 326        fi
 327      ])
 328      CXXFLAGS="$save_CXXFLAGS"
 329      LIBS="$save_LIBS"
 330      AC_LANG_POP([C++])
 331     ],
 332     [if test $cvc4_use_cln = 1; then
 333        # fail
 334        AC_MSG_ERROR([CLN not installed (or too old) or pkgconfig missing])
 335      else
 336        # fall back to GMP
 337        AC_MSG_NOTICE([CLN not installed (or too old) or pkgconfig missing, will use gmp])
 338        cvc4_use_cln=0
 339        cvc4_use_gmp=1
 340      fi
 341     ]
 342   )
 343 fi
 344 if test $cvc4_use_cln = 0; then
 345   # try GMPXX, fail if not found; don't need to link against it, only need its header
 346   AC_LANG_PUSH([C++])
 347   AC_CHECK_HEADER([gmpxx.h], , [AC_MSG_ERROR([GNU MP C++ library header (gmpxx.h) required but not found, see http://gmplib.org/])])
 348   AC_LANG_POP([C++])
 349   cvc4_cln_or_gmp=gmp
 350 else
 351   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }$CLN_CFLAGS"
 352   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }$CLN_CFLAGS"
 353   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }$CLN_CFLAGS"
 354   LIBS="$CLN_LIBS${LIBS:+ $LIBS}"
 355   cvc4_cln_or_gmp=cln
 356 fi
 357
 358 if test $cvc4_cln_or_gmp = cln; then
 359   AC_DEFINE_UNQUOTED(CVC4_CLN_IMP, [], [Defined if using the CLN multi-precision arithmetic library.])
 360 else
 361   AC_DEFINE_UNQUOTED(CVC4_GMP_IMP, [], [Defined if using the GMP multi-precision arithmetic library.])
 362 fi
 363 AM_CONDITIONAL([CVC4_CLN_IMP], [test $cvc4_cln_or_gmp = cln])
 364 AM_CONDITIONAL([CVC4_GMP_IMP], [test $cvc4_cln_or_gmp = gmp])
 365
 366 # construct the build string
 367 AC_MSG_CHECKING([for appropriate build string])
 368 if test -z "$ac_confdir"; then
 369   ac_confdir="$srcdir"
 370 fi
 371 build_type=`$ac_confdir/config/build-type $with_build $btargs $cvc4_cln_or_gmp`
 372 AC_MSG_RESULT($build_type)
 373
 374 # Require building in target and build-specific build directory:
 375 #
 376 # If the configure script is invoked from the top-level source
 377 # directory, it creates a suitable build directory (based on the build
 378 # architecture and build profile from $build_type), changes into it,
 379 # and reinvokes itself.  CVC4_CONFIGURE_IN_BUILDS is an envariable
 380 # that breaks any possibility of infinite recursion in this process.
 381 AC_MSG_CHECKING([what dir to configure])
 382 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
 383   AC_MSG_RESULT([this one (in builds/)])
 384 elif test "$CVC4_CONFIGURE_AT_TOP_LEVEL" = yes; then
 385   AC_MSG_RESULT([builds/$target/$build_type])
 386   $as_echo
 387   if test -z "$ac_srcdir"; then
 388     mkbuilddir=./config/mkbuilddir
 389   else
 390     mkbuilddir=$ac_srcdir/config/mkbuilddir
 391   fi
 392   $as_echo "$mkbuilddir $target $build_type"
 393   source $mkbuilddir "$target" "$build_type"
 394   $as_echo "cd builds/$target/$build_type"
 395   cd "builds/$target/$build_type"
 396   CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS
 397   # Runs the single recursive configure invocation using a relative path.
 398   # See https://lists.gnu.org/archive/html/autoconf/2011-04/msg00060.html
 399   echo "$SHELL ../../../configure ${config_cmdline[[@]]}"
 400   "$SHELL" "../../../configure" "${config_cmdline[[@]]}"
 401   exitval=$?
 402   cd ../../..
 403   if test $exitval -eq 0; then
 404     cat >config.reconfig <<EOF
 405 [#!/bin/bash
 406 # Generated by configure, `date`
 407 # This script is part of CVC4.
 408
 409 cd "\`dirname \\"\$0\\"\`"
 410
 411 if test -d builds; then :; else echo 'No builds/ directory!' >&2; exit; fi
 412
 413 current=(\`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]*\\)/\\(.*\\),\\1 \\2,'\`)
 414 arch=\${current[0]}
 415 build=\${current[1]}
 416
 417 echo "reconfiguring in builds/\$arch/\$build..."
 418 cd "builds/\$arch/\$build"
 419 echo ./config.status "\$@"
 420 ./config.status "\$@"]
 421 EOF
 422     chmod +x config.reconfig
 423   fi
 424   ln -sf "$target/$build_type/config.log" "builds/config.log"
 425   exit $exitval
 426 else
 427   AC_MSG_RESULT([this one (user-specified)])
 428 fi
 429
 430 as_me=configure
 431
 432 # Unpack standard build types. Any particular options can be overriden with
 433 # --enable/disable-X options
 434 # Tim: This needs to keep CVC4CPPFLAGS, CVC4CXXFLAGS, etc. set by earlier checks
 435 case "$with_build" in
 436   production) # highly optimized, no assertions, no tracing, dumping
 437     CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }"
 438     CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }"
 439     CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }"
 440     CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
 441     FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
 442     if test -z "${OPTLEVEL+set}"            ; then OPTLEVEL=3                       ; fi
 443     if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; fi
 444     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes         ; fi
 445     if test -z "${enable_statistics+set}"   ; then enable_statistics=yes            ; fi
 446     if test -z "${enable_replay+set}"       ; then enable_replay=no                 ; fi
 447     if test -z "${enable_assertions+set}"   ; then enable_assertions=no             ; fi
 448     if test -z "${enable_proof+set}"        ; then enable_proof=yes                 ; fi
 449     if test -z "${enable_tracing+set}"      ; then enable_tracing=no                ; fi
 450     if test -z "${enable_dumping+set}"      ; then enable_dumping=yes               ; fi
 451     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
 452     ;;
 453   debug) # unoptimized, debug symbols, assertions, tracing, dumping
 454     CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DEBUG"
 455     CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-fno-inline"
 456     CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-fno-inline"
 457     CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
 458     FLAG_VISIBILITY_HIDDEN=
 459     if test -z "${enable_optimized+set}"    ; then enable_optimized=no              ; fi
 460     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes         ; fi
 461     if test -z "${enable_statistics+set}"   ; then enable_statistics=yes            ; fi
 462     if test -z "${enable_replay+set}"       ; then enable_replay=yes                ; fi
 463     if test -z "${enable_assertions+set}"   ; then enable_assertions=yes            ; fi
 464     if test -z "${enable_proof+set}"        ; then enable_proof=yes                 ; fi
 465     if test -z "${enable_tracing+set}"      ; then enable_tracing=yes               ; fi
 466     if test -z "${enable_dumping+set}"      ; then enable_dumping=yes               ; fi
 467     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
 468     ;;
 469   default) # moderately optimized, assertions, tracing, dumping
 470     CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }"
 471     CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }"
 472     CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }"
 473     CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
 474     FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
 475     if test -z "${OPTLEVEL+set}"            ; then OPTLEVEL=2                       ; fi
 476     if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; fi
 477     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes         ; fi
 478     if test -z "${enable_statistics+set}"   ; then enable_statistics=yes            ; fi
 479     if test -z "${enable_replay+set}"       ; then enable_replay=yes                ; fi
 480     if test -z "${enable_assertions+set}"   ; then enable_assertions=yes            ; fi
 481     if test -z "${enable_proof+set}"        ; then enable_proof=yes                 ; fi
 482     if test -z "${enable_tracing+set}"      ; then enable_tracing=yes               ; fi
 483     if test -z "${enable_dumping+set}"      ; then enable_dumping=yes               ; fi
 484     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
 485     ;;
 486   competition) # maximally optimized, no assertions, no tracing, no dumping, muzzled
 487     CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COMPETITION_MODE"
 488     CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs"
 489     CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs"
 490     CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }"
 491     FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
 492     if test -z "${OPTLEVEL+set}"            ; then OPTLEVEL=9                       ; fi
 493     if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; fi
 494     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no          ; fi
 495     if test -z "${enable_statistics+set}"   ; then enable_statistics=no             ; fi
 496     if test -z "${enable_replay+set}"       ; then enable_replay=no                 ; fi
 497     if test -z "${enable_assertions+set}"   ; then enable_assertions=no             ; fi
 498     if test -z "${enable_proof+set}"        ; then enable_proof=no                  ; fi
 499     if test -z "${enable_tracing+set}"      ; then enable_tracing=no                ; fi
 500     if test -z "${enable_dumping+set}"      ; then enable_dumping=no                ; fi
 501     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=yes                ; fi
 502     if test -z "${user_specified_enable_or_disable_shared}"; then enable_shared=no; fi
 503     if test -z "${user_specified_enable_or_disable_static}"; then enable_static=yes; fi
 504     if test -z "${enable_static_binary+set}"; then enable_static_binary=yes         ; fi
 505     ;;
 506   *)
 507     AC_MSG_FAILURE([unknown build profile: $with_build])
 508     ;;
 509 esac
 510 if test -z "${OPTLEVEL+set}"; then OPTLEVEL=3; fi
 511
 512 AM_CONDITIONAL([CVC4_BUILD_PROFILE_PRODUCTION],  [test "$with_build" = production])
 513 AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEBUG],       [test "$with_build" = debug])
 514 AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEFAULT],     [test "$with_build" = default])
 515 AM_CONDITIONAL([CVC4_BUILD_PROFILE_COMPETITION], [test "$with_build" = competition])
 516
 517 # permit a static binary
 518 AC_MSG_CHECKING([whether to build a static binary])
 519 AC_ARG_ENABLE([static-binary],
 520      [AS_HELP_STRING([--enable-static-binary],
 521                      [build a fully statically-linked binary [default=no]])])
 522 if test -z "${enable_static_binary+set}"; then
 523   enable_static_binary=no
 524 fi
 525 AC_MSG_RESULT([$enable_static_binary])
 526 if test "$enable_static_binary" = yes; then
 527   if test "$target_vendor" = apple; then
 528     if test -z "$MAC_STATIC_BINARY_MANUAL_OVERRIDE"; then
 529       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)]])
 530     else
 531       AC_MSG_WARN([MAC_STATIC_BINARY_MANUAL_OVERRIDE was set!])
 532       AC_MSG_WARN([Will make a static binary during this build.  Note that it may fail!])
 533     fi
 534   fi
 535   if test "$enable_static" != yes; then
 536     enable_static=yes
 537     AC_MSG_WARN([forcing static-library building, --enable-static-binary given])
 538   fi
 539 fi
 540
 541 AC_MSG_CHECKING([whether to support proofs in libcvc4])
 542
 543 AC_ARG_ENABLE([proof],
 544   [AS_HELP_STRING([--disable-proof],
 545      [do not support proof generation])])
 546 if test -z "${enable_proof+set}"; then
 547   enable_proof=yes
 548 fi
 549 AC_MSG_RESULT([$enable_proof])
 550
 551 if test "$enable_proof" = yes; then
 552   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROOF"
 553 fi
 554 AM_CONDITIONAL([CVC4_PROOF], [test "$enable_proof" = yes])
 555
 556 AC_MSG_CHECKING([whether to optimize libcvc4])
 557
 558 AC_ARG_ENABLE([optimized],
 559   [AS_HELP_STRING([--enable-optimized],
 560      [optimize the build])])
 561
 562 if test -z "${enable_optimized+set}"; then
 563   enable_optimized=no
 564 fi
 565
 566 AC_MSG_RESULT([$enable_optimized])
 567
 568 if test "$enable_optimized" = yes; then
 569   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O$OPTLEVEL"
 570   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O$OPTLEVEL"
 571 else
 572   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O0"
 573   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O0"
 574 fi
 575
 576 AC_MSG_CHECKING([whether to include debugging symbols in libcvc4])
 577
 578 AC_ARG_ENABLE([debug-symbols],
 579   [AS_HELP_STRING([--disable-debug-symbols],
 580      [do not include debug symbols in libcvc4])])
 581
 582 if test -z "${enable_debug_symbols+set}"; then
 583   enable_debug_symbols=yes
 584 fi
 585
 586 AC_MSG_RESULT([$enable_debug_symbols])
 587
 588 if test "$enable_debug_symbols" = yes; then
 589   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-ggdb3"
 590   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-ggdb3"
 591 fi
 592
 593 AC_MSG_CHECKING([whether to include statistics are turned on in libcvc4])
 594
 595 AC_ARG_ENABLE([statistics],
 596   [AS_HELP_STRING([--disable-statistics],
 597      [do not include statistics in libcvc4])])
 598
 599 if test -z "${enable_statistics+set}"; then
 600   enable_statistics=yes
 601 fi
 602
 603 AC_MSG_RESULT([$enable_statistics])
 604
 605 if test "$enable_statistics" = yes; then
 606   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_STATISTICS_ON"
 607 fi
 608
 609 AC_MSG_CHECKING([whether the replay feature should be turned on in libcvc4])
 610
 611 AC_ARG_ENABLE([replay],
 612   [AS_HELP_STRING([--disable-replay],
 613      [turn off the replay feature in libcvc4])])
 614
 615 if test -z "${enable_replay+set}"; then
 616   enable_replay=yes
 617 fi
 618
 619 AC_MSG_RESULT([$enable_replay])
 620
 621 if test "$enable_replay" = yes; then
 622   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_REPLAY"
 623 fi
 624
 625 AC_MSG_CHECKING([whether to include assertions in build])
 626
 627 AC_ARG_ENABLE([assertions],
 628   [AS_HELP_STRING([--disable-assertions],
 629      [turn off assertions in build])])
 630
 631 if test -z "${enable_assertions+set}"; then
 632   enable_assertions=yes
 633 fi
 634
 635 AC_MSG_RESULT([$enable_assertions])
 636
 637 if test "$enable_assertions" = yes; then
 638   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_ASSERTIONS"
 639 else
 640   # turn off regular C assert() also
 641   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DNDEBUG"
 642 fi
 643
 644 AC_MSG_CHECKING([whether to do a traceable build of CVC4])
 645 AC_ARG_ENABLE([tracing],
 646   [AS_HELP_STRING([--disable-tracing],
 647      [remove all tracing code from CVC4])])
 648
 649 if test -z "${enable_tracing+set}"; then
 650   enable_tracing=yes
 651 fi
 652
 653 AC_MSG_RESULT([$enable_tracing])
 654
 655 if test "$enable_tracing" = yes; then
 656   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_TRACING"
 657 fi
 658
 659 AC_MSG_CHECKING([whether to do a dump-capable build of CVC4])
 660 AC_ARG_ENABLE([dumping],
 661   [AS_HELP_STRING([--disable-dumping],
 662      [remove all dumping code from CVC4])])
 663
 664 if test -z "${enable_dumping+set}"; then
 665   enable_dumping=yes
 666 fi
 667
 668 AC_MSG_RESULT([$enable_dumping])
 669
 670 if test "$enable_dumping" = yes; then
 671   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DUMPING"
 672 fi
 673
 674 AC_MSG_CHECKING([whether to do a muzzled build of CVC4])
 675 AC_ARG_ENABLE([muzzle],
 676   [AS_HELP_STRING([--enable-muzzle],
 677      [completely silence CVC4; remove ALL non-result output from build])])
 678
 679 if test -z "${enable_muzzle+set}"; then
 680   enable_muzzle=no
 681 fi
 682
 683 AC_MSG_RESULT([$enable_muzzle])
 684
 685 if test "$enable_muzzle" = yes; then
 686   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_MUZZLE"
 687 fi
 688
 689 AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4])
 690 AC_ARG_ENABLE([coverage],
 691   [AS_HELP_STRING([--enable-coverage],
 692      [build with support for gcov coverage testing])])
 693
 694 if test -z "${enable_coverage+set}"; then
 695   enable_coverage=no
 696 fi
 697
 698 AC_MSG_RESULT([$enable_coverage])
 699
 700 if test "$enable_coverage" = yes; then
 701   # For coverage testing, we prefer:
 702   #     --enable-static --disable-shared --disable-static-binary
 703   # If the user didn't specify these, we force them here.  If the
 704   # user specified them in opposite phase, give warnings that they
 705   # shouldn't do that, or bomb out.
 706   if test "$user_specified_enable_or_disable_shared" != yes; then
 707     enable_shared=no
 708     AC_MSG_WARN([turning off shared library building due to --enable-coverage])
 709   elif test "$enable_shared" = yes; then
 710     AC_MSG_WARN([])
 711     AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-shared])
 712     AC_MSG_WARN([gcov does not support shared libraries, so only your static libraries will be coverage-testable.])
 713     AC_MSG_WARN([Your cvc4 driver and testing binaries will not be coverage-testable.])
 714     AC_MSG_WARN([])
 715   fi
 716   if test "${enable_static_binary+set}" = set -a "$enable_static_binary" = yes; then
 717     AC_MSG_WARN([])
 718     AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-static-binary])
 719     AC_MSG_WARN([Your cvc4 driver and testing binaries will be fully-statically linked and may not be coverage-testable.])
 720     AC_MSG_WARN([])
 721   fi
 722   if test "$user_specified_enable_or_disable_static" != yes; then
 723     enable_static=yes
 724     AC_MSG_WARN([turning on static library building due to --enable-coverage])
 725   elif test "$enable_static" != yes; then
 726     AC_MSG_ERROR([--enable-coverage and --disable-static are incompatible; gcov only supports static libraries.])
 727   fi
 728
 729   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COVERAGE"
 730   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }--coverage"
 731   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }--coverage"
 732   CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }--coverage"
 733 fi
 734
 735 AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4])
 736
 737 AC_ARG_ENABLE([profiling],
 738   [AS_HELP_STRING([--enable-profiling],
 739      [build with support for gprof profiling])])
 740
 741 if test -z "${enable_profiling+set}"; then
 742   enable_profiling=no
 743 fi
 744
 745 AC_MSG_RESULT([$enable_profiling])
 746
 747 if test "$enable_profiling" = yes; then
 748   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROFILING"
 749   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-pg"
 750   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-pg"
 751   CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }-pg"
 752 fi
 753
 754 # Check for libglpk (defined in config/glpk.m4)
 755 AC_ARG_WITH([glpk],
 756   [AS_HELP_STRING([--with-glpk],
 757      [use GLPK simplex solver])], [], [with_glpk=])
 758 CVC4_CHECK_FOR_GLPK
 759 if test $have_libglpk -eq 1; then
 760   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_GLPK"
 761 fi
 762 AM_CONDITIONAL([CVC4_USE_GLPK], [test $have_libglpk -eq 1])
 763 AC_SUBST([GLPK_LDFLAGS])
 764 AC_SUBST([GLPK_LIBS])
 765
 766 # Build with libabc (defined in config/abc.m4)
 767 AC_ARG_WITH([abc],
 768   [AS_HELP_STRING([--with-abc],
 769      [use the ABC AIG library])], [], [with_abc=])
 770 CVC4_CHECK_FOR_ABC
 771 if test $have_libabc -eq 1; then
 772   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_ABC"
 773 fi
 774 AM_CONDITIONAL([CVC4_USE_ABC], [test $have_libabc -eq 1])
 775 AC_SUBST([ABC_LDFLAGS])
 776 AC_SUBST([ABC_LIBS])
 777
 778 # Check to see if this version/architecture of GNU C++ explicitly
 779 # instantiates __gnu_cxx::hash<uint64_t> or not.  Some do, some don't.
 780 # See src/util/hash.h.
 781 AC_MSG_CHECKING([whether __gnu_cxx::hash<uint64_t> is already specialized])
 782 AC_LANG_PUSH([C++])
 783 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
 784 #include <stdint.h>
 785 #include <ext/hash_map>
 786 namespace __gnu_cxx { template<> struct hash<uint64_t> {}; }])],
 787                   [AC_MSG_RESULT([no]); CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_NEED_HASH_UINT64_T"],
 788                   [AC_MSG_RESULT([yes])])
 789 AC_LANG_POP([C++])
 790
 791 # Check whether "long" and "int64_t" are distinct types w.r.t. overloading.
 792 # Even if they have the same size, they can be distinct, and some platforms
 793 # can have problems with ambiguous function calls when auto-converting
 794 # int64_t to long, and others will complain if you overload a function
 795 # that takes an int64_t with one that takes a long (giving a redefinition
 796 # error).  So we have to keep both happy.  Probably the same underlying
 797 # issue as the hash specialization above, but let's check separately
 798 # for flexibility.
 799 AC_MSG_CHECKING([for the relationship between long and int64_t])
 800 AC_LANG_PUSH([C++])
 801 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
 802 #include <stdint.h>
 803 void foo(long) {}
 804 void foo(int64_t) {}])],
 805                   [AC_MSG_RESULT([no relationship detected]); CVC4_NEED_INT64_T_OVERLOADS=1],
 806                   [AC_MSG_RESULT([typedef or similar]); CVC4_NEED_INT64_T_OVERLOADS=0])
 807 AC_LANG_POP([C++])
 808 AC_SUBST([CVC4_NEED_INT64_T_OVERLOADS])
 809
 810 # Check for ANTLR runantlr script (defined in config/antlr.m4)
 811 AC_PROG_ANTLR
 812
 813 CVC4_CXX_OPTION([-Werror], [WERROR])
 814 CVC4_C_OPTION([-Werror], [C_WERROR])
 815 CVC4_CXX_OPTION([-Wno-deprecated], [WNO_DEPRECATED])
 816 CVC4_C_OPTION([-Wno-deprecated], [C_WNO_DEPRECATED])
 817 CVC4_CXX_OPTION([-Wno-conversion-null], [WNO_CONVERSION_NULL])
 818 CVC4_CXX_OPTION([-Wno-tautological-compare], [WNO_TAUTOLOGICAL_COMPARE])
 819 CVC4_CXX_OPTION([-Wno-parentheses], [WNO_PARENTHESES])
 820 CVC4_CXX_OPTION([-Wno-uninitialized], [WNO_UNINITIALIZED])
 821 CVC4_CXX_OPTION([-Wno-unused-variable], [WNO_UNUSED_VARIABLE])
 822 CVC4_CXX_OPTION([-fno-strict-aliasing], [FNO_STRICT_ALIASING])
 823 AC_SUBST([WERROR])
 824 AC_SUBST([WNO_CONVERSION_NULL])
 825 AC_SUBST([WNO_TAUTOLOGICAL_COMPARE])
 826 AC_SUBST([WNO_PARENTHESES])
 827 AC_SUBST([WNO_UNINITIALIZED])
 828 AC_SUBST([WNO_UNUSED_VARIABLE])
 829 AC_SUBST([FNO_STRICT_ALIASING])
 830
 831 # On Mac, we have to fix the visibility of standard library symbols.
 832 # Otherwise, exported template instantiations---even though explicitly
 833 # CVC4_PUBLIC, can be generated as symbols with internal-only linkage.
 834 # Presumably, Apple is distributing a libstdc++ that is built *without*
 835 # --enable-libstdcxx-visibility (?)
 836 if test "$target_vendor" = apple; then
 837   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-D_GLIBCXX_VISIBILITY_DEFAULT=\"__attribute__((__visibility__(\\\"default\\\")))\""
 838 fi
 839
 840 # Tell top-level Makefile to include $(top_srcdir)/personal.mk
 841 AC_ARG_ENABLE([personal-make-rules],
 842   [AS_HELP_STRING([--enable-personal-make-rules],
 843      [include top-level personal.mk (if it exists)])])
 844 if test "$enable_personal_make_rules" = yes; then
 845   # This allows us to include a personal.mk makefile from every
 846   # generated makefile.  Named zz_* in order to make sure this
 847   # comes last, so it gets other definitions (in particular top_srcdir).
 848   zz_cvc4_use_personal_make_rules='yes
 849
 850 all:;
 851 include $(top_srcdir)/personal.mk
 852 $(top_srcdir)/personal.mk:; @touch "$@"'
 853   AC_SUBST([zz_cvc4_use_personal_make_rules])
 854 fi
 855
 856 # Doxygen configuration
 857 AC_ARG_ENABLE([internals-documentation],
 858   [AS_HELP_STRING([--enable-internals-documentation],
 859      [build Doxygen documentation for static and private member functions])])
 860 if test "$enable_internals_documentation" = yes; then
 861   DOXYGEN_EXTRACT_PRIVATE=YES
 862   DOXYGEN_EXTRACT_STATIC=YES
 863 else
 864   DOXYGEN_EXTRACT_PRIVATE=NO
 865   DOXYGEN_EXTRACT_STATIC=NO
 866 fi
 867 AC_SUBST([DOXYGEN_EXTRACT_PRIVATE])
 868 AC_SUBST([DOXYGEN_EXTRACT_STATIC])
 869
 870 DX_MAN_FEATURE(OFF)
 871 DX_PDF_FEATURE(OFF)
 872 DX_PS_FEATURE(OFF)
 873 DX_DOT_FEATURE(OFF)
 874 DX_INIT_DOXYGEN($PACKAGE_NAME, config/doxygen.cfg, $srcdir/doc/doxygen)
 875
 876 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])
 877 AC_ARG_VAR(CXXTEST, [path to CxxTest installation])
 878
 879 AC_SUBST([CXXTEST])
 880
 881 AC_ARG_WITH([cxxtest-dir],
 882   [AS_HELP_STRING([--with-cxxtest-dir=DIR], [path to CxxTest installation])],
 883   [CXXTEST="$withval"])
 884
 885 # In the case of "./configure --with-cxxtest-dir=../cxxtest" (or other
 886 # relative path) and having switched the configure directory (see above),
 887 # search with respect to the top source dir, not the build dir
 888 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes -a -n "$CXXTEST"; then
 889   case "$CXXTEST" in
 890     /*) ;;
 891     *)  CXXTEST="$srcdir/$CXXTEST" ;;
 892   esac
 893 fi
 894
 895 TESTS_ENVIRONMENT=
 896 RUN_REGRESSION_ARGS=
 897 if test "$enable_proof" = yes; then
 898   RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--proof"
 899 fi
 900 AC_SUBST([TESTS_ENVIRONMENT])
 901 AC_SUBST([RUN_REGRESSION_ARGS])
 902
 903 CXXTESTGEN=
 904 AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH])
 905 if test -z "$CXXTESTGEN"; then
 906   AC_PATH_PROG(CXXTESTGEN, cxxtestgen.py, [], [$CXXTEST:$PATH])
 907 fi
 908 if test -z "$CXXTESTGEN"; then
 909   AC_PATH_PROG(CXXTESTGEN, cxxtestgen, [], [$CXXTEST:$PATH])
 910 fi
 911 # The latest version of cxxtest distributed from the git repository places
 912 # cxxtest under <cxxtest-root>/bin/cxxtest
 913 if test -z "$CXXTESTGEN"; then
 914   AC_PATH_PROG(CXXTESTGEN, cxxtestgen, [], [$CXXTEST/bin:$PATH])
 915 fi
 916 if test "$enable_unit_testing" = "no"; then
 917   AC_MSG_NOTICE([unit tests disabled by user request.])
 918   CXXTESTGEN=
 919   CXXTEST=
 920 elif test -z "$CXXTESTGEN"; then
 921   AC_MSG_NOTICE([unit tests disabled, could not find cxxtestgen.pl or cxxtestgen.py or cxxtestgen])
 922 elif test -z "$CXXTEST"; then
 923   CXXTEST=`dirname "$CXXTESTGEN"`
 924   AC_MSG_CHECKING([for location of CxxTest headers])
 925   if test -e "$CXXTEST/cxxtest/TestRunner.h"; then
 926     AC_MSG_RESULT([$CXXTEST])
 927   else
 928     if test -e "/usr/include/cxxtest/TestRunner.h"; then
 929       AC_MSG_RESULT([/usr/include])
 930     else
 931       AC_MSG_RESULT([not found])
 932       AC_MSG_WARN([unit tests disabled, CxxTest headers not found.])
 933       CXXTESTGEN=
 934       CXXTEST=
 935     fi
 936   fi
 937 fi
 938
 939 if test "$enable_unit_testing" = yes -a -z "$CXXTESTGEN"; then
 940   AC_MSG_ERROR([--enable-unit-testing given but cxxtest not found.])
 941 fi
 942
 943 AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"])
 944
 945 AC_ARG_VAR(TEST_CPPFLAGS, [CPPFLAGS to use when testing (default=$CPPFLAGS)])
 946 AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)])
 947 AC_ARG_VAR(TEST_LDFLAGS,  [LDFLAGS to use when testing (default=$LDFLAGS)])
 948
 949 AC_ARG_VAR(PERL, [PERL interpreter (used when testing)])
 950
 951 if test -n "$CXXTEST"; then
 952   if test -z "$PERL"; then
 953     AC_CHECK_PROGS(PERL, perl, perl, [])
 954   else
 955     AC_CHECK_PROG(PERL, "$PERL", "$PERL", [])
 956   fi
 957
 958   if test -z "$PERL"; then
 959     AC_MSG_WARN([unit tests disabled, perl not found.])
 960     CXXTESTGEN=
 961     CXXTEST=
 962   fi
 963 fi
 964
 965 AC_ARG_VAR(PYTHON, [PYTHON interpreter (used for building legacy Java library interface)])
 966
 967 if test -z "$PYTHON"; then
 968   AC_CHECK_PROGS(PYTHON, python, python, [])
 969 else
 970   AC_CHECK_PROG(PYTHON, "$PYTHON", "$PYTHON", [])
 971 fi
 972
 973 if test -z "$PYTHON"; then
 974   AC_MSG_WARN([python not found, cannot build libcvc4compat_java (the legacy Java interface).])
 975   CXXTESTGEN=
 976   CXXTEST=
 977 fi
 978
 979 # Checks for libraries.
 980
 981 AC_SEARCH_LIBS([clock_gettime], [rt],
 982                [AC_DEFINE([HAVE_CLOCK_GETTIME], [1],
 983                           [Defined to 1 if clock_gettime() is supported by the platform.])],
 984                [AC_LIBOBJ([clock_gettime])])
 985 AC_CHECK_FUNC([strtok_r], [AC_DEFINE([HAVE_STRTOK_R], [1],
 986                                      [Defined to 1 if strtok_r() is supported by the platform.])],
 987                           [AC_LIBOBJ([strtok_r])])
 988 AC_CHECK_FUNC([ffs], [AC_DEFINE([HAVE_FFS], [1],
 989                                 [Defined to 1 if ffs() is supported by the platform.])],
 990                      [AC_LIBOBJ([ffs])])
 991
 992 # Check for antlr C++ runtime (defined in config/antlr.m4)
 993 AC_LIB_ANTLR
 994
 995 # Check for user preferences for language bindings to build, and for
 996 # build support.  The arg list is the default set if unspecified by
 997 # the user (the actual built set is the subset that appears to be
 998 # supported by the build host).
 999 CVC4_CHECK_BINDINGS([c java])dnl csharp perl php python ruby tcl ocaml])
1000
1001 # Checks for header files and their contents.
1002 AC_CHECK_HEADERS([getopt.h unistd.h ext/stdio_filebuf.h])
1003
1004 # Checks for typedefs, structures, and compiler characteristics.
1005 #AC_HEADER_STDBOOL
1006 # these are bad macros, they clash with system header <stdint.h> !!
1007 #AC_TYPE_UINT16_T
1008 #AC_TYPE_UINT32_T
1009 #AC_TYPE_UINT64_T
1010 #AC_TYPE_SIZE_T
1011
1012 # guard against double-inclusion of the autoheader
1013 AH_TOP([#ifndef __CVC4__CVC4AUTOCONFIG_H
1014 #define __CVC4__CVC4AUTOCONFIG_H])
1015 AH_BOTTOM([#endif /* __CVC4__CVC4AUTOCONFIG_H */])
1016
1017 AC_CHECK_DECLS([optreset], [], [], [#include <getopt.h>])
1018
1019 # check with which standard strerror_r() complies
1020 AC_FUNC_STRERROR_R
1021
1022 # is is_sorted() in std or __gnu_cxx?
1023 CHECK_FOR_IS_SORTED
1024
1025 # require boost library
1026 BOOST_REQUIRE()
1027
1028 # look for boost threading library
1029 AC_ARG_WITH([portfolio],
1030     AS_HELP_STRING([--with-portfolio], [build the multithreaded portfolio version of CVC4 (pcvc4)]))
1031 cvc4_save_LDFLAGS="$LDFLAGS"
1032 if test "$enable_static_binary" = yes; then
1033   LDFLAGS="-static $LDFLAGS"
1034 fi
1035 cvc4_has_threads=yes
1036 AC_ARG_ENABLE([thread-support],
1037     AS_HELP_STRING([--disable-thread-support], [do not support multithreaded-capable library]))
1038 if test "$enable_thread_support" = no; then
1039   cvc4_has_threads=no
1040   if test "$with_portfolio" = yes; then
1041     AC_MSG_ERROR([user gave both --with-portfolio and --disable-thread-support, which are contradictory])
1042   fi
1043 else
1044   BOOST_THREADS([], [AC_MSG_WARN([disabling multithreaded support])
1045                      cvc4_has_threads=no])
1046 fi
1047 LDFLAGS="$cvc4_save_LDFLAGS"
1048 if test $cvc4_has_threads = no; then
1049   if test "$enable_thread_support" = yes; then
1050     AC_MSG_ERROR([user gave --enable-thread-support but could not build with threads; maybe boost threading library is missing?])
1051   fi
1052   if test "$with_portfolio" = yes; then
1053     AC_MSG_ERROR([user gave --with-portfolio but could not build with threads; maybe boost threading library is missing?])
1054   fi
1055   with_portfolio=no
1056 fi
1057 if test "$with_portfolio" != yes; then
1058   with_portfolio=no
1059 fi
1060 AM_CONDITIONAL([CVC4_BUILD_PCVC4], [test "$with_portfolio" = yes])
1061 if test "$with_portfolio" = yes; then
1062   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PORTFOLIO"
1063
1064   # see if Boost has thread attributes (should be any version >= 1.50.0)
1065   # non-fatal error if not, but we won't support --thread-stack option
1066   AC_MSG_CHECKING([whether Boost threads support thread attrs])
1067   AC_LANG_PUSH([C++])
1068   cvc4_save_CPPFLAGS="$CPPFLAGS"
1069   cvc4_save_LIBS="$LIBS"
1070   cvc4_save_LDFLAGS="$LDFLAGS"
1071   CPPFLAGS="$CPPFLAGS $BOOST_CPPFLAGS"
1072   LIBS="$LIBS $BOOST_THREAD_LIBS"
1073   LDFLAGS="$LDFLAGS $BOOST_THREAD_LDFLAGS"
1074   AC_LINK_IFELSE([AC_LANG_PROGRAM([#include <boost/thread.hpp>],
1075          [boost::thread::attributes attrs; attrs.set_stack_size(10 * 1024 * 1024);])],
1076     [cvc4_boost_has_thread_attr=1;
1077      AC_MSG_RESULT([yes])],
1078     [cvc4_boost_has_thread_attr=0;
1079      AC_MSG_RESULT([no])])
1080   CPPFLAGS="$cvc4_save_CPPFLAGS"
1081   LIBS="$cvc4_save_LIBS"
1082   LDFLAGS="$cvc4_save_LDFLAGS"
1083   AC_LANG_POP([C++])
1084 else
1085   cvc4_boost_has_thread_attr=0
1086 fi
1087 AC_DEFINE_UNQUOTED([BOOST_HAS_THREAD_ATTR], $cvc4_boost_has_thread_attr, [Define to 1 if Boost threading library has support for thread attributes])
1088
1089 # Check for libreadline (defined in config/readline.m4)
1090 AC_ARG_WITH([readline], [AS_HELP_STRING([--with-readline], [support the readline library])], [], [with_readline=check])
1091 # make the flags as close as possible to the final flags, because the Boost
1092 # flags can bring in a different, incompatible readline library than we'd
1093 # get otherwise (e.g. on Mac, where there are commonly two different readlines,
1094 # one in /usr and one in /opt/local)
1095 cvc4_rlcheck_save_CPPFLAGS="$CPPFLAGS"
1096 cvc4_rlcheck_save_CXXFLAGS="$CXXFLAGS"
1097 cvc4_rlcheck_save_CFLAGS="$CFLAGS"
1098 cvc4_rlcheck_save_LDFLAGS="$LDFLAGS"
1099 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
1100 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS $WNO_DEPRECATED"
1101 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS $C_WNO_DEPRECATED -fexceptions"
1102 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
1103 CVC4_CHECK_FOR_READLINE
1104 CPPFLAGS="$cvc4_rlcheck_save_CPPFLAGS"
1105 CXXFLAGS="$cvc4_rlcheck_save_CXXFLAGS"
1106 CFLAGS="$cvc4_rlcheck_save_CFLAGS"
1107 LDFLAGS="$cvc4_rlcheck_save_LDFLAGS"
1108 AC_DEFINE_UNQUOTED([HAVE_LIBREADLINE], $have_libreadline, [Define to 1 to use libreadline])
1109 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])
1110 AC_SUBST([READLINE_LIBS])
1111
1112 # Whether to build compatibility library
1113 CVC4_BUILD_LIBCOMPAT=yes
1114 AC_ARG_WITH([compat],
1115     AS_HELP_STRING([--with-compat], [build compatibility library (CVC3 API layer)]),
1116     [if test "$withval" = no; then CVC4_BUILD_LIBCOMPAT=no; fi])
1117 AC_MSG_CHECKING([whether to build compatibility library (CVC3 API layer)])
1118 if test "$CVC4_BUILD_LIBCOMPAT" = yes; then
1119   AC_MSG_RESULT([yes])
1120 else
1121   AC_MSG_RESULT([no, disabled by user])
1122 fi
1123 AC_SUBST(CVC4_BUILD_LIBCOMPAT)
1124 AM_CONDITIONAL([CVC4_BUILD_LIBCOMPAT], [test "$CVC4_BUILD_LIBCOMPAT" = yes])
1125
1126 # Check for availability of TLS support (e.g. __thread storage class)
1127 AC_MSG_CHECKING([whether to use compiler-supported TLS if available])
1128 AC_ARG_ENABLE([tls], AS_HELP_STRING([--disable-tls], [don't use compiler-native TLS]))
1129 if test $cvc4_has_threads = no; then
1130   # We disable TLS entirely by simply telling the build system that
1131   # the empty string is the __thread keyword.
1132   AC_MSG_RESULT([multithreading disabled])
1133   CVC4_TLS_SUPPORTED=1
1134   CVC4_TLS=
1135   CVC4_TLS_explanation='disabled (no multithreading support)'
1136 else
1137   if test -z "${enable_tls+set}" || test "$enable_tls" = "yes"; then
1138     AC_MSG_RESULT([yes])
1139     AX_TLS([CVC4_TLS=$ac_cv_tls], [CVC4_TLS=])
1140   else
1141     AC_MSG_RESULT([no])
1142     CVC4_TLS=
1143   fi
1144   if test -n "$CVC4_TLS"; then
1145     CVC4_TLS_SUPPORTED=1
1146     CVC4_TLS_explanation="$CVC4_TLS"
1147   else
1148     CVC4_TLS_explanation='pthread_getspecific()'
1149     CVC4_TLS_SUPPORTED=0
1150   fi
1151 fi
1152 AC_SUBST([CVC4_TLS])
1153 AC_SUBST([CVC4_TLS_SUPPORTED])
1154
1155 # Whether to compile with google profiling tools
1156 cvc4_use_google_perftools=0
1157 AC_ARG_WITH(
1158     [google_perftools],
1159     AS_HELP_STRING(
1160         [--with-google-perftools],
1161         [use Google Performance Tools]
1162     ),
1163     [if test "$withval" != no; then
1164         cvc4_use_google_perftools=1
1165      fi
1166     ]
1167 )
1168 AC_MSG_CHECKING([whether to link in google perftools libraries])
1169 if test $cvc4_use_google_perftools = 1; then
1170   AC_MSG_RESULT([yes])
1171   AC_CHECK_LIB([tcmalloc], [MallocExtension_GetAllocatedSize], , [AC_MSG_ERROR([cannot link google-perftools test program with -ltcmalloc])], [-lpthread])
1172   AC_CHECK_LIB([profiler], [ProfilerStart], , [AC_MSG_ERROR([cannot link google-perftools test program with -lprofiler])], [-lpthread])
1173 else
1174   AC_MSG_RESULT([no (user didn't request it)])
1175 fi
1176
1177 # Java
1178 AC_ARG_VAR(JAVA, [Java interpreter (used when testing Java interface)])
1179 AC_ARG_VAR(JAVAC, [Java compiler (used when building and testing Java interface)])
1180 AC_ARG_VAR(JAVAH, [Java compiler (used when building and testing Java interface)])
1181 AC_ARG_VAR(JAR, [Jar archiver (used when building Java interface)])
1182 if test "$cvc4_build_java_bindings"; then
1183   dnl AM_PROG_GCJ
1184   if test -z "$JAVA"; then
1185     AC_CHECK_PROGS(JAVA, java, java, [])
1186   else
1187     AC_CHECK_PROG(JAVA, "$JAVA", "$JAVA", [])
1188   fi
1189   if test -z "$JAVAC"; then
1190     AC_CHECK_PROGS(JAVAC, javac gcj, javac, [])
1191     if test "$JAVAC" = gcj; then JAVAC='gcj -C'; fi
1192   else
1193     AC_CHECK_PROG(JAVAC, "$JAVAC", "$JAVAC", [])
1194   fi
1195   if test -z "$JAVAH"; then
1196     AC_CHECK_PROGS(JAVAH, javah gcjh, javah, [])
1197   else
1198     AC_CHECK_PROG(JAVAH, "$JAVAH", "$JAVAH", [])
1199   fi
1200   if test -z "$JAR"; then
1201     AC_CHECK_PROGS(JAR, jar, jar, [])
1202   else
1203     AC_CHECK_PROG(JAR, "$JAR", "$JAR", [])
1204   fi
1205 fi
1206
1207 # on Mac OS X, Java doesn't like the .so module extension; it wants .dylib
1208 module=no eval CVC4_JAVA_MODULE_EXT="$shrext_cmds"
1209 if test -z "$CVC4_JAVA_MODULE_EXT"; then
1210   CVC4_JAVA_MODULE_EXT=.so
1211 fi
1212 AC_SUBST([CVC4_JAVA_MODULE_EXT])
1213
1214 # Prepare configure output
1215
1216 if test "$enable_shared" = yes; then BUILDING_SHARED=1; else BUILDING_SHARED=0; fi
1217 if test "$enable_static" = yes; then BUILDING_STATIC=1; else BUILDING_STATIC=0; fi
1218 if test "$enable_static_binary" = yes; then STATIC_BINARY=1; else STATIC_BINARY=0; fi
1219 AC_SUBST(BUILDING_SHARED)
1220 AC_SUBST(BUILDING_STATIC)
1221 AC_SUBST(STATIC_BINARY)
1222 AM_CONDITIONAL([STATIC_BINARY], [test "$enable_static_binary" = yes])
1223 AM_CONDITIONAL([COVERAGE_ENABLED], [test "$enable_coverage" = yes])
1224
1225 AM_CONDITIONAL([CVC4_DEBUG], [test "$with_build" = debug])
1226 AM_CONDITIONAL([CVC4_TRACING], [test "$enable_tracing" = yes])
1227
1228 AC_SUBST(CVC4_LIBRARY_VERSION)
1229 AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
1230 AC_SUBST(CVC4_COMPAT_LIBRARY_VERSION)
1231 AC_SUBST(CVC4_BINDINGS_LIBRARY_VERSION)
1232
1233 AC_DEFINE_UNQUOTED(CVC4_MAJOR, ${CVC4_MAJOR}, [Major component of the version of CVC4.])
1234 AC_DEFINE_UNQUOTED(CVC4_MINOR, ${CVC4_MINOR}, [Minor component of the version of CVC4.])
1235 AC_DEFINE_UNQUOTED(CVC4_RELEASE, ${CVC4_RELEASE}, [Release component of the version of CVC4.])
1236 AC_DEFINE_UNQUOTED(CVC4_EXTRAVERSION, ["${CVC4_EXTRAVERSION}"], [Extraversion component of the version of CVC4.])
1237 AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full release string for CVC4.])
1238
1239 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
1240 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
1241 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions"
1242 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
1243
1244 # visibility flag not supported for Windows builds
1245 # also increase default stack size for Windows binaries
1246 case $host_os in
1247   (*mingw*) FLAG_VISIBILITY_HIDDEN=
1248             cvc4_LDFLAGS=-Wl,--stack,134217728
1249             pcvc4_LDFLAGS=-Wl,--stack,134217728
1250 esac
1251
1252 AC_SUBST(FLAG_VISIBILITY_HIDDEN)
1253 AC_SUBST(cvc4_LDFLAGS)
1254 AC_SUBST(pcvc4_LDFLAGS)
1255
1256 AM_CONDITIONAL(WHITE_AND_BLACK_TESTS, [test -z "$FLAG_VISIBILITY_HIDDEN"])
1257
1258 # remember the command line used for configure
1259 AC_SUBST(cvc4_config_cmdline)
1260
1261 # mk_include
1262 #
1263 # When automake scans Makefiles, it complains about non-standard make
1264 # features (including GNU extensions), and breaks GNU Make's
1265 # "if/endif" construct, replacing the "if" with AM_CONDITIONAL if
1266 # constructs.  automake even follows "include" and messes with
1267 # included Makefiles.
1268 #
1269 # CVC4 assumes GNU Make and we want to use GNU Make if/endifs, so we
1270 # have to hide some included Makefiles with GNU extensions.  We do
1271 # this by defining mk_include as an autoconf substitution and then
1272 # using "@mk_include@ other_makefile" in Makefile.am to include
1273 # makefiles with GNU extensions; this hides them from automake.
1274 mk_include=include
1275 AC_SUBST(mk_include)
1276 # Similar trickery for "if"
1277 mk_if=if
1278 AC_SUBST(mk_if)
1279 mk_empty=
1280 AC_SUBST(mk_empty)
1281
1282 # CVC4_FALSE
1283 #
1284 # This is used to _always_ comment out rules in automake makefiles, but
1285 # still trigger certain automake behavior; see test/unit/Makefile.am.
1286 AM_CONDITIONAL([CVC4_FALSE], [false])
1287
1288 # set up substitutions for src/util/{rational,integer}.h.in
1289 if test $cvc4_cln_or_gmp = cln; then
1290   CVC4_USE_CLN_IMP=1
1291   CVC4_USE_GMP_IMP=0
1292 else
1293   CVC4_USE_CLN_IMP=0
1294   CVC4_USE_GMP_IMP=1
1295 fi
1296 AC_SUBST(CVC4_USE_CLN_IMP)
1297 AC_SUBST(CVC4_USE_GMP_IMP)
1298
1299 # month/year for man pages
1300 MAN_DATE=`date '+%B %Y'`
1301 AC_SUBST(MAN_DATE)
1302
1303 AC_CONFIG_FILES([
1304   Makefile.builds
1305   Makefile
1306   proofs/signatures/Makefile]
1307   m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | grep -v '^contrib/alttheoryskel/' | sort | sed 's,\.am$,,'])
1308 )
1309
1310 if test $cvc4_has_threads = yes; then
1311   support_multithreaded='with boost threading library'
1312   AM_CONDITIONAL([CVC4_HAS_THREADS], [true])
1313   AC_SUBST([CVC4_HAS_THREADS], 1)
1314 else
1315   support_multithreaded='no'
1316   AM_CONDITIONAL([CVC4_HAS_THREADS], [false])
1317   AC_SUBST([CVC4_HAS_THREADS], 0)
1318 fi
1319
1320 AM_CONDITIONAL([CVC4_NEEDS_REPLACEMENT_FUNCTIONS], [test -n "$LIBOBJS"])
1321
1322 # Final information to the user
1323 gpl=no
1324 licensewarn=
1325
1326 if test "$custom_build_profile" = yes; then
1327   with_build="$with_build (customized)"
1328 fi
1329
1330 support_unit_tests='cxxtest not found; unit tests not supported'
1331 if test -n "$CXXTEST"; then
1332   support_unit_tests='unit testing infrastructure enabled in build directory'
1333 elif test "$enable_unit_testing" = no; then
1334   support_unit_tests='unit testing disabled by user'
1335 fi
1336
1337 if test "$enable_optimized" = yes; then
1338   optimized="yes, at level $OPTLEVEL"
1339 else
1340   optimized="no"
1341 fi
1342
1343 if test $have_libglpk -eq 1; then
1344   gpl=yes
1345   gpllibs="${gpllibs} glpk"
1346 fi
1347
1348 if test $have_libreadline -eq 1; then
1349   gpl=yes
1350   gpllibs="${gpllibs} readline"
1351 fi
1352
1353 if test $cvc4_cln_or_gmp = cln; then
1354   mplibrary='cln (GPL)'
1355   gpl=yes
1356   gpllibs="${gpllibs} cln"
1357   if test $with_portfolio = yes; then
1358     AC_ERROR([Bad configuration detected: cannot build portfolio with CLN.
1359 Please specify only one of --with-portfolio and --with-cln.])
1360   fi
1361 else
1362   mplibrary='gmp'
1363 fi
1364
1365 if test "$gpl" = yes; then
1366   if test "$CVC4_BSD_LICENSED_CODE_ONLY" = 1; then
1367     AC_ERROR([Bad configuration detected: BSD-licensed code only, but also requested GPLed libraries:$gpllibs
1368 To permit GPL'ed dependences, use the configure flag --enable-gpl])
1369   fi
1370
1371   licensewarn="${licensewarn}"'****************************************************************************
1372 Please note that CVC4 will be built against the following GPLed libraries:
1373  '"$gpllibs"'
1374 As these libraries are covered under the GPLv3, so is this build of CVC4.
1375 CVC4 is also available to you under the terms of the (modified) BSD license.
1376 If you prefer to license CVC4 under those terms, please configure with the
1377 option "--bsd", which will disable all optional GPLed library dependences.
1378 ****************************************************************************
1379
1380 '
1381   license="GPLv3 (due to optional libraries; see below)"
1382 else
1383   licensewarn="${licensewarn}Please note that this configuration is NOT built against any GPL'ed
1384 libraries, so it is covered by the (modified) BSD license.  This is,
1385 however, not the best-performing configuration of CVC4.  To build
1386 against GPL'ed libraries which improve CVC4's performance, re-configure
1387 with '--best --enable-gpl'.
1388
1389 "
1390   license="modified BSD"
1391 fi
1392
1393 if test "$gpl" = yes; then isgpl=1; else isgpl=0; fi
1394 AC_DEFINE_UNQUOTED(CVC4_GPL_DEPS, $isgpl, [Whether CVC4 is built with the (optional) GPLed library dependences.])
1395
1396 CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="$CVC4_COMPAT_LIBRARY_VERSION"
1397 CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="$CVC4_BINDINGS_LIBRARY_VERSION"
1398 if test "$CVC4_BUILD_LIBCOMPAT" = no; then
1399   CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="N/A"
1400 fi
1401 if test -z "$CVC4_LANGUAGE_BINDINGS"; then
1402   CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="N/A"
1403 fi
1404
1405 bindings_to_be_built=none
1406 if test -n "$CVC4_LANGUAGE_BINDINGS"; then
1407   bindings_to_be_built="$CVC4_LANGUAGE_BINDINGS"
1408   if test -z "$SWIG"; then
1409     bindings_to_be_built="$bindings_to_be_built (for CVC3 compatibility layer only; SWIG not found)"
1410   fi
1411 fi
1412
1413 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/base/tls.h])
1414 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
1415 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
1416
1417 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template])
1418 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5])
1419 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3_template])
1420 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc_template])
1421 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc_template])
1422 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3])
1423 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3])
1424
1425 AC_OUTPUT
1426
1427 cat <<EOF
1428
1429 CVC4 $VERSION
1430
1431 Build profile: $with_build
1432 Build ID     : $build_type
1433 Optimized    : $optimized
1434 Debug symbols: $enable_debug_symbols
1435 Proofs       : $enable_proof
1436 Statistics   : $enable_statistics
1437 Replay       : $enable_replay
1438 Assertions   : $enable_assertions
1439 Tracing      : $enable_tracing
1440 Dumping      : $enable_dumping
1441 Muzzle       : $enable_muzzle
1442
1443 Unit tests   : $support_unit_tests
1444 gcov support : $enable_coverage
1445 gprof support: $enable_profiling
1446
1447 Static libs  : $enable_static
1448 Shared libs  : $enable_shared
1449 Static binary: $enable_static_binary
1450 Compat lib   : $CVC4_BUILD_LIBCOMPAT
1451 Bindings     : $bindings_to_be_built
1452
1453 Multithreaded: $support_multithreaded
1454 TLS support  : $CVC4_TLS_explanation
1455 Portfolio    : $with_portfolio
1456
1457 MP library   : $mplibrary
1458 GLPK         : $with_glpk
1459 ABC          : $with_abc
1460 Readline     : $with_readline
1461
1462 CPPFLAGS     : $CPPFLAGS
1463 CXXFLAGS     : $CXXFLAGS
1464 CFLAGS       : $CFLAGS
1465 LIBS         : $LIBS
1466 LDFLAGS      : $LDFLAGS
1467
1468 libcvc4 version        : $CVC4_LIBRARY_VERSION
1469 libcvc4parser version  : $CVC4_PARSER_LIBRARY_VERSION
1470 libcvc4compat version  : $CVC4_COMPAT_LIBRARY_VERSION_or_nobuild
1471 libcvc4bindings version: $CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild
1472
1473 Install into : $prefix
1474
1475 CVC4 license : $license
1476
1477 ${licensewarn}Now just type make, followed by make check or make install, as you like.
1478
1479 EOF
1480
1481 if test -n "$CVC4_UNSUPPORTED_LANGUAGE_BINDINGS"; then
1482   AC_MSG_WARN([])
1483   AC_MSG_WARN([You are electing to build unsupported language binding(s):])
1484   AC_MSG_WARN([    $CVC4_UNSUPPORTED_LANGUAGE_BINDINGS])
1485   AC_MSG_WARN([Please be aware that these bindings may not compile, or])
1486   AC_MSG_WARN([work, and the interface to CVC4 via these bindings may])
1487   AC_MSG_WARN([change drastically in upcoming releases of CVC4.])
1488   AC_MSG_WARN([])
1489 fi
1490
1491 if test -n "$CVC4_INTEGRITY_WARNING"; then
1492   AC_MSG_WARN([])
1493   AC_MSG_WARN($CVC4_INTEGRITY_WARNING)
1494   AC_MSG_WARN([Please run "make check" after building to ensure integrity of the binary and library])
1495   AC_MSG_WARN([])
1496 fi