Copyright | (c) Levent Erkok |
---|---|
License | BSD3 |
Maintainer | erkokl@gmail.com |
Stability | experimental |
Safe Haskell | None |
Language | Haskell2010 |
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.
Documentation
goodSum :: Symbolic [(Integer, Integer)] Source #
Find all solutions to x + y .== 10
for positive x
and y
.
This is rather silly to do in the query mode as allSat
can do
this automatically, but it demonstrates how we can dynamically
query the result and put in new constraints based on those.
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)]