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.SomeBV

Contents

Constructing and pattern matching on SomeBV
Synonyms
Helpers for manipulating SomeBV

Description

Synopsis

data SomeBV (bv :: Nat -> Type) where
- SomeBV :: forall (n :: Nat) (bv :: Nat -> Type). (KnownNat n, 1 <= n) => bv n -> SomeBV bv
- SomeBVLit :: forall (bv :: Nat -> Type). SomeBVLit -> SomeBV bv
data SomeBVException
- = BitwidthMismatch
- | UndeterminedBitwidth Text
unsafeSomeBV :: Int -> (forall (proxy :: Nat -> Type) (n :: Nat). (KnownNat n, 1 <= n) => proxy n -> bv n) -> SomeBV bv
conBV :: forall (cbv :: Natural -> Type) (bv :: Natural -> Type). (forall (n :: Nat). (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV cbv -> SomeBV bv
conBVView :: forall (cbv :: Natural -> Type) (bv :: Natural -> Type). (forall (n :: Nat). (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV bv -> Maybe (SomeBV cbv)
pattern ConBV :: (forall (n :: Nat). (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV cbv -> SomeBV bv
symBV :: forall (cbv :: Natural -> Type) (bv :: Natural -> Type). (forall (n :: Nat). (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Symbol -> SomeBV bv
ssymBV :: forall (cbv :: Natural -> Type) (bv :: Natural -> Type). (forall (n :: Nat). (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Identifier -> SomeBV bv
isymBV :: forall (cbv :: Natural -> Type) (bv :: Natural -> Type). (forall (n :: Nat). (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Identifier -> Int -> SomeBV bv
arbitraryBV :: forall (bv :: Nat -> Type). (forall (n :: Nat). (KnownNat n, 1 <= n) => Arbitrary (bv n)) => Int -> Gen (SomeBV bv)
pattern SomeIntN :: forall (n :: Nat). () => (KnownNat n, 1 <= n) => IntN n -> SomeIntN
type SomeIntN = SomeBV IntN
pattern SomeWordN :: forall (n :: Nat). () => (KnownNat n, 1 <= n) => WordN n -> SomeWordN
type SomeWordN = SomeBV WordN
pattern SomeSymIntN :: forall (n :: Nat). () => (KnownNat n, 1 <= n) => SymIntN n -> SomeSymIntN
type SomeSymIntN = SomeBV SymIntN
pattern SomeSymWordN :: forall (n :: Nat). () => (KnownNat n, 1 <= n) => SymWordN n -> SomeSymWordN
type SomeSymWordN = SomeBV SymWordN
unarySomeBV :: (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r) -> (SomeBVLit -> r) -> SomeBV bv -> r
unarySomeBVR1 :: (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n) -> (SomeBVLit -> SomeBVLit) -> SomeBV bv -> SomeBV bv
binSomeBV :: (forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r) -> (SomeBVLit -> SomeBVLit -> r) -> SomeBV bv -> SomeBV bv -> r
binSomeBVR1 :: (forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n) -> (SomeBVLit -> SomeBVLit -> SomeBVLit) -> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR2 :: (forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> (bv n, bv n)) -> (SomeBVLit -> SomeBVLit -> (SomeBVLit, SomeBVLit)) -> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)
binSomeBVSafe :: (MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e, Mergeable r, forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m r) -> (SomeBVLit -> SomeBVLit -> ExceptT (Either SomeBVException e) m r) -> SomeBV bv -> SomeBV bv -> m r
binSomeBVSafeR1 :: (MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e, forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n), forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n)) -> (SomeBVLit -> SomeBVLit -> ExceptT (Either SomeBVException e) m SomeBVLit) -> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR2 :: (MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e, forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n), forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n, bv n)) -> (SomeBVLit -> SomeBVLit -> ExceptT (Either SomeBVException e) m (SomeBVLit, SomeBVLit)) -> SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)

Documentation

data SomeBV (bv :: Nat -> Type) where Source #

Non-indexed bitvectors.

The creation of SomeBV can be done with the bv function with a positive bit width and a value:

>>> bv 4 0xf :: SomeBV IntN
0xf

Operations on two SomeBV values require the bitwidths to be the same. So you should check for the bit width (via finiteBitSize) before performing operations:

>>> bv 4 0x3 + bv 4 0x3 :: SomeBV IntN
0x6
>>> bv 4 0x3 + bv 8 0x3 :: SomeBV IntN
*** Exception: BitwidthMismatch

One exception is that the equality testing (both concrete and symbolic via SymEq) does not require the bitwidths to be the same. Different bitwidths means the values are not equal:

>>> (bv 4 0x3 :: SomeBV IntN) == (bv 8 0x3)
False

Note: SomeBV can be constructed out of integer literals without the bit width provided. Further binary operations will usually require at least one operand has the bit-width, and will use that as the bit-width for the result.

For example:

3 :: SomeBV IntN bvlit(3) >>> bv 4 0x1 + 3 :: SomeBV IntN 0x4 >>> 3 * bv 4 0x1 :: SomeBV IntN 0x3 >>> 3 * 3 :: SomeBV IntN *** Exception: UndeterminedBitwidth "(*)"

Some operations allows the literals to be used without the bit-width, such as (+), (-), negate, toUnsigned, toSigned, .&., .|., xor, complement, setBit, clearBit, complementBit, shiftL, and unsafeShiftL.

>>> 3 + 3 :: SomeBV IntN
bvlit(6)

Constructors

SomeBV :: forall (n :: Nat) (bv :: Nat -> Type). (KnownNat n, 1 <= n) => bv n -> SomeBV bv
SomeBVLit :: forall (bv :: Nat -> Type). SomeBVLit -> SomeBV bv

Instances

Instances details

FromBits SomeIntN Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods fromBits :: [Bool] -> SomeIntN Source #
FromBits SomeWordN Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods fromBits :: [Bool] -> SomeWordN Source #
UnifiedFiniteBits 'C SomeIntN Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits Methods withBaseFiniteBits :: (If (IsConMode 'C) (FiniteBits SomeIntN, FromBits SomeIntN) (SymFiniteBits SomeIntN) => r) -> r Source #
UnifiedFiniteBits 'C SomeWordN Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits Methods withBaseFiniteBits :: (If (IsConMode 'C) (FiniteBits SomeWordN, FromBits SomeWordN) (SymFiniteBits SomeWordN) => r) -> r Source #
UnifiedFiniteBits 'S SomeSymIntN Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits Methods withBaseFiniteBits :: (If (IsConMode 'S) (FiniteBits SomeSymIntN, FromBits SomeSymIntN) (SymFiniteBits SomeSymIntN) => r) -> r Source #
UnifiedFiniteBits 'S SomeSymWordN Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits Methods withBaseFiniteBits :: (If (IsConMode 'S) (FiniteBits SomeSymWordN, FromBits SomeSymWordN) (SymFiniteBits SomeSymWordN) => r) -> r Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => GenSym () (bv n), Mergeable (SomeBV bv)) => GenSym Int (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods fresh :: MonadFresh m => Int -> m (Union (SomeBV bv)) Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => GenSymSimple () (bv n), Mergeable (SomeBV bv)) => GenSymSimple Int (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods simpleFresh :: MonadFresh m => Int -> m (SomeBV bv) Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => Lift (bv n)) => Lift (SomeBV bv :: Type) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods lift :: Quote m => SomeBV bv -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => SomeBV bv -> Code m (SomeBV bv) #
(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeDiv 'S (Either SomeBVException ArithException) SomeSymIntN m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv Methods withBaseSafeDiv :: (SafeDiv (Either SomeBVException ArithException) SomeSymIntN m => r) -> r Source #
(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeDiv 'S (Either SomeBVException ArithException) SomeSymWordN m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv Methods withBaseSafeDiv :: (SafeDiv (Either SomeBVException ArithException) SomeSymWordN m => r) -> r Source #
(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeDiv mode (Either SomeBVException ArithException) SomeIntN m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv Methods withBaseSafeDiv :: (SafeDiv (Either SomeBVException ArithException) SomeIntN m => r) -> r Source #
(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeDiv mode (Either SomeBVException ArithException) SomeWordN m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv Methods withBaseSafeDiv :: (SafeDiv (Either SomeBVException ArithException) SomeWordN m => r) -> r Source #
(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeLinearArith 'S (Either SomeBVException ArithException) SomeSymIntN m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith Methods withBaseSafeLinearArith :: (SafeLinearArith (Either SomeBVException ArithException) SomeSymIntN m => r) -> r Source #
(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeLinearArith 'S (Either SomeBVException ArithException) SomeSymWordN m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith Methods withBaseSafeLinearArith :: (SafeLinearArith (Either SomeBVException ArithException) SomeSymWordN m => r) -> r Source #
(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeLinearArith mode (Either SomeBVException ArithException) SomeIntN m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith Methods withBaseSafeLinearArith :: (SafeLinearArith (Either SomeBVException ArithException) SomeIntN m => r) -> r Source #
(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeLinearArith mode (Either SomeBVException ArithException) SomeWordN m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith Methods withBaseSafeLinearArith :: (SafeLinearArith (Either SomeBVException ArithException) SomeWordN m => r) -> r Source #
(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeSymRotate 'S (Either SomeBVException ArithException) SomeSymIntN m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate Methods withBaseSafeSymRotate :: (SafeSymRotate (Either SomeBVException ArithException) SomeSymIntN m => r) -> r Source #
(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeSymRotate 'S (Either SomeBVException ArithException) SomeSymWordN m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate Methods withBaseSafeSymRotate :: (SafeSymRotate (Either SomeBVException ArithException) SomeSymWordN m => r) -> r Source #
(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymRotate mode (Either SomeBVException ArithException) SomeIntN m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate Methods withBaseSafeSymRotate :: (SafeSymRotate (Either SomeBVException ArithException) SomeIntN m => r) -> r Source #
(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymRotate mode (Either SomeBVException ArithException) SomeWordN m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate Methods withBaseSafeSymRotate :: (SafeSymRotate (Either SomeBVException ArithException) SomeWordN m => r) -> r Source #
(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeSymShift 'S (Either SomeBVException ArithException) SomeSymIntN m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift Methods withBaseSafeSymShift :: (SafeSymShift (Either SomeBVException ArithException) SomeSymIntN m => r) -> r Source #
(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeSymShift 'S (Either SomeBVException ArithException) SomeSymWordN m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift Methods withBaseSafeSymShift :: (SafeSymShift (Either SomeBVException ArithException) SomeSymWordN m => r) -> r Source #
(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymShift mode (Either SomeBVException ArithException) SomeIntN m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift Methods withBaseSafeSymShift :: (SafeSymShift (Either SomeBVException ArithException) SomeIntN m => r) -> r Source #
(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymShift mode (Either SomeBVException ArithException) SomeWordN m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift Methods withBaseSafeSymShift :: (SafeSymShift (Either SomeBVException ArithException) SomeWordN m => r) -> r Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => Serial (bv n)) => Binary (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods put :: SomeBV bv -> Put # get :: Get (SomeBV bv) # putList :: [SomeBV bv] -> Put #
(forall (n :: Nat). (KnownNat n, 1 <= n) => Serial (bv n)) => Serial (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods serialize :: MonadPut m => SomeBV bv -> m () # deserialize :: MonadGet m => m (SomeBV bv) #
(forall (n :: Nat). (KnownNat n, 1 <= n) => Serial (bv n)) => Serialize (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods put :: Putter (SomeBV bv) # get :: Get (SomeBV bv) #
(forall (n :: Nat). (KnownNat n, 1 <= n) => NFData (bv n)) => NFData (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods rnf :: SomeBV bv -> () #
(forall (n :: Nat). (KnownNat n, 1 <= n) => Bits (bv n), forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => Bits (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods (.&.) :: SomeBV bv -> SomeBV bv -> SomeBV bv # (.\|.) :: SomeBV bv -> SomeBV bv -> SomeBV bv # xor :: SomeBV bv -> SomeBV bv -> SomeBV bv # complement :: SomeBV bv -> SomeBV bv # shift :: SomeBV bv -> Int -> SomeBV bv # rotate :: SomeBV bv -> Int -> SomeBV bv # zeroBits :: SomeBV bv # bit :: Int -> SomeBV bv # setBit :: SomeBV bv -> Int -> SomeBV bv # clearBit :: SomeBV bv -> Int -> SomeBV bv # complementBit :: SomeBV bv -> Int -> SomeBV bv # testBit :: SomeBV bv -> Int -> Bool # bitSizeMaybe :: SomeBV bv -> Maybe Int # bitSize :: SomeBV bv -> Int # isSigned :: SomeBV bv -> Bool # shiftL :: SomeBV bv -> Int -> SomeBV bv # unsafeShiftL :: SomeBV bv -> Int -> SomeBV bv # shiftR :: SomeBV bv -> Int -> SomeBV bv # unsafeShiftR :: SomeBV bv -> Int -> SomeBV bv # rotateL :: SomeBV bv -> Int -> SomeBV bv # rotateR :: SomeBV bv -> Int -> SomeBV bv # popCount :: SomeBV bv -> Int #
(forall (n :: Nat). (KnownNat n, 1 <= n) => FiniteBits (bv n), forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => FiniteBits (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods finiteBitSize :: SomeBV bv -> Int # countLeadingZeros :: SomeBV bv -> Int # countTrailingZeros :: SomeBV bv -> Int #
(forall (n :: Nat). (KnownNat n, 1 <= n) => Enum (bv n)) => Enum (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods succ :: SomeBV bv -> SomeBV bv # pred :: SomeBV bv -> SomeBV bv # toEnum :: Int -> SomeBV bv # fromEnum :: SomeBV bv -> Int # enumFrom :: SomeBV bv -> [SomeBV bv] # enumFromThen :: SomeBV bv -> SomeBV bv -> [SomeBV bv] # enumFromTo :: SomeBV bv -> SomeBV bv -> [SomeBV bv] # enumFromThenTo :: SomeBV bv -> SomeBV bv -> SomeBV bv -> [SomeBV bv] #
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => Num (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods (+) :: SomeBV bv -> SomeBV bv -> SomeBV bv # (-) :: SomeBV bv -> SomeBV bv -> SomeBV bv # (*) :: SomeBV bv -> SomeBV bv -> SomeBV bv # negate :: SomeBV bv -> SomeBV bv # abs :: SomeBV bv -> SomeBV bv # signum :: SomeBV bv -> SomeBV bv # fromInteger :: Integer -> SomeBV bv #
(forall (n :: Nat). (KnownNat n, 1 <= n) => Integral (bv n), MaySomeBV bv) => Integral (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods quot :: SomeBV bv -> SomeBV bv -> SomeBV bv # rem :: SomeBV bv -> SomeBV bv -> SomeBV bv # div :: SomeBV bv -> SomeBV bv -> SomeBV bv # mod :: SomeBV bv -> SomeBV bv -> SomeBV bv # quotRem :: SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv) # divMod :: SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv) # toInteger :: SomeBV bv -> Integer #
(forall (n :: Nat). (KnownNat n, 1 <= n) => Real (bv n), MaySomeBV bv) => Real (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods toRational :: SomeBV bv -> Rational #
(forall (n :: Nat). (KnownNat n, 1 <= n) => Show (bv n)) => Show (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods showsPrec :: Int -> SomeBV bv -> ShowS # show :: SomeBV bv -> String # showList :: [SomeBV bv] -> ShowS #
(forall (n :: Nat). (KnownNat n, 1 <= n) => Eq (bv n), forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => Eq (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods (==) :: SomeBV bv -> SomeBV bv -> Bool # (/=) :: SomeBV bv -> SomeBV bv -> Bool #
(forall (n :: Nat). (KnownNat n, 1 <= n) => Ord (bv n), forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => Ord (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods compare :: SomeBV bv -> SomeBV bv -> Ordering # (<) :: SomeBV bv -> SomeBV bv -> Bool # (<=) :: SomeBV bv -> SomeBV bv -> Bool # (>) :: SomeBV bv -> SomeBV bv -> Bool # (>=) :: SomeBV bv -> SomeBV bv -> Bool # max :: SomeBV bv -> SomeBV bv -> SomeBV bv # min :: SomeBV bv -> SomeBV bv -> SomeBV bv #
SizedBV bv => BV (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods bvConcat :: SomeBV bv -> SomeBV bv -> SomeBV bv Source # bvZext :: Int -> SomeBV bv -> SomeBV bv Source # bvSext :: Int -> SomeBV bv -> SomeBV bv Source # bvExt :: Int -> SomeBV bv -> SomeBV bv Source # bvSelect :: Int -> Int -> SomeBV bv -> SomeBV bv Source # bv :: Integral a => Int -> a -> SomeBV bv Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => ITEOp (bv n), forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => ITEOp (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods symIte :: SymBool -> SomeBV bv -> SomeBV bv -> SomeBV bv Source #
SymFiniteBits (SomeBV SymIntN) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods symTestBit :: SomeBV SymIntN -> Int -> SymBool Source # symSetBitTo :: SomeBV SymIntN -> Int -> SymBool -> SomeBV SymIntN Source # symFromBits :: [SymBool] -> SomeBV SymIntN Source #
SymFiniteBits (SomeBV SymWordN) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods symTestBit :: SomeBV SymWordN -> Int -> SymBool Source # symSetBitTo :: SomeBV SymWordN -> Int -> SymBool -> SomeBV SymWordN Source # symFromBits :: [SymBool] -> SomeBV SymWordN Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => SymRotate (bv n), forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => SymRotate (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods symRotate :: SomeBV bv -> SomeBV bv -> SomeBV bv Source # symRotateNegated :: SomeBV bv -> SomeBV bv -> SomeBV bv 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 #
(forall (n :: Nat). (KnownNat n, 1 <= n) => EvalSym (bv n)) => EvalSym (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods evalSym :: Bool -> Model -> SomeBV bv -> SomeBV bv Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => ExtractSym (bv n)) => ExtractSym (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods extractSym :: SomeBV bv -> AnySymbolSet Source # extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => SomeBV bv -> Maybe (SymbolSet knd) Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) => Mergeable (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods rootStrategy :: MergingStrategy (SomeBV bv) Source # sortIndices :: SomeBV bv -> [DynamicSortedIdx] Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => PPrint (bv n)) => PPrint (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods pformat :: SomeBV bv -> Doc ann Source # pformatPrec :: Int -> SomeBV bv -> Doc ann Source # pformatList :: [SomeBV bv] -> Doc ann Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => DivOr (bv n), forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => DivOr (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods divOr :: SomeBV bv -> SomeBV bv -> SomeBV bv -> SomeBV bv Source # modOr :: SomeBV bv -> SomeBV bv -> SomeBV bv -> SomeBV bv Source # divModOr :: (SomeBV bv, SomeBV bv) -> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv) Source # quotOr :: SomeBV bv -> SomeBV bv -> SomeBV bv -> SomeBV bv Source # remOr :: SomeBV bv -> SomeBV bv -> SomeBV bv -> SomeBV bv Source # quotRemOr :: (SomeBV bv, SomeBV bv) -> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv) Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => SubstSym (bv n)) => SubstSym (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> SomeBV bv -> SomeBV bv Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => SymEq (bv n), forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => SymEq (SomeBV bv) Source #	The `symDistinct` instance for `SomeBV` will have the following behavior: If the list is empty or has only one element, it will return `True`. If none of the elements have a bit-width, it will throw `UndeterminedBitwidth` exception. If the elements have different bit-widths, it will throw a `BitwidthMismatch` exception. If there are at least one element have a bit-width, and all elements with known bit-width have the same bit-width, it will generate a single symbolic formula using `distinct`.
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods (.==) :: SomeBV bv -> SomeBV bv -> SymBool Source # (./=) :: SomeBV bv -> SomeBV bv -> SymBool Source # symDistinct :: [SomeBV bv] -> SymBool Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => SymOrd (bv n), forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => SymOrd (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods (.<) :: SomeBV bv -> SomeBV bv -> SymBool Source # (.<=) :: SomeBV bv -> SomeBV bv -> SymBool Source # (.>) :: SomeBV bv -> SomeBV bv -> SymBool Source # (.>=) :: SomeBV bv -> SomeBV bv -> SymBool Source # symCompare :: SomeBV bv -> SomeBV bv -> Union Ordering Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => AllSyms (bv n), MaySomeBV bv) => AllSyms (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods allSymsS :: SomeBV bv -> [SomeSym] -> [SomeSym] Source # allSyms :: SomeBV bv -> [SomeSym] Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => Hashable (bv n), forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => Hashable (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods hashWithSalt :: Int -> SomeBV bv -> Int # hash :: SomeBV bv -> Int #
(forall (m :: Nat). (KnownNat m, 1 <= m) => GenSym () (bv m), Mergeable (SomeBV bv)) => GenSym (SomeBV bv) (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods fresh :: MonadFresh m => SomeBV bv -> m (Union (SomeBV bv)) Source #
(forall (m :: Nat). (KnownNat m, 1 <= m) => GenSymSimple () (bv m), Mergeable (SomeBV bv)) => GenSymSimple (SomeBV bv) (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods simpleFresh :: MonadFresh m => SomeBV bv -> m (SomeBV bv) Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => SignConversion (ubv n) (sbv n), SignConversion (ubv 1) (sbv 1)) => SignConversion (SomeBV ubv) (SomeBV sbv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods toSigned :: SomeBV ubv -> SomeBV sbv Source # toUnsigned :: SomeBV sbv -> SomeBV ubv Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => ToCon (sbv n) (cbv n)) => ToCon (SomeBV sbv) (SomeBV cbv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods toCon :: SomeBV sbv -> Maybe (SomeBV cbv) Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => ToSym (cbv n) (sbv n)) => ToSym (SomeBV cbv) (SomeBV sbv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods toSym :: SomeBV cbv -> SomeBV sbv Source #
(KnownNat n, 1 <= n, forall (m :: Nat). (KnownNat m, 1 <= m) => GenSym () (bv m), Mergeable (SomeBV bv)) => GenSym (Proxy n) (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods fresh :: MonadFresh m => Proxy n -> m (Union (SomeBV bv)) Source #
(KnownNat n, 1 <= n, forall (m :: Nat). (KnownNat m, 1 <= m) => GenSymSimple () (bv m), Mergeable (SomeBV bv)) => GenSymSimple (Proxy n) (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods simpleFresh :: MonadFresh m => Proxy n -> m (SomeBV bv) Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => SafeLinearArith e (bv n) (ExceptT e m), MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e, forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => SafeLinearArith (Either SomeBVException e) (SomeBV bv) m Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods safeAdd :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source # safeNeg :: SomeBV bv -> m (SomeBV bv) Source # safeSub :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => SafeSymRotate e (bv n) (ExceptT e m), MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e, forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => SafeSymRotate (Either SomeBVException e) (SomeBV bv) m Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods safeSymRotateL :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source # safeSymRotateR :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => SafeSymShift e (bv n) (ExceptT e m), MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e, forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => SafeSymShift (Either SomeBVException e) (SomeBV bv) m Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods safeSymShiftL :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source # safeSymShiftR :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source # safeSymStrictShiftL :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source # safeSymStrictShiftR :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => SafeDiv e (bv n) (ExceptT e m), MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e, forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => SafeDiv (Either SomeBVException e) (SomeBV bv) m Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods safeDiv :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source # safeMod :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source # safeDivMod :: SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv) Source # safeQuot :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source # safeRem :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source # safeQuotRem :: SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv) Source #

data SomeBVException Source #

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

Constructors

BitwidthMismatch
UndeterminedBitwidth Text

Instances

Instances details

NFData SomeBVException Source #

Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

rnf :: SomeBVException -> () #

Exception SomeBVException Source #

Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

toException :: SomeBVException -> SomeException #

fromException :: SomeException -> Maybe SomeBVException #

displayException :: SomeBVException -> String #

backtraceDesired :: SomeBVException -> Bool #

Generic SomeBVException Source #

Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Associated Types

type Rep SomeBVException

Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

type Rep SomeBVException = D1 ('MetaData "SomeBVException" "Grisette.Internal.SymPrim.SomeBV" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) (C1 ('MetaCons "BitwidthMismatch" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UndeterminedBitwidth" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)))

Methods

from :: SomeBVException -> Rep SomeBVException x #

to :: Rep SomeBVException x -> SomeBVException #

Show SomeBVException Source #

Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

showsPrec :: Int -> SomeBVException -> ShowS #

show :: SomeBVException -> String #

showList :: [SomeBVException] -> ShowS #

Eq SomeBVException Source #

Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

(==) :: SomeBVException -> SomeBVException -> Bool #

(/=) :: SomeBVException -> SomeBVException -> Bool #

Ord SomeBVException Source #

Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

compare :: SomeBVException -> SomeBVException -> Ordering #

(<) :: SomeBVException -> SomeBVException -> Bool #

(<=) :: SomeBVException -> SomeBVException -> Bool #

(>) :: SomeBVException -> SomeBVException -> Bool #

(>=) :: SomeBVException -> SomeBVException -> Bool #

max :: SomeBVException -> SomeBVException -> SomeBVException #

min :: SomeBVException -> SomeBVException -> SomeBVException #

EvalSym SomeBVException Source #

Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

evalSym :: Bool -> Model -> SomeBVException -> SomeBVException Source #

ExtractSym SomeBVException Source #

Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

extractSym :: SomeBVException -> AnySymbolSet Source #

extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => SomeBVException -> Maybe (SymbolSet knd) Source #

Mergeable SomeBVException Source #

Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

rootStrategy :: MergingStrategy SomeBVException Source #

sortIndices :: SomeBVException -> [DynamicSortedIdx] Source #

PPrint SomeBVException Source #

Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

pformat :: SomeBVException -> Doc ann Source #

pformatPrec :: Int -> SomeBVException -> Doc ann Source #

pformatList :: [SomeBVException] -> Doc ann Source #

SubstSym SomeBVException Source #

Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> SomeBVException -> SomeBVException Source #

SymEq SomeBVException Source #

Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

(.==) :: SomeBVException -> SomeBVException -> SymBool Source #

(./=) :: SomeBVException -> SomeBVException -> SymBool Source #

symDistinct :: [SomeBVException] -> SymBool Source #

SymOrd SomeBVException Source #

Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

(.<) :: SomeBVException -> SomeBVException -> SymBool Source #

(.<=) :: SomeBVException -> SomeBVException -> SymBool Source #

(.>) :: SomeBVException -> SomeBVException -> SymBool Source #

(.>=) :: SomeBVException -> SomeBVException -> SymBool Source #

symCompare :: SomeBVException -> SomeBVException -> Union Ordering Source #

Hashable SomeBVException Source #

Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

hashWithSalt :: Int -> SomeBVException -> Int #

hash :: SomeBVException -> Int #

ToCon SomeBVException SomeBVException Source #

Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

toCon :: SomeBVException -> Maybe SomeBVException Source #

ToSym SomeBVException SomeBVException Source #

Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

toSym :: SomeBVException -> SomeBVException Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeDiv 'S (Either SomeBVException ArithException) SomeSymIntN m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

Methods

withBaseSafeDiv :: (SafeDiv (Either SomeBVException ArithException) SomeSymIntN m => r) -> r Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeDiv 'S (Either SomeBVException ArithException) SomeSymWordN m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

Methods

withBaseSafeDiv :: (SafeDiv (Either SomeBVException ArithException) SomeSymWordN m => r) -> r Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeDiv mode (Either SomeBVException ArithException) SomeIntN m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

Methods

withBaseSafeDiv :: (SafeDiv (Either SomeBVException ArithException) SomeIntN m => r) -> r Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeDiv mode (Either SomeBVException ArithException) SomeWordN m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

Methods

withBaseSafeDiv :: (SafeDiv (Either SomeBVException ArithException) SomeWordN m => r) -> r Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeLinearArith 'S (Either SomeBVException ArithException) SomeSymIntN m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

Methods

withBaseSafeLinearArith :: (SafeLinearArith (Either SomeBVException ArithException) SomeSymIntN m => r) -> r Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeLinearArith 'S (Either SomeBVException ArithException) SomeSymWordN m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

Methods

withBaseSafeLinearArith :: (SafeLinearArith (Either SomeBVException ArithException) SomeSymWordN m => r) -> r Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeLinearArith mode (Either SomeBVException ArithException) SomeIntN m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

Methods

withBaseSafeLinearArith :: (SafeLinearArith (Either SomeBVException ArithException) SomeIntN m => r) -> r Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeLinearArith mode (Either SomeBVException ArithException) SomeWordN m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

Methods

withBaseSafeLinearArith :: (SafeLinearArith (Either SomeBVException ArithException) SomeWordN m => r) -> r Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeSymRotate 'S (Either SomeBVException ArithException) SomeSymIntN m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate

Methods

withBaseSafeSymRotate :: (SafeSymRotate (Either SomeBVException ArithException) SomeSymIntN m => r) -> r Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeSymRotate 'S (Either SomeBVException ArithException) SomeSymWordN m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate

Methods

withBaseSafeSymRotate :: (SafeSymRotate (Either SomeBVException ArithException) SomeSymWordN m => r) -> r Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymRotate mode (Either SomeBVException ArithException) SomeIntN m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate

Methods

withBaseSafeSymRotate :: (SafeSymRotate (Either SomeBVException ArithException) SomeIntN m => r) -> r Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymRotate mode (Either SomeBVException ArithException) SomeWordN m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate

Methods

withBaseSafeSymRotate :: (SafeSymRotate (Either SomeBVException ArithException) SomeWordN m => r) -> r Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeSymShift 'S (Either SomeBVException ArithException) SomeSymIntN m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift

Methods

withBaseSafeSymShift :: (SafeSymShift (Either SomeBVException ArithException) SomeSymIntN m => r) -> r Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeSymShift 'S (Either SomeBVException ArithException) SomeSymWordN m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift

Methods

withBaseSafeSymShift :: (SafeSymShift (Either SomeBVException ArithException) SomeSymWordN m => r) -> r Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymShift mode (Either SomeBVException ArithException) SomeIntN m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift

Methods

withBaseSafeSymShift :: (SafeSymShift (Either SomeBVException ArithException) SomeIntN m => r) -> r Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymShift mode (Either SomeBVException ArithException) SomeWordN m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift

Methods

withBaseSafeSymShift :: (SafeSymShift (Either SomeBVException ArithException) SomeWordN m => r) -> r Source #

(forall (n :: Nat). (KnownNat n, 1 <= n) => SafeLinearArith e (bv n) (ExceptT e m), MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e, forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => SafeLinearArith (Either SomeBVException e) (SomeBV bv) m Source #

Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

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

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

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

(forall (n :: Nat). (KnownNat n, 1 <= n) => SafeSymRotate e (bv n) (ExceptT e m), MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e, forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => SafeSymRotate (Either SomeBVException e) (SomeBV bv) m Source #

Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

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

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

(forall (n :: Nat). (KnownNat n, 1 <= n) => SafeSymShift e (bv n) (ExceptT e m), MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e, forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => SafeSymShift (Either SomeBVException e) (SomeBV bv) m Source #

Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

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

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

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

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

(forall (n :: Nat). (KnownNat n, 1 <= n) => SafeDiv e (bv n) (ExceptT e m), MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e, forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => SafeDiv (Either SomeBVException e) (SomeBV bv) m Source #

Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

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

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

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

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

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

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

type Rep SomeBVException Source #

Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

type Rep SomeBVException = D1 ('MetaData "SomeBVException" "Grisette.Internal.SymPrim.SomeBV" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) (C1 ('MetaCons "BitwidthMismatch" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UndeterminedBitwidth" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)))

Constructing and pattern matching on SomeBV

unsafeSomeBV :: Int -> (forall (proxy :: Nat -> Type) (n :: Nat). (KnownNat n, 1 <= n) => proxy n -> bv n) -> SomeBV bv Source #

Construct a SomeBV with a given run-time bitwidth and a polymorphic value for the underlying bitvector.

conBV :: forall (cbv :: Natural -> Type) (bv :: Natural -> Type). (forall (n :: Nat). (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV cbv -> SomeBV bv Source #

Construct a symbolic SomeBV with a given concrete SomeBV. Similar to con but for SomeBV.

>>> a = bv 8 0x12 :: SomeIntN
>>> conBV a :: SomeSymIntN
0x12

conBVView :: forall (cbv :: Natural -> Type) (bv :: Natural -> Type). (forall (n :: Nat). (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV bv -> Maybe (SomeBV cbv) Source #

View pattern for symbolic SomeBV to see if it contains a concrete value and extract it. Similar to conView but for SomeBV.

>>> conBVView (bv 8 0x12 :: SomeSymIntN)
Just 0x12
>>> conBVView (ssymBV 4 "a" :: SomeSymIntN)
Nothing

pattern ConBV :: (forall (n :: Nat). (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV cbv -> SomeBV bv Source #

Pattern synonym for symbolic SomeBV to see if it contains a concrete value and extract it. Similar to Con but for SomeBV.

>>> case (bv 8 0x12 :: SomeSymIntN) of { ConBV c -> c; _ -> error "impossible" }
0x12

symBV :: forall (cbv :: Natural -> Type) (bv :: Natural -> Type). (forall (n :: Nat). (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Symbol -> SomeBV bv Source #

Construct a symbolic SomeBV with a given run-time bitwidth and a symbol. Similar to sym but for SomeBV.

>>> symBV 8 "a" :: SomeSymIntN
a

ssymBV :: forall (cbv :: Natural -> Type) (bv :: Natural -> Type). (forall (n :: Nat). (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Identifier -> SomeBV bv Source #

Construct a symbolic SomeBV with a given run-time bitwidth and an identifier. Similar to ssym but for SomeBV.

>>> ssymBV 8 "a" :: SomeSymIntN
a

isymBV :: forall (cbv :: Natural -> Type) (bv :: Natural -> Type). (forall (n :: Nat). (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Identifier -> Int -> SomeBV bv Source #

Construct a symbolic SomeBV with a given run-time bitwidth, an identifier and an index. Similar to isym but for SomeBV.

>>> isymBV 8 "a" 1 :: SomeSymIntN
a@1

arbitraryBV :: forall (bv :: Nat -> Type). (forall (n :: Nat). (KnownNat n, 1 <= n) => Arbitrary (bv n)) => Int -> Gen (SomeBV bv) Source #

Generate an arbitrary SomeBV with a given run-time bitwidth.

Synonyms

pattern SomeIntN :: forall (n :: Nat). () => (KnownNat n, 1 <= n) => IntN n -> SomeIntN Source #

Pattern synonym for SomeBV for concrete signed bitvectors.

type SomeIntN = SomeBV IntN Source #

Type synonym for SomeBV for concrete signed bitvectors.

pattern SomeWordN :: forall (n :: Nat). () => (KnownNat n, 1 <= n) => WordN n -> SomeWordN Source #

Pattern synonym for SomeBV for concrete unsigned bitvectors.

type SomeWordN = SomeBV WordN Source #

Type synonym for SomeBV for concrete unsigned bitvectors.

pattern SomeSymIntN :: forall (n :: Nat). () => (KnownNat n, 1 <= n) => SymIntN n -> SomeSymIntN Source #

Pattern synonym for SomeBV for symbolic signed bitvectors.

type SomeSymIntN = SomeBV SymIntN Source #

Type synonym for SomeBV for symbolic signed bitvectors.

pattern SomeSymWordN :: forall (n :: Nat). () => (KnownNat n, 1 <= n) => SymWordN n -> SomeSymWordN Source #

Pattern synonym for SomeBV for symbolic unsigned bitvectors.

type SomeSymWordN = SomeBV SymWordN Source #

Type synonym for SomeBV for symbolic unsigned bitvectors.

Helpers for manipulating SomeBV

unarySomeBV :: (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r) -> (SomeBVLit -> r) -> SomeBV bv -> r Source #

Lift a unary operation on sized bitvectors that returns anything to SomeBV.

unarySomeBVR1 :: (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n) -> (SomeBVLit -> SomeBVLit) -> SomeBV bv -> SomeBV bv Source #

Lift a unary operation on sized bitvectors that returns a bitvector to SomeBV. The result will also be wrapped with SomeBV.

binSomeBV :: (forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r) -> (SomeBVLit -> SomeBVLit -> r) -> SomeBV bv -> SomeBV bv -> r Source #

Lift a binary operation on sized bitvectors that returns anything to SomeBV. Crash if the bitwidths do not match.

binSomeBVR1 :: (forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n) -> (SomeBVLit -> SomeBVLit -> SomeBVLit) -> SomeBV bv -> SomeBV bv -> SomeBV bv Source #

Lift a binary operation on sized bitvectors that returns a bitvector to SomeBV. The result will also be wrapped with SomeBV. Crash if the bitwidths do not match.

binSomeBVR2 :: (forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> (bv n, bv n)) -> (SomeBVLit -> SomeBVLit -> (SomeBVLit, SomeBVLit)) -> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv) Source #

Lift a binary operation on sized bitvectors that returns two bitvectors to SomeBV. The results will also be wrapped with SomeBV. Crash if the bitwidths do not match.

binSomeBVSafe :: (MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e, Mergeable r, forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m r) -> (SomeBVLit -> SomeBVLit -> ExceptT (Either SomeBVException e) m r) -> SomeBV bv -> SomeBV bv -> m r Source #

Lift a binary operation on sized bitvectors that returns anything wrapped with ExceptT to SomeBV. If the bitwidths do not match, throw an BitwidthMismatch error to the monadic context.

binSomeBVSafeR1 :: (MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e, forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n), forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n)) -> (SomeBVLit -> SomeBVLit -> ExceptT (Either SomeBVException e) m SomeBVLit) -> SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source #

Lift a binary operation on sized bitvectors that returns a bitvector wrapped with ExceptT to SomeBV. The result will also be wrapped with SomeBV.

If the bitwidths do not match, throw an BitwidthMismatch error to the monadic context.

binSomeBVSafeR2 :: (MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e, forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n), forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n, bv n)) -> (SomeBVLit -> SomeBVLit -> ExceptT (Either SomeBVException e) m (SomeBVLit, SomeBVLit)) -> SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv) Source #

Lift a binary operation on sized bitvectors that returns two bitvectors wrapped with ExceptT to SomeBV. The results will also be wrapped with SomeBV.

If the bitwidths do not match, throw an BitwidthMismatch error to the monadic context.