diff options
Diffstat (limited to 'src/theory/strings/sequences_rewriter.cpp')
-rw-r--r-- | src/theory/strings/sequences_rewriter.cpp | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index a0e627423..ff718c124 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -1312,12 +1312,16 @@ Node SequencesRewriter::rewriteMembership(TNode node) else if (r.getKind() == REGEXP_RANGE) { // x in re.range( char_i, char_j ) ---> i <= str.code(x) <= j - Node xcode = nm->mkNode(STRING_TO_CODE, x); - Node retNode = - nm->mkNode(AND, - nm->mkNode(LEQ, nm->mkNode(STRING_TO_CODE, r[0]), xcode), - nm->mkNode(LEQ, xcode, nm->mkNode(STRING_TO_CODE, r[1]))); - return returnRewrite(node, retNode, Rewrite::RE_IN_RANGE); + // we do not do this if the arguments are not constant + if (RegExpEntail::isConstRegExp(r)) + { + Node xcode = nm->mkNode(STRING_TO_CODE, x); + Node retNode = + nm->mkNode(AND, + nm->mkNode(LEQ, nm->mkNode(STRING_TO_CODE, r[0]), xcode), + nm->mkNode(LEQ, xcode, nm->mkNode(STRING_TO_CODE, r[1]))); + return returnRewrite(node, retNode, Rewrite::RE_IN_RANGE); + } } else if (r.getKind() == REGEXP_COMPLEMENT) { |