what4-1.5.1: Solver-agnostic symbolic values support for issuing queries

Copyright | (c) Galois Inc 2016-2020
License | BSD3
Maintainer | jhendrix@galois.com
Safe Haskell | Safe-Inferred
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

Instances details

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

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 #