diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-02-03 16:17:37 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-02-03 16:17:37 -0800 |
commit | b396d78982e109dc642611d32578bbca82b210cd (patch) | |
tree | e29dce4fdd0c2190860ddbc9f1c611f9eb443a83 /src/theory | |
parent | e374c7fbde3b3a5148b6e8fc302277b6e786965e (diff) |
Add rewrite for contains + const strings replace (#2828)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index f90d5bcfd..e8abc37a5 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -2041,8 +2041,7 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { if( node[0][i].isConst() ){ CVC4::String s = node[0][i].getConst<String>(); // if no overlap, we can split into disjunction - if (t.find(s) == std::string::npos && s.overlap(t) == 0 - && t.overlap(s) == 0) + if (s.noOverlapWith(t)) { std::vector<Node> nc0; getConcat(node[0], nc0); @@ -2080,6 +2079,19 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { } else if (node[0].getKind() == kind::STRING_STRREPL) { + if (node[1].isConst() && node[0][1].isConst() && node[0][2].isConst()) + { + String c = node[1].getConst<String>(); + if (c.noOverlapWith(node[0][1].getConst<String>()) + && c.noOverlapWith(node[0][2].getConst<String>())) + { + // (str.contains (str.replace x c1 c2) c3) ---> (str.contains x c3) + // if there is no overlap between c1 and c3 and none between c2 and c3 + Node ret = nm->mkNode(STRING_STRCTN, node[0][0], node[1]); + return returnRewrite(node, ret, "ctn-repl-cnsts-to-ctn"); + } + } + if (node[0][0] == node[0][2]) { // (str.contains (str.replace x y x) y) ---> (str.contains x y) |