Merge branch 'revertMoveSSCombine' into aggSkolemSharingaggSkolemSharing

3 files changed, 6 insertions, 28 deletions

diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index ae053930c..46dcb7151 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -1677,10 +1677,6 @@ Node ExtendedRewriter::extendedRewriteStrings(Node ret)
   {
     new_ret = strings::TheoryStringsRewriter::rewriteEqualityExt(ret);
   }
-  else if (ret.getKind() == STRING_SUBSTR)
-  {
-    new_ret = strings::TheoryStringsRewriter::rewriteSubstrExt(ret);
-  }
 
   return new_ret;
 }
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 0de42f686..57a99532e 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1806,18 +1806,8 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node)
       }
     }
   }
-  Trace("strings-rewrite-nf") << "No rewrites for : " << node << std::endl;
-  return node;
-}
-
-Node TheoryStringsRewriter::rewriteSubstrExt(Node node)
-{
-  Assert(node.getKind() == STRING_SUBSTR);
-
-  NodeManager* nm = NodeManager::currentNM();
-
   // combine substr
-  if (node[0].getKind() == STRING_SUBSTR)
+  if (node[0].getKind() == kind::STRING_SUBSTR)
   {
     Node start_inner = node[0][1];
     Node start_outer = node[1];
@@ -1830,7 +1820,7 @@ Node TheoryStringsRewriter::rewriteSubstrExt(Node node)
       // the length of a string from the inner substr subtracts the start point
       // of the outer substr
       Node len_from_inner =
-          Rewriter::rewrite(nm->mkNode(MINUS, node[0][2], start_outer));
+          Rewriter::rewrite(nm->mkNode(kind::MINUS, node[0][2], start_outer));
       Node len_from_outer = node[2];
       Node new_len;
       // take quantity that is for sure smaller than the other
@@ -1848,13 +1838,14 @@ Node TheoryStringsRewriter::rewriteSubstrExt(Node node)
       }
       if (!new_len.isNull())
       {
-        Node new_start = nm->mkNode(PLUS, start_inner, start_outer);
-        Node ret = nm->mkNode(STRING_SUBSTR, node[0][0], new_start, new_len);
+        Node new_start = nm->mkNode(kind::PLUS, start_inner, start_outer);
+        Node ret =
+            nm->mkNode(kind::STRING_SUBSTR, node[0][0], new_start, new_len);
         return returnRewrite(node, ret, "ss-combine");
       }
     }
   }
-
+  Trace("strings-rewrite-nf") << "No rewrites for : " << node << std::endl;
   return node;
 }
 
diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index 7731cd078..69d6ff68e 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -159,21 +159,12 @@ class TheoryStringsRewriter {
   * Returns the rewritten form of node.
   */
   static Node rewriteConcat(Node node);
-
   /** rewrite substr
   * This is the entry point for post-rewriting terms node of the form
   *   str.substr( s, i1, i2 )
   * Returns the rewritten form of node.
   */
   static Node rewriteSubstr(Node node);
-
-  /** rewrite substr extended
-   * This is the entry point for extended post-rewriting terms node of the form
-   *   str.substr( s, i1, i2 )
-   * Returns the rewritten form of node.
-   */
-  static Node rewriteSubstrExt(Node node);
-
   /** rewrite contains
   * This is the entry point for post-rewriting terms node of the form
   *   str.contains( t, s )