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

Grisette.Internal.Core.Data.Class.EvalSym

Contents

Evaluating symbolic values with model
Generic EvalSym

Description

Synopsis

class EvalSym a where
- evalSym :: Bool -> Model -> a -> a
evalSymToCon :: (ToCon a b, EvalSym a) => Model -> a -> b
class (forall a. EvalSym a => EvalSym (f a)) => EvalSym1 (f :: Type -> Type) where
- liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> f a -> f a
evalSym1 :: (EvalSym1 f, EvalSym a) => Bool -> Model -> f a -> f a
evalSymToCon1 :: (EvalSym1 f, EvalSym a, ToCon1 f g, ToCon a b) => Model -> f a -> g b
class (forall a. EvalSym a => EvalSym1 (f a)) => EvalSym2 (f :: Type -> Type -> Type) where
- liftEvalSym2 :: (Bool -> Model -> a -> a) -> (Bool -> Model -> b -> b) -> Bool -> Model -> f a b -> f a b
evalSym2 :: (EvalSym2 f, EvalSym a, EvalSym b) => Bool -> Model -> f a b -> f a b
evalSymToCon2 :: (EvalSym2 f, EvalSym a, EvalSym c, ToCon2 f g, ToCon a b, ToCon c d) => Model -> f a c -> g b d
data family EvalSymArgs arity a
class GEvalSym arity (f :: Type -> Type) where
- gevalSym :: EvalSymArgs arity a -> Bool -> Model -> f a -> f a
genericEvalSym :: (Generic a, GEvalSym Arity0 (Rep a)) => Bool -> Model -> a -> a
genericLiftEvalSym :: (Generic1 f, GEvalSym Arity1 (Rep1 f)) => (Bool -> Model -> a -> a) -> Bool -> Model -> f a -> f a

Evaluating symbolic values with model

class EvalSym a where Source #

Evaluating symbolic values with some model. This would substitute the symbols (symbolic constants) with the values in the model.

>>> let model = insertValue "a" (1 :: Integer) emptyModel :: Model
>>> evalSym False model ([ssym "a", ssym "b"] :: [SymInteger])
[1,b]

If we set the first argument true, the missing symbols will be filled in with some default values:

>>> evalSym True model ([ssym "a", ssym "b"] :: [SymInteger])
[1,0]

Note 1: This type class can be derived for algebraic data types. You may need the DerivingVia and DerivingStrategies extensions.

data X = ... deriving Generic deriving EvalSym via (Default X)

Methods

evalSym :: Bool -> Model -> a -> a Source #

Evaluate a symbolic value with some model, possibly fill in values for the missing symbols.

Instances

Instances details

EvalSym ByteString Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> ByteString -> ByteString Source #
EvalSym All Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> All -> All Source #
EvalSym Any Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Any -> Any Source #
EvalSym Int16 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Int16 -> Int16 Source #
EvalSym Int32 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Int32 -> Int32 Source #
EvalSym Int64 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Int64 -> Int64 Source #
EvalSym Int8 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Int8 -> Int8 Source #
EvalSym Word16 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Word16 -> Word16 Source #
EvalSym Word32 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Word32 -> Word32 Source #
EvalSym Word64 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Word64 -> Word64 Source #
EvalSym Word8 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Word8 -> Word8 Source #
EvalSym Ordering Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Ordering -> Ordering Source #
EvalSym AssertionError Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> AssertionError -> AssertionError Source #
EvalSym VerificationConditions Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> VerificationConditions -> VerificationConditions Source #
EvalSym CEGISCondition Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.CEGISSolver Methods evalSym :: Bool -> Model -> CEGISCondition -> CEGISCondition Source #
EvalSym AlgReal Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> AlgReal -> AlgReal Source #
EvalSym FPRoundingMode Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> FPRoundingMode -> FPRoundingMode Source #
EvalSym NotRepresentableFPError Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> NotRepresentableFPError -> NotRepresentableFPError Source #
EvalSym SomeBVException Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods evalSym :: Bool -> Model -> SomeBVException -> SomeBVException Source #
EvalSym SymAlgReal Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> SymAlgReal -> SymAlgReal Source #
EvalSym SymBool Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> SymBool -> SymBool Source #
EvalSym SymFPRoundingMode Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> SymFPRoundingMode -> SymFPRoundingMode Source #
EvalSym SymInteger Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> SymInteger -> SymInteger Source #
EvalSym Text Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Text -> Text Source #
EvalSym Integer Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Integer -> Integer Source #
EvalSym () Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> () -> () Source #
EvalSym Bool Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Bool -> Bool Source #
EvalSym Char Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Char -> Char Source #
EvalSym Double Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Double -> Double Source #
EvalSym Float Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Float -> Float Source #
EvalSym Int Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Int -> Int Source #
EvalSym Word Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Word -> Word Source #
(Generic a, GEvalSym Arity0 (Rep a)) => EvalSym (Default a) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Default a -> Default a Source #
EvalSym a => EvalSym (Identity a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Identity a -> Identity a Source #
EvalSym a => EvalSym (First a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> First a -> First a Source #
EvalSym a => EvalSym (Last a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Last a -> Last a Source #
EvalSym a => EvalSym (Down a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Down a -> Down a Source #
EvalSym a => EvalSym (Dual a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Dual a -> Dual a Source #
EvalSym a => EvalSym (Product a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Product a -> Product a Source #
EvalSym a => EvalSym (Sum a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Sum a -> Sum a Source #
EvalSym p => EvalSym (Par1 p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Par1 p -> Par1 p Source #
(Integral a, EvalSym a) => EvalSym (Ratio a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Ratio a -> Ratio a Source #
EvalSym a => EvalSym (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods evalSym :: Bool -> Model -> Union a -> Union a Source #
(KnownNat n, 1 <= n) => EvalSym (IntN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> IntN n -> IntN n Source #
(KnownNat n, 1 <= n) => EvalSym (WordN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> WordN n -> WordN n Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => EvalSym (bv n)) => EvalSym (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods evalSym :: Bool -> Model -> SomeBV bv -> SomeBV bv Source #
(KnownNat n, 1 <= n) => EvalSym (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> SymIntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => EvalSym (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> SymWordN n -> SymWordN n Source #
EvalSym a => EvalSym (Maybe a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Maybe a -> Maybe a Source #
EvalSym a => EvalSym [a] Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> [a] -> [a] Source #
(Generic1 f, GEvalSym Arity1 (Rep1 f), EvalSym a) => EvalSym (Default1 f a) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Default1 f a -> Default1 f a Source #
(EvalSym a1, EvalSym a2) => EvalSym (Either a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Either a1 a2 -> Either a1 a2 Source #
EvalSym (Proxy a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Proxy a -> Proxy a Source #
EvalSym (U1 p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> U1 p -> U1 p Source #
EvalSym (V1 p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> V1 p -> V1 p Source #
(EvalSym a, EvalSym b) => EvalSym (CBMCEither a b) Source #
Instance details Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept Methods evalSym :: Bool -> Model -> CBMCEither a b -> CBMCEither a b Source #
ValidFP eb fb => EvalSym (FP eb fb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> FP eb fb -> FP eb fb 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 #
ValidFP eb sb => EvalSym (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> SymFP eb sb -> SymFP eb sb Source #
EvalSym (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> (sa -~> sb) -> sa -~> sb Source #
EvalSym (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> (sa =~> sb) -> sa =~> sb Source #
(EvalSym a, EvalSym b) => EvalSym (a =-> b) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> (a =-> b) -> a =-> b Source #
(EvalSym1 a1, EvalSym a2) => EvalSym (MaybeT a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> MaybeT a1 a2 -> MaybeT a1 a2 Source #
(EvalSym a1, EvalSym a2) => EvalSym (a1, a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> (a1, a2) -> (a1, a2) Source #
EvalSym a => EvalSym (Const a b) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Const a b -> Const a b Source #
EvalSym (f a) => EvalSym (Ap f a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Ap f a -> Ap f a Source #
EvalSym (f a) => EvalSym (Alt f a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Alt f a -> Alt f a Source #
EvalSym (f p) => EvalSym (Rec1 f p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Rec1 f p -> Rec1 f p Source #
EvalSym (m (CBMCEither e a)) => EvalSym (CBMCExceptT e m a) Source #
Instance details Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept Methods evalSym :: Bool -> Model -> CBMCExceptT e m a -> CBMCExceptT e m a Source #
(EvalSym a1, EvalSym1 a2, EvalSym a3) => EvalSym (ExceptT a1 a2 a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> ExceptT a1 a2 a3 -> ExceptT a1 a2 a3 Source #
(EvalSym1 m, EvalSym a) => EvalSym (IdentityT m a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> IdentityT m a -> IdentityT m a Source #
(EvalSym a1, EvalSym1 a2, EvalSym a3) => EvalSym (WriterT a1 a2 a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> WriterT a1 a2 a3 -> WriterT a1 a2 a3 Source #
(EvalSym a1, EvalSym1 a2, EvalSym a3) => EvalSym (WriterT a1 a2 a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> WriterT a1 a2 a3 -> WriterT a1 a2 a3 Source #
(EvalSym a1, EvalSym a2, EvalSym a3) => EvalSym (a1, a2, a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> (a1, a2, a3) -> (a1, a2, a3) Source #
(EvalSym (l a), EvalSym (r a)) => EvalSym (Product l r a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Product l r a -> Product l r a Source #
(EvalSym (l a), EvalSym (r a)) => EvalSym (Sum l r a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Sum l r a -> Sum l r a Source #
(EvalSym (f p), EvalSym (g p)) => EvalSym ((f :*: g) p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> (f :: g) p -> (f :: g) p Source #
(EvalSym (f p), EvalSym (g p)) => EvalSym ((f :+: g) p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> (f :+: g) p -> (f :+: g) p Source #
EvalSym c => EvalSym (K1 i c p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> K1 i c p -> K1 i c p Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4) => EvalSym (a1, a2, a3, a4) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> (a1, a2, a3, a4) -> (a1, a2, a3, a4) Source #
EvalSym (f (g a)) => EvalSym (Compose f g a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> Compose f g a -> Compose f g a Source #
EvalSym (f (g p)) => EvalSym ((f :.: g) p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> (f :.: g) p -> (f :.: g) p Source #
EvalSym (f p) => EvalSym (M1 i c f p) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> M1 i c f p -> M1 i c f p Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5) => EvalSym (a1, a2, a3, a4, a5) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> (a1, a2, a3, a4, a5) -> (a1, a2, a3, a4, a5) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6) => EvalSym (a1, a2, a3, a4, a5, a6) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> (a1, a2, a3, a4, a5, a6) -> (a1, a2, a3, a4, a5, a6) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6, EvalSym a7) => EvalSym (a1, a2, a3, a4, a5, a6, a7) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> (a1, a2, a3, a4, a5, a6, a7) -> (a1, a2, a3, a4, a5, a6, a7) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6, EvalSym a7, EvalSym a8) => EvalSym (a1, a2, a3, a4, a5, a6, a7, a8) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> (a1, a2, a3, a4, a5, a6, a7, a8) -> (a1, a2, a3, a4, a5, a6, a7, a8) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6, EvalSym a7, EvalSym a8, EvalSym a9) => EvalSym (a1, a2, a3, a4, a5, a6, a7, a8, a9) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6, EvalSym a7, EvalSym a8, EvalSym a9, EvalSym a10) => EvalSym (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6, EvalSym a7, EvalSym a8, EvalSym a9, EvalSym a10, EvalSym a11) => EvalSym (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6, EvalSym a7, EvalSym a8, EvalSym a9, EvalSym a10, EvalSym a11, EvalSym a12) => EvalSym (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6, EvalSym a7, EvalSym a8, EvalSym a9, EvalSym a10, EvalSym a11, EvalSym a12, EvalSym a13) => EvalSym (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6, EvalSym a7, EvalSym a8, EvalSym a9, EvalSym a10, EvalSym a11, EvalSym a12, EvalSym a13, EvalSym a14) => EvalSym (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6, EvalSym a7, EvalSym a8, EvalSym a9, EvalSym a10, EvalSym a11, EvalSym a12, EvalSym a13, EvalSym a14, EvalSym a15) => EvalSym (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods evalSym :: Bool -> Model -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) Source #

evalSymToCon :: (ToCon a b, EvalSym a) => Model -> a -> b Source #

Evaluate a symbolic value with some model, fill in values for the missing symbols, and convert the result to a concrete value.

>>> let model = insertValue "a" (1 :: Integer) emptyModel :: Model
>>> evalSymToCon model ([ssym "a", ssym "b"] :: [SymInteger]) :: [Integer]
[1,0]

class (forall a. EvalSym a => EvalSym (f a)) => EvalSym1 (f :: Type -> Type) where Source #

Lifting of EvalSym to unary type constructors.

Methods

liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> f a -> f a Source #

Lift the evalSym function to unary type constructors.

Instances

Instances details

EvalSym1 Identity Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Identity a -> Identity a Source #
EvalSym1 First Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> First a -> First a Source #
EvalSym1 Last Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Last a -> Last a Source #
EvalSym1 Down Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Down a -> Down a Source #
EvalSym1 Dual Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Dual a -> Dual a Source #
EvalSym1 Product Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Product a -> Product a Source #
EvalSym1 Sum Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Sum a -> Sum a Source #
EvalSym1 Union Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Union a -> Union a Source #
EvalSym1 Maybe Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Maybe a -> Maybe a Source #
EvalSym1 [] Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> [a] -> [a] Source #
(Generic1 f, GEvalSym Arity1 (Rep1 f)) => EvalSym1 (Default1 f) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Default1 f a -> Default1 f a Source #
EvalSym a => EvalSym1 (Either a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a0 -> a0) -> Bool -> Model -> Either a a0 -> Either a a0 Source #
EvalSym1 (Proxy :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Proxy a -> Proxy a Source #
EvalSym1 a => EvalSym1 (MaybeT a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a0 -> a0) -> Bool -> Model -> MaybeT a a0 -> MaybeT a a0 Source #
EvalSym a => EvalSym1 ((,) a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a0 -> a0) -> Bool -> Model -> (a, a0) -> (a, a0) Source #
EvalSym a => EvalSym1 (Const a :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a0 -> a0) -> Bool -> Model -> Const a a0 -> Const a a0 Source #
EvalSym1 f => EvalSym1 (Ap f) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Ap f a -> Ap f a Source #
EvalSym1 f => EvalSym1 (Alt f) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Alt f a -> Alt f a Source #
(EvalSym a1, EvalSym1 a2) => EvalSym1 (ExceptT a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> ExceptT a1 a2 a -> ExceptT a1 a2 a Source #
EvalSym1 m => EvalSym1 (IdentityT m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> IdentityT m a -> IdentityT m a Source #
(EvalSym a1, EvalSym1 a2) => EvalSym1 (WriterT a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> WriterT a1 a2 a -> WriterT a1 a2 a Source #
(EvalSym a1, EvalSym1 a2) => EvalSym1 (WriterT a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> WriterT a1 a2 a -> WriterT a1 a2 a Source #
(EvalSym a1, EvalSym a2) => EvalSym1 ((,,) a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> (a1, a2, a) -> (a1, a2, a) Source #
(EvalSym1 l, EvalSym1 r) => EvalSym1 (Product l r) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Product l r a -> Product l r a Source #
(EvalSym1 l, EvalSym1 r) => EvalSym1 (Sum l r) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Sum l r a -> Sum l r a Source #
(EvalSym a1, EvalSym a2, EvalSym a3) => EvalSym1 ((,,,) a1 a2 a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> (a1, a2, a3, a) -> (a1, a2, a3, a) Source #
(EvalSym1 f, EvalSym1 g) => EvalSym1 (Compose f g) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Compose f g a -> Compose f g a Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4) => EvalSym1 ((,,,,) a1 a2 a3 a4) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> (a1, a2, a3, a4, a) -> (a1, a2, a3, a4, a) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5) => EvalSym1 ((,,,,,) a1 a2 a3 a4 a5) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> (a1, a2, a3, a4, a5, a) -> (a1, a2, a3, a4, a5, a) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6) => EvalSym1 ((,,,,,,) a1 a2 a3 a4 a5 a6) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> (a1, a2, a3, a4, a5, a6, a) -> (a1, a2, a3, a4, a5, a6, a) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6, EvalSym a7) => EvalSym1 ((,,,,,,,) a1 a2 a3 a4 a5 a6 a7) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> (a1, a2, a3, a4, a5, a6, a7, a) -> (a1, a2, a3, a4, a5, a6, a7, a) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6, EvalSym a7, EvalSym a8) => EvalSym1 ((,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> (a1, a2, a3, a4, a5, a6, a7, a8, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6, EvalSym a7, EvalSym a8, EvalSym a9) => EvalSym1 ((,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6, EvalSym a7, EvalSym a8, EvalSym a9, EvalSym a10) => EvalSym1 ((,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6, EvalSym a7, EvalSym a8, EvalSym a9, EvalSym a10, EvalSym a11) => EvalSym1 ((,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6, EvalSym a7, EvalSym a8, EvalSym a9, EvalSym a10, EvalSym a11, EvalSym a12) => EvalSym1 ((,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6, EvalSym a7, EvalSym a8, EvalSym a9, EvalSym a10, EvalSym a11, EvalSym a12, EvalSym a13) => EvalSym1 ((,,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6, EvalSym a7, EvalSym a8, EvalSym a9, EvalSym a10, EvalSym a11, EvalSym a12, EvalSym a13, EvalSym a14) => EvalSym1 ((,,,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a) Source #

evalSym1 :: (EvalSym1 f, EvalSym a) => Bool -> Model -> f a -> f a Source #

Lifting the standard evalSym to unary type constructors.

evalSymToCon1 :: (EvalSym1 f, EvalSym a, ToCon1 f g, ToCon a b) => Model -> f a -> g b Source #

Evaluate and convert to concrete values with lifted standard evalSym for unary type constructors. See evalSymToCon.

class (forall a. EvalSym a => EvalSym1 (f a)) => EvalSym2 (f :: Type -> Type -> Type) where Source #

Lifting of EvalSym1 to binary type constructors.

Methods

liftEvalSym2 :: (Bool -> Model -> a -> a) -> (Bool -> Model -> b -> b) -> Bool -> Model -> f a b -> f a b Source #

Lift the evalSym function to binary type constructors.

Instances

Instances details

EvalSym2 Either Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym2 :: (Bool -> Model -> a -> a) -> (Bool -> Model -> b -> b) -> Bool -> Model -> Either a b -> Either a b Source #
EvalSym2 (,) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym2 :: (Bool -> Model -> a -> a) -> (Bool -> Model -> b -> b) -> Bool -> Model -> (a, b) -> (a, b) Source #
EvalSym a => EvalSym2 ((,,) a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym2 :: (Bool -> Model -> a0 -> a0) -> (Bool -> Model -> b -> b) -> Bool -> Model -> (a, a0, b) -> (a, a0, b) Source #
(EvalSym a1, EvalSym a2) => EvalSym2 ((,,,) a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym2 :: (Bool -> Model -> a -> a) -> (Bool -> Model -> b -> b) -> Bool -> Model -> (a1, a2, a, b) -> (a1, a2, a, b) Source #
(EvalSym a1, EvalSym a2, EvalSym a3) => EvalSym2 ((,,,,) a1 a2 a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym2 :: (Bool -> Model -> a -> a) -> (Bool -> Model -> b -> b) -> Bool -> Model -> (a1, a2, a3, a, b) -> (a1, a2, a3, a, b) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4) => EvalSym2 ((,,,,,) a1 a2 a3 a4) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym2 :: (Bool -> Model -> a -> a) -> (Bool -> Model -> b -> b) -> Bool -> Model -> (a1, a2, a3, a4, a, b) -> (a1, a2, a3, a4, a, b) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5) => EvalSym2 ((,,,,,,) a1 a2 a3 a4 a5) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym2 :: (Bool -> Model -> a -> a) -> (Bool -> Model -> b -> b) -> Bool -> Model -> (a1, a2, a3, a4, a5, a, b) -> (a1, a2, a3, a4, a5, a, b) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6) => EvalSym2 ((,,,,,,,) a1 a2 a3 a4 a5 a6) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym2 :: (Bool -> Model -> a -> a) -> (Bool -> Model -> b -> b) -> Bool -> Model -> (a1, a2, a3, a4, a5, a6, a, b) -> (a1, a2, a3, a4, a5, a6, a, b) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6, EvalSym a7) => EvalSym2 ((,,,,,,,,) a1 a2 a3 a4 a5 a6 a7) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym2 :: (Bool -> Model -> a -> a) -> (Bool -> Model -> b -> b) -> Bool -> Model -> (a1, a2, a3, a4, a5, a6, a7, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a, b) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6, EvalSym a7, EvalSym a8) => EvalSym2 ((,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym2 :: (Bool -> Model -> a -> a) -> (Bool -> Model -> b -> b) -> Bool -> Model -> (a1, a2, a3, a4, a5, a6, a7, a8, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a8, a, b) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6, EvalSym a7, EvalSym a8, EvalSym a9) => EvalSym2 ((,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym2 :: (Bool -> Model -> a -> a) -> (Bool -> Model -> b -> b) -> Bool -> Model -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a, b) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6, EvalSym a7, EvalSym a8, EvalSym a9, EvalSym a10) => EvalSym2 ((,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym2 :: (Bool -> Model -> a -> a) -> (Bool -> Model -> b -> b) -> Bool -> Model -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a, b) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6, EvalSym a7, EvalSym a8, EvalSym a9, EvalSym a10, EvalSym a11) => EvalSym2 ((,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym2 :: (Bool -> Model -> a -> a) -> (Bool -> Model -> b -> b) -> Bool -> Model -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a, b) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6, EvalSym a7, EvalSym a8, EvalSym a9, EvalSym a10, EvalSym a11, EvalSym a12) => EvalSym2 ((,,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym2 :: (Bool -> Model -> a -> a) -> (Bool -> Model -> b -> b) -> Bool -> Model -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a, b) Source #
(EvalSym a1, EvalSym a2, EvalSym a3, EvalSym a4, EvalSym a5, EvalSym a6, EvalSym a7, EvalSym a8, EvalSym a9, EvalSym a10, EvalSym a11, EvalSym a12, EvalSym a13) => EvalSym2 ((,,,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym Methods liftEvalSym2 :: (Bool -> Model -> a -> a) -> (Bool -> Model -> b -> b) -> Bool -> Model -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a, b) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a, b) Source #

evalSym2 :: (EvalSym2 f, EvalSym a, EvalSym b) => Bool -> Model -> f a b -> f a b Source #

Lifting the standard evalSym to binary type constructors.

evalSymToCon2 :: (EvalSym2 f, EvalSym a, EvalSym c, ToCon2 f g, ToCon a b, ToCon c d) => Model -> f a c -> g b d Source #

Evaluate and convert to concrete values with lifted standard evalSym for binary type constructors. See evalSymToCon.

Generic `EvalSym`

data family EvalSymArgs arity a Source #

The arguments to the generic evalSym function.

Instances

Instances details

data EvalSymArgs Arity0 _ Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.EvalSym data EvalSymArgs Arity0 _ = EvalSymArgs0
newtype EvalSymArgs Arity1 a Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.EvalSym newtype EvalSymArgs Arity1 a = EvalSymArgs1 (Bool -> Model -> a -> a)

class GEvalSym arity (f :: Type -> Type) where Source #

The class of types that can be generically evaluated.

Methods

gevalSym :: EvalSymArgs arity a -> Bool -> Model -> f a -> f a Source #

Instances

Instances details

GEvalSym Arity1 Par1 Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.EvalSym Methods gevalSym :: EvalSymArgs Arity1 a -> Bool -> Model -> Par1 a -> Par1 a Source #
GEvalSym arity (U1 :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.EvalSym Methods gevalSym :: EvalSymArgs arity a -> Bool -> Model -> U1 a -> U1 a Source #
GEvalSym arity (V1 :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.EvalSym Methods gevalSym :: EvalSymArgs arity a -> Bool -> Model -> V1 a -> V1 a Source #
EvalSym1 a => GEvalSym Arity1 (Rec1 a) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.EvalSym Methods gevalSym :: EvalSymArgs Arity1 a0 -> Bool -> Model -> Rec1 a a0 -> Rec1 a a0 Source #
(GEvalSym arity a, GEvalSym arity b) => GEvalSym arity (a :*: b) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.EvalSym Methods gevalSym :: EvalSymArgs arity a0 -> Bool -> Model -> (a :: b) a0 -> (a :: b) a0 Source #
(GEvalSym arity a, GEvalSym arity b) => GEvalSym arity (a :+: b) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.EvalSym Methods gevalSym :: EvalSymArgs arity a0 -> Bool -> Model -> (a :+: b) a0 -> (a :+: b) a0 Source #
EvalSym a => GEvalSym arity (K1 i a :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.EvalSym Methods gevalSym :: EvalSymArgs arity a0 -> Bool -> Model -> K1 i a a0 -> K1 i a a0 Source #
(EvalSym1 f, GEvalSym Arity1 g) => GEvalSym Arity1 (f :.: g) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.EvalSym Methods gevalSym :: EvalSymArgs Arity1 a -> Bool -> Model -> (f :.: g) a -> (f :.: g) a Source #
GEvalSym arity a => GEvalSym arity (M1 i c a) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Data.Class.EvalSym Methods gevalSym :: EvalSymArgs arity a0 -> Bool -> Model -> M1 i c a a0 -> M1 i c a a0 Source #

genericEvalSym :: (Generic a, GEvalSym Arity0 (Rep a)) => Bool -> Model -> a -> a Source #

Generic evalSym function.

genericLiftEvalSym :: (Generic1 f, GEvalSym Arity1 (Rep1 f)) => (Bool -> Model -> a -> a) -> Bool -> Model -> f a -> f a Source #

Generic liftEvalSym function.

Evaluating symbolic values with model

Instances

Instances

Instances

Generic EvalSym

Instances

Instances

Generic `EvalSym`