;; lib/minikanren/tests/clpfd-neq.sx — fd-neq with constraint propagation.

;; --- ground / domain interaction ---

(mk-test
  "fd-neq-ground-distinct"
  (run*
    q
    (fresh
      (x)
      (fd-neq x 5)
      (fd-in x (list 4 5 6))
      (fd-label (list x))
      (== q x)))
  (list 4 6))

(mk-test
  "fd-neq-ground-equal-fails"
  (run* q (fresh (x) (== x 5) (fd-neq x 5) (== q x)))
  (list))

(mk-test
  "fd-neq-symmetric"
  (run*
    q
    (fresh
      (x)
      (fd-neq 7 x)
      (fd-in x (list 5 6 7 8 9))
      (fd-label (list x))
      (== q x)))
  (list 5 6 8 9))

;; --- two vars with overlapping domains ---

(mk-test
  "fd-neq-pair-from-3"
  (let
    ((res (run* q (fresh (x y) (fd-in x (list 1 2 3)) (fd-in y (list 1 2 3)) (fd-neq x y) (fd-label (list x y)) (== q (list x y))))))
    (= (len res) 6))
  true)

(mk-test
  "fd-all-distinct-3-of-3"
  (let
    ((res (run* q (fresh (a b c) (fd-in a (list 1 2 3)) (fd-in b (list 1 2 3)) (fd-in c (list 1 2 3)) (fd-neq a b) (fd-neq a c) (fd-neq b c) (fd-label (list a b c)) (== q (list a b c))))))
    (= (len res) 6))
  true)

(mk-test
  "fd-pigeonhole-fails"
  (run*
    q
    (fresh
      (a b c)
      (fd-in a (list 1 2))
      (fd-in b (list 1 2))
      (fd-in c (list 1 2))
      (fd-neq a b)
      (fd-neq a c)
      (fd-neq b c)
      (fd-label (list a b c))
      (== q (list a b c))))
  (list))

;; --- propagation when one side becomes ground ---

(mk-test
  "fd-neq-propagates-after-ground"
  (run*
    q
    (fresh
      (x y)
      (fd-in x (list 1 2 3))
      (fd-in y (list 1 2 3))
      (fd-neq x y)
      (== x 2)
      (fd-label (list y))
      (== q y)))
  (list 1 3))

(mk-tests-run!)