From 27637aa0f9401b485803d52e4a3a1c147f7d29b1 Mon Sep 17 00:00:00 2001 From: giles Date: Fri, 8 May 2026 14:24:28 +0000 Subject: [PATCH] =?UTF-8?q?mk:=20phase=206D=20=E2=80=94=20fd-neq=20with=20?= =?UTF-8?q?propagation=20+=20constraint=20reactivation?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 | 103 ++++++++++++++++++++++++++---- lib/minikanren/tests/clpfd-neq.sx | 82 ++++++++++++++++++++++++ 2 files changed, 171 insertions(+), 14 deletions(-) create mode 100644 lib/minikanren/tests/clpfd-neq.sx diff --git a/lib/minikanren/clpfd.sx b/lib/minikanren/clpfd.sx index 46c3ff52..b55df8ba 100644 --- a/lib/minikanren/clpfd.sx +++ b/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 diff --git a/lib/minikanren/tests/clpfd-neq.sx b/lib/minikanren/tests/clpfd-neq.sx new file mode 100644 index 00000000..2a533e3c --- /dev/null +++ b/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!)