From: guykatzz <katz911@gmail.com>
Date: Sat, 6 Feb 2016 00:10:36 +0000 (-0800)
Subject: Changing the way the equality engine explains disequalities.
X-Git-Tag: cvc5-1.0.0~6085
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3c4c4420ebae4d27d53084453591363942eb4d2e;p=cvc5.git

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 8df323992..0ac5096d2 100644
--- 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;