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.

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

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 => EvaluateSym (FP eb fb)

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

Methods

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

ValidFP eb sb => ExtractSymbolics (FP eb sb)

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

Methods

extractSymbolics :: FP eb sb -> SymbolSet

ValidFP eb sb => GPretty (FP eb sb)

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

Methods

gpretty :: FP eb sb -> Doc ann

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

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

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 => SEq (FP eb sb)

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

Methods

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

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

ValidFP eb sb => SOrd (FP eb sb)

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

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 -> UnionM Ordering

ValidFP eb sb => SubstituteSym (FP eb sb)

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

Methods

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

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 (UnionM (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

Constructors

RNE

RNA

RTP

RTN

RTZ

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

EvaluateSym FPRoundingMode

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

Methods

evaluateSym :: Bool -> Model -> FPRoundingMode -> FPRoundingMode

ExtractSymbolics FPRoundingMode

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

Methods

extractSymbolics :: FPRoundingMode -> SymbolSet

GPretty FPRoundingMode

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

Methods

gpretty :: FPRoundingMode -> Doc ann

gprettyPrec :: Int -> FPRoundingMode -> Doc ann

gprettyList :: [FPRoundingMode] -> Doc ann

Mergeable FPRoundingMode

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

Methods

rootStrategy :: MergingStrategy FPRoundingMode

SEq FPRoundingMode

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

Methods

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

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

SOrd FPRoundingMode

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

Methods

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

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

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

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

symCompare :: FPRoundingMode -> FPRoundingMode -> UnionM Ordering

SubstituteSym FPRoundingMode

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

Methods

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

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 (UnionM 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

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.6.0.0-LwdEaDUg4LU9IthQ8SjToU" '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]