mk: phase 6F — fd-distinct (pairwise alldifferent)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 53s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 53s
(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.
This commit is contained in:
@@ -459,3 +459,28 @@
|
|||||||
(cond
|
(cond
|
||||||
((empty? vars) succeed)
|
((empty? vars) succeed)
|
||||||
(:else (mk-conj (fd-label-one (first vars)) (fd-label (rest vars)))))))
|
(: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)))))))
|
||||||
|
|||||||
52
lib/minikanren/tests/clpfd-distinct.sx
Normal file
52
lib/minikanren/tests/clpfd-distinct.sx
Normal file
@@ -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!)
|
||||||
Reference in New Issue
Block a user