From 12ad4cf2de936acbf8c21117804c69b2deaa7272 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 15 Mar 2010 21:10:29 +0000 Subject: [PATCH] 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) --- configure.ac | 30 ++++++++++++++++++++++-------- src/expr/Makefile.am | 2 +- src/theory/Makefile.am | 2 +- src/theory/theory_engine.h | 11 ++++++----- src/theory/uf/theory_uf.cpp | 3 ++- src/util/exception.h | 1 - src/util/output.h | 18 ++++++++---------- 7 files changed, 40 insertions(+), 27 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 < conflict" << std::endl; - ok = false; } - return ok; + return d_theoryOut.d_conflictNode.get().isNull(); } /** diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 6d949d6de..ee3cb4734 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -310,7 +310,8 @@ void TheoryUF::check(Effort level){ if(sameCongruenceClass(left, right)){ Node remakeNeq = (*diseqIter).notNode(); Node conflict = constructConflict(remakeNeq); - d_out->conflict(conflict, true); + d_out->conflict(conflict, false); + return; } } } diff --git a/src/util/exception.h b/src/util/exception.h index 5449d67f7..ff88b5d81 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -17,7 +17,6 @@ #define __CVC4__EXCEPTION_H #include -#include #include "cvc4_config.h" namespace CVC4 { diff --git a/src/util/output.h b/src/util/output.h index d0db064f0..5c265e699 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -24,8 +24,6 @@ #include #include -#include "util/exception.h" - namespace CVC4 { /** @@ -60,25 +58,25 @@ public: DebugC(std::ostream* os) : d_os(os) {} void operator()(const char* tag, const char* s) { - if(d_tags.find(std::string(tag)) != d_tags.end()) { + if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) { *d_os << s; } } void operator()(const char* tag, const std::string& s) { - if(d_tags.find(std::string(tag)) != d_tags.end()) { + if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) { *d_os << s; } } void operator()(const std::string& tag, const char* s) { - if(d_tags.find(tag) != d_tags.end()) { + if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { *d_os << s; } } void operator()(const std::string& tag, const std::string& s) { - if(d_tags.find(tag) != d_tags.end()) { + if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { *d_os << s; } } @@ -87,14 +85,14 @@ public: void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))); std::ostream& operator()(const char* tag) { - if(d_tags.find(std::string(tag)) != d_tags.end()) { + if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) { return *d_os; } else { return null_os; } } std::ostream& operator()(std::string tag) { - if(d_tags.find(tag) != d_tags.end()) { + if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { return *d_os; } else { return null_os; @@ -223,7 +221,7 @@ public: void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))); std::ostream& operator()(const char* tag) { - if(d_tags.find(tag) != d_tags.end()) { + if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { return *d_os; } else { return null_os; @@ -231,7 +229,7 @@ public: } std::ostream& operator()(std::string tag) { - if(d_tags.find(tag) != d_tags.end()) { + if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { return *d_os; } else { return null_os; -- 2.30.2