From 196d12720518e80fac6dd6e33351460b608e7a99 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 6 Dec 2019 16:55:31 -0800 Subject: test rewrite --- src/theory/strings/theory_strings_rewriter.cpp | 13 +++++++++---- 1 file 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 endStr = r[1].getConst(); + NodeBuilder<> nb(OR); + for (unsigned i = startStr.front(), end = endStr.front(); i <= end; i++) + { + std::vector 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 ); } -- cgit v1.2.3