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)
fpPosZero :: IsExprBuilder sym => sym -> Integer -> Integer -> IO (SFloat sym)
fpNegZero :: 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
fpNe :: IsExprBuilder sym => SFloatRel sym
fpEqIEEE :: IsExprBuilder sym => SFloatRel sym
fpNeIEEE :: IsExprBuilder sym => SFloatRel sym
fpLeIEEE :: IsExprBuilder sym => SFloatRel sym
fpLtIEEE :: IsExprBuilder sym => SFloatRel sym
fpGeIEEE :: IsExprBuilder sym => SFloatRel sym
fpGtIEEE :: IsExprBuilder sym => SFloatRel sym
fpUnordered :: 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
fpRem :: IsExprBuilder sym => sym -> SFloat sym -> SFloat sym -> IO (SFloat 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)
fpCast :: IsExprBuilder sym => sym -> Integer -> Integer -> RoundingMode -> SFloat sym -> IO (SFloat sym)
fpFromBV :: IsExprBuilder sym => sym -> Integer -> Integer -> RoundingMode -> SWord sym -> IO (SFloat sym)
fpFromSBV :: IsExprBuilder sym => sym -> Integer -> Integer -> RoundingMode -> SWord sym -> IO (SFloat sym)
fpToBV :: IsExprBuilder sym => sym -> Natural -> RoundingMode -> SFloat sym -> IO (SWord sym)
fpToSBV :: IsExprBuilder sym => sym -> Natural -> RoundingMode -> SFloat sym -> IO (SWord 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)
fpIsPos :: 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 #

See asFloat.

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

See floatIte.

Constants

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

A fresh variable of the given type (see freshConstant).

fpNaN Source #

Arguments

:: IsExprBuilder sym
=> sym
-> Integer	Exponent width
-> Integer	Precision width
-> IO (SFloat sym)

Not a number (see floatNaN).

fpPosZero Source #

Arguments

:: IsExprBuilder sym
=> sym
-> Integer	Exponent width
-> Integer	Precision width
-> IO (SFloat sym)

Positive zero (see floatPZero).

fpNegZero Source #

Arguments

:: IsExprBuilder sym
=> sym
-> Integer	Exponent width
-> Integer	Precision width
-> IO (SFloat sym)

Negative zero (see floatNZero).

fpPosInf Source #

Arguments

:: IsExprBuilder sym
=> sym
-> Integer	Exponent width
-> Integer	Precision width
-> IO (SFloat sym)

Positive infinity (see floatPInf).

fpNegInf Source #

Arguments

:: IsExprBuilder sym
=> sym
-> Integer	Exponent width
-> Integer	Precision width
-> IO (SFloat sym)

Negative infinity (see floatNInf).

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 (see floatLit).

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 (see floatLitRational).

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 (see floatFromBinary).

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

See floatToBinary.

Relations

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

fpEq :: IsExprBuilder sym => SFloatRel sym Source #

See floatEq.

fpNe :: IsExprBuilder sym => SFloatRel sym Source #

See floatNe.

fpEqIEEE :: IsExprBuilder sym => SFloatRel sym Source #

See floatFpEq.

fpNeIEEE :: IsExprBuilder sym => SFloatRel sym Source #

See floatFpApart.

fpLeIEEE :: IsExprBuilder sym => SFloatRel sym Source #

See floatLe.

fpLtIEEE :: IsExprBuilder sym => SFloatRel sym Source #

See floatLt.

fpGeIEEE :: IsExprBuilder sym => SFloatRel sym Source #

See floatGe.

fpGtIEEE :: IsExprBuilder sym => SFloatRel sym Source #

See floatGt.

fpUnordered :: IsExprBuilder sym => SFloatRel sym Source #

See floatFpUnordered.

Arithmetic

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

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

See floatNeg.

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

See floatAbs.

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

See floatSqrt.

fpAdd :: IsExprBuilder sym => SFloatBinArith sym Source #

See floatAdd.

fpSub :: IsExprBuilder sym => SFloatBinArith sym Source #

See floatSub.

fpMul :: IsExprBuilder sym => SFloatBinArith sym Source #

See floatMul.

fpDiv :: IsExprBuilder sym => SFloatBinArith sym Source #

See floatDiv.

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

See floatRem.

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

See floatMin.

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

See floatMax.

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

See floatRMA.

Conversions

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

See floatRound.

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

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

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

See realToFloat.

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 #

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

Change the precision of a floating point number (see floatCast).

fpFromBV :: IsExprBuilder sym => sym -> Integer -> Integer -> RoundingMode -> SWord sym -> IO (SFloat sym) Source #

Convert a unsigned bitvector to a floating point number (see bvToFloat).

fpFromSBV :: IsExprBuilder sym => sym -> Integer -> Integer -> RoundingMode -> SWord sym -> IO (SFloat sym) Source #

Convert a signed bitvector to a floating point number (see sbvToFloat).

fpToBV :: IsExprBuilder sym => sym -> Natural -> RoundingMode -> SFloat sym -> IO (SWord sym) Source #

Convert a floating point number to a unsigned bitvector (see floatToBV). Precondition: the supplied Natural (the bit width of the returned bitvector) is non-zero.

fpToSBV :: IsExprBuilder sym => sym -> Natural -> RoundingMode -> SFloat sym -> IO (SWord sym) Source #

Convert a floating point number to a signed bitvector (see floatToSBV). Precondition: the supplied Natural (the bit width of the returned bitvector) is non-zero.

Queries

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

See floatIsInf.

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

See floatIsNaN.

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

See floatIsZero.

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

See floatIsNeg.

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

See floatIsPos.

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

See floatIsSubnorm.

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

See floatIsNorm.

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 # fromException :: SomeException -> Maybe UnsupportedFloat # displayException :: UnsupportedFloat -> String #
Show UnsupportedFloat Source #
Instance details Defined in What4.SFloat Methods showsPrec :: Int -> UnsupportedFloat -> ShowS # show :: UnsupportedFloat -> String # showList :: [UnsupportedFloat] -> ShowS #

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 # fromException :: SomeException -> Maybe FPTypeError # displayException :: FPTypeError -> String #
Show FPTypeError Source #
Instance details Defined in What4.SFloat Methods showsPrec :: Int -> FPTypeError -> ShowS # show :: FPTypeError -> String # showList :: [FPTypeError] -> ShowS #