Add substr, contains and equality rewrites (#2665)

2 files changed, 82 insertions, 0 deletions

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 1dc894117..5ba9d6e3f 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -575,6 +575,21 @@ Node TheoryStringsRewriter::rewriteStrEqualityExt(Node node)
           return returnRewrite(node, ret, "str-eq-repl-not-ctn");
         }
       }
+
+      // (= (str.replace x y z) z) --> (or (= x y) (= x z))
+      // if (str.len y) = (str.len z)
+      if (repl[2] == x)
+      {
+        Node lenY = nm->mkNode(STRING_LENGTH, repl[1]);
+        Node lenZ = nm->mkNode(STRING_LENGTH, repl[2]);
+        if (checkEntailArithEq(lenY, lenZ))
+        {
+          Node ret = nm->mkNode(OR,
+                                nm->mkNode(EQUAL, repl[0], repl[1]),
+                                nm->mkNode(EQUAL, repl[0], repl[2]));
+          return returnRewrite(node, ret, "str-eq-repl-to-dis");
+        }
+      }
     }
   }
 
@@ -1733,6 +1748,15 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node)
         return returnRewrite(node, ret, "ss-start-entails-zero-len");
       }
 
+      // (str.substr s x y) --> "" if 0 < y |= x >= str.len(s)
+      Node non_zero_len =
+          Rewriter::rewrite(nm->mkNode(kind::LT, zero, node[2]));
+      if (checkEntailArithWithAssumption(non_zero_len, node[1], tot_len, false))
+      {
+        Node ret = nm->mkConst(::CVC4::String(""));
+        return returnRewrite(node, ret, "ss-non-zero-len-entails-oob");
+      }
+
       // (str.substr s x x) ---> "" if (str.len s) <= 1
       if (node[1] == node[2] && checkEntailLengthOne(node[0]))
       {
@@ -2165,6 +2189,24 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
                             nm->mkNode(STRING_STRCTN, node[0][0], node[0][2]));
       return returnRewrite(node, ret, "ctn-repl-to-ctn-disj");
     }
+
+    // (str.contains (str.replace x y z) w) --->
+    //   (str.contains (str.replace x y "") w)
+    // if (str.contains z w) ---> false and (str.len w) = 1
+    if (checkEntailLengthOne(node[1]))
+    {
+      Node ctn = Rewriter::rewrite(
+          nm->mkNode(kind::STRING_STRCTN, node[1], node[0][2]));
+      if (ctn.isConst() && !ctn.getConst<bool>())
+      {
+        Node empty = nm->mkConst(String(""));
+        Node ret = nm->mkNode(
+            kind::STRING_STRCTN,
+            nm->mkNode(kind::STRING_STRREPL, node[0][0], node[0][1], empty),
+            node[1]);
+        return returnRewrite(node, ret, "ctn-repl-simp-repl");
+      }
+    }
   }
 
   if (node[1].getKind() == kind::STRING_STRREPL)
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index 87817872b..87aef3704 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -145,6 +145,10 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     Node z = d_nm->mkVar("z", intType);
 
     Node zero = d_nm->mkConst(Rational(0));
+    Node one = d_nm->mkConst(Rational(1));
+
+    Node empty = d_nm->mkConst(::CVC4::String(""));
+    Node a = d_nm->mkConst(::CVC4::String("A"));
 
     Node slen_y = d_nm->mkNode(kind::STRING_LENGTH, y);
     Node x_plus_slen_y = d_nm->mkNode(kind::PLUS, x, slen_y);
@@ -198,6 +202,14 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     // x + 5 < 5 |= 0 > x --> true
     TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption(
         x_plus_five_lt_five, zero, x, false));
+
+    // 0 < x |= x >= (str.len (int.to.str x))
+    Node assm = Rewriter::rewrite(d_nm->mkNode(kind::LT, zero, x));
+    TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption(
+        assm,
+        x,
+        d_nm->mkNode(kind::STRING_LENGTH, d_nm->mkNode(kind::STRING_ITOS, x)),
+        false));
   }
 
   void testRewriteSubstr()
@@ -313,6 +325,11 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
                                substr_y,
                                b);
     sameNormalForm(substr_repl, repl_substr);
+
+    // (str.substr (str.int.to.str x) x x) ---> empty
+    Node substr_itos = d_nm->mkNode(
+        kind::STRING_SUBSTR, d_nm->mkNode(kind::STRING_ITOS, x), x, x);
+    sameNormalForm(substr_itos, empty);
   }
 
   void testRewriteConcat()
@@ -816,6 +833,18 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     rhs = d_nm->mkNode(
         kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, x, z, y), y);
     sameNormalForm(lhs, rhs);
+
+    // Same normal form for:
+    //
+    // (str.contains (str.replace x "A" "B") "A")
+    //
+    // (str.contains (str.replace x "A" "") "A")
+    lhs = d_nm->mkNode(
+        kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_STRREPL, x, a, b), a);
+    rhs = d_nm->mkNode(kind::STRING_STRCTN,
+                       d_nm->mkNode(kind::STRING_STRREPL, x, a, empty),
+                       a);
+    sameNormalForm(lhs, rhs);
   }
 
   void testInferEqsFromContains()
@@ -1024,6 +1053,17 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
         kind::EQUAL, d_nm->mkNode(kind::STRING_STRREPL, x, a, b), empty);
     Node eq_x = d_nm->mkNode(kind::EQUAL, x, empty);
     sameNormalForm(eq_repl, eq_x);
+
+    // Same normal form for:
+    //
+    // (= (str.replace y "A" "B") "B")
+    //
+    // (= (str.replace y "B" "A") "A")
+    Node lhs = d_nm->mkNode(
+        kind::EQUAL, d_nm->mkNode(kind::STRING_STRREPL, x, a, b), b);
+    Node rhs = d_nm->mkNode(
+        kind::EQUAL, d_nm->mkNode(kind::STRING_STRREPL, x, b, a), a);
+    sameNormalForm(lhs, rhs);
   }
 
  private: