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.Sort

Description

Demonstrates uninterpreted sorts, together with axioms.

Synopsis

- data Q = Q ()
- f :: SBV Q -> SBV Q
- t1 :: IO SatResult
- t2 :: IO SatResult

# Documentation

data Q Source

A new data-type that we expect to use in an uninterpreted fashion in the backend SMT solver. Note the custom `deriving` clause, which takes care of most of the boilerplate. The () field is needed so SBV will not translate it to an enumerated data-type

Constructors

Q () |

Instances

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

f :: SBV Q -> SBV Q Source

Declare an uninterpreted function that works over Q's

t1 :: IO SatResult Source

A satisfiable example, stating that there is an element of the domain `Q` such that `f` returns a different element. Note that this is valid only when the domain `Q` has at least two elements. We have:

    >>> t1
    Satisfiable. Model:
      x = Q!val!0 :: Q

t2 :: IO SatResult Source

This is a variant on the first example, except we also add an axiom for the sort, stating that the domain `Q` has only one element. In this case the problem naturally becomes unsat. We have:

    >>> t2
    Unsatisfiable