diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-27 16:59:01 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-27 16:59:01 +0000 |
commit | 21f9e53792ba5f94594fccb7bef880aa77b266cb (patch) | |
tree | 730a0f6fe26c8eb339844b5bb64ee666550334fa /src | |
parent | b390cfa8f095048472cb3dd0b9ccc22fbd51f411 (diff) |
some reordering to keep invariants
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 30 |
1 files changed, 19 insertions, 11 deletions
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 72966d0b3..5093e5a7b 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -414,17 +414,6 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect trigger.classId = class1Id; // If they became the same, call the trigger if (otherTrigger.classId == class1Id) { - const TriggerInfo& triggerInfo = d_equalityTriggersOriginal[currentTrigger]; - if (triggerInfo.trigger.getKind() == kind::EQUAL && !triggerInfo.polarity) { - TNode equality = triggerInfo.trigger; - EqualityNodeId original = getNodeId(equality); - d_deducedDisequalityReasons.push_back(EqualityPair(original, d_falseId)); - if (!storePropagatedDisequality(equality[0], equality[1], 1)) { - // Go to the next trigger - currentTrigger = trigger.nextTrigger; - continue; - } - } // Id of the real trigger is half the internal one triggersFired.push_back(currentTrigger); } @@ -492,6 +481,25 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // Now merge the lists class1.merge<true>(class2); + + // Go through the triggers and store the dis-equalities + unsigned i = 0, j = 0; + for (; i < triggersFired.size();) { + const TriggerInfo& triggerInfo = d_equalityTriggersOriginal[triggersFired[i]]; + if (triggerInfo.trigger.getKind() == kind::EQUAL && !triggerInfo.polarity) { + TNode equality = triggerInfo.trigger; + EqualityNodeId original = getNodeId(equality); + d_deducedDisequalityReasons.push_back(EqualityPair(original, d_falseId)); + if (!storePropagatedDisequality(equality[0], equality[1], 1)) { + // Already notified, go to the next trigger + ++ i; + continue; + } + } + // Copy + triggersFired[j++] = triggersFired[i++]; + } + triggersFired.resize(j); // Notify the trigger term merges TriggerTermSetRef class2triggerRef = d_nodeIndividualTrigger[class2Id]; |