datalog_structural_model/stratify/
types.rs

1//! Public stratification result types and error.
2
3use std::collections::{BTreeMap, BTreeSet};
4
5use crate::ir::{Atom, ConstantSymbol, PredicateSymbol, Term};
6
7/// Stratification of a Datalog¬ program.
8#[derive(Clone, Debug, Eq, PartialEq, serde::Serialize, serde::Deserialize)]
9#[serde(deny_unknown_fields)]
10pub struct Stratification {
11    /// Strata ordered by ascending index. Stratum `k` must be
12    /// evaluated to a fixed point before stratum `k+1`.
13    pub strata: Vec<Stratum>,
14    /// Map from predicate to its stratum index. context-aware rolls up
15    /// the underlying `(predicate, head-graph-class)` dependency
16    /// nodes by taking the **maximum** stratum across head-graph
17    /// classes of the same predicate — so a producer that emits
18    /// facts in more than one graph class is scheduled late
19    /// enough for every downstream consumer.
20    pub predicate_stratum: BTreeMap<PredicateSymbol, usize>,
21}
22
23impl Stratification {
24    /// Returns the stratum index for a predicate, or `None` if
25    /// the predicate does not appear in the program (pure EDB
26    /// predicates not derived by any rule).
27    #[must_use]
28    pub fn stratum_of(&self, predicate: &PredicateSymbol) -> Option<usize> {
29        self.predicate_stratum.get(predicate).copied()
30    }
31}
32
33/// A single stratum — the set of predicates defined together.
34#[derive(Clone, Debug, Default, Eq, PartialEq, serde::Serialize, serde::Deserialize)]
35#[serde(deny_unknown_fields)]
36pub struct Stratum {
37    /// Predicates whose rules must be evaluated to a fixed point
38    /// within this stratum.
39    pub predicates: BTreeSet<PredicateSymbol>,
40}
41
42/// Stratification failure.
43#[derive(Clone, Debug, Eq, PartialEq, serde::Serialize, serde::Deserialize)]
44#[serde(deny_unknown_fields)]
45pub enum StratificationError {
46    /// The predicate dependency graph contains a cycle that
47    /// passes through a negation edge.
48    UnstratifiableCycle {
49        /// Every predicate in the offending strongly connected
50        /// component.
51        predicates: Vec<PredicateSymbol>,
52    },
53}
54
55/// Classification of a rule head's trailing graph slot (context-aware).
56///
57/// Stratification keys dependency-graph nodes on
58/// `(PredicateSymbol, HeadGraphClass)` so a producer that pins
59/// every inferred quad to a fixed graph
60/// (`GraphExpr::Literal { graph }` in the reasoner — head ends in
61/// a constant graph IRI) creates a node that's distinct from a
62/// producer emitting into a body-inherited graph
63/// (`GraphExpr::InheritFromBody { .. }` — head ends in a graph
64/// variable like `__g0`). Downstream consumers that constrain
65/// their body graph slot to a constant IRI then depend only on
66/// the producers compatible with that graph.
67///
68/// For the canonical RDFS / OWL-RL profile every rule head ends
69/// in a graph variable (context-aware's `InheritFromBody { 0 }` default),
70/// so every node collapses to [`HeadGraphClass::Inherit`] and the
71/// per-predicate strata that come out the other end match the
72/// pre-context-aware algorithm bit-for-bit.
73#[derive(Clone, Debug, Eq, Hash, Ord, PartialEq, PartialOrd)]
74pub(super) enum HeadGraphClass {
75    /// Head has no trailing term — pre-context-aware narrow atoms
76    /// (predicate-only facts or rules whose head atom is
77    /// constructed without a graph slot).
78    Narrow,
79    /// Head's trailing graph term is a variable — the inferred
80    /// quad inherits its graph from whichever body atom binds
81    /// that variable, so the rule contributes facts to every
82    /// graph class its body atom matches.
83    Inherit,
84    /// Head's trailing graph term is a constant IRI — every
85    /// inferred quad lands in this fixed graph.
86    Literal(ConstantSymbol),
87}
88
89impl HeadGraphClass {
90    /// Classify a head atom's trailing term.
91    ///
92    /// The classification mirrors how the reasoner's
93    /// `GraphExpr` rewrites head atoms at compile time
94    /// ([`super::super`] of this module sees only the resulting
95    /// term, not the original `GraphExpr`):
96    ///
97    /// - trailing `Term::Variable` → [`HeadGraphClass::Inherit`]
98    /// - trailing `Term::Constant` → [`HeadGraphClass::Literal`]
99    /// - no trailing term → [`HeadGraphClass::Narrow`]
100    /// - trailing `Term::TripleTerm` / `Term::Skolem` collapses to
101    ///   [`HeadGraphClass::Inherit`] because both produce a value computed from
102    ///   body bindings rather than a fixed IRI known at compile time.
103    #[must_use]
104    pub(super) fn classify(head: &Atom) -> Self {
105        match head.terms.last() {
106            None => Self::Narrow,
107            Some(Term::Constant(c)) => Self::Literal(c.clone()),
108            Some(Term::Variable(_) | Term::TripleTerm(_) | Term::Skolem { .. }) => Self::Inherit,
109        }
110    }
111}
datalog_structural_model/stratify/types.rs

datalog_structural_model/stratify/
types.rs
