Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Documentation

bvIsNonZeroFromGEq1 :: forall w r proxy. 1 <= w => proxy w -> (BVIsNonZero w => r) -> r

Orphan instances

NonFuncSBVRep Integer

Associated Types

type NonFuncSBVBaseType n Integer

SBVRep Integer

Associated Types

type SBVType n Integer

SupportedNonFuncPrim Integer

Methods

conNonFuncSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> Integer -> SBV (NonFuncSBVBaseType n Integer)

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

withNonFuncPrim :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> ((SymVal (NonFuncSBVBaseType n Integer), EqSymbolic (SBVType n Integer), Mergeable (SBVType n Integer), SMTDefinable (SBVType n Integer), Mergeable (SBVType n Integer), SBVType n Integer ~ SBV (NonFuncSBVBaseType n Integer), PrimConstraint n Integer) => r) -> r

SupportedPrim Integer

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

SupportedPrimConstraint Integer

Associated Types

type PrimConstraint n Integer

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

Associated Types

type NonFuncSBVBaseType n (IntN w)

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

Associated Types

type NonFuncSBVBaseType n (WordN w)

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

Associated Types

type SBVType n (IntN w)

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

Associated Types

type SBVType n (WordN w)

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

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) => SupportedNonFuncPrim (WordN w)

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 (IntN w)

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)

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 (IntN w)

Associated Types

type PrimConstraint n (IntN w)

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

Associated Types

type PrimConstraint n (WordN w)