Safe Haskell	None
Language	Haskell2010

What4.InterpretedFloatingPoint

Contents

FloatInfo data kind
Interface classes

Synopsis

data FloatInfo
type HalfFloat = HalfFloat
type SingleFloat = SingleFloat
type DoubleFloat = DoubleFloat
type QuadFloat = QuadFloat
type X86_80Float = X86_80Float
type DoubleDoubleFloat = DoubleDoubleFloat
data FloatInfoRepr (fi :: FloatInfo) where
- HalfFloatRepr :: FloatInfoRepr HalfFloat
- SingleFloatRepr :: FloatInfoRepr SingleFloat
- DoubleFloatRepr :: FloatInfoRepr DoubleFloat
- QuadFloatRepr :: FloatInfoRepr QuadFloat
- X86_80FloatRepr :: FloatInfoRepr X86_80Float
- DoubleDoubleFloatRepr :: FloatInfoRepr DoubleDoubleFloat
data X86_80Val = X86_80Val Word16 Word64
fp80ToBits :: X86_80Val -> Integer
fp80ToRational :: X86_80Val -> Maybe Rational
type family FloatInfoToPrecision (fi :: FloatInfo) :: FloatPrecision where ...
type family FloatPrecisionToInfo (fpp :: FloatPrecision) :: FloatInfo where ...
floatInfoToPrecisionRepr :: FloatInfoRepr fi -> FloatPrecisionRepr (FloatInfoToPrecision fi)
floatPrecisionToInfoRepr :: FloatPrecisionRepr fpp -> FloatInfoRepr (FloatPrecisionToInfo fpp)
type family FloatInfoToBitWidth (fi :: FloatInfo) :: Nat where ...
floatInfoToBVTypeRepr :: FloatInfoRepr fi -> BaseTypeRepr (BaseBVType (FloatInfoToBitWidth fi))
type family SymInterpretedFloatType (sym :: Type) (fi :: FloatInfo) :: BaseType
type SymInterpretedFloat sym fi = SymExpr sym (SymInterpretedFloatType sym fi)
class IsExprBuilder sym => IsInterpretedFloatExprBuilder sym where
- iFloatPZero :: sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
- iFloatNZero :: sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
- iFloatNaN :: sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
- iFloatPInf :: sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
- iFloatNInf :: sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
- iFloatLit :: sym -> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat sym fi)
- iFloatLitSingle :: sym -> Float -> IO (SymInterpretedFloat sym SingleFloat)
- iFloatLitDouble :: sym -> Double -> IO (SymInterpretedFloat sym DoubleFloat)
- iFloatLitLongDouble :: sym -> X86_80Val -> IO (SymInterpretedFloat sym X86_80Float)
- iFloatNeg :: sym -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi)
- iFloatAbs :: sym -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi)
- iFloatSqrt :: sym -> RoundingMode -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi)
- iFloatAdd :: sym -> RoundingMode -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi)
- iFloatSub :: sym -> RoundingMode -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi)
- iFloatMul :: sym -> RoundingMode -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi)
- iFloatDiv :: sym -> RoundingMode -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi)
- iFloatRem :: sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi)
- iFloatMin :: sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi)
- iFloatMax :: sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi)
- iFloatFMA :: sym -> RoundingMode -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi)
- iFloatEq :: sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (Pred sym)
- iFloatNe :: sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (Pred sym)
- iFloatFpEq :: sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (Pred sym)
- iFloatFpNe :: sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (Pred sym)
- iFloatLe :: sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (Pred sym)
- iFloatLt :: sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (Pred sym)
- iFloatGe :: sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (Pred sym)
- iFloatGt :: sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (Pred sym)
- iFloatIsNaN :: sym -> SymInterpretedFloat sym fi -> IO (Pred sym)
- iFloatIsInf :: sym -> SymInterpretedFloat sym fi -> IO (Pred sym)
- iFloatIsZero :: sym -> SymInterpretedFloat sym fi -> IO (Pred sym)
- iFloatIsPos :: sym -> SymInterpretedFloat sym fi -> IO (Pred sym)
- iFloatIsNeg :: sym -> SymInterpretedFloat sym fi -> IO (Pred sym)
- iFloatIsSubnorm :: sym -> SymInterpretedFloat sym fi -> IO (Pred sym)
- iFloatIsNorm :: sym -> SymInterpretedFloat sym fi -> IO (Pred sym)
- iFloatIte :: sym -> Pred sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi)
- iFloatCast :: sym -> FloatInfoRepr fi -> RoundingMode -> SymInterpretedFloat sym fi' -> IO (SymInterpretedFloat sym fi)
- iFloatRound :: sym -> RoundingMode -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi)
- iFloatFromBinary :: sym -> FloatInfoRepr fi -> SymBV sym (FloatInfoToBitWidth fi) -> IO (SymInterpretedFloat sym fi)
- iFloatToBinary :: sym -> FloatInfoRepr fi -> SymInterpretedFloat sym fi -> IO (SymBV sym (FloatInfoToBitWidth fi))
- iBVToFloat :: 1 <= w => sym -> FloatInfoRepr fi -> RoundingMode -> SymBV sym w -> IO (SymInterpretedFloat sym fi)
- iSBVToFloat :: 1 <= w => sym -> FloatInfoRepr fi -> RoundingMode -> SymBV sym w -> IO (SymInterpretedFloat sym fi)
- iRealToFloat :: sym -> FloatInfoRepr fi -> RoundingMode -> SymReal sym -> IO (SymInterpretedFloat sym fi)
- iFloatToBV :: 1 <= w => sym -> NatRepr w -> RoundingMode -> SymInterpretedFloat sym fi -> IO (SymBV sym w)
- iFloatToSBV :: 1 <= w => sym -> NatRepr w -> RoundingMode -> SymInterpretedFloat sym fi -> IO (SymBV sym w)
- iFloatToReal :: sym -> SymInterpretedFloat sym fi -> IO (SymReal sym)
- iFloatBaseTypeRepr :: sym -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType sym fi)
class (IsSymExprBuilder sym, IsInterpretedFloatExprBuilder sym) => IsInterpretedFloatSymExprBuilder sym where
- freshFloatConstant :: sym -> SolverSymbol -> FloatInfoRepr fi -> IO (SymExpr sym (SymInterpretedFloatType sym fi))
- freshFloatLatch :: sym -> SolverSymbol -> FloatInfoRepr fi -> IO (SymExpr sym (SymInterpretedFloatType sym fi))
- freshFloatBoundVar :: sym -> SolverSymbol -> FloatInfoRepr fi -> IO (BoundVar sym (SymInterpretedFloatType sym fi))

FloatInfo data kind

data FloatInfo Source #

This data kind describes the types of floating-point formats. This consist of the standard IEEE 754-2008 binary floating point formats, as well as the X86 extended 80-bit format and the double-double format.

Instances

TestEquality FloatInfoRepr Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods testEquality :: FloatInfoRepr a -> FloatInfoRepr b -> Maybe (a :~: b) #
OrdF FloatInfoRepr Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods compareF :: FloatInfoRepr x -> FloatInfoRepr y -> OrderingF x y # leqF :: FloatInfoRepr x -> FloatInfoRepr y -> Bool # ltF :: FloatInfoRepr x -> FloatInfoRepr y -> Bool # geqF :: FloatInfoRepr x -> FloatInfoRepr y -> Bool # gtF :: FloatInfoRepr x -> FloatInfoRepr y -> Bool #
ShowF FloatInfoRepr Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods withShow :: p FloatInfoRepr -> q tp -> (Show (FloatInfoRepr tp) -> a) -> a # showF :: FloatInfoRepr tp -> String # showsPrecF :: Int -> FloatInfoRepr tp -> String -> String #
HashableF FloatInfoRepr Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods hashWithSaltF :: Int -> FloatInfoRepr tp -> Int # hashF :: FloatInfoRepr tp -> Int #
KnownRepr FloatInfoRepr DoubleDoubleFloat Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr DoubleDoubleFloat #
KnownRepr FloatInfoRepr X86_80Float Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr X86_80Float #
KnownRepr FloatInfoRepr QuadFloat Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr QuadFloat #
KnownRepr FloatInfoRepr DoubleFloat Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr DoubleFloat #
KnownRepr FloatInfoRepr SingleFloat Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr SingleFloat #
KnownRepr FloatInfoRepr HalfFloat Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr HalfFloat #

Constructors for kind FloatInfo

type HalfFloat Source #

Arguments

= HalfFloat

16 bit binary IEEE754.

type SingleFloat Source #

Arguments

= SingleFloat

32 bit binary IEEE754.

type DoubleFloat Source #

Arguments

= DoubleFloat

64 bit binary IEEE754.

type QuadFloat Source #

Arguments

= QuadFloat

128 bit binary IEEE754.

type X86_80Float Source #

Arguments

= X86_80Float

X86 80-bit extended floats.

type DoubleDoubleFloat Source #

Arguments

= DoubleDoubleFloat

Two 64-bit floats fused in the "double-double" style.

Representations of FloatInfo types

data FloatInfoRepr (fi :: FloatInfo) where Source #

A family of value-level representatives for floating-point types.

Constructors

HalfFloatRepr :: FloatInfoRepr HalfFloat
SingleFloatRepr :: FloatInfoRepr SingleFloat
DoubleFloatRepr :: FloatInfoRepr DoubleFloat
QuadFloatRepr :: FloatInfoRepr QuadFloat
X86_80FloatRepr :: FloatInfoRepr X86_80Float
DoubleDoubleFloatRepr :: FloatInfoRepr DoubleDoubleFloat

Instances

TestEquality FloatInfoRepr Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods testEquality :: FloatInfoRepr a -> FloatInfoRepr b -> Maybe (a :~: b) #
OrdF FloatInfoRepr Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods compareF :: FloatInfoRepr x -> FloatInfoRepr y -> OrderingF x y # leqF :: FloatInfoRepr x -> FloatInfoRepr y -> Bool # ltF :: FloatInfoRepr x -> FloatInfoRepr y -> Bool # geqF :: FloatInfoRepr x -> FloatInfoRepr y -> Bool # gtF :: FloatInfoRepr x -> FloatInfoRepr y -> Bool #
ShowF FloatInfoRepr Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods withShow :: p FloatInfoRepr -> q tp -> (Show (FloatInfoRepr tp) -> a) -> a # showF :: FloatInfoRepr tp -> String # showsPrecF :: Int -> FloatInfoRepr tp -> String -> String #
HashableF FloatInfoRepr Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods hashWithSaltF :: Int -> FloatInfoRepr tp -> Int # hashF :: FloatInfoRepr tp -> Int #
KnownRepr FloatInfoRepr DoubleDoubleFloat Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr DoubleDoubleFloat #
KnownRepr FloatInfoRepr X86_80Float Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr X86_80Float #
KnownRepr FloatInfoRepr QuadFloat Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr QuadFloat #
KnownRepr FloatInfoRepr DoubleFloat Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr DoubleFloat #
KnownRepr FloatInfoRepr SingleFloat Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr SingleFloat #
KnownRepr FloatInfoRepr HalfFloat Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr HalfFloat #
Show (FloatInfoRepr fi) Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods showsPrec :: Int -> FloatInfoRepr fi -> ShowS # show :: FloatInfoRepr fi -> String # showList :: [FloatInfoRepr fi] -> ShowS #
Pretty (FloatInfoRepr fi) Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods pretty :: FloatInfoRepr fi -> Doc # prettyList :: [FloatInfoRepr fi] -> Doc #
Hashable (FloatInfoRepr fi) Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods hashWithSalt :: Int -> FloatInfoRepr fi -> Int # hash :: FloatInfoRepr fi -> Int #

extended 80 bit float values ("long double")

data X86_80Val Source #

Representation of 80-bit floating values, since there's no native Haskell type for these.

Constructors

X86_80Val Word16 Word64

Instances

Eq X86_80Val Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods (==) :: X86_80Val -> X86_80Val -> Bool # (/=) :: X86_80Val -> X86_80Val -> Bool #
Ord X86_80Val Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods compare :: X86_80Val -> X86_80Val -> Ordering # (<) :: X86_80Val -> X86_80Val -> Bool # (<=) :: X86_80Val -> X86_80Val -> Bool # (>) :: X86_80Val -> X86_80Val -> Bool # (>=) :: X86_80Val -> X86_80Val -> Bool # max :: X86_80Val -> X86_80Val -> X86_80Val # min :: X86_80Val -> X86_80Val -> X86_80Val #
Show X86_80Val Source #
Instance details Defined in What4.InterpretedFloatingPoint Methods showsPrec :: Int -> X86_80Val -> ShowS # show :: X86_80Val -> String # showList :: [X86_80Val] -> ShowS #

fp80ToBits :: X86_80Val -> Integer Source #

fp80ToRational :: X86_80Val -> Maybe Rational Source #

FloatInfo to/from FloatPrecision

type family FloatInfoToPrecision (fi :: FloatInfo) :: FloatPrecision where ... Source #

Equations

FloatInfoToPrecision HalfFloat = Prec16
FloatInfoToPrecision SingleFloat = Prec32
FloatInfoToPrecision DoubleFloat = Prec64
FloatInfoToPrecision X86_80Float = Prec80
FloatInfoToPrecision QuadFloat = Prec128

type family FloatPrecisionToInfo (fpp :: FloatPrecision) :: FloatInfo where ... Source #

Equations

FloatPrecisionToInfo Prec16 = HalfFloat
FloatPrecisionToInfo Prec32 = SingleFloat
FloatPrecisionToInfo Prec64 = DoubleFloat
FloatPrecisionToInfo Prec80 = X86_80Float
FloatPrecisionToInfo Prec128 = QuadFloat

floatInfoToPrecisionRepr :: FloatInfoRepr fi -> FloatPrecisionRepr (FloatInfoToPrecision fi) Source #

floatPrecisionToInfoRepr :: FloatPrecisionRepr fpp -> FloatInfoRepr (FloatPrecisionToInfo fpp) Source #

Bit-width type family

type family FloatInfoToBitWidth (fi :: FloatInfo) :: Nat where ... Source #

Equations

FloatInfoToBitWidth HalfFloat = 16
FloatInfoToBitWidth SingleFloat = 32
FloatInfoToBitWidth DoubleFloat = 64
FloatInfoToBitWidth X86_80Float = 80
FloatInfoToBitWidth QuadFloat = 128
FloatInfoToBitWidth DoubleDoubleFloat = 128

floatInfoToBVTypeRepr :: FloatInfoRepr fi -> BaseTypeRepr (BaseBVType (FloatInfoToBitWidth fi)) Source #

Interface classes

Interpretation type family

type family SymInterpretedFloatType (sym :: Type) (fi :: FloatInfo) :: BaseType Source #

Interpretation of the floating point type.

Instances

type SymInterpretedFloatType (ExprBuilder t st (Flags FloatIEEE)) fi Source #
Instance details Defined in What4.Expr.Builder type SymInterpretedFloatType (ExprBuilder t st (Flags FloatIEEE)) fi = BaseFloatType (FloatInfoToPrecision fi)
type SymInterpretedFloatType (ExprBuilder t st (Flags FloatUninterpreted)) fi Source #
Instance details Defined in What4.Expr.Builder type SymInterpretedFloatType (ExprBuilder t st (Flags FloatUninterpreted)) fi = BaseBVType (FloatInfoToBitWidth fi)
type SymInterpretedFloatType (ExprBuilder t st (Flags FloatReal)) fi Source #
Instance details Defined in What4.Expr.Builder type SymInterpretedFloatType (ExprBuilder t st (Flags FloatReal)) fi = BaseRealType

Type alias

type SymInterpretedFloat sym fi = SymExpr sym (SymInterpretedFloatType sym fi) Source #

Symbolic floating point numbers.

IsInterpretedFloatExprBuilder

class IsExprBuilder sym => IsInterpretedFloatExprBuilder sym where Source #

Abstact floating point operations.

Methods

iFloatPZero :: sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi) Source #

Return floating point number +0.

iFloatNZero :: sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi) Source #

Return floating point number -0.

iFloatNaN :: sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi) Source #

Return floating point NaN.

iFloatPInf :: sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi) Source #

Return floating point +infinity.

iFloatNInf :: sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi) Source #

Return floating point -infinity.

iFloatLit :: sym -> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat sym fi) Source #

Create a floating point literal from a rational literal.

iFloatLitSingle :: sym -> Float -> IO (SymInterpretedFloat sym SingleFloat) Source #

Create a (single precision) floating point literal.

iFloatLitDouble :: sym -> Double -> IO (SymInterpretedFloat sym DoubleFloat) Source #

Create a (double precision) floating point literal.

iFloatLitLongDouble :: sym -> X86_80Val -> IO (SymInterpretedFloat sym X86_80Float) Source #

Create an (extended double precision) floating point literal.

iFloatNeg :: sym -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi) Source #

Negate a floating point number.

iFloatAbs :: sym -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi) Source #

Return the absolute value of a floating point number.

iFloatSqrt :: sym -> RoundingMode -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi) Source #

Compute the square root of a floating point number.

iFloatAdd :: sym -> RoundingMode -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi) Source #

Add two floating point numbers.

iFloatSub :: sym -> RoundingMode -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi) Source #

Subtract two floating point numbers.

iFloatMul :: sym -> RoundingMode -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi) Source #

Multiply two floating point numbers.

iFloatDiv :: sym -> RoundingMode -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi) Source #

Divide two floating point numbers.

iFloatRem :: sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi) Source #

Compute the reminder: x - y * n, where n in Z is nearest to x / y.

iFloatMin :: sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi) Source #

Return the min of two floating point numbers.

iFloatMax :: sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi) Source #

Return the max of two floating point numbers.

iFloatFMA :: sym -> RoundingMode -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi) Source #

Compute the fused multiplication and addition: (x * y) + z.

iFloatEq :: sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (Pred sym) Source #

Check logical equality of two floating point numbers.

iFloatNe :: sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (Pred sym) Source #

Check logical non-equality of two floating point numbers.

iFloatFpEq :: sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (Pred sym) Source #

Check IEEE equality of two floating point numbers.

iFloatFpNe :: sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (Pred sym) Source #

Check IEEE non-equality of two floating point numbers.

iFloatLe :: sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (Pred sym) Source #

Check <= on two floating point numbers.

iFloatLt :: sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (Pred sym) Source #

Check < on two floating point numbers.

iFloatGe :: sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (Pred sym) Source #

Check >= on two floating point numbers.

iFloatGt :: sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (Pred sym) Source #

Check > on two floating point numbers.

iFloatIsNaN :: sym -> SymInterpretedFloat sym fi -> IO (Pred sym) Source #

iFloatIsInf :: sym -> SymInterpretedFloat sym fi -> IO (Pred sym) Source #

iFloatIsZero :: sym -> SymInterpretedFloat sym fi -> IO (Pred sym) Source #

iFloatIsPos :: sym -> SymInterpretedFloat sym fi -> IO (Pred sym) Source #

iFloatIsNeg :: sym -> SymInterpretedFloat sym fi -> IO (Pred sym) Source #

iFloatIsSubnorm :: sym -> SymInterpretedFloat sym fi -> IO (Pred sym) Source #

iFloatIsNorm :: sym -> SymInterpretedFloat sym fi -> IO (Pred sym) Source #

iFloatIte :: sym -> Pred sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi) Source #

If-then-else on floating point numbers.

iFloatCast :: sym -> FloatInfoRepr fi -> RoundingMode -> SymInterpretedFloat sym fi' -> IO (SymInterpretedFloat sym fi) Source #

Change the precision of a floating point number.

iFloatRound :: sym -> RoundingMode -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi) Source #

Round a floating point number to an integral value.

iFloatFromBinary :: sym -> FloatInfoRepr fi -> SymBV sym (FloatInfoToBitWidth fi) -> IO (SymInterpretedFloat sym fi) Source #

Convert from binary representation in IEEE 754-2008 format to floating point.

iFloatToBinary :: sym -> FloatInfoRepr fi -> SymInterpretedFloat sym fi -> IO (SymBV sym (FloatInfoToBitWidth fi)) Source #

Convert from floating point from to the binary representation in IEEE 754-2008 format.

iBVToFloat :: 1 <= w => sym -> FloatInfoRepr fi -> RoundingMode -> SymBV sym w -> IO (SymInterpretedFloat sym fi) Source #

Convert a unsigned bitvector to a floating point number.

iSBVToFloat :: 1 <= w => sym -> FloatInfoRepr fi -> RoundingMode -> SymBV sym w -> IO (SymInterpretedFloat sym fi) Source #

Convert a signed bitvector to a floating point number.

iRealToFloat :: sym -> FloatInfoRepr fi -> RoundingMode -> SymReal sym -> IO (SymInterpretedFloat sym fi) Source #

Convert a real number to a floating point number.

iFloatToBV :: 1 <= w => sym -> NatRepr w -> RoundingMode -> SymInterpretedFloat sym fi -> IO (SymBV sym w) Source #

Convert a floating point number to a unsigned bitvector.

iFloatToSBV :: 1 <= w => sym -> NatRepr w -> RoundingMode -> SymInterpretedFloat sym fi -> IO (SymBV sym w) Source #

Convert a floating point number to a signed bitvector.

iFloatToReal :: sym -> SymInterpretedFloat sym fi -> IO (SymReal sym) Source #

Convert a floating point number to a real number.

iFloatBaseTypeRepr :: sym -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType sym fi) Source #

The associated BaseType representative of the floating point interpretation for each format.

Instances

IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatIEEE)) Source #
Instance details Defined in What4.Expr.Builder Methods iFloatPZero :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatNZero :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatNaN :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatPInf :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatNInf :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatLit :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatLitSingle :: ExprBuilder t st (Flags FloatIEEE) -> Float -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) SingleFloat) Source # iFloatLitDouble :: ExprBuilder t st (Flags FloatIEEE) -> Double -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) DoubleFloat) Source # iFloatLitLongDouble :: ExprBuilder t st (Flags FloatIEEE) -> X86_80Val -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) X86_80Float) Source # iFloatNeg :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatAbs :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatSqrt :: ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatAdd :: ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatSub :: ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatMul :: ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatDiv :: ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatRem :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatMin :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatMax :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatFMA :: ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatEq :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatNe :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatFpEq :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatFpNe :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatLe :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatLt :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatGe :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatGt :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatIsNaN :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatIsInf :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatIsZero :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatIsPos :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatIsNeg :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatIsSubnorm :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatIsNorm :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatIte :: ExprBuilder t st (Flags FloatIEEE) -> Pred (ExprBuilder t st (Flags FloatIEEE)) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatCast :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi' -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatRound :: ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatFromBinary :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> SymBV (ExprBuilder t st (Flags FloatIEEE)) (FloatInfoToBitWidth fi) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatToBinary :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatIEEE)) (FloatInfoToBitWidth fi)) Source # iBVToFloat :: 1 <= w => ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> RoundingMode -> SymBV (ExprBuilder t st (Flags FloatIEEE)) w -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iSBVToFloat :: 1 <= w => ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> RoundingMode -> SymBV (ExprBuilder t st (Flags FloatIEEE)) w -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iRealToFloat :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> RoundingMode -> SymReal (ExprBuilder t st (Flags FloatIEEE)) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatToBV :: 1 <= w => ExprBuilder t st (Flags FloatIEEE) -> NatRepr w -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatIEEE)) w) Source # iFloatToSBV :: 1 <= w => ExprBuilder t st (Flags FloatIEEE) -> NatRepr w -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatIEEE)) w) Source # iFloatToReal :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymReal (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatBaseTypeRepr :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType (ExprBuilder t st (Flags FloatIEEE)) fi) Source #
IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatUninterpreted)) Source #
Instance details Defined in What4.Expr.Builder Methods iFloatPZero :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatNZero :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatNaN :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatPInf :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatNInf :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatLit :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatLitSingle :: ExprBuilder t st (Flags FloatUninterpreted) -> Float -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) SingleFloat) Source # iFloatLitDouble :: ExprBuilder t st (Flags FloatUninterpreted) -> Double -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) DoubleFloat) Source # iFloatLitLongDouble :: ExprBuilder t st (Flags FloatUninterpreted) -> X86_80Val -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) X86_80Float) Source # iFloatNeg :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatAbs :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatSqrt :: ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatAdd :: ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatSub :: ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatMul :: ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatDiv :: ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatRem :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatMin :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatMax :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatFMA :: ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatEq :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatNe :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatFpEq :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatFpNe :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatLe :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatLt :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatGe :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatGt :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatIsNaN :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatIsInf :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatIsZero :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatIsPos :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatIsNeg :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatIsSubnorm :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatIsNorm :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatIte :: ExprBuilder t st (Flags FloatUninterpreted) -> Pred (ExprBuilder t st (Flags FloatUninterpreted)) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatCast :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi' -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatRound :: ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatFromBinary :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> SymBV (ExprBuilder t st (Flags FloatUninterpreted)) (FloatInfoToBitWidth fi) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatToBinary :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatUninterpreted)) (FloatInfoToBitWidth fi)) Source # iBVToFloat :: 1 <= w => ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> RoundingMode -> SymBV (ExprBuilder t st (Flags FloatUninterpreted)) w -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iSBVToFloat :: 1 <= w => ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> RoundingMode -> SymBV (ExprBuilder t st (Flags FloatUninterpreted)) w -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iRealToFloat :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> RoundingMode -> SymReal (ExprBuilder t st (Flags FloatUninterpreted)) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatToBV :: 1 <= w => ExprBuilder t st (Flags FloatUninterpreted) -> NatRepr w -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatUninterpreted)) w) Source # iFloatToSBV :: 1 <= w => ExprBuilder t st (Flags FloatUninterpreted) -> NatRepr w -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatUninterpreted)) w) Source # iFloatToReal :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymReal (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatBaseTypeRepr :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #
IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatReal)) Source #
Instance details Defined in What4.Expr.Builder Methods iFloatPZero :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatNZero :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatNaN :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatPInf :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatNInf :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatLit :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatLitSingle :: ExprBuilder t st (Flags FloatReal) -> Float -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) SingleFloat) Source # iFloatLitDouble :: ExprBuilder t st (Flags FloatReal) -> Double -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) DoubleFloat) Source # iFloatLitLongDouble :: ExprBuilder t st (Flags FloatReal) -> X86_80Val -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) X86_80Float) Source # iFloatNeg :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatAbs :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatSqrt :: ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatAdd :: ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatSub :: ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatMul :: ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatDiv :: ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatRem :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatMin :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatMax :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatFMA :: ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatEq :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatNe :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatFpEq :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatFpNe :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatLe :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatLt :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatGe :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatGt :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatIsNaN :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatIsInf :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatIsZero :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatIsPos :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatIsNeg :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatIsSubnorm :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatIsNorm :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatIte :: ExprBuilder t st (Flags FloatReal) -> Pred (ExprBuilder t st (Flags FloatReal)) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatCast :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi' -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatRound :: ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatFromBinary :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> SymBV (ExprBuilder t st (Flags FloatReal)) (FloatInfoToBitWidth fi) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatToBinary :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatReal)) (FloatInfoToBitWidth fi)) Source # iBVToFloat :: 1 <= w => ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> RoundingMode -> SymBV (ExprBuilder t st (Flags FloatReal)) w -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iSBVToFloat :: 1 <= w => ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> RoundingMode -> SymBV (ExprBuilder t st (Flags FloatReal)) w -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iRealToFloat :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> RoundingMode -> SymReal (ExprBuilder t st (Flags FloatReal)) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatToBV :: 1 <= w => ExprBuilder t st (Flags FloatReal) -> NatRepr w -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatReal)) w) Source # iFloatToSBV :: 1 <= w => ExprBuilder t st (Flags FloatReal) -> NatRepr w -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatReal)) w) Source # iFloatToReal :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymReal (ExprBuilder t st (Flags FloatReal))) Source # iFloatBaseTypeRepr :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType (ExprBuilder t st (Flags FloatReal)) fi) Source #