Grisette.Internal.SymPrim.SymBV

Documentation

newtype SymWordN (n :: Nat)

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

>>> :set -XOverloadedStrings -XDataKinds -XBinaryLiterals
>>> "a" + 5 :: SymWordN 5
(+ 0b00101 a)
>>> sizedBVConcat (con 0b101 :: SymWordN 3) (con 0b110 :: SymWordN 3)
0b101110
>>> sizedBVExt (Proxy @6) (con 0b101 :: SymWordN 3)
0b000101
>>> (8 :: SymWordN 4) .< (7 :: SymWordN 4)
false

More symbolic operations are available. Please refer to the documentation for the type class instances.

Constructors

SymWordN

Fields

• underlyingWordNTerm :: Term (WordN n)

Instances

SizedBV SymWordN

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

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

sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymWordN l -> SymWordN 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 -> SymWordN n -> SymWordN w

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

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

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

Methods

fresh :: MonadFresh m => () -> m (UnionM (SymWordN n))

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

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

Methods

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

ToSym Word16 (SymWordN 16)

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

Methods

toSym :: Word16 -> SymWordN 16

ToSym Word32 (SymWordN 32)

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

Methods

toSym :: Word32 -> SymWordN 32

ToSym Word64 (SymWordN 64)

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

Methods

toSym :: Word64 -> SymWordN 64

ToSym Word8 (SymWordN 8)

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

Methods

toSym :: Word8 -> SymWordN 8

ToSym Word (SymWordN 64)

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

Methods

toSym :: Word -> SymWordN 64

Lift (SymWordN n :: Type)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeDivision ArithException (SymWordN n) m

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

Methods

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

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

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

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

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

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

(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymWordN n) m

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

Methods

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

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

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

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

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

Methods

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

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

(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeSymShift ArithException (SymWordN n) m

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

Methods

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

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

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

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

(KnownNat n, 1 <= n) => IsString (SymWordN n)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

fromString :: String -> SymWordN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

xor :: SymWordN n -> SymWordN n -> SymWordN n

complement :: SymWordN n -> SymWordN n

shift :: SymWordN n -> Int -> SymWordN n

rotate :: SymWordN n -> Int -> SymWordN n

zeroBits :: SymWordN n

bit :: Int -> SymWordN n

setBit :: SymWordN n -> Int -> SymWordN n

clearBit :: SymWordN n -> Int -> SymWordN n

complementBit :: SymWordN n -> Int -> SymWordN n

testBit :: SymWordN n -> Int -> Bool

bitSizeMaybe :: SymWordN n -> Maybe Int

bitSize :: SymWordN n -> Int

isSigned :: SymWordN n -> Bool

shiftL :: SymWordN n -> Int -> SymWordN n

unsafeShiftL :: SymWordN n -> Int -> SymWordN n

shiftR :: SymWordN n -> Int -> SymWordN n

unsafeShiftR :: SymWordN n -> Int -> SymWordN n

rotateL :: SymWordN n -> Int -> SymWordN n

rotateR :: SymWordN n -> Int -> SymWordN n

popCount :: SymWordN n -> Int

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

finiteBitSize :: SymWordN n -> Int

countLeadingZeros :: SymWordN n -> Int

countTrailingZeros :: SymWordN n -> Int

Generic (SymWordN n)

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

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

Methods

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

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

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

(+) :: SymWordN n -> SymWordN n -> SymWordN n

(-) :: SymWordN n -> SymWordN n -> SymWordN n

(*) :: SymWordN n -> SymWordN n -> SymWordN n

negate :: SymWordN n -> SymWordN n

abs :: SymWordN n -> SymWordN n

signum :: SymWordN n -> SymWordN n

fromInteger :: Integer -> SymWordN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

showsPrec :: Int -> SymWordN n -> ShowS

show :: SymWordN n -> String

showList :: [SymWordN n] -> ShowS

NFData (SymWordN n)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

rnf :: SymWordN n -> ()

(KnownNat n, 1 <= n) => Eq (SymWordN n)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

(KnownNat n, 1 <= n) => EvaluateSym (SymWordN n)

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

Methods

evaluateSym :: Bool -> Model -> SymWordN n -> SymWordN n

(KnownNat n, 1 <= n) => ExtractSymbolics (SymWordN n)

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

Methods

extractSymbolics :: SymWordN n -> SymbolSet

(KnownNat n, 1 <= n) => Apply (SymWordN n)

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type FunType (SymWordN n)

Methods

apply :: SymWordN n -> FunType (SymWordN n)

(KnownNat n, 1 <= n) => GPretty (SymWordN n)

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

Methods

gpretty :: SymWordN n -> Doc ann

gprettyPrec :: Int -> SymWordN n -> Doc ann

gprettyList :: [SymWordN n] -> Doc ann

(KnownNat n, 1 <= n) => ITEOp (SymWordN n)

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

Methods

symIte :: SymBool -> SymWordN n -> SymWordN n -> SymWordN n

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

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

Methods

rootStrategy :: MergingStrategy (SymWordN n)

(KnownNat n, 1 <= n) => SEq (SymWordN n)

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

Methods

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

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

(KnownNat n, 1 <= n) => SOrd (SymWordN n)

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

Methods

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

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

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

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

symCompare :: SymWordN n -> SymWordN n -> UnionM Ordering

(KnownNat n, 1 <= n) => SimpleMergeable (SymWordN n)

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

Methods

mrgIte :: SymBool -> SymWordN n -> SymWordN n -> SymWordN n

(KnownNat n, 1 <= n) => SubstituteSym (SymWordN n)

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

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SymWordN n -> SymWordN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

symRotate :: SymWordN n -> SymWordN n -> SymWordN n

symRotateNegated :: SymWordN n -> SymWordN n -> SymWordN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

symShift :: SymWordN n -> SymWordN n -> SymWordN n

symShiftNegated :: SymWordN n -> SymWordN n -> SymWordN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

allSyms :: SymWordN n -> [SomeSym]

(KnownNat n, 1 <= n) => ConRep (SymWordN n)

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type ConType (SymWordN n)

(KnownNat n, 1 <= n) => Hashable (SymWordN n)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

hashWithSalt :: Int -> SymWordN n -> Int

hash :: SymWordN n -> Int

ToCon (SymWordN 8) Word8

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

Methods

toCon :: SymWordN 8 -> Maybe Word8

ToCon (SymWordN 16) Word16

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

Methods

toCon :: SymWordN 16 -> Maybe Word16

ToCon (SymWordN 32) Word32

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

Methods

toCon :: SymWordN 32 -> Maybe Word32

ToCon (SymWordN 64) Word64

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

Methods

toCon :: SymWordN 64 -> Maybe Word64

ToCon (SymWordN 64) Word

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

Methods

toCon :: SymWordN 64 -> Maybe Word

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

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

Methods

fresh :: MonadFresh m => SymWordN n -> m (UnionM (SymWordN n))

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

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

Methods

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

(KnownNat n, 1 <= n) => SignConversion (SymWordN n) (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

toSigned :: SymWordN n -> SymIntN n

toUnsigned :: SymIntN n -> SymWordN 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 (SymWordN n) (WordN n)

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

Methods

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

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

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

Methods

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

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

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

Methods

toSym :: UnionM (WordN n) -> SymWordN 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) => ToSym (SymWordN n) (SymWordN n)

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

Methods

toSym :: SymWordN 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

type Rep (SymWordN n)

Defined in Grisette.Internal.SymPrim.SymBV

type Rep (SymWordN n) = D1 ('MetaData "SymWordN" "Grisette.Internal.SymPrim.SymBV" "grisette-0.5.0.1-IKpKourvCOdG0l1QW5fLHa" 'True) (C1 ('MetaCons "SymWordN" 'PrefixI 'True) (S1 ('MetaSel ('Just "underlyingWordNTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term (WordN n)))))

type FunType (SymWordN n)

Defined in Grisette.Internal.SymPrim.SymBV

type FunType (SymWordN n) = SymWordN n

type ConType (SymWordN n)

Defined in Grisette.Internal.SymPrim.SymBV

type ConType (SymWordN n) = WordN n

newtype SymIntN (n :: Nat)

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

>>> :set -XOverloadedStrings -XDataKinds -XBinaryLiterals
>>> "a" + 5 :: SymIntN 5
(+ 0b00101 a)
>>> sizedBVConcat (con 0b101 :: SymIntN 3) (con 0b110 :: SymIntN 3)
0b101110
>>> sizedBVExt (Proxy @6) (con 0b101 :: SymIntN 3)
0b111101
>>> (8 :: SymIntN 4) .< (7 :: SymIntN 4)
true

More symbolic operations are available. Please refer to the documentation for the type class instances.

Constructors

SymIntN

Fields

• underlyingIntNTerm :: Term (IntN n)

Instances

SizedBV SymIntN

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

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

sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymIntN l -> SymIntN 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 -> SymIntN n -> SymIntN w

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

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

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

Methods

fresh :: MonadFresh m => () -> m (UnionM (SymIntN n))

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

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

Methods

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

ToSym Int16 (SymIntN 16)

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

Methods

toSym :: Int16 -> SymIntN 16

ToSym Int32 (SymIntN 32)

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

Methods

toSym :: Int32 -> SymIntN 32

ToSym Int64 (SymIntN 64)

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

Methods

toSym :: Int64 -> SymIntN 64

ToSym Int8 (SymIntN 8)

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

Methods

toSym :: Int8 -> SymIntN 8

ToSym Int (SymIntN 64)

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

Methods

toSym :: Int -> SymIntN 64

Lift (SymIntN n :: Type)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeDivision ArithException (SymIntN n) m

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

Methods

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

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

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

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

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

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

(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymIntN n) m

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

Methods

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

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

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

(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeSymRotate ArithException (SymIntN n) m

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

Methods

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

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

(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeSymShift ArithException (SymIntN n) m

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

Methods

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

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

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

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

(KnownNat n, 1 <= n) => IsString (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

fromString :: String -> SymIntN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

xor :: SymIntN n -> SymIntN n -> SymIntN n

complement :: SymIntN n -> SymIntN n

shift :: SymIntN n -> Int -> SymIntN n

rotate :: SymIntN n -> Int -> SymIntN n

zeroBits :: SymIntN n

bit :: Int -> SymIntN n

setBit :: SymIntN n -> Int -> SymIntN n

clearBit :: SymIntN n -> Int -> SymIntN n

complementBit :: SymIntN n -> Int -> SymIntN n

testBit :: SymIntN n -> Int -> Bool

bitSizeMaybe :: SymIntN n -> Maybe Int

bitSize :: SymIntN n -> Int

isSigned :: SymIntN n -> Bool

shiftL :: SymIntN n -> Int -> SymIntN n

unsafeShiftL :: SymIntN n -> Int -> SymIntN n

shiftR :: SymIntN n -> Int -> SymIntN n

unsafeShiftR :: SymIntN n -> Int -> SymIntN n

rotateL :: SymIntN n -> Int -> SymIntN n

rotateR :: SymIntN n -> Int -> SymIntN n

popCount :: SymIntN n -> Int

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

finiteBitSize :: SymIntN n -> Int

countLeadingZeros :: SymIntN n -> Int

countTrailingZeros :: SymIntN n -> Int

Generic (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

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

Methods

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

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

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

(+) :: SymIntN n -> SymIntN n -> SymIntN n

(-) :: SymIntN n -> SymIntN n -> SymIntN n

(*) :: SymIntN n -> SymIntN n -> SymIntN n

negate :: SymIntN n -> SymIntN n

abs :: SymIntN n -> SymIntN n

signum :: SymIntN n -> SymIntN n

fromInteger :: Integer -> SymIntN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

showsPrec :: Int -> SymIntN n -> ShowS

show :: SymIntN n -> String

showList :: [SymIntN n] -> ShowS

NFData (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

rnf :: SymIntN n -> ()

(KnownNat n, 1 <= n) => Eq (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

(KnownNat n, 1 <= n) => EvaluateSym (SymIntN n)

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

Methods

evaluateSym :: Bool -> Model -> SymIntN n -> SymIntN n

(KnownNat n, 1 <= n) => ExtractSymbolics (SymIntN n)

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

Methods

extractSymbolics :: SymIntN n -> SymbolSet

(KnownNat n, 1 <= n) => Apply (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type FunType (SymIntN n)

Methods

apply :: SymIntN n -> FunType (SymIntN n)

(KnownNat n, 1 <= n) => GPretty (SymIntN n)

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

Methods

gpretty :: SymIntN n -> Doc ann

gprettyPrec :: Int -> SymIntN n -> Doc ann

gprettyList :: [SymIntN n] -> Doc ann

(KnownNat n, 1 <= n) => ITEOp (SymIntN n)

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

Methods

symIte :: SymBool -> SymIntN n -> SymIntN n -> SymIntN n

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

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

Methods

rootStrategy :: MergingStrategy (SymIntN n)

(KnownNat n, 1 <= n) => SEq (SymIntN n)

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

Methods

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

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

(KnownNat n, 1 <= n) => SOrd (SymIntN n)

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

Methods

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

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

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

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

symCompare :: SymIntN n -> SymIntN n -> UnionM Ordering

(KnownNat n, 1 <= n) => SimpleMergeable (SymIntN n)

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

Methods

mrgIte :: SymBool -> SymIntN n -> SymIntN n -> SymIntN n

(KnownNat n, 1 <= n) => SubstituteSym (SymIntN n)

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

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SymIntN n -> SymIntN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

symRotate :: SymIntN n -> SymIntN n -> SymIntN n

symRotateNegated :: SymIntN n -> SymIntN n -> SymIntN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

symShift :: SymIntN n -> SymIntN n -> SymIntN n

symShiftNegated :: SymIntN n -> SymIntN n -> SymIntN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

allSyms :: SymIntN n -> [SomeSym]

(KnownNat n, 1 <= n) => ConRep (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type ConType (SymIntN n)

(KnownNat n, 1 <= n) => Hashable (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

hashWithSalt :: Int -> SymIntN n -> Int

hash :: SymIntN n -> Int

ToCon (SymIntN 8) Int8

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

Methods

toCon :: SymIntN 8 -> Maybe Int8

ToCon (SymIntN 16) Int16

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

Methods

toCon :: SymIntN 16 -> Maybe Int16

ToCon (SymIntN 32) Int32

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

Methods

toCon :: SymIntN 32 -> Maybe Int32

ToCon (SymIntN 64) Int64

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

Methods

toCon :: SymIntN 64 -> Maybe Int64

ToCon (SymIntN 64) Int

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

Methods

toCon :: SymIntN 64 -> Maybe Int

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

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

Methods

fresh :: MonadFresh m => SymIntN n -> m (UnionM (SymIntN n))

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

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

Methods

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

(KnownNat n, 1 <= n) => SignConversion (SymWordN n) (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

toSigned :: SymWordN n -> SymIntN n

toUnsigned :: SymIntN n -> SymWordN 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 (SymIntN n) (IntN n)

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

Methods

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

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

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

Methods

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

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

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

Methods

toSym :: UnionM (IntN n) -> SymIntN 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) => ToSym (SymIntN n) (SymIntN n)

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

Methods

toSym :: SymIntN 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

type Rep (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

type Rep (SymIntN n) = D1 ('MetaData "SymIntN" "Grisette.Internal.SymPrim.SymBV" "grisette-0.5.0.1-IKpKourvCOdG0l1QW5fLHa" 'True) (C1 ('MetaCons "SymIntN" 'PrefixI 'True) (S1 ('MetaSel ('Just "underlyingIntNTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term (IntN n)))))

type FunType (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

type FunType (SymIntN n) = SymIntN n

type ConType (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

type ConType (SymIntN n) = IntN n

Orphan instances

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

Associated Types

type SymType (IntN n)

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

Associated Types

type SymType (WordN n)

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

Methods

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

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

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

Methods

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

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