From: Dejan Jovanovic <dejan.jovanovic@gmail.com>
Date: Wed, 8 Apr 2015 06:48:57 +0000 (-0700)
Subject: Removing the reference to THEORY_BOOL from the equality engine. This theory
X-Git-Tag: cvc5-1.0.0~6364
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c871e203705d3e191b8c8028a3f22bca6adb0d16;p=cvc5.git

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.
---

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;