Grisette.IR.SymPrim.Data.BV

Documentation

newtype IntN (n :: Nat)

Symbolic signed bit vectors.

Constructors

IntN

Fields

• unIntN :: Integer

Instances

ToSym Int16 (Sym (IntN 16))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int16 -> Sym (IntN 16)

ToSym Int32 (Sym (IntN 32))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int32 -> Sym (IntN 32)

ToSym Int64 (Sym (IntN 64))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int64 -> Sym (IntN 64)

ToSym Int8 (Sym (IntN 8))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int8 -> Sym (IntN 8)

ToSym Int (Sym (IntN 64))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int -> Sym (IntN 64)

Lift (IntN n :: Type)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

lift :: Quote m => IntN n -> m Exp

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

(KnownNat n, 1 <= n) => Bits (IntN n)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

(.&.) :: IntN n -> IntN n -> IntN n

(.|.) :: IntN n -> IntN n -> IntN n

xor :: IntN n -> IntN n -> IntN n

complement :: IntN n -> IntN n

shift :: IntN n -> Int -> IntN n

rotate :: IntN n -> Int -> IntN n

zeroBits :: IntN n

bit :: Int -> IntN n

setBit :: IntN n -> Int -> IntN n

clearBit :: IntN n -> Int -> IntN n

complementBit :: IntN n -> Int -> IntN n

testBit :: IntN n -> Int -> Bool

bitSizeMaybe :: IntN n -> Maybe Int

bitSize :: IntN n -> Int

isSigned :: IntN n -> Bool

shiftL :: IntN n -> Int -> IntN n

unsafeShiftL :: IntN n -> Int -> IntN n

shiftR :: IntN n -> Int -> IntN n

unsafeShiftR :: IntN n -> Int -> IntN n

rotateL :: IntN n -> Int -> IntN n

rotateR :: IntN n -> Int -> IntN n

popCount :: IntN n -> Int

SupportedPrim (IntN n) => Bits (Sym (IntN n))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(.&.) :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n)

(.|.) :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n)

xor :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n)

complement :: Sym (IntN n) -> Sym (IntN n)

shift :: Sym (IntN n) -> Int -> Sym (IntN n)

rotate :: Sym (IntN n) -> Int -> Sym (IntN n)

zeroBits :: Sym (IntN n)

bit :: Int -> Sym (IntN n)

setBit :: Sym (IntN n) -> Int -> Sym (IntN n)

clearBit :: Sym (IntN n) -> Int -> Sym (IntN n)

complementBit :: Sym (IntN n) -> Int -> Sym (IntN n)

testBit :: Sym (IntN n) -> Int -> Bool

bitSizeMaybe :: Sym (IntN n) -> Maybe Int

bitSize :: Sym (IntN n) -> Int

isSigned :: Sym (IntN n) -> Bool

shiftL :: Sym (IntN n) -> Int -> Sym (IntN n)

unsafeShiftL :: Sym (IntN n) -> Int -> Sym (IntN n)

shiftR :: Sym (IntN n) -> Int -> Sym (IntN n)

unsafeShiftR :: Sym (IntN n) -> Int -> Sym (IntN n)

rotateL :: Sym (IntN n) -> Int -> Sym (IntN n)

rotateR :: Sym (IntN n) -> Int -> Sym (IntN n)

popCount :: Sym (IntN n) -> Int

(KnownNat n, 1 <= n) => FiniteBits (IntN n)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

finiteBitSize :: IntN n -> Int

countLeadingZeros :: IntN n -> Int

countTrailingZeros :: IntN n -> Int

(KnownNat n, 1 <= n) => Bounded (IntN n)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

minBound :: IntN n

maxBound :: IntN n

(KnownNat n, 1 <= n) => Enum (IntN n)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

succ :: IntN n -> IntN n

pred :: IntN n -> IntN n

toEnum :: Int -> IntN n

fromEnum :: IntN n -> Int

enumFrom :: IntN n -> [IntN n]

enumFromThen :: IntN n -> IntN n -> [IntN n]

enumFromTo :: IntN n -> IntN n -> [IntN n]

enumFromThenTo :: IntN n -> IntN n -> IntN n -> [IntN n]

Generic (IntN n)

Defined in Grisette.IR.SymPrim.Data.BV

Associated Types

type Rep (IntN n) :: Type -> Type

Methods

from :: IntN n -> Rep (IntN n) x

to :: Rep (IntN n) x -> IntN n

(KnownNat n, 1 <= n) => Num (IntN n)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

(+) :: IntN n -> IntN n -> IntN n

(-) :: IntN n -> IntN n -> IntN n

(*) :: IntN n -> IntN n -> IntN n

negate :: IntN n -> IntN n

abs :: IntN n -> IntN n

signum :: IntN n -> IntN n

fromInteger :: Integer -> IntN n

SupportedPrim (IntN n) => Num (Sym (IntN n))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(+) :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n)

(-) :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n)

(*) :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n)

negate :: Sym (IntN n) -> Sym (IntN n)

abs :: Sym (IntN n) -> Sym (IntN n)

signum :: Sym (IntN n) -> Sym (IntN n)

fromInteger :: Integer -> Sym (IntN n)

(KnownNat n, 1 <= n) => Integral (IntN n)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

quot :: IntN n -> IntN n -> IntN n

rem :: IntN n -> IntN n -> IntN n

div :: IntN n -> IntN n -> IntN n

mod :: IntN n -> IntN n -> IntN n

quotRem :: IntN n -> IntN n -> (IntN n, IntN n)

divMod :: IntN n -> IntN n -> (IntN n, IntN n)

toInteger :: IntN n -> Integer

(KnownNat n, 1 <= n) => Real (IntN n)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

toRational :: IntN n -> Rational

(KnownNat n, 1 <= n) => Show (IntN n)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

showsPrec :: Int -> IntN n -> ShowS

show :: IntN n -> String

showList :: [IntN n] -> ShowS

NFData (IntN n)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

rnf :: IntN n -> ()

Eq (IntN n)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

(==) :: IntN n -> IntN n -> Bool

(/=) :: IntN n -> IntN n -> Bool

(KnownNat n, 1 <= n) => Ord (IntN n)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

compare :: IntN n -> IntN n -> Ordering

(<) :: IntN n -> IntN n -> Bool

(<=) :: IntN n -> IntN n -> Bool

(>) :: IntN n -> IntN n -> Bool

(>=) :: IntN n -> IntN n -> Bool

max :: IntN n -> IntN n -> IntN n

min :: IntN n -> IntN n -> IntN n

SupportedPrim (IntN n) => SEq (Sym (IntN n))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(==~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool

(/=~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool

SupportedPrim (IntN n) => SOrd (Sym (IntN n))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(<~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool

(<=~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool

(>~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool

(>=~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool

symCompare :: Sym (IntN n) -> Sym (IntN n) -> UnionM Ordering

(KnownNat w, 1 <= w) => SupportedPrim (IntN w)

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type PrimConstraint (IntN w)

Methods

withPrim :: proxy (IntN w) -> (PrimConstraint (IntN w) => a) -> a

termCache :: Cache (Term (IntN w))

pformatCon :: IntN w -> String

pformatSym :: TypedSymbol (IntN w) -> String

defaultValue :: IntN w

defaultValueDynamic :: proxy (IntN w) -> ModelValue

Hashable (IntN n)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

hashWithSalt :: Int -> IntN n -> Int

hash :: IntN n -> Int

ToCon (Sym (IntN 8)) Int8

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 8) -> Maybe Int8

ToCon (Sym (IntN 16)) Int16

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 16) -> Maybe Int16

ToCon (Sym (IntN 32)) Int32

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 32) -> Maybe Int32

ToCon (Sym (IntN 64)) Int64

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 64) -> Maybe Int64

ToCon (Sym (IntN 64)) Int

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 64) -> Maybe Int

(KnownNat n, 1 <= n, KnownNat ix, KnownNat w, 1 <= w, (ix + w) <= n) => BVSelect (IntN n) ix w (IntN w)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

bvselect :: proxy ix -> proxy w -> IntN n -> IntN w

(KnownNat ix, KnownNat w, KnownNat ow, (ix + w) <= ow, 1 <= ow, 1 <= w) => BVSelect (Sym (IntN ow)) ix w (Sym (IntN w))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvselect :: proxy ix -> proxy w -> Sym (IntN ow) -> Sym (IntN w)

(KnownNat n, 1 <= n, KnownNat r, n <= r) => BVExtend (IntN n) r (IntN r)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

bvzeroExtend :: proxy r -> IntN n -> IntN r

bvsignExtend :: proxy r -> IntN n -> IntN r

bvextend :: proxy r -> IntN n -> IntN r

(KnownNat w, KnownNat w', 1 <= w, 1 <= w', w <= w', (w + 1) <= w', 1 <= (w' - w), KnownNat (w' - w)) => BVExtend (Sym (IntN w)) w' (Sym (IntN w'))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvzeroExtend :: proxy w' -> Sym (IntN w) -> Sym (IntN w')

bvsignExtend :: proxy w' -> Sym (IntN w) -> Sym (IntN w')

bvextend :: proxy w' -> Sym (IntN w) -> Sym (IntN w')

(KnownNat n, 1 <= n, KnownNat m, 1 <= m, KnownNat w, 1 <= w, w ~ (n + m)) => BVConcat (IntN n) (IntN m) (IntN w)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

bvconcat :: IntN n -> IntN m -> IntN w

(KnownNat w', KnownNat n, KnownNat w, w' ~ (n + w), 1 <= n, 1 <= w, 1 <= w') => BVConcat (Sym (IntN n)) (Sym (IntN w)) (Sym (IntN w'))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvconcat :: Sym (IntN n) -> Sym (IntN w) -> Sym (IntN w')

type Rep (IntN n)

Defined in Grisette.IR.SymPrim.Data.BV

type Rep (IntN n) = D1 ('MetaData "IntN" "Grisette.IR.SymPrim.Data.BV" "grisette-0.1.0.0-7JmpZvRpjzaDDLSSjCfe9O" 'True) (C1 ('MetaCons "IntN" 'PrefixI 'True) (S1 ('MetaSel ('Just "unIntN") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))

type PrimConstraint (IntN w)

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

type PrimConstraint (IntN w) = (KnownNat w, 1 <= w)

newtype WordN (n :: Nat)

Symbolic unsigned bit vectors.

Constructors

WordN

Fields

• unWordN :: Integer

Instances

ToSym Word16 (Sym (WordN 16))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word16 -> Sym (WordN 16)

ToSym Word32 (Sym (WordN 32))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word32 -> Sym (WordN 32)

ToSym Word64 (Sym (WordN 64))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word64 -> Sym (WordN 64)

ToSym Word8 (Sym (WordN 8))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word8 -> Sym (WordN 8)

ToSym Word (Sym (WordN 64))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word -> Sym (WordN 64)

Lift (WordN n :: Type)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

lift :: Quote m => WordN n -> m Exp

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

(KnownNat n, 1 <= n) => Bits (WordN n)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

(.&.) :: WordN n -> WordN n -> WordN n

(.|.) :: WordN n -> WordN n -> WordN n

xor :: WordN n -> WordN n -> WordN n

complement :: WordN n -> WordN n

shift :: WordN n -> Int -> WordN n

rotate :: WordN n -> Int -> WordN n

zeroBits :: WordN n

bit :: Int -> WordN n

setBit :: WordN n -> Int -> WordN n

clearBit :: WordN n -> Int -> WordN n

complementBit :: WordN n -> Int -> WordN n

testBit :: WordN n -> Int -> Bool

bitSizeMaybe :: WordN n -> Maybe Int

bitSize :: WordN n -> Int

isSigned :: WordN n -> Bool

shiftL :: WordN n -> Int -> WordN n

unsafeShiftL :: WordN n -> Int -> WordN n

shiftR :: WordN n -> Int -> WordN n

unsafeShiftR :: WordN n -> Int -> WordN n

rotateL :: WordN n -> Int -> WordN n

rotateR :: WordN n -> Int -> WordN n

popCount :: WordN n -> Int

SupportedPrim (WordN n) => Bits (Sym (WordN n))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(.&.) :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n)

(.|.) :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n)

xor :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n)

complement :: Sym (WordN n) -> Sym (WordN n)

shift :: Sym (WordN n) -> Int -> Sym (WordN n)

rotate :: Sym (WordN n) -> Int -> Sym (WordN n)

zeroBits :: Sym (WordN n)

bit :: Int -> Sym (WordN n)

setBit :: Sym (WordN n) -> Int -> Sym (WordN n)

clearBit :: Sym (WordN n) -> Int -> Sym (WordN n)

complementBit :: Sym (WordN n) -> Int -> Sym (WordN n)

testBit :: Sym (WordN n) -> Int -> Bool

bitSizeMaybe :: Sym (WordN n) -> Maybe Int

bitSize :: Sym (WordN n) -> Int

isSigned :: Sym (WordN n) -> Bool

shiftL :: Sym (WordN n) -> Int -> Sym (WordN n)

unsafeShiftL :: Sym (WordN n) -> Int -> Sym (WordN n)

shiftR :: Sym (WordN n) -> Int -> Sym (WordN n)

unsafeShiftR :: Sym (WordN n) -> Int -> Sym (WordN n)

rotateL :: Sym (WordN n) -> Int -> Sym (WordN n)

rotateR :: Sym (WordN n) -> Int -> Sym (WordN n)

popCount :: Sym (WordN n) -> Int

(KnownNat n, 1 <= n) => FiniteBits (WordN n)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

finiteBitSize :: WordN n -> Int

countLeadingZeros :: WordN n -> Int

countTrailingZeros :: WordN n -> Int

(KnownNat n, 1 <= n) => Bounded (WordN n)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

minBound :: WordN n

maxBound :: WordN n

(KnownNat n, 1 <= n) => Enum (WordN n)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

succ :: WordN n -> WordN n

pred :: WordN n -> WordN n

toEnum :: Int -> WordN n

fromEnum :: WordN n -> Int

enumFrom :: WordN n -> [WordN n]

enumFromThen :: WordN n -> WordN n -> [WordN n]

enumFromTo :: WordN n -> WordN n -> [WordN n]

enumFromThenTo :: WordN n -> WordN n -> WordN n -> [WordN n]

Generic (WordN n)

Defined in Grisette.IR.SymPrim.Data.BV

Associated Types

type Rep (WordN n) :: Type -> Type

Methods

from :: WordN n -> Rep (WordN n) x

to :: Rep (WordN n) x -> WordN n

(KnownNat n, 1 <= n) => Num (WordN n)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

(+) :: WordN n -> WordN n -> WordN n

(-) :: WordN n -> WordN n -> WordN n

(*) :: WordN n -> WordN n -> WordN n

negate :: WordN n -> WordN n

abs :: WordN n -> WordN n

signum :: WordN n -> WordN n

fromInteger :: Integer -> WordN n

SupportedPrim (WordN n) => Num (Sym (WordN n))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(+) :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n)

(-) :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n)

(*) :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n)

negate :: Sym (WordN n) -> Sym (WordN n)

abs :: Sym (WordN n) -> Sym (WordN n)

signum :: Sym (WordN n) -> Sym (WordN n)

fromInteger :: Integer -> Sym (WordN n)

(KnownNat n, 1 <= n) => Integral (WordN n)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

quot :: WordN n -> WordN n -> WordN n

rem :: WordN n -> WordN n -> WordN n

div :: WordN n -> WordN n -> WordN n

mod :: WordN n -> WordN n -> WordN n

quotRem :: WordN n -> WordN n -> (WordN n, WordN n)

divMod :: WordN n -> WordN n -> (WordN n, WordN n)

toInteger :: WordN n -> Integer

(KnownNat n, 1 <= n) => Real (WordN n)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

toRational :: WordN n -> Rational

(KnownNat n, 1 <= n) => Show (WordN n)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

showsPrec :: Int -> WordN n -> ShowS

show :: WordN n -> String

showList :: [WordN n] -> ShowS

NFData (WordN n)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

rnf :: WordN n -> ()

Eq (WordN n)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

(==) :: WordN n -> WordN n -> Bool

(/=) :: WordN n -> WordN n -> Bool

Ord (WordN n)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

compare :: WordN n -> WordN n -> Ordering

(<) :: WordN n -> WordN n -> Bool

(<=) :: WordN n -> WordN n -> Bool

(>) :: WordN n -> WordN n -> Bool

(>=) :: WordN n -> WordN n -> Bool

max :: WordN n -> WordN n -> WordN n

min :: WordN n -> WordN n -> WordN n

SupportedPrim (WordN n) => SEq (Sym (WordN n))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(==~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool

(/=~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool

SupportedPrim (WordN n) => SOrd (Sym (WordN n))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(<~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool

(<=~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool

(>~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool

(>=~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool

symCompare :: Sym (WordN n) -> Sym (WordN n) -> UnionM Ordering

(KnownNat w, 1 <= w) => SupportedPrim (WordN w)

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type PrimConstraint (WordN w)

Methods

withPrim :: proxy (WordN w) -> (PrimConstraint (WordN w) => a) -> a

termCache :: Cache (Term (WordN w))

pformatCon :: WordN w -> String

pformatSym :: TypedSymbol (WordN w) -> String

defaultValue :: WordN w

defaultValueDynamic :: proxy (WordN w) -> ModelValue

Hashable (WordN n)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

hashWithSalt :: Int -> WordN n -> Int

hash :: WordN n -> Int

ToCon (Sym (WordN 8)) Word8

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 8) -> Maybe Word8

ToCon (Sym (WordN 16)) Word16

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 16) -> Maybe Word16

ToCon (Sym (WordN 32)) Word32

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 32) -> Maybe Word32

ToCon (Sym (WordN 64)) Word64

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 64) -> Maybe Word64

ToCon (Sym (WordN 64)) Word

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 64) -> Maybe Word

(KnownNat n, 1 <= n, KnownNat ix, KnownNat w, 1 <= w, (ix + w) <= n) => BVSelect (WordN n) ix w (WordN w)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

bvselect :: proxy ix -> proxy w -> WordN n -> WordN w

(KnownNat ix, KnownNat w, KnownNat ow, (ix + w) <= ow, 1 <= ow, 1 <= w) => BVSelect (Sym (WordN ow)) ix w (Sym (WordN w))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvselect :: proxy ix -> proxy w -> Sym (WordN ow) -> Sym (WordN w)

(KnownNat n, 1 <= n, KnownNat r, n <= r) => BVExtend (WordN n) r (WordN r)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

bvzeroExtend :: proxy r -> WordN n -> WordN r

bvsignExtend :: proxy r -> WordN n -> WordN r

bvextend :: proxy r -> WordN n -> WordN r

(KnownNat w, KnownNat w', 1 <= w, 1 <= w', (w + 1) <= w', w <= w', 1 <= (w' - w), KnownNat (w' - w)) => BVExtend (Sym (WordN w)) w' (Sym (WordN w'))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvzeroExtend :: proxy w' -> Sym (WordN w) -> Sym (WordN w')

bvsignExtend :: proxy w' -> Sym (WordN w) -> Sym (WordN w')

bvextend :: proxy w' -> Sym (WordN w) -> Sym (WordN w')

(KnownNat n, 1 <= n, KnownNat m, 1 <= m, KnownNat w, 1 <= w, w ~ (n + m)) => BVConcat (WordN n) (WordN m) (WordN w)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

bvconcat :: WordN n -> WordN m -> WordN w

(KnownNat w', KnownNat n, KnownNat w, w' ~ (n + w), 1 <= n, 1 <= w, 1 <= w') => BVConcat (Sym (WordN n)) (Sym (WordN w)) (Sym (WordN w'))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvconcat :: Sym (WordN n) -> Sym (WordN w) -> Sym (WordN w')

type Rep (WordN n)

Defined in Grisette.IR.SymPrim.Data.BV

type Rep (WordN n) = D1 ('MetaData "WordN" "Grisette.IR.SymPrim.Data.BV" "grisette-0.1.0.0-7JmpZvRpjzaDDLSSjCfe9O" 'True) (C1 ('MetaCons "WordN" 'PrefixI 'True) (S1 ('MetaSel ('Just "unWordN") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))

type PrimConstraint (WordN w)

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

type PrimConstraint (WordN w) = (KnownNat w, 1 <= w)