Grisette.Internal.SymPrim.FP

Documentation

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

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

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

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

>>> :set -XDataKinds
>>> 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

BitCast Int16 FP16

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: Int16 -> FP16

BitCast Int32 FP32

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: Int32 -> FP32

BitCast Int64 FP64

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: Int64 -> FP64

BitCast Word16 FP16

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: Word16 -> FP16

BitCast Word32 FP32

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: Word32 -> FP32

BitCast Word64 FP64

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: Word64 -> FP64

BitCast FP16 Int16

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: FP16 -> Int16

BitCast FP16 Word16

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: FP16 -> Word16

BitCast FP32 Int32

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: FP32 -> Int32

BitCast FP32 Word32

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: FP32 -> Word32

BitCast FP32 Float

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: FP32 -> Float

BitCast FP64 Int64

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: FP64 -> Int64

BitCast FP64 Word64

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: FP64 -> Word64

BitCast FP64 Double

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: FP64 -> Double

BitCast Double FP64

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: Double -> FP64

BitCast Float FP32

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: Float -> FP32

(Typeable mode, ValidFP eb sb) => UnifiedSymEq mode (FP eb sb)

Defined in Grisette.Unified.Internal.Class.UnifiedSymEq

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (FP eb sb)) (SymEq (FP eb sb)) => r) -> r

(Typeable mode, ValidFP eb sb) => UnifiedSymOrd mode (FP eb sb)

Defined in Grisette.Unified.Internal.Class.UnifiedSymOrd

Methods

withBaseSymOrd :: (If (IsConMode mode) (Ord (FP eb sb)) (SymOrd (FP eb sb)) => r) -> r

ValidFP eb sb => Lift (FP eb sb :: Type)

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, r ~ (eb + sb)) => BitCast (IntN r) (FP eb sb)

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: IntN r -> FP eb sb

(ValidFP eb sb, r ~ (eb + sb)) => BitCast (WordN r) (FP eb sb)

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: WordN r -> FP eb sb

ValidFloat eb sb => Arbitrary (FP eb sb)

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)

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)

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)

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)

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)

Defined in Grisette.Internal.SymPrim.FP

Methods

toRational :: FP eb sb -> Rational

ValidFloat eb sb => RealFrac (FP eb sb)

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)

Defined in Grisette.Internal.SymPrim.FP

Methods

showsPrec :: Int -> FP eb sb -> ShowS

show :: FP eb sb -> String

showList :: [FP eb sb] -> ShowS

NFData (FP eb sb)

Defined in Grisette.Internal.SymPrim.FP

Methods

rnf :: FP eb sb -> ()

Eq (FP eb sb)

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)

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

ValidFP eb fb => EvalSym (FP eb fb)

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

Methods

evalSym :: Bool -> Model -> FP eb fb -> FP eb fb

ValidFP eb sb => ExtractSym (FP eb sb)

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

Methods

extractSym :: FP eb sb -> SymbolSet

ValidFP eb sb => IEEEConstants (FP eb sb)

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

Methods

fpPositiveInfinite :: FP eb sb

fpNegativeInfinite :: FP eb sb

fpNaN :: FP eb sb

fpNegativeZero :: FP eb sb

fpPositiveZero :: FP eb sb

ValidFP eb sb => SymIEEEFPTraits (FP eb sb)

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

Methods

symFpIsNaN :: FP eb sb -> SymBool

symFpIsPositive :: FP eb sb -> SymBool

symFpIsNegative :: FP eb sb -> SymBool

symFpIsPositiveInfinite :: FP eb sb -> SymBool

symFpIsNegativeInfinite :: FP eb sb -> SymBool

symFpIsInfinite :: FP eb sb -> SymBool

symFpIsPositiveZero :: FP eb sb -> SymBool

symFpIsNegativeZero :: FP eb sb -> SymBool

symFpIsZero :: FP eb sb -> SymBool

symFpIsNormal :: FP eb sb -> SymBool

symFpIsSubnormal :: FP eb sb -> SymBool

symFpIsPoint :: FP eb sb -> SymBool

ValidFP eb sb => Mergeable (FP eb sb)

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

Methods

rootStrategy :: MergingStrategy (FP eb sb)

ValidFP eb sb => PPrint (FP eb sb)

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

Methods

pformat :: FP eb sb -> Doc ann

pformatPrec :: Int -> FP eb sb -> Doc ann

pformatList :: [FP eb sb] -> Doc ann

ValidFP eb sb => SubstSym (FP eb sb)

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

Methods

substSym :: LinkedRep cb sb0 => TypedSymbol cb -> sb0 -> FP eb sb -> FP eb sb

ValidFP eb sb => SymEq (FP eb sb)

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

Methods

(.==) :: FP eb sb -> FP eb sb -> SymBool

(./=) :: FP eb sb -> FP eb sb -> SymBool

ValidFP eb sb => SymOrd (FP eb sb)

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

Methods

(.<) :: FP eb sb -> FP eb sb -> SymBool

(.<=) :: FP eb sb -> FP eb sb -> SymBool

(.>) :: FP eb sb -> FP eb sb -> SymBool

(.>=) :: FP eb sb -> FP eb sb -> SymBool

symCompare :: FP eb sb -> FP eb sb -> Union Ordering

ValidFP eb sb => AllSyms (FP eb sb)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: FP eb sb -> [SomeSym] -> [SomeSym]

allSyms :: FP eb sb -> [SomeSym]

ValidFP eb sb => NonFuncSBVRep (FP eb sb)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type NonFuncSBVBaseType n (FP eb sb)

ValidFP eb sb => PEvalFloatingTerm (FP eb sb)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFloatingTerm

Methods

pevalSqrtTerm :: Term (FP eb sb) -> Term (FP eb sb)

withSbvFloatingTermConstraint :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> (Floating (SBVType n (FP eb sb)) => r) -> r

sbvSqrtTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb)

ValidFP eb sb => PEvalFractionalTerm (FP eb sb)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFractionalTerm

Methods

pevalFdivTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)

pevalRecipTerm :: Term (FP eb sb) -> Term (FP eb sb)

withSbvFractionalTermConstraint :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> (Fractional (SBVType n (FP eb sb)) => r) -> r

sbvFdivTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) -> SBVType n (FP eb sb)

sbvRecipTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb)

ValidFP eb sb => PEvalNumTerm (FP eb sb)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm

Methods

pevalAddNumTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)

pevalNegNumTerm :: Term (FP eb sb) -> Term (FP eb sb)

pevalMulNumTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)

pevalAbsNumTerm :: Term (FP eb sb) -> Term (FP eb sb)

pevalSignumNumTerm :: Term (FP eb sb) -> Term (FP eb sb)

withSbvNumTermConstraint :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> (Num (SBVType n (FP eb sb)) => r) -> r

sbvAddNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) -> SBVType n (FP eb sb)

sbvNegNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb)

sbvMulNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) -> SBVType n (FP eb sb)

sbvAbsNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb)

sbvSignumNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb)

ValidFP eb sb => PEvalOrdTerm (FP eb sb)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm

Methods

pevalLtOrdTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term Bool

pevalLeOrdTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term Bool

withSbvOrdTermConstraint :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> (OrdSymbolic (SBVType n (FP eb sb)) => r) -> r

sbvLtOrdTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) -> SBV Bool

sbvLeOrdTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) -> SBV Bool

ValidFP eb sb => SBVRep (FP eb sb)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type SBVType n (FP eb sb)

ValidFP eb sb => SupportedNonFuncPrim (FP eb sb)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Methods

conNonFuncSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> FP eb sb -> SBV (NonFuncSBVBaseType n (FP eb sb))

symNonFuncSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBV (NonFuncSBVBaseType n (FP eb sb)))

withNonFuncPrim :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> ((SymVal (NonFuncSBVBaseType n (FP eb sb)), EqSymbolic (SBVType n (FP eb sb)), Mergeable (SBVType n (FP eb sb)), SMTDefinable (SBVType n (FP eb sb)), Mergeable (SBVType n (FP eb sb)), SBVType n (FP eb sb) ~ SBV (NonFuncSBVBaseType n (FP eb sb)), PrimConstraint n (FP eb sb)) => r) -> r

ValidFP eb sb => SupportedPrim (FP eb sb)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Methods

termCache :: Cache (Term (FP eb sb))

pformatCon :: FP eb sb -> String

pformatSym :: TypedSymbol (FP eb sb) -> String

defaultValue :: FP eb sb

defaultValueDynamic :: proxy (FP eb sb) -> ModelValue

pevalITETerm :: Term Bool -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)

pevalEqTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> FP eb sb -> SBVType n (FP eb sb)

symSBVName :: TypedSymbol (FP eb sb) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (FP eb sb))

withPrim :: forall (n :: Nat) p a. KnownIsZero n => p n -> ((PrimConstraint n (FP eb sb), SMTDefinable (SBVType n (FP eb sb)), Mergeable (SBVType n (FP eb sb)), Typeable (SBVType n (FP eb sb))) => a) -> a

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) -> SBVType n (FP eb sb)

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> FP eb sb

ValidFP eb sb => SupportedPrimConstraint (FP eb sb)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type PrimConstraint n (FP eb sb)

ValidFP eb sb => SymRep (FP eb sb)

Defined in Grisette.Internal.SymPrim.SymFP

Associated Types

type SymType (FP eb sb)

ValidFP eb sb => Hashable (FP eb sb)

Defined in Grisette.Internal.SymPrim.FP

Methods

hashWithSalt :: Int -> FP eb sb -> Int

hash :: FP eb sb -> Int

(ValidFP eb sb, r ~ (eb + sb)) => BitCast (FP eb sb) (IntN r)

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: FP eb sb -> IntN r

(ValidFP eb sb, r ~ (eb + sb)) => BitCast (FP eb sb) (WordN r)

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: FP eb sb -> WordN r

ValidFP eb sb => GenSym (FP eb sb) (FP eb sb)

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

Methods

fresh :: MonadFresh m => FP eb sb -> m (Union (FP eb sb))

ValidFP eb sb => GenSymSimple (FP eb sb) (FP eb sb)

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

Methods

simpleFresh :: MonadFresh m => FP eb sb -> m (FP eb sb)

ValidFP eb sb => Solvable (FP eb sb) (SymFP eb sb)

Defined in Grisette.Internal.SymPrim.SymFP

Methods

con :: FP eb sb -> SymFP eb sb

conView :: SymFP eb sb -> Maybe (FP eb sb)

sym :: Symbol -> SymFP eb sb

ssym :: Identifier -> SymFP eb sb

isym :: Identifier -> Int -> SymFP eb sb

ValidFP eb sb => ToCon (FP eb sb) (FP eb sb)

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

Methods

toCon :: FP eb sb -> Maybe (FP eb sb)

ValidFP eb sb => ToCon (SymFP eb sb) (FP eb sb)

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

Methods

toCon :: SymFP eb sb -> Maybe (FP eb sb)

ValidFP eb sb => ToSym (FP eb sb) (FP eb sb)

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

Methods

toSym :: FP eb sb -> FP eb sb

ValidFP eb sb => ToSym (FP eb sb) (SymFP eb sb)

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

Methods

toSym :: FP eb sb -> SymFP eb sb

ValidFP eb sb => LinkedRep (FP eb sb) (SymFP eb sb)

Defined in Grisette.Internal.SymPrim.SymFP

Methods

underlyingTerm :: SymFP eb sb -> Term (FP eb sb)

wrapTerm :: Term (FP eb sb) -> SymFP eb sb

type NonFuncSBVBaseType _1 (FP eb sb)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type NonFuncSBVBaseType _1 (FP eb sb) = FloatingPoint eb sb

type PrimConstraint _1 (FP eb sb)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type PrimConstraint _1 (FP eb sb) = ValidFP eb sb

type SBVType _1 (FP eb sb)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type SBVType _1 (FP eb sb) = SBV (FloatingPoint eb sb)

type SymType (FP eb sb)

Defined in Grisette.Internal.SymPrim.SymFP

type SymType (FP eb sb) = SymFP eb sb

type FP16 = FP 5 11

IEEE 754 half-precision floating-point number.

type FP32 = FP 8 24

IEEE 754 single-precision floating-point number.

type FP64 = FP 11 53

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

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

data FPRoundingMode

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

Arbitrary FPRoundingMode

Defined in Grisette.Internal.SymPrim.FP

Methods

arbitrary :: Gen FPRoundingMode

shrink :: FPRoundingMode -> [FPRoundingMode]

Generic FPRoundingMode

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

Defined in Grisette.Internal.SymPrim.FP

Methods

showsPrec :: Int -> FPRoundingMode -> ShowS

show :: FPRoundingMode -> String

showList :: [FPRoundingMode] -> ShowS

NFData FPRoundingMode

Defined in Grisette.Internal.SymPrim.FP

Methods

rnf :: FPRoundingMode -> ()

Eq FPRoundingMode

Defined in Grisette.Internal.SymPrim.FP

Methods

(==) :: FPRoundingMode -> FPRoundingMode -> Bool

(/=) :: FPRoundingMode -> FPRoundingMode -> Bool

Ord FPRoundingMode

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

EvalSym FPRoundingMode

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

Methods

evalSym :: Bool -> Model -> FPRoundingMode -> FPRoundingMode

ExtractSym FPRoundingMode

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

Methods

extractSym :: FPRoundingMode -> SymbolSet

IEEEFPRoundingMode FPRoundingMode

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

Methods

rne :: FPRoundingMode

rna :: FPRoundingMode

rtp :: FPRoundingMode

rtn :: FPRoundingMode

rtz :: FPRoundingMode

Mergeable FPRoundingMode

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

Methods

rootStrategy :: MergingStrategy FPRoundingMode

PPrint FPRoundingMode

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

Methods

pformat :: FPRoundingMode -> Doc ann

pformatPrec :: Int -> FPRoundingMode -> Doc ann

pformatList :: [FPRoundingMode] -> Doc ann

SubstSym FPRoundingMode

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

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> FPRoundingMode -> FPRoundingMode

SymEq FPRoundingMode

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

Methods

(.==) :: FPRoundingMode -> FPRoundingMode -> SymBool

(./=) :: FPRoundingMode -> FPRoundingMode -> SymBool

SymOrd FPRoundingMode

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

Methods

(.<) :: FPRoundingMode -> FPRoundingMode -> SymBool

(.<=) :: FPRoundingMode -> FPRoundingMode -> SymBool

(.>) :: FPRoundingMode -> FPRoundingMode -> SymBool

(.>=) :: FPRoundingMode -> FPRoundingMode -> SymBool

symCompare :: FPRoundingMode -> FPRoundingMode -> Union Ordering

AllSyms FPRoundingMode

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: FPRoundingMode -> [SomeSym] -> [SomeSym]

allSyms :: FPRoundingMode -> [SomeSym]

NonFuncSBVRep FPRoundingMode

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type NonFuncSBVBaseType n FPRoundingMode

PEvalOrdTerm FPRoundingMode

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm

Methods

pevalLtOrdTerm :: Term FPRoundingMode -> Term FPRoundingMode -> Term Bool

pevalLeOrdTerm :: Term FPRoundingMode -> Term FPRoundingMode -> Term Bool

withSbvOrdTermConstraint :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> (OrdSymbolic (SBVType n FPRoundingMode) => r) -> r

sbvLtOrdTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n FPRoundingMode -> SBVType n FPRoundingMode -> SBV Bool

sbvLeOrdTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n FPRoundingMode -> SBVType n FPRoundingMode -> SBV Bool

SBVRep FPRoundingMode

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type SBVType n FPRoundingMode

SupportedNonFuncPrim FPRoundingMode

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Methods

conNonFuncSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> FPRoundingMode -> SBV (NonFuncSBVBaseType n FPRoundingMode)

symNonFuncSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBV (NonFuncSBVBaseType n FPRoundingMode))

withNonFuncPrim :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> ((SymVal (NonFuncSBVBaseType n FPRoundingMode), EqSymbolic (SBVType n FPRoundingMode), Mergeable (SBVType n FPRoundingMode), SMTDefinable (SBVType n FPRoundingMode), Mergeable (SBVType n FPRoundingMode), SBVType n FPRoundingMode ~ SBV (NonFuncSBVBaseType n FPRoundingMode), PrimConstraint n FPRoundingMode) => r) -> r

SupportedPrim FPRoundingMode

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Methods

termCache :: Cache (Term FPRoundingMode)

pformatCon :: FPRoundingMode -> String

pformatSym :: TypedSymbol FPRoundingMode -> String

defaultValue :: FPRoundingMode

defaultValueDynamic :: proxy FPRoundingMode -> ModelValue

pevalITETerm :: Term Bool -> Term FPRoundingMode -> Term FPRoundingMode -> Term FPRoundingMode

pevalEqTerm :: Term FPRoundingMode -> Term FPRoundingMode -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> FPRoundingMode -> SBVType n FPRoundingMode

symSBVName :: TypedSymbol FPRoundingMode -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n FPRoundingMode)

withPrim :: forall (n :: Nat) p a. KnownIsZero n => p n -> ((PrimConstraint n FPRoundingMode, SMTDefinable (SBVType n FPRoundingMode), Mergeable (SBVType n FPRoundingMode), Typeable (SBVType n FPRoundingMode)) => a) -> a

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n FPRoundingMode -> SBVType n FPRoundingMode -> SBVType n FPRoundingMode

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n FPRoundingMode -> SBVType n FPRoundingMode -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> FPRoundingMode

SupportedPrimConstraint FPRoundingMode

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type PrimConstraint n FPRoundingMode

SymRep FPRoundingMode

Defined in Grisette.Internal.SymPrim.SymFP

Associated Types

type SymType FPRoundingMode

Hashable FPRoundingMode

Defined in Grisette.Internal.SymPrim.FP

Methods

hashWithSalt :: Int -> FPRoundingMode -> Int

hash :: FPRoundingMode -> Int

GenSym FPRoundingMode FPRoundingMode

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

Methods

fresh :: MonadFresh m => FPRoundingMode -> m (Union FPRoundingMode)

GenSymSimple FPRoundingMode FPRoundingMode

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

Methods

simpleFresh :: MonadFresh m => FPRoundingMode -> m FPRoundingMode

Solvable FPRoundingMode SymFPRoundingMode

Defined in Grisette.Internal.SymPrim.SymFP

Methods

con :: FPRoundingMode -> SymFPRoundingMode

conView :: SymFPRoundingMode -> Maybe FPRoundingMode

sym :: Symbol -> SymFPRoundingMode

ssym :: Identifier -> SymFPRoundingMode

isym :: Identifier -> Int -> SymFPRoundingMode

ToCon FPRoundingMode FPRoundingMode

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

Methods

toCon :: FPRoundingMode -> Maybe FPRoundingMode

ToCon SymFPRoundingMode FPRoundingMode

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

Methods

toCon :: SymFPRoundingMode -> Maybe FPRoundingMode

ToSym FPRoundingMode FPRoundingMode

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

Methods

toSym :: FPRoundingMode -> FPRoundingMode

ToSym FPRoundingMode SymFPRoundingMode

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

Methods

toSym :: FPRoundingMode -> SymFPRoundingMode

LinkedRep FPRoundingMode SymFPRoundingMode

Defined in Grisette.Internal.SymPrim.SymFP

Methods

underlyingTerm :: SymFPRoundingMode -> Term FPRoundingMode

wrapTerm :: Term FPRoundingMode -> SymFPRoundingMode

Typeable mode => UnifiedSymEq mode FPRoundingMode

Defined in Grisette.Unified.Internal.Class.UnifiedSymEq

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq FPRoundingMode) (SymEq FPRoundingMode) => r) -> r

Typeable mode => UnifiedSymOrd mode FPRoundingMode

Defined in Grisette.Unified.Internal.Class.UnifiedSymOrd

Methods

withBaseSymOrd :: (If (IsConMode mode) (Ord FPRoundingMode) (SymOrd FPRoundingMode) => r) -> r

Lift FPRoundingMode

Defined in Grisette.Internal.SymPrim.FP

Methods

lift :: Quote m => FPRoundingMode -> m Exp

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

type Rep FPRoundingMode

Defined in Grisette.Internal.SymPrim.FP

type Rep FPRoundingMode = D1 ('MetaData "FPRoundingMode" "Grisette.Internal.SymPrim.FP" "grisette-0.7.0.0-3DYM4wcz8TiF8sSQ1gvVO8" '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 SymType FPRoundingMode

Defined in Grisette.Internal.SymPrim.SymFP

type SymType FPRoundingMode = SymFPRoundingMode

type NonFuncSBVBaseType _1 FPRoundingMode

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type NonFuncSBVBaseType _1 FPRoundingMode = RoundingMode

type PrimConstraint n FPRoundingMode

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type PrimConstraint n FPRoundingMode = ()

type SBVType _1 FPRoundingMode

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type SBVType _1 FPRoundingMode = SBV RoundingMode

allFPRoundingMode :: [FPRoundingMode]

All IEEE 754 rounding modes.