ExDatalog.Engine.Naive (ExDatalog v0.2.0)

Copy Markdown View Source

Semi-naive fixpoint evaluation engine.

Evaluates a compiled IR program stratum by stratum. Within each stratum, it iterates until no new facts are derived (fixpoint), using the k-position delta algorithm to avoid redundant derivations.

Negation

Rules with negative body atoms must be stratified: every relation that appears under negation must belong to a strictly lower stratum than the rule's head relation. The engine validates this invariant before evaluation and returns {:error, reason} for unstratifiable programs.

Negative atoms are evaluated against the fully-materialised full relation snapshot, ensuring correctness under stratified evaluation.

Provenance

When the :explain option is true, the result's provenance field records which rule derived each fact. Base facts (EDB) are attributed as :base. When :explain is false (default), provenance tracking is disabled entirely, ensuring zero overhead.

Algorithm

For each stratum:

  1. Load EDB base facts into storage.
  2. full ← snapshot of all current facts.
  3. delta ← full (all EDB facts are "new" on the first iteration).
  4. old ← empty (nothing existed "before" iteration 0).
  5. Loop: a. Evaluate all stratum rules using k-position delta with (full, delta, old). b. Collect newly derived tuples; remove those already in full. c. If no new tuples: fixpoint reached, stop. d. Insert new tuples into storage. e. old ← full (snapshot before this iteration). f. full ← new snapshot. g. delta ← full old (per-relation difference).

Options

  • :storage — storage module (default: ExDatalog.Storage.Map)
  • :storage_opts — keyword list passed to storage.init/2 (default: [])
  • :max_iterations — per-stratum iteration limit (default: 10_000)
  • :timeout_ms — per-stratum wall-clock timeout in ms (default: 30_000)
  • :explain — enable provenance tracking (default: false)

Summary

Functions

evaluate(ir, opts \\ [])

Evaluates a compiled IR program to fixpoint.

name()

Returns the engine's stable identifier, "naive".

Functions

evaluate(ir, opts \\ [])

@spec evaluate(
  ExDatalog.IR.t(),
  keyword()
) :: {:ok, ExDatalog.Result.t()} | {:error, term()}

Evaluates a compiled IR program to fixpoint.

Accepts a compiled IR.t() struct (from Compiler.compile/1) and an optional keyword list of options. Returns {:ok, %Result{}} on success or {:error, reason} on failure.

Options

  • :storage — storage module (default: ExDatalog.Storage.Map)
  • :storage_opts — keyword list passed to storage.init/2 (default: [])
  • :max_iterations — per-stratum iteration limit (default: 10_000)
  • :timeout_ms — per-stratum wall-clock timeout in ms (default: 30_000)
  • :explain — enable provenance tracking (default: false)

See ExDatalog.Engine.Naive moduledoc for algorithm details.

name()

@spec name() :: String.t()

Returns the engine's stable identifier, "naive".

Used for telemetry metadata and engine dispatch.