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

Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

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

Documentation

data Color #

Colors of houses

Constructors

Red 
Green 
White 
Yellow 
Blue 

Instances

Eq Color # 

Methods

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

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

Data Color # 

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 # 

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 # 
Show Color # 

Methods

showsPrec :: Int -> Color -> ShowS #

show :: Color -> String #

showList :: [Color] -> ShowS #

HasKind Color # 
SymWord Color # 
SatModel Color # 

Methods

parseCWs :: [CW] -> Maybe (Color, [CW]) #

cvtModel :: (Color -> Maybe b) -> Maybe (Color, [CW]) -> Maybe (b, [CW]) #

SMTValue Color # 

Methods

sexprToVal :: SExpr -> Maybe Color #

data Nationality #

Nationalities of the occupants

Constructors

Briton 
Dane 
Swede 
Norwegian 
German 

Instances

Eq Nationality # 
Data Nationality # 

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 # 
Read Nationality # 
Show Nationality # 
HasKind Nationality # 
SymWord Nationality # 
SatModel Nationality # 

Methods

parseCWs :: [CW] -> Maybe (Nationality, [CW]) #

cvtModel :: (Nationality -> Maybe b) -> Maybe (Nationality, [CW]) -> Maybe (b, [CW]) #

SMTValue Nationality # 

Methods

sexprToVal :: SExpr -> Maybe Nationality #

data Beverage #

Beverage choices

Constructors

Tea 
Coffee 
Milk 
Beer 
Water 

Instances

Eq Beverage # 
Data Beverage # 

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 # 
Read Beverage # 
Show Beverage # 
HasKind Beverage # 
SymWord Beverage # 
SatModel Beverage # 

Methods

parseCWs :: [CW] -> Maybe (Beverage, [CW]) #

cvtModel :: (Beverage -> Maybe b) -> Maybe (Beverage, [CW]) -> Maybe (b, [CW]) #

SMTValue Beverage # 

Methods

sexprToVal :: SExpr -> Maybe Beverage #

data Pet #

Pets they keep

Constructors

Dog 
Horse 
Cat 
Bird 
Fish 

Instances

Eq Pet # 

Methods

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

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

Data Pet # 

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 # 

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 # 
Show Pet # 

Methods

showsPrec :: Int -> Pet -> ShowS #

show :: Pet -> String #

showList :: [Pet] -> ShowS #

HasKind Pet # 
SymWord Pet # 
SatModel Pet # 

Methods

parseCWs :: [CW] -> Maybe (Pet, [CW]) #

cvtModel :: (Pet -> Maybe b) -> Maybe (Pet, [CW]) -> Maybe (b, [CW]) #

SMTValue Pet # 

Methods

sexprToVal :: SExpr -> Maybe Pet #

data Sport #

Sports they engage in

Instances

Eq Sport # 

Methods

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

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

Data Sport # 

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 # 

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 # 
Show Sport # 

Methods

showsPrec :: Int -> Sport -> ShowS #

show :: Sport -> String #

showList :: [Sport] -> ShowS #

HasKind Sport # 
SymWord Sport # 
SatModel Sport # 

Methods

parseCWs :: [CW] -> Maybe (Sport, [CW]) #

cvtModel :: (Sport -> Maybe b) -> Maybe (Sport, [CW]) -> Maybe (b, [CW]) #

SMTValue Sport # 

Methods

sexprToVal :: SExpr -> Maybe Sport #

fishOwner :: IO () #

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!