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	None
Language	Haskell2010

Grisette.Internal.SymPrim.SymBV

Contents

Orphan instances

Description

Synopsis

newtype SymWordN (n :: Nat) = SymWordN (Term (WordN n))
type SymWordN8 = SymWordN 8
type SymWordN16 = SymWordN 16
type SymWordN32 = SymWordN 32
type SymWordN64 = SymWordN 64
newtype SymIntN (n :: Nat) = SymIntN (Term (IntN n))
type SymIntN8 = SymIntN 8
type SymIntN16 = SymIntN 16
type SymIntN32 = SymIntN 32
type SymIntN64 = SymIntN 64

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.

>>> "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 operations are available. Please refer to Grisette.Core for more information.

Constructors

SymWordN (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 #

UnifiedFiniteBits 'S SomeSymWordN Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits

Methods

withBaseFiniteBits :: (If (IsConMode 'S) (FiniteBits SomeSymWordN, FromBits SomeSymWordN) (SymFiniteBits SomeSymWordN) => r) -> r Source #

(KnownNat n, 1 <= n) => UnifiedBVImpl 'S SymWordN SymIntN n (SymWordN n) (SymIntN n) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedBV

Associated Types

type GetWordN 'S
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedBV type GetWordN 'S = SymWordN
type GetIntN 'S
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedBV type GetIntN 'S = SymIntN

(KnownNat n, 1 <= n) => UnifiedFromIntegral 'S SymInteger (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'S) (Integral SymInteger, Num (SymWordN n)) (SymFromIntegral SymInteger (SymWordN n)) => r) -> r Source #

(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeDiv 'S ArithException (SymWordN n) m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

Methods

withBaseSafeDiv :: (SafeDiv ArithException (SymWordN n) m => r) -> r Source #

(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeLinearArith 'S ArithException (SymWordN n) m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

Methods

withBaseSafeLinearArith :: (SafeLinearArith ArithException (SymWordN n) m => r) -> r Source #

(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeSymRotate 'S ArithException (SymWordN n) m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate

Methods

withBaseSafeSymRotate :: (SafeSymRotate ArithException (SymWordN n) m => r) -> r Source #

(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeSymShift 'S ArithException (SymWordN n) m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift

Methods

withBaseSafeSymShift :: (SafeSymShift ArithException (SymWordN n) m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP 'S NotRepresentableFPError (SymWordN n) (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (SymWordN n) (SymFP eb sb) SymFPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) => UnifiedSafeBitCast 'S NotRepresentableFPError (SymFP eb sb) (SymWordN n) m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeBitCast

Methods

withBaseSafeBitCast :: (SafeBitCast NotRepresentableFPError (SymFP eb sb) (SymWordN n) m => r) -> r Source #

BitCast SymBool (SymWordN 1) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

bitCast :: SymBool -> SymWordN 1 Source #

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

Instance details

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

Methods

fresh :: MonadFresh m => () -> m (Union (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 #

(KnownNat n, 1 <= n) => SymFromIntegral SymInteger (SymWordN n) Source #

Instance details

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

Methods

symFromIntegral :: SymInteger -> SymWordN n Source #

ToSym Word16 (SymWordN 16) Source #

Instance details

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

Methods

toSym :: Word16 -> SymWordN 16 Source #

ToSym Word32 (SymWordN 32) Source #

Instance details

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

Methods

toSym :: Word32 -> SymWordN 32 Source #

ToSym Word64 (SymWordN 64) Source #

Instance details

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

Methods

toSym :: Word64 -> SymWordN 64 Source #

ToSym Word8 (SymWordN 8) Source #

Instance details

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

Methods

toSym :: Word8 -> SymWordN 8 Source #

ToSym Word (SymWordN 64) Source #

Instance details

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

Methods

toSym :: Word -> SymWordN 64 Source #

(KnownNat n, 1 <= n) => UnifiedFiniteBits 'S (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits

Methods

withBaseFiniteBits :: (If (IsConMode 'S) (FiniteBits (SymWordN n), FromBits (SymWordN n)) (SymFiniteBits (SymWordN n)) => r) -> r 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) => 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 #

(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeDiv ArithException (SymWordN n) m Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv

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 #

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'S (SymWordN n') SymAlgReal Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymWordN n'), Num SymAlgReal) (SymFromIntegral (SymWordN n') SymAlgReal) => r) -> r Source #

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'S (SymWordN n') SymInteger Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymWordN n'), Num SymInteger) (SymFromIntegral (SymWordN n') SymInteger) => r) -> r Source #

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'S (SymIntN n') (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymIntN n'), Num (SymWordN n)) (SymFromIntegral (SymIntN n') (SymWordN n)) => r) -> r Source #

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'S (SymWordN n') (SymIntN n) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymWordN n'), Num (SymIntN n)) (SymFromIntegral (SymWordN n') (SymIntN n)) => r) -> r Source #

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'S (SymWordN n') (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymWordN n'), Num (SymWordN n)) (SymFromIntegral (SymWordN n') (SymWordN n)) => r) -> r Source #

(KnownNat n, 1 <= n) => UnifiedSolvable 'S (SymWordN n) (WordN n) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSolvable

Methods

withBaseSolvable :: (If (IsConMode 'S) (SymWordN n ~ WordN n) (Solvable (WordN n) (SymWordN n)) => r) -> r Source #

(KnownNat n', 1 <= n', ValidFP eb sb) => UnifiedFromIntegral 'S (SymWordN n') (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymWordN n'), Num (SymFP eb sb)) (SymFromIntegral (SymWordN n') (SymFP eb sb)) => r) -> r Source #

(MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (SymWordN n) (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

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

Methods

safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m (SymWordN n) Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeDiv 'S (Either SomeBVException ArithException) SomeSymWordN m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

Methods

withBaseSafeDiv :: (SafeDiv (Either SomeBVException ArithException) SomeSymWordN m => r) -> r Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeLinearArith 'S (Either SomeBVException ArithException) SomeSymWordN m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

Methods

withBaseSafeLinearArith :: (SafeLinearArith (Either SomeBVException ArithException) SomeSymWordN m => r) -> r Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeSymRotate 'S (Either SomeBVException ArithException) SomeSymWordN m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate

Methods

withBaseSafeSymRotate :: (SafeSymRotate (Either SomeBVException ArithException) SomeSymWordN m => r) -> r Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeSymShift 'S (Either SomeBVException ArithException) SomeSymWordN m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift

Methods

withBaseSafeSymShift :: (SafeSymShift (Either SomeBVException ArithException) SomeSymWordN m => r) -> r Source #

(ValidFP eb sb, r ~ (eb + sb), KnownNat r, 1 <= r, MonadUnion m, MonadError NotRepresentableFPError m) => SafeBitCast NotRepresentableFPError (SymFP eb sb) (SymWordN r) m Source #

Instance details

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

Methods

safeBitCast :: SymFP eb sb -> m (SymWordN r) Source #

(KnownNat n, 1 <= n) => Binary (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

put :: SymWordN n -> Put #

get :: Get (SymWordN n) #

putList :: [SymWordN n] -> Put #

(KnownNat n, 1 <= n) => Serial (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

serialize :: MonadPut m => SymWordN n -> m () #

deserialize :: MonadGet m => m (SymWordN n) #

(KnownNat n, 1 <= n) => Serialize (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

put :: Putter (SymWordN n) #

get :: Get (SymWordN n) #

NFData (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

rnf :: 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 #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

fromString :: String -> SymWordN n #

Generic (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

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

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 #

(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) => Apply (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type FunType (SymWordN n)
Instance details Defined in Grisette.Internal.SymPrim.SymBV type FunType (SymWordN n) = SymWordN n

Methods

apply :: SymWordN n -> FunType (SymWordN n) 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 #

SymFiniteBits (SomeBV SymWordN) Source #

Instance details

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

Methods

symTestBit :: SomeBV SymWordN -> Int -> SymBool Source #

symSetBitTo :: SomeBV SymWordN -> Int -> SymBool -> SomeBV SymWordN Source #

symFromBits :: [SymBool] -> SomeBV SymWordN Source #

(KnownNat n, 1 <= n) => SymFiniteBits (SymWordN n) Source #

Instance details

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

Methods

symTestBit :: SymWordN n -> Int -> SymBool Source #

symSetBitTo :: SymWordN n -> Int -> SymBool -> SymWordN n Source #

symFromBits :: [SymBool] -> 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) => EvalSym (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> SymWordN n -> SymWordN n Source #

(KnownNat n, 1 <= n) => ExtractSym (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ExtractSym

Methods

extractSym :: SymWordN n -> AnySymbolSet Source #

extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => SymWordN n -> Maybe (SymbolSet knd) Source #

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

Instance details

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

Methods

rootStrategy :: MergingStrategy (SymWordN n) Source #

sortIndices :: SymWordN n -> [DynamicSortedIdx] Source #

(KnownNat n, 1 <= n) => PPrint (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.PPrint

Methods

pformat :: SymWordN n -> Doc ann Source #

pformatPrec :: Int -> SymWordN n -> Doc ann Source #

pformatList :: [SymWordN n] -> Doc ann Source #

(KnownNat n, 1 <= n) => DivOr (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv

Methods

divOr :: SymWordN n -> SymWordN n -> SymWordN n -> SymWordN n Source #

modOr :: SymWordN n -> SymWordN n -> SymWordN n -> SymWordN n Source #

divModOr :: (SymWordN n, SymWordN n) -> SymWordN n -> SymWordN n -> (SymWordN n, SymWordN n) Source #

quotOr :: SymWordN n -> SymWordN n -> SymWordN n -> SymWordN n Source #

remOr :: SymWordN n -> SymWordN n -> SymWordN n -> SymWordN n Source #

quotRemOr :: (SymWordN n, SymWordN n) -> SymWordN n -> SymWordN n -> (SymWordN n, SymWordN n) Source #

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

Instance details

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

Methods

mrgIte :: SymBool -> SymWordN n -> SymWordN n -> SymWordN n Source #

(KnownNat n, 1 <= n) => SubstSym (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym

Methods

substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> SymWordN n -> SymWordN n Source #

(KnownNat n, 1 <= n) => SymEq (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq

Methods

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

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

symDistinct :: [SymWordN n] -> SymBool Source #

(KnownNat n, 1 <= n) => SymOrd (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd

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 -> Union Ordering 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)
Instance details Defined in Grisette.Internal.SymPrim.SymBV type ConType (SymWordN n) = WordN n

(KnownNat n, 1 <= n) => UnifiedConRep (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

Associated Types

type ConType (SymWordN n)
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedRep type ConType (SymWordN n) = WordN n

(KnownNat n, 1 <= n) => UnifiedSymRep (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

Associated Types

type SymType (SymWordN n)
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedRep type SymType (SymWordN n) = SymWordN n

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

BitCast (SymWordN 1) SymBool Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

bitCast :: SymWordN 1 -> SymBool Source #

(KnownNat n, 1 <= n) => SymFromIntegral (SymWordN n) SymAlgReal Source #

Instance details

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

Methods

symFromIntegral :: SymWordN n -> SymAlgReal Source #

(KnownNat n, 1 <= n) => SymFromIntegral (SymWordN n) SymInteger Source #

Instance details

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

Methods

symFromIntegral :: SymWordN n -> SymInteger Source #

ToCon (SymWordN 8) Word8 Source #

Instance details

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

Methods

toCon :: SymWordN 8 -> Maybe Word8 Source #

ToCon (SymWordN 16) Word16 Source #

Instance details

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

Methods

toCon :: SymWordN 16 -> Maybe Word16 Source #

ToCon (SymWordN 32) Word32 Source #

Instance details

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

Methods

toCon :: SymWordN 32 -> Maybe Word32 Source #

ToCon (SymWordN 64) Word64 Source #

Instance details

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

Methods

toCon :: SymWordN 64 -> Maybe Word64 Source #

ToCon (SymWordN 64) Word Source #

Instance details

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

Methods

toCon :: SymWordN 64 -> Maybe Word Source #

(KnownNat n, 1 <= n) => BitCast (SymIntN n) (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

bitCast :: SymIntN n -> SymWordN n Source #

(KnownNat n, 1 <= n) => BitCast (SymWordN n) (SymIntN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

bitCast :: SymWordN n -> SymIntN n 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 (Union (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, KnownNat m, 1 <= n, 1 <= m) => SymFromIntegral (SymIntN n) (SymWordN m) Source #

Instance details

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

Methods

symFromIntegral :: SymIntN n -> SymWordN m Source #

(KnownNat n, KnownNat m, 1 <= n, 1 <= m) => SymFromIntegral (SymWordN n) (SymIntN m) Source #

Instance details

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

Methods

symFromIntegral :: SymWordN n -> SymIntN m Source #

(KnownNat n, KnownNat m, 1 <= n, 1 <= m) => SymFromIntegral (SymWordN n) (SymWordN m) Source #

Instance details

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

Methods

symFromIntegral :: SymWordN n -> SymWordN m Source #

(KnownNat n, 1 <= n) => ToCon (SymWordN n) (WordN n) Source #

Instance details

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

Methods

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

ToCon (SymWordN n) (SymWordN n) Source #

Instance details

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

Methods

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

(KnownNat n, 1 <= n) => ToSym (Union (WordN n)) (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union

Methods

toSym :: Union (WordN n) -> SymWordN n Source #

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

Instance details

Defined in Grisette.Internal.Internal.Impl.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.Internal.Impl.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 #

(ValidFP eb sb, r ~ (eb + sb)) => BitCast (SymWordN r) (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

bitCast :: SymWordN r -> SymFP eb sb Source #

(KnownNat n, 1 <= n, ValidFP eb sb) => SymFromIntegral (SymWordN n) (SymFP eb sb) Source #

Instance details

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

Methods

symFromIntegral :: SymWordN n -> SymFP eb sb Source #

(ValidFP eb sb, KnownNat n, 1 <= n) => IEEEFPConvertible (SymWordN n) (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fromFPOr :: SymWordN n -> SymFPRoundingMode -> SymFP eb sb -> SymWordN n Source #

toFP :: SymFPRoundingMode -> SymWordN n -> SymFP eb sb Source #

(ValidFP eb sb, r ~ (eb + sb)) => BitCastCanonical (SymFP eb sb) (SymWordN r) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

bitCastCanonicalValue :: proxy (SymFP eb sb) -> SymWordN r Source #

(ValidFP eb sb, r ~ (eb + sb)) => BitCastOr (SymFP eb sb) (SymWordN r) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

bitCastOr :: SymWordN r -> SymFP eb sb -> SymWordN r 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.11.0.0-HndeEPlDvvDHSETLw6O8c" '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

type ConType (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type ConType (SymWordN n) = WordN n

type SymType (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type SymType (SymWordN n) = SymWordN n

type SymWordN8 = SymWordN 8 Source #

Symbolic 8-bit unsigned bit-vector.

type SymWordN16 = SymWordN 16 Source #

Symbolic 16-bit unsigned bit-vector.

type SymWordN32 = SymWordN 32 Source #

Symbolic 32-bit unsigned bit-vector.

type SymWordN64 = SymWordN 64 Source #

Symbolic 64-bit unsigned bit-vector.

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.

>>> "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 operations are available. Please refer to Grisette.Core for more information.

Constructors

SymIntN (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 #

UnifiedFiniteBits 'S SomeSymIntN Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits

Methods

withBaseFiniteBits :: (If (IsConMode 'S) (FiniteBits SomeSymIntN, FromBits SomeSymIntN) (SymFiniteBits SomeSymIntN) => r) -> r Source #

(KnownNat n, 1 <= n) => UnifiedBVImpl 'S SymWordN SymIntN n (SymWordN n) (SymIntN n) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedBV

Associated Types

type GetWordN 'S
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedBV type GetWordN 'S = SymWordN
type GetIntN 'S
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedBV type GetIntN 'S = SymIntN

(KnownNat n, 1 <= n) => UnifiedFromIntegral 'S SymInteger (SymIntN n) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'S) (Integral SymInteger, Num (SymIntN n)) (SymFromIntegral SymInteger (SymIntN n)) => r) -> r Source #

(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeDiv 'S ArithException (SymIntN n) m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

Methods

withBaseSafeDiv :: (SafeDiv ArithException (SymIntN n) m => r) -> r Source #

(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeLinearArith 'S ArithException (SymIntN n) m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

Methods

withBaseSafeLinearArith :: (SafeLinearArith ArithException (SymIntN n) m => r) -> r Source #

(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeSymRotate 'S ArithException (SymIntN n) m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate

Methods

withBaseSafeSymRotate :: (SafeSymRotate ArithException (SymIntN n) m => r) -> r Source #

(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeSymShift 'S ArithException (SymIntN n) m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift

Methods

withBaseSafeSymShift :: (SafeSymShift ArithException (SymIntN n) m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP 'S NotRepresentableFPError (SymIntN n) (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (SymIntN n) (SymFP eb sb) SymFPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) => UnifiedSafeBitCast 'S NotRepresentableFPError (SymFP eb sb) (SymIntN n) m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeBitCast

Methods

withBaseSafeBitCast :: (SafeBitCast NotRepresentableFPError (SymFP eb sb) (SymIntN n) m => r) -> r Source #

BitCast SymBool (SymIntN 1) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

bitCast :: SymBool -> SymIntN 1 Source #

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

Instance details

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

Methods

fresh :: MonadFresh m => () -> m (Union (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 #

(KnownNat n, 1 <= n) => SymFromIntegral SymInteger (SymIntN n) Source #

Instance details

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

Methods

symFromIntegral :: SymInteger -> SymIntN n Source #

ToSym Int16 (SymIntN 16) Source #

Instance details

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

Methods

toSym :: Int16 -> SymIntN 16 Source #

ToSym Int32 (SymIntN 32) Source #

Instance details

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

Methods

toSym :: Int32 -> SymIntN 32 Source #

ToSym Int64 (SymIntN 64) Source #

Instance details

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

Methods

toSym :: Int64 -> SymIntN 64 Source #

ToSym Int8 (SymIntN 8) Source #

Instance details

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

Methods

toSym :: Int8 -> SymIntN 8 Source #

ToSym Int (SymIntN 64) Source #

Instance details

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

Methods

toSym :: Int -> SymIntN 64 Source #

(KnownNat n, 1 <= n) => UnifiedFiniteBits 'S (SymIntN n) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits

Methods

withBaseFiniteBits :: (If (IsConMode 'S) (FiniteBits (SymIntN n), FromBits (SymIntN n)) (SymFiniteBits (SymIntN n)) => r) -> r 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) => 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 #

(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeDiv ArithException (SymIntN n) m Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv

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 #

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'S (SymIntN n') SymAlgReal Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymIntN n'), Num SymAlgReal) (SymFromIntegral (SymIntN n') SymAlgReal) => r) -> r Source #

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'S (SymIntN n') SymInteger Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymIntN n'), Num SymInteger) (SymFromIntegral (SymIntN n') SymInteger) => r) -> r Source #

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'S (SymIntN n') (SymIntN n) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymIntN n'), Num (SymIntN n)) (SymFromIntegral (SymIntN n') (SymIntN n)) => r) -> r Source #

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'S (SymIntN n') (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymIntN n'), Num (SymWordN n)) (SymFromIntegral (SymIntN n') (SymWordN n)) => r) -> r Source #

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'S (SymWordN n') (SymIntN n) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymWordN n'), Num (SymIntN n)) (SymFromIntegral (SymWordN n') (SymIntN n)) => r) -> r Source #

(KnownNat n, 1 <= n) => UnifiedSolvable 'S (SymIntN n) (IntN n) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSolvable

Methods

withBaseSolvable :: (If (IsConMode 'S) (SymIntN n ~ IntN n) (Solvable (IntN n) (SymIntN n)) => r) -> r Source #

(KnownNat n', 1 <= n', ValidFP eb sb) => UnifiedFromIntegral 'S (SymIntN n') (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymIntN n'), Num (SymFP eb sb)) (SymFromIntegral (SymIntN n') (SymFP eb sb)) => r) -> r Source #

(MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (SymIntN n) (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

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

Methods

safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m (SymIntN n) Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeDiv 'S (Either SomeBVException ArithException) SomeSymIntN m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

Methods

withBaseSafeDiv :: (SafeDiv (Either SomeBVException ArithException) SomeSymIntN m => r) -> r Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeLinearArith 'S (Either SomeBVException ArithException) SomeSymIntN m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

Methods

withBaseSafeLinearArith :: (SafeLinearArith (Either SomeBVException ArithException) SomeSymIntN m => r) -> r Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeSymRotate 'S (Either SomeBVException ArithException) SomeSymIntN m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate

Methods

withBaseSafeSymRotate :: (SafeSymRotate (Either SomeBVException ArithException) SomeSymIntN m => r) -> r Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeSymShift 'S (Either SomeBVException ArithException) SomeSymIntN m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift

Methods

withBaseSafeSymShift :: (SafeSymShift (Either SomeBVException ArithException) SomeSymIntN m => r) -> r Source #

(ValidFP eb sb, r ~ (eb + sb), KnownNat r, 1 <= r, MonadUnion m, MonadError NotRepresentableFPError m) => SafeBitCast NotRepresentableFPError (SymFP eb sb) (SymIntN r) m Source #

Instance details

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

Methods

safeBitCast :: SymFP eb sb -> m (SymIntN r) Source #

(KnownNat n, 1 <= n) => Binary (SymIntN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

put :: SymIntN n -> Put #

get :: Get (SymIntN n) #

putList :: [SymIntN n] -> Put #

(KnownNat n, 1 <= n) => Serial (SymIntN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

serialize :: MonadPut m => SymIntN n -> m () #

deserialize :: MonadGet m => m (SymIntN n) #

(KnownNat n, 1 <= n) => Serialize (SymIntN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

put :: Putter (SymIntN n) #

get :: Get (SymIntN n) #

NFData (SymIntN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

rnf :: 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 #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

fromString :: String -> SymIntN n #

Generic (SymIntN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

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