BoolRef Class Reference

Inheritance diagram for BoolRef:

Public Member Functions
	sort (self)
	__add__ (self, other)
	__radd__ (self, other)
	__rmul__ (self, other)
	__mul__ (self, other)
	__and__ (self, other)
	__or__ (self, other)
	__xor__ (self, other)
	__invert__ (self)
	py_value (self)
Public Member Functions inherited from ExprRef
	as_ast (self)
	get_id (self)
	sort_kind (self)
	__eq__ (self, other)
	__hash__ (self)
	__ne__ (self, other)
	params (self)
	decl (self)
	kind (self)
	num_args (self)
	arg (self, idx)
	children (self)
	update (self, *args)
	from_string (self, s)
	serialize (self)
Public Member Functions inherited from AstRef
	__init__ (self, ast, ctx=None)
	__del__ (self)
	__deepcopy__ (self, memo={})
	__str__ (self)
	__repr__ (self)
	__eq__ (self, other)
	__hash__ (self)
	__nonzero__ (self)
	__bool__ (self)
	sexpr (self)
	ctx_ref (self)
	eq (self, other)
	translate (self, target)
	__copy__ (self)
	hash (self)
Public Member Functions inherited from Z3PPObject
	use_pp (self)

Additional Inherited Members
Data Fields inherited from AstRef
	ast = ast
	ctx = _get_ctx(ctx)
Protected Member Functions inherited from Z3PPObject
	_repr_html_ (self)

Detailed Description

All Boolean expressions are instances of this class.

Definition at line 1654 of file z3py.py.

Member Function Documentation

__add__()

__add__	(		self,
			other )

Definition at line 1660 of file z3py.py.

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

__and__()

__and__	(		self,
			other )

Definition at line 1682 of file z3py.py.

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

__invert__()

__invert__

(

self

)

Definition at line 1691 of file z3py.py.

    def __invert__(self):
        return Not(self)
 

__mul__()

__mul__	(		self,
			other )

Create the Z3 expression `self * other`.

Definition at line 1671 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__()

__or__	(		self,
			other )

Definition at line 1685 of file z3py.py.

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

__radd__()

__radd__	(		self,
			other )

Definition at line 1665 of file z3py.py.

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

__rmul__()

__rmul__	(		self,
			other )

Definition at line 1668 of file z3py.py.

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

__xor__()

__xor__	(		self,
			other )

Definition at line 1688 of file z3py.py.

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

py_value()

py_value

(

self

)

Return a Python value that is equivalent to `self`.

Reimplemented from AstRef.

Definition at line 1694 of file z3py.py.

    def py_value(self):
        if is_true(self):
            return True
        if is_false(self):
            return False
        return None
    
    
 

sort()

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

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