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

Safe Haskell | None
Language | Haskell2010

What4.SFloat

Contents

- Interface
- Constants
- Interchange formats
- Relations
- Arithmetic
- Conversions
- Queries
- Exceptions

Description

Working with floats of dynamic sizes.

Synopsis

- data SFloat sym where
  - SFloat :: forall sym (fpp :: FloatPrecision). IsExpr (SymExpr sym) => SymFloat sym fpp -> SFloat sym
- fpReprOf :: forall sym (fpp :: FloatPrecision). IsExpr (SymExpr sym) => sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
- fpSize :: SFloat sym -> (Integer, Integer)
- fpRepr :: Integer -> Integer -> Maybe (Some FloatPrecisionRepr)
- fpAsLit :: SFloat sym -> Maybe BigFloat
- fpIte :: IsExprBuilder sym => sym -> Pred sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
- fpFresh :: IsSymExprBuilder sym => sym -> Integer -> Integer -> IO (SFloat sym)
- fpNaN :: IsExprBuilder sym => sym -> Integer -> Integer -> IO (SFloat sym)
- fpPosInf :: IsExprBuilder sym => sym -> Integer -> Integer -> IO (SFloat sym)
- fpNegInf :: IsExprBuilder sym => sym -> Integer -> Integer -> IO (SFloat sym)
- fpFromLit :: IsExprBuilder sym => sym -> Integer -> Integer -> BigFloat -> IO (SFloat sym)
- fpFromRationalLit :: IsExprBuilder sym => sym -> Integer -> Integer -> Rational -> IO (SFloat sym)
- fpFromBinary :: IsExprBuilder sym => sym -> Integer -> Integer -> SWord sym -> IO (SFloat sym)
- fpToBinary :: IsExprBuilder sym => sym -> SFloat sym -> IO (SWord sym)
- type SFloatRel sym = sym -> SFloat sym -> SFloat sym -> IO (Pred sym)
- fpEq :: IsExprBuilder sym => SFloatRel sym
- fpEqIEEE :: IsExprBuilder sym => SFloatRel sym
- fpLtIEEE :: IsExprBuilder sym => SFloatRel sym
- fpGtIEEE :: IsExprBuilder sym => SFloatRel sym
- type SFloatBinArith sym = sym -> RoundingMode -> SFloat sym -> SFloat sym -> IO (SFloat sym)
- fpNeg :: IsExprBuilder sym => sym -> SFloat sym -> IO (SFloat sym)
- fpAbs :: IsExprBuilder sym => sym -> SFloat sym -> IO (SFloat sym)
- fpSqrt :: IsExprBuilder sym => sym -> RoundingMode -> SFloat sym -> IO (SFloat sym)
- fpAdd :: IsExprBuilder sym => SFloatBinArith sym
- fpSub :: IsExprBuilder sym => SFloatBinArith sym
- fpMul :: IsExprBuilder sym => SFloatBinArith sym
- fpDiv :: IsExprBuilder sym => SFloatBinArith sym
- fpMin :: IsExprBuilder sym => sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
- fpMax :: IsExprBuilder sym => sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
- fpFMA :: IsExprBuilder sym => sym -> RoundingMode -> SFloat sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
- fpRound :: IsExprBuilder sym => sym -> RoundingMode -> SFloat sym -> IO (SFloat sym)
- fpToReal :: IsExprBuilder sym => sym -> SFloat sym -> IO (SymReal sym)
- fpFromReal :: IsExprBuilder sym => sym -> Integer -> Integer -> RoundingMode -> SymReal sym -> IO (SFloat sym)
- fpFromRational :: IsExprBuilder sym => sym -> Integer -> Integer -> RoundingMode -> SymInteger sym -> SymInteger sym -> IO (SFloat sym)
- fpToRational :: IsSymExprBuilder sym => sym -> SFloat sym -> IO (Pred sym, SymInteger sym, SymInteger sym)
- fpFromInteger :: IsExprBuilder sym => sym -> Integer -> Integer -> RoundingMode -> SymInteger sym -> IO (SFloat sym)
- fpIsInf :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
- fpIsNaN :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
- fpIsZero :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
- fpIsNeg :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
- fpIsSubnorm :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
- fpIsNorm :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
- data UnsupportedFloat = UnsupportedFloat {
  - fpWho :: String
  - exponentBits :: Integer
  - precisionBits :: Integer
  }
- data FPTypeError = FPTypeError {
  - fpExpected :: Some BaseTypeRepr
  - fpActual :: Some BaseTypeRepr
  }

# Interface

data SFloat sym where Source #

Symbolic floating point numbers.

Constructors

SFloat :: forall sym (fpp :: FloatPrecision). IsExpr (SymExpr sym) => SymFloat sym fpp -> SFloat sym |

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

fpSize :: SFloat sym -> (Integer, Integer) Source #

fpRepr Source #

Arguments

:: Integer | Exponent width
-> Integer | Precision width
-> Maybe (Some FloatPrecisionRepr) |

Construct the `FloatPrecisionRepr` with the given parameters.

fpAsLit :: SFloat sym -> Maybe BigFloat Source #

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 #

fpEq :: IsExprBuilder sym => SFloatRel sym Source #

fpEqIEEE :: IsExprBuilder sym => SFloatRel sym Source #

fpLtIEEE :: IsExprBuilder sym => SFloatRel sym Source #

fpGtIEEE :: IsExprBuilder sym => SFloatRel 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 #

fpAdd :: IsExprBuilder sym => SFloatBinArith sym Source #

fpSub :: IsExprBuilder sym => SFloatBinArith sym Source #

fpMul :: IsExprBuilder sym => SFloatBinArith sym Source #

fpDiv :: IsExprBuilder sym => SFloatBinArith 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 #

fpFromRational :: IsExprBuilder sym => sym -> Integer -> Integer -> RoundingMode -> SymInteger sym -> SymInteger 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.

fpFromInteger :: IsExprBuilder sym => sym -> Integer -> Integer -> RoundingMode -> SymInteger sym -> IO (SFloat sym) Source #

# 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

Constructors

UnsupportedFloat |

Fields

- fpWho :: String
- exponentBits :: Integer
- precisionBits :: Integer

#### Instances

Instances details

Exception UnsupportedFloat Source # |
Instance details Defined in What4.SFloat Methods toException :: UnsupportedFloat -> SomeException Source # fromException :: SomeException -> Maybe UnsupportedFloat Source # displayException :: UnsupportedFloat -> String Source # backtraceDesired :: UnsupportedFloat -> Bool Source #
Show UnsupportedFloat Source # |
Instance details Defined in What4.SFloat Methods showsPrec :: Int -> UnsupportedFloat -> ShowS Source # show :: UnsupportedFloat -> String Source # showList :: [UnsupportedFloat] -> ShowS Source #

data FPTypeError Source #

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

Constructors

FPTypeError |

Fields

- fpExpected :: Some BaseTypeRepr
- fpActual :: Some BaseTypeRepr

#### Instances

Instances details

Exception FPTypeError Source # |
Instance details Defined in What4.SFloat Methods toException :: FPTypeError -> SomeException Source # fromException :: SomeException -> Maybe FPTypeError Source # displayException :: FPTypeError -> String Source # backtraceDesired :: FPTypeError -> Bool Source #
Show FPTypeError Source # |
Instance details Defined in What4.SFloat Methods showsPrec :: Int -> FPTypeError -> ShowS Source # show :: FPTypeError -> String Source # showList :: [FPTypeError] -> ShowS Source #