sbv-7.7: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.Queries.GuessNumber

Description

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.

Synopsis

Documentation

guess :: Integer -> Symbolic [Integer] Source #

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 () Source #

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