From f88388b2f926e2ffbff82c7e6ae89497b6114893 Mon Sep 17 00:00:00 2001
From: giles <giles.bradshaw@rose-ash.com>
Date: Fri, 8 May 2026 14:35:19 +0000
Subject: [PATCH] =?UTF-8?q?mk:=20phase=206F=20=E2=80=94=20fd-distinct=20(p?=
 =?UTF-8?q?airwise=20alldifferent)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

(fd-distinct (list a b c ...)) imposes pairwise distinctness via O(n²)
fd-neq constraints. Each fd-neq propagates independently when any pair
becomes ground or has a domain-removable value.

Tests: empty/singleton trivially succeed; pair-distinct/equal cover
correctness; 3-perms-of-3 = 6 and 4-perms-of-4 = 24 confirm full
permutation enumeration; pigeonhole 4-of-3 fails.

7 new tests, 610/610 cumulative.
---
 lib/minikanren/clpfd.sx                | 25 +++++++++++++
 lib/minikanren/tests/clpfd-distinct.sx | 52 ++++++++++++++++++++++++++
 2 files changed, 77 insertions(+)
 create mode 100644 lib/minikanren/tests/clpfd-distinct.sx

diff --git a/lib/minikanren/clpfd.sx b/lib/minikanren/clpfd.sx
index e356e60a..fedc87c7 100644
--- a/lib/minikanren/clpfd.sx
+++ b/lib/minikanren/clpfd.sx
@@ -459,3 +459,28 @@
     (cond
       ((empty? vars) succeed)
       (:else (mk-conj (fd-label-one (first vars)) (fd-label (rest vars)))))))
+
+;; --- fd-distinct (pairwise distinct via fd-neq) ---
+
+(define
+  fd-distinct-from-head
+  (fn
+    (x others)
+    (cond
+      ((empty? others) succeed)
+      (:else
+        (mk-conj
+          (fd-neq x (first others))
+          (fd-distinct-from-head x (rest others)))))))
+
+(define
+  fd-distinct
+  (fn
+    (vars)
+    (cond
+      ((empty? vars) succeed)
+      ((empty? (rest vars)) succeed)
+      (:else
+        (mk-conj
+          (fd-distinct-from-head (first vars) (rest vars))
+          (fd-distinct (rest vars)))))))
diff --git a/lib/minikanren/tests/clpfd-distinct.sx b/lib/minikanren/tests/clpfd-distinct.sx
new file mode 100644
index 00000000..1c2d7d11
--- /dev/null
+++ b/lib/minikanren/tests/clpfd-distinct.sx
@@ -0,0 +1,52 @@
+;; lib/minikanren/tests/clpfd-distinct.sx — fd-distinct (alldifferent).
+
+(mk-test
+  "fd-distinct-empty"
+  (run* q (fd-distinct (list)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "fd-distinct-singleton"
+  (run* q (fd-distinct (list 5)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "fd-distinct-pair-distinct"
+  (run* q (fd-distinct (list 1 2)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "fd-distinct-pair-equal-fails"
+  (run* q (fd-distinct (list 5 5)))
+  (list))
+
+(mk-test
+  "fd-distinct-3-perms-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-distinct (list a b c)) (fd-label (list a b c)) (== q (list a b c))))))
+    (= (len res) 6))
+  true)
+
+(mk-test
+  "fd-distinct-4-perms-of-4-count"
+  (let
+    ((res (run* q (fresh (a b c d) (fd-in a (list 1 2 3 4)) (fd-in b (list 1 2 3 4)) (fd-in c (list 1 2 3 4)) (fd-in d (list 1 2 3 4)) (fd-distinct (list a b c d)) (fd-label (list a b c d)) (== q (list a b c d))))))
+    (= (len res) 24))
+  true)
+
+(mk-test
+  "fd-distinct-pigeonhole-fails"
+  (run*
+    q
+    (fresh
+      (a b c d)
+      (fd-in a (list 1 2 3))
+      (fd-in b (list 1 2 3))
+      (fd-in c (list 1 2 3))
+      (fd-in d (list 1 2 3))
+      (fd-distinct (list a b c d))
+      (fd-label (list a b c d))
+      (== q (list a b c d))))
+  (list))
+
+(mk-tests-run!)