Improve reasoning about empty strings in rewriter (#2615)

1 files changed, 44 insertions, 2 deletions

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 00a711a31..6ee01e992 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -489,6 +489,13 @@ Node TheoryStringsRewriter::rewriteStrEqualityExt(Node node)
       Node ne = node[1 - i];
       if (ne.getKind() == STRING_STRREPL)
       {
+        // (= "" (str.replace x y x)) ---> (= x "")
+        if (ne[0] == ne[2])
+        {
+          Node ret = nm->mkNode(EQUAL, ne[0], empty);
+          return returnRewrite(node, ret, "str-emp-repl-x-y-x");
+        }
+
         // (= "" (str.replace x y "A")) ---> (and (= x "") (not (= y "")))
         if (checkEntailNonEmpty(ne[2]))
         {
@@ -512,9 +519,17 @@ Node TheoryStringsRewriter::rewriteStrEqualityExt(Node node)
       {
         Node zero = nm->mkConst(Rational(0));
 
-        // (= "" (str.substr x n m)) ---> (<= (str.len x) n) if n >= 0 and m > 0
         if (checkEntailArith(ne[1], false) && checkEntailArith(ne[2], true))
         {
+          // (= "" (str.substr x 0 m)) ---> (= "" x) if m > 0
+          if (ne[1] == zero)
+          {
+            Node ret = nm->mkNode(EQUAL, ne[0], empty);
+            return returnRewrite(node, ret, "str-emp-substr-leq-len");
+          }
+
+          // (= "" (str.substr x n m)) ---> (<= (str.len x) n)
+          // if n >= 0 and m > 0
           Node ret = nm->mkNode(LEQ, nm->mkNode(STRING_LENGTH, ne[0]), ne[1]);
           return returnRewrite(node, ret, "str-emp-substr-leq-len");
         }
@@ -2476,8 +2491,9 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
     //
     Node empty = nm->mkConst(::CVC4::String(""));
 
-    // Collect the equalities of the form (= x "")
+    // Collect the equalities of the form (= x "") (sorted)
     std::set<TNode> emptyNodes;
+    bool allEmptyEqs = true;
     if (cmp_conr.getKind() == kind::EQUAL)
     {
       if (cmp_conr[0] == empty)
@@ -2488,6 +2504,10 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
       {
         emptyNodes.insert(cmp_conr[0]);
       }
+      else
+      {
+        allEmptyEqs = false;
+      }
     }
     else
     {
@@ -2504,6 +2524,10 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
             emptyNodes.insert(c[0]);
           }
         }
+        else
+        {
+          allEmptyEqs = false;
+        }
       }
     }
 
@@ -2514,6 +2538,24 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
       Node nn2 = node[2].substitute(
           emptyNodes.begin(), emptyNodes.end(), substs.begin(), substs.end());
 
+      // If the contains rewrites to a conjunction of empty-string equalities
+      // and we are doing the replacement in an empty string, we can rewrite
+      // the string-to-replace with a concatenation of all the terms that must
+      // be empty:
+      //
+      // (str.replace "" y z) ---> (str.replace "" (str.++ y1 ... yn)  z)
+      // if (str.contains "" y) ---> (and (= y1 "") ... (= yn ""))
+      if (node[0] == empty && allEmptyEqs)
+      {
+        std::vector<Node> emptyNodesList(emptyNodes.begin(), emptyNodes.end());
+        Node nn1 = mkConcat(STRING_CONCAT, emptyNodesList);
+        if (nn1 != node[1] || nn2 != node[2])
+        {
+          Node res = nm->mkNode(kind::STRING_STRREPL, node[0], nn1, nn2);
+          return returnRewrite(node, res, "rpl-emp-cnts-substs");
+        }
+      }
+
       if (nn2 != node[2])
       {
         Node res = nm->mkNode(kind::STRING_STRREPL, node[0], node[1], nn2);