diff --git a/lib/minikanren/clpfd.sx b/lib/minikanren/clpfd.sx index ab2fb10b..46fd4fff 100644 --- a/lib/minikanren/clpfd.sx +++ b/lib/minikanren/clpfd.sx @@ -519,6 +519,118 @@ (cond ((= s2 nil) nil) (:else s2))))))) (:else nil)))) +(define + fd-narrow-or-skip + (fn + (s var-key d lo hi) + (cond + ((= d nil) s) + (:else + (fd-set-domain + s + var-key + (filter (fn (v) (and (>= v lo) (<= v hi))) d)))))) + +(define + fd-plus-prop-vvn + (fn + (wx wy wz s) + (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 + ((s1 (fd-narrow-or-skip s (var-name wx) xd (- wz (fd-dom-max yd)) (- wz (fd-dom-min yd))))) + (cond + ((= s1 nil) nil) + (:else + (let + ((xd2 (fd-domain-of s1 (var-name wx)))) + (fd-narrow-or-skip + s1 + (var-name wy) + yd + (- wz (fd-dom-max xd2)) + (- wz (fd-dom-min xd2)))))))))))) + +(define + fd-plus-prop-nvv + (fn + (wx wy wz s) + (let + ((yd (fd-domain-of s (var-name wy))) + (zd (fd-domain-of s (var-name wz)))) + (cond + ((or (= yd nil) (= zd nil)) s) + (:else + (let + ((s1 (fd-narrow-or-skip s (var-name wy) yd (- (fd-dom-min zd) wx) (- (fd-dom-max zd) wx)))) + (cond + ((= s1 nil) nil) + (:else + (let + ((yd2 (fd-domain-of s1 (var-name wy)))) + (fd-narrow-or-skip + s1 + (var-name wz) + zd + (+ wx (fd-dom-min yd2)) + (+ wx (fd-dom-max yd2)))))))))))) + +(define + fd-plus-prop-vnv + (fn + (wx wy wz s) + (let + ((xd (fd-domain-of s (var-name wx))) + (zd (fd-domain-of s (var-name wz)))) + (cond + ((or (= xd nil) (= zd nil)) s) + (:else + (let + ((s1 (fd-narrow-or-skip s (var-name wx) xd (- (fd-dom-min zd) wy) (- (fd-dom-max zd) wy)))) + (cond + ((= s1 nil) nil) + (:else + (let + ((xd2 (fd-domain-of s1 (var-name wx)))) + (fd-narrow-or-skip + s1 + (var-name wz) + zd + (+ (fd-dom-min xd2) wy) + (+ (fd-dom-max xd2) wy))))))))))) + +(define + fd-plus-prop-vvv + (fn + (wx wy wz s) + (let + ((xd (fd-domain-of s (var-name wx))) + (yd (fd-domain-of s (var-name wy))) + (zd (fd-domain-of s (var-name wz)))) + (cond + ((or (= xd nil) (or (= yd nil) (= zd nil))) s) + (:else + (let + ((s1 (fd-narrow-or-skip s (var-name wx) xd (- (fd-dom-min zd) (fd-dom-max yd)) (- (fd-dom-max zd) (fd-dom-min yd))))) + (cond + ((= s1 nil) nil) + (:else + (let + ((s2 (fd-narrow-or-skip s1 (var-name wy) yd (- (fd-dom-min zd) (fd-dom-max xd)) (- (fd-dom-max zd) (fd-dom-min xd))))) + (cond + ((= s2 nil) nil) + (:else + (fd-narrow-or-skip + s2 + (var-name wz) + zd + (+ (fd-dom-min xd) (fd-dom-min yd)) + (+ (fd-dom-max xd) (fd-dom-max yd)))))))))))))) + (define fd-plus-prop (fn @@ -534,6 +646,14 @@ (fd-bind-or-narrow wy (- wz wx) s)) ((and (number? wy) (number? wz)) (fd-bind-or-narrow wx (- wz wy) s)) + ((and (is-var? wx) (is-var? wy) (number? wz)) + (fd-plus-prop-vvn wx wy wz s)) + ((and (number? wx) (is-var? wy) (is-var? wz)) + (fd-plus-prop-nvv wx wy wz s)) + ((and (is-var? wx) (number? wy) (is-var? wz)) + (fd-plus-prop-vnv wx wy wz s)) + ((and (is-var? wx) (is-var? wy) (is-var? wz)) + (fd-plus-prop-vvv wx wy wz s)) (:else s))))) (define @@ -552,6 +672,134 @@ ;; --- fd-times (x * y = z, ground-cases propagator) --- +(define + fd-int-ceil-div + (fn + (a b) + (cond + ((= (mod a b) 0) (/ a b)) + (:else (+ (fd-int-floor-div a b) 1))))) + +(define fd-int-floor-div (fn (a b) (/ (- a (mod a b)) b))) + +(define + fd-dom-positive? + (fn + (d) + (cond ((empty? d) false) (:else (>= (fd-dom-min d) 1))))) + +(define + fd-times-prop-vvv + (fn + (wx wy wz s) + (let + ((xd (fd-domain-of s (var-name wx))) + (yd (fd-domain-of s (var-name wy))) + (zd (fd-domain-of s (var-name wz)))) + (cond + ((or (= xd nil) (or (= yd nil) (= zd nil))) s) + ((not (and (fd-dom-positive? xd) (and (fd-dom-positive? yd) (fd-dom-positive? zd)))) + s) + (:else + (let + ((s1 (fd-narrow-or-skip s (var-name wx) xd (fd-int-ceil-div (fd-dom-min zd) (fd-dom-max yd)) (fd-int-floor-div (fd-dom-max zd) (fd-dom-min yd))))) + (cond + ((= s1 nil) nil) + (:else + (let + ((s2 (fd-narrow-or-skip s1 (var-name wy) yd (fd-int-ceil-div (fd-dom-min zd) (fd-dom-max xd)) (fd-int-floor-div (fd-dom-max zd) (fd-dom-min xd))))) + (cond + ((= s2 nil) nil) + (:else + (fd-narrow-or-skip + s2 + (var-name wz) + zd + (* (fd-dom-min xd) (fd-dom-min yd)) + (* (fd-dom-max xd) (fd-dom-max yd)))))))))))))) + +(define + fd-times-prop-vvn + (fn + (wx wy wz s) + (let + ((xd (fd-domain-of s (var-name wx))) + (yd (fd-domain-of s (var-name wy)))) + (cond + ((or (= xd nil) (= yd nil)) s) + ((not (and (fd-dom-positive? xd) (fd-dom-positive? yd))) s) + ((<= wz 0) s) + (:else + (let + ((s1 (fd-narrow-or-skip s (var-name wx) xd (fd-int-ceil-div wz (fd-dom-max yd)) (fd-int-floor-div wz (fd-dom-min yd))))) + (cond + ((= s1 nil) nil) + (:else + (let + ((xd2 (fd-domain-of s1 (var-name wx)))) + (fd-narrow-or-skip + s1 + (var-name wy) + yd + (fd-int-ceil-div wz (fd-dom-max xd2)) + (fd-int-floor-div wz (fd-dom-min xd2)))))))))))) + +(define + fd-times-prop-nvv + (fn + (wx wy wz s) + (cond + ((<= wx 0) s) + (:else + (let + ((yd (fd-domain-of s (var-name wy))) + (zd (fd-domain-of s (var-name wz)))) + (cond + ((or (= yd nil) (= zd nil)) s) + ((not (and (fd-dom-positive? yd) (fd-dom-positive? zd))) s) + (:else + (let + ((s1 (fd-narrow-or-skip s (var-name wy) yd (fd-int-ceil-div (fd-dom-min zd) wx) (fd-int-floor-div (fd-dom-max zd) wx)))) + (cond + ((= s1 nil) nil) + (:else + (let + ((yd2 (fd-domain-of s1 (var-name wy)))) + (fd-narrow-or-skip + s1 + (var-name wz) + zd + (* wx (fd-dom-min yd2)) + (* wx (fd-dom-max yd2)))))))))))))) + +(define + fd-times-prop-vnv + (fn + (wx wy wz s) + (cond + ((<= wy 0) s) + (:else + (let + ((xd (fd-domain-of s (var-name wx))) + (zd (fd-domain-of s (var-name wz)))) + (cond + ((or (= xd nil) (= zd nil)) s) + ((not (and (fd-dom-positive? xd) (fd-dom-positive? zd))) s) + (:else + (let + ((s1 (fd-narrow-or-skip s (var-name wx) xd (fd-int-ceil-div (fd-dom-min zd) wy) (fd-int-floor-div (fd-dom-max zd) wy)))) + (cond + ((= s1 nil) nil) + (:else + (let + ((xd2 (fd-domain-of s1 (var-name wx)))) + (fd-narrow-or-skip + s1 + (var-name wz) + zd + (* (fd-dom-min xd2) wy) + (* (fd-dom-max xd2) wy))))))))))))) + (define fd-times-prop (fn @@ -573,6 +821,14 @@ ((= wy 0) (cond ((= wz 0) s) (:else nil))) ((not (= (mod wz wy) 0)) nil) (:else (fd-bind-or-narrow wx (/ wz wy) s)))) + ((and (is-var? wx) (is-var? wy) (number? wz)) + (fd-times-prop-vvn wx wy wz s)) + ((and (number? wx) (is-var? wy) (is-var? wz)) + (fd-times-prop-nvv wx wy wz s)) + ((and (is-var? wx) (number? wy) (is-var? wz)) + (fd-times-prop-vnv wx wy wz s)) + ((and (is-var? wx) (is-var? wy) (is-var? wz)) + (fd-times-prop-vvv wx wy wz s)) (:else s))))) (define diff --git a/lib/minikanren/tests/clpfd-bounds.sx b/lib/minikanren/tests/clpfd-bounds.sx new file mode 100644 index 00000000..32a02f44 --- /dev/null +++ b/lib/minikanren/tests/clpfd-bounds.sx @@ -0,0 +1,316 @@ +;; lib/minikanren/tests/clpfd-bounds.sx — Phase 6 piece B: bounds-consistency +;; for fd-plus and fd-times in the partial- and all-domain cases. +;; +;; We probe domains directly (peek at the FD store) before any labelling +;; happens. This isolates the propagator's narrowing behaviour from the +;; search engine. + +(define + probe-dom + (fn + (goal var-key) + (let + ((s (first (stream-take 1 (goal empty-s))))) + (cond ((= s nil) :no-subst) (:else (fd-domain-of s var-key)))))) + +;; --- fd-plus partial-domain narrowing --- + +(mk-test + "fd-plus-vvn-narrows-x" + (let + ((x (mk-var "x")) (y (mk-var "y"))) + (probe-dom + (mk-conj + (fd-in + x + (list + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 + 10)) + (fd-in y (list 1 2 3)) + (fd-plus x y 10)) + "x")) + (list 7 8 9)) + +(mk-test + "fd-plus-vvn-narrows-y" + (let + ((x (mk-var "x")) (y (mk-var "y"))) + (probe-dom + (mk-conj + (fd-in + x + (list + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 + 10)) + (fd-in y (list 1 2 3)) + (fd-plus x y 10)) + "y")) + (list 1 2 3)) + +(mk-test + "fd-plus-nvv-narrows" + (let + ((y (mk-var "y")) (z (mk-var "z"))) + (probe-dom + (mk-conj + (fd-in y (list 1 2 3)) + (fd-in + z + (list + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 + 10 + 11 + 12 + 13 + 14 + 15 + 16 + 17 + 18 + 19 + 20)) + (fd-plus 5 y z)) + "z")) + (list 6 7 8)) + +(mk-test + "fd-plus-vvv-narrows-z" + (let + ((x (mk-var "x")) (y (mk-var "y")) (z (mk-var "z"))) + (probe-dom + (mk-conj + (fd-in x (list 1 2 3)) + (fd-in y (list 1 2 3)) + (fd-in + z + (list + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 + 10 + 11 + 12 + 13 + 14 + 15 + 16 + 17 + 18 + 19 + 20)) + (fd-plus x y z)) + "z")) + (list 2 3 4 5 6)) + +(mk-test + "fd-plus-vvv-narrows-x" + (let + ((x (mk-var "x")) (y (mk-var "y")) (z (mk-var "z"))) + (probe-dom + (mk-conj + (fd-in + x + (list + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 + 10)) + (fd-in y (list 1 2 3)) + (fd-in z (list 5 6 7)) + (fd-plus x y z)) + "x")) + (list 2 3 4 5 6)) + +;; --- fd-times partial-domain narrowing (positive domains) --- + +(mk-test + "fd-times-vvn-narrows" + (let + ((x (mk-var "x")) (y (mk-var "y"))) + (probe-dom + (mk-conj + (fd-in + x + (list + 1 + 2 + 3 + 4 + 5 + 6)) + (fd-in + y + (list + 1 + 2 + 3 + 4 + 5 + 6)) + (fd-times x y 12)) + "x")) + (list 2 3 4 5 6)) + +(mk-test + "fd-times-nvv-narrows" + (let + ((y (mk-var "y")) (z (mk-var "z"))) + (probe-dom + (mk-conj + (fd-in y (list 1 2 3 4)) + (fd-in + z + (list + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 + 10 + 11 + 12 + 13 + 14 + 15 + 16 + 17 + 18 + 19 + 20)) + (fd-times 3 y z)) + "z")) + (list + 3 + 4 + 5 + 6 + 7 + 8 + 9 + 10 + 11 + 12)) + +(mk-test + "fd-times-vvv-narrows" + (let + ((x (mk-var "x")) (y (mk-var "y")) (z (mk-var "z"))) + (probe-dom + (mk-conj + (fd-in x (list 1 2 3)) + (fd-in y (list 1 2 3)) + (fd-in + z + (list + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 + 10 + 11 + 12 + 13 + 14 + 15 + 16 + 17 + 18 + 19 + 20)) + (fd-times x y z)) + "z")) + (list + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9)) + +;; --- bounds force impossible branches to fail early --- + +(mk-test + "fd-plus-impossible-via-bounds" + (let + ((x (mk-var "x")) (y (mk-var "y"))) + (probe-dom + (mk-conj + (fd-in + x + (list + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 + 10)) + (fd-in + y + (list + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 + 10)) + (fd-plus x y 100)) + "x")) + :no-subst) + +(mk-tests-run!)