Copyright	(c) Galois Inc 2016-2020
License	BSD3
Maintainer	jhendrix@galois.com
Safe Haskell	None
Language	Haskell2010

What4.Protocol.PolyRoot

Description

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

data Root c Source #

Instances

Show c => Show (Root c) Source #
Instance details Defined in What4.Protocol.PolyRoot Methods showsPrec :: Int -> Root c -> ShowS # show :: Root c -> String # showList :: [Root c] -> ShowS #
(Ord c, Num c, Pretty c) => Pretty (Root c) Source #
Instance details Defined in What4.Protocol.PolyRoot Methods pretty :: Root c -> Doc # prettyList :: [Root c] -> Doc #

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.

fromYicesText :: Text -> Maybe (Root Rational) Source #

Convert text to a root

parseYicesRoot :: Parser (Root Rational) Source #