From c01ddc2b2392dafe6ca9a4cecef5afdd2c44ba28 Mon Sep 17 00:00:00 2001
From: giles <giles.bradshaw@rose-ash.com>
Date: Fri, 8 May 2026 14:34:10 +0000
Subject: [PATCH] =?UTF-8?q?mk:=20phase=206E=20=E2=80=94=20fd-lt=20+=20fd-l?=
 =?UTF-8?q?te=20+=20fd-eq=20with=20propagation?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Three more constraint goals built on the same propagator-store
machinery as fd-neq:

fd-lt: x < y. Ground/ground compares; var/num filters domain;
var/var narrows x's domain to (< y-max) and y's to (> x-min).

fd-lte: ≤ variant.

fd-eq: x = y. Ground/ground checks. Var/num: requires num to be in
var's domain (or var unconstrained) before binding. Var/var: intersect
domains, narrow both, then unify the vars.

10 new tests: narrowing against ground, ordered-pair generation,
chained x<y<z determinism, domain-sharing, out-of-domain rejection.
603/603 cumulative (100/100 across the four CLP(FD) test files).
---
 lib/minikanren/clpfd.sx           | 200 +++++++++++++++++++++++++++++-
 lib/minikanren/tests/clpfd-ord.sx | 128 +++++++++++++++++++
 2 files changed, 327 insertions(+), 1 deletion(-)
 create mode 100644 lib/minikanren/tests/clpfd-ord.sx

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