From: Andrew Reynolds Date: Wed, 19 May 2021 19:42:21 +0000 (-0500) Subject: Fix strings rewriter for non-standard re range (#6570) X-Git-Tag: cvc5-1.0.0~1738 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=64d727b9dc07bfde5d8a1c326f5fcfe0d1a79a4b;p=cvc5.git 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. --- 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().size() != 1) + { + // not applied to characters, it is not handled + return node; + } + ch[i] = node[i].getConst().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().size() != 1) - { - appliedCh = false; - break; - } - ch[i] = node[i].getConst().front(); - } - if (appliedCh && ch[0] > ch[1]) + if (ch[0] > ch[1]) { // re.range( "B", "A" ) ---> re.none Node retNode = nm->mkNode(REGEXP_EMPTY, {});