SeqSortRef Class Reference

Strings, Sequences and Regular expressions. More...

Inheritance diagram for SeqSortRef:

Public Member Functions
def	is_string (self)
def	basis (self)
Public Member Functions inherited from SortRef
def	as_ast (self)
def	get_id (self)
def	kind (self)
def	subsort (self, other)
def	cast (self, val)
def	name (self)
def	__eq__ (self, other)
def	__ne__ (self, other)
def	__hash__ (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

Strings, Sequences and Regular expressions.

Sequence sort.

Definition at line 10858 of file z3py.py.

Member Function Documentation

basis()

def basis

(

self

)

Definition at line 10872 of file z3py.py.

    def basis(self):
        return _to_sort_ref(Z3_get_seq_sort_basis(self.ctx_ref(), self.ast), self.ctx)
 

is_string()

def is_string

(

self

)

Determine if sort is a string
>>> s = StringSort()
>>> s.is_string()
True
>>> s = SeqSort(IntSort())
>>> s.is_string()
False

Definition at line 10861 of file z3py.py.

    def is_string(self):
        """Determine if sort is a string
        >>> s = StringSort()
        >>> s.is_string()
        True
        >>> s = SeqSort(IntSort())
        >>> s.is_string()
        False
        """
        return Z3_is_string_sort(self.ctx_ref(), self.ast)