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

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

Colors of houses

Constructors

 Red Green White Yellow Blue

Instances

 Source # Methods(==) :: Color -> Color -> Bool #(/=) :: Color -> Color -> Bool # Source # Methodsgfoldl :: (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 #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 # Source # Methods(<) :: Color -> Color -> Bool #(<=) :: Color -> Color -> Bool #(>) :: Color -> Color -> Bool #(>=) :: Color -> Color -> Bool #max :: Color -> Color -> Color #min :: Color -> Color -> Color # Source # Methods Source # MethodsshowsPrec :: Int -> Color -> ShowS #show :: Color -> String #showList :: [Color] -> ShowS # Source # Methods Source # Methodssymbolics :: [String] -> Symbolic [SBV Color] Source #isConcretely :: SBV Color -> (Color -> Bool) -> Bool Source #

Nationalities of the occupants

Constructors

 Briton Dane Swede Norwegian German

Instances

 Source # Methods Source # Methodsgfoldl :: (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 #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 # Source # Methods Source # Methods Source # MethodsshowList :: [Nationality] -> ShowS # Source # Methods Source # Methods

data Beverage Source #

Beverage choices

Constructors

 Tea Coffee Milk Beer Water

Instances

 Source # Methods Source # Methodsgfoldl :: (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 #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 # Source # Methods(<) :: Beverage -> Beverage -> Bool #(>) :: Beverage -> Beverage -> Bool # Source # Methods Source # MethodsshowList :: [Beverage] -> ShowS # Source # Methods Source # MethodsisConcretely :: SBV Beverage -> (Beverage -> Bool) -> Bool Source #

data Pet Source #

Pets they keep

Constructors

 Dog Horse Cat Bird Fish

Instances

 Source # Methods(==) :: Pet -> Pet -> Bool #(/=) :: Pet -> Pet -> Bool # Source # Methodsgfoldl :: (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 #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 # Source # Methodscompare :: Pet -> Pet -> Ordering #(<) :: Pet -> Pet -> Bool #(<=) :: Pet -> Pet -> Bool #(>) :: Pet -> Pet -> Bool #(>=) :: Pet -> Pet -> Bool #max :: Pet -> Pet -> Pet #min :: Pet -> Pet -> Pet # Source # Methods Source # MethodsshowsPrec :: Int -> Pet -> ShowS #show :: Pet -> String #showList :: [Pet] -> ShowS # Source # Methods Source # Methodssymbolics :: [String] -> Symbolic [SBV Pet] Source #isConcretely :: SBV Pet -> (Pet -> Bool) -> Bool Source #

data Sport Source #

Sports they engage in

Constructors

 Football Baseball Volleyball Hockey Tennis

Instances

 Source # Methods(==) :: Sport -> Sport -> Bool #(/=) :: Sport -> Sport -> Bool # Source # Methodsgfoldl :: (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 #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 # Source # Methods(<) :: Sport -> Sport -> Bool #(<=) :: Sport -> Sport -> Bool #(>) :: Sport -> Sport -> Bool #(>=) :: Sport -> Sport -> Bool #max :: Sport -> Sport -> Sport #min :: Sport -> Sport -> Sport # Source # Methods Source # MethodsshowsPrec :: Int -> Sport -> ShowS #show :: Sport -> String #showList :: [Sport] -> ShowS # Source # Methods Source # Methodssymbolics :: [String] -> Symbolic [SBV Sport] Source #isConcretely :: SBV Sport -> (Sport -> Bool) -> Bool 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!