PyMPF

The PyMPF library contains two modules intended for most users:

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:

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.

to_rational()

Convert from MPF to Rational

Raises AssertionError for infinities or NaN.

unpack()

Unpack into sign, exponent, and significand

Returns a tuple of integers (S, E, T) where S is the sign bit, E is the exponent, and T is the significand.

This is the inverse of pack().

exception mpf.floats.Not_Implemented_Yet
__weakref__

list of weak references to the object (if defined)

exception mpf.floats.Unspecified
__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() and fp_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
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.