Documentation.SBV.Examples.Puzzles.Murder

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?

Documentation

data Location

Locations

Constructors

Bar

Beach

Alone

Instances

Data Location

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Location -> c Location

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Location

toConstr :: Location -> Constr

dataTypeOf :: Location -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Location)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Location)

gmapT :: (forall b. Data b => b -> b) -> Location -> Location

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Location -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Location -> r

gmapQ :: (forall d. Data d => d -> u) -> Location -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Location -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Location -> m Location

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Location -> m Location

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Location -> m Location

Read Location

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

readsPrec :: Int -> ReadS Location

readList :: ReadS [Location]

readPrec :: ReadPrec Location

readListPrec :: ReadPrec [Location]

Show Location

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

showsPrec :: Int -> Location -> ShowS

show :: Location -> String

showList :: [Location] -> ShowS

Eq Location

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

(==) :: Location -> Location -> Bool

(/=) :: Location -> Location -> Bool

Ord Location

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

compare :: Location -> Location -> Ordering

(<) :: Location -> Location -> Bool

(<=) :: Location -> Location -> Bool

(>) :: Location -> Location -> Bool

(>=) :: Location -> Location -> Bool

max :: Location -> Location -> Location

min :: Location -> Location -> Location

SymVal Location

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Location)

literal :: Location -> SBV Location

fromCV :: CV -> Location

isConcretely :: SBV Location -> (Location -> Bool) -> Bool

sbvForall :: MonadSymbolic m => String -> m (SBV Location)

sbvForall_ :: MonadSymbolic m => m (SBV Location)

mkForallVars :: MonadSymbolic m => Int -> m [SBV Location]

sbvExists :: MonadSymbolic m => String -> m (SBV Location)

sbvExists_ :: MonadSymbolic m => m (SBV Location)

mkExistVars :: MonadSymbolic m => Int -> m [SBV Location]

free :: MonadSymbolic m => String -> m (SBV Location)

free_ :: MonadSymbolic m => m (SBV Location)

mkFreeVars :: MonadSymbolic m => Int -> m [SBV Location]

symbolic :: MonadSymbolic m => String -> m (SBV Location)

symbolics :: MonadSymbolic m => [String] -> m [SBV Location]

unliteral :: SBV Location -> Maybe Location

isConcrete :: SBV Location -> Bool

isSymbolic :: SBV Location -> Bool

HasKind Location

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

kindOf :: Location -> Kind

hasSign :: Location -> Bool

intSizeOf :: Location -> Int

isBoolean :: Location -> Bool

isBounded :: Location -> Bool

isReal :: Location -> Bool

isFloat :: Location -> Bool

isDouble :: Location -> Bool

isRational :: Location -> Bool

isFP :: Location -> Bool

isUnbounded :: Location -> Bool

isUserSort :: Location -> Bool

isChar :: Location -> Bool

isString :: Location -> Bool

isList :: Location -> Bool

isSet :: Location -> Bool

isTuple :: Location -> Bool

isMaybe :: Location -> Bool

isEither :: Location -> Bool

showType :: Location -> String

SatModel Location

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

parseCVs :: [CV] -> Maybe (Location, [CV])

cvtModel :: (Location -> Maybe b) -> Maybe (Location, [CV]) -> Maybe (b, [CV])

data Sex

Sexes

Constructors

Male

Female

Instances

Data Sex

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sex -> c Sex

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sex

toConstr :: Sex -> Constr

dataTypeOf :: Sex -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Sex)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sex)

gmapT :: (forall b. Data b => b -> b) -> Sex -> Sex

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sex -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sex -> r

gmapQ :: (forall d. Data d => d -> u) -> Sex -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Sex -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sex -> m Sex

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sex -> m Sex

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sex -> m Sex

Read Sex

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

readsPrec :: Int -> ReadS Sex

readList :: ReadS [Sex]

readPrec :: ReadPrec Sex

readListPrec :: ReadPrec [Sex]

Show Sex

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

showsPrec :: Int -> Sex -> ShowS

show :: Sex -> String

showList :: [Sex] -> ShowS

Eq Sex

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

(==) :: Sex -> Sex -> Bool

(/=) :: Sex -> Sex -> Bool

Ord Sex

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

compare :: Sex -> Sex -> Ordering

(<) :: Sex -> Sex -> Bool

(<=) :: Sex -> Sex -> Bool

(>) :: Sex -> Sex -> Bool

(>=) :: Sex -> Sex -> Bool

max :: Sex -> Sex -> Sex

min :: Sex -> Sex -> Sex

SymVal Sex

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Sex)

literal :: Sex -> SBV Sex

fromCV :: CV -> Sex

isConcretely :: SBV Sex -> (Sex -> Bool) -> Bool

sbvForall :: MonadSymbolic m => String -> m (SBV Sex)

sbvForall_ :: MonadSymbolic m => m (SBV Sex)

mkForallVars :: MonadSymbolic m => Int -> m [SBV Sex]

sbvExists :: MonadSymbolic m => String -> m (SBV Sex)

sbvExists_ :: MonadSymbolic m => m (SBV Sex)

mkExistVars :: MonadSymbolic m => Int -> m [SBV Sex]

free :: MonadSymbolic m => String -> m (SBV Sex)

free_ :: MonadSymbolic m => m (SBV Sex)

mkFreeVars :: MonadSymbolic m => Int -> m [SBV Sex]

symbolic :: MonadSymbolic m => String -> m (SBV Sex)

symbolics :: MonadSymbolic m => [String] -> m [SBV Sex]

unliteral :: SBV Sex -> Maybe Sex

isConcrete :: SBV Sex -> Bool

isSymbolic :: SBV Sex -> Bool

HasKind Sex

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

kindOf :: Sex -> Kind

hasSign :: Sex -> Bool

intSizeOf :: Sex -> Int

isBoolean :: Sex -> Bool

isBounded :: Sex -> Bool

isReal :: Sex -> Bool

isFloat :: Sex -> Bool

isDouble :: Sex -> Bool

isRational :: Sex -> Bool

isFP :: Sex -> Bool

isUnbounded :: Sex -> Bool

isUserSort :: Sex -> Bool

isChar :: Sex -> Bool

isString :: Sex -> Bool

isList :: Sex -> Bool

isSet :: Sex -> Bool

isTuple :: Sex -> Bool

isMaybe :: Sex -> Bool

isEither :: Sex -> Bool

showType :: Sex -> String

SatModel Sex

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

parseCVs :: [CV] -> Maybe (Sex, [CV])

cvtModel :: (Sex -> Maybe b) -> Maybe (Sex, [CV]) -> Maybe (b, [CV])

data Role

Roles

Constructors

Victim

Killer

Bystander

Instances

Data Role

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Role -> c Role

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Role

toConstr :: Role -> Constr

dataTypeOf :: Role -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Role)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Role)

gmapT :: (forall b. Data b => b -> b) -> Role -> Role

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r

gmapQ :: (forall d. Data d => d -> u) -> Role -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Role -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Role -> m Role

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role

Read Role

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

readsPrec :: Int -> ReadS Role

readList :: ReadS [Role]

readPrec :: ReadPrec Role

readListPrec :: ReadPrec [Role]

Show Role

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

showsPrec :: Int -> Role -> ShowS

show :: Role -> String

showList :: [Role] -> ShowS

Eq Role

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

(==) :: Role -> Role -> Bool

(/=) :: Role -> Role -> Bool

Ord Role

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

compare :: Role -> Role -> Ordering

(<) :: Role -> Role -> Bool

(<=) :: Role -> Role -> Bool

(>) :: Role -> Role -> Bool

(>=) :: Role -> Role -> Bool

max :: Role -> Role -> Role

min :: Role -> Role -> Role

SymVal Role

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Role)

literal :: Role -> SBV Role

fromCV :: CV -> Role

isConcretely :: SBV Role -> (Role -> Bool) -> Bool

sbvForall :: MonadSymbolic m => String -> m (SBV Role)

sbvForall_ :: MonadSymbolic m => m (SBV Role)

mkForallVars :: MonadSymbolic m => Int -> m [SBV Role]

sbvExists :: MonadSymbolic m => String -> m (SBV Role)

sbvExists_ :: MonadSymbolic m => m (SBV Role)

mkExistVars :: MonadSymbolic m => Int -> m [SBV Role]

free :: MonadSymbolic m => String -> m (SBV Role)

free_ :: MonadSymbolic m => m (SBV Role)

mkFreeVars :: MonadSymbolic m => Int -> m [SBV Role]

symbolic :: MonadSymbolic m => String -> m (SBV Role)

symbolics :: MonadSymbolic m => [String] -> m [SBV Role]

unliteral :: SBV Role -> Maybe Role

isConcrete :: SBV Role -> Bool

isSymbolic :: SBV Role -> Bool

HasKind Role

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

kindOf :: Role -> Kind

hasSign :: Role -> Bool

intSizeOf :: Role -> Int

isBoolean :: Role -> Bool

isBounded :: Role -> Bool

isReal :: Role -> Bool

isFloat :: Role -> Bool

isDouble :: Role -> Bool

isRational :: Role -> Bool

isFP :: Role -> Bool

isUnbounded :: Role -> Bool

isUserSort :: Role -> Bool

isChar :: Role -> Bool

isString :: Role -> Bool

isList :: Role -> Bool

isSet :: Role -> Bool

isTuple :: Role -> Bool

isMaybe :: Role -> Bool

isEither :: Role -> Bool

showType :: Role -> String

SatModel Role

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

parseCVs :: [CV] -> Maybe (Role, [CV])

cvtModel :: (Role -> Maybe b) -> Maybe (Role, [CV]) -> Maybe (b, [CV])

type SLocation = SBV Location

Symbolic version of the type Location.

sAlone :: SBV Location

Symbolic version of the constructor Alone.

sBeach :: SBV Location

Symbolic version of the constructor Beach.

sBar :: SBV Location

Symbolic version of the constructor Bar.

type SSex = SBV Sex

Symbolic version of the type Sex.

sFemale :: SBV Sex

Symbolic version of the constructor Female.

sMale :: SBV Sex

Symbolic version of the constructor Male.

type SRole = SBV Role

Symbolic version of the type Role.

sBystander :: SBV Role

Symbolic version of the constructor Bystander.

sKiller :: SBV Role

Symbolic version of the constructor Killer.

sVictim :: SBV Role

Symbolic version of the constructor Victim.

data Person f

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.

Constructors

Person

Fields

• nm :: String
• age :: f Integer
• location :: f Location
• sex :: f Sex
• role :: f Role

Instances

Show (Person Const)

Show a person

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

showsPrec :: Int -> Person Const -> ShowS

show :: Person Const -> String

showList :: [Person Const] -> ShowS

newtype Const a

Helper functor

Constructors

Const

Fields

• getConst :: a

Instances

Show (Person Const)

Show a person

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

showsPrec :: Int -> Person Const -> ShowS

show :: Person Const -> String

showList :: [Person Const] -> ShowS

newPerson :: String -> Symbolic (Person SBV)

Create a new symbolic person

getPerson :: Person SBV -> Query (Person Const)

Get the concrete value of the person in the model

killer :: IO ()

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.

puzzle :: IO [Person Const]

Constraints of the puzzle, coded following the English description.