-----------------------------------------------------------------------------
-- |
-- 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 hiding (some)
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, Integer -> String
forall a. Show a => a -> String
show (Const Integer -> Integer
forall a. Const a -> a
getConst Const Integer
a), Location -> String
forall a. Show a => a -> String
show (Const Location -> Location
forall a. Const a -> a
getConst Const Location
l), Sex -> String
forall a. Show a => a -> String
show (Const Sex -> Sex
forall a. Const a -> a
getConst Const Sex
s), Role -> String
forall a. Show a => a -> String
show (Const Role -> Role
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
        p <- String
-> SBV Integer -> SBV Location -> SBV Sex -> SBV Role -> Person SBV
forall (f :: * -> *).
String -> f Integer -> f Location -> f Sex -> f Role -> Person f
Person String
n (SBV Integer -> SBV Location -> SBV Sex -> SBV Role -> Person SBV)
-> SymbolicT IO (SBV Integer)
-> SymbolicT IO (SBV Location -> SBV Sex -> SBV Role -> Person SBV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SymbolicT IO (SBV Integer)
forall a. SymVal a => Symbolic (SBV a)
free_ SymbolicT IO (SBV Location -> SBV Sex -> SBV Role -> Person SBV)
-> SymbolicT IO (SBV Location)
-> SymbolicT IO (SBV Sex -> SBV Role -> Person SBV)
forall a b.
SymbolicT IO (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolicT IO (SBV Location)
forall a. SymVal a => Symbolic (SBV a)
free_ SymbolicT IO (SBV Sex -> SBV Role -> Person SBV)
-> SymbolicT IO (SBV Sex) -> SymbolicT IO (SBV Role -> Person SBV)
forall a b.
SymbolicT IO (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolicT IO (SBV Sex)
forall a. SymVal a => Symbolic (SBV a)
free_ SymbolicT IO (SBV Role -> Person SBV)
-> SymbolicT IO (SBV Role) -> Symbolic (Person SBV)
forall a b.
SymbolicT IO (a -> b) -> SymbolicT IO a -> SymbolicT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolicT IO (SBV Role)
forall a. SymVal a => Symbolic (SBV a)
free_
        constrain $ age p .>= 20
        constrain $ age p .<= 50
        pure 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 :: forall (f :: * -> *). Person f -> String
nm :: String
nm, SBV Integer
age :: forall (f :: * -> *). Person f -> f Integer
age :: SBV Integer
age, SBV Location
location :: forall (f :: * -> *). Person f -> f Location
location :: SBV Location
location, SBV Sex
sex :: forall (f :: * -> *). Person f -> f Sex
sex :: SBV Sex
sex, SBV Role
role :: forall (f :: * -> *). Person f -> f Role
role :: SBV Role
role} = String
-> Const Integer
-> Const Location
-> Const Sex
-> Const Role
-> Person Const
forall (f :: * -> *).
String -> f Integer -> f Location -> f Sex -> f Role -> Person f
Person String
nm (Const Integer
 -> Const Location -> Const Sex -> Const Role -> Person Const)
-> QueryT IO (Const Integer)
-> QueryT
     IO (Const Location -> Const Sex -> Const Role -> Person Const)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer -> Const Integer
forall a. a -> Const a
Const (Integer -> Const Integer)
-> QueryT IO Integer -> QueryT IO (Const Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV Integer -> QueryT IO Integer
forall a. SymVal a => SBV a -> Query a
getValue SBV Integer
age)
                                                           QueryT
  IO (Const Location -> Const Sex -> Const Role -> Person Const)
-> QueryT IO (Const Location)
-> QueryT IO (Const Sex -> Const Role -> Person Const)
forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Location -> Const Location
forall a. a -> Const a
Const (Location -> Const Location)
-> QueryT IO Location -> QueryT IO (Const Location)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV Location -> QueryT IO Location
forall a. SymVal a => SBV a -> Query a
getValue SBV Location
location)
                                                           QueryT IO (Const Sex -> Const Role -> Person Const)
-> QueryT IO (Const Sex) -> QueryT IO (Const Role -> Person Const)
forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Sex -> Const Sex
forall a. a -> Const a
Const (Sex -> Const Sex) -> QueryT IO Sex -> QueryT IO (Const Sex)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV Sex -> QueryT IO Sex
forall a. SymVal a => SBV a -> Query a
getValue SBV Sex
sex)
                                                           QueryT IO (Const Role -> Person Const)
-> QueryT IO (Const Role) -> Query (Person Const)
forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Role -> Const Role
forall a. a -> Const a
Const (Role -> Const Role) -> QueryT IO Role -> QueryT IO (Const Role)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV Role -> QueryT IO Role
forall a. SymVal a => SBV a -> Query a
getValue SBV Role
role)

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

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

  -- Sex of each character
  constrain $ sex alice    .== sFemale
  constrain $ sex husband  .== sMale
  constrain $ sex brother  .== sMale
  constrain $ sex daughter .== sFemale
  constrain $ sex son      .== sMale

  let 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
  constrain $ age son      .<  age alice    - 25
  constrain $ age son      .<  age husband  - 25
  constrain $ age daughter .<  age alice    - 25
  constrain $ age daughter .<  age husband  - 25

  -- Ensure that there's a twin. Looking at the characters, the
  -- only possibilities are either Alice's kids, or Alice and her brother
  constrain $ age son .== age daughter .|| age alice .== age brother

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

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

      every Person SBV -> SBool
f = (Person SBV -> SBool) -> [Person SBV] -> SBool
forall a. (a -> SBool) -> [a] -> SBool
sAll Person SBV -> SBool
f [Person SBV]
chars
      some  Person SBV -> SBool
f = (Person SBV -> SBool) -> [Person SBV] -> SBool
forall a. (a -> SBool) -> [a] -> SBool
sAny Person SBV -> SBool
f [Person SBV]
chars

  -- A man and a woman were together in a bar at the time of the murder.
  constrain $ some $ \Person SBV
c -> Person SBV -> SBV Sex
forall (f :: * -> *). Person f -> f Sex
sex Person SBV
c SBV Sex -> SBV Sex -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Sex
sFemale SBool -> SBool -> SBool
.&& Person SBV -> SBV Location
forall (f :: * -> *). Person f -> f Location
location Person SBV
c SBV Location -> SBV Location -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Location
sBar
  constrain $ some $ \Person SBV
c -> Person SBV -> SBV Sex
forall (f :: * -> *). Person f -> f Sex
sex Person SBV
c SBV Sex -> SBV Sex -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Sex
sMale   SBool -> SBool -> SBool
.&& Person SBV -> SBV Location
forall (f :: * -> *). Person f -> f Location
location Person SBV
c SBV Location -> SBV Location -> SBool
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.
  constrain $ every $ \Person SBV
c -> Person SBV -> SBool
ifVictim Person SBV
c SBool -> SBool -> SBool
.=> Person SBV -> SBV Location
forall (f :: * -> *). Person f -> f Location
location Person SBV
c SBV Location -> SBV Location -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Location
sBeach
  constrain $ every $ \Person SBV
c -> Person SBV -> SBool
ifKiller Person SBV
c SBool -> SBool -> SBool
.=> Person SBV -> SBV Location
forall (f :: * -> *). Person f -> f Location
location Person SBV
c SBV Location -> SBV Location -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Location
sBeach

  -- One of Alice’s two children was alone at the time of the murder.
  constrain $ location daughter .== sAlone .|| location son .== sAlone

  -- Alice and her husband were not together at the time of the murder.
  constrain $ location alice ./= location husband

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

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

  -- The killer was younger than the victim.
  constrain $ every $ \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
.=> Person SBV -> SBV Integer
forall (f :: * -> *). Person f -> f Integer
age Person SBV
c SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< Person SBV -> SBV Integer
forall (f :: * -> *). Person f -> f Integer
age Person SBV
d)

  -- Ensure certain pairs can't be twins
  constrain $ age husband ./= age brother
  constrain $ age husband ./= age alice

  query $ do cs <- checkSat
             case cs of
               CheckSatResult
Sat -> do a <- Person SBV -> Query (Person Const)
getPerson Person SBV
alice
                         h <- getPerson husband
                         b <- getPerson brother
                         d <- getPerson daughter
                         s <- getPerson son
                         pure [a, h, b, d, s]
               CheckSatResult
_   -> String -> Query [Person Const]
forall a. HasCallStack => String -> a
error (String -> Query [Person Const]) -> String -> Query [Person Const]
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

{- HLint ignore getPerson "Functor law" -}