```-----------------------------------------------------------------------------
-- |
-- Module      :  Data.SBV.Examples.Puzzles.SendMoreMoney
-- Copyright   :  (c) Levent Erkok
-- Maintainer  :  erkokl@gmail.com
-- Stability   :  experimental
--
-- Solves the classic @send + more = money@ puzzle.
-----------------------------------------------------------------------------

module Data.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 \$ bAll isDigit ds
constrain \$ allDifferent ds
constrain \$ s ./= 0 &&& m ./= 0
solve [send + more .== money]
```