Z3 |

Public Member Functions
FPNumRef Class Reference
Inheritance diagram for FPNumRef:

## Public Member Functions
def | sign (self)
def | sign_as_bv (self)
def | significand (self)
def | significand_as_long (self)
def | significand_as_bv (self)
def | exponent (self, biased=True)
def | exponent_as_long (self, biased=True)
def | exponent_as_bv (self, biased=True)
def | isNaN (self)
def | isInf (self)
def | isZero (self)
def | isNormal (self)
def | isSubnormal (self)
def | isPositive (self)
def | isNegative (self)
def | as_string (self)
Public Member Functions inherited from FPRef
def | sort (self)
def | ebits (self)
def | sbits (self)
def | as_string (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 (self)
def | sort_kind (self)
def | __eq__ (self, other)
def | __hash__ (self)
def | __ne__ (self, other)
def | params (self)
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 | __deepcopy__ (self, memo={})
def | __str__ (self)
def | __repr__ (self)
def | __eq__ (self, other)
def | __hash__ (self)
def | __nonzero__ (self)
def | __bool__ (self)
def | sexpr (self)
def | as_ast (self)
def | get_id (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)

## Additional Inherited Members
Data Fields inherited from AstRef
| ast
| ctx

## Detailed Description

    The sign of the numeral.

    >>> x = FPVal(+1.0, FPSort(8, 24))
    >>> x.sign()
    False
    >>> x = FPVal(-1.0, FPSort(8, 24))
    >>> x.sign()
    True

Definition at line 9562 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 9693 of file z3py.py.

9693 def as_string(self):
9694 s = Z3_get_numeral_string(self.ctx.ref(), self.as_ast())
9695 return ("FPVal(%s, %s)" % (s, self.sort()))
9696
9697
Z3_get_numeral_string
Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a)
Return numeral value, as a decimal string of a numeric constant term.

Referenced by IntNumRef.as_long(), BitVecNumRef.as_long(), and FiniteDomainNumRef.as_long().

## ◆ exponent()

def exponent | ( |  | self,
|  |  | biased = `True`
| ) |  |

Definition at line 9626 of file z3py.py.

9626 def exponent(self, biased=True):
9627 return Z3_fpa_get_numeral_exponent_string(self.ctx.ref(), self.as_ast(), biased)
9628
Z3_fpa_get_numeral_exponent_string
Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t, bool biased)
Return the exponent value of a floating-point numeral as a string.

## ◆ exponent_as_bv()

def exponent_as_bv | ( |  | self,
|  |  | biased = `True`
| ) |  |

Definition at line 9647 of file z3py.py.

9647 def exponent_as_bv(self, biased=True):
9648 return BitVecNumRef(Z3_fpa_get_numeral_exponent_bv(self.ctx.ref(), self.as_ast(), biased), self.ctx)
9649
Z3_fpa_get_numeral_exponent_bv
Z3_ast Z3_API Z3_fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t, bool biased)
Retrieves the exponent of a floating-point literal as a bit-vector expression.

## ◆ exponent_as_long()

def exponent_as_long | ( |  | self,
|  |  | biased = `True`
| ) |  |

Definition at line 9636 of file z3py.py.

9636 def exponent_as_long(self, biased=True):
9637 ptr = (ctypes.c_longlong * 1)()
9638 if not Z3_fpa_get_numeral_exponent_int64(self.ctx.ref(), self.as_ast(), ptr, biased):
9639 raise Z3Exception("error retrieving the exponent of a numeral.")
9640 return ptr[0]
9641
Z3_fpa_get_numeral_exponent_int64
bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, int64_t *n, bool biased)
Return the exponent value of a floating-point numeral as a signed 64-bit integer.

## ◆ isInf()

def isInf | ( |  | self | ) |

Definition at line 9657 of file z3py.py.

9657 def isInf(self):
9658 return Z3_fpa_is_numeral_inf(self.ctx.ref(), self.as_ast())
9659
Z3_fpa_is_numeral_inf
bool Z3_API Z3_fpa_is_numeral_inf(Z3_context c, Z3_ast t)
Checks whether a given floating-point numeral is a +oo or -oo.

## ◆ isNaN()

def isNaN | ( |  | self | ) |

Definition at line 9652 of file z3py.py.

9652 def isNaN(self):
9653 return Z3_fpa_is_numeral_nan(self.ctx.ref(), self.as_ast())
9654
Z3_fpa_is_numeral_nan
bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t)
Checks whether a given floating-point numeral is a NaN.

## ◆ isNegative()

def isNegative | ( |  | self | ) |

Definition at line 9682 of file z3py.py.

9682 def isNegative(self):
9683 return Z3_fpa_is_numeral_negative(self.ctx.ref(), self.as_ast())
9684
Z3_fpa_is_numeral_negative
bool Z3_API Z3_fpa_is_numeral_negative(Z3_context c, Z3_ast t)
Checks whether a given floating-point numeral is negative.

## ◆ isNormal()

def isNormal | ( |  | self | ) |

Definition at line 9667 of file z3py.py.

9667 def isNormal(self):
9668 return Z3_fpa_is_numeral_normal(self.ctx.ref(), self.as_ast())
9669
Z3_fpa_is_numeral_normal
bool Z3_API Z3_fpa_is_numeral_normal(Z3_context c, Z3_ast t)
Checks whether a given floating-point numeral is normal.

## ◆ isPositive()

def isPositive | ( |  | self | ) |

Definition at line 9677 of file z3py.py.

9677 def isPositive(self):
9678 return Z3_fpa_is_numeral_positive(self.ctx.ref(), self.as_ast())
9679
Z3_fpa_is_numeral_positive
bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t)
Checks whether a given floating-point numeral is positive.

## ◆ isSubnormal()

def isSubnormal | ( |  | self | ) |

Definition at line 9672 of file z3py.py.

9672 def isSubnormal(self):
9673 return Z3_fpa_is_numeral_subnormal(self.ctx.ref(), self.as_ast())
9674
Z3_fpa_is_numeral_subnormal
bool Z3_API Z3_fpa_is_numeral_subnormal(Z3_context c, Z3_ast t)
Checks whether a given floating-point numeral is subnormal.

## ◆ isZero()

def isZero | ( |  | self | ) |

Definition at line 9662 of file z3py.py.

9662 def isZero(self):
9663 return Z3_fpa_is_numeral_zero(self.ctx.ref(), self.as_ast())
9664
Z3_fpa_is_numeral_zero
bool Z3_API Z3_fpa_is_numeral_zero(Z3_context c, Z3_ast t)
Checks whether a given floating-point numeral is +zero or -zero.

## ◆ sign()

def sign | ( |  | self | ) |

Definition at line 9573 of file z3py.py.

9573 def sign(self):
9574 num = (ctypes.c_int)()
9575 nsign = Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(l))
9576 if nsign is False:
9577 raise Z3Exception("error retrieving the sign of a numeral.")
9578 return num.value != 0
9579
Z3_fpa_get_numeral_sign
bool Z3_API Z3_fpa_get_numeral_sign(Z3_context c, Z3_ast t, int *sgn)
Retrieves the sign of a floating-point literal.

## ◆ sign_as_bv()

def sign_as_bv | ( |  | self | ) |

Definition at line 9585 of file z3py.py.

9585 def sign_as_bv(self):
9586 return BitVecNumRef(Z3_fpa_get_numeral_sign_bv(self.ctx.ref(), self.as_ast()), self.ctx)
9587
Z3_fpa_get_numeral_sign_bv
Z3_ast Z3_API Z3_fpa_get_numeral_sign_bv(Z3_context c, Z3_ast t)
Retrieves the sign of a floating-point literal as a bit-vector expression.

## ◆ significand()

def significand | ( |  | self | ) |

Definition at line 9595 of file z3py.py.

9595 def significand(self):
9596 return Z3_fpa_get_numeral_significand_string(self.ctx.ref(), self.as_ast())
9597
Z3_fpa_get_numeral_significand_string
Z3_string Z3_API Z3_fpa_get_numeral_significand_string(Z3_context c, Z3_ast t)
Return the significand value of a floating-point numeral as a string.

## ◆ significand_as_bv()

def significand_as_bv | ( |  | self | ) |

Definition at line 9616 of file z3py.py.

9616 def significand_as_bv(self):
9617 return BitVecNumRef(Z3_fpa_get_numeral_significand_bv(self.ctx.ref(), self.as_ast()), self.ctx)
9618
Z3_fpa_get_numeral_significand_bv
Z3_ast Z3_API Z3_fpa_get_numeral_significand_bv(Z3_context c, Z3_ast t)
Retrieves the significand of a floating-point literal as a bit-vector expression.

## ◆ significand_as_long()

def significand_as_long | ( |  | self | ) |

Definition at line 9605 of file z3py.py.

9605 def significand_as_long(self):
9606 ptr = (ctypes.c_ulonglong * 1)()
9607 if not Z3_fpa_get_numeral_significand_uint64(self.ctx.ref(), self.as_ast(), ptr):
9608 raise Z3Exception("error retrieving the significand of a numeral.")
9609 return ptr[0]
9610
Z3_fpa_get_numeral_significand_uint64
bool Z3_API Z3_fpa_get_numeral_significand_uint64(Z3_context c, Z3_ast t, uint64_t *n)
Return the significand value of a floating-point numeral as a uint64.