Copyright | (c) Galois Inc 2016-2020 |
---|---|

License | BSD3 |

Maintainer | jhendrix@galois.com |

Safe Haskell | None |

Language | Haskell2010 |

Defines a numeric data-type where each number is represented as the root of a polynomial over a single variable.

This currently only defines operations for parsing the roots from the format generated by Yices, and evaluating a polynomial over rational coefficients to the rational derived from the closest double.

## Synopsis

- data Root c
- approximate :: Root Rational -> Rational
- fromYicesText :: Text -> Maybe (Root Rational)
- parseYicesRoot :: Parser (Root Rational)

# Documentation

approximate :: Root Rational -> Rational Source #

This either returns the root exactly, or it computes the closest double precision approximation of the root.

Underneath the hood, this uses rational arithmetic to guarantee precision, so this operation is relatively slow. However, it is guaranteed to provide an exact answer.

If performance is a concern, there are faster algorithms for computing this.