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__
def	__del__ (self)
def	__deepcopy__
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 1518 of file z3py.py.

Member Function Documentation

def __mul__	(		self,
			other
	)

Create the Z3 expression `self * other`.

Definition at line 1527 of file z3py.py.

    def __mul__(self, other):
        """Create the Z3 expression `self * other`.
        """
        if other == 1:
            return self
        if other == 0:
            return 0
        return If(self, other, 0)

def __rmul__	(		self,
			other
	)

Definition at line 1524 of file z3py.py.

    def __rmul__(self, other):
        return self * other

def sort

(

self

)

Definition at line 1521 of file z3py.py.

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