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

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

Contents

Orphan instances

Description

Documentation

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

Orphan instances

NonFuncSBVRep Integer Source #
Instance details Associated Types type NonFuncSBVBaseType n Integer Source #
SBVRep Integer Source #
Instance details Associated Types type SBVType n Integer Source #
SupportedNonFuncPrim Integer Source #
Instance details Methods conNonFuncSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> Integer -> SBV (NonFuncSBVBaseType n Integer) Source # symNonFuncSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBV (NonFuncSBVBaseType n Integer)) Source # 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 Source #
SupportedPrim Integer Source #
Instance details Methods termCache :: Cache (Term Integer) Source # pformatCon :: Integer -> String Source # pformatSym :: TypedSymbol Integer -> String Source # defaultValue :: Integer Source # defaultValueDynamic :: proxy Integer -> ModelValue Source # pevalITETerm :: Term Bool -> Term Integer -> Term Integer -> Term Integer Source # pevalEqTerm :: Term Integer -> Term Integer -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> Integer -> SBVType n Integer Source # symSBVName :: TypedSymbol Integer -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n Integer) Source # 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 Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n Integer -> SBVType n Integer -> SBVType n Integer Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n Integer -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> Integer Source #
SupportedPrimConstraint Integer Source #
Instance details Associated Types type PrimConstraint n Integer Source #
(KnownNat w, 1 <= w) => NonFuncSBVRep (IntN w) Source #
Instance details Associated Types type NonFuncSBVBaseType n (IntN w) Source #
(KnownNat w, 1 <= w) => NonFuncSBVRep (WordN w) Source #
Instance details Associated Types type NonFuncSBVBaseType n (WordN w) Source #
(KnownNat w, 1 <= w) => SBVRep (IntN w) Source #
Instance details Associated Types type SBVType n (IntN w) Source #
(KnownNat w, 1 <= w) => SBVRep (WordN w) Source #
Instance details Associated Types type SBVType n (WordN w) Source #
(KnownNat w, 1 <= w) => SupportedNonFuncPrim (IntN w) Source #
Instance details Methods conNonFuncSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> IntN w -> SBV (NonFuncSBVBaseType n (IntN w)) Source # symNonFuncSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBV (NonFuncSBVBaseType n (IntN w))) Source # withNonFuncPrim :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> ((SymVal (NonFuncSBVBaseType n (IntN w)), EqSymbolic (SBVType n (IntN w)), Mergeable (SBVType n (IntN w)), SMTDefinable (SBVType n (IntN w)), Mergeable (SBVType n (IntN w)), SBVType n (IntN w) ~ SBV (NonFuncSBVBaseType n (IntN w)), PrimConstraint n (IntN w)) => r) -> r Source #
(KnownNat w, 1 <= w) => SupportedNonFuncPrim (WordN w) Source #
Instance details Methods conNonFuncSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> WordN w -> SBV (NonFuncSBVBaseType n (WordN w)) Source # symNonFuncSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBV (NonFuncSBVBaseType n (WordN w))) Source # withNonFuncPrim :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> ((SymVal (NonFuncSBVBaseType n (WordN w)), EqSymbolic (SBVType n (WordN w)), Mergeable (SBVType n (WordN w)), SMTDefinable (SBVType n (WordN w)), Mergeable (SBVType n (WordN w)), SBVType n (WordN w) ~ SBV (NonFuncSBVBaseType n (WordN w)), PrimConstraint n (WordN w)) => r) -> r Source #
(KnownNat w, 1 <= w) => SupportedPrim (IntN w) Source #
Instance details Methods termCache :: Cache (Term (IntN w)) Source # pformatCon :: IntN w -> String Source # pformatSym :: TypedSymbol (IntN w) -> String Source # defaultValue :: IntN w Source # defaultValueDynamic :: proxy (IntN w) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (IntN w) -> Term (IntN w) -> Term (IntN w) Source # pevalEqTerm :: Term (IntN w) -> Term (IntN w) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> IntN w -> SBVType n (IntN w) Source # symSBVName :: TypedSymbol (IntN w) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (IntN w)) Source # withPrim :: forall (n :: Nat) p a. KnownIsZero n => p n -> ((PrimConstraint n (IntN w), SMTDefinable (SBVType n (IntN w)), Mergeable (SBVType n (IntN w)), Typeable (SBVType n (IntN w))) => a) -> a Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (IntN w) -> SBVType n (IntN w) -> SBVType n (IntN w) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (IntN w) -> SBVType n (IntN w) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> IntN w Source #
(KnownNat w, 1 <= w) => SupportedPrim (WordN w) Source #
Instance details Methods termCache :: Cache (Term (WordN w)) Source # pformatCon :: WordN w -> String Source # pformatSym :: TypedSymbol (WordN w) -> String Source # defaultValue :: WordN w Source # defaultValueDynamic :: proxy (WordN w) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (WordN w) -> Term (WordN w) -> Term (WordN w) Source # pevalEqTerm :: Term (WordN w) -> Term (WordN w) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> WordN w -> SBVType n (WordN w) Source # symSBVName :: TypedSymbol (WordN w) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (WordN w)) Source # withPrim :: forall (n :: Nat) p a. KnownIsZero n => p n -> ((PrimConstraint n (WordN w), SMTDefinable (SBVType n (WordN w)), Mergeable (SBVType n (WordN w)), Typeable (SBVType n (WordN w))) => a) -> a Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (WordN w) -> SBVType n (WordN w) -> SBVType n (WordN w) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (WordN w) -> SBVType n (WordN w) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> WordN w Source #
(KnownNat w, 1 <= w) => SupportedPrimConstraint (IntN w) Source #
Instance details Associated Types type PrimConstraint n (IntN w) Source #
(KnownNat w, 1 <= w) => SupportedPrimConstraint (WordN w) Source #
Instance details Associated Types type PrimConstraint n (WordN w) Source #