Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

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

data Location
- = Bar
- | Beach
- | Alone
data Sex
- = Male
- | Female
data Role
- = Victim
- | Killer
- | Bystander
type SLocation = SBV Location
sAlone :: SBV Location
sBeach :: SBV Location
sBar :: SBV Location
type SSex = SBV Sex
sFemale :: SBV Sex
sMale :: SBV Sex
type SRole = SBV Role
sBystander :: SBV Role
sKiller :: SBV Role
sVictim :: SBV Role
data Person f = Person {
- nm :: String
- age :: f Integer
- location :: f Location
- sex :: f Sex
- role :: f Role
}
newtype Const a = Const {
- getConst :: a
}
newPerson :: String -> Symbolic (Person SBV)
getPerson :: Person SBV -> Query (Person Const)
killer :: IO ()
puzzle :: IO [Person Const]

Documentation

data Location Source #

Locations

Constructors

Bar
Beach
Alone

Instances

Instances details

Eq Location Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Murder Methods (==) :: Location -> Location -> Bool # (/=) :: Location -> Location -> Bool #
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 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 #
Read Location Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Murder Methods readsPrec :: Int -> ReadS Location # readList :: ReadS [Location] # readPrec :: ReadPrec Location # readListPrec :: ReadPrec [Location] #
Show Location Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Murder Methods showsPrec :: Int -> Location -> ShowS # show :: Location -> String # showList :: [Location] -> ShowS #
HasKind Location Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Murder Methods kindOf :: Location -> Kind Source # hasSign :: Location -> Bool Source # intSizeOf :: Location -> Int Source # isBoolean :: Location -> Bool Source # isBounded :: Location -> Bool Source # isReal :: Location -> Bool Source # isFloat :: Location -> Bool Source # isDouble :: Location -> Bool Source # isFP :: Location -> Bool Source # isUnbounded :: Location -> Bool Source # isUserSort :: Location -> Bool Source # isChar :: Location -> Bool Source # isString :: Location -> Bool Source # isList :: Location -> Bool Source # isSet :: Location -> Bool Source # isTuple :: Location -> Bool Source # isMaybe :: Location -> Bool Source # isEither :: Location -> Bool Source # showType :: Location -> String Source #
SymVal Location Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Murder Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Location) Source # literal :: Location -> SBV Location Source # fromCV :: CV -> Location Source # isConcretely :: SBV Location -> (Location -> Bool) -> Bool Source # forall :: MonadSymbolic m => String -> m (SBV Location) Source # forall_ :: MonadSymbolic m => m (SBV Location) Source # mkForallVars :: MonadSymbolic m => Int -> m [SBV Location] Source # exists :: MonadSymbolic m => String -> m (SBV Location) Source # exists_ :: MonadSymbolic m => m (SBV Location) Source # mkExistVars :: MonadSymbolic m => Int -> m [SBV Location] Source # free :: MonadSymbolic m => String -> m (SBV Location) Source # free_ :: MonadSymbolic m => m (SBV Location) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV Location] Source # symbolic :: MonadSymbolic m => String -> m (SBV Location) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV Location] Source # unliteral :: SBV Location -> Maybe Location Source # isConcrete :: SBV Location -> Bool Source # isSymbolic :: SBV Location -> Bool Source #
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 Methods readsPrec :: Int -> ReadS Sex # readList :: ReadS [Sex] # readPrec :: ReadPrec Sex # readListPrec :: ReadPrec [Sex] #
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 Methods kindOf :: Sex -> Kind Source # hasSign :: Sex -> Bool Source # intSizeOf :: Sex -> Int Source # isBoolean :: Sex -> Bool Source # isBounded :: Sex -> Bool Source # isReal :: Sex -> Bool Source # isFloat :: Sex -> Bool Source # isDouble :: Sex -> Bool Source # isFP :: Sex -> Bool Source # isUnbounded :: Sex -> Bool Source # isUserSort :: Sex -> Bool Source # isChar :: Sex -> Bool Source # isString :: Sex -> Bool Source # isList :: Sex -> Bool Source # isSet :: Sex -> Bool Source # isTuple :: Sex -> Bool Source # isMaybe :: Sex -> Bool Source # isEither :: Sex -> Bool Source # showType :: Sex -> String Source #
SymVal Sex Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Murder Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Sex) Source # literal :: Sex -> SBV Sex Source # fromCV :: CV -> Sex Source # isConcretely :: SBV Sex -> (Sex -> Bool) -> Bool Source # forall :: MonadSymbolic m => String -> m (SBV Sex) Source # forall_ :: MonadSymbolic m => m (SBV Sex) Source # mkForallVars :: MonadSymbolic m => Int -> m [SBV Sex] Source # exists :: MonadSymbolic m => String -> m (SBV Sex) Source # exists_ :: MonadSymbolic m => m (SBV Sex) Source # mkExistVars :: MonadSymbolic m => Int -> m [SBV Sex] Source # free :: MonadSymbolic m => String -> m (SBV Sex) Source # free_ :: MonadSymbolic m => m (SBV Sex) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV Sex] Source # symbolic :: MonadSymbolic m => String -> m (SBV Sex) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV Sex] Source # unliteral :: SBV Sex -> Maybe Sex Source # isConcrete :: SBV Sex -> Bool Source # isSymbolic :: SBV Sex -> Bool Source #
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 Methods readsPrec :: Int -> ReadS Role # readList :: ReadS [Role] # readPrec :: ReadPrec Role # readListPrec :: ReadPrec [Role] #
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 Methods kindOf :: Role -> Kind Source # hasSign :: Role -> Bool Source # intSizeOf :: Role -> Int Source # isBoolean :: Role -> Bool Source # isBounded :: Role -> Bool Source # isReal :: Role -> Bool Source # isFloat :: Role -> Bool Source # isDouble :: Role -> Bool Source # isFP :: Role -> Bool Source # isUnbounded :: Role -> Bool Source # isUserSort :: Role -> Bool Source # isChar :: Role -> Bool Source # isString :: Role -> Bool Source # isList :: Role -> Bool Source # isSet :: Role -> Bool Source # isTuple :: Role -> Bool Source # isMaybe :: Role -> Bool Source # isEither :: Role -> Bool Source # showType :: Role -> String Source #
SymVal Role Source #
Instance details Defined in Documentation.SBV.Examples.Puzzles.Murder Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Role) Source # literal :: Role -> SBV Role Source # fromCV :: CV -> Role Source # isConcretely :: SBV Role -> (Role -> Bool) -> Bool Source # forall :: MonadSymbolic m => String -> m (SBV Role) Source # forall_ :: MonadSymbolic m => m (SBV Role) Source # mkForallVars :: MonadSymbolic m => Int -> m [SBV Role] Source # exists :: MonadSymbolic m => String -> m (SBV Role) Source # exists_ :: MonadSymbolic m => m (SBV Role) Source # mkExistVars :: MonadSymbolic m => Int -> m [SBV Role] Source # free :: MonadSymbolic m => String -> m (SBV Role) Source # free_ :: MonadSymbolic m => m (SBV Role) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV Role] Source # symbolic :: MonadSymbolic m => String -> m (SBV Role) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV Role] Source # unliteral :: SBV Role -> Maybe Role Source # isConcrete :: SBV Role -> Bool Source # isSymbolic :: SBV Role -> Bool Source #
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 #

sAlone :: SBV Location Source #

sBeach :: SBV Location Source #

sBar :: SBV Location Source #

type SSex = SBV Sex Source #

sFemale :: SBV Sex Source #

sMale :: SBV Sex Source #

type SRole = SBV Role Source #

sBystander :: SBV Role Source #

sKiller :: SBV Role Source #

sVictim :: SBV Role 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 nm :: String age :: f Integer location :: f Location sex :: f Sex role :: f Role

Instances

Instances details

Show (Person Const) Source #	Show a person
Instance details Defined in Documentation.SBV.Examples.Puzzles.Murder Methods showsPrec :: Int -> Person Const -> ShowS # show :: Person Const -> String # showList :: [Person Const] -> ShowS #

newtype Const a Source #

Helper functor

Constructors

Const
Fields getConst :: a

Instances

Instances details

Show (Person Const) Source #	Show a person
Instance details 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) 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     47  Bar    Female  Bystander
Husband   46  Beach  Male    Killer
Brother   47  Beach  Male    Victim
Daughter  20  Alone  Female  Bystander
Son       20  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.