mk: phase 6D — fd-neq with propagation + constraint reactivation

fd-neq adds a closure to the constraint store and runs it once on
post. After every label binding, fd-fire-store re-runs all stored
constraints — when one side of a fd-neq later becomes ground, the
domain of the other side has the value removed.

Propagator semantics:
  (number, number)  -> equal? fail : ok
  (number, var)     -> remove number from var's domain
  (var, number)     -> symmetric
  (var, var)        -> defer (re-fires after each label step)

Pigeonhole-fails test confirms the constraint flow ends correctly:
3 vars all-pairwise-distinct over a 2-element domain has no solutions.

7 new tests, 593/593 cumulative.

lib/minikanren/clpfd.sx

@@ -1,20 +1,19 @@
-;; lib/minikanren/clpfd.sx — Phase 6 piece B: CLP(FD) foundation.
+;; lib/minikanren/clpfd.sx — Phase 6: native CLP(FD) on miniKanren.
 ;;
-;; A finite-domain layer on top of the existing miniKanren machinery. The
-;; substitution dict carries an extra reserved key "_fd" that holds a
+;; The substitution dict carries an extra reserved key "_fd" that holds a
 ;; constraint-store record:
 ;;
 ;;   {:domains    {var-name -> sorted-int-list}
-;;    :constraints (... pending constraints ...)}
+;;    :constraints (... pending constraint closures ...)}
 ;;
-;; Domains are sorted SX lists of ints (no duplicates). The constraints
-;; field is reserved for later iterations; this commit ships only the
-;; domain machinery + accessors.
-;;
-;; Naming: fd-* (domain primitives, kernel-style).
+;; Domains are sorted SX lists of ints (no duplicates).
+;; Constraints are functions s -> s-or-nil that propagate / re-check.
+;; They are re-fired after every label binding via fd-fire-store.
 
 (define fd-key "_fd")
 
+;; --- domain primitives ---
+
 (define
   fd-dom-rev
   (fn
@@ -56,7 +55,6 @@
     (cond ((empty? (rest d)) (first d)) (:else (fd-dom-last (rest d))))))
 
 (define fd-dom-max (fn (d) (fd-dom-last d)))
-
 (define fd-dom-member? (fn (x d) (some (fn (y) (= x y)) d)))
 
 (define
@@ -89,6 +87,8 @@
       ((> lo hi) (list))
       (:else (cons lo (fd-dom-range (+ lo 1) hi))))))
 
+;; --- constraint store accessors ---
+
 (define fd-store-empty (fn () {:domains {} :constraints (list)}))
 
 (define
@@ -98,7 +98,6 @@
     (cond ((has-key? s fd-key) (get s fd-key)) (:else (fd-store-empty)))))
 
 (define fd-domains-of (fn (s) (get (fd-store-of s) :domains)))
-
 (define fd-with-store (fn (s store) (assoc s fd-key store)))
 
 (define
@@ -124,6 +123,37 @@
               ((store-prime (assoc store :domains doms-prime)))
               (fd-with-store s store-prime))))))))
 
+(define
+  fd-add-constraint
+  (fn
+    (s c)
+    (let
+      ((store (fd-store-of s)))
+      (let
+        ((cs-prime (cons c (get store :constraints))))
+        (let
+          ((store-prime (assoc store :constraints cs-prime)))
+          (fd-with-store s store-prime))))))
+
+(define
+  fd-fire-list
+  (fn
+    (cs s)
+    (cond
+      ((empty? cs) s)
+      (:else
+        (let
+          ((s2 ((first cs) s)))
+          (cond ((= s2 nil) nil) (:else (fd-fire-list (rest cs) s2))))))))
+
+(define
+  fd-fire-store
+  (fn
+    (s)
+    (let ((cs (get (fd-store-of s) :constraints))) (fd-fire-list cs s))))
+
+;; --- user-facing goals ---
+
 (define
   fd-in
   (fn
@@ -147,6 +177,49 @@
                     (cond ((= s2 nil) mzero) (:else (unit s2)))))))
             (:else mzero)))))))
 
+;; --- fd-neq with propagation ---
+
+(define
+  fd-neq-prop
+  (fn
+    (x y s)
+    (let
+      ((wx (mk-walk x s)) (wy (mk-walk y s)))
+      (cond
+        ((and (number? wx) (number? wy))
+          (cond ((= wx wy) nil) (:else s)))
+        ((and (number? wx) (is-var? wy))
+          (let
+            ((y-dom (fd-domain-of s (var-name wy))))
+            (cond
+              ((= y-dom nil) s)
+              (:else
+                (fd-set-domain s (var-name wy) (fd-dom-without wx y-dom))))))
+        ((and (number? wy) (is-var? wx))
+          (let
+            ((x-dom (fd-domain-of s (var-name wx))))
+            (cond
+              ((= x-dom nil) s)
+              (:else
+                (fd-set-domain s (var-name wx) (fd-dom-without wy x-dom))))))
+        (:else s)))))
+
+(define
+  fd-neq
+  (fn
+    (x y)
+    (fn
+      (s)
+      (let
+        ((c (fn (s-prime) (fd-neq-prop x y s-prime))))
+        (let
+          ((s2 (fd-add-constraint s c)))
+          (let
+            ((s3 (c s2)))
+            (cond ((= s3 nil) mzero) (:else (unit s3)))))))))
+
+;; --- labelling ---
+
 (define
   fd-try-each-value
   (fn
@@ -157,9 +230,11 @@
         (let
           ((s2 (mk-unify x (first dom) s)))
           (let
-            ((this-stream (cond ((= s2 nil) mzero) (:else (unit s2))))
-              (rest-stream (fd-try-each-value x (rest dom) s)))
-            (mk-mplus this-stream rest-stream)))))))
+            ((s3 (cond ((= s2 nil) nil) (:else (fd-fire-store s2)))))
+            (let
+              ((this-stream (cond ((= s3 nil) mzero) (:else (unit s3))))
+                (rest-stream (fd-try-each-value x (rest dom) s)))
+              (mk-mplus this-stream rest-stream))))))))
 
 (define
   fd-label-one

lib/minikanren/tests/clpfd-neq.sx

@@ -0,0 +1,82 @@
+;; 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!)