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