diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-03-15 21:10:29 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-03-15 21:10:29 +0000 |
| commit | 12ad4cf2de936acbf8c21117804c69b2deaa7272 (patch) | |
| tree | 39280aebed0a299b080512d1c26d1adad827fcc7 /configure.ac | |
| parent | bb21cdc3a551fa46b5e77345bb5cbcb55cba2fa6 (diff) | |
This checkin resolves bug #57.
* CVC4::theory::Interrupted no longer derives CVC4::Exception.
* Interrupted is only thrown if "safe" parameter is TRUE !
* UF returns one conflict (instead of waiting for Interrupted to be thrown).
* Minor build system work (quieter builds if V=0, better handling of build
profiles in configure)
Diffstat (limited to 'configure.ac')
| -rw-r--r-- | configure.ac | 30 |
1 files changed, 22 insertions, 8 deletions
diff --git a/configure.ac b/configure.ac index 8cabfe98b..f540cab11 100644 --- a/configure.ac +++ b/configure.ac @@ -159,11 +159,15 @@ fi # Unpack standard build types. Any particular options can be overriden with # --enable/disable-X options +if test -z "${OPTLEVEL+set}"; then OPTLEVEL=3; fi +# our defaults for CXXFLAGS are better than autoconf's +if test -z "${CXXFLAGS+set}"; then CXXFLAGS=; fi case "$with_build" in production) # highly optimized, no assertions, no tracing CVC4CPPFLAGS= - CVC4CXXFLAGS=-O3 + CVC4CXXFLAGS= CVC4LDFLAGS= + if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=3 ; fi if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi @@ -172,7 +176,7 @@ case "$with_build" in ;; debug) # unoptimized, debug symbols, assertions, tracing CVC4CPPFLAGS=-DCVC4_DEBUG - CVC4CXXFLAGS='-O0 -fno-inline -ggdb3' + CVC4CXXFLAGS='-fno-inline' CVC4LDFLAGS= if test -z "${enable_optimized+set}" ; then enable_optimized=no ; fi if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi @@ -182,9 +186,10 @@ case "$with_build" in ;; default) # moderately optimized, assertions, tracing CVC4CPPFLAGS= - CVC4CXXFLAGS=-O2 + CVC4CXXFLAGS= CVC4LDFLAGS= - if test -z "${enable_optimized+set}" ; then enable_optimized=no ; fi + if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=2 ; fi + if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi @@ -192,9 +197,10 @@ case "$with_build" in ;; competition) # maximally optimized, no assertions, no tracing, muzzled CVC4CPPFLAGS= - CVC4CXXFLAGS='-O9 -funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs' + CVC4CXXFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs' CVC4LDFLAGS= - if test -z "${enable_optimized+set}" ; then enable_optimized=no ; fi + if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=9 ; fi + if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no ; fi if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi @@ -232,7 +238,9 @@ fi AC_MSG_RESULT([$enable_optimized]) if test "$enable_optimized" = yes; then - CVC4CXXFLAGS="$CVC4CXXFLAGS -O3" + CVC4CXXFLAGS="$CVC4CXXFLAGS -O$OPTLEVEL" +else + CVC4CXXFLAGS="$CVC4CXXFLAGS -O0" fi AC_MSG_CHECKING([whether to include debugging symbols in libcvc4]) @@ -497,13 +505,19 @@ if test -n "$CXXTEST"; then support_unit_tests='unit testing infrastructure enabled in build directory' fi +if test "$enable_optimized" = yes; then + optimized="yes, at level $OPTLEVEL" +else + optimized="no" +fi + cat <<EOF CVC4 $VERSION Build profile: $with_build Build ID : $build_type -Optimized : $enable_optimized +Optimized : $optimized Debug symbols: $enable_debug_symbols Assertions : $enable_assertions Tracing : $enable_tracing |