diff --git a/lib/minikanren/intarith.sx b/lib/minikanren/intarith.sx new file mode 100644 index 00000000..7f16a36b --- /dev/null +++ b/lib/minikanren/intarith.sx @@ -0,0 +1,56 @@ +;; lib/minikanren/intarith.sx — fast integer arithmetic via project. +;; +;; These are ground-only escapes into host arithmetic. They run at native +;; speed (host ints) but require their arguments to walk to actual numbers +;; — they are not relational the way `pluso` (Peano) is. Use them when +;; the puzzle size makes Peano impractical. +;; +;; Naming: `-i` suffix marks "integer-only" goals. + +(define + pluso-i + (fn + (a b c) + (project + (a b) + (if (and (number? a) (number? b)) (== c (+ a b)) fail)))) + +(define + minuso-i + (fn + (a b c) + (project + (a b) + (if (and (number? a) (number? b)) (== c (- a b)) fail)))) + +(define + *o-i + (fn + (a b c) + (project + (a b) + (if (and (number? a) (number? b)) (== c (* a b)) fail)))) + +(define + lto-i + (fn + (a b) + (project + (a b) + (if (and (number? a) (and (number? b) (< a b))) succeed fail)))) + +(define + lteo-i + (fn + (a b) + (project + (a b) + (if (and (number? a) (and (number? b) (<= a b))) succeed fail)))) + +(define + neqo-i + (fn + (a b) + (project + (a b) + (if (and (number? a) (and (number? b) (not (= a b)))) succeed fail)))) diff --git a/lib/minikanren/tests/intarith.sx b/lib/minikanren/tests/intarith.sx new file mode 100644 index 00000000..d81db4c1 --- /dev/null +++ b/lib/minikanren/tests/intarith.sx @@ -0,0 +1,89 @@ +;; lib/minikanren/tests/intarith.sx — ground-only integer arithmetic +;; goals that escape into host operations via project. + +;; --- pluso-i --- + +(mk-test + "pluso-i-forward" + (run* q (pluso-i 7 8 q)) + (list 15)) +(mk-test + "pluso-i-zero" + (run* q (pluso-i 0 0 q)) + (list 0)) +(mk-test + "pluso-i-negatives" + (run* q (pluso-i -5 3 q)) + (list -2)) +(mk-test + "pluso-i-non-ground-fails" + (run* q (fresh (a) (pluso-i a 3 5))) + (list)) + +;; --- minuso-i --- + +(mk-test + "minuso-i-forward" + (run* q (minuso-i 10 4 q)) + (list 6)) +(mk-test + "minuso-i-zero" + (run* q (minuso-i 5 5 q)) + (list 0)) + +;; --- *o-i --- + +(mk-test + "times-i-forward" + (run* q (*o-i 6 7 q)) + (list 42)) +(mk-test + "times-i-by-zero" + (run* q (*o-i 0 99 q)) + (list 0)) +(mk-test + "times-i-by-one" + (run* q (*o-i 1 17 q)) + (list 17)) + +;; --- comparisons --- + +(mk-test + "lto-i-true" + (run 1 q (lto-i 2 5)) + (list (make-symbol "_.0"))) +(mk-test "lto-i-false" (run* q (lto-i 5 2)) (list)) +(mk-test "lto-i-equal-false" (run* q (lto-i 3 3)) (list)) + +(mk-test + "lteo-i-equal" + (run 1 q (lteo-i 4 4)) + (list (make-symbol "_.0"))) +(mk-test + "lteo-i-less" + (run 1 q (lteo-i 1 4)) + (list (make-symbol "_.0"))) +(mk-test "lteo-i-more" (run* q (lteo-i 9 4)) (list)) + +(mk-test + "neqo-i-different" + (run 1 q (neqo-i 3 5)) + (list (make-symbol "_.0"))) +(mk-test "neqo-i-same" (run* q (neqo-i 3 3)) (list)) + +;; --- composition with relational vars --- + +(mk-test + "intarith-with-membero" + (run* + q + (fresh + (x) + (membero + x + (list 1 2 3 4 5)) + (lto-i x 3) + (== q x))) + (list 1 2)) + +(mk-tests-run!) diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md index 82f2c568..8e58641c 100644 --- a/plans/minikanren-on-sx.md +++ b/plans/minikanren-on-sx.md @@ -173,6 +173,13 @@ _(none yet)_ _Newest first._ +- **2026-05-08** — **intarith.sx — fast ground-only integer arithmetic**: + pluso-i / minuso-i / *o-i / lto-i / lteo-i / neqo-i wrap host arithmetic + via `project`. They are not relational like Peano `pluso` (require args + to walk to numbers), but run at native host speed — a viable escape + hatch when puzzle size makes Peano impractical. Composes with relational + goals: `(membero x dom) (lto-i x 3)` filters dom by `< 3`. 18 new tests, + 287/287 cumulative. - **2026-05-08** — **2x2 Latin square**: small classic constraint demo using `ino` + 4 `all-distincto` constraints. Enumerates exactly 2 squares (`((1 2)(2 1))` and `((2 1)(1 2))`); a clue (top-left = 1) narrows to one.