    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Documentation.SBV.Examples.Queries.AllSat
    -- Copyright   :  (c) Levent Erkok
    -- License     :  BSD3
    -- Maintainer  :  erkokl@gmail.com
    -- Stability   :  experimental
    --
    -- 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 'Data.SBV.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.
    -----------------------------------------------------------------------------

    module Documentation.SBV.Examples.Queries.AllSat where

    import Data.SBV
    import Data.SBV.Control

    import Data.List

    -- | 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 at least twice as large as
    -- the previous one. This is rather silly, but demonstrates how we can dynamically
    -- query the result and put in new constraints based on those.
    goodSum :: Symbolic [(Integer, Integer)]
    goodSum = do x <- sInteger "x"
                 y <- sInteger "y"

                 -- constrain positive and sum:
                 constrain $ x .>= 0
                 constrain $ y .>= 0
                 constrain $ x + y .== 10

                 -- Capture the "next" solution function:
                 let next i sofar = do
                        io $ putStrLn $ "Iteration: " ++ show (i :: Int)

                        cs <- checkSat
                        case cs of
                          Unk   -> error "Too bad, solver said unknown.." -- Won't happen
                          Unsat -> do io $ putStrLn "No other solution!"
                                      return sofar

                          Sat   -> do xv <- getValue x
                                      yv <- getValue y

                                      io $ putStrLn $ "Current solution is: " ++ show (xv, yv)

                                      -- For next iteration: Put in constraints outlawing the current one:
                                      -- Note that we do *not* put these separately, as we do want
                                      -- to allow repetition on one value if the other is different!
                                      constrain $   x ./= literal xv
                                                ||| y ./= literal yv

                                      -- Also request @x@ to be twice as large, for demo purposes:
                                      constrain $ x .>= 2 * literal xv

                                      -- loop around!
                                      next (i+1) ((xv, yv) : sofar)

                 -- Go into query mode and execute the loop:
                 query $ do io $ putStrLn "Starting the all-sat engine!"
                            next 1 []

    -- | 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: (4,6)
    -- Iteration: 5
    -- Current solution is: (8,2)
    -- Iteration: 6
    -- No other solution!
    -- [(0,10),(1,9),(2,8),(4,6),(8,2)]
    demo :: IO ()
    demo = do ss <- runSMT goodSum
              print $ sort ss