Data.SBV.Examples.Uninterpreted.Function

Demonstrates function counter-examples

Documentation

f :: SWord8 -> SWord8 -> SWord16

An uninterpreted function

thmGood :: SWord8 -> SWord8 -> SWord8 -> SBool

Asserts that f x z == f (y+2) z whenever x == y+2. Naturally correct:

>>> prove thmGood
Q.E.D.

thmBad :: SWord8 -> SWord8 -> SBool

Asserts that f is commutative; which is not necessarily true! Indeed, the SMT solver returns a counter-example function that is not commutative. (Note that we have to use Yices as Z3 function counterexamples are not yet supported by sbv.) We have:

>>> proveWith yicesSMT09 $ forAll ["x", "y"] thmBad
Falsifiable. Counter-example:
  x = 0 :: Word8
  y = 128 :: Word8
  -- uninterpreted: f
       f 128 0 = 32768
       f _   _ = 0

Note how the counterexample function f returned by Yices violates commutativity; thus providing evidence that the asserted theorem is not valid.

yicesSMT09 :: SMTConfig

Old version of Yices, which supports nice output for uninterpreted functions.

Inspecting symbolic traces