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.

diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index 404bb850c1b675a71fc3943dfa0c0c69c5117ada..b583a55dac56ed8573d7c684f32a4e064fdea447 100644 (file)
--- 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 57a99532eb98d808ae04301f5bcc43942d4df931..0de42f686256adf654591e814be3f854f5382765 100644 (file)
--- 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 69d6ff68eea6571d66f2bd48daae5081209e9459..7731cd0786b272359c5ed6214985c815e0a12344 100644 (file)
--- 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 )