what4-1.6.3: Solver-agnostic symbolic values support for issuing queries

Safe Haskell | None
Language | Haskell2010

What4.InterpretedFloatingPoint

Contents

- FloatInfo data kind
  - Constructors for kind FloatInfo
  - Representations of FloatInfo types
  - extended 80 bit float values ("long double")
  - FloatInfo to/from FloatPrecision
  - Bit-width type family
- Interface classes
  - Interpretation type family
  - Type alias
  - IsInterpretedFloatExprBuilder

Synopsis

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

# FloatInfo data kind

data FloatInfo Source #

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

#### Instances

Instances details

TestEquality FloatInfoRepr Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods testEquality :: forall (a :: FloatInfo) (b :: FloatInfo). FloatInfoRepr a -> FloatInfoRepr b -> Maybe (a :~: b) Source #
HashableF FloatInfoRepr Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods hashWithSaltF :: forall (tp :: FloatInfo). Int -> FloatInfoRepr tp -> Int Source # hashF :: forall (tp :: FloatInfo). FloatInfoRepr tp -> Int Source #
OrdF FloatInfoRepr Source # |

Instance details

Defined in What4.InterpretedFloatingPoint

Methods

compareF :: forall (x :: FloatInfo) (y :: FloatInfo). FloatInfoRepr x -> FloatInfoRepr y -> OrderingF x y Source #

leqF :: forall (x :: FloatInfo) (y :: FloatInfo). FloatInfoRepr x -> FloatInfoRepr y -> Bool Source #

ltF :: forall (x :: FloatInfo) (y :: FloatInfo). FloatInfoRepr x -> FloatInfoRepr y -> Bool Source #

geqF :: forall (x :: FloatInfo) (y :: FloatInfo). FloatInfoRepr x -> FloatInfoRepr y -> Bool Source #

gtF :: forall (x :: FloatInfo) (y :: FloatInfo). FloatInfoRepr x -> FloatInfoRepr y -> Bool Source #

ShowF FloatInfoRepr Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods withShow :: forall p q (tp :: FloatInfo) a. p FloatInfoRepr -> q tp -> (Show (FloatInfoRepr tp) => a) -> a Source # showF :: forall (tp :: FloatInfo). FloatInfoRepr tp -> String Source # showsPrecF :: forall (tp :: FloatInfo). Int -> FloatInfoRepr tp -> String -> String Source #
KnownRepr FloatInfoRepr DoubleDoubleFloat Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr DoubleDoubleFloat Source #
KnownRepr FloatInfoRepr DoubleFloat Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr DoubleFloat Source #
KnownRepr FloatInfoRepr HalfFloat Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr HalfFloat Source #
KnownRepr FloatInfoRepr QuadFloat Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr QuadFloat Source #
KnownRepr FloatInfoRepr SingleFloat Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr SingleFloat Source #
KnownRepr FloatInfoRepr X86_80Float Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr X86_80Float Source #

## Constructors for kind FloatInfo

type HalfFloat Source #

Arguments

= 'HalfFloat | 16 bit binary IEEE754.

type SingleFloat Source #

Arguments

= 'SingleFloat | 32 bit binary IEEE754.

type DoubleFloat Source #

Arguments

= 'DoubleFloat | 64 bit binary IEEE754.

type QuadFloat Source #

Arguments

= 'QuadFloat | 128 bit binary IEEE754.

type X86_80Float Source #

Arguments

= 'X86_80Float | X86 80-bit extended floats.

type DoubleDoubleFloat Source #

Arguments

= 'DoubleDoubleFloat | Two 64-bit floats fused in the "double-double" style.

## Representations of FloatInfo types

data FloatInfoRepr (fi :: FloatInfo) where Source #

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

Constructors

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

#### Instances

Instances details

TestEquality FloatInfoRepr Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods testEquality :: forall (a :: FloatInfo) (b :: FloatInfo). FloatInfoRepr a -> FloatInfoRepr b -> Maybe (a :~: b) Source #
HashableF FloatInfoRepr Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods hashWithSaltF :: forall (tp :: FloatInfo). Int -> FloatInfoRepr tp -> Int Source # hashF :: forall (tp :: FloatInfo). FloatInfoRepr tp -> Int Source #
OrdF FloatInfoRepr Source # |

Instance details

Defined in What4.InterpretedFloatingPoint

Methods

compareF :: forall (x :: FloatInfo) (y :: FloatInfo). FloatInfoRepr x -> FloatInfoRepr y -> OrderingF x y Source #

leqF :: forall (x :: FloatInfo) (y :: FloatInfo). FloatInfoRepr x -> FloatInfoRepr y -> Bool Source #

ltF :: forall (x :: FloatInfo) (y :: FloatInfo). FloatInfoRepr x -> FloatInfoRepr y -> Bool Source #

geqF :: forall (x :: FloatInfo) (y :: FloatInfo). FloatInfoRepr x -> FloatInfoRepr y -> Bool Source #

gtF :: forall (x :: FloatInfo) (y :: FloatInfo). FloatInfoRepr x -> FloatInfoRepr y -> Bool Source #

ShowF FloatInfoRepr Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods withShow :: forall p q (tp :: FloatInfo) a. p FloatInfoRepr -> q tp -> (Show (FloatInfoRepr tp) => a) -> a Source # showF :: forall (tp :: FloatInfo). FloatInfoRepr tp -> String Source # showsPrecF :: forall (tp :: FloatInfo). Int -> FloatInfoRepr tp -> String -> String Source #
KnownRepr FloatInfoRepr DoubleDoubleFloat Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr DoubleDoubleFloat Source #
KnownRepr FloatInfoRepr DoubleFloat Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr DoubleFloat Source #
KnownRepr FloatInfoRepr HalfFloat Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr HalfFloat Source #
KnownRepr FloatInfoRepr QuadFloat Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr QuadFloat Source #
KnownRepr FloatInfoRepr SingleFloat Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr SingleFloat Source #
KnownRepr FloatInfoRepr X86_80Float Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr X86_80Float Source #
Show (FloatInfoRepr fi) Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods showsPrec :: Int -> FloatInfoRepr fi -> ShowS Source # show :: FloatInfoRepr fi -> String Source # showList :: [FloatInfoRepr fi] -> ShowS Source #
Eq (FloatInfoRepr fi) Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods (==) :: FloatInfoRepr fi -> FloatInfoRepr fi -> Bool Source # (/=) :: FloatInfoRepr fi -> FloatInfoRepr fi -> Bool Source #
Hashable (FloatInfoRepr fi) Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods hashWithSalt :: Int -> FloatInfoRepr fi -> Int Source # hash :: FloatInfoRepr fi -> Int Source #
Pretty (FloatInfoRepr fi) Source # |
Instance details Defined in What4.InterpretedFloatingPoint Methods pretty :: FloatInfoRepr fi -> Doc ann Source # prettyList :: [FloatInfoRepr fi] -> Doc ann Source #

## extended 80 bit float values ("long double")

data X86_80Val Source #

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

Constructors

X86_80Val Word16 Word64 |

#### Instances

Instances details

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

Instance details

Defined in What4.InterpretedFloatingPoint

Methods

compare :: X86_80Val -> X86_80Val -> Ordering Source #

(<) :: X86_80Val -> X86_80Val -> Bool Source #

(<=) :: X86_80Val -> X86_80Val -> Bool Source #

(>) :: X86_80Val -> X86_80Val -> Bool Source #

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

max :: X86_80Val -> X86_80Val -> X86_80Val Source #

min :: X86_80Val -> X86_80Val -> X86_80Val Source #

fp80ToBits :: X86_80Val -> Integer Source #

fp80ToRational :: X86_80Val -> Maybe Rational Source #

## FloatInfo to/from FloatPrecision

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

Equations

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

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

Equations

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

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

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

## Bit-width type family

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

Equations

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

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

# Interface classes

## Interpretation type family

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

Interpretation of the floating point type.

#### Instances

Instances details

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

## Type alias

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

Symbolic floating point numbers.

## IsInterpretedFloatExprBuilder

class IsExprBuilder sym => IsInterpretedFloatExprBuilder sym where Source #

Abstact floating point operations.

Minimal complete definition

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

Methods

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

Return floating point number `+0`.

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

Return floating point number `-0`.

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

Return floating point NaN.

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

Return floating point `+infinity`.

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

Return floating point `-infinity`.

iFloatLitRational :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). sym -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi) Source #

Negate a floating point number.

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

Return the absolute value of a floating point number.

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

Compute the square root of a floating point number.

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

Add two floating point numbers.

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

Subtract two floating point numbers.

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

Multiply two floating point numbers.

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

Divide two floating point numbers.

iFloatRem :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi) Source #

Return the min of two floating point numbers.

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

Return the max of two floating point numbers.

iFloatFMA :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). sym -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (Pred sym) Source #

Check logical equality of two floating point numbers.

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

Check logical non-equality of two floating point numbers.

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

Check IEEE equality of two floating point numbers.

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

Check IEEE apartness of two floating point numbers.

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

Check `<=` on two floating point numbers.

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

Check `<` on two floating point numbers.

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

Check `>=` on two floating point numbers.

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

Check `>` on two floating point numbers.

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

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

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

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

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

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

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

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

If-then-else on floating point numbers.

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

Change the precision of a floating point number.

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

Round a floating point number to an integral value.

iFloatFromBinary :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (w :: Natural) (fi :: FloatInfo). 1 <= w => sym -> FloatInfoRepr fi -> RoundingMode -> SymBV sym w -> IO (SymInterpretedFloat sym fi) Source #

Convert a unsigned bitvector to a floating point number.

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

Convert a signed bitvector to a floating point number.

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

Convert a real number to a floating point number.

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

Convert a floating point number to a unsigned bitvector.

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

Convert a floating point number to a signed bitvector.

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

Convert a floating point number to a real number.

iFloatSpecialFunction :: forall (fi :: FloatInfo) (args :: Ctx Type). sym -> FloatInfoRepr fi -> SpecialFunction args -> Assignment (SpecialFnArg (SymExpr sym) (SymInterpretedFloatType sym fi)) args -> IO (SymInterpretedFloat sym fi) Source #

Apply a special function to floating-point arguments

iFloatSpecialFunction0 :: forall (fi :: FloatInfo). sym -> FloatInfoRepr fi -> SpecialFunction (EmptyCtx :: Ctx Type) -> IO (SymInterpretedFloat sym fi) Source #

Access a 0-arity special function constant

iFloatSpecialFunction1 :: forall (fi :: FloatInfo). sym -> FloatInfoRepr fi -> SpecialFunction ((EmptyCtx :: Ctx Type) ::> R) -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi) Source #

Apply a 1-argument special function

iFloatSpecialFunction2 :: forall (fi :: FloatInfo). sym -> FloatInfoRepr fi -> SpecialFunction (((EmptyCtx :: Ctx Type) ::> R) ::> R) -> SymInterpretedFloat sym fi -> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi) Source #

Apply a 2-argument special function

iFloatBaseTypeRepr :: forall (fi :: FloatInfo). 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 :: Natural) (fi :: FloatInfo). 1 <= w => ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> RoundingMode -> SymBV (ExprBuilder t st (Flags FloatIEEE)) w -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iSBVToFloat :: forall (w :: Natural) (fi :: FloatInfo). 1 <= w => ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> RoundingMode -> SymBV (ExprBuilder t st (Flags FloatIEEE)) w -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) 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 :: Natural) (fi :: FloatInfo). 1 <= w => ExprBuilder t st (Flags FloatIEEE) -> NatRepr w -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatIEEE)) w) Source #

iFloatToSBV :: forall (w :: Natural) (fi :: FloatInfo). 1 <= w => ExprBuilder t st (Flags FloatIEEE) -> NatRepr w -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatIEEE)) w) 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 #

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

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

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

iFloatSpecialFunction2 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> SpecialFunction (((EmptyCtx :: Ctx Type) ::> R) ::> R) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) 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 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 :: Natural) (fi :: FloatInfo). 1 <= w => ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> RoundingMode -> SymBV (ExprBuilder t st (Flags FloatReal)) w -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iSBVToFloat :: forall (w :: Natural) (fi :: FloatInfo). 1 <= w => ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> RoundingMode -> SymBV (ExprBuilder t st (Flags FloatReal)) w -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) 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 :: Natural) (fi :: FloatInfo). 1 <= w => ExprBuilder t st (Flags FloatReal) -> NatRepr w -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatReal)) w) Source #

iFloatToSBV :: forall (w :: Natural) (fi :: FloatInfo). 1 <= w => ExprBuilder t st (Flags FloatReal) -> NatRepr w -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatReal)) w) 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 #

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

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

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

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

iFloatBaseTypeRepr :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType (ExprBuilder t st (Flags FloatReal)) 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 :: Natural) (fi :: FloatInfo). 1 <= w => ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> RoundingMode -> SymBV (ExprBuilder t st (Flags FloatUninterpreted)) w -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iSBVToFloat :: forall (w :: Natural) (fi :: FloatInfo). 1 <= w => ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> RoundingMode -> SymBV (ExprBuilder t st (Flags FloatUninterpreted)) w -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) 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 :: Natural) (fi :: FloatInfo). 1 <= w => ExprBuilder t st (Flags FloatUninterpreted) -> NatRepr w -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatUninterpreted)) w) Source #

iFloatToSBV :: forall (w :: Natural) (fi :: FloatInfo). 1 <= w => ExprBuilder t st (Flags FloatUninterpreted) -> NatRepr w -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatUninterpreted)) w) 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 #

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

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

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

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

iFloatBaseTypeRepr :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType (ExprBuilder t st (Flags FloatUninterpreted)) 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 :: forall (fi :: FloatInfo). sym -> SolverSymbol -> FloatInfoRepr fi -> IO (SymExpr sym (SymInterpretedFloatType sym fi)) Source #

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

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

Create a fresh floating-point latch variable.

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

Methods

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

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

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