diff options
| author | guykatzz <katz911@gmail.com> | 2016-02-05 16:10:36 -0800 |
|---|---|---|
| committer | guykatzz <katz911@gmail.com> | 2016-02-05 16:10:36 -0800 |
| commit | 3c4c4420ebae4d27d53084453591363942eb4d2e (patch) | |
| tree | ade8c2bc56a3900911c987d8708be9db675b9446 /src | |
| parent | dab7f460511bf0f36c286eaf456a4be11f4fea4b (diff) | |
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.
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/uf/equality_engine.cpp | 8 |
1 files changed, 2 insertions, 6 deletions
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; |