Minor refactoring of equality notifications (#3798)

Towards moving functionalities to proper places in strings. Also removes a block of code that was duplicated as a result of splitting the ExtfSolver.

1 files changed, 29 insertions, 0 deletions

diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 2fc49d8b7..5eb0818b7 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -206,6 +206,35 @@ const context::CDList<Node>& SolverState::getDisequalityList() const
   return d_eeDisequalities;
 }
 
+void SolverState::eqNotifyNewClass(TNode t)
+{
+  Kind k = t.getKind();
+  if (k == STRING_LENGTH || k == STRING_CODE)
+  {
+    Node r = d_ee.getRepresentative(t[0]);
+    EqcInfo* ei = getOrMakeEqcInfo(r);
+    if (k == STRING_LENGTH)
+    {
+      ei->d_lengthTerm = t[0];
+    }
+    else
+    {
+      ei->d_codeTerm = t[0];
+    }
+  }
+  else if (k == CONST_STRING)
+  {
+    EqcInfo* ei = getOrMakeEqcInfo(t);
+    ei->d_prefixC = t;
+    ei->d_suffixC = t;
+    return;
+  }
+  else if (k == STRING_CONCAT)
+  {
+    addEndpointsToEqcInfo(t, t, t);
+  }
+}
+
 void SolverState::eqNotifyPreMerge(TNode t1, TNode t2)
 {
   EqcInfo* e2 = getOrMakeEqcInfo(t2, false);