Public Member Functions | |
def | sort |
def sort | ( | self | ) |
Return the sort of expression `self`. >>> x = Int('x') >>> (x + 1).sort() Int >>> y = Real('y') >>> (x + y).sort() Real
Reimplemented from ExprRef.
Reimplemented in QuantifierRef.
Definition at line 1222 of file z3py.py.
Referenced by ArrayRef.domain(), and ArrayRef.range().
01222 01223 def sort(self): 01224 return BoolSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)