-----------------------------------------------------------------------------
-- |
-- 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 { Person f -> String
nm       :: String
                       , Person f -> f Integer
age      :: f Integer
                       , Person f -> f Location
location :: f Location
                       , Person f -> f Sex
sex      :: f Sex
                       , Person f -> f Role
role     :: f Role
                       }

-- | Helper functor
newtype Const a = Const { 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
        Person SBV
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 (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 (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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SymbolicT IO (SBV Role)
forall a. SymVal a => Symbolic (SBV a)
free_
        SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ Person SBV -> SBV Integer
forall (f :: * -> *). Person f -> f Integer
age Person SBV
p SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
20
        SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ Person SBV -> SBV Integer
forall (f :: * -> *). Person f -> f Integer
age Person SBV
p SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV Integer
50
        Person SBV -> Symbolic (Person SBV)
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} = 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 (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 (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 (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     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      = (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 :: [Int]
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 (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 (t :: * -> *) a. Foldable t => t a -> Int
length) ([[String]] -> [[String]]
forall a. [[a]] -> [[a]]
transpose [[String]]
wps)
       align :: [String] -> String
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
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
   ([String] -> IO ()) -> [[String]] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> IO ()
putStrLn (String -> IO ()) -> ([String] -> String) -> [String] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
trim ShowS -> ([String] -> String) -> [String] -> String
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 = 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
  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
  SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ Person SBV -> SBV Sex
forall (f :: * -> *). Person f -> f Sex
sex Person SBV
alice    SBV Sex -> SBV Sex -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Sex
sFemale
  SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ Person SBV -> SBV Sex
forall (f :: * -> *). Person f -> f Sex
sex Person SBV
husband  SBV Sex -> SBV Sex -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Sex
sMale
  SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ Person SBV -> SBV Sex
forall (f :: * -> *). Person f -> f Sex
sex Person SBV
brother  SBV Sex -> SBV Sex -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Sex
sMale
  SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ Person SBV -> SBV Sex
forall (f :: * -> *). Person f -> f Sex
sex Person SBV
daughter SBV Sex -> SBV Sex -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Sex
sFemale
  SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ Person SBV -> SBV Sex
forall (f :: * -> *). Person f -> f Sex
sex Person SBV
son      SBV Sex -> SBV Sex -> SBool
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
  SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ Person SBV -> SBV Integer
forall (f :: * -> *). Person f -> f Integer
age Person SBV
son      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
alice    SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
- SBV Integer
25
  SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ Person SBV -> SBV Integer
forall (f :: * -> *). Person f -> f Integer
age Person SBV
son      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
husband  SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
- SBV Integer
25
  SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ Person SBV -> SBV Integer
forall (f :: * -> *). Person f -> f Integer
age Person SBV
daughter 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
alice    SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
- SBV Integer
25
  SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ Person SBV -> SBV Integer
forall (f :: * -> *). Person f -> f Integer
age Person SBV
daughter 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
husband  SBV Integer -> SBV Integer -> SBV Integer
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
  SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ Person SBV -> SBV Integer
forall (f :: * -> *). Person f -> f Integer
age Person SBV
son 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
daughter SBool -> SBool -> SBool
.|| Person SBV -> SBV Integer
forall (f :: * -> *). Person f -> f Integer
age Person SBV
alice 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
brother

  -- One victim, one killer
  SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ [SBV Integer] -> SBV Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((Person SBV -> SBV Integer) -> [Person SBV] -> [SBV Integer]
forall a b. (a -> b) -> [a] -> [b]
map (\Person SBV
c -> SBool -> SBV Integer
forall a. (Ord a, Num 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)) [Person SBV]
chars) SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Integer
1 :: SInteger)
  SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ [SBV Integer] -> SBV Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((Person SBV -> SBV Integer) -> [Person SBV] -> [SBV Integer]
forall a b. (a -> b) -> [a] -> [b]
map (\Person SBV
c -> SBool -> SBV Integer
forall a. (Ord a, Num 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)) [Person SBV]
chars) SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Integer
1 :: SInteger)

  let ifVictim :: Person SBV -> SBool
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 -> SBool
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) -> SBool
every Person SBV -> SBool
f = [SBool] -> SBool
sAnd ((Person SBV -> SBool) -> [Person SBV] -> [SBool]
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  ((Person SBV -> SBool) -> [Person SBV] -> [SBool]
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.
  SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ (Person SBV -> SBool) -> SBool
some ((Person SBV -> SBool) -> SBool) -> (Person SBV -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \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
  SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ (Person SBV -> SBool) -> SBool
some ((Person SBV -> SBool) -> SBool) -> (Person SBV -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \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.
  SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ (Person SBV -> SBool) -> SBool
every ((Person SBV -> SBool) -> SBool) -> (Person SBV -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \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
  SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ (Person SBV -> SBool) -> SBool
every ((Person SBV -> SBool) -> SBool) -> (Person SBV -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \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.
  SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ Person SBV -> SBV Location
forall (f :: * -> *). Person f -> f Location
location Person SBV
daughter SBV Location -> SBV Location -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Location
sAlone SBool -> SBool -> SBool
.|| Person SBV -> SBV Location
forall (f :: * -> *). Person f -> f Location
location Person SBV
son SBV Location -> SBV Location -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Location
sAlone

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

  -- The victim has a twin
  SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ (Person SBV -> SBool) -> SBool
every ((Person SBV -> SBool) -> SBool) -> (Person SBV -> SBool) -> SBool
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 -> 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.
  SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ (Person SBV -> SBool) -> SBool
every ((Person SBV -> SBool) -> SBool) -> (Person SBV -> SBool) -> SBool
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 -> 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.
  SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ (Person SBV -> SBool) -> SBool
every ((Person SBV -> SBool) -> SBool) -> (Person SBV -> SBool) -> SBool
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
.=> 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
  SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ Person SBV -> SBV Integer
forall (f :: * -> *). Person f -> f Integer
age Person SBV
husband 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
brother
  SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ Person SBV -> SBV Integer
forall (f :: * -> *). Person f -> f Integer
age Person SBV
husband 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
alice

  Query [Person Const] -> Symbolic [Person Const]
forall a. Query a -> Symbolic a
query (Query [Person Const] -> Symbolic [Person Const])
-> Query [Person Const] -> Symbolic [Person Const]
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
                         [Person Const] -> Query [Person Const]
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
_   -> 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