content: -----------------------------------------------------------------------------
  -- |
  -- 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 = 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
  