    -----------------------------------------------------------------------------
    -- |
    -- 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 <=> bnot 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