sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Documentation.SBV.Examples.Puzzles.Birthday

Contents

- Types and values
- The puzzle

Description

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.

Synopsis

- data Month
  - = May
  - | Jun
  - | Jul
  - | Aug
- data Day
  - = D14
  - | D15
  - | D16
  - | D17
  - | D18
  - | D19
- type SMonth = SBV Month
- sAug :: SBV Month
- sJul :: SBV Month
- sJun :: SBV Month
- sMay :: SBV Month
- type SDay = SBV Day
- sD19 :: SBV Day
- sD18 :: SBV Day
- sD17 :: SBV Day
- sD16 :: SBV Day
- sD15 :: SBV Day
- sD14 :: SBV Day
- data Birthday = BD SMonth SDay
- mkBirthday :: Symbolic Birthday
- valid :: Birthday -> SBool
- puzzle :: ConstraintSet
- cheryl :: IO ()

# Types and values

data Month Source #

Months. We only put in the months involved in the puzzle for simplicity

Constructors

May |
Jun |
Jul |
Aug |

#### Instances

Instances details

Data Month Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Birthday

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Month -> c Month Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Month Source #

toConstr :: Month -> Constr Source #

dataTypeOf :: Month -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Month) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Month) Source #

gmapT :: (forall b. Data b => b -> b) -> Month -> Month Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Month -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Month -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Month -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Month -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Month -> m Month Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Month -> m Month Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Month -> m Month Source #

Read Month Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Birthday Methods readsPrec :: Int -> ReadS Month Source # readList :: ReadS [Month] Source # readPrec :: ReadPrec Month Source # readListPrec :: ReadPrec [Month] Source #
Show Month Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Birthday Methods showsPrec :: Int -> Month -> ShowS Source # show :: Month -> String Source # showList :: [Month] -> ShowS Source #
Eq Month Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Birthday Methods (==) :: Month -> Month -> Bool Source # (/=) :: Month -> Month -> Bool Source #
Ord Month Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Birthday Methods compare :: Month -> Month -> Ordering Source # (<) :: Month -> Month -> Bool Source # (<=) :: Month -> Month -> Bool Source # (>) :: Month -> Month -> Bool Source # (>=) :: Month -> Month -> Bool Source # max :: Month -> Month -> Month Source # min :: Month -> Month -> Month Source #
SymVal Month Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Birthday

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Month) Source #

literal :: Month -> SBV Month Source #

fromCV :: CV -> Month Source #

isConcretely :: SBV Month -> (Month -> Bool) -> Bool Source #

free :: MonadSymbolic m => String -> m (SBV Month) Source #

free_ :: MonadSymbolic m => m (SBV Month) Source #

mkFreeVars :: MonadSymbolic m => Int -> m [SBV Month] Source #

symbolic :: MonadSymbolic m => String -> m (SBV Month) Source #

symbolics :: MonadSymbolic m => [String] -> m [SBV Month] Source #

unliteral :: SBV Month -> Maybe Month Source #

isConcrete :: SBV Month -> Bool Source #

isSymbolic :: SBV Month -> Bool Source #

HasKind Month Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Birthday

Methods

kindOf :: Month -> Kind Source #

hasSign :: Month -> Bool Source #

intSizeOf :: Month -> Int Source #

isBoolean :: Month -> Bool Source #

isBounded :: Month -> Bool Source #

isReal :: Month -> Bool Source #

isFloat :: Month -> Bool Source #

isDouble :: Month -> Bool Source #

isRational :: Month -> Bool Source #

isFP :: Month -> Bool Source #

isUnbounded :: Month -> Bool Source #

isUserSort :: Month -> Bool Source #

isChar :: Month -> Bool Source #

isString :: Month -> Bool Source #

isList :: Month -> Bool Source #

isSet :: Month -> Bool Source #

isTuple :: Month -> Bool Source #

isMaybe :: Month -> Bool Source #

isEither :: Month -> Bool Source #

showType :: Month -> String Source #

SatModel Month Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Birthday Methods parseCVs :: [CV] -> Maybe (Month, [CV]) Source # cvtModel :: (Month -> Maybe b) -> Maybe (Month, [CV]) -> Maybe (b, [CV]) Source #

data Day Source #

Days. Again, only the ones mentioned in the puzzle.

Constructors

D14 |
D15 |
D16 |
D17 |
D18 |
D19 |

#### Instances

Instances details

Data Day Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Birthday

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Day -> c Day Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Day Source #

toConstr :: Day -> Constr Source #

dataTypeOf :: Day -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Day) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Day) Source #

gmapT :: (forall b. Data b => b -> b) -> Day -> Day Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Day -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Day -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Day -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Day -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Day -> m Day Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Day -> m Day Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Day -> m Day Source #

Read Day Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Birthday Methods readsPrec :: Int -> ReadS Day Source # readList :: ReadS [Day] Source # readPrec :: ReadPrec Day Source # readListPrec :: ReadPrec [Day] Source #
Show Day Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Birthday Methods showsPrec :: Int -> Day -> ShowS Source # show :: Day -> String Source # showList :: [Day] -> ShowS Source #
Eq Day Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Birthday Methods (==) :: Day -> Day -> Bool Source # (/=) :: Day -> Day -> Bool Source #
Ord Day Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Birthday Methods compare :: Day -> Day -> Ordering Source # (<) :: Day -> Day -> Bool Source # (<=) :: Day -> Day -> Bool Source # (>) :: Day -> Day -> Bool Source # (>=) :: Day -> Day -> Bool Source # max :: Day -> Day -> Day Source # min :: Day -> Day -> Day Source #
SymVal Day Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Birthday

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Day) Source #

literal :: Day -> SBV Day Source #

fromCV :: CV -> Day Source #

isConcretely :: SBV Day -> (Day -> Bool) -> Bool Source #

free :: MonadSymbolic m => String -> m (SBV Day) Source #

free_ :: MonadSymbolic m => m (SBV Day) Source #

mkFreeVars :: MonadSymbolic m => Int -> m [SBV Day] Source #

symbolic :: MonadSymbolic m => String -> m (SBV Day) Source #

symbolics :: MonadSymbolic m => [String] -> m [SBV Day] Source #

unliteral :: SBV Day -> Maybe Day Source #

isConcrete :: SBV Day -> Bool Source #

isSymbolic :: SBV Day -> Bool Source #

HasKind Day Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Birthday

Methods

kindOf :: Day -> Kind Source #

hasSign :: Day -> Bool Source #

intSizeOf :: Day -> Int Source #

isBoolean :: Day -> Bool Source #

isBounded :: Day -> Bool Source #

isReal :: Day -> Bool Source #

isFloat :: Day -> Bool Source #

isDouble :: Day -> Bool Source #

isRational :: Day -> Bool Source #

isFP :: Day -> Bool Source #

isUnbounded :: Day -> Bool Source #

isUserSort :: Day -> Bool Source #

isChar :: Day -> Bool Source #

isString :: Day -> Bool Source #

isList :: Day -> Bool Source #

isSet :: Day -> Bool Source #

isTuple :: Day -> Bool Source #

isMaybe :: Day -> Bool Source #

isEither :: Day -> Bool Source #

showType :: Day -> String Source #

SatModel Day Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Birthday Methods parseCVs :: [CV] -> Maybe (Day, [CV]) Source # cvtModel :: (Day -> Maybe b) -> Maybe (Day, [CV]) -> Maybe (b, [CV]) Source #

type SMonth = SBV Month Source #

Symbolic version of the type `Month`.

sAug :: SBV Month Source #

Symbolic version of the constructor `Aug`.

sJul :: SBV Month Source #

Symbolic version of the constructor `Jul`.

sJun :: SBV Month Source #

Symbolic version of the constructor `Jun`.

sMay :: SBV Month Source #

Symbolic version of the constructor `May`.

type SDay = SBV Day Source #

Symbolic version of the type `Day`.

sD19 :: SBV Day Source #

Symbolic version of the constructor `D19`.

sD18 :: SBV Day Source #

Symbolic version of the constructor `D18`.

sD17 :: SBV Day Source #

Symbolic version of the constructor `D17`.

sD16 :: SBV Day Source #

Symbolic version of the constructor `D16`.

sD15 :: SBV Day Source #

Symbolic version of the constructor `D15`.

sD14 :: SBV Day Source #

Symbolic version of the constructor `D14`.

data Birthday Source #

Represent the birthday as a record

Constructors

BD SMonth SDay |

mkBirthday :: Symbolic Birthday Source #

Make a valid symbolic birthday

valid :: Birthday -> SBool Source #

Is this a valid birthday? i.e., one that was declared by Cheryl to be a possibility.

# The puzzle

puzzle :: ConstraintSet Source #

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.

cheryl :: IO () Source #

Find all solutions to the birthday problem. We have:

    >>> cheryl
    Solution #1:
      birthMonth = Jul :: Month
      birthDay   = D16 :: Day
    This is the only solution.