sbv-8.7: 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

Documentation.SBV.Examples.Queries.AllSat

Description

When we would like to find all solutions to a problem, we can query the solver repeatedly, telling it to give us a new model each time. SBV already provides `allSat` that precisely does this. However, this example demonstrates how the query mode can be used to achieve the same, and can also incorporate extra conditions with easy as we walk through solutions.

Synopsis

- goodSum :: Symbolic [(Integer, Integer)]
- demo :: IO ()

# Documentation

goodSum :: Symbolic [(Integer, Integer)] Source #

Find all solutions to `x + y .== 10` for positive `x` and `y`, but at each iteration we would like to ensure that the value of `x` we get is one more than the previous one. This is rather silly, but demonstrates how we can dynamically query the result and put in new constraints based on those.

demo :: IO () Source #

Run the query. We have:

    >>> demo
    Starting the all-sat engine!
    Iteration: 1
    Current solution is: (0,10)
    Iteration: 2
    Current solution is: (1,9)
    Iteration: 3
    Current solution is: (2,8)
    Iteration: 4
    Current solution is: (3,7)
    Iteration: 5
    Current solution is: (4,6)
    Iteration: 6
    Current solution is: (5,5)
    Iteration: 7
    Current solution is: (6,4)
    Iteration: 8
    Current solution is: (7,3)
    Iteration: 9
    Current solution is: (8,2)
    Iteration: 10
    Current solution is: (9,1)
    Iteration: 11
    Current solution is: (10,0)
    Iteration: 12
    No other solution!
    [(0,10),(1,9),(2,8),(3,7),(4,6),(5,5),(6,4),(7,3),(8,2),(9,1),(10,0)]