diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-29 10:17:06 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-01-29 10:17:06 -0800 |
commit | 1eaf6cf987fa1452528dc0598ca7235be735ba3b (patch) | |
tree | c327198308289e343aabf576ff3e3a05637aa166 /src | |
parent | 467ef8692009f440bda74083d476131ff1e88b51 (diff) |
Strings: Remove redundant replace rewrite (#2822)
Pulling the first constant string from a replace if there is no overlap
with the search term is subsumed by the rewrite using
`stripConstantEndpoints()`.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 8e5e22d38..0c8d6ac8d 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -2373,19 +2373,6 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { { return returnRewrite(node, node[0], "rpl-const-nfind"); } - // if no overlap, we can pull the first child - if (s.overlap(t) == 0) - { - std::vector<Node> spl(children0.begin() + 1, children0.end()); - Node ret = NodeManager::currentNM()->mkNode( - kind::STRING_CONCAT, - children0[0], - NodeManager::currentNM()->mkNode(kind::STRING_STRREPL, - mkConcat(kind::STRING_CONCAT, spl), - node[1], - node[2])); - return returnRewrite(node, ret, "rpl-prefix-nfind"); - } } else { |