    -----------------------------------------------------------------------------
    -- |
    -- 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

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

                              -- Assert the current bound:
                              SBool -> Query ()
    forall a. QuantifiedBool a => a -> Query ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> Query ()) -> SBool -> Query ()
    forall a b. (a -> b) -> a -> b
    $ SInteger
    g SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= Integer -> SInteger
    forall a. SymVal a => a -> SBV a
    literal Integer
    lb
                              SBool -> Query ()
    forall a. QuantifiedBool a => a -> Query ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> Query ()) -> SBool -> Query ()
    forall a b. (a -> b) -> a -> b
    $ SInteger
    g SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .<= Integer -> SInteger
    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    -> String -> QueryT IO [Integer]
    forall a. HasCallStack => String -> a
    error String
    "Too bad, solver said Unknown.." -- Won't really happen
                                DSat{} -> String -> QueryT IO [Integer]
    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!
                                       String -> QueryT IO [Integer]
    forall a. HasCallStack => String -> a
    error (String -> QueryT IO [Integer]) -> String -> QueryT IO [Integer]
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ String
    "There's no solution!"
                                                       , String
    "Guess sequence: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [Integer] -> String
    forall a. Show a => a -> String
    show ([Integer] -> [Integer]
    forall a. [a] -> [a]
    reverse [Integer]
    sofar)
                                                       ]
                                CheckSatResult
    Sat    -> do Integer
    gv <- SInteger -> Query Integer
    forall a. SymVal a => SBV a -> Query a
    getValue SInteger
    g
                                             case Integer
    gv Integer -> Integer -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare` Integer
    input of
                                               Ordering
    EQ -> -- Got it, return:
                                                     [Integer] -> QueryT IO [Integer]
    forall a. a -> QueryT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Integer] -> [Integer]
    forall a. [a] -> [a]
    reverse (Integer
    gv Integer -> [Integer] -> [Integer]
    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
    lbInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    1) Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    `max` (Integer
    lb Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + (Integer
    input Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    lb) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer
    2)) Integer
    ub (Integer
    gv Integer -> [Integer] -> [Integer]
    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
    ubInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1) Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    `min` (Integer
    ub Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - (Integer
    ub Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    input) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer
    2)) (Integer
    gv Integer -> [Integer] -> [Integer]
    forall a. a -> [a] -> [a]
    : [Integer]
    sofar)

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