Move ss-combine rewrite to extended rewritersat2019pldi2019

We found that the `ss-combine` rewrite hurts solving performance, so
this commit is moving it to the extended rewriter.

3 files changed, 28 insertions, 5 deletions

diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index 656eceac9..89ab7c7f1 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -3534,6 +3534,10 @@ 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 aa5b616fe..26222084f 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1804,8 +1804,18 @@ 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() == kind::STRING_SUBSTR)
+  if (node[0].getKind() == STRING_SUBSTR)
   {
     Node start_inner = node[0][1];
     Node start_outer = node[1];
@@ -1818,7 +1828,7 @@ Node TheoryStringsRewriter::rewriteSubstr(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(kind::MINUS, node[0][2], start_outer));
+          Rewriter::rewrite(nm->mkNode(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
@@ -1836,13 +1846,13 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node)
       }
       if (!new_len.isNull())
       {
-        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);
+        Node new_start = nm->mkNode(PLUS, start_inner, start_outer);
+        Node ret = nm->mkNode(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 2e356f8f7..32512ae00 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -159,12 +159,21 @@ 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 )