Data.SBV.Examples.Misc.Enumerate

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

data E

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.

Constructors

A

B

C

Instances

Eq E

Data E

Ord E

Read E

Show E

SymWord E

The SymWord instance for E. In GHC 7.10 and forward, we'll be able to add these to the deriving clause as well.

HasKind E

The HasKind instance for E. In GHC 7.10 and forward, we'll be able to add these to the deriving clause as well.

SatModel E

The SatModel instance for E. In GHC 7.10 and forward, we'll be able to add these to the deriving clause as well. Note that the SatModel instance is only needed if you use getModel and its friends; but it does not hurt to always derive the default definitions.

Typeable * E

type SE = SBV E

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

elts :: IO AllSatResult

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.

four :: IO SatResult

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

maxE :: IO SatResult

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

minE :: IO SatResult

Similarly, we get the minumum element. We have:

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