    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Puzzles.Birthday
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- This is a formalization of the Cheryl's birthday 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.
    -----------------------------------------------------------------------------

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.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 :: SWord8
    may, june :: SWord8
    june, july :: SWord8
    july, august :: SWord8
    august] = [5, 6, 7, 8]

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

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

    -- | Assert that the given function holds for one of the possible days.
    existsDay :: (Day -> SBool) -> SBool
    existsDay :: (SWord8 -> SBool) -> SBool
    existsDay f :: SWord8 -> SBool
    f = (Word8 -> SBool) -> [Word8] -> SBool
    forall a. (a -> SBool) -> [a] -> SBool
    sAny (SWord8 -> SBool
    f (SWord8 -> SBool) -> (Word8 -> SWord8) -> Word8 -> SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Word8 -> SWord8
    forall a. SymVal a => a -> SBV a
    literal) [14 .. 19]

    -- | Assert that the given function holds for all of the possible days.
    forallDay :: (Day -> SBool) -> SBool
    forallDay :: (SWord8 -> SBool) -> SBool
    forallDay f :: SWord8 -> SBool
    f = (Word8 -> SBool) -> [Word8] -> SBool
    forall a. (a -> SBool) -> [a] -> SBool
    sAll (SWord8 -> SBool
    f (SWord8 -> SBool) -> (Word8 -> SWord8) -> Word8 -> SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Word8 -> SWord8
    forall a. SymVal a => a -> SBV a
    literal) [14 .. 19]

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

    -- | Assert that the given function holds for all of the possible months.
    forallMonth :: (Month -> SBool) -> SBool
    forallMonth :: (SWord8 -> SBool) -> SBool
    forallMonth f :: SWord8 -> SBool
    f = (SWord8 -> SBool) -> [SWord8] -> SBool
    forall a. (a -> SBool) -> [a] -> SBool
    sAll SWord8 -> SBool
    f [SWord8
    may .. SWord8
    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 :: Predicate
    puzzle = do SWord8
    birthDay   <- String -> Symbolic SWord8
    forall a. SymVal a => String -> Symbolic (SBV a)
    exists "birthDay"
                SWord8
    birthMonth <- String -> Symbolic SWord8
    forall a. SymVal a => String -> Symbolic (SBV a)
    exists "birthMonth"

                -- Albert: I do not know
                let a1 :: SWord8 -> SBool
    a1 m :: SWord8
    m = (SWord8 -> SBool) -> SBool
    existsDay ((SWord8 -> SBool) -> SBool) -> (SWord8 -> SBool) -> SBool
    forall a b. (a -> b) -> a -> b
    $ \d1 :: SWord8
    d1 -> (SWord8 -> SBool) -> SBool
    existsDay ((SWord8 -> SBool) -> SBool) -> (SWord8 -> SBool) -> SBool
    forall a b. (a -> b) -> a -> b
    $ \d2 :: SWord8
    d2 ->
                               SWord8
    d1 SWord8 -> SWord8 -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    ./= SWord8
    d2 SBool -> SBool -> SBool
    .&& SWord8 -> SWord8 -> SBool
    valid SWord8
    m SWord8
    d1 SBool -> SBool -> SBool
    .&& SWord8 -> SWord8 -> SBool
    valid SWord8
    m SWord8
    d2

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

                -- Bernard: I did not know
                let b1 :: SWord8 -> SBool
    b1 d :: SWord8
    d = (SWord8 -> SBool) -> SBool
    existsMonth ((SWord8 -> SBool) -> SBool) -> (SWord8 -> SBool) -> SBool
    forall a b. (a -> b) -> a -> b
    $ \m1 :: SWord8
    m1 -> (SWord8 -> SBool) -> SBool
    existsMonth ((SWord8 -> SBool) -> SBool) -> (SWord8 -> SBool) -> SBool
    forall a b. (a -> b) -> a -> b
    $ \m2 :: SWord8
    m2 ->
                               SWord8
    m1 SWord8 -> SWord8 -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    ./= SWord8
    m2 SBool -> SBool -> SBool
    .&& SWord8 -> SWord8 -> SBool
    valid SWord8
    m1 SWord8
    d SBool -> SBool -> SBool
    .&& SWord8 -> SWord8 -> SBool
    valid SWord8
    m2 SWord8
    d

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

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

                -- Assert all the statements made:
                SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SWord8 -> SBool
    a1 SWord8
    birthMonth
                SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SWord8 -> SBool
    a2 SWord8
    birthMonth
                SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SWord8 -> SBool
    b1 SWord8
    birthDay
                SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SWord8 -> SBool
    b2 SWord8
    birthDay
                SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SWord8 -> SBool
    a3 SWord8
    birthMonth

                -- Find a valid birth-day that satisfies the above constraints:
                SBool -> Predicate
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SBool -> Predicate) -> SBool -> Predicate
    forall a b. (a -> b) -> a -> b
    $ SWord8 -> SWord8 -> SBool
    valid SWord8
    birthMonth SWord8
    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 :: IO ()
    cheryl = AllSatResult -> IO ()
    forall a. Show a => a -> IO ()
    print (AllSatResult -> IO ()) -> IO AllSatResult -> IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Predicate -> IO AllSatResult
    forall a. Provable a => a -> IO AllSatResult
    allSat Predicate
    puzzle