Copyright	(c) Sirui Lu 2021-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.TabularFun

Description

Synopsis

data a =-> b = TabularFun {
- funcTable :: [(a, b)]
- defaultFuncValue :: b
}

Documentation

data a =-> b infixr 0 Source #

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

Instances details

Generic1 ((=->) a :: Type -> Type) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods liftRnf :: (a0 -> ()) -> (a =-> a0) -> () #
(SupportedPrim (ca =-> cb), SupportedNonFuncPrim ca, LinkedRep ca sa, LinkedRep cb sb) => ToSym (Union (ca =-> cb)) (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods toSym :: Union (ca =-> cb) -> sa =~> sb Source #
Generic (a =-> b) Source #
Instance details 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) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods showsPrec :: Int -> (a =-> b) -> ShowS # show :: (a =-> b) -> String # showList :: [a =-> b] -> ShowS #
(Serial a, Serial b) => Binary (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods put :: (a =-> b) -> Put # get :: Get (a =-> b) # putList :: [a =-> b] -> Put #
(Serial a, Serial b) => Serial (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods serialize :: MonadPut m => (a =-> b) -> m () # deserialize :: MonadGet m => m (a =-> b) #
(Serial a, Serial b) => Serialize (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods put :: Putter (a =-> b) # get :: Get (a =-> b) #
(NFData a, NFData b) => NFData (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods rnf :: (a =-> b) -> () #
(Eq a, Eq b) => Eq (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods (==) :: (a =-> b) -> (a =-> b) -> Bool # (/=) :: (a =-> b) -> (a =-> b) -> Bool #
(Apply t, Eq a) => Apply (a =-> t) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Associated Types type FunType (a =-> t) Source # Methods apply :: (a =-> t) -> FunType (a =-> t) Source #
(EvalSym a, EvalSym b) => EvalSym (a =-> b) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> (a =-> b) -> a =-> b Source #
(ExtractSym a, ExtractSym b) => ExtractSym (a =-> b) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ExtractSym Methods extractSym :: (a =-> b) -> AnySymbolSet Source # extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => (a =-> b) -> Maybe (SymbolSet knd) Source #
Mergeable (a =-> b) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy (a =-> b) Source #
(Show a, Show b) => PPrint (a =-> b) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.PPrint Methods pformat :: (a =-> b) -> Doc ann Source # pformatPrec :: Int -> (a =-> b) -> Doc ann Source # pformatList :: [a =-> b] -> Doc ann Source #
(SubstSym a, SubstSym b) => SubstSym (a =-> b) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> (a =-> b) -> a =-> b Source #
(SupportedNonFuncPrim a, SupportedPrim b) => SBVRep (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Associated Types type SBVType (a =-> b) Source #
(SupportedNonFuncPrim a0, Eq a0, Show a0, Hashable a0, Typeable a0, SupportedNonFuncPrim a1, Eq a1, Show a1, Hashable a1, Typeable a1, SupportedNonFuncPrim a2, Eq a2, Show a2, Hashable a2, Typeable a2, SupportedNonFuncPrim a3, Eq a3, Show a3, Hashable a3, Typeable a3, SupportedNonFuncPrim a4, Eq a4, Show a4, Hashable a4, Typeable a4, SupportedNonFuncPrim a5, Eq a5, Show a5, Hashable a5, Typeable a5, SupportedNonFuncPrim a6, Eq a6, Show a6, Hashable a6, Typeable a6, SupportedNonFuncPrim a7, Eq a7, Show a7, Hashable a7, Typeable a7) => SupportedPrim (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods primTypeRep :: TypeRep (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) Source # sameCon :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> Bool Source # hashConWithSalt :: Int -> (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> Int Source # pformatCon :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> String Source # defaultValue :: a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7)))))) Source # 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))))))) Source # pevalEqTerm :: Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> Term Bool Source # pevalDistinctTerm :: NonEmpty (Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7)))))))) -> Term Bool Source # conSBVTerm :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) Source # symSBVName :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> Int -> String Source # symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7)))))))) Source # 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 Source # 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))))))) Source # sbvEq :: SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> SBV Bool Source # sbvDistinct :: NonEmpty (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7)))))))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7)))))) Source # 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)))))))) Source # funcDummyConstraint :: SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> SBV Bool Source #
(SupportedNonFuncPrim a0, Eq a0, Show a0, Hashable a0, Typeable a0, SupportedNonFuncPrim a1, Eq a1, Show a1, Hashable a1, Typeable a1, SupportedNonFuncPrim a2, Eq a2, Show a2, Hashable a2, Typeable a2, SupportedNonFuncPrim a3, Eq a3, Show a3, Hashable a3, Typeable a3, SupportedNonFuncPrim a4, Eq a4, Show a4, Hashable a4, Typeable a4, SupportedNonFuncPrim a5, Eq a5, Show a5, Hashable a5, Typeable a5, SupportedNonFuncPrim a6, Eq a6, Show a6, Hashable a6, Typeable a6) => SupportedPrim (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods primTypeRep :: TypeRep (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) Source # sameCon :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> Bool Source # hashConWithSalt :: Int -> (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> Int Source # pformatCon :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> String Source # defaultValue :: a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6))))) Source # 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)))))) Source # pevalEqTerm :: Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> Term Bool Source # pevalDistinctTerm :: NonEmpty (Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6))))))) -> Term Bool Source # conSBVTerm :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) Source # symSBVName :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> Int -> String Source # symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6))))))) Source # 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 Source # 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)))))) Source # sbvEq :: SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> SBV Bool Source # sbvDistinct :: NonEmpty (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6))))))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6))))) Source # 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))))))) Source # funcDummyConstraint :: SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> SBV Bool Source #
(SupportedNonFuncPrim a0, Eq a0, Show a0, Hashable a0, Typeable a0, SupportedNonFuncPrim a1, Eq a1, Show a1, Hashable a1, Typeable a1, SupportedNonFuncPrim a2, Eq a2, Show a2, Hashable a2, Typeable a2, SupportedNonFuncPrim a3, Eq a3, Show a3, Hashable a3, Typeable a3, SupportedNonFuncPrim a4, Eq a4, Show a4, Hashable a4, Typeable a4, SupportedNonFuncPrim a5, Eq a5, Show a5, Hashable a5, Typeable a5) => SupportedPrim (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods primTypeRep :: TypeRep (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) Source # sameCon :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> Bool Source # hashConWithSalt :: Int -> (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> Int Source # pformatCon :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> String Source # defaultValue :: a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5)))) Source # pevalITETerm :: Term Bool -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) Source # pevalEqTerm :: Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> Term Bool Source # pevalDistinctTerm :: NonEmpty (Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5)))))) -> Term Bool Source # conSBVTerm :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) Source # symSBVName :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> Int -> String Source # symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5)))))) Source # 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 Source # sbvIte :: SBV Bool -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) Source # sbvEq :: SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> SBV Bool Source # sbvDistinct :: NonEmpty (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5)))))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5)))) Source # 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)))))) Source # funcDummyConstraint :: SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> SBV Bool Source #
(SupportedNonFuncPrim a0, Eq a0, Show a0, Hashable a0, Typeable a0, SupportedNonFuncPrim a1, Eq a1, Show a1, Hashable a1, Typeable a1, SupportedNonFuncPrim a2, Eq a2, Show a2, Hashable a2, Typeable a2, SupportedNonFuncPrim a3, Eq a3, Show a3, Hashable a3, Typeable a3, SupportedNonFuncPrim a4, Eq a4, Show a4, Hashable a4, Typeable a4) => SupportedPrim (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods primTypeRep :: TypeRep (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) Source # sameCon :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> Bool Source # hashConWithSalt :: Int -> (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> Int Source # pformatCon :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> String Source # defaultValue :: a0 =-> (a1 =-> (a2 =-> (a3 =-> a4))) Source # pevalITETerm :: Term Bool -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) Source # pevalEqTerm :: Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> Term Bool Source # pevalDistinctTerm :: NonEmpty (Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4))))) -> Term Bool Source # conSBVTerm :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) Source # symSBVName :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> Int -> String Source # symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4))))) Source # 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 Source # sbvIte :: SBV Bool -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) Source # sbvEq :: SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> SBV Bool Source # sbvDistinct :: NonEmpty (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4))))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 =-> (a1 =-> (a2 =-> (a3 =-> a4))) Source # castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> Maybe (TypedSymbol knd' (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4))))) Source # funcDummyConstraint :: SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> SBV Bool Source #
(SupportedNonFuncPrim a0, Eq a0, Show a0, Hashable a0, Typeable a0, SupportedNonFuncPrim a1, Eq a1, Show a1, Hashable a1, Typeable a1, SupportedNonFuncPrim a2, Eq a2, Show a2, Hashable a2, Typeable a2, SupportedNonFuncPrim a3, Eq a3, Show a3, Hashable a3, Typeable a3) => SupportedPrim (a0 =-> (a1 =-> (a2 =-> a3))) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods primTypeRep :: TypeRep (a0 =-> (a1 =-> (a2 =-> a3))) Source # sameCon :: (a0 =-> (a1 =-> (a2 =-> a3))) -> (a0 =-> (a1 =-> (a2 =-> a3))) -> Bool Source # hashConWithSalt :: Int -> (a0 =-> (a1 =-> (a2 =-> a3))) -> Int Source # pformatCon :: (a0 =-> (a1 =-> (a2 =-> a3))) -> String Source # defaultValue :: a0 =-> (a1 =-> (a2 =-> a3)) Source # pevalITETerm :: Term Bool -> Term (a0 =-> (a1 =-> (a2 =-> a3))) -> Term (a0 =-> (a1 =-> (a2 =-> a3))) -> Term (a0 =-> (a1 =-> (a2 =-> a3))) Source # pevalEqTerm :: Term (a0 =-> (a1 =-> (a2 =-> a3))) -> Term (a0 =-> (a1 =-> (a2 =-> a3))) -> Term Bool Source # pevalDistinctTerm :: NonEmpty (Term (a0 =-> (a1 =-> (a2 =-> a3)))) -> Term Bool Source # conSBVTerm :: (a0 =-> (a1 =-> (a2 =-> a3))) -> SBVType (a0 =-> (a1 =-> (a2 =-> a3))) Source # symSBVName :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> a3))) -> Int -> String Source # symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 =-> (a1 =-> (a2 =-> a3)))) Source # 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 Source # sbvIte :: SBV Bool -> SBVType (a0 =-> (a1 =-> (a2 =-> a3))) -> SBVType (a0 =-> (a1 =-> (a2 =-> a3))) -> SBVType (a0 =-> (a1 =-> (a2 =-> a3))) Source # sbvEq :: SBVType (a0 =-> (a1 =-> (a2 =-> a3))) -> SBVType (a0 =-> (a1 =-> (a2 =-> a3))) -> SBV Bool Source # sbvDistinct :: NonEmpty (SBVType (a0 =-> (a1 =-> (a2 =-> a3)))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 =-> (a1 =-> (a2 =-> a3)) Source # castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 =-> (a1 =-> (a2 =-> a3))) -> Maybe (TypedSymbol knd' (a0 =-> (a1 =-> (a2 =-> a3)))) Source # funcDummyConstraint :: SBVType (a0 =-> (a1 =-> (a2 =-> a3))) -> SBV Bool Source #
(SupportedNonFuncPrim a0, Eq a0, Show a0, Hashable a0, Typeable a0, SupportedNonFuncPrim a1, Eq a1, Show a1, Hashable a1, Typeable a1, SupportedNonFuncPrim a2, Eq a2, Show a2, Hashable a2, Typeable a2) => SupportedPrim (a0 =-> (a1 =-> a2)) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods primTypeRep :: TypeRep (a0 =-> (a1 =-> a2)) Source # sameCon :: (a0 =-> (a1 =-> a2)) -> (a0 =-> (a1 =-> a2)) -> Bool Source # hashConWithSalt :: Int -> (a0 =-> (a1 =-> a2)) -> Int Source # pformatCon :: (a0 =-> (a1 =-> a2)) -> String Source # defaultValue :: a0 =-> (a1 =-> a2) Source # pevalITETerm :: Term Bool -> Term (a0 =-> (a1 =-> a2)) -> Term (a0 =-> (a1 =-> a2)) -> Term (a0 =-> (a1 =-> a2)) Source # pevalEqTerm :: Term (a0 =-> (a1 =-> a2)) -> Term (a0 =-> (a1 =-> a2)) -> Term Bool Source # pevalDistinctTerm :: NonEmpty (Term (a0 =-> (a1 =-> a2))) -> Term Bool Source # conSBVTerm :: (a0 =-> (a1 =-> a2)) -> SBVType (a0 =-> (a1 =-> a2)) Source # symSBVName :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> a2)) -> Int -> String Source # symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 =-> (a1 =-> a2))) Source # withPrim :: ((PrimConstraint (a0 =-> (a1 =-> a2)), SMTDefinable (SBVType (a0 =-> (a1 =-> a2))), Mergeable (SBVType (a0 =-> (a1 =-> a2))), Typeable (SBVType (a0 =-> (a1 =-> a2)))) => a) -> a Source # sbvIte :: SBV Bool -> SBVType (a0 =-> (a1 =-> a2)) -> SBVType (a0 =-> (a1 =-> a2)) -> SBVType (a0 =-> (a1 =-> a2)) Source # sbvEq :: SBVType (a0 =-> (a1 =-> a2)) -> SBVType (a0 =-> (a1 =-> a2)) -> SBV Bool Source # sbvDistinct :: NonEmpty (SBVType (a0 =-> (a1 =-> a2))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 =-> (a1 =-> a2) Source # castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 =-> (a1 =-> a2)) -> Maybe (TypedSymbol knd' (a0 =-> (a1 =-> a2))) Source # funcDummyConstraint :: SBVType (a0 =-> (a1 =-> a2)) -> SBV Bool Source #
(SupportedNonFuncPrim a0, Eq a0, Show a0, Hashable a0, Typeable a0, SupportedNonFuncPrim a1, Eq a1, Show a1, Hashable a1, Typeable a1) => SupportedPrim (a0 =-> a1) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods primTypeRep :: TypeRep (a0 =-> a1) Source # sameCon :: (a0 =-> a1) -> (a0 =-> a1) -> Bool Source # hashConWithSalt :: Int -> (a0 =-> a1) -> Int Source # pformatCon :: (a0 =-> a1) -> String Source # defaultValue :: a0 =-> a1 Source # pevalITETerm :: Term Bool -> Term (a0 =-> a1) -> Term (a0 =-> a1) -> Term (a0 =-> a1) Source # pevalEqTerm :: Term (a0 =-> a1) -> Term (a0 =-> a1) -> Term Bool Source # pevalDistinctTerm :: NonEmpty (Term (a0 =-> a1)) -> Term Bool Source # conSBVTerm :: (a0 =-> a1) -> SBVType (a0 =-> a1) Source # symSBVName :: TypedSymbol 'AnyKind (a0 =-> a1) -> Int -> String Source # symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 =-> a1)) Source # withPrim :: ((PrimConstraint (a0 =-> a1), SMTDefinable (SBVType (a0 =-> a1)), Mergeable (SBVType (a0 =-> a1)), Typeable (SBVType (a0 =-> a1))) => a) -> a Source # sbvIte :: SBV Bool -> SBVType (a0 =-> a1) -> SBVType (a0 =-> a1) -> SBVType (a0 =-> a1) Source # sbvEq :: SBVType (a0 =-> a1) -> SBVType (a0 =-> a1) -> SBV Bool Source # sbvDistinct :: NonEmpty (SBVType (a0 =-> a1)) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 =-> a1 Source # castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 =-> a1) -> Maybe (TypedSymbol knd' (a0 =-> a1)) Source # funcDummyConstraint :: SBVType (a0 =-> a1) -> SBV Bool Source #
(SupportedNonFuncPrim a, SupportedPrim b) => SupportedPrimConstraint (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Associated Types type PrimConstraint (a =-> b) Source #
(SymRep a, SymRep b, SupportedPrim (a =-> b)) => SymRep (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymTabularFun Associated Types type SymType (a =-> b) Source #
(Hashable a, Hashable b) => Hashable (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods hashWithSalt :: Int -> (a =-> b) -> Int # hash :: (a =-> b) -> Int #
Eq a => Function (a =-> b) a b Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods (#) :: (a =-> b) -> a -> b Source #
(SupportedPrim a, SupportedPrim b, Eq a, SupportedPrim (a =-> b)) => PEvalApplyTerm (a =-> b) a b Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods pevalApplyTerm :: Term (a =-> b) -> Term a -> Term b Source # sbvApplyTerm :: SBVType (a =-> b) -> SBVType a -> SBVType b Source #
(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca =-> cb), SupportedNonFuncPrim ca) => Solvable (ca =-> cb) (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymTabularFun Methods con :: (ca =-> cb) -> sa =~> sb Source # conView :: (sa =~> sb) -> Maybe (ca =-> cb) Source # sym :: Symbol -> sa =~> sb Source # ssym :: Identifier -> sa =~> sb Source # isym :: Identifier -> Int -> sa =~> sb Source #
(LinkedRep ca sa, LinkedRep cb sb) => ToCon (sa =~> sb) (ca =-> cb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: (sa =~> sb) -> Maybe (ca =-> cb) Source #
ToCon (a =-> b) (a =-> b) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon Methods toCon :: (a =-> b) -> Maybe (a =-> b) Source #
ToSym (a =-> b) (a =-> b) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: (a =-> b) -> a =-> b Source #
(SupportedPrim (ca =-> cb), SupportedNonFuncPrim ca, LinkedRep ca sa, LinkedRep cb sb) => ToSym (ca =-> cb) (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym Methods toSym :: (ca =-> cb) -> sa =~> sb Source #
(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca =-> cb), SupportedNonFuncPrim ca) => LinkedRep (ca =-> cb) (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymTabularFun Methods underlyingTerm :: (sa =~> sb) -> Term (ca =-> cb) Source # wrapTerm :: Term (ca =-> cb) -> sa =~> sb Source #
type Rep1 ((=->) a :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun type Rep1 ((=->) a :: Type -> Type) = D1 ('MetaData "=->" "Grisette.Internal.SymPrim.TabularFun" "grisette-0.11.0.0-En6Ko5xIwnQLAUQ39GJ2kN" '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) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun type Rep (a =-> b) = D1 ('MetaData "=->" "Grisette.Internal.SymPrim.TabularFun" "grisette-0.11.0.0-En6Ko5xIwnQLAUQ39GJ2kN" '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 FunType (a =-> t) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun type FunType (a =-> t) = a -> FunType t
type PrimConstraint (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun type PrimConstraint (a =-> b) = (SupportedNonFuncPrim a, SupportedPrim b, NonFuncPrimConstraint a, PrimConstraint b)
type SBVType (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun type SBVType (a =-> b) = SBV (NonFuncSBVBaseType a) -> SBVType b
type SymType (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymTabularFun type SymType (a =-> b) = SymType a =~> SymType b