FPSortRef Class Reference

FP Sorts. More...

Inheritance diagram for FPSortRef:

Public Member Functions
def	ebits (self)
def	sbits (self)
def	cast (self, val)
Public Member Functions inherited from SortRef
def	as_ast (self)
def	get_id (self)
def	kind (self)
def	subsort (self, other)
def	name (self)
def	__eq__ (self, other)
def	__ne__ (self, other)
def	__hash__ (self)
Public Member Functions inherited from AstRef
def	__init__ (self, ast, ctx=None)
def	__del__ (self)
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	hash (self)
Public Member Functions inherited from Z3PPObject
def	use_pp (self)

Data Fields
	ctx
Data Fields inherited from AstRef
	ast
	ctx

Detailed Description

FP Sorts.

Floating-point sort.

Definition at line 8110 of file z3py.py.

Member Function Documentation

cast()

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

Reimplemented from SortRef.

Definition at line 8129 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)

ebits()

def 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 8113 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()

def 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 8121 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))

Field Documentation

ctx

ctx

Definition at line 8139 of file z3py.py.