sbv-9.1: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellSafe-Inferred
LanguageHaskell2010

Documentation.SBV.Examples.Puzzles.Fish

Description

Solves the following logic puzzle, attributed to Albert Einstein:

  • 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

Instances details
Data Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

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 :: forall r r'. (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 #

Read Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Show Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

showsPrec :: Int -> Color -> ShowS #

show :: Color -> String #

showList :: [Color] -> ShowS #

Eq Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

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

Ord Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

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 #

SymVal Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

HasKind Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

SatModel Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

parseCVs :: [CV] -> Maybe (Color, [CV]) Source #

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

type SColor = SBV Color Source #

Symbolic version of the type Color.

sBlue :: SBV Color Source #

Symbolic version of the constructor Blue.

sYellow :: SBV Color Source #

Symbolic version of the constructor Yellow.

sWhite :: SBV Color Source #

Symbolic version of the constructor White.

sGreen :: SBV Color Source #

Symbolic version of the constructor Green.

sRed :: SBV Color Source #

Symbolic version of the constructor Red.

data Nationality Source #

Nationalities of the occupants

Constructors

Briton 
Dane 
Swede 
Norwegian 
German 

Instances

Instances details
Data Nationality Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

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 :: forall r r'. (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 #

Read Nationality Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Show Nationality Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Eq Nationality Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Ord Nationality Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

SymVal Nationality Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

HasKind Nationality Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

SatModel Nationality Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

parseCVs :: [CV] -> Maybe (Nationality, [CV]) Source #

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

type SNationality = SBV Nationality Source #

Symbolic version of the type Nationality.

sGerman :: SBV Nationality Source #

Symbolic version of the constructor German.

sNorwegian :: SBV Nationality Source #

Symbolic version of the constructor Norwegian.

sSwede :: SBV Nationality Source #

Symbolic version of the constructor Swede.

sDane :: SBV Nationality Source #

Symbolic version of the constructor Dane.

sBriton :: SBV Nationality Source #

Symbolic version of the constructor Briton.

data Beverage Source #

Beverage choices

Constructors

Tea 
Coffee 
Milk 
Beer 
Water 

Instances

Instances details
Data Beverage Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

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 :: forall r r'. (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 #

Read Beverage Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Show Beverage Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Eq Beverage Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Ord Beverage Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

SymVal Beverage Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

HasKind Beverage Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

SatModel Beverage Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

parseCVs :: [CV] -> Maybe (Beverage, [CV]) Source #

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

type SBeverage = SBV Beverage Source #

Symbolic version of the type Beverage.

sWater :: SBV Beverage Source #

Symbolic version of the constructor Water.

sBeer :: SBV Beverage Source #

Symbolic version of the constructor Beer.

sMilk :: SBV Beverage Source #

Symbolic version of the constructor Milk.

sCoffee :: SBV Beverage Source #

Symbolic version of the constructor Coffee.

sTea :: SBV Beverage Source #

Symbolic version of the constructor Tea.

data Pet Source #

Pets they keep

Constructors

Dog 
Horse 
Cat 
Bird 
Fish 

Instances

Instances details
Data Pet Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

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 :: forall r r'. (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 #

Read Pet Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Show Pet Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

showsPrec :: Int -> Pet -> ShowS #

show :: Pet -> String #

showList :: [Pet] -> ShowS #

Eq Pet Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

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

Ord Pet Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

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 #

SymVal Pet Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

HasKind Pet Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

SatModel Pet Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

parseCVs :: [CV] -> Maybe (Pet, [CV]) Source #

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

type SPet = SBV Pet Source #

Symbolic version of the type Pet.

sFish :: SBV Pet Source #

Symbolic version of the constructor Fish.

sBird :: SBV Pet Source #

Symbolic version of the constructor Bird.

sCat :: SBV Pet Source #

Symbolic version of the constructor Cat.

sHorse :: SBV Pet Source #

Symbolic version of the constructor Horse.

sDog :: SBV Pet Source #

Symbolic version of the constructor Dog.

data Sport Source #

Sports they engage in

Instances

Instances details
Data Sport Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

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 :: forall r r'. (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 #

Read Sport Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Show Sport Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

showsPrec :: Int -> Sport -> ShowS #

show :: Sport -> String #

showList :: [Sport] -> ShowS #

Eq Sport Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

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

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

Ord Sport Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

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 #

SymVal Sport Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

HasKind Sport Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

SatModel Sport Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

Methods

parseCVs :: [CV] -> Maybe (Sport, [CV]) Source #

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

type SSport = SBV Sport Source #

Symbolic version of the type Sport.

sTennis :: SBV Sport Source #

Symbolic version of the constructor Tennis.

sHockey :: SBV Sport Source #

Symbolic version of the constructor Hockey.

sVolleyball :: SBV Sport Source #

Symbolic version of the constructor Volleyball.

sBaseball :: SBV Sport Source #

Symbolic version of the constructor Baseball.

sFootball :: SBV Sport Source #

Symbolic version of the constructor Football.

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! NB. We use the satTrackUFs configuration to indicate that the uninterpreted function changes do not matter for generating different values. All we care is that the fishOwner changes!