grisette-0.5.0.1: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2023
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellSafe-Inferred
LanguageHaskell2010

Grisette.Internal.SymPrim.SymBV

Description

 
Synopsis

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 

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

(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

(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

(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

(KnownNat n, 1 <= n) => FiniteBits (SymWordN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymBV

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

(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

(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

(KnownNat n, 1 <= n) => SEq (SymWordN n) Source # 
Instance details

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

(KnownNat n, 1 <= n) => SOrd (SymWordN n) Source # 
Instance details

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

(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

(KnownNat n, 1 <= n) => SymShift (SymWordN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymBV

(KnownNat n, 1 <= n) => AllSyms (SymWordN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymBV

(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

(KnownNat n, 1 <= n) => Solvable (WordN n) (SymWordN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymBV

(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

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.1-IKpKourvCOdG0l1QW5fLHa" '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 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 

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

(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

(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

(KnownNat n, 1 <= n) => FiniteBits (SymIntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymBV

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

(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

(KnownNat n, 1 <= n) => SEq (SymIntN n) Source # 
Instance details

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

(KnownNat n, 1 <= n) => SOrd (SymIntN n) Source # 
Instance details

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

(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

(KnownNat n, 1 <= n) => SymShift (SymIntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymBV

(KnownNat n, 1 <= n) => AllSyms (SymIntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymBV

(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

(KnownNat n, 1 <= n) => Solvable (IntN n) (SymIntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymBV

(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

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.1-IKpKourvCOdG0l1QW5fLHa" '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

(KnownNat n, 1 <= n) => LinkedRep (WordN n) (SymWordN n) Source # 
Instance details