diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-18 20:54:13 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-09-18 18:54:13 -0700 |
commit | 8ed4c0c135fcdd49a777fed1a03b378861af9757 (patch) | |
tree | 2e98bc295b11bbe83459f7a9441e8511b4f71299 | |
parent | 2bb0196d4f9d0891bc7e95fff444c61ab09ee651 (diff) |
Add two rewrites for string contains character (#2492)
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 7e5f7102d..dd280f52c 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1495,6 +1495,45 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { Node ret = NodeManager::currentNM()->mkConst(true); return returnRewrite(node, ret, "ctn-rhs-emptystr"); } + else if (t.size() == 1) + { + // The following rewrites are specific to a single character second + // argument of contains, where we can reason that this character is + // not split over multiple components in the first argument. + if (node[0].getKind() == STRING_CONCAT) + { + std::vector<Node> nc1; + getConcat(node[0], nc1); + NodeBuilder<> nb(OR); + for (const Node& ncc : nc1) + { + nb << nm->mkNode(STRING_STRCTN, ncc, node[1]); + } + Node ret = nb.constructNode(); + // str.contains( x ++ y, "A" ) ---> + // str.contains( x, "A" ) OR str.contains( y, "A" ) + return returnRewrite(node, ret, "ctn-concat-char"); + } + else if (node[0].getKind() == STRING_STRREPL) + { + Node rplDomain = nm->mkNode(STRING_STRCTN, node[0][1], node[1]); + rplDomain = Rewriter::rewrite(rplDomain); + if (rplDomain.isConst() && !rplDomain.getConst<bool>()) + { + Node d1 = nm->mkNode(STRING_STRCTN, node[0][0], node[1]); + Node d2 = + nm->mkNode(AND, + nm->mkNode(STRING_STRCTN, node[0][0], node[0][1]), + nm->mkNode(STRING_STRCTN, node[0][2], node[1])); + Node ret = nm->mkNode(OR, d1, d2); + // If str.contains( y, "A" ) ---> false, then: + // str.contains( str.replace( x, y, z ), "A" ) ---> + // str.contains( x, "A" ) OR + // ( str.contains( x, y ) AND str.contains( z, "A" ) ) + return returnRewrite(node, ret, "ctn-repl-char"); + } + } + } } std::vector<Node> nc1; getConcat(node[0], nc1); |