diff --git a/lib/minikanren/clpfd.sx b/lib/minikanren/clpfd.sx index b55df8ba..e356e60a 100644 --- a/lib/minikanren/clpfd.sx +++ b/lib/minikanren/clpfd.sx @@ -177,7 +177,7 @@ (cond ((= s2 nil) mzero) (:else (unit s2))))))) (:else mzero))))))) -;; --- fd-neq with propagation --- +;; --- fd-neq --- (define fd-neq-prop @@ -218,6 +218,204 @@ ((s3 (c s2))) (cond ((= s3 nil) mzero) (:else (unit s3))))))))) +;; --- fd-lt --- + +(define + fd-lt-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) s) (:else nil))) + ((and (number? wx) (is-var? wy)) + (let + ((yd (fd-domain-of s (var-name wy)))) + (cond + ((= yd nil) s) + (:else + (fd-set-domain + s + (var-name wy) + (filter (fn (v) (> v wx)) yd)))))) + ((and (is-var? wx) (number? wy)) + (let + ((xd (fd-domain-of s (var-name wx)))) + (cond + ((= xd nil) s) + (:else + (fd-set-domain + s + (var-name wx) + (filter (fn (v) (< v wy)) xd)))))) + ((and (is-var? wx) (is-var? wy)) + (let + ((xd (fd-domain-of s (var-name wx))) + (yd (fd-domain-of s (var-name wy)))) + (cond + ((or (= xd nil) (= yd nil)) s) + (:else + (let + ((xd-prime (filter (fn (v) (< v (fd-dom-max yd))) xd))) + (let + ((s2 (fd-set-domain s (var-name wx) xd-prime))) + (cond + ((= s2 nil) nil) + (:else + (let + ((yd-prime (filter (fn (v) (> v (fd-dom-min xd-prime))) yd))) + (fd-set-domain s2 (var-name wy) yd-prime)))))))))) + (:else s))))) + +(define + fd-lt + (fn + (x y) + (fn + (s) + (let + ((c (fn (sp) (fd-lt-prop x y sp)))) + (let + ((s2 (fd-add-constraint s c))) + (let + ((s3 (c s2))) + (cond ((= s3 nil) mzero) (:else (unit s3))))))))) + +;; --- fd-lte --- + +(define + fd-lte-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) s) (:else nil))) + ((and (number? wx) (is-var? wy)) + (let + ((yd (fd-domain-of s (var-name wy)))) + (cond + ((= yd nil) s) + (:else + (fd-set-domain + s + (var-name wy) + (filter (fn (v) (>= v wx)) yd)))))) + ((and (is-var? wx) (number? wy)) + (let + ((xd (fd-domain-of s (var-name wx)))) + (cond + ((= xd nil) s) + (:else + (fd-set-domain + s + (var-name wx) + (filter (fn (v) (<= v wy)) xd)))))) + ((and (is-var? wx) (is-var? wy)) + (let + ((xd (fd-domain-of s (var-name wx))) + (yd (fd-domain-of s (var-name wy)))) + (cond + ((or (= xd nil) (= yd nil)) s) + (:else + (let + ((xd-prime (filter (fn (v) (<= v (fd-dom-max yd))) xd))) + (let + ((s2 (fd-set-domain s (var-name wx) xd-prime))) + (cond + ((= s2 nil) nil) + (:else + (let + ((yd-prime (filter (fn (v) (>= v (fd-dom-min xd-prime))) yd))) + (fd-set-domain s2 (var-name wy) yd-prime)))))))))) + (:else s))))) + +(define + fd-lte + (fn + (x y) + (fn + (s) + (let + ((c (fn (sp) (fd-lte-prop x y sp)))) + (let + ((s2 (fd-add-constraint s c))) + (let + ((s3 (c s2))) + (cond ((= s3 nil) mzero) (:else (unit s3))))))))) + +;; --- fd-eq --- + +(define + fd-eq-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) s) (:else nil))) + ((and (number? wx) (is-var? wy)) + (let + ((yd (fd-domain-of s (var-name wy)))) + (cond + ((and (not (= yd nil)) (not (fd-dom-member? wx yd))) nil) + (:else + (let + ((s2 (mk-unify wy wx s))) + (cond ((= s2 nil) nil) (:else s2))))))) + ((and (is-var? wx) (number? wy)) + (let + ((xd (fd-domain-of s (var-name wx)))) + (cond + ((and (not (= xd nil)) (not (fd-dom-member? wy xd))) nil) + (:else + (let + ((s2 (mk-unify wx wy s))) + (cond ((= s2 nil) nil) (:else s2))))))) + ((and (is-var? wx) (is-var? wy)) + (let + ((xd (fd-domain-of s (var-name wx))) + (yd (fd-domain-of s (var-name wy)))) + (cond + ((and (= xd nil) (= yd nil)) + (let + ((s2 (mk-unify wx wy s))) + (cond ((= s2 nil) nil) (:else s2)))) + (:else + (let + ((shared (cond ((= xd nil) yd) ((= yd nil) xd) (:else (fd-dom-intersect xd yd))))) + (cond + ((fd-dom-empty? shared) nil) + (:else + (let + ((s2 (fd-set-domain s (var-name wx) shared))) + (cond + ((= s2 nil) nil) + (:else + (let + ((s3 (fd-set-domain s2 (var-name wy) shared))) + (cond + ((= s3 nil) nil) + (:else (mk-unify wx wy s3)))))))))))))) + (:else s))))) + +(define + fd-eq + (fn + (x y) + (fn + (s) + (let + ((c (fn (sp) (fd-eq-prop x y sp)))) + (let + ((s2 (fd-add-constraint s c))) + (let + ((s3 (c s2))) + (cond ((= s3 nil) mzero) (:else (unit s3))))))))) + ;; --- labelling --- (define diff --git a/lib/minikanren/tests/clpfd-ord.sx b/lib/minikanren/tests/clpfd-ord.sx new file mode 100644 index 00000000..535f127d --- /dev/null +++ b/lib/minikanren/tests/clpfd-ord.sx @@ -0,0 +1,128 @@ +;; lib/minikanren/tests/clpfd-ord.sx — fd-lt / fd-lte / fd-eq. + +;; --- fd-lt --- + +(mk-test + "fd-lt-narrows-x-against-num" + (run* + q + (fresh + (x) + (fd-in x (list 1 2 3 4 5)) + (fd-lt x 3) + (fd-label (list x)) + (== q x))) + (list 1 2)) + +(mk-test + "fd-lt-narrows-x-against-num-symmetric" + (run* + q + (fresh + (x) + (fd-in x (list 1 2 3 4 5)) + (fd-lt 3 x) + (fd-label (list x)) + (== q x))) + (list 4 5)) + +(mk-test + "fd-lt-pair-ordered" + (let + ((res (run* q (fresh (x y) (fd-in x (list 1 2 3 4)) (fd-in y (list 1 2 3 4)) (fd-lt x y) (fd-label (list x y)) (== q (list x y)))))) + (= (len res) 6)) + true) + +(mk-test + "fd-lt-impossible-fails" + (run* + q + (fresh + (x) + (fd-in x (list 5 6 7)) + (fd-lt x 3) + (fd-label (list x)) + (== q x))) + (list)) + +;; --- fd-lte --- + +(mk-test + "fd-lte-includes-equal" + (run* + q + (fresh + (x) + (fd-in x (list 1 2 3 4 5)) + (fd-lte x 3) + (fd-label (list x)) + (== q x))) + (list 1 2 3)) + +(mk-test + "fd-lte-equal-bound" + (run* + q + (fresh + (x) + (fd-in x (list 1 2 3 4 5)) + (fd-lte 3 x) + (fd-label (list x)) + (== q x))) + (list 3 4 5)) + +;; --- fd-eq --- + +(mk-test + "fd-eq-bind" + (run* + q + (fresh + (x) + (fd-in x (list 1 2 3 4 5)) + (fd-eq x 3) + (== q x))) + (list 3)) + +(mk-test + "fd-eq-out-of-domain-fails" + (run* + q + (fresh + (x) + (fd-in x (list 1 2 3)) + (fd-eq x 5) + (== q x))) + (list)) + +(mk-test + "fd-eq-two-vars-share-domain" + (run* + q + (fresh + (x y) + (fd-in x (list 1 2 3)) + (fd-in y (list 2 3 4)) + (fd-eq x y) + (fd-label (list x y)) + (== q (list x y)))) + (list (list 2 2) (list 3 3))) + +;; --- combine fd-lt + fd-neq for "between" puzzle --- + +(mk-test + "fd-lt-neq-combined" + (run* + q + (fresh + (x y z) + (fd-in x (list 1 2 3)) + (fd-in y (list 1 2 3)) + (fd-in z (list 1 2 3)) + (fd-lt x y) + (fd-lt y z) + (fd-label (list x y z)) + (== q (list x y z)))) + (list (list 1 2 3))) + +(mk-tests-run!)