diff options
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 16 | ||||
| -rw-r--r-- | src/util/regexp.h | 16 | ||||
| -rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 42 |
3 files changed, 72 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, diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index bbaa4733f..191d0ba58 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -650,6 +650,9 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node a = d_nm->mkConst(::CVC4::String("A")); Node b = d_nm->mkConst(::CVC4::String("B")); Node c = d_nm->mkConst(::CVC4::String("C")); + Node abc = d_nm->mkConst(::CVC4::String("ABC")); + Node def = d_nm->mkConst(::CVC4::String("DEF")); + Node ghi = d_nm->mkConst(::CVC4::String("GHI")); Node x = d_nm->mkVar("x", strType); Node y = d_nm->mkVar("y", strType); Node xy = d_nm->mkNode(kind::STRING_CONCAT, x, y); @@ -888,6 +891,45 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite d_nm->mkNode(kind::STRING_CONCAT, b, x)); sameNormalForm(ctn, f); } + + { + // Same normal form for: + // + // (str.contains (str.replace x "ABC" "DEF") "GHI") + // + // (str.contains x "GHI") + lhs = d_nm->mkNode(kind::STRING_STRCTN, + d_nm->mkNode(kind::STRING_STRREPL, x, abc, def), + ghi); + rhs = d_nm->mkNode(kind::STRING_STRCTN, x, ghi); + sameNormalForm(lhs, rhs); + } + + { + // Different normal forms for: + // + // (str.contains (str.replace x "ABC" "DEF") "B") + // + // (str.contains x "B") + lhs = d_nm->mkNode(kind::STRING_STRCTN, + d_nm->mkNode(kind::STRING_STRREPL, x, abc, def), + b); + rhs = d_nm->mkNode(kind::STRING_STRCTN, x, b); + differentNormalForms(lhs, rhs); + } + + { + // Different normal forms for: + // + // (str.contains (str.replace x "B" "DEF") "ABC") + // + // (str.contains x "ABC") + lhs = d_nm->mkNode(kind::STRING_STRCTN, + d_nm->mkNode(kind::STRING_STRREPL, x, b, def), + abc); + rhs = d_nm->mkNode(kind::STRING_STRCTN, x, abc); + differentNormalForms(lhs, rhs); + } } void testInferEqsFromContains() |