    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Documentation.SBV.Examples.Puzzles.DogCatMouse
    -- Copyright   :  (c) Levent Erkok
    -- License     :  BSD3
    -- Maintainer  :  erkokl@gmail.com
    -- Stability   :  experimental
    --
    -- Puzzle:
    --   Spend exactly 100 dollars and buy exactly 100 animals.
    --   Dogs cost 15 dollars, cats cost 1 dollar, and mice cost 25 cents each.
    --   You have to buy at least one of each.
    --   How many of each should you buy?
    -----------------------------------------------------------------------------

    module Documentation.SBV.Examples.Puzzles.DogCatMouse where

    import Data.SBV

    -- | Prints the only solution:
    --
    -- >>> puzzle
    -- Solution #1:
    --   dog   =  3 :: Integer
    --   cat   = 41 :: Integer
    --   mouse = 56 :: Integer
    -- This is the only solution.
    puzzle :: IO AllSatResult
    puzzle = allSat $ do
               [dog, cat, mouse] <- sIntegers ["dog", "cat", "mouse"]
               solve [ dog   .>= 1                                           -- at least one dog
                     , cat   .>= 1                                           -- at least one cat
                     , mouse .>= 1                                           -- at least one mouse
                     , dog + cat + mouse .== 100                             -- buy precisely 100 animals
                     , 15 `per` dog + 1 `per` cat + 0.25 `per` mouse .== 100 -- spend exactly 100 dollars
                     ]
      where p `per` q = p * (sFromIntegral q :: SReal)