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	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	__nonzero__ (self)

def	__bool__ (self)

def	sexpr (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 1514 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 1517 of file z3py.py.

     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
         """
         if isinstance(val, bool):
             return BoolVal(val, self.ctx)
         if z3_debug():
             if not is_expr(val):
                 msg = "True, False or Z3 Boolean expression expected. Received %s of type %s"
                 _z3_assert(is_expr(val), msg % (val, type(val)))
             if not self.eq(val.sort()):
                 _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
         return val
  

◆ is_bool()

def is_bool ( self )

Definition at line 1546 of file z3py.py.

     def is_bool(self):
         return True

◆ is_int()

def is_int ( self )

Definition at line 1543 of file z3py.py.

     def is_int(self):
         return True
  

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