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

Safe Haskell | None
Language | Haskell2010

What4.Utils.FloatHelpers

Synopsis

- data RoundingMode
  - = RNE
  - | RNA
  - | RTP
  - | RTN
  - | RTZ
- bfStatus :: HasCallStack => (a, Status) -> a
- fppOpts :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> BFOpts
- toRoundMode :: RoundingMode -> RoundMode
- fpOpts :: Integer -> Integer -> RoundMode -> BFOpts
- floatFromInteger :: BFOpts -> Integer -> BigFloat
- floatFromRational :: BFOpts -> Rational -> BigFloat
- floatToRational :: BigFloat -> Maybe Rational
- floatToInteger :: RoundingMode -> BigFloat -> Maybe Integer
- floatRoundToInt :: forall (fpp :: FloatPrecision). HasCallStack => FloatPrecisionRepr fpp -> RoundingMode -> BigFloat -> BigFloat

# Documentation

data RoundingMode Source #

Rounding modes for IEEE-754 floating point operations.

Constructors

RNE | Round to nearest even.
RNA | Round to nearest away.
RTP | Round toward plus Infinity.
RTN | Round toward minus Infinity.
RTZ | Round toward zero.

#### Instances

Instances details

Enum RoundingMode Source # |

Instance details

Defined in What4.Utils.FloatHelpers

Methods

succ :: RoundingMode -> RoundingMode Source #

pred :: RoundingMode -> RoundingMode Source #

toEnum :: Int -> RoundingMode Source #

fromEnum :: RoundingMode -> Int Source #

enumFrom :: RoundingMode -> [RoundingMode] Source #

enumFromThen :: RoundingMode -> RoundingMode -> [RoundingMode] Source #

enumFromTo :: RoundingMode -> RoundingMode -> [RoundingMode] Source #

enumFromThenTo :: RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode] Source #

Generic RoundingMode Source # |

Instance details

Defined in What4.Utils.FloatHelpers

Associated Types

type Rep RoundingMode |

Instance details

Defined in What4.Utils.FloatHelpers

type Rep RoundingMode = D1 ('MetaData "RoundingMode" "What4.Utils.FloatHelpers" "what4-1.6.3-9uBVkRxr1Ru1evGDxWAmM9" 'False) ((C1 ('MetaCons "RNE" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RNA" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RTP" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "RTN" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RTZ" 'PrefixI 'False) (U1 :: Type -> Type))))

Methods

from :: RoundingMode -> Rep RoundingMode x Source #

to :: Rep RoundingMode x -> RoundingMode Source #

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

Instance details

Defined in What4.Utils.FloatHelpers

Methods

compare :: RoundingMode -> RoundingMode -> Ordering Source #

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

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

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

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

max :: RoundingMode -> RoundingMode -> RoundingMode Source #

min :: RoundingMode -> RoundingMode -> RoundingMode Source #

Hashable RoundingMode Source # |
Instance details Defined in What4.Utils.FloatHelpers Methods hashWithSalt :: Int -> RoundingMode -> Int Source # hash :: RoundingMode -> Int Source #
type Rep RoundingMode Source # |

Instance details

Defined in What4.Utils.FloatHelpers

type Rep RoundingMode = D1 ('MetaData "RoundingMode" "What4.Utils.FloatHelpers" "what4-1.6.3-9uBVkRxr1Ru1evGDxWAmM9" 'False) ((C1 ('MetaCons "RNE" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RNA" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RTP" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "RTN" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RTZ" 'PrefixI 'False) (U1 :: Type -> Type))))

bfStatus :: HasCallStack => (a, Status) -> a Source #

fppOpts :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> BFOpts Source #

toRoundMode :: RoundingMode -> RoundMode Source #

fpOpts :: Integer -> Integer -> RoundMode -> BFOpts Source #

Make LibBF options for the given precision and rounding mode.

floatFromInteger :: BFOpts -> Integer -> BigFloat Source #

Make a floating point number from an integer, using the given rounding mode

floatFromRational :: BFOpts -> Rational -> BigFloat Source #

Make a floating point number from a rational, using the given rounding mode

floatToRational :: BigFloat -> Maybe Rational Source #

Convert a floating point number to a rational, if possible.

floatToInteger :: RoundingMode -> BigFloat -> Maybe Integer Source #

Convert a floating point number to an integer, if possible.

floatRoundToInt :: forall (fpp :: FloatPrecision). HasCallStack => FloatPrecisionRepr fpp -> RoundingMode -> BigFloat -> BigFloat Source #