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)

diff --git a/configure.ac b/configure.ac
index 8cabfe98b0f88922636048af2e3d8e8904b0566a..f540cab11f5fb6ec6aabed6c7084d31062fe5e5d 100644 (file)
--- 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 6d041814f74d9a948bf713111b3c0766659954d7..0b6dbed4b82251431092fb340eb31ca2914c1385 100644 (file)
--- 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 43ed0574a175603da6b3557590100a635cc83104..d387cf7a9c59124674fe9013a32ce2ca49aec085 100644 (file)
--- 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 cb0158dfe5cc1f839dabe9f70f528a302fbe4cb1..15c80434fa4c33d4a461325aff4af66c39b71a0b 100644 (file)
--- 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 6d949d6de2a66197a72be483805646eea54f0f04..ee3cb4734805c43ad8e8ad3c7f040ad92997304e 100644 (file)
--- 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 5449d67f7ee1b6e375a2d7415acab0520720a12c..ff88b5d81c8ad676acb48a2b70d1eef20680348b 100644 (file)
--- 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 d0db064f0b06e5dbe141cf3222a461aa30436b31..5c265e699251f3330044634c6ec9caf4ff8d8e7f 100644 (file)
--- 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;