From f2817bb6beb1a5a226257b52b86a2ea87c142a64 Mon Sep 17 00:00:00 2001 From: giles Date: Fri, 8 May 2026 14:09:18 +0000 Subject: [PATCH] =?UTF-8?q?mk:=20phase=206C=20=E2=80=94=20fd-in=20+=20fd-l?= =?UTF-8?q?abel=20(domain=20narrowing=20+=20labelling)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit fd-in x dom-list: narrows x's domain. If x is a ground number, checks membership; if x is a logic var, intersects existing domain (or sets fresh) and stores via fd-set-domain. Fails if domain becomes empty. fd-label vars: drives search by enumerating each var's domain. Each var is unified with each value in its domain, in order, via mk-mplus of singleton streams. Forward: (fd-in x dom) (fd-label (list x)) iterates x over dom. Intersection: two fd-in goals on the same var compose via dom-intersect. Disjoint domains -> empty answer set. Ground value membership check gates pass/fail. Composes with the rest of the miniKanren machinery — fresh / conde / membero etc. all work alongside. 9 new tests, 586/586 cumulative. --- lib/minikanren/clpfd.sx | 63 +++++++++++++ lib/minikanren/tests/clpfd-in-label.sx | 120 +++++++++++++++++++++++++ 2 files changed, 183 insertions(+) create mode 100644 lib/minikanren/tests/clpfd-in-label.sx diff --git a/lib/minikanren/clpfd.sx b/lib/minikanren/clpfd.sx index 0b9134ee..46c3ff52 100644 --- a/lib/minikanren/clpfd.sx +++ b/lib/minikanren/clpfd.sx @@ -123,3 +123,66 @@ (let ((store-prime (assoc store :domains doms-prime))) (fd-with-store s store-prime)))))))) + +(define + fd-in + (fn + (x dom-list) + (fn + (s) + (let + ((new-dom (fd-dom-from-list dom-list))) + (let + ((wx (mk-walk x s))) + (cond + ((number? wx) + (cond ((fd-dom-member? wx new-dom) (unit s)) (:else mzero))) + ((is-var? wx) + (let + ((existing (fd-domain-of s (var-name wx)))) + (let + ((narrowed (cond ((= existing nil) new-dom) (:else (fd-dom-intersect existing new-dom))))) + (let + ((s2 (fd-set-domain s (var-name wx) narrowed))) + (cond ((= s2 nil) mzero) (:else (unit s2))))))) + (:else mzero))))))) + +(define + fd-try-each-value + (fn + (x dom s) + (cond + ((empty? dom) mzero) + (:else + (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))))))) + +(define + fd-label-one + (fn + (x) + (fn + (s) + (let + ((wx (mk-walk x s))) + (cond + ((number? wx) (unit s)) + ((is-var? wx) + (let + ((dom (fd-domain-of s (var-name wx)))) + (cond + ((= dom nil) mzero) + (:else (fd-try-each-value wx dom s))))) + (:else mzero)))))) + +(define + fd-label + (fn + (vars) + (cond + ((empty? vars) succeed) + (:else (mk-conj (fd-label-one (first vars)) (fd-label (rest vars))))))) diff --git a/lib/minikanren/tests/clpfd-in-label.sx b/lib/minikanren/tests/clpfd-in-label.sx new file mode 100644 index 00000000..7393fdf6 --- /dev/null +++ b/lib/minikanren/tests/clpfd-in-label.sx @@ -0,0 +1,120 @@ +;; lib/minikanren/tests/clpfd-in-label.sx — fd-in (domain narrowing) + fd-label. + +;; --- fd-in: domain narrowing --- + +(mk-test + "fd-in-bare-label" + (run* + q + (fresh + (x) + (fd-in x (list 1 2 3 4 5)) + (fd-label (list x)) + (== q x))) + (list 1 2 3 4 5)) + +(mk-test + "fd-in-intersection" + (run* + q + (fresh + (x) + (fd-in x (list 1 2 3 4 5)) + (fd-in x (list 3 4 5 6 7)) + (fd-label (list x)) + (== q x))) + (list 3 4 5)) + +(mk-test + "fd-in-disjoint-empty" + (run* + q + (fresh + (x) + (fd-in x (list 1 2 3)) + (fd-in x (list 7 8 9)) + (fd-label (list x)) + (== q x))) + (list)) + +(mk-test + "fd-in-singleton-domain" + (run* + q + (fresh (x) (fd-in x (list 5)) (fd-label (list x)) (== q x))) + (list 5)) + +;; --- ground value checks the domain --- + +(mk-test + "fd-in-ground-in-domain" + (run* + q + (fresh + (x) + (== x 3) + (fd-in x (list 1 2 3 4 5)) + (== q x))) + (list 3)) + +(mk-test + "fd-in-ground-not-in-domain" + (run* + q + (fresh + (x) + (== x 9) + (fd-in x (list 1 2 3 4 5)) + (== q x))) + (list)) + +;; --- fd-label across multiple vars --- + +(mk-test + "fd-label-multiple-vars" + (let + ((res (run* q (fresh (a b) (fd-in a (list 1 2 3)) (fd-in b (list 10 20)) (fd-label (list a b)) (== q (list a b)))))) + (= (len res) 6)) + true) + +(mk-test + "fd-label-empty-vars" + (run* q (fd-label (list))) + (list (make-symbol "_.0"))) + +;; --- composition with regular goals --- + +(mk-test + "fd-in-with-membero-style-filtering" + (run* + q + (fresh + (x) + (fd-in + x + (list + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 + 10)) + (fd-label (list x)) + (== q x))) + (list + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 + 10)) + +(mk-tests-run!)