grisette-0.11.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 HaskellNone
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 :: forall a b. (SupportedNonFuncPrim 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), 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 #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Methods

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

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

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

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

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

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 #

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

Defined in Grisette.Internal.SymPrim.GeneralFun

Methods

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

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

(Apply st, LinkedRep ca sa, LinkedRep ct st) => Apply (ca --> ct) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.GeneralFun

Associated Types

type FunType (ca --> ct) 
Instance details

Defined in Grisette.Internal.SymPrim.GeneralFun

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

Methods

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

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

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

Methods

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

EvalSym (SymType 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 (SymType 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 #

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 #

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

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

Methods

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

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

Associated Types

type SBVType (a --> b) 
Instance details

Defined in Grisette.Internal.SymPrim.GeneralFun

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

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

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

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

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

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

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

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

Associated Types

type PrimConstraint (a --> b) 
Instance details

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

Defined in Grisette.Internal.SymPrim.SymGeneralFun

type SymType (ca --> cb) = SymType ca -~> SymType cb
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 #

(SupportedNonFuncPrim ca, 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 #

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 #

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

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 cb, SupportedPrim (ca --> cb), SupportedNonFuncPrim ca) => 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 FunType (ca --> ct) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.GeneralFun

type FunType (ca --> ct) = SymType ca -> FunType (SymType ct)
type PrimConstraint (a --> b) Source # 
Instance details

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) 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 a. TypedSymbol 'AnyKind a -> Term a) -> HashSet SomeTypedConstantSymbol -> Term v -> Term v Source #

General procedure for substituting symbols in a term.

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

Substitute a term for a symbol in a term.

freshArgSymbol :: SupportedNonFuncPrim a => [SomeTerm] -> TypedConstantSymbol a Source #

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