Copyright	(c) Sirui Lu 2021-2023
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.SymBV

Contents

Orphan instances

Description

Synopsis

newtype SymWordN (n :: Nat) = SymWordN {
- underlyingWordNTerm :: Term (WordN n)
}
newtype SymIntN (n :: Nat) = SymIntN {
- underlyingIntNTerm :: Term (IntN n)
}

Documentation

newtype SymWordN (n :: Nat) Source #

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

Instances details

SizedBV SymWordN Source #
Instance details 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) Source # sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymWordN l -> SymWordN r Source # sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymWordN l -> SymWordN r Source # sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymWordN l -> SymWordN r Source # 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 Source # sizedBVFromIntegral :: forall a (n :: Nat). (Integral a, KnownNat n, 1 <= n) => a -> SymWordN n Source #
(KnownNat n, 1 <= n) => GenSym () (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => () -> m (UnionM (SymWordN n)) Source #
(KnownNat n, 1 <= n) => GenSymSimple () (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods simpleFresh :: MonadFresh m => () -> m (SymWordN n) Source #
ToSym Word16 (SymWordN 16) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Word16 -> SymWordN 16 Source #
ToSym Word32 (SymWordN 32) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Word32 -> SymWordN 32 Source #
ToSym Word64 (SymWordN 64) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Word64 -> SymWordN 64 Source #
ToSym Word8 (SymWordN 8) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Word8 -> SymWordN 8 Source #
ToSym Word (SymWordN 64) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Word -> SymWordN 64 Source #
Lift (SymWordN n :: Type) Source #
Instance details 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 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeMod :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeDivMod :: SymWordN n -> SymWordN n -> m (SymWordN n, SymWordN n) Source # safeQuot :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeRem :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeQuotRem :: SymWordN n -> SymWordN n -> m (SymWordN n, SymWordN n) Source #
(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymWordN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith Methods safeAdd :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeNeg :: SymWordN n -> m (SymWordN n) Source # safeSub :: SymWordN n -> SymWordN n -> m (SymWordN n) Source #
(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymRotate ArithException (SymWordN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate Methods safeSymRotateL :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeSymRotateR :: SymWordN n -> SymWordN n -> m (SymWordN n) Source #
(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeSymShift ArithException (SymWordN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymShift Methods safeSymShiftL :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeSymShiftR :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeSymStrictShiftL :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeSymStrictShiftR :: SymWordN n -> SymWordN n -> m (SymWordN n) Source #
(KnownNat n, 1 <= n) => IsString (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods fromString :: String -> SymWordN n #
(KnownNat n, 1 <= n) => Bits (SymWordN n) Source #
Instance details 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) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods finiteBitSize :: SymWordN n -> Int # countLeadingZeros :: SymWordN n -> Int # countTrailingZeros :: SymWordN n -> Int #
Generic (SymWordN n) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods showsPrec :: Int -> SymWordN n -> ShowS # show :: SymWordN n -> String # showList :: [SymWordN n] -> ShowS #
NFData (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods rnf :: SymWordN n -> () #
(KnownNat n, 1 <= n) => Eq (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods (==) :: SymWordN n -> SymWordN n -> Bool # (/=) :: SymWordN n -> SymWordN n -> Bool #
(KnownNat n, 1 <= n) => EvaluateSym (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.EvaluateSym Methods evaluateSym :: Bool -> Model -> SymWordN n -> SymWordN n Source #
(KnownNat n, 1 <= n) => ExtractSymbolics (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: SymWordN n -> SymbolSet Source #
(KnownNat n, 1 <= n) => Apply (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Associated Types type FunType (SymWordN n) Source # Methods apply :: SymWordN n -> FunType (SymWordN n) Source #
(KnownNat n, 1 <= n) => GPretty (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GPretty Methods gpretty :: SymWordN n -> Doc ann Source # gprettyPrec :: Int -> SymWordN n -> Doc ann Source # gprettyList :: [SymWordN n] -> Doc ann Source #
(KnownNat n, 1 <= n) => ITEOp (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ITEOp Methods symIte :: SymBool -> SymWordN n -> SymWordN n -> SymWordN n Source #
(KnownNat n, 1 <= n) => Mergeable (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy (SymWordN n) Source #
(KnownNat n, 1 <= n) => SEq (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: SymWordN n -> SymWordN n -> SymBool Source # (./=) :: SymWordN n -> SymWordN n -> SymBool Source #
(KnownNat n, 1 <= n) => SOrd (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: SymWordN n -> SymWordN n -> SymBool Source # (.<=) :: SymWordN n -> SymWordN n -> SymBool Source # (.>) :: SymWordN n -> SymWordN n -> SymBool Source # (.>=) :: SymWordN n -> SymWordN n -> SymBool Source # symCompare :: SymWordN n -> SymWordN n -> UnionM Ordering Source #
(KnownNat n, 1 <= n) => SimpleMergeable (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> SymWordN n -> SymWordN n -> SymWordN n Source #
(KnownNat n, 1 <= n) => SubstituteSym (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SymWordN n -> SymWordN n Source #
(KnownNat n, 1 <= n) => SymRotate (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods symRotate :: SymWordN n -> SymWordN n -> SymWordN n Source # symRotateNegated :: SymWordN n -> SymWordN n -> SymWordN n Source #
(KnownNat n, 1 <= n) => SymShift (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods symShift :: SymWordN n -> SymWordN n -> SymWordN n Source # symShiftNegated :: SymWordN n -> SymWordN n -> SymWordN n Source #
(KnownNat n, 1 <= n) => AllSyms (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods allSymsS :: SymWordN n -> [SomeSym] -> [SomeSym] Source # allSyms :: SymWordN n -> [SomeSym] Source #
(KnownNat n, 1 <= n) => ConRep (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Associated Types type ConType (SymWordN n) Source #
(KnownNat n, 1 <= n) => Hashable (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods hashWithSalt :: Int -> SymWordN n -> Int # hash :: SymWordN n -> Int #
ToCon (SymWordN 8) Word8 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: SymWordN 8 -> Maybe Word8 Source #
ToCon (SymWordN 16) Word16 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: SymWordN 16 -> Maybe Word16 Source #
ToCon (SymWordN 32) Word32 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: SymWordN 32 -> Maybe Word32 Source #
ToCon (SymWordN 64) Word64 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: SymWordN 64 -> Maybe Word64 Source #
ToCon (SymWordN 64) Word Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: SymWordN 64 -> Maybe Word Source #
(KnownNat n, 1 <= n) => GenSym (SymWordN n) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => SymWordN n -> m (UnionM (SymWordN n)) Source #
(KnownNat n, 1 <= n) => GenSymSimple (SymWordN n) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods simpleFresh :: MonadFresh m => SymWordN n -> m (SymWordN n) Source #
(KnownNat n, 1 <= n) => SignConversion (SymWordN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods toSigned :: SymWordN n -> SymIntN n Source # toUnsigned :: SymIntN n -> SymWordN n Source #
(KnownNat n, 1 <= n) => Solvable (WordN n) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods con :: WordN n -> SymWordN n Source # conView :: SymWordN n -> Maybe (WordN n) Source # sym :: Symbol -> SymWordN n Source # ssym :: Identifier -> SymWordN n Source # isym :: Identifier -> Int -> SymWordN n Source #
(KnownNat n, 1 <= n) => ToCon (SymWordN n) (WordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: SymWordN n -> Maybe (WordN n) Source #
(KnownNat n, 1 <= n) => ToCon (SymWordN n) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: SymWordN n -> Maybe (SymWordN n) Source #
(KnownNat n, 1 <= n) => ToSym (UnionM (WordN n)) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Control.Monad.UnionM Methods toSym :: UnionM (WordN n) -> SymWordN n Source #
(KnownNat n, 1 <= n) => ToSym (WordN n) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: WordN n -> SymWordN n Source #
(KnownNat n, 1 <= n) => ToSym (SymWordN n) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: SymWordN n -> SymWordN n Source #
(KnownNat n, 1 <= n) => LinkedRep (WordN n) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods underlyingTerm :: SymWordN n -> Term (WordN n) Source # wrapTerm :: Term (WordN n) -> SymWordN n Source #
type Rep (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV type Rep (SymWordN n) = D1 ('MetaData "SymWordN" "Grisette.Internal.SymPrim.SymBV" "grisette-0.5.0.0-2ZDAuzWdzg48yPrBcRstUR" 'True) (C1 ('MetaCons "SymWordN" 'PrefixI 'True) (S1 ('MetaSel ('Just "underlyingWordNTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term (WordN n)))))
type FunType (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV type FunType (SymWordN n) = SymWordN n
type ConType (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV type ConType (SymWordN n) = WordN n

newtype SymIntN (n :: Nat) Source #

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

Instances details

SizedBV SymIntN Source #
Instance details 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) Source # sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymIntN l -> SymIntN r Source # sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymIntN l -> SymIntN r Source # sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymIntN l -> SymIntN r Source # 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 Source # sizedBVFromIntegral :: forall a (n :: Nat). (Integral a, KnownNat n, 1 <= n) => a -> SymIntN n Source #
(KnownNat n, 1 <= n) => GenSym () (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => () -> m (UnionM (SymIntN n)) Source #
(KnownNat n, 1 <= n) => GenSymSimple () (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods simpleFresh :: MonadFresh m => () -> m (SymIntN n) Source #
ToSym Int16 (SymIntN 16) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Int16 -> SymIntN 16 Source #
ToSym Int32 (SymIntN 32) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Int32 -> SymIntN 32 Source #
ToSym Int64 (SymIntN 64) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Int64 -> SymIntN 64 Source #
ToSym Int8 (SymIntN 8) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Int8 -> SymIntN 8 Source #
ToSym Int (SymIntN 64) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Int -> SymIntN 64 Source #
Lift (SymIntN n :: Type) Source #
Instance details 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 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeMod :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeDivMod :: SymIntN n -> SymIntN n -> m (SymIntN n, SymIntN n) Source # safeQuot :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeRem :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeQuotRem :: SymIntN n -> SymIntN n -> m (SymIntN n, SymIntN n) Source #
(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymIntN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith Methods safeAdd :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeNeg :: SymIntN n -> m (SymIntN n) Source # safeSub :: SymIntN n -> SymIntN n -> m (SymIntN n) Source #
(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeSymRotate ArithException (SymIntN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate Methods safeSymRotateL :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeSymRotateR :: SymIntN n -> SymIntN n -> m (SymIntN n) Source #
(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeSymShift ArithException (SymIntN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymShift Methods safeSymShiftL :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeSymShiftR :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeSymStrictShiftL :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeSymStrictShiftR :: SymIntN n -> SymIntN n -> m (SymIntN n) Source #
(KnownNat n, 1 <= n) => IsString (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods fromString :: String -> SymIntN n #
(KnownNat n, 1 <= n) => Bits (SymIntN n) Source #
Instance details 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) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods finiteBitSize :: SymIntN n -> Int # countLeadingZeros :: SymIntN n -> Int # countTrailingZeros :: SymIntN n -> Int #
Generic (SymIntN n) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods showsPrec :: Int -> SymIntN n -> ShowS # show :: SymIntN n -> String # showList :: [SymIntN n] -> ShowS #
NFData (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods rnf :: SymIntN n -> () #
(KnownNat n, 1 <= n) => Eq (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods (==) :: SymIntN n -> SymIntN n -> Bool # (/=) :: SymIntN n -> SymIntN n -> Bool #
(KnownNat n, 1 <= n) => EvaluateSym (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.EvaluateSym Methods evaluateSym :: Bool -> Model -> SymIntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => ExtractSymbolics (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: SymIntN n -> SymbolSet Source #
(KnownNat n, 1 <= n) => Apply (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Associated Types type FunType (SymIntN n) Source # Methods apply :: SymIntN n -> FunType (SymIntN n) Source #
(KnownNat n, 1 <= n) => GPretty (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GPretty Methods gpretty :: SymIntN n -> Doc ann Source # gprettyPrec :: Int -> SymIntN n -> Doc ann Source # gprettyList :: [SymIntN n] -> Doc ann Source #
(KnownNat n, 1 <= n) => ITEOp (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ITEOp Methods symIte :: SymBool -> SymIntN n -> SymIntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => Mergeable (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy (SymIntN n) Source #
(KnownNat n, 1 <= n) => SEq (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: SymIntN n -> SymIntN n -> SymBool Source # (./=) :: SymIntN n -> SymIntN n -> SymBool Source #
(KnownNat n, 1 <= n) => SOrd (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: SymIntN n -> SymIntN n -> SymBool Source # (.<=) :: SymIntN n -> SymIntN n -> SymBool Source # (.>) :: SymIntN n -> SymIntN n -> SymBool Source # (.>=) :: SymIntN n -> SymIntN n -> SymBool Source # symCompare :: SymIntN n -> SymIntN n -> UnionM Ordering Source #
(KnownNat n, 1 <= n) => SimpleMergeable (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> SymIntN n -> SymIntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => SubstituteSym (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SymIntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => SymRotate (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods symRotate :: SymIntN n -> SymIntN n -> SymIntN n Source # symRotateNegated :: SymIntN n -> SymIntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => SymShift (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods symShift :: SymIntN n -> SymIntN n -> SymIntN n Source # symShiftNegated :: SymIntN n -> SymIntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => AllSyms (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods allSymsS :: SymIntN n -> [SomeSym] -> [SomeSym] Source # allSyms :: SymIntN n -> [SomeSym] Source #
(KnownNat n, 1 <= n) => ConRep (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Associated Types type ConType (SymIntN n) Source #
(KnownNat n, 1 <= n) => Hashable (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods hashWithSalt :: Int -> SymIntN n -> Int # hash :: SymIntN n -> Int #
ToCon (SymIntN 8) Int8 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: SymIntN 8 -> Maybe Int8 Source #
ToCon (SymIntN 16) Int16 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: SymIntN 16 -> Maybe Int16 Source #
ToCon (SymIntN 32) Int32 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: SymIntN 32 -> Maybe Int32 Source #
ToCon (SymIntN 64) Int64 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: SymIntN 64 -> Maybe Int64 Source #
ToCon (SymIntN 64) Int Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: SymIntN 64 -> Maybe Int Source #
(KnownNat n, 1 <= n) => GenSym (SymIntN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => SymIntN n -> m (UnionM (SymIntN n)) Source #
(KnownNat n, 1 <= n) => GenSymSimple (SymIntN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods simpleFresh :: MonadFresh m => SymIntN n -> m (SymIntN n) Source #
(KnownNat n, 1 <= n) => SignConversion (SymWordN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods toSigned :: SymWordN n -> SymIntN n Source # toUnsigned :: SymIntN n -> SymWordN n Source #
(KnownNat n, 1 <= n) => Solvable (IntN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods con :: IntN n -> SymIntN n Source # conView :: SymIntN n -> Maybe (IntN n) Source # sym :: Symbol -> SymIntN n Source # ssym :: Identifier -> SymIntN n Source # isym :: Identifier -> Int -> SymIntN n Source #
(KnownNat n, 1 <= n) => ToCon (SymIntN n) (IntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: SymIntN n -> Maybe (IntN n) Source #
(KnownNat n, 1 <= n) => ToCon (SymIntN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: SymIntN n -> Maybe (SymIntN n) Source #
(KnownNat n, 1 <= n) => ToSym (UnionM (IntN n)) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Control.Monad.UnionM Methods toSym :: UnionM (IntN n) -> SymIntN n Source #
(KnownNat n, 1 <= n) => ToSym (IntN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: IntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => ToSym (SymIntN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: SymIntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => LinkedRep (IntN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods underlyingTerm :: SymIntN n -> Term (IntN n) Source # wrapTerm :: Term (IntN n) -> SymIntN n Source #
type Rep (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV type Rep (SymIntN n) = D1 ('MetaData "SymIntN" "Grisette.Internal.SymPrim.SymBV" "grisette-0.5.0.0-2ZDAuzWdzg48yPrBcRstUR" 'True) (C1 ('MetaCons "SymIntN" 'PrefixI 'True) (S1 ('MetaSel ('Just "underlyingIntNTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term (IntN n)))))
type FunType (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV type FunType (SymIntN n) = SymIntN n
type ConType (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV type ConType (SymIntN n) = IntN n

Orphan instances

(KnownNat n, 1 <= n) => SymRep (IntN n) Source #
Instance details Associated Types type SymType (IntN n) Source #
(KnownNat n, 1 <= n) => SymRep (WordN n) Source #
Instance details Associated Types type SymType (WordN n) Source #
(KnownNat n, 1 <= n) => LinkedRep (IntN n) (SymIntN n) Source #
Instance details Methods underlyingTerm :: SymIntN n -> Term (IntN n) Source # wrapTerm :: Term (IntN n) -> SymIntN n Source #
(KnownNat n, 1 <= n) => LinkedRep (WordN n) (SymWordN n) Source #
Instance details Methods underlyingTerm :: SymWordN n -> Term (WordN n) Source # wrapTerm :: Term (WordN n) -> SymWordN n Source #