    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- From Raymond Smullyan: On a fictional island, all inhabitants are either knights,
    -- who always tell the truth, or knaves, who always lie. John and Bill are residents
    -- of the island of knights and knaves. John and Bill make several utterances.
    -- Determine which one is a knave or a knight, depending on their answers.
    -----------------------------------------------------------------------------

    {-# LANGUAGE DeriveAnyClass     #-}
    {-# LANGUAGE DeriveDataTypeable #-}
    {-# LANGUAGE StandaloneDeriving #-}
    {-# LANGUAGE TemplateHaskell    #-}

    module Documentation.SBV.Examples.Puzzles.KnightsAndKnaves where

    import Prelude hiding (and, not)

    import Data.SBV
    import Data.SBV.Control

    -- | Inhabitants of the island, as an uninterpreted sort
    data Inhabitant
    mkUninterpretedSort ''Inhabitant

    -- | Each inhabitant is either a knave or a knight
    data Identity = Knave | Knight
    mkSymbolicEnumeration ''Identity

    -- | Statements are utterances which are either true or false
    data Statement = Truth | Falsity
    mkSymbolicEnumeration ''Statement

    -- | John is an inhabitant of the island.
    john :: SInhabitant
    john :: SInhabitant
    john = String -> SInhabitant
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "John"

    -- | Bill is an inhabitant of the island.
    bill :: SInhabitant
    bill :: SInhabitant
    bill = String -> SInhabitant
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "Bill"

    -- | The connective 'is' makes a statement about an inhabitant regarding his/her identity.
    is :: SInhabitant -> SIdentity -> SStatement
    is :: SInhabitant -> SIdentity -> SStatement
    is = String -> SInhabitant -> SIdentity -> SStatement
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "is"

    -- | The connective 'says' makes a predicate from what an inhabitant states
    says :: SInhabitant -> SStatement -> SBool
    says :: SInhabitant -> SStatement -> SBool
    says = String -> SInhabitant -> SStatement -> SBool
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "says"

    -- | The connective 'holds' is will be true if the statement is true
    holds :: SStatement -> SBool
    holds :: SStatement -> SBool
    holds = String -> SStatement -> SBool
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "holds"

    -- | The connective 'and' creates the conjunction of two statements
    and :: SStatement -> SStatement -> SStatement
    and :: SStatement -> SStatement -> SStatement
    and = String -> SStatement -> SStatement -> SStatement
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "AND"

    -- | The connective 'not' negates a statement
    not :: SStatement -> SStatement
    not :: SStatement -> SStatement
    not = String -> SStatement -> SStatement
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "NOT"

    -- | The connective 'iff' creates a statement that equates the truth values of its argument statements
    iff :: SStatement -> SStatement -> SStatement
    iff :: SStatement -> SStatement -> SStatement
    iff = String -> SStatement -> SStatement -> SStatement
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "IFF"

    -- | Encode Smullyan's puzzle. We have:
    --
    -- >>> puzzle
    -- Question 1.
    --   John says, We are both knaves
    --     Then, John is: Knave
    --     And,  Bill is: Knight
    -- Question 2.
    --   John says If (and only if) Bill is a knave, then I am a knave.
    --   Bill says We are of different kinds.
    --     Then, John is: Knave
    --     And,  Bill is: Knight
    puzzle :: IO ()
    puzzle :: IO ()
    puzzle = Symbolic () -> IO ()
    forall a. Symbolic a -> IO a
    runSMT (Symbolic () -> IO ()) -> Symbolic () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ do

        -- truth holds, falsity doesn't
        SBool -> Symbolic ()
    forall a. QuantifiedBool a => a -> Symbolic ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
    forall a b. (a -> b) -> a -> b
    $ SStatement -> SBool
    holds SStatement
    sTruth
        SBool -> Symbolic ()
    forall a. QuantifiedBool a => a -> Symbolic ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
    forall a b. (a -> b) -> a -> b
    $ SBool -> SBool
    sNot (SBool -> SBool) -> SBool -> SBool
    forall a b. (a -> b) -> a -> b
    $ SStatement -> SBool
    holds SStatement
    sFalsity

        -- Each inhabitant is either a knave or a knight
        (Forall Any Inhabitant -> SBool) -> Symbolic ()
    forall a. QuantifiedBool a => a -> Symbolic ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain ((Forall Any Inhabitant -> SBool) -> Symbolic ())
    -> (Forall Any Inhabitant -> SBool) -> Symbolic ()
    forall a b. (a -> b) -> a -> b
    $ \(Forall SInhabitant
    x) -> SStatement -> SBool
    holds (SInhabitant -> SIdentity -> SStatement
    is SInhabitant
    x SIdentity
    sKnave) SBool -> SBool -> SBool
    .<+> SStatement -> SBool
    holds (SInhabitant -> SIdentity -> SStatement
    is SInhabitant
    x SIdentity
    sKnight)

        -- If x is a knave and he says something, then that statement is false
        (Forall Any Inhabitant -> Forall Any Statement -> SBool)
    -> Symbolic ()
    forall a. QuantifiedBool a => a -> Symbolic ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain ((Forall Any Inhabitant -> Forall Any Statement -> SBool)
     -> Symbolic ())
    -> (Forall Any Inhabitant -> Forall Any Statement -> SBool)
    -> Symbolic ()
    forall a b. (a -> b) -> a -> b
    $ \(Forall SInhabitant
    x) (Forall SStatement
    y) -> SStatement -> SBool
    holds (SInhabitant -> SIdentity -> SStatement
    is SInhabitant
    x SIdentity
    sKnave)  SBool -> SBool -> SBool
    .=> (SInhabitant -> SStatement -> SBool
    says SInhabitant
    x SStatement
    y SBool -> SBool -> SBool
    .=> SBool -> SBool
    sNot (SStatement -> SBool
    holds SStatement
    y))

        -- If x is a knight and he says something, then that statement is true
        (Forall Any Inhabitant -> Forall Any Statement -> SBool)
    -> Symbolic ()
    forall a. QuantifiedBool a => a -> Symbolic ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain ((Forall Any Inhabitant -> Forall Any Statement -> SBool)
     -> Symbolic ())
    -> (Forall Any Inhabitant -> Forall Any Statement -> SBool)
    -> Symbolic ()
    forall a b. (a -> b) -> a -> b
    $ \(Forall SInhabitant
    x) (Forall SStatement
    y) -> SStatement -> SBool
    holds (SInhabitant -> SIdentity -> SStatement
    is SInhabitant
    x SIdentity
    sKnight) SBool -> SBool -> SBool
    .=> (SInhabitant -> SStatement -> SBool
    says SInhabitant
    x SStatement
    y SBool -> SBool -> SBool
    .=> SStatement -> SBool
    holds SStatement
    y)

        -- The meaning of conjunction: It holds whenever both statements hold
        (Forall Any Statement -> Forall Any Statement -> SBool)
    -> Symbolic ()
    forall a. QuantifiedBool a => a -> Symbolic ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain ((Forall Any Statement -> Forall Any Statement -> SBool)
     -> Symbolic ())
    -> (Forall Any Statement -> Forall Any Statement -> SBool)
    -> Symbolic ()
    forall a b. (a -> b) -> a -> b
    $ \(Forall SStatement
    x) (Forall SStatement
    y) -> SStatement -> SBool
    holds (SStatement -> SStatement -> SStatement
    and SStatement
    x SStatement
    y) SBool -> SBool -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== (SStatement -> SBool
    holds SStatement
    x SBool -> SBool -> SBool
    .&& SStatement -> SBool
    holds SStatement
    y)

        -- The meaning of negation: It holds when the original doesn't
        (Forall Any Statement -> SBool) -> Symbolic ()
    forall a. QuantifiedBool a => a -> Symbolic ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain ((Forall Any Statement -> SBool) -> Symbolic ())
    -> (Forall Any Statement -> SBool) -> Symbolic ()
    forall a b. (a -> b) -> a -> b
    $ \(Forall SStatement
    x) -> SStatement -> SBool
    holds (SStatement -> SStatement
    not SStatement
    x) SBool -> SBool -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SBool -> SBool
    sNot (SStatement -> SBool
    holds SStatement
    x)

        -- The meaning of iff: both statements hold or don't hold at the same time
        (Forall Any Statement -> Forall Any Statement -> SBool)
    -> Symbolic ()
    forall a. QuantifiedBool a => a -> Symbolic ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain ((Forall Any Statement -> Forall Any Statement -> SBool)
     -> Symbolic ())
    -> (Forall Any Statement -> Forall Any Statement -> SBool)
    -> Symbolic ()
    forall a b. (a -> b) -> a -> b
    $ \(Forall SStatement
    x) (Forall SStatement
    y) -> SStatement -> SBool
    holds (SStatement -> SStatement -> SStatement
    iff SStatement
    x SStatement
    y) SBool -> SBool -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== (SStatement -> SBool
    holds SStatement
    x SBool -> SBool -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SStatement -> SBool
    holds SStatement
    y)

        Query () -> Symbolic ()
    forall a. Query a -> Symbolic a
    query (Query () -> Symbolic ()) -> Query () -> Symbolic ()
    forall a b. (a -> b) -> a -> b
    $ do

          -- helper to get the responses out
          let checkStatus :: Query ()
    checkStatus = do CheckSatResult
    cs <- Query CheckSatResult
    checkSat
                               case CheckSatResult
    cs of
                                 CheckSatResult
    Sat -> do Bool
    jk <- SBool -> Query Bool
    forall a. SymVal a => SBV a -> Query a
    getValue (SStatement -> SBool
    holds (SInhabitant -> SIdentity -> SStatement
    is SInhabitant
    john SIdentity
    sKnight))
                                           Bool
    bk <- SBool -> Query Bool
    forall a. SymVal a => SBV a -> Query a
    getValue (SStatement -> SBool
    holds (SInhabitant -> SIdentity -> SStatement
    is SInhabitant
    bill SIdentity
    sKnight))
                                           IO () -> Query ()
    forall a. IO a -> Query a
    io (IO () -> Query ()) -> IO () -> Query ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String
    "    Then, John is: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ if Bool
    jk then String
    "Knight" else String
    "Knave"
                                           IO () -> Query ()
    forall a. IO a -> Query a
    io (IO () -> Query ()) -> IO () -> Query ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String
    "    And,  Bill is: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ if Bool
    bk then String
    "Knight" else String
    "Knave"
                                 CheckSatResult
    _   -> String -> Query ()
    forall a. HasCallStack => String -> a
    error (String -> Query ()) -> String -> Query ()
    forall a b. (a -> b) -> a -> b
    $ String
    "Solver said: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ CheckSatResult -> String
    forall a. Show a => a -> String
    show CheckSatResult
    cs

              question :: String -> QueryT IO a -> Query ()
    question String
    w QueryT IO a
    q = Query () -> Query ()
    forall a. Query a -> Query a
    inNewAssertionStack (Query () -> Query ()) -> Query () -> Query ()
    forall a b. (a -> b) -> a -> b
    $ do
                    IO () -> Query ()
    forall a. IO a -> Query a
    io (IO () -> Query ()) -> IO () -> Query ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn String
    w
                    QueryT IO a
    q QueryT IO a -> Query () -> Query ()
    forall a b. QueryT IO a -> QueryT IO b -> QueryT IO b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Query ()
    checkStatus

          -- Question 1
          String -> Query () -> Query ()
    forall {a}. String -> QueryT IO a -> Query ()
    question String
    "Question 1." (Query () -> Query ()) -> Query () -> Query ()
    forall a b. (a -> b) -> a -> b
    $ do
             IO () -> Query ()
    forall a. IO a -> Query a
    io (IO () -> Query ()) -> IO () -> Query ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn String
    "  John says, We are both knaves"
             SBool -> Query ()
    forall a. QuantifiedBool a => a -> Query ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> Query ()) -> SBool -> Query ()
    forall a b. (a -> b) -> a -> b
    $ SInhabitant -> SStatement -> SBool
    says SInhabitant
    john (SStatement -> SStatement -> SStatement
    and (SInhabitant -> SIdentity -> SStatement
    is SInhabitant
    john SIdentity
    sKnave) (SInhabitant -> SIdentity -> SStatement
    is SInhabitant
    bill SIdentity
    sKnave))

          -- Question 2
          String -> Query () -> Query ()
    forall {a}. String -> QueryT IO a -> Query ()
    question String
    "Question 2." (Query () -> Query ()) -> Query () -> Query ()
    forall a b. (a -> b) -> a -> b
    $ do
             IO () -> Query ()
    forall a. IO a -> Query a
    io (IO () -> Query ()) -> IO () -> Query ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn String
    "  John says If (and only if) Bill is a knave, then I am a knave."
             IO () -> Query ()
    forall a. IO a -> Query a
    io (IO () -> Query ()) -> IO () -> Query ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn String
    "  Bill says We are of different kinds."
             SBool -> Query ()
    forall a. QuantifiedBool a => a -> Query ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> Query ()) -> SBool -> Query ()
    forall a b. (a -> b) -> a -> b
    $ SInhabitant -> SStatement -> SBool
    says SInhabitant
    john (SStatement -> SStatement -> SStatement
    iff (SInhabitant -> SIdentity -> SStatement
    is SInhabitant
    bill SIdentity
    sKnave) (SInhabitant -> SIdentity -> SStatement
    is SInhabitant
    john SIdentity
    sKnave))
             SBool -> Query ()
    forall a. QuantifiedBool a => a -> Query ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> Query ()) -> SBool -> Query ()
    forall a b. (a -> b) -> a -> b
    $ SInhabitant -> SStatement -> SBool
    says SInhabitant
    bill (SStatement -> SStatement
    not (SStatement -> SStatement -> SStatement
    iff (SInhabitant -> SIdentity -> SStatement
    is SInhabitant
    bill SIdentity
    sKnave) (SInhabitant -> SIdentity -> SStatement
    is SInhabitant
    john SIdentity
    sKnave)))