Sequences 

Basic Sequence Term Builders 

cvc5.pythonic. SeqSort ( s ) 

Create a sequence sort over elements provided in the argument >>> s = SeqSort(IntSort()) >>> s == Unit(IntVal(1)).sort() True

cvc5.pythonic. Unit ( a ) 

Create a singleton sequence

>>> i = Unit(IntVal(1))
>>> i.sort()
(Seq Int)

Sequence Operators 

cvc5.pythonic. Empty ( s ) 

Create the empty sequence of the given sort

>>> e = Empty(StringSort())
>>> e2 = StringVal("")
>>> print(e.eq(e2))
True
>>> e3 = Empty(SeqSort(IntSort()))
>>> print(e3)
(as seq.empty (Seq Int))()

cvc5.pythonic. Length ( s , ctx = None ) 

obtain the length of a string or sequence s

>>> s = StringVal('s')
>>> l = Length(s)
>>> simplify(l)
1

cvc5.pythonic. SubSeq ( s , offset , length ) 

Extract subsequence starting at offset

>>> seq = Concat(Unit(IntVal(1)),Unit(IntVal(2)))
>>> simplify(SubSeq(seq,1,1))
(seq.unit 2)()
>>> simplify(SubSeq(seq,1,0))
(as seq.empty (Seq Int))()

cvc5.pythonic. SeqUpdate ( s , t , i ) 

Update a sequence s by replacing its content starting at index i with sequence t.

>>> lst = Unit(IntVal(1)) + Unit(IntVal(2)) + Unit(IntVal(3))
>>> simplify(lst)
(seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3))()
>>> simplify(SeqUpdate(lst,Unit(IntVal(4)),2))
(seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 4))()
>>> simplify(SeqUpdate(lst,Unit(IntVal(1)),4))
(seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3))()

See the following operator overload for sequence terms:

• is member: cvc5.pythonic.SeqRef.__getitem__()

Classes (with overloads) 

class cvc5.pythonic. SeqSortRef ( ast , ctx = None ) 

elem_sort ( ) 

Get the element sort for this sequence

>>> SeqSort(IntSort()).elem_sort()
Int
>>> SeqSort(SeqSort(IntSort())).elem_sort()
(Seq Int)

is_string ( ) 

Determine if sort is a string

>>> s = StringSort()
>>> s.is_string()
True
>>> s = SeqSort(IntSort())
>>> s.is_string()
False

class cvc5.pythonic. SeqRef ( ast , ctx = None , reverse_children = False ) 

Sequence Expressions

__add__ ( other ) 

Concatenation of two sequences.

>>> s,t = Consts('s t',SeqSort(RealSort()))
>>> s+t
Concat(s, t)
>>> (s+t).sort()
(Seq Real)

__getitem__ ( i ) 

Return the SMT expression self[arg]

>>> seq = Const('seq',SeqSort(IntSort()))
>>> seq[0]
seq [] 0
>>> seq[0].sort()
Int

as_string ( ) 

Return a string representation of sequence expression.

>>> s = Unit(IntVal(1)) + Unit(IntVal(2))
>>> s.as_string()
'(seq.++ (seq.unit 1) (seq.unit 2))'
>>> x = Unit(RealVal(1.5))
>>> print(x.as_string())
(seq.unit (/ 3 2))

at ( i ) 

Return the sequence at index i

>>> seq = Const('seq',SeqSort(IntSort()))
>>> seq.at(0)
At(seq, 0)
>>> seq.at(0).sort()
(Seq Int)

is_string_value ( ) 

Return True if self is a string value

>>> s = String('s')
>>> s.is_string_value()
False
>>> t = StringVal('t')
>>> t.is_string_value()
True