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

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

    -- One boolean for each of the presence of the tigers
    [SBool
tiger1, SBool
tiger2, SBool
tiger3] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM String -> Symbolic SBool
sBool [String
"tiger1", String
"tiger2", String
"tiger3"]

    -- Room 1 sign: A Tiger is in this room
    forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBool
sign1 SBool -> SBool -> SBool
.<=> SBool
tiger1

    -- Room 2 sign: A Lady is in this room
    forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBool
sign2 SBool -> SBool -> SBool
.<=> SBool -> SBool
sNot SBool
tiger2

    -- Room 3 sign: A Tiger is in room 2
    forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBool
sign3 SBool -> SBool -> SBool
.<=> SBool
tiger2

    -- At most one sign is true
    forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ [SBool
sign1, SBool
sign2, SBool
sign3] [SBool] -> Int -> SBool
`pbAtMost` Int
1

    -- There are precisely two tigers
    forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ [SBool
tiger1, SBool
tiger2, SBool
tiger3] [SBool] -> Int -> SBool
`pbExactly` Int
2