[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.

diff --git a/src/theory/strings/rewrites.cpp b/src/theory/strings/rewrites.cpp
index bfe9021aaf39b5ca389053f6f215d761d11df632..262459b4f6531f5348a27139c66600a1ee037790 100644 (file)
--- 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 b57c5f2765041963f6834857a28657a965a3e29b..eedd0fb402dd9c25295d6e6392d8039b5c6860cc 100644 (file)
--- 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 1094bd14d4e1c75021c438d473d732cd5a9c7d4b..374b43c34c18380587520f07b5faa4661aaa51bd 100644 (file)
--- 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 7c536454a5f58b219ee9518094439563951c3c9d..70331803c6b3c523edc002cee51471371e586dc3 100644 (file)
--- 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 (file)
index 0000000..7557086
--- /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)