Minor cleanup related to notifications (#4898)

This includes eliminating TheoryBV's call to eqNotifyNewEqClass and fixing an issue with string's eqNotifyNewEqClass method, which was registering constant integers.

It also removes some unnecessary methods in Theory.

2 files changed, 6 insertions, 10 deletions

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 02570b12c..c49909fe6 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -102,6 +102,11 @@ void CoreSolver::preRegister(TNode node) {
       }
   } else {
     d_equalityEngine.addTerm(node);
+    // Register with the extended theory, for context-dependent simplification.
+    // Notice we do this for registered terms but not internally generated
+    // equivalence classes. The two should roughly cooincide. Since ExtTheory is
+    // being used as a heuristic, it is good enough to be registered here.
+    d_extTheory->registerTerm(node);
   }
 }
 
@@ -397,10 +402,6 @@ void CoreSolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
   d_solver.conflict(t1, t2);
 }
 
-void CoreSolver::NotifyClass::eqNotifyNewClass(TNode t) {
-  d_solver.eqNotifyNewClass( t );
-}
-
 bool CoreSolver::storePropagation(TNode literal) {
   return d_bv->storePropagation(literal, SUB_CORE);
 }
@@ -412,8 +413,6 @@ void CoreSolver::conflict(TNode a, TNode b) {
   d_bv->setConflict(conflict);
 }
 
-void CoreSolver::eqNotifyNewClass(TNode t) { d_extTheory->registerTerm(t); }
-
 bool CoreSolver::isCompleteForTerm(TNode term, TNodeBoolMap& seen) {
   if (d_useSlicer)
     return utils::isCoreTerm(term, seen);
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 181d6ec79..ea652e7cd 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -61,7 +61,7 @@ class CoreSolver : public SubtheorySolver {
                                      TNode t2,
                                      bool value) override;
     void eqNotifyConstantTermMerge(TNode t1, TNode t2) override;
-    void eqNotifyNewClass(TNode t) override;
+    void eqNotifyNewClass(TNode t) override {}
     void eqNotifyMerge(TNode t1, TNode t2) override {}
     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
   };
@@ -79,9 +79,6 @@ class CoreSolver : public SubtheorySolver {
   /** Store a conflict from merging two constants */
   void conflict(TNode a, TNode b);
 
-  /** new equivalence class */
-  void eqNotifyNewClass(TNode t);
-
   std::unique_ptr<Slicer> d_slicer;
   context::CDO<bool> d_isComplete;
   unsigned d_lemmaThreshold;