FPSortRef Class Reference

FP Sorts. More...

Inheritance diagram for FPSortRef:

Public Member Functions
def	ebits
def	sbits
def	cast
Public Member Functions inherited from SortRef
def	as_ast
def	get_id
def	kind
def	subsort
def	cast
def	name
def	__eq__
def	__ne__
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

Data Fields
	ctx
Data Fields inherited from AstRef
	ast
	ctx

Detailed Description

FP Sorts.

Floating-point sort.

Definition at line 7698 of file z3py.py.

Member Function Documentation

def cast	(		self,
			val
	)

Try to cast `val` as a Floating-point expression

>>> b = FPSort(8, 24)
>>> b.cast(1.0)
1
>>> b.cast(1.0).sexpr()
'(fp #b0 #x7f #b00000000000000000000000)'

Definition at line 7717 of file z3py.py.

    def cast(self, val):
        """Try to cast `val` as a Floating-point expression

        >>> b = FPSort(8, 24)
        >>> b.cast(1.0)
        1
        >>> b.cast(1.0).sexpr()
        '(fp #b0 #x7f #b00000000000000000000000)'
        """
        if is_expr(val):
            if __debug__:
                _z3_assert(self.ctx == val.ctx, "Context mismatch")
            return val
        else:
            return FPVal(val, None, self, self.ctx)