sbv-9.0: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
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
Eq Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

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 #

Ord Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

Read Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

Show Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

HasKind Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

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

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

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

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

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 #

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 #

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 #

HasKind Sex Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

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

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

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

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

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 #

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 #

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 #

HasKind Role Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

SymVal 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 #

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.