    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Puzzles.Coins
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Solves the following puzzle:
    --
    -- @
    -- You and a friend pass by a standard coin operated vending machine and you decide to get a candy bar.
    -- The price is US $0.95, but after checking your pockets you only have a dollar (US $1) and the machine
    -- only takes coins. You turn to your friend and have this conversation:
    --   you: Hey, do you have change for a dollar?
    --   friend: Let's see. I have 6 US coins but, although they add up to a US $1.15, I can't break a dollar.
    --   you: Huh? Can you make change for half a dollar?
    --   friend: No.
    --   you: How about a quarter?
    --   friend: Nope, and before you ask I cant make change for a dime or nickel either.
    --   you: Really? and these six coins are all US government coins currently in production?
    --   friend: Yes.
    --   you: Well can you just put your coins into the vending machine and buy me a candy bar, and I'll pay you back?
    --   friend: Sorry, I would like to but I cant with the coins I have.
    -- What coins are your friend holding?
    -- @
    --
    -- To be fair, the problem has no solution /mathematically/. But there is a solution when one takes into account that
    -- vending machines typically do not take the 50 cent coins!
    --
    -----------------------------------------------------------------------------

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Puzzles.Coins where

    import Data.SBV

    -- | We will represent coins with 16-bit words (more than enough precision for coins).
    type Coin = SWord16

    -- | Create a coin. The argument Int argument just used for naming the coin. Note that
    -- we constrain the value to be one of the valid U.S. coin values as we create it.
    mkCoin :: Int -> Symbolic Coin
    mkCoin :: Int -> Symbolic Coin
    mkCoin i :: Int
    i = do Coin
    c <- String -> Symbolic Coin
    forall a. SymVal a => String -> Symbolic (SBV a)
    exists (String -> Symbolic Coin) -> String -> Symbolic Coin
    forall a b. (a -> b) -> a -> b
    $ 'c' Char -> String -> String
    forall a. a -> [a] -> [a]
    : Int -> String
    forall a. Show a => a -> String
    show Int
    i
                  SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ (Coin -> SBool) -> [Coin] -> SBool
    forall a. (a -> SBool) -> [a] -> SBool
    sAny (Coin -> Coin -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== Coin
    c) [1, 5, 10, 25, 50, 100]
                  Coin -> Symbolic Coin
    forall (m :: * -> *) a. Monad m => a -> m a
    return Coin
    c

    -- | Return all combinations of a sequence of values.
    combinations :: [a] -> [[a]]
    combinations :: [a] -> [[a]]
    combinations coins :: [a]
    coins = [[[a]]] -> [[a]]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [Int -> [a] -> [[a]]
    forall t a. (Eq t, Num t) => t -> [a] -> [[a]]
    combs Int
    i [a]
    coins | Int
    i <- [1 .. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [a]
    coins]]
      where combs :: t -> [a] -> [[a]]
    combs 0 _      = [[]]
            combs _ []     = []
            combs k :: t
    k (x :: a
    x:xs :: [a]
    xs) = ([a] -> [a]) -> [[a]] -> [[a]]
    forall a b. (a -> b) -> [a] -> [b]
    map (a
    xa -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :) (t -> [a] -> [[a]]
    combs (t
    kt -> t -> t
    forall a. Num a => a -> a -> a
    -1) [a]
    xs) [[a]] -> [[a]] -> [[a]]
    forall a. [a] -> [a] -> [a]
    ++ t -> [a] -> [[a]]
    combs t
    k [a]
    xs

    -- | Constraint 1: Cannot make change for a dollar.
    c1 :: [Coin] -> SBool
    c1 :: [Coin] -> SBool
    c1 xs :: [Coin]
    xs = [Coin] -> Coin
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    sum [Coin]
    xs Coin -> Coin -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    ./= 100

    -- | Constraint 2: Cannot make change for half a dollar.
    c2 :: [Coin] -> SBool
    c2 :: [Coin] -> SBool
    c2 xs :: [Coin]
    xs = [Coin] -> Coin
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    sum [Coin]
    xs Coin -> Coin -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    ./= 50

    -- | Constraint 3: Cannot make change for a quarter.
    c3 :: [Coin] -> SBool
    c3 :: [Coin] -> SBool
    c3 xs :: [Coin]
    xs = [Coin] -> Coin
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    sum [Coin]
    xs Coin -> Coin -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    ./= 25

    -- | Constraint 4: Cannot make change for a dime.
    c4 :: [Coin] -> SBool
    c4 :: [Coin] -> SBool
    c4 xs :: [Coin]
    xs = [Coin] -> Coin
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    sum [Coin]
    xs Coin -> Coin -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    ./= 10

    -- | Constraint 5: Cannot make change for a nickel
    c5 :: [Coin] -> SBool
    c5 :: [Coin] -> SBool
    c5 xs :: [Coin]
    xs = [Coin] -> Coin
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    sum [Coin]
    xs Coin -> Coin -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    ./= 5

    -- | Constraint 6: Cannot buy the candy either. Here's where we need to have the extra knowledge
    -- that the vending machines do not take 50 cent coins.
    c6 :: [Coin] -> SBool
    c6 :: [Coin] -> SBool
    c6 xs :: [Coin]
    xs = [Coin] -> Coin
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    sum ((Coin -> Coin) -> [Coin] -> [Coin]
    forall a b. (a -> b) -> [a] -> [b]
    map Coin -> Coin
    forall a. (Mergeable a, EqSymbolic a, Num a) => a -> a
    val [Coin]
    xs) Coin -> Coin -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    ./= 95
       where val :: a -> a
    val x :: a
    x = SBool -> a -> a -> a
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (a
    x a -> a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== 50) 0 a
    x

    -- | Solve the puzzle. We have:
    --
    -- >>> puzzle
    -- Satisfiable. Model:
    --   c1 = 50 :: Word16
    --   c2 = 25 :: Word16
    --   c3 = 10 :: Word16
    --   c4 = 10 :: Word16
    --   c5 = 10 :: Word16
    --   c6 = 10 :: Word16
    --
    -- i.e., your friend has 4 dimes, a quarter, and a half dollar.
    puzzle :: IO SatResult
    puzzle :: IO SatResult
    puzzle = SymbolicT IO SBool -> IO SatResult
    forall a. Provable a => a -> IO SatResult
    sat (SymbolicT IO SBool -> IO SatResult)
    -> SymbolicT IO SBool -> IO SatResult
    forall a b. (a -> b) -> a -> b
    $ do
            [Coin]
    cs <- (Int -> Symbolic Coin) -> [Int] -> SymbolicT IO [Coin]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Int -> Symbolic Coin
    mkCoin [1..6]
            -- Assert each of the constraints for all combinations that has
            -- at least two coins (to make change)
            (SBool -> SymbolicT IO ()) -> [SBool] -> SymbolicT IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain [[Coin] -> SBool
    c [Coin]
    s | [Coin]
    s <- [Coin] -> [[Coin]]
    forall a. [a] -> [[a]]
    combinations [Coin]
    cs, [Coin] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Coin]
    s Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= 2, [Coin] -> SBool
    c <- [[Coin] -> SBool
    c1, [Coin] -> SBool
    c2, [Coin] -> SBool
    c3, [Coin] -> SBool
    c4, [Coin] -> SBool
    c5, [Coin] -> SBool
    c6]]
            -- the following constraint is not necessary for solving the puzzle
            -- however, it makes sure that the solution comes in decreasing value of coins,
            -- thus allowing the above test to succeed regardless of the solver used.
            SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ [SBool] -> SBool
    sAnd ([SBool] -> SBool) -> [SBool] -> SBool
    forall a b. (a -> b) -> a -> b
    $ (Coin -> Coin -> SBool) -> [Coin] -> [Coin] -> [SBool]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Coin -> Coin -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    (.>=) [Coin]
    cs ([Coin] -> [Coin]
    forall a. [a] -> [a]
    tail [Coin]
    cs)
            -- assert that the sum must be 115 cents.
            SBool -> SymbolicT IO SBool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
    forall a b. (a -> b) -> a -> b
    $ [Coin] -> Coin
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    sum [Coin]
    cs Coin -> Coin -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== 115