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. bit-vectors.
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 n-th 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
sub-sequence 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 sub-sequence of s that starts at
index i and has length at most j,
in case both i and j are non-negative 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 i-th 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 sub-sequence 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
.
SMT-LIB 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 |
|
|
Sub-sequence with single element |
|
|
Sequence containment |
|
|
Sequence indexof |
|
|
Sub-sequence replace |
|
|
Sub-sequence replace all |
|
|
Sequence reverse |
|
|
Sequence prefix of |
|
|
Sequence suffix of |
|
|
Examples
(set-logic QF_SLIA)
(set-info :status unsat)
(declare-fun x () (Seq Int))
(declare-fun y () (Seq Int))
(declare-fun z () (Seq Int))
(declare-fun a () Int)
(declare-fun 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))
(check-sat)
(set-logic QF_SLIA)
(set-info :status unsat)
(declare-fun A () (Seq Int))
(declare-fun S () (Seq Int))
(declare-fun 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)))
(check-sat)
(set-logic QF_SLIA)
(set-info :status unsat)
(declare-fun x () (Seq Int))
(declare-fun y () (Seq Int))
(declare-fun a () Int)
(declare-fun b () Int)
(assert (= (seq.++ (seq.unit a) y) (seq.update x 0 (seq.unit b))))
(assert (not (= a b)))
(check-sat)