The SMT (Satisfiability Modulo Theories) theory of arrays is well-established and widely used, with various decision procedures and extensions developed for it. However, recent works suggest that developing tailored reasoning for some theories, such as sequences and strings, is more eficient than reasoning over them through axiomatization over the theory of arrays. In this paper, we are interested in reasoning over n-indexed sequences as they are found in some programming languages, such as Ada. We propose an SMT theory of n-indexed sequences and explore diferent ways to represent and reason over n-indexed sequences using existing theories, as well as tailored calculi for the theory.
The SMT theory of sequences was introduced by Bjorner et al. [
Our theory of n-indexed sequences and the calculi we developed are based on the contribution by
Sheng et al. [
Other contributions have extended the theory of arrays with properties that are present in sequences,
such as length [
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. • set(, , ): if is within the bounds of , creates a new n-sequence in which is associated with , and the other indices within the bounds are associated with the same values as the corresponding indices in ; otherwise, returns . • const(, , ): creates an n-sequence with as the first index and as the last, and if it is not empty, all the indices within its bounds are associated with the value . • relocate(, ): given an n-sequence and an index , returns a new n-sequence which has as its first index and ( + l − f) as its last index, and associates with each index within the bounds of the same value associated with the index ( − f + f) in . • concat(, ): if is empty, returns ; if is empty, returns ; if f = l +1, returns a new nsequence in which the first index is f, the last index is l, and all the indices within the bounds of are associated with the same values as the corresponding indices in , as well as the indices within the bounds of are associated with the same values as the corresponding indices in ; if f ̸= l +1, returns . • slice(, , ): if f ≤ ≤ ≤ l, returns a new n-sequence for which the first index is , the last index is , and all the indices between and are associated with the same values as the corresponding indices in ; otherwise, returns . • update(, ): if is empty, or is empty, or the property f ≤ f ≤ l ≤ l doesn’t hold, returns ; otherwise, returns a new n-sequence such that f = f and l = l, and for all the indices within the bounds of , if they are within the bounds of , then they are associated with the same values as they are in , otherwise they are associated with the values to which they are associated in .
Definition 1 (Bounds). The bounds of an n-sequence are its first and last index, which are respectively denoted as f and l, and which correspond to the values returned by the functions nseq.first() and nseq.last() respectively. An index is said to be within the bounds of an n-sequence if: f ≤ ≤ l Definition 2 (Extensionality). 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 : f = f ∧ l = l ∧ (∀ : Int, f ≤ ≤ l → get(, ) = get(, ))
→ = Definition 3 (Empty n-sequence). 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 ofset to zero): (declare-datatype NSeq (par (T) ((nseq.mk (nseq.first Int) (nseq.seq (Seq T))))))
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:
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 diferences 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.
[
The NSeq theory difers 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 ofset, 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: 1 = 2 ≡ l2 = l1 − f1 + f2 ∧∀ : , f1 ≤ ≤ l1 ⇒ (1, ) = (2, − f1 + f2 ) 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 diferent indices.
Definition 5 ( NSeq term normal form). For simplicity and consistency with Seq theory calculi, we introduce the concatenation operator :: with the invariant: = 1 :: 2 =⇒
f = f1 ∧ l = l2 ∧ f2 = l1 +1 This operator is used to normalize NSeq terms. It difers from concat by not having to check the condition that f2 = l1 +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 :: 2 1 :: 2 1 :: 2 → 1 → 2 → 1 :: 1 :: ... :: → 1 :: ... :: :: 2 when l2 < f2 (1) when l1 < f1 (2) when 2 = 1 :: ... :: (3) 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.
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(, , ) f = ∧ l =
NS-Slice 1 = (2, ) = f2 ∧1 = 2 ̸= f2 ∧ f1 = ∧ l1 = + l2 − f2 ∧1 = 2
|| 1 = (, , ) ( < f ∨ < ∨ l < ) ∧ 1 = || f ≤ ≤ ≤ l ∧ = 1 :: 1 :: 2 NS-Update
NS-Concat
NS-Split NS-Comp-Reloc
= (1, 2) l1 < f1 ∧ = 2 (l2 < f2 ∨ l1 +1 ̸= f2 ) ∧ = 1 f1 ≤ l1 ∧ f2 ≤ l2 ∧ f2 = l1 +1 ∧ = 1 :: 2 || || 1 = (2, ) (l < f ∨ < f2 ∨ l2 < l) ∧ 1 = 2 f2 ≤ f ≤ l ≤ l2 ∧1 = 1 :: :: 3 ∧ 2 = 1 :: 2 :: 3 || = :: 1 :: 1
= :: 2 :: 2 l1 = l2 ∧1 = 2 || l1 > l2 ∧1 = 2 :: ∧ f = l2 +1 ∧ l = l1 || l1 < l2 ∧2 = 1 :: ∧ f = l1 +1 ∧ l = l2 1 = 1 :: 2 :: ... ::
The extended calculus consists of the rules in figures 1 and 3. It difers from the base calculus by handling
the get and set functions similarly to how they are treated in the array decision procedure described
in [
Set-Concat Set-Concat-Inv
= 1 :: ... :: 1 = (2, , )
2 = 1 :: ... :: < f2 ∨ l2 < 1 = 1 :: ... :: ∧ f1 ≤ ≤ l1 ∧1 = (1, , )∧
f1 = f1 ∧ l1 = l1 ∧... ∧ f = f ∧ l = l 1 = 1 :: ... :: ∧ f ≤ ≤ l ∧ = (, , )∧ f1 = f1 ∧ l1 = l1 ∧... ∧ f = f ∧ l = l the operations afect the right component of the concatenation within its bounds. The Get-Const rule addresses the special case where a get operation is applied to a constant NSeq term. The Get-Reloc rule facilitates the propagation of constraints on index-associated values in NSeq terms from one term to others that are equivalent modulo relocation.
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 ofset from the representative, they are equal. The data structure maintains, for each equivalence class, a mapping from ofset to an element of the class that is at that specific relocation ofset from the representative. This facilitates eficient detection of such equalities with minimal overhead.
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 [
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(): l − f +1 • seq.nth(, ): get(, ) • seq.update(1, , 2): • seq.extract(, , ): • seq.++(1, 2, 3, ..., ): let(, relocate(2, ), ite(f1 ≤ ≤ l1 ∧ l1 < l,
update(1, slice(, , l1 )), update(1, ))) ite( < f ∨ l < ∨ ≤ 0, , slice(, , min(l, + − 1))) let(1, concat(1, relocate(2, l1 +1)), let(2, concat(1, relocate(3, l1 +1)),
...
concat(− 2, relocate(, l− 2 +1))))
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 diferent command-line options. NSBASE 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 diferent 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 diferent 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. 1Available at: https://git.frama-c.com/pub/colibrics/-/tree/smt2024 (commit SHA: 43024e674ef26673d2495f3b186954fa37bc3890)
(declare-datatypes ((NSeq 1))
((par (T) ((nseq.mk (nseq.first Int) (nseq.seq (Seq T))))))) (declare-fun nseq.const (par (T) (Int Int T) (NSeq T))) (define-fun nseq.concat (par (T) ((s1 (NSeq T)) (s2 (NSeq T))) (NSeq T) (ite (< (nseq.last s1) (nseq.first s1)) s2 (ite (or (< (nseq.last s2) (nseq.first s2)) (not (= (nseq.first s2) (+ (nseq.last s1) 1)))) s1 (nseq.mk (nseq.first s1) (seq.++ (nseq.seq s1) (nseq.seq s2))))))) (define-fun nseq.slice (par (T) ((s (NSeq T)) (f Int) (l Int)) (NSeq T) (ite (and (<= f l) (and (<= (nseq.first s) f) (<= l (nseq.last s)))) (nseq.mk f (seq.extract (nseq.seq s) (- f (nseq.first s)) (+ (- l f) 1))) s))) (define-fun nseq.update (par (T) ((s1 (NSeq T)) (s2 (NSeq T))) (NSeq T) (ite (and (<= (nseq.first s2) (nseq.last s2)) (<= (nseq.first s1) (nseq.first s2)) (<= (nseq.last s2) (nseq.last s1))) (nseq.mk (nseq.first s1) (seq.update (nseq.seq s1) (- (nseq.first s2) (nseq.first s1)) (nseq.seq s2))) s1)))