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.

4 files changed, 13 insertions, 17 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;
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 970b832a9..a554ac595 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -118,10 +118,12 @@ void SolverState::eqNotifyNewClass(TNode t)
   }
   else if (t.isConst())
   {
-    EqcInfo* ei = getOrMakeEqcInfo(t);
-    ei->d_prefixC = t;
-    ei->d_suffixC = t;
-    return;
+    if (t.getType().isStringLike())
+    {
+      EqcInfo* ei = getOrMakeEqcInfo(t);
+      ei->d_prefixC = t;
+      ei->d_suffixC = t;
+    }
   }
   else if (k == STRING_CONCAT)
   {
@@ -134,6 +136,7 @@ void SolverState::eqNotifyMerge(TNode t1, TNode t2)
   EqcInfo* e2 = getOrMakeEqcInfo(t2, false);
   if (e2)
   {
+    Assert(t1.getType().isStringLike());
     EqcInfo* e1 = getOrMakeEqcInfo(t1);
     // add information from e2 to e1
     if (!e2->d_lengthTerm.get().isNull())
diff --git a/src/theory/theory.h b/src/theory/theory.h
index e40534dc4..ef06732fb 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -522,9 +522,6 @@ class Theory {
   /** Called to set the decision manager. */
   void setDecisionManager(DecisionManager* dm);
 
-  /** Setup an ExtTheory module for this Theory. Can only be called once. */
-  void setupExtTheory();
-
   /**
    * Return the current theory care graph. Theories should overload
    * computeCareGraph to do the actual computation, and use addCarePair to add