Grisette.Internal.SymPrim.BV

Documentation

data BitwidthMismatch

An exception that would be thrown when operations are performed on incompatible bit widths.

Constructors

BitwidthMismatch

Instances

Exception BitwidthMismatch

Defined in Grisette.Internal.SymPrim.BV

Methods

toException :: BitwidthMismatch -> SomeException

fromException :: SomeException -> Maybe BitwidthMismatch

displayException :: BitwidthMismatch -> String

Generic BitwidthMismatch

Defined in Grisette.Internal.SymPrim.BV

Associated Types

type Rep BitwidthMismatch :: Type -> Type

Methods

from :: BitwidthMismatch -> Rep BitwidthMismatch x

to :: Rep BitwidthMismatch x -> BitwidthMismatch

Show BitwidthMismatch

Defined in Grisette.Internal.SymPrim.BV

Methods

showsPrec :: Int -> BitwidthMismatch -> ShowS

show :: BitwidthMismatch -> String

showList :: [BitwidthMismatch] -> ShowS

Eq BitwidthMismatch

Defined in Grisette.Internal.SymPrim.BV

Methods

(==) :: BitwidthMismatch -> BitwidthMismatch -> Bool

(/=) :: BitwidthMismatch -> BitwidthMismatch -> Bool

Ord BitwidthMismatch

Defined in Grisette.Internal.SymPrim.BV

Methods

compare :: BitwidthMismatch -> BitwidthMismatch -> Ordering

(<) :: BitwidthMismatch -> BitwidthMismatch -> Bool

(<=) :: BitwidthMismatch -> BitwidthMismatch -> Bool

(>) :: BitwidthMismatch -> BitwidthMismatch -> Bool

(>=) :: BitwidthMismatch -> BitwidthMismatch -> Bool

max :: BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch

min :: BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch

Mergeable BitwidthMismatch

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

Methods

rootStrategy :: MergingStrategy BitwidthMismatch

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching 'Sym m) => UnifiedSafeDivision 'Sym (Either BitwidthMismatch ArithException) SomeSymIntN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeDivision

Methods

withBaseSafeDivision :: (SafeDivision (Either BitwidthMismatch ArithException) SomeSymIntN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching 'Sym m) => UnifiedSafeDivision 'Sym (Either BitwidthMismatch ArithException) SomeSymWordN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeDivision

Methods

withBaseSafeDivision :: (SafeDivision (Either BitwidthMismatch ArithException) SomeSymWordN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching mode m) => UnifiedSafeDivision mode (Either BitwidthMismatch ArithException) SomeIntN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeDivision

Methods

withBaseSafeDivision :: (SafeDivision (Either BitwidthMismatch ArithException) SomeIntN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching mode m) => UnifiedSafeDivision mode (Either BitwidthMismatch ArithException) SomeWordN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeDivision

Methods

withBaseSafeDivision :: (SafeDivision (Either BitwidthMismatch ArithException) SomeWordN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching 'Sym m) => UnifiedSafeLinearArith 'Sym (Either BitwidthMismatch ArithException) SomeSymIntN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeLinearArith

Methods

withBaseSafeLinearArith :: (SafeLinearArith (Either BitwidthMismatch ArithException) SomeSymIntN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching 'Sym m) => UnifiedSafeLinearArith 'Sym (Either BitwidthMismatch ArithException) SomeSymWordN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeLinearArith

Methods

withBaseSafeLinearArith :: (SafeLinearArith (Either BitwidthMismatch ArithException) SomeSymWordN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching mode m) => UnifiedSafeLinearArith mode (Either BitwidthMismatch ArithException) SomeIntN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeLinearArith

Methods

withBaseSafeLinearArith :: (SafeLinearArith (Either BitwidthMismatch ArithException) SomeIntN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching mode m) => UnifiedSafeLinearArith mode (Either BitwidthMismatch ArithException) SomeWordN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeLinearArith

Methods

withBaseSafeLinearArith :: (SafeLinearArith (Either BitwidthMismatch ArithException) SomeWordN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching 'Sym m) => UnifiedSafeSymRotate 'Sym (Either BitwidthMismatch ArithException) SomeSymIntN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymRotate

Methods

withBaseSafeSymRotate :: (SafeSymRotate (Either BitwidthMismatch ArithException) SomeSymIntN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching 'Sym m) => UnifiedSafeSymRotate 'Sym (Either BitwidthMismatch ArithException) SomeSymWordN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymRotate

Methods

withBaseSafeSymRotate :: (SafeSymRotate (Either BitwidthMismatch ArithException) SomeSymWordN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymRotate mode (Either BitwidthMismatch ArithException) SomeIntN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymRotate

Methods

withBaseSafeSymRotate :: (SafeSymRotate (Either BitwidthMismatch ArithException) SomeIntN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymRotate mode (Either BitwidthMismatch ArithException) SomeWordN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymRotate

Methods

withBaseSafeSymRotate :: (SafeSymRotate (Either BitwidthMismatch ArithException) SomeWordN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching 'Sym m) => UnifiedSafeSymShift 'Sym (Either BitwidthMismatch ArithException) SomeSymIntN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymShift

Methods

withBaseSafeSymShift :: (SafeSymShift (Either BitwidthMismatch ArithException) SomeSymIntN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching 'Sym m) => UnifiedSafeSymShift 'Sym (Either BitwidthMismatch ArithException) SomeSymWordN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymShift

Methods

withBaseSafeSymShift :: (SafeSymShift (Either BitwidthMismatch ArithException) SomeSymWordN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymShift mode (Either BitwidthMismatch ArithException) SomeIntN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymShift

Methods

withBaseSafeSymShift :: (SafeSymShift (Either BitwidthMismatch ArithException) SomeIntN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymShift mode (Either BitwidthMismatch ArithException) SomeWordN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymShift

Methods

withBaseSafeSymShift :: (SafeSymShift (Either BitwidthMismatch ArithException) SomeWordN m => r) -> r

(forall (n :: Nat). (KnownNat n, 1 <= n) => SafeDivision e (bv n) (ExceptT e m), MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e) => SafeDivision (Either BitwidthMismatch e) (SomeBV bv) m

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

safeDiv :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeMod :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeDivMod :: SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)

safeQuot :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeRem :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeQuotRem :: SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)

(forall (n :: Nat). (KnownNat n, 1 <= n) => SafeLinearArith e (bv n) (ExceptT e m), MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e) => SafeLinearArith (Either BitwidthMismatch e) (SomeBV bv) m

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

safeAdd :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeNeg :: SomeBV bv -> m (SomeBV bv)

safeSub :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

(forall (n :: Nat). (KnownNat n, 1 <= n) => SafeSymRotate e (bv n) (ExceptT e m), MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e) => SafeSymRotate (Either BitwidthMismatch e) (SomeBV bv) m

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

safeSymRotateL :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeSymRotateR :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

(forall (n :: Nat). (KnownNat n, 1 <= n) => SafeSymShift e (bv n) (ExceptT e m), MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e) => SafeSymShift (Either BitwidthMismatch e) (SomeBV bv) m

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

safeSymShiftL :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeSymShiftR :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeSymStrictShiftL :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeSymStrictShiftR :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

type Rep BitwidthMismatch

Defined in Grisette.Internal.SymPrim.BV

type Rep BitwidthMismatch = D1 ('MetaData "BitwidthMismatch" "Grisette.Internal.SymPrim.BV" "grisette-0.7.0.0-3DYM4wcz8TiF8sSQ1gvVO8" 'False) (C1 ('MetaCons "BitwidthMismatch" 'PrefixI 'False) (U1 :: Type -> Type))

newtype IntN (n :: Nat)

Signed bit vector type. Indexed with the bit width. Signedness affects the semantics of the operations, including comparison/extension, etc.

>>> :set -XOverloadedStrings -XDataKinds -XBinaryLiterals
>>> 3 + 5 :: IntN 5
0b01000
>>> sizedBVConcat (0b101 :: IntN 3) (0b110 :: IntN 3)
0b101110
>>> sizedBVExt (Proxy @6) (0b101 :: IntN 3)
0b111101
>>> (8 :: IntN 4) < (7 :: IntN 4)
True

More operations are available. Please refer to Grisette.Core for more information.

Constructors

IntN

Fields

• unIntN :: Integer

Instances

SizedBV IntN

Defined in Grisette.Internal.SymPrim.BV

Methods

sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => IntN l -> IntN r -> IntN (l + r)

sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r

sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r

sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r

sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> IntN n -> IntN w

sizedBVFromIntegral :: forall a (n :: Nat). (Integral a, KnownNat n, 1 <= n) => a -> IntN n

PEvalBVTerm IntN

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval

Methods

pevalBVConcatTerm :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => Term (IntN l) -> Term (IntN r) -> Term (IntN (l + r))

pevalBVExtendTerm :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => Bool -> proxy r -> Term (IntN l) -> Term (IntN r)

pevalBVSelectTerm :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> Term (IntN n) -> Term (IntN w)

sbvBVConcatTerm :: forall (n :: Nat) (l :: Nat) (r :: Nat) p0 p1 p2. (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r) => p0 n -> p1 l -> p2 r -> SBVType n (IntN l) -> SBVType n (IntN r) -> SBVType n (IntN (l + r))

sbvBVExtendTerm :: forall (n :: Nat) (l :: Nat) (r :: Nat) p0 p1 p2. (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => p0 n -> p1 l -> p2 r -> Bool -> SBVType n (IntN l) -> SBVType n (IntN r)

sbvBVSelectTerm :: forall (int :: Nat) (ix :: Nat) (w :: Nat) (n :: Nat) p0 p1 p2 p3. (KnownIsZero int, KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w, (ix + w) <= n) => p0 int -> p1 ix -> p2 w -> p3 n -> SBVType int (IntN n) -> SBVType int (IntN w)

BitCast IntN32 Float

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN32 -> Float

BitCast IntN64 Double

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN64 -> Double

BitCast Double IntN64

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Double -> IntN64

BitCast Float IntN32

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Float -> IntN32

PEvalBVSignConversionTerm WordN IntN

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval

Methods

pevalBVToSignedTerm :: forall (n :: Nat). (KnownNat n, 1 <= n) => Term (WordN n) -> Term (IntN n)

pevalBVToUnsignedTerm :: forall (n :: Nat). (KnownNat n, 1 <= n) => Term (IntN n) -> Term (WordN n)

withSbvSignConversionTermConstraint :: forall (n :: Nat) (integerBitwidth :: Nat) p q r. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => p n -> q integerBitwidth -> ((Integral (NonFuncSBVBaseType integerBitwidth (WordN n)), Integral (NonFuncSBVBaseType integerBitwidth (IntN n))) => r) -> r

sbvToSigned :: forall (n :: Nat) (integerBitwidth :: Nat) o p q. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => o WordN -> p n -> q integerBitwidth -> SBVType integerBitwidth (WordN n) -> SBVType integerBitwidth (IntN n)

sbvToUnsigned :: forall (n :: Nat) (integerBitwidth :: Nat) o p q. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => o IntN -> p n -> q integerBitwidth -> SBVType integerBitwidth (IntN n) -> SBVType integerBitwidth (WordN n)

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeDivision mode ArithException (IntN n) m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeDivision

Methods

withBaseSafeDivision :: (SafeDivision ArithException (IntN n) m => r) -> r

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeLinearArith mode ArithException (IntN n) m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeLinearArith

Methods

withBaseSafeLinearArith :: (SafeLinearArith ArithException (IntN n) m => r) -> r

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeSymRotate mode ArithException (IntN n) m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymRotate

Methods

withBaseSafeSymRotate :: (SafeSymRotate ArithException (IntN n) m => r) -> r

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeSymShift mode ArithException (IntN n) m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymShift

Methods

withBaseSafeSymShift :: (SafeSymShift ArithException (IntN n) m => r) -> r

BitCast Int16 (IntN 16)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Int16 -> IntN 16

BitCast Int32 (IntN 32)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Int32 -> IntN 32

BitCast Int64 (IntN 64)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Int64 -> IntN 64

BitCast Int8 (IntN 8)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Int8 -> IntN 8

BitCast Word16 (IntN 16)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Word16 -> IntN 16

BitCast Word32 (IntN 32)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Word32 -> IntN 32

BitCast Word64 (IntN 64)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Word64 -> IntN 64

BitCast Word8 (IntN 8)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Word8 -> IntN 8

(Typeable mode, KnownNat n, 1 <= n) => UnifiedSymEq mode (IntN n)

Defined in Grisette.Unified.Internal.Class.UnifiedSymEq

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (IntN n)) (SymEq (IntN n)) => r) -> r

(Typeable mode, KnownNat n, 1 <= n) => UnifiedSymOrd mode (IntN n)

Defined in Grisette.Unified.Internal.Class.UnifiedSymOrd

Methods

withBaseSymOrd :: (If (IsConMode mode) (Ord (IntN n)) (SymOrd (IntN n)) => r) -> r

Lift (IntN n :: Type)

Defined in Grisette.Internal.SymPrim.BV

Methods

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

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

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeDivision ArithException (IntN n) m

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

Methods

safeDiv :: IntN n -> IntN n -> m (IntN n)

safeMod :: IntN n -> IntN n -> m (IntN n)

safeDivMod :: IntN n -> IntN n -> m (IntN n, IntN n)

safeQuot :: IntN n -> IntN n -> m (IntN n)

safeRem :: IntN n -> IntN n -> m (IntN n)

safeQuotRem :: IntN n -> IntN n -> m (IntN n, IntN n)

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (IntN n) m

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

Methods

safeAdd :: IntN n -> IntN n -> m (IntN n)

safeNeg :: IntN n -> m (IntN n)

safeSub :: IntN n -> IntN n -> m (IntN n)

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymRotate ArithException (IntN n) m

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

Methods

safeSymRotateL :: IntN n -> IntN n -> m (IntN n)

safeSymRotateR :: IntN n -> IntN n -> m (IntN n)

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymShift ArithException (IntN n) m

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

Methods

safeSymShiftL :: IntN n -> IntN n -> m (IntN n)

safeSymShiftR :: IntN n -> IntN n -> m (IntN n)

safeSymStrictShiftL :: IntN n -> IntN n -> m (IntN n)

safeSymStrictShiftR :: IntN n -> IntN n -> m (IntN n)

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching mode m) => UnifiedSafeDivision mode (Either BitwidthMismatch ArithException) SomeIntN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeDivision

Methods

withBaseSafeDivision :: (SafeDivision (Either BitwidthMismatch ArithException) SomeIntN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching mode m) => UnifiedSafeLinearArith mode (Either BitwidthMismatch ArithException) SomeIntN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeLinearArith

Methods

withBaseSafeLinearArith :: (SafeLinearArith (Either BitwidthMismatch ArithException) SomeIntN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymRotate mode (Either BitwidthMismatch ArithException) SomeIntN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymRotate

Methods

withBaseSafeSymRotate :: (SafeSymRotate (Either BitwidthMismatch ArithException) SomeIntN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymShift mode (Either BitwidthMismatch ArithException) SomeIntN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymShift

Methods

withBaseSafeSymShift :: (SafeSymShift (Either BitwidthMismatch ArithException) SomeIntN m => r) -> r

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

Defined in Grisette.Internal.SymPrim.BV

Methods

arbitrary :: Gen (IntN n)

shrink :: IntN n -> [IntN n]

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

Defined in Grisette.Internal.SymPrim.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

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

Defined in Grisette.Internal.SymPrim.BV

Methods

finiteBitSize :: IntN n -> Int

countLeadingZeros :: IntN n -> Int

countTrailingZeros :: IntN n -> Int

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

Defined in Grisette.Internal.SymPrim.BV

Methods

minBound :: IntN n

maxBound :: IntN n

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

Defined in Grisette.Internal.SymPrim.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.Internal.SymPrim.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.Internal.SymPrim.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

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

Defined in Grisette.Internal.SymPrim.BV

Methods

readsPrec :: Int -> ReadS (IntN n)

readList :: ReadS [IntN n]

readPrec :: ReadPrec (IntN n)

readListPrec :: ReadPrec [IntN n]

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

Defined in Grisette.Internal.SymPrim.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.Internal.SymPrim.BV

Methods

toRational :: IntN n -> Rational

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

Defined in Grisette.Internal.SymPrim.BV

Methods

showsPrec :: Int -> IntN n -> ShowS

show :: IntN n -> String

showList :: [IntN n] -> ShowS

NFData (IntN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

rnf :: IntN n -> ()

Eq (IntN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

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

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

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

Defined in Grisette.Internal.SymPrim.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

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

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

Methods

evalSym :: Bool -> Model -> IntN n -> IntN n

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

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

Methods

extractSym :: IntN n -> SymbolSet

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

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

Methods

rootStrategy :: MergingStrategy (IntN n)

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

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

Methods

pformat :: IntN n -> Doc ann

pformatPrec :: Int -> IntN n -> Doc ann

pformatList :: [IntN n] -> Doc ann

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

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

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> IntN n -> IntN n

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

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

Methods

(.==) :: IntN n -> IntN n -> SymBool

(./=) :: IntN n -> IntN n -> SymBool

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

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

Methods

(.<) :: IntN n -> IntN n -> SymBool

(.<=) :: IntN n -> IntN n -> SymBool

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

(.>=) :: IntN n -> IntN n -> SymBool

symCompare :: IntN n -> IntN n -> Union Ordering

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

Defined in Grisette.Internal.SymPrim.BV

Methods

symRotate :: IntN n -> IntN n -> IntN n

symRotateNegated :: IntN n -> IntN n -> IntN n

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

Defined in Grisette.Internal.SymPrim.BV

Methods

symShift :: IntN n -> IntN n -> IntN n

symShiftNegated :: IntN n -> IntN n -> IntN n

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

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: IntN n -> [SomeSym] -> [SomeSym]

allSyms :: IntN n -> [SomeSym]

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type NonFuncSBVBaseType n (IntN w)

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitwiseTerm

Methods

pevalAndBitsTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)

pevalOrBitsTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)

pevalXorBitsTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)

pevalComplementBitsTerm :: Term (IntN n) -> Term (IntN n)

withSbvBitwiseTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (Bits (SBVType n0 (IntN n)) => r) -> r

sbvAndBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

sbvOrBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

sbvXorBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

sbvComplementBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalDivModIntegralTerm

Methods

pevalDivIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)

pevalModIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)

pevalQuotIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)

pevalRemIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)

withSbvDivModIntegralTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SDivisible (SBVType n0 (IntN n)) => r) -> r

sbvDivIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

sbvModIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

sbvQuotIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

sbvRemIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm

Methods

pevalAddNumTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)

pevalNegNumTerm :: Term (IntN n) -> Term (IntN n)

pevalMulNumTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)

pevalAbsNumTerm :: Term (IntN n) -> Term (IntN n)

pevalSignumNumTerm :: Term (IntN n) -> Term (IntN n)

withSbvNumTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (Num (SBVType n0 (IntN n)) => r) -> r

sbvAddNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

sbvNegNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

sbvMulNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

sbvAbsNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

sbvSignumNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm

Methods

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

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

withSbvOrdTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (OrdSymbolic (SBVType n0 (IntN n)) => r) -> r

sbvLtOrdTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBV Bool

sbvLeOrdTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBV Bool

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalRotateTerm

Methods

pevalRotateLeftTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)

pevalRotateRightTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)

withSbvRotateTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SIntegral (NonFuncSBVBaseType n0 (IntN n)) => r) -> r

sbvRotateLeftTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

sbvRotateRightTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalShiftTerm

Methods

pevalShiftLeftTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)

pevalShiftRightTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)

withSbvShiftTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SIntegral (NonFuncSBVBaseType n0 (IntN n)) => r) -> r

sbvShiftLeftTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

sbvShiftRightTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type SBVType n (IntN w)

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Methods

conNonFuncSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> IntN w -> SBV (NonFuncSBVBaseType n (IntN w))

symNonFuncSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBV (NonFuncSBVBaseType n (IntN w)))

withNonFuncPrim :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> ((SymVal (NonFuncSBVBaseType n (IntN w)), EqSymbolic (SBVType n (IntN w)), Mergeable (SBVType n (IntN w)), SMTDefinable (SBVType n (IntN w)), Mergeable (SBVType n (IntN w)), SBVType n (IntN w) ~ SBV (NonFuncSBVBaseType n (IntN w)), PrimConstraint n (IntN w)) => r) -> r

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Methods

termCache :: Cache (Term (IntN w))

pformatCon :: IntN w -> String

pformatSym :: TypedSymbol (IntN w) -> String

defaultValue :: IntN w

defaultValueDynamic :: proxy (IntN w) -> ModelValue

pevalITETerm :: Term Bool -> Term (IntN w) -> Term (IntN w) -> Term (IntN w)

pevalEqTerm :: Term (IntN w) -> Term (IntN w) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> IntN w -> SBVType n (IntN w)

symSBVName :: TypedSymbol (IntN w) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (IntN w))

withPrim :: forall (n :: Nat) p a. KnownIsZero n => p n -> ((PrimConstraint n (IntN w), SMTDefinable (SBVType n (IntN w)), Mergeable (SBVType n (IntN w)), Typeable (SBVType n (IntN w))) => a) -> a

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (IntN w) -> SBVType n (IntN w) -> SBVType n (IntN w)

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (IntN w) -> SBVType n (IntN w) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> IntN w

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type PrimConstraint n (IntN w)

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

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type SymType (IntN n)

Hashable (IntN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

hashWithSalt :: Int -> IntN n -> Int

hash :: IntN n -> Int

BitCast (IntN 8) Int8

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 8 -> Int8

BitCast (IntN 8) Word8

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 8 -> Word8

BitCast (IntN 16) Int16

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 16 -> Int16

BitCast (IntN 16) Word16

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 16 -> Word16

BitCast (IntN 32) Int32

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 32 -> Int32

BitCast (IntN 32) Word32

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 32 -> Word32

BitCast (IntN 64) Int64

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 64 -> Int64

BitCast (IntN 64) Word64

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 64 -> Word64

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

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN n -> WordN n

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

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN n -> IntN n

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

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

Methods

fresh :: MonadFresh m => IntN n -> m (Union (IntN n))

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

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

Methods

simpleFresh :: MonadFresh m => IntN n -> m (IntN n)

(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

(KnownNat n, 1 <= n) => Solvable (IntN n) (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

con :: IntN n -> SymIntN n

conView :: SymIntN n -> Maybe (IntN n)

sym :: Symbol -> SymIntN n

ssym :: Identifier -> SymIntN n

isym :: Identifier -> Int -> SymIntN n

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

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

Methods

toCon :: IntN n -> Maybe (IntN n)

(KnownNat n, 1 <= n) => ToCon (SymIntN n) (IntN n)

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

Methods

toCon :: SymIntN n -> Maybe (IntN n)

(KnownNat n, 1 <= n) => ToSym (Union (IntN n)) (SymIntN n)

Defined in Grisette.Internal.Core.Control.Monad.Union

Methods

toSym :: Union (IntN n) -> SymIntN n

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

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

Methods

toSym :: IntN n -> IntN n

(KnownNat n, 1 <= n) => ToSym (IntN n) (SymIntN n)

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

Methods

toSym :: IntN n -> SymIntN n

(KnownNat n, 1 <= n) => LinkedRep (IntN n) (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

underlyingTerm :: SymIntN n -> Term (IntN n)

wrapTerm :: Term (IntN n) -> SymIntN n

(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 (FP eb sb) (IntN r)

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: FP eb sb -> IntN r

type NonFuncSBVBaseType _1 (IntN w)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type NonFuncSBVBaseType _1 (IntN w) = IntN w

type PrimConstraint _1 (IntN w)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

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

type SBVType _1 (IntN w)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type SBVType _1 (IntN w) = SBV (IntN w)

type Rep (IntN n)

Defined in Grisette.Internal.SymPrim.BV

type Rep (IntN n) = D1 ('MetaData "IntN" "Grisette.Internal.SymPrim.BV" "grisette-0.7.0.0-3DYM4wcz8TiF8sSQ1gvVO8" 'True) (C1 ('MetaCons "IntN" 'PrefixI 'True) (S1 ('MetaSel ('Just "unIntN") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))

type SymType (IntN n)

Defined in Grisette.Internal.SymPrim.SymBV

type SymType (IntN n) = SymIntN n

type IntN8 = IntN 8

8-bit signed bit-vector

type IntN16 = IntN 16

16-bit signed bit-vector

type IntN32 = IntN 32

32-bit signed bit-vector

type IntN64 = IntN 64

64-bit signed bit-vector

newtype WordN (n :: Nat)

Unsigned bit vector type. Indexed with the bit width. Signedness affect the semantics of the operations, including comparison/extension, etc.

>>> :set -XOverloadedStrings -XDataKinds -XBinaryLiterals
>>> 3 + 5 :: WordN 5
0b01000
>>> sizedBVConcat (0b101 :: WordN 3) (0b110 :: WordN 3)
0b101110
>>> sizedBVExt (Proxy @6) (0b101 :: WordN 3)
0b000101
>>> (8 :: WordN 4) < (7 :: WordN 4)
False

More operations are available. Please refer to Grisette.Core for more information.

Constructors

WordN

Fields

• unWordN :: Integer

Instances

SizedBV WordN

Defined in Grisette.Internal.SymPrim.BV

Methods

sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => WordN l -> WordN r -> WordN (l + r)

sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r

sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r

sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r

sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> WordN n -> WordN w

sizedBVFromIntegral :: forall a (n :: Nat). (Integral a, KnownNat n, 1 <= n) => a -> WordN n

PEvalBVTerm WordN

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval

Methods

pevalBVConcatTerm :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => Term (WordN l) -> Term (WordN r) -> Term (WordN (l + r))

pevalBVExtendTerm :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => Bool -> proxy r -> Term (WordN l) -> Term (WordN r)

pevalBVSelectTerm :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> Term (WordN n) -> Term (WordN w)

sbvBVConcatTerm :: forall (n :: Nat) (l :: Nat) (r :: Nat) p0 p1 p2. (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r) => p0 n -> p1 l -> p2 r -> SBVType n (WordN l) -> SBVType n (WordN r) -> SBVType n (WordN (l + r))

sbvBVExtendTerm :: forall (n :: Nat) (l :: Nat) (r :: Nat) p0 p1 p2. (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => p0 n -> p1 l -> p2 r -> Bool -> SBVType n (WordN l) -> SBVType n (WordN r)

sbvBVSelectTerm :: forall (int :: Nat) (ix :: Nat) (w :: Nat) (n :: Nat) p0 p1 p2 p3. (KnownIsZero int, KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w, (ix + w) <= n) => p0 int -> p1 ix -> p2 w -> p3 n -> SBVType int (WordN n) -> SBVType int (WordN w)

BitCast WordN32 Float

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN32 -> Float

BitCast WordN64 Double

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN64 -> Double

BitCast Double WordN64

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Double -> WordN64

BitCast Float WordN32

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Float -> WordN32

PEvalBVSignConversionTerm WordN IntN

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval

Methods

pevalBVToSignedTerm :: forall (n :: Nat). (KnownNat n, 1 <= n) => Term (WordN n) -> Term (IntN n)

pevalBVToUnsignedTerm :: forall (n :: Nat). (KnownNat n, 1 <= n) => Term (IntN n) -> Term (WordN n)

withSbvSignConversionTermConstraint :: forall (n :: Nat) (integerBitwidth :: Nat) p q r. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => p n -> q integerBitwidth -> ((Integral (NonFuncSBVBaseType integerBitwidth (WordN n)), Integral (NonFuncSBVBaseType integerBitwidth (IntN n))) => r) -> r

sbvToSigned :: forall (n :: Nat) (integerBitwidth :: Nat) o p q. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => o WordN -> p n -> q integerBitwidth -> SBVType integerBitwidth (WordN n) -> SBVType integerBitwidth (IntN n)

sbvToUnsigned :: forall (n :: Nat) (integerBitwidth :: Nat) o p q. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => o IntN -> p n -> q integerBitwidth -> SBVType integerBitwidth (IntN n) -> SBVType integerBitwidth (WordN n)

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeDivision mode ArithException (WordN n) m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeDivision

Methods

withBaseSafeDivision :: (SafeDivision ArithException (WordN n) m => r) -> r

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeLinearArith mode ArithException (WordN n) m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeLinearArith

Methods

withBaseSafeLinearArith :: (SafeLinearArith ArithException (WordN n) m => r) -> r

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeSymRotate mode ArithException (WordN n) m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymRotate

Methods

withBaseSafeSymRotate :: (SafeSymRotate ArithException (WordN n) m => r) -> r

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeSymShift mode ArithException (WordN n) m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymShift

Methods

withBaseSafeSymShift :: (SafeSymShift ArithException (WordN n) m => r) -> r

BitCast Int16 (WordN 16)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Int16 -> WordN 16

BitCast Int32 (WordN 32)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Int32 -> WordN 32

BitCast Int64 (WordN 64)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Int64 -> WordN 64

BitCast Int8 (WordN 8)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Int8 -> WordN 8

BitCast Word16 (WordN 16)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Word16 -> WordN 16

BitCast Word32 (WordN 32)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Word32 -> WordN 32

BitCast Word64 (WordN 64)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Word64 -> WordN 64

BitCast Word8 (WordN 8)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Word8 -> WordN 8

(Typeable mode, KnownNat n, 1 <= n) => UnifiedSymEq mode (WordN n)

Defined in Grisette.Unified.Internal.Class.UnifiedSymEq

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (WordN n)) (SymEq (WordN n)) => r) -> r

(Typeable mode, KnownNat n, 1 <= n) => UnifiedSymOrd mode (WordN n)

Defined in Grisette.Unified.Internal.Class.UnifiedSymOrd

Methods

withBaseSymOrd :: (If (IsConMode mode) (Ord (WordN n)) (SymOrd (WordN n)) => r) -> r

Lift (WordN n :: Type)

Defined in Grisette.Internal.SymPrim.BV

Methods

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

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

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeDivision ArithException (WordN n) m

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

Methods

safeDiv :: WordN n -> WordN n -> m (WordN n)

safeMod :: WordN n -> WordN n -> m (WordN n)

safeDivMod :: WordN n -> WordN n -> m (WordN n, WordN n)

safeQuot :: WordN n -> WordN n -> m (WordN n)

safeRem :: WordN n -> WordN n -> m (WordN n)

safeQuotRem :: WordN n -> WordN n -> m (WordN n, WordN n)

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (WordN n) m

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

Methods

safeAdd :: WordN n -> WordN n -> m (WordN n)

safeNeg :: WordN n -> m (WordN n)

safeSub :: WordN n -> WordN n -> m (WordN n)

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymRotate ArithException (WordN n) m

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

Methods

safeSymRotateL :: WordN n -> WordN n -> m (WordN n)

safeSymRotateR :: WordN n -> WordN n -> m (WordN n)

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymShift ArithException (WordN n) m

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

Methods

safeSymShiftL :: WordN n -> WordN n -> m (WordN n)

safeSymShiftR :: WordN n -> WordN n -> m (WordN n)

safeSymStrictShiftL :: WordN n -> WordN n -> m (WordN n)

safeSymStrictShiftR :: WordN n -> WordN n -> m (WordN n)

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching mode m) => UnifiedSafeDivision mode (Either BitwidthMismatch ArithException) SomeWordN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeDivision

Methods

withBaseSafeDivision :: (SafeDivision (Either BitwidthMismatch ArithException) SomeWordN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching mode m) => UnifiedSafeLinearArith mode (Either BitwidthMismatch ArithException) SomeWordN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeLinearArith

Methods

withBaseSafeLinearArith :: (SafeLinearArith (Either BitwidthMismatch ArithException) SomeWordN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymRotate mode (Either BitwidthMismatch ArithException) SomeWordN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymRotate

Methods

withBaseSafeSymRotate :: (SafeSymRotate (Either BitwidthMismatch ArithException) SomeWordN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymShift mode (Either BitwidthMismatch ArithException) SomeWordN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymShift

Methods

withBaseSafeSymShift :: (SafeSymShift (Either BitwidthMismatch ArithException) SomeWordN m => r) -> r

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

Defined in Grisette.Internal.SymPrim.BV

Methods

arbitrary :: Gen (WordN n)

shrink :: WordN n -> [WordN n]

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

Defined in Grisette.Internal.SymPrim.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

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

Defined in Grisette.Internal.SymPrim.BV

Methods

finiteBitSize :: WordN n -> Int

countLeadingZeros :: WordN n -> Int

countTrailingZeros :: WordN n -> Int

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

Defined in Grisette.Internal.SymPrim.BV

Methods

minBound :: WordN n

maxBound :: WordN n

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

Defined in Grisette.Internal.SymPrim.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.Internal.SymPrim.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.Internal.SymPrim.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

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

Defined in Grisette.Internal.SymPrim.BV

Methods

readsPrec :: Int -> ReadS (WordN n)

readList :: ReadS [WordN n]

readPrec :: ReadPrec (WordN n)

readListPrec :: ReadPrec [WordN n]

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

Defined in Grisette.Internal.SymPrim.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.Internal.SymPrim.BV

Methods

toRational :: WordN n -> Rational

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

Defined in Grisette.Internal.SymPrim.BV

Methods

showsPrec :: Int -> WordN n -> ShowS

show :: WordN n -> String

showList :: [WordN n] -> ShowS

NFData (WordN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

rnf :: WordN n -> ()

Eq (WordN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

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

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

Ord (WordN n)

Defined in Grisette.Internal.SymPrim.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

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

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

Methods

evalSym :: Bool -> Model -> WordN n -> WordN n

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

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

Methods

extractSym :: WordN n -> SymbolSet

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

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

Methods

rootStrategy :: MergingStrategy (WordN n)

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

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

Methods

pformat :: WordN n -> Doc ann

pformatPrec :: Int -> WordN n -> Doc ann

pformatList :: [WordN n] -> Doc ann

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

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

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> WordN n -> WordN n

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

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

Methods

(.==) :: WordN n -> WordN n -> SymBool

(./=) :: WordN n -> WordN n -> SymBool

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

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

Methods

(.<) :: WordN n -> WordN n -> SymBool

(.<=) :: WordN n -> WordN n -> SymBool

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

(.>=) :: WordN n -> WordN n -> SymBool

symCompare :: WordN n -> WordN n -> Union Ordering

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

Defined in Grisette.Internal.SymPrim.BV

Methods

symRotate :: WordN n -> WordN n -> WordN n

symRotateNegated :: WordN n -> WordN n -> WordN n

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

Defined in Grisette.Internal.SymPrim.BV

Methods

symShift :: WordN n -> WordN n -> WordN n

symShiftNegated :: WordN n -> WordN n -> WordN n

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

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: WordN n -> [SomeSym] -> [SomeSym]

allSyms :: WordN n -> [SomeSym]

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type NonFuncSBVBaseType n (WordN w)

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitwiseTerm

Methods

pevalAndBitsTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)

pevalOrBitsTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)

pevalXorBitsTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)

pevalComplementBitsTerm :: Term (WordN n) -> Term (WordN n)

withSbvBitwiseTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (Bits (SBVType n0 (WordN n)) => r) -> r

sbvAndBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

sbvOrBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

sbvXorBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

sbvComplementBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalDivModIntegralTerm

Methods

pevalDivIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)

pevalModIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)

pevalQuotIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)

pevalRemIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)

withSbvDivModIntegralTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SDivisible (SBVType n0 (WordN n)) => r) -> r

sbvDivIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

sbvModIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

sbvQuotIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

sbvRemIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm

Methods

pevalAddNumTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)

pevalNegNumTerm :: Term (WordN n) -> Term (WordN n)

pevalMulNumTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)

pevalAbsNumTerm :: Term (WordN n) -> Term (WordN n)

pevalSignumNumTerm :: Term (WordN n) -> Term (WordN n)

withSbvNumTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (Num (SBVType n0 (WordN n)) => r) -> r

sbvAddNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

sbvNegNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

sbvMulNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

sbvAbsNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

sbvSignumNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm

Methods

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

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

withSbvOrdTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (OrdSymbolic (SBVType n0 (WordN n)) => r) -> r

sbvLtOrdTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBV Bool

sbvLeOrdTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBV Bool

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalRotateTerm

Methods

pevalRotateLeftTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)

pevalRotateRightTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)

withSbvRotateTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SIntegral (NonFuncSBVBaseType n0 (WordN n)) => r) -> r

sbvRotateLeftTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

sbvRotateRightTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalShiftTerm

Methods

pevalShiftLeftTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)

pevalShiftRightTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)

withSbvShiftTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SIntegral (NonFuncSBVBaseType n0 (WordN n)) => r) -> r

sbvShiftLeftTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

sbvShiftRightTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type SBVType n (WordN w)

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Methods

conNonFuncSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> WordN w -> SBV (NonFuncSBVBaseType n (WordN w))

symNonFuncSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBV (NonFuncSBVBaseType n (WordN w)))

withNonFuncPrim :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> ((SymVal (NonFuncSBVBaseType n (WordN w)), EqSymbolic (SBVType n (WordN w)), Mergeable (SBVType n (WordN w)), SMTDefinable (SBVType n (WordN w)), Mergeable (SBVType n (WordN w)), SBVType n (WordN w) ~ SBV (NonFuncSBVBaseType n (WordN w)), PrimConstraint n (WordN w)) => r) -> r

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Methods

termCache :: Cache (Term (WordN w))

pformatCon :: WordN w -> String

pformatSym :: TypedSymbol (WordN w) -> String

defaultValue :: WordN w

defaultValueDynamic :: proxy (WordN w) -> ModelValue

pevalITETerm :: Term Bool -> Term (WordN w) -> Term (WordN w) -> Term (WordN w)

pevalEqTerm :: Term (WordN w) -> Term (WordN w) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> WordN w -> SBVType n (WordN w)

symSBVName :: TypedSymbol (WordN w) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (WordN w))

withPrim :: forall (n :: Nat) p a. KnownIsZero n => p n -> ((PrimConstraint n (WordN w), SMTDefinable (SBVType n (WordN w)), Mergeable (SBVType n (WordN w)), Typeable (SBVType n (WordN w))) => a) -> a

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (WordN w) -> SBVType n (WordN w) -> SBVType n (WordN w)

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (WordN w) -> SBVType n (WordN w) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> WordN w

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type PrimConstraint n (WordN w)

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

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type SymType (WordN n)

Hashable (WordN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

hashWithSalt :: Int -> WordN n -> Int

hash :: WordN n -> Int

BitCast (WordN 8) Int8

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 8 -> Int8

BitCast (WordN 8) Word8

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 8 -> Word8

BitCast (WordN 16) Int16

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 16 -> Int16

BitCast (WordN 16) Word16

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 16 -> Word16

BitCast (WordN 32) Int32

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 32 -> Int32

BitCast (WordN 32) Word32

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 32 -> Word32

BitCast (WordN 64) Int64

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 64 -> Int64

BitCast (WordN 64) Word64

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 64 -> Word64

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

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN n -> WordN n

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

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN n -> IntN n

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

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

Methods

fresh :: MonadFresh m => WordN n -> m (Union (WordN n))

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

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

Methods

simpleFresh :: MonadFresh m => WordN n -> m (WordN n)

(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

(KnownNat n, 1 <= n) => Solvable (WordN n) (SymWordN n)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

con :: WordN n -> SymWordN n

conView :: SymWordN n -> Maybe (WordN n)

sym :: Symbol -> SymWordN n

ssym :: Identifier -> SymWordN n

isym :: Identifier -> Int -> SymWordN n

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

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

Methods

toCon :: WordN n -> Maybe (WordN n)

(KnownNat n, 1 <= n) => ToCon (SymWordN n) (WordN n)

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

Methods

toCon :: SymWordN n -> Maybe (WordN n)

(KnownNat n, 1 <= n) => ToSym (Union (WordN n)) (SymWordN n)

Defined in Grisette.Internal.Core.Control.Monad.Union

Methods

toSym :: Union (WordN n) -> SymWordN n

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

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

Methods

toSym :: WordN n -> WordN n

(KnownNat n, 1 <= n) => ToSym (WordN n) (SymWordN n)

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

Methods

toSym :: WordN n -> SymWordN n

(KnownNat n, 1 <= n) => LinkedRep (WordN n) (SymWordN n)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

underlyingTerm :: SymWordN n -> Term (WordN n)

wrapTerm :: Term (WordN n) -> SymWordN n

(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

(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

type NonFuncSBVBaseType _1 (WordN w)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type NonFuncSBVBaseType _1 (WordN w) = WordN w

type PrimConstraint _1 (WordN w)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

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

type SBVType _1 (WordN w)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type SBVType _1 (WordN w) = SBV (WordN w)

type Rep (WordN n)

Defined in Grisette.Internal.SymPrim.BV

type Rep (WordN n) = D1 ('MetaData "WordN" "Grisette.Internal.SymPrim.BV" "grisette-0.7.0.0-3DYM4wcz8TiF8sSQ1gvVO8" 'True) (C1 ('MetaCons "WordN" 'PrefixI 'True) (S1 ('MetaSel ('Just "unWordN") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))

type SymType (WordN n)

Defined in Grisette.Internal.SymPrim.SymBV

type SymType (WordN n) = SymWordN n

type WordN8 = WordN 8

8-bit unsigned bit-vector

type WordN16 = WordN 16

16-bit unsigned bit-vector

type WordN32 = WordN 32

32-bit unsigned bit-vector

type WordN64 = WordN 64

64-bit unsigned bit-vector