FPSortRef Class Reference

Inheritance diagram for FPSortRef:

Public Member Functions
	ebits (self)
	sbits (self)
	cast (self, val)
Public Member Functions inherited from SortRef
	as_ast (self)
	get_id (self)
	kind (self)
	subsort (self, other)
	name (self)
	__eq__ (self, other)
	__ne__ (self, other)
	__gt__ (self, other)
	__hash__ (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)
	py_value (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

Floating-point sort.

Definition at line 9772 of file z3py.py.

Member Function Documentation

cast()

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)'

Reimplemented from SortRef.

Definition at line 9791 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 z3_debug():
                _z3_assert(self.ctx == val.ctx, "Context mismatch")
            return val
        else:
            return FPVal(val, None, self, self.ctx)
 
 

ebits()

ebits

(

self

)

Retrieves the number of bits reserved for the exponent in the FloatingPoint sort `self`.
>>> b = FPSort(8, 24)
>>> b.ebits()
8

Definition at line 9775 of file z3py.py.

    def ebits(self):
        """Retrieves the number of bits reserved for the exponent in the FloatingPoint sort `self`.
        >>> b = FPSort(8, 24)
        >>> b.ebits()
        8
        """
        return int(Z3_fpa_get_ebits(self.ctx_ref(), self.ast))
 

sbits()

sbits

(

self

)

Retrieves the number of bits reserved for the significand in the FloatingPoint sort `self`.
>>> b = FPSort(8, 24)
>>> b.sbits()
24

Definition at line 9783 of file z3py.py.

    def sbits(self):
        """Retrieves the number of bits reserved for the significand in the FloatingPoint sort `self`.
        >>> b = FPSort(8, 24)
        >>> b.sbits()
        24
        """
        return int(Z3_fpa_get_sbits(self.ctx_ref(), self.ast))