Copyright	(c) Sirui Lu 2024
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	None
Language	Haskell2010

Grisette.Internal.SymPrim.GeneralFun

Description

Synopsis

data a --> b where
- GeneralFun :: forall a b. (SupportedNonFuncPrim a, SupportedPrim b) => TypedConstantSymbol a -> Term b -> a --> b
buildGeneralFun :: (SupportedNonFuncPrim a, SupportedPrim b) => TypedConstantSymbol a -> Term b -> a --> b
generalSubstSomeTerm :: (forall a. TypedSymbol 'AnyKind a -> Term a) -> HashSet SomeTypedConstantSymbol -> Term v -> Term v
substTerm :: forall (knd :: SymbolKind) a b. (SupportedPrim a, SupportedPrim b, IsSymbolKind knd) => TypedSymbol knd a -> Term a -> HashSet SomeTypedConstantSymbol -> Term b -> Term b
freshArgSymbol :: SupportedNonFuncPrim a => [SomeTerm] -> TypedConstantSymbol a

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 #

Checks if two formulas are the same. Not building the actual symbolic equality formula.

The reason why we choose this behavior is to allow symbolic variables to be used as keys in hash maps, which can be useful for memoization.

Use with caution. Usually you should use SymEq instead.

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 #