mk: phase 6H — fd-times (x * y = z)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 56s

Ground-cases propagator parallel to fd-plus. Division back-direction
checks (mod z x) = 0 before recovering a divisor. Edge cases:
multiplying by zero binds the product to zero; with z=0 and one
factor zero, the other factor is unconstrained.

7 tests including divisor enumeration, square-of-each, divisibility
rejection. 624/624 cumulative.
This commit is contained in:
2026-05-08 14:37:17 +00:00
parent 5d3c248fdd
commit a6e758664b
2 changed files with 124 additions and 0 deletions

View File

@@ -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)))))))))