diff options
Diffstat (limited to 'src/theory/strings/theory_strings_rewriter.cpp')
-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 ); } |