Changing the way the equality engine explains disequalities.

The explanation for a != b is now:
1. a == find(a)
2. ( find(a) == find(b) ) == false
3. find(b) == b

This simplifies the creation of transitivity proofs for disequalities.

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 8df323992115f36d1ca448476ca8e3faf780f600..0ac5096d29d1b8449621fda38d30177e2abdad2c 100644 (file)
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -1567,10 +1567,8 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
       if (ensureProof) {
         const FunctionApplication original = d_applications[find->second].original;
         nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t1Id, original.a));
-        nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t2Id, original.b));
-        nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(original.a, t1ClassId));
-        nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(original.b, t2ClassId));
         nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(find->second, d_falseId));
+        nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t2Id, original.b));
         nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
       }
       return true;
@@ -1585,10 +1583,8 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
       if (ensureProof) {
         const FunctionApplication original = d_applications[find->second].original;
         nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t2Id, original.a));
-        nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t1Id, original.b));
-        nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(original.a, t2ClassId));
-        nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(original.b, t1ClassId));
         nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(find->second, d_falseId));
+        nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t1Id, original.b));
         nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
       }
       return true;