-----------------------------------------------------------------------------
-- |
-- 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 -Wno-incomplete-uni-patterns #-}

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

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

-- | Check that a given month/day combo is a possible birth-date.
valid :: Month -> Day -> SBool
valid :: SWord8 -> SWord8 -> SBool
valid SWord8
month 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, SWord8
15), (   SWord8
may, SWord8
16), (   SWord8
may, SWord8
19)
                     , (  SWord8
june, SWord8
17), (  SWord8
june, SWord8
18)
                     , (  SWord8
july, SWord8
14), (  SWord8
july, SWord8
16)
                     , (SWord8
august, SWord8
14), (SWord8
august, SWord8
15), (SWord8
august, SWord8
17)
                     ]

-- | Assert that the given function holds for one of the possible days.
existsDay :: (Day -> SBool) -> SBool
existsDay :: (SWord8 -> SBool) -> SBool
existsDay 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) [Word8
14 .. Word8
19]

-- | Assert that the given function holds for all of the possible days.
forallDay :: (Day -> SBool) -> SBool
forallDay :: (SWord8 -> SBool) -> SBool
forallDay 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) [Word8
14 .. Word8
19]

-- | Assert that the given function holds for one of the possible months.
existsMonth :: (Month -> SBool) -> SBool
existsMonth :: (SWord8 -> SBool) -> SBool
existsMonth 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 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)
sbvExists String
"birthDay"
            SWord8
birthMonth <- String -> Symbolic SWord8
forall a. SymVal a => String -> Symbolic (SBV a)
sbvExists String
"birthMonth"

            -- Albert: I do not know
            let a1 :: SWord8 -> SBool
a1 SWord8
m = (SWord8 -> SBool) -> SBool
existsDay ((SWord8 -> SBool) -> SBool) -> (SWord8 -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \SWord8
d1 -> (SWord8 -> SBool) -> SBool
existsDay ((SWord8 -> SBool) -> SBool) -> (SWord8 -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \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 SWord8
m = (SWord8 -> SBool) -> SBool
forallDay ((SWord8 -> SBool) -> SBool) -> (SWord8 -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \SWord8
d -> SWord8 -> SWord8 -> SBool
valid SWord8
m SWord8
d SBool -> SBool -> SBool
.=>
                          (SWord8 -> SBool) -> SBool
existsMonth (\SWord8
m1 -> (SWord8 -> SBool) -> SBool
existsMonth ((SWord8 -> SBool) -> SBool) -> (SWord8 -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \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 SWord8
d = (SWord8 -> SBool) -> SBool
existsMonth ((SWord8 -> SBool) -> SBool) -> (SWord8 -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \SWord8
m1 -> (SWord8 -> SBool) -> SBool
existsMonth ((SWord8 -> SBool) -> SBool) -> (SWord8 -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \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 SWord8
m 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  SWord8
d   = (SWord8 -> SBool) -> SBool
forallMonth ((SWord8 -> SBool) -> SBool) -> (SWord8 -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \SWord8
m1 -> (SWord8 -> SBool) -> SBool
forallMonth ((SWord8 -> SBool) -> SBool) -> (SWord8 -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \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 SWord8
m 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 SWord8
m    = (SWord8 -> SBool) -> SBool
forallDay ((SWord8 -> SBool) -> SBool) -> (SWord8 -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \SWord8
d1 -> (SWord8 -> SBool) -> SBool
forallDay ((SWord8 -> SBool) -> SBool) -> (SWord8 -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \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