From e644cb6dc8b5b8c64663bd4e57d14e1d86588695 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 14 Dec 2018 23:37:56 -0800
Subject: Revert "Move ss-combine rewrite to extended rewriter (#2703)"

This reverts commit eb7226ebeabf7cc70ec023107d74ffc5c1bad5e7. After
merging #2740, our experiments show that the ss-combine rewrite is
now beneficial for solving performance.
---
 src/theory/quantifiers/extended_rewrite.cpp    |  4 ----
 src/theory/strings/theory_strings_rewriter.cpp | 21 ++++++---------------
 src/theory/strings/theory_strings_rewriter.h   |  9 ---------
 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 )
-- 
cgit v1.2.3