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