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

What4.Utils.FloatHelpers

Synopsis

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

Eq RoundingMode Source # 
Instance details

Defined in What4.Utils.FloatHelpers

Ord RoundingMode Source # 
Instance details

Defined in What4.Utils.FloatHelpers

Show RoundingMode Source # 
Instance details

Defined in What4.Utils.FloatHelpers

Generic RoundingMode Source # 
Instance details

Defined in What4.Utils.FloatHelpers

Associated Types

type Rep RoundingMode :: Type -> Type #

Hashable RoundingMode Source # 
Instance details

Defined in What4.Utils.FloatHelpers

type Rep RoundingMode Source # 
Instance details

Defined in What4.Utils.FloatHelpers

type Rep RoundingMode = D1 ('MetaData "RoundingMode" "What4.Utils.FloatHelpers" "what4-1.1-F6JmVDCUG2e4tsAmUzrLc2" '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))))

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.