PyMPF¶
The PyMPF library contains two modules intended for most users:
- floats (arbitrary precision IEEE-754 floating point, see
mpf.floats.MPF
) - rationals (rational numbers, see
mpf.rationals.Rational
)
It also contains the following modules indended for internal use and the SMT-LIB testcase generator:
- bitvectors (very simple bitvector support, only literal printing currently)
- interval_q (rational intervals)
- bisect (binary search)
Fast tutorial¶
Import the relevant classes. Most likely you want to do this:
>>> from mpf.rationals import Rational
>>> from mpf.floats import *
You can now create a float like this (here we create a single precision float):
>>> x = MPF(8, 24)
To quickly see what we have we can use the
mpf.floats.MPF.to_python_string()
member function.
>>> x.to_python_string()
'0.0'
To set the float to a specific value, such as \(\frac{1}{3}\) we
can use the mpf.floats.MPF.from_rational()
member
function. Since we convert from rationals to floats we might need to
round.
>>> x.from_rational(RM_RNE, Rational(1, 3))
>>> x.to_python_string()
'0.3333333432674407958984375'
PyMPF supports all rounding modes defined by IEEE-754:
- RM_RNE (Round nearest even: to break ties, round to the nearest floating point number whos bit-pattern is even. This is the default on most desktop processors and programming languages.)
- RM_RNA (Round nearest away: to break ties, round to the floating point number furthest away from zero. Note that this is unsupported on most hardware (including i686 and amd64), other floating point libraries (e.g. MPFR).
- RM_RTZ (Round to zero: always round towards zero)
- RM_RTP (Round to positive: always round towards \(+\infty\))
- RM_RTN (Round to negative: always round towards \(-\infty\))
One of the main use-cases for this library is to generate test-cases
for SMT-LIB. To create an SMT-LIB literal you can use the
mpf.floats.MPF.smtlib_literal()
function:
>>> x.smtlib_literal()
'(fp #b0 #b01111101 #b01010101010101010101011)'
The MPF class supports all floating-point comparisons:
>>> y = MPF(8, 24)
>>> x > y
True
>>> y.set_nan()
>>> x > y
False
Note that equality considers +0 and -0 to be equal. You can use the
mpf.floats.smtlib_eq()
if you want bitwise equality:
>>> z = MPF(8, 24)
>>> z.set_zero(1)
>>> y.set_zero(0)
>>> y == z
True
>>> smtlib_eq(y, z)
False
To set values you can use the following functions:
mpf.floats.MPF.from_rational()
set to value closest to given rationalmpf.floats.MPF.set_zero()
set to +0 (if sign is 0) or -0 (if sign is 1)mpf.floats.MPF.set_infinite()
set to \(+\infty\) (if sign is 0) or \(-\infty\) (if sign is 1)mpf.floats.MPF.set_nan()
set to NaN. PyMPF does not support the distinction between signalling and non-signalling NaNs, similarly to SMT-LIB.
Finally, to do arithmetic, you can use the fp_* functions. Most take a rounding mode and two parameters:
>>> x.from_rational(RM_RNE, Rational(1, 10))
>>> y.from_rational(RM_RNE, Rational(10))
>>> z = fp_mul(RM_RNE, x, y)
>>> z.to_python_string()
'1.0'
Here an example demonstrating accumulated rounding errors:
>>> y.set_zero(0)
>>> for i in range(10):
>>> y = fp_add(RM_RNE, y, x)
>>> print(y.to_python_string())
0.100000001490116119384765625
0.20000000298023223876953125
0.300000011920928955078125
0.4000000059604644775390625
0.5
0.60000002384185791015625
0.7000000476837158203125
0.80000007152557373046875
0.900000095367431640625
1.00000011920928955078125
Rationals¶
This module defines class to deal with Rational numbers.
Todo
This should be a subclass of fractions.Fraction.
-
class
mpf.rationals.
Rational
(a=0, b=1)¶ Rational number
a is the numerator
b is the denominator
-
__abs__
()¶ Absolute value
-
__add__
(other)¶ Addition
-
__eq__
(other)¶ Equality
-
__ge__
(other)¶ >=
-
__gt__
(other)¶ >
-
__init__
(a=0, b=1)¶ Initialize self. See help(type(self)) for accurate signature.
-
__le__
(other)¶ <=
-
__lt__
(other)¶ <
-
__mul__
(other)¶ Multiplication
-
__ne__
(other)¶ Inequality
-
__neg__
()¶ Negation
-
__pow__
(other)¶ Exponentiation
The right-hand side must be an integral Rational, otherwise AssertionError is raised.
-
__repr__
()¶ Return repr(self).
-
__sub__
(other)¶ Substraction
-
__truediv__
(other)¶ Division
-
__weakref__
¶ list of weak references to the object (if defined)
-
isIntegral
()¶ Test if integral
-
isNegative
()¶ Test if negative
Returns false for 0.
-
isZero
()¶ Test if zero
-
to_decimal_string
()¶ Convert to decimal string
If the fraction does not terminate (e.g. for 1 / 3), an exception is thrown.
-
to_python_float
()¶ Convert to python float
-
to_python_int
()¶ Convert to python int
-
to_smtlib
()¶ Convert to SMT-LIB Real expression
Returns literal for integrals, e.g. “1.0”.
Returns an s-expression otherwise, e.g. “(- (/ 1.0 3.0))”.
-
-
mpf.rationals.
q_from_decimal_fragments
(sign, integer_part, fraction_part, exp_part)¶ Build a rational from string fragments of a decimal number.
- E.g. for “1.23E-1” we have fragments for
- sign = “” integer_part = “1” fraction_part = “23” exp_part = “-1”
-
mpf.rationals.
q_pow2
(number)¶ Create rational for 2^number
n can be negative
-
mpf.rationals.
q_round_rna
(n)¶ Round to nearest integer, away from zero
-
mpf.rationals.
q_round_rne
(n)¶ Round to nearest even integer
-
mpf.rationals.
q_round_rtn
(n)¶ Round to nearest integer, towards negative
-
mpf.rationals.
q_round_rtp
(n)¶ Round to nearest integer, towards positive
-
mpf.rationals.
q_round_rtz
(n)¶ Round to nearest integer, towards zero
-
mpf.rationals.
q_round_to_nearest
(n, tiebreak)¶ Round to nearest integer
Round n to the nearest integer
Calls the tiebreak*(upper, lower) function with the two alternatives if *n is precisely between two integers.
MPF¶
This module implements IEEE floats using bitvectors as the in-memory format, but rationals (plus rounding and special case handling) for calculation. This allows us to directly implement the semantics described in IEEE-754 (2008) without having to consider any of the difficult normalisation problems.
The main objective is that the implementation should be simple and simple to understand and as close to IEEE-754 and SMTLIB as possible (as opposed to fast) since the main use is the validation of other IEEE float implementations in SMT solvers (which have to be fast). It is also not a replacement for libraries such as MPFR (which is fast, but complicated and does not totally map onto IEEE floats).
-
class
mpf.floats.
MPF
(eb, sb, bitvec=0)¶ Arbitrary precision IEEE-754 floating point number
eb is the number of bits for the exponent.
sb is the number of bits for the significand.
This includes the “hidden bit”, so for example to create a single-precision floating point number we use:
>>> x = MPF(8, 24)
By default the created float is +0, however bitvec can be used to set the initial value. The expected format is an integer \(0 \le bitvec < 2^{eb+sb}\) corresponding to the binary interchange format. For example to create the single precision float representing +1:
>>> x = MPF(8, 24, 0x3f800000) >>> x.to_python_string() '1.0'
The lowest precision that is supported is MPF(2, 2). The largest eb supported is 18 (a practical limitation given we need to compute 2 ** (2 ** eb)) which can get pretty large pretty quickly.
-
__abs__
()¶ Compute absolute value
-
__eq__
(other)¶ Test floating-point equality
Note that this is floating-point equality, so comparisons to NaN always fail and -0 and +0 are considered equal.
If you want true equality, use
smtlib_eq()
-
__ge__
(other)¶ Test floating-point greater than or equal
-
__gt__
(other)¶ Test floating-point greater than
-
__init__
(eb, sb, bitvec=0)¶ Initialize self. See help(type(self)) for accurate signature.
-
__le__
(other)¶ Test floating-point less than or equal
-
__lt__
(other)¶ Test floating-point less than
-
__neg__
()¶ Compute inverse
-
__repr__
()¶ Return repr(self).
-
__str__
()¶ Return str(self).
-
__weakref__
¶ list of weak references to the object (if defined)
-
compatible
(other)¶ Test if another MPF has the same precision
-
from_rational
(rm, q)¶ Convert from rational to MPF
Sets the value to the nearest representable floating-point value described by q, rounded according to rm.
-
inf_boundary
()¶ Compute the point after which we round to infinity
Determines the (positive) boundary for rounding modes RNE and RNA, at which point we always round to infinity. Numbers smaller than this may be rounded to infinity, but numbers larger than this will always be rounded to infinity.
>>> MPF(8, 24).inf_boundary() Rational(340282356779733661637539395458142568448)
This is usually an integer, except for pathological precisions.
>>> MPF(2, 2).inf_boundary() Rational(7, 2)
Note that IEEE 754 is not precisely clear if numbers equal to or larger than this, or just larger than this are rounded to infinty. We have decided to interpret it as equal to or larger.
-
isFinite
()¶ Test if value is finite
Returns true for zero, subnormals, or normal numbers.
Returns false for infinities, and not a number.
-
isInfinite
()¶ Test if value is infinite
-
isIntegral
()¶ Test if value is integral
Returns true if the floating-point value is an integer, and false in all other cases (including infinities and not a number).
-
isNaN
()¶ Test if value is not a number
-
isNegative
()¶ Test if value is negative
Returns always false for NaN.
-
isNormal
()¶ Test if value is normal
-
isPositive
()¶ Test if value is positive
Returns always false for NaN.
-
isSubnormal
()¶ Test if value is subnormal
-
isZero
()¶ Test if value is zero
-
new_mpf
()¶ Copy constructor
Returns a new MPF with the same precision and value.
-
pack
(S, E, T)¶ Pack sign, exponent, and significand
Sets the value of the floating point number, such that
The sign corresponds to S, the exponent is E, and the significand is T.
This is the inverse of
unpack()
.
-
set_infinite
(sign)¶ Set value to infinite with the given sign bit
-
set_nan
()¶ Set value to NaN
-
set_sign_bit
(sign)¶ Set sign bit
-
set_zero
(sign)¶ Set value to zero with the given sign bit
-
smtlib_from_binary_interchange
()¶ SMT-LIB function for converting from bitvector
-
smtlib_from_float
()¶ SMT-LIB function for converting from FloatingPoint
-
smtlib_from_int
()¶ SMT-LIB function for converting from Int
-
smtlib_from_real
()¶ SMT-LIB function for converting from Real
-
smtlib_from_sbv
()¶ SMT-LIB function for converting from signed bitvector
-
smtlib_from_ubv
()¶ SMT-LIB function for converting from unsigned bitvector
-
smtlib_literal
()¶ Return an SMT-LIB literal
Favours special cases, such as (_ +zero 8 24), otherwise returns literals of the form (fp …).
-
smtlib_literals
()¶ Return list of all possible SMTLIB literals
Includes:
- Binary interchange conversion, e.g. ((_ to_fp 8 24) #x00000000)
- FP literal, e.g. (fp #b0 #b00 #b000)
- Special value, e.g. (_ +zero 2 4)
-
smtlib_random_literal
()¶ Return an SMT-LIB literal (randomly chosen)
Chooses randomly from
smtlib_literals()
.
-
smtlib_sort
()¶ SMT-LIB sort
Returns “Float16”, “Float32”, “Float64”, or “Float128” if possible.
Returns “(_ FloatingPoint eb sb)” otherwise.
-
smtlib_to_int
()¶ SMT-LIB function for converting to Int
-
smtlib_to_real
()¶ SMT-LIB function for converting to Real
-
to_int
(rm)¶ Convert from MPF to Python int`
Raises AssertionError for infinities and NaN. Returns the integer closest to the floating point, rounded according to rm.
-
to_python_float
()¶ Convert from MPF to Python float`
Convert to python float. Do not rely on this to be precise for now.
Todo
Use sys.float_info to first convert to the correct format and then directly interpret the bit-pattern.
If you want something precise, then use
to_python_string()
instead.
-
to_python_string
()¶ Convert from MPF to Python string`
Return a string describing the float. We return a decimal string (e.g. ‘0.25’), except for the following special cases: ‘-0’, ‘Infinity’, ‘-Infinity’, and ‘NaN’.
The decimal string might be very long (but precise), so if you want something compact then
to_python_float()
might be more appropriate.
-
-
exception
mpf.floats.
Not_Implemented_Yet
¶ -
__weakref__
¶ list of weak references to the object (if defined)
-
-
mpf.floats.
fp_add
(rm, left, right)¶ Floating-point addition
Performs a correctly rounded \(left + right\). The following special cases apply:
- NaN propagates
- Adding opposite infinities results in NaN, otherwise infinities propagate
- If the precise result is exactly 0 (i.e. 0 + 0 or a + -a) then we
special case according to Section 6.3 in IEEE-754:
- we preserve the sign if left and right have the same sign
- otherwise, we return -0 if the rounding mode is RTN
- otherwise, we return +0
-
mpf.floats.
fp_div
(rm, left, right)¶ Floating-point division
Performs a correctly rounded \(left \div right\). The following special cases apply:
- NaN propagates
- When dividing by infinity
- NaN when dividing two infinities
- 0 otherwise
- When dividing by zero
- NaN when dividing zero by zero
- Infinity otherwise
-
mpf.floats.
fp_fma
(rm, x, y, z)¶ Floating-point fused multiply add
Performs a correctly rounded \(x * y + z\). The special cases of
fp_mul()
andfp_add()
apply, and in addition:- On a precise 0 result the sign of zero is:
- Preserved if the sign of x * y is the same as z
- -0 for RTN
- +0 otherwise
- On a precise 0 result the sign of zero is:
-
mpf.floats.
fp_from_float
(eb, sb, rm, op)¶ Conversion from MPF to MPF (of a different precision)
-
mpf.floats.
fp_from_int
(eb, sb, rm, op)¶ Conversion from Python integer to MPF
-
mpf.floats.
fp_from_sbv
(eb, sb, rm, op)¶ Conversion from signed bitvector to MPF
-
mpf.floats.
fp_from_ubv
(eb, sb, rm, op)¶ Conversion from unsigned bitvector to MPF
-
mpf.floats.
fp_max
(left, right)¶ Floating-point maximum
-
mpf.floats.
fp_min
(left, right)¶ Floating-point minimum
-
mpf.floats.
fp_mul
(rm, left, right)¶ Floating-point multiplication
Performs a correctly rounded \(left * right\). The following special cases apply:
- NaN propagates
- Infinities propagate (for non-zero operands)
- Multiplying by zero gives the following results
- NaN if the other operand is infinite
- 0 of the same sign as the 0 operand
-
mpf.floats.
fp_nextDown
(op)¶ Floating-point predecessor
-
mpf.floats.
fp_nextUp
(op)¶ Floating-point successor
-
mpf.floats.
fp_rem
(left, right)¶ Floating-point remainder
-
mpf.floats.
fp_roundToIntegral
(rm, op)¶ Floating-point round to integer
-
mpf.floats.
fp_sqrt
(rm, op)¶ Floating-point square root
-
mpf.floats.
fp_sub
(rm, left, right)¶ Floating-point substraction
Performs a correctly rounded \(left - right\), which is equivalent to \(left + -right\).
See
fp_add()
for special cases.
-
mpf.floats.
fp_to_int
(rm, op)¶ Conversion from MPF to Python integer
-
mpf.floats.
fp_to_sbv
(op, rm, width)¶ Conversion from MPF to signed bitvector
-
mpf.floats.
fp_to_ubv
(op, rm, width)¶ Conversion from MPF to unsigned bitvector
-
mpf.floats.
smtlib_eq
(left, right)¶ Bit-wise equality
Changelog¶
1.0¶
1.0.4 (2020-05-20)¶
- We now run PyLint
- Support pathological precisions such as MPF(2, 2) where the infinity boundary is in fact not an integer (3.5 in this example).
- Add practical limit on the size of the exponent of 18. The infinity boundary evaluates 2 ** 2 ** eb, which obviously grows very fast.
- More support for older python versions. We still target and support 3.6+, but it makes it a bit less painless to use on non-supported versions.
1.0.3 (2019-03-18)¶
- Add basic documentation (fast tutorial, and basic descriptions of MPF and Rational classes).
1.0.2 (2019-03-13)¶
- First public release on PyPI.