What4.InterpretedFloatingPoint

FloatInfo data kind

data FloatInfo

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

Defined in What4.InterpretedFloatingPoint

Methods

testEquality :: forall (a :: k) (b :: k). FloatInfoRepr a -> FloatInfoRepr b -> Maybe (a :~: b)

HashableF FloatInfoRepr

Defined in What4.InterpretedFloatingPoint

Methods

hashWithSaltF :: forall (tp :: k). Int -> FloatInfoRepr tp -> Int

hashF :: forall (tp :: k). FloatInfoRepr tp -> Int

OrdF FloatInfoRepr

Defined in What4.InterpretedFloatingPoint

Methods

compareF :: forall (x :: k) (y :: k). FloatInfoRepr x -> FloatInfoRepr y -> OrderingF x y

leqF :: forall (x :: k) (y :: k). FloatInfoRepr x -> FloatInfoRepr y -> Bool

ltF :: forall (x :: k) (y :: k). FloatInfoRepr x -> FloatInfoRepr y -> Bool

geqF :: forall (x :: k) (y :: k). FloatInfoRepr x -> FloatInfoRepr y -> Bool

gtF :: forall (x :: k) (y :: k). FloatInfoRepr x -> FloatInfoRepr y -> Bool

ShowF FloatInfoRepr

Defined in What4.InterpretedFloatingPoint

Methods

withShow :: forall p q (tp :: k) a. p FloatInfoRepr -> q tp -> (Show (FloatInfoRepr tp) => a) -> a

showF :: forall (tp :: k). FloatInfoRepr tp -> String

showsPrecF :: forall (tp :: k). Int -> FloatInfoRepr tp -> String -> String

KnownRepr FloatInfoRepr DoubleDoubleFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr DoubleDoubleFloat

KnownRepr FloatInfoRepr DoubleFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr DoubleFloat

KnownRepr FloatInfoRepr HalfFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr HalfFloat

KnownRepr FloatInfoRepr QuadFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr QuadFloat

KnownRepr FloatInfoRepr SingleFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr SingleFloat

KnownRepr FloatInfoRepr X86_80Float

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr X86_80Float

Constructors for kind FloatInfo

type HalfFloat

Arguments

 = 'HalfFloat

16 bit binary IEEE754.

type SingleFloat

Arguments

 = 'SingleFloat

32 bit binary IEEE754.

type DoubleFloat

Arguments

 = 'DoubleFloat

64 bit binary IEEE754.

type QuadFloat

Arguments

 = 'QuadFloat

128 bit binary IEEE754.

type X86_80Float

Arguments

 = 'X86_80Float

X86 80-bit extended floats.

type DoubleDoubleFloat

Arguments

 = 'DoubleDoubleFloat

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

Representations of FloatInfo types

data FloatInfoRepr (fi :: FloatInfo) where

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

Defined in What4.InterpretedFloatingPoint

Methods

testEquality :: forall (a :: k) (b :: k). FloatInfoRepr a -> FloatInfoRepr b -> Maybe (a :~: b)

HashableF FloatInfoRepr

Defined in What4.InterpretedFloatingPoint

Methods

hashWithSaltF :: forall (tp :: k). Int -> FloatInfoRepr tp -> Int

hashF :: forall (tp :: k). FloatInfoRepr tp -> Int

OrdF FloatInfoRepr

Defined in What4.InterpretedFloatingPoint

Methods

compareF :: forall (x :: k) (y :: k). FloatInfoRepr x -> FloatInfoRepr y -> OrderingF x y

leqF :: forall (x :: k) (y :: k). FloatInfoRepr x -> FloatInfoRepr y -> Bool

ltF :: forall (x :: k) (y :: k). FloatInfoRepr x -> FloatInfoRepr y -> Bool

geqF :: forall (x :: k) (y :: k). FloatInfoRepr x -> FloatInfoRepr y -> Bool

gtF :: forall (x :: k) (y :: k). FloatInfoRepr x -> FloatInfoRepr y -> Bool

ShowF FloatInfoRepr

Defined in What4.InterpretedFloatingPoint

Methods

withShow :: forall p q (tp :: k) a. p FloatInfoRepr -> q tp -> (Show (FloatInfoRepr tp) => a) -> a

showF :: forall (tp :: k). FloatInfoRepr tp -> String

showsPrecF :: forall (tp :: k). Int -> FloatInfoRepr tp -> String -> String

KnownRepr FloatInfoRepr DoubleDoubleFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr DoubleDoubleFloat

KnownRepr FloatInfoRepr DoubleFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr DoubleFloat

KnownRepr FloatInfoRepr HalfFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr HalfFloat

KnownRepr FloatInfoRepr QuadFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr QuadFloat

KnownRepr FloatInfoRepr SingleFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr SingleFloat

KnownRepr FloatInfoRepr X86_80Float

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr X86_80Float

Show (FloatInfoRepr fi)

Defined in What4.InterpretedFloatingPoint

Methods

showsPrec :: Int -> FloatInfoRepr fi -> ShowS

show :: FloatInfoRepr fi -> String

showList :: [FloatInfoRepr fi] -> ShowS

Eq (FloatInfoRepr fi)

Defined in What4.InterpretedFloatingPoint

Methods

(==) :: FloatInfoRepr fi -> FloatInfoRepr fi -> Bool

(/=) :: FloatInfoRepr fi -> FloatInfoRepr fi -> Bool

Hashable (FloatInfoRepr fi)

Defined in What4.InterpretedFloatingPoint

Methods

hashWithSalt :: Int -> FloatInfoRepr fi -> Int

hash :: FloatInfoRepr fi -> Int

Pretty (FloatInfoRepr fi)

Defined in What4.InterpretedFloatingPoint

Methods

pretty :: FloatInfoRepr fi -> Doc ann

prettyList :: [FloatInfoRepr fi] -> Doc ann

extended 80 bit float values ("long double")

data X86_80Val

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

Constructors

X86_80Val Word16 Word64

Instances

Show X86_80Val

Defined in What4.InterpretedFloatingPoint

Methods

showsPrec :: Int -> X86_80Val -> ShowS

show :: X86_80Val -> String

showList :: [X86_80Val] -> ShowS

Eq X86_80Val

Defined in What4.InterpretedFloatingPoint

Methods

(==) :: X86_80Val -> X86_80Val -> Bool

(/=) :: X86_80Val -> X86_80Val -> Bool

Ord X86_80Val

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

fp80ToBits :: X86_80Val -> Integer

fp80ToRational :: X86_80Val -> Maybe Rational

FloatInfo to/from FloatPrecision

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

Equations

FloatInfoToPrecision HalfFloat = Prec16

FloatInfoToPrecision SingleFloat = Prec32

FloatInfoToPrecision DoubleFloat = Prec64

FloatInfoToPrecision X86_80Float = Prec80

FloatInfoToPrecision QuadFloat = Prec128

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

Equations

FloatPrecisionToInfo Prec16 = HalfFloat

FloatPrecisionToInfo Prec32 = SingleFloat

FloatPrecisionToInfo Prec64 = DoubleFloat

FloatPrecisionToInfo Prec80 = X86_80Float

FloatPrecisionToInfo Prec128 = QuadFloat

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

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

Bit-width type family

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

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))

Interface classes

Interpretation type family

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

Interpretation of the floating point type.

Instances

type SymInterpretedFloatType (ExprBuilder t st (Flags FloatIEEE)) fi

Defined in What4.Expr.Builder

type SymInterpretedFloatType (ExprBuilder t st (Flags FloatIEEE)) fi = BaseFloatType (FloatInfoToPrecision fi)

type SymInterpretedFloatType (ExprBuilder t st (Flags FloatReal)) fi

Defined in What4.Expr.Builder

type SymInterpretedFloatType (ExprBuilder t st (Flags FloatReal)) fi = BaseRealType

type SymInterpretedFloatType (ExprBuilder t st (Flags FloatUninterpreted)) fi

Defined in What4.Expr.Builder

type SymInterpretedFloatType (ExprBuilder t st (Flags FloatUninterpreted)) fi = BaseBVType (FloatInfoToBitWidth fi)

Type alias

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

Symbolic floating point numbers.

IsInterpretedFloatExprBuilder

class IsExprBuilder sym => IsInterpretedFloatExprBuilder sym where

Abstact floating point operations.

Minimal complete definition

iFloatPZero, iFloatNZero, iFloatNaN, iFloatPInf, iFloatNInf, iFloatLitRational, iFloatLitSingle, iFloatLitDouble, iFloatLitLongDouble, iFloatNeg, iFloatAbs, iFloatSqrt, iFloatAdd, iFloatSub, iFloatMul, iFloatDiv, iFloatRem, iFloatMin, iFloatMax, iFloatFMA, iFloatEq, iFloatNe, iFloatFpEq, iFloatFpApart, iFloatLe, iFloatLt, iFloatGe, iFloatGt, iFloatIsNaN, iFloatIsInf, iFloatIsZero, iFloatIsPos, iFloatIsNeg, iFloatIsSubnorm, iFloatIsNorm, iFloatIte, iFloatCast, iFloatRound, iFloatFromBinary, iFloatToBinary, iBVToFloat, iSBVToFloat, iRealToFloat, iFloatToBV, iFloatToSBV, iFloatToReal, iFloatSpecialFunction, iFloatBaseTypeRepr

Methods

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

Return floating point number +0.

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

Return floating point number -0.

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

Return floating point NaN.

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

Return floating point +infinity.

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

Return floating point -infinity.

iFloatLitRational :: sym -> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat sym fi)

Create a floating point literal from a rational literal.

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

Create a (single precision) floating point literal.

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

Create a (double precision) floating point literal.

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

Create an (extended double precision) floating point literal.

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

Negate a floating point number.

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

Return the absolute value of a floating point number.

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

Compute the square root of a floating point number.

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

Add two floating point numbers.

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

Subtract two floating point numbers.

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

Multiply two floating point numbers.

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

Divide two floating point numbers.

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

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)

Return the min of two floating point numbers.

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

Return the max of two floating point numbers.

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

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

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

Check logical equality of two floating point numbers.

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

Check logical non-equality of two floating point numbers.

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

Check IEEE equality of two floating point numbers.

iFloatFpApart :: sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (Pred sym)

Check IEEE apartness of two floating point numbers.

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

Check <= on two floating point numbers.

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

Check < on two floating point numbers.

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

Check >= on two floating point numbers.

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

Check > on two floating point numbers.

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)

If-then-else on floating point numbers.

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

Change the precision of a floating point number.

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

Round a floating point number to an integral value.

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

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

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

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)

Convert a unsigned bitvector to a floating point number.

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

Convert a signed bitvector to a floating point number.

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

Convert a real number to a floating point number.

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

Convert a floating point number to a unsigned bitvector.

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

Convert a floating point number to a signed bitvector.

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

Convert a floating point number to a real number.

iFloatSpecialFunction :: sym -> FloatInfoRepr fi -> SpecialFunction args -> Assignment (SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi)) args -> IO (SymInterpretedFloat sym fi)

Apply a special function to floating-point arguments

iFloatSpecialFunction0 :: sym -> FloatInfoRepr fi -> SpecialFunction EmptyCtx -> IO (SymInterpretedFloat sym fi)

Access a 0-arity special function constant

iFloatSpecialFunction1 :: sym -> FloatInfoRepr fi -> SpecialFunction (EmptyCtx ::> R) -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi)

Apply a 1-argument special function

iFloatSpecialFunction2 :: sym -> FloatInfoRepr fi -> SpecialFunction ((EmptyCtx ::> R) ::> R) -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi)

Apply a 2-argument special function

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

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

Instances

IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatIEEE))

Defined in What4.Expr.Builder

Methods

iFloatPZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi)

iFloatNZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi)

iFloatNaN :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi)

iFloatPInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi)

iFloatNInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi)

iFloatLitRational :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi)

iFloatLitSingle :: ExprBuilder t st (Flags FloatIEEE) -> Float -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) SingleFloat)

iFloatLitDouble :: ExprBuilder t st (Flags FloatIEEE) -> Double -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) DoubleFloat)

iFloatLitLongDouble :: ExprBuilder t st (Flags FloatIEEE) -> X86_80Val -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) X86_80Float)

iFloatNeg :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi)

iFloatAbs :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi)

iFloatSqrt :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi)

iFloatAdd :: forall (fi :: FloatInfo). 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)

iFloatSub :: forall (fi :: FloatInfo). 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)

iFloatMul :: forall (fi :: FloatInfo). 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)

iFloatDiv :: forall (fi :: FloatInfo). 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)

iFloatRem :: forall (fi :: FloatInfo). 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)

iFloatMin :: forall (fi :: FloatInfo). 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)

iFloatMax :: forall (fi :: FloatInfo). 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)

iFloatFMA :: forall (fi :: FloatInfo). 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)

iFloatEq :: forall (fi :: FloatInfo). 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)))

iFloatNe :: forall (fi :: FloatInfo). 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)))

iFloatFpEq :: forall (fi :: FloatInfo). 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)))

iFloatFpApart :: forall (fi :: FloatInfo). 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)))

iFloatLe :: forall (fi :: FloatInfo). 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)))

iFloatLt :: forall (fi :: FloatInfo). 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)))

iFloatGe :: forall (fi :: FloatInfo). 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)))

iFloatGt :: forall (fi :: FloatInfo). 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)))

iFloatIsNaN :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE)))

iFloatIsInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE)))

iFloatIsZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE)))

iFloatIsPos :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE)))

iFloatIsNeg :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE)))

iFloatIsSubnorm :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE)))

iFloatIsNorm :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE)))

iFloatIte :: forall (fi :: FloatInfo). 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)

iFloatCast :: forall (fi :: FloatInfo) (fi' :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi' -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi)

iFloatRound :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi)

iFloatFromBinary :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> SymBV (ExprBuilder t st (Flags FloatIEEE)) (FloatInfoToBitWidth fi) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi)

iFloatToBinary :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatIEEE)) (FloatInfoToBitWidth fi))

iBVToFloat :: forall (w :: Natural) (fi :: FloatInfo). 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)

iSBVToFloat :: forall (w :: Natural) (fi :: FloatInfo). 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)

iRealToFloat :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> RoundingMode -> SymReal (ExprBuilder t st (Flags FloatIEEE)) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi)

iFloatToBV :: forall (w :: Natural) (fi :: FloatInfo). 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)

iFloatToSBV :: forall (w :: Natural) (fi :: FloatInfo). 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)

iFloatToReal :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymReal (ExprBuilder t st (Flags FloatIEEE)))

iFloatSpecialFunction :: forall (fi :: FloatInfo) (args :: Ctx Type). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> SpecialFunction args -> Assignment (SpecialFnArg (SymExpr (ExprBuilder t st (Flags FloatIEEE))) (SymInterpretedFloatType (ExprBuilder t st (Flags FloatIEEE)) fi)) args -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi)

iFloatSpecialFunction0 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> SpecialFunction EmptyCtx -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi)

iFloatSpecialFunction1 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> SpecialFunction (EmptyCtx ::> R) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi)

iFloatSpecialFunction2 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> SpecialFunction ((EmptyCtx ::> R) ::> R) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi)

iFloatBaseTypeRepr :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType (ExprBuilder t st (Flags FloatIEEE)) fi)

IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatReal))

Defined in What4.Expr.Builder

Methods

iFloatPZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi)

iFloatNZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi)

iFloatNaN :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi)

iFloatPInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi)

iFloatNInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi)

iFloatLitRational :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi)

iFloatLitSingle :: ExprBuilder t st (Flags FloatReal) -> Float -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) SingleFloat)

iFloatLitDouble :: ExprBuilder t st (Flags FloatReal) -> Double -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) DoubleFloat)

iFloatLitLongDouble :: ExprBuilder t st (Flags FloatReal) -> X86_80Val -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) X86_80Float)

iFloatNeg :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi)

iFloatAbs :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi)

iFloatSqrt :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi)

iFloatAdd :: forall (fi :: FloatInfo). 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)

iFloatSub :: forall (fi :: FloatInfo). 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)

iFloatMul :: forall (fi :: FloatInfo). 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)

iFloatDiv :: forall (fi :: FloatInfo). 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)

iFloatRem :: forall (fi :: FloatInfo). 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)

iFloatMin :: forall (fi :: FloatInfo). 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)

iFloatMax :: forall (fi :: FloatInfo). 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)

iFloatFMA :: forall (fi :: FloatInfo). 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)

iFloatEq :: forall (fi :: FloatInfo). 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)))

iFloatNe :: forall (fi :: FloatInfo). 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)))

iFloatFpEq :: forall (fi :: FloatInfo). 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)))

iFloatFpApart :: forall (fi :: FloatInfo). 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)))

iFloatLe :: forall (fi :: FloatInfo). 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)))

iFloatLt :: forall (fi :: FloatInfo). 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)))

iFloatGe :: forall (fi :: FloatInfo). 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)))

iFloatGt :: forall (fi :: FloatInfo). 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)))

iFloatIsNaN :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal)))

iFloatIsInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal)))

iFloatIsZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal)))

iFloatIsPos :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal)))

iFloatIsNeg :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal)))

iFloatIsSubnorm :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal)))

iFloatIsNorm :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal)))

iFloatIte :: forall (fi :: FloatInfo). 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)

iFloatCast :: forall (fi :: FloatInfo) (fi' :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi' -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi)

iFloatRound :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi)

iFloatFromBinary :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> SymBV (ExprBuilder t st (Flags FloatReal)) (FloatInfoToBitWidth fi) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi)

iFloatToBinary :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatReal)) (FloatInfoToBitWidth fi))

iBVToFloat :: forall (w :: Natural) (fi :: FloatInfo). 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)

iSBVToFloat :: forall (w :: Natural) (fi :: FloatInfo). 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)

iRealToFloat :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> RoundingMode -> SymReal (ExprBuilder t st (Flags FloatReal)) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi)

iFloatToBV :: forall (w :: Natural) (fi :: FloatInfo). 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)

iFloatToSBV :: forall (w :: Natural) (fi :: FloatInfo). 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)

iFloatToReal :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymReal (ExprBuilder t st (Flags FloatReal)))

iFloatSpecialFunction :: forall (fi :: FloatInfo) (args :: Ctx Type). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> SpecialFunction args -> Assignment (SpecialFnArg (SymExpr (ExprBuilder t st (Flags FloatReal))) (SymInterpretedFloatType (ExprBuilder t st (Flags FloatReal)) fi)) args -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi)

iFloatSpecialFunction0 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> SpecialFunction EmptyCtx -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi)

iFloatSpecialFunction1 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> SpecialFunction (EmptyCtx ::> R) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi)

iFloatSpecialFunction2 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> SpecialFunction ((EmptyCtx ::> R) ::> R) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi)

iFloatBaseTypeRepr :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType (ExprBuilder t st (Flags FloatReal)) fi)

IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatUninterpreted))

Defined in What4.Expr.Builder

Methods

iFloatPZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi)

iFloatNZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi)

iFloatNaN :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi)

iFloatPInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi)

iFloatNInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi)

iFloatLitRational :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi)

iFloatLitSingle :: ExprBuilder t st (Flags FloatUninterpreted) -> Float -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) SingleFloat)

iFloatLitDouble :: ExprBuilder t st (Flags FloatUninterpreted) -> Double -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) DoubleFloat)

iFloatLitLongDouble :: ExprBuilder t st (Flags FloatUninterpreted) -> X86_80Val -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) X86_80Float)

iFloatNeg :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi)

iFloatAbs :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi)

iFloatSqrt :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi)

iFloatAdd :: forall (fi :: FloatInfo). 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)

iFloatSub :: forall (fi :: FloatInfo). 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)

iFloatMul :: forall (fi :: FloatInfo). 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)

iFloatDiv :: forall (fi :: FloatInfo). 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)

iFloatRem :: forall (fi :: FloatInfo). 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)

iFloatMin :: forall (fi :: FloatInfo). 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)

iFloatMax :: forall (fi :: FloatInfo). 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)

iFloatFMA :: forall (fi :: FloatInfo). 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)

iFloatEq :: forall (fi :: FloatInfo). 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)))

iFloatNe :: forall (fi :: FloatInfo). 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)))

iFloatFpEq :: forall (fi :: FloatInfo). 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)))

iFloatFpApart :: forall (fi :: FloatInfo). 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)))

iFloatLe :: forall (fi :: FloatInfo). 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)))

iFloatLt :: forall (fi :: FloatInfo). 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)))

iFloatGe :: forall (fi :: FloatInfo). 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)))

iFloatGt :: forall (fi :: FloatInfo). 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)))

iFloatIsNaN :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted)))

iFloatIsInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted)))

iFloatIsZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted)))

iFloatIsPos :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted)))

iFloatIsNeg :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted)))

iFloatIsSubnorm :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted)))

iFloatIsNorm :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted)))

iFloatIte :: forall (fi :: FloatInfo). 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)

iFloatCast :: forall (fi :: FloatInfo) (fi' :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi' -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi)

iFloatRound :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi)

iFloatFromBinary :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> SymBV (ExprBuilder t st (Flags FloatUninterpreted)) (FloatInfoToBitWidth fi) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi)

iFloatToBinary :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatUninterpreted)) (FloatInfoToBitWidth fi))

iBVToFloat :: forall (w :: Natural) (fi :: FloatInfo). 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)

iSBVToFloat :: forall (w :: Natural) (fi :: FloatInfo). 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)

iRealToFloat :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> RoundingMode -> SymReal (ExprBuilder t st (Flags FloatUninterpreted)) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi)

iFloatToBV :: forall (w :: Natural) (fi :: FloatInfo). 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)

iFloatToSBV :: forall (w :: Natural) (fi :: FloatInfo). 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)

iFloatToReal :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymReal (ExprBuilder t st (Flags FloatUninterpreted)))

iFloatSpecialFunction :: forall (fi :: FloatInfo) (args :: Ctx Type). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> SpecialFunction args -> Assignment (SpecialFnArg (SymExpr (ExprBuilder t st (Flags FloatUninterpreted))) (SymInterpretedFloatType (ExprBuilder t st (Flags FloatUninterpreted)) fi)) args -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi)

iFloatSpecialFunction0 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> SpecialFunction EmptyCtx -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi)

iFloatSpecialFunction1 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> SpecialFunction (EmptyCtx ::> R) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi)

iFloatSpecialFunction2 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> SpecialFunction ((EmptyCtx ::> R) ::> R) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi)

iFloatBaseTypeRepr :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType (ExprBuilder t st (Flags FloatUninterpreted)) fi)

class (IsSymExprBuilder sym, IsInterpretedFloatExprBuilder sym) => IsInterpretedFloatSymExprBuilder sym where

Helper interface for creating new symbolic floating-point constants and variables.

Minimal complete definition

Nothing

Methods

freshFloatConstant :: sym -> SolverSymbol -> FloatInfoRepr fi -> IO (SymExpr sym (SymInterpretedFloatType sym fi))

Create a fresh top-level floating-point uninterpreted constant.

freshFloatLatch :: sym -> SolverSymbol -> FloatInfoRepr fi -> IO (SymExpr sym (SymInterpretedFloatType sym fi))

Create a fresh floating-point latch variable.

freshFloatBoundVar :: sym -> SolverSymbol -> FloatInfoRepr fi -> IO (BoundVar sym (SymInterpretedFloatType sym fi))

Creates a floating-point bound variable.

Instances

IsInterpretedFloatExprBuilder (ExprBuilder t st fs) => IsInterpretedFloatSymExprBuilder (ExprBuilder t st fs)

Defined in What4.Expr.Builder

Methods

freshFloatConstant :: forall (fi :: FloatInfo). ExprBuilder t st fs -> SolverSymbol -> FloatInfoRepr fi -> IO (SymExpr (ExprBuilder t st fs) (SymInterpretedFloatType (ExprBuilder t st fs) fi))

freshFloatLatch :: forall (fi :: FloatInfo). ExprBuilder t st fs -> SolverSymbol -> FloatInfoRepr fi -> IO (SymExpr (ExprBuilder t st fs) (SymInterpretedFloatType (ExprBuilder t st fs) fi))

freshFloatBoundVar :: forall (fi :: FloatInfo). ExprBuilder t st fs -> SolverSymbol -> FloatInfoRepr fi -> IO (BoundVar (ExprBuilder t st fs) (SymInterpretedFloatType (ExprBuilder t st fs) fi))