diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-19 14:42:21 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-19 19:42:21 +0000 |
commit | 64d727b9dc07bfde5d8a1c326f5fcfe0d1a79a4b (patch) | |
tree | cfa42ee1239ce63e33d18ee01e0afd4a8fe151c5 /src | |
parent | 9bbf41fb6cb5a33cfbfc3a711b82a4783a61b66f (diff) |
Fix strings rewriter for non-standard re range (#6570)
Fixes #6561.
Previously we missed a case where a rewrite fired for (re.range x x) where x is not a character.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/strings/sequences_rewriter.cpp | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 1577a5625..e827e87d3 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -1129,6 +1129,17 @@ Node SequencesRewriter::rewriteDifferenceRegExp(TNode node) Node SequencesRewriter::rewriteRangeRegExp(TNode node) { Assert(node.getKind() == REGEXP_RANGE); + unsigned ch[2]; + for (size_t i = 0; i < 2; ++i) + { + if (!node[i].isConst() || node[i].getConst<String>().size() != 1) + { + // not applied to characters, it is not handled + return node; + } + ch[i] = node[i].getConst<String>().front(); + } + NodeManager* nm = NodeManager::currentNM(); if (node[0] == node[1]) { @@ -1137,18 +1148,7 @@ Node SequencesRewriter::rewriteRangeRegExp(TNode node) return returnRewrite(node, retNode, Rewrite::RE_RANGE_SINGLE); } - bool appliedCh = true; - unsigned ch[2]; - for (size_t i = 0; i < 2; ++i) - { - if (node[i].isConst() || node[i].getConst<String>().size() != 1) - { - appliedCh = false; - break; - } - ch[i] = node[i].getConst<String>().front(); - } - if (appliedCh && ch[0] > ch[1]) + if (ch[0] > ch[1]) { // re.range( "B", "A" ) ---> re.none Node retNode = nm->mkNode(REGEXP_EMPTY, {}); |