SeqRef Class Reference

Inheritance diagram for SeqRef:

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

Additional Inherited Members
Data Fields inherited from AstRef
	ast = ast
	ctx = _get_ctx(ctx)
Protected Member Functions inherited from Z3PPObject
	_repr_html_ (self)

Detailed Description

Sequence expression.

Definition at line 11138 of file z3py.py.

Member Function Documentation

__add__()

__add__	(		self,
			other )

Definition at line 11144 of file z3py.py.

    def __add__(self, other):
        return Concat(self, other)
 

__ge__()

__ge__	(		self,
			other )

Definition at line 11183 of file z3py.py.

    def __ge__(self, other):
        return _to_expr_ref(Z3_mk_str_le(self.ctx_ref(), other.as_ast(), self.as_ast()), self.ctx)
 

__getitem__()

__getitem__	(		self,
			i )

Definition at line 11150 of file z3py.py.

    def __getitem__(self, i):
        if _is_int(i):
            i = IntVal(i, self.ctx)
        return _to_expr_ref(Z3_mk_seq_nth(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx)
 

__gt__()

__gt__	(		self,
			other )

Definition at line 11186 of file z3py.py.

    def __gt__(self, other):
        return _to_expr_ref(Z3_mk_str_lt(self.ctx_ref(), other.as_ast(), self.as_ast()), self.ctx)
 
 

__le__()

__le__	(		self,
			other )

Definition at line 11177 of file z3py.py.

    def __le__(self, other):
        return _to_expr_ref(Z3_mk_str_le(self.ctx_ref(), self.as_ast(), other.as_ast()), self.ctx)
 

__lt__()

__lt__	(		self,
			other )

Definition at line 11180 of file z3py.py.

    def __lt__(self, other):
        return _to_expr_ref(Z3_mk_str_lt(self.ctx_ref(), self.as_ast(), other.as_ast()), self.ctx)
 

__radd__()

__radd__	(		self,
			other )

Definition at line 11147 of file z3py.py.

    def __radd__(self, other):
        return Concat(other, self)
 

as_string()

as_string

(

self

)

Return a string representation of sequence expression.

Definition at line 11166 of file z3py.py.

    def as_string(self):
        """Return a string representation of sequence expression."""
        if self.is_string_value():
            string_length = ctypes.c_uint()
            chars = Z3_get_lstring(self.ctx_ref(), self.as_ast(), byref(string_length))
            return string_at(chars, size=string_length.value).decode("latin-1")
        return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
 

at()

at	(		self,
			i )

Definition at line 11155 of file z3py.py.

    def at(self, i):
        if _is_int(i):
            i = IntVal(i, self.ctx)
        return SeqRef(Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx)
 

is_string()

is_string

(

self

)

Definition at line 11160 of file z3py.py.

    def is_string(self):
        return Z3_is_string_sort(self.ctx_ref(), Z3_get_sort(self.ctx_ref(), self.as_ast()))
 

is_string_value()

is_string_value

(

self

)

Definition at line 11163 of file z3py.py.

    def is_string_value(self):
        return Z3_is_string(self.ctx_ref(), self.as_ast())
 

py_value()

py_value

(

self

)

Return a Python value that is equivalent to `self`.

Reimplemented from AstRef.

Definition at line 11174 of file z3py.py.

    def py_value(self):
        return self.as_string()
 

sort()

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 11141 of file z3py.py.

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