Copyright	(c) Sirui Lu 2021-2023
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	Safe-Inferred
Language	Haskell2010

Grisette.Internal.SymPrim.SymBV

Contents

Orphan instances

Description

Synopsis

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

Documentation

newtype SymWordN (n :: Nat) Source #

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

>>> "a" + 5 :: SymWordN 5
(+ 0b00101 a)
>>> sizedBVConcat (con 0b101 :: SymWordN 3) (con 0b110 :: SymWordN 3)
0b101110
>>> sizedBVExt (Proxy @6) (con 0b101 :: SymWordN 3)
0b000101
>>> (8 :: SymWordN 4) .< (7 :: SymWordN 4)
false

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

Constructors

SymWordN (Term (WordN n))

Instances

Instances details

SizedBV SymWordN Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => SymWordN l -> SymWordN r -> SymWordN (l + r) Source # sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymWordN l -> SymWordN r Source # sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymWordN l -> SymWordN r Source # sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymWordN l -> SymWordN r Source # sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> SymWordN n -> SymWordN w Source # sizedBVFromIntegral :: forall a (n :: Nat). (Integral a, KnownNat n, 1 <= n) => a -> SymWordN n Source #
UnifiedFiniteBits 'S SomeSymWordN Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits Methods withBaseFiniteBits :: (If (IsConMode 'S) (FiniteBits SomeSymWordN, FromBits SomeSymWordN) (SymFiniteBits SomeSymWordN) => r) -> r Source #
(KnownNat n, 1 <= n) => UnifiedBVImpl 'S SymWordN SymIntN n (SymWordN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedBV Associated Types type GetWordN 'S = (w :: Nat -> Type) Source # type GetIntN 'S = (i :: Nat -> Type) Source #
(KnownNat n, 1 <= n) => UnifiedFromIntegral 'S SymInteger (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral SymInteger, Num (SymWordN n)) (SymFromIntegral SymInteger (SymWordN n)) => r) -> r Source #
(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeDiv 'S ArithException (SymWordN n) m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv Methods withBaseSafeDiv :: (SafeDiv ArithException (SymWordN n) m => r) -> r Source #
(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeLinearArith 'S ArithException (SymWordN n) m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith Methods withBaseSafeLinearArith :: (SafeLinearArith ArithException (SymWordN n) m => r) -> r Source #
(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeSymRotate 'S ArithException (SymWordN n) m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate Methods withBaseSafeSymRotate :: (SafeSymRotate ArithException (SymWordN n) m => r) -> r Source #
(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeSymShift 'S ArithException (SymWordN n) m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift Methods withBaseSafeSymShift :: (SafeSymShift ArithException (SymWordN n) m => r) -> r Source #
(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP 'S NotRepresentableFPError (SymWordN n) (SymFP eb sb) SymFPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP Methods withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (SymWordN n) (SymFP eb sb) SymFPRoundingMode m => r) -> r Source #
(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) => UnifiedSafeBitCast 'S NotRepresentableFPError (SymFP eb sb) (SymWordN n) m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeBitCast Methods withBaseSafeBitCast :: (SafeBitCast NotRepresentableFPError (SymFP eb sb) (SymWordN n) m => r) -> r Source #
BitCast SymBool (SymWordN 1) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods bitCast :: SymBool -> SymWordN 1 Source #
(KnownNat n, 1 <= n) => GenSym () (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => () -> m (Union (SymWordN n)) Source #
(KnownNat n, 1 <= n) => GenSymSimple () (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods simpleFresh :: MonadFresh m => () -> m (SymWordN n) Source #
(KnownNat n, 1 <= n) => SymFromIntegral SymInteger (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFromIntegral Methods symFromIntegral :: SymInteger -> SymWordN n Source #
ToSym Word16 (SymWordN 16) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: Word16 -> SymWordN 16 Source #
ToSym Word32 (SymWordN 32) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: Word32 -> SymWordN 32 Source #
ToSym Word64 (SymWordN 64) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: Word64 -> SymWordN 64 Source #
ToSym Word8 (SymWordN 8) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: Word8 -> SymWordN 8 Source #
ToSym Word (SymWordN 64) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: Word -> SymWordN 64 Source #
(KnownNat n, 1 <= n) => UnifiedFiniteBits 'S (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits Methods withBaseFiniteBits :: (If (IsConMode 'S) (FiniteBits (SymWordN n), FromBits (SymWordN n)) (SymFiniteBits (SymWordN n)) => r) -> r Source #
Lift (SymWordN n :: Type) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods lift :: Quote m => SymWordN n -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => SymWordN n -> Code m (SymWordN n) #
(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymWordN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith Methods safeAdd :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeNeg :: SymWordN n -> m (SymWordN n) Source # safeSub :: SymWordN n -> SymWordN n -> m (SymWordN n) Source #
(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymRotate ArithException (SymWordN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate Methods safeSymRotateL :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeSymRotateR :: SymWordN n -> SymWordN n -> m (SymWordN n) Source #
(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeSymShift ArithException (SymWordN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymShift Methods safeSymShiftL :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeSymShiftR :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeSymStrictShiftL :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeSymStrictShiftR :: SymWordN n -> SymWordN n -> m (SymWordN n) Source #
(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeDiv ArithException (SymWordN n) m Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv Methods safeDiv :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeMod :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeDivMod :: SymWordN n -> SymWordN n -> m (SymWordN n, SymWordN n) Source # safeQuot :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeRem :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeQuotRem :: SymWordN n -> SymWordN n -> m (SymWordN n, SymWordN n) Source #
(KnownNat n', 1 <= n') => UnifiedFromIntegral 'S (SymWordN n') SymAlgReal Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymWordN n'), Num SymAlgReal) (SymFromIntegral (SymWordN n') SymAlgReal) => r) -> r Source #
(KnownNat n', 1 <= n') => UnifiedFromIntegral 'S (SymWordN n') SymInteger Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymWordN n'), Num SymInteger) (SymFromIntegral (SymWordN n') SymInteger) => r) -> r Source #
(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'S (SymIntN n') (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymIntN n'), Num (SymWordN n)) (SymFromIntegral (SymIntN n') (SymWordN n)) => r) -> r Source #
(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'S (SymWordN n') (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymWordN n'), Num (SymIntN n)) (SymFromIntegral (SymWordN n') (SymIntN n)) => r) -> r Source #
(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'S (SymWordN n') (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymWordN n'), Num (SymWordN n)) (SymFromIntegral (SymWordN n') (SymWordN n)) => r) -> r Source #
(KnownNat n, 1 <= n) => UnifiedSolvable 'S (SymWordN n) (WordN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSolvable Methods withBaseSolvable :: (If (IsConMode 'S) (SymWordN n ~ WordN n) (Solvable (WordN n) (SymWordN n)) => r) -> r Source #
(KnownNat n', 1 <= n', ValidFP eb sb) => UnifiedFromIntegral 'S (SymWordN n') (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymWordN n'), Num (SymFP eb sb)) (SymFromIntegral (SymWordN n') (SymFP eb sb)) => r) -> r Source #
(MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (SymWordN n) (SymFP eb sb) SymFPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeFromFP Methods safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m (SymWordN n) Source #
(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeDiv 'S (Either SomeBVException ArithException) SomeSymWordN m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv Methods withBaseSafeDiv :: (SafeDiv (Either SomeBVException ArithException) SomeSymWordN m => r) -> r Source #
(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeLinearArith 'S (Either SomeBVException ArithException) SomeSymWordN m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith Methods withBaseSafeLinearArith :: (SafeLinearArith (Either SomeBVException ArithException) SomeSymWordN m => r) -> r Source #
(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeSymRotate 'S (Either SomeBVException ArithException) SomeSymWordN m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate Methods withBaseSafeSymRotate :: (SafeSymRotate (Either SomeBVException ArithException) SomeSymWordN m => r) -> r Source #
(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeSymShift 'S (Either SomeBVException ArithException) SomeSymWordN m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift Methods withBaseSafeSymShift :: (SafeSymShift (Either SomeBVException ArithException) SomeSymWordN m => r) -> r Source #
(ValidFP eb sb, r ~ (eb + sb), KnownNat r, 1 <= r, MonadUnion m, MonadError NotRepresentableFPError m) => SafeBitCast NotRepresentableFPError (SymFP eb sb) (SymWordN r) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeBitCast Methods safeBitCast :: SymFP eb sb -> m (SymWordN r) Source #
(KnownNat n, 1 <= n) => IsString (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods fromString :: String -> SymWordN n #
(KnownNat n, 1 <= n) => Bits (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods (.&.) :: SymWordN n -> SymWordN n -> SymWordN n # (.\|.) :: SymWordN n -> SymWordN n -> SymWordN n # xor :: SymWordN n -> SymWordN n -> SymWordN n # complement :: SymWordN n -> SymWordN n # shift :: SymWordN n -> Int -> SymWordN n # rotate :: SymWordN n -> Int -> SymWordN n # zeroBits :: SymWordN n # bit :: Int -> SymWordN n # setBit :: SymWordN n -> Int -> SymWordN n # clearBit :: SymWordN n -> Int -> SymWordN n # complementBit :: SymWordN n -> Int -> SymWordN n # testBit :: SymWordN n -> Int -> Bool # bitSizeMaybe :: SymWordN n -> Maybe Int # bitSize :: SymWordN n -> Int # isSigned :: SymWordN n -> Bool # shiftL :: SymWordN n -> Int -> SymWordN n # unsafeShiftL :: SymWordN n -> Int -> SymWordN n # shiftR :: SymWordN n -> Int -> SymWordN n # unsafeShiftR :: SymWordN n -> Int -> SymWordN n # rotateL :: SymWordN n -> Int -> SymWordN n # rotateR :: SymWordN n -> Int -> SymWordN n # popCount :: SymWordN n -> Int #
(KnownNat n, 1 <= n) => FiniteBits (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods finiteBitSize :: SymWordN n -> Int # countLeadingZeros :: SymWordN n -> Int # countTrailingZeros :: SymWordN n -> Int #
Generic (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Associated Types type Rep (SymWordN n) :: Type -> Type # Methods from :: SymWordN n -> Rep (SymWordN n) x # to :: Rep (SymWordN n) x -> SymWordN n #
(KnownNat n, 1 <= n) => Num (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods (+) :: SymWordN n -> SymWordN n -> SymWordN n # (-) :: SymWordN n -> SymWordN n -> SymWordN n # (*) :: SymWordN n -> SymWordN n -> SymWordN n # negate :: SymWordN n -> SymWordN n # abs :: SymWordN n -> SymWordN n # signum :: SymWordN n -> SymWordN n # fromInteger :: Integer -> SymWordN n #
(KnownNat n, 1 <= n) => Show (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods showsPrec :: Int -> SymWordN n -> ShowS # show :: SymWordN n -> String # showList :: [SymWordN n] -> ShowS #
(KnownNat n, 1 <= n) => Binary (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods put :: SymWordN n -> Put # get :: Get (SymWordN n) # putList :: [SymWordN n] -> Put #
(KnownNat n, 1 <= n) => Serial (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods serialize :: MonadPut m => SymWordN n -> m () # deserialize :: MonadGet m => m (SymWordN n) #
(KnownNat n, 1 <= n) => Serialize (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods put :: Putter (SymWordN n) # get :: Get (SymWordN n) #
NFData (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods rnf :: SymWordN n -> () #
(KnownNat n, 1 <= n) => Eq (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods (==) :: SymWordN n -> SymWordN n -> Bool # (/=) :: SymWordN n -> SymWordN n -> Bool #
(KnownNat n, 1 <= n) => Apply (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Associated Types type FunType (SymWordN n) Source # Methods apply :: SymWordN n -> FunType (SymWordN n) Source #
(KnownNat n, 1 <= n) => ITEOp (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ITEOp Methods symIte :: SymBool -> SymWordN n -> SymWordN n -> SymWordN n Source #
SymFiniteBits (SomeBV SymWordN) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods symTestBit :: SomeBV SymWordN -> Int -> SymBool Source # symSetBitTo :: SomeBV SymWordN -> Int -> SymBool -> SomeBV SymWordN Source # symFromBits :: [SymBool] -> SomeBV SymWordN Source #
(KnownNat n, 1 <= n) => SymFiniteBits (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods symTestBit :: SymWordN n -> Int -> SymBool Source # symSetBitTo :: SymWordN n -> Int -> SymBool -> SymWordN n Source # symFromBits :: [SymBool] -> SymWordN n Source #
(KnownNat n, 1 <= n) => SymRotate (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods symRotate :: SymWordN n -> SymWordN n -> SymWordN n Source # symRotateNegated :: SymWordN n -> SymWordN n -> SymWordN n Source #
(KnownNat n, 1 <= n) => SymShift (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods symShift :: SymWordN n -> SymWordN n -> SymWordN n Source # symShiftNegated :: SymWordN n -> SymWordN n -> SymWordN n Source #
(KnownNat n, 1 <= n) => EvalSym (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> SymWordN n -> SymWordN n Source #
(KnownNat n, 1 <= n) => ExtractSym (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ExtractSym Methods extractSym :: SymWordN n -> AnySymbolSet Source # extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => SymWordN n -> Maybe (SymbolSet knd) Source #
(KnownNat n, 1 <= n) => Mergeable (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy (SymWordN n) Source # sortIndices :: SymWordN n -> [DynamicSortedIdx] Source #
(KnownNat n, 1 <= n) => PPrint (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.PPrint Methods pformat :: SymWordN n -> Doc ann Source # pformatPrec :: Int -> SymWordN n -> Doc ann Source # pformatList :: [SymWordN n] -> Doc ann Source #
(KnownNat n, 1 <= n) => DivOr (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv Methods divOr :: SymWordN n -> SymWordN n -> SymWordN n -> SymWordN n Source # modOr :: SymWordN n -> SymWordN n -> SymWordN n -> SymWordN n Source # divModOr :: (SymWordN n, SymWordN n) -> SymWordN n -> SymWordN n -> (SymWordN n, SymWordN n) Source # quotOr :: SymWordN n -> SymWordN n -> SymWordN n -> SymWordN n Source # remOr :: SymWordN n -> SymWordN n -> SymWordN n -> SymWordN n Source # quotRemOr :: (SymWordN n, SymWordN n) -> SymWordN n -> SymWordN n -> (SymWordN n, SymWordN n) Source #
(KnownNat n, 1 <= n) => SimpleMergeable (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> SymWordN n -> SymWordN n -> SymWordN n Source #
(KnownNat n, 1 <= n) => SubstSym (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> SymWordN n -> SymWordN n Source #
(KnownNat n, 1 <= n) => SymEq (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: SymWordN n -> SymWordN n -> SymBool Source # (./=) :: SymWordN n -> SymWordN n -> SymBool Source # symDistinct :: [SymWordN n] -> SymBool Source #
(KnownNat n, 1 <= n) => SymOrd (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd Methods (.<) :: SymWordN n -> SymWordN n -> SymBool Source # (.<=) :: SymWordN n -> SymWordN n -> SymBool Source # (.>) :: SymWordN n -> SymWordN n -> SymBool Source # (.>=) :: SymWordN n -> SymWordN n -> SymBool Source # symCompare :: SymWordN n -> SymWordN n -> Union Ordering Source #
(KnownNat n, 1 <= n) => AllSyms (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods allSymsS :: SymWordN n -> [SomeSym] -> [SomeSym] Source # allSyms :: SymWordN n -> [SomeSym] Source #
(KnownNat n, 1 <= n) => ConRep (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Associated Types type ConType (SymWordN n) Source #
(KnownNat n, 1 <= n) => UnifiedConRep (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedRep Associated Types type ConType (SymWordN n) Source #
(KnownNat n, 1 <= n) => UnifiedSymRep (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedRep Associated Types type SymType (SymWordN n) Source #
(KnownNat n, 1 <= n) => Hashable (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods hashWithSalt :: Int -> SymWordN n -> Int # hash :: SymWordN n -> Int #
BitCast (SymWordN 1) SymBool Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods bitCast :: SymWordN 1 -> SymBool Source #
(KnownNat n, 1 <= n) => SymFromIntegral (SymWordN n) SymAlgReal Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFromIntegral Methods symFromIntegral :: SymWordN n -> SymAlgReal Source #
(KnownNat n, 1 <= n) => SymFromIntegral (SymWordN n) SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFromIntegral Methods symFromIntegral :: SymWordN n -> SymInteger Source #
ToCon (SymWordN 8) Word8 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: SymWordN 8 -> Maybe Word8 Source #
ToCon (SymWordN 16) Word16 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: SymWordN 16 -> Maybe Word16 Source #
ToCon (SymWordN 32) Word32 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: SymWordN 32 -> Maybe Word32 Source #
ToCon (SymWordN 64) Word64 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: SymWordN 64 -> Maybe Word64 Source #
ToCon (SymWordN 64) Word Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: SymWordN 64 -> Maybe Word Source #
(KnownNat n, 1 <= n) => BitCast (SymIntN n) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods bitCast :: SymIntN n -> SymWordN n Source #
(KnownNat n, 1 <= n) => BitCast (SymWordN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods bitCast :: SymWordN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => GenSym (SymWordN n) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => SymWordN n -> m (Union (SymWordN n)) Source #
(KnownNat n, 1 <= n) => GenSymSimple (SymWordN n) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods simpleFresh :: MonadFresh m => SymWordN n -> m (SymWordN n) Source #
(KnownNat n, 1 <= n) => SignConversion (SymWordN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods toSigned :: SymWordN n -> SymIntN n Source # toUnsigned :: SymIntN n -> SymWordN n Source #
(KnownNat n, 1 <= n) => Solvable (WordN n) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods con :: WordN n -> SymWordN n Source # conView :: SymWordN n -> Maybe (WordN n) Source # sym :: Symbol -> SymWordN n Source # ssym :: Identifier -> SymWordN n Source # isym :: Identifier -> Int -> SymWordN n Source #
(KnownNat n, KnownNat m, 1 <= n, 1 <= m) => SymFromIntegral (SymIntN n) (SymWordN m) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFromIntegral Methods symFromIntegral :: SymIntN n -> SymWordN m Source #
(KnownNat n, KnownNat m, 1 <= n, 1 <= m) => SymFromIntegral (SymWordN n) (SymIntN m) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFromIntegral Methods symFromIntegral :: SymWordN n -> SymIntN m Source #
(KnownNat n, KnownNat m, 1 <= n, 1 <= m) => SymFromIntegral (SymWordN n) (SymWordN m) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFromIntegral Methods symFromIntegral :: SymWordN n -> SymWordN m Source #
(KnownNat n, 1 <= n) => ToCon (SymWordN n) (WordN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: SymWordN n -> Maybe (WordN n) Source #
ToCon (SymWordN n) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: SymWordN n -> Maybe (SymWordN n) Source #
(KnownNat n, 1 <= n) => ToSym (Union (WordN n)) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods toSym :: Union (WordN n) -> SymWordN n Source #
(KnownNat n, 1 <= n) => ToSym (WordN n) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: WordN n -> SymWordN n Source #
(KnownNat n, 1 <= n) => ToSym (SymWordN n) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: SymWordN n -> SymWordN n Source #
(KnownNat n, 1 <= n) => LinkedRep (WordN n) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods underlyingTerm :: SymWordN n -> Term (WordN n) Source # wrapTerm :: Term (WordN n) -> SymWordN n Source #
(ValidFP eb sb, r ~ (eb + sb)) => BitCast (SymWordN r) (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods bitCast :: SymWordN r -> SymFP eb sb Source #
(KnownNat n, 1 <= n, ValidFP eb sb) => SymFromIntegral (SymWordN n) (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFromIntegral Methods symFromIntegral :: SymWordN n -> SymFP eb sb Source #
(ValidFP eb sb, KnownNat n, 1 <= n) => IEEEFPConvertible (SymWordN n) (SymFP eb sb) SymFPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods fromFPOr :: SymWordN n -> SymFPRoundingMode -> SymFP eb sb -> SymWordN n Source # toFP :: SymFPRoundingMode -> SymWordN n -> SymFP eb sb Source #
(ValidFP eb sb, r ~ (eb + sb)) => BitCastCanonical (SymFP eb sb) (SymWordN r) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods bitCastCanonicalValue :: proxy (SymFP eb sb) -> SymWordN r Source #
(ValidFP eb sb, r ~ (eb + sb)) => BitCastOr (SymFP eb sb) (SymWordN r) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods bitCastOr :: SymWordN r -> SymFP eb sb -> SymWordN r Source #
type Rep (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV type Rep (SymWordN n) = D1 ('MetaData "SymWordN" "Grisette.Internal.SymPrim.SymBV" "grisette-0.12.0.0-2YnemY67TX446CMac8R8vR" 'True) (C1 ('MetaCons "SymWordN" 'PrefixI 'True) (S1 ('MetaSel ('Just "underlyingWordNTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term (WordN n)))))
type FunType (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV type FunType (SymWordN n) = SymWordN n
type ConType (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV type ConType (SymWordN n) = WordN n
type ConType (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedRep type ConType (SymWordN n) = WordN n
type SymType (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedRep type SymType (SymWordN n) = SymWordN n

type SymWordN8 = SymWordN 8 Source #

Symbolic 8-bit unsigned bit-vector.

type SymWordN16 = SymWordN 16 Source #

Symbolic 16-bit unsigned bit-vector.

type SymWordN32 = SymWordN 32 Source #

Symbolic 32-bit unsigned bit-vector.

type SymWordN64 = SymWordN 64 Source #

Symbolic 64-bit unsigned bit-vector.

newtype SymIntN (n :: Nat) Source #

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

>>> "a" + 5 :: SymIntN 5
(+ 0b00101 a)
>>> sizedBVConcat (con 0b101 :: SymIntN 3) (con 0b110 :: SymIntN 3)
0b101110
>>> sizedBVExt (Proxy @6) (con 0b101 :: SymIntN 3)
0b111101
>>> (8 :: SymIntN 4) .< (7 :: SymIntN 4)
true

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

Constructors

SymIntN (Term (IntN n))

Instances

Instances details

SizedBV SymIntN Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => SymIntN l -> SymIntN r -> SymIntN (l + r) Source # sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymIntN l -> SymIntN r Source # sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymIntN l -> SymIntN r Source # sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymIntN l -> SymIntN r Source # sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> SymIntN n -> SymIntN w Source # sizedBVFromIntegral :: forall a (n :: Nat). (Integral a, KnownNat n, 1 <= n) => a -> SymIntN n Source #
UnifiedFiniteBits 'S SomeSymIntN Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits Methods withBaseFiniteBits :: (If (IsConMode 'S) (FiniteBits SomeSymIntN, FromBits SomeSymIntN) (SymFiniteBits SomeSymIntN) => r) -> r Source #
(KnownNat n, 1 <= n) => UnifiedBVImpl 'S SymWordN SymIntN n (SymWordN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedBV Associated Types type GetWordN 'S = (w :: Nat -> Type) Source # type GetIntN 'S = (i :: Nat -> Type) Source #
(KnownNat n, 1 <= n) => UnifiedFromIntegral 'S SymInteger (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral SymInteger, Num (SymIntN n)) (SymFromIntegral SymInteger (SymIntN n)) => r) -> r Source #
(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeDiv 'S ArithException (SymIntN n) m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv Methods withBaseSafeDiv :: (SafeDiv ArithException (SymIntN n) m => r) -> r Source #
(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeLinearArith 'S ArithException (SymIntN n) m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith Methods withBaseSafeLinearArith :: (SafeLinearArith ArithException (SymIntN n) m => r) -> r Source #
(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeSymRotate 'S ArithException (SymIntN n) m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate Methods withBaseSafeSymRotate :: (SafeSymRotate ArithException (SymIntN n) m => r) -> r Source #
(MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) => UnifiedSafeSymShift 'S ArithException (SymIntN n) m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift Methods withBaseSafeSymShift :: (SafeSymShift ArithException (SymIntN n) m => r) -> r Source #
(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP 'S NotRepresentableFPError (SymIntN n) (SymFP eb sb) SymFPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP Methods withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (SymIntN n) (SymFP eb sb) SymFPRoundingMode m => r) -> r Source #
(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) => UnifiedSafeBitCast 'S NotRepresentableFPError (SymFP eb sb) (SymIntN n) m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeBitCast Methods withBaseSafeBitCast :: (SafeBitCast NotRepresentableFPError (SymFP eb sb) (SymIntN n) m => r) -> r Source #
BitCast SymBool (SymIntN 1) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods bitCast :: SymBool -> SymIntN 1 Source #
(KnownNat n, 1 <= n) => GenSym () (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => () -> m (Union (SymIntN n)) Source #
(KnownNat n, 1 <= n) => GenSymSimple () (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods simpleFresh :: MonadFresh m => () -> m (SymIntN n) Source #
(KnownNat n, 1 <= n) => SymFromIntegral SymInteger (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFromIntegral Methods symFromIntegral :: SymInteger -> SymIntN n Source #
ToSym Int16 (SymIntN 16) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: Int16 -> SymIntN 16 Source #
ToSym Int32 (SymIntN 32) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: Int32 -> SymIntN 32 Source #
ToSym Int64 (SymIntN 64) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: Int64 -> SymIntN 64 Source #
ToSym Int8 (SymIntN 8) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: Int8 -> SymIntN 8 Source #
ToSym Int (SymIntN 64) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: Int -> SymIntN 64 Source #
(KnownNat n, 1 <= n) => UnifiedFiniteBits 'S (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits Methods withBaseFiniteBits :: (If (IsConMode 'S) (FiniteBits (SymIntN n), FromBits (SymIntN n)) (SymFiniteBits (SymIntN n)) => r) -> r Source #
Lift (SymIntN n :: Type) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods lift :: Quote m => SymIntN n -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => SymIntN n -> Code m (SymIntN n) #
(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymIntN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith Methods safeAdd :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeNeg :: SymIntN n -> m (SymIntN n) Source # safeSub :: SymIntN n -> SymIntN n -> m (SymIntN n) Source #
(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeSymRotate ArithException (SymIntN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate Methods safeSymRotateL :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeSymRotateR :: SymIntN n -> SymIntN n -> m (SymIntN n) Source #
(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeSymShift ArithException (SymIntN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymShift Methods safeSymShiftL :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeSymShiftR :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeSymStrictShiftL :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeSymStrictShiftR :: SymIntN n -> SymIntN n -> m (SymIntN n) Source #
(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeDiv ArithException (SymIntN n) m Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv Methods safeDiv :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeMod :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeDivMod :: SymIntN n -> SymIntN n -> m (SymIntN n, SymIntN n) Source # safeQuot :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeRem :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeQuotRem :: SymIntN n -> SymIntN n -> m (SymIntN n, SymIntN n) Source #
(KnownNat n', 1 <= n') => UnifiedFromIntegral 'S (SymIntN n') SymAlgReal Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymIntN n'), Num SymAlgReal) (SymFromIntegral (SymIntN n') SymAlgReal) => r) -> r Source #
(KnownNat n', 1 <= n') => UnifiedFromIntegral 'S (SymIntN n') SymInteger Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymIntN n'), Num SymInteger) (SymFromIntegral (SymIntN n') SymInteger) => r) -> r Source #
(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'S (SymIntN n') (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymIntN n'), Num (SymIntN n)) (SymFromIntegral (SymIntN n') (SymIntN n)) => r) -> r Source #
(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'S (SymIntN n') (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymIntN n'), Num (SymWordN n)) (SymFromIntegral (SymIntN n') (SymWordN n)) => r) -> r Source #
(KnownNat n', 1 <= n', KnownNat n, 1 <= n) => UnifiedFromIntegral 'S (SymWordN n') (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymWordN n'), Num (SymIntN n)) (SymFromIntegral (SymWordN n') (SymIntN n)) => r) -> r Source #
(KnownNat n, 1 <= n) => UnifiedSolvable 'S (SymIntN n) (IntN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSolvable Methods withBaseSolvable :: (If (IsConMode 'S) (SymIntN n ~ IntN n) (Solvable (IntN n) (SymIntN n)) => r) -> r Source #
(KnownNat n', 1 <= n', ValidFP eb sb) => UnifiedFromIntegral 'S (SymIntN n') (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral Methods withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymIntN n'), Num (SymFP eb sb)) (SymFromIntegral (SymIntN n') (SymFP eb sb)) => r) -> r Source #
(MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (SymIntN n) (SymFP eb sb) SymFPRoundingMode m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeFromFP Methods safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m (SymIntN n) Source #
(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeDiv 'S (Either SomeBVException ArithException) SomeSymIntN m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv Methods withBaseSafeDiv :: (SafeDiv (Either SomeBVException ArithException) SomeSymIntN m => r) -> r Source #
(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeLinearArith 'S (Either SomeBVException ArithException) SomeSymIntN m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith Methods withBaseSafeLinearArith :: (SafeLinearArith (Either SomeBVException ArithException) SomeSymIntN m => r) -> r Source #
(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeSymRotate 'S (Either SomeBVException ArithException) SomeSymIntN m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate Methods withBaseSafeSymRotate :: (SafeSymRotate (Either SomeBVException ArithException) SomeSymIntN m => r) -> r Source #
(MonadError (Either SomeBVException ArithException) m, UnifiedBranching 'S m) => UnifiedSafeSymShift 'S (Either SomeBVException ArithException) SomeSymIntN m Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift Methods withBaseSafeSymShift :: (SafeSymShift (Either SomeBVException ArithException) SomeSymIntN m => r) -> r Source #
(ValidFP eb sb, r ~ (eb + sb), KnownNat r, 1 <= r, MonadUnion m, MonadError NotRepresentableFPError m) => SafeBitCast NotRepresentableFPError (SymFP eb sb) (SymIntN r) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeBitCast Methods safeBitCast :: SymFP eb sb -> m (SymIntN r) Source #
(KnownNat n, 1 <= n) => IsString (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods fromString :: String -> SymIntN n #
(KnownNat n, 1 <= n) => Bits (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods (.&.) :: SymIntN n -> SymIntN n -> SymIntN n # (.\|.) :: SymIntN n -> SymIntN n -> SymIntN n # xor :: SymIntN n -> SymIntN n -> SymIntN n # complement :: SymIntN n -> SymIntN n # shift :: SymIntN n -> Int -> SymIntN n # rotate :: SymIntN n -> Int -> SymIntN n # zeroBits :: SymIntN n # bit :: Int -> SymIntN n # setBit :: SymIntN n -> Int -> SymIntN n # clearBit :: SymIntN n -> Int -> SymIntN n # complementBit :: SymIntN n -> Int -> SymIntN n # testBit :: SymIntN n -> Int -> Bool # bitSizeMaybe :: SymIntN n -> Maybe Int # bitSize :: SymIntN n -> Int # isSigned :: SymIntN n -> Bool # shiftL :: SymIntN n -> Int -> SymIntN n # unsafeShiftL :: SymIntN n -> Int -> SymIntN n # shiftR :: SymIntN n -> Int -> SymIntN n # unsafeShiftR :: SymIntN n -> Int -> SymIntN n # rotateL :: SymIntN n -> Int -> SymIntN n # rotateR :: SymIntN n -> Int -> SymIntN n # popCount :: SymIntN n -> Int #
(KnownNat n, 1 <= n) => FiniteBits (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods finiteBitSize :: SymIntN n -> Int # countLeadingZeros :: SymIntN n -> Int # countTrailingZeros :: SymIntN n -> Int #
Generic (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Associated Types type Rep (SymIntN n) :: Type -> Type # Methods from :: SymIntN n -> Rep (SymIntN n) x # to :: Rep (SymIntN n) x -> SymIntN n #
(KnownNat n, 1 <= n) => Num (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods (+) :: SymIntN n -> SymIntN n -> SymIntN n # (-) :: SymIntN n -> SymIntN n -> SymIntN n # (*) :: SymIntN n -> SymIntN n -> SymIntN n # negate :: SymIntN n -> SymIntN n # abs :: SymIntN n -> SymIntN n # signum :: SymIntN n -> SymIntN n # fromInteger :: Integer -> SymIntN n #
(KnownNat n, 1 <= n) => Show (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods showsPrec :: Int -> SymIntN n -> ShowS # show :: SymIntN n -> String # showList :: [SymIntN n] -> ShowS #
(KnownNat n, 1 <= n) => Binary (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods put :: SymIntN n -> Put # get :: Get (SymIntN n) # putList :: [SymIntN n] -> Put #
(KnownNat n, 1 <= n) => Serial (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods serialize :: MonadPut m => SymIntN n -> m () # deserialize :: MonadGet m => m (SymIntN n) #
(KnownNat n, 1 <= n) => Serialize (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods put :: Putter (SymIntN n) # get :: Get (SymIntN n) #
NFData (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods rnf :: SymIntN n -> () #
(KnownNat n, 1 <= n) => Eq (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods (==) :: SymIntN n -> SymIntN n -> Bool # (/=) :: SymIntN n -> SymIntN n -> Bool #
(KnownNat n, 1 <= n) => Apply (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Associated Types type FunType (SymIntN n) Source # Methods apply :: SymIntN n -> FunType (SymIntN n) Source #
(KnownNat n, 1 <= n) => ITEOp (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ITEOp Methods symIte :: SymBool -> SymIntN n -> SymIntN n -> SymIntN n Source #
SymFiniteBits (SomeBV SymIntN) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods symTestBit :: SomeBV SymIntN -> Int -> SymBool Source # symSetBitTo :: SomeBV SymIntN -> Int -> SymBool -> SomeBV SymIntN Source # symFromBits :: [SymBool] -> SomeBV SymIntN Source #
(KnownNat n, 1 <= n) => SymFiniteBits (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFiniteBits Methods symTestBit :: SymIntN n -> Int -> SymBool Source # symSetBitTo :: SymIntN n -> Int -> SymBool -> SymIntN n Source # symFromBits :: [SymBool] -> SymIntN n Source #
(KnownNat n, 1 <= n) => SymRotate (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods symRotate :: SymIntN n -> SymIntN n -> SymIntN n Source # symRotateNegated :: SymIntN n -> SymIntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => SymShift (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods symShift :: SymIntN n -> SymIntN n -> SymIntN n Source # symShiftNegated :: SymIntN n -> SymIntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => EvalSym (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> SymIntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => ExtractSym (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ExtractSym Methods extractSym :: SymIntN n -> AnySymbolSet Source # extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => SymIntN n -> Maybe (SymbolSet knd) Source #
(KnownNat n, 1 <= n) => Mergeable (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy (SymIntN n) Source # sortIndices :: SymIntN n -> [DynamicSortedIdx] Source #
(KnownNat n, 1 <= n) => PPrint (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.PPrint Methods pformat :: SymIntN n -> Doc ann Source # pformatPrec :: Int -> SymIntN n -> Doc ann Source # pformatList :: [SymIntN n] -> Doc ann Source #
(KnownNat n, 1 <= n) => DivOr (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv Methods divOr :: SymIntN n -> SymIntN n -> SymIntN n -> SymIntN n Source # modOr :: SymIntN n -> SymIntN n -> SymIntN n -> SymIntN n Source # divModOr :: (SymIntN n, SymIntN n) -> SymIntN n -> SymIntN n -> (SymIntN n, SymIntN n) Source # quotOr :: SymIntN n -> SymIntN n -> SymIntN n -> SymIntN n Source # remOr :: SymIntN n -> SymIntN n -> SymIntN n -> SymIntN n Source # quotRemOr :: (SymIntN n, SymIntN n) -> SymIntN n -> SymIntN n -> (SymIntN n, SymIntN n) Source #
(KnownNat n, 1 <= n) => SimpleMergeable (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> SymIntN n -> SymIntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => SubstSym (SymIntN 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 -> SymIntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => SymEq (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq Methods (.==) :: SymIntN n -> SymIntN n -> SymBool Source # (./=) :: SymIntN n -> SymIntN n -> SymBool Source # symDistinct :: [SymIntN n] -> SymBool Source #
(KnownNat n, 1 <= n) => SymOrd (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd Methods (.<) :: SymIntN n -> SymIntN n -> SymBool Source # (.<=) :: SymIntN n -> SymIntN n -> SymBool Source # (.>) :: SymIntN n -> SymIntN n -> SymBool Source # (.>=) :: SymIntN n -> SymIntN n -> SymBool Source # symCompare :: SymIntN n -> SymIntN n -> Union Ordering Source #
(KnownNat n, 1 <= n) => AllSyms (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods allSymsS :: SymIntN n -> [SomeSym] -> [SomeSym] Source # allSyms :: SymIntN n -> [SomeSym] Source #
(KnownNat n, 1 <= n) => ConRep (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Associated Types type ConType (SymIntN n) Source #
(KnownNat n, 1 <= n) => UnifiedConRep (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedRep Associated Types type ConType (SymIntN n) Source #
(KnownNat n, 1 <= n) => UnifiedSymRep (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedRep Associated Types type SymType (SymIntN n) Source #
(KnownNat n, 1 <= n) => Hashable (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods hashWithSalt :: Int -> SymIntN n -> Int # hash :: SymIntN n -> Int #
BitCast (SymIntN 1) SymBool Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods bitCast :: SymIntN 1 -> SymBool Source #
(KnownNat n, 1 <= n) => SymFromIntegral (SymIntN n) SymAlgReal Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFromIntegral Methods symFromIntegral :: SymIntN n -> SymAlgReal Source #
(KnownNat n, 1 <= n) => SymFromIntegral (SymIntN n) SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFromIntegral Methods symFromIntegral :: SymIntN n -> SymInteger Source #
ToCon (SymIntN 8) Int8 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: SymIntN 8 -> Maybe Int8 Source #
ToCon (SymIntN 16) Int16 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: SymIntN 16 -> Maybe Int16 Source #
ToCon (SymIntN 32) Int32 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: SymIntN 32 -> Maybe Int32 Source #
ToCon (SymIntN 64) Int64 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: SymIntN 64 -> Maybe Int64 Source #
ToCon (SymIntN 64) Int Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: SymIntN 64 -> Maybe Int Source #
(KnownNat n, 1 <= n) => BitCast (SymIntN n) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods bitCast :: SymIntN n -> SymWordN n Source #
(KnownNat n, 1 <= n) => BitCast (SymWordN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods bitCast :: SymWordN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => GenSym (SymIntN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => SymIntN n -> m (Union (SymIntN n)) Source #
(KnownNat n, 1 <= n) => GenSymSimple (SymIntN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods simpleFresh :: MonadFresh m => SymIntN n -> m (SymIntN n) Source #
(KnownNat n, 1 <= n) => SignConversion (SymWordN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods toSigned :: SymWordN n -> SymIntN n Source # toUnsigned :: SymIntN n -> SymWordN n Source #
(KnownNat n, 1 <= n) => Solvable (IntN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods con :: IntN n -> SymIntN n Source # conView :: SymIntN n -> Maybe (IntN n) Source # sym :: Symbol -> SymIntN n Source # ssym :: Identifier -> SymIntN n Source # isym :: Identifier -> Int -> SymIntN n Source #
(KnownNat n, KnownNat m, 1 <= n, 1 <= m) => SymFromIntegral (SymIntN n) (SymIntN m) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFromIntegral Methods symFromIntegral :: SymIntN n -> SymIntN m Source #
(KnownNat n, KnownNat m, 1 <= n, 1 <= m) => SymFromIntegral (SymIntN n) (SymWordN m) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFromIntegral Methods symFromIntegral :: SymIntN n -> SymWordN m Source #
(KnownNat n, KnownNat m, 1 <= n, 1 <= m) => SymFromIntegral (SymWordN n) (SymIntN m) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFromIntegral Methods symFromIntegral :: SymWordN n -> SymIntN m Source #
(KnownNat n, 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 #
ToCon (SymIntN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: SymIntN n -> Maybe (SymIntN 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) (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) => ToSym (SymIntN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: SymIntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => LinkedRep (IntN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods underlyingTerm :: SymIntN n -> Term (IntN n) Source # wrapTerm :: Term (IntN n) -> SymIntN n Source #
(ValidFP eb sb, r ~ (eb + sb)) => BitCast (SymIntN r) (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods bitCast :: SymIntN r -> SymFP eb sb Source #
(KnownNat n, 1 <= n, ValidFP eb sb) => SymFromIntegral (SymIntN n) (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SymFromIntegral Methods symFromIntegral :: SymIntN n -> SymFP eb sb Source #
(ValidFP eb sb, KnownNat n, 1 <= n) => IEEEFPConvertible (SymIntN n) (SymFP eb sb) SymFPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods fromFPOr :: SymIntN n -> SymFPRoundingMode -> SymFP eb sb -> SymIntN n Source # toFP :: SymFPRoundingMode -> SymIntN n -> SymFP eb sb Source #
(ValidFP eb sb, r ~ (eb + sb)) => BitCastCanonical (SymFP eb sb) (SymIntN r) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods bitCastCanonicalValue :: proxy (SymFP eb sb) -> SymIntN r Source #
(ValidFP eb sb, r ~ (eb + sb)) => BitCastOr (SymFP eb sb) (SymIntN r) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods bitCastOr :: SymIntN r -> SymFP eb sb -> SymIntN r Source #
type Rep (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV type Rep (SymIntN n) = D1 ('MetaData "SymIntN" "Grisette.Internal.SymPrim.SymBV" "grisette-0.12.0.0-2YnemY67TX446CMac8R8vR" 'True) (C1 ('MetaCons "SymIntN" 'PrefixI 'True) (S1 ('MetaSel ('Just "underlyingIntNTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term (IntN n)))))
type FunType (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV type FunType (SymIntN n) = SymIntN n
type ConType (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV type ConType (SymIntN n) = IntN n
type ConType (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedRep type ConType (SymIntN n) = IntN n
type SymType (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedRep type SymType (SymIntN n) = SymIntN n

type SymIntN8 = SymIntN 8 Source #

Symbolic 8-bit signed bit-vector.

type SymIntN16 = SymIntN 16 Source #

Symbolic 16-bit signed bit-vector.

type SymIntN32 = SymIntN 32 Source #

Symbolic 32-bit signed bit-vector.

type SymIntN64 = SymIntN 64 Source #

Symbolic 64-bit signed bit-vector.

Orphan instances

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