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

Grisette.Core.Data.Class.GenSym

Description

 
Synopsis

Indices and identifiers for fresh symbolic value generation

newtype FreshIndex Source #

Index type used for GenSym.

To generate fresh variables, a monadic stateful context will be maintained. The index should be increased every time a new symbolic constant is generated.

Constructors

FreshIndex Int 

data FreshIdent where Source #

Identifier type used for GenSym

The constructor is hidden intentionally. You can construct an identifier by:

  • a raw name

The following two expressions will refer to the same identifier (the solver won't distinguish them and would assign the same value to them). The user may need to use unique names to avoid unintentional identifier collision.

>>> name "a"
a
>>> "a" :: FreshIdent -- available when OverloadedStrings is enabled
a
  • bundle the calling file location with the name to ensure global uniqueness

Identifiers created at different locations will not be the same. The identifiers created at the same location will be the same.

>>> $$(nameWithLoc "a") -- a sample result could be "a:<interactive>:18:4-18"
a:<interactive>:...
  • bundle the calling file location with some user provided information

Identifiers created with different name or different additional information will not be the same.

>>> nameWithInfo "a" (1 :: Int)
a:1

Constructors

FreshIdent :: String -> FreshIdent 
FreshIdentWithInfo :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> FreshIdent 

name :: String -> FreshIdent Source #

Simple name identifier. The same identifier refers to the same symbolic variable in the whole program.

The user may need to use unique names to avoid unintentional identifier collision.

nameWithInfo :: forall a. (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> FreshIdent Source #

Identifier with extra information. The same name with the same information refers to the same symbolic variable in the whole program.

The user may need to use unique names or additional information to avoid unintentional identifier collision.

Monad for fresh symbolic value generation

class Monad m => MonadFresh m where Source #

Monad class for fresh symbolic value generation.

The monad should be a reader monad for the FreshIdent and a state monad for the FreshIndex.

Methods

nextFreshIndex :: m FreshIndex Source #

Increase the index by one and return the new index.

getFreshIdent :: m FreshIdent Source #

Get the identifier.

Instances

Instances details
Monad m => MonadFresh (FreshT m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

MonadFresh m => MonadFresh (ExceptT e m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

MonadFresh m => MonadFresh (ReaderT r m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

MonadFresh m => MonadFresh (StateT s m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

MonadFresh m => MonadFresh (StateT s m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

(MonadFresh m, Monoid w) => MonadFresh (WriterT w m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

(MonadFresh m, Monoid w) => MonadFresh (WriterT w m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

(MonadFresh m, Monoid w) => MonadFresh (RWST r w s m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

(MonadFresh m, Monoid w) => MonadFresh (RWST r w s m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

data FreshT m a Source #

A symbolic generation monad transformer. It is a reader monad transformer for identifiers and a state monad transformer for indices.

Each time a fresh symbolic variable is generated, the index should be increased.

Instances

Instances details
MonadTrans FreshT Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

lift :: Monad m => m a -> FreshT m a #

MonadRWS r w s m => MonadRWS r w s (FreshT m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

MonadError e m => MonadError e (FreshT m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

throwError :: e -> FreshT m a #

catchError :: FreshT m a -> (e -> FreshT m a) -> FreshT m a #

MonadReader r m => MonadReader r (FreshT m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

ask :: FreshT m r #

local :: (r -> r) -> FreshT m a -> FreshT m a #

reader :: (r -> a) -> FreshT m a #

MonadState s m => MonadState s (FreshT m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

get :: FreshT m s #

put :: s -> FreshT m () #

state :: (s -> (a, s)) -> FreshT m a #

MonadWriter w m => MonadWriter w (FreshT m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

writer :: (a, w) -> FreshT m a #

tell :: w -> FreshT m () #

listen :: FreshT m a -> FreshT m (a, w) #

pass :: FreshT m (a, w -> w) -> FreshT m a #

(Applicative m, Monad m) => Applicative (FreshT m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

pure :: a -> FreshT m a #

(<*>) :: FreshT m (a -> b) -> FreshT m a -> FreshT m b #

liftA2 :: (a -> b -> c) -> FreshT m a -> FreshT m b -> FreshT m c #

(*>) :: FreshT m a -> FreshT m b -> FreshT m b #

(<*) :: FreshT m a -> FreshT m b -> FreshT m a #

Functor f => Functor (FreshT f) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fmap :: (a -> b) -> FreshT f a -> FreshT f b #

(<$) :: a -> FreshT f b -> FreshT f a #

Monad m => Monad (FreshT m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

(>>=) :: FreshT m a -> (a -> FreshT m b) -> FreshT m b #

(>>) :: FreshT m a -> FreshT m b -> FreshT m b #

return :: a -> FreshT m a #

Monad m => MonadFresh (FreshT m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Mergeable1 m => Mergeable1 (FreshT m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

UnionLike m => SimpleMergeable1 (FreshT m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> FreshT m a -> FreshT m a -> FreshT m a Source #

UnionLike m => UnionLike (FreshT m) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

(Mergeable a, Mergeable1 m) => Mergeable (FreshT m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

(UnionLike m, Mergeable a) => SimpleMergeable (FreshT m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

mrgIte :: SymBool -> FreshT m a -> FreshT m a -> FreshT m a Source #

type Fresh = FreshT Identity Source #

FreshT specialized with Identity.

runFreshT :: Monad m => FreshT m a -> FreshIdent -> m a Source #

Run the symbolic generation with the given identifier and 0 as the initial index.

runFresh :: Fresh a -> FreshIdent -> a Source #

Run the symbolic generation with the given identifier and 0 as the initial index.

Symbolic value generation

class Mergeable a => GenSym spec a where Source #

Class of types in which symbolic values can be generated with respect to some specification.

The result will be wrapped in a union-like monad. This ensures that we can generate those types with complex merging rules.

The uniqueness of symbolic constants is managed with the a monadic context. Fresh and FreshT can be useful.

Minimal complete definition

Nothing

Methods

fresh :: MonadFresh m => spec -> m (UnionM a) Source #

Generate a symbolic value given some specification. Within a single MonadFresh context, calls to fresh would generate unique symbolic constants.

The following example generates a symbolic boolean. No specification is needed.

>>> runFresh (fresh ()) "a" :: UnionM SymBool
{a@0}

The following example generates booleans, which cannot be merged into a single value with type Bool. No specification is needed.

>>> runFresh (fresh ()) "a" :: UnionM Bool
{If a@0 False True}

The following example generates Maybe Bools. There are more than one symbolic constants introduced, and their uniqueness is ensured. No specification is needed.

>>> runFresh (fresh ()) "a" :: UnionM (Maybe Bool)
{If a@0 Nothing (If a@1 (Just False) (Just True))}

The following example generates lists of symbolic booleans with length 1 to 2.

>>> runFresh (fresh (ListSpec 1 2 ())) "a" :: UnionM [SymBool]
{If a@2 [a@1] [a@0,a@1]}

When multiple symbolic values are generated, there will not be any identifier collision

>>> runFresh (do; a <- fresh (); b <- fresh (); return (a, b)) "a" :: (UnionM SymBool, UnionM SymBool)
({a@0},{a@1})

default fresh :: GenSymSimple spec a => MonadFresh m => spec -> m (UnionM a) Source #

Instances

Instances details
GenSym Int16 Int16 Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => Int16 -> m (UnionM Int16) Source #

GenSym Int32 Int32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => Int32 -> m (UnionM Int32) Source #

GenSym Int64 Int64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => Int64 -> m (UnionM Int64) Source #

GenSym Int8 Int8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => Int8 -> m (UnionM Int8) Source #

GenSym Word16 Word16 Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => Word16 -> m (UnionM Word16) Source #

GenSym Word32 Word32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => Word32 -> m (UnionM Word32) Source #

GenSym Word64 Word64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => Word64 -> m (UnionM Word64) Source #

GenSym Word8 Word8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => Word8 -> m (UnionM Word8) Source #

GenSym ByteString ByteString Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

GenSym SomeIntN SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

GenSym SomeWordN SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

GenSym SomeSymIntN SomeSymIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

GenSym SomeSymWordN SomeSymWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

GenSym SymBool SymBool Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => SymBool -> m (UnionM SymBool) Source #

GenSym SymInteger SymInteger Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

GenSym Integer Integer Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => Integer -> m (UnionM Integer) Source #

GenSym () SymBool Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (UnionM SymBool) Source #

GenSym () SymInteger Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (UnionM SymInteger) Source #

GenSym () () Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (UnionM ()) Source #

GenSym () Bool Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (UnionM Bool) Source #

GenSym Bool Bool Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => Bool -> m (UnionM Bool) Source #

GenSym Char Char Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => Char -> m (UnionM Char) Source #

GenSym Int Int Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => Int -> m (UnionM Int) Source #

GenSym Word Word Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => Word -> m (UnionM Word) Source #

(GenSymSimple () a, Mergeable a) => GenSym Integer [a] Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => Integer -> m (UnionM [a]) Source #

(KnownNat n, 1 <= n) => GenSym () (SymIntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (UnionM (SymIntN n)) Source #

(KnownNat n, 1 <= n) => GenSym () (SymWordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (UnionM (SymWordN n)) Source #

(GenSym () a, Mergeable a) => GenSym () (Maybe a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (UnionM (Maybe a)) Source #

(GenSym spec a, Mergeable a) => GenSym spec (UnionM a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

fresh :: MonadFresh m => spec -> m (UnionM (UnionM a)) Source #

(GenSym () a, Mergeable a, GenSym () b, Mergeable b) => GenSym () (Either a b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (UnionM (Either a b)) Source #

(GenSym () a, Mergeable a, GenSym () b, Mergeable b) => GenSym () (CBMCEither a b) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

fresh :: MonadFresh m => () -> m (UnionM (CBMCEither a b)) Source #

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

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (UnionM (sa -~> sb)) Source #

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

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (UnionM (sa =~> sb)) Source #

(GenSym () a, Mergeable a, GenSym () b, Mergeable b) => GenSym () (a, b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (UnionM (a, b)) Source #

(GenSym spec (m (Maybe a)), Mergeable1 m, Mergeable a) => GenSym spec (MaybeT m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m0 => spec -> m0 (UnionM (MaybeT m a)) Source #

(GenSym () a, Mergeable a, GenSym () b, Mergeable b, GenSym () c, Mergeable c) => GenSym () (a, b, c) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (UnionM (a, b, c)) Source #

(GenSym spec (m (CBMCEither a b)), Mergeable1 m, Mergeable a, Mergeable b) => GenSym spec (CBMCExceptT a m b) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

fresh :: MonadFresh m0 => spec -> m0 (UnionM (CBMCExceptT a m b)) Source #

(GenSym spec (m (Either a b)), Mergeable1 m, Mergeable a, Mergeable b) => GenSym spec (ExceptT a m b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m0 => spec -> m0 (UnionM (ExceptT a m b)) Source #

(GenSym () a, Mergeable a, GenSym () b, Mergeable b, GenSym () c, Mergeable c, GenSym () d, Mergeable d) => GenSym () (a, b, c, d) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (UnionM (a, b, c, d)) Source #

(GenSym () a, Mergeable a, GenSym () b, Mergeable b, GenSym () c, Mergeable c, GenSym () d, Mergeable d, GenSym () e, Mergeable e) => GenSym () (a, b, c, d, e) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (UnionM (a, b, c, d, e)) Source #

(GenSym () a, Mergeable a, GenSym () b, Mergeable b, GenSym () c, Mergeable c, GenSym () d, Mergeable d, GenSym () e, Mergeable e, GenSym () f, Mergeable f) => GenSym () (a, b, c, d, e, f) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (UnionM (a, b, c, d, e, f)) Source #

(GenSym () a, Mergeable a, GenSym () b, Mergeable b, GenSym () c, Mergeable c, GenSym () d, Mergeable d, GenSym () e, Mergeable e, GenSym () f, Mergeable f, GenSym () g, Mergeable g) => GenSym () (a, b, c, d, e, f, g) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (UnionM (a, b, c, d, e, f, g)) Source #

(GenSym () a, Mergeable a, GenSym () b, Mergeable b, GenSym () c, Mergeable c, GenSym () d, Mergeable d, GenSym () e, Mergeable e, GenSym () f, Mergeable f, GenSym () g, Mergeable g, GenSym () h, Mergeable h) => GenSym () (a, b, c, d, e, f, g, h) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (UnionM (a, b, c, d, e, f, g, h)) Source #

(GenSym a a, Mergeable a) => GenSym (UnionM a) a Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

fresh :: MonadFresh m => UnionM a -> m (UnionM a) Source #

(Enum v, Mergeable v) => GenSym (EnumGenBound v) v Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => EnumGenBound v -> m (UnionM v) Source #

(Enum v, Mergeable v) => GenSym (EnumGenUpperBound v) v Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => EnumGenUpperBound v -> m (UnionM v) Source #

(KnownNat n, 1 <= n) => GenSym (p n) SomeSymIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => p n -> m (UnionM SomeSymIntN) Source #

(KnownNat n, 1 <= n) => GenSym (p n) SomeSymWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => p n -> m (UnionM SomeSymWordN) Source #

(KnownNat n, 1 <= n) => GenSym (IntN n) (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => IntN n -> m (UnionM (IntN n)) Source #

(KnownNat n, 1 <= n) => GenSym (WordN n) (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => WordN n -> m (UnionM (WordN n)) Source #

(GenSymSimple spec a, Mergeable a) => GenSym (ListSpec spec) [a] Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => ListSpec spec -> m (UnionM [a]) Source #

(GenSymSimple spec a, Mergeable a) => GenSym (SimpleListSpec spec) [a] Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => SimpleListSpec spec -> m (UnionM [a]) Source #

(KnownNat n, 1 <= n) => GenSym (SymIntN n) (SymIntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => SymIntN n -> m (UnionM (SymIntN n)) Source #

(KnownNat n, 1 <= n) => GenSym (SymWordN n) (SymWordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => SymWordN n -> m (UnionM (SymWordN n)) Source #

(GenSymSimple a a, Mergeable a) => GenSym (Maybe a) (Maybe a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => Maybe a -> m (UnionM (Maybe a)) Source #

(GenSymSimple a a, Mergeable a) => GenSym [a] [a] Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => [a] -> m (UnionM [a]) Source #

(GenSymSimple a a, Mergeable a, GenSymSimple b b, Mergeable b) => GenSym (Either a b) (Either a b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => Either a b -> m (UnionM (Either a b)) Source #

(GenSymSimple a a, Mergeable a, GenSymSimple b b, Mergeable b) => GenSym (CBMCEither a b) (CBMCEither a b) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

fresh :: MonadFresh m => CBMCEither a b -> m (UnionM (CBMCEither a b)) Source #

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

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => (sa -~> sb) -> m (UnionM (sa -~> sb)) Source #

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

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => (sa =~> sb) -> m (UnionM (sa =~> sb)) Source #

(GenSymSimple (m (Maybe a)) (m (Maybe a)), Mergeable1 m, Mergeable a) => GenSym (MaybeT m a) (MaybeT m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m0 => MaybeT m a -> m0 (UnionM (MaybeT m a)) Source #

(GenSym aspec a, Mergeable a, GenSym bspec b, Mergeable b) => GenSym (aspec, bspec) (a, b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => (aspec, bspec) -> m (UnionM (a, b)) Source #

(GenSymSimple (m (CBMCEither e a)) (m (CBMCEither e a)), Mergeable1 m, Mergeable e, Mergeable a) => GenSym (CBMCExceptT e m a) (CBMCExceptT e m a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

fresh :: MonadFresh m0 => CBMCExceptT e m a -> m0 (UnionM (CBMCExceptT e m a)) Source #

(GenSymSimple (m (Either e a)) (m (Either e a)), Mergeable1 m, Mergeable e, Mergeable a) => GenSym (ExceptT e m a) (ExceptT e m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m0 => ExceptT e m a -> m0 (UnionM (ExceptT e m a)) Source #

(GenSym aspec a, Mergeable a, GenSym bspec b, Mergeable b, GenSym cspec c, Mergeable c) => GenSym (aspec, bspec, cspec) (a, b, c) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => (aspec, bspec, cspec) -> m (UnionM (a, b, c)) Source #

(GenSym aspec a, Mergeable a, GenSym bspec b, Mergeable b, GenSym cspec c, Mergeable c, GenSym dspec d, Mergeable d) => GenSym (aspec, bspec, cspec, dspec) (a, b, c, d) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => (aspec, bspec, cspec, dspec) -> m (UnionM (a, b, c, d)) Source #

(GenSym aspec a, Mergeable a, GenSym bspec b, Mergeable b, GenSym cspec c, Mergeable c, GenSym dspec d, Mergeable d, GenSym espec e, Mergeable e) => GenSym (aspec, bspec, cspec, dspec, espec) (a, b, c, d, e) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => (aspec, bspec, cspec, dspec, espec) -> m (UnionM (a, b, c, d, e)) Source #

(GenSym aspec a, Mergeable a, GenSym bspec b, Mergeable b, GenSym cspec c, Mergeable c, GenSym dspec d, Mergeable d, GenSym espec e, Mergeable e, GenSym fspec f, Mergeable f) => GenSym (aspec, bspec, cspec, dspec, espec, fspec) (a, b, c, d, e, f) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => (aspec, bspec, cspec, dspec, espec, fspec) -> m (UnionM (a, b, c, d, e, f)) Source #

(GenSym aspec a, Mergeable a, GenSym bspec b, Mergeable b, GenSym cspec c, Mergeable c, GenSym dspec d, Mergeable d, GenSym espec e, Mergeable e, GenSym fspec f, Mergeable f, GenSym gspec g, Mergeable g) => GenSym (aspec, bspec, cspec, dspec, espec, fspec, gspec) (a, b, c, d, e, f, g) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => (aspec, bspec, cspec, dspec, espec, fspec, gspec) -> m (UnionM (a, b, c, d, e, f, g)) Source #

(GenSym aspec a, Mergeable a, GenSym bspec b, Mergeable b, GenSym cspec c, Mergeable c, GenSym dspec d, Mergeable d, GenSym espec e, Mergeable e, GenSym fspec f, Mergeable f, GenSym gspec g, Mergeable g, GenSym hspec h, Mergeable h) => GenSym (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) (a, b, c, d, e, f, g, h) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) -> m (UnionM (a, b, c, d, e, f, g, h)) Source #

class GenSymSimple spec a where Source #

Class of types in which symbolic values can be generated with respect to some specification.

The result will not be wrapped in a union-like monad.

The uniqueness of symbolic constants is managed with the a monadic context. Fresh and FreshT can be useful.

Methods

simpleFresh :: MonadFresh m => spec -> m a Source #

Generate a symbolic value given some specification. The uniqueness is ensured.

The following example generates a symbolic boolean. No specification is needed.

>>> runFresh (simpleFresh ()) "a" :: SymBool
a@0

The following code generates list of symbolic boolean with length 2. As the length is fixed, we don't have to wrap the result in unions.

>>> runFresh (simpleFresh (SimpleListSpec 2 ())) "a" :: [SymBool]
[a@0,a@1]

Instances

Instances details
GenSymSimple Int16 Int16 Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

GenSymSimple Int32 Int32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

GenSymSimple Int64 Int64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

GenSymSimple Int8 Int8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => Int8 -> m Int8 Source #

GenSymSimple Word16 Word16 Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

GenSymSimple Word32 Word32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

GenSymSimple Word64 Word64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

GenSymSimple Word8 Word8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

GenSymSimple ByteString ByteString Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

GenSymSimple SomeIntN SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

GenSymSimple SomeWordN SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

GenSymSimple SomeSymIntN SomeSymIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

GenSymSimple SomeSymWordN SomeSymWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

GenSymSimple SymBool SymBool Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

GenSymSimple SymInteger SymInteger Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

GenSymSimple Integer Integer Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

GenSymSimple () SymBool Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => () -> m SymBool Source #

GenSymSimple () SymInteger Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => () -> m SymInteger Source #

GenSymSimple () () Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => () -> m () Source #

GenSymSimple Bool Bool Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => Bool -> m Bool Source #

GenSymSimple Char Char Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => Char -> m Char Source #

GenSymSimple Int Int Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => Int -> m Int Source #

GenSymSimple Word Word Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => Word -> m Word Source #

(KnownNat n, 1 <= n) => GenSymSimple () (SymIntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => () -> m (SymIntN n) Source #

(KnownNat n, 1 <= n) => GenSymSimple () (SymWordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => () -> m (SymWordN n) Source #

GenSym spec a => GenSymSimple spec (UnionM a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

simpleFresh :: MonadFresh m => spec -> m (UnionM a) Source #

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

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => () -> m (sa -~> sb) Source #

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

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => () -> m (sa =~> sb) Source #

(GenSymSimple () a, GenSymSimple () b) => GenSymSimple () (a, b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => () -> m (a, b) Source #

GenSymSimple spec (m (Maybe a)) => GenSymSimple spec (MaybeT m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m0 => spec -> m0 (MaybeT m a) Source #

(GenSymSimple () a, GenSymSimple () b, GenSymSimple () c) => GenSymSimple () (a, b, c) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => () -> m (a, b, c) Source #

GenSymSimple spec (m (CBMCEither a b)) => GenSymSimple spec (CBMCExceptT a m b) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

simpleFresh :: MonadFresh m0 => spec -> m0 (CBMCExceptT a m b) Source #

GenSymSimple spec (m (Either a b)) => GenSymSimple spec (ExceptT a m b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m0 => spec -> m0 (ExceptT a m b) Source #

(GenSymSimple () a, GenSymSimple () b, GenSymSimple () c, GenSymSimple () d) => GenSymSimple () (a, b, c, d) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => () -> m (a, b, c, d) Source #

(GenSymSimple () a, GenSymSimple () b, GenSymSimple () c, GenSymSimple () d, GenSymSimple () e) => GenSymSimple () (a, b, c, d, e) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => () -> m (a, b, c, d, e) Source #

(GenSymSimple () a, GenSymSimple () b, GenSymSimple () c, GenSymSimple () d, GenSymSimple () e, GenSymSimple () f) => GenSymSimple () (a, b, c, d, e, f) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => () -> m (a, b, c, d, e, f) Source #

(GenSymSimple () a, GenSymSimple () b, GenSymSimple () c, GenSymSimple () d, GenSymSimple () e, GenSymSimple () f, GenSymSimple () g) => GenSymSimple () (a, b, c, d, e, f, g) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => () -> m (a, b, c, d, e, f, g) Source #

(GenSymSimple () a, GenSymSimple () b, GenSymSimple () c, GenSymSimple () d, GenSymSimple () e, GenSymSimple () f, GenSymSimple () g, GenSymSimple () h) => GenSymSimple () (a, b, c, d, e, f, g, h) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => () -> m (a, b, c, d, e, f, g, h) Source #

(KnownNat n, 1 <= n) => GenSymSimple (p n) SomeSymIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => p n -> m SomeSymIntN Source #

(KnownNat n, 1 <= n) => GenSymSimple (p n) SomeSymWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => p n -> m SomeSymWordN Source #

(KnownNat n, 1 <= n) => GenSymSimple (IntN n) (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => IntN n -> m (IntN n) Source #

(KnownNat n, 1 <= n) => GenSymSimple (WordN n) (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => WordN n -> m (WordN n) Source #

GenSymSimple spec a => GenSymSimple (SimpleListSpec spec) [a] Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => SimpleListSpec spec -> m [a] Source #

(KnownNat n, 1 <= n) => GenSymSimple (SymIntN n) (SymIntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => SymIntN n -> m (SymIntN n) Source #

(KnownNat n, 1 <= n) => GenSymSimple (SymWordN n) (SymWordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => SymWordN n -> m (SymWordN n) Source #

GenSymSimple a a => GenSymSimple (Maybe a) (Maybe a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => Maybe a -> m (Maybe a) Source #

GenSymSimple a a => GenSymSimple [a] [a] Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => [a] -> m [a] Source #

(GenSymSimple a a, GenSymSimple b b) => GenSymSimple (Either a b) (Either a b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => Either a b -> m (Either a b) Source #

(GenSymSimple a a, GenSymSimple b b) => GenSymSimple (CBMCEither a b) (CBMCEither a b) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

simpleFresh :: MonadFresh m => CBMCEither a b -> m (CBMCEither a b) Source #

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

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => (sa -~> sb) -> m (sa -~> sb) Source #

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

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => (sa =~> sb) -> m (sa =~> sb) Source #

GenSymSimple (m (Maybe a)) (m (Maybe a)) => GenSymSimple (MaybeT m a) (MaybeT m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m0 => MaybeT m a -> m0 (MaybeT m a) Source #

(GenSymSimple aspec a, GenSymSimple bspec b) => GenSymSimple (aspec, bspec) (a, b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => (aspec, bspec) -> m (a, b) Source #

GenSymSimple (m (CBMCEither e a)) (m (CBMCEither e a)) => GenSymSimple (CBMCExceptT e m a) (CBMCExceptT e m a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

simpleFresh :: MonadFresh m0 => CBMCExceptT e m a -> m0 (CBMCExceptT e m a) Source #

GenSymSimple (m (Either e a)) (m (Either e a)) => GenSymSimple (ExceptT e m a) (ExceptT e m a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m0 => ExceptT e m a -> m0 (ExceptT e m a) Source #

(GenSymSimple aspec a, GenSymSimple bspec b, GenSymSimple cspec c) => GenSymSimple (aspec, bspec, cspec) (a, b, c) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => (aspec, bspec, cspec) -> m (a, b, c) Source #

(GenSymSimple aspec a, GenSymSimple bspec b, GenSymSimple cspec c, GenSymSimple dspec d) => GenSymSimple (aspec, bspec, cspec, dspec) (a, b, c, d) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => (aspec, bspec, cspec, dspec) -> m (a, b, c, d) Source #

(GenSymSimple aspec a, GenSymSimple bspec b, GenSymSimple cspec c, GenSymSimple dspec d, GenSymSimple espec e) => GenSymSimple (aspec, bspec, cspec, dspec, espec) (a, b, c, d, e) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => (aspec, bspec, cspec, dspec, espec) -> m (a, b, c, d, e) Source #

(GenSymSimple aspec a, GenSymSimple bspec b, GenSymSimple cspec c, GenSymSimple dspec d, GenSymSimple espec e, GenSymSimple fspec f) => GenSymSimple (aspec, bspec, cspec, dspec, espec, fspec) (a, b, c, d, e, f) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => (aspec, bspec, cspec, dspec, espec, fspec) -> m (a, b, c, d, e, f) Source #

(GenSymSimple aspec a, GenSymSimple bspec b, GenSymSimple cspec c, GenSymSimple dspec d, GenSymSimple espec e, GenSymSimple fspec f, GenSymSimple gspec g) => GenSymSimple (aspec, bspec, cspec, dspec, espec, fspec, gspec) (a, b, c, d, e, f, g) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => (aspec, bspec, cspec, dspec, espec, fspec, gspec) -> m (a, b, c, d, e, f, g) Source #

(GenSymSimple aspec a, GenSymSimple bspec b, GenSymSimple cspec c, GenSymSimple dspec d, GenSymSimple espec e, GenSymSimple fspec f, GenSymSimple gspec g, GenSymSimple hspec h) => GenSymSimple (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) (a, b, c, d, e, f, g, h) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) -> m (a, b, c, d, e, f, g, h) Source #

genSym :: GenSym spec a => spec -> FreshIdent -> UnionM a Source #

Generate a symbolic variable wrapped in a Union without the monadic context. A globally unique identifier should be supplied to ensure the uniqueness of symbolic constants in the generated symbolic values.

>>> genSym (ListSpec 1 2 ()) "a" :: UnionM [SymBool]
{If a@2 [a@1] [a@0,a@1]}

genSymSimple :: forall spec a. GenSymSimple spec a => spec -> FreshIdent -> a Source #

Generate a simple symbolic variable wrapped in a Union without the monadic context. A globally unique identifier should be supplied to ensure the uniqueness of symbolic constants in the generated symbolic values.

>>> genSymSimple (SimpleListSpec 2 ()) "a" :: [SymBool]
[a@0,a@1]

derivedNoSpecFresh :: forall bool a m u. (Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) => () -> m (UnionM a) Source #

We cannot provide DerivingVia style derivation for GenSym, while you can use this fresh implementation to implement GenSym for your own types.

This fresh implementation is for the types that does not need any specification. It will generate product types by generating each fields with () as specification, and generate all possible values for a sum type.

Note: Never use on recursive types.

derivedNoSpecSimpleFresh :: forall a m. (Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) => () -> m a Source #

We cannot provide DerivingVia style derivation for GenSymSimple, while you can use this simpleFresh implementation to implement GenSymSimple fo your own types.

This simpleFresh implementation is for the types that does not need any specification. It will generate product types by generating each fields with () as specification. It will not work on sum types.

Note: Never use on recursive types.

derivedSameShapeSimpleFresh :: forall a m. (Generic a, GenSymSameShape (Rep a), MonadFresh m) => a -> m a Source #

We cannot provide DerivingVia style derivation for GenSymSimple, while you can use this simpleFresh implementation to implement GenSymSimple fo your own types.

This simpleFresh implementation is for the types that can be generated with a reference value of the same type.

For sum types, it will generate the result with the same data constructor. For product types, it will generate the result by generating each field with the corresponding reference value.

Note: Can be used on recursive types.

Symbolic choices

chooseFresh :: forall bool a m u. (Mergeable a, MonadFresh m) => [a] -> m (UnionM a) Source #

Symbolically chooses one of the provided values. The procedure creates n - 1 fresh symbolic boolean variables every time it is evaluated, and use these variables to conditionally select one of the n provided expressions.

The result will be wrapped in a union-like monad, and also a monad maintaining the MonadFresh context.

>>> runFresh (chooseFresh [1,2,3]) "a" :: UnionM Integer
{If a@0 1 (If a@1 2 3)}

chooseSimpleFresh :: forall a m. (SimpleMergeable a, MonadFresh m) => [a] -> m a Source #

Symbolically chooses one of the provided values. The procedure creates n - 1 fresh symbolic boolean variables every time it is evaluated, and use these variables to conditionally select one of the n provided expressions.

The result will not be wrapped in a union-like monad, but will be wrapped in a monad maintaining the Fresh context.

>>> import Data.Proxy
>>> runFresh (chooseSimpleFresh [ssym "b", ssym "c", ssym "d"]) "a" :: SymInteger
(ite a@0 b (ite a@1 c d))

chooseUnionFresh :: forall bool a m u. (Mergeable a, MonadFresh m) => [UnionM a] -> m (UnionM a) Source #

Symbolically chooses one of the provided values wrapped in union-like monads. The procedure creates n - 1 fresh symbolic boolean variables every time it is evaluated, and use these variables to conditionally select one of the n provided expressions.

The result will be wrapped in a union-like monad, and also a monad maintaining the Fresh context.

>>> let a = runFresh (chooseFresh [1, 2]) "a" :: UnionM Integer
>>> let b = runFresh (chooseFresh [2, 3]) "b" :: UnionM Integer
>>> runFresh (chooseUnionFresh [a, b]) "c" :: UnionM Integer
{If (&& c@0 a@0) 1 (If (|| c@0 b@0) 2 3)}

choose :: forall bool a u. Mergeable a => [a] -> FreshIdent -> UnionM a Source #

A wrapper for chooseFresh that executes the MonadFresh context. A globally unique identifier should be supplied to ensure the uniqueness of symbolic constants in the generated symbolic values.

chooseSimple :: forall a. SimpleMergeable a => [a] -> FreshIdent -> a Source #

A wrapper for chooseSimpleFresh that executes the MonadFresh context. A globally unique identifier should be supplied to ensure the uniqueness of symbolic constants in the generated symbolic values.

chooseUnion :: forall a u. Mergeable a => [UnionM a] -> FreshIdent -> UnionM a Source #

A wrapper for chooseUnionFresh that executes the MonadFresh context. A globally unique identifier should be supplied to ensure the uniqueness of symbolic constants in the generated symbolic values.

Some common GenSym specifications

data ListSpec spec Source #

Specification for list generation.

>>> runFresh (fresh (ListSpec 0 2 ())) "c" :: UnionM [SymBool]
{If c@2 [] (If c@3 [c@1] [c@0,c@1])}
>>> runFresh (fresh (ListSpec 0 2 (SimpleListSpec 1 ()))) "c" :: UnionM [[SymBool]]
{If c@2 [] (If c@3 [[c@1]] [[c@0],[c@1]])}

Constructors

ListSpec 

Fields

Instances

Instances details
Show spec => Show (ListSpec spec) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

showsPrec :: Int -> ListSpec spec -> ShowS #

show :: ListSpec spec -> String #

showList :: [ListSpec spec] -> ShowS #

(GenSymSimple spec a, Mergeable a) => GenSym (ListSpec spec) [a] Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => ListSpec spec -> m (UnionM [a]) Source #

data SimpleListSpec spec Source #

Specification for list generation of a specific length.

>>> runFresh (simpleFresh (SimpleListSpec 2 ())) "c" :: [SymBool]
[c@0,c@1]

Constructors

SimpleListSpec 

Fields

Instances

Instances details
Show spec => Show (SimpleListSpec spec) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

(GenSymSimple spec a, Mergeable a) => GenSym (SimpleListSpec spec) [a] Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => SimpleListSpec spec -> m (UnionM [a]) Source #

GenSymSimple spec a => GenSymSimple (SimpleListSpec spec) [a] Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => SimpleListSpec spec -> m [a] Source #

data EnumGenBound a Source #

Specification for numbers with lower bound (inclusive) and upper bound (exclusive)

>>> runFresh (fresh (EnumGenBound @Integer 0 4)) "c" :: UnionM Integer
{If c@0 0 (If c@1 1 (If c@2 2 3))}

Constructors

EnumGenBound a a 

Instances

Instances details
(Enum v, Mergeable v) => GenSym (EnumGenBound v) v Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => EnumGenBound v -> m (UnionM v) Source #

newtype EnumGenUpperBound a Source #

Specification for enum values with upper bound (exclusive). The result would chosen from [0 .. upperbound].

>>> runFresh (fresh (EnumGenUpperBound @Integer 4)) "c" :: UnionM Integer
{If c@0 0 (If c@1 1 (If c@2 2 3))}

Constructors

EnumGenUpperBound a 

Instances

Instances details
(Enum v, Mergeable v) => GenSym (EnumGenUpperBound v) v Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => EnumGenUpperBound v -> m (UnionM v) Source #