Raadsel oplossen met een SMT solver via SBV

Raadsel.hs

module Main (main) where

import Data.SBV

raadsel :: Symbolic SBool
raadsel = do
  vars@[s, e, n, d, m, o, r, y] <- sIntegers ["s", "e", "n", "d", "m", "o", "r", "y"]

  -- Helper, maakt bvb. (100 * a + 10 * b + c) uit [a, b, c]
  let woord w = sum (zipWith (*) (reverse w) (iterate (* 10) 1))

      send = woord [s, e, n, d]
      more = woord [m, o, r, e]
      money = woord [m, o, n, e, y]

  solve [
    -- Elke letter is een getal tussen 0 en 9 (inclusief)
      sAll (\v -> v .>= 0 .&& v .<= 9) vars
    -- Alle letters zijn een ander getal
    , distinct vars
    -- 's' en 'm' zijn niet 0
    , s ./= 0
    , m ./= 0
    -- Opgave
    , send + more .== money
    ]

main :: IO ()
main = allSat raadsel >>= print

{-

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.

-}