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 slew of classes we need: `Eq`

, `Ord`

, `Data`

, `Typeable`

, `Read`

,
and `Show`

. For symbolic enumerated types, you should
always let GHC derive these instances. Aside from these, we also need
instances for `SymWord`

, `HasKind`

and `SatModel`

. Again, the default definitions suffice
so the actual declarations are straightforward.

Also note that we need to `import Data.Generics`

and have the `LANGUAGE`

option `DeriveDataTypeable`

set.

Eq E | |

Data E | |

Ord E | |

Read E | |

Show E | |

SymWord E | The |

HasKind E | The |

SatModel E | The |

Typeable * E |

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`