sbv-9.1: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellSafe-Inferred
LanguageHaskell2010

Documentation.SBV.Examples.Puzzles.Murder

Description

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?
Synopsis

Documentation

data Location Source #

Locations

Constructors

Bar 
Beach 
Alone 

Instances

Instances details
Data Location Source # 
Instance details

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 Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

Show Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

Eq Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

Ord Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

SymVal Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

HasKind Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

SatModel Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

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

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

data Sex Source #

Sexes

Constructors

Male 
Female 

Instances

Instances details
Data Sex Source # 
Instance details

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 Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

Show Sex Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

showsPrec :: Int -> Sex -> ShowS #

show :: Sex -> String #

showList :: [Sex] -> ShowS #

Eq Sex Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

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

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

Ord Sex Source # 
Instance details

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 Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

HasKind Sex Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

SatModel Sex Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

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

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

data Role Source #

Roles

Constructors

Victim 
Killer 
Bystander 

Instances

Instances details
Data Role Source # 
Instance details

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 Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

Show Role Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

showsPrec :: Int -> Role -> ShowS #

show :: Role -> String #

showList :: [Role] -> ShowS #

Eq Role Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

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

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

Ord Role Source # 
Instance details

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 Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

HasKind Role Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

SatModel Role Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

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

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

type SLocation = SBV Location Source #

Symbolic version of the type Location.

sAlone :: SBV Location Source #

Symbolic version of the constructor Alone.

sBeach :: SBV Location Source #

Symbolic version of the constructor Beach.

sBar :: SBV Location Source #

Symbolic version of the constructor Bar.

type SSex = SBV Sex Source #

Symbolic version of the type Sex.

sFemale :: SBV Sex Source #

Symbolic version of the constructor Female.

sMale :: SBV Sex Source #

Symbolic version of the constructor Male.

type SRole = SBV Role Source #

Symbolic version of the type Role.

sBystander :: SBV Role Source #

Symbolic version of the constructor Bystander.

sKiller :: SBV Role Source #

Symbolic version of the constructor Killer.

sVictim :: SBV Role Source #

Symbolic version of the constructor Victim.

data Person f Source #

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

Instances

Instances details
Show (Person Const) Source #

Show a person

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

newtype Const a Source #

Helper functor

Constructors

Const 

Fields

Instances

Instances details
Show (Person Const) Source #

Show a person

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

newPerson :: String -> Symbolic (Person SBV) Source #

Create a new symbolic person

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

Get the concrete value of the person in the model

killer :: IO () Source #

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] Source #

Constraints of the puzzle, coded following the English description.