;; lib/minikanren/tests/send-more-money.sx — classic cryptarithmetic
;;
;;     S E N D
;;   + M O R E
;;   ---------
;;   M O N E Y
;;
;; Column-by-column encoding with carries c1, c2, c3, and the
;; leftmost column produces a carry which equals M (the result is 5 digits).
;; All 8 letters distinct; S ≠ 0, M ≠ 0.
;; Unique solution: S=9, E=5, N=6, D=7, M=1, O=0, R=8, Y=2.
;;
;; Note: the full search labelling 11 variables from {0..9} is too slow
;; for naive labelling order (10^11 combinations naively, even with
;; bounds-consistency the branching factor dominates). Real CLP(FD)
;; systems use first-fail heuristics. Here we only verify the encoding
;; against the known answer.

(define
  digits-0-9
  (list
    0
    1
    2
    3
    4
    5
    6
    7
    8
    9))
(define
  digits-1-9
  (list
    1
    2
    3
    4
    5
    6
    7
    8
    9))

(define
  smm-col-with-carry
  (fn
    (x y carry-in z carry-out)
    (fresh
      (xy xyc ten-cout z-plus-ten-cout)
      (fd-plus x y xy)
      (fd-plus xy carry-in xyc)
      (fd-times 10 carry-out ten-cout)
      (fd-plus z ten-cout z-plus-ten-cout)
      (fd-eq xyc z-plus-ten-cout))))

(define
  send-more-money
  (fn
    (S E N D M O R Y)
    (fresh
      (c1 c2 c3)
      (mk-conj
        (fd-in S digits-1-9)
        (fd-in M digits-1-9)
        (fd-in E digits-0-9)
        (fd-in N digits-0-9)
        (fd-in D digits-0-9)
        (fd-in O digits-0-9)
        (fd-in R digits-0-9)
        (fd-in Y digits-0-9)
        (fd-in c1 (list 0 1))
        (fd-in c2 (list 0 1))
        (fd-in c3 (list 0 1))
        (fd-distinct (list S E N D M O R Y))
        (smm-col-with-carry D E 0 Y c1)
        (smm-col-with-carry N R c1 E c2)
        (smm-col-with-carry E O c2 N c3)
        (smm-col-with-carry S M c3 O M)
        (fd-label (list S E N D M O R Y c1 c2 c3))))))

(mk-test
  "send-more-money-verify-known-solution"
  (run*
    q
    (send-more-money
      9
      5
      6
      7
      1
      0
      8
      2))
  (list (make-symbol "_.0")))

(mk-tests-run!)