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	Safe-Inferred
Language	Haskell2010

Grisette.Internal.SymPrim.SomeBV

Contents

Constructing and pattern matching on SomeBV
Synonyms
Helpers for manipulating SomeBV

Description

Synopsis

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

Documentation

data SomeBV bv where Source #

Non-indexed bitvectors.

Constructors

SomeBV :: (KnownNat n, 1 <= n) => bv n -> SomeBV bv

Instances

Instances details

(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 (UnionM (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) #
(forall (n :: Nat). (KnownNat n, 1 <= n) => Bits (bv n)) => 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)) => 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)) => 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)) => 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)) => 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) => 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) => Eq (bv n)) => 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)) => 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) => EvaluateSym (bv n)) => EvaluateSym (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods evaluateSym :: Bool -> Model -> SomeBV bv -> SomeBV bv Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => ExtractSymbolics (bv n)) => ExtractSymbolics (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods extractSymbolics :: SomeBV bv -> SymbolSet Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => GPretty (bv n)) => GPretty (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods gpretty :: SomeBV bv -> Doc ann Source # gprettyPrec :: Int -> SomeBV bv -> Doc ann Source # gprettyList :: [SomeBV bv] -> Doc ann Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => ITEOp (bv n)) => ITEOp (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods symIte :: SymBool -> SomeBV bv -> SomeBV bv -> SomeBV bv 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 #
(forall (n :: Nat). (KnownNat n, 1 <= n) => SEq (bv n)) => SEq (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods (.==) :: SomeBV bv -> SomeBV bv -> SymBool Source # (./=) :: SomeBV bv -> SomeBV bv -> SymBool Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => SOrd (bv n)) => SOrd (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 -> UnionM Ordering Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => SubstituteSym (bv n)) => SubstituteSym (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SomeBV bv -> SomeBV bv Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => SymRotate (bv n)) => 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)) => 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) => AllSyms (bv n)) => 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)) => 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 (UnionM (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 (UnionM (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) => SafeDivision e (bv n) (ExceptT e m), MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e) => SafeDivision (Either BitwidthMismatch 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 #
(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 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 BitwidthMismatch e) m, TryMerge m, Mergeable e) => SafeSymRotate (Either BitwidthMismatch 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 BitwidthMismatch e) m, TryMerge m, Mergeable e) => SafeSymShift (Either BitwidthMismatch 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 #

Constructing and pattern matching on SomeBV

unsafeSomeBV :: forall bv. Int -> (forall proxy n. (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 bv. (forall n. (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 bv. (forall n. (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 cbv bv. (forall n. (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 bv. (forall n. (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 bv. (forall n. (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 bv. (forall n. (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. (forall n. (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 :: () => (KnownNat n, 1 <= n) => IntN n -> SomeIntN Source #

Pattern synonym for SomeBV with concrete signed bitvectors.

type SomeIntN = SomeBV IntN Source #

Type synonym for SomeBV with concrete signed bitvectors.

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

Pattern synonym for SomeBV with concrete unsigned bitvectors.

type SomeWordN = SomeBV WordN Source #

Type synonym for SomeBV with concrete unsigned bitvectors.

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

Pattern synonym for SomeBV with symbolic signed bitvectors.

type SomeSymIntN = SomeBV SymIntN Source #

Type synonym for SomeBV with symbolic signed bitvectors.

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

Pattern synonym for SomeBV with symbolic unsigned bitvectors.

type SomeSymWordN = SomeBV SymWordN Source #

Type synonym for SomeBV with symbolic unsigned bitvectors.

Helpers for manipulating SomeBV

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

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

unarySomeBVR1 :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n) -> 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. (KnownNat n, 1 <= n) => bv n -> bv n -> 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. (KnownNat n, 1 <= n) => bv n -> bv n -> bv n) -> 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. (KnownNat n, 1 <= n) => bv n -> bv n -> (bv n, bv n)) -> 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 BitwidthMismatch e) m, TryMerge m, Mergeable e, Mergeable r) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT 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 BitwidthMismatch e) m, TryMerge m, Mergeable e, forall n. (KnownNat n, 1 <= n) => Mergeable (bv n)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n)) -> 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 BitwidthMismatch e) m, TryMerge m, Mergeable e, forall n. (KnownNat n, 1 <= n) => Mergeable (bv n)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n, bv n)) -> 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.