From eb7226ebeabf7cc70ec023107d74ffc5c1bad5e7 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 21 Nov 2018 17:44:50 -0800
Subject: [PATCH] Move ss-combine rewrite to extended rewriter (#2703)

We found that the `ss-combine` rewrite hurts solving performance, so
this commit is moving it to the extended rewriter.
---
 src/theory/quantifiers/extended_rewrite.cpp   |  4 ++++
 .../strings/theory_strings_rewriter.cpp       | 21 +++++++++++++------
 src/theory/strings/theory_strings_rewriter.h  |  9 ++++++++
 3 files changed, 28 insertions(+), 6 deletions(-)

diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index 404bb850c..b583a55da 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -1676,6 +1676,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 57a99532e..0de42f686 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1806,8 +1806,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];
@@ -1820,7 +1830,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
@@ -1838,14 +1848,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 69d6ff68e..7731cd078 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 )
-- 
2.30.2