FPNumRef Class Reference

FP Numerals. More...

Inheritance diagram for FPNumRef:

Public Member Functions
def	isNaN (self)
def	isInf (self)
def	isZero (self)
def	isNegative (self)
def	sign (self)
def	significand (self)
def	exponent (self)
def	exponent_as_long (self)
def	as_string (self)
Public Member Functions inherited from FPRef
def	sort (self)
def	ebits (self)
def	sbits (self)
def	__le__ (self, other)
def	__lt__ (self, other)
def	__ge__ (self, other)
def	__gt__ (self, other)
def	__add__ (self, other)
def	__radd__ (self, other)
def	__sub__ (self, other)
def	__rsub__ (self, other)
def	__mul__ (self, other)
def	__rmul__ (self, other)
def	__pos__ (self)
def	__neg__ (self)
def	__div__ (self, other)
def	__rdiv__ (self, other)
def	__truediv__ (self, other)
def	__rtruediv__ (self, other)
def	__mod__ (self, other)
def	__rmod__ (self, other)
Public Member Functions inherited from ExprRef
def	as_ast (self)
def	get_id (self)
def	sort_kind (self)
def	__eq__ (self, other)
def	__hash__ (self)
def	__ne__ (self, other)
def	decl (self)
def	num_args (self)
def	arg (self, idx)
def	children (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)

Additional Inherited Members
Data Fields inherited from AstRef
	ast
	ctx

Detailed Description

FP Numerals.

Definition at line 8455 of file z3py.py.

Member Function Documentation

as_string()

def as_string

(

self

)

Return a Z3 floating point expression as a Python string.

Reimplemented from FPRef.

Definition at line 8525 of file z3py.py.

    def as_string(self):
        s = Z3_fpa_get_numeral_string(self.ctx.ref(), self.as_ast())
        return ("FPVal(%s, %s)" % (s, self.sort()))

exponent()

def exponent

(

self

)

Definition at line 8502 of file z3py.py.

    def exponent(self):
        return Z3_fpa_get_numeral_exponent_string(self.ctx.ref(), self.as_ast())

exponent_as_long()

def exponent_as_long

(

self

)

Definition at line 8512 of file z3py.py.

    def exponent_as_long(self):
        ptr = (ctypes.c_longlong * 1)()
        if not Z3_fpa_get_numeral_exponent_int64(self.ctx.ref(), self.as_ast(), ptr):
            raise Z3Exception("error retrieving the exponent of a numeral.")
        return ptr[0]

isInf()

def isInf

(

self

)

Definition at line 8459 of file z3py.py.

    def isInf(self):
        return self.decl().kind() == Z3_OP_FPA_PLUS_INF or self.decl().kind() == Z3_OP_FPA_MINUS_INF

isNaN()

def isNaN

(

self

)

Definition at line 8456 of file z3py.py.

    def isNaN(self):
        return self.decl().kind() == Z3_OP_FPA_NAN

isNegative()

def isNegative

(

self

)

Definition at line 8465 of file z3py.py.

    def isNegative(self):
        k = self.decl().kind()
        return (self.num_args() == 0 and (k == Z3_OP_FPA_MINUS_INF or k == Z3_OP_FPA_MINUS_ZERO)) or (self.sign() == True)

isZero()

def isZero

(

self

)

Definition at line 8462 of file z3py.py.

    def isZero(self):
        return self.decl().kind() == Z3_OP_FPA_PLUS_ZERO or self.decl().kind() == Z3_OP_FPA_MINUS_ZERO

sign()

def sign

(

self

)

Definition at line 8479 of file z3py.py.

    def sign(self):
        l = (ctypes.c_int)()
        if Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(l)) == False:
            raise Z3Exception("error retrieving the sign of a numeral.")
        return l.value != 0

Referenced by FPNumRef.isNegative().

significand()

def significand

(

self

)

Definition at line 8492 of file z3py.py.

    def significand(self):
        return Z3_fpa_get_numeral_significand_string(self.ctx.ref(), self.as_ast())