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.

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

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.

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 class for fresh symbolic value generation.

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

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.

FreshT specialized with Identity.

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

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

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.

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.

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]}

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]

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.

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.

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.

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)}

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))

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)}

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.

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.

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.

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]])}

Specification for list generation of a specific length.

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

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))}

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))}