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

datalog_structural_model/stratify/
types.rs
