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()
'(str.++ (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