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.

Also note that we need to have the following `LANGUAGE`

options defined:
`TemplateHaskell`

, `StandaloneDeriving`

, `DeriveDataTypeable`

, `DeriveAnyClass`

for
this to work.

elts :: IO AllSatResult Source #

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

`>>>`

Solution #1: s0 = B :: E Solution #2: s0 = A :: 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`