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.SymPrim.FP

Description

Synopsis

type ValidFP (eb :: Nat) (sb :: Nat) = ValidFloat eb sb
newtype FP (eb :: Nat) (sb :: Nat) = FP {
- unFP :: FloatingPoint eb sb
}
type FP16 = FP 5 11
type FP32 = FP 8 24
type FP64 = FP 11 53
withValidFPProofs :: forall eb sb r. ValidFP eb sb => ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb), 1 <= eb, 1 <= sb) => r) -> r
data FPRoundingMode
- = RNE
- | RNA
- | RTP
- | RTN
- | RTZ
allFPRoundingMode :: [FPRoundingMode]
data NotRepresentableFPError
- = NaNError
- | FPUnderflowError
- | FPOverflowError
class ConvertibleBound bv where
- convertibleLowerBound :: forall eb sb n. (ValidFP eb sb, KnownNat n, 1 <= n) => bv n -> FPRoundingMode -> FP eb sb
- convertibleUpperBound :: forall eb sb n. (ValidFP eb sb, KnownNat n, 1 <= n) => bv n -> FPRoundingMode -> FP eb sb
nextFP :: forall eb sb. ValidFP eb sb => FP eb sb -> FP eb sb
prevFP :: forall eb sb. ValidFP eb sb => FP eb sb -> FP eb sb
withUnsafeValidFP :: forall eb sb r. (KnownNat eb, KnownNat sb) => (ValidFP eb sb => r) -> r
checkDynamicValidFP :: Natural -> Natural -> Bool
invalidFPMessage :: String

Documentation

type ValidFP (eb :: Nat) (sb :: Nat) = ValidFloat eb sb Source #

A type-level proof that the given bit-widths are valid for a floating-point number.

newtype FP (eb :: Nat) (sb :: Nat) Source #

IEEE 754 floating-point number with eb exponent bits and sb significand bits.

>>> 1.0 + 2.0 :: FP 11 53
3.0

More operations are available. Please refer to Grisette.Core for more information.

Constructors

FP
Fields unFP :: FloatingPoint eb sb

Instances

Instances details

PEvalFPTerm FP Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFP Methods pevalFPTraitTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPTrait -> Term (FP eb sb) -> Term Bool Source # pevalFPUnaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPUnaryOp -> Term (FP eb sb) -> Term (FP eb sb) Source # pevalFPBinaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPBinaryOp -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source # pevalFPRoundingUnaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPRoundingUnaryOp -> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb) Source # pevalFPRoundingBinaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPRoundingBinaryOp -> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source # pevalFPFMATerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source # sbvFPTraitTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPTrait -> SBVType (FP eb sb) -> SBVType Bool Source # sbvFPUnaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPUnaryOp -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source # sbvFPBinaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPBinaryOp -> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source # sbvFPRoundingUnaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPRoundingUnaryOp -> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source # sbvFPRoundingBinaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPRoundingBinaryOp -> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source # sbvFPFMATerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source #
BitCast Int16 FP16 Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCast :: Int16 -> FP16 Source #
BitCast Int32 FP32 Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCast :: Int32 -> FP32 Source #
BitCast Int64 FP64 Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCast :: Int64 -> FP64 Source #
BitCast Word16 FP16 Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCast :: Word16 -> FP16 Source #
BitCast Word32 FP32 Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCast :: Word32 -> FP32 Source #
BitCast Word64 FP64 Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCast :: Word64 -> FP64 Source #
BitCast Double FP64 Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCast :: Double -> FP64 Source #
BitCast Float FP32 Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCast :: Float -> FP32 Source #
BitCastCanonical FP16 Int16 Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCastCanonicalValue :: proxy FP16 -> Int16 Source #
BitCastCanonical FP16 Word16 Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCastCanonicalValue :: proxy FP16 -> Word16 Source #
BitCastCanonical FP32 Int32 Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCastCanonicalValue :: proxy FP32 -> Int32 Source #
BitCastCanonical FP32 Word32 Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCastCanonicalValue :: proxy FP32 -> Word32 Source #
BitCastCanonical FP32 Float Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCastCanonicalValue :: proxy FP32 -> Float Source #
BitCastCanonical FP64 Int64 Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCastCanonicalValue :: proxy FP64 -> Int64 Source #
BitCastCanonical FP64 Word64 Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCastCanonicalValue :: proxy FP64 -> Word64 Source #
BitCastCanonical FP64 Double Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCastCanonicalValue :: proxy FP64 -> Double Source #
BitCastOr FP16 Int16 Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCastOr :: Int16 -> FP16 -> Int16 Source #
BitCastOr FP16 Word16 Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCastOr :: Word16 -> FP16 -> Word16 Source #
BitCastOr FP32 Int32 Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCastOr :: Int32 -> FP32 -> Int32 Source #
BitCastOr FP32 Word32 Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCastOr :: Word32 -> FP32 -> Word32 Source #
BitCastOr FP32 Float Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCastOr :: Float -> FP32 -> Float Source #
BitCastOr FP64 Int64 Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCastOr :: Int64 -> FP64 -> Int64 Source #
BitCastOr FP64 Word64 Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCastOr :: Word64 -> FP64 -> Word64 Source #
BitCastOr FP64 Double Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCastOr :: Double -> FP64 -> Double Source #
(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP16 Int16 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeBitCast Methods safeBitCast :: FP16 -> m Int16 Source #
(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP16 Word16 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeBitCast Methods safeBitCast :: FP16 -> m Word16 Source #
(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP32 Int32 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeBitCast Methods safeBitCast :: FP32 -> m Int32 Source #
(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP32 Word32 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeBitCast Methods safeBitCast :: FP32 -> m Word32 Source #
(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP32 Float m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeBitCast Methods safeBitCast :: FP32 -> m Float Source #
(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP64 Int64 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeBitCast Methods safeBitCast :: FP64 -> m Int64 Source #
(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP64 Word64 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeBitCast Methods safeBitCast :: FP64 -> m Word64 Source #
(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP64 Double m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeBitCast Methods safeBitCast :: FP64 -> m Double Source #
ValidFP eb sb => UnifiedFPImpl 'C FP eb sb (FP eb sb) FPRoundingMode Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedFP Associated Types type GetFP 'C = (f :: Nat -> Nat -> Type) Source # type GetFPRoundingMode 'C = (r :: Type) Source #
(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb) => UnifiedSafeFromFP mode NotRepresentableFPError AlgReal (FP eb sb) FPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP Methods withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError AlgReal (FP eb sb) FPRoundingMode m => r) -> r Source #
(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb) => UnifiedSafeFromFP mode NotRepresentableFPError Integer (FP eb sb) FPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP Methods withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError Integer (FP eb sb) FPRoundingMode m => r) -> r Source #
(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP mode NotRepresentableFPError (IntN n) (FP eb sb) FPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP Methods withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (IntN n) (FP eb sb) FPRoundingMode m => r) -> r Source #
(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP mode NotRepresentableFPError (WordN n) (FP eb sb) FPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP Methods withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (WordN n) (FP eb sb) FPRoundingMode m => r) -> r Source #
ValidFP eb sb => UnifiedFromIntegral 'C Integer (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'C) (Integral Integer, Num (FP eb sb)) (SymFromIntegral Integer (FP eb sb)) => r) -> r Source #
(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb) => SafeFromFP NotRepresentableFPError AlgReal (FP eb sb) FPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeFromFP Methods safeFromFP :: FPRoundingMode -> FP eb sb -> m AlgReal Source #
(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb) => SafeFromFP NotRepresentableFPError Integer (FP eb sb) FPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeFromFP Methods safeFromFP :: FPRoundingMode -> FP eb sb -> m Integer Source #
(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) => UnifiedSafeBitCast mode NotRepresentableFPError (FP eb sb) (IntN n) m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeBitCast Methods withBaseSafeBitCast :: (SafeBitCast NotRepresentableFPError (FP eb sb) (IntN n) m => r) -> r Source #
(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) => UnifiedSafeBitCast mode NotRepresentableFPError (FP eb sb) (WordN n) m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeBitCast Methods withBaseSafeBitCast :: (SafeBitCast NotRepresentableFPError (FP eb sb) (WordN n) m => r) -> r Source #
(KnownNat n', 1 <= n', ValidFP eb sb) => UnifiedFromIntegral 'C (IntN n') (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'C) (Integral (IntN n'), Num (FP eb sb)) (SymFromIntegral (IntN n') (FP eb sb)) => r) -> r Source #
(KnownNat n', 1 <= n', ValidFP eb sb) => UnifiedFromIntegral 'C (WordN n') (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'C) (Integral (WordN n'), Num (FP eb sb)) (SymFromIntegral (WordN n') (FP eb sb)) => r) -> r Source #
(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (IntN n) (FP eb sb) FPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeFromFP Methods safeFromFP :: FPRoundingMode -> FP eb sb -> m (IntN n) Source #
(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (WordN n) (FP eb sb) FPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeFromFP Methods safeFromFP :: FPRoundingMode -> FP eb sb -> m (WordN n) Source #
(DecideEvalMode mode, ValidFP a1 a2) => UnifiedSymEq mode (FP a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymEq Methods withBaseSymEq :: (If (IsConMode mode) (Eq (FP a1 a2)) (SymEq (FP a1 a2)) => r) -> r Source #
(DecideEvalMode mode, ValidFP a1 a2) => UnifiedSymOrd mode (FP a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymOrd Methods withBaseSymOrd :: (If (IsConMode mode) (Ord (FP a1 a2)) (SymOrd (FP a1 a2)) => r) -> r Source #
ValidFP eb sb => PEvalFromIntegralTerm Integer (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm Methods pevalFromIntegralTerm :: Term Integer -> Term (FP eb sb) Source # sbvFromIntegralTerm :: SBVType Integer -> SBVType (FP eb sb) Source #
ValidFP eb sb => Lift (FP eb sb :: Type) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods lift :: Quote m => FP eb sb -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => FP eb sb -> Code m (FP eb sb) #
ValidFP eb sb => IEEEFPConvertible AlgReal (FP eb sb) FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods fromFPOr :: AlgReal -> FPRoundingMode -> FP eb sb -> AlgReal Source # toFP :: FPRoundingMode -> AlgReal -> FP eb sb Source #
ValidFP eb sb => IEEEFPConvertible Integer (FP eb sb) FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods fromFPOr :: Integer -> FPRoundingMode -> FP eb sb -> Integer Source # toFP :: FPRoundingMode -> Integer -> FP eb sb Source #
ValidFP eb sb => IEEEFPToAlgReal AlgReal (FP eb sb) FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods fpToAlgReal :: AlgReal -> FP eb sb -> AlgReal Source #
(ValidFP eb sb, r ~ (eb + sb), KnownNat r, 1 <= r, TryMerge m, MonadError NotRepresentableFPError m) => SafeBitCast NotRepresentableFPError (FP eb sb) (IntN r) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeBitCast Methods safeBitCast :: FP eb sb -> m (IntN r) Source #
(ValidFP eb sb, r ~ (eb + sb), KnownNat r, 1 <= r, TryMerge m, MonadError NotRepresentableFPError m) => SafeBitCast NotRepresentableFPError (FP eb sb) (WordN r) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeBitCast Methods safeBitCast :: FP eb sb -> m (WordN r) Source #
ValidFP eb sb => UnifiedSolvable 'C (FP eb sb) (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSolvable Methods withBaseSolvable :: (If (IsConMode 'C) (FP eb sb ~ FP eb sb) (Solvable (FP eb sb) (FP eb sb)) => r) -> r Source #
ValidFP eb sb => UnifiedSolvable 'S (SymFP eb sb) (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSolvable Methods withBaseSolvable :: (If (IsConMode 'S) (SymFP eb sb ~ FP eb sb) (Solvable (FP eb sb) (SymFP eb sb)) => r) -> r Source #
(ValidFP eb sb, r ~ (eb + sb)) => BitCast (IntN r) (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCast :: IntN r -> FP eb sb Source #
(ValidFP eb sb, r ~ (eb + sb)) => BitCast (WordN r) (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCast :: WordN r -> FP eb sb Source #
(n ~ (eb + sb), ValidFP eb sb, KnownNat n, 1 <= n) => PEvalBitCastTerm (IntN n) (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm Methods pevalBitCastTerm :: Term (IntN n) -> Term (FP eb sb) Source # sbvBitCast :: SBVType (IntN n) -> SBVType (FP eb sb) Source #
(n ~ (eb + sb), ValidFP eb sb, KnownNat n, 1 <= n) => PEvalBitCastTerm (WordN n) (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm Methods pevalBitCastTerm :: Term (WordN n) -> Term (FP eb sb) Source # sbvBitCast :: SBVType (WordN n) -> SBVType (FP eb sb) Source #
(KnownNat n, 1 <= n, ValidFP eb sb) => PEvalFromIntegralTerm (IntN n) (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm Methods pevalFromIntegralTerm :: Term (IntN n) -> Term (FP eb sb) Source # sbvFromIntegralTerm :: SBVType (IntN n) -> SBVType (FP eb sb) Source #
(KnownNat n, 1 <= n, ValidFP eb sb) => PEvalFromIntegralTerm (WordN n) (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm Methods pevalFromIntegralTerm :: Term (WordN n) -> Term (FP eb sb) Source # sbvFromIntegralTerm :: SBVType (WordN n) -> SBVType (FP eb sb) Source #
(ValidFP eb sb, KnownNat n, 1 <= n) => IEEEFPConvertible (IntN n) (FP eb sb) FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods fromFPOr :: IntN n -> FPRoundingMode -> FP eb sb -> IntN n Source # toFP :: FPRoundingMode -> IntN n -> FP eb sb Source #
(ValidFP eb sb, KnownNat n, 1 <= n) => IEEEFPConvertible (WordN n) (FP eb sb) FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods fromFPOr :: WordN n -> FPRoundingMode -> FP eb sb -> WordN n Source # toFP :: FPRoundingMode -> WordN n -> FP eb sb Source #
ValidFloat eb sb => Arbitrary (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods arbitrary :: Gen (FP eb sb) # shrink :: FP eb sb -> [FP eb sb] #
ValidFloat eb sb => Floating (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods pi :: FP eb sb # exp :: FP eb sb -> FP eb sb # log :: FP eb sb -> FP eb sb # sqrt :: FP eb sb -> FP eb sb # (**) :: FP eb sb -> FP eb sb -> FP eb sb # logBase :: FP eb sb -> FP eb sb -> FP eb sb # sin :: FP eb sb -> FP eb sb # cos :: FP eb sb -> FP eb sb # tan :: FP eb sb -> FP eb sb # asin :: FP eb sb -> FP eb sb # acos :: FP eb sb -> FP eb sb # atan :: FP eb sb -> FP eb sb # sinh :: FP eb sb -> FP eb sb # cosh :: FP eb sb -> FP eb sb # tanh :: FP eb sb -> FP eb sb # asinh :: FP eb sb -> FP eb sb # acosh :: FP eb sb -> FP eb sb # atanh :: FP eb sb -> FP eb sb # log1p :: FP eb sb -> FP eb sb # expm1 :: FP eb sb -> FP eb sb # log1pexp :: FP eb sb -> FP eb sb # log1mexp :: FP eb sb -> FP eb sb #
ValidFloat eb sb => RealFloat (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods floatRadix :: FP eb sb -> Integer # floatDigits :: FP eb sb -> Int # floatRange :: FP eb sb -> (Int, Int) # decodeFloat :: FP eb sb -> (Integer, Int) # encodeFloat :: Integer -> Int -> FP eb sb # exponent :: FP eb sb -> Int # significand :: FP eb sb -> FP eb sb # scaleFloat :: Int -> FP eb sb -> FP eb sb # isNaN :: FP eb sb -> Bool # isInfinite :: FP eb sb -> Bool # isDenormalized :: FP eb sb -> Bool # isNegativeZero :: FP eb sb -> Bool # isIEEE :: FP eb sb -> Bool # atan2 :: FP eb sb -> FP eb sb -> FP eb sb #
ValidFloat eb sb => Num (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods (+) :: FP eb sb -> FP eb sb -> FP eb sb # (-) :: FP eb sb -> FP eb sb -> FP eb sb # (*) :: FP eb sb -> FP eb sb -> FP eb sb # negate :: FP eb sb -> FP eb sb # abs :: FP eb sb -> FP eb sb # signum :: FP eb sb -> FP eb sb # fromInteger :: Integer -> FP eb sb #
ValidFloat eb sb => Fractional (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods (/) :: FP eb sb -> FP eb sb -> FP eb sb # recip :: FP eb sb -> FP eb sb # fromRational :: Rational -> FP eb sb #
ValidFloat eb sb => Real (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods toRational :: FP eb sb -> Rational #
ValidFloat eb sb => RealFrac (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods properFraction :: Integral b => FP eb sb -> (b, FP eb sb) # truncate :: Integral b => FP eb sb -> b # round :: Integral b => FP eb sb -> b # ceiling :: Integral b => FP eb sb -> b # floor :: Integral b => FP eb sb -> b #
Show (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods showsPrec :: Int -> FP eb sb -> ShowS # show :: FP eb sb -> String # showList :: [FP eb sb] -> ShowS #
ValidFP eb sb => Binary (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods put :: FP eb sb -> Put # get :: Get (FP eb sb) # putList :: [FP eb sb] -> Put #
ValidFP eb sb => Serial (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods serialize :: MonadPut m => FP eb sb -> m () # deserialize :: MonadGet m => m (FP eb sb) #
ValidFP eb sb => Serialize (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods put :: Putter (FP eb sb) # get :: Get (FP eb sb) #
NFData (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods rnf :: FP eb sb -> () #
Eq (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods (==) :: FP eb sb -> FP eb sb -> Bool # (/=) :: FP eb sb -> FP eb sb -> Bool #
ValidFP eb sb => Ord (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods compare :: FP eb sb -> FP eb sb -> Ordering # (<) :: FP eb sb -> FP eb sb -> Bool # (<=) :: FP eb sb -> FP eb sb -> Bool # (>) :: FP eb sb -> FP eb sb -> Bool # (>=) :: FP eb sb -> FP eb sb -> Bool # max :: FP eb sb -> FP eb sb -> FP eb sb # min :: FP eb sb -> FP eb sb -> FP eb sb #
Apply (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Associated Types type FunType (FP eb sb) Source # Methods apply :: FP eb sb -> FunType (FP eb sb) Source #
ValidFP eb sb => IEEEFPConstants (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP 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 # fpMinNormalized :: FP eb sb Source # fpMinSubnormal :: FP eb sb Source # fpMaxNormalized :: FP eb sb Source # fpMaxSubnormal :: FP eb sb Source #
ValidFP eb sb => IEEEFPOp (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods fpAbs :: FP eb sb -> FP eb sb Source # fpNeg :: FP eb sb -> FP eb sb Source # fpRem :: FP eb sb -> FP eb sb -> FP eb sb Source # fpMinimum :: FP eb sb -> FP eb sb -> FP eb sb Source # fpMinimumNumber :: FP eb sb -> FP eb sb -> FP eb sb Source # fpMaximum :: FP eb sb -> FP eb sb -> FP eb sb Source # fpMaximumNumber :: FP eb sb -> FP eb sb -> FP eb sb Source #
ValidFP eb sb => SymIEEEFPTraits (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymIEEEFP 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 fb => EvalSym (FP eb fb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> FP eb fb -> FP eb fb Source #
ValidFP eb sb => ExtractSym (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ExtractSym Methods extractSym :: FP eb sb -> AnySymbolSet Source # extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => FP eb sb -> Maybe (SymbolSet knd) Source #
ValidFP eb sb => Mergeable (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy (FP eb sb) Source # sortIndices :: FP eb sb -> [DynamicSortedIdx] Source #
ValidFP eb sb => PPrint (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.PPrint Methods pformat :: FP eb sb -> Doc ann Source # pformatPrec :: Int -> FP eb sb -> Doc ann Source # pformatList :: [FP eb sb] -> Doc ann Source #
ValidFP eb sb => SubstSym (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb0 (knd :: SymbolKind). (LinkedRep cb sb0, IsSymbolKind knd) => TypedSymbol knd cb -> sb0 -> FP eb sb -> FP eb sb Source #
ValidFP eb sb => SymEq (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: FP eb sb -> FP eb sb -> SymBool Source # (./=) :: FP eb sb -> FP eb sb -> SymBool Source # symDistinct :: [FP eb sb] -> SymBool Source #
ValidFP eb sb => SymOrd (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd Methods (.<) :: FP eb sb -> FP eb sb -> SymBool Source # (.<=) :: FP eb sb -> FP eb sb -> SymBool Source # (.>) :: FP eb sb -> FP eb sb -> SymBool Source # (.>=) :: FP eb sb -> FP eb sb -> SymBool Source # symCompare :: FP eb sb -> FP eb sb -> Union Ordering Source #
ValidFP eb sb => AllSyms (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: FP eb sb -> [SomeSym] -> [SomeSym] Source # allSyms :: FP eb sb -> [SomeSym] Source #
ValidFP eb sb => NonFuncSBVRep (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Associated Types type NonFuncSBVBaseType (FP eb sb) Source #
ValidFP eb sb => PEvalFloatingTerm (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFloatingTerm Methods pevalFloatingUnaryTerm :: FloatingUnaryOp -> Term (FP eb sb) -> Term (FP eb sb) Source # pevalPowerTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source # withSbvFloatingTermConstraint :: (Floating (SBVType (FP eb sb)) => r) -> r Source # sbvPowerTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source # sbvFloatingUnaryTerm :: FloatingUnaryOp -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source #
ValidFP eb sb => PEvalFractionalTerm (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFractionalTerm Methods pevalFdivTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source # pevalRecipTerm :: Term (FP eb sb) -> Term (FP eb sb) Source # withSbvFractionalTermConstraint :: (Fractional (SBVType (FP eb sb)) => r) -> r Source # sbvFdivTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source # sbvRecipTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) Source #
ValidFP eb sb => PEvalIEEEFPConvertibleTerm (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalIEEEFPConvertibleTerm Methods pevalFromFPOrTerm :: forall (eb0 :: Nat) (sb0 :: Nat). ValidFP eb0 sb0 => Term (FP eb sb) -> Term FPRoundingMode -> Term (FP eb0 sb0) -> Term (FP eb sb) Source # pevalToFPTerm :: forall (eb0 :: Nat) (sb0 :: Nat). ValidFP eb0 sb0 => Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb0 sb0) Source # sbvFromFPOrTerm :: forall (eb0 :: Nat) (sb0 :: Nat). ValidFP eb0 sb0 => SBVType (FP eb sb) -> SBVType FPRoundingMode -> SBVType (FP eb0 sb0) -> SBVType (FP eb sb) Source # sbvToFPTerm :: forall (eb0 :: Nat) (sb0 :: Nat). ValidFP eb0 sb0 => SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType (FP eb0 sb0) Source #
ValidFP eb sb => PEvalNumTerm (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm Methods pevalAddNumTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source # pevalNegNumTerm :: Term (FP eb sb) -> Term (FP eb sb) Source # pevalMulNumTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source # pevalAbsNumTerm :: Term (FP eb sb) -> Term (FP eb sb) Source # pevalSignumNumTerm :: Term (FP eb sb) -> Term (FP eb sb) Source # withSbvNumTermConstraint :: (Num (SBVType (FP eb sb)) => r) -> r Source # sbvAddNumTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source # sbvNegNumTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) Source # sbvMulNumTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source # sbvAbsNumTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) Source # sbvSignumNumTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) Source #
ValidFP eb sb => PEvalOrdTerm (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm Methods pevalLtOrdTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term Bool Source # pevalLeOrdTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term Bool Source # withSbvOrdTermConstraint :: (OrdSymbolic (SBVType (FP eb sb)) => r) -> r Source # sbvLtOrdTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBV Bool Source # sbvLeOrdTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBV Bool Source #
ValidFP eb sb => SBVRep (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Associated Types type SBVType (FP eb sb) Source #
ValidFP eb sb => SupportedNonFuncPrim (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods conNonFuncSBVTerm :: FP eb sb -> SBV (NonFuncSBVBaseType (FP eb sb)) Source # symNonFuncSBVTerm :: SBVFreshMonad m => String -> m (SBV (NonFuncSBVBaseType (FP eb sb))) Source # withNonFuncPrim :: (NonFuncPrimConstraint (FP eb sb) => r) -> r Source #
ValidFP eb sb => SupportedPrim (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods primTypeRep :: TypeRep (FP eb sb) Source # sameCon :: FP eb sb -> FP eb sb -> Bool Source # hashConWithSalt :: Int -> FP eb sb -> Int Source # pformatCon :: FP eb sb -> String Source # defaultValue :: FP eb sb Source # pevalITETerm :: Term Bool -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source # pevalEqTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term Bool Source # pevalDistinctTerm :: NonEmpty (Term (FP eb sb)) -> Term Bool Source # conSBVTerm :: FP eb sb -> SBVType (FP eb sb) Source # symSBVName :: TypedSymbol 'AnyKind (FP eb sb) -> Int -> String Source # symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (FP eb sb)) Source # withPrim :: ((PrimConstraint (FP eb sb), SMTDefinable (SBVType (FP eb sb)), Mergeable (SBVType (FP eb sb)), Typeable (SBVType (FP eb sb))) => a) -> a Source # sbvIte :: SBV Bool -> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source # sbvEq :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBV Bool Source # sbvDistinct :: NonEmpty (SBVType (FP eb sb)) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> FP eb sb Source # castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (FP eb sb) -> Maybe (TypedSymbol knd' (FP eb sb)) Source # funcDummyConstraint :: SBVType (FP eb sb) -> SBV Bool Source #
ValidFP eb sb => SupportedPrimConstraint (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Associated Types type PrimConstraint (FP eb sb) Source #
ValidFP eb sb => SymRep (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Associated Types type SymType (FP eb sb) Source #
ValidFP eb sb => UnifiedConRep (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedRep Associated Types type ConType (FP eb sb) Source #
ValidFP eb sb => UnifiedSymRep (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedRep Associated Types type SymType (FP eb sb) Source #
ValidFP eb sb => Hashable (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods hashWithSalt :: Int -> FP eb sb -> Int # hash :: FP eb sb -> Int #
ValidFP eb sb => IEEEFPRoundingOp (FP eb sb) FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods fpAdd :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb Source # fpSub :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb Source # fpMul :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb Source # fpDiv :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb Source # fpFMA :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb -> FP eb sb Source # fpSqrt :: FPRoundingMode -> FP eb sb -> FP eb sb Source # fpRoundToIntegral :: FPRoundingMode -> FP eb sb -> FP eb sb Source #
(ValidFP eb sb, n ~ (eb + sb)) => BitCastCanonical (FP eb sb) (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCastCanonicalValue :: proxy (FP eb sb) -> IntN n Source #
(ValidFP eb sb, n ~ (eb + sb)) => BitCastCanonical (FP eb sb) (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCastCanonicalValue :: proxy (FP eb sb) -> WordN n Source #
(ValidFP eb sb, n ~ (eb + sb)) => BitCastOr (FP eb sb) (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCastOr :: IntN n -> FP eb sb -> IntN n Source #
(ValidFP eb sb, r ~ (eb + sb)) => BitCastOr (FP eb sb) (WordN r) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods bitCastOr :: WordN r -> FP eb sb -> WordN r Source #
(n ~ (eb + sb), ValidFP eb sb, KnownNat n, 1 <= n) => PEvalBitCastOrTerm (FP eb sb) (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm Methods pevalBitCastOrTerm :: Term (IntN n) -> Term (FP eb sb) -> Term (IntN n) Source # sbvBitCastOr :: SBVType (IntN n) -> SBVType (FP eb sb) -> SBVType (IntN n) Source #
(n ~ (eb + sb), ValidFP eb sb, KnownNat n, 1 <= n) => PEvalBitCastOrTerm (FP eb sb) (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm Methods pevalBitCastOrTerm :: Term (WordN n) -> Term (FP eb sb) -> Term (WordN n) Source # sbvBitCastOr :: SBVType (WordN n) -> SBVType (FP eb sb) -> SBVType (WordN n) Source #
ValidFP eb sb => GenSym (FP eb sb) (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => FP eb sb -> m (Union (FP eb sb)) Source #
ValidFP eb sb => GenSymSimple (FP eb sb) (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods simpleFresh :: MonadFresh m => FP eb sb -> m (FP eb sb) Source #
ValidFP eb sb => Solvable (FP eb sb) (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods con :: FP eb sb -> SymFP eb sb Source # conView :: SymFP eb sb -> Maybe (FP eb sb) Source # sym :: Symbol -> SymFP eb sb Source # ssym :: Identifier -> SymFP eb sb Source # isym :: Identifier -> Int -> SymFP eb sb Source #
ValidFP eb sb => ToCon (FP eb sb) (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: FP eb sb -> Maybe (FP eb sb) Source #
ValidFP eb sb => ToCon (SymFP eb sb) (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: SymFP eb sb -> Maybe (FP eb sb) Source #
ValidFP eb sb => ToSym (FP eb sb) (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: FP eb sb -> FP eb sb Source #
ValidFP eb sb => ToSym (FP eb sb) (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: FP eb sb -> SymFP eb sb Source #
ValidFP eb sb => LinkedRep (FP eb sb) (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods underlyingTerm :: SymFP eb sb -> Term (FP eb sb) Source # wrapTerm :: Term (FP eb sb) -> SymFP eb sb Source #
(ValidFP eb sb, ValidFP eb' sb') => IEEEFPConvertible (FP eb' sb') (FP eb sb) FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods fromFPOr :: FP eb' sb' -> FPRoundingMode -> FP eb sb -> FP eb' sb' Source # toFP :: FPRoundingMode -> FP eb' sb' -> FP eb sb Source #
type FunType (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.FP type FunType (FP eb sb) = FP eb sb
type NonFuncSBVBaseType (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term type NonFuncSBVBaseType (FP eb sb) = FloatingPoint eb sb
type PrimConstraint (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term type PrimConstraint (FP eb sb) = ValidFP eb sb
type SBVType (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term type SBVType (FP eb sb) = SBV (FloatingPoint eb sb)
type SymType (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP type SymType (FP eb sb) = SymFP eb sb
type ConType (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedRep type ConType (FP eb sb) = FP eb sb
type SymType (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedRep type SymType (FP eb sb) = SymFP eb sb

type FP16 = FP 5 11 Source #

IEEE 754 half-precision floating-point number.

type FP32 = FP 8 24 Source #

IEEE 754 single-precision floating-point number.

type FP64 = FP 11 53 Source #

IEEE 754 double-precision floating-point number.

withValidFPProofs :: forall eb sb r. ValidFP eb sb => ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb), 1 <= eb, 1 <= sb) => r) -> r Source #

Some type-level witnesses that could be derived from ValidFP.

data FPRoundingMode Source #

Rounding mode for floating-point operations.

Constructors

RNE	Round to nearest, ties to even.
RNA	Round to nearest, ties to away from zero.
RTP	Round towards positive infinity.
RTN	Round towards negative infinity.
RTZ	Round towards zero.

Instances

Instances details

Arbitrary FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods arbitrary :: Gen FPRoundingMode # shrink :: FPRoundingMode -> [FPRoundingMode] #
Generic FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Associated Types type Rep FPRoundingMode :: Type -> Type # Methods from :: FPRoundingMode -> Rep FPRoundingMode x # to :: Rep FPRoundingMode x -> FPRoundingMode #
Show FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods showsPrec :: Int -> FPRoundingMode -> ShowS # show :: FPRoundingMode -> String # showList :: [FPRoundingMode] -> ShowS #
Serial FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods serialize :: MonadPut m => FPRoundingMode -> m () # deserialize :: MonadGet m => m FPRoundingMode #
NFData FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods rnf :: FPRoundingMode -> () #
Eq FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods (==) :: FPRoundingMode -> FPRoundingMode -> Bool # (/=) :: FPRoundingMode -> FPRoundingMode -> Bool #
Ord FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods compare :: FPRoundingMode -> FPRoundingMode -> Ordering # (<) :: FPRoundingMode -> FPRoundingMode -> Bool # (<=) :: FPRoundingMode -> FPRoundingMode -> Bool # (>) :: FPRoundingMode -> FPRoundingMode -> Bool # (>=) :: FPRoundingMode -> FPRoundingMode -> Bool # max :: FPRoundingMode -> FPRoundingMode -> FPRoundingMode # min :: FPRoundingMode -> FPRoundingMode -> FPRoundingMode #
Apply FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Associated Types type FunType FPRoundingMode Source # Methods apply :: FPRoundingMode -> FunType FPRoundingMode Source #
IEEEFPRoundingMode FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods rne :: FPRoundingMode Source # rna :: FPRoundingMode Source # rtp :: FPRoundingMode Source # rtn :: FPRoundingMode Source # rtz :: FPRoundingMode Source #
EvalSym FPRoundingMode Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> FPRoundingMode -> FPRoundingMode Source #
ExtractSym FPRoundingMode Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ExtractSym Methods extractSym :: FPRoundingMode -> AnySymbolSet Source # extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => FPRoundingMode -> Maybe (SymbolSet knd) Source #
Mergeable FPRoundingMode Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy FPRoundingMode Source # sortIndices :: FPRoundingMode -> [DynamicSortedIdx] Source #
PPrint FPRoundingMode Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.PPrint Methods pformat :: FPRoundingMode -> Doc ann Source # pformatPrec :: Int -> FPRoundingMode -> Doc ann Source # pformatList :: [FPRoundingMode] -> Doc ann Source #
SubstSym FPRoundingMode Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> FPRoundingMode -> FPRoundingMode Source #
SymEq FPRoundingMode Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: FPRoundingMode -> FPRoundingMode -> SymBool Source # (./=) :: FPRoundingMode -> FPRoundingMode -> SymBool Source # symDistinct :: [FPRoundingMode] -> SymBool Source #
SymOrd FPRoundingMode Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd Methods (.<) :: FPRoundingMode -> FPRoundingMode -> SymBool Source # (.<=) :: FPRoundingMode -> FPRoundingMode -> SymBool Source # (.>) :: FPRoundingMode -> FPRoundingMode -> SymBool Source # (.>=) :: FPRoundingMode -> FPRoundingMode -> SymBool Source # symCompare :: FPRoundingMode -> FPRoundingMode -> Union Ordering Source #
AllSyms FPRoundingMode Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: FPRoundingMode -> [SomeSym] -> [SomeSym] Source # allSyms :: FPRoundingMode -> [SomeSym] Source #
NonFuncSBVRep FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Associated Types type NonFuncSBVBaseType FPRoundingMode Source #
PEvalOrdTerm FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm Methods pevalLtOrdTerm :: Term FPRoundingMode -> Term FPRoundingMode -> Term Bool Source # pevalLeOrdTerm :: Term FPRoundingMode -> Term FPRoundingMode -> Term Bool Source # withSbvOrdTermConstraint :: (OrdSymbolic (SBVType FPRoundingMode) => r) -> r Source # sbvLtOrdTerm :: SBVType FPRoundingMode -> SBVType FPRoundingMode -> SBV Bool Source # sbvLeOrdTerm :: SBVType FPRoundingMode -> SBVType FPRoundingMode -> SBV Bool Source #
SBVRep FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Associated Types type SBVType FPRoundingMode Source #
SupportedNonFuncPrim FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods conNonFuncSBVTerm :: FPRoundingMode -> SBV (NonFuncSBVBaseType FPRoundingMode) Source # symNonFuncSBVTerm :: SBVFreshMonad m => String -> m (SBV (NonFuncSBVBaseType FPRoundingMode)) Source # withNonFuncPrim :: (NonFuncPrimConstraint FPRoundingMode => r) -> r Source #
SupportedPrim FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods primTypeRep :: TypeRep FPRoundingMode Source # sameCon :: FPRoundingMode -> FPRoundingMode -> Bool Source # hashConWithSalt :: Int -> FPRoundingMode -> Int Source # pformatCon :: FPRoundingMode -> String Source # defaultValue :: FPRoundingMode Source # pevalITETerm :: Term Bool -> Term FPRoundingMode -> Term FPRoundingMode -> Term FPRoundingMode Source # pevalEqTerm :: Term FPRoundingMode -> Term FPRoundingMode -> Term Bool Source # pevalDistinctTerm :: NonEmpty (Term FPRoundingMode) -> Term Bool Source # conSBVTerm :: FPRoundingMode -> SBVType FPRoundingMode Source # symSBVName :: TypedSymbol 'AnyKind FPRoundingMode -> Int -> String Source # symSBVTerm :: SBVFreshMonad m => String -> m (SBVType FPRoundingMode) Source # withPrim :: ((PrimConstraint FPRoundingMode, SMTDefinable (SBVType FPRoundingMode), Mergeable (SBVType FPRoundingMode), Typeable (SBVType FPRoundingMode)) => a) -> a Source # sbvIte :: SBV Bool -> SBVType FPRoundingMode -> SBVType FPRoundingMode -> SBVType FPRoundingMode Source # sbvEq :: SBVType FPRoundingMode -> SBVType FPRoundingMode -> SBV Bool Source # sbvDistinct :: NonEmpty (SBVType FPRoundingMode) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> FPRoundingMode Source # castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd FPRoundingMode -> Maybe (TypedSymbol knd' FPRoundingMode) Source # funcDummyConstraint :: SBVType FPRoundingMode -> SBV Bool Source #
SupportedPrimConstraint FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Associated Types type PrimConstraint FPRoundingMode Source #
SymRep FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Associated Types type SymType FPRoundingMode Source #
Hashable FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods hashWithSalt :: Int -> FPRoundingMode -> Int # hash :: FPRoundingMode -> Int #
GenSym FPRoundingMode FPRoundingMode Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => FPRoundingMode -> m (Union FPRoundingMode) Source #
GenSymSimple FPRoundingMode FPRoundingMode Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods simpleFresh :: MonadFresh m => FPRoundingMode -> m FPRoundingMode Source #
Solvable FPRoundingMode SymFPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods con :: FPRoundingMode -> SymFPRoundingMode Source # conView :: SymFPRoundingMode -> Maybe FPRoundingMode Source # sym :: Symbol -> SymFPRoundingMode Source # ssym :: Identifier -> SymFPRoundingMode Source # isym :: Identifier -> Int -> SymFPRoundingMode Source #
ToCon FPRoundingMode FPRoundingMode Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: FPRoundingMode -> Maybe FPRoundingMode Source #
ToCon SymFPRoundingMode FPRoundingMode Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: SymFPRoundingMode -> Maybe FPRoundingMode Source #
ToSym FPRoundingMode FPRoundingMode Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: FPRoundingMode -> FPRoundingMode Source #
ToSym FPRoundingMode SymFPRoundingMode Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: FPRoundingMode -> SymFPRoundingMode Source #
DecideEvalMode mode => UnifiedSymEq mode FPRoundingMode Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymEq Methods withBaseSymEq :: (If (IsConMode mode) (Eq FPRoundingMode) (SymEq FPRoundingMode) => r) -> r Source #
DecideEvalMode mode => UnifiedSymOrd mode FPRoundingMode Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymOrd Methods withBaseSymOrd :: (If (IsConMode mode) (Ord FPRoundingMode) (SymOrd FPRoundingMode) => r) -> r Source #
LinkedRep FPRoundingMode SymFPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods underlyingTerm :: SymFPRoundingMode -> Term FPRoundingMode Source # wrapTerm :: Term FPRoundingMode -> SymFPRoundingMode Source #
Lift FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods lift :: Quote m => FPRoundingMode -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => FPRoundingMode -> Code m FPRoundingMode #
ValidFP eb sb => UnifiedFPImpl 'C FP eb sb (FP eb sb) FPRoundingMode Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedFP Associated Types type GetFP 'C = (f :: Nat -> Nat -> Type) Source # type GetFPRoundingMode 'C = (r :: Type) Source #
(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb) => UnifiedSafeFromFP mode NotRepresentableFPError AlgReal (FP eb sb) FPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP Methods withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError AlgReal (FP eb sb) FPRoundingMode m => r) -> r Source #
(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb) => UnifiedSafeFromFP mode NotRepresentableFPError Integer (FP eb sb) FPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP Methods withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError Integer (FP eb sb) FPRoundingMode m => r) -> r Source #
(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP mode NotRepresentableFPError (IntN n) (FP eb sb) FPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP Methods withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (IntN n) (FP eb sb) FPRoundingMode m => r) -> r Source #
(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP mode NotRepresentableFPError (WordN n) (FP eb sb) FPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP Methods withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (WordN n) (FP eb sb) FPRoundingMode m => r) -> r Source #
(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb) => SafeFromFP NotRepresentableFPError AlgReal (FP eb sb) FPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeFromFP Methods safeFromFP :: FPRoundingMode -> FP eb sb -> m AlgReal Source #
(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb) => SafeFromFP NotRepresentableFPError Integer (FP eb sb) FPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeFromFP Methods safeFromFP :: FPRoundingMode -> FP eb sb -> m Integer Source #
(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (IntN n) (FP eb sb) FPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeFromFP Methods safeFromFP :: FPRoundingMode -> FP eb sb -> m (IntN n) Source #
(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (WordN n) (FP eb sb) FPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeFromFP Methods safeFromFP :: FPRoundingMode -> FP eb sb -> m (WordN n) Source #
ValidFP eb sb => IEEEFPConvertible AlgReal (FP eb sb) FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods fromFPOr :: AlgReal -> FPRoundingMode -> FP eb sb -> AlgReal Source # toFP :: FPRoundingMode -> AlgReal -> FP eb sb Source #
ValidFP eb sb => IEEEFPConvertible Integer (FP eb sb) FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods fromFPOr :: Integer -> FPRoundingMode -> FP eb sb -> Integer Source # toFP :: FPRoundingMode -> Integer -> FP eb sb Source #
ValidFP eb sb => IEEEFPToAlgReal AlgReal (FP eb sb) FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods fpToAlgReal :: AlgReal -> FP eb sb -> AlgReal Source #
(ValidFP eb sb, KnownNat n, 1 <= n) => IEEEFPConvertible (IntN n) (FP eb sb) FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods fromFPOr :: IntN n -> FPRoundingMode -> FP eb sb -> IntN n Source # toFP :: FPRoundingMode -> IntN n -> FP eb sb Source #
(ValidFP eb sb, KnownNat n, 1 <= n) => IEEEFPConvertible (WordN n) (FP eb sb) FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods fromFPOr :: WordN n -> FPRoundingMode -> FP eb sb -> WordN n Source # toFP :: FPRoundingMode -> WordN n -> FP eb sb Source #
ValidFP eb sb => IEEEFPRoundingOp (FP eb sb) FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods fpAdd :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb Source # fpSub :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb Source # fpMul :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb Source # fpDiv :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb Source # fpFMA :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb -> FP eb sb Source # fpSqrt :: FPRoundingMode -> FP eb sb -> FP eb sb Source # fpRoundToIntegral :: FPRoundingMode -> FP eb sb -> FP eb sb Source #
(ValidFP eb sb, ValidFP eb' sb') => IEEEFPConvertible (FP eb' sb') (FP eb sb) FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods fromFPOr :: FP eb' sb' -> FPRoundingMode -> FP eb sb -> FP eb' sb' Source # toFP :: FPRoundingMode -> FP eb' sb' -> FP eb sb Source #
type Rep FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP type Rep FPRoundingMode = D1 ('MetaData "FPRoundingMode" "Grisette.Internal.SymPrim.FP" "grisette-0.12.0.0-2YnemY67TX446CMac8R8vR" '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))))
type FunType FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.FP type FunType FPRoundingMode = FPRoundingMode
type NonFuncSBVBaseType FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term type NonFuncSBVBaseType FPRoundingMode = RoundingMode
type PrimConstraint FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term type PrimConstraint FPRoundingMode = ()
type SBVType FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term type SBVType FPRoundingMode = SBV RoundingMode
type SymType FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP type SymType FPRoundingMode = SymFPRoundingMode

allFPRoundingMode :: [FPRoundingMode] Source #

All IEEE 754 rounding modes.

data NotRepresentableFPError Source #

An error thrown when bitcasting or converting FP NaN to other types.

Constructors

NaNError
FPUnderflowError
FPOverflowError

Instances

Instances details

Exception NotRepresentableFPError Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods toException :: NotRepresentableFPError -> SomeException # fromException :: SomeException -> Maybe NotRepresentableFPError # displayException :: NotRepresentableFPError -> String #
Generic NotRepresentableFPError Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Associated Types type Rep NotRepresentableFPError :: Type -> Type # Methods from :: NotRepresentableFPError -> Rep NotRepresentableFPError x # to :: Rep NotRepresentableFPError x -> NotRepresentableFPError #
Show NotRepresentableFPError Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods showsPrec :: Int -> NotRepresentableFPError -> ShowS # show :: NotRepresentableFPError -> String # showList :: [NotRepresentableFPError] -> ShowS #
Eq NotRepresentableFPError Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods (==) :: NotRepresentableFPError -> NotRepresentableFPError -> Bool # (/=) :: NotRepresentableFPError -> NotRepresentableFPError -> Bool #
Ord NotRepresentableFPError Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods compare :: NotRepresentableFPError -> NotRepresentableFPError -> Ordering # (<) :: NotRepresentableFPError -> NotRepresentableFPError -> Bool # (<=) :: NotRepresentableFPError -> NotRepresentableFPError -> Bool # (>) :: NotRepresentableFPError -> NotRepresentableFPError -> Bool # (>=) :: NotRepresentableFPError -> NotRepresentableFPError -> Bool # max :: NotRepresentableFPError -> NotRepresentableFPError -> NotRepresentableFPError # min :: NotRepresentableFPError -> NotRepresentableFPError -> NotRepresentableFPError #
EvalSym NotRepresentableFPError Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> NotRepresentableFPError -> NotRepresentableFPError Source #
ExtractSym NotRepresentableFPError Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ExtractSym Methods extractSym :: NotRepresentableFPError -> AnySymbolSet Source # extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => NotRepresentableFPError -> Maybe (SymbolSet knd) Source #
Mergeable NotRepresentableFPError Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy NotRepresentableFPError Source # sortIndices :: NotRepresentableFPError -> [DynamicSortedIdx] Source #
PPrint NotRepresentableFPError Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.PPrint Methods pformat :: NotRepresentableFPError -> Doc ann Source # pformatPrec :: Int -> NotRepresentableFPError -> Doc ann Source # pformatList :: [NotRepresentableFPError] -> Doc ann Source #
SubstSym NotRepresentableFPError Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> NotRepresentableFPError -> NotRepresentableFPError Source #
SymEq NotRepresentableFPError Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: NotRepresentableFPError -> NotRepresentableFPError -> SymBool Source # (./=) :: NotRepresentableFPError -> NotRepresentableFPError -> SymBool Source # symDistinct :: [NotRepresentableFPError] -> SymBool Source #
SymOrd NotRepresentableFPError Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd Methods (.<) :: NotRepresentableFPError -> NotRepresentableFPError -> SymBool Source # (.<=) :: NotRepresentableFPError -> NotRepresentableFPError -> SymBool Source # (.>) :: NotRepresentableFPError -> NotRepresentableFPError -> SymBool Source # (.>=) :: NotRepresentableFPError -> NotRepresentableFPError -> SymBool Source # symCompare :: NotRepresentableFPError -> NotRepresentableFPError -> Union Ordering Source #
ToCon NotRepresentableFPError NotRepresentableFPError Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: NotRepresentableFPError -> Maybe NotRepresentableFPError Source #
ToSym NotRepresentableFPError NotRepresentableFPError Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: NotRepresentableFPError -> NotRepresentableFPError Source #
(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP16 Int16 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeBitCast Methods safeBitCast :: FP16 -> m Int16 Source #
(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP16 Word16 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeBitCast Methods safeBitCast :: FP16 -> m Word16 Source #
(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP32 Int32 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeBitCast Methods safeBitCast :: FP32 -> m Int32 Source #
(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP32 Word32 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeBitCast Methods safeBitCast :: FP32 -> m Word32 Source #
(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP32 Float m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeBitCast Methods safeBitCast :: FP32 -> m Float Source #
(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP64 Int64 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeBitCast Methods safeBitCast :: FP64 -> m Int64 Source #
(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP64 Word64 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeBitCast Methods safeBitCast :: FP64 -> m Word64 Source #
(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP64 Double m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeBitCast Methods safeBitCast :: FP64 -> m Double Source #
(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb) => UnifiedSafeFromFP 'S NotRepresentableFPError SymAlgReal (SymFP eb sb) SymFPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP Methods withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError SymAlgReal (SymFP eb sb) SymFPRoundingMode m => r) -> r Source #
(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb) => UnifiedSafeFromFP 'S NotRepresentableFPError SymInteger (SymFP eb sb) SymFPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP Methods withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError SymInteger (SymFP eb sb) SymFPRoundingMode m => r) -> r Source #
(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb) => UnifiedSafeFromFP mode NotRepresentableFPError AlgReal (FP eb sb) FPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP Methods withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError AlgReal (FP eb sb) FPRoundingMode m => r) -> r Source #
(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb) => UnifiedSafeFromFP mode NotRepresentableFPError Integer (FP eb sb) FPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP Methods withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError Integer (FP eb sb) FPRoundingMode m => r) -> r Source #
(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP 'S NotRepresentableFPError (SymIntN n) (SymFP eb sb) SymFPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP Methods withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (SymIntN n) (SymFP eb sb) SymFPRoundingMode m => r) -> r Source #
(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP 'S NotRepresentableFPError (SymWordN n) (SymFP eb sb) SymFPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP Methods withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (SymWordN n) (SymFP eb sb) SymFPRoundingMode m => r) -> r Source #
(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP mode NotRepresentableFPError (IntN n) (FP eb sb) FPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP Methods withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (IntN n) (FP eb sb) FPRoundingMode m => r) -> r Source #
(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP mode NotRepresentableFPError (WordN n) (FP eb sb) FPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP Methods withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (WordN n) (FP eb sb) FPRoundingMode m => r) -> r Source #
(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb) => SafeFromFP NotRepresentableFPError AlgReal (FP eb sb) FPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeFromFP Methods safeFromFP :: FPRoundingMode -> FP eb sb -> m AlgReal Source #
(MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb) => SafeFromFP NotRepresentableFPError SymAlgReal (SymFP eb sb) SymFPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeFromFP Methods safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m SymAlgReal Source #
(MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb) => SafeFromFP NotRepresentableFPError SymInteger (SymFP eb sb) SymFPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeFromFP Methods safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m SymInteger Source #
(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb) => SafeFromFP NotRepresentableFPError Integer (FP eb sb) FPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeFromFP Methods safeFromFP :: FPRoundingMode -> FP eb sb -> m Integer Source #
(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) => UnifiedSafeBitCast 'S NotRepresentableFPError (SymFP eb sb) (SymIntN n) m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeBitCast Methods withBaseSafeBitCast :: (SafeBitCast NotRepresentableFPError (SymFP eb sb) (SymIntN n) m => r) -> r Source #
(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) => UnifiedSafeBitCast 'S NotRepresentableFPError (SymFP eb sb) (SymWordN n) m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeBitCast Methods withBaseSafeBitCast :: (SafeBitCast NotRepresentableFPError (SymFP eb sb) (SymWordN n) m => r) -> r Source #
(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) => UnifiedSafeBitCast mode NotRepresentableFPError (FP eb sb) (IntN n) m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeBitCast Methods withBaseSafeBitCast :: (SafeBitCast NotRepresentableFPError (FP eb sb) (IntN n) m => r) -> r Source #
(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) => UnifiedSafeBitCast mode NotRepresentableFPError (FP eb sb) (WordN n) m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeBitCast Methods withBaseSafeBitCast :: (SafeBitCast NotRepresentableFPError (FP eb sb) (WordN n) m => r) -> r Source #
ToSym NotRepresentableFPError (Union NotRepresentableFPError) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: NotRepresentableFPError -> Union NotRepresentableFPError Source #
(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (IntN n) (FP eb sb) FPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeFromFP Methods safeFromFP :: FPRoundingMode -> FP eb sb -> m (IntN n) Source #
(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (WordN n) (FP eb sb) FPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeFromFP Methods safeFromFP :: FPRoundingMode -> FP eb sb -> m (WordN n) Source #
(MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (SymIntN n) (SymFP eb sb) SymFPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeFromFP Methods safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m (SymIntN n) Source #
(MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (SymWordN n) (SymFP eb sb) SymFPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeFromFP Methods safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m (SymWordN n) Source #
(ValidFP eb sb, r ~ (eb + sb), KnownNat r, 1 <= r, TryMerge m, MonadError NotRepresentableFPError m) => SafeBitCast NotRepresentableFPError (FP eb sb) (IntN r) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeBitCast Methods safeBitCast :: FP eb sb -> m (IntN r) Source #
(ValidFP eb sb, r ~ (eb + sb), KnownNat r, 1 <= r, TryMerge m, MonadError NotRepresentableFPError m) => SafeBitCast NotRepresentableFPError (FP eb sb) (WordN r) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeBitCast Methods safeBitCast :: FP eb sb -> m (WordN r) Source #
(ValidFP eb sb, r ~ (eb + sb), KnownNat r, 1 <= r, MonadUnion m, MonadError NotRepresentableFPError m) => SafeBitCast NotRepresentableFPError (SymFP eb sb) (SymIntN r) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeBitCast Methods safeBitCast :: SymFP eb sb -> m (SymIntN r) Source #
(ValidFP eb sb, r ~ (eb + sb), KnownNat r, 1 <= r, MonadUnion m, MonadError NotRepresentableFPError m) => SafeBitCast NotRepresentableFPError (SymFP eb sb) (SymWordN r) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeBitCast Methods safeBitCast :: SymFP eb sb -> m (SymWordN r) Source #
ToCon (Union NotRepresentableFPError) NotRepresentableFPError Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: Union NotRepresentableFPError -> Maybe NotRepresentableFPError Source #
type Rep NotRepresentableFPError Source #
Instance details Defined in Grisette.Internal.SymPrim.FP type Rep NotRepresentableFPError = D1 ('MetaData "NotRepresentableFPError" "Grisette.Internal.SymPrim.FP" "grisette-0.12.0.0-2YnemY67TX446CMac8R8vR" 'False) (C1 ('MetaCons "NaNError" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FPUnderflowError" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPOverflowError" 'PrefixI 'False) (U1 :: Type -> Type)))

class ConvertibleBound bv where Source #

Bounds for converting bit vectors to floating-point numbers. Out-of-range FP values cannot be converted to a representable bit-vector.

Methods

convertibleLowerBound :: forall eb sb n. (ValidFP eb sb, KnownNat n, 1 <= n) => bv n -> FPRoundingMode -> FP eb sb Source #

convertibleUpperBound :: forall eb sb n. (ValidFP eb sb, KnownNat n, 1 <= n) => bv n -> FPRoundingMode -> FP eb sb Source #

Instances

Instances details

ConvertibleBound IntN Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods convertibleLowerBound :: forall (eb :: Nat) (sb :: Nat) (n :: Nat). (ValidFP eb sb, KnownNat n, 1 <= n) => IntN n -> FPRoundingMode -> FP eb sb Source # convertibleUpperBound :: forall (eb :: Nat) (sb :: Nat) (n :: Nat). (ValidFP eb sb, KnownNat n, 1 <= n) => IntN n -> FPRoundingMode -> FP eb sb Source #
ConvertibleBound WordN Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods convertibleLowerBound :: forall (eb :: Nat) (sb :: Nat) (n :: Nat). (ValidFP eb sb, KnownNat n, 1 <= n) => WordN n -> FPRoundingMode -> FP eb sb Source # convertibleUpperBound :: forall (eb :: Nat) (sb :: Nat) (n :: Nat). (ValidFP eb sb, KnownNat n, 1 <= n) => WordN n -> FPRoundingMode -> FP eb sb Source #

nextFP :: forall eb sb. ValidFP eb sb => FP eb sb -> FP eb sb Source #

Next representable floating-point number.

Note:

nextFP(+inf) = +inf
nextFP(-inf) = -maxNormalized
nextFP(NaN) = NaN

The function do not distinguish between -0 and +0.

prevFP :: forall eb sb. ValidFP eb sb => FP eb sb -> FP eb sb Source #

Previous representable floating-point number.

Note:

prevFP(+inf) = +maxNormalized
prevFP(-inf) = -inf
prevFP(NaN) = NaN

The function do not distinguish between -0 and +0.

withUnsafeValidFP :: forall eb sb r. (KnownNat eb, KnownNat sb) => (ValidFP eb sb => r) -> r Source #

Provide an (unsafe) type-level proof that the given floating-point type is valid.

checkDynamicValidFP :: Natural -> Natural -> Bool Source #

Check if the given floating-point type is valid.

invalidFPMessage :: String Source #

A message thrown when the floating-point type is invalid.