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_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	__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)
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 10030 of file z3py.py.

Member Function Documentation

__add__()

def __add__	(		self,
			other
	)

Definition at line 10036 of file z3py.py.

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

__ge__()

def __ge__	(		self,
			other
	)

Definition at line 10073 of file z3py.py.

    def __ge__(self, other):
        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.

    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__()

def __gt__	(		self,
			other
	)

Definition at line 10076 of file z3py.py.

    def __gt__(self, other):
        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.

    def __le__(self, other):
        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.

    def __lt__(self, other):
        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.

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

as_string()

def as_string

(

self

)

Return a string representation of sequence expression.

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

def at	(		self,
			i
	)

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

def is_string

(

self

)

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

def is_string_value

(

self

)

Definition at line 10055 of file z3py.py.

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

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

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