sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Documentation.SBV.Examples.Misc.Definitions

Contents

- Simple functions
- Basic recursive functions
- Mutual recursion
- Nested recursion

Description

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

Synopsis

- add1 :: SInteger -> SInteger
- add1Example :: IO SatResult
- sumToN :: SInteger -> SInteger
- sumToNExample :: IO SatResult
- len :: SList Integer -> SInteger
- lenExample :: IO SatResult
- pingPong :: IO SatResult
- evenOdd :: IO SatResult
- isEvenOdd :: SInteger -> STuple Bool Bool
- isEven :: SInteger -> SBool
- isOdd :: SInteger -> SBool
- evenOdd2 :: IO SatResult
- ack :: SInteger -> SInteger -> SInteger
- ack1y :: IO SatResult

# Simple functions

add1 :: SInteger -> SInteger Source #

Add one to an argument

add1Example :: IO SatResult Source #

Reverse run the add1 function. Note that the generated SMTLib will have the function add1 itself defined. You can verify this by running the below in verbose mode.

    >>> add1Example
    Satisfiable. Model:
      x = 4 :: Integer

# Basic recursive functions

sumToN :: SInteger -> SInteger Source #

Sum of numbers from 0 to the given number. Since this is a recursive definition, we cannot simply symbolically simulate it as it wouldn't terminat. So, we use the function generation facilities to define it directly in SMTLib. Note how the function itself takes a "recursive version" of itself, and all recursive calls are made with this name.

sumToNExample :: IO SatResult Source #

Prove that sumToN works as expected.

We have:

    >>> sumToNExample
    Satisfiable. Model:
      s0 =  5 :: Integer
      s1 = 15 :: Integer

len :: SList Integer -> SInteger Source #

Coding list-length recursively. Again, we map directly to an SMTLib function.

lenExample :: IO SatResult Source #

Calculate the length of a list, using recursive functions.

We have:

    >>> lenExample
    Satisfiable. Model:
      s0 = [1,2,3] :: [Integer]
      s1 =       3 :: Integer

# Mutual recursion

pingPong :: IO SatResult Source #

A simple mutual-recursion example, from the z3 documentation. We have:

    >>> pingPong
    Satisfiable. Model:
      s0 = 1 :: Integer

evenOdd :: IO SatResult Source #

Usual way to define even-odd mutually recursively. Unfortunately, while this goes through, the backend solver does not terminate on this example. See `evenOdd2` for an alternative technique to handle such definitions, which seems to be more solver friendly.

isEvenOdd :: SInteger -> STuple Bool Bool Source #

Another technique to handle mutually definitions is to define the functions together, and pull the results out individually. This usually works better than defining the functions separately, from a solver perspective.

isEven :: SInteger -> SBool Source #

Extract the isEven function for easier use.

isOdd :: SInteger -> SBool Source #

Extract the isOdd function for easier use.

evenOdd2 :: IO SatResult Source #

We can prove 20 is even and definitely not odd, thusly:

    >>> evenOdd2
    Satisfiable. Model:
      s0 =    20 :: Integer
      s1 =  True :: Bool
      s2 = False :: Bool

# Nested recursion

ack :: SInteger -> SInteger -> SInteger Source #

Ackermann function, demonstrating nested recursion.

ack1y :: IO SatResult Source #

We can prove constant-folding instances of the equality `ack 1 y == y + 2`:

    >>> ack1y
    Satisfiable. Model:
      s0 = 5 :: Integer
      s1 = 7 :: Integer

Expecting the prover to handle the general case for arbitrary `y` is beyond the current scope of what SMT solvers do out-of-the-box for the time being.