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, SoftFloat, or SymFPU is 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, CVC5, Z3, MathSAT, BitWuzla, SONOLAR, Alt-Ergo, Colibri, goSAT, and xsat; and has found bugs in all of them ;)

SMT-LIB random testcase generator

See https://github.com/florianschanda/smtlib_schanda

Requirements

Python 3.8 or later.

Documentation

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

• PyMPF API Documentation

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