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

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

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

- guess :: Integer -> Symbolic [Integer]
- play :: IO ()

# 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