Documentation.SBV.Examples.Misc.Definitions

Demonstrates how we can add actual SMT-definitions for functions that cannot otherwise be defined in SBV. Typically, these are used for recursive definitions.

Documentation

sumToN :: SInteger -> SInteger

Sum of numbers from 0 to the given number. Note that this cannot be defined as a regular Haskell function, as it wouldn't terminate as it recurses on a symbolic argument.

defineSum :: Symbolic ()

Add the definition of sum to the SMT solver. Note that SBV performs no checks on your definition, neither that it is well formed, or even has the correct type!

badExample :: IO ThmResult

A simple proof using sumToN. We get a failure, because we haven't given the solver the definition, and thus it goes completely uninterpreted.

We have:

>>> badExample
Falsifiable. Counter-example:
  sumToN :: Integer -> Integer
  sumToN _ = 0

Since sumToN remains uninterpreted, the solver gave us a model that obviously fails the property.

goodExample :: IO ThmResult

Same example, except this time we give the solver the definition of the function, and thus the proof goes through.

We have:

>>> goodExample
Q.E.D.

In this case, the solver has the definition, and proves the predicate as expected.