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 | |
parent | e374c7fbde3b3a5148b6e8fc302277b6e786965e (diff) |
Add rewrite for contains + const strings replace (#2828)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 16 | ||||
-rw-r--r-- | src/util/regexp.h | 16 |
2 files changed, 30 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) diff --git a/src/util/regexp.h b/src/util/regexp.h index 2ab6b659c..1588b5174 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -149,6 +149,22 @@ class CVC4_PUBLIC String { String prefix(std::size_t i) const { return substr(0, i); } String suffix(std::size_t i) const { return substr(size() - i, i); } + + /** + * Checks if there is any overlap between this string and another string. This + * corresponds to checking whether one string contains the other and wether a + * substring of one is a prefix of the other and vice-versa. + * + * @param y The other string + * @return True if there is an overlap, false otherwise + */ + bool noOverlapWith(const String& y) const + { + return y.find(*this) == std::string::npos + && this->find(y) == std::string::npos && this->overlap(y) == 0 + && y.overlap(*this) == 0; + } + /** string overlap * * if overlap returns m>0, |