FPSortRef Class Reference

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	__deepcopy__ (self, memo={})
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	__copy__ (self)
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

Floating-point sort.

Definition at line 9195 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 9214 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()

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 9198 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 9206 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 9224 of file z3py.py.

Referenced by UserPropagateBase.conflict(), and UserPropagateBase.ctx_ref().