sbv-5.14: 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 # |
Methods (==) :: Color -> Color -> Bool # (/=) :: Color -> Color -> Bool #
Data Color Source # |

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Color -> c Color #

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

toConstr :: Color -> Constr #

dataTypeOf :: Color -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord Color Source # |
Methods compare :: Color -> Color -> Ordering # (<) :: Color -> Color -> Bool # (<=) :: Color -> Color -> Bool # (>) :: Color -> Color -> Bool # (>=) :: Color -> Color -> Bool # max :: Color -> Color -> Color # min :: Color -> Color -> Color #
Read Color Source # |
Methods readsPrec :: Int -> ReadS Color # readList :: ReadS [Color] # readPrec :: ReadPrec Color # readListPrec :: ReadPrec [Color] #
Show Color Source # |
Methods showsPrec :: Int -> Color -> ShowS # show :: Color -> String # showList :: [Color] -> ShowS #
HasKind Color Source # |
Methods kindOf :: Color -> Kind Source # hasSign :: Color -> Bool Source # intSizeOf :: Color -> Int Source # isBoolean :: Color -> Bool Source # isBounded :: Color -> Bool Source # isReal :: Color -> Bool Source # isFloat :: Color -> Bool Source # isDouble :: Color -> Bool Source # isInteger :: Color -> Bool Source # isUninterpreted :: Color -> Bool Source # showType :: Color -> String Source #
SymWord Color Source # |

Methods

forall :: String -> Symbolic (SBV Color) Source #

forall_ :: Symbolic (SBV Color) Source #

mkForallVars :: Int -> Symbolic [SBV Color] Source #

exists :: String -> Symbolic (SBV Color) Source #

exists_ :: Symbolic (SBV Color) Source #

mkExistVars :: Int -> Symbolic [SBV Color] Source #

free :: String -> Symbolic (SBV Color) Source #

free_ :: Symbolic (SBV Color) Source #

mkFreeVars :: Int -> Symbolic [SBV Color] Source #

symbolic :: String -> Symbolic (SBV Color) Source #

symbolics :: [String] -> Symbolic [SBV Color] Source #

literal :: Color -> SBV Color Source #

unliteral :: SBV Color -> Maybe Color Source #

fromCW :: CW -> Color Source #

isConcrete :: SBV Color -> Bool Source #

isSymbolic :: SBV Color -> Bool Source #

isConcretely :: SBV Color -> (Color -> Bool) -> Bool Source #

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Color) Source #

data Nationality Source #

Nationalities of the occupants

Constructors

Briton |
Dane |
Swede |
Norwegian |
German |

Instances

Eq Nationality Source # |
Methods (==) :: Nationality -> Nationality -> Bool # (/=) :: Nationality -> Nationality -> Bool #
Data Nationality Source # |

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Nationality -> c Nationality #

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

toConstr :: Nationality -> Constr #

dataTypeOf :: Nationality -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord Nationality Source # |
Methods compare :: Nationality -> Nationality -> Ordering # (<) :: Nationality -> Nationality -> Bool # (<=) :: Nationality -> Nationality -> Bool # (>) :: Nationality -> Nationality -> Bool # (>=) :: Nationality -> Nationality -> Bool # max :: Nationality -> Nationality -> Nationality # min :: Nationality -> Nationality -> Nationality #
Read Nationality Source # |
Methods readsPrec :: Int -> ReadS Nationality # readList :: ReadS [Nationality] # readPrec :: ReadPrec Nationality # readListPrec :: ReadPrec [Nationality] #
Show Nationality Source # |
Methods showsPrec :: Int -> Nationality -> ShowS # show :: Nationality -> String # showList :: [Nationality] -> ShowS #
HasKind Nationality Source # |

Methods

kindOf :: Nationality -> Kind Source #

hasSign :: Nationality -> Bool Source #

intSizeOf :: Nationality -> Int Source #

isBoolean :: Nationality -> Bool Source #

isBounded :: Nationality -> Bool Source #

isReal :: Nationality -> Bool Source #

isFloat :: Nationality -> Bool Source #

isDouble :: Nationality -> Bool Source #

isInteger :: Nationality -> Bool Source #

isUninterpreted :: Nationality -> Bool Source #

showType :: Nationality -> String Source #

SymWord Nationality Source # |

Methods

forall :: String -> Symbolic (SBV Nationality) Source #

forall_ :: Symbolic (SBV Nationality) Source #

mkForallVars :: Int -> Symbolic [SBV Nationality] Source #

exists :: String -> Symbolic (SBV Nationality) Source #

exists_ :: Symbolic (SBV Nationality) Source #

mkExistVars :: Int -> Symbolic [SBV Nationality] Source #

free :: String -> Symbolic (SBV Nationality) Source #

free_ :: Symbolic (SBV Nationality) Source #

mkFreeVars :: Int -> Symbolic [SBV Nationality] Source #

symbolic :: String -> Symbolic (SBV Nationality) Source #

symbolics :: [String] -> Symbolic [SBV Nationality] Source #

literal :: Nationality -> SBV Nationality Source #

unliteral :: SBV Nationality -> Maybe Nationality Source #

fromCW :: CW -> Nationality Source #

isConcrete :: SBV Nationality -> Bool Source #

isSymbolic :: SBV Nationality -> Bool Source #

isConcretely :: SBV Nationality -> (Nationality -> Bool) -> Bool Source #

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Nationality) Source #

data Beverage Source #

Beverage choices

Constructors

Tea |
Coffee |
Milk |
Beer |
Water |

Instances

Eq Beverage Source # |
Methods (==) :: Beverage -> Beverage -> Bool # (/=) :: Beverage -> Beverage -> Bool #
Data Beverage Source # |

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Beverage -> c Beverage #

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

toConstr :: Beverage -> Constr #

dataTypeOf :: Beverage -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord Beverage Source # |
Methods compare :: Beverage -> Beverage -> Ordering # (<) :: Beverage -> Beverage -> Bool # (<=) :: Beverage -> Beverage -> Bool # (>) :: Beverage -> Beverage -> Bool # (>=) :: Beverage -> Beverage -> Bool # max :: Beverage -> Beverage -> Beverage # min :: Beverage -> Beverage -> Beverage #
Read Beverage Source # |
Methods readsPrec :: Int -> ReadS Beverage # readList :: ReadS [Beverage] # readPrec :: ReadPrec Beverage # readListPrec :: ReadPrec [Beverage] #
Show Beverage Source # |
Methods showsPrec :: Int -> Beverage -> ShowS # show :: Beverage -> String # showList :: [Beverage] -> ShowS #
HasKind Beverage Source # |

Methods

kindOf :: Beverage -> Kind Source #

hasSign :: Beverage -> Bool Source #

intSizeOf :: Beverage -> Int Source #

isBoolean :: Beverage -> Bool Source #

isBounded :: Beverage -> Bool Source #

isReal :: Beverage -> Bool Source #

isFloat :: Beverage -> Bool Source #

isDouble :: Beverage -> Bool Source #

isInteger :: Beverage -> Bool Source #

isUninterpreted :: Beverage -> Bool Source #

showType :: Beverage -> String Source #

SymWord Beverage Source # |

Methods

forall :: String -> Symbolic (SBV Beverage) Source #

forall_ :: Symbolic (SBV Beverage) Source #

mkForallVars :: Int -> Symbolic [SBV Beverage] Source #

exists :: String -> Symbolic (SBV Beverage) Source #

exists_ :: Symbolic (SBV Beverage) Source #

mkExistVars :: Int -> Symbolic [SBV Beverage] Source #

free :: String -> Symbolic (SBV Beverage) Source #

free_ :: Symbolic (SBV Beverage) Source #

mkFreeVars :: Int -> Symbolic [SBV Beverage] Source #

symbolic :: String -> Symbolic (SBV Beverage) Source #

symbolics :: [String] -> Symbolic [SBV Beverage] Source #

literal :: Beverage -> SBV Beverage Source #

unliteral :: SBV Beverage -> Maybe Beverage Source #

fromCW :: CW -> Beverage Source #

isConcrete :: SBV Beverage -> Bool Source #

isSymbolic :: SBV Beverage -> Bool Source #

isConcretely :: SBV Beverage -> (Beverage -> Bool) -> Bool Source #

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Beverage) Source #

data Pet Source #

Pets they keep

Constructors

Dog |
Horse |
Cat |
Bird |
Fish |

Instances

Eq Pet Source # |
Methods (==) :: Pet -> Pet -> Bool # (/=) :: Pet -> Pet -> Bool #
Data Pet Source # |

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pet -> c Pet #

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

toConstr :: Pet -> Constr #

dataTypeOf :: Pet -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord Pet Source # |
Methods compare :: Pet -> Pet -> Ordering # (<) :: Pet -> Pet -> Bool # (<=) :: Pet -> Pet -> Bool # (>) :: Pet -> Pet -> Bool # (>=) :: Pet -> Pet -> Bool # max :: Pet -> Pet -> Pet # min :: Pet -> Pet -> Pet #
Read Pet Source # |
Methods readsPrec :: Int -> ReadS Pet # readList :: ReadS [Pet] # readPrec :: ReadPrec Pet # readListPrec :: ReadPrec [Pet] #
Show Pet Source # |
Methods showsPrec :: Int -> Pet -> ShowS # show :: Pet -> String # showList :: [Pet] -> ShowS #
HasKind Pet Source # |
Methods kindOf :: Pet -> Kind Source # hasSign :: Pet -> Bool Source # intSizeOf :: Pet -> Int Source # isBoolean :: Pet -> Bool Source # isBounded :: Pet -> Bool Source # isReal :: Pet -> Bool Source # isFloat :: Pet -> Bool Source # isDouble :: Pet -> Bool Source # isInteger :: Pet -> Bool Source # isUninterpreted :: Pet -> Bool Source # showType :: Pet -> String Source #
SymWord Pet Source # |

Methods

forall :: String -> Symbolic (SBV Pet) Source #

forall_ :: Symbolic (SBV Pet) Source #

mkForallVars :: Int -> Symbolic [SBV Pet] Source #

exists :: String -> Symbolic (SBV Pet) Source #

exists_ :: Symbolic (SBV Pet) Source #

mkExistVars :: Int -> Symbolic [SBV Pet] Source #

free :: String -> Symbolic (SBV Pet) Source #

free_ :: Symbolic (SBV Pet) Source #

mkFreeVars :: Int -> Symbolic [SBV Pet] Source #

symbolic :: String -> Symbolic (SBV Pet) Source #

symbolics :: [String] -> Symbolic [SBV Pet] Source #

literal :: Pet -> SBV Pet Source #

unliteral :: SBV Pet -> Maybe Pet Source #

fromCW :: CW -> Pet Source #

isConcrete :: SBV Pet -> Bool Source #

isSymbolic :: SBV Pet -> Bool Source #

isConcretely :: SBV Pet -> (Pet -> Bool) -> Bool Source #

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Pet) Source #

data Sport Source #

Sports they engage in

Constructors

Football |
Baseball |
Volleyball |
Hockey |
Tennis |

Instances

Eq Sport Source # |
Methods (==) :: Sport -> Sport -> Bool # (/=) :: Sport -> Sport -> Bool #
Data Sport Source # |

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sport -> c Sport #

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

toConstr :: Sport -> Constr #

dataTypeOf :: Sport -> DataType #

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

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

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

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

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

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

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

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

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

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

Ord Sport Source # |
Methods compare :: Sport -> Sport -> Ordering # (<) :: Sport -> Sport -> Bool # (<=) :: Sport -> Sport -> Bool # (>) :: Sport -> Sport -> Bool # (>=) :: Sport -> Sport -> Bool # max :: Sport -> Sport -> Sport # min :: Sport -> Sport -> Sport #
Read Sport Source # |
Methods readsPrec :: Int -> ReadS Sport # readList :: ReadS [Sport] # readPrec :: ReadPrec Sport # readListPrec :: ReadPrec [Sport] #
Show Sport Source # |
Methods showsPrec :: Int -> Sport -> ShowS # show :: Sport -> String # showList :: [Sport] -> ShowS #
HasKind Sport Source # |
Methods kindOf :: Sport -> Kind Source # hasSign :: Sport -> Bool Source # intSizeOf :: Sport -> Int Source # isBoolean :: Sport -> Bool Source # isBounded :: Sport -> Bool Source # isReal :: Sport -> Bool Source # isFloat :: Sport -> Bool Source # isDouble :: Sport -> Bool Source # isInteger :: Sport -> Bool Source # isUninterpreted :: Sport -> Bool Source # showType :: Sport -> String Source #
SymWord Sport Source # |

Methods

forall :: String -> Symbolic (SBV Sport) Source #

forall_ :: Symbolic (SBV Sport) Source #

mkForallVars :: Int -> Symbolic [SBV Sport] Source #

exists :: String -> Symbolic (SBV Sport) Source #

exists_ :: Symbolic (SBV Sport) Source #

mkExistVars :: Int -> Symbolic [SBV Sport] Source #

free :: String -> Symbolic (SBV Sport) Source #

free_ :: Symbolic (SBV Sport) Source #

mkFreeVars :: Int -> Symbolic [SBV Sport] Source #

symbolic :: String -> Symbolic (SBV Sport) Source #

symbolics :: [String] -> Symbolic [SBV Sport] Source #

literal :: Sport -> SBV Sport Source #

unliteral :: SBV Sport -> Maybe Sport Source #

fromCW :: CW -> Sport Source #

isConcrete :: SBV Sport -> Bool Source #

isSymbolic :: SBV Sport -> Bool Source #

isConcretely :: SBV Sport -> (Sport -> Bool) -> Bool Source #

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV 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!