grisette-0.11.0.0: 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 HaskellNone
LanguageHaskell2010

Grisette.Internal.SymPrim.BV

Description

 
Synopsis

Documentation

newtype IntN (n :: Nat) Source #

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

>>> 3 + 5 :: IntN 5
0b01000
>>> sizedBVConcat (0b101 :: IntN 3) (0b110 :: IntN 3)
0b101110
>>> sizedBVExt (Proxy @6) (0b101 :: IntN 3)
0b111101
>>> (8 :: IntN 4) < (7 :: IntN 4)
True

More operations are available. Please refer to Grisette.Core for more information.

Constructors

IntN 

Fields

Instances

Instances details
SizedBV IntN Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

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

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

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

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

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

FromBits SomeIntN Source # 
Instance details

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

Methods

fromBits :: [Bool] -> SomeIntN Source #

ConvertibleBound IntN Source # 
Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

convertibleLowerBound :: forall (eb :: Nat) (sb :: Nat) (n :: Nat). (ValidFP eb sb, KnownNat n, 1 <= n) => IntN n -> FPRoundingMode -> FP eb sb Source #

convertibleUpperBound :: forall (eb :: Nat) (sb :: Nat) (n :: Nat). (ValidFP eb sb, KnownNat n, 1 <= n) => IntN n -> FPRoundingMode -> FP eb sb Source #

PEvalBVTerm IntN Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval

Methods

pevalBVConcatTerm :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => Term (IntN l) -> Term (IntN r) -> Term (IntN (l + r)) Source #

pevalBVExtendTerm :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => Bool -> proxy r -> Term (IntN l) -> Term (IntN r) Source #

pevalBVSelectTerm :: 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 -> Term (IntN n) -> Term (IntN w) Source #

sbvBVConcatTerm :: forall (l :: Nat) (r :: Nat) p1 p2. (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => p1 l -> p2 r -> SBVType (IntN l) -> SBVType (IntN r) -> SBVType (IntN (l + r)) Source #

sbvBVExtendTerm :: forall (l :: Nat) (r :: Nat) p1 p2. (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => p1 l -> p2 r -> Bool -> SBVType (IntN l) -> SBVType (IntN r) Source #

sbvBVSelectTerm :: forall (ix :: Nat) (w :: Nat) (n :: Nat) p1 p2 p3. (KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w, (ix + w) <= n) => p1 ix -> p2 w -> p3 n -> SBVType (IntN n) -> SBVType (IntN w) Source #

BitCast IntN32 Float Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN32 -> Float Source #

BitCast IntN64 Double Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN64 -> Double Source #

BitCast Double IntN64 Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Double -> IntN64 Source #

BitCast Float IntN32 Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Float -> IntN32 Source #

UnifiedFiniteBits 'C SomeIntN Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits

Methods

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

(KnownNat n, 1 <= n) => UnifiedBVImpl 'C WordN IntN n (WordN n) (IntN n) Source # 
Instance details

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

Associated Types

type GetWordN 'C 
Instance details

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

type GetWordN 'C = WordN
type GetIntN 'C 
Instance details

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

type GetIntN 'C = IntN
(KnownNat n, 1 <= n) => UnifiedFromIntegral 'C Integer (IntN n) Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'C) (Integral Integer, Num (IntN n)) (SymFromIntegral Integer (IntN n)) => r) -> r Source #

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeDiv mode ArithException (IntN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

Methods

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

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeLinearArith mode ArithException (IntN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

Methods

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

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeSymRotate mode ArithException (IntN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate

Methods

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

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeSymShift mode ArithException (IntN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift

Methods

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

(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP mode NotRepresentableFPError (IntN n) (FP eb sb) FPRoundingMode m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (IntN n) (FP eb sb) FPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) => UnifiedSafeBitCast mode NotRepresentableFPError (FP eb sb) (IntN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeBitCast

Methods

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

BitCast Int16 (IntN 16) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Int16 -> IntN 16 Source #

BitCast Int32 (IntN 32) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Int32 -> IntN 32 Source #

BitCast Int64 (IntN 64) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Int64 -> IntN 64 Source #

BitCast Int8 (IntN 8) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Int8 -> IntN 8 Source #

BitCast Word16 (IntN 16) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Word16 -> IntN 16 Source #

BitCast Word32 (IntN 32) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Word32 -> IntN 32 Source #

BitCast Word64 (IntN 64) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Word64 -> IntN 64 Source #

BitCast Word8 (IntN 8) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Word8 -> IntN 8 Source #

BitCast Bool (IntN 1) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Bool -> IntN 1 Source #

(DecideEvalMode mode, KnownNat a, 1 <= a) => UnifiedSymEq mode (IntN a) Source # 
Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymEq

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (IntN a)) (SymEq (IntN a)) => r) -> r Source #

(DecideEvalMode mode, KnownNat a, 1 <= a) => UnifiedSymOrd mode (IntN a) Source # 
Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymOrd

Methods

withBaseSymOrd :: (If (IsConMode mode) (Ord (IntN a)) (SymOrd (IntN a)) => r) -> r Source #

PEvalBitCastTerm Bool (IntN 1) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm

Methods

pevalBitCastTerm :: Term Bool -> Term (IntN 1) Source #

sbvBitCast :: SBVType Bool -> SBVType (IntN 1) Source #

(KnownNat n, 1 <= n) => PEvalFromIntegralTerm Integer (IntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm

Methods

pevalFromIntegralTerm :: Term Integer -> Term (IntN n) Source #

sbvFromIntegralTerm :: SBVType Integer -> SBVType (IntN n) Source #

(KnownNat n, 1 <= n) => UnifiedFiniteBits 'C (IntN n) Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits

Methods

withBaseFiniteBits :: (If (IsConMode 'C) (FiniteBits (IntN n), FromBits (IntN n)) (SymFiniteBits (IntN n)) => r) -> r Source #

Lift (IntN n :: Type) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

lift :: Quote m => IntN n -> m Exp #

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

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (IntN n) m Source # 
Instance details

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

Methods

safeAdd :: IntN n -> IntN n -> m (IntN n) Source #

safeNeg :: IntN n -> m (IntN n) Source #

safeSub :: IntN n -> IntN n -> m (IntN n) Source #

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymRotate ArithException (IntN n) m Source # 
Instance details

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

Methods

safeSymRotateL :: IntN n -> IntN n -> m (IntN n) Source #

safeSymRotateR :: IntN n -> IntN n -> m (IntN n) Source #

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymShift ArithException (IntN n) m Source # 
Instance details

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

Methods

safeSymShiftL :: IntN n -> IntN n -> m (IntN n) Source #

safeSymShiftR :: IntN n -> IntN n -> m (IntN n) Source #

safeSymStrictShiftL :: IntN n -> IntN n -> m (IntN n) Source #

safeSymStrictShiftR :: IntN n -> IntN n -> m (IntN n) Source #

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeDiv ArithException (IntN n) m Source # 
Instance details

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

Methods

safeDiv :: IntN n -> IntN n -> m (IntN n) Source #

safeMod :: IntN n -> IntN n -> m (IntN n) Source #

safeDivMod :: IntN n -> IntN n -> m (IntN n, IntN n) Source #

safeQuot :: IntN n -> IntN n -> m (IntN n) Source #

safeRem :: IntN n -> IntN n -> m (IntN n) Source #

safeQuotRem :: IntN n -> IntN n -> m (IntN n, IntN n) Source #

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'C (IntN n') AlgReal Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'C) (Integral (IntN n'), Num AlgReal) (SymFromIntegral (IntN n') AlgReal) => r) -> r Source #

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'C (IntN n') Integer Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'C) (Integral (IntN n'), Num Integer) (SymFromIntegral (IntN n') Integer) => r) -> r Source #

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'C (IntN n') (IntN n) Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'C (IntN n') (WordN n) Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'C) (Integral (IntN n'), Num (WordN n)) (SymFromIntegral (IntN n') (WordN n)) => r) -> r Source #

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'C (WordN n') (IntN n) Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'C) (Integral (WordN n'), Num (IntN n)) (SymFromIntegral (WordN n') (IntN n)) => r) -> r Source #

(KnownNat n, 1 <= n) => UnifiedSolvable 'C (IntN n) (IntN n) Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSolvable

Methods

withBaseSolvable :: (If (IsConMode 'C) (IntN n ~ IntN n) (Solvable (IntN n) (IntN 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 'C (IntN n') (FP eb sb) Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'C) (Integral (IntN n'), Num (FP eb sb)) (SymFromIntegral (IntN n') (FP eb sb)) => r) -> r Source #

(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (IntN n) (FP eb sb) FPRoundingMode m Source # 
Instance details

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

Methods

safeFromFP :: FPRoundingMode -> FP eb sb -> m (IntN n) Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeDiv mode (Either SomeBVException ArithException) SomeIntN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

Methods

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

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeLinearArith mode (Either SomeBVException ArithException) SomeIntN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

Methods

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

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymRotate mode (Either SomeBVException ArithException) SomeIntN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate

Methods

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

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymShift mode (Either SomeBVException ArithException) SomeIntN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift

Methods

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

(ValidFP eb sb, r ~ (eb + sb), KnownNat r, 1 <= r, TryMerge m, MonadError NotRepresentableFPError m) => SafeBitCast NotRepresentableFPError (FP eb sb) (IntN r) m Source # 
Instance details

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

Methods

safeBitCast :: FP eb sb -> m (IntN r) Source #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

arbitrary :: Gen (IntN n) #

shrink :: IntN n -> [IntN n] #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

put :: IntN n -> Put #

get :: Get (IntN n) #

putList :: [IntN n] -> Put #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

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

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

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

Defined in Grisette.Internal.SymPrim.BV

Methods

put :: Putter (IntN n) #

get :: Get (IntN n) #

NFData (IntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

rnf :: IntN n -> () #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

(.&.) :: IntN n -> IntN n -> IntN n #

(.|.) :: IntN n -> IntN n -> IntN n #

xor :: IntN n -> IntN n -> IntN n #

complement :: IntN n -> IntN n #

shift :: IntN n -> Int -> IntN n #

rotate :: IntN n -> Int -> IntN n #

zeroBits :: IntN n #

bit :: Int -> IntN n #

setBit :: IntN n -> Int -> IntN n #

clearBit :: IntN n -> Int -> IntN n #

complementBit :: IntN n -> Int -> IntN n #

testBit :: IntN n -> Int -> Bool #

bitSizeMaybe :: IntN n -> Maybe Int #

bitSize :: IntN n -> Int #

isSigned :: IntN n -> Bool #

shiftL :: IntN n -> Int -> IntN n #

unsafeShiftL :: IntN n -> Int -> IntN n #

shiftR :: IntN n -> Int -> IntN n #

unsafeShiftR :: IntN n -> Int -> IntN n #

rotateL :: IntN n -> Int -> IntN n #

rotateR :: IntN n -> Int -> IntN n #

popCount :: IntN n -> Int #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

finiteBitSize :: IntN n -> Int #

countLeadingZeros :: IntN n -> Int #

countTrailingZeros :: IntN n -> Int #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

minBound :: IntN n #

maxBound :: IntN n #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

succ :: IntN n -> IntN n #

pred :: IntN n -> IntN n #

toEnum :: Int -> IntN n #

fromEnum :: IntN n -> Int #

enumFrom :: IntN n -> [IntN n] #

enumFromThen :: IntN n -> IntN n -> [IntN n] #

enumFromTo :: IntN n -> IntN n -> [IntN n] #

enumFromThenTo :: IntN n -> IntN n -> IntN n -> [IntN n] #

Generic (IntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Associated Types

type Rep (IntN n) 
Instance details

Defined in Grisette.Internal.SymPrim.BV

type Rep (IntN n) = D1 ('MetaData "IntN" "Grisette.Internal.SymPrim.BV" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'True) (C1 ('MetaCons "IntN" 'PrefixI 'True) (S1 ('MetaSel ('Just "unIntN") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))

Methods

from :: IntN n -> Rep (IntN n) x #

to :: Rep (IntN n) x -> IntN n #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

(+) :: IntN n -> IntN n -> IntN n #

(-) :: IntN n -> IntN n -> IntN n #

(*) :: IntN n -> IntN n -> IntN n #

negate :: IntN n -> IntN n #

abs :: IntN n -> IntN n #

signum :: IntN n -> IntN n #

fromInteger :: Integer -> IntN n #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

readsPrec :: Int -> ReadS (IntN n) #

readList :: ReadS [IntN n] #

readPrec :: ReadPrec (IntN n) #

readListPrec :: ReadPrec [IntN n] #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

quot :: IntN n -> IntN n -> IntN n #

rem :: IntN n -> IntN n -> IntN n #

div :: IntN n -> IntN n -> IntN n #

mod :: IntN n -> IntN n -> IntN n #

quotRem :: IntN n -> IntN n -> (IntN n, IntN n) #

divMod :: IntN n -> IntN n -> (IntN n, IntN n) #

toInteger :: IntN n -> Integer #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

toRational :: IntN n -> Rational #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

showsPrec :: Int -> IntN n -> ShowS #

show :: IntN n -> String #

showList :: [IntN n] -> ShowS #

Eq (IntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

(==) :: IntN n -> IntN n -> Bool #

(/=) :: IntN n -> IntN n -> Bool #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

compare :: IntN n -> IntN n -> Ordering #

(<) :: IntN n -> IntN n -> Bool #

(<=) :: IntN n -> IntN n -> Bool #

(>) :: IntN n -> IntN n -> Bool #

(>=) :: IntN n -> IntN n -> Bool #

max :: IntN n -> IntN n -> IntN n #

min :: IntN n -> IntN n -> IntN n #

Apply (IntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Associated Types

type FunType (IntN n) 
Instance details

Defined in Grisette.Internal.SymPrim.BV

type FunType (IntN n) = IntN n

Methods

apply :: IntN n -> FunType (IntN n) Source #

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

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

Methods

fromBits :: [Bool] -> IntN n Source #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

symRotate :: IntN n -> IntN n -> IntN n Source #

symRotateNegated :: IntN n -> IntN n -> IntN n Source #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

symShift :: IntN n -> IntN n -> IntN n Source #

symShiftNegated :: IntN n -> IntN n -> IntN n Source #

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

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

Methods

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

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

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

Methods

extractSym :: IntN n -> AnySymbolSet Source #

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

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

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

Methods

rootStrategy :: MergingStrategy (IntN n) Source #

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

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

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

Methods

pformat :: IntN n -> Doc ann Source #

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

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

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

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

Methods

divOr :: IntN n -> IntN n -> IntN n -> IntN n Source #

modOr :: IntN n -> IntN n -> IntN n -> IntN n Source #

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

quotOr :: IntN n -> IntN n -> IntN n -> IntN n Source #

remOr :: IntN n -> IntN n -> IntN n -> IntN n Source #

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

(KnownNat n, 1 <= n) => SubstSym (IntN 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 -> IntN n -> IntN n Source #

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

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

Methods

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

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

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

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

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

Methods

(.<) :: IntN n -> IntN n -> SymBool Source #

(.<=) :: IntN n -> IntN n -> SymBool Source #

(.>) :: IntN n -> IntN n -> SymBool Source #

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

symCompare :: IntN n -> IntN n -> Union Ordering Source #

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

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: IntN n -> [SomeSym] -> [SomeSym] Source #

allSyms :: IntN n -> [SomeSym] Source #

(KnownNat w, 1 <= w) => NonFuncSBVRep (IntN w) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type NonFuncSBVBaseType (IntN w) 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type NonFuncSBVBaseType (IntN w) = IntN w
(KnownNat n, 1 <= n) => PEvalBitwiseTerm (IntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitwiseTerm

Methods

pevalAndBitsTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source #

pevalOrBitsTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source #

pevalXorBitsTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source #

pevalComplementBitsTerm :: Term (IntN n) -> Term (IntN n) Source #

withSbvBitwiseTermConstraint :: (Bits (SBVType (IntN n)) => r) -> r Source #

sbvAndBitsTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source #

sbvOrBitsTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source #

sbvXorBitsTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source #

sbvComplementBitsTerm :: SBVType (IntN n) -> SBVType (IntN n) Source #

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalDivModIntegralTerm

Methods

pevalDivIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source #

pevalModIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source #

pevalQuotIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source #

pevalRemIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source #

withSbvDivModIntegralTermConstraint :: (SDivisible (SBVType (IntN n)) => r) -> r Source #

sbvDivIntegralTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source #

sbvModIntegralTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source #

sbvQuotIntegralTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source #

sbvRemIntegralTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source #

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalIEEEFPConvertibleTerm

Methods

pevalFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term (IntN n) -> Term FPRoundingMode -> Term (FP eb sb) -> Term (IntN n) Source #

pevalToFPTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term FPRoundingMode -> Term (IntN n) -> Term (FP eb sb) Source #

sbvFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType (IntN n) -> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType (IntN n) Source #

sbvToFPTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType FPRoundingMode -> SBVType (IntN n) -> SBVType (FP eb sb) Source #

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm

Methods

pevalAddNumTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source #

pevalNegNumTerm :: Term (IntN n) -> Term (IntN n) Source #

pevalMulNumTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source #

pevalAbsNumTerm :: Term (IntN n) -> Term (IntN n) Source #

pevalSignumNumTerm :: Term (IntN n) -> Term (IntN n) Source #

withSbvNumTermConstraint :: (Num (SBVType (IntN n)) => r) -> r Source #

sbvAddNumTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source #

sbvNegNumTerm :: SBVType (IntN n) -> SBVType (IntN n) Source #

sbvMulNumTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source #

sbvAbsNumTerm :: SBVType (IntN n) -> SBVType (IntN n) Source #

sbvSignumNumTerm :: SBVType (IntN n) -> SBVType (IntN n) Source #

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm

Methods

pevalLtOrdTerm :: Term (IntN n) -> Term (IntN n) -> Term Bool Source #

pevalLeOrdTerm :: Term (IntN n) -> Term (IntN n) -> Term Bool Source #

withSbvOrdTermConstraint :: (OrdSymbolic (SBVType (IntN n)) => r) -> r Source #

sbvLtOrdTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBV Bool Source #

sbvLeOrdTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBV Bool Source #

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalRotateTerm

Methods

pevalRotateLeftTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source #

pevalRotateRightTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source #

withSbvRotateTermConstraint :: (SIntegral (NonFuncSBVBaseType (IntN n)) => r) -> r Source #

sbvRotateLeftTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source #

sbvRotateRightTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source #

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalShiftTerm

Methods

pevalShiftLeftTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source #

pevalShiftRightTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source #

withSbvShiftTermConstraint :: (SIntegral (NonFuncSBVBaseType (IntN n)) => r) -> r Source #

sbvShiftLeftTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source #

sbvShiftRightTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source #

(KnownNat w, 1 <= w) => SBVRep (IntN w) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type SBVType (IntN w) 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type SBVType (IntN w) = SBV (IntN w)
(KnownNat w, 1 <= w) => SupportedNonFuncPrim (IntN w) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Methods

conNonFuncSBVTerm :: IntN w -> SBV (NonFuncSBVBaseType (IntN w)) Source #

symNonFuncSBVTerm :: SBVFreshMonad m => String -> m (SBV (NonFuncSBVBaseType (IntN w))) Source #

withNonFuncPrim :: (NonFuncPrimConstraint (IntN w) => r) -> r Source #

(KnownNat w, 1 <= w) => SupportedPrim (IntN w) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Methods

primTypeRep :: TypeRep (IntN w) Source #

sameCon :: IntN w -> IntN w -> Bool Source #

hashConWithSalt :: Int -> IntN w -> Int Source #

pformatCon :: IntN w -> String Source #

defaultValue :: IntN w Source #

pevalITETerm :: Term Bool -> Term (IntN w) -> Term (IntN w) -> Term (IntN w) Source #

pevalEqTerm :: Term (IntN w) -> Term (IntN w) -> Term Bool Source #

pevalDistinctTerm :: NonEmpty (Term (IntN w)) -> Term Bool Source #

conSBVTerm :: IntN w -> SBVType (IntN w) Source #

symSBVName :: TypedSymbol 'AnyKind (IntN w) -> Int -> String Source #

symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (IntN w)) Source #

withPrim :: ((PrimConstraint (IntN w), SMTDefinable (SBVType (IntN w)), Mergeable (SBVType (IntN w)), Typeable (SBVType (IntN w))) => a) -> a Source #

sbvIte :: SBV Bool -> SBVType (IntN w) -> SBVType (IntN w) -> SBVType (IntN w) Source #

sbvEq :: SBVType (IntN w) -> SBVType (IntN w) -> SBV Bool Source #

sbvDistinct :: NonEmpty (SBVType (IntN w)) -> SBV Bool Source #

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> IntN w Source #

castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (IntN w) -> Maybe (TypedSymbol knd' (IntN w)) Source #

funcDummyConstraint :: SBVType (IntN w) -> SBV Bool Source #

(KnownNat w, 1 <= w) => SupportedPrimConstraint (IntN w) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type PrimConstraint (IntN w) 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type PrimConstraint (IntN w) = (KnownNat w, 1 <= w, BVIsNonZero w)
(KnownNat n, 1 <= n) => SymRep (IntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type SymType (IntN n) 
Instance details

Defined in Grisette.Internal.SymPrim.SymBV

type SymType (IntN n) = SymIntN n
(KnownNat n, 1 <= n) => UnifiedConRep (IntN n) Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

Associated Types

type ConType (IntN n) 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type ConType (IntN n) = IntN n
(KnownNat n, 1 <= n) => UnifiedSymRep (IntN n) Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

Associated Types

type SymType (IntN n) 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type SymType (IntN n) = SymIntN n
Hashable (IntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

hashWithSalt :: Int -> IntN n -> Int #

hash :: IntN n -> Int #

BitCast (IntN 1) Bool Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 1 -> Bool Source #

BitCast (IntN 8) Int8 Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 8 -> Int8 Source #

BitCast (IntN 8) Word8 Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 8 -> Word8 Source #

BitCast (IntN 16) Int16 Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 16 -> Int16 Source #

BitCast (IntN 16) Word16 Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 16 -> Word16 Source #

BitCast (IntN 32) Int32 Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 32 -> Int32 Source #

BitCast (IntN 32) Word32 Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 32 -> Word32 Source #

BitCast (IntN 64) Int64 Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 64 -> Int64 Source #

BitCast (IntN 64) Word64 Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 64 -> Word64 Source #

PEvalBitCastTerm (IntN 1) Bool Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm

Methods

pevalBitCastTerm :: Term (IntN 1) -> Term Bool Source #

sbvBitCast :: SBVType (IntN 1) -> SBVType Bool Source #

(KnownNat n, 1 <= n) => PEvalFromIntegralTerm (IntN n) AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm

Methods

pevalFromIntegralTerm :: Term (IntN n) -> Term AlgReal Source #

sbvFromIntegralTerm :: SBVType (IntN n) -> SBVType AlgReal Source #

(KnownNat n, 1 <= n) => PEvalFromIntegralTerm (IntN n) Integer Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm

Methods

pevalFromIntegralTerm :: Term (IntN n) -> Term Integer Source #

sbvFromIntegralTerm :: SBVType (IntN n) -> SBVType Integer Source #

(KnownNat n, 1 <= n) => BitCast (IntN n) (WordN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN n -> WordN n Source #

(KnownNat n, 1 <= n) => BitCast (WordN n) (IntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN n -> IntN n Source #

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

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

Methods

fresh :: MonadFresh m => IntN n -> m (Union (IntN n)) Source #

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

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

Methods

simpleFresh :: MonadFresh m => IntN n -> m (IntN n) Source #

(KnownNat n, 1 <= n) => SignConversion (WordN n) (IntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

toSigned :: WordN n -> IntN n Source #

toUnsigned :: IntN n -> WordN 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 (IntN n) (IntN n) Source # 
Instance details

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

Methods

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

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

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

Methods

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

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

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

Methods

toSym :: Union (IntN n) -> SymIntN n Source #

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

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

Methods

toSym :: IntN n -> IntN n Source #

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

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

Methods

toSym :: IntN 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 #

(KnownNat n, 1 <= n) => PEvalBitCastTerm (IntN n) (WordN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval

Methods

pevalBitCastTerm :: Term (IntN n) -> Term (WordN n) Source #

sbvBitCast :: SBVType (IntN n) -> SBVType (WordN n) Source #

(KnownNat n, 1 <= n) => PEvalBitCastTerm (WordN n) (IntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval

Methods

pevalBitCastTerm :: Term (WordN n) -> Term (IntN n) Source #

sbvBitCast :: SBVType (WordN n) -> SBVType (IntN n) Source #

(KnownNat n, 1 <= n, KnownNat m, 1 <= m) => PEvalFromIntegralTerm (IntN n) (IntN m) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm

Methods

pevalFromIntegralTerm :: Term (IntN n) -> Term (IntN m) Source #

sbvFromIntegralTerm :: SBVType (IntN n) -> SBVType (IntN m) Source #

(KnownNat n, 1 <= n, KnownNat m, 1 <= m) => PEvalFromIntegralTerm (IntN n) (WordN m) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm

Methods

pevalFromIntegralTerm :: Term (IntN n) -> Term (WordN m) Source #

sbvFromIntegralTerm :: SBVType (IntN n) -> SBVType (WordN m) Source #

(KnownNat n, 1 <= n, KnownNat m, 1 <= m) => PEvalFromIntegralTerm (WordN n) (IntN m) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm

Methods

pevalFromIntegralTerm :: Term (WordN n) -> Term (IntN m) Source #

sbvFromIntegralTerm :: SBVType (WordN n) -> SBVType (IntN m) Source #

(ValidFP eb sb, r ~ (eb + sb)) => BitCast (IntN r) (FP eb sb) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: IntN r -> FP eb sb Source #

(n ~ (eb + sb), ValidFP eb sb, KnownNat n, 1 <= n) => PEvalBitCastTerm (IntN n) (FP eb sb) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm

Methods

pevalBitCastTerm :: Term (IntN n) -> Term (FP eb sb) Source #

sbvBitCast :: SBVType (IntN n) -> SBVType (FP eb sb) Source #

(KnownNat n, 1 <= n, ValidFP eb sb) => PEvalFromIntegralTerm (IntN n) (FP eb sb) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm

Methods

pevalFromIntegralTerm :: Term (IntN n) -> Term (FP eb sb) Source #

sbvFromIntegralTerm :: SBVType (IntN n) -> SBVType (FP eb sb) Source #

(ValidFP eb sb, KnownNat n, 1 <= n) => IEEEFPConvertible (IntN n) (FP eb sb) FPRoundingMode Source # 
Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

fromFPOr :: IntN n -> FPRoundingMode -> FP eb sb -> IntN n Source #

toFP :: FPRoundingMode -> IntN n -> FP eb sb Source #

(ValidFP eb sb, n ~ (eb + sb)) => BitCastCanonical (FP eb sb) (IntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCastCanonicalValue :: proxy (FP eb sb) -> IntN n Source #

(ValidFP eb sb, n ~ (eb + sb)) => BitCastOr (FP eb sb) (IntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCastOr :: IntN n -> FP eb sb -> IntN n Source #

(n ~ (eb + sb), ValidFP eb sb, KnownNat n, 1 <= n) => PEvalBitCastOrTerm (FP eb sb) (IntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm

Methods

pevalBitCastOrTerm :: Term (IntN n) -> Term (FP eb sb) -> Term (IntN n) Source #

sbvBitCastOr :: SBVType (IntN n) -> SBVType (FP eb sb) -> SBVType (IntN n) Source #

type Rep (IntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

type Rep (IntN n) = D1 ('MetaData "IntN" "Grisette.Internal.SymPrim.BV" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'True) (C1 ('MetaCons "IntN" 'PrefixI 'True) (S1 ('MetaSel ('Just "unIntN") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))
type FunType (IntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

type FunType (IntN n) = IntN n
type NonFuncSBVBaseType (IntN w) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type NonFuncSBVBaseType (IntN w) = IntN w
type PrimConstraint (IntN w) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type PrimConstraint (IntN w) = (KnownNat w, 1 <= w, BVIsNonZero w)
type SBVType (IntN w) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type SBVType (IntN w) = SBV (IntN w)
type SymType (IntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymBV

type SymType (IntN n) = SymIntN n
type ConType (IntN n) Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type ConType (IntN n) = IntN n
type SymType (IntN n) Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type SymType (IntN n) = SymIntN n

type IntN8 = IntN 8 Source #

8-bit signed bit-vector

type IntN16 = IntN 16 Source #

16-bit signed bit-vector

type IntN32 = IntN 32 Source #

32-bit signed bit-vector

type IntN64 = IntN 64 Source #

64-bit signed bit-vector

newtype WordN (n :: Nat) Source #

Unsigned bit vector type. Indexed with the bit width. Signedness affect the semantics of the operations, including comparison/extension, etc.

>>> 3 + 5 :: WordN 5
0b01000
>>> sizedBVConcat (0b101 :: WordN 3) (0b110 :: WordN 3)
0b101110
>>> sizedBVExt (Proxy @6) (0b101 :: WordN 3)
0b000101
>>> (8 :: WordN 4) < (7 :: WordN 4)
False

More operations are available. Please refer to Grisette.Core for more information.

Constructors

WordN 

Fields

Instances

Instances details
SizedBV WordN Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

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

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

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

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

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

FromBits SomeWordN Source # 
Instance details

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

Methods

fromBits :: [Bool] -> SomeWordN Source #

ConvertibleBound WordN Source # 
Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

convertibleLowerBound :: forall (eb :: Nat) (sb :: Nat) (n :: Nat). (ValidFP eb sb, KnownNat n, 1 <= n) => WordN n -> FPRoundingMode -> FP eb sb Source #

convertibleUpperBound :: forall (eb :: Nat) (sb :: Nat) (n :: Nat). (ValidFP eb sb, KnownNat n, 1 <= n) => WordN n -> FPRoundingMode -> FP eb sb Source #

PEvalBVTerm WordN Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval

Methods

pevalBVConcatTerm :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => Term (WordN l) -> Term (WordN r) -> Term (WordN (l + r)) Source #

pevalBVExtendTerm :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => Bool -> proxy r -> Term (WordN l) -> Term (WordN r) Source #

pevalBVSelectTerm :: 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 -> Term (WordN n) -> Term (WordN w) Source #

sbvBVConcatTerm :: forall (l :: Nat) (r :: Nat) p1 p2. (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => p1 l -> p2 r -> SBVType (WordN l) -> SBVType (WordN r) -> SBVType (WordN (l + r)) Source #

sbvBVExtendTerm :: forall (l :: Nat) (r :: Nat) p1 p2. (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => p1 l -> p2 r -> Bool -> SBVType (WordN l) -> SBVType (WordN r) Source #

sbvBVSelectTerm :: forall (ix :: Nat) (w :: Nat) (n :: Nat) p1 p2 p3. (KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w, (ix + w) <= n) => p1 ix -> p2 w -> p3 n -> SBVType (WordN n) -> SBVType (WordN w) Source #

BitCast WordN32 Float Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN32 -> Float Source #

BitCast WordN64 Double Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN64 -> Double Source #

BitCast Double WordN64 Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Double -> WordN64 Source #

BitCast Float WordN32 Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Float -> WordN32 Source #

UnifiedFiniteBits 'C SomeWordN Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits

Methods

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

(KnownNat n, 1 <= n) => UnifiedBVImpl 'C WordN IntN n (WordN n) (IntN n) Source # 
Instance details

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

Associated Types

type GetWordN 'C 
Instance details

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

type GetWordN 'C = WordN
type GetIntN 'C 
Instance details

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

type GetIntN 'C = IntN
(KnownNat n, 1 <= n) => UnifiedFromIntegral 'C Integer (WordN n) Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'C) (Integral Integer, Num (WordN n)) (SymFromIntegral Integer (WordN n)) => r) -> r Source #

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeDiv mode ArithException (WordN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

Methods

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

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeLinearArith mode ArithException (WordN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

Methods

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

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeSymRotate mode ArithException (WordN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate

Methods

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

(MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) => UnifiedSafeSymShift mode ArithException (WordN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift

Methods

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

(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP mode NotRepresentableFPError (WordN n) (FP eb sb) FPRoundingMode m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (WordN n) (FP eb sb) FPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) => UnifiedSafeBitCast mode NotRepresentableFPError (FP eb sb) (WordN n) m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeBitCast

Methods

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

BitCast Int16 (WordN 16) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Int16 -> WordN 16 Source #

BitCast Int32 (WordN 32) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Int32 -> WordN 32 Source #

BitCast Int64 (WordN 64) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Int64 -> WordN 64 Source #

BitCast Int8 (WordN 8) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Int8 -> WordN 8 Source #

BitCast Word16 (WordN 16) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Word16 -> WordN 16 Source #

BitCast Word32 (WordN 32) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Word32 -> WordN 32 Source #

BitCast Word64 (WordN 64) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Word64 -> WordN 64 Source #

BitCast Word8 (WordN 8) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Word8 -> WordN 8 Source #

BitCast Bool (WordN 1) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Bool -> WordN 1 Source #

(DecideEvalMode mode, KnownNat a, 1 <= a) => UnifiedSymEq mode (WordN a) Source # 
Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymEq

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (WordN a)) (SymEq (WordN a)) => r) -> r Source #

(DecideEvalMode mode, KnownNat a, 1 <= a) => UnifiedSymOrd mode (WordN a) Source # 
Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymOrd

Methods

withBaseSymOrd :: (If (IsConMode mode) (Ord (WordN a)) (SymOrd (WordN a)) => r) -> r Source #

PEvalBitCastTerm Bool (WordN 1) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm

Methods

pevalBitCastTerm :: Term Bool -> Term (WordN 1) Source #

sbvBitCast :: SBVType Bool -> SBVType (WordN 1) Source #

(KnownNat n, 1 <= n) => PEvalFromIntegralTerm Integer (WordN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm

Methods

pevalFromIntegralTerm :: Term Integer -> Term (WordN n) Source #

sbvFromIntegralTerm :: SBVType Integer -> SBVType (WordN n) Source #

(KnownNat n, 1 <= n) => UnifiedFiniteBits 'C (WordN n) Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits

Methods

withBaseFiniteBits :: (If (IsConMode 'C) (FiniteBits (WordN n), FromBits (WordN n)) (SymFiniteBits (WordN n)) => r) -> r Source #

Lift (WordN n :: Type) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

lift :: Quote m => WordN n -> m Exp #

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

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (WordN n) m Source # 
Instance details

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

Methods

safeAdd :: WordN n -> WordN n -> m (WordN n) Source #

safeNeg :: WordN n -> m (WordN n) Source #

safeSub :: WordN n -> WordN n -> m (WordN n) Source #

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymRotate ArithException (WordN n) m Source # 
Instance details

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

Methods

safeSymRotateL :: WordN n -> WordN n -> m (WordN n) Source #

safeSymRotateR :: WordN n -> WordN n -> m (WordN n) Source #

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymShift ArithException (WordN n) m Source # 
Instance details

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

Methods

safeSymShiftL :: WordN n -> WordN n -> m (WordN n) Source #

safeSymShiftR :: WordN n -> WordN n -> m (WordN n) Source #

safeSymStrictShiftL :: WordN n -> WordN n -> m (WordN n) Source #

safeSymStrictShiftR :: WordN n -> WordN n -> m (WordN n) Source #

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeDiv ArithException (WordN n) m Source # 
Instance details

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

Methods

safeDiv :: WordN n -> WordN n -> m (WordN n) Source #

safeMod :: WordN n -> WordN n -> m (WordN n) Source #

safeDivMod :: WordN n -> WordN n -> m (WordN n, WordN n) Source #

safeQuot :: WordN n -> WordN n -> m (WordN n) Source #

safeRem :: WordN n -> WordN n -> m (WordN n) Source #

safeQuotRem :: WordN n -> WordN n -> m (WordN n, WordN n) Source #

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'C (WordN n') AlgReal Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'C) (Integral (WordN n'), Num AlgReal) (SymFromIntegral (WordN n') AlgReal) => r) -> r Source #

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'C (WordN n') Integer Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'C) (Integral (WordN n'), Num Integer) (SymFromIntegral (WordN n') Integer) => r) -> r Source #

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'C (IntN n') (WordN n) Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'C) (Integral (IntN n'), Num (WordN n)) (SymFromIntegral (IntN n') (WordN n)) => r) -> r Source #

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'C (WordN n') (IntN n) Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'C) (Integral (WordN n'), Num (IntN n)) (SymFromIntegral (WordN n') (IntN n)) => r) -> r Source #

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'C (WordN n') (WordN n) Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

(KnownNat n, 1 <= n) => UnifiedSolvable 'C (WordN n) (WordN n) Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSolvable

Methods

withBaseSolvable :: (If (IsConMode 'C) (WordN n ~ WordN n) (Solvable (WordN n) (WordN 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 'C (WordN n') (FP eb sb) Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'C) (Integral (WordN n'), Num (FP eb sb)) (SymFromIntegral (WordN n') (FP eb sb)) => r) -> r Source #

(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (WordN n) (FP eb sb) FPRoundingMode m Source # 
Instance details

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

Methods

safeFromFP :: FPRoundingMode -> FP eb sb -> m (WordN n) Source #

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeDiv mode (Either SomeBVException ArithException) SomeWordN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

Methods

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

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeLinearArith mode (Either SomeBVException ArithException) SomeWordN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

Methods

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

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymRotate mode (Either SomeBVException ArithException) SomeWordN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate

Methods

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

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymShift mode (Either SomeBVException ArithException) SomeWordN m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift

Methods

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

(ValidFP eb sb, r ~ (eb + sb), KnownNat r, 1 <= r, TryMerge m, MonadError NotRepresentableFPError m) => SafeBitCast NotRepresentableFPError (FP eb sb) (WordN r) m Source # 
Instance details

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

Methods

safeBitCast :: FP eb sb -> m (WordN r) Source #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

arbitrary :: Gen (WordN n) #

shrink :: WordN n -> [WordN n] #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

put :: WordN n -> Put #

get :: Get (WordN n) #

putList :: [WordN n] -> Put #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

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

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

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

Defined in Grisette.Internal.SymPrim.BV

Methods

put :: Putter (WordN n) #

get :: Get (WordN n) #

NFData (WordN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

rnf :: WordN n -> () #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

(.&.) :: WordN n -> WordN n -> WordN n #

(.|.) :: WordN n -> WordN n -> WordN n #

xor :: WordN n -> WordN n -> WordN n #

complement :: WordN n -> WordN n #

shift :: WordN n -> Int -> WordN n #

rotate :: WordN n -> Int -> WordN n #

zeroBits :: WordN n #

bit :: Int -> WordN n #

setBit :: WordN n -> Int -> WordN n #

clearBit :: WordN n -> Int -> WordN n #

complementBit :: WordN n -> Int -> WordN n #

testBit :: WordN n -> Int -> Bool #

bitSizeMaybe :: WordN n -> Maybe Int #

bitSize :: WordN n -> Int #

isSigned :: WordN n -> Bool #

shiftL :: WordN n -> Int -> WordN n #

unsafeShiftL :: WordN n -> Int -> WordN n #

shiftR :: WordN n -> Int -> WordN n #

unsafeShiftR :: WordN n -> Int -> WordN n #

rotateL :: WordN n -> Int -> WordN n #

rotateR :: WordN n -> Int -> WordN n #

popCount :: WordN n -> Int #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

finiteBitSize :: WordN n -> Int #

countLeadingZeros :: WordN n -> Int #

countTrailingZeros :: WordN n -> Int #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

minBound :: WordN n #

maxBound :: WordN n #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

succ :: WordN n -> WordN n #

pred :: WordN n -> WordN n #

toEnum :: Int -> WordN n #

fromEnum :: WordN n -> Int #

enumFrom :: WordN n -> [WordN n] #

enumFromThen :: WordN n -> WordN n -> [WordN n] #

enumFromTo :: WordN n -> WordN n -> [WordN n] #

enumFromThenTo :: WordN n -> WordN n -> WordN n -> [WordN n] #

Generic (WordN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Associated Types

type Rep (WordN n) 
Instance details

Defined in Grisette.Internal.SymPrim.BV

type Rep (WordN n) = D1 ('MetaData "WordN" "Grisette.Internal.SymPrim.BV" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'True) (C1 ('MetaCons "WordN" 'PrefixI 'True) (S1 ('MetaSel ('Just "unWordN") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))

Methods

from :: WordN n -> Rep (WordN n) x #

to :: Rep (WordN n) x -> WordN n #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

(+) :: WordN n -> WordN n -> WordN n #

(-) :: WordN n -> WordN n -> WordN n #

(*) :: WordN n -> WordN n -> WordN n #

negate :: WordN n -> WordN n #

abs :: WordN n -> WordN n #

signum :: WordN n -> WordN n #

fromInteger :: Integer -> WordN n #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

readsPrec :: Int -> ReadS (WordN n) #

readList :: ReadS [WordN n] #

readPrec :: ReadPrec (WordN n) #

readListPrec :: ReadPrec [WordN n] #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

quot :: WordN n -> WordN n -> WordN n #

rem :: WordN n -> WordN n -> WordN n #

div :: WordN n -> WordN n -> WordN n #

mod :: WordN n -> WordN n -> WordN n #

quotRem :: WordN n -> WordN n -> (WordN n, WordN n) #

divMod :: WordN n -> WordN n -> (WordN n, WordN n) #

toInteger :: WordN n -> Integer #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

toRational :: WordN n -> Rational #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

showsPrec :: Int -> WordN n -> ShowS #

show :: WordN n -> String #

showList :: [WordN n] -> ShowS #

Eq (WordN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

(==) :: WordN n -> WordN n -> Bool #

(/=) :: WordN n -> WordN n -> Bool #

Ord (WordN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

compare :: WordN n -> WordN n -> Ordering #

(<) :: WordN n -> WordN n -> Bool #

(<=) :: WordN n -> WordN n -> Bool #

(>) :: WordN n -> WordN n -> Bool #

(>=) :: WordN n -> WordN n -> Bool #

max :: WordN n -> WordN n -> WordN n #

min :: WordN n -> WordN n -> WordN n #

Apply (WordN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Associated Types

type FunType (WordN n) 
Instance details

Defined in Grisette.Internal.SymPrim.BV

type FunType (WordN n) = WordN n

Methods

apply :: WordN n -> FunType (WordN n) Source #

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

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

Methods

fromBits :: [Bool] -> WordN n Source #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

symRotate :: WordN n -> WordN n -> WordN n Source #

symRotateNegated :: WordN n -> WordN n -> WordN n Source #

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

Defined in Grisette.Internal.SymPrim.BV

Methods

symShift :: WordN n -> WordN n -> WordN n Source #

symShiftNegated :: WordN n -> WordN n -> WordN n Source #

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

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

Methods

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

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

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

Methods

extractSym :: WordN n -> AnySymbolSet Source #

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

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

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

Methods

rootStrategy :: MergingStrategy (WordN n) Source #

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

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

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

Methods

pformat :: WordN n -> Doc ann Source #

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

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

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

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

Methods

divOr :: WordN n -> WordN n -> WordN n -> WordN n Source #

modOr :: WordN n -> WordN n -> WordN n -> WordN n Source #

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

quotOr :: WordN n -> WordN n -> WordN n -> WordN n Source #

remOr :: WordN n -> WordN n -> WordN n -> WordN n Source #

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

(KnownNat n, 1 <= n) => SubstSym (WordN 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 -> WordN n -> WordN n Source #

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

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

Methods

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

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

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

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

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

Methods

(.<) :: WordN n -> WordN n -> SymBool Source #

(.<=) :: WordN n -> WordN n -> SymBool Source #

(.>) :: WordN n -> WordN n -> SymBool Source #

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

symCompare :: WordN n -> WordN n -> Union Ordering Source #

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

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: WordN n -> [SomeSym] -> [SomeSym] Source #

allSyms :: WordN n -> [SomeSym] Source #

(KnownNat w, 1 <= w) => NonFuncSBVRep (WordN w) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type NonFuncSBVBaseType (WordN w) 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type NonFuncSBVBaseType (WordN w) = WordN w
(KnownNat n, 1 <= n) => PEvalBitwiseTerm (WordN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitwiseTerm

Methods

pevalAndBitsTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source #

pevalOrBitsTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source #

pevalXorBitsTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source #

pevalComplementBitsTerm :: Term (WordN n) -> Term (WordN n) Source #

withSbvBitwiseTermConstraint :: (Bits (SBVType (WordN n)) => r) -> r Source #

sbvAndBitsTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source #

sbvOrBitsTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source #

sbvXorBitsTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source #

sbvComplementBitsTerm :: SBVType (WordN n) -> SBVType (WordN n) Source #

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalDivModIntegralTerm

Methods

pevalDivIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source #

pevalModIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source #

pevalQuotIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source #

pevalRemIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source #

withSbvDivModIntegralTermConstraint :: (SDivisible (SBVType (WordN n)) => r) -> r Source #

sbvDivIntegralTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source #

sbvModIntegralTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source #

sbvQuotIntegralTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source #

sbvRemIntegralTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source #

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalIEEEFPConvertibleTerm

Methods

pevalFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term (WordN n) -> Term FPRoundingMode -> Term (FP eb sb) -> Term (WordN n) Source #

pevalToFPTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term FPRoundingMode -> Term (WordN n) -> Term (FP eb sb) Source #

sbvFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType (WordN n) -> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType (WordN n) Source #

sbvToFPTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType FPRoundingMode -> SBVType (WordN n) -> SBVType (FP eb sb) Source #

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm

Methods

pevalAddNumTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source #

pevalNegNumTerm :: Term (WordN n) -> Term (WordN n) Source #

pevalMulNumTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source #

pevalAbsNumTerm :: Term (WordN n) -> Term (WordN n) Source #

pevalSignumNumTerm :: Term (WordN n) -> Term (WordN n) Source #

withSbvNumTermConstraint :: (Num (SBVType (WordN n)) => r) -> r Source #

sbvAddNumTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source #

sbvNegNumTerm :: SBVType (WordN n) -> SBVType (WordN n) Source #

sbvMulNumTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source #

sbvAbsNumTerm :: SBVType (WordN n) -> SBVType (WordN n) Source #

sbvSignumNumTerm :: SBVType (WordN n) -> SBVType (WordN n) Source #

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm

Methods

pevalLtOrdTerm :: Term (WordN n) -> Term (WordN n) -> Term Bool Source #

pevalLeOrdTerm :: Term (WordN n) -> Term (WordN n) -> Term Bool Source #

withSbvOrdTermConstraint :: (OrdSymbolic (SBVType (WordN n)) => r) -> r Source #

sbvLtOrdTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBV Bool Source #

sbvLeOrdTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBV Bool Source #

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalRotateTerm

Methods

pevalRotateLeftTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source #

pevalRotateRightTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source #

withSbvRotateTermConstraint :: (SIntegral (NonFuncSBVBaseType (WordN n)) => r) -> r Source #

sbvRotateLeftTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source #

sbvRotateRightTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source #

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

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalShiftTerm

Methods

pevalShiftLeftTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source #

pevalShiftRightTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source #

withSbvShiftTermConstraint :: (SIntegral (NonFuncSBVBaseType (WordN n)) => r) -> r Source #

sbvShiftLeftTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source #

sbvShiftRightTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source #

(KnownNat w, 1 <= w) => SBVRep (WordN w) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type SBVType (WordN w) 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type SBVType (WordN w) = SBV (WordN w)
(KnownNat w, 1 <= w) => SupportedNonFuncPrim (WordN w) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Methods

conNonFuncSBVTerm :: WordN w -> SBV (NonFuncSBVBaseType (WordN w)) Source #

symNonFuncSBVTerm :: SBVFreshMonad m => String -> m (SBV (NonFuncSBVBaseType (WordN w))) Source #

withNonFuncPrim :: (NonFuncPrimConstraint (WordN w) => r) -> r Source #

(KnownNat w, 1 <= w) => SupportedPrim (WordN w) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Methods

primTypeRep :: TypeRep (WordN w) Source #

sameCon :: WordN w -> WordN w -> Bool Source #

hashConWithSalt :: Int -> WordN w -> Int Source #

pformatCon :: WordN w -> String Source #

defaultValue :: WordN w Source #

pevalITETerm :: Term Bool -> Term (WordN w) -> Term (WordN w) -> Term (WordN w) Source #

pevalEqTerm :: Term (WordN w) -> Term (WordN w) -> Term Bool Source #

pevalDistinctTerm :: NonEmpty (Term (WordN w)) -> Term Bool Source #

conSBVTerm :: WordN w -> SBVType (WordN w) Source #

symSBVName :: TypedSymbol 'AnyKind (WordN w) -> Int -> String Source #

symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (WordN w)) Source #

withPrim :: ((PrimConstraint (WordN w), SMTDefinable (SBVType (WordN w)), Mergeable (SBVType (WordN w)), Typeable (SBVType (WordN w))) => a) -> a Source #

sbvIte :: SBV Bool -> SBVType (WordN w) -> SBVType (WordN w) -> SBVType (WordN w) Source #

sbvEq :: SBVType (WordN w) -> SBVType (WordN w) -> SBV Bool Source #

sbvDistinct :: NonEmpty (SBVType (WordN w)) -> SBV Bool Source #

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> WordN w Source #

castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (WordN w) -> Maybe (TypedSymbol knd' (WordN w)) Source #

funcDummyConstraint :: SBVType (WordN w) -> SBV Bool Source #

(KnownNat w, 1 <= w) => SupportedPrimConstraint (WordN w) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type PrimConstraint (WordN w) 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type PrimConstraint (WordN w) = (KnownNat w, 1 <= w, BVIsNonZero w)
(KnownNat n, 1 <= n) => SymRep (WordN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type SymType (WordN n) 
Instance details

Defined in Grisette.Internal.SymPrim.SymBV

type SymType (WordN n) = SymWordN n
(KnownNat n, 1 <= n) => UnifiedConRep (WordN n) Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

Associated Types

type ConType (WordN n) 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type ConType (WordN n) = WordN n
(KnownNat n, 1 <= n) => UnifiedSymRep (WordN n) Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

Associated Types

type SymType (WordN n) 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type SymType (WordN n) = SymWordN n
Hashable (WordN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

hashWithSalt :: Int -> WordN n -> Int #

hash :: WordN n -> Int #

BitCast (WordN 1) Bool Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 1 -> Bool Source #

BitCast (WordN 8) Int8 Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 8 -> Int8 Source #

BitCast (WordN 8) Word8 Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 8 -> Word8 Source #

BitCast (WordN 16) Int16 Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 16 -> Int16 Source #

BitCast (WordN 16) Word16 Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 16 -> Word16 Source #

BitCast (WordN 32) Int32 Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 32 -> Int32 Source #

BitCast (WordN 32) Word32 Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 32 -> Word32 Source #

BitCast (WordN 64) Int64 Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 64 -> Int64 Source #

BitCast (WordN 64) Word64 Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 64 -> Word64 Source #

PEvalBitCastTerm (WordN 1) Bool Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm

Methods

pevalBitCastTerm :: Term (WordN 1) -> Term Bool Source #

sbvBitCast :: SBVType (WordN 1) -> SBVType Bool Source #

(KnownNat n, 1 <= n) => PEvalFromIntegralTerm (WordN n) AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm

Methods

pevalFromIntegralTerm :: Term (WordN n) -> Term AlgReal Source #

sbvFromIntegralTerm :: SBVType (WordN n) -> SBVType AlgReal Source #

(KnownNat n, 1 <= n) => PEvalFromIntegralTerm (WordN n) Integer Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm

Methods

pevalFromIntegralTerm :: Term (WordN n) -> Term Integer Source #

sbvFromIntegralTerm :: SBVType (WordN n) -> SBVType Integer Source #

(KnownNat n, 1 <= n) => BitCast (IntN n) (WordN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN n -> WordN n Source #

(KnownNat n, 1 <= n) => BitCast (WordN n) (IntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN n -> IntN n Source #

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

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

Methods

fresh :: MonadFresh m => WordN n -> m (Union (WordN n)) Source #

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

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

Methods

simpleFresh :: MonadFresh m => WordN n -> m (WordN n) Source #

(KnownNat n, 1 <= n) => SignConversion (WordN n) (IntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

Methods

toSigned :: WordN n -> IntN n Source #

toUnsigned :: IntN n -> WordN 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 (WordN n) (WordN n) Source # 
Instance details

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

Methods

toCon :: WordN n -> Maybe (WordN n) 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 #

(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) (WordN n) Source # 
Instance details

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

Methods

toSym :: WordN n -> WordN 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) => 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 #

(KnownNat n, 1 <= n) => PEvalBitCastTerm (IntN n) (WordN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval

Methods

pevalBitCastTerm :: Term (IntN n) -> Term (WordN n) Source #

sbvBitCast :: SBVType (IntN n) -> SBVType (WordN n) Source #

(KnownNat n, 1 <= n) => PEvalBitCastTerm (WordN n) (IntN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval

Methods

pevalBitCastTerm :: Term (WordN n) -> Term (IntN n) Source #

sbvBitCast :: SBVType (WordN n) -> SBVType (IntN n) Source #

(KnownNat n, 1 <= n, KnownNat m, 1 <= m) => PEvalFromIntegralTerm (IntN n) (WordN m) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm

Methods

pevalFromIntegralTerm :: Term (IntN n) -> Term (WordN m) Source #

sbvFromIntegralTerm :: SBVType (IntN n) -> SBVType (WordN m) Source #

(KnownNat n, 1 <= n, KnownNat m, 1 <= m) => PEvalFromIntegralTerm (WordN n) (IntN m) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm

Methods

pevalFromIntegralTerm :: Term (WordN n) -> Term (IntN m) Source #

sbvFromIntegralTerm :: SBVType (WordN n) -> SBVType (IntN m) Source #

(KnownNat n, 1 <= n, KnownNat m, 1 <= m) => PEvalFromIntegralTerm (WordN n) (WordN m) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm

Methods

pevalFromIntegralTerm :: Term (WordN n) -> Term (WordN m) Source #

sbvFromIntegralTerm :: SBVType (WordN n) -> SBVType (WordN m) Source #

(ValidFP eb sb, r ~ (eb + sb)) => BitCast (WordN r) (FP eb sb) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: WordN r -> FP eb sb Source #

(n ~ (eb + sb), ValidFP eb sb, KnownNat n, 1 <= n) => PEvalBitCastTerm (WordN n) (FP eb sb) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm

Methods

pevalBitCastTerm :: Term (WordN n) -> Term (FP eb sb) Source #

sbvBitCast :: SBVType (WordN n) -> SBVType (FP eb sb) Source #

(KnownNat n, 1 <= n, ValidFP eb sb) => PEvalFromIntegralTerm (WordN n) (FP eb sb) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm

Methods

pevalFromIntegralTerm :: Term (WordN n) -> Term (FP eb sb) Source #

sbvFromIntegralTerm :: SBVType (WordN n) -> SBVType (FP eb sb) Source #

(ValidFP eb sb, KnownNat n, 1 <= n) => IEEEFPConvertible (WordN n) (FP eb sb) FPRoundingMode Source # 
Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

fromFPOr :: WordN n -> FPRoundingMode -> FP eb sb -> WordN n Source #

toFP :: FPRoundingMode -> WordN n -> FP eb sb Source #

(ValidFP eb sb, n ~ (eb + sb)) => BitCastCanonical (FP eb sb) (WordN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCastCanonicalValue :: proxy (FP eb sb) -> WordN n Source #

(ValidFP eb sb, r ~ (eb + sb)) => BitCastOr (FP eb sb) (WordN r) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCastOr :: WordN r -> FP eb sb -> WordN r Source #

(n ~ (eb + sb), ValidFP eb sb, KnownNat n, 1 <= n) => PEvalBitCastOrTerm (FP eb sb) (WordN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm

Methods

pevalBitCastOrTerm :: Term (WordN n) -> Term (FP eb sb) -> Term (WordN n) Source #

sbvBitCastOr :: SBVType (WordN n) -> SBVType (FP eb sb) -> SBVType (WordN n) Source #

type Rep (WordN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

type Rep (WordN n) = D1 ('MetaData "WordN" "Grisette.Internal.SymPrim.BV" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'True) (C1 ('MetaCons "WordN" 'PrefixI 'True) (S1 ('MetaSel ('Just "unWordN") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))
type FunType (WordN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.BV

type FunType (WordN n) = WordN n
type NonFuncSBVBaseType (WordN w) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type NonFuncSBVBaseType (WordN w) = WordN w
type PrimConstraint (WordN w) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type PrimConstraint (WordN w) = (KnownNat w, 1 <= w, BVIsNonZero w)
type SBVType (WordN w) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type SBVType (WordN w) = SBV (WordN w)
type SymType (WordN n) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymBV

type SymType (WordN n) = SymWordN n
type ConType (WordN n) Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type ConType (WordN n) = WordN n
type SymType (WordN n) Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type SymType (WordN n) = SymWordN n

type WordN8 = WordN 8 Source #

8-bit unsigned bit-vector

type WordN16 = WordN 16 Source #

16-bit unsigned bit-vector

type WordN32 = WordN 32 Source #

32-bit unsigned bit-vector

type WordN64 = WordN 64 Source #

64-bit unsigned bit-vector

readBinary :: Num a => ReadPrec a Source #

Read a binary number.