configure.ac

   1 #                                               -*- Autoconf -*-
   2 # Process this file with autoconf to produce a configure script.
   3
   4 m4_define(_CVC4_MAJOR,          0)       dnl version (major)
   5 m4_define(_CVC4_MINOR,          0)       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])
 207 AC_CONFIG_HEADERS([cvc4autoconfig.h])
 208
 209 # Initialize libtool's configuration options.
 210 _LT_SET_OPTION([LT_INIT],[win32-dll])
 211 LT_INIT
 212
 213 # Checks for programs.
 214 AC_PROG_CC
 215 AC_PROG_CXX
 216 AC_PROG_INSTALL
 217
 218 CVC4_GCC_VERSION
 219
 220 # [chris 8/24/2010] The user *must* specify --with-cln to get CLN
 221 # (and, thus, opt in to the GPL dependency).
 222
 223 cvc4_use_gmp=0
 224 cvc4_use_cln=0
 225
 226 AC_ARG_WITH(
 227   [cln],
 228   AS_HELP_STRING(
 229     [--with-cln],
 230     [use CLN instead of GMP]
 231   ),
 232   [if test "$withval" != no; then
 233      cvc4_use_cln=1
 234    fi
 235   ]
 236 )
 237
 238 # [chris 8/24/2010] --with-gmp has no practical effect, since GMP is
 239 # the default. Could be useful if other options are added later.
 240
 241 AC_ARG_WITH(
 242   [gmp],
 243   AS_HELP_STRING(
 244     [--with-gmp],
 245     [use GMP instead of CLN (default)]
 246   ),
 247   [if test "$withval" = no; then
 248      if test $cvc4_use_cln = 0; then
 249        AC_MSG_ERROR([You must use either CLN and GMP.  Please pick one.])
 250      fi
 251    else
 252      cvc4_use_gmp=1
 253    fi
 254   ]
 255 )
 256
 257 if test $cvc4_use_cln = 1 && test $cvc4_use_gmp = 1; then
 258   # error
 259   AC_MSG_ERROR([You cannot use both CLN and GMP.  Please pick one.])
 260 fi
 261
 262 # try GMP, fail if not found; GMP is required for both CLN and for GMP
 263 # versions of CVC4
 264 AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP (libgmp) not found, see http://gmplib.org/])])
 265
 266 if test $cvc4_use_cln = 1; then
 267   # [mdeters] The PKG_CHECK_MODULES macro isn't customizable and doesn't fail
 268   # gracefully.  You can only specify it once for a given library name.  That
 269   # is, even on separate if/else branches, you can't put
 270   # PKG_CHECK_MODULES([CLN], ...).  That's why things are so convoluted here,
 271   # we have to have PKG_CHECK_MODULES _exactly_ once in configure.ac !
 272   PKG_CHECK_MODULES([CLN], [cln >= 1.2.2],
 273     [cvc4_use_cln=1
 274      AC_LANG_PUSH([C++])
 275      AC_LINK_IFELSE([AC_LANG_PROGRAM([[#include <cln/cln.h>]], [[cln::cl_F pi = "3.1415926";]])])
 276      AC_LANG_POP([C++])
 277     ],
 278     [if test $cvc4_use_cln = 0; then
 279        # fall back to GMP
 280        AC_MSG_NOTICE([CLN not installed (or too old) or pkgconfig missing, will use gmp])
 281      else
 282        # fail
 283        AC_MSG_ERROR([CLN not installed (or too old) or pkgconfig missing])
 284      fi
 285     ]
 286   )
 287 fi
 288 if test $cvc4_use_cln = 0; then
 289   # try GMPXX, fail if not found
 290   AC_CHECK_LIB(gmpxx, __gmpz_init, , [AC_MSG_ERROR([GNU MP C++ library (libgmpxx) not found, see http://gmplib.org/])])
 291   cvc4_cln_or_gmp=gmp
 292 else
 293   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }$CLN_CFLAGS"
 294   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }$CLN_CFLAGS"
 295   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }$CLN_CFLAGS"
 296   LIBS="${LIBS:+$LIBS }$CLN_LIBS"
 297   cvc4_cln_or_gmp=cln
 298 fi
 299
 300 if test $cvc4_cln_or_gmp = cln; then
 301   AC_DEFINE_UNQUOTED(CVC4_CLN_IMP, [], [Defined if using the CLN multi-precision arithmetic library.])
 302 else
 303   AC_DEFINE_UNQUOTED(CVC4_GMP_IMP, [], [Defined if using the GMP multi-precision arithmetic library.])
 304 fi
 305 AM_CONDITIONAL([CVC4_CLN_IMP], [test $cvc4_cln_or_gmp = cln])
 306 AM_CONDITIONAL([CVC4_GMP_IMP], [test $cvc4_cln_or_gmp = gmp])
 307
 308 # construct the build string
 309 AC_MSG_CHECKING([for appropriate build string])
 310 if test -z "$ac_confdir"; then
 311   ac_confdir="$srcdir"
 312 fi
 313 build_type=`$ac_confdir/config/build-type $with_build $btargs $cvc4_cln_or_gmp`
 314 if test "$custom_build_profile" = yes; then
 315   if test "$with_build" = default; then
 316     build_type=`$ac_confdir/config/build-type custom $btargs $cvc4_cln_or_gmp`
 317   fi
 318 fi
 319 AC_MSG_RESULT($build_type)
 320
 321 # Require building in target and build-specific build directory:
 322 #
 323 # If the configure script is invoked from the top-level source
 324 # directory, it creates a suitable build directory (based on the build
 325 # architecture and build profile from $build_type), changes into it,
 326 # and reinvokes itself.  CVC4_CONFIGURE_IN_BUILDS is an envariable
 327 # that breaks any possibility of infinite recursion in this process.
 328 AC_MSG_CHECKING([what dir to configure])
 329 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes; then
 330   AC_MSG_RESULT([this one (in builds/)])
 331 elif test "$CVC4_CONFIGURE_AT_TOP_LEVEL" = yes; then
 332   AC_MSG_RESULT([builds/$target/$build_type])
 333   $as_echo
 334   if test -z "$ac_srcdir"; then
 335     mkbuilddir=./config/mkbuilddir
 336   else
 337     mkbuilddir=$ac_srcdir/config/mkbuilddir
 338   fi
 339   $as_echo "$mkbuilddir $target $build_type"
 340   source $mkbuilddir "$target" "$build_type"
 341   $as_echo "cd builds/$target/$build_type"
 342   cd "builds/$target/$build_type"
 343   CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS
 344   echo "$SHELL ../../../configure ${config_cmdline[[@]]}"
 345   "$SHELL" "`pwd`/../../../configure" "${config_cmdline[[@]]}"
 346   exitval=$?
 347   cd ../../..
 348   if test $exitval -eq 0; then
 349     cat >config.reconfig <<EOF
 350 [#!/bin/bash
 351 # Generated by configure, `date`
 352 # This script is part of CVC4.
 353
 354 cd "\`dirname \\"\$0\\"\`"
 355
 356 if test -d builds; then :; else echo 'No builds/ directory!' >&2; exit; fi
 357
 358 current=(\`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]*\\)/\\(.*\\),\\1 \\2,'\`)
 359 arch=\${current[0]}
 360 build=\${current[1]}
 361
 362 echo "reconfiguring in builds/\$arch/\$build..."
 363 cd "builds/\$arch/\$build"
 364 echo ./config.status "\$@"
 365 ./config.status "\$@"]
 366 EOF
 367     chmod +x config.reconfig
 368   fi
 369   exit $exitval
 370 else
 371   AC_MSG_RESULT([this one (user-specified)])
 372 fi
 373
 374 as_me=configure
 375
 376 # Unpack standard build types. Any particular options can be overriden with
 377 # --enable/disable-X options
 378 case "$with_build" in
 379   production) # highly optimized, no assertions, no tracing, dumping
 380     CVC4CPPFLAGS=
 381     CVC4CXXFLAGS=
 382     CVC4CFLAGS=
 383     CVC4LDFLAGS=
 384     FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
 385     if test -z "${OPTLEVEL+set}"            ; then OPTLEVEL=3                       ; fi
 386     if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; fi
 387     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes         ; fi
 388     if test -z "${enable_statistics+set}"   ; then enable_statistics=yes            ; fi
 389     if test -z "${enable_replay+set}"       ; then enable_replay=no                 ; fi
 390     if test -z "${enable_assertions+set}"   ; then enable_assertions=no             ; fi
 391     if test -z "${enable_proof+set}"        ; then enable_proof=no                  ; fi
 392     if test -z "${enable_tracing+set}"      ; then enable_tracing=no                ; fi
 393     if test -z "${enable_dumping+set}"      ; then enable_dumping=yes               ; fi
 394     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
 395     ;;
 396   debug) # unoptimized, debug symbols, assertions, tracing, dumping
 397     CVC4CPPFLAGS=-DCVC4_DEBUG
 398     CVC4CXXFLAGS='-fno-inline'
 399     CVC4CFLAGS='-fno-inline'
 400     CVC4LDFLAGS=
 401     FLAG_VISIBILITY_HIDDEN=
 402     if test -z "${enable_optimized+set}"    ; then enable_optimized=no              ; fi
 403     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes         ; fi
 404     if test -z "${enable_statistics+set}"   ; then enable_statistics=yes            ; fi
 405     if test -z "${enable_replay+set}"       ; then enable_replay=yes                ; fi
 406     if test -z "${enable_assertions+set}"   ; then enable_assertions=yes            ; fi
 407     if test -z "${enable_proof+set}"        ; then enable_proof=no                  ; fi
 408     if test -z "${enable_tracing+set}"      ; then enable_tracing=yes               ; fi
 409     if test -z "${enable_dumping+set}"      ; then enable_dumping=yes               ; fi
 410     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
 411     ;;
 412   default) # moderately optimized, assertions, tracing, dumping
 413     CVC4CPPFLAGS=
 414     CVC4CXXFLAGS=
 415     CVC4CFLAGS=
 416     CVC4LDFLAGS=
 417     FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
 418     if test -z "${OPTLEVEL+set}"            ; then OPTLEVEL=2                       ; fi
 419     if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; fi
 420     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes         ; fi
 421     if test -z "${enable_statistics+set}"   ; then enable_statistics=yes            ; fi
 422     if test -z "${enable_replay+set}"       ; then enable_replay=yes                ; fi
 423     if test -z "${enable_assertions+set}"   ; then enable_assertions=yes            ; fi
 424     if test -z "${enable_proof+set}"        ; then enable_proof=no                  ; fi
 425     if test -z "${enable_tracing+set}"      ; then enable_tracing=yes               ; fi
 426     if test -z "${enable_dumping+set}"      ; then enable_dumping=yes               ; fi
 427     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
 428     ;;
 429   competition) # maximally optimized, no assertions, no tracing, no dumping, muzzled
 430     CVC4CPPFLAGS='-DCVC4_COMPETITION_MODE'
 431     CVC4CXXFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
 432     CVC4CFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
 433     CVC4LDFLAGS=
 434     FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
 435     if test -z "${OPTLEVEL+set}"            ; then OPTLEVEL=9                       ; fi
 436     if test -z "${enable_optimized+set}"    ; then enable_optimized=yes             ; fi
 437     if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no          ; fi
 438     if test -z "${enable_statistics+set}"   ; then enable_statistics=no             ; fi
 439     if test -z "${enable_replay+set}"       ; then enable_replay=no                 ; fi
 440     if test -z "${enable_assertions+set}"   ; then enable_assertions=no             ; fi
 441     if test -z "${enable_proof+set}"        ; then enable_proof=no                  ; fi
 442     if test -z "${enable_tracing+set}"      ; then enable_tracing=no                ; fi
 443     if test -z "${enable_dumping+set}"      ; then enable_dumping=no                ; fi
 444     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=yes                ; fi
 445     if test -z "${user_specified_enable_or_disable_shared}"; then enable_shared=no; fi
 446     if test -z "${user_specified_enable_or_disable_static}"; then enable_static=yes; fi
 447     if test -z "${enable_static_binary+set}"; then enable_static_binary=yes         ; fi
 448     ;;
 449   *)
 450     AC_MSG_FAILURE([unknown build profile: $with_build])
 451     ;;
 452 esac
 453 if test -z "${OPTLEVEL+set}"; then OPTLEVEL=3; fi
 454
 455 AM_CONDITIONAL([CVC4_BUILD_PROFILE_PRODUCTION],  [test "$with_build" = production])
 456 AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEBUG],       [test "$with_build" = debug])
 457 AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEFAULT],     [test "$with_build" = default])
 458 AM_CONDITIONAL([CVC4_BUILD_PROFILE_COMPETITION], [test "$with_build" = competition])
 459
 460 # permit a static binary
 461 AC_MSG_CHECKING([whether to build a static binary])
 462 AC_ARG_ENABLE([static-binary],
 463      [AS_HELP_STRING([--enable-static-binary],
 464                      [build a fully statically-linked binary [default=no]])])
 465 if test -z "${enable_static_binary+set}"; then
 466   enable_static_binary=no
 467 fi
 468 AC_MSG_RESULT([$enable_static_binary])
 469 if test "$enable_static_binary" = yes -a "$enable_static" != yes; then
 470   enable_static=yes
 471   AC_MSG_WARN([forcing static-library building, --enable-static-binary given])
 472 fi
 473
 474 AC_MSG_CHECKING([whether to support proof in libcvc4])
 475
 476 AC_ARG_ENABLE([proof],
 477   [AS_HELP_STRING([--enable-proof],
 478      [support proof generation])])
 479 if test -z "${enable_proof+set}"; then
 480   enable_proof=no
 481 fi
 482 AC_MSG_RESULT([$enable_proof])
 483
 484 if test "$enable_proof" = yes; then
 485   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROOF"
 486 fi
 487
 488 AC_MSG_CHECKING([whether to optimize libcvc4])
 489
 490 AC_ARG_ENABLE([optimized],
 491   [AS_HELP_STRING([--enable-optimized],
 492      [optimize the build])])
 493
 494 if test -z "${enable_optimized+set}"; then
 495   enable_optimized=no
 496 fi
 497
 498 AC_MSG_RESULT([$enable_optimized])
 499
 500 if test "$enable_optimized" = yes; then
 501   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O$OPTLEVEL"
 502   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O$OPTLEVEL"
 503 else
 504   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O0"
 505   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O0"
 506 fi
 507
 508 AC_MSG_CHECKING([whether to include debugging symbols in libcvc4])
 509
 510 AC_ARG_ENABLE([debug-symbols],
 511   [AS_HELP_STRING([--disable-debug-symbols],
 512      [do not include debug symbols in libcvc4])])
 513
 514 if test -z "${enable_debug_symbols+set}"; then
 515   enable_debug_symbols=yes
 516 fi
 517
 518 AC_MSG_RESULT([$enable_debug_symbols])
 519
 520 if test "$enable_debug_symbols" = yes; then
 521   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-ggdb3"
 522   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-ggdb3"
 523 fi
 524
 525 AC_MSG_CHECKING([whether to include statistics are turned on in libcvc4])
 526
 527 AC_ARG_ENABLE([statistics],
 528   [AS_HELP_STRING([--disable-statistics],
 529      [do not include statistics in libcvc4])])
 530
 531 if test -z "${enable_statistics+set}"; then
 532   enable_statistics=yes
 533 fi
 534
 535 AC_MSG_RESULT([$enable_statistics])
 536
 537 if test "$enable_statistics" = yes; then
 538   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_STATISTICS_ON"
 539 fi
 540
 541 AC_MSG_CHECKING([whether the replay feature should be turned on in libcvc4])
 542
 543 AC_ARG_ENABLE([replay],
 544   [AS_HELP_STRING([--disable-replay],
 545      [turn off the replay feature in libcvc4])])
 546
 547 if test -z "${enable_replay+set}"; then
 548   enable_replay=yes
 549 fi
 550
 551 AC_MSG_RESULT([$enable_replay])
 552
 553 if test "$enable_replay" = yes; then
 554   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_REPLAY"
 555 fi
 556
 557 AC_MSG_CHECKING([whether to include assertions in build])
 558
 559 AC_ARG_ENABLE([assertions],
 560   [AS_HELP_STRING([--disable-assertions],
 561      [turn off assertions in build])])
 562
 563 if test -z "${enable_assertions+set}"; then
 564   enable_assertions=yes
 565 fi
 566
 567 AC_MSG_RESULT([$enable_assertions])
 568
 569 if test "$enable_assertions" = yes; then
 570   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_ASSERTIONS"
 571 else
 572   # turn off regular C assert() also
 573   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DNDEBUG"
 574 fi
 575
 576 AC_MSG_CHECKING([whether to do a traceable build of CVC4])
 577 AC_ARG_ENABLE([tracing],
 578   [AS_HELP_STRING([--disable-tracing],
 579      [remove all tracing code from CVC4])])
 580
 581 if test -z "${enable_tracing+set}"; then
 582   enable_tracing=yes
 583 fi
 584
 585 AC_MSG_RESULT([$enable_tracing])
 586
 587 if test "$enable_tracing" = yes; then
 588   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_TRACING"
 589 fi
 590
 591 AC_MSG_CHECKING([whether to do a dump-capable build of CVC4])
 592 AC_ARG_ENABLE([dumping],
 593   [AS_HELP_STRING([--disable-dumping],
 594      [remove all dumping code from CVC4])])
 595
 596 if test -z "${enable_dumping+set}"; then
 597   enable_dumping=yes
 598 fi
 599
 600 AC_MSG_RESULT([$enable_dumping])
 601
 602 if test "$enable_dumping" = yes; then
 603   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DUMPING"
 604 fi
 605
 606 AC_MSG_CHECKING([whether to do a muzzled build of CVC4])
 607 AC_ARG_ENABLE([muzzle],
 608   [AS_HELP_STRING([--enable-muzzle],
 609      [completely silence CVC4; remove ALL non-result output from build])])
 610
 611 if test -z "${enable_muzzle+set}"; then
 612   enable_muzzle=no
 613 fi
 614
 615 AC_MSG_RESULT([$enable_muzzle])
 616
 617 if test "$enable_muzzle" = yes; then
 618   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_MUZZLE"
 619 fi
 620
 621 AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4])
 622 AC_ARG_ENABLE([coverage],
 623   [AS_HELP_STRING([--enable-coverage],
 624      [build with support for gcov coverage testing])])
 625
 626 if test -z "${enable_coverage+set}"; then
 627   enable_coverage=no
 628 fi
 629
 630 AC_MSG_RESULT([$enable_coverage])
 631
 632 if test "$enable_coverage" = yes; then
 633   # For coverage testing, we prefer:
 634   #     --enable-static --disable-shared --disable-static-binary
 635   # If the user didn't specify these, we force them here.  If the
 636   # user specified them in opposite phase, give warnings that they
 637   # shouldn't do that, or bomb out.
 638   if test "$user_specified_enable_or_disable_shared" != yes; then
 639     enable_shared=no
 640     AC_MSG_WARN([turning off shared library building due to --enable-coverage])
 641   elif test "$enable_shared" = yes; then
 642     AC_MSG_WARN([])
 643     AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-shared])
 644     AC_MSG_WARN([gcov does not support shared libraries, so only your static libraries will be coverage-testable.])
 645     AC_MSG_WARN([Your cvc4 driver and testing binaries will not be coverage-testable.])
 646     AC_MSG_WARN([])
 647   fi
 648   if test "${enable_static_binary+set}" = set -a "$enable_static_binary" = yes; then
 649     AC_MSG_WARN([])
 650     AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-static-binary])
 651     AC_MSG_WARN([Your cvc4 driver and testing binaries will be fully-statically linked and may not be coverage-testable.])
 652     AC_MSG_WARN([])
 653   fi
 654   if test "$user_specified_enable_or_disable_static" != yes; then
 655     enable_static=yes
 656     AC_MSG_WARN([turning on static library building due to --enable-coverage])
 657   elif test "$enable_static" != yes; then
 658     AC_MSG_ERROR([--enable-coverage and --disable-static are incompatible; gcov only supports static libraries.])
 659   fi
 660
 661   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COVERAGE"
 662   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }--coverage"
 663   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }--coverage"
 664   CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }--coverage"
 665 fi
 666
 667 AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4])
 668
 669 AC_ARG_ENABLE([profiling],
 670   [AS_HELP_STRING([--enable-profiling],
 671      [build with support for gprof profiling])])
 672
 673 if test -z "${enable_profiling+set}"; then
 674   enable_profiling=no
 675 fi
 676
 677 AC_MSG_RESULT([$enable_profiling])
 678
 679 if test "$enable_profiling" = yes; then
 680   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROFILING"
 681   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-pg"
 682   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-pg"
 683   CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }-pg"
 684 fi
 685
 686 # Check to see if this version/architecture of GNU C++ explicitly
 687 # instantiates __gnu_cxx::hash<uint64_t> or not.  Some do, some don't.
 688 # See src/util/hash.h.
 689 AC_MSG_CHECKING([whether __gnu_cxx::hash<uint64_t> is already specialized])
 690 AC_LANG_PUSH([C++])
 691 AC_COMPILE_IFELSE([AC_LANG_SOURCE([
 692 #include <stdint.h>
 693 #include <ext/hash_map>
 694 namespace __gnu_cxx { template<> struct hash<uint64_t> {}; }])],
 695                   [AC_MSG_RESULT([no]); CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_NEED_HASH_UINT64_T"],
 696                   [AC_MSG_RESULT([yes])])
 697 AC_LANG_POP([C++])
 698
 699 # Check for ANTLR runantlr script (defined in config/antlr.m4)
 700 AC_PROG_ANTLR
 701
 702 CVC4_CXX_OPTION([-Wno-conversion-null], [WNO_CONVERSION_NULL])
 703 AC_SUBST([WNO_CONVERSION_NULL])
 704
 705 # Doxygen configuration
 706 AC_ARG_ENABLE([internals-documentation],
 707   [AS_HELP_STRING([--enable-internals-documentation],
 708      [build Doxygen documentation for static and private member functions])])
 709 if test "$enable_internals_documentation" = yes; then
 710   DOXYGEN_EXTRACT_PRIVATE=YES
 711   DOXYGEN_EXTRACT_STATIC=YES
 712 else
 713   DOXYGEN_EXTRACT_PRIVATE=NO
 714   DOXYGEN_EXTRACT_STATIC=NO
 715 fi
 716 AC_SUBST([DOXYGEN_EXTRACT_PRIVATE])
 717 AC_SUBST([DOXYGEN_EXTRACT_STATIC])
 718
 719 DX_MAN_FEATURE(OFF)
 720 DX_PDF_FEATURE(OFF)
 721 DX_PS_FEATURE(OFF)
 722 DX_DOT_FEATURE(OFF)
 723 DX_INIT_DOXYGEN($PACKAGE_NAME, config/doxygen.cfg, $srcdir/doc/doxygen)
 724
 725 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])
 726 AC_ARG_VAR(CXXTEST, [path to CxxTest installation])
 727
 728 AC_SUBST([CXXTEST])
 729
 730 AC_ARG_WITH([cxxtest-dir],
 731   [AS_HELP_STRING([--with-cxxtest-dir=DIR], [path to CxxTest installation])],
 732   [CXXTEST="$withval"])
 733
 734 # In the case of "./configure --with-cxxtest-dir=../cxxtest" (or other
 735 # relative path) and having switched the configure directory (see above),
 736 # search with respect to the top source dir, not the build dir
 737 if test "$CVC4_CONFIGURE_IN_BUILDS" = yes -a -n "$CXXTEST"; then
 738   case "$CXXTEST" in
 739     /*) ;;
 740     *)  CXXTEST="$srcdir/$CXXTEST" ;;
 741   esac
 742 fi
 743
 744 AC_ARG_VAR(LFSC, [path to LFSC proof checker])
 745 AC_ARG_VAR(LFSCARGS, [arguments to pass to LFSC proof checker])
 746 if test -z "$LFSC"; then
 747   AC_CHECK_PROGS(LFSC, lfsc, [], [])
 748 else
 749   AC_CHECK_PROG(LFSC, "$LFSC", [], [])
 750 fi
 751 AM_CONDITIONAL([PROOF_REGRESSIONS], [test -n "$LFSC" -a "$enable_proof" = yes])
 752 if test -z "$LFSC"; then
 753   support_proof_tests='no, lfsc proof checker unavailable'
 754 elif test "$enable_proof" = yes; then
 755   support_proof_tests='yes, proof regression tests enabled'
 756 else
 757   support_proof_tests='no, proof generation disabled for this build'
 758 fi
 759 AC_SUBST([LFSC])
 760 AC_SUBST([LFSCARGS])
 761
 762 CXXTESTGEN=
 763 AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH])
 764 if test -z "$CXXTESTGEN"; then
 765   AC_PATH_PROG(CXXTESTGEN, cxxtestgen.py, [], [$CXXTEST:$PATH])
 766 fi
 767 if test "$enable_unit_testing" = "no"; then
 768   AC_MSG_NOTICE([unit tests disabled by user request.])
 769   CXXTESTGEN=
 770   CXXTEST=
 771 elif test -z "$CXXTESTGEN"; then
 772   AC_MSG_NOTICE([unit tests disabled, neither cxxtestgen.pl nor cxxtestgen.py found.])
 773 elif test -z "$CXXTEST"; then
 774   CXXTEST=`dirname "$CXXTESTGEN"`
 775   AC_MSG_CHECKING([for location of CxxTest headers])
 776   if test -e "$CXXTEST/cxxtest/TestRunner.h"; then
 777     AC_MSG_RESULT([$CXXTEST])
 778   else
 779     if test -e "/usr/include/cxxtest/TestRunner.h"; then
 780       AC_MSG_RESULT([/usr/include])
 781     else
 782       AC_MSG_RESULT([not found])
 783       AC_MSG_WARN([unit tests disabled, CxxTest headers not found.])
 784       CXXTESTGEN=
 785       CXXTEST=
 786     fi
 787   fi
 788 fi
 789
 790 if test "$enable_unit_testing" = yes -a -z "$CXXTESTGEN"; then
 791   AC_MSG_ERROR([--enable-unit-testing given but cxxtest not found.])
 792 fi
 793
 794 AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"])
 795
 796 AC_ARG_VAR(TEST_CPPFLAGS, [CPPFLAGS to use when testing (default=$CPPFLAGS)])
 797 AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)])
 798 AC_ARG_VAR(TEST_LDFLAGS,  [LDFLAGS to use when testing (default=$LDFLAGS)])
 799
 800 AC_ARG_VAR(PERL, [PERL interpreter (used when testing)])
 801
 802 if test -n "$CXXTEST"; then
 803   if test -z "$PERL"; then
 804     AC_CHECK_PROGS(PERL, perl, perl, [])
 805   else
 806     AC_CHECK_PROG(PERL, "$PERL", "$PERL", [])
 807   fi
 808
 809   if test -z "$PERL"; then
 810     AC_MSG_WARN([unit tests disabled, perl not found.])
 811     CXXTESTGEN=
 812     CXXTEST=
 813   fi
 814 fi
 815
 816 AC_ARG_VAR(PYTHON, [PYTHON interpreter (used for building legacy Java library interface)])
 817
 818 if test -z "$PYTHON"; then
 819   AC_CHECK_PROGS(PYTHON, python, python, [])
 820 else
 821   AC_CHECK_PROG(PYTHON, "$PYTHON", "$PYTHON", [])
 822 fi
 823
 824 if test -z "$PYTHON"; then
 825   AC_MSG_WARN([python not found, cannot build libcvc4compat_java (the legacy Java interface).])
 826   CXXTESTGEN=
 827   CXXTEST=
 828 fi
 829
 830 # Checks for libraries.
 831
 832 # Check for libreadline (defined in config/readline.m4)
 833 CVC4_CHECK_FOR_READLINE
 834
 835 AC_SEARCH_LIBS([clock_gettime], [rt],
 836                [AC_DEFINE([HAVE_CLOCK_GETTIME], [1],
 837                           [Defined to 1 if clock_gettime() is supported by the platform.])],
 838                [AC_LIBOBJ([clock_gettime])])
 839
 840 # Check for the presence of CUDD libraries
 841 CVC4_CHECK_CUDD
 842
 843 # Check for antlr C++ runtime (defined in config/antlr.m4)
 844 AC_LIB_ANTLR
 845
 846 # Check for user preferences for language bindings to build, and for
 847 # build support.  The arg list is the default set if unspecified by
 848 # the user (the actual built set is the subset that appears to be
 849 # supported by the build host).
 850 CVC4_CHECK_BINDINGS([c java])dnl csharp perl php python ruby tcl ocaml])
 851
 852 # Checks for header files.
 853 AC_CHECK_HEADERS([getopt.h unistd.h])
 854
 855 # Checks for typedefs, structures, and compiler characteristics.
 856 #AC_HEADER_STDBOOL
 857 # these are bad macros, they clash with system header <stdint.h> !!
 858 #AC_TYPE_UINT16_T
 859 #AC_TYPE_UINT32_T
 860 #AC_TYPE_UINT64_T
 861 #AC_TYPE_SIZE_T
 862
 863 AC_CHECK_DECLS([optreset], [], [], [#include <getopt.h>])
 864
 865 # require boost library
 866 BOOST_REQUIRE()
 867
 868 # look for boost threading library
 869 AC_ARG_WITH([portfolio],
 870     AS_HELP_STRING([--with-portfolio], [build the multithreaded portfolio version of CVC4 (pcvc4)]))
 871 cvc4_save_LDFLAGS="$LDFLAGS"
 872 if test "$enable_static_binary" = yes; then
 873   LDFLAGS="-static $LDFLAGS"
 874 fi
 875 cvc4_has_threads=yes
 876 AC_ARG_ENABLE([thread-support],
 877     AS_HELP_STRING([--disable-thread-support], [do not support multithreaded-capable library]))
 878 if test "$enable_thread_support" = no; then
 879   cvc4_has_threads=no
 880   if test "$with_portfolio" = yes; then
 881     AC_MSG_ERROR([user gave both --with-portfolio and --disable-thread-support, which are contradictory])
 882   fi
 883 else
 884   BOOST_THREADS([], [AC_MSG_WARN([disabling multithreaded support])
 885                    cvc4_has_threads=no])
 886 fi
 887 LDFLAGS="$cvc4_save_LDFLAGS"
 888 if test $cvc4_has_threads = no; then
 889   if test "$enable_thread_support" = yes; then
 890     AC_MSG_ERROR([user gave --enable-thread-support but could not build with threads; maybe boost threading library is missing?])
 891   fi
 892   if test "$with_portfolio" = yes; then
 893     AC_MSG_ERROR([user gave --with-portfolio but could not build with threads; maybe boost threading library is missing?])
 894   fi
 895   with_portfolio=no
 896 fi
 897 if test "$with_portfolio" != yes; then
 898   with_portfolio=no
 899 fi
 900 AM_CONDITIONAL([CVC4_BUILD_PCVC4], [test "$with_portfolio" = yes])
 901 if test "$with_portfolio" = yes; then
 902   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PORTFOLIO"
 903 fi
 904
 905 # Whether to build compatibility library
 906 CVC4_BUILD_LIBCOMPAT=yes
 907 AC_ARG_WITH([compat],
 908     AS_HELP_STRING([--with-compat], [build compatibility library (CVC3 API layer)]),
 909     [if test "$withval" = no; then CVC4_BUILD_LIBCOMPAT=no; fi])
 910 AC_MSG_CHECKING([whether to build compatibility library (CVC3 API layer)])
 911 if test "$CVC4_BUILD_LIBCOMPAT" = yes; then
 912   AC_MSG_RESULT([yes])
 913 else
 914   AC_MSG_RESULT([no, disabled by user])
 915 fi
 916 AC_SUBST(CVC4_BUILD_LIBCOMPAT)
 917 AM_CONDITIONAL([CVC4_BUILD_LIBCOMPAT], [test "$CVC4_BUILD_LIBCOMPAT" = yes])
 918
 919 # Check for availability of TLS support (e.g. __thread storage class)
 920 AC_MSG_CHECKING([whether to use compiler-supported TLS if available])
 921 AC_ARG_ENABLE([tls], AS_HELP_STRING([--disable-tls], [don't use compiler-native TLS]))
 922 if test $cvc4_has_threads = no; then
 923   # We disable TLS entirely by simply telling the build system that
 924   # the empty string is the __thread keyword.
 925   AC_MSG_RESULT([multithreading disabled])
 926   CVC4_TLS_SUPPORTED=1
 927   CVC4_TLS=
 928   CVC4_TLS_explanation='disabled (no multithreading support)'
 929 else
 930   if test -z "${enable_tls+set}" || test "$enable_tls" = "yes"; then
 931     AC_MSG_RESULT([yes])
 932     AX_TLS([CVC4_TLS=$ac_cv_tls], [CVC4_TLS=])
 933   else
 934     AC_MSG_RESULT([no])
 935     CVC4_TLS=
 936   fi
 937   if test -n "$CVC4_TLS"; then
 938     CVC4_TLS_SUPPORTED=1
 939     CVC4_TLS_explanation="$CVC4_TLS"
 940   else
 941     CVC4_TLS_explanation='pthread_getspecific()'
 942     CVC4_TLS_SUPPORTED=0
 943   fi
 944 fi
 945 AC_SUBST([CVC4_TLS])
 946 AC_SUBST([CVC4_TLS_SUPPORTED])
 947
 948 # Whether to compile with google profiling tools
 949 cvc4_use_google_perftools=0
 950 AC_ARG_WITH(
 951     [google_perftools],
 952     AS_HELP_STRING(
 953         [--with-google-perftools],
 954         [use Google Performance Tools]
 955     ),
 956     [if test "$withval" != no; then
 957         cvc4_use_google_perftools=1
 958      fi
 959     ]
 960 )
 961 AC_MSG_CHECKING([whether to link in google perftools libraries])
 962 if test $cvc4_use_google_perftools = 1; then
 963   AC_MSG_RESULT([yes])
 964   AC_CHECK_LIB([tcmalloc], [MallocExtension_GetAllocatedSize], , [AC_MSG_ERROR([cannot link google-perftools test program with -ltcmalloc])], [-lpthread])
 965   AC_CHECK_LIB([profiler], [ProfilerStart], , [AC_MSG_ERROR([cannot link google-perftools test program with -lprofiler])], [-lpthread])
 966 else
 967   AC_MSG_RESULT([no (user didn't request it)])
 968 fi
 969
 970 # Java
 971 AC_ARG_VAR(JAVA, [Java interpreter (used when testing Java interface)])
 972 AC_ARG_VAR(JAVAC, [Java compiler (used when building and testing Java interface)])
 973 AC_ARG_VAR(JAVAH, [Java compiler (used when building and testing Java interface)])
 974 AC_ARG_VAR(JAR, [Jar archiver (used when building Java interface)])
 975 if test "$cvc4_build_java_bindings"; then
 976   dnl AM_PROG_GCJ
 977   if test -z "$JAVA"; then
 978     AC_CHECK_PROGS(JAVA, java, java, [])
 979   else
 980     AC_CHECK_PROG(JAVA, "$JAVA", "$JAVA", [])
 981   fi
 982   if test -z "$JAVAC"; then
 983     AC_CHECK_PROGS(JAVAC, javac gcj, javac, [])
 984     if test "$JAVAC" = gcj; then JAVAC='gcj -C'; fi
 985   else
 986     AC_CHECK_PROG(JAVAC, "$JAVAC", "$JAVAC", [])
 987   fi
 988   if test -z "$JAVAH"; then
 989     AC_CHECK_PROGS(JAVAH, javah gcjh, javah, [])
 990   else
 991     AC_CHECK_PROG(JAVAH, "$JAVAH", "$JAVAH", [])
 992   fi
 993   if test -z "$JAR"; then
 994     AC_CHECK_PROGS(JAR, jar, jar, [])
 995   else
 996     AC_CHECK_PROG(JAR, "$JAR", "$JAR", [])
 997   fi
 998 fi
 999
1000 # Prepare configure output
1001
1002 if test "$enable_shared" = yes; then BUILDING_SHARED=1; else BUILDING_SHARED=0; fi
1003 if test "$enable_static" = yes; then BUILDING_STATIC=1; else BUILDING_STATIC=0; fi
1004 if test "$enable_static_binary" = yes; then STATIC_BINARY=1; else STATIC_BINARY=0; fi
1005 AC_SUBST(BUILDING_SHARED)
1006 AC_SUBST(BUILDING_STATIC)
1007 AC_SUBST(STATIC_BINARY)
1008 AM_CONDITIONAL([STATIC_BINARY], [test "$enable_static_binary" = yes])
1009 AM_CONDITIONAL([COVERAGE_ENABLED], [test "$enable_coverage" = yes])
1010
1011 AM_CONDITIONAL([CVC4_DEBUG], [test "$with_build" = debug])
1012 AM_CONDITIONAL([CVC4_TRACING], [test "$enable_tracing" = yes])
1013
1014 AC_SUBST(CVC4_LIBRARY_VERSION)
1015 AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
1016 AC_SUBST(CVC4_COMPAT_LIBRARY_VERSION)
1017 AC_SUBST(CVC4_BINDINGS_LIBRARY_VERSION)
1018
1019 AC_DEFINE_UNQUOTED(CVC4_MAJOR, ${CVC4_MAJOR}, [Major component of the version of CVC4.])
1020 AC_DEFINE_UNQUOTED(CVC4_MINOR, ${CVC4_MINOR}, [Minor component of the version of CVC4.])
1021 AC_DEFINE_UNQUOTED(CVC4_RELEASE, ${CVC4_RELEASE}, [Release component of the version of CVC4.])
1022 AC_DEFINE_UNQUOTED(CVC4_EXTRAVERSION, ["${CVC4_EXTRAVERSION}"], [Extraversion component of the version of CVC4.])
1023 AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full release string for CVC4.])
1024
1025 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
1026 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
1027 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions"
1028 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
1029
1030 AC_SUBST(FLAG_VISIBILITY_HIDDEN)
1031
1032 # mk_include
1033 #
1034 # When automake scans Makefiles, it complains about non-standard make
1035 # features (including GNU extensions), and breaks GNU Make's
1036 # "if/endif" construct, replacing the "if" with AM_CONDITIONAL if
1037 # constructs.  automake even follows "include" and messes with
1038 # included Makefiles.
1039 #
1040 # CVC4 assumes GNU Make and we want to use GNU Make if/endifs, so we
1041 # have to hide some included Makefiles with GNU extensions.  We do
1042 # this by defining mk_include as an autoconf substitution and then
1043 # using "@mk_include@ other_makefile" in Makefile.am to include
1044 # makefiles with GNU extensions; this hides them from automake.
1045 mk_include=include
1046 AC_SUBST(mk_include)
1047
1048 # CVC4_FALSE
1049 #
1050 # This is used to _always_ comment out rules in automake makefiles, but
1051 # still trigger certain automake behavior; see test/unit/Makefile.am.
1052 AM_CONDITIONAL([CVC4_FALSE], [false])
1053
1054 # set up substitutions for src/util/{rational,integer}.h.in
1055 if test $cvc4_cln_or_gmp = cln; then
1056   CVC4_USE_CLN_IMP=1
1057   CVC4_USE_GMP_IMP=0
1058 else
1059   CVC4_USE_CLN_IMP=0
1060   CVC4_USE_GMP_IMP=1
1061 fi
1062 AC_SUBST(CVC4_USE_CLN_IMP)
1063 AC_SUBST(CVC4_USE_GMP_IMP)
1064
1065 MAN_DATE=`date '+%B %Y'`
1066 AC_SUBST(MAN_DATE)
1067
1068 AC_CONFIG_FILES([
1069   Makefile.builds
1070   Makefile]
1071   m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | grep -v '^src/prop/cryptominisat/' | sort | sed 's,\.am$,,'])
1072 )
1073
1074 if test $cvc4_has_threads = yes; then
1075   support_multithreaded='with boost threading library'
1076   AM_CONDITIONAL([CVC4_HAS_THREADS], [true])
1077   AC_SUBST([CVC4_HAS_THREADS], 1)
1078 else
1079   support_multithreaded='no'
1080   AM_CONDITIONAL([CVC4_HAS_THREADS], [false])
1081   AC_SUBST([CVC4_HAS_THREADS], 0)
1082 fi
1083
1084 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
1085 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
1086 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/tls.h])
1087
1088 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1])
1089 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5])
1090 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3])
1091 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3])
1092 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3])
1093
1094 # AC_CONFIG_SUBDIRS([src/prop/cryptominisat])
1095
1096 AC_OUTPUT
1097
1098 # Final information to the user
1099 licensewarn=
1100
1101 if test "$custom_build_profile" = yes; then
1102   if test "$with_build" = default; then
1103     with_build=custom
1104   else
1105     with_build="$with_build (customized)"
1106   fi
1107 fi
1108
1109 support_unit_tests='cxxtest not found; unit tests not supported'
1110 if test -n "$CXXTEST"; then
1111   support_unit_tests='unit testing infrastructure enabled in build directory'
1112 elif test "$enable_unit_testing" = no; then
1113   support_unit_tests='unit testing disabled by user'
1114 fi
1115
1116 if test "$enable_optimized" = yes; then
1117   optimized="yes, at level $OPTLEVEL"
1118 else
1119   optimized="no"
1120 fi
1121
1122 if test $cvc4_cln_or_gmp = cln; then
1123   mplibrary='cln (GPL)'
1124   licensewarn="${licensewarn}Please note that CVC4 will be built against the Class Library for
1125 Numbers (CLN).  This library is covered under the GPL, so use of this
1126 build of CVC4 will be more restrictive than CVC4's license would
1127 normally suggest.  For full details of CLN and its license, please visit
1128   http://www.ginac.de/CLN/
1129 To build CVC4 with GMP instead (which is covered under the more permissive
1130 LGPL), configure --without-cln.
1131
1132 "
1133   if test $with_portfolio = yes; then
1134     licensewarn="${licensewarn}
1135 WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
1136 WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
1137
1138 Note that CLN is UNSAFE FOR USE in parallel contexts!
1139 This build of CVC4 cannot be used safely as a portfolio solver.
1140 since the result of building with CLN will include numerous race
1141 conditions on the refcounts internal to CLN.
1142
1143 WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
1144 WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
1145
1146 "
1147   fi
1148 else
1149   mplibrary='gmp (LGPL)'
1150 fi
1151
1152 CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="$CVC4_COMPAT_LIBRARY_VERSION"
1153 CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="$CVC4_BINDINGS_LIBRARY_VERSION"
1154 if test "$CVC4_BUILD_LIBCOMPAT" = no; then
1155   CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="N/A"
1156 fi
1157 if test -z "$CVC4_LANGUAGE_BINDINGS"; then
1158   CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="N/A"
1159 fi
1160
1161 cat <<EOF
1162
1163 CVC4 $VERSION
1164
1165 Build profile: $with_build
1166 Build ID     : $build_type
1167 Optimized    : $optimized
1168 Debug symbols: $enable_debug_symbols
1169 Proof        : $enable_proof
1170 Statistics   : $enable_statistics
1171 Replay       : $enable_replay
1172 Assertions   : $enable_assertions
1173 Tracing      : $enable_tracing
1174 Dumping      : $enable_dumping
1175 Muzzle       : $enable_muzzle
1176
1177 Unit tests   : $support_unit_tests
1178 Proof tests  : $support_proof_tests
1179 gcov support : $enable_coverage
1180 gprof support: $enable_profiling
1181 CUDD         : $cvc4cudd
1182 Readline     : $with_readline
1183
1184 Static libs  : $enable_static
1185 Shared libs  : $enable_shared
1186 Static binary: $enable_static_binary
1187 Compat lib   : $CVC4_BUILD_LIBCOMPAT
1188 Bindings     : ${CVC4_LANGUAGE_BINDINGS:-none}
1189
1190 Multithreaded: $support_multithreaded
1191 TLS support  : $CVC4_TLS_explanation
1192 Portfolio    : $with_portfolio
1193
1194 MP library   : $mplibrary
1195
1196 CPPFLAGS     : $CPPFLAGS
1197 CXXFLAGS     : $CXXFLAGS
1198 CFLAGS       : $CFLAGS
1199 LIBS         : $LIBS
1200 LDFLAGS      : $LDFLAGS
1201
1202 libcvc4 version        : $CVC4_LIBRARY_VERSION
1203 libcvc4parser version  : $CVC4_PARSER_LIBRARY_VERSION
1204 libcvc4compat version  : $CVC4_COMPAT_LIBRARY_VERSION_or_nobuild
1205 libcvc4bindings version: $CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild
1206
1207 Install into : $prefix
1208
1209 ${licensewarn}Now just type make, followed by make check or make install, as you like.
1210
1211 EOF
1212
1213 if test -n "$CVC4_INTEGRITY_WARNING"; then
1214   AC_MSG_WARN([])
1215   AC_MSG_WARN($CVC4_INTEGRITY_WARNING)
1216   AC_MSG_WARN([Please run "make check" after building to ensure integrity of the binary and library])
1217   AC_MSG_WARN([])
1218 fi