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)

6 files changed, 18 insertions, 19 deletions

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;