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

    {-# LANGUAGE DeriveAnyClass      #-}
    {-# LANGUAGE DeriveDataTypeable  #-}
    {-# LANGUAGE StandaloneDeriving  #-}
    {-# LANGUAGE TemplateHaskell     #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Puzzles.Birthday where

    import Data.SBV

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

    -- | Months. We only put in the months involved in the puzzle for simplicity
    data Month = May | Jun | Jul | Aug

    -- | Days. Again, only the ones mentioned in the puzzle.
    data Day = D14 | D15 | D16 | D17 | D18 | D19

    mkSymbolicEnumeration ''Month
    mkSymbolicEnumeration ''Day

    -- | Represent the birthday as a record
    data Birthday = BD SMonth SDay

    -- | Make a valid symbolic birthday
    mkBirthday :: Symbolic Birthday
    mkBirthday :: Symbolic Birthday
    mkBirthday = do Birthday
    b <- SMonth -> SDay -> Birthday
    BD (SMonth -> SDay -> Birthday)
    -> SymbolicT IO SMonth -> SymbolicT IO (SDay -> Birthday)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> SymbolicT IO SMonth
    forall a. SymVal a => String -> Symbolic (SBV a)
    free String
    "birthMonth" SymbolicT IO (SDay -> Birthday)
    -> SymbolicT IO SDay -> Symbolic Birthday
    forall a b.
    SymbolicT IO (a -> b) -> SymbolicT IO a -> SymbolicT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> String -> SymbolicT IO SDay
    forall a. SymVal a => String -> Symbolic (SBV a)
    free String
    "birthDay"
                    SBool -> ConstraintSet
    forall a. QuantifiedBool a => a -> ConstraintSet
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
    forall a b. (a -> b) -> a -> b
    $ Birthday -> SBool
    valid Birthday
    b
                    Birthday -> Symbolic Birthday
    forall a. a -> SymbolicT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Birthday
    b

    -- | Is this a valid birthday? i.e., one that was declared by Cheryl to be a possibility.
    valid :: Birthday -> SBool
    valid :: Birthday -> SBool
    valid (BD SMonth
    m SDay
    d) =   (SMonth
    m SMonth -> SMonth -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SMonth
    sMay SBool -> SBool -> SBool
    .=> SDay
    d SDay -> [SDay] -> SBool
    forall a. EqSymbolic a => a -> [a] -> SBool
    `sElem` [SDay
    sD15, SDay
    sD16, SDay
    sD19])
                   SBool -> SBool -> SBool
    .&& (SMonth
    m SMonth -> SMonth -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SMonth
    sJun SBool -> SBool -> SBool
    .=> SDay
    d SDay -> [SDay] -> SBool
    forall a. EqSymbolic a => a -> [a] -> SBool
    `sElem` [SDay
    sD17, SDay
    sD18])
                   SBool -> SBool -> SBool
    .&& (SMonth
    m SMonth -> SMonth -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SMonth
    sJul SBool -> SBool -> SBool
    .=> SDay
    d SDay -> [SDay] -> SBool
    forall a. EqSymbolic a => a -> [a] -> SBool
    `sElem` [SDay
    sD14, SDay
    sD16])
                   SBool -> SBool -> SBool
    .&& (SMonth
    m SMonth -> SMonth -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SMonth
    sAug SBool -> SBool -> SBool
    .=> SDay
    d SDay -> [SDay] -> SBool
    forall a. EqSymbolic a => a -> [a] -> SBool
    `sElem` [SDay
    sD14, SDay
    sD15, SDay
    sD17])

    -----------------------------------------------------------------------------------------------
    -- * 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 :: ConstraintSet
    puzzle :: ConstraintSet
    puzzle = do BD SMonth
    birthMonth SDay
    birthDay <- Symbolic Birthday
    mkBirthday

                let ok :: [Birthday] -> SBool
    ok    = (Birthday -> SBool) -> [Birthday] -> SBool
    forall a. (a -> SBool) -> [a] -> SBool
    sAll Birthday -> SBool
    valid
                    qe :: a -> SBool
    qe a
    qb = a -> SBool
    forall a. QuantifiedBool a => a -> SBool
    quantifiedBool a
    qb

                -- Albert: I do not know
                let a1 :: SMonth -> SBool
    a1 SMonth
    m = (Exists Any Day -> Exists Any Day -> SBool) -> SBool
    forall a. QuantifiedBool a => a -> SBool
    qe ((Exists Any Day -> Exists Any Day -> SBool) -> SBool)
    -> (Exists Any Day -> Exists Any Day -> SBool) -> SBool
    forall a b. (a -> b) -> a -> b
    $ \(Exists SDay
    d1) (Exists SDay
    d2) -> [Birthday] -> SBool
    ok [SMonth -> SDay -> Birthday
    BD SMonth
    m SDay
    d1, SMonth -> SDay -> Birthday
    BD SMonth
    m SDay
    d2] SBool -> SBool -> SBool
    .&& SDay
    d1 SDay -> SDay -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    ./= SDay
    d2
                SBool -> ConstraintSet
    forall a. QuantifiedBool a => a -> ConstraintSet
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
    forall a b. (a -> b) -> a -> b
    $ SMonth -> SBool
    a1 SMonth
    birthMonth

                -- Albert: I know that Bernard doesn't know
                let a2 :: SMonth -> SBool
    a2 SMonth
    m = (Forall Any Day -> SBool) -> SBool
    forall a. QuantifiedBool a => a -> SBool
    qe ((Forall Any Day -> SBool) -> SBool)
    -> (Forall Any Day -> SBool) -> SBool
    forall a b. (a -> b) -> a -> b
    $ \(Forall SDay
    d) -> [Birthday] -> SBool
    ok [SMonth -> SDay -> Birthday
    BD SMonth
    m SDay
    d] SBool -> SBool -> SBool
    .=> (Exists Any Month -> Exists Any Month -> SBool) -> SBool
    forall a. QuantifiedBool a => a -> SBool
    qe (\(Exists SMonth
    m1) (Exists SMonth
    m2) -> [Birthday] -> SBool
    ok [SMonth -> SDay -> Birthday
    BD SMonth
    m1 SDay
    d, SMonth -> SDay -> Birthday
    BD SMonth
    m2 SDay
    d] SBool -> SBool -> SBool
    .&& SMonth
    m1 SMonth -> SMonth -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    ./= SMonth
    m2)
                SBool -> ConstraintSet
    forall a. QuantifiedBool a => a -> ConstraintSet
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
    forall a b. (a -> b) -> a -> b
    $ SMonth -> SBool
    a2 SMonth
    birthMonth

                -- Bernard: I did not know
                let b1 :: SDay -> SBool
    b1 SDay
    d = (Exists Any Month -> Exists Any Month -> SBool) -> SBool
    forall a. QuantifiedBool a => a -> SBool
    qe ((Exists Any Month -> Exists Any Month -> SBool) -> SBool)
    -> (Exists Any Month -> Exists Any Month -> SBool) -> SBool
    forall a b. (a -> b) -> a -> b
    $ \(Exists SMonth
    m1) (Exists SMonth
    m2) -> [Birthday] -> SBool
    ok [SMonth -> SDay -> Birthday
    BD SMonth
    m1 SDay
    d, SMonth -> SDay -> Birthday
    BD SMonth
    m2 SDay
    d] SBool -> SBool -> SBool
    .&& SMonth
    m1 SMonth -> SMonth -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    ./= SMonth
    m2
                SBool -> ConstraintSet
    forall a. QuantifiedBool a => a -> ConstraintSet
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
    forall a b. (a -> b) -> a -> b
    $ SDay -> SBool
    b1 SDay
    birthDay

                -- Bernard: But now I know
                let b2p :: SMonth -> SDay -> SBool
    b2p SMonth
    m SDay
    d = [Birthday] -> SBool
    ok [SMonth -> SDay -> Birthday
    BD SMonth
    m SDay
    d] SBool -> SBool -> SBool
    .&& SMonth -> SBool
    a1 SMonth
    m SBool -> SBool -> SBool
    .&& SMonth -> SBool
    a2 SMonth
    m
                    b2 :: SDay -> SBool
    b2  SDay
    d   = (Forall Any Month -> Forall Any Month -> SBool) -> SBool
    forall a. QuantifiedBool a => a -> SBool
    qe ((Forall Any Month -> Forall Any Month -> SBool) -> SBool)
    -> (Forall Any Month -> Forall Any Month -> SBool) -> SBool
    forall a b. (a -> b) -> a -> b
    $ \(Forall SMonth
    m1) (Forall SMonth
    m2) -> (SMonth -> SDay -> SBool
    b2p SMonth
    m1 SDay
    d SBool -> SBool -> SBool
    .&& SMonth -> SDay -> SBool
    b2p SMonth
    m2 SDay
    d) SBool -> SBool -> SBool
    .=> SMonth
    m1 SMonth -> SMonth -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SMonth
    m2
                SBool -> ConstraintSet
    forall a. QuantifiedBool a => a -> ConstraintSet
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
    forall a b. (a -> b) -> a -> b
    $ SDay -> SBool
    b2 SDay
    birthDay

                -- Albert: Now I know too
                let a3p :: SMonth -> SDay -> SBool
    a3p SMonth
    m SDay
    d = [Birthday] -> SBool
    ok [SMonth -> SDay -> Birthday
    BD SMonth
    m SDay
    d] SBool -> SBool -> SBool
    .&& SMonth -> SBool
    a1 SMonth
    m SBool -> SBool -> SBool
    .&& SMonth -> SBool
    a2 SMonth
    m SBool -> SBool -> SBool
    .&& SDay -> SBool
    b1 SDay
    d SBool -> SBool -> SBool
    .&& SDay -> SBool
    b2 SDay
    d
                    a3 :: SMonth -> Forall nm Day -> Forall nm Day -> SBool
    a3  SMonth
    m   = \(Forall SDay
    d1) (Forall SDay
    d2) -> (SMonth -> SDay -> SBool
    a3p SMonth
    m SDay
    d1 SBool -> SBool -> SBool
    .&& SMonth -> SDay -> SBool
    a3p SMonth
    m SDay
    d2) SBool -> SBool -> SBool
    .=> SDay
    d1 SDay -> SDay -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SDay
    d2
                (Forall Any Day -> Forall Any Day -> SBool) -> ConstraintSet
    forall a. QuantifiedBool a => a -> ConstraintSet
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain ((Forall Any Day -> Forall Any Day -> SBool) -> ConstraintSet)
    -> (Forall Any Day -> Forall Any Day -> SBool) -> ConstraintSet
    forall a b. (a -> b) -> a -> b
    $ SMonth -> Forall Any Day -> Forall Any Day -> SBool
    forall {nm :: Symbol} {nm :: Symbol}.
    SMonth -> Forall nm Day -> Forall nm Day -> SBool
    a3 SMonth
    birthMonth

    -- | Find all solutions to the birthday problem. We have:
    --
    -- >>> cheryl
    -- Solution #1:
    --   birthMonth = Jul :: Month
    --   birthDay   = D16 :: Day
    -- 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
    =<< ConstraintSet -> IO AllSatResult
    forall a. Satisfiable a => a -> IO AllSatResult
    allSat ConstraintSet
    puzzle

    {- HLint ignore puzzle "Redundant lambda" -}
    {- HLint ignore puzzle "Eta reduce"       -}