|
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) |
|
def | as_ast (self) |
|
def | get_id (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) |
|
def | __init__ (self, ast, ctx=None) |
|
def | __del__ (self) |
|
def | __deepcopy__ (self, memo={}) |
|
def | __str__ (self) |
|
def | __repr__ (self) |
|
def | __nonzero__ (self) |
|
def | __bool__ (self) |
|
def | sexpr (self) |
|
def | ctx_ref (self) |
|
def | eq (self, other) |
|
def | translate (self, target) |
|
def | __copy__ (self) |
|
def | hash (self) |
|
def | use_pp (self) |
|
Sequence expression.
Definition at line 10030 of file z3py.py.
◆ __add__()
def __add__ |
( |
|
self, |
|
|
|
other |
|
) |
| |
Definition at line 10036 of file z3py.py.
10036 def __add__(self, other):
10037 return Concat(self, other)
◆ __ge__()
def __ge__ |
( |
|
self, |
|
|
|
other |
|
) |
| |
Definition at line 10073 of file z3py.py.
10073 def __ge__(self, other):
10074 return SeqRef(
Z3_mk_str_le(self.ctx_ref(), other.as_ast(), self.as_ast()), self.ctx)
◆ __getitem__()
def __getitem__ |
( |
|
self, |
|
|
|
i |
|
) |
| |
Definition at line 10042 of file z3py.py.
10042 def __getitem__(self, i):
10045 return _to_expr_ref(
Z3_mk_seq_nth(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx)
◆ __gt__()
def __gt__ |
( |
|
self, |
|
|
|
other |
|
) |
| |
Definition at line 10076 of file z3py.py.
10076 def __gt__(self, other):
10077 return SeqRef(
Z3_mk_str_lt(self.ctx_ref(), other.as_ast(), self.as_ast()), self.ctx)
◆ __le__()
def __le__ |
( |
|
self, |
|
|
|
other |
|
) |
| |
Definition at line 10067 of file z3py.py.
10067 def __le__(self, other):
10068 return SeqRef(
Z3_mk_str_le(self.ctx_ref(), self.as_ast(), other.as_ast()), self.ctx)
◆ __lt__()
def __lt__ |
( |
|
self, |
|
|
|
other |
|
) |
| |
Definition at line 10070 of file z3py.py.
10070 def __lt__(self, other):
10071 return SeqRef(
Z3_mk_str_lt(self.ctx_ref(), self.as_ast(), other.as_ast()), self.ctx)
◆ __radd__()
def __radd__ |
( |
|
self, |
|
|
|
other |
|
) |
| |
Definition at line 10039 of file z3py.py.
10039 def __radd__(self, other):
10040 return Concat(other, self)
◆ as_string()
Return a string representation of sequence expression.
Definition at line 10059 of file z3py.py.
10059 def as_string(self):
10060 """Return a string representation of sequence expression."""
10061 if self.is_string_value():
10062 string_length = ctypes.c_uint()
10063 chars =
Z3_get_lstring(self.ctx_ref(), self.as_ast(), byref(string_length))
10064 return string_at(chars, size=string_length.value).decode(
'latin-1')
◆ at()
Definition at line 10047 of file z3py.py.
10050 return SeqRef(
Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx)
◆ is_string()
◆ is_string_value()
def is_string_value |
( |
|
self | ) |
|
◆ sort()
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 10033 of file z3py.py.
10034 return SeqSortRef(
Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
Z3_char_ptr Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned *length)
Retrieve the unescaped string constant stored in s.
def IntVal(val, ctx=None)
bool Z3_API Z3_is_string(Z3_context c, Z3_ast s)
Determine if s is a string constant.
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.
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.
bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s)
Check if s is a string sort.
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.
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...
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.
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...