datalog: magic pre-saturation is conditional, not unconditional

Previously dl-magic-query always pre-saturated the source db so it
gave correct results for stratified programs (where the rewriter
doesn't propagate magic to aggregate inner-goals or negated rels).
Pure positive programs paid the full bottom-up cost twice.

Add dl-rules-need-presaturation? — checks whether any rule body
contains an aggregate or negation. Only pre-saturate in that case.
Pure positive programs (the common case for magic-sets) keep their
full goal-directed efficiency.

276/276; identical answers on the existing aggregate-of-IDB test.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

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
+          ;; If the rule set has aggregates or negation, pre-saturate
-          ;; aggregate body lits through unchanged (no magic
+          ;; the source db before copying facts. The magic rewriter
-          ;; propagation generated for them) — so if an aggregate's
+          ;; passes aggregate body lits and negated lits through
-          ;; inner-goal relation is IDB, it would be empty in the
+          ;; unchanged (no magic propagation generated for them) — so
-          ;; magic db unless its tuples are already materialised in
+          ;; if their inner-goal relation is IDB, it would be empty in
-          ;; the source. Same for negation against IDB. Pre-saturating
+          ;; the magic db. Pre-saturating ensures equivalence with
-          ;; guarantees `dl-magic-query` returns the same answers as
+          ;; `dl-query` for every stratified program. Pure positive
-          ;; `dl-query` for every stratified program; the efficiency
+          ;; programs skip this and keep the full magic-sets perf win
-          ;; benefit then comes from goal-directed re-derivation of
+          ;; from goal-directed re-derivation.
-          ;; the query relation under the magic seed.
+          (when
-          (dl-saturate! db)
+            (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)))