Z3 |

Public Member Functions
SeqRef Class Reference
Inheritance diagram for SeqRef:

## Public Member Functions
def | sort (self)
def | __add__ (self, other)
def | __radd__ (self, other)
def | __getitem__ (self, i)
def | at (self, i)
def | is_string (self)
def | is_string_value (self)
def | as_string (self)
def | __le__ (self, other)
def | __lt__ (self, other)
def | __ge__ (self, other)
def | __gt__ (self, other)
Public Member Functions inherited from ExprRef
def | as_ast (self)
def | get_id (self)
def | sort (self)
def | sort_kind (self)
def | __eq__ (self, other)
def | __hash__ (self)
def | __ne__ (self, other)
def | params (self)
def | decl (self)
def | num_args (self)
def | arg (self, idx)
def | children (self)
Public Member Functions inherited from AstRef
def | __init__ (self, ast, ctx=None)
def | __del__ (self)
def | __deepcopy__ (self, memo={})
def | __str__ (self)
def | __repr__ (self)
def | __eq__ (self, other)
def | __hash__ (self)
def | __nonzero__ (self)
def | __bool__ (self)
def | sexpr (self)
def | as_ast (self)
def | get_id (self)
def | ctx_ref (self)
def | eq (self, other)
def | translate (self, target)
def | __copy__ (self)
def | hash (self)
Public Member Functions inherited from Z3PPObject
def | use_pp (self)

## Additional Inherited Members
Data Fields inherited from AstRef
| ast
| ctx

## Detailed Description

    Sequence expression.

Definition at line 10588 of file z3py.py.

## Member Function Documentation

## ◆ __add__()

def __add__ | ( |  | self,
|  |  | other
| ) |  |

Definition at line 10594 of file z3py.py.

10594 def __add__(self, other):
10595 return Concat(self, other)
10596
z3py.Concat
def Concat(*args)
Definition: z3py.py:4044

## ◆ __ge__()

def __ge__ | ( |  | self,
|  |  | other
| ) |  |

Definition at line 10630 of file z3py.py.

10630 def __ge__(self, other):
10631 return SeqRef(Z3_mk_str_le(self.ctx_ref(), other.as_ast(), self.as_ast()), self.ctx)
10632
Z3_mk_str_le
Z3_ast Z3_API Z3_mk_str_le(Z3_context c, Z3_ast prefix, Z3_ast s)
Check if s1 is equal or lexicographically strictly less than s2.

## ◆ __getitem__()

def __getitem__ | ( |  | self,
|  |  | i
| ) |  |

Definition at line 10600 of file z3py.py.

10600 def __getitem__(self, i):
10601 if _is_int(i):
10602 i = IntVal(i, self.ctx)
10603 return _to_expr_ref(Z3_mk_seq_nth(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx)
10604
z3py.IntVal
def IntVal(val, ctx=None)
Definition: z3py.py:3150
Z3_mk_seq_nth
Z3_ast Z3_API Z3_mk_seq_nth(Z3_context c, Z3_ast s, Z3_ast index)
Retrieve from s the element positioned at position index. The function is under-specified if the inde...

## ◆ __gt__()

def __gt__ | ( |  | self,
|  |  | other
| ) |  |

Definition at line 10633 of file z3py.py.

10633 def __gt__(self, other):
10634 return SeqRef(Z3_mk_str_lt(self.ctx_ref(), other.as_ast(), self.as_ast()), self.ctx)
10635
10636
Z3_mk_str_lt
Z3_ast Z3_API Z3_mk_str_lt(Z3_context c, Z3_ast prefix, Z3_ast s)
Check if s1 is lexicographically strictly less than s2.

## ◆ __le__()

def __le__ | ( |  | self,
|  |  | other
| ) |  |

Definition at line 10624 of file z3py.py.

10624 def __le__(self, other):
10625 return SeqRef(Z3_mk_str_le(self.ctx_ref(), self.as_ast(), other.as_ast()), self.ctx)
10626

## ◆ __lt__()

def __lt__ | ( |  | self,
|  |  | other
| ) |  |

Definition at line 10627 of file z3py.py.

10627 def __lt__(self, other):
10628 return SeqRef(Z3_mk_str_lt(self.ctx_ref(), self.as_ast(), other.as_ast()), self.ctx)
10629

## ◆ __radd__()

def __radd__ | ( |  | self,
|  |  | other
| ) |  |

Definition at line 10597 of file z3py.py.

10597 def __radd__(self, other):
10598 return Concat(other, self)
10599

## ◆ as_string()

def as_string | ( |  | self | ) |

    Return a string representation of sequence expression.

Definition at line 10616 of file z3py.py.

10616 def as_string(self):
10617 """Return a string representation of sequence expression."""
10618 if self.is_string_value():
10619 string_length = ctypes.c_uint()
10620 chars = Z3_get_lstring(self.ctx_ref(), self.as_ast(), byref(string_length))
10621 return string_at(chars, size=string_length.value).decode("latin-1")
10622 return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
10623
Z3_ast_to_string
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.
Z3_get_lstring
Z3_char_ptr Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned *length)
Retrieve the unescaped string constant stored in s.

Referenced by IntNumRef.as_long(), BitVecNumRef.as_long(), and FiniteDomainNumRef.as_long().

## ◆ at()

def at | ( |  | self,
|  |  | i
| ) |  |

Definition at line 10605 of file z3py.py.

10605 def at(self, i):
10606 if _is_int(i):
10607 i = IntVal(i, self.ctx)
10608 return SeqRef(Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx)
10609
Z3_mk_seq_at
Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index)
Retrieve from s the unit sequence positioned at position index. The sequence is empty if the index is...

## ◆ is_string()

def is_string | ( |  | self | ) |

Definition at line 10610 of file z3py.py.

10610 def is_string(self):
10611 return Z3_is_string_sort(self.ctx_ref(), Z3_get_sort(self.ctx_ref(), self.as_ast()))
10612
z3py.is_string
def is_string(a)
Definition: z3py.py:10668
Z3_is_string_sort
bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s)
Check if s is a string sort.
Z3_get_sort
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.

## ◆ is_string_value()

def is_string_value | ( |  | self | ) |

Definition at line 10613 of file z3py.py.

10613 def is_string_value(self):
10614 return Z3_is_string(self.ctx_ref(), self.as_ast())
10615
z3py.is_string_value
def is_string_value(a)
Definition: z3py.py:10676
Z3_is_string
bool Z3_API Z3_is_string(Z3_context c, Z3_ast s)
Determine if s is a string constant.

Referenced by SeqRef.as_string().

## ◆ sort()

def sort | ( |  | self | ) |

    Return the sort of expression `self`.

    >>> x = Int('x')
    >>> (x + 1).sort()
    Int
    >>> y = Real('y')
    >>> (x + y).sort()
    Real

Reimplemented from ExprRef.

Definition at line 10591 of file z3py.py.

10591 def sort(self):
10592 return SeqSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
10593

Referenced by QuantifierRef.__getitem__(), FPNumRef.as_string(), ArrayRef.domain(), FPRef.ebits(), ArithRef.is_int(), ArithRef.is_real(), ArrayRef.range(), FPRef.sbits(), BitVecRef.size(), and ExprRef.sort_kind().