Improve reasoning about empty strings in rewriter (#2615)

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 00a711a31b1125b93220afdb43b42712ec4a5871..6ee01e992a62108ecaef54eed750e728e801acaf 100644 (file)
--- 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);

diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index d967ab7930319fc238ae7df5514d701d56bcf4f5..cc29efb23a9a11f10a19bab7559d55624bc4c396 100644 (file)
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -381,6 +381,8 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     Node x = d_nm->mkVar("x", strType);
     Node y = d_nm->mkVar("y", strType);
     Node z = d_nm->mkVar("z", strType);
+    Node zero = d_nm->mkConst(Rational(0));
+    Node one = d_nm->mkConst(Rational(1));
 
     // (str.replace (str.replace x "B" x) x "A") -->
     //   (str.replace (str.replace x "B" "A") x "A")
@@ -452,6 +454,32 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
                              d_nm->mkNode(kind::STRING_STRREPL, y, x, a),
                              y);
     sameNormalForm(repl_repl, empty);
+
+    // (str.replace "" (str.replace x y x) x) ---> ""
+    repl_repl = d_nm->mkNode(kind::STRING_STRREPL,
+                             empty,
+                             d_nm->mkNode(kind::STRING_STRREPL, x, y, x),
+                             x);
+    sameNormalForm(repl_repl, empty);
+
+    // (str.replace "" (str.substr x 0 1) x) ---> ""
+    repl_repl = d_nm->mkNode(kind::STRING_STRREPL,
+                             empty,
+                             d_nm->mkNode(kind::STRING_SUBSTR, x, zero, one),
+                             x);
+    sameNormalForm(repl_repl, empty);
+
+    // Same normal form for:
+    //
+    // (str.replace "" (str.replace x y x) y)
+    //
+    // (str.replace "" x y)
+    repl_repl = d_nm->mkNode(kind::STRING_STRREPL,
+                             empty,
+                             d_nm->mkNode(kind::STRING_STRREPL, x, y, x),
+                             y);
+    Node repl = d_nm->mkNode(kind::STRING_STRREPL, empty, x, y);
+    sameNormalForm(repl_repl, repl);
   }
 
   void testRewriteContains()