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

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

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

- data E
  - = A
  - | B
  - | C
- type SE = SBV E
- elts :: IO AllSatResult
- four :: IO SatResult
- maxE :: IO SatResult
- minE :: IO SatResult

# 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

Eq E Source |
Data E Source |
Ord E Source |
Read E Source |
Show E Source |
HasKind E Source |
SymWord E Source |

type SE = SBV E Source

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

elts :: IO AllSatResult Source

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 Source

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 Source

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 Source

Similarly, we get the minumum element. We have:

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