diff --git a/lib/minikanren/clpfd.sx b/lib/minikanren/clpfd.sx index e356e60a..fedc87c7 100644 --- a/lib/minikanren/clpfd.sx +++ b/lib/minikanren/clpfd.sx @@ -459,3 +459,28 @@ (cond ((empty? vars) succeed) (: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))))))) diff --git a/lib/minikanren/tests/clpfd-distinct.sx b/lib/minikanren/tests/clpfd-distinct.sx new file mode 100644 index 00000000..1c2d7d11 --- /dev/null +++ b/lib/minikanren/tests/clpfd-distinct.sx @@ -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!)