    -----------------------------------------------------------------------------
    -- |
    -- 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?
    -----------------------------------------------------------------------------

    {-# OPTIONS_GHC -Wall -Werror #-}

    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 :: IO AllSatResult
    puzzle = SymbolicT IO SBool -> IO AllSatResult
    forall a. Provable a => a -> IO AllSatResult
    allSat (SymbolicT IO SBool -> IO AllSatResult)
    -> SymbolicT IO SBool -> IO AllSatResult
    forall a b. (a -> b) -> a -> b
    $ do
               [dog :: SInteger
    dog, cat :: SInteger
    cat, mouse :: SInteger
    mouse] <- [String] -> Symbolic [SInteger]
    sIntegers ["dog", "cat", "mouse"]
               [SBool] -> SymbolicT IO SBool
    solve [ SInteger
    dog   SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= 1                                           -- at least one dog
                     , SInteger
    cat   SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= 1                                           -- at least one cat
                     , SInteger
    mouse SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= 1                                           -- at least one mouse
                     , SInteger
    dog SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    + SInteger
    cat SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    + SInteger
    mouse SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== 100                             -- buy precisely 100 animals
                     , 15 SReal -> SInteger -> SReal
    forall a. (Integral a, SymVal a) => SReal -> SBV a -> SReal
    `per` SInteger
    dog SReal -> SReal -> SReal
    forall a. Num a => a -> a -> a
    + 1 SReal -> SInteger -> SReal
    forall a. (Integral a, SymVal a) => SReal -> SBV a -> SReal
    `per` SInteger
    cat SReal -> SReal -> SReal
    forall a. Num a => a -> a -> a
    + 0.25 SReal -> SInteger -> SReal
    forall a. (Integral a, SymVal a) => SReal -> SBV a -> SReal
    `per` SInteger
    mouse SReal -> SReal -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== 100 -- spend exactly 100 dollars
                     ]
      where p :: SReal
    p per :: SReal -> SBV a -> SReal
    `per` q :: SBV a
    q = SReal
    p SReal -> SReal -> SReal
    forall a. Num a => a -> a -> a
    * (SBV a -> SReal
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    sFromIntegral SBV a
    q :: SReal)