    -----------------------------------------------------------------------------
    -- |
    -- 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
        [SBool
    sign1, SBool
    sign2, SBool
    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
        [SBool
    tiger1, SBool
    tiger2, SBool
    tiger3] <- (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
    "tiger1", String
    "tiger2", String
    "tiger3"]

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

        -- Room 2 sign: A Lady is in this room
        SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    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
        SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SBool
    sign3 SBool -> SBool -> SBool
    .<=> SBool
    tiger2

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

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