From 12f3384db0d6afade79252c28532ee6830fe767f Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Sun, 16 Jan 2022 19:55:27 -0800
Subject: [PATCH] [Strings] Fix rewriter for `re.loop` (#7956)

Fixes cvc5/cvc5-projects#409. Our
strings/sequences rewriter was applying rewrites for re.loop in the
wrong order. As a result, it rewrote ((_ re.loop 2 1) re.all) to
re.all instead of re.none as required by the SMT-LIB standard when
the lower bound is greater than the upper bound. This commit changes the
order s.t. the bounds check happens first.
---
 src/theory/strings/rewrites.cpp               |  1 +
 src/theory/strings/rewrites.h                 |  1 +
 src/theory/strings/sequences_rewriter.cpp     | 27 ++++++++++---------
 test/regress/CMakeLists.txt                   |  1 +
 .../strings/proj-issue409-re-loop-none.smt2   |  4 +++
 5 files changed, 22 insertions(+), 12 deletions(-)
 create mode 100644 test/regress/regress0/strings/proj-issue409-re-loop-none.smt2

diff --git a/src/theory/strings/rewrites.cpp b/src/theory/strings/rewrites.cpp
index bfe9021aa..262459b4f 100644
--- a/src/theory/strings/rewrites.cpp
+++ b/src/theory/strings/rewrites.cpp
@@ -91,6 +91,7 @@ const char* toString(Rewrite r)
     case Rewrite::RE_IN_SIGMA_STAR: return "RE_IN_SIGMA_STAR";
     case Rewrite::RE_IN_CHAR_MODULUS_STAR: return "RE_IN_CHAR_MODULUS_STAR";
     case Rewrite::RE_LOOP: return "RE_LOOP";
+    case Rewrite::RE_LOOP_NONE: return "RE_LOOP_NONE";
     case Rewrite::RE_LOOP_STAR: return "RE_LOOP_STAR";
     case Rewrite::RE_OR_ALL: return "RE_OR_ALL";
     case Rewrite::RE_SIMPLE_CONSUME: return "RE_SIMPLE_CONSUME";
diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h
index b57c5f276..eedd0fb40 100644
--- a/src/theory/strings/rewrites.h
+++ b/src/theory/strings/rewrites.h
@@ -94,6 +94,7 @@ enum class Rewrite : uint32_t
   RE_IN_SIGMA_STAR,
   RE_IN_CHAR_MODULUS_STAR,
   RE_LOOP,
+  RE_LOOP_NONE,
   RE_LOOP_STAR,
   RE_OR_ALL,
   RE_SIMPLE_CONSUME,
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 1094bd14d..374b43c34 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -1166,15 +1166,24 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node)
 Node SequencesRewriter::rewriteLoopRegExp(TNode node)
 {
   Assert(node.getKind() == REGEXP_LOOP);
-  Node retNode = node;
+  uint32_t l = utils::getLoopMinOccurrences(node);
+  uint32_t u = utils::getLoopMaxOccurrences(node);
   Node r = node[0];
-  if (r.getKind() == REGEXP_STAR)
+  Node retNode = node;
+
+  NodeManager* nm = NodeManager::currentNM();
+  if (u < l)
+  {
+    // ((_ re.loop l u) r) --> re.none if u < l
+    std::vector<Node> nvec;
+    retNode = nm->mkNode(REGEXP_NONE, nvec);
+    return returnRewrite(node, retNode, Rewrite::RE_LOOP_NONE);
+  }
+  else if (r.getKind() == REGEXP_STAR)
   {
     return returnRewrite(node, r, Rewrite::RE_LOOP_STAR);
   }
-  NodeManager* nm = NodeManager::currentNM();
-  cvc5::Rational rMaxInt(String::maxSize());
-  uint32_t l = utils::getLoopMinOccurrences(node);
+
   std::vector<Node> vec_nodes;
   for (unsigned i = 0; i < l; i++)
   {
@@ -1184,13 +1193,7 @@ Node SequencesRewriter::rewriteLoopRegExp(TNode node)
       vec_nodes.size() == 0
           ? nm->mkNode(STRING_TO_REGEXP, nm->mkConst(String("")))
           : vec_nodes.size() == 1 ? r : nm->mkNode(REGEXP_CONCAT, vec_nodes);
-  uint32_t u = utils::getLoopMaxOccurrences(node);
-  if (u < l)
-  {
-    std::vector<Node> nvec;
-    retNode = nm->mkNode(REGEXP_NONE, nvec);
-  }
-  else if (u == l)
+  if (u == l)
   {
     retNode = n;
   }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 7c536454a..70331803c 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1293,6 +1293,7 @@ set(regress_0_tests
   regress0/strings/parser-syms.cvc.smt2
   regress0/strings/proj-issue316-regexp-ite.smt2
   regress0/strings/proj-issue390-update-rev-rewrite.smt2
+  regress0/strings/proj-issue409-re-loop-none.smt2
   regress0/strings/re_diff.smt2
   regress0/strings/re-in-rewrite.smt2
   regress0/strings/re-syntax.smt2
diff --git a/test/regress/regress0/strings/proj-issue409-re-loop-none.smt2 b/test/regress/regress0/strings/proj-issue409-re-loop-none.smt2
new file mode 100644
index 000000000..75570864f
--- /dev/null
+++ b/test/regress/regress0/strings/proj-issue409-re-loop-none.smt2
@@ -0,0 +1,4 @@
+(set-logic QF_SLIA)
+(assert (str.in_re (str.from_code 0) ((_ re.loop 2 1) re.all)))
+(set-info :status unsat)
+(check-sat)
-- 
2.30.2