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	None
Language	Haskell2010

Grisette.Internal.SymPrim.SymFP

Contents

Orphan instances

Description

Synopsis

newtype SymFP (eb :: Nat) (sb :: Nat) = SymFP (Term (FP eb sb))
type SymFP16 = SymFP 5 11
type SymFP32 = SymFP 8 24
type SymFP64 = SymFP 11 53
newtype SymFPRoundingMode = SymFPRoundingMode (Term FPRoundingMode)

Documentation

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

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

>>> "a" + 2.0 :: SymFP 11 53
(+ a 2.0)
>>> fpAdd rne "a" 2.0 :: SymFP 11 53
(fp.add rne a 2.0)

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

Constructors

SymFP (Term (FP eb sb))

Instances

Instances details

ToCon SymFP32 Float Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon

Methods

toCon :: SymFP32 -> Maybe Float Source #

ToCon SymFP64 Double Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon

Methods

toCon :: SymFP64 -> Maybe Double Source #

ToSym Double SymFP64 Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym

Methods

toSym :: Double -> SymFP64 Source #

ToSym Float SymFP32 Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym

Methods

toSym :: Float -> SymFP32 Source #

ValidFP eb sb => UnifiedFPImpl 'S SymFP eb sb (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedFP

Associated Types

type GetFP 'S
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedFP type GetFP 'S = SymFP
type GetFPRoundingMode 'S
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedFP type GetFPRoundingMode 'S = SymFPRoundingMode

(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 '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 #

ValidFP eb sb => UnifiedFromIntegral 'S SymInteger (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'S) (Integral SymInteger, Num (SymFP eb sb)) (SymFromIntegral SymInteger (SymFP eb sb)) => r) -> r 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, 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 #

(KnownNat n', 1 <= n', ValidFP eb sb) => UnifiedFromIntegral 'S (SymIntN n') (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymIntN n'), Num (SymFP eb sb)) (SymFromIntegral (SymIntN n') (SymFP eb sb)) => r) -> r Source #

(KnownNat n', 1 <= n', ValidFP eb sb) => UnifiedFromIntegral 'S (SymWordN n') (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymWordN n'), Num (SymFP eb sb)) (SymFromIntegral (SymWordN n') (SymFP eb sb)) => r) -> r 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 => GenSym () (SymFP eb sb) Source #

Instance details

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

Methods

fresh :: MonadFresh m => () -> m (Union (SymFP eb sb)) Source #

ValidFP eb sb => GenSymSimple () (SymFP eb sb) Source #

Instance details

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

Methods

simpleFresh :: MonadFresh m => () -> m (SymFP eb sb) Source #

ValidFP eb sb => SymFromIntegral SymInteger (SymFP eb sb) Source #

Instance details

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

Methods

symFromIntegral :: SymInteger -> SymFP eb sb Source #

Lift (SymFP eb sb :: Type) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

lift :: Quote m => SymFP eb sb -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => SymFP eb sb -> Code m (SymFP eb sb) #

ValidFP eb sb => IEEEFPConvertible SymAlgReal (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fromFPOr :: SymAlgReal -> SymFPRoundingMode -> SymFP eb sb -> SymAlgReal Source #

toFP :: SymFPRoundingMode -> SymAlgReal -> SymFP eb sb Source #

ValidFP eb sb => IEEEFPConvertible SymInteger (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fromFPOr :: SymInteger -> SymFPRoundingMode -> SymFP eb sb -> SymInteger Source #

toFP :: SymFPRoundingMode -> SymInteger -> SymFP eb sb Source #

ValidFP eb sb => IEEEFPToAlgReal SymAlgReal (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fpToAlgReal :: SymAlgReal -> SymFP eb sb -> SymAlgReal 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 #

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 (SymIntN r) (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

bitCast :: SymIntN r -> SymFP eb sb Source #

(ValidFP eb sb, r ~ (eb + sb)) => BitCast (SymWordN r) (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

bitCast :: SymWordN r -> SymFP eb sb Source #

(KnownNat n, 1 <= n, ValidFP eb sb) => SymFromIntegral (SymIntN n) (SymFP eb sb) Source #

Instance details

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

Methods

symFromIntegral :: SymIntN n -> SymFP eb sb Source #

(KnownNat n, 1 <= n, ValidFP eb sb) => SymFromIntegral (SymWordN n) (SymFP eb sb) Source #

Instance details

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

Methods

symFromIntegral :: SymWordN n -> SymFP eb sb Source #

(ValidFP eb sb, KnownNat n, 1 <= n) => IEEEFPConvertible (SymIntN n) (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fromFPOr :: SymIntN n -> SymFPRoundingMode -> SymFP eb sb -> SymIntN n Source #

toFP :: SymFPRoundingMode -> SymIntN n -> SymFP eb sb Source #

(ValidFP eb sb, KnownNat n, 1 <= n) => IEEEFPConvertible (SymWordN n) (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fromFPOr :: SymWordN n -> SymFPRoundingMode -> SymFP eb sb -> SymWordN n Source #

toFP :: SymFPRoundingMode -> SymWordN n -> SymFP eb sb Source #

ValidFP eb sb => Binary (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

put :: SymFP eb sb -> Put #

get :: Get (SymFP eb sb) #

putList :: [SymFP eb sb] -> Put #

ValidFP eb sb => Serial (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

serialize :: MonadPut m => SymFP eb sb -> m () #

deserialize :: MonadGet m => m (SymFP eb sb) #

ValidFP eb sb => Serialize (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

put :: Putter (SymFP eb sb) #

get :: Get (SymFP eb sb) #

NFData (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

rnf :: SymFP eb sb -> () #

ValidFP eb sb => IsString (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fromString :: String -> SymFP eb sb #

ValidFP eb sb => Floating (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

pi :: SymFP eb sb #

exp :: SymFP eb sb -> SymFP eb sb #

log :: SymFP eb sb -> SymFP eb sb #

sqrt :: SymFP eb sb -> SymFP eb sb #

(**) :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb #

logBase :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb #

sin :: SymFP eb sb -> SymFP eb sb #

cos :: SymFP eb sb -> SymFP eb sb #

tan :: SymFP eb sb -> SymFP eb sb #

asin :: SymFP eb sb -> SymFP eb sb #

acos :: SymFP eb sb -> SymFP eb sb #

atan :: SymFP eb sb -> SymFP eb sb #

sinh :: SymFP eb sb -> SymFP eb sb #

cosh :: SymFP eb sb -> SymFP eb sb #

tanh :: SymFP eb sb -> SymFP eb sb #

asinh :: SymFP eb sb -> SymFP eb sb #

acosh :: SymFP eb sb -> SymFP eb sb #

atanh :: SymFP eb sb -> SymFP eb sb #

log1p :: SymFP eb sb -> SymFP eb sb #

expm1 :: SymFP eb sb -> SymFP eb sb #

log1pexp :: SymFP eb sb -> SymFP eb sb #

log1mexp :: SymFP eb sb -> SymFP eb sb #

Generic (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Associated Types

type Rep (SymFP eb sb)
Instance details Defined in Grisette.Internal.SymPrim.SymFP type Rep (SymFP eb sb) = D1 ('MetaData "SymFP" "Grisette.Internal.SymPrim.SymFP" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'True) (C1 ('MetaCons "SymFP" 'PrefixI 'True) (S1 ('MetaSel ('Just "underlyingFPTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term (FP eb sb)))))

Methods

from :: SymFP eb sb -> Rep (SymFP eb sb) x #

to :: Rep (SymFP eb sb) x -> SymFP eb sb #

ValidFP eb sb => Num (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

(+) :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb #

(-) :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb #

(*) :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb #

negate :: SymFP eb sb -> SymFP eb sb #

abs :: SymFP eb sb -> SymFP eb sb #

signum :: SymFP eb sb -> SymFP eb sb #

fromInteger :: Integer -> SymFP eb sb #

ValidFP eb sb => Fractional (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

(/) :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb #

recip :: SymFP eb sb -> SymFP eb sb #

fromRational :: Rational -> SymFP eb sb #

ValidFP eb sb => Show (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

showsPrec :: Int -> SymFP eb sb -> ShowS #

show :: SymFP eb sb -> String #

showList :: [SymFP eb sb] -> ShowS #

ValidFP eb sb => Eq (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

(==) :: SymFP eb sb -> SymFP eb sb -> Bool #

(/=) :: SymFP eb sb -> SymFP eb sb -> Bool #

ValidFP eb sb => Apply (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Associated Types

type FunType (SymFP eb sb)
Instance details Defined in Grisette.Internal.SymPrim.SymFP type FunType (SymFP eb sb) = SymFP eb sb

Methods

apply :: SymFP eb sb -> FunType (SymFP eb sb) Source #

ValidFP eb sb => IEEEFPConstants (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

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 #

fpMinNormalized :: SymFP eb sb Source #

fpMinSubnormal :: SymFP eb sb Source #

fpMaxNormalized :: SymFP eb sb Source #

fpMaxSubnormal :: SymFP eb sb Source #

ValidFP eb sb => IEEEFPOp (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fpAbs :: SymFP eb sb -> SymFP eb sb Source #

fpNeg :: SymFP eb sb -> SymFP eb sb Source #

fpRem :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

fpMinimum :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

fpMinimumNumber :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

fpMaximum :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

fpMaximumNumber :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

ValidFP eb sb => ITEOp (SymFP eb sb) Source #

Instance details

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

Methods

symIte :: SymBool -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

ValidFP eb sb => SymIEEEFPTraits (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

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 #

ValidFP eb sb => EvalSym (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> SymFP eb sb -> SymFP eb sb Source #

ValidFP eb fb => ExtractSym (SymFP eb fb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ExtractSym

Methods

extractSym :: SymFP eb fb -> AnySymbolSet Source #

extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => SymFP eb fb -> Maybe (SymbolSet knd) Source #

ValidFP eb sb => Mergeable (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.Mergeable

Methods

rootStrategy :: MergingStrategy (SymFP eb sb) Source #

sortIndices :: SymFP eb sb -> [DynamicSortedIdx] Source #

ValidFP eb sb => PPrint (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.PPrint

Methods

pformat :: SymFP eb sb -> Doc ann Source #

pformatPrec :: Int -> SymFP eb sb -> Doc ann Source #

pformatList :: [SymFP eb sb] -> Doc ann Source #

ValidFP eb sb => SimpleMergeable (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

ValidFP eb sb => SubstSym (SymFP 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 -> SymFP eb sb -> SymFP eb sb Source #

ValidFP eb sb => SymEq (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq

Methods

(.==) :: SymFP eb sb -> SymFP eb sb -> SymBool Source #

(./=) :: SymFP eb sb -> SymFP eb sb -> SymBool Source #

symDistinct :: [SymFP eb sb] -> SymBool Source #

ValidFP eb sb => SymOrd (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd

Methods

(.<) :: SymFP eb sb -> SymFP eb sb -> SymBool Source #

(.<=) :: SymFP eb sb -> SymFP eb sb -> SymBool Source #

(.>) :: SymFP eb sb -> SymFP eb sb -> SymBool Source #

(.>=) :: SymFP eb sb -> SymFP eb sb -> SymBool Source #

symCompare :: SymFP eb sb -> SymFP eb sb -> Union Ordering Source #

ValidFP eb sb => AllSyms (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

allSymsS :: SymFP eb sb -> [SomeSym] -> [SomeSym] Source #

allSyms :: SymFP eb sb -> [SomeSym] Source #

ConRep (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Associated Types

type ConType (SymFP eb sb)
Instance details Defined in Grisette.Internal.SymPrim.SymFP type ConType (SymFP eb sb) = FP eb sb

ValidFP eb sb => UnifiedConRep (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

Associated Types

type ConType (SymFP eb sb)
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedRep type ConType (SymFP eb sb) = FP eb sb

ValidFP eb sb => UnifiedSymRep (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

Associated Types

type SymType (SymFP eb sb)
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedRep type SymType (SymFP eb sb) = SymFP eb sb

ValidFP eb sb => Hashable (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

hashWithSalt :: Int -> SymFP eb sb -> Int #

hash :: SymFP eb sb -> Int #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

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

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

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

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

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

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

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

(ValidFP eb sb, r ~ (eb + sb)) => BitCastCanonical (SymFP eb sb) (SymIntN r) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

bitCastCanonicalValue :: proxy (SymFP eb sb) -> SymIntN r Source #

(ValidFP eb sb, r ~ (eb + sb)) => BitCastCanonical (SymFP eb sb) (SymWordN r) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

bitCastCanonicalValue :: proxy (SymFP eb sb) -> SymWordN r Source #

(ValidFP eb sb, r ~ (eb + sb)) => BitCastOr (SymFP eb sb) (SymIntN r) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

bitCastOr :: SymIntN r -> SymFP eb sb -> SymIntN r Source #

(ValidFP eb sb, r ~ (eb + sb)) => BitCastOr (SymFP eb sb) (SymWordN r) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

bitCastOr :: SymWordN r -> SymFP eb sb -> SymWordN r Source #

ValidFP eb sb => GenSym (SymFP eb sb) (SymFP eb sb) Source #

Instance details

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

Methods

fresh :: MonadFresh m => SymFP eb sb -> m (Union (SymFP eb sb)) Source #

ValidFP eb sb => GenSymSimple (SymFP eb sb) (SymFP eb sb) Source #

Instance details

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

Methods

simpleFresh :: MonadFresh m => SymFP eb sb -> m (SymFP 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 (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 => ToCon (SymFP eb sb) (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon

Methods

toCon :: SymFP eb sb -> Maybe (SymFP 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 => ToSym (SymFP eb sb) (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym

Methods

toSym :: SymFP 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 (SymFP eb' sb') (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fromFPOr :: SymFP eb' sb' -> SymFPRoundingMode -> SymFP eb sb -> SymFP eb' sb' Source #

toFP :: SymFPRoundingMode -> SymFP eb' sb' -> SymFP eb sb Source #

type Rep (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

type Rep (SymFP eb sb) = D1 ('MetaData "SymFP" "Grisette.Internal.SymPrim.SymFP" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'True) (C1 ('MetaCons "SymFP" 'PrefixI 'True) (S1 ('MetaSel ('Just "underlyingFPTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term (FP eb sb)))))

type FunType (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

type FunType (SymFP eb sb) = SymFP eb sb

type ConType (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

type ConType (SymFP eb sb) = FP eb sb

type ConType (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type ConType (SymFP eb sb) = FP eb sb

type SymType (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type SymType (SymFP eb sb) = SymFP eb sb

type SymFP16 = SymFP 5 11 Source #

Symbolic IEEE 754 half-precision floating-point number.

type SymFP32 = SymFP 8 24 Source #

Symbolic IEEE 754 single-precision floating-point number.

type SymFP64 = SymFP 11 53 Source #

Symbolic IEEE 754 double-precision floating-point number.

newtype SymFPRoundingMode Source #

Symbolic floating-point rounding mode.

Constructors

SymFPRoundingMode (Term FPRoundingMode)

Instances

Instances details

NFData SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

rnf :: SymFPRoundingMode -> () #

IsString SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fromString :: String -> SymFPRoundingMode #

Generic SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Associated Types

type Rep SymFPRoundingMode
Instance details Defined in Grisette.Internal.SymPrim.SymFP type Rep SymFPRoundingMode = D1 ('MetaData "SymFPRoundingMode" "Grisette.Internal.SymPrim.SymFP" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'True) (C1 ('MetaCons "SymFPRoundingMode" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term FPRoundingMode))))

Methods

from :: SymFPRoundingMode -> Rep SymFPRoundingMode x #

to :: Rep SymFPRoundingMode x -> SymFPRoundingMode #

Show SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

showsPrec :: Int -> SymFPRoundingMode -> ShowS #

show :: SymFPRoundingMode -> String #

showList :: [SymFPRoundingMode] -> ShowS #

Eq SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

(==) :: SymFPRoundingMode -> SymFPRoundingMode -> Bool #

(/=) :: SymFPRoundingMode -> SymFPRoundingMode -> Bool #

Apply SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Associated Types

type FunType SymFPRoundingMode
Instance details Defined in Grisette.Internal.SymPrim.SymFP type FunType SymFPRoundingMode = SymFPRoundingMode

Methods

apply :: SymFPRoundingMode -> FunType SymFPRoundingMode Source #

IEEEFPRoundingMode SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

rne :: SymFPRoundingMode Source #

rna :: SymFPRoundingMode Source #

rtp :: SymFPRoundingMode Source #

rtn :: SymFPRoundingMode Source #

rtz :: SymFPRoundingMode Source #

ITEOp SymFPRoundingMode Source #

Instance details

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

Methods

symIte :: SymBool -> SymFPRoundingMode -> SymFPRoundingMode -> SymFPRoundingMode Source #

EvalSym SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> SymFPRoundingMode -> SymFPRoundingMode Source #

ExtractSym SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ExtractSym

Methods

extractSym :: SymFPRoundingMode -> AnySymbolSet Source #

extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => SymFPRoundingMode -> Maybe (SymbolSet knd) Source #

Mergeable SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.Mergeable

Methods

rootStrategy :: MergingStrategy SymFPRoundingMode Source #

sortIndices :: SymFPRoundingMode -> [DynamicSortedIdx] Source #

PPrint SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.PPrint

Methods

pformat :: SymFPRoundingMode -> Doc ann Source #

pformatPrec :: Int -> SymFPRoundingMode -> Doc ann Source #

pformatList :: [SymFPRoundingMode] -> Doc ann Source #

SimpleMergeable SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> SymFPRoundingMode -> SymFPRoundingMode -> SymFPRoundingMode Source #

SubstSym SymFPRoundingMode 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 -> SymFPRoundingMode -> SymFPRoundingMode Source #

SymEq SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq

Methods

(.==) :: SymFPRoundingMode -> SymFPRoundingMode -> SymBool Source #

(./=) :: SymFPRoundingMode -> SymFPRoundingMode -> SymBool Source #

symDistinct :: [SymFPRoundingMode] -> SymBool Source #

SymOrd SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd

Methods

(.<) :: SymFPRoundingMode -> SymFPRoundingMode -> SymBool Source #

(.<=) :: SymFPRoundingMode -> SymFPRoundingMode -> SymBool Source #

(.>) :: SymFPRoundingMode -> SymFPRoundingMode -> SymBool Source #

(.>=) :: SymFPRoundingMode -> SymFPRoundingMode -> SymBool Source #

symCompare :: SymFPRoundingMode -> SymFPRoundingMode -> Union Ordering Source #

AllSyms SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

allSymsS :: SymFPRoundingMode -> [SomeSym] -> [SomeSym] Source #

allSyms :: SymFPRoundingMode -> [SomeSym] Source #

ConRep SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Associated Types

type ConType SymFPRoundingMode
Instance details Defined in Grisette.Internal.SymPrim.SymFP type ConType SymFPRoundingMode = FPRoundingMode

Hashable SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

hashWithSalt :: Int -> SymFPRoundingMode -> Int #

hash :: SymFPRoundingMode -> Int #

GenSym SymFPRoundingMode SymFPRoundingMode Source #

Instance details

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

Methods

fresh :: MonadFresh m => SymFPRoundingMode -> m (Union SymFPRoundingMode) Source #

GenSym () SymFPRoundingMode Source #

Instance details

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

Methods

fresh :: MonadFresh m => () -> m (Union SymFPRoundingMode) Source #

GenSymSimple SymFPRoundingMode SymFPRoundingMode Source #

Instance details

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

Methods

simpleFresh :: MonadFresh m => SymFPRoundingMode -> m SymFPRoundingMode Source #

GenSymSimple () SymFPRoundingMode Source #

Instance details

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

Methods

simpleFresh :: MonadFresh m => () -> m SymFPRoundingMode 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 SymFPRoundingMode FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon

Methods

toCon :: SymFPRoundingMode -> Maybe FPRoundingMode Source #

ToCon SymFPRoundingMode SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon

Methods

toCon :: SymFPRoundingMode -> Maybe SymFPRoundingMode Source #

ToSym FPRoundingMode SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym

Methods

toSym :: FPRoundingMode -> SymFPRoundingMode Source #

ToSym SymFPRoundingMode SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym

Methods

toSym :: SymFPRoundingMode -> SymFPRoundingMode 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 SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

lift :: Quote m => SymFPRoundingMode -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => SymFPRoundingMode -> Code m SymFPRoundingMode #

ValidFP eb sb => UnifiedFPImpl 'S SymFP eb sb (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedFP

Associated Types

type GetFP 'S
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedFP type GetFP 'S = SymFP
type GetFPRoundingMode 'S
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedFP type GetFPRoundingMode 'S = SymFPRoundingMode