datalog_structural_model/stratify/
types.rs

1//! Public rule scheduling result types and errors.
2
3use crate::ir::PredicateSymbol;
4use std::collections::BTreeSet;
5
6/// Rule-level stratification of a finite Datalog program.
7///
8/// Dependencies connect a producer to a consumer only when the producer's
9/// complete head pattern can unify with a body atom. EDB facts are available
10/// before stratum zero. Rule indices refer to the analyzed program's rule order.
11#[derive(Clone, Debug, Eq, PartialEq, serde::Serialize, serde::Deserialize)]
12#[serde(deny_unknown_fields)]
13pub struct Stratification {
14    /// Strata in evaluation order; close each to a fixed point before advancing.
15    pub strata: Vec<Stratum>,
16    /// One stratum index for each rule, in program order.
17    pub rule_stratum: Vec<usize>,
18}
19
20impl Stratification {
21    /// Return the stratum of a rule, or `None` for an out-of-range rule index.
22    #[must_use]
23    pub fn stratum_of_rule(&self, rule_index: usize) -> Option<usize> {
24        self.rule_stratum.get(rule_index).copied()
25    }
26}
27
28/// A set of rules evaluated together to a fixed point.
29#[derive(Clone, Debug, Default, Eq, PartialEq, serde::Serialize, serde::Deserialize)]
30#[serde(deny_unknown_fields)]
31pub struct Stratum {
32    /// Indices into the analyzed program's rule list.
33    pub rules: BTreeSet<usize>,
34}
35
36/// Stratification failure.
37#[derive(Clone, Debug, Eq, PartialEq, serde::Serialize, serde::Deserialize)]
38#[serde(deny_unknown_fields)]
39pub enum StratificationError {
40    /// A cycle of compatible rule dependencies contains negation or aggregation.
41    UnstratifiableCycle {
42        /// Predicates of the rules in the offending component, sorted and unique.
43        predicates: Vec<PredicateSymbol>,
44    },
45}
datalog_structural_model/stratify/types.rs

datalog_structural_model/stratify/
types.rs
