what4-1.1: Solver-agnostic symbolic values support for issuing queries
Safe HaskellNone
LanguageHaskell2010

What4.InterpretedFloatingPoint

Synopsis

FloatInfo data kind

data FloatInfo Source #

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

Instances

Instances details
TestEquality FloatInfoRepr Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

Methods

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

OrdF FloatInfoRepr Source # 
Instance details

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 Source # 
Instance details

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 Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

Methods

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

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

KnownRepr FloatInfoRepr DoubleDoubleFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

KnownRepr FloatInfoRepr X86_80Float Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

KnownRepr FloatInfoRepr QuadFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

KnownRepr FloatInfoRepr DoubleFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

KnownRepr FloatInfoRepr SingleFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

KnownRepr FloatInfoRepr HalfFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

Constructors for kind FloatInfo

type HalfFloat Source #

Arguments

 = 'HalfFloat

16 bit binary IEEE754.

type SingleFloat Source #

Arguments

 = 'SingleFloat

32 bit binary IEEE754.

type DoubleFloat Source #

Arguments

 = 'DoubleFloat

64 bit binary IEEE754.

type QuadFloat Source #

Arguments

 = 'QuadFloat

128 bit binary IEEE754.

type X86_80Float Source #

Arguments

 = 'X86_80Float

X86 80-bit extended floats.

type DoubleDoubleFloat Source #

Arguments

 = 'DoubleDoubleFloat

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

Representations of FloatInfo types

data FloatInfoRepr (fi :: FloatInfo) where Source #

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

Instances

Instances details
TestEquality FloatInfoRepr Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

Methods

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

OrdF FloatInfoRepr Source # 
Instance details

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 Source # 
Instance details

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 Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

Methods

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

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

KnownRepr FloatInfoRepr DoubleDoubleFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

KnownRepr FloatInfoRepr X86_80Float Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

KnownRepr FloatInfoRepr QuadFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

KnownRepr FloatInfoRepr DoubleFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

KnownRepr FloatInfoRepr SingleFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

KnownRepr FloatInfoRepr HalfFloat Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

Show (FloatInfoRepr fi) Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

Hashable (FloatInfoRepr fi) Source # 
Instance details

Defined in What4.InterpretedFloatingPoint

Pretty (FloatInfoRepr fi) Source # 
Instance details

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 Source #

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

Constructors

X86_80Val Word16 Word64 

FloatInfo to/from FloatPrecision

Bit-width type family

Interface classes

Interpretation type family

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

Interpretation of the floating point type.

Type alias

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

Symbolic floating point numbers.

IsInterpretedFloatExprBuilder

class IsExprBuilder sym => IsInterpretedFloatExprBuilder sym where Source #

Abstact floating point operations.

Methods

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

Return floating point number +0.

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

Return floating point number -0.

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

Return floating point NaN.

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

Return floating point +infinity.

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

Return floating point -infinity.

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

Create a floating point literal from a rational literal.

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

Create a (single precision) floating point literal.

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

Create a (double precision) floating point literal.

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

Create an (extended double precision) floating point literal.

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

Negate a floating point number.

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

Return the absolute value of a floating point number.

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

Compute the square root of a floating point number.

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

Add two floating point numbers.

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

Subtract two floating point numbers.

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

Multiply two floating point numbers.

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

Divide two floating point numbers.

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

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

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

Return the min of two floating point numbers.

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

Return the max of two floating point numbers.

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

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

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

Check logical equality of two floating point numbers.

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

Check logical non-equality of two floating point numbers.

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

Check IEEE equality of two floating point numbers.

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

Check IEEE apartness of two floating point numbers.

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

Check <= on two floating point numbers.

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

Check < on two floating point numbers.

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

Check >= on two floating point numbers.

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

Check > on two floating point numbers.

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

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

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

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

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

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

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

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

If-then-else on floating point numbers.

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

Change the precision of a floating point number.

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

Round a floating point number to an integral value.

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

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

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

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

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

Convert a unsigned bitvector to a floating point number.

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

Convert a signed bitvector to a floating point number.

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

Convert a real number to a floating point number.

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

Convert a floating point number to a unsigned bitvector.

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

Convert a floating point number to a signed bitvector.

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

Convert a floating point number to a real number.

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

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

Instances

Instances details
IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatIEEE)) Source # 
Instance details

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatUninterpreted)) Source # 
Instance details

Defined in What4.Expr.Builder

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatReal)) Source # 
Instance details

Defined in What4.Expr.Builder

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Create a fresh floating-point latch variable.

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

Creates a floating-point bound variable.

Instances

Instances details
IsInterpretedFloatExprBuilder (ExprBuilder t st fs) => IsInterpretedFloatSymExprBuilder (ExprBuilder t st fs) Source # 
Instance details

Defined in What4.Expr.Builder