Rewrites for (= "" _) and (= (str.replace _) _) (#2546)

3 files changed, 238 insertions, 11 deletions

diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index ab292e7bb..404bb850c 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -1672,6 +1672,11 @@ Node ExtendedRewriter::extendedRewriteStrings(Node ret)
   Trace("q-ext-rewrite-debug")
       << "Extended rewrite strings : " << ret << std::endl;
 
+  if (ret.getKind() == EQUAL)
+  {
+    new_ret = strings::TheoryStringsRewriter::rewriteEqualityExt(ret);
+  }
+
   return new_ret;
 }
 
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index ad8591b3b..9813848a1 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -469,7 +469,90 @@ Node TheoryStringsRewriter::rewriteEqualityExt(Node node)
     }
   }
 
-  Assert(node.getKind() == EQUAL);
+  // ------- rewrites for (= "" _)
+  Node empty = nm->mkConst(::CVC4::String(""));
+  for (size_t i = 0; i < 2; i++)
+  {
+    if (node[i] == empty)
+    {
+      Node ne = node[1 - i];
+      if (ne.getKind() == STRING_STRREPL)
+      {
+        // (= "" (str.replace x y "A")) ---> (and (= x "") (not (= y "")))
+        if (checkEntailNonEmpty(ne[2]))
+        {
+          Node ret =
+              nm->mkNode(AND,
+                         nm->mkNode(EQUAL, ne[0], empty),
+                         nm->mkNode(NOT, nm->mkNode(EQUAL, ne[1], empty)));
+          return returnRewrite(node, ret, "str-emp-repl-emp");
+        }
+
+        // (= "" (str.replace x "A" "")) ---> (str.prefix x "A")
+        Node one = nm->mkConst(Rational(1));
+        Node ylen = nm->mkNode(STRING_LENGTH, ne[1]);
+        if (checkEntailArithEq(ylen, one) && ne[2] == empty)
+        {
+          Node ret = nm->mkNode(STRING_PREFIX, ne[0], ne[1]);
+          return returnRewrite(node, ret, "str-emp-repl-emp");
+        }
+      }
+      else if (ne.getKind() == STRING_SUBSTR)
+      {
+        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))
+        {
+          Node ret = nm->mkNode(LEQ, nm->mkNode(STRING_LENGTH, ne[0]), ne[1]);
+          return returnRewrite(node, ret, "str-emp-substr-leq-len");
+        }
+
+        // (= "" (str.substr "A" 0 z)) ---> (<= z 0)
+        if (checkEntailNonEmpty(ne[0]) && ne[1] == zero)
+        {
+          Node ret = nm->mkNode(LEQ, ne[2], zero);
+          return returnRewrite(node, ret, "str-emp-substr-leq-z");
+        }
+      }
+    }
+  }
+
+  // ------- rewrites for (= (str.replace _ _ _) _)
+  for (size_t i = 0; i < 2; i++)
+  {
+    if (node[i].getKind() == STRING_STRREPL)
+    {
+      Node repl = node[i];
+      Node x = node[1 - i];
+
+      // (= "A" (str.replace "" x y)) ---> (= "" (str.replace "A" y x))
+      if (checkEntailNonEmpty(x) && repl[0] == empty)
+      {
+        Node ret = nm->mkNode(
+            EQUAL, empty, nm->mkNode(STRING_STRREPL, x, repl[2], repl[1]));
+        return returnRewrite(node, ret, "str-eq-repl-emp");
+      }
+
+      // (= x (str.replace y x y)) ---> (= x y)
+      if (repl[0] == repl[2] && x == repl[1])
+      {
+        Node ret = nm->mkNode(EQUAL, x, repl[0]);
+        return returnRewrite(node, ret, "str-eq-repl-to-eq");
+      }
+
+      // (= x (str.replace x "A" "B")) ---> (not (str.contains x "A"))
+      if (x == repl[0])
+      {
+        Node eq = Rewriter::rewrite(nm->mkNode(EQUAL, repl[1], repl[2]));
+        if (eq.isConst() && !eq.getConst<bool>())
+        {
+          Node ret = nm->mkNode(NOT, nm->mkNode(STRING_STRCTN, x, repl[1]));
+          return returnRewrite(node, ret, "str-eq-repl-not-ctn");
+        }
+      }
+    }
+  }
 
   // Try to rewrite (= x y) into a conjunction of equalities based on length
   // entailment.
@@ -481,12 +564,16 @@ Node TheoryStringsRewriter::rewriteEqualityExt(Node node)
   //   (<= (str.len x) (str.++ y1' ... ym'))
   for (unsigned i = 0; i < 2; i++)
   {
-    new_ret = inferEqsFromContains(node[i], node[1 - i]);
-    if (!new_ret.isNull())
+    if (node[1 - i].getKind() == STRING_CONCAT)
     {
-      return returnRewrite(node, new_ret, "str-eq-conj-len-entail");
+      new_ret = inferEqsFromContains(node[i], node[1 - i]);
+      if (!new_ret.isNull())
+      {
+        return returnRewrite(node, new_ret, "str-eq-conj-len-entail");
+      }
     }
   }
+
   return node;
 }
 
@@ -2328,13 +2415,16 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
     {
       for (const Node& c : cmp_conr)
       {
-        if (c[0] == empty)
+        if (c.getKind() == kind::EQUAL)
         {
-          emptyNodes.insert(c[1]);
-        }
-        else if (c[1] == empty)
-        {
-          emptyNodes.insert(c[0]);
+          if (c[0] == empty)
+          {
+            emptyNodes.insert(c[1]);
+          }
+          else if (c[1] == empty)
+          {
+            emptyNodes.insert(c[0]);
+          }
         }
       }
     }
@@ -4064,6 +4154,9 @@ Node TheoryStringsRewriter::returnRewrite(Node node, Node ret, const char* c)
 {
   Trace("strings-rewrite") << "Rewrite " << node << " to " << ret << " by " << c
                            << "." << std::endl;
+
+  NodeManager* nm = NodeManager::currentNM();
+
   // standard post-processing
   // We rewrite (string) equalities immediately here. This allows us to forego
   // the standard invariant on equality rewrites (that s=t must rewrite to one
@@ -4080,14 +4173,22 @@ Node TheoryStringsRewriter::returnRewrite(Node node, Node ret, const char* c)
       {
         creter = rewriteEqualityExt(cret);
       }
+      else if (cret.getKind() == NOT && cret[0].getKind() == EQUAL)
+      {
+        creter = nm->mkNode(NOT, rewriteEqualityExt(cret[0]));
+      }
       childChanged = childChanged || cret != creter;
       children.push_back(creter);
     }
     if (childChanged)
     {
-      ret = NodeManager::currentNM()->mkNode(retk, children);
+      ret = nm->mkNode(retk, children);
     }
   }
+  else if (retk == NOT && ret[0].getKind() == EQUAL)
+  {
+    ret = nm->mkNode(NOT, rewriteEqualityExt(ret[0]));
+  }
   else if (retk == EQUAL && node.getKind() != EQUAL)
   {
     Trace("strings-rewrite")
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index 0b569394d..d038b310e 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -411,6 +411,13 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
                                      d_nm->mkNode(kind::STRING_CONCAT, a, x),
                                      empty);
     differentNormalForms(repl_ab_ax_e, repl_ab_xa_e);
+
+    // (str.replace "" (str.replace y x "A") y) ---> ""
+    repl_repl = d_nm->mkNode(kind::STRING_STRREPL,
+                             empty,
+                             d_nm->mkNode(kind::STRING_STRREPL, y, x, a),
+                             y);
+    sameNormalForm(repl_repl, empty);
   }
 
   void testRewriteContains()
@@ -661,6 +668,120 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     sameNormalForm(p_xxa, f);
   }
 
+  void testRewriteEqualityExt()
+  {
+    TypeNode strType = d_nm->stringType();
+    TypeNode intType = d_nm->integerType();
+
+    Node empty = d_nm->mkConst(::CVC4::String(""));
+    Node a = d_nm->mkConst(::CVC4::String("A"));
+    Node b = d_nm->mkConst(::CVC4::String("B"));
+    Node x = d_nm->mkVar("x", strType);
+    Node y = d_nm->mkVar("y", strType);
+    Node xxa = d_nm->mkNode(kind::STRING_CONCAT, x, x, a);
+    Node f = d_nm->mkConst(false);
+    Node n = d_nm->mkVar("n", intType);
+    Node zero = d_nm->mkConst(Rational(0));
+    Node one = d_nm->mkConst(Rational(1));
+    Node three = d_nm->mkConst(Rational(3));
+
+    // Same normal form for:
+    //
+    // (= "" (str.replace "" x "B"))
+    //
+    // (not (= x ""))
+    Node empty_repl = d_nm->mkNode(
+        kind::EQUAL, empty, d_nm->mkNode(kind::STRING_STRREPL, empty, x, b));
+    Node empty_x = d_nm->mkNode(kind::NOT, d_nm->mkNode(kind::EQUAL, x, empty));
+    sameNormalForm(empty_repl, empty_x);
+
+    // Same normal form for:
+    //
+    // (= "" (str.replace x y (str.++ x x "A")))
+    //
+    // (and (= x "") (not (= y "")))
+    Node empty_repl_xaa = d_nm->mkNode(
+        kind::EQUAL, empty, d_nm->mkNode(kind::STRING_STRREPL, x, y, xxa));
+    Node empty_xy = d_nm->mkNode(
+        kind::AND,
+        d_nm->mkNode(kind::EQUAL, x, empty),
+        d_nm->mkNode(kind::NOT, d_nm->mkNode(kind::EQUAL, y, empty)));
+    sameNormalForm(empty_repl_xaa, empty_xy);
+
+    // (= "" (str.replace (str.++ x x "A") x y)) ---> false
+    Node empty_repl_xxaxy = d_nm->mkNode(
+        kind::EQUAL, empty, d_nm->mkNode(kind::STRING_STRREPL, xxa, x, y));
+    Node eq_xxa_repl = d_nm->mkNode(
+        kind::EQUAL, xxa, d_nm->mkNode(kind::STRING_STRREPL, empty, y, x));
+    sameNormalForm(empty_repl_xxaxy, f);
+
+    // Same normal form for:
+    //
+    // (= "" (str.replace "A" x y))
+    //
+    // (= "A" (str.replace "" y x))
+    Node empty_repl_axy = d_nm->mkNode(
+        kind::EQUAL, empty, d_nm->mkNode(kind::STRING_STRREPL, a, x, y));
+    Node eq_a_repl = d_nm->mkNode(
+        kind::EQUAL, a, d_nm->mkNode(kind::STRING_STRREPL, empty, y, x));
+    sameNormalForm(empty_repl_axy, eq_a_repl);
+
+    // Same normal form for:
+    //
+    // (= "" (str.replace x "A" ""))
+    //
+    // (str.prefix x "A")
+    Node empty_repl_a = d_nm->mkNode(
+        kind::EQUAL, empty, d_nm->mkNode(kind::STRING_STRREPL, x, a, empty));
+    Node prefix_a = d_nm->mkNode(kind::STRING_PREFIX, x, a);
+    sameNormalForm(empty_repl_a, prefix_a);
+
+    // Same normal form for:
+    //
+    // (= "" (str.substr x 1 2))
+    //
+    // (<= (str.len x) 1)
+    Node empty_substr = d_nm->mkNode(
+        kind::EQUAL, empty, d_nm->mkNode(kind::STRING_SUBSTR, x, one, three));
+    Node leq_len_x =
+        d_nm->mkNode(kind::LEQ, d_nm->mkNode(kind::STRING_LENGTH, x), one);
+    sameNormalForm(empty_substr, leq_len_x);
+
+    // Different normal form for:
+    //
+    // (= "" (str.substr x 0 n))
+    //
+    // (<= n 0)
+    Node empty_substr_x = d_nm->mkNode(
+        kind::EQUAL, empty, d_nm->mkNode(kind::STRING_SUBSTR, x, zero, n));
+    Node leq_n = d_nm->mkNode(kind::LEQ, n, zero);
+    differentNormalForms(empty_substr_x, leq_n);
+
+    // Same normal form for:
+    //
+    // (= "" (str.substr "A" 0 n))
+    //
+    // (<= n 0)
+    Node empty_substr_a = d_nm->mkNode(
+        kind::EQUAL, empty, d_nm->mkNode(kind::STRING_SUBSTR, a, zero, n));
+    sameNormalForm(empty_substr_a, leq_n);
+
+    // Same normal form for:
+    //
+    // (= (str.++ x x a) (str.replace y (str.++ x x a) y))
+    //
+    // (= (str.++ x x a) y)
+    Node eq_xxa_repl_y = d_nm->mkNode(
+        kind::EQUAL, xxa, d_nm->mkNode(kind::STRING_STRREPL, y, xxa, y));
+    Node eq_xxa_y = d_nm->mkNode(kind::EQUAL, xxa, y);
+    sameNormalForm(eq_xxa_repl_y, eq_xxa_y);
+
+    // (= (str.++ x x a) (str.replace (str.++ x x a) "A" "B")) ---> false
+    Node eq_xxa_repl_xxa = d_nm->mkNode(
+        kind::EQUAL, xxa, d_nm->mkNode(kind::STRING_STRREPL, xxa, a, b));
+    sameNormalForm(eq_xxa_repl_xxa, f);
+  }
+
  private:
   ExprManager* d_em;
   SmtEngine* d_smt;