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:
>>>
elts
Solution #1: s0 = A :: E Solution #2: s0 = B :: E Solution #3: s0 = C :: E Found 3 different solutions.
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
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