sbv-5.14: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Data.SBV.Examples.Puzzles.SendMoreMoney

Description

Solves the classic `send + more = money` puzzle.

Synopsis

- sendMoreMoney :: IO AllSatResult

# Documentation

sendMoreMoney :: IO AllSatResult Source #

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