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

Documentation

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

Orphan instances

NonFuncSBVRep FPRoundingMode

Associated Types

type NonFuncSBVBaseType n FPRoundingMode

NonFuncSBVRep Integer

Associated Types

type NonFuncSBVBaseType n Integer

SBVRep FPRoundingMode

Associated Types

type SBVType n FPRoundingMode

SBVRep Integer

Associated Types

type SBVType n Integer

SupportedNonFuncPrim FPRoundingMode

Methods

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

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

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

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 FPRoundingMode

Methods

termCache :: Cache (Term FPRoundingMode)

pformatCon :: FPRoundingMode -> String

pformatSym :: TypedSymbol FPRoundingMode -> String

defaultValue :: FPRoundingMode

defaultValueDynamic :: proxy FPRoundingMode -> ModelValue

pevalITETerm :: Term Bool -> Term FPRoundingMode -> Term FPRoundingMode -> Term FPRoundingMode

pevalEqTerm :: Term FPRoundingMode -> Term FPRoundingMode -> Term Bool

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

symSBVName :: TypedSymbol FPRoundingMode -> Int -> String

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

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

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

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

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> FPRoundingMode

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 FPRoundingMode

Associated Types

type PrimConstraint n FPRoundingMode

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)

ValidFP eb sb => NonFuncSBVRep (FP eb sb)

Associated Types

type NonFuncSBVBaseType n (FP eb sb)

ValidFP eb sb => SBVRep (FP eb sb)

Associated Types

type SBVType n (FP eb sb)

ValidFP eb sb => SupportedNonFuncPrim (FP eb sb)

Methods

conNonFuncSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> FP eb sb -> SBV (NonFuncSBVBaseType n (FP eb sb))

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

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

ValidFP eb sb => SupportedPrim (FP eb sb)

Methods

termCache :: Cache (Term (FP eb sb))

pformatCon :: FP eb sb -> String

pformatSym :: TypedSymbol (FP eb sb) -> String

defaultValue :: FP eb sb

defaultValueDynamic :: proxy (FP eb sb) -> ModelValue

pevalITETerm :: Term Bool -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)

pevalEqTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term Bool

conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> FP eb sb -> SBVType n (FP eb sb)

symSBVName :: TypedSymbol (FP eb sb) -> Int -> String

symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (FP eb sb))

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

sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) -> SBVType n (FP eb sb)

sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> FP eb sb

ValidFP eb sb => SupportedPrimConstraint (FP eb sb)

Associated Types

type PrimConstraint n (FP eb sb)