Copyright | (c) Levent Erkok |
---|---|
License | BSD3 |
Maintainer | erkokl@gmail.com |
Stability | experimental |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Documentation.SBV.Examples.Uninterpreted.UISortAllSat
Description
Demonstrates uninterpreted sorts and how all-sat behaves for them. Thanks to Eric Seidel for the idea.
Documentation
A "list-like" data type, but one we plan to uninterpret at the SMT level. The actual shape is really immaterial for us.
Instances
classify :: SL -> SInteger Source #
An uninterpreted "classify" function. Really, we only care about the fact that such a function exists, not what it does.
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:
>>>
allSat genLs
Solution #1: l = L!val!2 :: L l0 = L!val!0 :: L l1 = L!val!1 :: L l2 = L!val!2 :: L classify :: L -> Integer classify L!val!2 = 2 classify L!val!1 = 1 classify _ = 0 Solution #2: l = L!val!1 :: L l0 = L!val!0 :: L l1 = L!val!1 :: L l2 = L!val!2 :: L classify :: L -> Integer classify L!val!2 = 2 classify L!val!1 = 1 classify _ = 0 Solution #3: l = L!val!0 :: L l0 = L!val!0 :: L l1 = L!val!1 :: L l2 = L!val!2 :: L classify :: L -> Integer classify L!val!2 = 2 classify L!val!1 = 1 classify _ = 0 Found 3 different solutions.