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.Core.Data.BV

Description

Synopsis

data BitwidthMismatch = BitwidthMismatch
newtype IntN (n :: Nat) = IntN {
- unIntN :: Integer
}
newtype WordN (n :: Nat) = WordN {
- unWordN :: Integer
}
data SomeIntN where
- SomeIntN :: (KnownNat n, 1 <= n) => IntN n -> SomeIntN
data SomeWordN where
- SomeWordN :: (KnownNat n, 1 <= n) => WordN n -> SomeWordN
unarySomeIntN :: (forall n. (KnownNat n, 1 <= n) => IntN n -> r) -> SomeIntN -> r
unarySomeIntNR1 :: (forall n. (KnownNat n, 1 <= n) => IntN n -> IntN n) -> SomeIntN -> SomeIntN
binSomeIntN :: (forall n. (KnownNat n, 1 <= n) => IntN n -> IntN n -> r) -> SomeIntN -> SomeIntN -> r
binSomeIntNR1 :: (forall n. (KnownNat n, 1 <= n) => IntN n -> IntN n -> IntN n) -> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR2 :: (forall n. (KnownNat n, 1 <= n) => IntN n -> IntN n -> (IntN n, IntN n)) -> SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN)
unarySomeWordN :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> r) -> SomeWordN -> r
unarySomeWordNR1 :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n) -> SomeWordN -> SomeWordN
binSomeWordN :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> r) -> SomeWordN -> SomeWordN -> r
binSomeWordNR1 :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> WordN n) -> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR2 :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> (WordN n, WordN n)) -> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)

Documentation

data BitwidthMismatch Source #

Constructors

BitwidthMismatch

Instances

Instances details

Exception BitwidthMismatch Source #
Instance details Defined in Grisette.Core.Data.BV Methods toException :: BitwidthMismatch -> SomeException # fromException :: SomeException -> Maybe BitwidthMismatch # displayException :: BitwidthMismatch -> String #
Generic BitwidthMismatch Source #
Instance details Defined in Grisette.Core.Data.BV Associated Types type Rep BitwidthMismatch :: Type -> Type # Methods from :: BitwidthMismatch -> Rep BitwidthMismatch x # to :: Rep BitwidthMismatch x -> BitwidthMismatch #
Show BitwidthMismatch Source #
Instance details Defined in Grisette.Core.Data.BV Methods showsPrec :: Int -> BitwidthMismatch -> ShowS # show :: BitwidthMismatch -> String # showList :: [BitwidthMismatch] -> ShowS #
Eq BitwidthMismatch Source #
Instance details Defined in Grisette.Core.Data.BV Methods (==) :: BitwidthMismatch -> BitwidthMismatch -> Bool # (/=) :: BitwidthMismatch -> BitwidthMismatch -> Bool #
Ord BitwidthMismatch Source #
Instance details Defined in Grisette.Core.Data.BV Methods compare :: BitwidthMismatch -> BitwidthMismatch -> Ordering # (<) :: BitwidthMismatch -> BitwidthMismatch -> Bool # (<=) :: BitwidthMismatch -> BitwidthMismatch -> Bool # (>) :: BitwidthMismatch -> BitwidthMismatch -> Bool # (>=) :: BitwidthMismatch -> BitwidthMismatch -> Bool # max :: BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch # min :: BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch #
Mergeable BitwidthMismatch Source #
Instance details Defined in Grisette.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy BitwidthMismatch Source #
SafeDivision (Either BitwidthMismatch ArithException) SomeIntN Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source # safeMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source # safeDivMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source # safeQuot :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source # safeRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source # safeQuotRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source #
SafeDivision (Either BitwidthMismatch ArithException) SomeWordN Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source # safeMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source # safeDivMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source # safeQuot :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source # safeRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source # safeQuotRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source #
SafeLinearArith (Either BitwidthMismatch ArithException) SomeIntN Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source # safeNeg :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> uf SomeIntN Source # safeMinus :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> uf SomeIntN Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source #
SafeLinearArith (Either BitwidthMismatch ArithException) SomeWordN Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source # safeNeg :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> uf SomeWordN Source # safeMinus :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> uf SomeWordN Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source #
type Rep BitwidthMismatch Source #
Instance details Defined in Grisette.Core.Data.BV type Rep BitwidthMismatch = D1 ('MetaData "BitwidthMismatch" "Grisette.Core.Data.BV" "grisette-0.3.0.0-D2Nbhnc0iuRKig0VAC9Xli" 'False) (C1 ('MetaCons "BitwidthMismatch" 'PrefixI 'False) (U1 :: Type -> Type))

newtype IntN (n :: Nat) Source #

Symbolic signed bit vectors.

Constructors

IntN
Fields unIntN :: Integer

Instances

Instances details

SizedBV IntN Source #
Instance details Defined in Grisette.Core.Data.BV Methods sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => IntN l -> IntN r -> IntN (l + r) Source # sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r Source # sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r Source # sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r Source # sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> IntN n -> IntN w Source #
(KnownNat n, 1 <= n) => SafeDivision ArithException (IntN n) Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n, IntN n) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n, IntN n) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n, IntN n) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n, IntN n) Source #
(KnownNat n, 1 <= n) => SafeLinearArith ArithException (IntN n) Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> uf (IntN n) Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> uf (IntN n) Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source #
(KnownNat n, 1 <= n) => Bits (IntN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods (.&.) :: IntN n -> IntN n -> IntN n # (.\|.) :: IntN n -> IntN n -> IntN n # xor :: IntN n -> IntN n -> IntN n # complement :: IntN n -> IntN n # shift :: IntN n -> Int -> IntN n # rotate :: IntN n -> Int -> IntN n # zeroBits :: IntN n # bit :: Int -> IntN n # setBit :: IntN n -> Int -> IntN n # clearBit :: IntN n -> Int -> IntN n # complementBit :: IntN n -> Int -> IntN n # testBit :: IntN n -> Int -> Bool # bitSizeMaybe :: IntN n -> Maybe Int # bitSize :: IntN n -> Int # isSigned :: IntN n -> Bool # shiftL :: IntN n -> Int -> IntN n # unsafeShiftL :: IntN n -> Int -> IntN n # shiftR :: IntN n -> Int -> IntN n # unsafeShiftR :: IntN n -> Int -> IntN n # rotateL :: IntN n -> Int -> IntN n # rotateR :: IntN n -> Int -> IntN n # popCount :: IntN n -> Int #
(KnownNat n, 1 <= n) => FiniteBits (IntN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods finiteBitSize :: IntN n -> Int # countLeadingZeros :: IntN n -> Int # countTrailingZeros :: IntN n -> Int #
(KnownNat n, 1 <= n) => Bounded (IntN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods minBound :: IntN n # maxBound :: IntN n #
(KnownNat n, 1 <= n) => Enum (IntN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods succ :: IntN n -> IntN n # pred :: IntN n -> IntN n # toEnum :: Int -> IntN n # fromEnum :: IntN n -> Int # enumFrom :: IntN n -> [IntN n] # enumFromThen :: IntN n -> IntN n -> [IntN n] # enumFromTo :: IntN n -> IntN n -> [IntN n] # enumFromThenTo :: IntN n -> IntN n -> IntN n -> [IntN n] #
Generic (IntN n) Source #
Instance details Defined in Grisette.Core.Data.BV Associated Types type Rep (IntN n) :: Type -> Type # Methods from :: IntN n -> Rep (IntN n) x # to :: Rep (IntN n) x -> IntN n #
(KnownNat n, 1 <= n) => Num (IntN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods (+) :: IntN n -> IntN n -> IntN n # (-) :: IntN n -> IntN n -> IntN n # (*) :: IntN n -> IntN n -> IntN n # negate :: IntN n -> IntN n # abs :: IntN n -> IntN n # signum :: IntN n -> IntN n # fromInteger :: Integer -> IntN n #
(KnownNat n, 1 <= n) => Read (IntN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods readsPrec :: Int -> ReadS (IntN n) # readList :: ReadS [IntN n] # readPrec :: ReadPrec (IntN n) # readListPrec :: ReadPrec [IntN n] #
(KnownNat n, 1 <= n) => Integral (IntN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods quot :: IntN n -> IntN n -> IntN n # rem :: IntN n -> IntN n -> IntN n # div :: IntN n -> IntN n -> IntN n # mod :: IntN n -> IntN n -> IntN n # quotRem :: IntN n -> IntN n -> (IntN n, IntN n) # divMod :: IntN n -> IntN n -> (IntN n, IntN n) # toInteger :: IntN n -> Integer #
(KnownNat n, 1 <= n) => Real (IntN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods toRational :: IntN n -> Rational #
(KnownNat n, 1 <= n) => Show (IntN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods showsPrec :: Int -> IntN n -> ShowS # show :: IntN n -> String # showList :: [IntN n] -> ShowS #
NFData (IntN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods rnf :: IntN n -> () #
Eq (IntN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods (==) :: IntN n -> IntN n -> Bool # (/=) :: IntN n -> IntN n -> Bool #
(KnownNat n, 1 <= n) => Ord (IntN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods compare :: IntN n -> IntN n -> Ordering # (<) :: IntN n -> IntN n -> Bool # (<=) :: IntN n -> IntN n -> Bool # (>) :: IntN n -> IntN n -> Bool # (>=) :: IntN n -> IntN n -> Bool # max :: IntN n -> IntN n -> IntN n # min :: IntN n -> IntN n -> IntN n #
(KnownNat n, 1 <= n) => SEq (IntN n) Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~) :: IntN n -> IntN n -> SymBool Source # (/=~) :: IntN n -> IntN n -> SymBool Source #
(KnownNat n, 1 <= n) => EvaluateSym (IntN n) Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> IntN n -> IntN n Source #
(KnownNat n, 1 <= n) => ExtractSymbolics (IntN n) Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: IntN n -> SymbolSet Source #
(KnownNat n, 1 <= n) => Mergeable (IntN n) Source #
Instance details Defined in Grisette.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy (IntN n) Source #
(KnownNat n, 1 <= n) => SOrd (IntN n) Source #
Instance details Defined in Grisette.Core.Data.Class.SOrd Methods (<~) :: IntN n -> IntN n -> SymBool Source # (<=~) :: IntN n -> IntN n -> SymBool Source # (>~) :: IntN n -> IntN n -> SymBool Source # (>=~) :: IntN n -> IntN n -> SymBool Source # symCompare :: IntN n -> IntN n -> UnionM Ordering Source #
(KnownNat n, 1 <= n) => SubstituteSym (IntN n) Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> IntN n -> IntN n Source #
(KnownNat w, 1 <= w) => SupportedPrim (IntN w) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term Associated Types type PrimConstraint (IntN w) Source # Methods withPrim :: proxy (IntN w) -> (PrimConstraint (IntN w) => a) -> a Source # termCache :: Cache (Term (IntN w)) Source # pformatCon :: IntN w -> String Source # pformatSym :: TypedSymbol (IntN w) -> String Source # defaultValue :: IntN w Source # defaultValueDynamic :: proxy (IntN w) -> ModelValue Source #
(KnownNat n, 1 <= n) => SymRep (IntN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Associated Types type SymType (IntN n) Source #
Hashable (IntN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods hashWithSalt :: Int -> IntN n -> Int # hash :: IntN n -> Int #
(KnownNat n, 1 <= n) => ToSym (IntN n) SomeSymIntN Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods toSym :: IntN n -> SomeSymIntN Source #
(KnownNat n, 1 <= n) => BVSignConversion (WordN n) (IntN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods toSigned :: WordN n -> IntN n Source # toUnsigned :: IntN n -> WordN n Source #
(KnownNat n, 1 <= n) => GenSym (IntN n) (IntN n) Source #
Instance details Defined in Grisette.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => IntN n -> m (UnionM (IntN n)) Source #
(KnownNat n, 1 <= n) => GenSymSimple (IntN n) (IntN n) Source #
Instance details Defined in Grisette.Core.Data.Class.GenSym Methods simpleFresh :: MonadFresh m => IntN n -> m (IntN n) Source #
(KnownNat n, 1 <= n) => Solvable (IntN n) (SymIntN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods con :: IntN n -> SymIntN n Source # conView :: SymIntN n -> Maybe (IntN n) Source # ssym :: String -> SymIntN n Source # isym :: String -> Int -> SymIntN n Source # sinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> SymIntN n Source # iinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> Int -> a -> SymIntN n Source #
(KnownNat n, 1 <= n) => ToCon (IntN n) (IntN n) Source #
Instance details Defined in Grisette.Core.Data.Class.ToCon Methods toCon :: IntN n -> Maybe (IntN n) Source #
(KnownNat n, 1 <= n) => ToCon (SymIntN n) (IntN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods toCon :: SymIntN n -> Maybe (IntN n) Source #
(KnownNat n, 1 <= n) => ToSym (UnionM (IntN n)) (SymIntN n) Source #
Instance details Defined in Grisette.Core.Control.Monad.UnionM Methods toSym :: UnionM (IntN n) -> SymIntN n Source #
(KnownNat n, 1 <= n) => ToSym (IntN n) (IntN n) Source #
Instance details Defined in Grisette.Core.Data.Class.ToSym Methods toSym :: IntN n -> IntN n Source #
(KnownNat n, 1 <= n) => ToSym (IntN n) (SymIntN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods toSym :: IntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => LinkedRep (IntN n) (SymIntN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods underlyingTerm :: SymIntN n -> Term (IntN n) Source # wrapTerm :: Term (IntN n) -> SymIntN n Source #
Lift (IntN n :: TYPE LiftedRep) Source #
Instance details Defined in Grisette.Core.Data.BV Methods lift :: Quote m => IntN n -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => IntN n -> Code m (IntN n) #
type Rep (IntN n) Source #
Instance details Defined in Grisette.Core.Data.BV type Rep (IntN n) = D1 ('MetaData "IntN" "Grisette.Core.Data.BV" "grisette-0.3.0.0-D2Nbhnc0iuRKig0VAC9Xli" 'True) (C1 ('MetaCons "IntN" 'PrefixI 'True) (S1 ('MetaSel ('Just "unIntN") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))
type PrimConstraint (IntN w) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term type PrimConstraint (IntN w) = (KnownNat w, 1 <= w)
type SymType (IntN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim type SymType (IntN n) = SymIntN n

newtype WordN (n :: Nat) Source #

Symbolic unsigned bit vectors.

Constructors

WordN
Fields unWordN :: Integer

Instances

Instances details

SizedBV WordN Source #
Instance details Defined in Grisette.Core.Data.BV Methods sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => WordN l -> WordN r -> WordN (l + r) Source # sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r Source # sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r Source # sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r Source # sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> WordN n -> WordN w Source #
(KnownNat n, 1 <= n) => SafeDivision ArithException (WordN n) Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source # safeMod :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source # safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n, WordN n) Source # safeQuot :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source # safeRem :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source # safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n, WordN n) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n, WordN n) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n, WordN n) Source #
(KnownNat n, 1 <= n) => SafeLinearArith ArithException (WordN n) Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source # safeNeg :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> uf (WordN n) Source # safeMinus :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> uf (WordN n) Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source #
(KnownNat n, 1 <= n) => Bits (WordN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods (.&.) :: WordN n -> WordN n -> WordN n # (.\|.) :: WordN n -> WordN n -> WordN n # xor :: WordN n -> WordN n -> WordN n # complement :: WordN n -> WordN n # shift :: WordN n -> Int -> WordN n # rotate :: WordN n -> Int -> WordN n # zeroBits :: WordN n # bit :: Int -> WordN n # setBit :: WordN n -> Int -> WordN n # clearBit :: WordN n -> Int -> WordN n # complementBit :: WordN n -> Int -> WordN n # testBit :: WordN n -> Int -> Bool # bitSizeMaybe :: WordN n -> Maybe Int # bitSize :: WordN n -> Int # isSigned :: WordN n -> Bool # shiftL :: WordN n -> Int -> WordN n # unsafeShiftL :: WordN n -> Int -> WordN n # shiftR :: WordN n -> Int -> WordN n # unsafeShiftR :: WordN n -> Int -> WordN n # rotateL :: WordN n -> Int -> WordN n # rotateR :: WordN n -> Int -> WordN n # popCount :: WordN n -> Int #
(KnownNat n, 1 <= n) => FiniteBits (WordN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods finiteBitSize :: WordN n -> Int # countLeadingZeros :: WordN n -> Int # countTrailingZeros :: WordN n -> Int #
(KnownNat n, 1 <= n) => Bounded (WordN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods minBound :: WordN n # maxBound :: WordN n #
(KnownNat n, 1 <= n) => Enum (WordN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods succ :: WordN n -> WordN n # pred :: WordN n -> WordN n # toEnum :: Int -> WordN n # fromEnum :: WordN n -> Int # enumFrom :: WordN n -> [WordN n] # enumFromThen :: WordN n -> WordN n -> [WordN n] # enumFromTo :: WordN n -> WordN n -> [WordN n] # enumFromThenTo :: WordN n -> WordN n -> WordN n -> [WordN n] #
Generic (WordN n) Source #
Instance details Defined in Grisette.Core.Data.BV Associated Types type Rep (WordN n) :: Type -> Type # Methods from :: WordN n -> Rep (WordN n) x # to :: Rep (WordN n) x -> WordN n #
(KnownNat n, 1 <= n) => Num (WordN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods (+) :: WordN n -> WordN n -> WordN n # (-) :: WordN n -> WordN n -> WordN n # (*) :: WordN n -> WordN n -> WordN n # negate :: WordN n -> WordN n # abs :: WordN n -> WordN n # signum :: WordN n -> WordN n # fromInteger :: Integer -> WordN n #
(KnownNat n, 1 <= n) => Read (WordN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods readsPrec :: Int -> ReadS (WordN n) # readList :: ReadS [WordN n] # readPrec :: ReadPrec (WordN n) # readListPrec :: ReadPrec [WordN n] #
(KnownNat n, 1 <= n) => Integral (WordN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods quot :: WordN n -> WordN n -> WordN n # rem :: WordN n -> WordN n -> WordN n # div :: WordN n -> WordN n -> WordN n # mod :: WordN n -> WordN n -> WordN n # quotRem :: WordN n -> WordN n -> (WordN n, WordN n) # divMod :: WordN n -> WordN n -> (WordN n, WordN n) # toInteger :: WordN n -> Integer #
(KnownNat n, 1 <= n) => Real (WordN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods toRational :: WordN n -> Rational #
(KnownNat n, 1 <= n) => Show (WordN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods showsPrec :: Int -> WordN n -> ShowS # show :: WordN n -> String # showList :: [WordN n] -> ShowS #
NFData (WordN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods rnf :: WordN n -> () #
Eq (WordN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods (==) :: WordN n -> WordN n -> Bool # (/=) :: WordN n -> WordN n -> Bool #
Ord (WordN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods compare :: WordN n -> WordN n -> Ordering # (<) :: WordN n -> WordN n -> Bool # (<=) :: WordN n -> WordN n -> Bool # (>) :: WordN n -> WordN n -> Bool # (>=) :: WordN n -> WordN n -> Bool # max :: WordN n -> WordN n -> WordN n # min :: WordN n -> WordN n -> WordN n #
(KnownNat n, 1 <= n) => SEq (WordN n) Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~) :: WordN n -> WordN n -> SymBool Source # (/=~) :: WordN n -> WordN n -> SymBool Source #
(KnownNat n, 1 <= n) => EvaluateSym (WordN n) Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> WordN n -> WordN n Source #
(KnownNat n, 1 <= n) => ExtractSymbolics (WordN n) Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: WordN n -> SymbolSet Source #
(KnownNat n, 1 <= n) => Mergeable (WordN n) Source #
Instance details Defined in Grisette.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy (WordN n) Source #
(KnownNat n, 1 <= n) => SOrd (WordN n) Source #
Instance details Defined in Grisette.Core.Data.Class.SOrd Methods (<~) :: WordN n -> WordN n -> SymBool Source # (<=~) :: WordN n -> WordN n -> SymBool Source # (>~) :: WordN n -> WordN n -> SymBool Source # (>=~) :: WordN n -> WordN n -> SymBool Source # symCompare :: WordN n -> WordN n -> UnionM Ordering Source #
(KnownNat n, 1 <= n) => SubstituteSym (WordN n) Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> WordN n -> WordN n Source #
(KnownNat w, 1 <= w) => SupportedPrim (WordN w) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term Associated Types type PrimConstraint (WordN w) Source # Methods withPrim :: proxy (WordN w) -> (PrimConstraint (WordN w) => a) -> a Source # termCache :: Cache (Term (WordN w)) Source # pformatCon :: WordN w -> String Source # pformatSym :: TypedSymbol (WordN w) -> String Source # defaultValue :: WordN w Source # defaultValueDynamic :: proxy (WordN w) -> ModelValue Source #
(KnownNat n, 1 <= n) => SymRep (WordN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Associated Types type SymType (WordN n) Source #
Hashable (WordN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods hashWithSalt :: Int -> WordN n -> Int # hash :: WordN n -> Int #
(KnownNat n, 1 <= n) => ToSym (WordN n) SomeSymWordN Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods toSym :: WordN n -> SomeSymWordN Source #
(KnownNat n, 1 <= n) => BVSignConversion (WordN n) (IntN n) Source #
Instance details Defined in Grisette.Core.Data.BV Methods toSigned :: WordN n -> IntN n Source # toUnsigned :: IntN n -> WordN n Source #
(KnownNat n, 1 <= n) => GenSym (WordN n) (WordN n) Source #
Instance details Defined in Grisette.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => WordN n -> m (UnionM (WordN n)) Source #
(KnownNat n, 1 <= n) => GenSymSimple (WordN n) (WordN n) Source #
Instance details Defined in Grisette.Core.Data.Class.GenSym Methods simpleFresh :: MonadFresh m => WordN n -> m (WordN n) Source #
(KnownNat n, 1 <= n) => Solvable (WordN n) (SymWordN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods con :: WordN n -> SymWordN n Source # conView :: SymWordN n -> Maybe (WordN n) Source # ssym :: String -> SymWordN n Source # isym :: String -> Int -> SymWordN n Source # sinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> SymWordN n Source # iinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> Int -> a -> SymWordN n Source #
(KnownNat n, 1 <= n) => ToCon (WordN n) (WordN n) Source #
Instance details Defined in Grisette.Core.Data.Class.ToCon Methods toCon :: WordN n -> Maybe (WordN n) Source #
(KnownNat n, 1 <= n) => ToCon (SymWordN n) (WordN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods toCon :: SymWordN n -> Maybe (WordN n) Source #
(KnownNat n, 1 <= n) => ToSym (UnionM (WordN n)) (SymWordN n) Source #
Instance details Defined in Grisette.Core.Control.Monad.UnionM Methods toSym :: UnionM (WordN n) -> SymWordN n Source #
(KnownNat n, 1 <= n) => ToSym (WordN n) (WordN n) Source #
Instance details Defined in Grisette.Core.Data.Class.ToSym Methods toSym :: WordN n -> WordN n Source #
(KnownNat n, 1 <= n) => ToSym (WordN n) (SymWordN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods toSym :: WordN n -> SymWordN n Source #
(KnownNat n, 1 <= n) => LinkedRep (WordN n) (SymWordN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods underlyingTerm :: SymWordN n -> Term (WordN n) Source # wrapTerm :: Term (WordN n) -> SymWordN n Source #
Lift (WordN n :: TYPE LiftedRep) Source #
Instance details Defined in Grisette.Core.Data.BV Methods lift :: Quote m => WordN n -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => WordN n -> Code m (WordN n) #
type Rep (WordN n) Source #
Instance details Defined in Grisette.Core.Data.BV type Rep (WordN n) = D1 ('MetaData "WordN" "Grisette.Core.Data.BV" "grisette-0.3.0.0-D2Nbhnc0iuRKig0VAC9Xli" 'True) (C1 ('MetaCons "WordN" 'PrefixI 'True) (S1 ('MetaSel ('Just "unWordN") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))
type PrimConstraint (WordN w) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term type PrimConstraint (WordN w) = (KnownNat w, 1 <= w)
type SymType (WordN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim type SymType (WordN n) = SymWordN n

data SomeIntN where Source #

A non-indexed version of IntN.

Constructors

SomeIntN :: (KnownNat n, 1 <= n) => IntN n -> SomeIntN

Instances

Instances details

Bits SomeIntN Source #
Instance details Defined in Grisette.Core.Data.BV Methods (.&.) :: SomeIntN -> SomeIntN -> SomeIntN # (.\|.) :: SomeIntN -> SomeIntN -> SomeIntN # xor :: SomeIntN -> SomeIntN -> SomeIntN # complement :: SomeIntN -> SomeIntN # shift :: SomeIntN -> Int -> SomeIntN # rotate :: SomeIntN -> Int -> SomeIntN # zeroBits :: SomeIntN # bit :: Int -> SomeIntN # setBit :: SomeIntN -> Int -> SomeIntN # clearBit :: SomeIntN -> Int -> SomeIntN # complementBit :: SomeIntN -> Int -> SomeIntN # testBit :: SomeIntN -> Int -> Bool # bitSizeMaybe :: SomeIntN -> Maybe Int # bitSize :: SomeIntN -> Int # isSigned :: SomeIntN -> Bool # shiftL :: SomeIntN -> Int -> SomeIntN # unsafeShiftL :: SomeIntN -> Int -> SomeIntN # shiftR :: SomeIntN -> Int -> SomeIntN # unsafeShiftR :: SomeIntN -> Int -> SomeIntN # rotateL :: SomeIntN -> Int -> SomeIntN # rotateR :: SomeIntN -> Int -> SomeIntN # popCount :: SomeIntN -> Int #
FiniteBits SomeIntN Source #
Instance details Defined in Grisette.Core.Data.BV Methods finiteBitSize :: SomeIntN -> Int # countLeadingZeros :: SomeIntN -> Int # countTrailingZeros :: SomeIntN -> Int #
Enum SomeIntN Source #
Instance details Defined in Grisette.Core.Data.BV Methods succ :: SomeIntN -> SomeIntN # pred :: SomeIntN -> SomeIntN # toEnum :: Int -> SomeIntN # fromEnum :: SomeIntN -> Int # enumFrom :: SomeIntN -> [SomeIntN] # enumFromThen :: SomeIntN -> SomeIntN -> [SomeIntN] # enumFromTo :: SomeIntN -> SomeIntN -> [SomeIntN] # enumFromThenTo :: SomeIntN -> SomeIntN -> SomeIntN -> [SomeIntN] #
Num SomeIntN Source #
Instance details Defined in Grisette.Core.Data.BV Methods (+) :: SomeIntN -> SomeIntN -> SomeIntN # (-) :: SomeIntN -> SomeIntN -> SomeIntN # (*) :: SomeIntN -> SomeIntN -> SomeIntN # negate :: SomeIntN -> SomeIntN # abs :: SomeIntN -> SomeIntN # signum :: SomeIntN -> SomeIntN # fromInteger :: Integer -> SomeIntN #
Integral SomeIntN Source #
Instance details Defined in Grisette.Core.Data.BV Methods quot :: SomeIntN -> SomeIntN -> SomeIntN # rem :: SomeIntN -> SomeIntN -> SomeIntN # div :: SomeIntN -> SomeIntN -> SomeIntN # mod :: SomeIntN -> SomeIntN -> SomeIntN # quotRem :: SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN) # divMod :: SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN) # toInteger :: SomeIntN -> Integer #
Real SomeIntN Source #
Instance details Defined in Grisette.Core.Data.BV Methods toRational :: SomeIntN -> Rational #
Show SomeIntN Source #
Instance details Defined in Grisette.Core.Data.BV Methods showsPrec :: Int -> SomeIntN -> ShowS # show :: SomeIntN -> String # showList :: [SomeIntN] -> ShowS #
NFData SomeIntN Source #
Instance details Defined in Grisette.Core.Data.BV Methods rnf :: SomeIntN -> () #
Eq SomeIntN Source #
Instance details Defined in Grisette.Core.Data.BV Methods (==) :: SomeIntN -> SomeIntN -> Bool # (/=) :: SomeIntN -> SomeIntN -> Bool #
Ord SomeIntN Source #
Instance details Defined in Grisette.Core.Data.BV Methods compare :: SomeIntN -> SomeIntN -> Ordering # (<) :: SomeIntN -> SomeIntN -> Bool # (<=) :: SomeIntN -> SomeIntN -> Bool # (>) :: SomeIntN -> SomeIntN -> Bool # (>=) :: SomeIntN -> SomeIntN -> Bool # max :: SomeIntN -> SomeIntN -> SomeIntN # min :: SomeIntN -> SomeIntN -> SomeIntN #
BV SomeIntN Source #
Instance details Defined in Grisette.Core.Data.BV Methods bvConcat :: SomeIntN -> SomeIntN -> SomeIntN Source # bvZext :: Int -> SomeIntN -> SomeIntN Source # bvSext :: Int -> SomeIntN -> SomeIntN Source # bvExt :: Int -> SomeIntN -> SomeIntN Source # bvSelect :: Int -> Int -> SomeIntN -> SomeIntN Source #
SEq SomeIntN Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~) :: SomeIntN -> SomeIntN -> SymBool Source # (/=~) :: SomeIntN -> SomeIntN -> SymBool Source #
EvaluateSym SomeIntN Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> SomeIntN -> SomeIntN Source #
ExtractSymbolics SomeIntN Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: SomeIntN -> SymbolSet Source #
Mergeable SomeIntN Source #
Instance details Defined in Grisette.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy SomeIntN Source #
SOrd SomeIntN Source #
Instance details Defined in Grisette.Core.Data.Class.SOrd Methods (<~) :: SomeIntN -> SomeIntN -> SymBool Source # (<=~) :: SomeIntN -> SomeIntN -> SymBool Source # (>~) :: SomeIntN -> SomeIntN -> SymBool Source # (>=~) :: SomeIntN -> SomeIntN -> SymBool Source # symCompare :: SomeIntN -> SomeIntN -> UnionM Ordering Source #
SubstituteSym SomeIntN Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SomeIntN -> SomeIntN Source #
Hashable SomeIntN Source #
Instance details Defined in Grisette.Core.Data.BV Methods hashWithSalt :: Int -> SomeIntN -> Int # hash :: SomeIntN -> Int #
BVSignConversion SomeWordN SomeIntN Source #
Instance details Defined in Grisette.Core.Data.BV Methods toSigned :: SomeWordN -> SomeIntN Source # toUnsigned :: SomeIntN -> SomeWordN Source #
GenSym SomeIntN SomeIntN Source #
Instance details Defined in Grisette.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => SomeIntN -> m (UnionM SomeIntN) Source #
GenSymSimple SomeIntN SomeIntN Source #
Instance details Defined in Grisette.Core.Data.Class.GenSym Methods simpleFresh :: MonadFresh m => SomeIntN -> m SomeIntN Source #
ToCon SomeIntN SomeIntN Source #
Instance details Defined in Grisette.Core.Data.Class.ToCon Methods toCon :: SomeIntN -> Maybe SomeIntN Source #
ToCon SomeSymIntN SomeIntN Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods toCon :: SomeSymIntN -> Maybe SomeIntN Source #
ToSym SomeIntN SomeIntN Source #
Instance details Defined in Grisette.Core.Data.Class.ToSym Methods toSym :: SomeIntN -> SomeIntN Source #
ToSym SomeIntN SomeSymIntN Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods toSym :: SomeIntN -> SomeSymIntN Source #
Lift SomeIntN Source #
Instance details Defined in Grisette.Core.Data.BV Methods lift :: Quote m => SomeIntN -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => SomeIntN -> Code m SomeIntN #
SafeDivision (Either BitwidthMismatch ArithException) SomeIntN Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source # safeMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source # safeDivMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source # safeQuot :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source # safeRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source # safeQuotRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source #
SafeLinearArith (Either BitwidthMismatch ArithException) SomeIntN Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source # safeNeg :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> uf SomeIntN Source # safeMinus :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> uf SomeIntN Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source #

data SomeWordN where Source #

A non-indexed version of WordN.

Constructors

SomeWordN :: (KnownNat n, 1 <= n) => WordN n -> SomeWordN

Instances

Instances details

Bits SomeWordN Source #
Instance details Defined in Grisette.Core.Data.BV Methods (.&.) :: SomeWordN -> SomeWordN -> SomeWordN # (.\|.) :: SomeWordN -> SomeWordN -> SomeWordN # xor :: SomeWordN -> SomeWordN -> SomeWordN # complement :: SomeWordN -> SomeWordN # shift :: SomeWordN -> Int -> SomeWordN # rotate :: SomeWordN -> Int -> SomeWordN # zeroBits :: SomeWordN # bit :: Int -> SomeWordN # setBit :: SomeWordN -> Int -> SomeWordN # clearBit :: SomeWordN -> Int -> SomeWordN # complementBit :: SomeWordN -> Int -> SomeWordN # testBit :: SomeWordN -> Int -> Bool # bitSizeMaybe :: SomeWordN -> Maybe Int # bitSize :: SomeWordN -> Int # isSigned :: SomeWordN -> Bool # shiftL :: SomeWordN -> Int -> SomeWordN # unsafeShiftL :: SomeWordN -> Int -> SomeWordN # shiftR :: SomeWordN -> Int -> SomeWordN # unsafeShiftR :: SomeWordN -> Int -> SomeWordN # rotateL :: SomeWordN -> Int -> SomeWordN # rotateR :: SomeWordN -> Int -> SomeWordN # popCount :: SomeWordN -> Int #
FiniteBits SomeWordN Source #
Instance details Defined in Grisette.Core.Data.BV Methods finiteBitSize :: SomeWordN -> Int # countLeadingZeros :: SomeWordN -> Int # countTrailingZeros :: SomeWordN -> Int #
Enum SomeWordN Source #
Instance details Defined in Grisette.Core.Data.BV Methods succ :: SomeWordN -> SomeWordN # pred :: SomeWordN -> SomeWordN # toEnum :: Int -> SomeWordN # fromEnum :: SomeWordN -> Int # enumFrom :: SomeWordN -> [SomeWordN] # enumFromThen :: SomeWordN -> SomeWordN -> [SomeWordN] # enumFromTo :: SomeWordN -> SomeWordN -> [SomeWordN] # enumFromThenTo :: SomeWordN -> SomeWordN -> SomeWordN -> [SomeWordN] #
Num SomeWordN Source #
Instance details Defined in Grisette.Core.Data.BV Methods (+) :: SomeWordN -> SomeWordN -> SomeWordN # (-) :: SomeWordN -> SomeWordN -> SomeWordN # (*) :: SomeWordN -> SomeWordN -> SomeWordN # negate :: SomeWordN -> SomeWordN # abs :: SomeWordN -> SomeWordN # signum :: SomeWordN -> SomeWordN # fromInteger :: Integer -> SomeWordN #
Integral SomeWordN Source #
Instance details Defined in Grisette.Core.Data.BV Methods quot :: SomeWordN -> SomeWordN -> SomeWordN # rem :: SomeWordN -> SomeWordN -> SomeWordN # div :: SomeWordN -> SomeWordN -> SomeWordN # mod :: SomeWordN -> SomeWordN -> SomeWordN # quotRem :: SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN) # divMod :: SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN) # toInteger :: SomeWordN -> Integer #
Real SomeWordN Source #
Instance details Defined in Grisette.Core.Data.BV Methods toRational :: SomeWordN -> Rational #
Show SomeWordN Source #
Instance details Defined in Grisette.Core.Data.BV Methods showsPrec :: Int -> SomeWordN -> ShowS # show :: SomeWordN -> String # showList :: [SomeWordN] -> ShowS #
NFData SomeWordN Source #
Instance details Defined in Grisette.Core.Data.BV Methods rnf :: SomeWordN -> () #
Eq SomeWordN Source #
Instance details Defined in Grisette.Core.Data.BV Methods (==) :: SomeWordN -> SomeWordN -> Bool # (/=) :: SomeWordN -> SomeWordN -> Bool #
Ord SomeWordN Source #
Instance details Defined in Grisette.Core.Data.BV Methods compare :: SomeWordN -> SomeWordN -> Ordering # (<) :: SomeWordN -> SomeWordN -> Bool # (<=) :: SomeWordN -> SomeWordN -> Bool # (>) :: SomeWordN -> SomeWordN -> Bool # (>=) :: SomeWordN -> SomeWordN -> Bool # max :: SomeWordN -> SomeWordN -> SomeWordN # min :: SomeWordN -> SomeWordN -> SomeWordN #
BV SomeWordN Source #
Instance details Defined in Grisette.Core.Data.BV Methods bvConcat :: SomeWordN -> SomeWordN -> SomeWordN Source # bvZext :: Int -> SomeWordN -> SomeWordN Source # bvSext :: Int -> SomeWordN -> SomeWordN Source # bvExt :: Int -> SomeWordN -> SomeWordN Source # bvSelect :: Int -> Int -> SomeWordN -> SomeWordN Source #
SEq SomeWordN Source #
Instance details Defined in Grisette.Core.Data.Class.Bool Methods (==~) :: SomeWordN -> SomeWordN -> SymBool Source # (/=~) :: SomeWordN -> SomeWordN -> SymBool Source #
EvaluateSym SomeWordN Source #
Instance details Defined in Grisette.Core.Data.Class.Evaluate Methods evaluateSym :: Bool -> Model -> SomeWordN -> SomeWordN Source #
ExtractSymbolics SomeWordN Source #
Instance details Defined in Grisette.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: SomeWordN -> SymbolSet Source #
Mergeable SomeWordN Source #
Instance details Defined in Grisette.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy SomeWordN Source #
SOrd SomeWordN Source #
Instance details Defined in Grisette.Core.Data.Class.SOrd Methods (<~) :: SomeWordN -> SomeWordN -> SymBool Source # (<=~) :: SomeWordN -> SomeWordN -> SymBool Source # (>~) :: SomeWordN -> SomeWordN -> SymBool Source # (>=~) :: SomeWordN -> SomeWordN -> SymBool Source # symCompare :: SomeWordN -> SomeWordN -> UnionM Ordering Source #
SubstituteSym SomeWordN Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SomeWordN -> SomeWordN Source #
Hashable SomeWordN Source #
Instance details Defined in Grisette.Core.Data.BV Methods hashWithSalt :: Int -> SomeWordN -> Int # hash :: SomeWordN -> Int #
BVSignConversion SomeWordN SomeIntN Source #
Instance details Defined in Grisette.Core.Data.BV Methods toSigned :: SomeWordN -> SomeIntN Source # toUnsigned :: SomeIntN -> SomeWordN Source #
GenSym SomeWordN SomeWordN Source #
Instance details Defined in Grisette.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => SomeWordN -> m (UnionM SomeWordN) Source #
GenSymSimple SomeWordN SomeWordN Source #
Instance details Defined in Grisette.Core.Data.Class.GenSym Methods simpleFresh :: MonadFresh m => SomeWordN -> m SomeWordN Source #
ToCon SomeWordN SomeWordN Source #
Instance details Defined in Grisette.Core.Data.Class.ToCon Methods toCon :: SomeWordN -> Maybe SomeWordN Source #
ToCon SomeSymWordN SomeWordN Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods toCon :: SomeSymWordN -> Maybe SomeWordN Source #
ToSym SomeWordN SomeWordN Source #
Instance details Defined in Grisette.Core.Data.Class.ToSym Methods toSym :: SomeWordN -> SomeWordN Source #
ToSym SomeWordN SomeSymWordN Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods toSym :: SomeWordN -> SomeSymWordN Source #
Lift SomeWordN Source #
Instance details Defined in Grisette.Core.Data.BV Methods lift :: Quote m => SomeWordN -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => SomeWordN -> Code m SomeWordN #
SafeDivision (Either BitwidthMismatch ArithException) SomeWordN Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeDiv :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source # safeMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source # safeDivMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source # safeQuot :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source # safeRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source # safeQuotRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source # safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source # safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source # safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source # safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source # safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source # safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source #
SafeLinearArith (Either BitwidthMismatch ArithException) SomeWordN Source #
Instance details Defined in Grisette.Core.Data.Class.SafeArith Methods safeAdd :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source # safeNeg :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> uf SomeWordN Source # safeMinus :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source # safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source # safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> uf SomeWordN Source # safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source #

unarySomeIntN :: (forall n. (KnownNat n, 1 <= n) => IntN n -> r) -> SomeIntN -> r Source #

unarySomeIntNR1 :: (forall n. (KnownNat n, 1 <= n) => IntN n -> IntN n) -> SomeIntN -> SomeIntN Source #

binSomeIntN :: (forall n. (KnownNat n, 1 <= n) => IntN n -> IntN n -> r) -> SomeIntN -> SomeIntN -> r Source #

binSomeIntNR1 :: (forall n. (KnownNat n, 1 <= n) => IntN n -> IntN n -> IntN n) -> SomeIntN -> SomeIntN -> SomeIntN Source #

binSomeIntNR2 :: (forall n. (KnownNat n, 1 <= n) => IntN n -> IntN n -> (IntN n, IntN n)) -> SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN) Source #

unarySomeWordN :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> r) -> SomeWordN -> r Source #

unarySomeWordNR1 :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n) -> SomeWordN -> SomeWordN Source #

binSomeWordN :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> r) -> SomeWordN -> SomeWordN -> r Source #

binSomeWordNR1 :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> WordN n) -> SomeWordN -> SomeWordN -> SomeWordN Source #

binSomeWordNR2 :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> (WordN n, WordN n)) -> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN) Source #