what4-1.3: Solver-agnostic symbolic values support for issuing queries
Safe HaskellNone
LanguageHaskell2010

What4.SFloat

Description

Working with floats of dynamic sizes.

Synopsis

Interface

data SFloat sym where Source #

Symbolic floating point numbers.

Constructors

SFloat :: IsExpr (SymExpr sym) => SymFloat sym fpp -> SFloat sym 

fpReprOf :: IsExpr (SymExpr sym) => sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp Source #

fpRepr Source #

Arguments

:: Integer

Exponent width

-> Integer

Precision width

-> Maybe (Some FloatPrecisionRepr) 

Construct the FloatPrecisionRepr with the given parameters.

fpIte :: IsExprBuilder sym => sym -> Pred sym -> SFloat sym -> SFloat sym -> IO (SFloat sym) Source #

Constants

fpFresh :: IsSymExprBuilder sym => sym -> Integer -> Integer -> IO (SFloat sym) Source #

A fresh variable of the given type.

fpNaN Source #

Arguments

:: IsExprBuilder sym 
=> sym 
-> Integer

Exponent width

-> Integer

Precision width

-> IO (SFloat sym) 

Not a number

fpPosInf Source #

Arguments

:: IsExprBuilder sym 
=> sym 
-> Integer

Exponent width

-> Integer

Precision width

-> IO (SFloat sym) 

Positive infinity

fpNegInf Source #

Arguments

:: IsExprBuilder sym 
=> sym 
-> Integer

Exponent width

-> Integer

Precision width

-> IO (SFloat sym) 

Negative infinity

fpFromLit Source #

Arguments

:: IsExprBuilder sym 
=> sym 
-> Integer

Exponent width

-> Integer

Precision width

-> BigFloat 
-> IO (SFloat sym) 

A floating point number corresponding to the given BigFloat.

fpFromRationalLit Source #

Arguments

:: IsExprBuilder sym 
=> sym 
-> Integer

Exponent width

-> Integer

Precision width

-> Rational 
-> IO (SFloat sym) 

A floating point number corresponding to the given rational.

Interchange formats

fpFromBinary Source #

Arguments

:: IsExprBuilder sym 
=> sym 
-> Integer

Exponent width

-> Integer

Precision width

-> SWord sym 
-> IO (SFloat sym) 

Make a floating point number with the given bit representation.

fpToBinary :: IsExprBuilder sym => sym -> SFloat sym -> IO (SWord sym) Source #

Relations

type SFloatRel sym = sym -> SFloat sym -> SFloat sym -> IO (Pred sym) Source #

Arithmetic

type SFloatBinArith sym = sym -> RoundingMode -> SFloat sym -> SFloat sym -> IO (SFloat sym) Source #

fpNeg :: IsExprBuilder sym => sym -> SFloat sym -> IO (SFloat sym) Source #

fpAbs :: IsExprBuilder sym => sym -> SFloat sym -> IO (SFloat sym) Source #

fpSqrt :: IsExprBuilder sym => sym -> RoundingMode -> SFloat sym -> IO (SFloat sym) Source #

fpMin :: IsExprBuilder sym => sym -> SFloat sym -> SFloat sym -> IO (SFloat sym) Source #

fpMax :: IsExprBuilder sym => sym -> SFloat sym -> SFloat sym -> IO (SFloat sym) Source #

fpFMA :: IsExprBuilder sym => sym -> RoundingMode -> SFloat sym -> SFloat sym -> SFloat sym -> IO (SFloat sym) Source #

Conversions

fpRound :: IsExprBuilder sym => sym -> RoundingMode -> SFloat sym -> IO (SFloat sym) Source #

fpToReal :: IsExprBuilder sym => sym -> SFloat sym -> IO (SymReal sym) Source #

This is undefined on "special" values (NaN,infinity)

fpFromReal :: IsExprBuilder sym => sym -> Integer -> Integer -> RoundingMode -> SymReal sym -> IO (SFloat sym) Source #

fpToRational :: IsSymExprBuilder sym => sym -> SFloat sym -> IO (Pred sym, SymInteger sym, SymInteger sym) Source #

Returns a predicate and two integers, x and y. If the the predicate holds, then x / y is a rational representing the floating point number. Assumes the FP number is not one of the special ones that has no real representation.

Queries

fpIsInf :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym) Source #

fpIsNaN :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym) Source #

fpIsZero :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym) Source #

fpIsNeg :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym) Source #

fpIsSubnorm :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym) Source #

fpIsNorm :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym) Source #

Exceptions

data UnsupportedFloat Source #

This exception is thrown if the operations try to create a floating point value we do not support

data FPTypeError Source #

This exceptoin is throws if the types don't match.