    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Puzzles.Garden
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- 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.
    ------------------------------------------------------------------------------

    {-# LANGUAGE DeriveAnyClass      #-}
    {-# LANGUAGE DeriveDataTypeable  #-}
    {-# LANGUAGE OverloadedStrings   #-}
    {-# LANGUAGE StandaloneDeriving  #-}
    {-# LANGUAGE TemplateHaskell     #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Puzzles.Garden where

    import Data.SBV

    -- | Colors of the flowers
    data Color = Red | Yellow | Blue

    -- | Make 'Color' a symbolic value.
    mkSymbolicEnumeration ''Color

    -- | Represent flowers by symbolic integers
    type Flower = SInteger

    -- | The uninterpreted function 'col' assigns a color to each flower.
    col :: Flower -> SBV Color
    col :: Flower -> SBV Color
    col = String -> Flower -> SBV Color
    forall a. SMTDefinable a => String -> a
    uninterpret String
    "col"

    -- | 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.
    validPick :: SInteger -> Flower -> Flower -> Flower -> SBool
    validPick :: Flower -> Flower -> Flower -> Flower -> SBool
    validPick Flower
    n Flower
    i Flower
    j Flower
    k = [Flower] -> SBool
    forall a. EqSymbolic a => [a] -> SBool
    distinct [Flower
    i, Flower
    j, Flower
    k] SBool -> SBool -> SBool
    .&& (Flower -> SBool) -> [Flower] -> SBool
    forall a. (a -> SBool) -> [a] -> SBool
    sAll Flower -> SBool
    ok [Flower
    i, Flower
    j, Flower
    k]
      where ok :: Flower -> SBool
    ok Flower
    x = Flower -> (Flower, Flower) -> SBool
    forall a. OrdSymbolic a => a -> (a, a) -> SBool
    inRange Flower
    x (Flower
    1, Flower
    n)

    -- | Count the number of flowers that occur in a given set of flowers.
    count :: Color -> [Flower] -> SInteger
    count :: Color -> [Flower] -> Flower
    count Color
    c [Flower]
    fs = [Flower] -> Flower
    forall a. Num a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    sum [SBool -> Flower -> Flower -> Flower
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (Flower -> SBV Color
    col Flower
    f SBV Color -> SBV Color -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== Color -> SBV Color
    forall a. SymVal a => a -> SBV a
    literal Color
    c) Flower
    1 Flower
    0 | Flower
    f <- [Flower]
    fs]

    -- | Smullyan's puzzle.
    puzzle :: ConstraintSet
    puzzle :: ConstraintSet
    puzzle = do Flower
    n <- String -> Symbolic Flower
    sInteger String
    "N"

                let valid :: Flower -> Flower -> Flower -> SBool
    valid = Flower -> Flower -> Flower -> Flower -> SBool
    validPick Flower
    n

                -- Each color is represented:
                (Exists Any Integer
     -> Exists Any Integer -> Exists Any Integer -> SBool)
    -> ConstraintSet
    forall a. QuantifiedBool a => a -> ConstraintSet
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain ((Exists Any Integer
      -> Exists Any Integer -> Exists Any Integer -> SBool)
     -> ConstraintSet)
    -> (Exists Any Integer
        -> Exists Any Integer -> Exists Any Integer -> SBool)
    -> ConstraintSet
    forall a b. (a -> b) -> a -> b
    $ \(Exists Flower
    ef1) (Exists Flower
    ef2) (Exists Flower
    ef3) ->
                   Flower -> Flower -> Flower -> SBool
    valid Flower
    ef1 Flower
    ef2 Flower
    ef3 SBool -> SBool -> SBool
    .&& (Flower -> SBV Color) -> [Flower] -> [SBV Color]
    forall a b. (a -> b) -> [a] -> [b]
    map Flower -> SBV Color
    col [Flower
    ef1, Flower
    ef2, Flower
    ef3] [SBV Color] -> [SBV Color] -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== [SBV Color
    sRed, SBV Color
    sYellow, SBV Color
    sBlue]

                -- Pick any three, at least one is Red, one is Yellow, one is Blue
                (Forall Any Integer
     -> Forall Any Integer -> Forall Any Integer -> SBool)
    -> ConstraintSet
    forall a. QuantifiedBool a => a -> ConstraintSet
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain ((Forall Any Integer
      -> Forall Any Integer -> Forall Any Integer -> SBool)
     -> ConstraintSet)
    -> (Forall Any Integer
        -> Forall Any Integer -> Forall Any Integer -> SBool)
    -> ConstraintSet
    forall a b. (a -> b) -> a -> b
    $ \(Forall Flower
    af1) (Forall Flower
    af2) (Forall Flower
    af3) ->
                    let atLeastOne :: Color -> SBool
    atLeastOne Color
    c = Color -> [Flower] -> Flower
    count Color
    c [Flower
    af1, Flower
    af2, Flower
    af3] Flower -> Flower -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= Flower
    1
                    in Flower -> Flower -> Flower -> SBool
    valid Flower
    af1 Flower
    af2 Flower
    af3 SBool -> SBool -> SBool
    .=> Color -> SBool
    atLeastOne Color
    Red SBool -> SBool -> SBool
    .&& Color -> SBool
    atLeastOne Color
    Yellow SBool -> SBool -> SBool
    .&& Color -> SBool
    atLeastOne Color
    Blue

    -- | 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.)
    flowerCount :: IO ()
    flowerCount :: IO ()
    flowerCount = AllSatResult -> IO ()
    forall a. Show a => a -> IO ()
    print (AllSatResult -> IO ()) -> IO AllSatResult -> IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< SMTConfig -> ConstraintSet -> IO AllSatResult
    forall a. Satisfiable a => SMTConfig -> a -> IO AllSatResult
    allSatWith SMTConfig
    z3{allSatTrackUFs=False} ConstraintSet
    puzzle