Grisette.Internal.SymPrim.TabularFun

Documentation

data a =-> b infixr 0

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

>>> 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 (Union (ca =-> cb)) (sa =~> sb)

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

Methods

toSym :: Union (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

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

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

Methods

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

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

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

Methods

extractSym :: (a =-> b) -> AnySymbolSet

extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => (a =-> b) -> Maybe (SymbolSet knd)

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

Defined in Grisette.Internal.SymPrim.TabularFun

Associated Types

type SBVType (a =-> b)

(SupportedNonFuncPrim a0, SupportedNonFuncPrim a1, SupportedNonFuncPrim a2, SupportedNonFuncPrim a3, SupportedNonFuncPrim a4, SupportedNonFuncPrim a5, SupportedNonFuncPrim a6, SupportedNonFuncPrim a7) => SupportedPrim (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7)))))))

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

termCache :: Cache (Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))))

pformatCon :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> String

pformatSym :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> String

defaultValue :: a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))

defaultValueDynamic :: proxy (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7)))))))

pevalEqTerm :: Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> Term Bool

pevalDistinctTerm :: NonEmpty (Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7)))))))) -> Term Bool

conSBVTerm :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7)))))))

symSBVName :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> Int -> String

symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))))

withPrim :: ((PrimConstraint (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))), SMTDefinable (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7)))))))), Mergeable (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7)))))))), Typeable (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))))) => a) -> a

sbvIte :: SBV Bool -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7)))))))

sbvEq :: SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> SBV Bool

sbvDistinct :: NonEmpty (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7)))))))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))

castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> Maybe (TypedSymbol knd' (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))))

isFuncType :: Bool

funcDummyConstraint :: SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> SBV Bool

(SupportedNonFuncPrim a0, SupportedNonFuncPrim a1, SupportedNonFuncPrim a2, SupportedNonFuncPrim a3, SupportedNonFuncPrim a4, SupportedNonFuncPrim a5, SupportedNonFuncPrim a6) => SupportedPrim (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6))))))

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

termCache :: Cache (Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))))

pformatCon :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> String

pformatSym :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> String

defaultValue :: a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))

defaultValueDynamic :: proxy (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6))))))

pevalEqTerm :: Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> Term Bool

pevalDistinctTerm :: NonEmpty (Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6))))))) -> Term Bool

conSBVTerm :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6))))))

symSBVName :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> Int -> String

symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))))

withPrim :: ((PrimConstraint (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))), SMTDefinable (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6))))))), Mergeable (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6))))))), Typeable (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))))) => a) -> a

sbvIte :: SBV Bool -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6))))))

sbvEq :: SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> SBV Bool

sbvDistinct :: NonEmpty (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6))))))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))

castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> Maybe (TypedSymbol knd' (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))))

isFuncType :: Bool

funcDummyConstraint :: SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> SBV Bool

(SupportedNonFuncPrim a0, SupportedNonFuncPrim a1, SupportedNonFuncPrim a2, SupportedNonFuncPrim a3, SupportedNonFuncPrim a4, SupportedNonFuncPrim a5) => SupportedPrim (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5)))))

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

termCache :: Cache (Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))))

pformatCon :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> String

pformatSym :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> String

defaultValue :: a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))

defaultValueDynamic :: proxy (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5)))))

pevalEqTerm :: Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> Term Bool

pevalDistinctTerm :: NonEmpty (Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5)))))) -> Term Bool

conSBVTerm :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5)))))

symSBVName :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> Int -> String

symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))))

withPrim :: ((PrimConstraint (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))), SMTDefinable (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5)))))), Mergeable (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5)))))), Typeable (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))))) => a) -> a

sbvIte :: SBV Bool -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5)))))

sbvEq :: SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> SBV Bool

sbvDistinct :: NonEmpty (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5)))))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))

castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> Maybe (TypedSymbol knd' (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))))

isFuncType :: Bool

funcDummyConstraint :: SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> SBV Bool

(SupportedNonFuncPrim a0, SupportedNonFuncPrim a1, SupportedNonFuncPrim a2, SupportedNonFuncPrim a3, SupportedNonFuncPrim a4) => SupportedPrim (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4))))

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

termCache :: Cache (Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))))

pformatCon :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> String

pformatSym :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> String

defaultValue :: a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))

defaultValueDynamic :: proxy (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4))))

pevalEqTerm :: Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> Term Bool

pevalDistinctTerm :: NonEmpty (Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4))))) -> Term Bool

conSBVTerm :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4))))

symSBVName :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> Int -> String

symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))))

withPrim :: ((PrimConstraint (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))), SMTDefinable (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4))))), Mergeable (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4))))), Typeable (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))))) => a) -> a

sbvIte :: SBV Bool -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4))))

sbvEq :: SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> SBV Bool

sbvDistinct :: NonEmpty (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4))))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))

castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> Maybe (TypedSymbol knd' (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))))

isFuncType :: Bool

funcDummyConstraint :: SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> SBV Bool

(SupportedNonFuncPrim a0, SupportedNonFuncPrim a1, SupportedNonFuncPrim a2, SupportedNonFuncPrim a3) => SupportedPrim (a0 =-> (a1 =-> (a2 =-> a3)))

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

termCache :: Cache (Term (a0 =-> (a1 =-> (a2 =-> a3))))

pformatCon :: (a0 =-> (a1 =-> (a2 =-> a3))) -> String

pformatSym :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> a3))) -> String

defaultValue :: a0 =-> (a1 =-> (a2 =-> a3))

defaultValueDynamic :: proxy (a0 =-> (a1 =-> (a2 =-> a3))) -> ModelValue

pevalITETerm :: Term Bool -> Term (a0 =-> (a1 =-> (a2 =-> a3))) -> Term (a0 =-> (a1 =-> (a2 =-> a3))) -> Term (a0 =-> (a1 =-> (a2 =-> a3)))

pevalEqTerm :: Term (a0 =-> (a1 =-> (a2 =-> a3))) -> Term (a0 =-> (a1 =-> (a2 =-> a3))) -> Term Bool

pevalDistinctTerm :: NonEmpty (Term (a0 =-> (a1 =-> (a2 =-> a3)))) -> Term Bool

conSBVTerm :: (a0 =-> (a1 =-> (a2 =-> a3))) -> SBVType (a0 =-> (a1 =-> (a2 =-> a3)))

symSBVName :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> a3))) -> Int -> String

symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 =-> (a1 =-> (a2 =-> a3))))

withPrim :: ((PrimConstraint (a0 =-> (a1 =-> (a2 =-> a3))), SMTDefinable (SBVType (a0 =-> (a1 =-> (a2 =-> a3)))), Mergeable (SBVType (a0 =-> (a1 =-> (a2 =-> a3)))), Typeable (SBVType (a0 =-> (a1 =-> (a2 =-> a3))))) => a) -> a

sbvIte :: SBV Bool -> SBVType (a0 =-> (a1 =-> (a2 =-> a3))) -> SBVType (a0 =-> (a1 =-> (a2 =-> a3))) -> SBVType (a0 =-> (a1 =-> (a2 =-> a3)))

sbvEq :: SBVType (a0 =-> (a1 =-> (a2 =-> a3))) -> SBVType (a0 =-> (a1 =-> (a2 =-> a3))) -> SBV Bool

sbvDistinct :: NonEmpty (SBVType (a0 =-> (a1 =-> (a2 =-> a3)))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 =-> (a1 =-> (a2 =-> a3))

castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 =-> (a1 =-> (a2 =-> a3))) -> Maybe (TypedSymbol knd' (a0 =-> (a1 =-> (a2 =-> a3))))

isFuncType :: Bool

funcDummyConstraint :: SBVType (a0 =-> (a1 =-> (a2 =-> a3))) -> SBV Bool

(SupportedNonFuncPrim a0, SupportedNonFuncPrim a1, SupportedNonFuncPrim a2) => SupportedPrim (a0 =-> (a1 =-> a2))

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

termCache :: Cache (Term (a0 =-> (a1 =-> a2)))

pformatCon :: (a0 =-> (a1 =-> a2)) -> String

pformatSym :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> a2)) -> String

defaultValue :: a0 =-> (a1 =-> a2)

defaultValueDynamic :: proxy (a0 =-> (a1 =-> a2)) -> ModelValue

pevalITETerm :: Term Bool -> Term (a0 =-> (a1 =-> a2)) -> Term (a0 =-> (a1 =-> a2)) -> Term (a0 =-> (a1 =-> a2))

pevalEqTerm :: Term (a0 =-> (a1 =-> a2)) -> Term (a0 =-> (a1 =-> a2)) -> Term Bool

pevalDistinctTerm :: NonEmpty (Term (a0 =-> (a1 =-> a2))) -> Term Bool

conSBVTerm :: (a0 =-> (a1 =-> a2)) -> SBVType (a0 =-> (a1 =-> a2))

symSBVName :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> a2)) -> Int -> String

symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 =-> (a1 =-> a2)))

withPrim :: ((PrimConstraint (a0 =-> (a1 =-> a2)), SMTDefinable (SBVType (a0 =-> (a1 =-> a2))), Mergeable (SBVType (a0 =-> (a1 =-> a2))), Typeable (SBVType (a0 =-> (a1 =-> a2)))) => a) -> a

sbvIte :: SBV Bool -> SBVType (a0 =-> (a1 =-> a2)) -> SBVType (a0 =-> (a1 =-> a2)) -> SBVType (a0 =-> (a1 =-> a2))

sbvEq :: SBVType (a0 =-> (a1 =-> a2)) -> SBVType (a0 =-> (a1 =-> a2)) -> SBV Bool

sbvDistinct :: NonEmpty (SBVType (a0 =-> (a1 =-> a2))) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 =-> (a1 =-> a2)

castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 =-> (a1 =-> a2)) -> Maybe (TypedSymbol knd' (a0 =-> (a1 =-> a2)))

isFuncType :: Bool

funcDummyConstraint :: SBVType (a0 =-> (a1 =-> a2)) -> SBV Bool

(SupportedNonFuncPrim a0, SupportedNonFuncPrim a1) => SupportedPrim (a0 =-> a1)

Defined in Grisette.Internal.SymPrim.TabularFun

Methods

termCache :: Cache (Term (a0 =-> a1))

pformatCon :: (a0 =-> a1) -> String

pformatSym :: TypedSymbol 'AnyKind (a0 =-> a1) -> String

defaultValue :: a0 =-> a1

defaultValueDynamic :: proxy (a0 =-> a1) -> ModelValue

pevalITETerm :: Term Bool -> Term (a0 =-> a1) -> Term (a0 =-> a1) -> Term (a0 =-> a1)

pevalEqTerm :: Term (a0 =-> a1) -> Term (a0 =-> a1) -> Term Bool

pevalDistinctTerm :: NonEmpty (Term (a0 =-> a1)) -> Term Bool

conSBVTerm :: (a0 =-> a1) -> SBVType (a0 =-> a1)

symSBVName :: TypedSymbol 'AnyKind (a0 =-> a1) -> Int -> String

symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 =-> a1))

withPrim :: ((PrimConstraint (a0 =-> a1), SMTDefinable (SBVType (a0 =-> a1)), Mergeable (SBVType (a0 =-> a1)), Typeable (SBVType (a0 =-> a1))) => a) -> a

sbvIte :: SBV Bool -> SBVType (a0 =-> a1) -> SBVType (a0 =-> a1) -> SBVType (a0 =-> a1)

sbvEq :: SBVType (a0 =-> a1) -> SBVType (a0 =-> a1) -> SBV Bool

sbvDistinct :: NonEmpty (SBVType (a0 =-> a1)) -> SBV Bool

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 =-> a1

castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 =-> a1) -> Maybe (TypedSymbol knd' (a0 =-> a1))

isFuncType :: Bool

funcDummyConstraint :: SBVType (a0 =-> a1) -> SBV Bool

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

Defined in Grisette.Internal.SymPrim.TabularFun

Associated Types

type PrimConstraint (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 :: SBVType (a =-> b) -> SBVType a -> SBVType 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.8.0.0-9ziui23pS5H4p62qxsVv1c" '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 Rep (a =-> b)

Defined in Grisette.Internal.SymPrim.TabularFun

type Rep (a =-> b) = D1 ('MetaData "=->" "Grisette.Internal.SymPrim.TabularFun" "grisette-0.8.0.0-9ziui23pS5H4p62qxsVv1c" '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 PrimConstraint (a =-> b)

Defined in Grisette.Internal.SymPrim.TabularFun

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

type SBVType (a =-> b)

Defined in Grisette.Internal.SymPrim.TabularFun

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

type SymType (a =-> b)

Defined in Grisette.Internal.SymPrim.SymTabularFun

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