Copyright | (c) Levent Erkok |
---|---|
License | BSD3 |
Maintainer | erkokl@gmail.com |
Stability | experimental |
Safe Haskell | None |
Language | Haskell2010 |
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?
Documentation
Colors of houses
Instances
Eq Color Source # | |
Data Color Source # | |
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 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 | |
Ord Color Source # | |
Read Color Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Fish | |
Show Color Source # | |
HasKind Color Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Fish Methods kindOf :: Color -> Kind Source # hasSign :: Color -> Bool Source # intSizeOf :: Color -> Int Source # isBoolean :: Color -> Bool Source # isBounded :: Color -> Bool Source # isReal :: Color -> Bool Source # isFloat :: Color -> Bool Source # isDouble :: Color -> Bool Source # isUnbounded :: Color -> Bool Source # isUninterpreted :: Color -> Bool Source # isChar :: Color -> Bool Source # isString :: Color -> Bool Source # isList :: Color -> Bool Source # isSet :: Color -> Bool Source # isTuple :: Color -> Bool Source # isMaybe :: Color -> Bool Source # | |
SymVal Color Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Fish Methods mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV Color) Source # literal :: Color -> SBV Color Source # fromCV :: CV -> Color Source # isConcretely :: 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 # unliteral :: SBV Color -> Maybe Color Source # isConcrete :: SBV Color -> Bool Source # isSymbolic :: SBV Color -> Bool Source # | |
SatModel Color Source # | Make |
SMTValue Color Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Fish Methods sexprToVal :: SExpr -> Maybe Color Source # |
data Nationality Source #
Nationalities of the occupants
Instances
Beverage choices
Instances
Pets they keep
Instances
Eq Pet Source # | |
Data Pet Source # | |
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 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 | |
Ord Pet Source # | |
Read Pet Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Fish | |
Show Pet Source # | |
HasKind Pet Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Fish Methods kindOf :: Pet -> Kind Source # hasSign :: Pet -> Bool Source # intSizeOf :: Pet -> Int Source # isBoolean :: Pet -> Bool Source # isBounded :: Pet -> Bool Source # isReal :: Pet -> Bool Source # isFloat :: Pet -> Bool Source # isDouble :: Pet -> Bool Source # isUnbounded :: Pet -> Bool Source # isUninterpreted :: Pet -> Bool Source # isChar :: Pet -> Bool Source # isString :: Pet -> Bool Source # isList :: Pet -> Bool Source # isTuple :: Pet -> Bool Source # isMaybe :: Pet -> Bool Source # | |
SymVal Pet Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Fish Methods mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV Pet) Source # literal :: Pet -> 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 # unliteral :: SBV Pet -> Maybe Pet Source # isConcrete :: SBV Pet -> Bool Source # isSymbolic :: SBV Pet -> Bool Source # | |
SatModel Pet Source # | Make |
SMTValue Pet Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Fish Methods sexprToVal :: SExpr -> Maybe Pet Source # |
Sports they engage in
Constructors
Football | |
Baseball | |
Volleyball | |
Hockey | |
Tennis |
Instances
Eq Sport Source # | |
Data Sport Source # | |
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 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 | |
Ord Sport Source # | |
Read Sport Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Fish | |
Show Sport Source # | |
HasKind Sport Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Fish Methods kindOf :: Sport -> Kind Source # hasSign :: Sport -> Bool Source # intSizeOf :: Sport -> Int Source # isBoolean :: Sport -> Bool Source # isBounded :: Sport -> Bool Source # isReal :: Sport -> Bool Source # isFloat :: Sport -> Bool Source # isDouble :: Sport -> Bool Source # isUnbounded :: Sport -> Bool Source # isUninterpreted :: Sport -> Bool Source # isChar :: Sport -> Bool Source # isString :: Sport -> Bool Source # isList :: Sport -> Bool Source # isSet :: Sport -> Bool Source # isTuple :: Sport -> Bool Source # isMaybe :: Sport -> Bool Source # | |
SymVal Sport Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Fish Methods mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV Sport) Source # literal :: Sport -> SBV Sport Source # fromCV :: CV -> Sport Source # isConcretely :: 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 # unliteral :: SBV Sport -> Maybe Sport Source # isConcrete :: SBV Sport -> Bool Source # isSymbolic :: SBV Sport -> Bool Source # | |
SatModel Sport Source # | Make |
SMTValue Sport Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Fish Methods sexprToVal :: 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!