sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
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

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

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

toConstr :: Location -> Constr Source #

dataTypeOf :: Location -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Read Location Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Murder Methods readsPrec :: Int -> ReadS Location Source # readList :: ReadS [Location] Source # readPrec :: ReadPrec Location Source # readListPrec :: ReadPrec [Location] Source #
Show Location Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Murder Methods showsPrec :: Int -> Location -> ShowS Source # show :: Location -> String Source # showList :: [Location] -> ShowS Source #
Eq Location Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Murder Methods (==) :: Location -> Location -> Bool Source # (/=) :: Location -> Location -> Bool Source #
Ord Location Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Murder

Methods

compare :: Location -> Location -> Ordering Source #

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

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

(>) :: Location -> Location -> Bool Source #

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

max :: Location -> Location -> Location Source #

min :: Location -> Location -> Location 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 #

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 #

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 #

isRational :: 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 #

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

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

toConstr :: Sex -> Constr Source #

dataTypeOf :: Sex -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Read Sex Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Murder Methods readsPrec :: Int -> ReadS Sex Source # readList :: ReadS [Sex] Source # readPrec :: ReadPrec Sex Source # readListPrec :: ReadPrec [Sex] Source #
Show Sex Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Murder Methods showsPrec :: Int -> Sex -> ShowS Source # show :: Sex -> String Source # showList :: [Sex] -> ShowS Source #
Eq Sex Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Murder Methods (==) :: Sex -> Sex -> Bool Source # (/=) :: Sex -> Sex -> Bool Source #
Ord Sex Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Murder Methods compare :: Sex -> Sex -> Ordering Source # (<) :: Sex -> Sex -> Bool Source # (<=) :: Sex -> Sex -> Bool Source # (>) :: Sex -> Sex -> Bool Source # (>=) :: Sex -> Sex -> Bool Source # max :: Sex -> Sex -> Sex Source # min :: Sex -> Sex -> Sex 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 #

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 #

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 #

isRational :: 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 #

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

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

toConstr :: Role -> Constr Source #

dataTypeOf :: Role -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Read Role Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Murder Methods readsPrec :: Int -> ReadS Role Source # readList :: ReadS [Role] Source # readPrec :: ReadPrec Role Source # readListPrec :: ReadPrec [Role] Source #
Show Role Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Murder Methods showsPrec :: Int -> Role -> ShowS Source # show :: Role -> String Source # showList :: [Role] -> ShowS Source #
Eq Role Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Murder Methods (==) :: Role -> Role -> Bool Source # (/=) :: Role -> Role -> Bool Source #
Ord Role Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Murder Methods compare :: Role -> Role -> Ordering Source # (<) :: Role -> Role -> Bool Source # (<=) :: Role -> Role -> Bool Source # (>) :: Role -> Role -> Bool Source # (>=) :: Role -> Role -> Bool Source # max :: Role -> Role -> Role Source # min :: Role -> Role -> Role 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 #

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 #

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 #

isRational :: 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 #

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

- 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 Source # show :: Person Const -> String Source # showList :: [Person Const] -> ShowS Source #

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 Source # show :: Person Const -> String Source # showList :: [Person Const] -> ShowS Source #

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  21  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.