-----------------------------------------------------------------------------
-- |
-- Module : Documentation.SBV.Examples.Puzzles.LadyAndTigers
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Puzzle:
--
-- You are standing in front of three rooms and must choose one. In one room is a Lady
-- (whom you could and wish to marry), in the other two rooms are tigers (that if you
-- choose either of these rooms, the tiger invites you to breakfast – the problem is
-- that you are the main course). Your job is to choose the room with the Lady.
-- The signs on the doors are:
--
-- * A Tiger is in this room
-- * A Lady is in this room
-- * A Tiger is in room two
--
-- At most only 1 statement is true. Where’s the Lady?
-----------------------------------------------------------------------------
module Documentation.SBV.Examples.Puzzles.LadyAndTigers where
import Data.SBV
-- | Prints the only solution:
--
-- >>> ladyAndTigers
-- Solution #1:
-- sign1 = False :: Bool
-- sign2 = False :: Bool
-- sign3 = True :: Bool
-- tiger1 = False :: Bool
-- tiger2 = True :: Bool
-- tiger3 = True :: Bool
-- This is the only solution.
--
-- That is, the lady is in room 1, and only the third room's sign is true.
ladyAndTigers :: IO AllSatResult
ladyAndTigers = allSat $ do
-- One boolean for each of the correctness of the signs
[sign1, sign2, sign3] <- mapM sBool ["sign1", "sign2", "sign3"]
-- One boolean for each of the presence of the tigers
[tiger1, tiger2, tiger3] <- mapM sBool ["tiger1", "tiger2", "tiger3"]
-- Room 1 sign: A Tiger is in this room
constrain $ sign1 .<=> tiger1
-- Room 2 sign: A Lady is in this room
constrain $ sign2 .<=> sNot tiger2
-- Room 3 sign: A Tiger is in room 2
constrain $ sign3 .<=> tiger2
-- At most one sign is true
constrain $ [sign1, sign2, sign3] `pbAtMost` 1
-- There are precisely two tigers
constrain $ [tiger1, tiger2, tiger3] `pbExactly` 2