diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-18 19:59:09 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-19 00:59:09 +0000 |
| commit | 9ee8b184d9e97ae241ff079803b82859ed014dfa (patch) | |
| tree | c82137409293b477d606a111e0932158563ed9f9 /src/theory/strings/sequences_rewriter.cpp | |
| parent | 47f71a6d94b600cf7c132569fa05ad1666edc408 (diff) | |
Fix handling of non-standard re.range terms (#6563)
Fixes #6561. That benchmark now gives an error:
(error "expecting a single constant string term in regexp range").
This PR also makes isConstRegExp do a non-recursive dag traversal.
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) { |