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

Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Data.SBV.Examples.Puzzles.SendMoreMoney

Description

Solves the classic send + more = money puzzle.

Synopsis

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