1-----------------------------------------------------------------------------
2-- |
3-- Module    : Documentation.SBV.Examples.Queries.GuessNumber
4-- Copyright : (c) Levent Erkok
5-- License   : BSD3
6-- Maintainer: erkokl@gmail.com
7-- Stability : experimental
8--
9-- A simple number-guessing game implementation via queries. Clearly an
10-- SMT solver is hardly needed for this problem, but it is a nice demo
11-- for the interactive-query programming.
12-----------------------------------------------------------------------------
13
14{-# OPTIONS_GHC -Wall -Werror #-}
15
16module Documentation.SBV.Examples.Queries.GuessNumber where
17
18import Data.SBV
19import Data.SBV.Control
20
21-- | Use the backend solver to guess the number given as argument.
22-- The number is assumed to be between @0@ and @1000@, and we use a simple
23-- binary search. Returns the sequence of guesses we performed during
24-- the search process.
25guess :: Integer -> Symbolic [Integer]
26guess input = do g <- sInteger "guess"
27
28                 -- A simple loop to find the value in a query. lb and up
29                 -- correspond to the current lower/upper bound we operate in.
30                 let loop lb ub sofar = do
31
32                          io $ putStrLn $ "Current bounds: " ++ show (lb, ub)
33
34                          -- Assert the current bound:
35                          constrain $ g .>= literal lb
36                          constrain $ g .<= literal ub
37
38                          -- Issue a check-sat
39                          cs <- checkSat
40                          case cs of
41                            Unk    -> error "Too bad, solver said Unknown.." -- Won't really happen
42                            DSat{} -> error "Unexpected delta-sat result.."  -- Won't really happen
43                            Unsat  ->
44                                   -- This cannot happen! If it does, the input was
45                                   -- not properly constrainted. Note that we found this
46                                   -- by getting an Unsat, not by checking the value!
47                                   error $ unlines [ "There's no solution!"
48                                                   , "Guess sequence: " ++ show (reverse sofar)
49                                                   ]
50                            Sat    -> do gv <- getValue g
51                                         case gv `compare` input of
52                                           EQ -> -- Got it, return:
53                                                 return (reverse (gv : sofar))
54                                           LT -> -- Solver guess is too small, increase the lower bound:
55                                                 loop ((lb+1) `max` (lb + (input - lb) `div` 2)) ub (gv : sofar)
56                                           GT -> -- Solver guess is too big, decrease the upper bound:
57                                                 loop lb ((ub-1) `min` (ub - (ub - input) `div` 2)) (gv : sofar)
58
59                 -- Start the search
60                 query $ loop 0 1000 []
61
62-- | Play a round of the game, making the solver guess the secret number 42.
63-- Note that you can generate a random-number and make the solver guess it too!
64-- We have:
65--
66-- >>> play
67-- Current bounds: (0,1000)
68-- Current bounds: (0,521)
69-- Current bounds: (21,521)
70-- Current bounds: (31,521)
71-- Current bounds: (36,521)
72-- Current bounds: (39,521)
73-- Current bounds: (40,521)
74-- Current bounds: (41,521)
75-- Current bounds: (42,521)
76-- Solved in: 9 guesses:
77--   776 0 21 31 36 39 40 41 42
78play :: IO ()
79play = do gs <- runSMT (guess 42)
80          putStrLn $ "Solved in: " ++ show (length gs) ++ " guesses:"
81          putStrLn $ "  " ++ unwords (map show gs)
82