FPRef Class Reference

FP Expressions. More...

Inheritance diagram for FPRef:

Public Member Functions
def	sort
def	ebits
def	sbits
def	as_string
def	__le__
def	__lt__
def	__ge__
def	__gt__
def	__ne__
def	__add__
def	__radd__
def	__sub__
def	__rsub__
def	__mul__
def	__rmul__
def	__pos__
def	__neg__
def	__truediv__
def	__rtruediv__
def	__mod__
def	__rmod__
Public Member Functions inherited from ExprRef
def	as_ast
def	get_id
def	sort
def	sort_kind
def	__eq__
def	__ne__
def	decl
def	num_args
def	arg
def	children
Public Member Functions inherited from AstRef
def	__init__
def	__del__
def	__str__
def	__repr__
def	sexpr
def	as_ast
def	get_id
def	ctx_ref
def	eq
def	translate
def	hash
Public Member Functions inherited from Z3PPObject
def	use_pp

Additional Inherited Members
Data Fields inherited from AstRef
	ast
	ctx

Detailed Description

FP Expressions.

Floating-point expressions.

Definition at line 7800 of file z3py.py.

Member Function Documentation

def __add__	(		self,
			other
	)

Create the Z3 expression `self + other`.

>>> x = FP('x', FPSort(8, 24))
>>> y = FP('y', FPSort(8, 24))
>>> x + y
x + y
>>> (x + y).sort()
FPSort(8, 24)

Definition at line 7850 of file z3py.py.

    def __add__(self, other):
        """Create the Z3 expression `self + other`.
        
        >>> x = FP('x', FPSort(8, 24))
        >>> y = FP('y', FPSort(8, 24))
        >>> x + y
        x + y
        >>> (x + y).sort()
        FPSort(8, 24)
        """
        a, b = z3._coerce_exprs(self, other)
        return fpAdd(_dflt_rm(), self, other)