diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-03 10:05:01 -0800 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-03 12:05:01 -0600 |
commit | d47530bd5924286781325cf2db3477e83a3c6d4f (patch) | |
tree | 25c709632df6029b6bccd94b22d7f21662c8adf8 /src/theory/strings | |
parent | 8a114b1899a5b31dfe733b0dd4ed897942e43f03 (diff) |
Rewrite `str.contains` used for character matching (#3519)
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 45 |
1 files changed, 45 insertions, 0 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 1e5b2a65a..fa3650b58 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -2048,6 +2048,7 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { NodeManager::currentNM()->mkConst(s.find(t) != std::string::npos); return returnRewrite(node, ret, "ctn-const"); }else{ + Node t = node[1]; if (s.size() == 0) { Node len1 = @@ -2061,6 +2062,50 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { return returnRewrite(node, ret, "ctn-lhs-emptystr"); } } + else if (checkEntailLengthOne(t)) + { + std::vector<unsigned> svec = s.getVec(); + std::sort(svec.begin(), svec.end()); + + 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++) + { + 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]; + } + } + + 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") + // if len(t) <= 1 + return returnRewrite(node, ret, "ctn-split"); + } else if (node[1].getKind() == kind::STRING_CONCAT) { int firstc, lastc; |