From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 9 Feb 2022 04:58:23 +0000 (-0800)
Subject: [Seq] Fix rewrite of `(seq.nth s n)` for large `n` (#8083)
X-Git-Tag: cvc5-1.0.0~433
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b07543b20ab2e263035b75aca0b92636f5a9cdcb;p=cvc5.git

[Seq] Fix rewrite of `(seq.nth s n)` for large `n` (#8083)

When rewriting (seq.nth s n) where both terms are constants, cvc5 was
blindly converting the n to a uint32_t, which caused issues when n
was greater than the largest value that can be represented by a 32-bit
integer. This commit introduces a corresponding check and does not
perform the rewrite for large n.
---

diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 99978b015..d273df30a 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -1755,9 +1755,10 @@ Node SequencesRewriter::rewriteSeqNth(Node node)
     size_t len = Word::getLength(s);
     if (i.getConst<Rational>().sgn() != -1)
     {
-      size_t pos = i.getConst<Rational>().getNumerator().toUnsignedInt();
-      if (pos < len)
+      Integer posInt = i.getConst<Rational>().getNumerator();
+      if (posInt.fitsUnsignedInt() && posInt < Integer(len))
       {
+        size_t pos = posInt.toUnsignedInt();
         std::vector<Node> elements = s.getConst<Sequence>().getVec();
         const Node& ret = elements[pos];
         return returnRewrite(node, ret, Rewrite::SEQ_NTH_EVAL);
diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp
index 5ba583455..aee1ee75e 100644
--- a/test/unit/theory/sequences_rewriter_white.cpp
+++ b/test/unit/theory/sequences_rewriter_white.cpp
@@ -19,6 +19,7 @@
 
 #include "expr/node.h"
 #include "expr/node_manager.h"
+#include "expr/sequence.h"
 #include "test_smt.h"
 #include "theory/rewriter.h"
 #include "theory/strings/arith_entail.h"
@@ -228,7 +229,12 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_nth)
 
   Node zero = d_nodeManager->mkConstInt(0);
   Node one = d_nodeManager->mkConstInt(1);
+  // Position that is greater than the maximum value that can be represented
+  // with a uint32_t
+  Node largePos = d_nodeManager->mkConstInt(
+      static_cast<uint64_t>(std::numeric_limits<uint32_t>::max()) + 1);
 
+  Node s01 = d_nodeManager->mkConst(Sequence(intType, {zero, one}));
   Node sx = d_nodeManager->mkNode(SEQ_UNIT, x);
   Node sy = d_nodeManager->mkNode(SEQ_UNIT, y);
   Node sz = d_nodeManager->mkNode(SEQ_UNIT, z);
@@ -266,6 +272,14 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_nth)
     Node n = d_nodeManager->mkNode(SEQ_NTH, xyz, one);
     sameNormalForm(n, y);
   }
+
+  {
+    // Check that there are no errors when trying to rewrite
+    // (seq.nth (seq.++ (seq.unit 0) (seq.unit 1)) n) where n cannot be
+    // represented as a 32-bit integer
+    Node n = d_nodeManager->mkNode(SEQ_NTH, s01, largePos);
+    sameNormalForm(n, n);
+  }
 }
 
 TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr)