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

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

Data.SBV.Examples.Puzzles.Fish

Description

Solves the following logic puzzle:

- The Briton lives in the red house.
- The Swede keeps dogs as pets.
- The Dane drinks tea.
- The green house is left to the white house.
- The owner of the green house drinks coffee.
- The person who plays football rears birds.
- The owner of the yellow house plays baseball.
- The man living in the center house drinks milk.
- The Norwegian lives in the first house.
- The man who plays volleyball lives next to the one who keeps cats.
- The man who keeps the horse lives next to the one who plays baseball.
- The owner who plays tennis drinks beer.
- The German plays hockey.
- The Norwegian lives next to the blue house.
- The man who plays volleyball has a neighbor who drinks water.

Who owns the fish?

Synopsis

- data Color
  - = Red
  - | Green
  - | White
  - | Yellow
  - | Blue
- data Nationality
  - = Briton
  - | Dane
  - | Swede
  - | Norwegian
  - | German
- data Beverage
  - = Tea
  - | Coffee
  - | Milk
  - | Beer
  - | Water
- data Pet
  - = Dog
  - | Horse
  - | Cat
  - | Bird
  - | Fish
- data Sport
  - = Football
  - | Baseball
  - | Volleyball
  - | Hockey
  - | Tennis
- fishOwner :: IO ()

# Documentation

data Color Source

Colors of houses

Constructors

Red |
Green |
White |
Yellow |
Blue |

Instances

Eq Color Source |
Data Color Source |
Ord Color Source |
Read Color Source |
Show Color Source |
HasKind Color Source |
SymWord Color Source |

data Nationality Source

Nationalities of the occupants

Constructors

Briton |
Dane |
Swede |
Norwegian |
German |

Instances

Eq Nationality Source |
Data Nationality Source |
Ord Nationality Source |
Read Nationality Source |
Show Nationality Source |
HasKind Nationality Source |
SymWord Nationality Source |

data Beverage Source

Beverage choices

Constructors

Tea |
Coffee |
Milk |
Beer |
Water |

Instances

Eq Beverage Source |
Data Beverage Source |
Ord Beverage Source |
Read Beverage Source |
Show Beverage Source |
HasKind Beverage Source |
SymWord Beverage Source |

data Pet Source

Pets they keep

Constructors

Dog |
Horse |
Cat |
Bird |
Fish |

Instances

Eq Pet Source |
Data Pet Source |
Ord Pet Source |
Read Pet Source |
Show Pet Source |
HasKind Pet Source |
SymWord Pet Source |

data Sport Source

Sports they engage in

Constructors

Football |
Baseball |
Volleyball |
Hockey |
Tennis |

Instances

Eq Sport Source |
Data Sport Source |
Ord Sport Source |
Read Sport Source |
Show Sport Source |
HasKind Sport Source |
SymWord Sport Source |

fishOwner :: IO () Source

We have:

    >>> fishOwner
    German

It's not hard to modify this program to grab the values of all the assignments, i.e., the full solution to the puzzle. We leave that as an exercise to the interested reader!