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

{-# OPTIONS_GHC -Wall -Werror #-}

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 :: IO AllSatResult
ladyAndTigers = SymbolicT IO () -> IO AllSatResult
forall a. Satisfiable a => a -> IO AllSatResult
allSat (SymbolicT IO () -> IO AllSatResult)
-> SymbolicT IO () -> IO AllSatResult
forall a b. (a -> b) -> a -> b
$ do

    -- One boolean for each of the correctness of the signs
    [sign1, sign2, sign3] <- (String -> SymbolicT IO SBool) -> [String] -> SymbolicT IO [SBool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM String -> SymbolicT IO SBool
sBool [String
"sign1", String
"sign2", String
"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