    -----------------------------------------------------------------------------
    -- |
    -- 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 :: [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)
    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 -> 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 a. Num a => [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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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]