Grisette.SymPrim

Symbolic type implementation

Extended types

data IntN (n :: Nat)

Symbolic signed bit vectors.

Instances

SizedBV IntN

Defined in Grisette.Internal.SymPrim.BV

Methods

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

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

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

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

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

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

PEvalBVTerm IntN

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

Methods

pevalBVConcatTerm :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => Term (IntN l) -> Term (IntN r) -> Term (IntN (l + r))

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

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

sbvBVConcatTerm :: forall (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))

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)

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)

PEvalBVSignConversionTerm WordN IntN

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

Methods

pevalBVToSignedTerm :: forall (n :: Nat). (KnownNat n, 1 <= n) => Term (WordN n) -> Term (IntN n)

pevalBVToUnsignedTerm :: forall (n :: Nat). (KnownNat n, 1 <= n) => Term (IntN n) -> Term (WordN n)

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

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)

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)

Lift (IntN n :: Type)

Defined in Grisette.Internal.SymPrim.BV

Methods

lift :: Quote m => IntN n -> m Exp

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

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

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

Methods

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

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

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

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

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

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

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

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

Methods

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

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

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

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

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

Methods

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

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

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

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

Methods

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

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

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

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

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

Defined in Grisette.Internal.SymPrim.BV

Methods

arbitrary :: Gen (IntN n)

shrink :: IntN n -> [IntN n]

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

Defined in Grisette.Internal.SymPrim.BV

Methods

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

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

xor :: IntN n -> IntN n -> IntN n

complement :: IntN n -> IntN n

shift :: IntN n -> Int -> IntN n

rotate :: IntN n -> Int -> IntN n

zeroBits :: IntN n

bit :: Int -> IntN n

setBit :: IntN n -> Int -> IntN n

clearBit :: IntN n -> Int -> IntN n

complementBit :: IntN n -> Int -> IntN n

testBit :: IntN n -> Int -> Bool

bitSizeMaybe :: IntN n -> Maybe Int

bitSize :: IntN n -> Int

isSigned :: IntN n -> Bool

shiftL :: IntN n -> Int -> IntN n

unsafeShiftL :: IntN n -> Int -> IntN n

shiftR :: IntN n -> Int -> IntN n

unsafeShiftR :: IntN n -> Int -> IntN n

rotateL :: IntN n -> Int -> IntN n

rotateR :: IntN n -> Int -> IntN n

popCount :: IntN n -> Int

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

Defined in Grisette.Internal.SymPrim.BV

Methods

finiteBitSize :: IntN n -> Int

countLeadingZeros :: IntN n -> Int

countTrailingZeros :: IntN n -> Int

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

Defined in Grisette.Internal.SymPrim.BV

Methods

minBound :: IntN n

maxBound :: IntN n

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

Defined in Grisette.Internal.SymPrim.BV

Methods

succ :: IntN n -> IntN n

pred :: IntN n -> IntN n

toEnum :: Int -> IntN n

fromEnum :: IntN n -> Int

enumFrom :: IntN n -> [IntN n]

enumFromThen :: IntN n -> IntN n -> [IntN n]

enumFromTo :: IntN n -> IntN n -> [IntN n]

enumFromThenTo :: IntN n -> IntN n -> IntN n -> [IntN n]

Generic (IntN n)

Defined in Grisette.Internal.SymPrim.BV

Associated Types

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

Methods

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

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

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

Defined in Grisette.Internal.SymPrim.BV

Methods

(+) :: IntN n -> IntN n -> IntN n

(-) :: IntN n -> IntN n -> IntN n

(*) :: IntN n -> IntN n -> IntN n

negate :: IntN n -> IntN n

abs :: IntN n -> IntN n

signum :: IntN n -> IntN n

fromInteger :: Integer -> IntN n

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

Defined in Grisette.Internal.SymPrim.BV

Methods

readsPrec :: Int -> ReadS (IntN n)

readList :: ReadS [IntN n]

readPrec :: ReadPrec (IntN n)

readListPrec :: ReadPrec [IntN n]

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

Defined in Grisette.Internal.SymPrim.BV

Methods

quot :: IntN n -> IntN n -> IntN n

rem :: IntN n -> IntN n -> IntN n

div :: IntN n -> IntN n -> IntN n

mod :: IntN n -> IntN n -> IntN n

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

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

toInteger :: IntN n -> Integer

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

Defined in Grisette.Internal.SymPrim.BV

Methods

toRational :: IntN n -> Rational

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

Defined in Grisette.Internal.SymPrim.BV

Methods

showsPrec :: Int -> IntN n -> ShowS

show :: IntN n -> String

showList :: [IntN n] -> ShowS

NFData (IntN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

rnf :: IntN n -> ()

Eq (IntN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

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

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

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

Defined in Grisette.Internal.SymPrim.BV

Methods

compare :: IntN n -> IntN n -> Ordering

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

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

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

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

max :: IntN n -> IntN n -> IntN n

min :: IntN n -> IntN n -> IntN n

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

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

Methods

evaluateSym :: Bool -> Model -> IntN n -> IntN n

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

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

Methods

extractSymbolics :: IntN n -> SymbolSet

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

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

Methods

gpretty :: IntN n -> Doc ann

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

gprettyList :: [IntN n] -> Doc ann

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

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

Methods

rootStrategy :: MergingStrategy (IntN n)

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

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

Methods

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

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

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

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

Methods

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

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

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

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

symCompare :: IntN n -> IntN n -> UnionM Ordering

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

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

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> IntN n -> IntN n

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

Defined in Grisette.Internal.SymPrim.BV

Methods

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

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

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

Defined in Grisette.Internal.SymPrim.BV

Methods

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

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

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

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

Associated Types

type NonFuncSBVBaseType n (IntN w)

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

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

Methods

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

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

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

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

withSbvBitwiseTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (Bits (SBVType n0 (IntN n)) => r) -> r

sbvAndBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

sbvOrBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

sbvXorBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

sbvComplementBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

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

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

Methods

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

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

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

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

withSbvDivModIntegralTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SDivisible (SBVType n0 (IntN n)) => r) -> r

sbvDivIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

sbvModIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

sbvQuotIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

sbvRemIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

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

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

Methods

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

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

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

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

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

withSbvNumTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (Num (SBVType n0 (IntN n)) => r) -> r

sbvAddNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

sbvNegNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

sbvMulNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

sbvAbsNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

sbvSignumNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

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

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

Methods

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

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

withSbvOrdTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (OrdSymbolic (SBVType n0 (IntN n)) => r) -> r

sbvLtOrdTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBV Bool

sbvLeOrdTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBV Bool

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

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

Methods

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

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

withSbvRotateTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SIntegral (NonFuncSBVBaseType n0 (IntN n)) => r) -> r

sbvRotateLeftTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

sbvRotateRightTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

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

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

Methods

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

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

withSbvShiftTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SIntegral (NonFuncSBVBaseType n0 (IntN n)) => r) -> r

sbvShiftLeftTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

sbvShiftRightTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n)

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

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

Associated Types

type SBVType n (IntN w)

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

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

symNonFuncSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBV (NonFuncSBVBaseType n (IntN w)))

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

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

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

Methods

termCache :: Cache (Term (IntN w))

pformatCon :: IntN w -> String

pformatSym :: TypedSymbol (IntN w) -> String

defaultValue :: IntN w

defaultValueDynamic :: proxy (IntN w) -> ModelValue

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

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

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> IntN w -> SBVType n (IntN w)

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

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (IntN w))

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

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (IntN w) -> SBVType n (IntN w) -> SBVType n (IntN w)

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (IntN w) -> SBVType n (IntN w) -> SBV Bool

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

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

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

Associated Types

type PrimConstraint n (IntN w)

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

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type SymType (IntN n)

Hashable (IntN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

hashWithSalt :: Int -> IntN n -> Int

hash :: IntN n -> Int

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

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

Methods

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

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

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

Methods

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

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

Defined in Grisette.Internal.SymPrim.BV

Methods

toSigned :: WordN n -> IntN n

toUnsigned :: IntN n -> WordN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

con :: IntN n -> SymIntN n

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

sym :: Symbol -> SymIntN n

ssym :: Identifier -> SymIntN n

isym :: Identifier -> Int -> SymIntN n

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

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

Methods

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

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

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

Methods

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

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

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

Methods

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

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

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

Methods

toSym :: IntN n -> IntN n

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

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

Methods

toSym :: IntN n -> SymIntN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

type NonFuncSBVBaseType _1 (IntN w)

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

type NonFuncSBVBaseType _1 (IntN w) = IntN w

type PrimConstraint _1 (IntN w)

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)

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

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

type Rep (IntN n)

Defined in Grisette.Internal.SymPrim.BV

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

type SymType (IntN n)

Defined in Grisette.Internal.SymPrim.SymBV

type SymType (IntN n) = SymIntN n

data WordN (n :: Nat)

Symbolic unsigned bit vectors.

Instances

SizedBV WordN

Defined in Grisette.Internal.SymPrim.BV

Methods

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

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

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

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

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

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

PEvalBVTerm WordN

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

Methods

pevalBVConcatTerm :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => Term (WordN l) -> Term (WordN r) -> Term (WordN (l + r))

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

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

sbvBVConcatTerm :: forall (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))

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)

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)

PEvalBVSignConversionTerm WordN IntN

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

Methods

pevalBVToSignedTerm :: forall (n :: Nat). (KnownNat n, 1 <= n) => Term (WordN n) -> Term (IntN n)

pevalBVToUnsignedTerm :: forall (n :: Nat). (KnownNat n, 1 <= n) => Term (IntN n) -> Term (WordN n)

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

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)

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)

Lift (WordN n :: Type)

Defined in Grisette.Internal.SymPrim.BV

Methods

lift :: Quote m => WordN n -> m Exp

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

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

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

Methods

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

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

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

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

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

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

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

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

Methods

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

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

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

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

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

Methods

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

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

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

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

Methods

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

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

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

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

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

Defined in Grisette.Internal.SymPrim.BV

Methods

arbitrary :: Gen (WordN n)

shrink :: WordN n -> [WordN n]

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

Defined in Grisette.Internal.SymPrim.BV

Methods

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

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

xor :: WordN n -> WordN n -> WordN n

complement :: WordN n -> WordN n

shift :: WordN n -> Int -> WordN n

rotate :: WordN n -> Int -> WordN n

zeroBits :: WordN n

bit :: Int -> WordN n

setBit :: WordN n -> Int -> WordN n

clearBit :: WordN n -> Int -> WordN n

complementBit :: WordN n -> Int -> WordN n

testBit :: WordN n -> Int -> Bool

bitSizeMaybe :: WordN n -> Maybe Int

bitSize :: WordN n -> Int

isSigned :: WordN n -> Bool

shiftL :: WordN n -> Int -> WordN n

unsafeShiftL :: WordN n -> Int -> WordN n

shiftR :: WordN n -> Int -> WordN n

unsafeShiftR :: WordN n -> Int -> WordN n

rotateL :: WordN n -> Int -> WordN n

rotateR :: WordN n -> Int -> WordN n

popCount :: WordN n -> Int

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

Defined in Grisette.Internal.SymPrim.BV

Methods

finiteBitSize :: WordN n -> Int

countLeadingZeros :: WordN n -> Int

countTrailingZeros :: WordN n -> Int

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

Defined in Grisette.Internal.SymPrim.BV

Methods

minBound :: WordN n

maxBound :: WordN n

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

Defined in Grisette.Internal.SymPrim.BV

Methods

succ :: WordN n -> WordN n

pred :: WordN n -> WordN n

toEnum :: Int -> WordN n

fromEnum :: WordN n -> Int

enumFrom :: WordN n -> [WordN n]

enumFromThen :: WordN n -> WordN n -> [WordN n]

enumFromTo :: WordN n -> WordN n -> [WordN n]

enumFromThenTo :: WordN n -> WordN n -> WordN n -> [WordN n]

Generic (WordN n)

Defined in Grisette.Internal.SymPrim.BV

Associated Types

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

Methods

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

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

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

Defined in Grisette.Internal.SymPrim.BV

Methods

(+) :: WordN n -> WordN n -> WordN n

(-) :: WordN n -> WordN n -> WordN n

(*) :: WordN n -> WordN n -> WordN n

negate :: WordN n -> WordN n

abs :: WordN n -> WordN n

signum :: WordN n -> WordN n

fromInteger :: Integer -> WordN n

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

Defined in Grisette.Internal.SymPrim.BV

Methods

readsPrec :: Int -> ReadS (WordN n)

readList :: ReadS [WordN n]

readPrec :: ReadPrec (WordN n)

readListPrec :: ReadPrec [WordN n]

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

Defined in Grisette.Internal.SymPrim.BV

Methods

quot :: WordN n -> WordN n -> WordN n

rem :: WordN n -> WordN n -> WordN n

div :: WordN n -> WordN n -> WordN n

mod :: WordN n -> WordN n -> WordN n

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

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

toInteger :: WordN n -> Integer

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

Defined in Grisette.Internal.SymPrim.BV

Methods

toRational :: WordN n -> Rational

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

Defined in Grisette.Internal.SymPrim.BV

Methods

showsPrec :: Int -> WordN n -> ShowS

show :: WordN n -> String

showList :: [WordN n] -> ShowS

NFData (WordN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

rnf :: WordN n -> ()

Eq (WordN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

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

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

Ord (WordN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

compare :: WordN n -> WordN n -> Ordering

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

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

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

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

max :: WordN n -> WordN n -> WordN n

min :: WordN n -> WordN n -> WordN n

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

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

Methods

evaluateSym :: Bool -> Model -> WordN n -> WordN n

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

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

Methods

extractSymbolics :: WordN n -> SymbolSet

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

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

Methods

gpretty :: WordN n -> Doc ann

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

gprettyList :: [WordN n] -> Doc ann

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

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

Methods

rootStrategy :: MergingStrategy (WordN n)

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

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

Methods

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

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

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

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

Methods

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

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

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

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

symCompare :: WordN n -> WordN n -> UnionM Ordering

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

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

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> WordN n -> WordN n

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

Defined in Grisette.Internal.SymPrim.BV

Methods

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

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

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

Defined in Grisette.Internal.SymPrim.BV

Methods

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

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

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

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

Associated Types

type NonFuncSBVBaseType n (WordN w)

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

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

Methods

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

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

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

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

withSbvBitwiseTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (Bits (SBVType n0 (WordN n)) => r) -> r

sbvAndBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

sbvOrBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

sbvXorBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

sbvComplementBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

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

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

Methods

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

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

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

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

withSbvDivModIntegralTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SDivisible (SBVType n0 (WordN n)) => r) -> r

sbvDivIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

sbvModIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

sbvQuotIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

sbvRemIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

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

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

Methods

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

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

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

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

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

withSbvNumTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (Num (SBVType n0 (WordN n)) => r) -> r

sbvAddNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

sbvNegNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

sbvMulNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

sbvAbsNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

sbvSignumNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

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

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

Methods

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

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

withSbvOrdTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (OrdSymbolic (SBVType n0 (WordN n)) => r) -> r

sbvLtOrdTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBV Bool

sbvLeOrdTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBV Bool

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

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

Methods

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

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

withSbvRotateTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SIntegral (NonFuncSBVBaseType n0 (WordN n)) => r) -> r

sbvRotateLeftTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

sbvRotateRightTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

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

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

Methods

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

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

withSbvShiftTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SIntegral (NonFuncSBVBaseType n0 (WordN n)) => r) -> r

sbvShiftLeftTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

sbvShiftRightTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n)

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

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

Associated Types

type SBVType n (WordN w)

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

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

symNonFuncSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBV (NonFuncSBVBaseType n (WordN w)))

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

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

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

Methods

termCache :: Cache (Term (WordN w))

pformatCon :: WordN w -> String

pformatSym :: TypedSymbol (WordN w) -> String

defaultValue :: WordN w

defaultValueDynamic :: proxy (WordN w) -> ModelValue

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

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

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> WordN w -> SBVType n (WordN w)

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

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (WordN w))

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

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (WordN w) -> SBVType n (WordN w) -> SBVType n (WordN w)

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (WordN w) -> SBVType n (WordN w) -> SBV Bool

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

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

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

Associated Types

type PrimConstraint n (WordN w)

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

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type SymType (WordN n)

Hashable (WordN n)

Defined in Grisette.Internal.SymPrim.BV

Methods

hashWithSalt :: Int -> WordN n -> Int

hash :: WordN n -> Int

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

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

Methods

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

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

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

Methods

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

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

Defined in Grisette.Internal.SymPrim.BV

Methods

toSigned :: WordN n -> IntN n

toUnsigned :: IntN n -> WordN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

con :: WordN n -> SymWordN n

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

sym :: Symbol -> SymWordN n

ssym :: Identifier -> SymWordN n

isym :: Identifier -> Int -> SymWordN n

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

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

Methods

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

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

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

Methods

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

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

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

Methods

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

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

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

Methods

toSym :: WordN n -> WordN n

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

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

Methods

toSym :: WordN n -> SymWordN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

type NonFuncSBVBaseType _1 (WordN w)

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

type NonFuncSBVBaseType _1 (WordN w) = WordN w

type PrimConstraint _1 (WordN w)

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)

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

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

type Rep (WordN n)

Defined in Grisette.Internal.SymPrim.BV

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

type SymType (WordN n)

Defined in Grisette.Internal.SymPrim.SymBV

type SymType (WordN n) = SymWordN n

data SomeBV bv where

Non-indexed bitvectors.

Constructors

SomeBV :: (KnownNat n, 1 <= n) => bv n -> SomeBV bv

Instances

(forall (n :: Nat). (KnownNat n, 1 <= n) => GenSym () (bv n), Mergeable (SomeBV bv)) => GenSym Int (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

fresh :: MonadFresh m => Int -> m (UnionM (SomeBV bv))

(forall (n :: Nat). (KnownNat n, 1 <= n) => GenSymSimple () (bv n), Mergeable (SomeBV bv)) => GenSymSimple Int (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

simpleFresh :: MonadFresh m => Int -> m (SomeBV bv)

(forall (n :: Nat). (KnownNat n, 1 <= n) => Lift (bv n)) => Lift (SomeBV bv :: Type)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

lift :: Quote m => SomeBV bv -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => SomeBV bv -> Code m (SomeBV bv)

(forall (n :: Nat). (KnownNat n, 1 <= n) => Bits (bv n)) => Bits (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

(.&.) :: SomeBV bv -> SomeBV bv -> SomeBV bv

(.|.) :: SomeBV bv -> SomeBV bv -> SomeBV bv

xor :: SomeBV bv -> SomeBV bv -> SomeBV bv

complement :: SomeBV bv -> SomeBV bv

shift :: SomeBV bv -> Int -> SomeBV bv

rotate :: SomeBV bv -> Int -> SomeBV bv

zeroBits :: SomeBV bv

bit :: Int -> SomeBV bv

setBit :: SomeBV bv -> Int -> SomeBV bv

clearBit :: SomeBV bv -> Int -> SomeBV bv

complementBit :: SomeBV bv -> Int -> SomeBV bv

testBit :: SomeBV bv -> Int -> Bool

bitSizeMaybe :: SomeBV bv -> Maybe Int

bitSize :: SomeBV bv -> Int

isSigned :: SomeBV bv -> Bool

shiftL :: SomeBV bv -> Int -> SomeBV bv

unsafeShiftL :: SomeBV bv -> Int -> SomeBV bv

shiftR :: SomeBV bv -> Int -> SomeBV bv

unsafeShiftR :: SomeBV bv -> Int -> SomeBV bv

rotateL :: SomeBV bv -> Int -> SomeBV bv

rotateR :: SomeBV bv -> Int -> SomeBV bv

popCount :: SomeBV bv -> Int

(forall (n :: Nat). (KnownNat n, 1 <= n) => FiniteBits (bv n)) => FiniteBits (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

finiteBitSize :: SomeBV bv -> Int

countLeadingZeros :: SomeBV bv -> Int

countTrailingZeros :: SomeBV bv -> Int

(forall (n :: Nat). (KnownNat n, 1 <= n) => Enum (bv n)) => Enum (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

succ :: SomeBV bv -> SomeBV bv

pred :: SomeBV bv -> SomeBV bv

toEnum :: Int -> SomeBV bv

fromEnum :: SomeBV bv -> Int

enumFrom :: SomeBV bv -> [SomeBV bv]

enumFromThen :: SomeBV bv -> SomeBV bv -> [SomeBV bv]

enumFromTo :: SomeBV bv -> SomeBV bv -> [SomeBV bv]

enumFromThenTo :: SomeBV bv -> SomeBV bv -> SomeBV bv -> [SomeBV bv]

(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) => Num (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

(+) :: SomeBV bv -> SomeBV bv -> SomeBV bv

(-) :: SomeBV bv -> SomeBV bv -> SomeBV bv

(*) :: SomeBV bv -> SomeBV bv -> SomeBV bv

negate :: SomeBV bv -> SomeBV bv

abs :: SomeBV bv -> SomeBV bv

signum :: SomeBV bv -> SomeBV bv

fromInteger :: Integer -> SomeBV bv

(forall (n :: Nat). (KnownNat n, 1 <= n) => Integral (bv n)) => Integral (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

quot :: SomeBV bv -> SomeBV bv -> SomeBV bv

rem :: SomeBV bv -> SomeBV bv -> SomeBV bv

div :: SomeBV bv -> SomeBV bv -> SomeBV bv

mod :: SomeBV bv -> SomeBV bv -> SomeBV bv

quotRem :: SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)

divMod :: SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)

toInteger :: SomeBV bv -> Integer

(forall (n :: Nat). (KnownNat n, 1 <= n) => Real (bv n)) => Real (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

toRational :: SomeBV bv -> Rational

(forall (n :: Nat). (KnownNat n, 1 <= n) => Show (bv n)) => Show (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

showsPrec :: Int -> SomeBV bv -> ShowS

show :: SomeBV bv -> String

showList :: [SomeBV bv] -> ShowS

(forall (n :: Nat). (KnownNat n, 1 <= n) => NFData (bv n)) => NFData (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

rnf :: SomeBV bv -> ()

(forall (n :: Nat). (KnownNat n, 1 <= n) => Eq (bv n)) => Eq (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

(==) :: SomeBV bv -> SomeBV bv -> Bool

(/=) :: SomeBV bv -> SomeBV bv -> Bool

(forall (n :: Nat). (KnownNat n, 1 <= n) => Ord (bv n)) => Ord (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

compare :: SomeBV bv -> SomeBV bv -> Ordering

(<) :: SomeBV bv -> SomeBV bv -> Bool

(<=) :: SomeBV bv -> SomeBV bv -> Bool

(>) :: SomeBV bv -> SomeBV bv -> Bool

(>=) :: SomeBV bv -> SomeBV bv -> Bool

max :: SomeBV bv -> SomeBV bv -> SomeBV bv

min :: SomeBV bv -> SomeBV bv -> SomeBV bv

SizedBV bv => BV (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

bvConcat :: SomeBV bv -> SomeBV bv -> SomeBV bv

bvZext :: Int -> SomeBV bv -> SomeBV bv

bvSext :: Int -> SomeBV bv -> SomeBV bv

bvExt :: Int -> SomeBV bv -> SomeBV bv

bvSelect :: Int -> Int -> SomeBV bv -> SomeBV bv

bv :: Integral a => Int -> a -> SomeBV bv

(forall (n :: Nat). (KnownNat n, 1 <= n) => EvaluateSym (bv n)) => EvaluateSym (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

evaluateSym :: Bool -> Model -> SomeBV bv -> SomeBV bv

(forall (n :: Nat). (KnownNat n, 1 <= n) => ExtractSymbolics (bv n)) => ExtractSymbolics (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

extractSymbolics :: SomeBV bv -> SymbolSet

(forall (n :: Nat). (KnownNat n, 1 <= n) => GPretty (bv n)) => GPretty (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

gpretty :: SomeBV bv -> Doc ann

gprettyPrec :: Int -> SomeBV bv -> Doc ann

gprettyList :: [SomeBV bv] -> Doc ann

(forall (n :: Nat). (KnownNat n, 1 <= n) => ITEOp (bv n)) => ITEOp (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

symIte :: SymBool -> SomeBV bv -> SomeBV bv -> SomeBV bv

(forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) => Mergeable (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

rootStrategy :: MergingStrategy (SomeBV bv)

(forall (n :: Nat). (KnownNat n, 1 <= n) => SEq (bv n)) => SEq (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

(.==) :: SomeBV bv -> SomeBV bv -> SymBool

(./=) :: SomeBV bv -> SomeBV bv -> SymBool

(forall (n :: Nat). (KnownNat n, 1 <= n) => SOrd (bv n)) => SOrd (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

(.<) :: SomeBV bv -> SomeBV bv -> SymBool

(.<=) :: SomeBV bv -> SomeBV bv -> SymBool

(.>) :: SomeBV bv -> SomeBV bv -> SymBool

(.>=) :: SomeBV bv -> SomeBV bv -> SymBool

symCompare :: SomeBV bv -> SomeBV bv -> UnionM Ordering

(forall (n :: Nat). (KnownNat n, 1 <= n) => SubstituteSym (bv n)) => SubstituteSym (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SomeBV bv -> SomeBV bv

(forall (n :: Nat). (KnownNat n, 1 <= n) => SymRotate (bv n)) => SymRotate (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

symRotate :: SomeBV bv -> SomeBV bv -> SomeBV bv

symRotateNegated :: SomeBV bv -> SomeBV bv -> SomeBV bv

(forall (n :: Nat). (KnownNat n, 1 <= n) => SymShift (bv n)) => SymShift (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

symShift :: SomeBV bv -> SomeBV bv -> SomeBV bv

symShiftNegated :: SomeBV bv -> SomeBV bv -> SomeBV bv

(forall (n :: Nat). (KnownNat n, 1 <= n) => AllSyms (bv n)) => AllSyms (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

allSymsS :: SomeBV bv -> [SomeSym] -> [SomeSym]

allSyms :: SomeBV bv -> [SomeSym]

(forall (n :: Nat). (KnownNat n, 1 <= n) => Hashable (bv n)) => Hashable (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

hashWithSalt :: Int -> SomeBV bv -> Int

hash :: SomeBV bv -> Int

(forall (m :: Nat). (KnownNat m, 1 <= m) => GenSym () (bv m), Mergeable (SomeBV bv)) => GenSym (SomeBV bv) (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

fresh :: MonadFresh m => SomeBV bv -> m (UnionM (SomeBV bv))

(forall (m :: Nat). (KnownNat m, 1 <= m) => GenSymSimple () (bv m), Mergeable (SomeBV bv)) => GenSymSimple (SomeBV bv) (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

simpleFresh :: MonadFresh m => SomeBV bv -> m (SomeBV bv)

(forall (n :: Nat). (KnownNat n, 1 <= n) => SignConversion (ubv n) (sbv n), SignConversion (ubv 1) (sbv 1)) => SignConversion (SomeBV ubv) (SomeBV sbv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

toSigned :: SomeBV ubv -> SomeBV sbv

toUnsigned :: SomeBV sbv -> SomeBV ubv

(forall (n :: Nat). (KnownNat n, 1 <= n) => ToCon (sbv n) (cbv n)) => ToCon (SomeBV sbv) (SomeBV cbv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

toCon :: SomeBV sbv -> Maybe (SomeBV cbv)

(forall (n :: Nat). (KnownNat n, 1 <= n) => ToSym (cbv n) (sbv n)) => ToSym (SomeBV cbv) (SomeBV sbv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

toSym :: SomeBV cbv -> SomeBV sbv

(KnownNat n, 1 <= n, forall (m :: Nat). (KnownNat m, 1 <= m) => GenSym () (bv m), Mergeable (SomeBV bv)) => GenSym (Proxy n) (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

fresh :: MonadFresh m => Proxy n -> m (UnionM (SomeBV bv))

(KnownNat n, 1 <= n, forall (m :: Nat). (KnownNat m, 1 <= m) => GenSymSimple () (bv m), Mergeable (SomeBV bv)) => GenSymSimple (Proxy n) (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

simpleFresh :: MonadFresh m => Proxy n -> m (SomeBV bv)

(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

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

safeDiv :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeMod :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeDivMod :: SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)

safeQuot :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeRem :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeQuotRem :: SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)

(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

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

safeAdd :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeNeg :: SomeBV bv -> m (SomeBV bv)

safeSub :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

(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

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

safeSymRotateL :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeSymRotateR :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

(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

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

safeSymShiftL :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeSymShiftR :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeSymStrictShiftL :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeSymStrictShiftR :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

data BitwidthMismatch

Constructors

BitwidthMismatch

Instances

Exception BitwidthMismatch

Defined in Grisette.Internal.SymPrim.BV

Methods

toException :: BitwidthMismatch -> SomeException

fromException :: SomeException -> Maybe BitwidthMismatch

displayException :: BitwidthMismatch -> String

Generic BitwidthMismatch

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

Defined in Grisette.Internal.SymPrim.BV

Methods

showsPrec :: Int -> BitwidthMismatch -> ShowS

show :: BitwidthMismatch -> String

showList :: [BitwidthMismatch] -> ShowS

Eq BitwidthMismatch

Defined in Grisette.Internal.SymPrim.BV

Methods

(==) :: BitwidthMismatch -> BitwidthMismatch -> Bool

(/=) :: BitwidthMismatch -> BitwidthMismatch -> Bool

Ord BitwidthMismatch

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

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

Methods

rootStrategy :: MergingStrategy BitwidthMismatch

(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

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

safeDiv :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeMod :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeDivMod :: SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)

safeQuot :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeRem :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeQuotRem :: SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)

(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

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

safeAdd :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeNeg :: SomeBV bv -> m (SomeBV bv)

safeSub :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

(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

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

safeSymRotateL :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeSymRotateR :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

(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

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

safeSymShiftL :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeSymShiftR :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeSymStrictShiftL :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeSymStrictShiftR :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

type Rep BitwidthMismatch

Defined in Grisette.Internal.SymPrim.BV

type Rep BitwidthMismatch = D1 ('MetaData "BitwidthMismatch" "Grisette.Internal.SymPrim.BV" "grisette-0.5.0.1-IKpKourvCOdG0l1QW5fLHa" 'False) (C1 ('MetaCons "BitwidthMismatch" 'PrefixI 'False) (U1 :: Type -> Type))

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

Pattern synonym for SomeBV with concrete signed bitvectors.

type SomeIntN = SomeBV IntN

Type synonym for SomeBV with concrete signed bitvectors.

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

Pattern synonym for SomeBV with concrete unsigned bitvectors.

type SomeWordN = SomeBV WordN

Type synonym for SomeBV with concrete unsigned bitvectors.

data a =-> b infixr 0

Functions as a table. Use the # operator to apply the function.

>>> :set -XTypeOperators
>>> let f = TabularFun [(1, 2), (3, 4)] 0 :: Int =-> Int
>>> f # 1
2
>>> f # 2
0
>>> f # 3
4

Constructors

TabularFun

Fields

• funcTable :: [(a, b)]
• defaultFuncValue :: b

Instances

Generic1 ((=->) a :: Type -> Type)

Defined in Grisette.Internal.SymPrim.TabularFun

Associated Types

type Rep1 ((=->) a) :: k -> Type

Methods

from1 :: forall (a0 :: k). (a =-> a0) -> Rep1 ((=->) a) a0

to1 :: forall (a0 :: k). Rep1 ((=->) a) a0 -> a =-> a0

(Lift a, Lift b) => Lift (a =-> b :: Type)

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

lift :: Quote m => (a =-> b) -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => (a =-> b) -> Code m (a =-> b)

NFData a => NFData1 ((=->) a)

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

liftRnf :: (a0 -> ()) -> (a =-> a0) -> ()

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => ToSym (UnionM (ca =-> cb)) (sa =~> sb)

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

Methods

toSym :: UnionM (ca =-> cb) -> sa =~> sb

Generic (a =-> b)

Defined in Grisette.Internal.SymPrim.TabularFun

Associated Types

type Rep (a =-> b) :: Type -> Type

Methods

from :: (a =-> b) -> Rep (a =-> b) x

to :: Rep (a =-> b) x -> a =-> b

(Show a, Show b) => Show (a =-> b)

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

showsPrec :: Int -> (a =-> b) -> ShowS

show :: (a =-> b) -> String

showList :: [a =-> b] -> ShowS

(NFData a, NFData b) => NFData (a =-> b)

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

rnf :: (a =-> b) -> ()

(Eq a, Eq b) => Eq (a =-> b)

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

(==) :: (a =-> b) -> (a =-> b) -> Bool

(/=) :: (a =-> b) -> (a =-> b) -> Bool

(SupportedNonFuncPrim a, SupportedPrim b) => SBVRep (a =-> b)

Defined in Grisette.Internal.SymPrim.TabularFun

Associated Types

type SBVType n (a =-> b)

(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedNonFuncPrim f, SupportedNonFuncPrim g, SupportedNonFuncPrim h, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e, SupportedPrim f, SupportedPrim g, SupportedPrim h) => SupportedPrim (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

termCache :: Cache (Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))

pformatCon :: (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> String

pformatSym :: TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> String

defaultValue :: a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))

defaultValueDynamic :: proxy (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))

pevalEqTerm :: Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))

symSBVName :: TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))), SMTDefinable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))), Mergeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))), Typeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))

(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedNonFuncPrim f, SupportedNonFuncPrim g, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e, SupportedPrim f, SupportedPrim g) => SupportedPrim (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

termCache :: Cache (Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))

pformatCon :: (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> String

pformatSym :: TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> String

defaultValue :: a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))

defaultValueDynamic :: proxy (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))

pevalEqTerm :: Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))

symSBVName :: TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))), SMTDefinable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))), Mergeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))), Typeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))

(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedNonFuncPrim f, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e, SupportedPrim f) => SupportedPrim (a =-> (b =-> (c =-> (d =-> (e =-> f)))))

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

termCache :: Cache (Term (a =-> (b =-> (c =-> (d =-> (e =-> f))))))

pformatCon :: (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> String

pformatSym :: TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> String

defaultValue :: a =-> (b =-> (c =-> (d =-> (e =-> f))))

defaultValueDynamic :: proxy (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> f)))))

pevalEqTerm :: Term (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))

symSBVName :: TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a =-> (b =-> (c =-> (d =-> (e =-> f))))), SMTDefinable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))), Mergeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))), Typeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> (d =-> (e =-> f))))

(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e) => SupportedPrim (a =-> (b =-> (c =-> (d =-> e))))

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

termCache :: Cache (Term (a =-> (b =-> (c =-> (d =-> e)))))

pformatCon :: (a =-> (b =-> (c =-> (d =-> e)))) -> String

pformatSym :: TypedSymbol (a =-> (b =-> (c =-> (d =-> e)))) -> String

defaultValue :: a =-> (b =-> (c =-> (d =-> e)))

defaultValueDynamic :: proxy (a =-> (b =-> (c =-> (d =-> e)))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a =-> (b =-> (c =-> (d =-> e)))) -> Term (a =-> (b =-> (c =-> (d =-> e)))) -> Term (a =-> (b =-> (c =-> (d =-> e))))

pevalEqTerm :: Term (a =-> (b =-> (c =-> (d =-> e)))) -> Term (a =-> (b =-> (c =-> (d =-> e)))) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a =-> (b =-> (c =-> (d =-> e)))) -> SBVType n (a =-> (b =-> (c =-> (d =-> e))))

symSBVName :: TypedSymbol (a =-> (b =-> (c =-> (d =-> e)))) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a =-> (b =-> (c =-> (d =-> e)))), SMTDefinable (SBVType n (a =-> (b =-> (c =-> (d =-> e))))), Mergeable (SBVType n (a =-> (b =-> (c =-> (d =-> e))))), Typeable (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a =-> (b =-> (c =-> (d =-> e)))) -> SBVType n (a =-> (b =-> (c =-> (d =-> e)))) -> SBVType n (a =-> (b =-> (c =-> (d =-> e))))

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a =-> (b =-> (c =-> (d =-> e)))) -> SBVType n (a =-> (b =-> (c =-> (d =-> e)))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> (d =-> e)))

(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d) => SupportedPrim (a =-> (b =-> (c =-> d)))

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

termCache :: Cache (Term (a =-> (b =-> (c =-> d))))

pformatCon :: (a =-> (b =-> (c =-> d))) -> String

pformatSym :: TypedSymbol (a =-> (b =-> (c =-> d))) -> String

defaultValue :: a =-> (b =-> (c =-> d))

defaultValueDynamic :: proxy (a =-> (b =-> (c =-> d))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a =-> (b =-> (c =-> d))) -> Term (a =-> (b =-> (c =-> d))) -> Term (a =-> (b =-> (c =-> d)))

pevalEqTerm :: Term (a =-> (b =-> (c =-> d))) -> Term (a =-> (b =-> (c =-> d))) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a =-> (b =-> (c =-> d))) -> SBVType n (a =-> (b =-> (c =-> d)))

symSBVName :: TypedSymbol (a =-> (b =-> (c =-> d))) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a =-> (b =-> (c =-> d))))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a =-> (b =-> (c =-> d))), SMTDefinable (SBVType n (a =-> (b =-> (c =-> d)))), Mergeable (SBVType n (a =-> (b =-> (c =-> d)))), Typeable (SBVType n (a =-> (b =-> (c =-> d))))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a =-> (b =-> (c =-> d))) -> SBVType n (a =-> (b =-> (c =-> d))) -> SBVType n (a =-> (b =-> (c =-> d)))

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a =-> (b =-> (c =-> d))) -> SBVType n (a =-> (b =-> (c =-> d))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> d))

(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedPrim a, SupportedPrim b, SupportedPrim c) => SupportedPrim (a =-> (b =-> c))

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

termCache :: Cache (Term (a =-> (b =-> c)))

pformatCon :: (a =-> (b =-> c)) -> String

pformatSym :: TypedSymbol (a =-> (b =-> c)) -> String

defaultValue :: a =-> (b =-> c)

defaultValueDynamic :: proxy (a =-> (b =-> c)) -> ModelValue

pevalITETerm :: Term Bool -> Term (a =-> (b =-> c)) -> Term (a =-> (b =-> c)) -> Term (a =-> (b =-> c))

pevalEqTerm :: Term (a =-> (b =-> c)) -> Term (a =-> (b =-> c)) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a =-> (b =-> c)) -> SBVType n (a =-> (b =-> c))

symSBVName :: TypedSymbol (a =-> (b =-> c)) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a =-> (b =-> c)))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a =-> (b =-> c)), SMTDefinable (SBVType n (a =-> (b =-> c))), Mergeable (SBVType n (a =-> (b =-> c))), Typeable (SBVType n (a =-> (b =-> c)))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a =-> (b =-> c)) -> SBVType n (a =-> (b =-> c)) -> SBVType n (a =-> (b =-> c))

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a =-> (b =-> c)) -> SBVType n (a =-> (b =-> c)) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> (b =-> c)

(SupportedNonFuncPrim a, SupportedNonFuncPrim b) => SupportedPrim (a =-> b)

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

termCache :: Cache (Term (a =-> b))

pformatCon :: (a =-> b) -> String

pformatSym :: TypedSymbol (a =-> b) -> String

defaultValue :: a =-> b

defaultValueDynamic :: proxy (a =-> b) -> ModelValue

pevalITETerm :: Term Bool -> Term (a =-> b) -> Term (a =-> b) -> Term (a =-> b)

pevalEqTerm :: Term (a =-> b) -> Term (a =-> b) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a =-> b) -> SBVType n (a =-> b)

symSBVName :: TypedSymbol (a =-> b) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a =-> b))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a =-> b), SMTDefinable (SBVType n (a =-> b)), Mergeable (SBVType n (a =-> b)), Typeable (SBVType n (a =-> b))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a =-> b) -> SBVType n (a =-> b) -> SBVType n (a =-> b)

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a =-> b) -> SBVType n (a =-> b) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> b

(SupportedNonFuncPrim a, SupportedPrim b) => SupportedPrimConstraint (a =-> b)

Defined in Grisette.Internal.SymPrim.TabularFun

Associated Types

type PrimConstraint n (a =-> b)

(SymRep a, SymRep b, SupportedPrim (a =-> b)) => SymRep (a =-> b)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Associated Types

type SymType (a =-> b)

(Hashable a, Hashable b) => Hashable (a =-> b)

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

hashWithSalt :: Int -> (a =-> b) -> Int

hash :: (a =-> b) -> Int

Eq a => Function (a =-> b) a b

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

(#) :: (a =-> b) -> a -> b

(SupportedPrim a, SupportedPrim b, SupportedPrim (a =-> b)) => PEvalApplyTerm (a =-> b) a b

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

pevalApplyTerm :: Term (a =-> b) -> Term a -> Term b

sbvApplyTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a =-> b) -> SBVType n a -> SBVType n b

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca =-> cb)) => Solvable (ca =-> cb) (sa =~> sb)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

con :: (ca =-> cb) -> sa =~> sb

conView :: (sa =~> sb) -> Maybe (ca =-> cb)

sym :: Symbol -> sa =~> sb

ssym :: Identifier -> sa =~> sb

isym :: Identifier -> Int -> sa =~> sb

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => ToCon (sa =~> sb) (ca =-> cb)

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

Methods

toCon :: (sa =~> sb) -> Maybe (ca =-> cb)

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => ToSym (ca =-> cb) (sa =~> sb)

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

Methods

toSym :: (ca =-> cb) -> sa =~> sb

(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca =-> cb)) => LinkedRep (ca =-> cb) (sa =~> sb)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

underlyingTerm :: (sa =~> sb) -> Term (ca =-> cb)

wrapTerm :: Term (ca =-> cb) -> sa =~> sb

type Rep1 ((=->) a :: Type -> Type)

Defined in Grisette.Internal.SymPrim.TabularFun

type Rep1 ((=->) a :: Type -> Type) = D1 ('MetaData "=->" "Grisette.Internal.SymPrim.TabularFun" "grisette-0.5.0.1-IKpKourvCOdG0l1QW5fLHa" 'False) (C1 ('MetaCons "TabularFun" 'PrefixI 'True) (S1 ('MetaSel ('Just "funcTable") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (List :.: Rec1 ((,) a)) :*: S1 ('MetaSel ('Just "defaultFuncValue") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1))

type PrimConstraint n (a =-> b)

Defined in Grisette.Internal.SymPrim.TabularFun

type PrimConstraint n (a =-> b) = (SupportedNonFuncPrim a, SupportedPrim b, PrimConstraint n b)

type SBVType n (a =-> b)

Defined in Grisette.Internal.SymPrim.TabularFun

type SBVType n (a =-> b) = SBV (NonFuncSBVBaseType n a) -> SBVType n b

type Rep (a =-> b)

Defined in Grisette.Internal.SymPrim.TabularFun

type Rep (a =-> b) = D1 ('MetaData "=->" "Grisette.Internal.SymPrim.TabularFun" "grisette-0.5.0.1-IKpKourvCOdG0l1QW5fLHa" 'False) (C1 ('MetaCons "TabularFun" 'PrefixI 'True) (S1 ('MetaSel ('Just "funcTable") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(a, b)]) :*: S1 ('MetaSel ('Just "defaultFuncValue") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 b)))

type SymType (a =-> b)

Defined in Grisette.Internal.SymPrim.SymTabularFun

type SymType (a =-> b) = SymType a =~> SymType b

data a --> b infixr 0

General symbolic function type. Use the # operator to apply the function. Note that this function should be applied to symbolic values only. It is by itself already a symbolic value, but can be considered partially concrete as the function body is specified. Use -~> for uninterpreted general symbolic functions.

The result would be partially evaluated.

>>> :set -XOverloadedStrings
>>> :set -XTypeOperators
>>> let f = ("x" :: TypedSymbol Integer) --> ("x" + 1 + "y" :: SymInteger) :: Integer --> Integer
>>> f # 1    -- 1 has the type SymInteger
(+ 2 y)
>>> f # "a"  -- "a" has the type SymInteger
(+ 1 (+ a y))

Instances

Lift (a --> b :: Type)

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

lift :: Quote m => (a --> b) -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => (a --> b) -> Code m (a --> b)

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => ToSym (UnionM (ca --> cb)) (sa -~> sb)

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

Methods

toSym :: UnionM (ca --> cb) -> sa -~> sb

Show (a --> b)

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

showsPrec :: Int -> (a --> b) -> ShowS

show :: (a --> b) -> String

showList :: [a --> b] -> ShowS

NFData (a --> b)

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

rnf :: (a --> b) -> ()

Eq (a --> b)

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

(==) :: (a --> b) -> (a --> b) -> Bool

(/=) :: (a --> b) -> (a --> b) -> Bool

(SupportedNonFuncPrim a, SupportedPrim b) => SBVRep (a --> b)

Defined in Grisette.Internal.SymPrim.GeneralFun

Associated Types

type SBVType n (a --> b)

(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedNonFuncPrim f, SupportedNonFuncPrim g, SupportedNonFuncPrim h, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e, SupportedPrim f, SupportedPrim g, SupportedPrim h) => SupportedPrim (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

termCache :: Cache (Term (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))))

pformatCon :: (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> String

pformatSym :: TypedSymbol (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> String

defaultValue :: a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))

defaultValueDynamic :: proxy (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> Term (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> Term (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))

pevalEqTerm :: Term (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> Term (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))

symSBVName :: TypedSymbol (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))), SMTDefinable (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))), Mergeable (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))), Typeable (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))

(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedNonFuncPrim f, SupportedNonFuncPrim g, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e, SupportedPrim f, SupportedPrim g) => SupportedPrim (a --> (b --> (c --> (d --> (e --> (f --> g))))))

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

termCache :: Cache (Term (a --> (b --> (c --> (d --> (e --> (f --> g)))))))

pformatCon :: (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> String

pformatSym :: TypedSymbol (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> String

defaultValue :: a --> (b --> (c --> (d --> (e --> (f --> g)))))

defaultValueDynamic :: proxy (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> Term (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> Term (a --> (b --> (c --> (d --> (e --> (f --> g))))))

pevalEqTerm :: Term (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> Term (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g))))))

symSBVName :: TypedSymbol (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> (b --> (c --> (d --> (e --> (f --> g)))))), SMTDefinable (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g))))))), Mergeable (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g))))))), Typeable (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g))))))

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> (b --> (c --> (d --> (e --> (f --> g)))))

(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedNonFuncPrim f, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e, SupportedPrim f) => SupportedPrim (a --> (b --> (c --> (d --> (e --> f)))))

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

termCache :: Cache (Term (a --> (b --> (c --> (d --> (e --> f))))))

pformatCon :: (a --> (b --> (c --> (d --> (e --> f))))) -> String

pformatSym :: TypedSymbol (a --> (b --> (c --> (d --> (e --> f))))) -> String

defaultValue :: a --> (b --> (c --> (d --> (e --> f))))

defaultValueDynamic :: proxy (a --> (b --> (c --> (d --> (e --> f))))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a --> (b --> (c --> (d --> (e --> f))))) -> Term (a --> (b --> (c --> (d --> (e --> f))))) -> Term (a --> (b --> (c --> (d --> (e --> f)))))

pevalEqTerm :: Term (a --> (b --> (c --> (d --> (e --> f))))) -> Term (a --> (b --> (c --> (d --> (e --> f))))) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> (b --> (c --> (d --> (e --> f))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> f)))))

symSBVName :: TypedSymbol (a --> (b --> (c --> (d --> (e --> f))))) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> (b --> (c --> (d --> (e --> f))))))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> (b --> (c --> (d --> (e --> f))))), SMTDefinable (SBVType n (a --> (b --> (c --> (d --> (e --> f)))))), Mergeable (SBVType n (a --> (b --> (c --> (d --> (e --> f)))))), Typeable (SBVType n (a --> (b --> (c --> (d --> (e --> f))))))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> (b --> (c --> (d --> (e --> f))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> f))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> f)))))

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> (b --> (c --> (d --> (e --> f))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> f))))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> (b --> (c --> (d --> (e --> f))))

(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e) => SupportedPrim (a --> (b --> (c --> (d --> e))))

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

termCache :: Cache (Term (a --> (b --> (c --> (d --> e)))))

pformatCon :: (a --> (b --> (c --> (d --> e)))) -> String

pformatSym :: TypedSymbol (a --> (b --> (c --> (d --> e)))) -> String

defaultValue :: a --> (b --> (c --> (d --> e)))

defaultValueDynamic :: proxy (a --> (b --> (c --> (d --> e)))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a --> (b --> (c --> (d --> e)))) -> Term (a --> (b --> (c --> (d --> e)))) -> Term (a --> (b --> (c --> (d --> e))))

pevalEqTerm :: Term (a --> (b --> (c --> (d --> e)))) -> Term (a --> (b --> (c --> (d --> e)))) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> (b --> (c --> (d --> e)))) -> SBVType n (a --> (b --> (c --> (d --> e))))

symSBVName :: TypedSymbol (a --> (b --> (c --> (d --> e)))) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> (b --> (c --> (d --> e)))))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> (b --> (c --> (d --> e)))), SMTDefinable (SBVType n (a --> (b --> (c --> (d --> e))))), Mergeable (SBVType n (a --> (b --> (c --> (d --> e))))), Typeable (SBVType n (a --> (b --> (c --> (d --> e)))))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> (b --> (c --> (d --> e)))) -> SBVType n (a --> (b --> (c --> (d --> e)))) -> SBVType n (a --> (b --> (c --> (d --> e))))

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> (b --> (c --> (d --> e)))) -> SBVType n (a --> (b --> (c --> (d --> e)))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> (b --> (c --> (d --> e)))

(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d) => SupportedPrim (a --> (b --> (c --> d)))

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

termCache :: Cache (Term (a --> (b --> (c --> d))))

pformatCon :: (a --> (b --> (c --> d))) -> String

pformatSym :: TypedSymbol (a --> (b --> (c --> d))) -> String

defaultValue :: a --> (b --> (c --> d))

defaultValueDynamic :: proxy (a --> (b --> (c --> d))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a --> (b --> (c --> d))) -> Term (a --> (b --> (c --> d))) -> Term (a --> (b --> (c --> d)))

pevalEqTerm :: Term (a --> (b --> (c --> d))) -> Term (a --> (b --> (c --> d))) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> (b --> (c --> d))) -> SBVType n (a --> (b --> (c --> d)))

symSBVName :: TypedSymbol (a --> (b --> (c --> d))) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> (b --> (c --> d))))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> (b --> (c --> d))), SMTDefinable (SBVType n (a --> (b --> (c --> d)))), Mergeable (SBVType n (a --> (b --> (c --> d)))), Typeable (SBVType n (a --> (b --> (c --> d))))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> (b --> (c --> d))) -> SBVType n (a --> (b --> (c --> d))) -> SBVType n (a --> (b --> (c --> d)))

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> (b --> (c --> d))) -> SBVType n (a --> (b --> (c --> d))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> (b --> (c --> d))

(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedPrim a, SupportedPrim b, SupportedPrim c) => SupportedPrim (a --> (b --> c))

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

termCache :: Cache (Term (a --> (b --> c)))

pformatCon :: (a --> (b --> c)) -> String

pformatSym :: TypedSymbol (a --> (b --> c)) -> String

defaultValue :: a --> (b --> c)

defaultValueDynamic :: proxy (a --> (b --> c)) -> ModelValue

pevalITETerm :: Term Bool -> Term (a --> (b --> c)) -> Term (a --> (b --> c)) -> Term (a --> (b --> c))

pevalEqTerm :: Term (a --> (b --> c)) -> Term (a --> (b --> c)) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> (b --> c)) -> SBVType n (a --> (b --> c))

symSBVName :: TypedSymbol (a --> (b --> c)) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> (b --> c)))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> (b --> c)), SMTDefinable (SBVType n (a --> (b --> c))), Mergeable (SBVType n (a --> (b --> c))), Typeable (SBVType n (a --> (b --> c)))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> (b --> c)) -> SBVType n (a --> (b --> c)) -> SBVType n (a --> (b --> c))

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> (b --> c)) -> SBVType n (a --> (b --> c)) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> (b --> c)

(SupportedNonFuncPrim a, SupportedNonFuncPrim b) => SupportedPrim (a --> b)

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

termCache :: Cache (Term (a --> b))

pformatCon :: (a --> b) -> String

pformatSym :: TypedSymbol (a --> b) -> String

defaultValue :: a --> b

defaultValueDynamic :: proxy (a --> b) -> ModelValue

pevalITETerm :: Term Bool -> Term (a --> b) -> Term (a --> b) -> Term (a --> b)

pevalEqTerm :: Term (a --> b) -> Term (a --> b) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> b) -> SBVType n (a --> b)

symSBVName :: TypedSymbol (a --> b) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> b))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> b), SMTDefinable (SBVType n (a --> b)), Mergeable (SBVType n (a --> b)), Typeable (SBVType n (a --> b))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> b) -> SBVType n (a --> b) -> SBVType n (a --> b)

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> b) -> SBVType n (a --> b) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> b

(SupportedNonFuncPrim a, SupportedPrim b) => SupportedPrimConstraint (a --> b)

Defined in Grisette.Internal.SymPrim.GeneralFun

Associated Types

type PrimConstraint n (a --> b)

(SymRep ca, SymRep cb, SupportedPrim (ca --> cb)) => SymRep (ca --> cb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Associated Types

type SymType (ca --> cb)

Hashable (a --> b)

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

hashWithSalt :: Int -> (a --> b) -> Int

hash :: (a --> b) -> Int

(LinkedRep a sa, LinkedRep b sb) => Function (a --> b) sa sb

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

(#) :: (a --> b) -> sa -> sb

(SupportedPrim (a --> b), SupportedNonFuncPrim a, SupportedPrim b) => PEvalApplyTerm (a --> b) a b

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

pevalApplyTerm :: Term (a --> b) -> Term a -> Term b

sbvApplyTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> b) -> SBVType n a -> SBVType n b

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca --> cb)) => Solvable (ca --> cb) (sa -~> sb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

con :: (ca --> cb) -> sa -~> sb

conView :: (sa -~> sb) -> Maybe (ca --> cb)

sym :: Symbol -> sa -~> sb

ssym :: Identifier -> sa -~> sb

isym :: Identifier -> Int -> sa -~> sb

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => ToCon (sa -~> sb) (ca --> cb)

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

Methods

toCon :: (sa -~> sb) -> Maybe (ca --> cb)

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => ToSym (ca --> cb) (sa -~> sb)

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

Methods

toSym :: (ca --> cb) -> sa -~> sb

(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim ca, SupportedPrim cb, SupportedPrim (ca --> cb)) => LinkedRep (ca --> cb) (sa -~> sb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

underlyingTerm :: (sa -~> sb) -> Term (ca --> cb)

wrapTerm :: Term (ca --> cb) -> sa -~> sb

type PrimConstraint n (a --> b)

Defined in Grisette.Internal.SymPrim.GeneralFun

type PrimConstraint n (a --> b) = (SupportedNonFuncPrim a, SupportedPrim b, PrimConstraint n b, SBVType n (a --> b) ~ (SBV (NonFuncSBVBaseType n a) -> SBVType n b))

type SBVType n (a --> b)

Defined in Grisette.Internal.SymPrim.GeneralFun

type SBVType n (a --> b) = SBV (NonFuncSBVBaseType n a) -> SBVType n b

type SymType (ca --> cb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

type SymType (ca --> cb) = SymType ca -~> SymType cb

(-->) :: (SupportedPrim ca, SupportedPrim cb, LinkedRep cb sb) => TypedSymbol ca -> sb -> ca --> cb infixr 0

Construction of general symbolic functions.

>>> f = "a" --> "a" + 1 :: Integer --> Integer
>>> f
\(a:ARG :: Integer) -> (+ 1 a:ARG)

This general symbolic function needs to be applied to symbolic values: >>> f # ("a" :: SymInteger) (+ 1 a)

unsafeSomeBV :: forall bv. Int -> (forall proxy n. (KnownNat n, 1 <= n) => proxy n -> bv n) -> SomeBV bv

Construct a SomeBV with a given run-time bitwidth and a polymorphic value for the underlying bitvector.

unarySomeBV :: forall bv r. (forall n. (KnownNat n, 1 <= n) => bv n -> r) -> SomeBV bv -> r

Lift a unary operation on sized bitvectors that returns anything to SomeBV.

unarySomeBVR1 :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n) -> SomeBV bv -> SomeBV bv

Lift a unary operation on sized bitvectors that returns a bitvector to SomeBV. The result will also be wrapped with SomeBV.

binSomeBV :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> r) -> SomeBV bv -> SomeBV bv -> r

Lift a binary operation on sized bitvectors that returns anything to SomeBV. Crash if the bitwidths do not match.

binSomeBVR1 :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> bv n) -> SomeBV bv -> SomeBV bv -> SomeBV bv

Lift a binary operation on sized bitvectors that returns a bitvector to SomeBV. The result will also be wrapped with SomeBV. Crash if the bitwidths do not match.

binSomeBVR2 :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> (bv n, bv n)) -> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)

Lift a binary operation on sized bitvectors that returns two bitvectors to SomeBV. The results will also be wrapped with SomeBV. Crash if the bitwidths do not match.

binSomeBVSafe :: (MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e, Mergeable r) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m r) -> SomeBV bv -> SomeBV bv -> m r

Lift a binary operation on sized bitvectors that returns anything wrapped with ExceptT to SomeBV. If the bitwidths do not match, throw an BitwidthMismatch error to the monadic context.

binSomeBVSafeR1 :: (MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e, forall n. (KnownNat n, 1 <= n) => Mergeable (bv n)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n)) -> SomeBV bv -> SomeBV bv -> m (SomeBV bv)

Lift a binary operation on sized bitvectors that returns a bitvector wrapped with ExceptT to SomeBV. The result will also be wrapped with SomeBV.

If the bitwidths do not match, throw an BitwidthMismatch error to the monadic context.

binSomeBVSafeR2 :: (MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e, forall n. (KnownNat n, 1 <= n) => Mergeable (bv n)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n, bv n)) -> SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)

Lift a binary operation on sized bitvectors that returns two bitvectors wrapped with ExceptT to SomeBV. The results will also be wrapped with SomeBV.

If the bitwidths do not match, throw an BitwidthMismatch error to the monadic context.

conBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV cbv -> SomeBV bv

Construct a symbolic SomeBV with a given concrete SomeBV. Similar to con but for SomeBV.

>>> a = bv 8 0x12 :: SomeIntN
>>> conBV a :: SomeSymIntN
0x12

conBVView :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV bv -> Maybe (SomeBV cbv)

View pattern for symbolic SomeBV to see if it contains a concrete value and extract it. Similar to conView but for SomeBV.

>>> conBVView (bv 8 0x12 :: SomeSymIntN)
Just 0x12
>>> conBVView (ssymBV 4 "a" :: SomeSymIntN)
Nothing

pattern ConBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV cbv -> SomeBV bv

Pattern synonym for symbolic SomeBV to see if it contains a concrete value and extract it. Similar to Con but for SomeBV.

>>> case (bv 8 0x12 :: SomeSymIntN) of { ConBV c -> c; _ -> error "impossible" }
0x12

symBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Symbol -> SomeBV bv

Construct a symbolic SomeBV with a given run-time bitwidth and a symbol. Similar to sym but for SomeBV.

>>> symBV 8 "a" :: SomeSymIntN
a

ssymBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Identifier -> SomeBV bv

Construct a symbolic SomeBV with a given run-time bitwidth and an identifier. Similar to ssym but for SomeBV.

>>> ssymBV 8 "a" :: SomeSymIntN
a

isymBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Identifier -> Int -> SomeBV bv

Construct a symbolic SomeBV with a given run-time bitwidth, an identifier and an index. Similar to isym but for SomeBV.

>>> isymBV 8 "a" 1 :: SomeSymIntN
a@1

arbitraryBV :: forall bv. (forall n. (KnownNat n, 1 <= n) => Arbitrary (bv n)) => Int -> Gen (SomeBV bv)

Generate an arbitrary SomeBV with a given run-time bitwidth.

Symbolic types

class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t, SupportedPrimConstraint t, SBVRep t) => SupportedPrim t

Indicates that a type is supported and can be represented as a symbolic term.

Minimal complete definition

defaultValue, pevalITETerm, pevalEqTerm, conSBVTerm, symSBVName, symSBVTerm, parseSMTModelResult

Instances

SupportedPrim Integer

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

Methods

termCache :: Cache (Term Integer)

pformatCon :: Integer -> String

pformatSym :: TypedSymbol Integer -> String

defaultValue :: Integer

defaultValueDynamic :: proxy Integer -> ModelValue

pevalITETerm :: Term Bool -> Term Integer -> Term Integer -> Term Integer

pevalEqTerm :: Term Integer -> Term Integer -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> Integer -> SBVType n Integer

symSBVName :: TypedSymbol Integer -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n Integer)

withPrim :: forall (n :: Nat) p a. KnownIsZero n => p n -> ((PrimConstraint n Integer, SMTDefinable (SBVType n Integer), Mergeable (SBVType n Integer), Typeable (SBVType n Integer)) => a) -> a

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n Integer -> SBVType n Integer -> SBVType n Integer

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n Integer -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> Integer

SupportedPrim Bool

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

termCache :: Cache (Term Bool)

pformatCon :: Bool -> String

pformatSym :: TypedSymbol Bool -> String

defaultValue :: Bool

defaultValueDynamic :: proxy Bool -> ModelValue

pevalITETerm :: Term Bool -> Term Bool -> Term Bool -> Term Bool

pevalEqTerm :: Term Bool -> Term Bool -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> Bool -> SBVType n Bool

symSBVName :: TypedSymbol Bool -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n Bool)

withPrim :: forall (n :: Nat) p a. KnownIsZero n => p n -> ((PrimConstraint n Bool, SMTDefinable (SBVType n Bool), Mergeable (SBVType n Bool), Typeable (SBVType n Bool)) => a) -> a

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n Bool -> SBVType n Bool -> SBVType n Bool

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n Bool -> SBVType n Bool -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> Bool

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

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

Methods

termCache :: Cache (Term (IntN w))

pformatCon :: IntN w -> String

pformatSym :: TypedSymbol (IntN w) -> String

defaultValue :: IntN w

defaultValueDynamic :: proxy (IntN w) -> ModelValue

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

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

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> IntN w -> SBVType n (IntN w)

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

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (IntN w))

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

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (IntN w) -> SBVType n (IntN w) -> SBVType n (IntN w)

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (IntN w) -> SBVType n (IntN w) -> SBV Bool

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

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

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

Methods

termCache :: Cache (Term (WordN w))

pformatCon :: WordN w -> String

pformatSym :: TypedSymbol (WordN w) -> String

defaultValue :: WordN w

defaultValueDynamic :: proxy (WordN w) -> ModelValue

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

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

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> WordN w -> SBVType n (WordN w)

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

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (WordN w))

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

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (WordN w) -> SBVType n (WordN w) -> SBVType n (WordN w)

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (WordN w) -> SBVType n (WordN w) -> SBV Bool

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

(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedNonFuncPrim f, SupportedNonFuncPrim g, SupportedNonFuncPrim h, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e, SupportedPrim f, SupportedPrim g, SupportedPrim h) => SupportedPrim (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

termCache :: Cache (Term (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))))

pformatCon :: (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> String

pformatSym :: TypedSymbol (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> String

defaultValue :: a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))

defaultValueDynamic :: proxy (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> Term (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> Term (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))

pevalEqTerm :: Term (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> Term (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))

symSBVName :: TypedSymbol (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))), SMTDefinable (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))), Mergeable (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))), Typeable (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))

(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedNonFuncPrim f, SupportedNonFuncPrim g, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e, SupportedPrim f, SupportedPrim g) => SupportedPrim (a --> (b --> (c --> (d --> (e --> (f --> g))))))

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

termCache :: Cache (Term (a --> (b --> (c --> (d --> (e --> (f --> g)))))))

pformatCon :: (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> String

pformatSym :: TypedSymbol (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> String

defaultValue :: a --> (b --> (c --> (d --> (e --> (f --> g)))))

defaultValueDynamic :: proxy (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> Term (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> Term (a --> (b --> (c --> (d --> (e --> (f --> g))))))

pevalEqTerm :: Term (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> Term (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g))))))

symSBVName :: TypedSymbol (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> (b --> (c --> (d --> (e --> (f --> g)))))), SMTDefinable (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g))))))), Mergeable (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g))))))), Typeable (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g))))))

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> (b --> (c --> (d --> (e --> (f --> g)))))

(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedNonFuncPrim f, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e, SupportedPrim f) => SupportedPrim (a --> (b --> (c --> (d --> (e --> f)))))

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

termCache :: Cache (Term (a --> (b --> (c --> (d --> (e --> f))))))

pformatCon :: (a --> (b --> (c --> (d --> (e --> f))))) -> String

pformatSym :: TypedSymbol (a --> (b --> (c --> (d --> (e --> f))))) -> String

defaultValue :: a --> (b --> (c --> (d --> (e --> f))))

defaultValueDynamic :: proxy (a --> (b --> (c --> (d --> (e --> f))))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a --> (b --> (c --> (d --> (e --> f))))) -> Term (a --> (b --> (c --> (d --> (e --> f))))) -> Term (a --> (b --> (c --> (d --> (e --> f)))))

pevalEqTerm :: Term (a --> (b --> (c --> (d --> (e --> f))))) -> Term (a --> (b --> (c --> (d --> (e --> f))))) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> (b --> (c --> (d --> (e --> f))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> f)))))

symSBVName :: TypedSymbol (a --> (b --> (c --> (d --> (e --> f))))) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> (b --> (c --> (d --> (e --> f))))))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> (b --> (c --> (d --> (e --> f))))), SMTDefinable (SBVType n (a --> (b --> (c --> (d --> (e --> f)))))), Mergeable (SBVType n (a --> (b --> (c --> (d --> (e --> f)))))), Typeable (SBVType n (a --> (b --> (c --> (d --> (e --> f))))))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> (b --> (c --> (d --> (e --> f))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> f))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> f)))))

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> (b --> (c --> (d --> (e --> f))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> f))))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> (b --> (c --> (d --> (e --> f))))

(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e) => SupportedPrim (a --> (b --> (c --> (d --> e))))

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

termCache :: Cache (Term (a --> (b --> (c --> (d --> e)))))

pformatCon :: (a --> (b --> (c --> (d --> e)))) -> String

pformatSym :: TypedSymbol (a --> (b --> (c --> (d --> e)))) -> String

defaultValue :: a --> (b --> (c --> (d --> e)))

defaultValueDynamic :: proxy (a --> (b --> (c --> (d --> e)))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a --> (b --> (c --> (d --> e)))) -> Term (a --> (b --> (c --> (d --> e)))) -> Term (a --> (b --> (c --> (d --> e))))

pevalEqTerm :: Term (a --> (b --> (c --> (d --> e)))) -> Term (a --> (b --> (c --> (d --> e)))) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> (b --> (c --> (d --> e)))) -> SBVType n (a --> (b --> (c --> (d --> e))))

symSBVName :: TypedSymbol (a --> (b --> (c --> (d --> e)))) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> (b --> (c --> (d --> e)))))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> (b --> (c --> (d --> e)))), SMTDefinable (SBVType n (a --> (b --> (c --> (d --> e))))), Mergeable (SBVType n (a --> (b --> (c --> (d --> e))))), Typeable (SBVType n (a --> (b --> (c --> (d --> e)))))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> (b --> (c --> (d --> e)))) -> SBVType n (a --> (b --> (c --> (d --> e)))) -> SBVType n (a --> (b --> (c --> (d --> e))))

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> (b --> (c --> (d --> e)))) -> SBVType n (a --> (b --> (c --> (d --> e)))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> (b --> (c --> (d --> e)))

(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d) => SupportedPrim (a --> (b --> (c --> d)))

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

termCache :: Cache (Term (a --> (b --> (c --> d))))

pformatCon :: (a --> (b --> (c --> d))) -> String

pformatSym :: TypedSymbol (a --> (b --> (c --> d))) -> String

defaultValue :: a --> (b --> (c --> d))

defaultValueDynamic :: proxy (a --> (b --> (c --> d))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a --> (b --> (c --> d))) -> Term (a --> (b --> (c --> d))) -> Term (a --> (b --> (c --> d)))

pevalEqTerm :: Term (a --> (b --> (c --> d))) -> Term (a --> (b --> (c --> d))) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> (b --> (c --> d))) -> SBVType n (a --> (b --> (c --> d)))

symSBVName :: TypedSymbol (a --> (b --> (c --> d))) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> (b --> (c --> d))))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> (b --> (c --> d))), SMTDefinable (SBVType n (a --> (b --> (c --> d)))), Mergeable (SBVType n (a --> (b --> (c --> d)))), Typeable (SBVType n (a --> (b --> (c --> d))))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> (b --> (c --> d))) -> SBVType n (a --> (b --> (c --> d))) -> SBVType n (a --> (b --> (c --> d)))

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> (b --> (c --> d))) -> SBVType n (a --> (b --> (c --> d))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> (b --> (c --> d))

(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedPrim a, SupportedPrim b, SupportedPrim c) => SupportedPrim (a --> (b --> c))

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

termCache :: Cache (Term (a --> (b --> c)))

pformatCon :: (a --> (b --> c)) -> String

pformatSym :: TypedSymbol (a --> (b --> c)) -> String

defaultValue :: a --> (b --> c)

defaultValueDynamic :: proxy (a --> (b --> c)) -> ModelValue

pevalITETerm :: Term Bool -> Term (a --> (b --> c)) -> Term (a --> (b --> c)) -> Term (a --> (b --> c))

pevalEqTerm :: Term (a --> (b --> c)) -> Term (a --> (b --> c)) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> (b --> c)) -> SBVType n (a --> (b --> c))

symSBVName :: TypedSymbol (a --> (b --> c)) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> (b --> c)))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> (b --> c)), SMTDefinable (SBVType n (a --> (b --> c))), Mergeable (SBVType n (a --> (b --> c))), Typeable (SBVType n (a --> (b --> c)))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> (b --> c)) -> SBVType n (a --> (b --> c)) -> SBVType n (a --> (b --> c))

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> (b --> c)) -> SBVType n (a --> (b --> c)) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> (b --> c)

(SupportedNonFuncPrim a, SupportedNonFuncPrim b) => SupportedPrim (a --> b)

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

termCache :: Cache (Term (a --> b))

pformatCon :: (a --> b) -> String

pformatSym :: TypedSymbol (a --> b) -> String

defaultValue :: a --> b

defaultValueDynamic :: proxy (a --> b) -> ModelValue

pevalITETerm :: Term Bool -> Term (a --> b) -> Term (a --> b) -> Term (a --> b)

pevalEqTerm :: Term (a --> b) -> Term (a --> b) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> b) -> SBVType n (a --> b)

symSBVName :: TypedSymbol (a --> b) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> b))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> b), SMTDefinable (SBVType n (a --> b)), Mergeable (SBVType n (a --> b)), Typeable (SBVType n (a --> b))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> b) -> SBVType n (a --> b) -> SBVType n (a --> b)

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> b) -> SBVType n (a --> b) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> b

(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedNonFuncPrim f, SupportedNonFuncPrim g, SupportedNonFuncPrim h, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e, SupportedPrim f, SupportedPrim g, SupportedPrim h) => SupportedPrim (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

termCache :: Cache (Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))

pformatCon :: (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> String

pformatSym :: TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> String

defaultValue :: a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))

defaultValueDynamic :: proxy (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))

pevalEqTerm :: Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))

symSBVName :: TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))), SMTDefinable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))), Mergeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))), Typeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))

(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedNonFuncPrim f, SupportedNonFuncPrim g, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e, SupportedPrim f, SupportedPrim g) => SupportedPrim (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

termCache :: Cache (Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))

pformatCon :: (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> String

pformatSym :: TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> String

defaultValue :: a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))

defaultValueDynamic :: proxy (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))

pevalEqTerm :: Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))

symSBVName :: TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))), SMTDefinable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))), Mergeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))), Typeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))

(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedNonFuncPrim f, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e, SupportedPrim f) => SupportedPrim (a =-> (b =-> (c =-> (d =-> (e =-> f)))))

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

termCache :: Cache (Term (a =-> (b =-> (c =-> (d =-> (e =-> f))))))

pformatCon :: (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> String

pformatSym :: TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> String

defaultValue :: a =-> (b =-> (c =-> (d =-> (e =-> f))))

defaultValueDynamic :: proxy (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> f)))))

pevalEqTerm :: Term (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))

symSBVName :: TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a =-> (b =-> (c =-> (d =-> (e =-> f))))), SMTDefinable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))), Mergeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))), Typeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> (d =-> (e =-> f))))

(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e) => SupportedPrim (a =-> (b =-> (c =-> (d =-> e))))

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

termCache :: Cache (Term (a =-> (b =-> (c =-> (d =-> e)))))

pformatCon :: (a =-> (b =-> (c =-> (d =-> e)))) -> String

pformatSym :: TypedSymbol (a =-> (b =-> (c =-> (d =-> e)))) -> String

defaultValue :: a =-> (b =-> (c =-> (d =-> e)))

defaultValueDynamic :: proxy (a =-> (b =-> (c =-> (d =-> e)))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a =-> (b =-> (c =-> (d =-> e)))) -> Term (a =-> (b =-> (c =-> (d =-> e)))) -> Term (a =-> (b =-> (c =-> (d =-> e))))

pevalEqTerm :: Term (a =-> (b =-> (c =-> (d =-> e)))) -> Term (a =-> (b =-> (c =-> (d =-> e)))) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a =-> (b =-> (c =-> (d =-> e)))) -> SBVType n (a =-> (b =-> (c =-> (d =-> e))))

symSBVName :: TypedSymbol (a =-> (b =-> (c =-> (d =-> e)))) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a =-> (b =-> (c =-> (d =-> e)))), SMTDefinable (SBVType n (a =-> (b =-> (c =-> (d =-> e))))), Mergeable (SBVType n (a =-> (b =-> (c =-> (d =-> e))))), Typeable (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a =-> (b =-> (c =-> (d =-> e)))) -> SBVType n (a =-> (b =-> (c =-> (d =-> e)))) -> SBVType n (a =-> (b =-> (c =-> (d =-> e))))

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a =-> (b =-> (c =-> (d =-> e)))) -> SBVType n (a =-> (b =-> (c =-> (d =-> e)))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> (d =-> e)))

(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d) => SupportedPrim (a =-> (b =-> (c =-> d)))

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

termCache :: Cache (Term (a =-> (b =-> (c =-> d))))

pformatCon :: (a =-> (b =-> (c =-> d))) -> String

pformatSym :: TypedSymbol (a =-> (b =-> (c =-> d))) -> String

defaultValue :: a =-> (b =-> (c =-> d))

defaultValueDynamic :: proxy (a =-> (b =-> (c =-> d))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a =-> (b =-> (c =-> d))) -> Term (a =-> (b =-> (c =-> d))) -> Term (a =-> (b =-> (c =-> d)))

pevalEqTerm :: Term (a =-> (b =-> (c =-> d))) -> Term (a =-> (b =-> (c =-> d))) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a =-> (b =-> (c =-> d))) -> SBVType n (a =-> (b =-> (c =-> d)))

symSBVName :: TypedSymbol (a =-> (b =-> (c =-> d))) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a =-> (b =-> (c =-> d))))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a =-> (b =-> (c =-> d))), SMTDefinable (SBVType n (a =-> (b =-> (c =-> d)))), Mergeable (SBVType n (a =-> (b =-> (c =-> d)))), Typeable (SBVType n (a =-> (b =-> (c =-> d))))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a =-> (b =-> (c =-> d))) -> SBVType n (a =-> (b =-> (c =-> d))) -> SBVType n (a =-> (b =-> (c =-> d)))

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a =-> (b =-> (c =-> d))) -> SBVType n (a =-> (b =-> (c =-> d))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> d))

(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedPrim a, SupportedPrim b, SupportedPrim c) => SupportedPrim (a =-> (b =-> c))

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

termCache :: Cache (Term (a =-> (b =-> c)))

pformatCon :: (a =-> (b =-> c)) -> String

pformatSym :: TypedSymbol (a =-> (b =-> c)) -> String

defaultValue :: a =-> (b =-> c)

defaultValueDynamic :: proxy (a =-> (b =-> c)) -> ModelValue

pevalITETerm :: Term Bool -> Term (a =-> (b =-> c)) -> Term (a =-> (b =-> c)) -> Term (a =-> (b =-> c))

pevalEqTerm :: Term (a =-> (b =-> c)) -> Term (a =-> (b =-> c)) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a =-> (b =-> c)) -> SBVType n (a =-> (b =-> c))

symSBVName :: TypedSymbol (a =-> (b =-> c)) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a =-> (b =-> c)))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a =-> (b =-> c)), SMTDefinable (SBVType n (a =-> (b =-> c))), Mergeable (SBVType n (a =-> (b =-> c))), Typeable (SBVType n (a =-> (b =-> c)))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a =-> (b =-> c)) -> SBVType n (a =-> (b =-> c)) -> SBVType n (a =-> (b =-> c))

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a =-> (b =-> c)) -> SBVType n (a =-> (b =-> c)) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> (b =-> c)

(SupportedNonFuncPrim a, SupportedNonFuncPrim b) => SupportedPrim (a =-> b)

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

termCache :: Cache (Term (a =-> b))

pformatCon :: (a =-> b) -> String

pformatSym :: TypedSymbol (a =-> b) -> String

defaultValue :: a =-> b

defaultValueDynamic :: proxy (a =-> b) -> ModelValue

pevalITETerm :: Term Bool -> Term (a =-> b) -> Term (a =-> b) -> Term (a =-> b)

pevalEqTerm :: Term (a =-> b) -> Term (a =-> b) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a =-> b) -> SBVType n (a =-> b)

symSBVName :: TypedSymbol (a =-> b) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a =-> b))

withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a =-> b), SMTDefinable (SBVType n (a =-> b)), Mergeable (SBVType n (a =-> b)), Typeable (SBVType n (a =-> b))) => a0) -> a0

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a =-> b) -> SBVType n (a =-> b) -> SBVType n (a =-> b)

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a =-> b) -> SBVType n (a =-> b) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> b

class SupportedPrim con => SymRep con

Type family to resolve the symbolic type associated with a concrete type.

Associated Types

type SymType con

Instances

SymRep Integer

Defined in Grisette.Internal.SymPrim.SymInteger

Associated Types

type SymType Integer

SymRep Bool

Defined in Grisette.Internal.SymPrim.SymBool

Associated Types

type SymType Bool

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

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type SymType (IntN n)

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

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type SymType (WordN n)

(SymRep ca, SymRep cb, SupportedPrim (ca --> cb)) => SymRep (ca --> cb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Associated Types

type SymType (ca --> cb)

(SymRep a, SymRep b, SupportedPrim (a =-> b)) => SymRep (a =-> b)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Associated Types

type SymType (a =-> b)

class ConRep sym

Type family to resolve the concrete type associated with a symbolic type.

Associated Types

type ConType sym

Instances

ConRep SymBool

Defined in Grisette.Internal.SymPrim.SymBool

Associated Types

type ConType SymBool

ConRep SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Associated Types

type ConType SymInteger

(KnownNat n, 1 <= n) => ConRep (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type ConType (SymIntN n)

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

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type ConType (SymWordN n)

(ConRep a, ConRep b) => ConRep (a -~> b)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Associated Types

type ConType (a -~> b)

(ConRep a, ConRep b) => ConRep (a =~> b)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Associated Types

type ConType (a =~> b)

class (ConRep sym, SymRep con, sym ~ SymType con, con ~ ConType sym) => LinkedRep con sym | con -> sym, sym -> con

One-to-one mapping between symbolic types and concrete types.

Minimal complete definition

underlyingTerm, wrapTerm

Instances

LinkedRep Integer SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

underlyingTerm :: SymInteger -> Term Integer

wrapTerm :: Term Integer -> SymInteger

LinkedRep Bool SymBool

Defined in Grisette.Internal.SymPrim.SymBool

Methods

underlyingTerm :: SymBool -> Term Bool

wrapTerm :: Term Bool -> SymBool

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim ca, SupportedPrim cb, SupportedPrim (ca --> cb)) => LinkedRep (ca --> cb) (sa -~> sb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

underlyingTerm :: (sa -~> sb) -> Term (ca --> cb)

wrapTerm :: Term (ca --> cb) -> sa -~> sb

(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca =-> cb)) => LinkedRep (ca =-> cb) (sa =~> sb)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

underlyingTerm :: (sa =~> sb) -> Term (ca =-> cb)

wrapTerm :: Term (ca =-> cb) -> sa =~> sb

newtype SymBool

Symbolic Boolean type.

>>> :set -XOverloadedStrings
>>> "a" :: SymBool
a
>>> "a" .&& "b" :: SymBool
(&& a b)

More symbolic operations are available. Please refer to the documentation for the type class instances.

Constructors

SymBool (Term Bool)

Instances

IsString SymBool

Defined in Grisette.Internal.SymPrim.SymBool

Methods

fromString :: String -> SymBool

Generic SymBool

Defined in Grisette.Internal.SymPrim.SymBool

Associated Types

type Rep SymBool :: Type -> Type

Methods

from :: SymBool -> Rep SymBool x

to :: Rep SymBool x -> SymBool

Show SymBool

Defined in Grisette.Internal.SymPrim.SymBool

Methods

showsPrec :: Int -> SymBool -> ShowS

show :: SymBool -> String

showList :: [SymBool] -> ShowS

NFData SymBool

Defined in Grisette.Internal.SymPrim.SymBool

Methods

rnf :: SymBool -> ()

Eq SymBool

Defined in Grisette.Internal.SymPrim.SymBool

Methods

(==) :: SymBool -> SymBool -> Bool

(/=) :: SymBool -> SymBool -> Bool

EvaluateSym SymBool

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

Methods

evaluateSym :: Bool -> Model -> SymBool -> SymBool

ExtractSymbolics SymBool

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

Methods

extractSymbolics :: SymBool -> SymbolSet

Apply SymBool

Defined in Grisette.Internal.SymPrim.SymBool

Associated Types

type FunType SymBool

Methods

apply :: SymBool -> FunType SymBool

GPretty SymBool

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

Methods

gpretty :: SymBool -> Doc ann

gprettyPrec :: Int -> SymBool -> Doc ann

gprettyList :: [SymBool] -> Doc ann

ITEOp SymBool

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

Methods

symIte :: SymBool -> SymBool -> SymBool -> SymBool

LogicalOp SymBool

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

Methods

(.||) :: SymBool -> SymBool -> SymBool

(.&&) :: SymBool -> SymBool -> SymBool

symNot :: SymBool -> SymBool

symXor :: SymBool -> SymBool -> SymBool

symImplies :: SymBool -> SymBool -> SymBool

Mergeable SymBool

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

Methods

rootStrategy :: MergingStrategy SymBool

SEq SymBool

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

Methods

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

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

SOrd SymBool

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

Methods

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

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

(.>) :: SymBool -> SymBool -> SymBool

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

symCompare :: SymBool -> SymBool -> UnionM Ordering

SimpleMergeable SymBool

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

Methods

mrgIte :: SymBool -> SymBool -> SymBool -> SymBool

SubstituteSym SymBool

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

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SymBool -> SymBool

AllSyms SymBool

Defined in Grisette.Internal.SymPrim.SymBool

Methods

allSymsS :: SymBool -> [SomeSym] -> [SomeSym]

allSyms :: SymBool -> [SomeSym]

ConRep SymBool

Defined in Grisette.Internal.SymPrim.SymBool

Associated Types

type ConType SymBool

Hashable SymBool

Defined in Grisette.Internal.SymPrim.SymBool

Methods

hashWithSalt :: Int -> SymBool -> Int

hash :: SymBool -> Int

GenSym SymBool SymBool

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

Methods

fresh :: MonadFresh m => SymBool -> m (UnionM SymBool)

GenSym () SymBool

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

Methods

fresh :: MonadFresh m => () -> m (UnionM SymBool)

GenSymSimple SymBool SymBool

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

Methods

simpleFresh :: MonadFresh m => SymBool -> m SymBool

GenSymSimple () SymBool

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

Methods

simpleFresh :: MonadFresh m => () -> m SymBool

Solvable Bool SymBool

Defined in Grisette.Internal.SymPrim.SymBool

Methods

con :: Bool -> SymBool

conView :: SymBool -> Maybe Bool

sym :: Symbol -> SymBool

ssym :: Identifier -> SymBool

isym :: Identifier -> Int -> SymBool

ToCon SymBool SymBool

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

Methods

toCon :: SymBool -> Maybe SymBool

ToCon SymBool Bool

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

Methods

toCon :: SymBool -> Maybe Bool

ToSym SymBool SymBool

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

Methods

toSym :: SymBool -> SymBool

ToSym Bool SymBool

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

Methods

toSym :: Bool -> SymBool

LinkedRep Bool SymBool

Defined in Grisette.Internal.SymPrim.SymBool

Methods

underlyingTerm :: SymBool -> Term Bool

wrapTerm :: Term Bool -> SymBool

Lift SymBool

Defined in Grisette.Internal.SymPrim.SymBool

Methods

lift :: Quote m => SymBool -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => SymBool -> Code m SymBool

ToSym (UnionM Bool) SymBool

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

Methods

toSym :: UnionM Bool -> SymBool

type Rep SymBool

Defined in Grisette.Internal.SymPrim.SymBool

type Rep SymBool = D1 ('MetaData "SymBool" "Grisette.Internal.SymPrim.SymBool" "grisette-0.5.0.1-IKpKourvCOdG0l1QW5fLHa" 'True) (C1 ('MetaCons "SymBool" 'PrefixI 'True) (S1 ('MetaSel ('Just "underlyingBoolTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term Bool))))

type FunType SymBool

Defined in Grisette.Internal.SymPrim.SymBool

type FunType SymBool = SymBool

type ConType SymBool

Defined in Grisette.Internal.SymPrim.SymBool

type ConType SymBool = Bool

newtype SymInteger

Symbolic (unbounded, mathematical) integer type.

>>> "a" + 1 :: SymInteger
(+ 1 a)

More symbolic operations are available. Please refer to the documentation for the type class instances.

Constructors

SymInteger (Term Integer)

Instances

IsString SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

fromString :: String -> SymInteger

Generic SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Associated Types

type Rep SymInteger :: Type -> Type

Methods

from :: SymInteger -> Rep SymInteger x

to :: Rep SymInteger x -> SymInteger

Num SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

(+) :: SymInteger -> SymInteger -> SymInteger

(-) :: SymInteger -> SymInteger -> SymInteger

(*) :: SymInteger -> SymInteger -> SymInteger

negate :: SymInteger -> SymInteger

abs :: SymInteger -> SymInteger

signum :: SymInteger -> SymInteger

fromInteger :: Integer -> SymInteger

Show SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

showsPrec :: Int -> SymInteger -> ShowS

show :: SymInteger -> String

showList :: [SymInteger] -> ShowS

NFData SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

rnf :: SymInteger -> ()

Eq SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

(==) :: SymInteger -> SymInteger -> Bool

(/=) :: SymInteger -> SymInteger -> Bool

EvaluateSym SymInteger

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

Methods

evaluateSym :: Bool -> Model -> SymInteger -> SymInteger

ExtractSymbolics SymInteger

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

Methods

extractSymbolics :: SymInteger -> SymbolSet

Apply SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Associated Types

type FunType SymInteger

Methods

apply :: SymInteger -> FunType SymInteger

GPretty SymInteger

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

Methods

gpretty :: SymInteger -> Doc ann

gprettyPrec :: Int -> SymInteger -> Doc ann

gprettyList :: [SymInteger] -> Doc ann

ITEOp SymInteger

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

Methods

symIte :: SymBool -> SymInteger -> SymInteger -> SymInteger

Mergeable SymInteger

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

Methods

rootStrategy :: MergingStrategy SymInteger

SEq SymInteger

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

Methods

(.==) :: SymInteger -> SymInteger -> SymBool

(./=) :: SymInteger -> SymInteger -> SymBool

SOrd SymInteger

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

Methods

(.<) :: SymInteger -> SymInteger -> SymBool

(.<=) :: SymInteger -> SymInteger -> SymBool

(.>) :: SymInteger -> SymInteger -> SymBool

(.>=) :: SymInteger -> SymInteger -> SymBool

symCompare :: SymInteger -> SymInteger -> UnionM Ordering

SimpleMergeable SymInteger

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

Methods

mrgIte :: SymBool -> SymInteger -> SymInteger -> SymInteger

SubstituteSym SymInteger

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

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SymInteger -> SymInteger

AllSyms SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

allSymsS :: SymInteger -> [SomeSym] -> [SomeSym]

allSyms :: SymInteger -> [SomeSym]

ConRep SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Associated Types

type ConType SymInteger

Hashable SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

hashWithSalt :: Int -> SymInteger -> Int

hash :: SymInteger -> Int

GenSym SymInteger SymInteger

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

Methods

fresh :: MonadFresh m => SymInteger -> m (UnionM SymInteger)

GenSym () SymInteger

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

Methods

fresh :: MonadFresh m => () -> m (UnionM SymInteger)

GenSymSimple SymInteger SymInteger

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

Methods

simpleFresh :: MonadFresh m => SymInteger -> m SymInteger

GenSymSimple () SymInteger

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

Methods

simpleFresh :: MonadFresh m => () -> m SymInteger

Solvable Integer SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

con :: Integer -> SymInteger

conView :: SymInteger -> Maybe Integer

sym :: Symbol -> SymInteger

ssym :: Identifier -> SymInteger

isym :: Identifier -> Int -> SymInteger

ToCon SymInteger SymInteger

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

Methods

toCon :: SymInteger -> Maybe SymInteger

ToCon SymInteger Integer

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

Methods

toCon :: SymInteger -> Maybe Integer

ToSym SymInteger SymInteger

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

Methods

toSym :: SymInteger -> SymInteger

ToSym Integer SymInteger

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

Methods

toSym :: Integer -> SymInteger

LinkedRep Integer SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

underlyingTerm :: SymInteger -> Term Integer

wrapTerm :: Term Integer -> SymInteger

Lift SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

lift :: Quote m => SymInteger -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => SymInteger -> Code m SymInteger

(MonadUnion m, MonadError ArithException m) => SafeDivision ArithException SymInteger m

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

Methods

safeDiv :: SymInteger -> SymInteger -> m SymInteger

safeMod :: SymInteger -> SymInteger -> m SymInteger

safeDivMod :: SymInteger -> SymInteger -> m (SymInteger, SymInteger)

safeQuot :: SymInteger -> SymInteger -> m SymInteger

safeRem :: SymInteger -> SymInteger -> m SymInteger

safeQuotRem :: SymInteger -> SymInteger -> m (SymInteger, SymInteger)

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException SymInteger m

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

Methods

safeAdd :: SymInteger -> SymInteger -> m SymInteger

safeNeg :: SymInteger -> m SymInteger

safeSub :: SymInteger -> SymInteger -> m SymInteger

ToSym (UnionM Integer) SymInteger

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

Methods

toSym :: UnionM Integer -> SymInteger

type Rep SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

type Rep SymInteger = D1 ('MetaData "SymInteger" "Grisette.Internal.SymPrim.SymInteger" "grisette-0.5.0.1-IKpKourvCOdG0l1QW5fLHa" 'True) (C1 ('MetaCons "SymInteger" 'PrefixI 'True) (S1 ('MetaSel ('Just "underlyingIntegerTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term Integer))))

type FunType SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

type FunType SymInteger = SymInteger

type ConType SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

type ConType SymInteger = Integer

newtype SymWordN (n :: Nat)

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

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

More symbolic operations are available. Please refer to the documentation for the type class instances.

Constructors

SymWordN

Fields

• underlyingWordNTerm :: Term (WordN n)

Instances

SizedBV SymWordN

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

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

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

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

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

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

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

Methods

fresh :: MonadFresh m => () -> m (UnionM (SymWordN n))

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

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

Methods

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

ToSym Word16 (SymWordN 16)

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

Methods

toSym :: Word16 -> SymWordN 16

ToSym Word32 (SymWordN 32)

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

Methods

toSym :: Word32 -> SymWordN 32

ToSym Word64 (SymWordN 64)

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

Methods

toSym :: Word64 -> SymWordN 64

ToSym Word8 (SymWordN 8)

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

Methods

toSym :: Word8 -> SymWordN 8

ToSym Word (SymWordN 64)

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

Methods

toSym :: Word -> SymWordN 64

Lift (SymWordN n :: Type)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeDivision ArithException (SymWordN n) m

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

Methods

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

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

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

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

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

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

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

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

Methods

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

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

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

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

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

Methods

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

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

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

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

Methods

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

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

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

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

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

fromString :: String -> SymWordN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

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

complement :: SymWordN n -> SymWordN n

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

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

zeroBits :: SymWordN n

bit :: Int -> SymWordN n

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

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

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

testBit :: SymWordN n -> Int -> Bool

bitSizeMaybe :: SymWordN n -> Maybe Int

bitSize :: SymWordN n -> Int

isSigned :: SymWordN n -> Bool

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

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

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

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

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

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

popCount :: SymWordN n -> Int

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

finiteBitSize :: SymWordN n -> Int

countLeadingZeros :: SymWordN n -> Int

countTrailingZeros :: SymWordN n -> Int

Generic (SymWordN n)

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

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

Methods

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

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

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

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

negate :: SymWordN n -> SymWordN n

abs :: SymWordN n -> SymWordN n

signum :: SymWordN n -> SymWordN n

fromInteger :: Integer -> SymWordN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

showsPrec :: Int -> SymWordN n -> ShowS

show :: SymWordN n -> String

showList :: [SymWordN n] -> ShowS

NFData (SymWordN n)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

rnf :: SymWordN n -> ()

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

(KnownNat n, 1 <= n) => EvaluateSym (SymWordN n)

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

Methods

evaluateSym :: Bool -> Model -> SymWordN n -> SymWordN n

(KnownNat n, 1 <= n) => ExtractSymbolics (SymWordN n)

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

Methods

extractSymbolics :: SymWordN n -> SymbolSet

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

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type FunType (SymWordN n)

Methods

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

(KnownNat n, 1 <= n) => GPretty (SymWordN n)

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

Methods

gpretty :: SymWordN n -> Doc ann

gprettyPrec :: Int -> SymWordN n -> Doc ann

gprettyList :: [SymWordN n] -> Doc ann

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

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

Methods

symIte :: SymBool -> SymWordN n -> SymWordN n -> SymWordN n

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

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

Methods

rootStrategy :: MergingStrategy (SymWordN n)

(KnownNat n, 1 <= n) => SEq (SymWordN n)

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

Methods

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

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

(KnownNat n, 1 <= n) => SOrd (SymWordN n)

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

Methods

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

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

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

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

symCompare :: SymWordN n -> SymWordN n -> UnionM Ordering

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

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

Methods

mrgIte :: SymBool -> SymWordN n -> SymWordN n -> SymWordN n

(KnownNat n, 1 <= n) => SubstituteSym (SymWordN n)

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

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SymWordN n -> SymWordN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

symRotate :: SymWordN n -> SymWordN n -> SymWordN n

symRotateNegated :: SymWordN n -> SymWordN n -> SymWordN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

symShift :: SymWordN n -> SymWordN n -> SymWordN n

symShiftNegated :: SymWordN n -> SymWordN n -> SymWordN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

allSyms :: SymWordN n -> [SomeSym]

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

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type ConType (SymWordN n)

(KnownNat n, 1 <= n) => Hashable (SymWordN n)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

hashWithSalt :: Int -> SymWordN n -> Int

hash :: SymWordN n -> Int

ToCon (SymWordN 8) Word8

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

Methods

toCon :: SymWordN 8 -> Maybe Word8

ToCon (SymWordN 16) Word16

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

Methods

toCon :: SymWordN 16 -> Maybe Word16

ToCon (SymWordN 32) Word32

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

Methods

toCon :: SymWordN 32 -> Maybe Word32

ToCon (SymWordN 64) Word64

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

Methods

toCon :: SymWordN 64 -> Maybe Word64

ToCon (SymWordN 64) Word

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

Methods

toCon :: SymWordN 64 -> Maybe Word

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

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

Methods

fresh :: MonadFresh m => SymWordN n -> m (UnionM (SymWordN n))

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

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

Methods

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

(KnownNat n, 1 <= n) => SignConversion (SymWordN n) (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

toSigned :: SymWordN n -> SymIntN n

toUnsigned :: SymIntN n -> SymWordN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

con :: WordN n -> SymWordN n

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

sym :: Symbol -> SymWordN n

ssym :: Identifier -> SymWordN n

isym :: Identifier -> Int -> SymWordN n

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

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

Methods

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

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

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

Methods

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

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

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

Methods

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

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

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

Methods

toSym :: WordN n -> SymWordN n

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

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

Methods

toSym :: SymWordN n -> SymWordN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

type Rep (SymWordN n)

Defined in Grisette.Internal.SymPrim.SymBV

type Rep (SymWordN n) = D1 ('MetaData "SymWordN" "Grisette.Internal.SymPrim.SymBV" "grisette-0.5.0.1-IKpKourvCOdG0l1QW5fLHa" 'True) (C1 ('MetaCons "SymWordN" 'PrefixI 'True) (S1 ('MetaSel ('Just "underlyingWordNTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term (WordN n)))))

type FunType (SymWordN n)

Defined in Grisette.Internal.SymPrim.SymBV

type FunType (SymWordN n) = SymWordN n

type ConType (SymWordN n)

Defined in Grisette.Internal.SymPrim.SymBV

type ConType (SymWordN n) = WordN n

newtype SymIntN (n :: Nat)

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

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

More symbolic operations are available. Please refer to the documentation for the type class instances.

Constructors

SymIntN

Fields

• underlyingIntNTerm :: Term (IntN n)

Instances

SizedBV SymIntN

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

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

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

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

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

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

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

Methods

fresh :: MonadFresh m => () -> m (UnionM (SymIntN n))

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

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

Methods

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

ToSym Int16 (SymIntN 16)

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

Methods

toSym :: Int16 -> SymIntN 16

ToSym Int32 (SymIntN 32)

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

Methods

toSym :: Int32 -> SymIntN 32

ToSym Int64 (SymIntN 64)

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

Methods

toSym :: Int64 -> SymIntN 64

ToSym Int8 (SymIntN 8)

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

Methods

toSym :: Int8 -> SymIntN 8

ToSym Int (SymIntN 64)

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

Methods

toSym :: Int -> SymIntN 64

Lift (SymIntN n :: Type)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeDivision ArithException (SymIntN n) m

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

Methods

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

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

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

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

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

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

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

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

Methods

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

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

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

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

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

Methods

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

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

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

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

Methods

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

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

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

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

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

fromString :: String -> SymIntN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

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

complement :: SymIntN n -> SymIntN n

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

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

zeroBits :: SymIntN n

bit :: Int -> SymIntN n

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

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

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

testBit :: SymIntN n -> Int -> Bool

bitSizeMaybe :: SymIntN n -> Maybe Int

bitSize :: SymIntN n -> Int

isSigned :: SymIntN n -> Bool

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

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

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

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

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

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

popCount :: SymIntN n -> Int

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

finiteBitSize :: SymIntN n -> Int

countLeadingZeros :: SymIntN n -> Int

countTrailingZeros :: SymIntN n -> Int

Generic (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

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

Methods

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

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

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

(+) :: SymIntN n -> SymIntN n -> SymIntN n

(-) :: SymIntN n -> SymIntN n -> SymIntN n

(*) :: SymIntN n -> SymIntN n -> SymIntN n

negate :: SymIntN n -> SymIntN n

abs :: SymIntN n -> SymIntN n

signum :: SymIntN n -> SymIntN n

fromInteger :: Integer -> SymIntN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

showsPrec :: Int -> SymIntN n -> ShowS

show :: SymIntN n -> String

showList :: [SymIntN n] -> ShowS

NFData (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

rnf :: SymIntN n -> ()

(KnownNat n, 1 <= n) => Eq (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

(KnownNat n, 1 <= n) => EvaluateSym (SymIntN n)

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

Methods

evaluateSym :: Bool -> Model -> SymIntN n -> SymIntN n

(KnownNat n, 1 <= n) => ExtractSymbolics (SymIntN n)

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

Methods

extractSymbolics :: SymIntN n -> SymbolSet

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

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type FunType (SymIntN n)

Methods

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

(KnownNat n, 1 <= n) => GPretty (SymIntN n)

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

Methods

gpretty :: SymIntN n -> Doc ann

gprettyPrec :: Int -> SymIntN n -> Doc ann

gprettyList :: [SymIntN n] -> Doc ann

(KnownNat n, 1 <= n) => ITEOp (SymIntN n)

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

Methods

symIte :: SymBool -> SymIntN n -> SymIntN n -> SymIntN n

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

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

Methods

rootStrategy :: MergingStrategy (SymIntN n)

(KnownNat n, 1 <= n) => SEq (SymIntN n)

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

Methods

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

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

(KnownNat n, 1 <= n) => SOrd (SymIntN n)

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

Methods

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

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

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

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

symCompare :: SymIntN n -> SymIntN n -> UnionM Ordering

(KnownNat n, 1 <= n) => SimpleMergeable (SymIntN n)

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

Methods

mrgIte :: SymBool -> SymIntN n -> SymIntN n -> SymIntN n

(KnownNat n, 1 <= n) => SubstituteSym (SymIntN n)

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

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SymIntN n -> SymIntN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

symRotate :: SymIntN n -> SymIntN n -> SymIntN n

symRotateNegated :: SymIntN n -> SymIntN n -> SymIntN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

symShift :: SymIntN n -> SymIntN n -> SymIntN n

symShiftNegated :: SymIntN n -> SymIntN n -> SymIntN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

allSyms :: SymIntN n -> [SomeSym]

(KnownNat n, 1 <= n) => ConRep (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type ConType (SymIntN n)

(KnownNat n, 1 <= n) => Hashable (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

hashWithSalt :: Int -> SymIntN n -> Int

hash :: SymIntN n -> Int

ToCon (SymIntN 8) Int8

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

Methods

toCon :: SymIntN 8 -> Maybe Int8

ToCon (SymIntN 16) Int16

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

Methods

toCon :: SymIntN 16 -> Maybe Int16

ToCon (SymIntN 32) Int32

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

Methods

toCon :: SymIntN 32 -> Maybe Int32

ToCon (SymIntN 64) Int64

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

Methods

toCon :: SymIntN 64 -> Maybe Int64

ToCon (SymIntN 64) Int

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

Methods

toCon :: SymIntN 64 -> Maybe Int

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

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

Methods

fresh :: MonadFresh m => SymIntN n -> m (UnionM (SymIntN n))

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

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

Methods

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

(KnownNat n, 1 <= n) => SignConversion (SymWordN n) (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

Methods

toSigned :: SymWordN n -> SymIntN n

toUnsigned :: SymIntN n -> SymWordN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

con :: IntN n -> SymIntN n

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

sym :: Symbol -> SymIntN n

ssym :: Identifier -> SymIntN n

isym :: Identifier -> Int -> SymIntN n

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

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

Methods

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

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

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

Methods

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

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

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

Methods

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

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

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

Methods

toSym :: IntN n -> SymIntN n

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

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

Methods

toSym :: SymIntN n -> SymIntN n

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

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

type Rep (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

type Rep (SymIntN n) = D1 ('MetaData "SymIntN" "Grisette.Internal.SymPrim.SymBV" "grisette-0.5.0.1-IKpKourvCOdG0l1QW5fLHa" 'True) (C1 ('MetaCons "SymIntN" 'PrefixI 'True) (S1 ('MetaSel ('Just "underlyingIntNTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term (IntN n)))))

type FunType (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

type FunType (SymIntN n) = SymIntN n

type ConType (SymIntN n)

Defined in Grisette.Internal.SymPrim.SymBV

type ConType (SymIntN n) = IntN n

type SomeSymIntN = SomeBV SymIntN

Type synonym for SomeBV with symbolic signed bitvectors.

type SomeSymWordN = SomeBV SymWordN

Type synonym for SomeBV with symbolic unsigned bitvectors.

pattern SomeSymIntN :: () => (KnownNat n, 1 <= n) => SymIntN n -> SomeSymIntN

Pattern synonym for SomeBV with symbolic signed bitvectors.

pattern SomeSymWordN :: () => (KnownNat n, 1 <= n) => SymWordN n -> SomeSymWordN

Pattern synonym for SomeBV with symbolic unsigned bitvectors.

data sa =~> sb where infixr 0

Symbolic tabular function type.

>>> :set -XTypeOperators -XOverloadedStrings
>>> f' = "f" :: SymInteger =~> SymInteger
>>> f = (f' #)
>>> f 1
(apply f 1)

>>> f' = con (TabularFun [(1, 2), (2, 3)] 4) :: SymInteger =~> SymInteger
>>> f = (f' #)
>>> f 1
2
>>> f 2
3
>>> f 3
4
>>> f "b"
(ite (= b 1) 2 (ite (= b 2) 3 4))

Constructors

SymTabularFun :: (LinkedRep ca sa, LinkedRep cb sb) => Term (ca =-> cb) -> sa =~> sb

Instances

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => GenSym () (sa =~> sb)

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

Methods

fresh :: MonadFresh m => () -> m (UnionM (sa =~> sb))

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => GenSymSimple () (sa =~> sb)

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

Methods

simpleFresh :: MonadFresh m => () -> m (sa =~> sb)

Lift (sa =~> sb :: Type)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

lift :: Quote m => (sa =~> sb) -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => (sa =~> sb) -> Code m (sa =~> sb)

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => ToSym (UnionM (ca =-> cb)) (sa =~> sb)

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

Methods

toSym :: UnionM (ca =-> cb) -> sa =~> sb

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => IsString (sa =~> sb)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

fromString :: String -> sa =~> sb

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => Show (sa =~> sb)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

showsPrec :: Int -> (sa =~> sb) -> ShowS

show :: (sa =~> sb) -> String

showList :: [sa =~> sb] -> ShowS

NFData (sa =~> sb)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

rnf :: (sa =~> sb) -> ()

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => Eq (sa =~> sb)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

(==) :: (sa =~> sb) -> (sa =~> sb) -> Bool

(/=) :: (sa =~> sb) -> (sa =~> sb) -> Bool

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => EvaluateSym (sa =~> sb)

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

Methods

evaluateSym :: Bool -> Model -> (sa =~> sb) -> sa =~> sb

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => ExtractSymbolics (sa =~> sb)

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

Methods

extractSymbolics :: (sa =~> sb) -> SymbolSet

(LinkedRep ca sa, LinkedRep ct st, Apply st, SupportedPrim ca, SupportedPrim ct, SupportedPrim (ca =-> ct)) => Apply (sa =~> st)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Associated Types

type FunType (sa =~> st)

Methods

apply :: (sa =~> st) -> FunType (sa =~> st)

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => GPretty (sa =~> sb)

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

Methods

gpretty :: (sa =~> sb) -> Doc ann

gprettyPrec :: Int -> (sa =~> sb) -> Doc ann

gprettyList :: [sa =~> sb] -> Doc ann

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => ITEOp (sa =~> sb)

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

Methods

symIte :: SymBool -> (sa =~> sb) -> (sa =~> sb) -> sa =~> sb

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => Mergeable (sa =~> sb)

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

Methods

rootStrategy :: MergingStrategy (sa =~> sb)

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => SimpleMergeable (sa =~> sb)

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

Methods

mrgIte :: SymBool -> (sa =~> sb) -> (sa =~> sb) -> sa =~> sb

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => SubstituteSym (sa =~> sb)

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

Methods

substituteSym :: LinkedRep cb sb0 => TypedSymbol cb -> sb0 -> (sa =~> sb) -> sa =~> sb

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => AllSyms (sa =~> sb)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

allSymsS :: (sa =~> sb) -> [SomeSym] -> [SomeSym]

allSyms :: (sa =~> sb) -> [SomeSym]

(ConRep a, ConRep b) => ConRep (a =~> b)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Associated Types

type ConType (a =~> b)

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => Hashable (sa =~> sb)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

hashWithSalt :: Int -> (sa =~> sb) -> Int

hash :: (sa =~> sb) -> Int

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca =-> cb)) => Function (sa =~> sb) sa sb

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

(#) :: (sa =~> sb) -> sa -> sb

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => GenSym (sa =~> sb) (sa =~> sb)

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

Methods

fresh :: MonadFresh m => (sa =~> sb) -> m (UnionM (sa =~> sb))

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => GenSymSimple (sa =~> sb) (sa =~> sb)

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

Methods

simpleFresh :: MonadFresh m => (sa =~> sb) -> m (sa =~> sb)

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca =-> cb)) => Solvable (ca =-> cb) (sa =~> sb)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

con :: (ca =-> cb) -> sa =~> sb

conView :: (sa =~> sb) -> Maybe (ca =-> cb)

sym :: Symbol -> sa =~> sb

ssym :: Identifier -> sa =~> sb

isym :: Identifier -> Int -> sa =~> sb

(SupportedPrim a, SupportedPrim b) => ToCon (a =~> b) (a =~> b)

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

Methods

toCon :: (a =~> b) -> Maybe (a =~> b)

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => ToCon (sa =~> sb) (ca =-> cb)

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

Methods

toCon :: (sa =~> sb) -> Maybe (ca =-> cb)

(SupportedPrim a, SupportedPrim b) => ToSym (a =~> b) (a =~> b)

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

Methods

toSym :: (a =~> b) -> a =~> b

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => ToSym (ca =-> cb) (sa =~> sb)

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

Methods

toSym :: (ca =-> cb) -> sa =~> sb

(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca =-> cb)) => LinkedRep (ca =-> cb) (sa =~> sb)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

underlyingTerm :: (sa =~> sb) -> Term (ca =-> cb)

wrapTerm :: Term (ca =-> cb) -> sa =~> sb

type FunType (sa =~> st)

Defined in Grisette.Internal.SymPrim.SymTabularFun

type FunType (sa =~> st) = sa -> FunType st

type ConType (a =~> b)

Defined in Grisette.Internal.SymPrim.SymTabularFun

type ConType (a =~> b) = ConType a =-> ConType b

data sa -~> sb where infixr 0

Symbolic general function type.

>>> :set -XTypeOperators -XOverloadedStrings
>>> f' = "f" :: SymInteger -~> SymInteger
>>> f = (f' #)
>>> f 1
(apply f 1)

>>> f' = con ("a" --> "a" + 1) :: SymInteger -~> SymInteger
>>> f'
\(a:ARG :: Integer) -> (+ 1 a:ARG)
>>> f = (f' #)
>>> f 1
2
>>> f 2
3
>>> f 3
4
>>> f "b"
(+ 1 b)

Constructors

SymGeneralFun :: (LinkedRep ca sa, LinkedRep cb sb) => Term (ca --> cb) -> sa -~> sb

Instances

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => GenSym () (sa -~> sb)

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

Methods

fresh :: MonadFresh m => () -> m (UnionM (sa -~> sb))

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => GenSymSimple () (sa -~> sb)

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

Methods

simpleFresh :: MonadFresh m => () -> m (sa -~> sb)

Lift (sa -~> sb :: Type)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

lift :: Quote m => (sa -~> sb) -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => (sa -~> sb) -> Code m (sa -~> sb)

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => ToSym (UnionM (ca --> cb)) (sa -~> sb)

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

Methods

toSym :: UnionM (ca --> cb) -> sa -~> sb

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => IsString (sa -~> sb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

fromString :: String -> sa -~> sb

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => Show (sa -~> sb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

showsPrec :: Int -> (sa -~> sb) -> ShowS

show :: (sa -~> sb) -> String

showList :: [sa -~> sb] -> ShowS

NFData (sa -~> sb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

rnf :: (sa -~> sb) -> ()

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => Eq (sa -~> sb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

(==) :: (sa -~> sb) -> (sa -~> sb) -> Bool

(/=) :: (sa -~> sb) -> (sa -~> sb) -> Bool

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => EvaluateSym (sa -~> sb)

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

Methods

evaluateSym :: Bool -> Model -> (sa -~> sb) -> sa -~> sb

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => ExtractSymbolics (sa -~> sb)

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

Methods

extractSymbolics :: (sa -~> sb) -> SymbolSet

(LinkedRep ca sa, LinkedRep ct st, Apply st, SupportedNonFuncPrim ca, SupportedPrim ct, SupportedPrim (ca --> ct)) => Apply (sa -~> st)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Associated Types

type FunType (sa -~> st)

Methods

apply :: (sa -~> st) -> FunType (sa -~> st)

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => GPretty (sa -~> sb)

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

Methods

gpretty :: (sa -~> sb) -> Doc ann

gprettyPrec :: Int -> (sa -~> sb) -> Doc ann

gprettyList :: [sa -~> sb] -> Doc ann

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => ITEOp (sa -~> sb)

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

Methods

symIte :: SymBool -> (sa -~> sb) -> (sa -~> sb) -> sa -~> sb

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => Mergeable (sa -~> sb)

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

Methods

rootStrategy :: MergingStrategy (sa -~> sb)

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => SimpleMergeable (sa -~> sb)

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

Methods

mrgIte :: SymBool -> (sa -~> sb) -> (sa -~> sb) -> sa -~> sb

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => SubstituteSym (sa -~> sb)

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

Methods

substituteSym :: LinkedRep cb sb0 => TypedSymbol cb -> sb0 -> (sa -~> sb) -> sa -~> sb

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => AllSyms (sa -~> sb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

allSymsS :: (sa -~> sb) -> [SomeSym] -> [SomeSym]

allSyms :: (sa -~> sb) -> [SomeSym]

(ConRep a, ConRep b) => ConRep (a -~> b)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Associated Types

type ConType (a -~> b)

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => Hashable (sa -~> sb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

hashWithSalt :: Int -> (sa -~> sb) -> Int

hash :: (sa -~> sb) -> Int

(SupportedNonFuncPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca --> cb)) => Function (sa -~> sb) sa sb

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

(#) :: (sa -~> sb) -> sa -> sb

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => GenSym (sa -~> sb) (sa -~> sb)

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

Methods

fresh :: MonadFresh m => (sa -~> sb) -> m (UnionM (sa -~> sb))

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => GenSymSimple (sa -~> sb) (sa -~> sb)

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

Methods

simpleFresh :: MonadFresh m => (sa -~> sb) -> m (sa -~> sb)

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca --> cb)) => Solvable (ca --> cb) (sa -~> sb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

con :: (ca --> cb) -> sa -~> sb

conView :: (sa -~> sb) -> Maybe (ca --> cb)

sym :: Symbol -> sa -~> sb

ssym :: Identifier -> sa -~> sb

isym :: Identifier -> Int -> sa -~> sb

(SupportedPrim a, SupportedPrim b) => ToCon (a -~> b) (a -~> b)

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

Methods

toCon :: (a -~> b) -> Maybe (a -~> b)

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => ToCon (sa -~> sb) (ca --> cb)

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

Methods

toCon :: (sa -~> sb) -> Maybe (ca --> cb)

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => ToSym (ca --> cb) (sa -~> sb)

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

Methods

toSym :: (ca --> cb) -> sa -~> sb

(SupportedPrim a, SupportedPrim b) => ToSym (a -~> b) (a -~> b)

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

Methods

toSym :: (a -~> b) -> a -~> b

(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim ca, SupportedPrim cb, SupportedPrim (ca --> cb)) => LinkedRep (ca --> cb) (sa -~> sb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

underlyingTerm :: (sa -~> sb) -> Term (ca --> cb)

wrapTerm :: Term (ca --> cb) -> sa -~> sb

type FunType (sa -~> st)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

type FunType (sa -~> st) = sa -> FunType st

type ConType (a -~> b)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

type ConType (a -~> b) = ConType a --> ConType b

data TypedSymbol t where

A typed symbol is a symbol that is associated with a type. Note that the same symbol bodies with different types are considered different symbols and can coexist in a term.

Simple symbols can be created with the OverloadedStrings extension:

>>> :set -XOverloadedStrings
>>> "a" :: TypedSymbol Bool
a :: Bool

Constructors

TypedSymbol

Fields

• :: SupportedPrim t
• => { unTypedSymbol :: Symbol
•    } -> TypedSymbol t

Instances

SymbolSetOps SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

emptySet :: SymbolSet

isEmptySet :: SymbolSet -> Bool

containsSymbol :: TypedSymbol a -> SymbolSet -> Bool

insertSymbol :: TypedSymbol a -> SymbolSet -> SymbolSet

intersectionSet :: SymbolSet -> SymbolSet -> SymbolSet

unionSet :: SymbolSet -> SymbolSet -> SymbolSet

differenceSet :: SymbolSet -> SymbolSet -> SymbolSet

ModelOps Model SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

emptyModel :: Model

isEmptyModel :: Model -> Bool

modelContains :: TypedSymbol a -> Model -> Bool

valueOf :: TypedSymbol t -> Model -> Maybe t

insertValue :: TypedSymbol t -> t -> Model -> Model

exceptFor :: SymbolSet -> Model -> Model

exceptFor' :: TypedSymbol t -> Model -> Model

restrictTo :: SymbolSet -> Model -> Model

extendTo :: SymbolSet -> Model -> Model

exact :: SymbolSet -> Model -> Model

Lift (TypedSymbol t :: Type)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

lift :: Quote m => TypedSymbol t -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => TypedSymbol t -> Code m (TypedSymbol t)

SupportedPrim t => IsString (TypedSymbol t)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

fromString :: String -> TypedSymbol t

Show (TypedSymbol t)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

showsPrec :: Int -> TypedSymbol t -> ShowS

show :: TypedSymbol t -> String

showList :: [TypedSymbol t] -> ShowS

NFData (TypedSymbol t)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

rnf :: TypedSymbol t -> ()

Eq (TypedSymbol t)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

(==) :: TypedSymbol t -> TypedSymbol t -> Bool

(/=) :: TypedSymbol t -> TypedSymbol t -> Bool

Ord (TypedSymbol t)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

compare :: TypedSymbol t -> TypedSymbol t -> Ordering

(<) :: TypedSymbol t -> TypedSymbol t -> Bool

(<=) :: TypedSymbol t -> TypedSymbol t -> Bool

(>) :: TypedSymbol t -> TypedSymbol t -> Bool

(>=) :: TypedSymbol t -> TypedSymbol t -> Bool

max :: TypedSymbol t -> TypedSymbol t -> TypedSymbol t

min :: TypedSymbol t -> TypedSymbol t -> TypedSymbol t

Hashable (TypedSymbol t)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

hashWithSalt :: Int -> TypedSymbol t -> Int

hash :: TypedSymbol t -> Int

SymbolSetRep (TypedSymbol t) SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: TypedSymbol t -> SymbolSet

SymbolSetRep (TypedSymbol a, TypedSymbol b) SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: (TypedSymbol a, TypedSymbol b) -> SymbolSet

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c) SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c) -> SymbolSet

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d) SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d) -> SymbolSet

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e) SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e) -> SymbolSet

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f) SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f) -> SymbolSet

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g) SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g) -> SymbolSet

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g, TypedSymbol h) SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g, TypedSymbol h) -> SymbolSet

symSize :: forall con sym. LinkedRep con sym => sym -> Int

Get the size of a symbolic term. Duplicate sub-terms are counted for only once.

>>> symSize (1 :: SymInteger)
1
>>> symSize ("a" :: SymInteger)
1
>>> symSize ("a" + 1 :: SymInteger)
3
>>> symSize (("a" + 1) * ("a" + 1) :: SymInteger)
4

symsSize :: forall con sym. LinkedRep con sym => [sym] -> Int

Get the sum of the sizes of a list of symbolic terms. Duplicate sub-terms are counted for only once.

>>> symsSize [1, "a" :: SymInteger, "a" + 1 :: SymInteger]
3

class AllSyms a where

Extract all symbolic primitive values that are represented as SMT terms.

Note: This type class can be derived for algebraic data types. You may need the DerivingVia and DerivingStrategies extenstions.

data X = ... deriving Generic deriving AllSyms via (Default X)

Minimal complete definition

allSymsS | allSyms

Methods

allSymsS :: a -> [SomeSym] -> [SomeSym]

Convert a value to a list of symbolic primitive values. It should prepend to an existing list of symbolic primitive values.

allSyms :: a -> [SomeSym]

Specialized allSymsS that prepends to an empty list.

Instances

AllSyms Int16

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Int16 -> [SomeSym] -> [SomeSym]

allSyms :: Int16 -> [SomeSym]

AllSyms Int32

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Int32 -> [SomeSym] -> [SomeSym]

allSyms :: Int32 -> [SomeSym]

AllSyms Int64

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Int64 -> [SomeSym] -> [SomeSym]

allSyms :: Int64 -> [SomeSym]

AllSyms Int8

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Int8 -> [SomeSym] -> [SomeSym]

allSyms :: Int8 -> [SomeSym]

AllSyms Word16

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Word16 -> [SomeSym] -> [SomeSym]

allSyms :: Word16 -> [SomeSym]

AllSyms Word32

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Word32 -> [SomeSym] -> [SomeSym]

allSyms :: Word32 -> [SomeSym]

AllSyms Word64

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Word64 -> [SomeSym] -> [SomeSym]

allSyms :: Word64 -> [SomeSym]

AllSyms Word8

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Word8 -> [SomeSym] -> [SomeSym]

allSyms :: Word8 -> [SomeSym]

AllSyms ByteString

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: ByteString -> [SomeSym] -> [SomeSym]

allSyms :: ByteString -> [SomeSym]

AllSyms AssertionError

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: AssertionError -> [SomeSym] -> [SomeSym]

allSyms :: AssertionError -> [SomeSym]

AllSyms VerificationConditions

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: VerificationConditions -> [SomeSym] -> [SomeSym]

allSyms :: VerificationConditions -> [SomeSym]

AllSyms SymBool

Defined in Grisette.Internal.SymPrim.SymBool

Methods

allSymsS :: SymBool -> [SomeSym] -> [SomeSym]

allSyms :: SymBool -> [SomeSym]

AllSyms SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

allSymsS :: SymInteger -> [SomeSym] -> [SomeSym]

allSyms :: SymInteger -> [SomeSym]

AllSyms Text

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Text -> [SomeSym] -> [SomeSym]

allSyms :: Text -> [SomeSym]

AllSyms Integer

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Integer -> [SomeSym] -> [SomeSym]

allSyms :: Integer -> [SomeSym]

AllSyms ()

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: () -> [SomeSym] -> [SomeSym]

allSyms :: () -> [SomeSym]

AllSyms Bool

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Bool -> [SomeSym] -> [SomeSym]

allSyms :: Bool -> [SomeSym]

AllSyms Char

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Char -> [SomeSym] -> [SomeSym]

allSyms :: Char -> [SomeSym]

AllSyms Int

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Int -> [SomeSym] -> [SomeSym]

allSyms :: Int -> [SomeSym]

AllSyms Word

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Word -> [SomeSym] -> [SomeSym]

allSyms :: Word -> [SomeSym]

AllSyms a => AllSyms (Identity a)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Identity a -> [SomeSym] -> [SomeSym]

allSyms :: Identity a -> [SomeSym]

(Generic a, AllSyms' (Rep a)) => AllSyms (Default a)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Default a -> [SomeSym] -> [SomeSym]

allSyms :: Default a -> [SomeSym]

AllSyms a => AllSyms (UnionM a)

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

Methods

allSymsS :: UnionM a -> [SomeSym] -> [SomeSym]

allSyms :: UnionM a -> [SomeSym]

AllSyms a => AllSyms (Union a)

Defined in Grisette.Internal.Core.Data.Union

Methods

allSymsS :: Union a -> [SomeSym] -> [SomeSym]

allSyms :: Union a -> [SomeSym]

(forall (n :: Nat). (KnownNat n, 1 <= n) => AllSyms (bv n)) => AllSyms (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

allSymsS :: SomeBV bv -> [SomeSym] -> [SomeSym]

allSyms :: SomeBV bv -> [SomeSym]

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

allSyms :: SymIntN n -> [SomeSym]

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

Defined in Grisette.Internal.SymPrim.SymBV

Methods

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

allSyms :: SymWordN n -> [SomeSym]

AllSyms a => AllSyms (Maybe a)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Maybe a -> [SomeSym] -> [SomeSym]

allSyms :: Maybe a -> [SomeSym]

AllSyms a => AllSyms [a]

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: [a] -> [SomeSym] -> [SomeSym]

allSyms :: [a] -> [SomeSym]

(AllSyms a, AllSyms b) => AllSyms (Either a b)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Either a b -> [SomeSym] -> [SomeSym]

allSyms :: Either a b -> [SomeSym]

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => AllSyms (sa -~> sb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

allSymsS :: (sa -~> sb) -> [SomeSym] -> [SomeSym]

allSyms :: (sa -~> sb) -> [SomeSym]

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => AllSyms (sa =~> sb)

Defined in Grisette.Internal.SymPrim.SymTabularFun

Methods

allSymsS :: (sa =~> sb) -> [SomeSym] -> [SomeSym]

allSyms :: (sa =~> sb) -> [SomeSym]

AllSyms (m (Maybe a)) => AllSyms (MaybeT m a)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: MaybeT m a -> [SomeSym] -> [SomeSym]

allSyms :: MaybeT m a -> [SomeSym]

(AllSyms a, AllSyms b) => AllSyms (a, b)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: (a, b) -> [SomeSym] -> [SomeSym]

allSyms :: (a, b) -> [SomeSym]

AllSyms (m (Either e a)) => AllSyms (ExceptT e m a)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: ExceptT e m a -> [SomeSym] -> [SomeSym]

allSyms :: ExceptT e m a -> [SomeSym]

AllSyms (m a) => AllSyms (IdentityT m a)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: IdentityT m a -> [SomeSym] -> [SomeSym]

allSyms :: IdentityT m a -> [SomeSym]

AllSyms (m (a, s)) => AllSyms (WriterT s m a)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: WriterT s m a -> [SomeSym] -> [SomeSym]

allSyms :: WriterT s m a -> [SomeSym]

AllSyms (m (a, s)) => AllSyms (WriterT s m a)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: WriterT s m a -> [SomeSym] -> [SomeSym]

allSyms :: WriterT s m a -> [SomeSym]

(AllSyms a, AllSyms b, AllSyms c) => AllSyms (a, b, c)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: (a, b, c) -> [SomeSym] -> [SomeSym]

allSyms :: (a, b, c) -> [SomeSym]

(AllSyms (f a), AllSyms (g a)) => AllSyms (Sum f g a)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: Sum f g a -> [SomeSym] -> [SomeSym]

allSyms :: Sum f g a -> [SomeSym]

(AllSyms a, AllSyms b, AllSyms c, AllSyms d) => AllSyms (a, b, c, d)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: (a, b, c, d) -> [SomeSym] -> [SomeSym]

allSyms :: (a, b, c, d) -> [SomeSym]

(AllSyms a, AllSyms b, AllSyms c, AllSyms d, AllSyms e) => AllSyms (a, b, c, d, e)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: (a, b, c, d, e) -> [SomeSym] -> [SomeSym]

allSyms :: (a, b, c, d, e) -> [SomeSym]

(AllSyms a, AllSyms b, AllSyms c, AllSyms d, AllSyms e, AllSyms f) => AllSyms (a, b, c, d, e, f)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: (a, b, c, d, e, f) -> [SomeSym] -> [SomeSym]

allSyms :: (a, b, c, d, e, f) -> [SomeSym]

(AllSyms a, AllSyms b, AllSyms c, AllSyms d, AllSyms e, AllSyms f, AllSyms g) => AllSyms (a, b, c, d, e, f, g)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: (a, b, c, d, e, f, g) -> [SomeSym] -> [SomeSym]

allSyms :: (a, b, c, d, e, f, g) -> [SomeSym]

(AllSyms a, AllSyms b, AllSyms c, AllSyms d, AllSyms e, AllSyms f, AllSyms g, AllSyms h) => AllSyms (a, b, c, d, e, f, g, h)

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

allSymsS :: (a, b, c, d, e, f, g, h) -> [SomeSym] -> [SomeSym]

allSyms :: (a, b, c, d, e, f, g, h) -> [SomeSym]

allSymsSize :: AllSyms a => a -> Int

Get the total size of symbolic terms in a value. Duplicate sub-terms are counted for only once.

>>> allSymsSize ("a" :: SymInteger, "a" + "b" :: SymInteger, ("a" + "b") * "c" :: SymInteger)
5

Symbolic constant sets and models

newtype SymbolSet

Symbolic constant set.

Constructors

SymbolSet

Fields

• unSymbolSet :: HashSet SomeTypedSymbol

Instances

Monoid SymbolSet

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

mempty :: SymbolSet

mappend :: SymbolSet -> SymbolSet -> SymbolSet

mconcat :: [SymbolSet] -> SymbolSet

Semigroup SymbolSet

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

(<>) :: SymbolSet -> SymbolSet -> SymbolSet

sconcat :: NonEmpty SymbolSet -> SymbolSet

stimes :: Integral b => b -> SymbolSet -> SymbolSet

Generic SymbolSet

Defined in Grisette.Internal.SymPrim.Prim.Model

Associated Types

type Rep SymbolSet :: Type -> Type

Methods

from :: SymbolSet -> Rep SymbolSet x

to :: Rep SymbolSet x -> SymbolSet

Show SymbolSet

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

showsPrec :: Int -> SymbolSet -> ShowS

show :: SymbolSet -> String

showList :: [SymbolSet] -> ShowS

Eq SymbolSet

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

(==) :: SymbolSet -> SymbolSet -> Bool

(/=) :: SymbolSet -> SymbolSet -> Bool

Hashable SymbolSet

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

hashWithSalt :: Int -> SymbolSet -> Int

hash :: SymbolSet -> Int

SymbolSetOps SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

emptySet :: SymbolSet

isEmptySet :: SymbolSet -> Bool

containsSymbol :: TypedSymbol a -> SymbolSet -> Bool

insertSymbol :: TypedSymbol a -> SymbolSet -> SymbolSet

intersectionSet :: SymbolSet -> SymbolSet -> SymbolSet

unionSet :: SymbolSet -> SymbolSet -> SymbolSet

differenceSet :: SymbolSet -> SymbolSet -> SymbolSet

ModelOps Model SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

emptyModel :: Model

isEmptyModel :: Model -> Bool

modelContains :: TypedSymbol a -> Model -> Bool

valueOf :: TypedSymbol t -> Model -> Maybe t

insertValue :: TypedSymbol t -> t -> Model -> Model

exceptFor :: SymbolSet -> Model -> Model

exceptFor' :: TypedSymbol t -> Model -> Model

restrictTo :: SymbolSet -> Model -> Model

extendTo :: SymbolSet -> Model -> Model

exact :: SymbolSet -> Model -> Model

SymbolSetRep (TypedSymbol t) SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: TypedSymbol t -> SymbolSet

SymbolSetRep (TypedSymbol a, TypedSymbol b) SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: (TypedSymbol a, TypedSymbol b) -> SymbolSet

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c) SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c) -> SymbolSet

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d) SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d) -> SymbolSet

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e) SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e) -> SymbolSet

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f) SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f) -> SymbolSet

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g) SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g) -> SymbolSet

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g, TypedSymbol h) SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g, TypedSymbol h) -> SymbolSet

type Rep SymbolSet

Defined in Grisette.Internal.SymPrim.Prim.Model

type Rep SymbolSet = D1 ('MetaData "SymbolSet" "Grisette.Internal.SymPrim.Prim.Model" "grisette-0.5.0.1-IKpKourvCOdG0l1QW5fLHa" 'True) (C1 ('MetaCons "SymbolSet" 'PrefixI 'True) (S1 ('MetaSel ('Just "unSymbolSet") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet SomeTypedSymbol))))

newtype Model

Model returned by the solver.

Constructors

Model

Fields

• unModel :: HashMap SomeTypedSymbol ModelValue

Instances

Monoid Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

mempty :: Model

mappend :: Model -> Model -> Model

mconcat :: [Model] -> Model

Semigroup Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

(<>) :: Model -> Model -> Model

sconcat :: NonEmpty Model -> Model

stimes :: Integral b => b -> Model -> Model

Generic Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Associated Types

type Rep Model :: Type -> Type

Methods

from :: Model -> Rep Model x

to :: Rep Model x -> Model

Show Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

showsPrec :: Int -> Model -> ShowS

show :: Model -> String

showList :: [Model] -> ShowS

Eq Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

(==) :: Model -> Model -> Bool

(/=) :: Model -> Model -> Bool

Hashable Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

hashWithSalt :: Int -> Model -> Int

hash :: Model -> Int

ModelOps Model SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

emptyModel :: Model

isEmptyModel :: Model -> Bool

modelContains :: TypedSymbol a -> Model -> Bool

valueOf :: TypedSymbol t -> Model -> Maybe t

insertValue :: TypedSymbol t -> t -> Model -> Model

exceptFor :: SymbolSet -> Model -> Model

exceptFor' :: TypedSymbol t -> Model -> Model

restrictTo :: SymbolSet -> Model -> Model

extendTo :: SymbolSet -> Model -> Model

exact :: SymbolSet -> Model -> Model

ModelRep (ModelValuePair t) Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildModel :: ModelValuePair t -> Model

ModelRep (ModelSymPair ct st) Model

Defined in Grisette.Internal.SymPrim.ModelRep

Methods

buildModel :: ModelSymPair ct st -> Model

(ModelRep a Model, ModelRep b Model) => ModelRep (a, b) Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildModel :: (a, b) -> Model

(ModelRep a Model, ModelRep b Model, ModelRep c Model) => ModelRep (a, b, c) Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildModel :: (a, b, c) -> Model

(ModelRep a Model, ModelRep b Model, ModelRep c Model, ModelRep d Model) => ModelRep (a, b, c, d) Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildModel :: (a, b, c, d) -> Model

(ModelRep a Model, ModelRep b Model, ModelRep c Model, ModelRep d Model, ModelRep e Model) => ModelRep (a, b, c, d, e) Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildModel :: (a, b, c, d, e) -> Model

(ModelRep a Model, ModelRep b Model, ModelRep c Model, ModelRep d Model, ModelRep e Model, ModelRep f Model) => ModelRep (a, b, c, d, e, f) Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildModel :: (a, b, c, d, e, f) -> Model

(ModelRep a Model, ModelRep b Model, ModelRep c Model, ModelRep d Model, ModelRep e Model, ModelRep f Model, ModelRep g Model) => ModelRep (a, b, c, d, e, f, g) Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildModel :: (a, b, c, d, e, f, g) -> Model

(ModelRep a Model, ModelRep b Model, ModelRep c Model, ModelRep d Model, ModelRep e Model, ModelRep f Model, ModelRep g Model, ModelRep h Model) => ModelRep (a, b, c, d, e, f, g, h) Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildModel :: (a, b, c, d, e, f, g, h) -> Model

type Rep Model

Defined in Grisette.Internal.SymPrim.Prim.Model

type Rep Model = D1 ('MetaData "Model" "Grisette.Internal.SymPrim.Prim.Model" "grisette-0.5.0.1-IKpKourvCOdG0l1QW5fLHa" 'True) (C1 ('MetaCons "Model" 'PrefixI 'True) (S1 ('MetaSel ('Just "unModel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap SomeTypedSymbol ModelValue))))

data ModelValuePair t

A type used for building a model by hand.

>>> buildModel ("x" ::= (1 :: Integer), "y" ::= True) :: Model
Model {x -> 1 :: Integer, y -> True :: Bool}

Constructors

(TypedSymbol t) ::= t

Instances

Show t => Show (ModelValuePair t)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

showsPrec :: Int -> ModelValuePair t -> ShowS

show :: ModelValuePair t -> String

showList :: [ModelValuePair t] -> ShowS

ModelRep (ModelValuePair t) Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildModel :: ModelValuePair t -> Model

data ModelSymPair ct st where

A pair of a symbolic constant and its value. This is used to build a model from a list of symbolic constants and their values.

>>> buildModel ("a" := (1 :: Integer), "b" := True) :: Model
Model {a -> 1 :: Integer, b -> True :: Bool}

Constructors

(:=) :: LinkedRep ct st => st -> ct -> ModelSymPair ct st

Instances

ModelRep (ModelSymPair ct st) Model

Defined in Grisette.Internal.SymPrim.ModelRep

Methods

buildModel :: ModelSymPair ct st -> Model