    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Documentation.SBV.Examples.Queries.GuessNumber
    -- Copyright   :  (c) Levent Erkok
    -- License     :  BSD3
    -- Maintainer  :  erkokl@gmail.com
    -- Stability   :  experimental
    --
    -- A simple number-guessing game implementation via queries. Clearly an
    -- SMT solver is hardly needed for this problem, but it is a nice demo
    -- for the interactive-query programming.
    -----------------------------------------------------------------------------

    module Documentation.SBV.Examples.Queries.GuessNumber where

    import Data.SBV
    import Data.SBV.Control

    -- | Use the backend solver to guess the number given as argument.
    -- The number is assumed to be between @0@ and @1000@, and we use a simple
    -- binary search. Returns the sequence of guesses we performed during
    -- the search process.
    guess :: Integer -> Symbolic [Integer]
    guess input = do g <- sInteger "guess"

                     -- A simple loop to find the value in a query. lb and up
                     -- correspond to the current lower/upper bound we operate in.
                     let loop lb ub sofar = do

                              io $ putStrLn $ "Current bounds: " ++ show (lb, ub)

                              -- Assert the current bound:
                              constrain $ g .>= literal lb
                              constrain $ g .<= literal ub

                              -- Issue a check-sat
                              cs <- checkSat
                              case cs of
                                Unk   -> error "Too bad, solver said Unknown.." -- Won't really happen
                                Unsat ->
                                      -- This cannot happen! If it does, the input was
                                      -- not properly constrainted. Note that we found this
                                      -- by getting an Unsat, not by checking the value!
                                      error $ unlines [ "There's no solution!"
                                                      , "Guess sequence: " ++ show (reverse sofar)
                                                      ]
                                Sat   -> do gv <- getValue g
                                            case gv `compare` input of
                                              EQ -> -- Got it, return:
                                                    return (reverse (gv : sofar))
                                              LT -> -- Solver guess is too small, increase the lower bound:
                                                    loop ((lb+1) `max` (lb + (input - lb) `div` 2)) ub (gv : sofar)
                                              GT -> -- Solver guess is too big, decrease the upper bound:
                                                    loop lb ((ub-1) `min` (ub - (ub - input) `div` 2)) (gv : sofar)

                     -- Start the search
                     query $ loop 0 1000 []

    -- | Play a round of the game, making the solver guess the secret number 42.
    -- Note that you can generate a random-number and make the solver guess it too!
    -- We have:
    --
    -- >>> play
    -- Current bounds: (0,1000)
    -- Current bounds: (0,521)
    -- Current bounds: (21,521)
    -- Current bounds: (31,521)
    -- Current bounds: (36,521)
    -- Current bounds: (39,521)
    -- Current bounds: (40,521)
    -- Current bounds: (41,521)
    -- Current bounds: (42,521)
    -- Solved in: 9 guesses:
    --   1000 0 21 31 36 39 40 41 42
    play :: IO ()
    play = do gs <- runSMT (guess 42)
              putStrLn $ "Solved in: " ++ show (length gs) ++ " guesses:"
              putStrLn $ "  " ++ unwords (map show gs)