Grisette.Internal.SymPrim.BV

Documentation

newtype IntN (n :: Nat)

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

• unIntN :: Integer

Instances

SizedBV IntN

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)

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

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

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

sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> IntN n -> IntN w

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

FromBits SomeIntN

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

Methods

fromBits :: [Bool] -> SomeIntN

ConvertibleBound IntN

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

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

PEvalBVTerm IntN

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))

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)

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)

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))

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)

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)

BitCast IntN32 Float

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN32 -> Float

BitCast IntN64 Double

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN64 -> Double

BitCast Double IntN64

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Double -> IntN64

BitCast Float IntN32

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Float -> IntN32

UnifiedFiniteBits 'Con SomeIntN

Defined in Grisette.Unified.Internal.Class.UnifiedFiniteBits

Methods

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

(KnownNat n, 1 <= n) => UnifiedBVImpl 'Con WordN IntN n (WordN n) (IntN n)

Defined in Grisette.Unified.Internal.UnifiedBV

Associated Types

type GetWordN 'Con = (w :: Nat -> Type)

type GetIntN 'Con = (i :: Nat -> Type)

(KnownNat n, 1 <= n) => UnifiedFromIntegral 'Con Integer (IntN n)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

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

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

Defined in Grisette.Unified.Internal.Class.UnifiedSafeDiv

Methods

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

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

Defined in Grisette.Unified.Internal.Class.UnifiedSafeLinearArith

Methods

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

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

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymRotate

Methods

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

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

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymShift

Methods

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

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

Defined in Grisette.Unified.Internal.Class.UnifiedSafeFromFP

Methods

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

(Typeable mode, 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

Defined in Grisette.Unified.Internal.Class.UnifiedSafeBitCast

Methods

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

BitCast Int16 (IntN 16)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Int16 -> IntN 16

BitCast Int32 (IntN 32)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Int32 -> IntN 32

BitCast Int64 (IntN 64)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Int64 -> IntN 64

BitCast Int8 (IntN 8)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Int8 -> IntN 8

BitCast Word16 (IntN 16)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Word16 -> IntN 16

BitCast Word32 (IntN 32)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Word32 -> IntN 32

BitCast Word64 (IntN 64)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Word64 -> IntN 64

BitCast Word8 (IntN 8)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Word8 -> IntN 8

BitCast Bool (IntN 1)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Bool -> IntN 1

PEvalBitCastTerm Bool (IntN 1)

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

Methods

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

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

(KnownNat n, 1 <= n) => PEvalFromIntegralTerm Integer (IntN n)

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

Methods

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

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

(KnownNat n, 1 <= n) => UnifiedFiniteBits 'Con (IntN n)

Defined in Grisette.Unified.Internal.Class.UnifiedFiniteBits

Methods

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

(Typeable mode, KnownNat n, 1 <= n) => UnifiedSymEq mode (IntN n)

Defined in Grisette.Unified.Internal.Class.UnifiedSymEq

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (IntN n)) (SymEq (IntN n)) => r) -> r

(Typeable mode, KnownNat n, 1 <= n) => UnifiedSymOrd mode (IntN n)

Defined in Grisette.Unified.Internal.Class.UnifiedSymOrd

Methods

withBaseSymOrd :: (If (IsConMode mode) (Ord (IntN n)) (SymOrd (IntN n)) => r) -> r

Lift (IntN n :: Type)

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) => SafeDiv ArithException (IntN n) m

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

Methods

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

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

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

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

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

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

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (IntN n) m

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

Methods

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

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

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

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

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

Methods

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

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

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymShift ArithException (IntN n) m

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

Methods

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

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

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

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

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'Con (IntN n') AlgReal

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

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

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'Con (IntN n') Integer

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

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

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'Con (IntN n') (IntN n)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

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

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'Con (IntN n') (WordN n)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

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

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'Con (WordN n') (IntN n)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

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

(KnownNat n', 1 <= n', ValidFP eb sb) => UnifiedFromIntegral 'Con (IntN n') (FP eb sb)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

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

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

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

Methods

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

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeDiv mode (Either SomeBVException ArithException) SomeIntN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeDiv

Methods

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

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeLinearArith mode (Either SomeBVException ArithException) SomeIntN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeLinearArith

Methods

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

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymRotate mode (Either SomeBVException ArithException) SomeIntN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymRotate

Methods

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

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymShift mode (Either SomeBVException ArithException) SomeIntN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymShift

Methods

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

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

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

Methods

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

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

Defined in Grisette.Internal.SymPrim.BV

Methods

arbitrary :: Gen (IntN n)

shrink :: IntN n -> [IntN n]

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

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)

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)

Defined in Grisette.Internal.SymPrim.BV

Methods

minBound :: IntN n

maxBound :: IntN n

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

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)

Defined in Grisette.Internal.SymPrim.BV

Associated Types

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

Methods

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

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

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

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)

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)

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)

Defined in Grisette.Internal.SymPrim.BV

Methods

toRational :: IntN n -> Rational

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

Defined in Grisette.Internal.SymPrim.BV

Methods

showsPrec :: Int -> IntN n -> ShowS

show :: IntN n -> String

showList :: [IntN n] -> ShowS

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

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)

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)

Defined in Grisette.Internal.SymPrim.BV

Methods

put :: Putter (IntN n)

get :: Get (IntN n)

NFData (IntN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

rnf :: IntN n -> ()

Eq (IntN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

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

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

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

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

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

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

Methods

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

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

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

Methods

extractSym :: IntN n -> AnySymbolSet

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

Apply (IntN n)

Defined in Grisette.Internal.SymPrim.BV

Associated Types

type FunType (IntN n)

Methods

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

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

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

Methods

rootStrategy :: MergingStrategy (IntN n)

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

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

Methods

pformat :: IntN n -> Doc ann

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

pformatList :: [IntN n] -> Doc ann

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

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

Methods

divOr :: IntN n -> IntN n -> IntN n -> IntN n

modOr :: IntN n -> IntN n -> IntN n -> IntN n

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

quotOr :: IntN n -> IntN n -> IntN n -> IntN n

remOr :: IntN n -> IntN n -> IntN n -> IntN n

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

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

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

Methods

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

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

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

Methods

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

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

symDistinct :: [IntN n] -> SymBool

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

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

Methods

fromBits :: [Bool] -> IntN n

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

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

Methods

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

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

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

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

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

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

Defined in Grisette.Internal.SymPrim.BV

Methods

symRotate :: IntN n -> IntN n -> IntN n

symRotateNegated :: IntN n -> IntN n -> IntN n

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

Defined in Grisette.Internal.SymPrim.BV

Methods

symShift :: IntN n -> IntN n -> IntN n

symShiftNegated :: IntN n -> IntN n -> IntN n

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

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

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

allSyms :: IntN n -> [SomeSym]

(KnownNat w, 1 <= w) => NonFuncSBVRep (IntN w)

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

Associated Types

type NonFuncSBVBaseType (IntN w)

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

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

Methods

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

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

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

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

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

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

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

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

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

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

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

Methods

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

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

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

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

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

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

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

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

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

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

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)

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

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

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

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

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

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

Methods

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

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

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

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

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

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

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

Methods

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

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

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

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

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

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

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

Methods

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

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

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

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

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

(KnownNat w, 1 <= w) => SBVRep (IntN w)

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

Associated Types

type SBVType (IntN w)

(KnownNat w, 1 <= w) => SupportedNonFuncPrim (IntN w)

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

Methods

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

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

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

(KnownNat w, 1 <= w) => SupportedPrim (IntN w)

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

Methods

primTypeRep :: TypeRep (IntN w)

sameCon :: IntN w -> IntN w -> Bool

hashConWithSalt :: Int -> IntN w -> Int

pformatCon :: IntN w -> String

defaultValue :: IntN w

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

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

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

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

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

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

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

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

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

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

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

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

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

(KnownNat w, 1 <= w) => SupportedPrimConstraint (IntN w)

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

Associated Types

type PrimConstraint (IntN w)

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

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type SymType (IntN n)

Hashable (IntN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

hashWithSalt :: Int -> IntN n -> Int

hash :: IntN n -> Int

BitCast (IntN 1) Bool

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 1 -> Bool

BitCast (IntN 8) Int8

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 8 -> Int8

BitCast (IntN 8) Word8

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 8 -> Word8

BitCast (IntN 16) Int16

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 16 -> Int16

BitCast (IntN 16) Word16

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 16 -> Word16

BitCast (IntN 32) Int32

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 32 -> Int32

BitCast (IntN 32) Word32

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 32 -> Word32

BitCast (IntN 64) Int64

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 64 -> Int64

BitCast (IntN 64) Word64

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN 64 -> Word64

PEvalBitCastTerm (IntN 1) Bool

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

Methods

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

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

(KnownNat n, 1 <= n) => PEvalFromIntegralTerm (IntN n) AlgReal

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

Methods

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

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

(KnownNat n, 1 <= n) => PEvalFromIntegralTerm (IntN n) Integer

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

Methods

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

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

(KnownNat n, 1 <= n) => BitCast (IntN n) (WordN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN n -> WordN n

(KnownNat n, 1 <= n) => BitCast (WordN n) (IntN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN n -> IntN n

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

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

Methods

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

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

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

Methods

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

(KnownNat n, 1 <= n) => SignConversion (WordN n) (IntN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

toSigned :: WordN n -> IntN n

toUnsigned :: IntN n -> WordN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

con :: IntN n -> SymIntN n

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

sym :: Symbol -> SymIntN n

ssym :: Identifier -> SymIntN n

isym :: Identifier -> Int -> SymIntN n

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

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

Methods

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

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

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

Methods

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

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

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

Methods

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

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

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

Methods

toSym :: IntN n -> IntN n

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

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

Methods

toSym :: IntN n -> SymIntN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

(KnownNat n, 1 <= n) => PEvalBitCastTerm (IntN n) (WordN n)

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

Methods

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

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

(KnownNat n, 1 <= n) => PEvalBitCastTerm (WordN n) (IntN n)

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

Methods

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

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

(KnownNat n, 1 <= n, KnownNat m, 1 <= m) => PEvalFromIntegralTerm (IntN n) (IntN m)

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

Methods

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

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

(KnownNat n, 1 <= n, KnownNat m, 1 <= m) => PEvalFromIntegralTerm (IntN n) (WordN m)

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

Methods

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

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

(KnownNat n, 1 <= n, KnownNat m, 1 <= m) => PEvalFromIntegralTerm (WordN n) (IntN m)

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

Methods

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

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

(ValidFP eb sb, r ~ (eb + sb)) => BitCast (IntN r) (FP eb sb)

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: IntN r -> FP eb sb

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

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

Methods

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

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

(KnownNat n, 1 <= n, ValidFP eb sb) => PEvalFromIntegralTerm (IntN n) (FP eb sb)

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

Methods

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

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

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

Defined in Grisette.Internal.SymPrim.FP

Methods

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

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

(ValidFP eb sb, n ~ (eb + sb)) => BitCastCanonical (FP eb sb) (IntN n)

Defined in Grisette.Internal.SymPrim.FP

Methods

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

(ValidFP eb sb, n ~ (eb + sb)) => BitCastOr (FP eb sb) (IntN n)

Defined in Grisette.Internal.SymPrim.FP

Methods

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

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

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

Methods

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

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

type Rep (IntN n)

Defined in Grisette.Internal.SymPrim.BV

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

type FunType (IntN n)

Defined in Grisette.Internal.SymPrim.BV

type FunType (IntN n) = IntN n

type NonFuncSBVBaseType (IntN w)

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

type NonFuncSBVBaseType (IntN w) = IntN w

type PrimConstraint (IntN w)

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

type PrimConstraint (IntN w) = (KnownNat w, 1 <= w, BVIsNonZero w)

type SBVType (IntN w)

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

type SBVType (IntN w) = SBV (IntN w)

type SymType (IntN n)

Defined in Grisette.Internal.SymPrim.SymBV

type SymType (IntN n) = SymIntN n

type IntN8 = IntN 8

8-bit signed bit-vector

type IntN16 = IntN 16

16-bit signed bit-vector

type IntN32 = IntN 32

32-bit signed bit-vector

type IntN64 = IntN 64

64-bit signed bit-vector

newtype WordN (n :: Nat)

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

• unWordN :: Integer

Instances

SizedBV WordN

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)

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

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

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

sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> WordN n -> WordN w

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

FromBits SomeWordN

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

Methods

fromBits :: [Bool] -> SomeWordN

ConvertibleBound WordN

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

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

PEvalBVTerm WordN

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))

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)

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)

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))

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)

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)

BitCast WordN32 Float

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN32 -> Float

BitCast WordN64 Double

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN64 -> Double

BitCast Double WordN64

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Double -> WordN64

BitCast Float WordN32

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Float -> WordN32

UnifiedFiniteBits 'Con SomeWordN

Defined in Grisette.Unified.Internal.Class.UnifiedFiniteBits

Methods

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

(KnownNat n, 1 <= n) => UnifiedBVImpl 'Con WordN IntN n (WordN n) (IntN n)

Defined in Grisette.Unified.Internal.UnifiedBV

Associated Types

type GetWordN 'Con = (w :: Nat -> Type)

type GetIntN 'Con = (i :: Nat -> Type)

(KnownNat n, 1 <= n) => UnifiedFromIntegral 'Con Integer (WordN n)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

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

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

Defined in Grisette.Unified.Internal.Class.UnifiedSafeDiv

Methods

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

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

Defined in Grisette.Unified.Internal.Class.UnifiedSafeLinearArith

Methods

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

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

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymRotate

Methods

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

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

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymShift

Methods

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

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

Defined in Grisette.Unified.Internal.Class.UnifiedSafeFromFP

Methods

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

(Typeable mode, 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

Defined in Grisette.Unified.Internal.Class.UnifiedSafeBitCast

Methods

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

BitCast Int16 (WordN 16)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Int16 -> WordN 16

BitCast Int32 (WordN 32)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Int32 -> WordN 32

BitCast Int64 (WordN 64)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Int64 -> WordN 64

BitCast Int8 (WordN 8)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Int8 -> WordN 8

BitCast Word16 (WordN 16)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Word16 -> WordN 16

BitCast Word32 (WordN 32)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Word32 -> WordN 32

BitCast Word64 (WordN 64)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Word64 -> WordN 64

BitCast Word8 (WordN 8)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Word8 -> WordN 8

BitCast Bool (WordN 1)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: Bool -> WordN 1

PEvalBitCastTerm Bool (WordN 1)

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

Methods

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

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

(KnownNat n, 1 <= n) => PEvalFromIntegralTerm Integer (WordN n)

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

Methods

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

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

(KnownNat n, 1 <= n) => UnifiedFiniteBits 'Con (WordN n)

Defined in Grisette.Unified.Internal.Class.UnifiedFiniteBits

Methods

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

(Typeable mode, KnownNat n, 1 <= n) => UnifiedSymEq mode (WordN n)

Defined in Grisette.Unified.Internal.Class.UnifiedSymEq

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (WordN n)) (SymEq (WordN n)) => r) -> r

(Typeable mode, KnownNat n, 1 <= n) => UnifiedSymOrd mode (WordN n)

Defined in Grisette.Unified.Internal.Class.UnifiedSymOrd

Methods

withBaseSymOrd :: (If (IsConMode mode) (Ord (WordN n)) (SymOrd (WordN n)) => r) -> r

Lift (WordN n :: Type)

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) => SafeDiv ArithException (WordN n) m

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

Methods

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

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

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

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

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

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

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (WordN n) m

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

Methods

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

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

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

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

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

Methods

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

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

(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymShift ArithException (WordN n) m

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

Methods

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

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

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

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

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'Con (WordN n') AlgReal

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

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

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'Con (WordN n') Integer

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

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

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'Con (IntN n') (WordN n)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

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

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'Con (WordN n') (IntN n)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

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

(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'Con (WordN n') (WordN n)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

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

(KnownNat n', 1 <= n', ValidFP eb sb) => UnifiedFromIntegral 'Con (WordN n') (FP eb sb)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

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

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

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

Methods

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

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeDiv mode (Either SomeBVException ArithException) SomeWordN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeDiv

Methods

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

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeLinearArith mode (Either SomeBVException ArithException) SomeWordN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeLinearArith

Methods

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

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymRotate mode (Either SomeBVException ArithException) SomeWordN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymRotate

Methods

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

(MonadError (Either SomeBVException ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymShift mode (Either SomeBVException ArithException) SomeWordN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymShift

Methods

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

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

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

Methods

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

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

Defined in Grisette.Internal.SymPrim.BV

Methods

arbitrary :: Gen (WordN n)

shrink :: WordN n -> [WordN n]

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

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)

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)

Defined in Grisette.Internal.SymPrim.BV

Methods

minBound :: WordN n

maxBound :: WordN n

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

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)

Defined in Grisette.Internal.SymPrim.BV

Associated Types

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

Methods

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

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

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

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)

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)

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)

Defined in Grisette.Internal.SymPrim.BV

Methods

toRational :: WordN n -> Rational

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

Defined in Grisette.Internal.SymPrim.BV

Methods

showsPrec :: Int -> WordN n -> ShowS

show :: WordN n -> String

showList :: [WordN n] -> ShowS

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

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)

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)

Defined in Grisette.Internal.SymPrim.BV

Methods

put :: Putter (WordN n)

get :: Get (WordN n)

NFData (WordN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

rnf :: WordN n -> ()

Eq (WordN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

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

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

Ord (WordN n)

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

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

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

Methods

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

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

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

Methods

extractSym :: WordN n -> AnySymbolSet

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

Apply (WordN n)

Defined in Grisette.Internal.SymPrim.BV

Associated Types

type FunType (WordN n)

Methods

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

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

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

Methods

rootStrategy :: MergingStrategy (WordN n)

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

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

Methods

pformat :: WordN n -> Doc ann

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

pformatList :: [WordN n] -> Doc ann

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

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

Methods

divOr :: WordN n -> WordN n -> WordN n -> WordN n

modOr :: WordN n -> WordN n -> WordN n -> WordN n

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

quotOr :: WordN n -> WordN n -> WordN n -> WordN n

remOr :: WordN n -> WordN n -> WordN n -> WordN n

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

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

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

Methods

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

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

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

Methods

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

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

symDistinct :: [WordN n] -> SymBool

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

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

Methods

fromBits :: [Bool] -> WordN n

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

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

Methods

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

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

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

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

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

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

Defined in Grisette.Internal.SymPrim.BV

Methods

symRotate :: WordN n -> WordN n -> WordN n

symRotateNegated :: WordN n -> WordN n -> WordN n

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

Defined in Grisette.Internal.SymPrim.BV

Methods

symShift :: WordN n -> WordN n -> WordN n

symShiftNegated :: WordN n -> WordN n -> WordN n

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

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

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

allSyms :: WordN n -> [SomeSym]

(KnownNat w, 1 <= w) => NonFuncSBVRep (WordN w)

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

Associated Types

type NonFuncSBVBaseType (WordN w)

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

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

Methods

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

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

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

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

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

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

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

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

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

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

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

Methods

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

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

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

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

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

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

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

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

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

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

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)

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

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

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

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

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

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

Methods

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

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

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

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

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

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

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

Methods

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

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

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

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

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

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

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

Methods

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

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

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

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

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

(KnownNat w, 1 <= w) => SBVRep (WordN w)

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

Associated Types

type SBVType (WordN w)

(KnownNat w, 1 <= w) => SupportedNonFuncPrim (WordN w)

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

Methods

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

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

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

(KnownNat w, 1 <= w) => SupportedPrim (WordN w)

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

Methods

primTypeRep :: TypeRep (WordN w)

sameCon :: WordN w -> WordN w -> Bool

hashConWithSalt :: Int -> WordN w -> Int

pformatCon :: WordN w -> String

defaultValue :: WordN w

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

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

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

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

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

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

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

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

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

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

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

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

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

(KnownNat w, 1 <= w) => SupportedPrimConstraint (WordN w)

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

Associated Types

type PrimConstraint (WordN w)

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

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type SymType (WordN n)

Hashable (WordN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

hashWithSalt :: Int -> WordN n -> Int

hash :: WordN n -> Int

BitCast (WordN 1) Bool

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 1 -> Bool

BitCast (WordN 8) Int8

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 8 -> Int8

BitCast (WordN 8) Word8

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 8 -> Word8

BitCast (WordN 16) Int16

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 16 -> Int16

BitCast (WordN 16) Word16

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 16 -> Word16

BitCast (WordN 32) Int32

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 32 -> Int32

BitCast (WordN 32) Word32

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 32 -> Word32

BitCast (WordN 64) Int64

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 64 -> Int64

BitCast (WordN 64) Word64

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN 64 -> Word64

PEvalBitCastTerm (WordN 1) Bool

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

Methods

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

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

(KnownNat n, 1 <= n) => PEvalFromIntegralTerm (WordN n) AlgReal

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

Methods

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

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

(KnownNat n, 1 <= n) => PEvalFromIntegralTerm (WordN n) Integer

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

Methods

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

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

(KnownNat n, 1 <= n) => BitCast (IntN n) (WordN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: IntN n -> WordN n

(KnownNat n, 1 <= n) => BitCast (WordN n) (IntN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

bitCast :: WordN n -> IntN n

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

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

Methods

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

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

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

Methods

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

(KnownNat n, 1 <= n) => SignConversion (WordN n) (IntN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

toSigned :: WordN n -> IntN n

toUnsigned :: IntN n -> WordN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

con :: WordN n -> SymWordN n

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

sym :: Symbol -> SymWordN n

ssym :: Identifier -> SymWordN n

isym :: Identifier -> Int -> SymWordN n

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

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

Methods

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

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

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

Methods

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

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

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

Methods

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

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

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

Methods

toSym :: WordN n -> WordN n

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

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

Methods

toSym :: WordN n -> SymWordN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

(KnownNat n, 1 <= n) => PEvalBitCastTerm (IntN n) (WordN n)

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

Methods

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

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

(KnownNat n, 1 <= n) => PEvalBitCastTerm (WordN n) (IntN n)

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

Methods

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

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

(KnownNat n, 1 <= n, KnownNat m, 1 <= m) => PEvalFromIntegralTerm (IntN n) (WordN m)

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

Methods

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

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

(KnownNat n, 1 <= n, KnownNat m, 1 <= m) => PEvalFromIntegralTerm (WordN n) (IntN m)

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

Methods

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

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

(KnownNat n, 1 <= n, KnownNat m, 1 <= m) => PEvalFromIntegralTerm (WordN n) (WordN m)

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

Methods

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

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

(ValidFP eb sb, r ~ (eb + sb)) => BitCast (WordN r) (FP eb sb)

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: WordN r -> FP eb sb

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

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

Methods

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

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

(KnownNat n, 1 <= n, ValidFP eb sb) => PEvalFromIntegralTerm (WordN n) (FP eb sb)

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

Methods

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

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

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

Defined in Grisette.Internal.SymPrim.FP

Methods

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

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

(ValidFP eb sb, n ~ (eb + sb)) => BitCastCanonical (FP eb sb) (WordN n)

Defined in Grisette.Internal.SymPrim.FP

Methods

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

(ValidFP eb sb, r ~ (eb + sb)) => BitCastOr (FP eb sb) (WordN r)

Defined in Grisette.Internal.SymPrim.FP

Methods

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

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

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

Methods

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

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

type Rep (WordN n)

Defined in Grisette.Internal.SymPrim.BV

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

type FunType (WordN n)

Defined in Grisette.Internal.SymPrim.BV

type FunType (WordN n) = WordN n

type NonFuncSBVBaseType (WordN w)

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

type NonFuncSBVBaseType (WordN w) = WordN w

type PrimConstraint (WordN w)

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

type PrimConstraint (WordN w) = (KnownNat w, 1 <= w, BVIsNonZero w)

type SBVType (WordN w)

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

type SBVType (WordN w) = SBV (WordN w)

type SymType (WordN n)

Defined in Grisette.Internal.SymPrim.SymBV

type SymType (WordN n) = SymWordN n

type WordN8 = WordN 8

8-bit unsigned bit-vector

type WordN16 = WordN 16

16-bit unsigned bit-vector

type WordN32 = WordN 32

32-bit unsigned bit-vector

type WordN64 = WordN 64

64-bit unsigned bit-vector