From b07543b20ab2e263035b75aca0b92636f5a9cdcb Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 8 Feb 2022 20:58:23 -0800 Subject: [PATCH] [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. --- src/theory/strings/sequences_rewriter.cpp | 5 +++-- test/unit/theory/sequences_rewriter_white.cpp | 14 ++++++++++++++ 2 files changed, 17 insertions(+), 2 deletions(-) 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().sgn() != -1) { - size_t pos = i.getConst().getNumerator().toUnsignedInt(); - if (pos < len) + Integer posInt = i.getConst().getNumerator(); + if (posInt.fitsUnsignedInt() && posInt < Integer(len)) { + size_t pos = posInt.toUnsignedInt(); std::vector elements = s.getConst().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(std::numeric_limits::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) -- 2.30.2