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:

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