----------------------------------------------------------------------------- -- | -- Module : Documentation.SBV.Examples.Puzzles.SendMoreMoney -- Copyright : (c) Levent Erkok -- License : BSD3 -- Maintainer: erkokl@gmail.com -- Stability : experimental -- -- Solves the classic @send + more = money@ puzzle. ----------------------------------------------------------------------------- module Documentation.SBV.Examples.Puzzles.SendMoreMoney where import Data.SBV -- | Solve the puzzle. We have: -- -- >>> sendMoreMoney -- Solution #1: -- s = 9 :: Integer -- e = 5 :: Integer -- n = 6 :: Integer -- d = 7 :: Integer -- m = 1 :: Integer -- o = 0 :: Integer -- r = 8 :: Integer -- y = 2 :: Integer -- This is the only solution. -- -- That is: -- -- >>> 9567 + 1085 == 10652 -- True sendMoreMoney :: IO AllSatResult sendMoreMoney = allSat \$ do ds@[s,e,n,d,m,o,r,y] <- mapM sInteger ["s", "e", "n", "d", "m", "o", "r", "y"] let isDigit x = x .>= 0 .&& x .<= 9 val xs = sum \$ zipWith (*) (reverse xs) (iterate (*10) 1) send = val [s,e,n,d] more = val [m,o,r,e] money = val [m,o,n,e,y] constrain \$ sAll isDigit ds constrain \$ distinct ds constrain \$ s ./= 0 .&& m ./= 0 solve [send + more .== money]