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

Grisette.Internal.SymPrim.SymBV

Contents

Orphan instances

Description

Synopsis

newtype SymWordN (n :: Nat) = SymWordN (Term (WordN n))
type SymWordN8 = SymWordN 8
type SymWordN16 = SymWordN 16
type SymWordN32 = SymWordN 32
type SymWordN64 = SymWordN 64
type SymWordNKey (n :: Nat) = AsKey (SymWordN n)
type SymWordN8Key = SymWordNKey 8
type SymWordN16Key = SymWordNKey 16
type SymWordN32Key = SymWordNKey 32
type SymWordN64Key = SymWordNKey 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
type SymIntNKey (n :: Nat) = AsKey (SymIntN n)
type SymIntN8Key = SymIntNKey 8
type SymIntN16Key = SymIntNKey 16
type SymIntN32Key = SymIntNKey 32
type SymIntN64Key = SymIntNKey 64

Documentation

newtype SymWordN (n :: Nat) Source #

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

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

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

Constructors

SymWordN (Term (WordN n))

Instances

Instances details

SizedBV SymWordN Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

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

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

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

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

UnifiedFiniteBits 'S SomeSymWordN Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits

Methods

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

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

Instance details

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

Associated Types

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeBitCast

Methods

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

BitCast SymBool (SymWordN 1) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

bitCast :: SymBool -> SymWordN 1 Source #

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

Instance details

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

Methods

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

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

Instance details

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

Methods

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

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

Instance details

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

Methods

symFromIntegral :: SymInteger -> SymWordN n Source #

ToSym Word16 (SymWordN 16) Source #

Instance details

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

Methods

toSym :: Word16 -> SymWordN 16 Source #

ToSym Word32 (SymWordN 32) Source #

Instance details

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

Methods

toSym :: Word32 -> SymWordN 32 Source #

ToSym Word64 (SymWordN 64) Source #

Instance details

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

Methods

toSym :: Word64 -> SymWordN 64 Source #

ToSym Word8 (SymWordN 8) Source #

Instance details

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

Methods

toSym :: Word8 -> SymWordN 8 Source #

ToSym Word (SymWordN 64) Source #

Instance details

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

Methods

toSym :: Word -> SymWordN 64 Source #

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits

Methods

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

Lift (SymWordN n :: Type) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

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

Instance details

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

Methods

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

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

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

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

Instance details

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

Methods

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

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

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

Instance details

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

Methods

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

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

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

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

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

Instance details

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

Methods

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

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

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

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

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

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSolvable

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

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

Instance details

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

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift

Methods

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

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

Instance details

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

Methods

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

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

put :: SymWordN n -> Put #

get :: Get (SymWordN n) #

putList :: [SymWordN n] -> Put #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

put :: Putter (SymWordN n) #

get :: Get (SymWordN n) #

NFData (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

rnf :: SymWordN n -> () #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

xor :: SymWordN n -> SymWordN n -> SymWordN n #

complement :: SymWordN n -> SymWordN n #

shift :: SymWordN n -> Int -> SymWordN n #

rotate :: SymWordN n -> Int -> SymWordN n #

zeroBits :: SymWordN n #

bit :: Int -> SymWordN n #

setBit :: SymWordN n -> Int -> SymWordN n #

clearBit :: SymWordN n -> Int -> SymWordN n #

complementBit :: SymWordN n -> Int -> SymWordN n #

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

bitSizeMaybe :: SymWordN n -> Maybe Int #

bitSize :: SymWordN n -> Int #

isSigned :: SymWordN n -> Bool #

shiftL :: SymWordN n -> Int -> SymWordN n #

unsafeShiftL :: SymWordN n -> Int -> SymWordN n #

shiftR :: SymWordN n -> Int -> SymWordN n #

unsafeShiftR :: SymWordN n -> Int -> SymWordN n #

rotateL :: SymWordN n -> Int -> SymWordN n #

rotateR :: SymWordN n -> Int -> SymWordN n #

popCount :: SymWordN n -> Int #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

finiteBitSize :: SymWordN n -> Int #

countLeadingZeros :: SymWordN n -> Int #

countTrailingZeros :: SymWordN n -> Int #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

fromString :: String -> SymWordN n #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

succ :: SymWordN n -> SymWordN n #

pred :: SymWordN n -> SymWordN n #

toEnum :: Int -> SymWordN n #

fromEnum :: SymWordN n -> Int #

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

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

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

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

Generic (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

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

Methods

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

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

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

(-) :: SymWordN n -> SymWordN n -> SymWordN n #

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

negate :: SymWordN n -> SymWordN n #

abs :: SymWordN n -> SymWordN n #

signum :: SymWordN n -> SymWordN n #

fromInteger :: Integer -> SymWordN n #

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

The functions are total and will not throw errors. The result is considered undefined if the divisor is 0.

It is the responsibility of the caller to ensure that the divisor is not zero with the symbolic constraints, or use the DivOr or SafeDiv classes.

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

quot :: SymWordN n -> SymWordN n -> SymWordN n #

rem :: SymWordN n -> SymWordN n -> SymWordN n #

div :: SymWordN n -> SymWordN n -> SymWordN n #

mod :: SymWordN n -> SymWordN n -> SymWordN n #

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

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

toInteger :: SymWordN n -> Integer #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

toRational :: SymWordN n -> Rational #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

show :: SymWordN n -> String #

showList :: [SymWordN n] -> ShowS #

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

This will crash the program.

SymWordN cannot be compared concretely.

If you want to use the type as keys in hash maps based on term equality, say memo table, you should use AsKey (SymWordN n) instead.

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

compare :: SymWordN n -> SymWordN n -> Ordering #

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

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

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

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

max :: SymWordN n -> SymWordN n -> SymWordN n #

min :: SymWordN n -> SymWordN n -> SymWordN n #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

keyEq :: SymWordN n -> SymWordN n -> Bool Source #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

keyHashWithSalt :: Int -> SymWordN n -> Int Source #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

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

Methods

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

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

Instance details

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

Methods

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

SymFiniteBits (SomeBV SymWordN) Source #

Instance details

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

Methods

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

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

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

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

Instance details

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

Methods

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

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

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

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

symRotate :: SymWordN n -> SymWordN n -> SymWordN n Source #

symRotateNegated :: SymWordN n -> SymWordN n -> SymWordN n Source #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

symShift :: SymWordN n -> SymWordN n -> SymWordN n Source #

symShiftNegated :: SymWordN n -> SymWordN n -> SymWordN n Source #

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

Instance details

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

Methods

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

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

Instance details

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

Methods

extractSym :: SymWordN n -> AnySymbolSet Source #

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

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

Instance details

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

Methods

rootStrategy :: MergingStrategy (SymWordN n) Source #

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

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

Instance details

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

Methods

pformat :: SymWordN n -> Doc ann Source #

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

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

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

Instance details

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

Methods

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

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

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

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

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

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

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

Instance details

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

Methods

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

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

Instance details

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

Methods

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

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

Instance details

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

Methods

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

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

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

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

Instance details

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

Methods

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

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

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

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

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

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

Associated Types

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

Associated Types

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

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-2G8wsM3ZzbCKYYnSn6PeBx" '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.

type SymWordNKey (n :: Nat) = AsKey (SymWordN n) Source #

SymWordN type with identity equality.

type SymWordN8Key = SymWordNKey 8 Source #

SymWordN 8@ type with identity equality.

type SymWordN16Key = SymWordNKey 16 Source #

SymWordN 16@ type with identity equality.

type SymWordN32Key = SymWordNKey 32 Source #

SymWordN 32@ type with identity equality.

type SymWordN64Key = SymWordNKey 64 Source #

SymWordN 64@ type with identity equality.

newtype SymIntN (n :: Nat) Source #

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

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

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

Constructors

SymIntN (Term (IntN n))

Instances

Instances details

SizedBV SymIntN Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

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

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

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

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

UnifiedFiniteBits 'S SomeSymIntN Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits

Methods

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

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

Instance details

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

Associated Types

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeBitCast

Methods

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

BitCast SymBool (SymIntN 1) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

bitCast :: SymBool -> SymIntN 1 Source #

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

Instance details

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

Methods

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

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

Instance details

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

Methods

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

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

Instance details

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

Methods

symFromIntegral :: SymInteger -> SymIntN n Source #

ToSym Int16 (SymIntN 16) Source #

Instance details

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

Methods

toSym :: Int16 -> SymIntN 16 Source #

ToSym Int32 (SymIntN 32) Source #

Instance details

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

Methods

toSym :: Int32 -> SymIntN 32 Source #

ToSym Int64 (SymIntN 64) Source #

Instance details

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

Methods

toSym :: Int64 -> SymIntN 64 Source #

ToSym Int8 (SymIntN 8) Source #

Instance details

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

Methods

toSym :: Int8 -> SymIntN 8 Source #

ToSym Int (SymIntN 64) Source #

Instance details

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

Methods

toSym :: Int -> SymIntN 64 Source #

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits

Methods

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

Lift (SymIntN n :: Type) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

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

Instance details

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

Methods

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

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

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

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

Instance details

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

Methods

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

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

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

Instance details

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

Methods

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

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

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

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

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

Instance details

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

Methods

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

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

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

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

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

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSolvable

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

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

Instance details

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

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymRotate

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeSymShift

Methods

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

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

Instance details

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

Methods

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

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

put :: SymIntN n -> Put #

get :: Get (SymIntN n) #

putList :: [SymIntN n] -> Put #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

put :: Putter (SymIntN n) #

get :: Get (SymIntN n) #

NFData (SymIntN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

rnf :: SymIntN n -> () #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

xor :: SymIntN n -> SymIntN n -> SymIntN n #

complement :: SymIntN n -> SymIntN n #

shift :: SymIntN n -> Int -> SymIntN n #

rotate :: SymIntN n -> Int -> SymIntN n #

zeroBits :: SymIntN n #

bit :: Int -> SymIntN n #

setBit :: SymIntN n -> Int -> SymIntN n #

clearBit :: SymIntN n -> Int -> SymIntN n #

complementBit :: SymIntN n -> Int -> SymIntN n #

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

bitSizeMaybe :: SymIntN n -> Maybe Int #

bitSize :: SymIntN n -> Int #

isSigned :: SymIntN n -> Bool #

shiftL :: SymIntN n -> Int -> SymIntN n #

unsafeShiftL :: SymIntN n -> Int -> SymIntN n #

shiftR :: SymIntN n -> Int -> SymIntN n #

unsafeShiftR :: SymIntN n -> Int -> SymIntN n #

rotateL :: SymIntN n -> Int -> SymIntN n #

rotateR :: SymIntN n -> Int -> SymIntN n #

popCount :: SymIntN n -> Int #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

finiteBitSize :: SymIntN n -> Int #

countLeadingZeros :: SymIntN n -> Int #

countTrailingZeros :: SymIntN n -> Int #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

fromString :: String -> SymIntN n #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

minBound :: SymIntN n #

maxBound :: SymIntN n #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

succ :: SymIntN n -> SymIntN n #

pred :: SymIntN n -> SymIntN n #

toEnum :: Int -> SymIntN n #

fromEnum :: SymIntN n -> Int #

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

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

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

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

Generic (SymIntN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

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

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) => Integral (SymIntN n) Source #

The functions are total and will not throw errors. The result is considered undefined if the divisor is 0.

It is the responsibility of the caller to ensure that the divisor is not zero with the symbolic constraints, or use the DivOr or SafeDiv classes.

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

quot :: SymIntN n -> SymIntN n -> SymIntN n #

rem :: SymIntN n -> SymIntN n -> SymIntN n #

div :: SymIntN n -> SymIntN n -> SymIntN n #

mod :: SymIntN n -> SymIntN n -> SymIntN n #

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

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

toInteger :: SymIntN n -> Integer #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

toRational :: SymIntN n -> Rational #

(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) => 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) => Ord (SymIntN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

compare :: SymIntN n -> SymIntN n -> Ordering #

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

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

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

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

max :: SymIntN n -> SymIntN n -> SymIntN n #

min :: SymIntN n -> SymIntN n -> SymIntN n #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

keyEq :: SymIntN n -> SymIntN n -> Bool Source #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

keyHashWithSalt :: Int -> SymIntN n -> Int Source #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

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

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)
Instance details Defined in Grisette.Internal.SymPrim.SymBV type ConType (SymIntN n) = IntN n

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

Associated Types

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

Associated Types

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

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-2G8wsM3ZzbCKYYnSn6PeBx" '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.

type SymIntNKey (n :: Nat) = AsKey (SymIntN n) Source #

SymIntN type with identity equality.

type SymIntN8Key = SymIntNKey 8 Source #

SymIntN 8 type with identity equality.

type SymIntN16Key = SymIntNKey 16 Source #

SymIntN 16 type with identity equality.

type SymIntN32Key = SymIntNKey 32 Source #

SymIntN 32 type with identity equality.

type SymIntN64Key = SymIntNKey 64 Source #

SymIntN 64 type with identity equality.

Orphan instances

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

Instance details

Associated Types

type SymType (IntN n)
Instance details Defined in Grisette.Internal.SymPrim.SymBV type SymType (IntN n) = SymIntN n

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

Instance details

Associated Types

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

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