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

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

Documentation.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 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 # 
Show Color Source # 

Methods

showsPrec :: Int -> Color -> ShowS #

show :: Color -> String #

showList :: [Color] -> ShowS #

HasKind Color Source # 
SymWord Color Source # 
SatModel Color Source #

Make Color a symbolic value.

Methods

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

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

SMTValue Color Source # 

Methods

sexprToVal :: SExpr -> Maybe Color Source #

data Nationality Source #

Nationalities of the occupants

Constructors

Briton 
Dane 
Swede 
Norwegian 
German 

Instances

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

Make Nationality a symbolic value.

Methods

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

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

SMTValue Nationality Source # 

Methods

sexprToVal :: SExpr -> Maybe Nationality Source #

data Beverage Source #

Beverage choices

Constructors

Tea 
Coffee 
Milk 
Beer 
Water 

Instances

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

Make Beverage a symbolic value.

Methods

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

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

SMTValue Beverage Source # 

Methods

sexprToVal :: SExpr -> Maybe 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 # 
Show Pet Source # 

Methods

showsPrec :: Int -> Pet -> ShowS #

show :: Pet -> String #

showList :: [Pet] -> ShowS #

HasKind Pet Source # 
SymWord Pet Source # 
SatModel Pet Source #

Make Pet a symbolic value.

Methods

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

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

SMTValue Pet Source # 

Methods

sexprToVal :: SExpr -> Maybe Pet Source #

data Sport Source #

Sports they engage in

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

Methods

showsPrec :: Int -> Sport -> ShowS #

show :: Sport -> String #

showList :: [Sport] -> ShowS #

HasKind Sport Source # 
SymWord Sport Source # 
SatModel Sport Source #

Make Sport a symbolic value.

Methods

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

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

SMTValue Sport Source # 

Methods

sexprToVal :: SExpr -> Maybe 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!