sbv-5.7: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Data.SBV.Examples.Misc.Enumerate

Description

Demonstrates how enumerations can be translated to their SMT-Lib counterparts, without losing any information content. Also see Data.SBV.Examples.Puzzles.U2Bridge for a more detailed example involving enumerations.

Synopsis

# Documentation

data E Source

A simple enumerated type, that we'd like to translate to SMT-Lib intact; i.e., this type will not be uninterpreted but rather preserved and will be just like any other symbolic type SBV provides. Note the automatically derived classes we need: `Eq`, `Ord`, `Data`, `Read`, `Show`, `SymWord`, `HasKind`, and `SatModel`. (The last one is only needed if `getModel` and friends are used.)

Also note that we need to `import Data.Generics` and have the `LANGUAGE` option `DeriveDataTypeable` and `DeriveAnyClass` set.

Constructors

 A B C

Instances

 Source Source Source Source Source Source Source

type SE = SBV E Source

Give a name to the symbolic variants of `E`, for convenience

Have the SMT solver enumerate the elements of the domain. We have:

````>>> ````elts
```Solution #1:
s0 = A :: E
Solution #2:
s0 = B :: E
Solution #3:
s0 = C :: E
Found 3 different solutions.
```

Shows that if we require 4 distinct elements of the type `E`, we shall fail; as the domain only has three elements. We have:

````>>> ````four
```Unsatisfiable
```

Enumerations are automatically ordered, so we can ask for the maximum element. Note the use of quantification. We have:

````>>> ````maxE
```Satisfiable. Model:
maxE = C :: E
```

Similarly, we get the minumum element. We have:

````>>> ````minE
```Satisfiable. Model:
minE = A :: E
```