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

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
 Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish Methods(==) :: Color -> Color -> Bool #(/=) :: Color -> Color -> Bool # Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish 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 # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish Methods(<) :: Color -> Color -> Bool #(<=) :: Color -> Color -> Bool #(>) :: Color -> Color -> Bool #(>=) :: Color -> Color -> Bool #max :: Color -> Color -> Color #min :: Color -> Color -> Color # Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish Methods Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish MethodsshowsPrec :: Int -> Color -> ShowS #show :: Color -> String #showList :: [Color] -> ShowS # Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish Methods Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish MethodsisConcretely :: SBV Color -> (Color -> Bool) -> Bool Source #forall :: MonadSymbolic m => String -> m (SBV Color) Source #forall_ :: MonadSymbolic m => m (SBV Color) Source #mkForallVars :: MonadSymbolic m => Int -> m [SBV Color] Source #exists :: MonadSymbolic m => String -> m (SBV Color) Source #exists_ :: MonadSymbolic m => m (SBV Color) Source #mkExistVars :: MonadSymbolic m => Int -> m [SBV Color] Source #free :: MonadSymbolic m => String -> m (SBV Color) Source #free_ :: MonadSymbolic m => m (SBV Color) Source #mkFreeVars :: MonadSymbolic m => Int -> m [SBV Color] Source #symbolic :: MonadSymbolic m => String -> m (SBV Color) Source #symbolics :: MonadSymbolic m => [String] -> m [SBV Color] Source # Source # Make Color a symbolic value. Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish MethodsparseCVs :: [CV] -> Maybe (Color, [CV]) Source #cvtModel :: (Color -> Maybe b) -> Maybe (Color, [CV]) -> Maybe (b, [CV]) Source # Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish MethodssexprToVal :: SExpr -> Maybe Color Source #

Nationalities of the occupants

Constructors

 Briton Dane Swede Norwegian German
Instances
 Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish Methods Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish 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 # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish Methods Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish Methods Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish MethodsshowList :: [Nationality] -> ShowS # Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish Methods Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish Methodsforall :: MonadSymbolic m => String -> m (SBV Nationality) Source #forall_ :: MonadSymbolic m => m (SBV Nationality) Source #mkForallVars :: MonadSymbolic m => Int -> m [SBV Nationality] Source #exists :: MonadSymbolic m => String -> m (SBV Nationality) Source #exists_ :: MonadSymbolic m => m (SBV Nationality) Source #mkExistVars :: MonadSymbolic m => Int -> m [SBV Nationality] Source #free :: MonadSymbolic m => String -> m (SBV Nationality) Source #free_ :: MonadSymbolic m => m (SBV Nationality) Source #mkFreeVars :: MonadSymbolic m => Int -> m [SBV Nationality] Source #symbolic :: MonadSymbolic m => String -> m (SBV Nationality) Source #symbolics :: MonadSymbolic m => [String] -> m [SBV Nationality] Source # Source # Make Nationality a symbolic value. Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish MethodsparseCVs :: [CV] -> Maybe (Nationality, [CV]) Source #cvtModel :: (Nationality -> Maybe b) -> Maybe (Nationality, [CV]) -> Maybe (b, [CV]) Source # Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish MethodssexprToVal :: SExpr -> Maybe Nationality Source #

data Beverage Source #

Beverage choices

Constructors

 Tea Coffee Milk Beer Water
Instances
 Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish Methods Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish 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 # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish Methods(<) :: Beverage -> Beverage -> Bool #(>) :: Beverage -> Beverage -> Bool # Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish Methods Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish MethodsshowList :: [Beverage] -> ShowS # Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish Methods Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish MethodsisConcretely :: SBV Beverage -> (Beverage -> Bool) -> Bool Source #forall :: MonadSymbolic m => String -> m (SBV Beverage) Source #forall_ :: MonadSymbolic m => m (SBV Beverage) Source #mkForallVars :: MonadSymbolic m => Int -> m [SBV Beverage] Source #exists :: MonadSymbolic m => String -> m (SBV Beverage) Source #exists_ :: MonadSymbolic m => m (SBV Beverage) Source #mkExistVars :: MonadSymbolic m => Int -> m [SBV Beverage] Source #free :: MonadSymbolic m => String -> m (SBV Beverage) Source #free_ :: MonadSymbolic m => m (SBV Beverage) Source #mkFreeVars :: MonadSymbolic m => Int -> m [SBV Beverage] Source #symbolic :: MonadSymbolic m => String -> m (SBV Beverage) Source #symbolics :: MonadSymbolic m => [String] -> m [SBV Beverage] Source # Source # Make Beverage a symbolic value. Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish MethodsparseCVs :: [CV] -> Maybe (Beverage, [CV]) Source #cvtModel :: (Beverage -> Maybe b) -> Maybe (Beverage, [CV]) -> Maybe (b, [CV]) Source # Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish MethodssexprToVal :: SExpr -> Maybe Beverage Source #

data Pet Source #

Pets they keep

Constructors

 Dog Horse Cat Bird Fish
Instances
 Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish Methods(==) :: Pet -> Pet -> Bool #(/=) :: Pet -> Pet -> Bool # Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish 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 # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish 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 # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish Methods Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish MethodsshowsPrec :: Int -> Pet -> ShowS #show :: Pet -> String #showList :: [Pet] -> ShowS # Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish Methods Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish MethodsmkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV Pet) Source #isConcretely :: SBV Pet -> (Pet -> Bool) -> Bool Source #forall :: MonadSymbolic m => String -> m (SBV Pet) Source #forall_ :: MonadSymbolic m => m (SBV Pet) Source #mkForallVars :: MonadSymbolic m => Int -> m [SBV Pet] Source #exists :: MonadSymbolic m => String -> m (SBV Pet) Source #exists_ :: MonadSymbolic m => m (SBV Pet) Source #mkExistVars :: MonadSymbolic m => Int -> m [SBV Pet] Source #free :: MonadSymbolic m => String -> m (SBV Pet) Source #free_ :: MonadSymbolic m => m (SBV Pet) Source #mkFreeVars :: MonadSymbolic m => Int -> m [SBV Pet] Source #symbolic :: MonadSymbolic m => String -> m (SBV Pet) Source #symbolics :: MonadSymbolic m => [String] -> m [SBV Pet] Source # Source # Make Pet a symbolic value. Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish MethodsparseCVs :: [CV] -> Maybe (Pet, [CV]) Source #cvtModel :: (Pet -> Maybe b) -> Maybe (Pet, [CV]) -> Maybe (b, [CV]) Source # Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish MethodssexprToVal :: SExpr -> Maybe Pet Source #

data Sport Source #

Sports they engage in

Constructors

 Football Baseball Volleyball Hockey Tennis
Instances
 Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish Methods(==) :: Sport -> Sport -> Bool #(/=) :: Sport -> Sport -> Bool # Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish 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 # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish Methods(<) :: Sport -> Sport -> Bool #(<=) :: Sport -> Sport -> Bool #(>) :: Sport -> Sport -> Bool #(>=) :: Sport -> Sport -> Bool #max :: Sport -> Sport -> Sport #min :: Sport -> Sport -> Sport # Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish Methods Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish MethodsshowsPrec :: Int -> Sport -> ShowS #show :: Sport -> String #showList :: [Sport] -> ShowS # Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish Methods Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish MethodsisConcretely :: SBV Sport -> (Sport -> Bool) -> Bool Source #forall :: MonadSymbolic m => String -> m (SBV Sport) Source #forall_ :: MonadSymbolic m => m (SBV Sport) Source #mkForallVars :: MonadSymbolic m => Int -> m [SBV Sport] Source #exists :: MonadSymbolic m => String -> m (SBV Sport) Source #exists_ :: MonadSymbolic m => m (SBV Sport) Source #mkExistVars :: MonadSymbolic m => Int -> m [SBV Sport] Source #free :: MonadSymbolic m => String -> m (SBV Sport) Source #free_ :: MonadSymbolic m => m (SBV Sport) Source #mkFreeVars :: MonadSymbolic m => Int -> m [SBV Sport] Source #symbolic :: MonadSymbolic m => String -> m (SBV Sport) Source #symbolics :: MonadSymbolic m => [String] -> m [SBV Sport] Source # Source # Make Sport a symbolic value. Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish MethodsparseCVs :: [CV] -> Maybe (Sport, [CV]) Source #cvtModel :: (Sport -> Maybe b) -> Maybe (Sport, [CV]) -> Maybe (b, [CV]) Source # Source # Instance detailsDefined in Documentation.SBV.Examples.Puzzles.Fish MethodssexprToVal :: SExpr -> Maybe Sport 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!