# `ExDatalog.Validator.Stratification`
[🔗](https://github.com/thanos/ex_datalog/blob/v0.5.0/lib/ex_datalog/validator/stratification.ex#L1)

Stratification checks for ExDatalog programs.

A Datalog program with negation must be **stratifiable** — there must be
no cycle in the dependency graph that contains a negative edge. If such a
cycle exists, evaluation order is ambiguous and the program is rejected.

This module:

1. Builds a **dependency graph** from the program's rules.
2. Computes **strongly connected components** (SCCs) using Tarjan's algorithm.
3. Checks that **no SCC contains a negative edge**.
4. Assigns a **stratum** to each relation.

# `edge`

```elixir
@type edge() :: {String.t(), :positive | :negative}
```

# `graph`

```elixir
@type graph() :: %{required(String.t()) =&gt; [edge()]}
```

# `scc`

```elixir
@type scc() :: [String.t()]
```

# `assign_strata`

```elixir
@spec assign_strata(ExDatalog.Program.t()) :: %{
  required(String.t()) =&gt; non_neg_integer()
}
```

Assigns strata to all relations in the program.

Returns a map from relation name to stratum number (0-based).
Every declared relation is included — relations that appear only in
facts (not in any rule) are assigned stratum 0. Only valid for
programs that pass `check/1`.

# `check`

```elixir
@spec check(ExDatalog.Program.t()) :: :ok | {:error, [ExDatalog.Validator.Error.t()]}
```

Checks whether the program has unstratifiable negation.

Returns `:ok` if all SCCs are stratifiable, or `{:error, errors}` listing
every SCC that contains a negative edge.

---

*Consult [api-reference.md](api-reference.md) for complete listing*
