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.Prim.Internal.Instances.PEvalIEEEFPConvertibleTerm

Contents

Orphan instances

Description

Synopsis

genericFPCast :: (HasKind a, HasKind r) => SRoundingMode -> SBV a -> SBV r

Documentation

genericFPCast :: (HasKind a, HasKind r) => SRoundingMode -> SBV a -> SBV r Source #

Generic implementation for floating-point casting operators for sbv.

Orphan instances

PEvalIEEEFPConvertibleTerm AlgReal Source #
Instance details Methods pevalFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term AlgReal -> Term FPRoundingMode -> Term (FP eb sb) -> Term AlgReal Source # pevalToFPTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term FPRoundingMode -> Term AlgReal -> Term (FP eb sb) Source # sbvFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType AlgReal -> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType AlgReal Source # sbvToFPTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType FPRoundingMode -> SBVType AlgReal -> SBVType (FP eb sb) Source #
PEvalIEEEFPConvertibleTerm Integer Source #
Instance details Methods pevalFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term Integer -> Term FPRoundingMode -> Term (FP eb sb) -> Term Integer Source # pevalToFPTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term FPRoundingMode -> Term Integer -> Term (FP eb sb) Source # sbvFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType Integer -> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType Integer Source # sbvToFPTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType FPRoundingMode -> SBVType Integer -> SBVType (FP eb sb) Source #
(KnownNat n, 1 <= n) => PEvalIEEEFPConvertibleTerm (IntN n) Source #
Instance details Methods pevalFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term (IntN n) -> Term FPRoundingMode -> Term (FP eb sb) -> Term (IntN n) Source # pevalToFPTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term FPRoundingMode -> Term (IntN n) -> Term (FP eb sb) Source # sbvFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType (IntN n) -> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType (IntN n) Source # sbvToFPTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType FPRoundingMode -> SBVType (IntN n) -> SBVType (FP eb sb) Source #
(KnownNat n, 1 <= n) => PEvalIEEEFPConvertibleTerm (WordN n) Source #
Instance details Methods pevalFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term (WordN n) -> Term FPRoundingMode -> Term (FP eb sb) -> Term (WordN n) Source # pevalToFPTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term FPRoundingMode -> Term (WordN n) -> Term (FP eb sb) Source # sbvFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType (WordN n) -> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType (WordN n) Source # sbvToFPTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType FPRoundingMode -> SBVType (WordN n) -> SBVType (FP eb sb) Source #
ValidFP eb sb => PEvalIEEEFPConvertibleTerm (FP eb sb) Source #
Instance details 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 #