Simplify trigger notifications in equality engine (#4921)

This is further work towards a centralized approach for equality engines.

This PR merges the eqNotifyTriggerEquality callback with the eqNotifyTriggerPredicate callback, and adds assertions that capture the current behavior. It furthermore makes addTriggerEquality private in equality engine and invoked as a special case of addTriggerPredicate. Note this PR does not impact the internal implementation of these methods in equality engine, which indeed is different.

There are two reasons to merge these callbacks:
(1) all theories implement exactly the same method for the two callbacks, whenever they implement both. It would be trivial to do something different (by case splitting on the kind of predicate that is being notified), and moreover it is not recommended they do anything other than immediately propagate the predicate (regardless of whether it is an equality).
(2) It leads to some confusion with eqNotifyTriggerTermEquality, which is invoked when two trigger terms are merged.

5 files changed, 29 insertions, 44 deletions

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 643029b05..5ccda1dc2 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -1704,11 +1704,11 @@ void EqualityEngine::addTriggerEquality(TNode eq) {
 
   // If they are equal or disequal already, no need for the trigger
   if (areEqual(eq[0], eq[1])) {
-    d_notify.eqNotifyTriggerEquality(eq, true);
+    d_notify.eqNotifyTriggerPredicate(eq, true);
     skipTrigger = true;
   }
   if (areDisequal(eq[0], eq[1], true)) {
-    d_notify.eqNotifyTriggerEquality(eq, false);
+    d_notify.eqNotifyTriggerPredicate(eq, false);
     skipTrigger = true;
   }
 
@@ -1726,8 +1726,12 @@ void EqualityEngine::addTriggerEquality(TNode eq) {
 }
 
 void EqualityEngine::addTriggerPredicate(TNode predicate) {
-  Assert(predicate.getKind() != kind::NOT
-         && predicate.getKind() != kind::EQUAL);
+  Assert(predicate.getKind() != kind::NOT);
+  if (predicate.getKind() == kind::EQUAL)
+  {
+    // equality is handled separately
+    return addTriggerEquality(predicate);
+  }
   Assert(d_congruenceKinds.tst(predicate.getKind()))
       << "No point in adding non-congruence predicates";
 
@@ -1997,8 +2001,8 @@ void EqualityEngine::propagate() {
                 d_deducedDisequalityReasons.push_back(EqualityPair(original, d_falseId));
               }
               storePropagatedDisequality(THEORY_LAST, lhsId, rhsId);
-              if (!d_notify.eqNotifyTriggerEquality(triggerInfo.d_trigger,
-                                                    triggerInfo.d_polarity))
+              if (!d_notify.eqNotifyTriggerPredicate(triggerInfo.d_trigger,
+                                                     triggerInfo.d_polarity))
               {
                 d_done = true;
               }
@@ -2007,8 +2011,8 @@ void EqualityEngine::propagate() {
           else
           {
             // Equalities are simple
-            if (!d_notify.eqNotifyTriggerEquality(triggerInfo.d_trigger,
-                                                  triggerInfo.d_polarity))
+            if (!d_notify.eqNotifyTriggerPredicate(triggerInfo.d_trigger,
+                                                   triggerInfo.d_polarity))
             {
               d_done = true;
             }
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 9d1fc6165..c3041dfe7 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -658,9 +658,15 @@ private:
 
   /** The internal addTerm */
   void addTermInternal(TNode t, bool isOperator = false);
+  /**
+   * Adds a notify trigger for equality. When equality becomes true
+   * eqNotifyTriggerPredicate will be called with value = true, and when
+   * equality becomes false eqNotifyTriggerPredicate will be called with value =
+   * false.
+   */
+  void addTriggerEquality(TNode equality);
 
-public:
-
+ public:
   /**
    * Adds a term to the term database.
    */
@@ -787,16 +793,13 @@ public:
   TNode getTriggerTermRepresentative(TNode t, TheoryId theoryTag) const;
 
   /**
-   * Adds a notify trigger for equality. When equality becomes true eqNotifyTriggerEquality
-   * will be called with value = true, and when equality becomes false eqNotifyTriggerEquality
-   * will be called with value = false.
-   */
-  void addTriggerEquality(TNode equality);
-
-  /**
-   * Adds a notify trigger for the predicate p. When the predicate becomes true
-   * eqNotifyTriggerPredicate will be called with value = true, and when equality becomes false
+   * Adds a notify trigger for the predicate p, where notice that p can be
+   * an equality. When the predicate becomes true, eqNotifyTriggerPredicate will
+   * be called with value = true, and when predicate becomes false
    * eqNotifyTriggerPredicate will be called with value = false.
+   *
+   * Notice that if p is an equality, then we use a separate method for
+   * determining when to call eqNotifyTriggerPredicate.
    */
   void addTriggerPredicate(TNode predicate);
 
diff --git a/src/theory/uf/equality_engine_notify.h b/src/theory/uf/equality_engine_notify.h
index f63a887ef..1467cacf3 100644
--- a/src/theory/uf/equality_engine_notify.h
+++ b/src/theory/uf/equality_engine_notify.h
@@ -33,15 +33,8 @@ class EqualityEngineNotify
   virtual ~EqualityEngineNotify(){};
 
   /**
-   * Notifies about a trigger equality that became true or false.
-   *
-   * @param equality the equality that became true or false
-   * @param value the value of the equality
-   */
-  virtual bool eqNotifyTriggerEquality(TNode equality, bool value) = 0;
-
-  /**
-   * Notifies about a trigger predicate that became true or false.
+   * Notifies about a trigger predicate that became true or false. Notice that
+   * predicate can be an equality.
    *
    * @param predicate the trigger predicate that became true or false
    * @param value the value of the predicate
@@ -103,10 +96,6 @@ class EqualityEngineNotify
 class EqualityEngineNotifyNone : public EqualityEngineNotify
 {
  public:
-  bool eqNotifyTriggerEquality(TNode equality, bool value) override
-  {
-    return true;
-  }
   bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
   {
     return true;
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 4f9c3bed5..7bca9da74 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -246,7 +246,7 @@ void TheoryUF::preRegisterTerm(TNode node) {
   switch (node.getKind()) {
   case kind::EQUAL:
     // Add the trigger for equality
-    d_equalityEngine->addTriggerEquality(node);
+    d_equalityEngine->addTriggerPredicate(node);
     break;
   case kind::APPLY_UF:
   case kind::HO_APPLY:
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 001c947e9..414a2dd6a 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -45,17 +45,6 @@ public:
   public:
     NotifyClass(TheoryUF& uf): d_uf(uf) {}
 
-    bool eqNotifyTriggerEquality(TNode equality, bool value) override
-    {
-      Debug("uf") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
-      if (value) {
-        return d_uf.propagate(equality);
-      } else {
-        // We use only literal triggers so taking not is safe
-        return d_uf.propagate(equality.notNode());
-      }
-    }
-
     bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
     {
       Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;