Skip to main content

An arbitrary precision IEEE-754 implementation in Python

Project description


This is an arbitrary precision IEEE-754 floating point implementation.

The main motivation is correctness and test-case generation, so a number of things might seem a bit strange. This library has a bunch of limitations and should never be used if you want things to be fast. MPFR, SymFPU or Z3's MPF library are what you want.

Why "yet another" implementation?

  • This library supports RNA (MPFR does not)
  • This library supports subnormals and infinities (MPFR does, but only with tricks)
  • This library uses IEEE or SMTLIB terminology where possible (MPFR tends to stick to more "maths" terminology)
  • This library is implemented completely in Python unlike gmpy, mpmath, etc.
  • This library is an independent implementation so can be used to check Z3/SymFPU
  • This library uses a stupid but simple algorithm to do rounding

The main use of this library is random test-case generation for SMT-LIB. It has been used to validate the FP implementations of CVC4, Z3, MathSAT, SONOLAR, Alt-Ergo, Colibri, goSAT, and xsat; and has found bugs in all of them ;)


Python 3.5 or later.

There is also a Python2 port, but I don't plan to maintain it (although do shout if you need it).


This is very much work in progress and entirely incomplete (I just started adding this).


This package is available on PyPI. To install simply run:

$ pip3 install PyMPF

License and Copyright

Everything in this repository is licensed under the GNU GPL v3.

Key copyright holders that contributed to this library are:

  • Florian Schanda
  • Altran UK Limited
  • Zenuity AB

Project details

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

pympf-1.0.3.tar.gz (16.5 kB view hashes)

Uploaded source

Built Distribution

pympf-1.0.3-py3-none-any.whl (31.5 kB view hashes)

Uploaded py3

Supported by

AWS AWS Cloud computing Datadog Datadog Monitoring Facebook / Instagram Facebook / Instagram PSF Sponsor Fastly Fastly CDN Google Google Object Storage and Download Analytics Huawei Huawei PSF Sponsor Microsoft Microsoft PSF Sponsor NVIDIA NVIDIA PSF Sponsor Pingdom Pingdom Monitoring Salesforce Salesforce PSF Sponsor Sentry Sentry Error logging StatusPage StatusPage Status page