Partial fix in arithmetic for propagating shared terms. This partially resolves bug 289. Adds failing tests to regress1.

1 files changed, 36 insertions, 2 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 53559d949..dfd82b960 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -889,6 +889,24 @@ Node TheoryArith::explain(TNode n) {
   }
 }
 
+void flattenAnd(Node n, std::vector<TNode>& out){
+  Assert(n.getKind() == kind::AND);
+  for(Node::iterator i=n.begin(), i_end=n.end(); i != i_end; ++i){
+    Node curr = *i;
+    if(curr.getKind() == kind::AND){
+      flattenAnd(curr, out);
+    }else{
+      out.push_back(curr);
+    }
+  }
+}
+
+Node flattenAnd(Node n){
+  std::vector<TNode> out;
+  flattenAnd(n, out);
+  return NodeManager::currentNM()->mkNode(kind::AND, out);
+}
+
 void TheoryArith::propagate(Effort e) {
   if(quickCheckOrMore(e)){
     bool propagated = false;
@@ -910,8 +928,24 @@ void TheoryArith::propagate(Effort e) {
       if(flag) {
         //Currently if the flag is set this came from an equality detected by the
         //equality engine in the the difference manager.
-        d_out->propagate(toProp);
-        propagated = true;
+        if(toProp.getKind() == kind::EQUAL){
+          Node normalized = Rewriter::rewrite(toProp);
+          Node notNormalized = normalized.notNode();
+
+          if(d_diseq.find(notNormalized) == d_diseq.end()){
+            d_out->propagate(toProp);
+            propagated = true;
+          }else{
+            Node exp = d_differenceManager.explain(toProp);
+            Node lp = flattenAnd(exp.andNode(exp));
+            d_out->conflict(exp);
+            propagated = true;
+            break;
+          }
+        }else{
+          d_out->propagate(toProp);
+          propagated = true;
+        }
       }else if(inContextAtom(atom)){
         Node satValue = d_valuation.getSatValue(toProp);
         AlwaysAssert(satValue.isNull());