In the SMT theory of sequences, sequences are viewed as a generalization of strings to non-character elements, with possibly infinite alphabets. Sequences are dynamically sized, and their theory has a rich signature. It allows selecting elements of a sequence by their index, concatenating two sequences, extracting sub-sequences, and performing other operations. The expressiveness of the theory of sequences makes it easier to represent various commonly found data structures in programming languages, such as arrays in the C language, lists in Python, etc.

The theory of arrays is less expressive as it only supports selecting and storing one value at one index at a time, and arrays have fixed sizes determined by the number of inhabitants of the sort of indices. In contrast, sequences have dynamic lengths and operations allowing the selection and updating of sets of indices at a time. To use the theory of arrays to represent sequences, one would need to extend it and axiomatize the necessary properties, such as dynamic length and additional operations like concatenation and extraction.

We are interested in a variant of the theory of sequences, which we call the theory of n-indexed sequences. They differ from sequences mainly in their indexing, as they are not necessarily 0-indexed but n-indexed, as their name suggests. This means they are defined as ordered collections of values of the same sort indexed from a first index 𝑛 to a last index 𝑚. Such sequences are present in some programming languages like Ada. Since there is no dedicated theory for such sequences, reasoning over them cannot be done straightforwardly using the existing theories of arrays and sequences. It is therefore necessary to use extensions and axiomatizations to reason over them.

In this paper, we will present the theory of n-indexed sequences, its signature and semantics, as well as different ways to reason over it using existing theories and by adapting calculi from the theory of sequences to the theory of n-indexed sequences.

The SMT theory of sequences was introduced by Bjorner et al. [1]. Several contributions explored this theory, its syntax and semantics [2], and its decidability [3,4].

Our theory of n-indexed sequences and the calculi we developed are based on the contribution by Sheng et al. [5], which in turn is based on reasoning about the theories of strings [6,7] and arrays [8]. Other contributions have extended the theory of arrays with properties that are present in sequences, such as length [9,10,11] and a concatenation function [12].

We refer to the theory of n-indexed sequences as the theory of n-sequences or the NSeq theory, and n-indexed sequence terms will be referred to as n-sequences, n-sequence terms, or NSeq terms. Their sort will be denoted as NSeq E, where E is the sort of the elements of the n-sequence. We will refer to the theory of sequences as the Seq theory. Int is the sort of integers from the theory of Linear Integer Arithmetic. min and max are the usual mathematical functions. ite is the ite SMT-LIB function; it takes a boolean expression and two expressions of the same sort and returns the first one if the boolean expression is true and the second otherwise. The let 𝑥 = 𝑣, 𝑦 symbol binds a variable 𝑥 to a value 𝑣 in a term 𝑦.

In the remainder of the paper, we will use 𝑠, 𝑠 𝑛 , 𝑤, 𝑤 𝑛 , 𝑦 1 , 𝑦 2 , 𝑧 1 , and 𝑧 2 to represent NSeq terms, with 𝑛 being a positive integer. 𝑘, 𝑘 1 , 𝑘 2 , and 𝑘 3 will represent fresh NSeq term variables. 𝑖 and 𝑗 will be used as integer index terms, and 𝑢 and 𝑣 will be used as NSeq element terms. We assume that all the terms we use are well-sorted. We present in this section the theory of n-indexed sequences. The signature of the NSeq theory is presented in the table 1. In the remainder of the paper, when referring to the symbols of the theory, the prefix "nseq." of the symbols will be omitted.

The following list describes the semantics of each symbol of the theory:

• f 𝑠 : the first index of 𝑠.

• l 𝑠 : the last index of 𝑠.

• get(𝑠, 𝑖): if the index 𝑖 is within the bounds of 𝑠, returns the element associated with 𝑖 in 𝑠; otherwise, returns an uninterpreted value. An uninterpreted value is one which is not constrained and can be any value of the right sort.

The theory of n-indexed sequences is extensional, which means that n-sequences that contain the same elements are equal. Therefore, given two n-sequences 𝑎 and 𝑏:

An n-sequence 𝑠 is said to be empty if l 𝑠 < f 𝑠 . Two empty nsequences 𝑎 and 𝑏 are equal if f 𝑎 = f 𝑏 and l 𝑎 = l 𝑏 ; otherwise, they are distinct.

One way to reason over the NSeq theory is by using the theory of arrays. It is done by extending it with the symbols of the NSeq theory and adding the right axioms that follow the semantics of the corresponding symbols in the NSeq theory.

Another way is to use the theory of sequences and the theory of algebraic data types. It consists in defining n-sequences as a pair of a sequence and the first index (the offset to zero):

The other symbols of the NSeq theory can also be defined using the NSeq data type defined above, for example: Except for the const function which needs to be axiomatized:

(declare-fun nseq.const (par (T) (Int Int T) (NSeq T)))

;; "nseq_const" (assert (par (T) (forall

The full NSeq theory, defined using the Seq theory and Algebraic Data Types, is attached in Appendix A.1.

Although this approach allows us to reason over n-indexed sequences, it is not ideal to depend on two theories to do so. Additionally, the differences in semantics between the update and 𝑠𝑙𝑖𝑐𝑒 functions of the NSeq theory, and the seq.update and seq.extract functions of the Seq theory, make the definitions relatively complex.

To develop our calculi over the NSeq theory, we based our work on the calculi developed by Sheng et al. [5] on the Seq theory, where two calculi were proposed. The first is called the BASE calculus, based on a string theory calculus that reduces functions selecting and storing one element at an index to concatenations of sequences. The second is called the EXT calculus, and it handles these functions using array-like reasoning. Our versions of these calculi are referred to as NS-BASE and NS-EXT, respectively.

The NSeq theory differs from the Seq theory in both syntax and semantics of many symbols:

• const and relocate do not appear in the Seq theory, while seq.empty, seq.unit, and seq.len do not appear in the NSeq theory. • The seq.nth function corresponds to the get function in the NSeq theory.

• seq.update from the Seq theory with a value as a third argument corresponds to set in the NSeq theory, while seq.update with a sequence as a third argument corresponds to update in the NSeq theory, which takes only two NSeq terms as arguments. • seq.extract in the Seq theory takes a sequence, an offset, and a length, and corresponds to slice in the NSeq theory, which takes an n-sequence, a first index, and a last index. • The concatenation function (seq.++) in Seq is n-ary, and it corresponds to concat in the NSeq theory, which is binary.

Therefore, we needed to make substantial changes to the Seq theory calculi to adapt them to the NSeq theory. In this section, we present the resulting calculi. We assume that we are in a theory combination framework where reasoning over the LIA (Linear Integer Arithmetic) theory is supported, and where unsatisfiability in one of the theories implies unsatisfiability of the entire reasoning. We will only present the rules that handle the symbols of the NSeq theory.

Definition 4 (Equivalence modulo relocation). Given two NSeq terms 𝑠 1 and 𝑠 2 , the terms are said to be equivalent modulo relocation, denoted with the equivalence relation 𝑠 1 = 𝑟𝑒𝑙𝑜𝑐 𝑠 2 , such that:

Equivalence modulo relocation represents equivalence between n-sequences relative to their starting index. Two n-sequences are equivalent modulo relocation if they have the same set of elements in the same order, but start at different indices.

For simplicity and consistency with Seq theory calculi, we introduce the concatenation operator :: with the invariant:

This operator is used to normalize NSeq terms. It differs from concat by not having to check the condition that f 𝑠 2 = l 𝑠 1 +1 before concatenation, as it is ensured by the invariant. Assumption 1. We assume that the following simplification rewrites are applied whenever possible:

) 𝑠 1 :: 𝑠 2 → 𝑠 1 :: 𝑤 1 :: ... :: 𝑤 𝑛 when 𝑠 2 = 𝑤 1 :: ... :: 𝑤 𝑛 (3) 𝑠 1 :: 𝑠 2 → 𝑤 1 :: ... :: 𝑤 𝑛 :: 𝑠 2 when 𝑠 1 = 𝑤 1 :: ... :: 𝑤 𝑛 (4)

(1) and (2) remove empty NSeq terms from normal form. (3) and (4) make sure that when an NSeq term appear in the normal of another NSeq term and has its own normal form, then it is replaced by its normal form.

Figure 1 illustrates a set of common rules shared between the two calculi NS-BASE and NS-EXT. The rules Const-Bounds and Reloc-Bounds propagate the bounds of constant and relocated n-sequences, which are created using the const and relocate functions, respectively. The rules NS-Slice, NS-Concat, and NS-Update handle slice, concat, and update by normalizing the NSeq terms under appropriate conditions. If an NSeq term has two normal forms where distinct terms begin at the same index but end at different indices, the NS-Split rule rewrites the longer term as a concatenation of the shorter one and a fresh variable. The NS-Comp-Reloc rule propagates concatenations over equivalence modulo relocation.

The base calculus comprises the rules in figures 1 and 2. The rules R-Get and R-Set handle the 𝑔𝑒𝑡 and 𝑠𝑒𝑡 operations by introducing a new normal form for the NSeq terms they operate on. In the R-Get rule, when 𝑖 is within the bounds of 𝑠, a new normal form of 𝑠 is introduced. It includes a constant NSeq term of size one at the 𝑖th position storing the value 𝑣, and two variables, 𝑘 1 and 𝑘 2 , to represent the left and right segments of NSeq term 𝑠 respectively. The R-Set rule operates similarly: when 𝑖 is within the bounds of 𝑠 2 , new normal forms are introduced for both 𝑠 1 and 𝑠 2 . These forms share two variables, 𝑘 1 and 𝑘 3 , representing segments on the left and right of the 𝑖th index. 𝑠 1 has a constant NSeq term of size one holding the value 𝑣 at the 𝑖th index, while 𝑠 2 introduces another variable, 𝑘 2 , of the same size and position.

Const-Bounds 𝑠 = const(𝑓, 𝑙, 𝑣)

The extended calculus consists of the rules in figures 1 and 3. It differs from the base calculus by handling the get and set functions similarly to how they are treated in the array decision procedure described in [8]. The Get-Intro rule introduces a get operation from a set operation. The Get-Set operation is equivalent to what is commonly referred to as the read-over-write or select-over-store rule in the Array theory, allowing the application of a get operation over a set operation. The Set-Bound rule ensures that a set operation is performed within the bounds of the target NSeq term, or that the resulting NSeq term is equivalent to the one it was applied on. The Get-Concat, Set-Concat, and Set-Concat-Inv rules illustrate how get and set operations are handled when applied to an NSeq term in normal form, where Get-Concat 𝑣 = 𝑔𝑒𝑡(𝑠, 𝑖) 𝑠 = 𝑤 1 :: ... ::

We have implemented a prototype of the described calculi in the Colibri2 CP (Constraint Programming) solver. In this section, we discuss some of the implementation choices we made.

The rewriting rules described in Assumption 1 are applied whenever applicable using a callback system. When the conditions are satisfied, the corresponding rewriting rule is triggered.

Equivalence modulo relocation is managed using a disjoint-set (union-find) data structure. In this data structure, the elements of the sets are NSeq terms, and the equivalence relation is defined by = 𝑟𝑒𝑙𝑜𝑐 as previously specified. By definition, if two elements of an equivalence class are at the same relocation

In this section, we present experimental results of the calculi described in the previous section. Currently, our experiments have focused exclusively on quantifier-free benchmarks that utilize only the theory of sequences and the theory of uninterpreted functions. These benchmarks constitute a subset of those employed in the paper [5], originally translated into the Seq theory from the QF_AX SMT-LIB benchmarks.

To achieve this, we implemented support for the Seq theory in our solver by translating Seq terms into NSeq terms. The translation process is as follows:

• Seq terms: NSeq terms for which the first index is 0 and the last index is greater or equal than −1.

• seq.empty: an NSeq term of the same sort, in which the first index is 0 and the last is −1, denoted 𝜖. • seq.unit(𝑣): const(0, 0, 𝑣) • seq.len(𝑠):

• seq.extract(𝑠, 𝑖, 𝑗):

The figure 4 depicts the number of satisfiable and unsatisfiable goals solved over accumulated time using our prototype implementation and the cvc5 SMT solver with different command-line options. NS-BASE and NS-EXT refer to our implementations1 , described in section 5, which can be used by running Colibri2 with the command-line options --nseq-base and --nseq-ext, respectively. We compare our implementation with the Seq theory implementation in cvc5 (version 1.1.1). In the graphs in figure 4, cvc5 corresponds to running cvc5 with the command-line option --strings-exp, necessary for using cvc5's solver for the Seq theory. cvc5-eager uses the same option with --seq-arrays=eager, and cvc5-lazy with --seq-arrays=lazy, these options indicate different strategies for using an array-inspired solver for the Seq theory.

Examining the graph on the right, which shows performance on unsatisfiable goals, we observe that our NS-EXT implementation outperforms cvc5 in both time and number of goals solved. Meanwhile, NS-BASE initially solves more goals than cvc5, but solves fewer overall. Additionally, cvc5-eager and cvc5-lazy solve more goals in less time compared to the others. The same trends apply to the satisfiable case, with the exception that cvc5 also surpasses NS-EXT in both time and number of goals solved once the 20-second threshold is reached.

In our context, focused on program verification, the performance on unsatisfiable goals holds greater significance, though the satisfiable case remains useful. Since Colibri2 constructs concrete counterexamples before concluding satisfiability, we aim to enhance our current model generation technique for n-sequences. In the unsatisfiable case, while we compete closely with the state-of-the-art SMT solver cvc5, we have observed that some goals unsolved within a short timeout (5 seconds) also remain unsolved with longer timeouts, suggesting potential performance limitations in our propagators for the NSeq theory. It's also notable that our translation from Seq to NSeq in Colibri2 introduces more complex terms, and Colibri2 lacks clause learning, making decisions costlier than in other SMT solvers.

In this paper, we explored the topic of n-indexed sequences in SMT. We proposed a theory for such sequences and discussed approaches for reasoning over it, whether by using existing theories or by adapting calculi from the theory of sequences to this theory.

Looking ahead, our future work will delve deeper into different reasoning approaches for this theory, exploring their respective strengths and weaknesses through benchmarking with n-indexed sequences. We aim to prove the correctness of our developed calculi and explore alternative methods for reasoning over n-sequences beyond traditional sequence or string reasoning. Moreover, we seek to identify additional applications for this theory beyond programming languages where n-indexed sequences are present.