-----------------------------------------------------------------------------
-- |
-- 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 Int
i = do Coin
c <- String -> Symbolic Coin
forall a. SymVal a => String -> Symbolic (SBV a)
sbvExists (String -> Symbolic Coin) -> String -> Symbolic Coin
forall a b. (a -> b) -> a -> b
$ Char
'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) [Coin
1, Coin
5, Coin
10, Coin
25, Coin
50, Coin
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 [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 <- [Int
1 .. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
coins]]
  where combs :: t -> [a] -> [[a]]
combs t
0 [a]
_      = [[]]
        combs t
_ []     = []
        combs t
k (a
x:[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
-t
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 [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
./= Coin
100

-- | Constraint 2: Cannot make change for half a dollar.
c2 :: [Coin] -> SBool
c2 :: [Coin] -> SBool
c2 [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
./= Coin
50

-- | Constraint 3: Cannot make change for a quarter.
c3 :: [Coin] -> SBool
c3 :: [Coin] -> SBool
c3 [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
./= Coin
25

-- | Constraint 4: Cannot make change for a dime.
c4 :: [Coin] -> SBool
c4 :: [Coin] -> SBool
c4 [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
./= Coin
10

-- | Constraint 5: Cannot make change for a nickel
c5 :: [Coin] -> SBool
c5 :: [Coin] -> SBool
c5 [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
./= Coin
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 [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
./= Coin
95
   where val :: a -> a
val 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
.== a
50) a
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 [Int
1..Int
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
>= Int
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
.== Coin
115