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

Grisette.Internal.SymPrim.GeneralFun

Description

 
Synopsis

Documentation

data a --> b where infixr 0 Source #

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 :: (SupportedPrim a, SupportedPrim b) => TypedConstantSymbol a -> Term b -> a --> b 

Instances

Instances details
Lift (a --> b :: Type) Source # 
Instance details

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), LinkedRep ca sa, LinkedRep cb sb) => ToSym (Union (ca --> cb)) (sa -~> sb) Source # 
Instance details

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

Methods

toSym :: Union (ca --> cb) -> sa -~> sb Source #

Show (a --> b) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

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

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

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

NFData (a --> b) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

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

Eq (a --> b) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

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

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

EvalSym (SymType b) => EvalSym (a --> b) Source # 
Instance details

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

Methods

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

ExtractSym (SymType b) => ExtractSym (a --> b) Source # 
Instance details

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

Methods

extractSym :: (a --> b) -> AnySymbolSet Source #

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

(SupportedNonFuncPrim a, SupportedPrim b) => SBVRep (a --> b) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.GeneralFun

Associated Types

type SBVType (a --> b) Source #

(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.GeneralFun

Methods

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

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

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

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

defaultValueDynamic :: proxy (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))) -> ModelValue 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 #

isFuncType :: Bool 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.GeneralFun

Methods

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

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

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

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

defaultValueDynamic :: proxy (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))) -> ModelValue 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 #

isFuncType :: Bool 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.GeneralFun

Methods

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

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

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

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

defaultValueDynamic :: proxy (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))) -> ModelValue 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 #

isFuncType :: Bool 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.GeneralFun

Methods

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

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

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

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

defaultValueDynamic :: proxy (a0 --> (a1 --> (a2 --> (a3 --> a4)))) -> ModelValue 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 #

isFuncType :: Bool 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.GeneralFun

Methods

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

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

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

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

defaultValueDynamic :: proxy (a0 --> (a1 --> (a2 --> a3))) -> ModelValue 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 #

isFuncType :: Bool 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.GeneralFun

Methods

termCache :: Cache (Term (a0 --> (a1 --> a2))) Source #

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

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

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

defaultValueDynamic :: proxy (a0 --> (a1 --> a2)) -> ModelValue 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 #

isFuncType :: Bool Source #

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

(SupportedNonFuncPrim a0, SupportedNonFuncPrim a1) => SupportedPrim (a0 --> a1) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

termCache :: Cache (Term (a0 --> a1)) Source #

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

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

defaultValue :: a0 --> a1 Source #

defaultValueDynamic :: proxy (a0 --> a1) -> ModelValue 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 #

isFuncType :: Bool Source #

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

(SupportedNonFuncPrim a, SupportedPrim b) => SupportedPrimConstraint (a --> b) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.GeneralFun

Associated Types

type PrimConstraint (a --> b) Source #

(SymRep ca, SymRep cb, SupportedPrim (ca --> cb)) => SymRep (ca --> cb) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Associated Types

type SymType (ca --> cb) Source #

Hashable (a --> b) Source # 
Instance details

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 Source # 
Instance details

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

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

(SupportedPrim (a --> b), SupportedNonFuncPrim a, SupportedPrim b) => PEvalApplyTerm (a --> b) a b Source # 
Instance details

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

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

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

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca --> cb)) => Solvable (ca --> cb) (sa -~> sb) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymGeneralFun

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 #

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => ToCon (sa -~> sb) (ca --> cb) Source # 
Instance details

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

Methods

toCon :: (sa -~> sb) -> Maybe (ca --> cb) Source #

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => ToSym (ca --> cb) (sa -~> sb) Source # 
Instance details

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

Methods

toSym :: (ca --> cb) -> sa -~> sb Source #

(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim ca, SupportedPrim cb, SupportedPrim (ca --> cb)) => LinkedRep (ca --> cb) (sa -~> sb) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Methods

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

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

type PrimConstraint (a --> b) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.GeneralFun

type SBVType (a --> b) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.GeneralFun

type SBVType (a --> b) = SBV (NonFuncSBVBaseType a) -> SBVType b
type SymType (ca --> cb) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymGeneralFun

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

buildGeneralFun :: (SupportedNonFuncPrim a, SupportedPrim b) => TypedConstantSymbol a -> Term b -> a --> b Source #

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 Source #

General procedure for substituting symbols in a term.

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

Substitute a term for a symbol in a term.