sbv-5.9: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Data.SBV.Examples.Puzzles.Coins

Description

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!

Synopsis

- type Coin = SWord16
- mkCoin :: Int -> Symbolic Coin
- combinations :: [a] -> [[a]]
- c1 :: [Coin] -> SBool
- c2 :: [Coin] -> SBool
- c3 :: [Coin] -> SBool
- c4 :: [Coin] -> SBool
- c5 :: [Coin] -> SBool
- c6 :: [Coin] -> SBool
- puzzle :: IO SatResult

# Documentation

type Coin = SWord16 Source

We will represent coins with 16-bit words (more than enough precision for coins).

mkCoin :: Int -> Symbolic Coin Source

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.

combinations :: [a] -> [[a]] Source

Return all combinations of a sequence of values.

c1 :: [Coin] -> SBool Source

Constraint 1: Cannot make change for a dollar.

c2 :: [Coin] -> SBool Source

Constraint 2: Cannot make change for half a dollar.

c3 :: [Coin] -> SBool Source

Constraint 3: Cannot make change for a quarter.

c4 :: [Coin] -> SBool Source

Constraint 4: Cannot make change for a dime.

c5 :: [Coin] -> SBool Source

Constraint 5: Cannot make change for a nickel

c6 :: [Coin] -> SBool Source

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.

puzzle :: IO SatResult Source

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.