From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
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<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, {});