diff options
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 40 | ||||
| -rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 27 |
2 files changed, 13 insertions, 54 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index fa3650b58..5ae0d87b3 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -2064,46 +2064,20 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { } else if (checkEntailLengthOne(t)) { - std::vector<unsigned> svec = s.getVec(); - std::sort(svec.begin(), svec.end()); + const std::vector<unsigned>& vec = s.getVec(); NodeBuilder<> nb(OR); nb << nm->mkConst(String("")).eqNode(t); - - Node tc = nm->mkNode(STRING_CODE, t); - unsigned lb = svec[0]; - unsigned curr = lb; - for (size_t i = 0, size = svec.size(); i <= size; i++) + for (unsigned c : vec) { - if (i == size || (svec[i] != curr && svec[i] != curr + 1)) - { - Node nlb = nm->mkConst(Rational(CVC4::String::convertUnsignedIntToCode(lb))); - Node nub = nm->mkConst(Rational(CVC4::String::convertUnsignedIntToCode(svec[i - 1]))); - if (nlb == nub) - { - nb << nm->mkNode(EQUAL, tc, nlb); - } - else - { - nb << nm->mkNode( - AND, nm->mkNode(LEQ, nlb, tc), nm->mkNode(LEQ, tc, nub)); - } - - if (i != size) { - lb = svec[i]; - curr = lb; - } - } else { - curr = svec[i]; - } + std::vector<unsigned> sv = {c}; + nb << nm->mkConst(String(sv)).eqNode(t); } - Node ret = nb; - - // str.contains("ABCDEFabcdef", t) ---> - // t = "" v str.code("A") <= str.code(t) <= str.code("F") v - // str.code("a") <= str.code(t) <= str.code("f") + // str.contains("ABCabc", t) ---> + // t = "" v t = "A" v t = "B" v t = "C" v t = "a" v t = "b" v t = "c" // if len(t) <= 1 + Node ret = nb; return returnRewrite(node, ret, "ctn-split"); } else if (node[1].getKind() == kind::STRING_CONCAT) diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index b5eb92900..d71df524c 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -710,7 +710,6 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite 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 abbchijp = d_nm->mkConst(::CVC4::String("ABBCHIJP")); Node x = d_nm->mkVar("x", strType); Node y = d_nm->mkVar("y", strType); Node xy = d_nm->mkNode(kind::STRING_CONCAT, x, y); @@ -1009,31 +1008,17 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite { // Same normal form for: // - // (str.contains "ABBCHIJP" (str.at x n)) + // (str.contains "ABC" (str.at x n)) // // (or (= x "") - // (and (<= (str.code "A") (str.code (str.at x n))) - // (<= (str.code (str.at x n)) (str.code "C"))) - // (and (<= (str.code "H") (str.code (str.at x n))) - // (<= (str.code (str.at x n)) (str.code "J"))) - // (= (str.code (str.at x n)) (str.code "P"))) + // (= x "A") (= x "B") (= x "C")) Node cat = d_nm->mkNode(kind::STRING_CHARAT, x, n); - lhs = d_nm->mkNode(kind::STRING_STRCTN, abbchijp, cat); - Node ca = d_nm->mkNode(kind::STRING_CODE, a); - Node cc = d_nm->mkNode(kind::STRING_CODE, c); - Node ch = d_nm->mkNode(kind::STRING_CODE, h); - Node cj = d_nm->mkNode(kind::STRING_CODE, j); - Node cp = d_nm->mkNode(kind::STRING_CODE, p); - Node ccat = d_nm->mkNode(kind::STRING_CODE, cat); + lhs = d_nm->mkNode(kind::STRING_STRCTN, abc, cat); rhs = d_nm->mkNode(kind::OR, d_nm->mkNode(kind::EQUAL, cat, empty), - d_nm->mkNode(kind::AND, - d_nm->mkNode(kind::LEQ, ca, ccat), - d_nm->mkNode(kind::LEQ, ccat, cc)), - d_nm->mkNode(kind::AND, - d_nm->mkNode(kind::LEQ, ch, ccat), - d_nm->mkNode(kind::LEQ, ccat, cj)), - d_nm->mkNode(kind::EQUAL, ccat, cp)); + d_nm->mkNode(kind::EQUAL, cat, a), + d_nm->mkNode(kind::EQUAL, cat, b), + d_nm->mkNode(kind::EQUAL, cat, c)); sameNormalForm(lhs, rhs); } } |