Single-rule evaluation using k-position semi-naive delta computation.
For a rule with k positive body atoms, each fixpoint iteration evaluates k variants. Variant i places the delta at body position i, uses full (existing + delta) for positions before i, and uses old (pre-iteration snapshot) for positions after i. This guarantees every derivation that involves at least one delta fact is counted exactly once, avoiding duplicates.
Negation handling
Negative body atoms ({:negative, %IR.Atom{}}) are filters, not
participants in the k-position delta scheme. After all positive atoms are
joined and constraints applied, each binding is checked against the negative
atoms: a binding survives only if no tuple in the full relation matches
the negative atom's terms under that binding. This ensures negation is
evaluated against the fully-materialised lower-stratum relation, which is
correct for stratified Datalog.
Four views per relation
The evaluator receives four logical "views" of each relation per iteration:
full— all facts currently known (existing + delta from previous iter).old— snapshot of the relation at the start of the current iteration.delta— facts newly derived in the previous iteration.
For the initial iteration (i=0), delta is the EDB (base facts) and old
is empty.
Constraint handling
After all body atoms are joined, constraints are applied sequentially. Comparisons filter bindings; arithmetic constraints extend bindings with their result variable. This matches the validator's sequential constraint ordering guarantee.
Summary
Functions
Checks whether a binding satisfies a negative body atom.
Evaluates a single rule for one fixpoint iteration using k-position delta.
Types
@type binding() :: ExDatalog.Engine.Binding.t()
Functions
@spec check_negative_atom(ExDatalog.IR.Atom.t(), binding(), relation_facts()) :: boolean()
Checks whether a binding satisfies a negative body atom.
A negative atom not R(t1, ..., tn) is satisfied when no tuple in full
for relation R matches the atom's terms under the given binding. If the
atom's terms contain variables already bound, only tuples consistent with
those bindings are considered. If the atom's terms contain only wildcards,
any tuple in the relation causes the negative atom to fail.
Returns true if the binding passes (no matching tuple), false otherwise.
@spec eval_rule_iteration( ExDatalog.IR.Rule.t(), relation_facts(), relation_facts(), relation_facts(), ExDatalog.Constraint.Context.t() ) :: [tuple()]
Evaluates a single rule for one fixpoint iteration using k-position delta.
Returns a list of head tuples derived by this rule in this iteration. Each tuple is an Elixir tuple of native values.
Parameters:
rule— the IR rule to evaluate.full— map from relation name to the full fact set.delta— map from relation name to delta facts (newly derived).old— map from relation name to old facts (pre-iteration snapshot).
For variant i (0 ≤ i < k, where k is the number of positive body atoms):
- Position i uses
delta(relation_i) - Positions j < i use
full(relation_j) - Positions j > i use
old(relation_j)
Negative atoms are applied as filters after the join, checking that no tuple
in the full relation matches under the current binding.
The results of all variants are unioned, then deduplicated against full
for the head relation.