From 8ed4c0c135fcdd49a777fed1a03b378861af9757 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 18 Sep 2018 20:54:13 -0500 Subject: [PATCH] Add two rewrites for string contains character (#2492) --- .../strings/theory_strings_rewriter.cpp | 39 +++++++++++++++++++ 1 file changed, 39 insertions(+) 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 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()) + { + 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 nc1; getConcat(node[0], nc1); -- 2.30.2