Data.SBV.Examples.Queries.GuessNumber

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.

Documentation

guess :: Integer -> Symbolic [Integer]

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.

play :: IO ()

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