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