=Paper=
{{Paper
|id=Vol-3725/short13
|storemode=property
|title=An SMT theory for N-Indexed Sequences
|pdfUrl=https://ceur-ws.org/Vol-3725/short13.pdf
|volume=Vol-3725
|authors=Hichem Rami Ait El Hara,François Bobot,Guillaume Bury
|dblpUrl=https://dblp.org/rec/conf/smt/HaraBB24
}}
==An SMT theory for N-Indexed Sequences==
https://ceur-ws.org/Vol-3725/short13.pdf
An SMT Theory for n-Indexed Sequences
Hichem Rami Ait El Hara1,2 , François Bobot2 and Guillaume Bury1
1
OCamlPro, Paris, France
2
UniversitΓ© Paris-Saclay, CEA, List, F-91120, Palaiseau, France
Abstract
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 efficient 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 different ways to represent and reason over n-indexed sequences using existing theories, as well as
tailored calculi for the theory.
1. Introduction
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.
Related work:
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].
SMT 2024: 22nd International Workshop on Satisfiability Modulo Theories
$ hra687261@gmail.com (H. R. Ait El Hara); francois.bobot@ocamlpro.com (F. Bobot); gbury@gmail.com (G. Bury)
Β https://hra687261.github.io/ (H. R. Ait El Hara); https://gbury.eu/ (G. Bury)
0000-0001-7909-0413 (H. R. Ait El Hara); 0000-0002-6756-0788 (F. Bobot); 0009-0002-1267-251X (G. Bury)
Β© 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
ceur-ws.org
Workshop ISSN 1613-0073
Proceedings
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].
2. Notation
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.
3. The Theory of n-Indexed Sequences
Table 1
The signature of the theory of n-indexed sequences
SMT-LIB symbol Sort
nseq.get NSeq E β Int β E
nseq.set NSeq E β Int β E β NSeq E
nseq.first NSeq E β Int
nseq.last NSeq E β Int
nseq.const Int β Int β E β NSeq E
nseq.relocate NSeq E β Int β NSeq E
nseq.concat NSeq E β NSeq E β NSeq E
nseq.slice NSeq E β Int β Int β NSeq E
nseq.update NSeq E β NSeq E β NSeq E
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 n-
sequence 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 n-
sequences π and π are equal if f π = f π and lπ = lπ ; otherwise, they are distinct.
4. Reasoning with existing theories
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):
(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:
(define-fun nseq.last (par (T) ((s (NSeq T))) Int
(+ (- (seq.len (nseq.seq s)) 1) (nseq.first s))))
(define-fun nseq.get (par (T) ((s (NSeq T)) (i Int)) T
(seq.nth (nseq.seq s) (- i (nseq.first s)))))
(define-fun nseq.set (par (T) ((s (NSeq T)) (i Int) (v T)) (NSeq T)
(nseq.mk (nseq.first s)
(seq.update (nseq.seq s) (- i (nseq.first s)) (seq.unit v)))))
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 ((f Int) (l Int) (v T))
(!
(let ((s (nseq.const f l v)))
(and
(= (nseq.first s) f)
(= (nseq.last s) l)
(forall ((i Int))
(=> (and (<= f i) (<= i l)) (= (nseq.get s i) v)))))
:pattern ((nseq.const f l v))))))
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.
5. Porting Calculi from the Seq Theory to the NSeq Theory
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.
5.1. Common calculus
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 β‘
lπ 2 = lπ 1 β f π 1 + f π 2 β§βπ : πΌππ‘, f π 1 β€ π β€ lπ 1 β πππ‘(π 1 , π) = πππ‘(π 2 , π β f π 1 + f π 2 )
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.
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 π = f π 1 β§ lπ = lπ 2 β§ f π 2 = lπ 1 +1
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 when lπ 2 < f π 2 (1)
π 1 :: π 2 β π 2 when lπ 1 < f π 1 (2)
π 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.
5.2. The base calculus
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(π, π, π£) π 1 = πππππππ‘π(π 2 , π)
Const-Bounds Reloc-Bounds
f π = π β§ lπ = π π = f π 2 β§π 1 = π 2 ||
π ΜΈ= f π 2 β§ f π 1 = π β§ lπ 1 = π + lπ 2 β f π 2
β§π 1 =πππππ π 2
π 1 = π ππππ(π , π, π)
NS-Slice
(π < f π β¨π < π β¨ lπ < π) β§ π 1 = π ||
f π β€ π β€ π β€ lπ β§π = π1 :: π 1 :: π2
π = ππππππ‘(π 1 , π 2 )
NS-Concat
lπ 1 < f π 1 β§π = π 2 ||
(lπ 2 < f π 2 β¨ lπ 1 +1 ΜΈ= f π 2 ) β§ π = π 1 ||
f π 1 β€ lπ 1 β§ f π 2 β€ lπ 2 β§ f π 2 = lπ 1 +1 β§ π = π 1 :: π 2
π 1 = π’ππππ‘π(π 2 , π )
NS-Update
(lπ < f π β¨ππ < f π 2 β¨ lπ 2 < lπ ) β§ π 1 = π 2 ||
f π 2 β€ f π β€ lπ β€ lπ 2 β§π 1 = π1 :: π :: π3 β§ π 2 = π1 :: π2 :: π3
π = π€ :: π¦1 :: π§1 π = π€ :: π¦2 :: π§2
NS-Split
lπ¦1 = lπ¦2 β§π¦1 = π¦2 ||
lπ¦1 > lπ¦2 β§π¦1 = π¦2 :: π β§ f π = lπ¦2 +1 β§ lπ = lπ¦1 ||
lπ¦1 < lπ¦2 β§π¦2 = π¦1 :: π β§ f π = lπ¦1 +1 β§ lπ = lπ¦2
π 1 = π1 :: π2 :: ... :: ππ π 1 =πππππ π 2
NS-Comp-Reloc
f π 1 = f π 2 β§π 1 = π 2 ||
π 2 = πππππππ‘π(π1 , f π 2 ) :: πππππππ‘π(π2 , f π2 β f π 1 + f π 2 ) :: ...
:: πππππππ‘π(ππ , f ππ β f π 1 + f π 2 )
Figure 1: Common inference rules for the NS-BASE and NS-EXT calculi
π£ = πππ‘(π , π)
R-Get
π < f π β¨ lπ < π ||
f π β€ π β€ lπ β§π = π1 :: ππππ π‘(π, π, π£) :: π2
π 1 = π ππ‘(π 2 , π, π£)
R-Set
(π < f π 2 β¨ lπ 2 < π) β§ π 1 = π 2 ||
f π 2 β€ π β€ lπ 2 β§ f π 1 = f π 2 β§ lπ 1 = lπ 2
π 1 = π1 :: ππππ π‘(π, π, π£) :: π3 β§ π 2 = π1 :: π2 :: π3
Figure 2: NS-BASE specific inference rules
5.3. The extended calculus
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
π£ = πππ‘(π , π) π = π€1 :: ... :: π€π
Get-Concat
π < f π β¨ lπ < π ||
f π€1 β€ π β€ lπ€1 β§πππ‘(π€1 , π) = π£ || ... ||
f π€π β€ π β€ lπ€π β§πππ‘(π€π , π) = π£
π 1 = π ππ‘(π 2 , π, π£) π 2 = π€1 :: ... :: π€π
Set-Concat
π < f π 2 β¨ lπ 2 < π ||
π 1 = π1 :: ... :: ππ β§ f π€1 β€ π β€ lπ€1 β§π1 = π ππ‘(π€1 , π, π£)β§
f π1 = f π€1 β§ lπ1 = lπ€1 β§... β§ f ππ = f π€π β§ lππ = lπ€π || ... ||
π 1 = π1 :: ... :: ππ β§ f π€π β€ π β€ lπ€π β§ππ = π ππ‘(π€π , π, π£)β§
f π1 = f π€1 β§ lπ1 = lπ€1 β§... β§ f ππ = f π€π β§ lππ = lπ€π
π 1 = π ππ‘(π 2 , π, π£) π 1 = π€1 :: ... :: π€π
Set-Concat-Inv
π < f π 2 β¨ lπ 2 < π ||
π 2 = π1 :: ... :: ππ β§ f π€1 β€ π β€ lπ€1 β§π€1 = π ππ‘(π1 , π, π£)β§
f π1 = f π€1 β§ lπ1 = lπ€1 β§... β§ f ππ = f π€π β§ lππ = lπ€π || ... ||
π 2 = π1 :: ... :: ππ β§ f π€π β€ π β€ lπ€π β§π€π = π ππ‘(ππ , π, π£)β§
f π1 = f π€1 β§ lπ1 = lπ€1 β§... β§ f ππ = f π€π β§ lππ = lπ€π
π = ππππ π‘(π, π, π£) π’ = πππ‘(π , π)
Get-Const
π < f π β¨ lπ < π || f π β€ π β€ lπ β§π’ = π£
π 1 = π ππ‘(π 2 , π, π£)
Get-Intro
π < f π 1 β¨ lπ 1 < π || f π 1 β€ π β€ lπ 1 β§π£ = πππ‘(π 1 , π)
π 1 = π ππ‘(π 2 , π, π£) π’ = πππ‘(π 1 , π)
Get-Set
π < f π 1 β¨ lπ 1 < π ||
π = π β§ f π 1 β€ π β€ lπ 1 β§π’ = π£ ||
π ΜΈ= π β§ f π 1 β€ π β€ lπ 1 β§π’ = πππ‘(π 2 , π)
π 1 = π ππ‘(π 2 , π, π£)
Set-Bound
π 1 = π 2 || f π 1 β€ π β€ lπ 1 β§πππ‘(π 2 , π) ΜΈ= π£
π£ = πππ‘(π 1 , π) π 1 =πππππ π 2
Get-Reloc
π < ππ β¨ ππ < π || ππ β€ π β€ ππ β§ π£ = πππ‘(π 2 , π β f π 1 β f π 2 )
Figure 3: NS-EXT specific inference rules
the operations affect 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.
6. Implementation
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
Figure 4: Number of solved goals by accumulated time in seconds on quantifier-free Seq benchmarks translated
from the QF_AX SMT-LIB benchmarks
offset from the representative, they are equal. The data structure maintains, for each equivalence
class, a mapping from offset to an element of the class that is at that specific relocation offset from the
representative. This facilitates efficient detection of such equalities with minimal overhead.
7. Experimental Results
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(π ): lπ β f π +1
β’ seq.nth(π , π): get(π , π)
β’ seq.update(π 1 , π, π 2 ):
let(π, relocate(π 2 , π), ite(f π 1 β€ π β€ lπ 1 β§ lπ 1 < lπ ,
update(π 1 , slice(π, π, lπ 1 )), update(π 1 , π)))
β’ seq.extract(π , π, π):
ite(π < f π β¨ lπ < π β¨ π β€ 0, π, slice(π , π, min(lπ , π + π β 1)))
β’ seq.++(π 1 , π 2 , π 3 , ..., π π ):
let(π1 , concat(π 1 , relocate(π 2 , lπ 1 +1)),
let(π2 , concat(π1 , relocate(π 3 , lπ1 +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 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 counterex-
amples 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.
8. Conclusion
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.
References
[1] N. BjΓΈrner, V. Ganesh, R. Michel, M. Veanes, An SMT-LIB Format for Sequences and Regular
Expressions, Strings (2012).
[2] H. R. Ait El Hara, F. Bobot, G. Bury, On SMT Theory Design: The Case of Sequences, in: Kalpa
Publications in Computing, volume 18, EasyChair, 2024, pp. 14β29. URL: https://easychair.org/
publications/paper/qdvJ. doi:10.29007/75tl, iSSN: 2515-1762.
[3] C. A. Furia, Whatβs Decidable about Sequences?, in: A. Bouajjani, W.-N. Chin (Eds.), Automated
Technology for Verification and Analysis, Springer, Berlin, Heidelberg, 2010, pp. 128β142. doi:10.
1007/978-3-642-15643-4_11.
[4] A. JeΕΌ, A. W. Lin, O. Markgraf, P. RΓΌmmer, Decision Procedures for Sequence Theories, in: C. Enea,
A. Lal (Eds.), Computer Aided Verification, Lecture Notes in Computer Science, Springer Nature
Switzerland, Cham, 2023, pp. 18β40. doi:10.1007/978-3-031-37703-7_2.
1
Available at: https://git.frama-c.com/pub/colibrics/-/tree/smt2024 (commit SHA: 43024e674ef26673d2495f3b186954fa37bc3890)
[5] Y. Sheng, A. NΓΆtzli, A. Reynolds, Y. Zohar, D. Dill, W. Grieskamp, J. Park, S. Qadeer, C. Barrett,
C. Tinelli, Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences, Journal
of Automated Reasoning 67 (2023) 32. URL: https://doi.org/10.1007/s10817-023-09682-2. doi:10.
1007/s10817-023-09682-2.
[6] T. Liang, A. Reynolds, C. Tinelli, C. Barrett, M. Deters, A DPLL(T) Theory Solver for a Theory
of Strings and Regular Expressions, volume 8559, Springer International Publishing, Cham,
2014, pp. 646β662. URL: http://link.springer.com/10.1007/978-3-319-08867-9_43. doi:10.1007/
978-3-319-08867-9_43, book Title: Computer Aided Verification Series Title: Lecture Notes
in Computer Science.
[7] M. Berzish, V. Ganesh, Y. Zheng, Z3str3: a string solver with theory-aware heuristics, in:
Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design, FMCAD β17,
FMCAD Inc, Austin, Texas, 2017, pp. 55β59.
[8] J. Christ, J. Hoenicke, Weakly Equivalent Arrays, in: C. Lutz, S. Ranise (Eds.), Frontiers of
Combining Systems, Lecture Notes in Computer Science, Springer International Publishing, Cham,
2015, pp. 119β134. doi:10.1007/978-3-319-24246-0_8.
[9] M. P. Bonacina, S. Graham-Lengrand, N. Shankar, CDSAT for Nondisjoint Theories
with Shared Predicates: Arrays With Abstract Length, Satisfiability Modulo Theo-
ries workshop, CEUR Workshop Proceedings 3185 (2022). URL: https://par.nsf.gov/biblio/
10358980-cdsat-nondisjoint-theories-shared-predicates-arrays-abstract-length.
[10] S. Ghilardi, A. Gianola, D. Kapur, C. Naso, Interpolation Results for Arrays with Length and
MaxDiff, ACM Transactions on Computational Logic 24 (2023) 28:1β28:33. URL: https://doi.org/10.
1145/3587161. doi:10.1145/3587161.
[11] A. R. Bradley, Z. Manna, H. B. Sipma, Whatβs Decidable About Arrays?, in: E. A. Emerson,
K. S. Namjoshi (Eds.), Verification, Model Checking, and Abstract Interpretation, Springer, Berlin,
Heidelberg, 2006, pp. 427β442. doi:10.1007/11609773_28.
[12] Q. Wang, A. W. Appel, A Solver for Arrays with Concatenation, Journal of Automated Reasoning 67
(2023) 4. URL: https://doi.org/10.1007/s10817-022-09654-y. doi:10.1007/s10817-022-09654-y.
A. Appendix
A.1. Representation of n-Indexed Sequences using Sequences and Algebraic Data
Types
(declare-datatypes ((NSeq 1))
((par (T) ((nseq.mk (nseq.first Int) (nseq.seq (Seq T)))))))
(define-fun nseq.last (par (T) ((s (NSeq T))) Int
(+ (- (seq.len (nseq.seq s)) 1) (nseq.first s))))
(define-fun nseq.get (par (T) ((s (NSeq T)) (i Int)) T
(seq.nth (nseq.seq s) (- i (nseq.first s)))))
(define-fun nseq.set (par (T) ((s (NSeq T)) (i Int) (v T)) (NSeq T)
(nseq.mk (nseq.first s)
(seq.update (nseq.seq s) (- i (nseq.first s)) (seq.unit v)))))
(declare-fun nseq.const (par (T) (Int Int T) (NSeq T)))
;; "nseq_const"
(assert (par (T) (forall ((f Int) (l Int) (v T))
(!
(let ((s (nseq.const f l v)))
(and
(= (nseq.first s) f)
(= (nseq.last s) l)
(forall ((i Int))
(=> (and (<= f i) (<= i l)) (= (nseq.get s i) v)))))
:pattern ((nseq.const f l v))))))
(define-fun nseq.relocate (par (T) ((s (NSeq T)) (f Int)) (NSeq T)
(nseq.mk f (nseq.seq s))))
(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)))