-----------------------------------------------------------------------------
-- |
-- 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 :: IO AllSatResult
sendMoreMoney = SymbolicT IO SBool -> IO AllSatResult
forall a. Satisfiable a => a -> IO AllSatResult
allSat (SymbolicT IO SBool -> IO AllSatResult)
-> SymbolicT IO SBool -> IO AllSatResult
forall a b. (a -> b) -> a -> b
$ do
        ds@[s,e,n,d,m,o,r,y] <- (String -> SymbolicT IO SInteger)
-> [String] -> SymbolicT IO [SInteger]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM String -> SymbolicT IO SInteger
sInteger [String
"s", String
"e", String
"n", String
"d", String
"m", String
"o", String
"r", String
"y"]
        let isDigit a
x = a
x a -> a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= a
0 SBool -> SBool -> SBool
.&& a
x a -> a -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= a
9
            val [b]
xs    = [b] -> b
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([b] -> b) -> [b] -> b
forall a b. (a -> b) -> a -> b
$ (b -> b -> b) -> [b] -> [b] -> [b]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith b -> b -> b
forall a. Num a => a -> a -> a
(*) ([b] -> [b]
forall a. [a] -> [a]
reverse [b]
xs) ((b -> b) -> b -> [b]
forall a. (a -> a) -> a -> [a]
iterate (b -> b -> b
forall a. Num a => a -> a -> a
*b
10) b
1)
            send      = [SInteger] -> SInteger
forall a. Num a => [a] -> a
val [SInteger
s,SInteger
e,SInteger
n,SInteger
d]
            more      = [SInteger] -> SInteger
forall a. Num a => [a] -> a
val [SInteger
m,SInteger
o,SInteger
r,SInteger
e]
            money     = [SInteger] -> SInteger
forall a. Num a => [a] -> a
val [SInteger
m,SInteger
o,SInteger
n,SInteger
e,SInteger
y]
        constrain $ sAll isDigit ds
        constrain $ distinct ds
        constrain $ s ./= 0 .&& m ./= 0
        solve [send + more .== money]