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 | |
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)
-rw-r--r-- | configure.ac | 30 | ||||
-rw-r--r-- | src/expr/Makefile.am | 2 | ||||
-rw-r--r-- | src/theory/Makefile.am | 2 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 11 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 3 | ||||
-rw-r--r-- | src/util/exception.h | 1 | ||||
-rw-r--r-- | 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 <<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 diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 6d041814f..0b6dbed4b 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -33,7 +33,7 @@ EXTRA_DIST = \ kind_epilogue.h @srcdir@/kind.h: mkkind kind_prologue.h kind_middle.h kind_epilogue.h builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds - chmod +x @srcdir@/mkkind + $(AM_V_at)chmod +x @srcdir@/mkkind $(AM_V_GEN)(@srcdir@/mkkind \ @srcdir@/kind_prologue.h \ @srcdir@/kind_middle.h \ diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 43ed0574a..d387cf7a9 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -26,7 +26,7 @@ EXTRA_DIST = \ theoryof_table_epilogue.h @srcdir@/theoryof_table.h: @srcdir@/mktheoryof theoryof_table_prologue.h theoryof_table_middle.h theoryof_table_epilogue.h @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds - chmod +x @srcdir@/mktheoryof + $(AM_V_at)chmod +x @srcdir@/mktheoryof $(AM_V_GEN)(@srcdir@/mktheoryof \ @srcdir@/theoryof_table_prologue.h \ @srcdir@/theoryof_table_middle.h \ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index cb0158dfe..15c80434f 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -69,10 +69,12 @@ class TheoryEngine { d_conflictNode(context) { } - void conflict(TNode conflictNode, bool) throw(theory::Interrupted) { + void conflict(TNode conflictNode, bool safe) throw(theory::Interrupted) { Debug("theory") << "EngineOutputChannel::conflict(" << conflictNode << ")" << std::endl; d_conflictNode = conflictNode; - throw theory::Interrupted(); + if(safe) { + throw theory::Interrupted(); + } } void propagate(TNode, bool) throw(theory::Interrupted) { @@ -255,7 +257,7 @@ public: * @param effort the effort level to use */ inline bool check(theory::Theory::Effort effort) { - bool ok = true; + d_theoryOut.d_conflictNode = Node::null(); try { //d_bool.check(effort); d_uf.check(effort); @@ -264,9 +266,8 @@ public: //d_bv.check(effort); } catch(const theory::Interrupted&) { Debug("theory") << "TheoryEngine::check() => 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 <string> -#include <iostream> #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 <cstdarg> #include <set> -#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; |