adding simple-uf to the regressions, and the code that apparently solves it

1 files changed, 33 insertions, 9 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 5453aab93..87a78d920 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -54,14 +54,26 @@ class TheoryEngine {
    * back to a TheoryEngine.
    */
   class EngineOutputChannel : public theory::OutputChannel {
+
+    friend class TheoryEngine;
+
     TheoryEngine* d_engine;
+    context::Context* d_context;
+    context::CDO<Node> d_conflictNode;
+
   public:
-    void setEngine(TheoryEngine& engine) throw() {
-      d_engine = &engine;
+
+    EngineOutputChannel(TheoryEngine* engine, context::Context* context)
+    : d_engine(engine),
+      d_context(context),
+      d_conflictNode(context)
+    {
     }
 
     void conflict(TNode conflictNode, bool) throw(theory::Interrupted) {
-      Debug("theory") << "conflict(" << conflictNode << ")" << std::endl;
+      Debug("theory") << "EngineOutputChannel::conflict(" << conflictNode << ")" << std::endl;
+      d_conflictNode = conflictNode;
+      throw theory::Interrupted();
     }
 
     void propagate(TNode, bool) throw(theory::Interrupted) {
@@ -88,13 +100,13 @@ public:
    */
   TheoryEngine(SmtEngine* smt, context::Context* ctxt) :
     d_smt(smt),
-    d_theoryOut(),
+    d_theoryOut(this, ctxt),
     d_bool(ctxt, d_theoryOut),
     d_uf(ctxt, d_theoryOut),
     d_arith(ctxt, d_theoryOut),
     d_arrays(ctxt, d_theoryOut),
-    d_bv(ctxt, d_theoryOut) {
-    d_theoryOut.setEngine(*this);
+    d_bv(ctxt, d_theoryOut)
+  {
     theoryOfTable.registerTheory(&d_bool);
     theoryOfTable.registerTheory(&d_uf);
     theoryOfTable.registerTheory(&d_arith);
@@ -109,7 +121,8 @@ public:
    * of built-in type.
    */
   theory::Theory* theoryOf(const TNode& node) {
-    return theoryOfTable[node];
+    if (node.getKind() == kind::EQUAL) return &d_uf;
+    else return NULL;
   }
 
   /**
@@ -118,12 +131,23 @@ public:
    */
   inline void assertFact(const TNode& node) {
     Debug("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl;
-    theory::Theory* theory = theoryOf(node);
+    theory::Theory* theory = node.getKind() == kind::NOT ? theoryOf(node[0]) : theoryOf(node);
     if (theory != NULL) theory->assertFact(node);
   }
 
   inline void check(theory::Theory::Effort effort) {
-    d_uf.check(effort);
+    try {
+      d_uf.check(effort);
+    } catch (const theory::Interrupted&) {
+      Debug("theory") << "TheoryEngine::check() => conflict" << std::endl;
+    }
+  }
+
+  /**
+   * Returns the last conflict (if any).
+   */
+  inline Node getConflict() {
+    return d_theoryOut.d_conflictNode;
   }
 
 };/* class TheoryEngine */