Dynamic arrays, also referred to as vectors, are fundamental data structures used in many programs. Modeling their semantics efficiently is crucial when reasoning about such programs. The theory of arrays is widely supported but is not ideal, because the number of elements is fixed (determined by its index sort) and cannot be adjusted, which is a problem, given that the length of vectors often plays an important role when reasoning about vector programs. In this paper, we propose reasoning about vectors using a theory of sequences. We introduce the theory, propose a basic calculus adapted from one for the theory of strings, and extend it to efficiently handle common vector operations. We prove that our calculus is sound and show how to construct a model when it terminates with a saturated configuration. Finally, we describe an implementation of the calculus in cvc5 and demonstrate its efficacy by evaluating it on verification conditions for smart contracts and benchmarks derived from existing array benchmarks.

翻译：动态数组,也称为矢量,是许多程序使用的基本数据结构。在对此类程序进行推理时,对其语义进行高效建模至关重要。阵列理论得到广泛支持,但并不理想,因为元素数量是固定的(根据其指数种类确定),无法调整,这是一个问题,因为矢量长度在矢量程序推理时往往起着重要作用。在本文中,我们提出使用序列理论的矢量推理。我们引入了理论,提出了从一个角度对字符串理论进行调整的基本微积分,并将它扩大到高效处理共同矢量操作。我们证明我们的计数是健全的,并展示了如何在元素以饱和配置终止时构建模型。最后,我们描述了在 cvc5 中对矢量计的计算结果的落实情况,并通过对现有阵列基准的智能合同和基准的核查条件进行评估来展示其有效性。