Copyright | (c) Levent Erkok |
---|---|

License | BSD3 |

Maintainer | erkokl@gmail.com |

Stability | experimental |

Safe Haskell | None |

Language | Haskell2010 |

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.

# Documentation

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.

elts :: IO AllSatResult Source

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

`>>>`

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

Shows that if we require 4 distinct elements of the type `E`

, we shall fail; as
the domain only has three elements. We have:

`>>>`

Unsatisfiable`four`

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

`>>>`

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