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