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.

2 files changed, 2 insertions, 13 deletions

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 48ec81a1e..7e2b8a8b0 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -105,7 +105,7 @@ void CoreSolver::enableSlicer() {
 void CoreSolver::preRegister(TNode node) {
   d_preregisterCalled = true;
   if (node.getKind() == kind::EQUAL) {
-    d_equalityEngine->addTriggerEquality(node);
+    d_equalityEngine->addTriggerPredicate(node);
     if (d_useSlicer)
     {
       d_slicer->processEquality(node);
@@ -383,22 +383,12 @@ bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
   return true;
 }
 
-bool CoreSolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) {
-  Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
-  if (value) {
-    return d_solver.storePropagation(equality);
-  } else {
-    return d_solver.storePropagation(equality.notNode());
-  }
-}
-
 bool CoreSolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) {
   Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl;
   if (value) {
     return d_solver.storePropagation(predicate);
-  } else {
-    return d_solver.storePropagation(predicate.notNode());
   }
+  return d_solver.storePropagation(predicate.notNode());
 }
 
 bool CoreSolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 33f119e5f..19183c129 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -54,7 +54,6 @@ class CoreSolver : public SubtheorySolver {
 
   public:
     NotifyClass(CoreSolver& solver): d_solver(solver) {}
-    bool eqNotifyTriggerEquality(TNode equality, bool value) override;
     bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
     bool eqNotifyTriggerTermEquality(TheoryId tag,
                                      TNode t1,