Z3 |

Public Member Functions
BoolSortRef Class Reference

Booleans. More...

Inheritance diagram for BoolSortRef:

## Public Member Functions
def | cast (self, val)
def | subsort (self, other)
def | is_int (self)
def | is_bool (self)
Public Member Functions inherited from SortRef
def | as_ast (self)
def | get_id (self)
def | kind (self)
def | subsort (self, other)
def | cast (self, val)
def | name (self)
def | __eq__ (self, other)
def | __ne__ (self, other)
def | __hash__ (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

Booleans.

    Boolean sort.

Definition at line 1480 of file z3py.py.

## Member Function Documentation

## ◆ cast()

def cast | ( |  | self,
|  |  | val
| ) |  |

    Try to cast `val` as a Boolean.

    >>> x = BoolSort().cast(True)
    >>> x
    True
    >>> is_expr(x)
    True
    >>> is_expr(True)
    False
    >>> x.sort()
    Bool

Reimplemented from SortRef.

Definition at line 1483 of file z3py.py.

1483 def cast(self, val):
1484 """Try to cast `val` as a Boolean.
1485
1486 >>> x = BoolSort().cast(True)
1487 >>> x
1488 True
1489 >>> is_expr(x)
1490 True
1491 >>> is_expr(True)
1492 False
1493 >>> x.sort()
1494 Bool
1495 """
1496 if isinstance(val, bool):
1497 return BoolVal(val, self.ctx)
1498 if z3_debug():
1499 if not is_expr(val):
1500 msg = "True, False or Z3 Boolean expression expected. Received %s of type %s"
1501 _z3_assert(is_expr(val), msg % (val, type(val)))
1502 if not self.eq(val.sort()):
1503 _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
1504 return val
1505
z3py.z3_debug
def z3_debug()
Definition: z3py.py:64
z3py.is_expr
def is_expr(a)
Definition: z3py.py:1210
z3py.BoolSort
def BoolSort(ctx=None)
Definition: z3py.py:1655
z3py.BoolVal
def BoolVal(val, ctx=None)
Definition: z3py.py:1673

Referenced by BoolSortRef.cast().

## ◆ is_bool()

def is_bool | ( |  | self | ) |

Definition at line 1512 of file z3py.py.

1512 def is_bool(self):
1513 return True
1514
1515
z3py.is_bool
def is_bool(a)
Definition: z3py.py:1535

## ◆ is_int()

def is_int | ( |  | self | ) |

Definition at line 1509 of file z3py.py.

1509 def is_int(self):
1510 return True
1511
z3py.is_int
def is_int(a)
Definition: z3py.py:2648

Referenced by IntNumRef.as_long(), and ArithSortRef.subsort().

## ◆ subsort()

def subsort | ( |  | self,
|  |  | other
| ) |  |

    Return `True` if `self` is a subsort of `other`.

    >>> IntSort().subsort(RealSort())
    True

Reimplemented from SortRef.

Definition at line 1506 of file z3py.py.

1506 def subsort(self, other):
1507 return isinstance(other, ArithSortRef)
1508