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 (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 ;)
SMT-LIB random testcase generator
This will move to a new project. For now it is still available in the "python2" branch of PyMPF.
Requirements
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).
Documentation
This is very much work in progress and entirely incomplete (I just started adding this).
Installation
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
