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

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.

Constructors

Q

Instances

Eq Q
Data Q
Ord Q
SymWord Q	We need `SymWord` and `HasKind` instances, but default definitions are always sufficient for uninterpreted sorts, so all we do is to declare them as such. Note that, starting with GHC 7.6.1, we will be able to simply derive these classes as well. (See http://hackage.haskell.org/trac/ghc/ticket/5462.)
HasKind Q	`HasKind` instance is again straightforward, no specific implementation needed.
Typeable * Q

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