-----------------------------------------------------------------------------
-- |
-- 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.
--
-- 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 FlexibleInstances #-}
{-# LANGUAGE TemplateHaskell   #-}
{-# LANGUAGE TypeApplications  #-}

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

mkSymbolic [''Month]
mkSymbolic [''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 <- SBV Month -> SBV Day -> Birthday
BD (SBV Month -> SBV Day -> Birthday)
-> SymbolicT IO (SBV Month) -> SymbolicT IO (SBV Day -> Birthday)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> SymbolicT IO (SBV Month)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"birthMonth" SymbolicT IO (SBV Day -> Birthday)
-> SymbolicT IO (SBV Day) -> 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 (SBV Day)
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 SBV Month
m SBV Day
d) =   (SBV Month
m SBV Month -> SBV Month -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Month
sMay SBool -> SBool -> SBool
.=> SBV Day
d SBV Day -> [SBV Day] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` [SBV Day
sD15, SBV Day
sD16, SBV Day
sD19])
               SBool -> SBool -> SBool
.&& (SBV Month
m SBV Month -> SBV Month -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Month
sJun SBool -> SBool -> SBool
.=> SBV Day
d SBV Day -> [SBV Day] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` [SBV Day
sD17, SBV Day
sD18])
               SBool -> SBool -> SBool
.&& (SBV Month
m SBV Month -> SBV Month -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Month
sJul SBool -> SBool -> SBool
.=> SBV Day
d SBV Day -> [SBV Day] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` [SBV Day
sD14, SBV Day
sD16])
               SBool -> SBool -> SBool
.&& (SBV Month
m SBV Month -> SBV Month -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Month
sAug SBool -> SBool -> SBool
.=> SBV Day
d SBV Day -> [SBV Day] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` [SBV Day
sD14, SBV Day
sD15, SBV Day
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 SBV Month
birthMonth SBV Day
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 :: SBV Month -> SBool
a1 SBV Month
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 SBV Day
d1) (Exists SBV Day
d2) -> [Birthday] -> SBool
ok [SBV Month -> SBV Day -> Birthday
BD SBV Month
m SBV Day
d1, SBV Month -> SBV Day -> Birthday
BD SBV Month
m SBV Day
d2] SBool -> SBool -> SBool
.&& SBV Day
d1 SBV Day -> SBV Day -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SBV Day
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
$ SBV Month -> SBool
a1 SBV Month
birthMonth

            -- Albert: I know that Bernard doesn't know
            let a2 :: SBV Month -> SBool
a2 SBV Month
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 SBV Day
d) -> [Birthday] -> SBool
ok [SBV Month -> SBV Day -> Birthday
BD SBV Month
m SBV Day
d] SBool -> SBool -> SBool
.=> (Exists Any Month -> Exists Any Month -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
qe (\(Exists SBV Month
m1) (Exists SBV Month
m2) -> [Birthday] -> SBool
ok [SBV Month -> SBV Day -> Birthday
BD SBV Month
m1 SBV Day
d, SBV Month -> SBV Day -> Birthday
BD SBV Month
m2 SBV Day
d] SBool -> SBool -> SBool
.&& SBV Month
m1 SBV Month -> SBV Month -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SBV Month
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
$ SBV Month -> SBool
a2 SBV Month
birthMonth

            -- Bernard: I did not know
            let b1 :: SBV Day -> SBool
b1 SBV Day
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 SBV Month
m1) (Exists SBV Month
m2) -> [Birthday] -> SBool
ok [SBV Month -> SBV Day -> Birthday
BD SBV Month
m1 SBV Day
d, SBV Month -> SBV Day -> Birthday
BD SBV Month
m2 SBV Day
d] SBool -> SBool -> SBool
.&& SBV Month
m1 SBV Month -> SBV Month -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SBV Month
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
$ SBV Day -> SBool
b1 SBV Day
birthDay

            -- Bernard: But now I know
            let b2p :: SBV Month -> SBV Day -> SBool
b2p SBV Month
m SBV Day
d = [Birthday] -> SBool
ok [SBV Month -> SBV Day -> Birthday
BD SBV Month
m SBV Day
d] SBool -> SBool -> SBool
.&& SBV Month -> SBool
a1 SBV Month
m SBool -> SBool -> SBool
.&& SBV Month -> SBool
a2 SBV Month
m
                b2 :: SBV Day -> SBool
b2  SBV Day
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 SBV Month
m1) (Forall SBV Month
m2) -> (SBV Month -> SBV Day -> SBool
b2p SBV Month
m1 SBV Day
d SBool -> SBool -> SBool
.&& SBV Month -> SBV Day -> SBool
b2p SBV Month
m2 SBV Day
d) SBool -> SBool -> SBool
.=> SBV Month
m1 SBV Month -> SBV Month -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Month
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
$ SBV Day -> SBool
b2 SBV Day
birthDay

            -- Albert: Now I know too
            let a3p :: SBV Month -> SBV Day -> SBool
a3p SBV Month
m SBV Day
d = [Birthday] -> SBool
ok [SBV Month -> SBV Day -> Birthday
BD SBV Month
m SBV Day
d] SBool -> SBool -> SBool
.&& SBV Month -> SBool
a1 SBV Month
m SBool -> SBool -> SBool
.&& SBV Month -> SBool
a2 SBV Month
m SBool -> SBool -> SBool
.&& SBV Day -> SBool
b1 SBV Day
d SBool -> SBool -> SBool
.&& SBV Day -> SBool
b2 SBV Day
d
                a3 :: SBV Month -> Forall nm Day -> Forall nm Day -> SBool
a3  SBV Month
m   = \(Forall SBV Day
d1) (Forall SBV Day
d2) -> (SBV Month -> SBV Day -> SBool
a3p SBV Month
m SBV Day
d1 SBool -> SBool -> SBool
.&& SBV Month -> SBV Day -> SBool
a3p SBV Month
m SBV Day
d2) SBool -> SBool -> SBool
.=> SBV Day
d1 SBV Day -> SBV Day -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Day
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
$ SBV Month -> Forall Any Day -> Forall Any Day -> SBool
forall {nm :: Symbol} {nm :: Symbol}.
SBV Month -> Forall nm Day -> Forall nm Day -> SBool
a3 SBV Month
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"       -}