-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Puzzles.Murder
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Solution to "Malice and Alice," from George J. Summers' Logical Deduction Puzzles:
--
-- @
-- A man and a woman were together in a bar at the time of the murder.
-- The victim and the killer were together on a beach at the time of the murder.
-- One of Alice’s two children was alone at the time of the murder.
-- Alice and her husband were not together at the time of the murder.
-- The victim's twin was not the killer.
-- The killer was younger than the victim.
--
-- Who killed who?
-- @
-----------------------------------------------------------------------------

{-# LANGUAGE DeriveAnyClass     #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleInstances  #-}
{-# LANGUAGE NamedFieldPuns     #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell    #-}
{-# OPTIONS_GHC -Wall -Werror   #-}

module Documentation.SBV.Examples.Puzzles.Murder where

import Data.Char
import Data.List

import Data.SBV
import Data.SBV.Control

-- | Locations
data Location = Bar | Beach | Alone

-- | Sexes
data Sex  = Male | Female

-- | Roles
data Role = Victim | Killer | Bystander

mkSymbolicEnumeration ''Location
mkSymbolicEnumeration ''Sex
mkSymbolicEnumeration ''Role

-- | A person has a name, age, together with location and sex.
-- We parameterize over a function so we can use this struct
-- both in a concrete context and a symbolic context. Note
-- that the name is always concrete.
data Person f = Person { forall (f :: * -> *). Person f -> String
nm       :: String
                       , forall (f :: * -> *). Person f -> f Integer
age      :: f Integer
                       , forall (f :: * -> *). Person f -> f Location
location :: f Location
                       , forall (f :: * -> *). Person f -> f Sex
sex      :: f Sex
                       , forall (f :: * -> *). Person f -> f Role
role     :: f Role
                       }

-- | Helper functor
newtype Const a = Const { forall a. Const a -> a
getConst :: a }

-- | Show a person
instance Show (Person Const) where
  show :: Person Const -> String
show (Person String
n Const Integer
a Const Location
l Const Sex
s Const Role
r) = [String] -> String
unwords [String
n, forall a. Show a => a -> String
show (forall a. Const a -> a
getConst Const Integer
a), forall a. Show a => a -> String
show (forall a. Const a -> a
getConst Const Location
l), forall a. Show a => a -> String
show (forall a. Const a -> a
getConst Const Sex
s), forall a. Show a => a -> String
show (forall a. Const a -> a
getConst Const Role
r)]

-- | Create a new symbolic person
newPerson :: String -> Symbolic (Person SBV)
newPerson :: String -> Symbolic (Person SBV)
newPerson String
n = do
        Person SBV
p <- forall (f :: * -> *).
String -> f Integer -> f Location -> f Sex -> f Role -> Person f
Person String
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. SymVal a => Symbolic (SBV a)
free_ forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. SymVal a => Symbolic (SBV a)
free_ forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. SymVal a => Symbolic (SBV a)
free_ forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. SymVal a => Symbolic (SBV a)
free_
        forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *). Person f -> f Integer
age Person SBV
p forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
20
        forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *). Person f -> f Integer
age Person SBV
p forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV Integer
50
        forall (f :: * -> *) a. Applicative f => a -> f a
pure Person SBV
p

-- | Get the concrete value of the person in the model
getPerson :: Person SBV -> Query (Person Const)
getPerson :: Person SBV -> Query (Person Const)
getPerson Person{String
nm :: String
nm :: forall (f :: * -> *). Person f -> String
nm, SBV Integer
age :: SBV Integer
age :: forall (f :: * -> *). Person f -> f Integer
age, SBV Location
location :: SBV Location
location :: forall (f :: * -> *). Person f -> f Location
location, SBV Sex
sex :: SBV Sex
sex :: forall (f :: * -> *). Person f -> f Sex
sex, SBV Role
role :: SBV Role
role :: forall (f :: * -> *). Person f -> f Role
role} = forall (f :: * -> *).
String -> f Integer -> f Location -> f Sex -> f Role -> Person f
Person String
nm forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. a -> Const a
Const forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. SymVal a => SBV a -> Query a
getValue SBV Integer
age)
                                                           forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall a. a -> Const a
Const forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. SymVal a => SBV a -> Query a
getValue SBV Location
location)
                                                           forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall a. a -> Const a
Const forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. SymVal a => SBV a -> Query a
getValue SBV Sex
sex)
                                                           forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall a. a -> Const a
Const forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. SymVal a => SBV a -> Query a
getValue SBV Role
role)

-- | Solve the puzzle. We have:
--
-- >>> killer
-- Alice     48  Bar    Female  Bystander
-- Husband   47  Beach  Male    Killer
-- Brother   48  Beach  Male    Victim
-- Daughter  20  Alone  Female  Bystander
-- Son       21  Bar    Male    Bystander
--
-- That is, Alice's brother was the victim and Alice's husband was the killer.
killer :: IO ()
killer :: IO ()
killer = do
   [Person Const]
persons <- IO [Person Const]
puzzle
   let wps :: [[String]]
wps      = forall a b. (a -> b) -> [a] -> [b]
map (String -> [String]
words forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) [Person Const]
persons
       cwidths :: [Int]
cwidths  = forall a b. (a -> b) -> [a] -> [b]
map ((forall a. Num a => a -> a -> a
+Int
2) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall (t :: * -> *) a. Foldable t => t a -> Int
length) (forall a. [[a]] -> [[a]]
transpose [[String]]
wps)
       align :: [String] -> String
align [String]
xs = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Int
i String
f -> forall a. Int -> [a] -> [a]
take Int
i (String
f forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat Char
' ')) [Int]
cwidths [String]
xs
       trim :: ShowS
trim     = forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse
   forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> IO ()
putStrLn forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
trim forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
align) [[String]]
wps

-- | Constraints of the puzzle, coded following the English description.
puzzle :: IO [Person Const]
puzzle :: IO [Person Const]
puzzle = forall a. Symbolic a -> IO a
runSMT forall a b. (a -> b) -> a -> b
$ do
  Person SBV
alice    <- String -> Symbolic (Person SBV)
newPerson String
"Alice"
  Person SBV
husband  <- String -> Symbolic (Person SBV)
newPerson String
"Husband"
  Person SBV
brother  <- String -> Symbolic (Person SBV)
newPerson String
"Brother"
  Person SBV
daughter <- String -> Symbolic (Person SBV)
newPerson String
"Daughter"
  Person SBV
son      <- String -> Symbolic (Person SBV)
newPerson String
"Son"

  -- Sex of each character
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *). Person f -> f Sex
sex Person SBV
alice    forall a. EqSymbolic a => a -> a -> SBool
.== SBV Sex
sFemale
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *). Person f -> f Sex
sex Person SBV
husband  forall a. EqSymbolic a => a -> a -> SBool
.== SBV Sex
sMale
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *). Person f -> f Sex
sex Person SBV
brother  forall a. EqSymbolic a => a -> a -> SBool
.== SBV Sex
sMale
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *). Person f -> f Sex
sex Person SBV
daughter forall a. EqSymbolic a => a -> a -> SBool
.== SBV Sex
sFemale
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *). Person f -> f Sex
sex Person SBV
son      forall a. EqSymbolic a => a -> a -> SBool
.== SBV Sex
sMale

  let chars :: [Person SBV]
chars = [Person SBV
alice, Person SBV
husband, Person SBV
brother, Person SBV
daughter, Person SBV
son]

  -- Age relationships. To come up with "reasonable" numbers,
  -- we make the kids at least 25 years younger than the parents
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *). Person f -> f Integer
age Person SBV
son      forall a. OrdSymbolic a => a -> a -> SBool
.<  forall (f :: * -> *). Person f -> f Integer
age Person SBV
alice    forall a. Num a => a -> a -> a
- SBV Integer
25
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *). Person f -> f Integer
age Person SBV
son      forall a. OrdSymbolic a => a -> a -> SBool
.<  forall (f :: * -> *). Person f -> f Integer
age Person SBV
husband  forall a. Num a => a -> a -> a
- SBV Integer
25
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *). Person f -> f Integer
age Person SBV
daughter forall a. OrdSymbolic a => a -> a -> SBool
.<  forall (f :: * -> *). Person f -> f Integer
age Person SBV
alice    forall a. Num a => a -> a -> a
- SBV Integer
25
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *). Person f -> f Integer
age Person SBV
daughter forall a. OrdSymbolic a => a -> a -> SBool
.<  forall (f :: * -> *). Person f -> f Integer
age Person SBV
husband  forall a. Num a => a -> a -> a
- SBV Integer
25

  -- Ensure that there's a twin. Looking at the characters, the
  -- only possibilities are either Alice's kids, or Alice and her brother
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *). Person f -> f Integer
age Person SBV
son forall a. EqSymbolic a => a -> a -> SBool
.== forall (f :: * -> *). Person f -> f Integer
age Person SBV
daughter SBool -> SBool -> SBool
.|| forall (f :: * -> *). Person f -> f Integer
age Person SBV
alice forall a. EqSymbolic a => a -> a -> SBool
.== forall (f :: * -> *). Person f -> f Integer
age Person SBV
brother

  -- One victim, one killer
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (forall a b. (a -> b) -> [a] -> [b]
map (\Person SBV
c -> forall a. (Ord a, Num a, SymVal a) => SBool -> SBV a
oneIf (forall (f :: * -> *). Person f -> f Role
role Person SBV
c forall a. EqSymbolic a => a -> a -> SBool
.== SBV Role
sVictim)) [Person SBV]
chars) forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Integer
1 :: SInteger)
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (forall a b. (a -> b) -> [a] -> [b]
map (\Person SBV
c -> forall a. (Ord a, Num a, SymVal a) => SBool -> SBV a
oneIf (forall (f :: * -> *). Person f -> f Role
role Person SBV
c forall a. EqSymbolic a => a -> a -> SBool
.== SBV Role
sKiller)) [Person SBV]
chars) forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Integer
1 :: SInteger)

  let ifVictim :: Person SBV -> SBool
ifVictim Person SBV
p = forall (f :: * -> *). Person f -> f Role
role Person SBV
p forall a. EqSymbolic a => a -> a -> SBool
.== SBV Role
sVictim
      ifKiller :: Person SBV -> SBool
ifKiller Person SBV
p = forall (f :: * -> *). Person f -> f Role
role Person SBV
p forall a. EqSymbolic a => a -> a -> SBool
.== SBV Role
sKiller

      every :: (Person SBV -> SBool) -> SBool
every Person SBV -> SBool
f = [SBool] -> SBool
sAnd (forall a b. (a -> b) -> [a] -> [b]
map Person SBV -> SBool
f [Person SBV]
chars)
      some :: (Person SBV -> SBool) -> SBool
some  Person SBV -> SBool
f = [SBool] -> SBool
sOr  (forall a b. (a -> b) -> [a] -> [b]
map Person SBV -> SBool
f [Person SBV]
chars)

  -- A man and a woman were together in a bar at the time of the murder.
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ (Person SBV -> SBool) -> SBool
some forall a b. (a -> b) -> a -> b
$ \Person SBV
c -> forall (f :: * -> *). Person f -> f Sex
sex Person SBV
c forall a. EqSymbolic a => a -> a -> SBool
.== SBV Sex
sFemale SBool -> SBool -> SBool
.&& forall (f :: * -> *). Person f -> f Location
location Person SBV
c forall a. EqSymbolic a => a -> a -> SBool
.== SBV Location
sBar
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ (Person SBV -> SBool) -> SBool
some forall a b. (a -> b) -> a -> b
$ \Person SBV
c -> forall (f :: * -> *). Person f -> f Sex
sex Person SBV
c forall a. EqSymbolic a => a -> a -> SBool
.== SBV Sex
sMale   SBool -> SBool -> SBool
.&& forall (f :: * -> *). Person f -> f Location
location Person SBV
c forall a. EqSymbolic a => a -> a -> SBool
.== SBV Location
sBar

  -- The victim and the killer were together on a beach at the time of the murder.
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ (Person SBV -> SBool) -> SBool
every forall a b. (a -> b) -> a -> b
$ \Person SBV
c -> Person SBV -> SBool
ifVictim Person SBV
c SBool -> SBool -> SBool
.=> forall (f :: * -> *). Person f -> f Location
location Person SBV
c forall a. EqSymbolic a => a -> a -> SBool
.== SBV Location
sBeach
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ (Person SBV -> SBool) -> SBool
every forall a b. (a -> b) -> a -> b
$ \Person SBV
c -> Person SBV -> SBool
ifKiller Person SBV
c SBool -> SBool -> SBool
.=> forall (f :: * -> *). Person f -> f Location
location Person SBV
c forall a. EqSymbolic a => a -> a -> SBool
.== SBV Location
sBeach

  -- One of Alice’s two children was alone at the time of the murder.
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *). Person f -> f Location
location Person SBV
daughter forall a. EqSymbolic a => a -> a -> SBool
.== SBV Location
sAlone SBool -> SBool -> SBool
.|| forall (f :: * -> *). Person f -> f Location
location Person SBV
son forall a. EqSymbolic a => a -> a -> SBool
.== SBV Location
sAlone

  -- Alice and her husband were not together at the time of the murder.
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *). Person f -> f Location
location Person SBV
alice forall a. EqSymbolic a => a -> a -> SBool
./= forall (f :: * -> *). Person f -> f Location
location Person SBV
husband

  -- The victim has a twin
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ (Person SBV -> SBool) -> SBool
every forall a b. (a -> b) -> a -> b
$ \Person SBV
c -> Person SBV -> SBool
ifVictim Person SBV
c SBool -> SBool -> SBool
.=> (Person SBV -> SBool) -> SBool
some (\Person SBV
d -> forall a. SymVal a => a -> SBV a
literal (forall (f :: * -> *). Person f -> String
nm Person SBV
c forall a. Eq a => a -> a -> Bool
/= forall (f :: * -> *). Person f -> String
nm Person SBV
d) SBool -> SBool -> SBool
.&& forall (f :: * -> *). Person f -> f Integer
age Person SBV
c forall a. EqSymbolic a => a -> a -> SBool
.== forall (f :: * -> *). Person f -> f Integer
age Person SBV
d)

  -- The victim's twin was not the killer.
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ (Person SBV -> SBool) -> SBool
every forall a b. (a -> b) -> a -> b
$ \Person SBV
c -> Person SBV -> SBool
ifVictim Person SBV
c SBool -> SBool -> SBool
.=> (Person SBV -> SBool) -> SBool
every (\Person SBV
d -> forall (f :: * -> *). Person f -> f Integer
age Person SBV
c forall a. EqSymbolic a => a -> a -> SBool
.== forall (f :: * -> *). Person f -> f Integer
age Person SBV
d SBool -> SBool -> SBool
.=> forall (f :: * -> *). Person f -> f Role
role Person SBV
d forall a. EqSymbolic a => a -> a -> SBool
./= SBV Role
sKiller)

  -- The killer was younger than the victim.
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ (Person SBV -> SBool) -> SBool
every forall a b. (a -> b) -> a -> b
$ \Person SBV
c -> Person SBV -> SBool
ifKiller Person SBV
c SBool -> SBool -> SBool
.=> (Person SBV -> SBool) -> SBool
every (\Person SBV
d -> Person SBV -> SBool
ifVictim Person SBV
d SBool -> SBool -> SBool
.=> forall (f :: * -> *). Person f -> f Integer
age Person SBV
c forall a. OrdSymbolic a => a -> a -> SBool
.< forall (f :: * -> *). Person f -> f Integer
age Person SBV
d)

  -- Ensure certain pairs can't be twins
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *). Person f -> f Integer
age Person SBV
husband forall a. EqSymbolic a => a -> a -> SBool
./= forall (f :: * -> *). Person f -> f Integer
age Person SBV
brother
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *). Person f -> f Integer
age Person SBV
husband forall a. EqSymbolic a => a -> a -> SBool
./= forall (f :: * -> *). Person f -> f Integer
age Person SBV
alice

  forall a. Query a -> Symbolic a
query forall a b. (a -> b) -> a -> b
$ do CheckSatResult
cs <- Query CheckSatResult
checkSat
             case CheckSatResult
cs of
               CheckSatResult
Sat -> do Person Const
a <- Person SBV -> Query (Person Const)
getPerson Person SBV
alice
                         Person Const
h <- Person SBV -> Query (Person Const)
getPerson Person SBV
husband
                         Person Const
b <- Person SBV -> Query (Person Const)
getPerson Person SBV
brother
                         Person Const
d <- Person SBV -> Query (Person Const)
getPerson Person SBV
daughter
                         Person Const
s <- Person SBV -> Query (Person Const)
getPerson Person SBV
son
                         forall (f :: * -> *) a. Applicative f => a -> f a
pure [Person Const
a, Person Const
h, Person Const
b, Person Const
d, Person Const
s]
               CheckSatResult
_   -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Solver said: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show CheckSatResult
cs