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, 2 insertions, 52 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index d3d75a98d..92af3cc0a 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -88,19 +88,6 @@ TheoryStrings::TheoryStrings(context::Context* c,
   d_esolver.reset(new ExtfSolver(
       c, u, d_state, d_im, d_sk_cache, d_bsolver, d_csolver, extt));
   d_rsolver.reset(new RegExpSolver(*this, d_state, d_im, *d_esolver, c, u));
-  getExtTheory()->addFunctionKind(kind::STRING_SUBSTR);
-  getExtTheory()->addFunctionKind(kind::STRING_STRIDOF);
-  getExtTheory()->addFunctionKind(kind::STRING_ITOS);
-  getExtTheory()->addFunctionKind(kind::STRING_STOI);
-  getExtTheory()->addFunctionKind(kind::STRING_STRREPL);
-  getExtTheory()->addFunctionKind(kind::STRING_STRREPLALL);
-  getExtTheory()->addFunctionKind(kind::STRING_STRCTN);
-  getExtTheory()->addFunctionKind(kind::STRING_IN_REGEXP);
-  getExtTheory()->addFunctionKind(kind::STRING_LEQ);
-  getExtTheory()->addFunctionKind(kind::STRING_CODE);
-  getExtTheory()->addFunctionKind(kind::STRING_TOLOWER);
-  getExtTheory()->addFunctionKind(kind::STRING_TOUPPER);
-  getExtTheory()->addFunctionKind(kind::STRING_REV);
 
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
@@ -740,52 +727,15 @@ void TheoryStrings::conflict(TNode a, TNode b){
   }
 }
 
-/** called when a new equivalance class is created */
 void TheoryStrings::eqNotifyNewClass(TNode t){
   Kind k = t.getKind();
-  if (k == kind::STRING_LENGTH || k == kind::STRING_CODE)
+  if (k == STRING_LENGTH || k == STRING_CODE)
   {
     Trace("strings-debug") << "New length eqc : " << t << std::endl;
-    Node r = d_equalityEngine.getRepresentative(t[0]);
-    EqcInfo* ei = d_state.getOrMakeEqcInfo(r);
-    if (k == kind::STRING_LENGTH)
-    {
-      ei->d_lengthTerm = t[0];
-    }
-    else
-    {
-      ei->d_codeTerm = t[0];
-    }
     //we care about the length of this string
     registerTerm( t[0], 1 );
-    return;
-  }
-  else if (k == CONST_STRING)
-  {
-    EqcInfo* ei = d_state.getOrMakeEqcInfo(t);
-    ei->d_prefixC = t;
-    ei->d_suffixC = t;
-    return;
   }
-  else if (k == STRING_CONCAT)
-  {
-    d_state.addEndpointsToEqcInfo(t, t, t);
-  }
-}
-
-/** called when two equivalance classes will merge */
-void TheoryStrings::eqNotifyPreMerge(TNode t1, TNode t2){
-  d_state.eqNotifyPreMerge(t1, t2);
-}
-
-/** called when two equivalance classes have merged */
-void TheoryStrings::eqNotifyPostMerge(TNode t1, TNode t2) {
-
-}
-
-/** called when two equivalance classes are disequal */
-void TheoryStrings::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
-  d_state.eqNotifyDisequal(t1, t2, reason);
+  d_state.eqNotifyNewClass(t);
 }
 
 void TheoryStrings::addCarePairs(TNodeTrie* t1,