Grisette.Internal.SymPrim.GeneralFun

Documentation

data a --> b where infixr 0

General symbolic function type. Use the # operator to apply the function. Note that this function should be applied to symbolic values only. It is by itself already a symbolic value, but can be considered partially concrete as the function body is specified. Use -~> for uninterpreted general symbolic functions.

The result would be partially evaluated.

>>> let f = ("x" :: TypedConstantSymbol Integer) --> ("x" + 1 + "y" :: SymInteger) :: Integer --> Integer
>>> f # 1    -- 1 has the type SymInteger
(+ 2 y)
>>> f # "a"  -- "a" has the type SymInteger
(+ 1 (+ a y))

Constructors

GeneralFun :: (SupportedNonFuncPrim a, SupportedPrim b) => TypedConstantSymbol a -> Term b -> a --> b

Instances

Lift (a --> b :: Type)

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

lift :: Quote m => (a --> b) -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => (a --> b) -> Code m (a --> b)

(SupportedPrim (ca --> cb), SupportedNonFuncPrim ca, 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

Show (a --> b)

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

showsPrec :: Int -> (a --> b) -> ShowS

show :: (a --> b) -> String

showList :: [a --> b] -> ShowS

(GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e, GeneralFunArg f, GeneralFunArg g, GeneralFunArg h, GeneralFunArg i) => Binary (a --> (b --> (c --> (d --> (e --> (f --> (g --> (h --> i))))))))

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

put :: (a --> (b --> (c --> (d --> (e --> (f --> (g --> (h --> i)))))))) -> Put

get :: Get (a --> (b --> (c --> (d --> (e --> (f --> (g --> (h --> i))))))))

putList :: [a --> (b --> (c --> (d --> (e --> (f --> (g --> (h --> i)))))))] -> Put

(GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e, GeneralFunArg f, GeneralFunArg g, GeneralFunArg h) => Binary (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

put :: (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> Put

get :: Get (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))

putList :: [a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))] -> Put

(GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e, GeneralFunArg f, GeneralFunArg g) => Binary (a --> (b --> (c --> (d --> (e --> (f --> g))))))

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

put :: (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> Put

get :: Get (a --> (b --> (c --> (d --> (e --> (f --> g))))))

putList :: [a --> (b --> (c --> (d --> (e --> (f --> g)))))] -> Put

(GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e, GeneralFunArg f) => Binary (a --> (b --> (c --> (d --> (e --> f)))))

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

put :: (a --> (b --> (c --> (d --> (e --> f))))) -> Put

get :: Get (a --> (b --> (c --> (d --> (e --> f)))))

putList :: [a --> (b --> (c --> (d --> (e --> f))))] -> Put

(GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e) => Binary (a --> (b --> (c --> (d --> e))))

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

put :: (a --> (b --> (c --> (d --> e)))) -> Put

get :: Get (a --> (b --> (c --> (d --> e))))

putList :: [a --> (b --> (c --> (d --> e)))] -> Put

(GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d) => Binary (a --> (b --> (c --> d)))

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

put :: (a --> (b --> (c --> d))) -> Put

get :: Get (a --> (b --> (c --> d)))

putList :: [a --> (b --> (c --> d))] -> Put

(GeneralFunArg a, GeneralFunArg b, GeneralFunArg c) => Binary (a --> (b --> c))

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

put :: (a --> (b --> c)) -> Put

get :: Get (a --> (b --> c))

putList :: [a --> (b --> c)] -> Put

(GeneralFunArg a, GeneralFunArg b) => Binary (a --> b)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

put :: (a --> b) -> Put

get :: Get (a --> b)

putList :: [a --> b] -> Put

(GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e, GeneralFunArg f, GeneralFunArg g, GeneralFunArg h, GeneralFunArg i) => Serial (a --> (b --> (c --> (d --> (e --> (f --> (g --> (h --> i))))))))

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

serialize :: MonadPut m => (a --> (b --> (c --> (d --> (e --> (f --> (g --> (h --> i)))))))) -> m ()

deserialize :: MonadGet m => m (a --> (b --> (c --> (d --> (e --> (f --> (g --> (h --> i))))))))

(GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e, GeneralFunArg f, GeneralFunArg g, GeneralFunArg h) => Serial (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

serialize :: MonadPut m => (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> m ()

deserialize :: MonadGet m => m (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))

(GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e, GeneralFunArg f, GeneralFunArg g) => Serial (a --> (b --> (c --> (d --> (e --> (f --> g))))))

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

serialize :: MonadPut m => (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> m ()

deserialize :: MonadGet m => m (a --> (b --> (c --> (d --> (e --> (f --> g))))))

(GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e, GeneralFunArg f) => Serial (a --> (b --> (c --> (d --> (e --> f)))))

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

serialize :: MonadPut m => (a --> (b --> (c --> (d --> (e --> f))))) -> m ()

deserialize :: MonadGet m => m (a --> (b --> (c --> (d --> (e --> f)))))

(GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e) => Serial (a --> (b --> (c --> (d --> e))))

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

serialize :: MonadPut m => (a --> (b --> (c --> (d --> e)))) -> m ()

deserialize :: MonadGet m => m (a --> (b --> (c --> (d --> e))))

(GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d) => Serial (a --> (b --> (c --> d)))

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

serialize :: MonadPut m => (a --> (b --> (c --> d))) -> m ()

deserialize :: MonadGet m => m (a --> (b --> (c --> d)))

(GeneralFunArg a, GeneralFunArg b, GeneralFunArg c) => Serial (a --> (b --> c))

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

serialize :: MonadPut m => (a --> (b --> c)) -> m ()

deserialize :: MonadGet m => m (a --> (b --> c))

(GeneralFunArg a, GeneralFunArg b) => Serial (a --> b)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

serialize :: MonadPut m => (a --> b) -> m ()

deserialize :: MonadGet m => m (a --> b)

(GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e, GeneralFunArg f, GeneralFunArg g, GeneralFunArg h, GeneralFunArg i) => Serialize (a --> (b --> (c --> (d --> (e --> (f --> (g --> (h --> i))))))))

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

put :: Putter (a --> (b --> (c --> (d --> (e --> (f --> (g --> (h --> i))))))))

get :: Get (a --> (b --> (c --> (d --> (e --> (f --> (g --> (h --> i))))))))

(GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e, GeneralFunArg f, GeneralFunArg g, GeneralFunArg h) => Serialize (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

put :: Putter (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))

get :: Get (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))

(GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e, GeneralFunArg f, GeneralFunArg g) => Serialize (a --> (b --> (c --> (d --> (e --> (f --> g))))))

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

put :: Putter (a --> (b --> (c --> (d --> (e --> (f --> g))))))

get :: Get (a --> (b --> (c --> (d --> (e --> (f --> g))))))

(GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e, GeneralFunArg f) => Serialize (a --> (b --> (c --> (d --> (e --> f)))))

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

put :: Putter (a --> (b --> (c --> (d --> (e --> f)))))

get :: Get (a --> (b --> (c --> (d --> (e --> f)))))

(GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e) => Serialize (a --> (b --> (c --> (d --> e))))

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

put :: Putter (a --> (b --> (c --> (d --> e))))

get :: Get (a --> (b --> (c --> (d --> e))))

(GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d) => Serialize (a --> (b --> (c --> d)))

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

put :: Putter (a --> (b --> (c --> d)))

get :: Get (a --> (b --> (c --> d)))

(GeneralFunArg a, GeneralFunArg b, GeneralFunArg c) => Serialize (a --> (b --> c))

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

put :: Putter (a --> (b --> c))

get :: Get (a --> (b --> c))

(GeneralFunArg a, GeneralFunArg b) => Serialize (a --> b)

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

put :: Putter (a --> b)

get :: Get (a --> b)

NFData (a --> b)

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

rnf :: (a --> b) -> ()

Eq (a --> b)

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

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

(/=) :: (a --> b) -> (a --> b) -> Bool

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

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

Methods

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

ExtractSym (SymType 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)

(Apply st, LinkedRep ca sa, LinkedRep ct st) => Apply (ca --> ct)

Defined in Grisette.Internal.SymPrim.GeneralFun

Associated Types

type FunType (ca --> ct)

Methods

apply :: (ca --> ct) -> FunType (ca --> ct)

ITEOp (a --> b)

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

Methods

symIte :: SymBool -> (a --> b) -> (a --> b) -> a --> b

Mergeable (a --> b)

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

Methods

rootStrategy :: MergingStrategy (a --> b)

PPrint (a --> b)

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

Methods

pformat :: (a --> b) -> Doc ann

pformatPrec :: Int -> (a --> b) -> Doc ann

pformatList :: [a --> b] -> Doc ann

SimpleMergeable (a --> b)

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

Methods

mrgIte :: SymBool -> (a --> b) -> (a --> b) -> a --> b

SubstSym (SymType b) => SubstSym (a --> b)

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

Methods

substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> (a --> b) -> a --> b

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

Defined in Grisette.Internal.SymPrim.GeneralFun

Associated Types

type SBVType (a --> b)

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

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

primTypeRep :: TypeRep (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7)))))))

sameCon :: (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))) -> (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))) -> Bool

hashConWithSalt :: Int -> (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))) -> Int

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

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

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

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

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

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

primTypeRep :: TypeRep (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6))))))

sameCon :: (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))) -> (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))) -> Bool

hashConWithSalt :: Int -> (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))) -> Int

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

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

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

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

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

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

primTypeRep :: TypeRep (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5)))))

sameCon :: (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))) -> (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))) -> Bool

hashConWithSalt :: Int -> (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))) -> Int

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

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

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

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

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

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

primTypeRep :: TypeRep (a0 --> (a1 --> (a2 --> (a3 --> a4))))

sameCon :: (a0 --> (a1 --> (a2 --> (a3 --> a4)))) -> (a0 --> (a1 --> (a2 --> (a3 --> a4)))) -> Bool

hashConWithSalt :: Int -> (a0 --> (a1 --> (a2 --> (a3 --> a4)))) -> Int

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

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

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

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

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

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

primTypeRep :: TypeRep (a0 --> (a1 --> (a2 --> a3)))

sameCon :: (a0 --> (a1 --> (a2 --> a3))) -> (a0 --> (a1 --> (a2 --> a3))) -> Bool

hashConWithSalt :: Int -> (a0 --> (a1 --> (a2 --> a3))) -> Int

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

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

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

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

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

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

primTypeRep :: TypeRep (a0 --> (a1 --> a2))

sameCon :: (a0 --> (a1 --> a2)) -> (a0 --> (a1 --> a2)) -> Bool

hashConWithSalt :: Int -> (a0 --> (a1 --> a2)) -> Int

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

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

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

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

(SupportedNonFuncPrim a0, Eq a0, Show a0, Hashable a0, Typeable a0, SupportedNonFuncPrim a1, Eq a1, Show a1, Hashable a1, Typeable a1) => SupportedPrim (a0 --> a1)

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

primTypeRep :: TypeRep (a0 --> a1)

sameCon :: (a0 --> a1) -> (a0 --> a1) -> Bool

hashConWithSalt :: Int -> (a0 --> a1) -> Int

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

defaultValue :: a0 --> a1

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

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

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

Defined in Grisette.Internal.SymPrim.GeneralFun

Associated Types

type PrimConstraint (a --> b)

(SymRep ca, SymRep cb, SupportedPrim (ca --> cb)) => SymRep (ca --> cb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Associated Types

type SymType (ca --> cb)

Hashable (a --> b)

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

hashWithSalt :: Int -> (a --> b) -> Int

hash :: (a --> b) -> Int

(LinkedRep a sa, LinkedRep b sb) => Function (a --> b) sa sb

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

(#) :: (a --> b) -> sa -> sb

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

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

pevalApplyTerm :: Term (a --> b) -> Term a -> Term b

sbvApplyTerm :: SBVType (a --> b) -> SBVType a -> SBVType b

(SupportedNonFuncPrim ca, LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca --> cb)) => Solvable (ca --> cb) (sa -~> sb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

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

ToCon (a --> b) (a --> b)

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

Methods

toCon :: (a --> b) -> Maybe (a --> b)

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

ToSym (a --> b) (a --> b)

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

Methods

toSym :: (a --> b) -> a --> b

(SupportedPrim (ca --> cb), SupportedNonFuncPrim ca, 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 cb, SupportedPrim (ca --> cb), SupportedNonFuncPrim ca) => LinkedRep (ca --> cb) (sa -~> sb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

underlyingTerm :: (sa -~> sb) -> Term (ca --> cb)

wrapTerm :: Term (ca --> cb) -> sa -~> sb

type FunType (ca --> ct)

Defined in Grisette.Internal.SymPrim.GeneralFun

type FunType (ca --> ct) = SymType ca -> FunType (SymType ct)

type PrimConstraint (a --> b)

Defined in Grisette.Internal.SymPrim.GeneralFun

type PrimConstraint (a --> b) = (SupportedNonFuncPrim a, SupportedPrim b, NonFuncPrimConstraint a, PrimConstraint b, SBVType (a --> b) ~ (SBV (NonFuncSBVBaseType a) -> SBVType b))

type SBVType (a --> b)

Defined in Grisette.Internal.SymPrim.GeneralFun

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

type SymType (ca --> cb)

Defined in Grisette.Internal.SymPrim.SymGeneralFun

type SymType (ca --> cb) = SymType ca -~> SymType cb

buildGeneralFun :: forall a b. (SupportedNonFuncPrim a, SupportedPrim b) => TypedConstantSymbol a -> Term b -> a --> b

Build a general symbolic function with a bounded symbol and a term.

generalSubstSomeTerm :: forall v. (forall a. TypedSymbol 'AnyKind a -> Term a) -> HashSet SomeTypedConstantSymbol -> Term v -> Term v

General procedure for substituting symbols in a term.

substTerm :: forall knd a b. (SupportedPrim a, SupportedPrim b, IsSymbolKind knd) => TypedSymbol knd a -> Term a -> HashSet SomeTypedConstantSymbol -> Term b -> Term b

Substitute a term for a symbol in a term.

freshArgSymbol :: forall a. SupportedNonFuncPrim a => [SomeTerm] -> TypedConstantSymbol a

Generate a fresh argument symbol that is not used as bounded or unbounded variables in the function body for a general symbolic function.