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)
def	from_string (self, s)
def	serialize (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 10907 of file z3py.py.

Member Function Documentation

__add__()

def __add__	(		self,
			other
	)

Definition at line 10913 of file z3py.py.

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

__ge__()

def __ge__	(		self,
			other
	)

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

def __getitem__	(		self,
			i
	)

Definition at line 10919 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 10952 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__()

def __le__	(		self,
			other
	)

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

def __lt__	(		self,
			other
	)

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

def __radd__	(		self,
			other
	)

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

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

at()

def at	(		self,
			i
	)

Definition at line 10924 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 10929 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 10932 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 10910 of file z3py.py.

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

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