SortRef Class Reference

Inheritance diagram for SortRef:

Public Member Functions
def	as_ast
def	get_id
def	kind
def	subsort
def	cast
def	name
def	__eq__
def	__ne__
Public Member Functions inherited from AstRef
def	__init__
def	__del__
def	__str__
def	__repr__
def	sexpr
def	as_ast
def	get_id
def	ctx_ref
def	eq
def	translate
def	hash
Public Member Functions inherited from Z3PPObject
def	use_pp

Additional Inherited Members
Data Fields inherited from AstRef
	ast
	ctx

Detailed Description

A Sort is essentially a type. Every Z3 expression has a sort. A sort is an AST node.

Definition at line 449 of file z3py.py.

Member Function Documentation

def __eq__	(		self,
			other
	)

Return `True` if `self` and `other` are the same Z3 sort.

>>> p = Bool('p')
>>> p.sort() == BoolSort()
True
>>> p.sort() == IntSort()
False

Definition at line 506 of file z3py.py.

Referenced by Probe.__ne__().

    def __eq__(self, other):
        """Return `True` if `self` and `other` are the same Z3 sort.
        
        >>> p = Bool('p')
        >>> p.sort() == BoolSort()
        True
        >>> p.sort() == IntSort()
        False
        """
        if other == None:
            return False
        return Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)