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

Grisette.Internal.SymPrim.BV

Description

Synopsis

data BitwidthMismatch = BitwidthMismatch
newtype IntN (n :: Nat) = IntN {
- unIntN :: Integer
}
newtype WordN (n :: Nat) = WordN {
- unWordN :: Integer
}

Documentation

data BitwidthMismatch Source #

Constructors

BitwidthMismatch

Instances

Instances details

Exception BitwidthMismatch Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods toException :: BitwidthMismatch -> SomeException # fromException :: SomeException -> Maybe BitwidthMismatch # displayException :: BitwidthMismatch -> String #
Generic BitwidthMismatch Source #
Instance details Defined in Grisette.Internal.SymPrim.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.Internal.SymPrim.BV Methods showsPrec :: Int -> BitwidthMismatch -> ShowS # show :: BitwidthMismatch -> String # showList :: [BitwidthMismatch] -> ShowS #
Eq BitwidthMismatch Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods (==) :: BitwidthMismatch -> BitwidthMismatch -> Bool # (/=) :: BitwidthMismatch -> BitwidthMismatch -> Bool #
Ord BitwidthMismatch Source #
Instance details Defined in Grisette.Internal.SymPrim.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.Internal.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy BitwidthMismatch Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => SafeDivision e (bv n) (ExceptT e m), MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e) => SafeDivision (Either BitwidthMismatch e) (SomeBV bv) m Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods safeDiv :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source # safeMod :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source # safeDivMod :: SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv) Source # safeQuot :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source # safeRem :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source # safeQuotRem :: SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv) Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => SafeLinearArith e (bv n) (ExceptT e m), MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e) => SafeLinearArith (Either BitwidthMismatch e) (SomeBV bv) m Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods safeAdd :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source # safeNeg :: SomeBV bv -> m (SomeBV bv) Source # safeSub :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => SafeSymRotate e (bv n) (ExceptT e m), MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e) => SafeSymRotate (Either BitwidthMismatch e) (SomeBV bv) m Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods safeSymRotateL :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source # safeSymRotateR :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => SafeSymShift e (bv n) (ExceptT e m), MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e) => SafeSymShift (Either BitwidthMismatch e) (SomeBV bv) m Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods safeSymShiftL :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source # safeSymShiftR :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source # safeSymStrictShiftL :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source # safeSymStrictShiftR :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source #
type Rep BitwidthMismatch Source #
Instance details Defined in Grisette.Internal.SymPrim.BV type Rep BitwidthMismatch = D1 ('MetaData "BitwidthMismatch" "Grisette.Internal.SymPrim.BV" "grisette-0.5.0.0-2ZDAuzWdzg48yPrBcRstUR" '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.Internal.SymPrim.BV Methods sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => IntN l -> IntN r -> IntN (l + r) Source # sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r Source # sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r Source # sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r Source # sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> IntN n -> IntN w Source # sizedBVFromIntegral :: forall a (n :: Nat). (Integral a, KnownNat n, 1 <= n) => a -> IntN n Source #
PEvalBVTerm IntN Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval Methods pevalBVConcatTerm :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => Term (IntN l) -> Term (IntN r) -> Term (IntN (l + r)) Source # pevalBVExtendTerm :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => Bool -> proxy r -> Term (IntN l) -> Term (IntN r) Source # pevalBVSelectTerm :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> Term (IntN n) -> Term (IntN w) Source # sbvBVConcatTerm :: forall (n :: Nat) (l :: Nat) (r :: Nat) p0 p1 p2. (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r) => p0 n -> p1 l -> p2 r -> SBVType n (IntN l) -> SBVType n (IntN r) -> SBVType n (IntN (l + r)) Source # sbvBVExtendTerm :: forall (n :: Nat) (l :: Nat) (r :: Nat) p0 p1 p2. (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => p0 n -> p1 l -> p2 r -> Bool -> SBVType n (IntN l) -> SBVType n (IntN r) Source # sbvBVSelectTerm :: forall (int :: Nat) (ix :: Nat) (w :: Nat) (n :: Nat) p0 p1 p2 p3. (KnownIsZero int, KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w, (ix + w) <= n) => p0 int -> p1 ix -> p2 w -> p3 n -> SBVType int (IntN n) -> SBVType int (IntN w) Source #
PEvalBVSignConversionTerm WordN IntN Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval Methods pevalBVToSignedTerm :: forall (n :: Nat). (KnownNat n, 1 <= n) => Term (WordN n) -> Term (IntN n) Source # pevalBVToUnsignedTerm :: forall (n :: Nat). (KnownNat n, 1 <= n) => Term (IntN n) -> Term (WordN n) Source # withSbvSignConversionTermConstraint :: forall (n :: Nat) (integerBitwidth :: Nat) p q r. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => p n -> q integerBitwidth -> ((Integral (NonFuncSBVBaseType integerBitwidth (WordN n)), Integral (NonFuncSBVBaseType integerBitwidth (IntN n))) => r) -> r Source # sbvToSigned :: forall (n :: Nat) (integerBitwidth :: Nat) o p q. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => o WordN -> p n -> q integerBitwidth -> SBVType integerBitwidth (WordN n) -> SBVType integerBitwidth (IntN n) Source # sbvToUnsigned :: forall (n :: Nat) (integerBitwidth :: Nat) o p q. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => o IntN -> p n -> q integerBitwidth -> SBVType integerBitwidth (IntN n) -> SBVType integerBitwidth (WordN n) Source #
Lift (IntN n :: Type) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods lift :: Quote m => IntN n -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => IntN n -> Code m (IntN n) #
(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeDivision ArithException (IntN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: IntN n -> IntN n -> m (IntN n) Source # safeMod :: IntN n -> IntN n -> m (IntN n) Source # safeDivMod :: IntN n -> IntN n -> m (IntN n, IntN n) Source # safeQuot :: IntN n -> IntN n -> m (IntN n) Source # safeRem :: IntN n -> IntN n -> m (IntN n) Source # safeQuotRem :: IntN n -> IntN n -> m (IntN n, IntN n) Source #
(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (IntN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith Methods safeAdd :: IntN n -> IntN n -> m (IntN n) Source # safeNeg :: IntN n -> m (IntN n) Source # safeSub :: IntN n -> IntN n -> m (IntN n) Source #
(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymRotate ArithException (IntN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate Methods safeSymRotateL :: IntN n -> IntN n -> m (IntN n) Source # safeSymRotateR :: IntN n -> IntN n -> m (IntN n) Source #
(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymShift ArithException (IntN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymShift Methods safeSymShiftL :: IntN n -> IntN n -> m (IntN n) Source # safeSymShiftR :: IntN n -> IntN n -> m (IntN n) Source # safeSymStrictShiftL :: IntN n -> IntN n -> m (IntN n) Source # safeSymStrictShiftR :: IntN n -> IntN n -> m (IntN n) Source #
(KnownNat n, 1 <= n) => Arbitrary (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods arbitrary :: Gen (IntN n) # shrink :: IntN n -> [IntN n] #
(KnownNat n, 1 <= n) => Bits (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods (.&.) :: IntN n -> IntN n -> IntN n # (.\|.) :: IntN n -> IntN n -> IntN n # xor :: IntN n -> IntN n -> IntN n # complement :: IntN n -> IntN n # shift :: IntN n -> Int -> IntN n # rotate :: IntN n -> Int -> IntN n # zeroBits :: IntN n # bit :: Int -> IntN n # setBit :: IntN n -> Int -> IntN n # clearBit :: IntN n -> Int -> IntN n # complementBit :: IntN n -> Int -> IntN n # testBit :: IntN n -> Int -> Bool # bitSizeMaybe :: IntN n -> Maybe Int # bitSize :: IntN n -> Int # isSigned :: IntN n -> Bool # shiftL :: IntN n -> Int -> IntN n # unsafeShiftL :: IntN n -> Int -> IntN n # shiftR :: IntN n -> Int -> IntN n # unsafeShiftR :: IntN n -> Int -> IntN n # rotateL :: IntN n -> Int -> IntN n # rotateR :: IntN n -> Int -> IntN n # popCount :: IntN n -> Int #
(KnownNat n, 1 <= n) => FiniteBits (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods finiteBitSize :: IntN n -> Int # countLeadingZeros :: IntN n -> Int # countTrailingZeros :: IntN n -> Int #
(KnownNat n, 1 <= n) => Bounded (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods minBound :: IntN n # maxBound :: IntN n #
(KnownNat n, 1 <= n) => Enum (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods succ :: IntN n -> IntN n # pred :: IntN n -> IntN n # toEnum :: Int -> IntN n # fromEnum :: IntN n -> Int # enumFrom :: IntN n -> [IntN n] # enumFromThen :: IntN n -> IntN n -> [IntN n] # enumFromTo :: IntN n -> IntN n -> [IntN n] # enumFromThenTo :: IntN n -> IntN n -> IntN n -> [IntN n] #
Generic (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Associated Types type Rep (IntN n) :: 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.Internal.SymPrim.BV Methods (+) :: IntN n -> IntN n -> IntN n # (-) :: IntN n -> IntN n -> IntN n # (*) :: IntN n -> IntN n -> IntN n # negate :: IntN n -> IntN n # abs :: IntN n -> IntN n # signum :: IntN n -> IntN n # fromInteger :: Integer -> IntN n #
(KnownNat n, 1 <= n) => Read (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods readsPrec :: Int -> ReadS (IntN n) # readList :: ReadS [IntN n] # readPrec :: ReadPrec (IntN n) # readListPrec :: ReadPrec [IntN n] #
(KnownNat n, 1 <= n) => Integral (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods quot :: IntN n -> IntN n -> IntN n # rem :: IntN n -> IntN n -> IntN n # div :: IntN n -> IntN n -> IntN n # mod :: IntN n -> IntN n -> IntN n # quotRem :: IntN n -> IntN n -> (IntN n, IntN n) # divMod :: IntN n -> IntN n -> (IntN n, IntN n) # toInteger :: IntN n -> Integer #
(KnownNat n, 1 <= n) => Real (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods toRational :: IntN n -> Rational #
(KnownNat n, 1 <= n) => Show (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods showsPrec :: Int -> IntN n -> ShowS # show :: IntN n -> String # showList :: [IntN n] -> ShowS #
NFData (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods rnf :: IntN n -> () #
Eq (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods (==) :: IntN n -> IntN n -> Bool # (/=) :: IntN n -> IntN n -> Bool #
(KnownNat n, 1 <= n) => Ord (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods compare :: IntN n -> IntN n -> Ordering # (<) :: IntN n -> IntN n -> Bool # (<=) :: IntN n -> IntN n -> Bool # (>) :: IntN n -> IntN n -> Bool # (>=) :: IntN n -> IntN n -> Bool # max :: IntN n -> IntN n -> IntN n # min :: IntN n -> IntN n -> IntN n #
(KnownNat n, 1 <= n) => EvaluateSym (IntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.EvaluateSym Methods evaluateSym :: Bool -> Model -> IntN n -> IntN n Source #
(KnownNat n, 1 <= n) => ExtractSymbolics (IntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: IntN n -> SymbolSet Source #
(KnownNat n, 1 <= n) => GPretty (IntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GPretty Methods gpretty :: IntN n -> Doc ann Source # gprettyPrec :: Int -> IntN n -> Doc ann Source # gprettyList :: [IntN n] -> Doc ann Source #
(KnownNat n, 1 <= n) => Mergeable (IntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy (IntN n) Source #
(KnownNat n, 1 <= n) => SEq (IntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: IntN n -> IntN n -> SymBool Source # (./=) :: IntN n -> IntN n -> SymBool Source #
(KnownNat n, 1 <= n) => SOrd (IntN n) Source #
Instance details Defined in Grisette.Internal.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.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> IntN n -> IntN n Source #
(KnownNat n, 1 <= n) => SymRotate (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods symRotate :: IntN n -> IntN n -> IntN n Source # symRotateNegated :: IntN n -> IntN n -> IntN n Source #
(KnownNat n, 1 <= n) => SymShift (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods symShift :: IntN n -> IntN n -> IntN n Source # symShiftNegated :: IntN n -> IntN n -> IntN n Source #
(KnownNat w, 1 <= w) => NonFuncSBVRep (IntN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type NonFuncSBVBaseType n (IntN w) Source #
(KnownNat n, 1 <= n) => PEvalBitwiseTerm (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitwiseTerm Methods pevalAndBitsTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalOrBitsTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalXorBitsTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalComplementBitsTerm :: Term (IntN n) -> Term (IntN n) Source # withSbvBitwiseTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (Bits (SBVType n0 (IntN n)) => r) -> r Source # sbvAndBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvOrBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvXorBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvComplementBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source #
(KnownNat n, 1 <= n) => PEvalDivModIntegralTerm (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalDivModIntegralTerm Methods pevalDivIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalModIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalQuotIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalRemIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # withSbvDivModIntegralTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SDivisible (SBVType n0 (IntN n)) => r) -> r Source # sbvDivIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvModIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvQuotIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvRemIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source #
(KnownNat n, 1 <= n) => PEvalNumTerm (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm Methods pevalAddNumTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalNegNumTerm :: Term (IntN n) -> Term (IntN n) Source # pevalMulNumTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalAbsNumTerm :: Term (IntN n) -> Term (IntN n) Source # pevalSignumNumTerm :: Term (IntN n) -> Term (IntN n) Source # withSbvNumTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (Num (SBVType n0 (IntN n)) => r) -> r Source # sbvAddNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvNegNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvMulNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvAbsNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvSignumNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source #
(KnownNat n, 1 <= n) => PEvalOrdTerm (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm Methods pevalLtOrdTerm :: Term (IntN n) -> Term (IntN n) -> Term Bool Source # pevalLeOrdTerm :: Term (IntN n) -> Term (IntN n) -> Term Bool Source # withSbvOrdTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (OrdSymbolic (SBVType n0 (IntN n)) => r) -> r Source # sbvLtOrdTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBV Bool Source # sbvLeOrdTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBV Bool Source #
(KnownNat n, 1 <= n) => PEvalRotateTerm (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalRotateTerm Methods pevalRotateLeftTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalRotateRightTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # withSbvRotateTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SIntegral (NonFuncSBVBaseType n0 (IntN n)) => r) -> r Source # sbvRotateLeftTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvRotateRightTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source #
(KnownNat n, 1 <= n) => PEvalShiftTerm (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalShiftTerm Methods pevalShiftLeftTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalShiftRightTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # withSbvShiftTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SIntegral (NonFuncSBVBaseType n0 (IntN n)) => r) -> r Source # sbvShiftLeftTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvShiftRightTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source #
(KnownNat w, 1 <= w) => SBVRep (IntN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type SBVType n (IntN w) Source #
(KnownNat w, 1 <= w) => SupportedNonFuncPrim (IntN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Methods conNonFuncSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> IntN w -> SBV (NonFuncSBVBaseType n (IntN w)) Source # symNonFuncSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBV (NonFuncSBVBaseType n (IntN w))) Source # withNonFuncPrim :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> ((SymVal (NonFuncSBVBaseType n (IntN w)), EqSymbolic (SBVType n (IntN w)), Mergeable (SBVType n (IntN w)), SMTDefinable (SBVType n (IntN w)), Mergeable (SBVType n (IntN w)), SBVType n (IntN w) ~ SBV (NonFuncSBVBaseType n (IntN w)), PrimConstraint n (IntN w)) => r) -> r Source #
(KnownNat w, 1 <= w) => SupportedPrim (IntN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Methods 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 # pevalITETerm :: Term Bool -> Term (IntN w) -> Term (IntN w) -> Term (IntN w) Source # pevalEqTerm :: Term (IntN w) -> Term (IntN w) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> IntN w -> SBVType n (IntN w) Source # symSBVName :: TypedSymbol (IntN w) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (IntN w)) Source # withPrim :: forall (n :: Nat) p a. KnownIsZero n => p n -> ((PrimConstraint n (IntN w), SMTDefinable (SBVType n (IntN w)), Mergeable (SBVType n (IntN w)), Typeable (SBVType n (IntN w))) => a) -> a Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (IntN w) -> SBVType n (IntN w) -> SBVType n (IntN w) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (IntN w) -> SBVType n (IntN w) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> IntN w Source #
(KnownNat w, 1 <= w) => SupportedPrimConstraint (IntN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type PrimConstraint n (IntN w) Source #
(KnownNat n, 1 <= n) => SymRep (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Associated Types type SymType (IntN n) Source #
Hashable (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods hashWithSalt :: Int -> IntN n -> Int # hash :: IntN n -> Int #
(KnownNat n, 1 <= n) => GenSym (IntN n) (IntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => IntN n -> m (UnionM (IntN n)) Source #
(KnownNat n, 1 <= n) => GenSymSimple (IntN n) (IntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods simpleFresh :: MonadFresh m => IntN n -> m (IntN n) Source #
(KnownNat n, 1 <= n) => SignConversion (WordN n) (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods toSigned :: WordN n -> IntN n Source # toUnsigned :: IntN n -> WordN n Source #
(KnownNat n, 1 <= n) => Solvable (IntN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods con :: IntN n -> SymIntN n Source # conView :: SymIntN n -> Maybe (IntN n) Source # sym :: Symbol -> SymIntN n Source # ssym :: Identifier -> SymIntN n Source # isym :: Identifier -> Int -> SymIntN n Source #
(KnownNat n, 1 <= n) => ToCon (IntN n) (IntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: IntN n -> Maybe (IntN n) Source #
(KnownNat n, 1 <= n) => ToCon (SymIntN n) (IntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: SymIntN n -> Maybe (IntN n) Source #
(KnownNat n, 1 <= n) => ToSym (UnionM (IntN n)) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.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.Internal.Core.Data.Class.ToSym Methods toSym :: IntN n -> IntN n Source #
(KnownNat n, 1 <= n) => ToSym (IntN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: IntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => LinkedRep (IntN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods underlyingTerm :: SymIntN n -> Term (IntN n) Source # wrapTerm :: Term (IntN n) -> SymIntN n Source #
type NonFuncSBVBaseType _1 (IntN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type NonFuncSBVBaseType _1 (IntN w) = IntN w
type PrimConstraint _1 (IntN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type PrimConstraint _1 (IntN w) = (KnownNat w, 1 <= w, BVIsNonZero w)
type SBVType _1 (IntN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type SBVType _1 (IntN w) = SBV (IntN w)
type Rep (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV type Rep (IntN n) = D1 ('MetaData "IntN" "Grisette.Internal.SymPrim.BV" "grisette-0.5.0.0-2ZDAuzWdzg48yPrBcRstUR" 'True) (C1 ('MetaCons "IntN" 'PrefixI 'True) (S1 ('MetaSel ('Just "unIntN") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))
type SymType (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV 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.Internal.SymPrim.BV Methods sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => WordN l -> WordN r -> WordN (l + r) Source # sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r Source # sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r Source # sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r Source # sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> WordN n -> WordN w Source # sizedBVFromIntegral :: forall a (n :: Nat). (Integral a, KnownNat n, 1 <= n) => a -> WordN n Source #
PEvalBVTerm WordN Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval Methods pevalBVConcatTerm :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => Term (WordN l) -> Term (WordN r) -> Term (WordN (l + r)) Source # pevalBVExtendTerm :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => Bool -> proxy r -> Term (WordN l) -> Term (WordN r) Source # pevalBVSelectTerm :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> Term (WordN n) -> Term (WordN w) Source # sbvBVConcatTerm :: forall (n :: Nat) (l :: Nat) (r :: Nat) p0 p1 p2. (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r) => p0 n -> p1 l -> p2 r -> SBVType n (WordN l) -> SBVType n (WordN r) -> SBVType n (WordN (l + r)) Source # sbvBVExtendTerm :: forall (n :: Nat) (l :: Nat) (r :: Nat) p0 p1 p2. (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => p0 n -> p1 l -> p2 r -> Bool -> SBVType n (WordN l) -> SBVType n (WordN r) Source # sbvBVSelectTerm :: forall (int :: Nat) (ix :: Nat) (w :: Nat) (n :: Nat) p0 p1 p2 p3. (KnownIsZero int, KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w, (ix + w) <= n) => p0 int -> p1 ix -> p2 w -> p3 n -> SBVType int (WordN n) -> SBVType int (WordN w) Source #
PEvalBVSignConversionTerm WordN IntN Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval Methods pevalBVToSignedTerm :: forall (n :: Nat). (KnownNat n, 1 <= n) => Term (WordN n) -> Term (IntN n) Source # pevalBVToUnsignedTerm :: forall (n :: Nat). (KnownNat n, 1 <= n) => Term (IntN n) -> Term (WordN n) Source # withSbvSignConversionTermConstraint :: forall (n :: Nat) (integerBitwidth :: Nat) p q r. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => p n -> q integerBitwidth -> ((Integral (NonFuncSBVBaseType integerBitwidth (WordN n)), Integral (NonFuncSBVBaseType integerBitwidth (IntN n))) => r) -> r Source # sbvToSigned :: forall (n :: Nat) (integerBitwidth :: Nat) o p q. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => o WordN -> p n -> q integerBitwidth -> SBVType integerBitwidth (WordN n) -> SBVType integerBitwidth (IntN n) Source # sbvToUnsigned :: forall (n :: Nat) (integerBitwidth :: Nat) o p q. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => o IntN -> p n -> q integerBitwidth -> SBVType integerBitwidth (IntN n) -> SBVType integerBitwidth (WordN n) Source #
Lift (WordN n :: Type) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods lift :: Quote m => WordN n -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => WordN n -> Code m (WordN n) #
(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeDivision ArithException (WordN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: WordN n -> WordN n -> m (WordN n) Source # safeMod :: WordN n -> WordN n -> m (WordN n) Source # safeDivMod :: WordN n -> WordN n -> m (WordN n, WordN n) Source # safeQuot :: WordN n -> WordN n -> m (WordN n) Source # safeRem :: WordN n -> WordN n -> m (WordN n) Source # safeQuotRem :: WordN n -> WordN n -> m (WordN n, WordN n) Source #
(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (WordN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith Methods safeAdd :: WordN n -> WordN n -> m (WordN n) Source # safeNeg :: WordN n -> m (WordN n) Source # safeSub :: WordN n -> WordN n -> m (WordN n) Source #
(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymRotate ArithException (WordN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate Methods safeSymRotateL :: WordN n -> WordN n -> m (WordN n) Source # safeSymRotateR :: WordN n -> WordN n -> m (WordN n) Source #
(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymShift ArithException (WordN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymShift Methods safeSymShiftL :: WordN n -> WordN n -> m (WordN n) Source # safeSymShiftR :: WordN n -> WordN n -> m (WordN n) Source # safeSymStrictShiftL :: WordN n -> WordN n -> m (WordN n) Source # safeSymStrictShiftR :: WordN n -> WordN n -> m (WordN n) Source #
(KnownNat n, 1 <= n) => Arbitrary (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods arbitrary :: Gen (WordN n) # shrink :: WordN n -> [WordN n] #
(KnownNat n, 1 <= n) => Bits (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods (.&.) :: WordN n -> WordN n -> WordN n # (.\|.) :: WordN n -> WordN n -> WordN n # xor :: WordN n -> WordN n -> WordN n # complement :: WordN n -> WordN n # shift :: WordN n -> Int -> WordN n # rotate :: WordN n -> Int -> WordN n # zeroBits :: WordN n # bit :: Int -> WordN n # setBit :: WordN n -> Int -> WordN n # clearBit :: WordN n -> Int -> WordN n # complementBit :: WordN n -> Int -> WordN n # testBit :: WordN n -> Int -> Bool # bitSizeMaybe :: WordN n -> Maybe Int # bitSize :: WordN n -> Int # isSigned :: WordN n -> Bool # shiftL :: WordN n -> Int -> WordN n # unsafeShiftL :: WordN n -> Int -> WordN n # shiftR :: WordN n -> Int -> WordN n # unsafeShiftR :: WordN n -> Int -> WordN n # rotateL :: WordN n -> Int -> WordN n # rotateR :: WordN n -> Int -> WordN n # popCount :: WordN n -> Int #
(KnownNat n, 1 <= n) => FiniteBits (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods finiteBitSize :: WordN n -> Int # countLeadingZeros :: WordN n -> Int # countTrailingZeros :: WordN n -> Int #
(KnownNat n, 1 <= n) => Bounded (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods minBound :: WordN n # maxBound :: WordN n #
(KnownNat n, 1 <= n) => Enum (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods succ :: WordN n -> WordN n # pred :: WordN n -> WordN n # toEnum :: Int -> WordN n # fromEnum :: WordN n -> Int # enumFrom :: WordN n -> [WordN n] # enumFromThen :: WordN n -> WordN n -> [WordN n] # enumFromTo :: WordN n -> WordN n -> [WordN n] # enumFromThenTo :: WordN n -> WordN n -> WordN n -> [WordN n] #
Generic (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Associated Types type Rep (WordN n) :: 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.Internal.SymPrim.BV Methods (+) :: WordN n -> WordN n -> WordN n # (-) :: WordN n -> WordN n -> WordN n # (*) :: WordN n -> WordN n -> WordN n # negate :: WordN n -> WordN n # abs :: WordN n -> WordN n # signum :: WordN n -> WordN n # fromInteger :: Integer -> WordN n #
(KnownNat n, 1 <= n) => Read (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods readsPrec :: Int -> ReadS (WordN n) # readList :: ReadS [WordN n] # readPrec :: ReadPrec (WordN n) # readListPrec :: ReadPrec [WordN n] #
(KnownNat n, 1 <= n) => Integral (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods quot :: WordN n -> WordN n -> WordN n # rem :: WordN n -> WordN n -> WordN n # div :: WordN n -> WordN n -> WordN n # mod :: WordN n -> WordN n -> WordN n # quotRem :: WordN n -> WordN n -> (WordN n, WordN n) # divMod :: WordN n -> WordN n -> (WordN n, WordN n) # toInteger :: WordN n -> Integer #
(KnownNat n, 1 <= n) => Real (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods toRational :: WordN n -> Rational #
(KnownNat n, 1 <= n) => Show (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods showsPrec :: Int -> WordN n -> ShowS # show :: WordN n -> String # showList :: [WordN n] -> ShowS #
NFData (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods rnf :: WordN n -> () #
Eq (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods (==) :: WordN n -> WordN n -> Bool # (/=) :: WordN n -> WordN n -> Bool #
Ord (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods compare :: WordN n -> WordN n -> Ordering # (<) :: WordN n -> WordN n -> Bool # (<=) :: WordN n -> WordN n -> Bool # (>) :: WordN n -> WordN n -> Bool # (>=) :: WordN n -> WordN n -> Bool # max :: WordN n -> WordN n -> WordN n # min :: WordN n -> WordN n -> WordN n #
(KnownNat n, 1 <= n) => EvaluateSym (WordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.EvaluateSym Methods evaluateSym :: Bool -> Model -> WordN n -> WordN n Source #
(KnownNat n, 1 <= n) => ExtractSymbolics (WordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: WordN n -> SymbolSet Source #
(KnownNat n, 1 <= n) => GPretty (WordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GPretty Methods gpretty :: WordN n -> Doc ann Source # gprettyPrec :: Int -> WordN n -> Doc ann Source # gprettyList :: [WordN n] -> Doc ann Source #
(KnownNat n, 1 <= n) => Mergeable (WordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy (WordN n) Source #
(KnownNat n, 1 <= n) => SEq (WordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: WordN n -> WordN n -> SymBool Source # (./=) :: WordN n -> WordN n -> SymBool Source #
(KnownNat n, 1 <= n) => SOrd (WordN n) Source #
Instance details Defined in Grisette.Internal.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.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> WordN n -> WordN n Source #
(KnownNat n, 1 <= n) => SymRotate (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods symRotate :: WordN n -> WordN n -> WordN n Source # symRotateNegated :: WordN n -> WordN n -> WordN n Source #
(KnownNat n, 1 <= n) => SymShift (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods symShift :: WordN n -> WordN n -> WordN n Source # symShiftNegated :: WordN n -> WordN n -> WordN n Source #
(KnownNat w, 1 <= w) => NonFuncSBVRep (WordN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type NonFuncSBVBaseType n (WordN w) Source #
(KnownNat n, 1 <= n) => PEvalBitwiseTerm (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitwiseTerm Methods pevalAndBitsTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalOrBitsTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalXorBitsTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalComplementBitsTerm :: Term (WordN n) -> Term (WordN n) Source # withSbvBitwiseTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (Bits (SBVType n0 (WordN n)) => r) -> r Source # sbvAndBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvOrBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvXorBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvComplementBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source #
(KnownNat n, 1 <= n) => PEvalDivModIntegralTerm (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalDivModIntegralTerm Methods pevalDivIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalModIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalQuotIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalRemIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # withSbvDivModIntegralTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SDivisible (SBVType n0 (WordN n)) => r) -> r Source # sbvDivIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvModIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvQuotIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvRemIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source #
(KnownNat n, 1 <= n) => PEvalNumTerm (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm Methods pevalAddNumTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalNegNumTerm :: Term (WordN n) -> Term (WordN n) Source # pevalMulNumTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalAbsNumTerm :: Term (WordN n) -> Term (WordN n) Source # pevalSignumNumTerm :: Term (WordN n) -> Term (WordN n) Source # withSbvNumTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (Num (SBVType n0 (WordN n)) => r) -> r Source # sbvAddNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvNegNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvMulNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvAbsNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvSignumNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source #
(KnownNat n, 1 <= n) => PEvalOrdTerm (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm Methods pevalLtOrdTerm :: Term (WordN n) -> Term (WordN n) -> Term Bool Source # pevalLeOrdTerm :: Term (WordN n) -> Term (WordN n) -> Term Bool Source # withSbvOrdTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (OrdSymbolic (SBVType n0 (WordN n)) => r) -> r Source # sbvLtOrdTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBV Bool Source # sbvLeOrdTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBV Bool Source #
(KnownNat n, 1 <= n) => PEvalRotateTerm (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalRotateTerm Methods pevalRotateLeftTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalRotateRightTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # withSbvRotateTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SIntegral (NonFuncSBVBaseType n0 (WordN n)) => r) -> r Source # sbvRotateLeftTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvRotateRightTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source #
(KnownNat n, 1 <= n) => PEvalShiftTerm (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalShiftTerm Methods pevalShiftLeftTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalShiftRightTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # withSbvShiftTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SIntegral (NonFuncSBVBaseType n0 (WordN n)) => r) -> r Source # sbvShiftLeftTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvShiftRightTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source #
(KnownNat w, 1 <= w) => SBVRep (WordN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type SBVType n (WordN w) Source #
(KnownNat w, 1 <= w) => SupportedNonFuncPrim (WordN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Methods conNonFuncSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> WordN w -> SBV (NonFuncSBVBaseType n (WordN w)) Source # symNonFuncSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBV (NonFuncSBVBaseType n (WordN w))) Source # withNonFuncPrim :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> ((SymVal (NonFuncSBVBaseType n (WordN w)), EqSymbolic (SBVType n (WordN w)), Mergeable (SBVType n (WordN w)), SMTDefinable (SBVType n (WordN w)), Mergeable (SBVType n (WordN w)), SBVType n (WordN w) ~ SBV (NonFuncSBVBaseType n (WordN w)), PrimConstraint n (WordN w)) => r) -> r Source #
(KnownNat w, 1 <= w) => SupportedPrim (WordN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Methods 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 # pevalITETerm :: Term Bool -> Term (WordN w) -> Term (WordN w) -> Term (WordN w) Source # pevalEqTerm :: Term (WordN w) -> Term (WordN w) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> WordN w -> SBVType n (WordN w) Source # symSBVName :: TypedSymbol (WordN w) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (WordN w)) Source # withPrim :: forall (n :: Nat) p a. KnownIsZero n => p n -> ((PrimConstraint n (WordN w), SMTDefinable (SBVType n (WordN w)), Mergeable (SBVType n (WordN w)), Typeable (SBVType n (WordN w))) => a) -> a Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (WordN w) -> SBVType n (WordN w) -> SBVType n (WordN w) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (WordN w) -> SBVType n (WordN w) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> WordN w Source #
(KnownNat w, 1 <= w) => SupportedPrimConstraint (WordN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type PrimConstraint n (WordN w) Source #
(KnownNat n, 1 <= n) => SymRep (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Associated Types type SymType (WordN n) Source #
Hashable (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods hashWithSalt :: Int -> WordN n -> Int # hash :: WordN n -> Int #
(KnownNat n, 1 <= n) => GenSym (WordN n) (WordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => WordN n -> m (UnionM (WordN n)) Source #
(KnownNat n, 1 <= n) => GenSymSimple (WordN n) (WordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods simpleFresh :: MonadFresh m => WordN n -> m (WordN n) Source #
(KnownNat n, 1 <= n) => SignConversion (WordN n) (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods toSigned :: WordN n -> IntN n Source # toUnsigned :: IntN n -> WordN n Source #
(KnownNat n, 1 <= n) => Solvable (WordN n) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods con :: WordN n -> SymWordN n Source # conView :: SymWordN n -> Maybe (WordN n) Source # sym :: Symbol -> SymWordN n Source # ssym :: Identifier -> SymWordN n Source # isym :: Identifier -> Int -> SymWordN n Source #
(KnownNat n, 1 <= n) => ToCon (WordN n) (WordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: WordN n -> Maybe (WordN n) Source #
(KnownNat n, 1 <= n) => ToCon (SymWordN n) (WordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: SymWordN n -> Maybe (WordN n) Source #
(KnownNat n, 1 <= n) => ToSym (UnionM (WordN n)) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.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.Internal.Core.Data.Class.ToSym Methods toSym :: WordN n -> WordN n Source #
(KnownNat n, 1 <= n) => ToSym (WordN n) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: WordN n -> SymWordN n Source #
(KnownNat n, 1 <= n) => LinkedRep (WordN n) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods underlyingTerm :: SymWordN n -> Term (WordN n) Source # wrapTerm :: Term (WordN n) -> SymWordN n Source #
type NonFuncSBVBaseType _1 (WordN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type NonFuncSBVBaseType _1 (WordN w) = WordN w
type PrimConstraint _1 (WordN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type PrimConstraint _1 (WordN w) = (KnownNat w, 1 <= w, BVIsNonZero w)
type SBVType _1 (WordN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type SBVType _1 (WordN w) = SBV (WordN w)
type Rep (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.BV type Rep (WordN n) = D1 ('MetaData "WordN" "Grisette.Internal.SymPrim.BV" "grisette-0.5.0.0-2ZDAuzWdzg48yPrBcRstUR" 'True) (C1 ('MetaCons "WordN" 'PrefixI 'True) (S1 ('MetaSel ('Just "unWordN") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))
type SymType (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV type SymType (WordN n) = SymWordN n