A Sort is essentially a type. Every Z3 expression has a sort. A sort is an AST node.
Definition at line 513 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 545 of file z3py.py.
546 """Try to cast `val` as an element of sort `self`. 548 This method is used in Z3Py to convert Python objects such as integers, 549 floats, longs and strings into Z3 expressions. 552 >>> RealSort().cast(x) 556 _z3_assert(
is_expr(val),
"Z3 expression expected")
557 _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 521 of file z3py.py.
522 """Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts. 525 >>> b.kind() == Z3_BOOL_SORT 527 >>> b.kind() == Z3_INT_SORT 529 >>> A = ArraySort(IntSort(), IntSort()) 530 >>> A.kind() == Z3_ARRAY_SORT 532 >>> A.kind() == Z3_INT_SORT 535 return _sort_kind(self.ctx, self.ast)
Referenced by ArithSortRef.is_int(), and ArithSortRef.is_real().