diff --git a/lib/minikanren/clpfd.sx b/lib/minikanren/clpfd.sx index ce2c36d8..bd03ece2 100644 --- a/lib/minikanren/clpfd.sx +++ b/lib/minikanren/clpfd.sx @@ -534,3 +534,42 @@ (let ((s3 (c s2))) (cond ((= s3 nil) mzero) (:else (unit s3))))))))) + +;; --- fd-times (x * y = z, ground-cases propagator) --- + +(define + fd-times-prop + (fn + (x y z s) + (let + ((wx (mk-walk x s)) (wy (mk-walk y s)) (wz (mk-walk z s))) + (cond + ((and (number? wx) (number? wy) (number? wz)) + (cond ((= (* wx wy) wz) s) (:else nil))) + ((and (number? wx) (number? wy)) + (fd-bind-or-narrow wz (* wx wy) s)) + ((and (number? wx) (number? wz)) + (cond + ((= wx 0) (cond ((= wz 0) s) (:else nil))) + ((not (= (mod wz wx) 0)) nil) + (:else (fd-bind-or-narrow wy (/ wz wx) s)))) + ((and (number? wy) (number? wz)) + (cond + ((= wy 0) (cond ((= wz 0) s) (:else nil))) + ((not (= (mod wz wy) 0)) nil) + (:else (fd-bind-or-narrow wx (/ wz wy) s)))) + (:else s))))) + +(define + fd-times + (fn + (x y z) + (fn + (s) + (let + ((c (fn (sp) (fd-times-prop x y z sp)))) + (let + ((s2 (fd-add-constraint s c))) + (let + ((s3 (c s2))) + (cond ((= s3 nil) mzero) (:else (unit s3))))))))) diff --git a/lib/minikanren/tests/clpfd-times.sx b/lib/minikanren/tests/clpfd-times.sx new file mode 100644 index 00000000..c858a537 --- /dev/null +++ b/lib/minikanren/tests/clpfd-times.sx @@ -0,0 +1,85 @@ +;; lib/minikanren/tests/clpfd-times.sx — fd-times (x * y = z). + +(mk-test + "fd-times-3-4" + (run* q (fresh (z) (fd-times 3 4 z) (== q z))) + (list 12)) + +(mk-test + "fd-times-recover-divisor" + (run* q (fresh (x) (fd-times x 5 30) (== q x))) + (list 6)) + +(mk-test + "fd-times-non-divisible-fails" + (run* q (fresh (x) (fd-times x 5 31) (== q x))) + (list)) + +(mk-test + "fd-times-by-zero" + (run* q (fresh (z) (fd-times 0 99 z) (== q z))) + (list 0)) + +(mk-test + "fd-times-zero-by-anything-zero" + (run* + q + (fresh + (x) + (fd-in x (list 1 2 3)) + (fd-times x 0 0) + (fd-label (list x)) + (== q x))) + (list 1 2 3)) + +(mk-test + "fd-times-12-divisor-pairs" + (run* + q + (fresh + (x y) + (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) + (fd-label (list x y)) + (== q (list x y)))) + (list + (list 2 6) + (list 3 4) + (list 4 3) + (list 6 2))) + +(mk-test + "fd-times-square-of-each" + (run* + q + (fresh + (x z) + (fd-in x (list 1 2 3 4 5)) + (fd-times x x z) + (fd-label (list x)) + (== q (list x z)))) + (list + (list 1 1) + (list 2 4) + (list 3 9) + (list 4 16) + (list 5 25))) + +(mk-tests-run!)