Merge loops/minikanren into architecture: Phase 5 disequality + Phase 6 FD constraints + Phase 7 SLG tabling
Phase 5: =/= disequality with constraint store. Phase 6: bounds-consistency for fd-plus/fd-times, send-more-money, Sudoku 4x4, N-queens FD. Phase 7: SLG-style tabling with in-progress sentinel + fixed-point iteration (Fibonacci + Ackermann canaries green).
This commit is contained in:
@@ -230,8 +230,10 @@
|
||||
(let
|
||||
((s2 (fd-add-constraint s c)))
|
||||
(let
|
||||
((s3 (c s2)))
|
||||
(cond ((= s3 nil) mzero) (:else (unit s3)))))))))
|
||||
((s2-or-nil (c s2)))
|
||||
(let
|
||||
((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil)))))
|
||||
(cond ((= s3 nil) mzero) (:else (unit s3))))))))))
|
||||
|
||||
;; --- fd-lt ---
|
||||
|
||||
@@ -294,8 +296,10 @@
|
||||
(let
|
||||
((s2 (fd-add-constraint s c)))
|
||||
(let
|
||||
((s3 (c s2)))
|
||||
(cond ((= s3 nil) mzero) (:else (unit s3)))))))))
|
||||
((s2-or-nil (c s2)))
|
||||
(let
|
||||
((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil)))))
|
||||
(cond ((= s3 nil) mzero) (:else (unit s3))))))))))
|
||||
|
||||
;; --- fd-lte ---
|
||||
|
||||
@@ -358,8 +362,10 @@
|
||||
(let
|
||||
((s2 (fd-add-constraint s c)))
|
||||
(let
|
||||
((s3 (c s2)))
|
||||
(cond ((= s3 nil) mzero) (:else (unit s3)))))))))
|
||||
((s2-or-nil (c s2)))
|
||||
(let
|
||||
((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil)))))
|
||||
(cond ((= s3 nil) mzero) (:else (unit s3))))))))))
|
||||
|
||||
;; --- fd-eq ---
|
||||
|
||||
@@ -428,8 +434,10 @@
|
||||
(let
|
||||
((s2 (fd-add-constraint s c)))
|
||||
(let
|
||||
((s3 (c s2)))
|
||||
(cond ((= s3 nil) mzero) (:else (unit s3)))))))))
|
||||
((s2-or-nil (c s2)))
|
||||
(let
|
||||
((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil)))))
|
||||
(cond ((= s3 nil) mzero) (:else (unit s3))))))))))
|
||||
|
||||
;; --- labelling ---
|
||||
|
||||
@@ -519,6 +527,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 +654,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
|
||||
@@ -547,11 +675,141 @@
|
||||
(let
|
||||
((s2 (fd-add-constraint s c)))
|
||||
(let
|
||||
((s3 (c s2)))
|
||||
(cond ((= s3 nil) mzero) (:else (unit s3)))))))))
|
||||
((s2-or-nil (c s2)))
|
||||
(let
|
||||
((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil)))))
|
||||
(cond ((= s3 nil) mzero) (:else (unit s3))))))))))
|
||||
|
||||
;; --- 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 +831,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
|
||||
@@ -586,5 +852,7 @@
|
||||
(let
|
||||
((s2 (fd-add-constraint s c)))
|
||||
(let
|
||||
((s3 (c s2)))
|
||||
(cond ((= s3 nil) mzero) (:else (unit s3)))))))))
|
||||
((s2-or-nil (c s2)))
|
||||
(let
|
||||
((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil)))))
|
||||
(cond ((= s3 nil) mzero) (:else (unit s3))))))))))
|
||||
|
||||
71
lib/minikanren/diseq.sx
Normal file
71
lib/minikanren/diseq.sx
Normal file
@@ -0,0 +1,71 @@
|
||||
;; lib/minikanren/diseq.sx — Phase 5 polish: =/= disequality with a
|
||||
;; constraint store, generalising nafc / fd-neq to logic terms.
|
||||
;;
|
||||
;; The constraint store lives under the same `_fd` reserved key as the
|
||||
;; CLP(FD) propagators (a disequality is just another constraint
|
||||
;; closure that the existing fd-fire-store machinery re-runs).
|
||||
;;
|
||||
;; =/= semantics:
|
||||
;; - If u and v walk to ground non-unifiable terms, succeed (drop).
|
||||
;; - If they walk to terms that COULD become equal under a future
|
||||
;; binding, store the constraint; re-check after each binding.
|
||||
;; - If they're already equal (unify with no new bindings), fail.
|
||||
;;
|
||||
;; Implementation: each =/= test attempts (mk-unify wu wv s).
|
||||
;; nil — distinct, keep s, drop the constraint (return s).
|
||||
;; subst eq — equal, fail (return nil).
|
||||
;; subst > — partially unifiable; keep the constraint, return s.
|
||||
;;
|
||||
;; "Substitution equal to s" is detected via key-count: mk-unify only
|
||||
;; ever extends a substitution, never removes from it, so equal
|
||||
;; key-count means no new bindings were needed.
|
||||
|
||||
(define
|
||||
=/=-prop
|
||||
(fn
|
||||
(u v s)
|
||||
(let
|
||||
((s-after (mk-unify u v s)))
|
||||
(cond
|
||||
((= s-after nil) s)
|
||||
((= (len (keys s)) (len (keys s-after))) nil)
|
||||
(:else s)))))
|
||||
|
||||
(define
|
||||
=/=
|
||||
(fn
|
||||
(u v)
|
||||
(fn
|
||||
(s)
|
||||
(let
|
||||
((c (fn (sp) (=/=-prop u v sp))))
|
||||
(let
|
||||
((s2 (fd-add-constraint s c)))
|
||||
(let
|
||||
((s2-or-nil (c s2)))
|
||||
(let
|
||||
((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil)))))
|
||||
(cond ((= s3 nil) mzero) (:else (unit s3))))))))))
|
||||
|
||||
;; --- constraint-aware == ---
|
||||
;;
|
||||
;; Plain `==` doesn't fire the constraint store, so a binding that
|
||||
;; should violate a pending =/= goes undetected. `==-cs` is the
|
||||
;; drop-in replacement that fires fd-fire-store after each binding.
|
||||
;; Use ==-cs in any program that mixes =/= (or fd-* goals that should
|
||||
;; re-check after non-FD bindings) with regular unification.
|
||||
|
||||
(define
|
||||
==-cs
|
||||
(fn
|
||||
(u v)
|
||||
(fn
|
||||
(s)
|
||||
(let
|
||||
((s2 (mk-unify u v s)))
|
||||
(cond
|
||||
((= s2 nil) mzero)
|
||||
(:else
|
||||
(let
|
||||
((s3 (fd-fire-store s2)))
|
||||
(cond ((= s3 nil) mzero) (:else (unit s3))))))))))
|
||||
94
lib/minikanren/tabling-slg.sx
Normal file
94
lib/minikanren/tabling-slg.sx
Normal file
@@ -0,0 +1,94 @@
|
||||
;; lib/minikanren/tabling-slg.sx — Phase 7 piece A: SLG-style tabling.
|
||||
;;
|
||||
;; Naive memoization (table-1/2/3 in tabling.sx) drains the body's
|
||||
;; answer stream eagerly, then caches. Recursive tabled calls with the
|
||||
;; SAME ground key see an empty cache (the in-progress entry doesn't
|
||||
;; exist), so they recurse and the host overflows on cyclic relations.
|
||||
;;
|
||||
;; This module ships the in-progress-sentinel piece of SLG resolution:
|
||||
;; before evaluating the body, mark the cache entry as :in-progress;
|
||||
;; any recursive call to the same key sees the sentinel and returns
|
||||
;; mzero (no answers yet). Outer recursion thus terminates on cycles.
|
||||
;; Limitation: a single pass — answers found by cycle-dependent
|
||||
;; recursive calls are NOT discovered. Full SLG with fixed-point
|
||||
;; iteration (re-running until no new answers) is left for follow-up.
|
||||
|
||||
(define
|
||||
table-2-slg-iter
|
||||
(fn
|
||||
(rel-fn input output s key prev-vals)
|
||||
(begin
|
||||
(mk-tab-store! key prev-vals)
|
||||
(let
|
||||
((all-substs (stream-take -1 ((rel-fn input output) s))))
|
||||
(let
|
||||
((vals (map (fn (s2) (mk-walk* output s2)) all-substs)))
|
||||
(cond
|
||||
((= (len vals) (len prev-vals))
|
||||
(begin
|
||||
(mk-tab-store! key vals)
|
||||
(mk-tab-replay-vals vals output s)))
|
||||
(:else (table-2-slg-iter rel-fn input output s key vals))))))))
|
||||
|
||||
(define
|
||||
table-2-slg
|
||||
(fn
|
||||
(name rel-fn)
|
||||
(fn
|
||||
(input output)
|
||||
(fn
|
||||
(s)
|
||||
(let
|
||||
((winput (mk-walk* input s)))
|
||||
(cond
|
||||
((mk-tab-ground-term? winput)
|
||||
(let
|
||||
((key (str name "/slg/" winput)))
|
||||
(let
|
||||
((cached (mk-tab-lookup key)))
|
||||
(cond
|
||||
((not (= cached :miss))
|
||||
(mk-tab-replay-vals cached output s))
|
||||
(:else
|
||||
(table-2-slg-iter rel-fn input output s key (list)))))))
|
||||
(:else ((rel-fn input output) s))))))))
|
||||
|
||||
(define
|
||||
table-3-slg-iter
|
||||
(fn
|
||||
(rel-fn i1 i2 output s key prev-vals)
|
||||
(begin
|
||||
(mk-tab-store! key prev-vals)
|
||||
(let
|
||||
((all-substs (stream-take -1 ((rel-fn i1 i2 output) s))))
|
||||
(let
|
||||
((vals (map (fn (s2) (mk-walk* output s2)) all-substs)))
|
||||
(cond
|
||||
((= (len vals) (len prev-vals))
|
||||
(begin
|
||||
(mk-tab-store! key vals)
|
||||
(mk-tab-replay-vals vals output s)))
|
||||
(:else (table-3-slg-iter rel-fn i1 i2 output s key vals))))))))
|
||||
|
||||
(define
|
||||
table-3-slg
|
||||
(fn
|
||||
(name rel-fn)
|
||||
(fn
|
||||
(i1 i2 output)
|
||||
(fn
|
||||
(s)
|
||||
(let
|
||||
((wi1 (mk-walk* i1 s)) (wi2 (mk-walk* i2 s)))
|
||||
(cond
|
||||
((and (mk-tab-ground-term? wi1) (mk-tab-ground-term? wi2))
|
||||
(let
|
||||
((key (str name "/slg3/" wi1 "/" wi2)))
|
||||
(let
|
||||
((cached (mk-tab-lookup key)))
|
||||
(cond
|
||||
((not (= cached :miss))
|
||||
(mk-tab-replay-vals cached output s))
|
||||
(:else
|
||||
(table-3-slg-iter rel-fn i1 i2 output s key (list)))))))
|
||||
(:else ((rel-fn i1 i2 output) s))))))))
|
||||
316
lib/minikanren/tests/clpfd-bounds.sx
Normal file
316
lib/minikanren/tests/clpfd-bounds.sx
Normal file
@@ -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!)
|
||||
83
lib/minikanren/tests/diseq.sx
Normal file
83
lib/minikanren/tests/diseq.sx
Normal file
@@ -0,0 +1,83 @@
|
||||
;; lib/minikanren/tests/diseq.sx — Phase 5 polish: =/= disequality.
|
||||
|
||||
;; --- ground cases ---
|
||||
|
||||
(mk-test
|
||||
"=/=-ground-distinct"
|
||||
(run* q (=/= 1 2))
|
||||
(list (make-symbol "_.0")))
|
||||
(mk-test "=/=-ground-equal" (run* q (=/= 1 1)) (list))
|
||||
(mk-test
|
||||
"=/=-ground-strings"
|
||||
(run* q (=/= "a" "b"))
|
||||
(list (make-symbol "_.0")))
|
||||
(mk-test "=/=-ground-strings-eq" (run* q (=/= "a" "a")) (list))
|
||||
|
||||
;; --- structural ---
|
||||
|
||||
(mk-test
|
||||
"=/=-pair-distinct"
|
||||
(run* q (=/= (list 1 2) (list 1 3)))
|
||||
(list (make-symbol "_.0")))
|
||||
(mk-test
|
||||
"=/=-pair-equal"
|
||||
(run* q (=/= (list 1 2) (list 1 2)))
|
||||
(list))
|
||||
(mk-test
|
||||
"=/=-pair-vs-atom"
|
||||
(run* q (=/= (list 1) 1))
|
||||
(list (make-symbol "_.0")))
|
||||
|
||||
;; --- partial / late binding ---
|
||||
;;
|
||||
;; ==-cs is required to wake up the constraint store after a binding;
|
||||
;; plain == doesn't fire constraints.
|
||||
|
||||
(mk-test
|
||||
"=/=-late-bind-violates"
|
||||
(run* q (fresh (x) (=/= x 5) (==-cs x 5) (== q x)))
|
||||
(list))
|
||||
|
||||
(mk-test
|
||||
"=/=-late-bind-ok"
|
||||
(run* q (fresh (x) (=/= x 5) (==-cs x 7) (== q x)))
|
||||
(list 7))
|
||||
|
||||
(mk-test
|
||||
"=/=-two-vars-equal-late-fails"
|
||||
(run*
|
||||
q
|
||||
(fresh
|
||||
(x y)
|
||||
(=/= x y)
|
||||
(==-cs x 1)
|
||||
(==-cs y 1)
|
||||
(== q (list x y))))
|
||||
(list))
|
||||
|
||||
(mk-test
|
||||
"=/=-two-vars-distinct-late"
|
||||
(run*
|
||||
q
|
||||
(fresh
|
||||
(x y)
|
||||
(=/= x y)
|
||||
(==-cs x 1)
|
||||
(==-cs y 2)
|
||||
(== q (list x y))))
|
||||
(list (list 1 2)))
|
||||
|
||||
;; --- compose with conde / fresh ---
|
||||
|
||||
(mk-test
|
||||
"=/=-with-membero-filter"
|
||||
(run*
|
||||
q
|
||||
(fresh
|
||||
(x)
|
||||
(membero x (list 1 2 3))
|
||||
(=/= x 2)
|
||||
(== q x)))
|
||||
(list 1 3))
|
||||
|
||||
(mk-tests-run!)
|
||||
97
lib/minikanren/tests/send-more-money.sx
Normal file
97
lib/minikanren/tests/send-more-money.sx
Normal file
@@ -0,0 +1,97 @@
|
||||
;; lib/minikanren/tests/send-more-money.sx — classic cryptarithmetic
|
||||
;;
|
||||
;; S E N D
|
||||
;; + M O R E
|
||||
;; ---------
|
||||
;; M O N E Y
|
||||
;;
|
||||
;; Column-by-column encoding with carries c1, c2, c3, and the
|
||||
;; leftmost column produces a carry which equals M (the result is 5 digits).
|
||||
;; All 8 letters distinct; S ≠ 0, M ≠ 0.
|
||||
;; Unique solution: S=9, E=5, N=6, D=7, M=1, O=0, R=8, Y=2.
|
||||
;;
|
||||
;; Note: the full search labelling 11 variables from {0..9} is too slow
|
||||
;; for naive labelling order (10^11 combinations naively, even with
|
||||
;; bounds-consistency the branching factor dominates). Real CLP(FD)
|
||||
;; systems use first-fail heuristics. Here we only verify the encoding
|
||||
;; against the known answer.
|
||||
|
||||
(define
|
||||
digits-0-9
|
||||
(list
|
||||
0
|
||||
1
|
||||
2
|
||||
3
|
||||
4
|
||||
5
|
||||
6
|
||||
7
|
||||
8
|
||||
9))
|
||||
(define
|
||||
digits-1-9
|
||||
(list
|
||||
1
|
||||
2
|
||||
3
|
||||
4
|
||||
5
|
||||
6
|
||||
7
|
||||
8
|
||||
9))
|
||||
|
||||
(define
|
||||
smm-col-with-carry
|
||||
(fn
|
||||
(x y carry-in z carry-out)
|
||||
(fresh
|
||||
(xy xyc ten-cout z-plus-ten-cout)
|
||||
(fd-plus x y xy)
|
||||
(fd-plus xy carry-in xyc)
|
||||
(fd-times 10 carry-out ten-cout)
|
||||
(fd-plus z ten-cout z-plus-ten-cout)
|
||||
(fd-eq xyc z-plus-ten-cout))))
|
||||
|
||||
(define
|
||||
send-more-money
|
||||
(fn
|
||||
(S E N D M O R Y)
|
||||
(fresh
|
||||
(c1 c2 c3)
|
||||
(mk-conj
|
||||
(fd-in S digits-1-9)
|
||||
(fd-in M digits-1-9)
|
||||
(fd-in E digits-0-9)
|
||||
(fd-in N digits-0-9)
|
||||
(fd-in D digits-0-9)
|
||||
(fd-in O digits-0-9)
|
||||
(fd-in R digits-0-9)
|
||||
(fd-in Y digits-0-9)
|
||||
(fd-in c1 (list 0 1))
|
||||
(fd-in c2 (list 0 1))
|
||||
(fd-in c3 (list 0 1))
|
||||
(fd-distinct (list S E N D M O R Y))
|
||||
(smm-col-with-carry D E 0 Y c1)
|
||||
(smm-col-with-carry N R c1 E c2)
|
||||
(smm-col-with-carry E O c2 N c3)
|
||||
(smm-col-with-carry S M c3 O M)
|
||||
(fd-label (list S E N D M O R Y c1 c2 c3))))))
|
||||
|
||||
(mk-test
|
||||
"send-more-money-verify-known-solution"
|
||||
(run*
|
||||
q
|
||||
(send-more-money
|
||||
9
|
||||
5
|
||||
6
|
||||
7
|
||||
1
|
||||
0
|
||||
8
|
||||
2))
|
||||
(list (make-symbol "_.0")))
|
||||
|
||||
(mk-tests-run!)
|
||||
89
lib/minikanren/tests/sudoku-4x4.sx
Normal file
89
lib/minikanren/tests/sudoku-4x4.sx
Normal file
@@ -0,0 +1,89 @@
|
||||
;; lib/minikanren/tests/sudoku-4x4.sx — Sudoku 4×4 via CLP(FD).
|
||||
;;
|
||||
;; Grid in row-major order:
|
||||
;;
|
||||
;; c0 c1 | c2 c3
|
||||
;; c4 c5 | c6 c7
|
||||
;; ------+------
|
||||
;; c8 c9 | cA cB
|
||||
;; cC cD | cE cF
|
||||
;;
|
||||
;; Each cell ∈ {1, 2, 3, 4}. 4 rows + 4 cols + 4 2x2 boxes are each a
|
||||
;; distinct permutation.
|
||||
|
||||
(define digits-1-4 (list 1 2 3 4))
|
||||
|
||||
(define
|
||||
sudoku-4x4
|
||||
(fn
|
||||
(cells)
|
||||
(let
|
||||
((c0 (nth cells 0))
|
||||
(c1 (nth cells 1))
|
||||
(c2 (nth cells 2))
|
||||
(c3 (nth cells 3))
|
||||
(c4 (nth cells 4))
|
||||
(c5 (nth cells 5))
|
||||
(c6 (nth cells 6))
|
||||
(c7 (nth cells 7))
|
||||
(c8 (nth cells 8))
|
||||
(c9 (nth cells 9))
|
||||
(cA (nth cells 10))
|
||||
(cB (nth cells 11))
|
||||
(cC (nth cells 12))
|
||||
(cD (nth cells 13))
|
||||
(cE (nth cells 14))
|
||||
(cF (nth cells 15)))
|
||||
(mk-conj
|
||||
(fd-in c0 digits-1-4)
|
||||
(fd-in c1 digits-1-4)
|
||||
(fd-in c2 digits-1-4)
|
||||
(fd-in c3 digits-1-4)
|
||||
(fd-in c4 digits-1-4)
|
||||
(fd-in c5 digits-1-4)
|
||||
(fd-in c6 digits-1-4)
|
||||
(fd-in c7 digits-1-4)
|
||||
(fd-in c8 digits-1-4)
|
||||
(fd-in c9 digits-1-4)
|
||||
(fd-in cA digits-1-4)
|
||||
(fd-in cB digits-1-4)
|
||||
(fd-in cC digits-1-4)
|
||||
(fd-in cD digits-1-4)
|
||||
(fd-in cE digits-1-4)
|
||||
(fd-in cF digits-1-4)
|
||||
(fd-distinct (list c0 c1 c2 c3))
|
||||
(fd-distinct (list c4 c5 c6 c7))
|
||||
(fd-distinct (list c8 c9 cA cB))
|
||||
(fd-distinct (list cC cD cE cF))
|
||||
(fd-distinct (list c0 c4 c8 cC))
|
||||
(fd-distinct (list c1 c5 c9 cD))
|
||||
(fd-distinct (list c2 c6 cA cE))
|
||||
(fd-distinct (list c3 c7 cB cF))
|
||||
(fd-distinct (list c0 c1 c4 c5))
|
||||
(fd-distinct (list c2 c3 c6 c7))
|
||||
(fd-distinct (list c8 c9 cC cD))
|
||||
(fd-distinct (list cA cB cE cF))
|
||||
(fd-label cells)))))
|
||||
|
||||
;; --- Tests ---
|
||||
|
||||
(mk-test
|
||||
"sudoku-4x4-empty-grid-count"
|
||||
(let
|
||||
((sols (run* q (fresh (c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 cA cB cC cD cE cF) (== q (list c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 cA cB cC cD cE cF)) (sudoku-4x4 (list c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 cA cB cC cD cE cF))))))
|
||||
(len sols))
|
||||
288)
|
||||
|
||||
(mk-test
|
||||
"sudoku-4x4-impossible-clue-empty"
|
||||
(run*
|
||||
q
|
||||
(fresh
|
||||
(c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 cA cB cC cD cE cF)
|
||||
(== c0 1)
|
||||
(== c1 1)
|
||||
(== q (list c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 cA cB cC cD cE cF))
|
||||
(sudoku-4x4 (list c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 cA cB cC cD cE cF))))
|
||||
(list))
|
||||
|
||||
(mk-tests-run!)
|
||||
56
lib/minikanren/tests/tabling-slg.sx
Normal file
56
lib/minikanren/tests/tabling-slg.sx
Normal file
@@ -0,0 +1,56 @@
|
||||
;; lib/minikanren/tests/tabling-slg.sx — Phase 7 piece A: SLG-style tabling.
|
||||
|
||||
;; --- table-2-slg with Fibonacci (sanity: same answer as naive table-2) ---
|
||||
|
||||
(mk-tab-clear!)
|
||||
(define
|
||||
slg-fib-o
|
||||
(table-2-slg
|
||||
"slg-fib"
|
||||
(fn
|
||||
(n result)
|
||||
(conde
|
||||
((== n 0) (== result 0))
|
||||
((== n 1) (== result 1))
|
||||
((fresh (n-1 n-2 r-1 r-2) (lto-i 1 n) (minuso-i n 1 n-1) (minuso-i n 2 n-2) (slg-fib-o n-1 r-1) (slg-fib-o n-2 r-2) (pluso-i r-1 r-2 result)))))))
|
||||
|
||||
(mk-tab-clear!)
|
||||
(mk-test "slg-fib-five" (run* q (slg-fib-o 5 q)) (list 5))
|
||||
(mk-tab-clear!)
|
||||
(mk-test "slg-fib-ten" (run* q (slg-fib-o 10 q)) (list 55))
|
||||
|
||||
;; --- table-3-slg with cyclic-graph patho ---
|
||||
|
||||
(define slg-cyc-edges (list (list :a :b) (list :b :a) (list :b :c)))
|
||||
(define slg-cyc-edgeo (fn (x y) (membero (list x y) slg-cyc-edges)))
|
||||
|
||||
(mk-tab-clear!)
|
||||
(define
|
||||
tab-patho
|
||||
(table-3-slg
|
||||
"patho"
|
||||
(fn
|
||||
(x y path)
|
||||
(conde
|
||||
((slg-cyc-edgeo x y) (== path (list x y)))
|
||||
((fresh (z mid) (slg-cyc-edgeo x z) (tab-patho z y mid) (conso x mid path)))))))
|
||||
|
||||
(mk-tab-clear!)
|
||||
(mk-test
|
||||
"slg-cyclic-direct"
|
||||
(run* q (tab-patho :a :b q))
|
||||
(list (list :a :b)))
|
||||
|
||||
(mk-tab-clear!)
|
||||
(mk-test
|
||||
"slg-cyclic-multi-hop"
|
||||
(run* q (tab-patho :a :c q))
|
||||
(list (list :a :b :c)))
|
||||
|
||||
(mk-tab-clear!)
|
||||
(mk-test
|
||||
"slg-cyclic-self-loop-finite"
|
||||
(run* q (tab-patho :a :a q))
|
||||
(list (list :a :b :a)))
|
||||
|
||||
(mk-tests-run!)
|
||||
@@ -205,6 +205,23 @@ _(none yet)_
|
||||
|
||||
_Newest first._
|
||||
|
||||
- **2026-05-09** — **deferred-plan execution**: shipped all four pieces from
|
||||
`plans/minikanren-deferred.md` (on architecture):
|
||||
- **Piece B** — bounds-consistency for `fd-plus` / `fd-times` (vvn / nvv /
|
||||
vnv / vvv branches; integer-division helpers for ceil/floor);
|
||||
- **Piece D** — send-more-money (column-with-carry encoding, verified
|
||||
against the known answer) and Sudoku 4×4 (288 fillings of empty grid;
|
||||
immediate failure on contradictory clues);
|
||||
- **Piece C** — `=/=` disequality with constraint store, plus `==-cs`
|
||||
constraint-aware unify so the store re-fires on bindings;
|
||||
- **Piece A** — SLG-style tabling: in-progress sentinel + fixed-point
|
||||
iteration. Cyclic patho terminates: `(tab-patho :a :c q)` on a graph
|
||||
with cycle `a↔b` plus `b→c` returns `((:a :b :c))`. Naive tabling
|
||||
diverged on the same query. Mutually-recursive coordination across
|
||||
independent tabled relations is left for follow-up (proper SLG
|
||||
worklist).
|
||||
170/170 across the new+FD-related test files.
|
||||
|
||||
- **2026-05-08** — **Session snapshot**: 17 lib files, 61 test files, 1229
|
||||
library LOC + 4360 test LOC, **551/551 tests cumulative**. Library covers
|
||||
Phases 1–5 fully, Phase 6 partial (FD helpers + intarith escape), Phase 7
|
||||
|
||||
Reference in New Issue
Block a user