datalog: dl-magic-query pre-saturates for aggregate correctness
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 13s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 13s
dl-magic-query could silently diverge from dl-query when an
aggregate's inner-goal relation was IDB. The rewriter passes
aggregate body lits through unchanged (no magic propagation
generated for them), so the inner relation was empty in the magic
db and the aggregate returned 0. Repro:
(dl-eval-magic
"u(a). u(b). u(c). u(d). banned(b). banned(d).
active(X) :- u(X), not(banned(X)).
n(N) :- count(N, X, active(X))."
"?- n(N).")
=> ({:N 0}) ; should be ({:N 2})
dl-magic-query now pre-saturates the source db before copying facts
into the magic db. This guarantees equivalence with dl-query for
every stratified program; the magic benefit still comes from
goal-directed re-derivation of the query relation under the seed
(which matters for large recursive joins). The existing test cases
happened to dodge this because their aggregate inner-goals were all
EDB.
1 new regression test; conformance 274/274.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This commit is contained in:
@@ -15,7 +15,7 @@ for rose-ash data (e.g. federation graph, content relationships).
|
||||
|
||||
## Status (rolling)
|
||||
|
||||
`bash lib/datalog/conformance.sh` → **273/273 across 11 suites**
|
||||
`bash lib/datalog/conformance.sh` → **274/274 across 11 suites**
|
||||
(tokenize, parse, unify, eval, builtins, semi_naive, negation, aggregates,
|
||||
api, magic, demo). Source is ~3100 LOC, tests ~2900 LOC, public API
|
||||
documented in `lib/datalog/datalog.sx`.
|
||||
@@ -320,6 +320,23 @@ large graphs.
|
||||
|
||||
_Newest first._
|
||||
|
||||
- 2026-05-11 — `dl-magic-query` could silently diverge from
|
||||
`dl-query` when an aggregate's inner-goal relation was IDB. The
|
||||
rewriter passes aggregate body lits through unchanged (no magic
|
||||
propagation for them), so the inner relation was empty in the
|
||||
magic db and the aggregate returned 0. Probe:
|
||||
`dl-eval-magic "u(a). u(b). u(c). u(d). banned(b). banned(d).
|
||||
active(X) :- u(X), not(banned(X)).
|
||||
n(N) :- count(N, X, active(X))." "?- n(N)."`
|
||||
returned `N=0` instead of `N=2`. Fix: `dl-magic-query` now
|
||||
pre-saturates the source db before copying facts into the magic
|
||||
db. This guarantees equivalence with `dl-query` for every
|
||||
stratified program; the magic benefit comes from goal-directed
|
||||
re-derivation of the query relation under the seed (which still
|
||||
matters for large recursive joins). The existing test suite's
|
||||
aggregate cases happened to dodge this because the inner goals
|
||||
were all EDB. 1 new regression test; 274/274.
|
||||
|
||||
- 2026-05-11 — Anonymous `_` in a negated literal was incorrectly
|
||||
flagged by the safety check. The canonical idiom
|
||||
`orphan(X) :- person(X), not(parent(X, _))` was rejected with
|
||||
|
||||
Reference in New Issue
Block a user