grisette-0.11.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2024
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellNone
LanguageHaskell2010

Grisette.Internal.SymPrim.TabularFun

Description

 
Synopsis

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

Instances

Instances details
Generic1 ((=->) a :: Type -> Type) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.TabularFun

Associated Types

type Rep1 ((=->) a :: Type -> Type) 
Instance details

Defined in Grisette.Internal.SymPrim.TabularFun

type Rep1 ((=->) a :: Type -> Type) = D1 ('MetaData "=->" "Grisette.Internal.SymPrim.TabularFun" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) (C1 ('MetaCons "TabularFun" 'PrefixI 'True) (S1 ('MetaSel ('Just "funcTable") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) ([] :.: Rec1 ((,) a)) :*: S1 ('MetaSel ('Just "defaultFuncValue") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1))

Methods

from1 :: (a =-> a0) -> Rep1 ((=->) a) a0 #

to1 :: 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 #

(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) -> () #

Generic (a =-> b) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.TabularFun

Associated Types

type Rep (a =-> b) 
Instance details

Defined in Grisette.Internal.SymPrim.TabularFun

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

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 #

(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) 
Instance details

Defined in Grisette.Internal.SymPrim.TabularFun

type FunType (a =-> t) = a -> FunType t

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 #

sortIndices :: (a =-> b) -> [DynamicSortedIdx] 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) 
Instance details

Defined in Grisette.Internal.SymPrim.TabularFun

type SBVType (a =-> b) = SBV (NonFuncSBVBaseType a) -> SBVType 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))))))) 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, SupportedNonFuncPrim a1, SupportedNonFuncPrim a2, SupportedNonFuncPrim a3, SupportedNonFuncPrim a4, SupportedNonFuncPrim a5, SupportedNonFuncPrim 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, SupportedNonFuncPrim a1, SupportedNonFuncPrim a2, SupportedNonFuncPrim a3, SupportedNonFuncPrim a4, SupportedNonFuncPrim 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, SupportedNonFuncPrim a1, SupportedNonFuncPrim a2, SupportedNonFuncPrim a3, SupportedNonFuncPrim 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, SupportedNonFuncPrim a1, SupportedNonFuncPrim a2, SupportedNonFuncPrim 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, SupportedNonFuncPrim a1, SupportedNonFuncPrim 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, SupportedNonFuncPrim 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) 
Instance details

Defined in Grisette.Internal.SymPrim.TabularFun

type PrimConstraint (a =-> b) = (SupportedNonFuncPrim a, SupportedPrim b, NonFuncPrimConstraint a, PrimConstraint b)
(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) 
Instance details

Defined in Grisette.Internal.SymPrim.SymTabularFun

type SymType (a =-> b) = SymType a =~> SymType b
(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-HndeEPlDvvDHSETLw6O8c" 'False) (C1 ('MetaCons "TabularFun" 'PrefixI 'True) (S1 ('MetaSel ('Just "funcTable") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) ([] :.: 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-HndeEPlDvvDHSETLw6O8c" '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