diff --git a/lib/datalog/eval.sx b/lib/datalog/eval.sx index 32db2f7f..e0fc1554 100644 --- a/lib/datalog/eval.sx +++ b/lib/datalog/eval.sx @@ -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 diff --git a/lib/datalog/scoreboard.json b/lib/datalog/scoreboard.json index 1a302808..95bc068c 100644 --- a/lib/datalog/scoreboard.json +++ b/lib/datalog/scoreboard.json @@ -1,13 +1,13 @@ { "lang": "datalog", - "total_passed": 209, + "total_passed": 212, "total_failed": 0, - "total": 209, + "total": 212, "suites": [ {"name":"tokenize","passed":26,"failed":0,"total":26}, {"name":"parse","passed":18,"failed":0,"total":18}, {"name":"unify","passed":28,"failed":0,"total":28}, - {"name":"eval","passed":25,"failed":0,"total":25}, + {"name":"eval","passed":28,"failed":0,"total":28}, {"name":"builtins","passed":19,"failed":0,"total":19}, {"name":"semi_naive","passed":8,"failed":0,"total":8}, {"name":"negation","passed":10,"failed":0,"total":10}, @@ -16,5 +16,5 @@ {"name":"magic","passed":22,"failed":0,"total":22}, {"name":"demo","passed":18,"failed":0,"total":18} ], - "generated": "2026-05-08T10:13:00+00:00" + "generated": "2026-05-08T10:15:09+00:00" } diff --git a/lib/datalog/scoreboard.md b/lib/datalog/scoreboard.md index 1e78dc45..4cb73b51 100644 --- a/lib/datalog/scoreboard.md +++ b/lib/datalog/scoreboard.md @@ -1,13 +1,13 @@ # datalog scoreboard -**209 / 209 passing** (0 failure(s)). +**212 / 212 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| | tokenize | 26 | 26 | ok | | parse | 18 | 18 | ok | | unify | 28 | 28 | ok | -| eval | 25 | 25 | ok | +| eval | 28 | 28 | ok | | builtins | 19 | 19 | ok | | semi_naive | 8 | 8 | ok | | negation | 10 | 10 | ok | diff --git a/lib/datalog/tests/eval.sx b/lib/datalog/tests/eval.sx index 8030f3f1..9c688f86 100644 --- a/lib/datalog/tests/eval.sx +++ b/lib/datalog/tests/eval.sx @@ -258,6 +258,31 @@ (do (dl-set-strategy! db :magic) (dl-get-strategy db))) :magic) + ;; dl-saturated?: no-work-left predicate. + (dl-et-test! "saturated? after saturation" + (let ((db (dl-program + "parent(a, b). + ancestor(X, Y) :- parent(X, Y)."))) + (do (dl-saturate! db) (dl-saturated? db))) + true) + + (dl-et-test! "saturated? before saturation" + (let ((db (dl-program + "parent(a, b). + ancestor(X, Y) :- parent(X, Y)."))) + (dl-saturated? db)) + false) + + (dl-et-test! "saturated? after assert" + (let ((db (dl-program + "parent(a, b). + ancestor(X, Y) :- parent(X, Y)."))) + (do + (dl-saturate! db) + (dl-add-fact! db (list (quote parent) (quote b) (quote c))) + (dl-saturated? db))) + false) + (dl-et-test-set! "magic-set still derives correctly" (let ((db (dl-program