    -----------------------------------------------------------------------------
    -- |
    -- 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, 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 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_
            SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. a -> SymbolicT IO a
    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 :: 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     48  Bar    Female  Bystander
    -- Husband   47  Beach  Male    Killer
    -- Brother   48  Beach  Male    Victim
    -- Daughter  21  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
       [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 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] -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ [SBV Integer] -> SBV Integer
    forall a. Num a => [a] -> a
    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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ [SBV Integer] -> SBV Integer
    forall a. Num a => [a] -> a
    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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. a -> QueryT IO a
    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