Theory Reference: Sequences
Note
cvc5 currently only supports sequences where the element sort either has an infinite domain, e.g., sequences of integers, or a finite domain of a fixed cardinality, e.g. bitvectors.
Semantics
* (seq.empty (Seq S))
⟦seq.empty⟧ = []
* (seq.unit S (Seq S))
⟦seq.unit⟧(x) = [x]
* (seq.len (Seq S) Int)
⟦seq.len⟧(s) is the length of the sequence s, denoted as s.
* (seq.nth ((Seq S) Int) S)
⟦seq.nth⟧(s, i) is the nth element in the sequence s,
denoted as nth(s, i).
It is uninterpreted if i out of bounds,
i.e. i < 0 or i >= s.
* (seq.update ((Seq S) Int (Seq S)) (Seq S))
⟦seq.update⟧(s, i, sub) is a sequence obtained by updating the continuous
subsequence of s starting at index i by sub.
The updated sequence has the same length as s.
If i + sub > s,
the out of bounds part of sub is ignored.
If i out of bounds, i.e. i < 0 or i >= s,
the updated sequence remains same with s.
* (seq.extract ((Seq S) Int Int) (Seq S))
⟦seq.extract⟧(s, i, j) is the maximal subsequence of s that starts at
index i and has length at most j,
in case both i and j are nonnegative and i is
smaller than s.
Otherwise, the return value is the empty sequence.
* (seq.++ ((Seq S) (Seq S)) (Seq S))
⟦seq.++⟧(s1, s2) is a sequence that is the concatenation of s1 and s2.
* (seq.at ((Seq S) Int) (Seq S))
⟦seq.at⟧(s, i) is a unit sequence that contains the ith element of s as
the only element, or is the empty sequence if i < 0 or i > s.
* (seq.contains ((Seq S) (Seq S)) Bool)
⟦seq.contains⟧(s, sub) is true if sub is a continuous subsequence of s,
i.e. sub = seq.extract(s, i, j) for some i, j,
and false if otherwise.
* (seq.indexof ((Seq S) (Seq S) Int) Int)
⟦seq.indexof⟧(s, sub, i) is the first position of sub at or after i in s,
and 1 if there is no occurrence.
* (seq.replace ((Seq S) (Seq S) (Seq S)) (Seq S))
⟦seq.replace⟧(s, src, dst) is the sequence obtained by replacing the
first occurrence of src by dst in s.
It is s if there is no occurrence.
* (seq.replace_all ((Seq S) (Seq S) (Seq S)) (Seq S))
⟦seq.replace_all⟧(s, src, dst) is the sequence obtained by replacing all
the occurrences of src by dst in s,
in the order from left to right.
It is s if there is no occurrence.
* (seq.rev (Seq S) (Seq S))
⟦seq.rev⟧(s) is the sequence obtained by reversing s.
* (seq.prefixof ((Seq S) (Seq S)) Bool)
⟦seq.prefixof⟧(pre s) is true if pre is a prefix of s, false otherwise.
* (seq.suffixof ((Seq S) (Seq S)) Bool)
⟦seq.suffixof⟧(suf s) is true if suf is a suffix of s, false otherwise.
Syntax
For the C++ API examples in the table below, we assume that we have created
a
Solver
object
solver
.
SMTLIB language 
C++ API 

Logic String 
use S for sequences and strings

use S for sequences and strings

Sort 


Constants 


Empty sequence 


Unit sequence 


Sequence length 


Element access 


Element update 


Extraction 


Concatenation 


Subsequence with single element 


Sequence containment 


Sequence indexof 


Subsequence replace 


Subsequence replace all 


Sequence reverse 


Sequence prefix of 


Sequence suffix of 


Examples
(setlogic QF_SLIA)
(setinfo :status unsat)
(declarefun x () (Seq Int))
(declarefun y () (Seq Int))
(declarefun z () (Seq Int))
(declarefun a () Int)
(declarefun b () Int)
(assert (= y (seq.update x 0 (seq.unit a))))
(assert (= z (seq.update x 0 (seq.unit b))))
(assert (not (= a b)))
(assert (= y z))
(assert (> (seq.len y) 0))
(checksat)
(setlogic QF_SLIA)
(setinfo :status unsat)
(declarefun A () (Seq Int))
(declarefun S () (Seq Int))
(declarefun i () Int)
(assert (<= 0 i))
(assert (< i ( (seq.len A) 1)))
(assert (= S (seq.extract A i 1)))
(assert (distinct (seq.nth S 0) (seq.nth A i)))
(checksat)
(setlogic QF_SLIA)
(setinfo :status unsat)
(declarefun x () (Seq Int))
(declarefun y () (Seq Int))
(declarefun a () Int)
(declarefun b () Int)
(assert (= (seq.++ (seq.unit a) y) (seq.update x 0 (seq.unit b))))
(assert (not (= a b)))
(checksat)