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)

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

HashableF FloatInfoRepr

Defined in What4.InterpretedFloatingPoint

Methods

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

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

KnownRepr FloatInfoRepr DoubleDoubleFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr DoubleDoubleFloat

KnownRepr FloatInfoRepr X86_80Float

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr X86_80Float

KnownRepr FloatInfoRepr QuadFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr QuadFloat

KnownRepr FloatInfoRepr DoubleFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr DoubleFloat

KnownRepr FloatInfoRepr SingleFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr SingleFloat

KnownRepr FloatInfoRepr HalfFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr HalfFloat

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)

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

HashableF FloatInfoRepr

Defined in What4.InterpretedFloatingPoint

Methods

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

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

KnownRepr FloatInfoRepr DoubleDoubleFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr DoubleDoubleFloat

KnownRepr FloatInfoRepr X86_80Float

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr X86_80Float

KnownRepr FloatInfoRepr QuadFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr QuadFloat

KnownRepr FloatInfoRepr DoubleFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr DoubleFloat

KnownRepr FloatInfoRepr SingleFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr SingleFloat

KnownRepr FloatInfoRepr HalfFloat

Defined in What4.InterpretedFloatingPoint

Methods

knownRepr :: FloatInfoRepr HalfFloat

Show (FloatInfoRepr fi)

Defined in What4.InterpretedFloatingPoint

Methods

showsPrec :: Int -> FloatInfoRepr fi -> ShowS

show :: FloatInfoRepr fi -> String

showList :: [FloatInfoRepr fi] -> ShowS

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

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

Show X86_80Val

Defined in What4.InterpretedFloatingPoint

Methods

showsPrec :: Int -> X86_80Val -> ShowS

show :: X86_80Val -> String

showList :: [X86_80Val] -> ShowS

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

Defined in What4.Expr.Builder

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

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

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)

Symbolic floating point numbers.

IsInterpretedFloatExprBuilder

class IsExprBuilder sym => IsInterpretedFloatExprBuilder sym where

Abstact floating point operations.

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.

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 :: Nat) (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 :: Nat) (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 :: Nat) (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 :: Nat) (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)))

iFloatBaseTypeRepr :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType (ExprBuilder t st (Flags FloatIEEE)) 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 :: Nat) (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 :: Nat) (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 :: Nat) (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 :: Nat) (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)))

iFloatBaseTypeRepr :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType (ExprBuilder t st (Flags FloatUninterpreted)) 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 :: Nat) (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 :: Nat) (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 :: Nat) (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 :: Nat) (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)))

iFloatBaseTypeRepr :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType (ExprBuilder t st (Flags FloatReal)) 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))