Copyright	(c) Sirui Lu 2024
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	Safe-Inferred
Language	Haskell2010

Grisette.Internal.Core.Data.Class.IEEEFP

Description

Synopsis

fpIsNaN :: RealFloat a => a -> Bool
fpIsPositiveZero :: RealFloat a => a -> Bool
fpIsNegativeZero :: RealFloat a => a -> Bool
fpIsPositiveInfinite :: RealFloat a => a -> Bool
fpIsNegativeInfinite :: RealFloat a => a -> Bool
fpIsPositive :: RealFloat a => a -> Bool
fpIsNegative :: RealFloat a => a -> Bool
fpIsInfinite :: RealFloat a => a -> Bool
fpIsZero :: RealFloat a => a -> Bool
fpIsNormal :: RealFloat a => a -> Bool
fpIsSubnormal :: RealFloat a => a -> Bool
fpIsPoint :: RealFloat a => a -> Bool
class SymIEEEFPTraits a where
- symFpIsNaN :: a -> SymBool
- symFpIsPositive :: a -> SymBool
- symFpIsNegative :: a -> SymBool
- symFpIsPositiveInfinite :: a -> SymBool
- symFpIsNegativeInfinite :: a -> SymBool
- symFpIsInfinite :: a -> SymBool
- symFpIsPositiveZero :: a -> SymBool
- symFpIsNegativeZero :: a -> SymBool
- symFpIsZero :: a -> SymBool
- symFpIsNormal :: a -> SymBool
- symFpIsSubnormal :: a -> SymBool
- symFpIsPoint :: a -> SymBool
class IEEEConstants a where
- fpPositiveInfinite :: a
- fpNegativeInfinite :: a
- fpNaN :: a
- fpNegativeZero :: a
- fpPositiveZero :: a
class IEEEFPRoundingMode mode where
- rne :: mode
- rna :: mode
- rtp :: mode
- rtn :: mode
- rtz :: mode
class IEEEFPOp a where
- symFpAbs :: a -> a
- symFpNeg :: a -> a
- symFpRem :: a -> a -> a
- symFpMin :: a -> a -> a
- symFpMax :: a -> a -> a
class IEEEFPRoundingMode mode => IEEEFPRoundingOp a mode | a -> mode where
- symFpAdd :: mode -> a -> a -> a
- symFpSub :: mode -> a -> a -> a
- symFpMul :: mode -> a -> a -> a
- symFpDiv :: mode -> a -> a -> a
- symFpFMA :: mode -> a -> a -> a -> a
- symFpSqrt :: mode -> a -> a
- symFpRoundToIntegral :: mode -> a -> a

Documentation

fpIsNaN :: RealFloat a => a -> Bool Source #

Check if a floating-point number is not-a-number.

fpIsPositiveZero :: RealFloat a => a -> Bool Source #

Check if a floating-point number is positive zero.

fpIsNegativeZero :: RealFloat a => a -> Bool Source #

Check if a floating-point number is negative zero.

fpIsPositiveInfinite :: RealFloat a => a -> Bool Source #

Check if a floating-point number is positive infinite.

fpIsNegativeInfinite :: RealFloat a => a -> Bool Source #

Check if a floating-point number is negative infinite.

fpIsPositive :: RealFloat a => a -> Bool Source #

Check if a floating-point number is positive. +0, +inf are considered positive. nan, -0, -inf are not positive.

fpIsNegative :: RealFloat a => a -> Bool Source #

Check if a floating-point number is negative. -0, -inf are considered negative. nan, +0, +inf are not negative.

fpIsInfinite :: RealFloat a => a -> Bool Source #

Check if a floating-point number is infinite.

fpIsZero :: RealFloat a => a -> Bool Source #

Check if a floating-point number is zero.

fpIsNormal :: RealFloat a => a -> Bool Source #

Check if a floating-point number is normal, i.e., not 0, not inf, not nan, and not denormalized.

fpIsSubnormal :: RealFloat a => a -> Bool Source #

Check if a floating-point number is subnormal, i.e., denormalized. 0, inf, or nan are not subnormal.

fpIsPoint :: RealFloat a => a -> Bool Source #

Check if a floating-point number is a point, i.e., not inf, not nan.

class SymIEEEFPTraits a where Source #

A class for symbolic traits of IEEE floating-point numbers.

Methods

symFpIsNaN :: a -> SymBool Source #

Check if a symbolic floating-point number is not-a-number.

symFpIsPositive :: a -> SymBool Source #

Check if a symbolic floating-point number is positive. +0, +inf are considered positive. nan, -0, -inf are not positive.

symFpIsNegative :: a -> SymBool Source #

Check if a symbolic floating-point number is negative. -0, -inf are considered negative. nan, +0, +inf are not negative.

symFpIsPositiveInfinite :: a -> SymBool Source #

Check if a symbolic floating-point number is positive infinite.

symFpIsNegativeInfinite :: a -> SymBool Source #

Check if a symbolic floating-point number is negative infinite.

symFpIsInfinite :: a -> SymBool Source #

Check if a symbolic floating-point number is infinite.

symFpIsPositiveZero :: a -> SymBool Source #

Check if a symbolic floating-point number is positive zero.

symFpIsNegativeZero :: a -> SymBool Source #

Check if a symbolic floating-point number is negative zero.

symFpIsZero :: a -> SymBool Source #

Check if a symbolic floating-point number is zero.

symFpIsNormal :: a -> SymBool Source #

Check if a symbolic floating-point number is normal, i.e., not 0, not inf, not nan, and not denormalized.

symFpIsSubnormal :: a -> SymBool Source #

Check if a symbolic floating-point number is subnormal, i.e., denormalized. 0, inf, or nan are not subnormal.

symFpIsPoint :: a -> SymBool Source #

Check if a symbolic floating-point number is a point, i.e., not inf, not nan.

Instances

Instances details

SymIEEEFPTraits Double Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.IEEEFP Methods symFpIsNaN :: Double -> SymBool Source # symFpIsPositive :: Double -> SymBool Source # symFpIsNegative :: Double -> SymBool Source # symFpIsPositiveInfinite :: Double -> SymBool Source # symFpIsNegativeInfinite :: Double -> SymBool Source # symFpIsInfinite :: Double -> SymBool Source # symFpIsPositiveZero :: Double -> SymBool Source # symFpIsNegativeZero :: Double -> SymBool Source # symFpIsZero :: Double -> SymBool Source # symFpIsNormal :: Double -> SymBool Source # symFpIsSubnormal :: Double -> SymBool Source # symFpIsPoint :: Double -> SymBool Source #
SymIEEEFPTraits Float Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.IEEEFP Methods symFpIsNaN :: Float -> SymBool Source # symFpIsPositive :: Float -> SymBool Source # symFpIsNegative :: Float -> SymBool Source # symFpIsPositiveInfinite :: Float -> SymBool Source # symFpIsNegativeInfinite :: Float -> SymBool Source # symFpIsInfinite :: Float -> SymBool Source # symFpIsPositiveZero :: Float -> SymBool Source # symFpIsNegativeZero :: Float -> SymBool Source # symFpIsZero :: Float -> SymBool Source # symFpIsNormal :: Float -> SymBool Source # symFpIsSubnormal :: Float -> SymBool Source # symFpIsPoint :: Float -> SymBool Source #
ValidFP eb sb => SymIEEEFPTraits (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.IEEEFP Methods symFpIsNaN :: FP eb sb -> SymBool Source # symFpIsPositive :: FP eb sb -> SymBool Source # symFpIsNegative :: FP eb sb -> SymBool Source # symFpIsPositiveInfinite :: FP eb sb -> SymBool Source # symFpIsNegativeInfinite :: FP eb sb -> SymBool Source # symFpIsInfinite :: FP eb sb -> SymBool Source # symFpIsPositiveZero :: FP eb sb -> SymBool Source # symFpIsNegativeZero :: FP eb sb -> SymBool Source # symFpIsZero :: FP eb sb -> SymBool Source # symFpIsNormal :: FP eb sb -> SymBool Source # symFpIsSubnormal :: FP eb sb -> SymBool Source # symFpIsPoint :: FP eb sb -> SymBool Source #
ValidFP eb sb => SymIEEEFPTraits (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.IEEEFP Methods symFpIsNaN :: SymFP eb sb -> SymBool Source # symFpIsPositive :: SymFP eb sb -> SymBool Source # symFpIsNegative :: SymFP eb sb -> SymBool Source # symFpIsPositiveInfinite :: SymFP eb sb -> SymBool Source # symFpIsNegativeInfinite :: SymFP eb sb -> SymBool Source # symFpIsInfinite :: SymFP eb sb -> SymBool Source # symFpIsPositiveZero :: SymFP eb sb -> SymBool Source # symFpIsNegativeZero :: SymFP eb sb -> SymBool Source # symFpIsZero :: SymFP eb sb -> SymBool Source # symFpIsNormal :: SymFP eb sb -> SymBool Source # symFpIsSubnormal :: SymFP eb sb -> SymBool Source # symFpIsPoint :: SymFP eb sb -> SymBool Source #

class IEEEConstants a where Source #

Constants for IEEE floating-point numbers.

Methods

fpPositiveInfinite :: a Source #

Positive infinity.

fpNegativeInfinite :: a Source #

Negative infinity.

fpNaN :: a Source #

Not-a-number.

fpNegativeZero :: a Source #

Negative zero.

fpPositiveZero :: a Source #

Positive zero.

Instances

Instances details

ValidFP eb sb => IEEEConstants (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.IEEEFP Methods fpPositiveInfinite :: FP eb sb Source # fpNegativeInfinite :: FP eb sb Source # fpNaN :: FP eb sb Source # fpNegativeZero :: FP eb sb Source # fpPositiveZero :: FP eb sb Source #
ValidFP eb sb => IEEEConstants (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.IEEEFP Methods fpPositiveInfinite :: SymFP eb sb Source # fpNegativeInfinite :: SymFP eb sb Source # fpNaN :: SymFP eb sb Source # fpNegativeZero :: SymFP eb sb Source # fpPositiveZero :: SymFP eb sb Source #

class IEEEFPRoundingMode mode where Source #

Rounding modes for floating-point operations.

Methods

rne :: mode Source #

Round to nearest, ties to even.

rna :: mode Source #

Round to nearest, ties to away from zero.

rtp :: mode Source #

Round towards positive infinity.

rtn :: mode Source #

Round towards negative infinity.

rtz :: mode Source #

Round towards zero.

Instances

Instances details

IEEEFPRoundingMode FPRoundingMode Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.IEEEFP Methods rne :: FPRoundingMode Source # rna :: FPRoundingMode Source # rtp :: FPRoundingMode Source # rtn :: FPRoundingMode Source # rtz :: FPRoundingMode Source #
IEEEFPRoundingMode SymFPRoundingMode Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.IEEEFP Methods rne :: SymFPRoundingMode Source # rna :: SymFPRoundingMode Source # rtp :: SymFPRoundingMode Source # rtn :: SymFPRoundingMode Source # rtz :: SymFPRoundingMode Source #

class IEEEFPOp a where Source #

Operations on IEEE floating-point numbers, without rounding mode.

Methods

symFpAbs :: a -> a Source #

symFpNeg :: a -> a Source #

symFpRem :: a -> a -> a Source #

symFpMin :: a -> a -> a Source #

symFpMax :: a -> a -> a Source #

Instances

Instances details

ValidFP eb sb => IEEEFPOp (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.IEEEFP Methods symFpAbs :: SymFP eb sb -> SymFP eb sb Source # symFpNeg :: SymFP eb sb -> SymFP eb sb Source # symFpRem :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source # symFpMin :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source # symFpMax :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

class IEEEFPRoundingMode mode => IEEEFPRoundingOp a mode | a -> mode where Source #

Operations on IEEE floating-point numbers, with rounding mode.

Methods

symFpAdd :: mode -> a -> a -> a Source #

symFpSub :: mode -> a -> a -> a Source #

symFpMul :: mode -> a -> a -> a Source #

symFpDiv :: mode -> a -> a -> a Source #

symFpFMA :: mode -> a -> a -> a -> a Source #

symFpSqrt :: mode -> a -> a Source #

symFpRoundToIntegral :: mode -> a -> a Source #

Instances

Instances details

ValidFP eb sb => IEEEFPRoundingOp (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.IEEEFP

Methods

symFpAdd :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

symFpSub :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

symFpMul :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

symFpDiv :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

symFpFMA :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

symFpSqrt :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb Source #

symFpRoundToIntegral :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb Source #