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.

4 files changed, 58 insertions, 75 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);
diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h
index 28dfbfd09..b295ba12d 100644
--- a/src/theory/strings/solver_state.h
+++ b/src/theory/strings/solver_state.h
@@ -121,6 +121,8 @@ class SolverState
   const context::CDList<Node>& getDisequalityList() const;
   //-------------------------------------- end equality information
   //-------------------------------------- notifications for equalities
+  /** called when a new equivalence class is created */
+  void eqNotifyNewClass(TNode t);
   /** called when two equivalence classes will merge */
   void eqNotifyPreMerge(TNode t1, TNode t2);
   /** called when two equivalence classes are made disequal */
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,
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index e0fca1b2e..79681a5f9 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -124,18 +124,21 @@ class TheoryStrings : public Theory {
 
   // NotifyClass for equality engine
   class NotifyClass : public eq::EqualityEngineNotify {
-    TheoryStrings& d_str;
   public:
-    NotifyClass(TheoryStrings& t_str): d_str(t_str) {}
-    bool eqNotifyTriggerEquality(TNode equality, bool value) override
-    {
-      Debug("strings") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
-      if (value) {
-        return d_str.propagate(equality);
-      } else {
-        // We use only literal triggers so taking not is safe
-        return d_str.propagate(equality.notNode());
-      }
+   NotifyClass(TheoryStrings& ts) : d_str(ts), d_state(ts.d_state) {}
+   bool eqNotifyTriggerEquality(TNode equality, bool value) override
+   {
+     Debug("strings") << "NotifyClass::eqNotifyTriggerEquality(" << equality
+                      << ", " << (value ? "true" : "false") << ")" << std::endl;
+     if (value)
+     {
+       return d_str.propagate(equality);
+     }
+     else
+     {
+       // We use only literal triggers so taking not is safe
+       return d_str.propagate(equality.notNode());
+     }
     }
     bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
     {
@@ -143,7 +146,7 @@ class TheoryStrings : public Theory {
       if (value) {
         return d_str.propagate(predicate);
       } else {
-         return d_str.propagate(predicate.notNode());
+        return d_str.propagate(predicate.notNode());
       }
     }
     bool eqNotifyTriggerTermEquality(TheoryId tag,
@@ -153,9 +156,9 @@ class TheoryStrings : public Theory {
     {
       Debug("strings") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
       if (value) {
-      return d_str.propagate(t1.eqNode(t2));
+        return d_str.propagate(t1.eqNode(t2));
       } else {
-      return d_str.propagate(t1.eqNode(t2).notNode());
+        return d_str.propagate(t1.eqNode(t2).notNode());
       }
     }
     void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
@@ -171,18 +174,23 @@ class TheoryStrings : public Theory {
     void eqNotifyPreMerge(TNode t1, TNode t2) override
     {
       Debug("strings") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl;
-      d_str.eqNotifyPreMerge(t1, t2);
+      d_state.eqNotifyPreMerge(t1, t2);
     }
     void eqNotifyPostMerge(TNode t1, TNode t2) override
     {
       Debug("strings") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl;
-      d_str.eqNotifyPostMerge(t1, t2);
     }
     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
     {
       Debug("strings") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl;
-      d_str.eqNotifyDisequal(t1, t2, reason);
+      d_state.eqNotifyDisequal(t1, t2, reason);
     }
+
+   private:
+    /** The theory of strings object to notify */
+    TheoryStrings& d_str;
+    /** The solver state of the theory of strings */
+    SolverState& d_state;
   };/* class TheoryStrings::NotifyClass */
 
   //--------------------------- helper functions
@@ -280,12 +288,6 @@ private:
   void conflict(TNode a, TNode b);
   /** called when a new equivalence class is created */
   void eqNotifyNewClass(TNode t);
-  /** called when two equivalence classes will merge */
-  void eqNotifyPreMerge(TNode t1, TNode t2);
-  /** called when two equivalence classes have merged */
-  void eqNotifyPostMerge(TNode t1, TNode t2);
-  /** called when two equivalence classes are made disequal */
-  void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
 
  protected:
   /** compute care graph */