diff --git a/lib/datalog/magic.sx b/lib/datalog/magic.sx index 43ab7404..448042e9 100644 --- a/lib/datalog/magic.sx +++ b/lib/datalog/magic.sx @@ -373,6 +373,35 @@ rules) seen)))) +;; True iff any rule's body contains a literal kind that the magic +;; rewriter doesn't propagate magic to — i.e. an aggregate or a +;; negation. Used by dl-magic-query to decide whether to pre-saturate +;; the source db (for correctness on stratified programs) or skip +;; that step (preserving full magic-sets efficiency for pure +;; positive programs). +(define + dl-rule-has-nonprop-lit? + (fn + (body i n) + (cond + ((>= i n) false) + ((let ((lit (nth body i))) + (or (and (dict? lit) (has-key? lit :neg)) + (dl-aggregate? lit))) + true) + (else (dl-rule-has-nonprop-lit? body (+ i 1) n))))) + +(define + dl-rules-need-presaturation? + (fn + (rules) + (cond + ((= (len rules) 0) false) + ((let ((body (get (first rules) :body))) + (dl-rule-has-nonprop-lit? body 0 (len body))) + true) + (else (dl-rules-need-presaturation? (rest rules)))))) + (define dl-magic-query (fn @@ -393,17 +422,18 @@ (dl-query db query-goal)) (else (do - ;; Pre-saturate the source db. The magic rewriter passes - ;; aggregate body lits through unchanged (no magic - ;; propagation generated for them) — so if an aggregate's - ;; inner-goal relation is IDB, it would be empty in the - ;; magic db unless its tuples are already materialised in - ;; the source. Same for negation against IDB. Pre-saturating - ;; guarantees `dl-magic-query` returns the same answers as - ;; `dl-query` for every stratified program; the efficiency - ;; benefit then comes from goal-directed re-derivation of - ;; the query relation under the magic seed. - (dl-saturate! db) + ;; If the rule set has aggregates or negation, pre-saturate + ;; the source db before copying facts. The magic rewriter + ;; passes aggregate body lits and negated lits through + ;; unchanged (no magic propagation generated for them) — so + ;; if their inner-goal relation is IDB, it would be empty in + ;; the magic db. Pre-saturating ensures equivalence with + ;; `dl-query` for every stratified program. Pure positive + ;; programs skip this and keep the full magic-sets perf win + ;; from goal-directed re-derivation. + (when + (dl-rules-need-presaturation? (dl-rules db)) + (dl-saturate! db)) (let ((query-rel (dl-rel-name query-goal)) (query-adn (dl-adorn-goal query-goal)))