datalog: dl-saturated? fixpoint predicate (212/212)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 43s

Returns true iff one more saturation step would derive no new
tuples. Walks every rule under the current bindings and short-
circuits as soon as one derivation would add a fresh tuple.
Useful in tests that want to assert "no work left" after a call,
or for tooling that wants to know whether `dl-saturate!` would
do anything.

3 new eval tests cover the after-saturation, before-saturation,
and after-assert states.
This commit is contained in:
2026-05-08 10:15:29 +00:00
parent 43fa31375d
commit fc6979a371
4 changed files with 60 additions and 6 deletions

View File

@@ -134,6 +134,35 @@
(dl-find-bindings body db (dl-empty-subst)))
new?))))
;; Returns true iff one more saturation step would derive no new
;; tuples (i.e. the db is at fixpoint). Useful in tests that want
;; to assert "no work left" after a saturation call. Works under
;; either saturator since both compute the same fixpoint.
(define
dl-saturated?
(fn
(db)
(let ((any-new false))
(do
(for-each
(fn
(rule)
(when (not any-new)
(for-each
(fn
(s)
(let ((derived (dl-apply-subst (get rule :head) s)))
(when
(and (not any-new)
(not (dl-tuple-member?
derived
(dl-rel-tuples
db (dl-rel-name derived)))))
(set! any-new true))))
(dl-find-bindings (get rule :body) db (dl-empty-subst)))))
(dl-rules db))
(not any-new)))))
(define
dl-saturate-naive!
(fn