Z3 |

Public Member Functions
BoolRef Class Reference
Inheritance diagram for BoolRef:

## Public Member Functions
def | sort (self)
def | __rmul__ (self, other)
def | __mul__ (self, other)
Public Member Functions inherited from ExprRef
def | as_ast (self)
def | get_id (self)
def | sort (self)
def | sort_kind (self)
def | __eq__ (self, other)
def | __hash__ (self)
def | __ne__ (self, other)
def | params (self)
def | decl (self)
def | num_args (self)
def | arg (self, idx)
def | children (self)
Public Member Functions inherited from AstRef
def | __init__ (self, ast, ctx=None)
def | __del__ (self)
def | __deepcopy__ (self, memo={})
def | __str__ (self)
def | __repr__ (self)
def | __eq__ (self, other)
def | __hash__ (self)
def | __nonzero__ (self)
def | __bool__ (self)
def | sexpr (self)
def | as_ast (self)
def | get_id (self)
def | ctx_ref (self)
def | eq (self, other)
def | translate (self, target)
def | __copy__ (self)
def | hash (self)
Public Member Functions inherited from Z3PPObject
def | use_pp (self)

## Additional Inherited Members
Data Fields inherited from AstRef
| ast
| ctx

## Detailed Description

    All Boolean expressions are instances of this class.

Definition at line 1516 of file z3py.py.

## Member Function Documentation

## ◆ __mul__()

def __mul__ | ( |  | self,
|  |  | other
| ) |  |

    Create the Z3 expression `self * other`.

Definition at line 1525 of file z3py.py.

1525 def __mul__(self, other):
1526 """Create the Z3 expression `self * other`.
1527 """
1528 if other == 1:
1529 return self
1530 if other == 0:
1531 return 0
1532 return If(self, other, 0)
1533
1534
z3py.If
def If(a, b, c, ctx=None)
Definition: z3py.py:1349

## ◆ __rmul__()

def __rmul__ | ( |  | self,
|  |  | other
| ) |  |

Definition at line 1522 of file z3py.py.

1522 def __rmul__(self, other):
1523 return self * other
1524

## ◆ 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 1519 of file z3py.py.

1519 def sort(self):
1520 return BoolSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
1521
Z3_get_sort
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.

Referenced by QuantifierRef.__getitem__(), FPNumRef.as_string(), ArrayRef.domain(), FPRef.ebits(), ArithRef.is_int(), ArithRef.is_real(), ArrayRef.range(), FPRef.sbits(), BitVecRef.size(), and ExprRef.sort_kind().