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

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
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.

Synopsis

- data Color
  - = Red
  - | Yellow
  - | Blue
- type SColor = SBV Color
- sBlue :: SBV Color
- sYellow :: SBV Color
- sRed :: SBV Color
- type Flower = SInteger
- col :: Flower -> SBV Color
- validPick :: SInteger -> Flower -> Flower -> Flower -> SBool
- count :: Color -> [Flower] -> SInteger
- puzzle :: ConstraintSet
- flowerCount :: IO ()

# Documentation

data Color Source #

Colors of the flowers

Constructors

Red |
Yellow |
Blue |

#### Instances

Instances details

Data Color Source # |

Instance details

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Color Source #

toConstr :: Color -> Constr Source #

dataTypeOf :: Color -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Color) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Color) Source #

gmapT :: (forall b. Data b => b -> b) -> Color -> Color Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Color -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Color -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Color -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Color -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Color -> m Color Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Color -> m Color Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Color -> m Color Source #

Read Color Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Garden Methods readsPrec :: Int -> ReadS Color Source # readList :: ReadS [Color] Source # readPrec :: ReadPrec Color Source # readListPrec :: ReadPrec [Color] Source #
Show Color Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Garden Methods showsPrec :: Int -> Color -> ShowS Source # show :: Color -> String Source # showList :: [Color] -> ShowS Source #
Eq Color Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Garden Methods (==) :: Color -> Color -> Bool Source # (/=) :: Color -> Color -> Bool Source #
Ord Color Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Garden Methods compare :: Color -> Color -> Ordering Source # (<) :: Color -> Color -> Bool Source # (<=) :: Color -> Color -> Bool Source # (>) :: Color -> Color -> Bool Source # (>=) :: Color -> Color -> Bool Source # max :: Color -> Color -> Color Source # min :: Color -> Color -> Color Source #
SymVal Color Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.Garden

Methods

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

literal :: Color -> SBV Color Source #

fromCV :: CV -> Color Source #

isConcretely :: SBV Color -> (Color -> Bool) -> Bool 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 #

HasKind Color Source # |

Instance details

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 #

isRational :: Color -> Bool Source #

isFP :: Color -> Bool Source #

isUnbounded :: Color -> Bool Source #

isUserSort :: 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 #

isEither :: Color -> Bool Source #

showType :: Color -> String Source #

SatModel Color Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.Garden Methods parseCVs :: [CV] -> Maybe (Color, [CV]) Source # cvtModel :: (Color -> Maybe b) -> Maybe (Color, [CV]) -> Maybe (b, [CV]) Source #

type SColor = SBV Color Source #

Symbolic version of the type `Color`.

sBlue :: SBV Color Source #

Symbolic version of the constructor `Blue`.

sYellow :: SBV Color Source #

Symbolic version of the constructor `Yellow`.

sRed :: SBV Color Source #

Symbolic version of the constructor `Red`.

type Flower = SInteger Source #

Represent flowers by symbolic integers

col :: Flower -> SBV Color Source #

The uninterpreted function `col` assigns a color to each flower.

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.

puzzle :: ConstraintSet Source #

Smullyan's puzzle.

flowerCount :: IO () Source #

Solve the puzzle. We have:

    >>> flowerCount
    Solution #1:
      N = 3 :: Integer
    This is the only solution.

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