{-# 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
data Inhabitant
mkUninterpretedSort ''Inhabitant
data Identity = Knave | Knight
mkSymbolicEnumeration ''Identity
data Statement = Truth | Falsity
mkSymbolicEnumeration ''Statement
john :: SInhabitant
john :: SInhabitant
john = String -> SInhabitant
forall a. SMTDefinable a => String -> a
uninterpret String
"John"
bill :: SInhabitant
bill :: SInhabitant
bill = String -> SInhabitant
forall a. SMTDefinable a => String -> a
uninterpret String
"Bill"
is :: SInhabitant -> SIdentity -> SStatement
is :: SInhabitant -> SIdentity -> SStatement
is = String -> SInhabitant -> SIdentity -> SStatement
forall a. SMTDefinable a => String -> a
uninterpret String
"is"
says :: SInhabitant -> SStatement -> SBool
says :: SInhabitant -> SStatement -> SBool
says = String -> SInhabitant -> SStatement -> SBool
forall a. SMTDefinable a => String -> a
uninterpret String
"says"
holds :: SStatement -> SBool
holds :: SStatement -> SBool
holds = String -> SStatement -> SBool
forall a. SMTDefinable a => String -> a
uninterpret String
"holds"
and :: SStatement -> SStatement -> SStatement
and :: SStatement -> SStatement -> SStatement
and = String -> SStatement -> SStatement -> SStatement
forall a. SMTDefinable a => String -> a
uninterpret String
"AND"
not :: SStatement -> SStatement
not :: SStatement -> SStatement
not = String -> SStatement -> SStatement
forall a. SMTDefinable a => String -> a
uninterpret String
"NOT"
iff :: SStatement -> SStatement -> SStatement
iff :: SStatement -> SStatement -> SStatement
iff = String -> SStatement -> SStatement -> SStatement
forall a. SMTDefinable a => String -> a
uninterpret String
"IFF"
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
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
(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)
(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))
(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)
(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)
(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)
(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
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
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))
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)))