From 10788f4bc499d4915473453c40bf72b8d4432afb Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 28 Sep 2018 10:18:04 -0700 Subject: [PATCH] Rewrites for (= "" _) and (= (str.replace _) _) (#2546) --- src/theory/quantifiers/extended_rewrite.cpp | 5 + .../strings/theory_strings_rewriter.cpp | 123 ++++++++++++++++-- .../theory/theory_strings_rewriter_white.h | 121 +++++++++++++++++ 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()) + { + 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; -- 2.30.2