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

Safe HaskellNone



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!



type Coin = SWord16Source

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

mkCoin :: Int -> Symbolic CoinSource

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] -> SBoolSource

Constraint 1: Cannot make change for a dollar.

c2 :: [Coin] -> SBoolSource

Constraint 2: Cannot make change for half a dollar.

c3 :: [Coin] -> SBoolSource

Constraint 3: Cannot make change for a quarter.

c4 :: [Coin] -> SBoolSource

Constraint 4: Cannot make change for a dime.

c5 :: [Coin] -> SBoolSource

Constraint 5: Cannot make change for a nickel

c6 :: [Coin] -> SBoolSource

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 SatResultSource

Solve the puzzle. We have:

>>> puzzle
Satisfiable. Model:
  c1 = 50 :: SWord16
  c2 = 25 :: SWord16
  c3 = 10 :: SWord16
  c4 = 10 :: SWord16
  c5 = 10 :: SWord16
  c6 = 10 :: SWord16

i.e., your friend has 4 dimes, a quarter, and a half dollar.