BoolRef Class Reference

Inheritance diagram for BoolRef:

Public Member Functions
def	sort

---

Detailed Description

All Boolean expressions are instances of this class.

Definition at line 1241 of file z3py.py.

---

Member Function Documentation

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 1243 of file z3py.py.

Referenced by ArrayRef.domain(), and ArrayRef.range().

    def sort(self):
        return BoolSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)