sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Data.SBV.Float

Contents

- Type-sized floats
- Constructing values
- Operations

Description

A collection of arbitrary float operations.

Synopsis

- data FP = FP {
  - fpExponentSize :: Int
  - fpSignificandSize :: Int
  - fpValue :: BigFloat
  }
- fpFromRawRep :: Bool -> (Integer, Int) -> (Integer, Int) -> FP
- fpFromBigFloat :: Int -> Int -> BigFloat -> FP
- fpNaN :: Int -> Int -> FP
- fpInf :: Bool -> Int -> Int -> FP
- fpZero :: Bool -> Int -> Int -> FP
- fpFromInteger :: Int -> Int -> Integer -> FP
- fpFromRational :: Int -> Int -> Rational -> FP
- fpFromFloat :: Int -> Int -> Float -> FP
- fpFromDouble :: Int -> Int -> Double -> FP
- fpEncodeFloat :: Int -> Int -> Integer -> Int -> FP

# Type-sized floats

data FP Source #

Internal representation of a parameterized float.

A note on cardinality: If we have eb exponent bits, and sb significand bits, then the total number of floats is 2^sb*(2^eb-1) + 3: All exponents except 11..11 is allowed. So we get, 2^eb-1, different combinations, each with a sign, giving us 2^sb*(2^eb-1) totals. Then we have two infinities, and one NaN, adding 3 more.

Constructors

FP |

Fields

- fpExponentSize :: Int
- fpSignificandSize :: Int
- fpValue :: BigFloat

#### Instances

Instances details

Floating FP Source # | Floating instance for big-floats

Instance details

Defined in Data.SBV.Core.SizedFloats

Methods

pi :: FP Source #

exp :: FP -> FP Source #

log :: FP -> FP Source #

sqrt :: FP -> FP Source #

(**) :: FP -> FP -> FP Source #

logBase :: FP -> FP -> FP Source #

sin :: FP -> FP Source #

cos :: FP -> FP Source #

tan :: FP -> FP Source #

asin :: FP -> FP Source #

acos :: FP -> FP Source #

atan :: FP -> FP Source #

sinh :: FP -> FP Source #

cosh :: FP -> FP Source #

tanh :: FP -> FP Source #

asinh :: FP -> FP Source #

acosh :: FP -> FP Source #

atanh :: FP -> FP Source #

log1p :: FP -> FP Source #

expm1 :: FP -> FP Source #

log1pexp :: FP -> FP Source #

log1mexp :: FP -> FP Source #

RealFloat FP Source # | Real-float instance for big-floats. Beware! Some of these aren't really all that well tested.

Instance details

Defined in Data.SBV.Core.SizedFloats

Methods

floatRadix :: FP -> Integer Source #

floatDigits :: FP -> Int Source #

floatRange :: FP -> (Int, Int) Source #

decodeFloat :: FP -> (Integer, Int) Source #

encodeFloat :: Integer -> Int -> FP Source #

exponent :: FP -> Int Source #

significand :: FP -> FP Source #

scaleFloat :: Int -> FP -> FP Source #

isNaN :: FP -> Bool Source #

isInfinite :: FP -> Bool Source #

isDenormalized :: FP -> Bool Source #

isNegativeZero :: FP -> Bool Source #

isIEEE :: FP -> Bool Source #

atan2 :: FP -> FP -> FP Source #

Num FP Source # | Num instance for big-floats
Instance details Defined in Data.SBV.Core.SizedFloats Methods (+) :: FP -> FP -> FP Source # (-) :: FP -> FP -> FP Source # (*) :: FP -> FP -> FP Source # negate :: FP -> FP Source # abs :: FP -> FP Source # signum :: FP -> FP Source # fromInteger :: Integer -> FP Source #
Fractional FP Source # | Fractional instance for big-floats
Instance details Defined in Data.SBV.Core.SizedFloats Methods (/) :: FP -> FP -> FP Source # recip :: FP -> FP Source # fromRational :: Rational -> FP Source #
Real FP Source # | Real instance for big-floats. Beware, not that well tested!
Instance details Defined in Data.SBV.Core.SizedFloats Methods toRational :: FP -> Rational Source #
RealFrac FP Source # | Real-frac instance for big-floats. Beware, not that well tested!
Instance details Defined in Data.SBV.Core.SizedFloats Methods properFraction :: Integral b => FP -> (b, FP) Source # truncate :: Integral b => FP -> b Source # round :: Integral b => FP -> b Source # ceiling :: Integral b => FP -> b Source # floor :: Integral b => FP -> b Source #
Show FP Source # |
Instance details Defined in Data.SBV.Core.SizedFloats Methods showsPrec :: Int -> FP -> ShowS Source # show :: FP -> String Source # showList :: [FP] -> ShowS Source #
Eq FP Source # |
Instance details Defined in Data.SBV.Core.SizedFloats Methods (==) :: FP -> FP -> Bool Source # (/=) :: FP -> FP -> Bool Source #
Ord FP Source # |
Instance details Defined in Data.SBV.Core.SizedFloats Methods compare :: FP -> FP -> Ordering Source # (<) :: FP -> FP -> Bool Source # (<=) :: FP -> FP -> Bool Source # (>) :: FP -> FP -> Bool Source # (>=) :: FP -> FP -> Bool Source # max :: FP -> FP -> FP Source # min :: FP -> FP -> FP Source #

# Constructing values

fpFromRawRep :: Bool -> (Integer, Int) -> (Integer, Int) -> FP Source #

Convert from an signexponentmantissa representation to a float. The values are the integers representing the bit-patterns of these values, i.e., the raw representation. We assume that these integers fit into the ranges given, i.e., no overflow checking is done here.

fpFromBigFloat :: Int -> Int -> BigFloat -> FP Source #

Construct a float, by appropriately rounding

fpNaN :: Int -> Int -> FP Source #

Make NaN. Exponent is all 1s. Significand is non-zero. The sign is irrelevant.

fpInf :: Bool -> Int -> Int -> FP Source #

Make Infinity. Exponent is all 1s. Significand is 0.

fpZero :: Bool -> Int -> Int -> FP Source #

Make a signed zero.

# Operations

fpFromInteger :: Int -> Int -> Integer -> FP Source #

Make from an integer value.

fpFromRational :: Int -> Int -> Rational -> FP Source #

Make a generalized floating-point value from a `Rational`.

fpFromFloat :: Int -> Int -> Float -> FP Source #

Convert from a IEEE float.

fpFromDouble :: Int -> Int -> Double -> FP Source #

Convert from a IEEE double.

fpEncodeFloat :: Int -> Int -> Integer -> Int -> FP Source #

Encode from exponent/mantissa form to a float representation. Corresponds to `encodeFloat` in Haskell.