datalog: indexed dl-find-bindings + chain-15 differential (Phase 5c, 153/153)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 59s

dl-find-bindings now uses dl-fb-aux lits db subst i n (indexed
iteration via nth) instead of recursive (rest lits). Eliminates
O(N²) list-copy per body of length N. chain-15 saturation 25s
→ 16s; chain-25 finishes in 33s real (vs. timeout previously).

Bumped semi_naive tests to chain-10 differential + chain-15
semi-only count (was chain-5/chain-5). Blocker entry refreshed.
This commit is contained in:
2026-05-08 08:50:24 +00:00
parent de302fc236
commit 790c17dfc1
4 changed files with 32 additions and 20 deletions

View File

@@ -83,14 +83,18 @@
(define
dl-find-bindings
(fn (lits db subst) (dl-fb-aux lits db subst 0 (len lits))))
(define
dl-fb-aux
(fn
(lits db subst)
(lits db subst i n)
(cond
((nil? subst) (list))
((= (len lits) 0) (list subst))
((>= i n) (list subst))
(else
(let
((options (dl-match-lit (first lits) db subst))
((options (dl-match-lit (nth lits i) db subst))
(results (list)))
(do
(for-each
@@ -98,7 +102,7 @@
(s)
(for-each
(fn (s2) (append! results s2))
(dl-find-bindings (rest lits) db s)))
(dl-fb-aux lits db s (+ i 1) n)))
options)
results))))))