-----------------------------------------------------------------------------
-- |
-- 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)))