Skip to main content

An arbitrary precision IEEE-754 implementation in Python

Project description

PyMPF

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 (unlike MPFR)
  • This library is done completely in Python unlike gmpy, mpmath, etc.
  • This library is an independent implementation so can be used to check Z3/CVC4
  • 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 ;)

License and Copyright

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

All code is written by Florian Schanda and is :copyright: Altran UK Limited and :copyright: 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.2.tar.gz (13.6 kB view hashes)

Uploaded source

Built Distribution

pympf-1.0.2-py3-none-any.whl (28.7 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