A Sort is essentially a type. Every Z3 expression has a sort. A sort is an AST node.
Definition at line 511 of file z3py.py.
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 FPSortRef, BitVecSortRef, ArithSortRef, and BoolSortRef.
Definition at line 543 of file z3py.py.
544 """Try to cast `val` as an element of sort `self`. 546 This method is used in Z3Py to convert Python objects such as integers, 547 floats, longs and strings into Z3 expressions. 550 >>> RealSort().cast(x) 554 _z3_assert(
is_expr(val),
"Z3 expression expected")
555 _z3_assert(self.eq(val.sort()),
"Sort mismatch")
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 519 of file z3py.py.
520 """Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts. 523 >>> b.kind() == Z3_BOOL_SORT 525 >>> b.kind() == Z3_INT_SORT 527 >>> A = ArraySort(IntSort(), IntSort()) 528 >>> A.kind() == Z3_ARRAY_SORT 530 >>> A.kind() == Z3_INT_SORT 533 return _sort_kind(self.ctx, self.ast)
Referenced by ArithSortRef.is_int(), and ArithSortRef.is_real().