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

Copyright | (c) Galois Inc 2014-2022
License | BSD3
Maintainer | rdockins@galois.com
Stability | provisional
Safe Haskell | Safe-Inferred
Language | Haskell2010

What4.FloatMode

Description

Desired instances for the `IsInterpretedFloatExprBuilder` class are selected via the different mode values from this module.

Synopsis

- data FloatMode
- data FloatModeRepr (a :: FloatMode) where
  - FloatIEEERepr :: FloatModeRepr 'FloatIEEE
  - FloatUninterpretedRepr :: FloatModeRepr 'FloatUninterpreted
  - FloatRealRepr :: FloatModeRepr 'FloatReal
- type FloatIEEE = 'FloatIEEE
- type FloatUninterpreted = 'FloatUninterpreted
- type FloatReal = 'FloatReal

# Documentation

data FloatMode Source #

Mode flag for how floating-point values should be interpreted.

#### Instances

Instances details

TestEquality FloatModeRepr Source # |
Instance details Defined in What4.FloatMode Methods testEquality :: forall (a :: FloatMode) (b :: FloatMode). FloatModeRepr a -> FloatModeRepr b -> Maybe (a :~: b) Source #
ShowF FloatModeRepr Source # |
Instance details Defined in What4.FloatMode Methods withShow :: forall p q (tp :: FloatMode) a. p FloatModeRepr -> q tp -> (Show (FloatModeRepr tp) => a) -> a Source # showF :: forall (tp :: FloatMode). FloatModeRepr tp -> String Source # showsPrecF :: forall (tp :: FloatMode). Int -> FloatModeRepr tp -> String -> String Source #
KnownRepr FloatModeRepr FloatIEEE Source # |
Instance details Defined in What4.FloatMode Methods knownRepr :: FloatModeRepr FloatIEEE Source #
KnownRepr FloatModeRepr FloatReal Source # |
Instance details Defined in What4.FloatMode Methods knownRepr :: FloatModeRepr FloatReal Source #
KnownRepr FloatModeRepr FloatUninterpreted Source # |
Instance details Defined in What4.FloatMode Methods knownRepr :: FloatModeRepr FloatUninterpreted Source #

data FloatModeRepr (a :: FloatMode) where Source #

Constructors

FloatIEEERepr :: FloatModeRepr 'FloatIEEE |
FloatUninterpretedRepr :: FloatModeRepr 'FloatUninterpreted |
FloatRealRepr :: FloatModeRepr 'FloatReal |

#### Instances

Instances details

TestEquality FloatModeRepr Source # |
Instance details Defined in What4.FloatMode Methods testEquality :: forall (a :: FloatMode) (b :: FloatMode). FloatModeRepr a -> FloatModeRepr b -> Maybe (a :~: b) Source #
ShowF FloatModeRepr Source # |
Instance details Defined in What4.FloatMode Methods withShow :: forall p q (tp :: FloatMode) a. p FloatModeRepr -> q tp -> (Show (FloatModeRepr tp) => a) -> a Source # showF :: forall (tp :: FloatMode). FloatModeRepr tp -> String Source # showsPrecF :: forall (tp :: FloatMode). Int -> FloatModeRepr tp -> String -> String Source #
KnownRepr FloatModeRepr FloatIEEE Source # |
Instance details Defined in What4.FloatMode Methods knownRepr :: FloatModeRepr FloatIEEE Source #
KnownRepr FloatModeRepr FloatReal Source # |
Instance details Defined in What4.FloatMode Methods knownRepr :: FloatModeRepr FloatReal Source #
KnownRepr FloatModeRepr FloatUninterpreted Source # |
Instance details Defined in What4.FloatMode Methods knownRepr :: FloatModeRepr FloatUninterpreted Source #
Show (FloatModeRepr fm) Source # |
Instance details Defined in What4.FloatMode Methods showsPrec :: Int -> FloatModeRepr fm -> ShowS Source # show :: FloatModeRepr fm -> String Source # showList :: [FloatModeRepr fm] -> ShowS Source #

type FloatIEEE = 'FloatIEEE Source #

In this mode "interpreted" floating-point values are treated as bit-precise IEEE-754 floats.

type FloatUninterpreted = 'FloatUninterpreted Source #

In this mode "interpreted" floating-point values are treated as bitvectors of the appropriate width, and all operations on them are translated as uninterpreted functions.

type FloatReal = 'FloatReal Source #

In this mode "interpreted" floating-point values are treated as real-number values, to the extent possible. Expressions that would result in infinities or NaN will yield unspecified values in this mode, or directly produce runtime errors.