mk: phase 6C — fd-in + fd-label (domain narrowing + labelling)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 51s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 51s
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.
This commit is contained in:
@@ -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)))))))
|
||||
|
||||
120
lib/minikanren/tests/clpfd-in-label.sx
Normal file
120
lib/minikanren/tests/clpfd-in-label.sx
Normal file
@@ -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!)
|
||||
Reference in New Issue
Block a user