From c871e203705d3e191b8c8028a3f22bca6adb0d16 Mon Sep 17 00:00:00 2001 From: Dejan Jovanovic Date: Tue, 7 Apr 2015 23:48:57 -0700 Subject: [PATCH] Removing the reference to THEORY_BOOL from the equality engine. This theory id was used as an internal marker in a set of theories tagging reasons of a propagated disequalities. Replaced it with THEORY_LAST which is not completely kosher but is safe in the context being used. --- src/theory/uf/equality_engine.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 42736a59b..cd6459a3c 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -1415,11 +1415,14 @@ void EqualityEngine::propagate() { TNode rhs = equality[1]; EqualityNodeId lhsId = getNodeId(lhs); EqualityNodeId rhsId = getNodeId(rhs); - if (!hasPropagatedDisequality(THEORY_BOOL, lhsId, rhsId)) { + // We use the THEORY_LAST as a marker for "marked as propagated, reasons stored". + // This tag is added to an internal theories set that is only inserted in, so this is + // safe. Had we iterated over, or done other set operations this might be dangerous. + if (!hasPropagatedDisequality(THEORY_LAST, lhsId, rhsId)) { if (!hasPropagatedDisequality(lhsId, rhsId)) { d_deducedDisequalityReasons.push_back(EqualityPair(original, d_falseId)); } - storePropagatedDisequality(THEORY_BOOL, lhsId, rhsId); + storePropagatedDisequality(THEORY_LAST, lhsId, rhsId); if (!d_notify.eqNotifyTriggerEquality(triggerInfo.trigger, triggerInfo.polarity)) { d_done = true; } @@ -1551,7 +1554,6 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) Debug("equality::trigger") << d_name << "::eq::addTriggerTerm(" << t << ", " << tag << ")" << std::endl; Assert(tag != THEORY_LAST); - Assert(tag != THEORY_BOOL, "This one is used internally, bummer"); if (d_done) { return; -- 2.30.2