content: -----------------------------------------------------------------------------
  -- |
  -- 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.
  -----------------------------------------------------------------------------
  
  {-# OPTIONS_GHC -Wall -Werror #-}
  
  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]
  