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

Grisette.Internal.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 

Instances

Instances details
Num FreshIndex Source # 
Instance details

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

Show FreshIndex Source # 
Instance details

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

Eq FreshIndex Source # 
Instance details

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

Ord FreshIndex Source # 
Instance details

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

Mergeable FreshIndex Source # 
Instance details

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

SimpleMergeable FreshIndex Source # 
Instance details

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

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 Identifier and a state monad for the FreshIndex.

Methods

getFreshIndex :: m FreshIndex Source #

Get the current index for fresh variable generation.

setFreshIndex :: FreshIndex -> m () Source #

Set the current index for fresh variable generation.

getIdentifier :: m Identifier Source #

Get the identifier.

localIdentifier :: (Identifier -> Identifier) -> m a -> m a Source #

Change the identifier locally and use a new index from 0 locally.

Instances

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

nextFreshIndex :: MonadFresh m => m FreshIndex Source #

Get the next fresh index and increase the current index.

liftFresh :: MonadFresh m => Fresh a -> m a Source #

Lifts an Fresh a into any MonadFresh.

newtype FreshT m a Source #

A symbolic generation monad transformer.

It is a reader monad transformer for an identifier and a state monad transformer for indices.

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

Constructors

FreshT 

Instances

Instances details
MonadTrans FreshT Source # 
Instance details

Defined in Grisette.Internal.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.Internal.Core.Data.Class.GenSym

(Typeable mode, UnifiedBranching mode m) => UnifiedBranching mode (FreshT m) Source # 
Instance details

Defined in Grisette.Unified.Internal.Class.UnifiedSimpleMergeable

Methods

withBaseBranching :: (If (IsConMode mode) (TryMerge (FreshT m)) (SymBranching (FreshT m)) => r) -> r Source #

(Typeable mode, UnifiedBranching mode m) => UnifiedSimpleMergeable1 mode (FreshT m) Source # 
Instance details

Defined in Grisette.Unified.Internal.Class.UnifiedSimpleMergeable

Methods

withBaseSimpleMergeable1 :: (If (IsConMode mode) () (SimpleMergeable1 (FreshT m)) => r) -> r Source #

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

Defined in Grisette.Internal.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.Internal.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.Internal.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.Internal.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 #

(Typeable mode, UnifiedBranching mode m, Mergeable a) => UnifiedSimpleMergeable mode (FreshT m a) Source # 
Instance details

Defined in Grisette.Unified.Internal.Class.UnifiedSimpleMergeable

Methods

withBaseSimpleMergeable :: (If (IsConMode mode) () (SimpleMergeable (FreshT m a)) => r) -> r Source #

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

Defined in Grisette.Internal.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.Internal.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.Internal.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.Internal.Core.Data.Class.GenSym

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

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

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

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

Methods

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

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

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

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

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

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

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

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

Defined in Grisette.Internal.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 -> Identifier -> m a Source #

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

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

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

mrgRunFreshT :: (Monad m, TryMerge m, Mergeable a) => FreshT m a -> Identifier -> m a Source #

Run the symbolic generation with the given identifier and 0 as the initial index, and try to merge the result.

freshString :: (MonadFresh m, IsString s) => String -> m s Source #

Generate a fresh string with the given postfix.

>>> runFresh (freshString "b") "a" :: String
"a@0[b]"

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 (Union 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" :: Union 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" :: Union 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" :: Union (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" :: Union [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" :: (Union SymBool, Union SymBool)
({a@0},{a@1})

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

Instances

Instances details
GenSym Int16 Int16 Source # 
Instance details

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

Methods

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

GenSym Int32 Int32 Source # 
Instance details

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

Methods

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

GenSym Int64 Int64 Source # 
Instance details

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

Methods

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

GenSym Int8 Int8 Source # 
Instance details

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

Methods

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

GenSym Word16 Word16 Source # 
Instance details

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

Methods

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

GenSym Word32 Word32 Source # 
Instance details

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

Methods

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

GenSym Word64 Word64 Source # 
Instance details

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

Methods

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

GenSym Word8 Word8 Source # 
Instance details

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

Methods

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

GenSym ByteString ByteString Source # 
Instance details

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

GenSym FPRoundingMode FPRoundingMode Source # 
Instance details

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

GenSym SymAlgReal SymAlgReal Source # 
Instance details

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

GenSym SymBool SymBool Source # 
Instance details

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

Methods

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

GenSym SymFPRoundingMode SymFPRoundingMode Source # 
Instance details

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

GenSym SymInteger SymInteger Source # 
Instance details

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

GenSym Text Text Source # 
Instance details

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

Methods

fresh :: MonadFresh m => Text -> m (Union Text) Source #

GenSym Integer Integer Source # 
Instance details

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

Methods

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

GenSym () SymAlgReal Source # 
Instance details

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

Methods

fresh :: MonadFresh m => () -> m (Union SymAlgReal) Source #

GenSym () SymBool Source # 
Instance details

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

Methods

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

GenSym () SymFPRoundingMode Source # 
Instance details

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

Methods

fresh :: MonadFresh m => () -> m (Union SymFPRoundingMode) Source #

GenSym () SymInteger Source # 
Instance details

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

Methods

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

GenSym () () Source # 
Instance details

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

Methods

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

GenSym () Bool Source # 
Instance details

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

Methods

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

GenSym Bool Bool Source # 
Instance details

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

Methods

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

GenSym Char Char Source # 
Instance details

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

Methods

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

GenSym Double Double Source # 
Instance details

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

Methods

fresh :: MonadFresh m => Double -> m (Union Double) Source #

GenSym Float Float Source # 
Instance details

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

Methods

fresh :: MonadFresh m => Float -> m (Union Float) Source #

GenSym Int Int Source # 
Instance details

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

Methods

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

GenSym Word Word Source # 
Instance details

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

Methods

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

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

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

Methods

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

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

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

Methods

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

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

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

Methods

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

(forall (n :: Nat). (KnownNat n, 1 <= n) => GenSym () (bv n), Mergeable (SomeBV bv)) => GenSym Int (SomeBV bv) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

fresh :: MonadFresh m => Int -> m (Union (SomeBV bv)) Source #

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

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

Methods

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

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

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

Methods

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

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

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

Methods

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

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

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

Methods

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

ValidFP eb sb => GenSym () (SymFP eb sb) Source # 
Instance details

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

Methods

fresh :: MonadFresh m => () -> m (Union (SymFP eb sb)) Source #

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

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

Methods

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

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

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

Methods

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

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

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

Methods

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

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

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

Methods

fresh :: MonadFresh m0 => spec -> m0 (Union (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.Internal.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (Union (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.Internal.Core.Control.Monad.CBMCExcept

Methods

fresh :: MonadFresh m0 => spec -> m0 (Union (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.Internal.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m0 => spec -> m0 (Union (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.Internal.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (Union (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.Internal.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (Union (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.Internal.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (Union (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.Internal.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (Union (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.Internal.Core.Data.Class.GenSym

Methods

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

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

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

Methods

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

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

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

Methods

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

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

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

Methods

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

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

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

Methods

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

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

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

Methods

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

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

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

Methods

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

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

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

Methods

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

(forall (m :: Nat). (KnownNat m, 1 <= m) => GenSym () (bv m), Mergeable (SomeBV bv)) => GenSym (SomeBV bv) (SomeBV bv) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

fresh :: MonadFresh m => SomeBV bv -> m (Union (SomeBV bv)) Source #

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

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

Methods

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

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

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

Methods

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

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

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

Methods

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

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

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

Methods

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

(KnownNat n, 1 <= n, forall (m :: Nat). (KnownNat m, 1 <= m) => GenSym () (bv m), Mergeable (SomeBV bv)) => GenSym (Proxy n) (SomeBV bv) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

fresh :: MonadFresh m => Proxy n -> m (Union (SomeBV bv)) Source #

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

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

Methods

fresh :: MonadFresh m => Either aspec bspec -> m (Union (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.Internal.Core.Control.Monad.CBMCExcept

Methods

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

ValidFP eb sb => GenSym (FP eb sb) (FP eb sb) Source # 
Instance details

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

Methods

fresh :: MonadFresh m => FP eb sb -> m (Union (FP eb sb)) Source #

ValidFP eb sb => GenSym (SymFP eb sb) (SymFP eb sb) Source # 
Instance details

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

Methods

fresh :: MonadFresh m => SymFP eb sb -> m (Union (SymFP eb sb)) Source #

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

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

Methods

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

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

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

Methods

fresh :: MonadFresh m => (sa =~> sb) -> m (Union (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.Internal.Core.Data.Class.GenSym

Methods

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

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

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

Methods

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

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

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

Methods

fresh :: MonadFresh m => (aspec, bspec) -> m (Union (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.Internal.Core.Control.Monad.CBMCExcept

Methods

fresh :: MonadFresh m0 => CBMCExceptT e m a -> m0 (Union (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.Internal.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m0 => ExceptT e m a -> m0 (Union (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.Internal.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => (aspec, bspec, cspec) -> m (Union (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.Internal.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => (aspec, bspec, cspec, dspec) -> m (Union (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.Internal.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => (aspec, bspec, cspec, dspec, espec) -> m (Union (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.Internal.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => (aspec, bspec, cspec, dspec, espec, fspec) -> m (Union (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.Internal.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => (aspec, bspec, cspec, dspec, espec, fspec, gspec) -> m (Union (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.Internal.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) -> m (Union (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.Internal.Core.Data.Class.GenSym

GenSymSimple Int32 Int32 Source # 
Instance details

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

GenSymSimple Int64 Int64 Source # 
Instance details

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

GenSymSimple Int8 Int8 Source # 
Instance details

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

Methods

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

GenSymSimple Word16 Word16 Source # 
Instance details

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

GenSymSimple Word32 Word32 Source # 
Instance details

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

GenSymSimple Word64 Word64 Source # 
Instance details

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

GenSymSimple Word8 Word8 Source # 
Instance details

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

GenSymSimple ByteString ByteString Source # 
Instance details

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

GenSymSimple FPRoundingMode FPRoundingMode Source # 
Instance details

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

GenSymSimple SymAlgReal SymAlgReal Source # 
Instance details

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

GenSymSimple SymBool SymBool Source # 
Instance details

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

GenSymSimple SymFPRoundingMode SymFPRoundingMode Source # 
Instance details

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

GenSymSimple SymInteger SymInteger Source # 
Instance details

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

GenSymSimple Text Text Source # 
Instance details

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

Methods

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

GenSymSimple Integer Integer Source # 
Instance details

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

GenSymSimple () SymAlgReal Source # 
Instance details

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

Methods

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

GenSymSimple () SymBool Source # 
Instance details

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

Methods

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

GenSymSimple () SymFPRoundingMode Source # 
Instance details

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

GenSymSimple () SymInteger Source # 
Instance details

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

Methods

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

GenSymSimple () () Source # 
Instance details

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

Methods

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

GenSymSimple Bool Bool Source # 
Instance details

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

Methods

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

GenSymSimple Char Char Source # 
Instance details

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

Methods

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

GenSymSimple Double Double Source # 
Instance details

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

GenSymSimple Float Float Source # 
Instance details

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

GenSymSimple Int Int Source # 
Instance details

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

Methods

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

GenSymSimple Word Word Source # 
Instance details

Defined in Grisette.Internal.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.Internal.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.Internal.Core.Data.Class.GenSym

Methods

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

(forall (n :: Nat). (KnownNat n, 1 <= n) => GenSymSimple () (bv n), Mergeable (SomeBV bv)) => GenSymSimple Int (SomeBV bv) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

simpleFresh :: MonadFresh m => Int -> m (SomeBV bv) Source #

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

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

Methods

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

ValidFP eb sb => GenSymSimple () (SymFP eb sb) Source # 
Instance details

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

Methods

simpleFresh :: MonadFresh m => () -> m (SymFP eb sb) Source #

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

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

Methods

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

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

Defined in Grisette.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.Core.Data.Class.GenSym

Methods

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

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

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

Methods

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

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

Defined in Grisette.Internal.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.Internal.Core.Data.Class.GenSym

Methods

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

(forall (m :: Nat). (KnownNat m, 1 <= m) => GenSymSimple () (bv m), Mergeable (SomeBV bv)) => GenSymSimple (SomeBV bv) (SomeBV bv) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

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

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

Defined in Grisette.Internal.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.Internal.Core.Data.Class.GenSym

Methods

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

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

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

Methods

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

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

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

Methods

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

(KnownNat n, 1 <= n, forall (m :: Nat). (KnownNat m, 1 <= m) => GenSymSimple () (bv m), Mergeable (SomeBV bv)) => GenSymSimple (Proxy n) (SomeBV bv) Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

simpleFresh :: MonadFresh m => Proxy n -> m (SomeBV bv) Source #

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

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

Methods

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

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

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

Methods

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

ValidFP eb sb => GenSymSimple (FP eb sb) (FP eb sb) Source # 
Instance details

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

Methods

simpleFresh :: MonadFresh m => FP eb sb -> m (FP eb sb) Source #

ValidFP eb sb => GenSymSimple (SymFP eb sb) (SymFP eb sb) Source # 
Instance details

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

Methods

simpleFresh :: MonadFresh m => SymFP eb sb -> m (SymFP eb sb) Source #

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

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

Methods

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

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

Defined in Grisette.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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 -> Identifier -> Union 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" :: Union [SymBool]
{If a@2 [a@1] [a@0,a@1]}

genSymSimple :: forall spec a. GenSymSimple spec a => spec -> Identifier -> 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 a m. (Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) => () -> m (Union 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 a m. (Mergeable a, MonadFresh m) => [a] -> m (Union 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" :: Union 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 a m. (Mergeable a, MonadFresh m) => [Union a] -> m (Union 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" :: Union Integer
>>> let b = runFresh (chooseFresh [2, 3]) "b" :: Union Integer
>>> runFresh (chooseUnionFresh [a, b]) "c" :: Union Integer
{If (&& c@0 a@0) 1 (If (|| c@0 b@0) 2 3)}

choose :: forall a. Mergeable a => [a] -> Identifier -> Union 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] -> Identifier -> 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. Mergeable a => [Union a] -> Identifier -> Union 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" :: Union [SymBool]
{If c@2 [] (If c@3 [c@1] [c@0,c@1])}
>>> runFresh (fresh (ListSpec 0 2 (SimpleListSpec 1 ()))) "c" :: Union [[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.Internal.Core.Data.Class.GenSym

Methods

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

show :: ListSpec spec -> String #

showList :: [ListSpec spec] -> ShowS #

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

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e m, MonadUnion m) => e -> ListSpec spec -> m (Union [a]) Source #

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

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

Methods

fresh :: MonadFresh m => ListSpec spec -> m (Union [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.Internal.Core.Data.Class.GenSym

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

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e m, MonadUnion m) => e -> SimpleListSpec spec -> m (Union [a]) Source #

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

Defined in Grisette.Experimental.GenSymConstrained

Methods

simpleFreshConstrained :: (MonadFresh m, MonadError e m, MonadUnion m) => e -> SimpleListSpec spec -> m [a] Source #

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

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

Methods

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

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

Defined in Grisette.Internal.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" :: Union 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.Internal.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => EnumGenBound v -> m (Union 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" :: Union 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.Internal.Core.Data.Class.GenSym

Methods

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