what4-1.1: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2016-2020
LicenseBSD3
Maintainerjhendrix@galois.com
Safe HaskellNone
LanguageHaskell2010

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

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 #

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 ann #

prettyList :: [Root c] -> Doc ann #

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