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