diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-06 16:55:31 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-06 16:55:31 -0800 |
commit | 196d12720518e80fac6dd6e33351460b608e7a99 (patch) | |
tree | ab49365649c296f9cd59f0b46cf9fd974910ebfb /src | |
parent | 642ac587031771ff655109892d1f306b060c12a8 (diff) |
test rewriterewContains
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 463b65a0a..f90d39ee6 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1476,10 +1476,15 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { else if (options::useCode() && r.getKind() == REGEXP_RANGE) { // x in re.range( char_i, char_j ) ---> i <= str.code(x) <= j - Node xcode = nm->mkNode(STRING_CODE, x); - retNode = nm->mkNode(AND, - nm->mkNode(LEQ, nm->mkNode(STRING_CODE, r[0]), xcode), - nm->mkNode(LEQ, xcode, nm->mkNode(STRING_CODE, r[1]))); + String startStr = r[0].getConst<String>(); + String endStr = r[1].getConst<String>(); + NodeBuilder<> nb(OR); + for (unsigned i = startStr.front(), end = endStr.front(); i <= end; i++) + { + std::vector<unsigned> sv = {c}; + nb << x.eqNode(nm->mkConst(String(sv))); + } + retNode = nb; }else if(x != node[0] || r != node[1]) { retNode = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, r ); } |