-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Queries.GuessNumber
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- 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.
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Queries.GuessNumber where

import Data.SBV
import Data.SBV.Control

-- | 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.
guess :: Integer -> Symbolic [Integer]
guess :: Integer -> Symbolic [Integer]
guess Integer
input = do SInteger
g <- String -> Symbolic SInteger
sInteger String
"guess"

                 -- A simple loop to find the value in a query. lb and up
                 -- correspond to the current lower/upper bound we operate in.
                 let loop :: Integer -> Integer -> [Integer] -> QueryT IO [Integer]
loop Integer
lb Integer
ub [Integer]
sofar = do

                          forall a. IO a -> Query a
io forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Current bounds: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Integer
lb, Integer
ub)

                          -- Assert the current bound:
                          forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SInteger
g forall a. OrdSymbolic a => a -> a -> SBool
.>= forall a. SymVal a => a -> SBV a
literal Integer
lb
                          forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SInteger
g forall a. OrdSymbolic a => a -> a -> SBool
.<= forall a. SymVal a => a -> SBV a
literal Integer
ub

                          -- Issue a check-sat
                          CheckSatResult
cs <- Query CheckSatResult
checkSat
                          case CheckSatResult
cs of
                            CheckSatResult
Unk    -> forall a. HasCallStack => String -> a
error String
"Too bad, solver said Unknown.." -- Won't really happen
                            DSat{} -> forall a. HasCallStack => String -> a
error String
"Unexpected delta-sat result.."  -- Won't really happen
                            CheckSatResult
Unsat  ->
                                   -- This cannot happen! If it does, the input was
                                   -- not properly constrainted. Note that we found this
                                   -- by getting an Unsat, not by checking the value!
                                   forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"There's no solution!"
                                                   , String
"Guess sequence: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. [a] -> [a]
reverse [Integer]
sofar)
                                                   ]
                            CheckSatResult
Sat    -> do Integer
gv <- forall a. SymVal a => SBV a -> Query a
getValue SInteger
g
                                         case Integer
gv forall a. Ord a => a -> a -> Ordering
`compare` Integer
input of
                                           Ordering
EQ -> -- Got it, return:
                                                 forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. [a] -> [a]
reverse (Integer
gv forall a. a -> [a] -> [a]
: [Integer]
sofar))
                                           Ordering
LT -> -- Solver guess is too small, increase the lower bound:
                                                 Integer -> Integer -> [Integer] -> QueryT IO [Integer]
loop ((Integer
lbforall a. Num a => a -> a -> a
+Integer
1) forall a. Ord a => a -> a -> a
`max` (Integer
lb forall a. Num a => a -> a -> a
+ (Integer
input forall a. Num a => a -> a -> a
- Integer
lb) forall a. Integral a => a -> a -> a
`div` Integer
2)) Integer
ub (Integer
gv forall a. a -> [a] -> [a]
: [Integer]
sofar)
                                           Ordering
GT -> -- Solver guess is too big, decrease the upper bound:
                                                 Integer -> Integer -> [Integer] -> QueryT IO [Integer]
loop Integer
lb ((Integer
ubforall a. Num a => a -> a -> a
-Integer
1) forall a. Ord a => a -> a -> a
`min` (Integer
ub forall a. Num a => a -> a -> a
- (Integer
ub forall a. Num a => a -> a -> a
- Integer
input) forall a. Integral a => a -> a -> a
`div` Integer
2)) (Integer
gv forall a. a -> [a] -> [a]
: [Integer]
sofar)

                 -- Start the search
                 forall a. Query a -> Symbolic a
query forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> [Integer] -> QueryT IO [Integer]
loop Integer
0 Integer
1000 []

-- | 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: (21,1000)
-- Current bounds: (31,1000)
-- Current bounds: (36,1000)
-- Current bounds: (39,1000)
-- Current bounds: (40,1000)
-- Current bounds: (41,1000)
-- Current bounds: (42,1000)
-- Solved in: 8 guesses:
--   0 21 31 36 39 40 41 42
play :: IO ()
play :: IO ()
play = do [Integer]
gs <- forall a. Symbolic a -> IO a
runSMT (Integer -> Symbolic [Integer]
guess Integer
42)
          String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Solved in: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Integer]
gs) forall a. [a] -> [a] -> [a]
++ String
" guesses:"
          String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"  " forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [Integer]
gs)