From 6e59b60947283d864877c2c2dc883e878913a2d8 Mon Sep 17 00:00:00 2001
From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Fri, 24 Sep 2010 22:38:21 +0000
Subject: equality triggers for the equality engine fixed order of destruction
 in smt_engine

---
 src/theory/bv/theory_bv.cpp | 56 +++++++++++++++++++++++++++++----------------
 1 file changed, 36 insertions(+), 20 deletions(-)

(limited to 'src/theory/bv/theory_bv.cpp')

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index e08c19dbd..f957c4f49 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -14,6 +14,9 @@ void TheoryBV::preRegisterTerm(TNode node) {
   if (node.getKind() == kind::EQUAL) {
     d_eqEngine.addTerm(node[0]);
     d_eqEngine.addTerm(node[1]);
+    size_t triggerId = d_eqEngine.addTrigger(node[0], node[1]);
+    Assert(triggerId == d_triggers.size());
+    d_triggers.push_back(node);
   }
 }
 
@@ -82,24 +85,26 @@ void TheoryBV::check(Effort e) {
 
     // Get the assertion
     TNode assertion = get();
+    d_assertions.insert(assertion);
 
     Debug("bitvector") << "TheoryBV::check(" << e << "): asserting: " << assertion << std::endl;
 
     // Do the right stuff
     switch (assertion.getKind()) {
-    case kind::EQUAL:
-      d_eqEngine.addEquality(assertion[0], assertion[1]);
+    case kind::EQUAL: {
+      bool ok = d_eqEngine.addEquality(assertion[0], assertion[1]);
+      if (!ok) return;
       break;
+    }
     case kind::NOT: {
+      // We need to check this as the equality trigger might have been true when we made it
       TNode equality = assertion[0];
       if (d_eqEngine.areEqual(equality[0], equality[1])) {
         vector<TNode> assertions;
         d_eqEngine.getExplanation(equality[0], equality[1], assertions);
-        // We can assume that the explanation is bigger than one node
         assertions.push_back(assertion);
-        d_out->conflict(mkAnd(assertions));        
-      } else {
-        d_disequalities.push_back(assertion);
+        d_out->conflict(mkAnd(assertions));
+        return;
       }
       break;
     }
@@ -107,21 +112,32 @@ void TheoryBV::check(Effort e) {
       Unhandled();
     }
   }
+}
 
-  // In full effort go back and check the disequalities
-  if (true) {
-    Debug("bitvector") << "TheoryBV::check(" << e << "): checking disequalities" << std::endl;
+bool TheoryBV::triggerEquality(size_t triggerId) {
+  Debug("bitvector") << "TheoryBV::triggerEquality(" << triggerId << ")" << std::endl;
+  Assert(triggerId < d_triggers.size());
+  Debug("bitvector") << "TheoryBV::triggerEquality(" << triggerId << "): " << d_triggers[triggerId] << std::endl;
 
-    for (unsigned i = 0; i < d_disequalities.size(); ++ i) {
-      TNode assertion = d_disequalities[i];
-      TNode equality = assertion[0];
-      if (d_eqEngine.areEqual(equality[0], equality[1])) {
-        vector<TNode> assertions;
-        d_eqEngine.getExplanation(equality[0], equality[1], assertions);
-        assertions.push_back(assertion);
-        // We can assume that the explanation is bigger than one node
-        d_out->conflict(mkAnd(assertions));
-      }
-    }
+  TNode equality = d_triggers[triggerId];
+
+  // If we have just asserted this equality ignore it
+  if (d_assertions.contains(equality)) return true;
+
+  // If we have a negation asserted, we have a confict
+  if (d_assertions.contains(equality.notNode())) {
+
+    vector<TNode> assertions;
+    d_eqEngine.getExplanation(equality[0], equality[1], assertions);
+    assertions.push_back(equality.notNode());
+    d_out->conflict(mkAnd(assertions));
+
+    return false;
   }
+
+  // Otherwise we propagate this equality
+  d_out->propagate(equality);
+
+  return true;
 }
+
-- 
cgit v1.2.3