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)

3 files changed, 9 insertions, 7 deletions

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;
       }
     }
   }