Copyright | (c) Levent Erkok |
---|---|
License | BSD3 |
Maintainer | erkokl@gmail.com |
Stability | experimental |
Safe Haskell | None |
Language | Haskell2010 |
Documentation.SBV.Examples.Puzzles.Garden
Description
The origin of this puzzle is Raymond Smullyan's "The Flower Garden" riddle:
In a certain flower garden, each flower was either red, yellow, or blue, and all three colors were represented. A statistician once visited the garden and made the observation that whatever three flowers you picked, at least one of them was bound to be red. A second statistician visited the garden and made the observation that whatever three flowers you picked, at least one was bound to be yellow.
Two logic students heard about this and got into an argument. The first student said: “It therefore follows that whatever three flowers you pick, at least one is bound to be blue, doesn’t it?” The second student said: “Of course not!”
Which student was right, and why?
We slightly modify the puzzle. Assuming the first student is right, we use SBV to show that the garden must contain exactly 3 flowers. In any other case, the second student would be right.
Documentation
Colors of the flowers
Instances
Eq Color Source # | |
Data Color Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Garden 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.Garden | |
Show Color Source # | |
HasKind Color Source # | |
Defined in Documentation.SBV.Examples.Puzzles.Garden 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.Garden 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.Garden Methods sexprToVal :: SExpr -> Maybe Color Source # |
validPick :: SInteger -> Flower -> Flower -> Flower -> SBool Source #
Describe a valid pick of three flowers i
, j
, k
, assuming
we have n
flowers to start with. Essentially the numbers should
be within bounds and distinct.
count :: Color -> [Flower] -> SInteger Source #
Count the number of flowers that occur in a given set of flowers.
flowerCount :: IO () Source #
Solve the puzzle. We have:
>>>
flowerCount
Solution #1: N = 3 :: Integer This is the only solution. (Unique up to prefix existentials.)
So, a garden with 3 flowers is the only solution. (Note that we simply skip
over the prefix existentials and the assignments to uninterpreted function col
for model purposes here, as they don't represent a different solution.)