Grisette.Internal.SymPrim.SomeBV

Documentation

data SomeBV bv where

Non-indexed bitvectors.

Constructors

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

Instances

(forall (n :: Nat). (KnownNat n, 1 <= n) => GenSym () (bv n), Mergeable (SomeBV bv)) => GenSym Int (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

fresh :: MonadFresh m => Int -> m (UnionM (SomeBV bv))

(forall (n :: Nat). (KnownNat n, 1 <= n) => GenSymSimple () (bv n), Mergeable (SomeBV bv)) => GenSymSimple Int (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

simpleFresh :: MonadFresh m => Int -> m (SomeBV bv)

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

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)

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)

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)

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)

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)

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)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

toRational :: SomeBV bv -> Rational

(forall (n :: Nat). (KnownNat n, 1 <= n) => Show (bv n)) => Show (SomeBV bv)

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)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

rnf :: SomeBV bv -> ()

(forall (n :: Nat). (KnownNat n, 1 <= n) => Eq (bv n)) => Eq (SomeBV bv)

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)

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)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

bvConcat :: SomeBV bv -> SomeBV bv -> SomeBV bv

bvZext :: Int -> SomeBV bv -> SomeBV bv

bvSext :: Int -> SomeBV bv -> SomeBV bv

bvExt :: Int -> SomeBV bv -> SomeBV bv

bvSelect :: Int -> Int -> SomeBV bv -> SomeBV bv

bv :: Integral a => Int -> a -> SomeBV bv

(forall (n :: Nat). (KnownNat n, 1 <= n) => EvaluateSym (bv n)) => EvaluateSym (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

evaluateSym :: Bool -> Model -> SomeBV bv -> SomeBV bv

(forall (n :: Nat). (KnownNat n, 1 <= n) => ExtractSymbolics (bv n)) => ExtractSymbolics (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

extractSymbolics :: SomeBV bv -> SymbolSet

(forall (n :: Nat). (KnownNat n, 1 <= n) => GPretty (bv n)) => GPretty (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

gpretty :: SomeBV bv -> Doc ann

gprettyPrec :: Int -> SomeBV bv -> Doc ann

gprettyList :: [SomeBV bv] -> Doc ann

(forall (n :: Nat). (KnownNat n, 1 <= n) => ITEOp (bv n)) => ITEOp (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

symIte :: SymBool -> SomeBV bv -> SomeBV bv -> SomeBV bv

(forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) => Mergeable (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

rootStrategy :: MergingStrategy (SomeBV bv)

(forall (n :: Nat). (KnownNat n, 1 <= n) => SEq (bv n)) => SEq (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

(.==) :: SomeBV bv -> SomeBV bv -> SymBool

(./=) :: SomeBV bv -> SomeBV bv -> SymBool

(forall (n :: Nat). (KnownNat n, 1 <= n) => SOrd (bv n)) => SOrd (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

(.<) :: SomeBV bv -> SomeBV bv -> SymBool

(.<=) :: SomeBV bv -> SomeBV bv -> SymBool

(.>) :: SomeBV bv -> SomeBV bv -> SymBool

(.>=) :: SomeBV bv -> SomeBV bv -> SymBool

symCompare :: SomeBV bv -> SomeBV bv -> UnionM Ordering

(forall (n :: Nat). (KnownNat n, 1 <= n) => SubstituteSym (bv n)) => SubstituteSym (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SomeBV bv -> SomeBV bv

(forall (n :: Nat). (KnownNat n, 1 <= n) => SymRotate (bv n)) => SymRotate (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

symRotate :: SomeBV bv -> SomeBV bv -> SomeBV bv

symRotateNegated :: SomeBV bv -> SomeBV bv -> SomeBV bv

(forall (n :: Nat). (KnownNat n, 1 <= n) => SymShift (bv n)) => SymShift (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

symShift :: SomeBV bv -> SomeBV bv -> SomeBV bv

symShiftNegated :: SomeBV bv -> SomeBV bv -> SomeBV bv

(forall (n :: Nat). (KnownNat n, 1 <= n) => AllSyms (bv n)) => AllSyms (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

allSymsS :: SomeBV bv -> [SomeSym] -> [SomeSym]

allSyms :: SomeBV bv -> [SomeSym]

(forall (n :: Nat). (KnownNat n, 1 <= n) => Hashable (bv n)) => Hashable (SomeBV bv)

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)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

fresh :: MonadFresh m => SomeBV bv -> m (UnionM (SomeBV bv))

(forall (m :: Nat). (KnownNat m, 1 <= m) => GenSymSimple () (bv m), Mergeable (SomeBV bv)) => GenSymSimple (SomeBV bv) (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

simpleFresh :: MonadFresh m => SomeBV bv -> m (SomeBV bv)

(forall (n :: Nat). (KnownNat n, 1 <= n) => SignConversion (ubv n) (sbv n), SignConversion (ubv 1) (sbv 1)) => SignConversion (SomeBV ubv) (SomeBV sbv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

toSigned :: SomeBV ubv -> SomeBV sbv

toUnsigned :: SomeBV sbv -> SomeBV ubv

(forall (n :: Nat). (KnownNat n, 1 <= n) => ToCon (sbv n) (cbv n)) => ToCon (SomeBV sbv) (SomeBV cbv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

toCon :: SomeBV sbv -> Maybe (SomeBV cbv)

(forall (n :: Nat). (KnownNat n, 1 <= n) => ToSym (cbv n) (sbv n)) => ToSym (SomeBV cbv) (SomeBV sbv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

toSym :: SomeBV cbv -> SomeBV sbv

(KnownNat n, 1 <= n, forall (m :: Nat). (KnownNat m, 1 <= m) => GenSym () (bv m), Mergeable (SomeBV bv)) => GenSym (Proxy n) (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

fresh :: MonadFresh m => Proxy n -> m (UnionM (SomeBV bv))

(KnownNat n, 1 <= n, forall (m :: Nat). (KnownNat m, 1 <= m) => GenSymSimple () (bv m), Mergeable (SomeBV bv)) => GenSymSimple (Proxy n) (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

simpleFresh :: MonadFresh m => Proxy n -> m (SomeBV bv)

(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)

Constructing and pattern matching on SomeBV

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

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

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)

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

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

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

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

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)

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

Synonyms

pattern SomeIntN :: () => (KnownNat n, 1 <= n) => IntN n -> SomeIntN

Pattern synonym for SomeBV with concrete signed bitvectors.

type SomeIntN = SomeBV IntN

Type synonym for SomeBV with concrete signed bitvectors.

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

Pattern synonym for SomeBV with concrete unsigned bitvectors.

type SomeWordN = SomeBV WordN

Type synonym for SomeBV with concrete unsigned bitvectors.

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

Pattern synonym for SomeBV with symbolic signed bitvectors.

type SomeSymIntN = SomeBV SymIntN

Type synonym for SomeBV with symbolic signed bitvectors.

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

Pattern synonym for SomeBV with symbolic unsigned bitvectors.

type SomeSymWordN = SomeBV SymWordN

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

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

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

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

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)

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

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)

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)

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.