    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Data.SBV.Examples.Puzzles.Birthday
    -- Copyright   :  (c) Levent Erkok
    -- License     :  BSD3
    -- Maintainer  :  erkokl@gmail.com
    -- Stability   :  experimental
    --
    -- This is a formalization of the Cheryl's birtday problem, which went viral in April 2015.
    -- (See <http://www.nytimes.com/2015/04/15/science/a-math-problem-from-singapore-goes-viral-when-is-cheryls-birthday.html>.)
    --
    -- Here's the puzzle:
    --
    -- @
    -- Albert and Bernard just met Cheryl. “When’s your birthday?” Albert asked Cheryl.
    --
    -- Cheryl thought a second and said, “I’m not going to tell you, but I’ll give you some clues.” She wrote down a list of 10 dates:
    --
    --   May 15, May 16, May 19
    --   June 17, June 18
    --   July 14, July 16
    --   August 14, August 15, August 17
    --
    -- “My birthday is one of these,” she said.
    --
    -- Then Cheryl whispered in Albert’s ear the month — and only the month — of her birthday. To Bernard, she whispered the day, and only the day.
    -- “Can you figure it out now?” she asked Albert.
    --
    -- Albert: I don’t know when your birthday is, but I know Bernard doesn’t know, either.
    -- Bernard: I didn’t know originally, but now I do.
    -- Albert: Well, now I know, too!
    --
    -- When is Cheryl’s birthday?
    -- @
    --
    -- NB. Thanks to Amit Goel for suggesting the formalization strategy used in here.
    -----------------------------------------------------------------------------

    module Data.SBV.Examples.Puzzles.Birthday where

    import Data.SBV

    -----------------------------------------------------------------------------------------------
    -- * Types and values
    -----------------------------------------------------------------------------------------------

    -- | Represent month by 8-bit words; We can also use an uninterpreted type, but numbers work well here.
    type Month = SWord8

    -- | Represent day by 8-bit words; Again, an uninterpreted type would work as well.
    type Day = SWord8

    -- | Months referenced in the problem.
    may, june, july, august :: SWord8
    [may, june, july, august] = [5, 6, 7, 8]

    -----------------------------------------------------------------------------------------------
    -- * Helper predicates
    -----------------------------------------------------------------------------------------------

    -- | Check that a given month/day combo is a possible birth-date.
    valid :: Month -> Day -> SBool
    valid month day = (month, day) `sElem` candidates
      where candidates :: [(Month, Day)]
            candidates = [ (   may, 15), (   may, 16), (   may, 19)
                         , (  june, 17), (  june, 18)
                         , (  july, 14), (  july, 16)
                         , (august, 14), (august, 15), (august, 17)
                         ]

    -- | Assert that the given function holds for one of the possible days.
    existsDay :: (Day -> SBool) -> SBool
    existsDay f = bAny (f . literal) [14 .. 19]

    -- | Assert that the given function holds for all of the possible days.
    forallDay :: (Day -> SBool) -> SBool
    forallDay f = bAll (f . literal) [14 .. 19]

    -- | Assert that the given function holds for one of the possible months.
    existsMonth :: (Month -> SBool) -> SBool
    existsMonth f = bAny f [may .. august]

    -- | Assert that the given function holds for all of the possible months.
    forallMonth :: (Month -> SBool) -> SBool
    forallMonth f = bAll f [may .. august]

    -----------------------------------------------------------------------------------------------
    -- * The puzzle
    -----------------------------------------------------------------------------------------------

    -- | Encode the conversation as given in the puzzle.
    --
    -- NB. Lee Pike pointed out that not all the constraints are actually necessary! (Private
    -- communication.) The puzzle still has a unique solution if the statements 'a1' and 'b1'
    -- (i.e., Albert and Bernard saying they themselves do not know the answer) are removed.
    -- To experiment you can simply comment out those statements and observe that there still
    -- is a unique solution. Thanks to Lee for pointing this out! In fact, it is instructive to
    -- assert the conversation line-by-line, and see how the search-space gets reduced in each
    -- step.
    puzzle :: Predicate
    puzzle = do birthDay   <- exists "birthDay"
                birthMonth <- exists "birthMonth"

                -- Albert: I do not know
                let a1 m = existsDay $ \d1 -> existsDay $ \d2 ->
                               d1 ./= d2 &&& valid m d1 &&& valid m d2

                -- Albert: I know that Bernard doesn't know
                let a2 m = forallDay $ \d -> valid m d ==>
                              existsMonth (\m1 -> existsMonth $ \m2 ->
                                    m1 ./= m2 &&& valid m1 d &&& valid m2 d)

                -- Bernard: I did not know
                let b1 d = existsMonth $ \m1 -> existsMonth $ \m2 ->
                               m1 ./= m2 &&& valid m1 d &&& valid m2 d

                -- Bernard: But now I know
                let b2p m d = valid m d &&& a1 m &&& a2 m
                    b2  d   = forallMonth $ \m1 -> forallMonth $ \m2 ->
                                    (b2p m1 d &&& b2p m2 d) ==> m1 .== m2

                -- Albert: Now I know too
                let a3p m d = valid m d &&& a1 m &&& a2 m &&& b1 d &&& b2 d
                    a3 m    = forallDay $ \d1 -> forallDay $ \d2 ->
                                    (a3p m d1 &&& a3p m d2) ==> d1 .== d2

                -- Assert all the statements made:
                constrain $ a1 birthMonth
                constrain $ a2 birthMonth
                constrain $ b1 birthDay
                constrain $ b2 birthDay
                constrain $ a3 birthMonth

                -- Find a valid birth-day that satisfies the above constraints:
                return $ valid birthMonth birthDay

    -- | Find all solutions to the birthday problem. We have:
    --
    -- >>> cheryl
    -- Solution #1:
    --   birthDay   = 16 :: Word8
    --   birthMonth =  7 :: Word8
    -- This is the only solution.
    cheryl :: IO ()
    cheryl = print =<< allSat puzzle