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	py_value (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	kind (self)
def	num_args (self)
def	arg (self, idx)
def	children (self)
def	from_string (self, s)
def	serialize (self)
Public Member Functions inherited from AstRef
def	__init__
def	__del__ (self)
def	__deepcopy__
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)
def	py_value (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 11014 of file z3py.py.

Member Function Documentation

def __add__	(		self,
			other
	)

Definition at line 11020 of file z3py.py.

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

def __ge__	(		self,
			other
	)

Definition at line 11059 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)

def __getitem__	(		self,
			i
	)

Definition at line 11026 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)

def __gt__	(		self,
			other
	)

Definition at line 11062 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)

def __le__	(		self,
			other
	)

Definition at line 11053 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)

def __lt__	(		self,
			other
	)

Definition at line 11056 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)

def __radd__	(		self,
			other
	)

Definition at line 11023 of file z3py.py.

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

def as_string

(

self

)

Return a string representation of sequence expression.

Definition at line 11042 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())

def at	(		self,
			i
	)

Definition at line 11031 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)

def is_string

(

self

)

Definition at line 11036 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()))

def is_string_value

(

self

)

Definition at line 11039 of file z3py.py.

Referenced by SeqRef.as_string().

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

def py_value

(

self

)

Definition at line 11050 of file z3py.py.

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

def sort

(

self

)

Definition at line 11017 of file z3py.py.

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