diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/uf/equality_engine.cpp | 42 | ||||
| -rw-r--r-- | src/theory/uf/equality_engine_types.h | 5 |
2 files changed, 36 insertions, 11 deletions
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 96c8e8b59..2ffb72d91 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -147,9 +147,9 @@ EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): no lookup, setting up" << std::endl; // Mark the normalization to the lookup storeApplicationLookup(funNormalized, funId); - // If an equality, we do some extra reasoning - if (isEquality && d_isConstant[t1ClassId] && d_isConstant[t2ClassId]) { - if (t1ClassId != t2ClassId) { + // If an equality over constants we merge to false + if (isEquality) { + if (d_isConstant[t1ClassId] && d_isConstant[t2ClassId] && t1ClassId != t2ClassId) { Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): got constants" << std::endl; Assert(d_nodes[funId].getKind() == kind::EQUAL); enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null())); @@ -161,6 +161,9 @@ EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId enqueue(MergeCandidate(symmFunId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null())); } } + if (t1ClassId == t2ClassId) { + enqueue(MergeCandidate(funId, d_trueId, MERGED_THROUGH_REFLEXIVITY, TNode::null())); + } } } else { // If it's there, we need to merge these two @@ -343,9 +346,6 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) { // Add equality between terms assertEqualityInternal(eq[0], eq[1], reason); propagate(); - // Add eq = true for dis-equality propagation - assertEqualityInternal(eq, d_true, reason); - propagate(); } else { // If two terms are already dis-equal, don't assert anything if (hasTerm(eq[0]) && hasTerm(eq[1]) && areDisequal(eq[0], eq[1], false)) { @@ -361,8 +361,6 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) { assertEqualityInternal(eq, d_false, reason); propagate(); - assertEqualityInternal(eq[1].eqNode(eq[0]), d_false, reason); - propagate(); if (d_done) { return; @@ -557,8 +555,11 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect } else { // There is no representative, so we can add one, we remove this when backtracking storeApplicationLookup(funNormalized, funId); + // Note: both checks below we don't need to do in the above case as the normalized lookup + // has already been checked for this // Now, if we're constant and it's an equality, check if the other guy is also a constant - if (funNormalized.isEquality) { + if (fun.isEquality) { + // If the equation normalizes to two constants, it's disequal if (d_isConstant[aNormalized] && d_isConstant[bNormalized] && aNormalized != bNormalized) { Assert(d_nodes[funId].getKind() == kind::EQUAL); enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null())); @@ -570,9 +571,14 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect enqueue(MergeCandidate(symmFunId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null())); } } - } + // If the function normalizes to a = a, we merge it with true, we check that its not + // already there so as not to enqueue multiple times when several things get merged + if (aNormalized == bNormalized && getEqualityNode(funId).getFind() != d_trueId) { + enqueue(MergeCandidate(funId, d_trueId, MERGED_THROUGH_REFLEXIVITY, TNode::null())); + } + } } - + // Go to the next one in the use list currentUseId = useNode.getNext(); } @@ -953,6 +959,20 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st Debug("equality") << d_name << "::eq::getExplanation(): adding: " << d_equalityEdges[currentEdge].getReason() << std::endl; equalities.push_back(d_equalityEdges[currentEdge].getReason()); break; + case MERGED_THROUGH_REFLEXIVITY: { + // f(x1, x2) == f(y1, y2) because x1 = y1 and x2 = y2 + Debug("equality") << d_name << "::eq::getExplanation(): due to reflexivity, going deeper" << std::endl; + EqualityNodeId eqId = currentNode == d_trueId ? edgeNode : currentNode; + const FunctionApplication& eq = d_applications[eqId].original; + Assert(eq.isEquality, "Must be an equality"); + + // Explain why a = b constant + Debug("equality") << push; + getExplanation(eq.a, eq.b, equalities); + Debug("equality") << pop; + + break; + } case MERGED_THROUGH_CONSTANTS: { // (a = b) == false because a and b are different constants Debug("equality") << d_name << "::eq::getExplanation(): due to constants, going deeper" << std::endl; diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h index 056ee0b84..591b15bf4 100644 --- a/src/theory/uf/equality_engine_types.h +++ b/src/theory/uf/equality_engine_types.h @@ -65,6 +65,8 @@ enum MergeReasonType { MERGED_THROUGH_CONGRUENCE, /** Terms were merged due to application of pure equality */ MERGED_THROUGH_EQUALITY, + /** Equality was merged to true, due to both sides of equality being in the same class */ + MERGED_THROUGH_REFLEXIVITY, /** Equality was merged to false, due to both sides of equality being a constant */ MERGED_THROUGH_CONSTANTS, }; @@ -77,6 +79,9 @@ inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) { case MERGED_THROUGH_EQUALITY: out << "pure equality"; break; + case MERGED_THROUGH_REFLEXIVITY: + out << "reflexivity"; + break; case MERGED_THROUGH_CONSTANTS: out << "constants disequal"; break; |