Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions
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 1220 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 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)

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines