Grisette.Internal.Core.Data.Class.SignConversion

Documentation

class SignConversion ubv sbv | ubv -> sbv, sbv -> ubv where

Convert values between signed and unsigned.

Methods

toSigned :: ubv -> sbv

Convert unsigned value to the corresponding signed value.

toUnsigned :: sbv -> ubv

Convert signed value to the corresponding unsigned value.

Instances

SignConversion Word16 Int16

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

Methods

toSigned :: Word16 -> Int16

toUnsigned :: Int16 -> Word16

SignConversion Word32 Int32

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

Methods

toSigned :: Word32 -> Int32

toUnsigned :: Int32 -> Word32

SignConversion Word64 Int64

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

Methods

toSigned :: Word64 -> Int64

toUnsigned :: Int64 -> Word64

SignConversion Word8 Int8

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

Methods

toSigned :: Word8 -> Int8

toUnsigned :: Int8 -> Word8

SignConversion Word Int

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

Methods

toSigned :: Word -> Int

toUnsigned :: Int -> Word

(KnownNat n, 1 <= n) => SignConversion (WordN n) (IntN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

toSigned :: WordN n -> IntN n

toUnsigned :: IntN n -> WordN n

(forall (n :: Nat). (KnownNat n, 1 <= n) => SignConversion (ubv n) (sbv n), SignConversion (ubv 1) (sbv 1)) => SignConversion (SomeBV ubv) (SomeBV sbv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

toSigned :: SomeBV ubv -> SomeBV sbv

toUnsigned :: SomeBV sbv -> SomeBV ubv

(KnownNat n, 1 <= n) => SignConversion (SymWordN n) (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

toSigned :: SymWordN n -> SymIntN n

toUnsigned :: SymIntN n -> SymWordN n