Public Member Functions | |
as_ast (self) | |
get_id (self) | |
kind (self) | |
subsort (self, other) | |
cast (self, val) | |
name (self) | |
__eq__ (self, other) | |
__ne__ (self, other) | |
__hash__ (self) | |
![]() | |
__init__ (self, ast, ctx=None) | |
__del__ (self) | |
__deepcopy__ (self, memo={}) | |
__str__ (self) | |
__repr__ (self) | |
__eq__ (self, other) | |
__hash__ (self) | |
__nonzero__ (self) | |
__bool__ (self) | |
sexpr (self) | |
ctx_ref (self) | |
eq (self, other) | |
translate (self, target) | |
__copy__ (self) | |
hash (self) | |
py_value (self) | |
![]() | |
use_pp (self) | |
Additional Inherited Members | |
![]() | |
ast = ast | |
ctx = _get_ctx(ctx) | |
![]() | |
_repr_html_ (self) | |
A Sort is essentially a type. Every Z3 expression has a sort. A sort is an AST node.
__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 632 of file z3py.py.
Referenced by CheckSatResult.__ne__().
__hash__ | ( | self | ) |
__ne__ | ( | self, | |
other ) |
Return `True` if `self` and `other` are not the same Z3 sort. >>> p = Bool('p') >>> p.sort() != BoolSort() False >>> p.sort() != IntSort() True
Definition at line 645 of file z3py.py.
as_ast | ( | self | ) |
cast | ( | self, | |
val ) |
Try to cast `val` as an element of sort `self`. This method is used in Z3Py to convert Python objects such as integers, floats, longs and strings into Z3 expressions. >>> x = Int('x') >>> RealSort().cast(x) ToReal(x)
Reimplemented in ArithSortRef, BitVecSortRef, BoolSortRef, FPSortRef, and TypeVarRef.
Definition at line 607 of file z3py.py.
get_id | ( | self | ) |
Return unique identifier for object. It can be used for hash-tables and maps.
Reimplemented from AstRef.
Definition at line 579 of file z3py.py.
kind | ( | self | ) |
Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts. >>> b = BoolSort() >>> b.kind() == Z3_BOOL_SORT True >>> b.kind() == Z3_INT_SORT False >>> A = ArraySort(IntSort(), IntSort()) >>> A.kind() == Z3_ARRAY_SORT True >>> A.kind() == Z3_INT_SORT False
Definition at line 582 of file z3py.py.
Referenced by ArithSortRef.is_int(), and ArithSortRef.is_real().
name | ( | self | ) |
Return the name (string) of sort `self`. >>> BoolSort().name() 'Bool' >>> ArraySort(IntSort(), IntSort()).name() 'Array'
Definition at line 622 of file z3py.py.
subsort | ( | self, | |
other ) |
Return `True` if `self` is a subsort of `other`. >>> IntSort().subsort(RealSort()) True
Reimplemented in ArithSortRef, BitVecSortRef, BoolSortRef, and TypeVarRef.
Definition at line 599 of file z3py.py.