grisette-0.11.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2023
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellSafe-Inferred
LanguageHaskell2010

Grisette.Internal.Core.Data.Class.SymShift

Description

 
Synopsis

Documentation

class Bits a => SymShift a where Source #

A class for shifting operations.

The symShift function shifts the value to the left if the shift amount is positive, and to the right if the shift amount is negative. If shifting beyond the bit width of the value, the result is the same as shifting with the bit width.

The symShiftNegated function shifts the value to the right if the shift amount is positive, and to the left if the shift amount is negative. This function is introduced to handle the asymmetry of the range of values.

Methods

symShift :: a -> a -> a Source #

symShiftNegated :: a -> a -> a Source #

Instances

Instances details
SymShift Int16 Source # 
Instance details

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

SymShift Int32 Source # 
Instance details

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

SymShift Int64 Source # 
Instance details

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

SymShift Int8 Source # 
Instance details

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

SymShift Word16 Source # 
Instance details

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

SymShift Word32 Source # 
Instance details

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

SymShift Word64 Source # 
Instance details

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

SymShift Word8 Source # 
Instance details

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

SymShift Int Source # 
Instance details

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

SymShift Word Source # 
Instance details

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

(Integral a, FiniteBits a) => SymShift (DefaultFiniteBitsSymShift a) Source # 
Instance details

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

(KnownNat n, 1 <= n) => SymShift (IntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

symShift :: IntN n -> IntN n -> IntN n Source #

symShiftNegated :: IntN n -> IntN n -> IntN n Source #

(KnownNat n, 1 <= n) => SymShift (WordN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

symShift :: WordN n -> WordN n -> WordN n Source #

symShiftNegated :: WordN n -> WordN n -> WordN n Source #

(forall (n :: Nat). (KnownNat n, 1 <= n) => SymShift (bv n), forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => SymShift (SomeBV bv) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

symShift :: SomeBV bv -> SomeBV bv -> SomeBV bv Source #

symShiftNegated :: SomeBV bv -> SomeBV bv -> SomeBV bv Source #

(KnownNat n, 1 <= n) => SymShift (SymIntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymBV

(KnownNat n, 1 <= n) => SymShift (SymWordN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymBV

newtype DefaultFiniteBitsSymShift a Source #

A newtype wrapper. Use this to derive SymShift for types that have FiniteBits instances.

Instances

Instances details
Bits a => Bits (DefaultFiniteBitsSymShift a) Source # 
Instance details

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

Methods

(.&.) :: DefaultFiniteBitsSymShift a -> DefaultFiniteBitsSymShift a -> DefaultFiniteBitsSymShift a #

(.|.) :: DefaultFiniteBitsSymShift a -> DefaultFiniteBitsSymShift a -> DefaultFiniteBitsSymShift a #

xor :: DefaultFiniteBitsSymShift a -> DefaultFiniteBitsSymShift a -> DefaultFiniteBitsSymShift a #

complement :: DefaultFiniteBitsSymShift a -> DefaultFiniteBitsSymShift a #

shift :: DefaultFiniteBitsSymShift a -> Int -> DefaultFiniteBitsSymShift a #

rotate :: DefaultFiniteBitsSymShift a -> Int -> DefaultFiniteBitsSymShift a #

zeroBits :: DefaultFiniteBitsSymShift a #

bit :: Int -> DefaultFiniteBitsSymShift a #

setBit :: DefaultFiniteBitsSymShift a -> Int -> DefaultFiniteBitsSymShift a #

clearBit :: DefaultFiniteBitsSymShift a -> Int -> DefaultFiniteBitsSymShift a #

complementBit :: DefaultFiniteBitsSymShift a -> Int -> DefaultFiniteBitsSymShift a #

testBit :: DefaultFiniteBitsSymShift a -> Int -> Bool #

bitSizeMaybe :: DefaultFiniteBitsSymShift a -> Maybe Int #

bitSize :: DefaultFiniteBitsSymShift a -> Int #

isSigned :: DefaultFiniteBitsSymShift a -> Bool #

shiftL :: DefaultFiniteBitsSymShift a -> Int -> DefaultFiniteBitsSymShift a #

unsafeShiftL :: DefaultFiniteBitsSymShift a -> Int -> DefaultFiniteBitsSymShift a #

shiftR :: DefaultFiniteBitsSymShift a -> Int -> DefaultFiniteBitsSymShift a #

unsafeShiftR :: DefaultFiniteBitsSymShift a -> Int -> DefaultFiniteBitsSymShift a #

rotateL :: DefaultFiniteBitsSymShift a -> Int -> DefaultFiniteBitsSymShift a #

rotateR :: DefaultFiniteBitsSymShift a -> Int -> DefaultFiniteBitsSymShift a #

popCount :: DefaultFiniteBitsSymShift a -> Int #

Eq a => Eq (DefaultFiniteBitsSymShift a) Source # 
Instance details

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

(Integral a, FiniteBits a) => SymShift (DefaultFiniteBitsSymShift a) Source # 
Instance details

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