BoolRef Class Reference

Inheritance diagram for BoolRef:

Public Member Functions
def	sort (self)
def	__add__ (self, other)
def	__radd__ (self, other)
def	__rmul__ (self, other)
def	__mul__ (self, other)
def	__and__ (self, other)
def	__or__ (self, other)
def	__xor__ (self, other)
def	__invert__ (self)
Public Member Functions inherited from ExprRef
def	as_ast (self)
def	get_id (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)
def	from_string (self, s)
def	serialize (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

All Boolean expressions are instances of this class.

Definition at line 1568 of file z3py.py.

Member Function Documentation

__add__()

def __add__	(		self,
			other
	)

Definition at line 1574 of file z3py.py.

    def __add__(self, other):
        if isinstance(other, BoolRef):
            other = If(other, 1, 0)
        return If(self, 1, 0) + other
 

__and__()

def __and__	(		self,
			other
	)

Definition at line 1596 of file z3py.py.

    def __and__(self, other):
        return And(self, other)
    

__invert__()

def __invert__

(

self

)

Definition at line 1605 of file z3py.py.

    def __invert__(self):
        return Not(self)
    
    
 

__mul__()

def __mul__	(		self,
			other
	)

Create the Z3 expression `self * other`.

Definition at line 1585 of file z3py.py.

    def __mul__(self, other):
        """Create the Z3 expression `self * other`.
        """
        if isinstance(other, int) and other == 1:
            return If(self, 1, 0)
        if isinstance(other, int) and other == 0:
            return IntVal(0, self.ctx)
        if isinstance(other, BoolRef):
            other = If(other, 1, 0)
        return If(self, other, 0)
        

__or__()

def __or__	(		self,
			other
	)

Definition at line 1599 of file z3py.py.

    def __or__(self, other):
        return Or(self, other)
 

__radd__()

def __radd__	(		self,
			other
	)

Definition at line 1579 of file z3py.py.

    def __radd__(self, other):
        return self + other
 

__rmul__()

def __rmul__	(		self,
			other
	)

Definition at line 1582 of file z3py.py.

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

__xor__()

def __xor__	(		self,
			other
	)

Definition at line 1602 of file z3py.py.

    def __xor__(self, other):
        return Xor(self, other)
    

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 1571 of file z3py.py.

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

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