;; lib/minikanren/tests/clpfd-times.sx — fd-times (x * y = z).

(mk-test
  "fd-times-3-4"
  (run* q (fresh (z) (fd-times 3 4 z) (== q z)))
  (list 12))

(mk-test
  "fd-times-recover-divisor"
  (run* q (fresh (x) (fd-times x 5 30) (== q x)))
  (list 6))

(mk-test
  "fd-times-non-divisible-fails"
  (run* q (fresh (x) (fd-times x 5 31) (== q x)))
  (list))

(mk-test
  "fd-times-by-zero"
  (run* q (fresh (z) (fd-times 0 99 z) (== q z)))
  (list 0))

(mk-test
  "fd-times-zero-by-anything-zero"
  (run*
    q
    (fresh
      (x)
      (fd-in x (list 1 2 3))
      (fd-times x 0 0)
      (fd-label (list x))
      (== q x)))
  (list 1 2 3))

(mk-test
  "fd-times-12-divisor-pairs"
  (run*
    q
    (fresh
      (x y)
      (fd-in
        x
        (list
          1
          2
          3
          4
          5
          6))
      (fd-in
        y
        (list
          1
          2
          3
          4
          5
          6))
      (fd-times x y 12)
      (fd-label (list x y))
      (== q (list x y))))
  (list
    (list 2 6)
    (list 3 4)
    (list 4 3)
    (list 6 2)))

(mk-test
  "fd-times-square-of-each"
  (run*
    q
    (fresh
      (x z)
      (fd-in x (list 1 2 3 4 5))
      (fd-times x x z)
      (fd-label (list x))
      (== q (list x z))))
  (list
    (list 1 1)
    (list 2 4)
    (list 3 9)
    (list 4 16)
    (list 5 25)))

(mk-tests-run!)