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.Uninterpreted.UISortAllSat

Description

Demonstrates uninterpreted sorts and how all-sat behaves for them. Thanks to Eric Seidel for the idea.

Synopsis

- data L
  - = Nil
  - | Cons Int L
- classify :: SBV L -> SInteger
- genLs :: IO AllSatResult

# Documentation

data L Source

A "list-like" data type, but one we plan to uninterpret at the SMT level. The actual shape is really immaterial for us, but could be used as a proxy to generate test cases or explore data-space in some other part of a program. Note that we neither rely on the shape of this data, nor need the actual constructors.

Constructors

Nil |
Cons Int L |

Instances

Eq L Source |
Data L Source |
Ord L Source |
Read L Source |
Show L Source |
HasKind L Source | Similarly, `HasKind`s default implementation is sufficient.
SymWord L Source | Declare instances to make `L` a usable uninterpreted sort. First we need the `SymWord` instance, with the default definition sufficing.

classify :: SBV L -> SInteger Source

An uninterpreted "classify" function. Really, we only care about the fact that such a function exists, not what it does.

genLs :: IO AllSatResult Source

Formulate a query that essentially asserts a cardinality constraint on the uninterpreted sort `L`. The goal is to say there are precisely 3 such things, as it might be the case. We manage this by declaring four elements, and asserting that for a free variable of this sort, the shape of the data matches one of these three instances. That is, we assert that all the instances of the data `L` can be classified into 3 equivalence classes. Then, allSat returns all the possible instances, which of course are all uninterpreted.

As expected, we have:

    >>> genLs
    Solution #1:
      l  = L!val!0 :: L
      l0 = L!val!0 :: L
      l1 = L!val!1 :: L
      l2 = L!val!2 :: L
    Solution #2:
      l  = L!val!2 :: L
      l0 = L!val!0 :: L
      l1 = L!val!1 :: L
      l2 = L!val!2 :: L
    Solution #3:
      l  = L!val!1 :: L
      l0 = L!val!0 :: L
      l1 = L!val!1 :: L
      l2 = L!val!2 :: L
    Found 3 different solutions.