Documentation.SBV.Examples.Puzzles.Garden

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

data Color

Colors of the flowers

Constructors

Red

Yellow

Blue

Instances

Data Color

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

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

Defined in Documentation.SBV.Examples.Puzzles.Garden

Methods

readsPrec :: Int -> ReadS Color

readList :: ReadS [Color]

readPrec :: ReadPrec Color

readListPrec :: ReadPrec [Color]

Show Color

Defined in Documentation.SBV.Examples.Puzzles.Garden

Methods

showsPrec :: Int -> Color -> ShowS

show :: Color -> String

showList :: [Color] -> ShowS

Eq Color

Defined in Documentation.SBV.Examples.Puzzles.Garden

Methods

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

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

Ord Color

Defined in Documentation.SBV.Examples.Puzzles.Garden

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

Defined in Documentation.SBV.Examples.Puzzles.Garden

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Color)

literal :: Color -> SBV Color

fromCV :: CV -> Color

isConcretely :: SBV Color -> (Color -> Bool) -> Bool

sbvForall :: MonadSymbolic m => String -> m (SBV Color)

sbvForall_ :: MonadSymbolic m => m (SBV Color)

mkForallVars :: MonadSymbolic m => Int -> m [SBV Color]

sbvExists :: MonadSymbolic m => String -> m (SBV Color)

sbvExists_ :: MonadSymbolic m => m (SBV Color)

mkExistVars :: MonadSymbolic m => Int -> m [SBV Color]

free :: MonadSymbolic m => String -> m (SBV Color)

free_ :: MonadSymbolic m => m (SBV Color)

mkFreeVars :: MonadSymbolic m => Int -> m [SBV Color]

symbolic :: MonadSymbolic m => String -> m (SBV Color)

symbolics :: MonadSymbolic m => [String] -> m [SBV Color]

unliteral :: SBV Color -> Maybe Color

isConcrete :: SBV Color -> Bool

isSymbolic :: SBV Color -> Bool

HasKind Color

Defined in Documentation.SBV.Examples.Puzzles.Garden

Methods

kindOf :: Color -> Kind

hasSign :: Color -> Bool

intSizeOf :: Color -> Int

isBoolean :: Color -> Bool

isBounded :: Color -> Bool

isReal :: Color -> Bool

isFloat :: Color -> Bool

isDouble :: Color -> Bool

isRational :: Color -> Bool

isFP :: Color -> Bool

isUnbounded :: Color -> Bool

isUserSort :: Color -> Bool

isChar :: Color -> Bool

isString :: Color -> Bool

isList :: Color -> Bool

isSet :: Color -> Bool

isTuple :: Color -> Bool

isMaybe :: Color -> Bool

isEither :: Color -> Bool

showType :: Color -> String

SatModel Color

Defined in Documentation.SBV.Examples.Puzzles.Garden

Methods

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

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

type SColor = SBV Color

Symbolic version of the type Color.

sBlue :: SBV Color

Symbolic version of the constructor Blue.

sYellow :: SBV Color

Symbolic version of the constructor Yellow.

sRed :: SBV Color

Symbolic version of the constructor Red.

type Flower = SInteger

Represent flowers by symbolic integers

col :: Flower -> SBV Color

The uninterpreted function col assigns a color to each flower.

validPick :: SInteger -> Flower -> Flower -> Flower -> SBool

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

Count the number of flowers that occur in a given set of flowers.

puzzle :: Goal

Smullyan's puzzle.

flowerCount :: IO ()

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.)