datalog_structural_model/ir/
program.rs

1//! Datalog [`Program`] — an ordered set of [`Rule`]s plus
2//! validation and stratification entry points.
3
4use super::atom::Atom;
5use super::equality_mode::EqualityMode;
6use super::error::ProgramValidationError;
7use super::literal::Literal;
8use super::rule::Rule;
9use super::term::MAX_TRIPLE_TERM_NESTING;
10use crate::stratify::{Stratification, stratify};
11
12/// Datalog program as an ordered set of rules.
13#[derive(Clone, Debug, Default, Eq, PartialEq)]
14pub struct Program {
15    /// Program rules.
16    pub rules: Vec<Rule>,
17}
18
19impl Program {
20    /// Validate all rules in the program for safety and
21    /// stratifiability.
22    ///
23    /// Runs two checks:
24    ///
25    /// 1. **Safety** — every rule must be range-restricted; head variables and
26    ///    variables inside negated body literals must also appear in some
27    ///    positive body literal.
28    /// 2. **Stratifiability** — the predicate dependency graph must have no
29    ///    cycle that includes a negation edge (see [`Program::stratify`]).
30    ///
31    /// # Errors
32    ///
33    /// Returns [`ProgramValidationError::UnsafeRule`] on a safety
34    /// failure, [`ProgramValidationError::UnsafeNegation`] when a
35    /// negated body literal references a variable that no positive
36    /// literal binds, or
37    /// [`ProgramValidationError::UnstratifiableNegation`] when the
38    /// program contains a recursive cycle through negation.
39    pub fn validate(&self) -> Result<(), ProgramValidationError> {
40        self.validate_with_equality_mode(EqualityMode::Default)
41    }
42
43    /// Validate the program under a specified equality-reasoning
44    /// mode (extension).
45    ///
46    /// Runs the same safety / stratification / triple-term-nesting
47    /// checks as [`Self::validate`] and additionally rejects
48    /// negation and aggregation when
49    /// `equality_mode == EqualityMode::SameAs`. The two features
50    /// interact non-monotonically with `owl:sameAs` rewriting; see
51    /// [`EqualityMode`] for the semantic rationale.
52    ///
53    /// # Errors
54    ///
55    /// Returns the same errors as [`Self::validate`] plus
56    /// [`ProgramValidationError::NegationUnderEqualityMode`] or
57    /// [`ProgramValidationError::AggregationUnderEqualityMode`]
58    /// when the corresponding feature is used under
59    /// [`EqualityMode::SameAs`].
60    pub fn validate_with_equality_mode(
61        &self,
62        equality_mode: EqualityMode,
63    ) -> Result<(), ProgramValidationError> {
64        if equality_mode == EqualityMode::SameAs {
65            check_equality_mode_compatibility(&self.rules)?;
66        }
67        for (index, rule) in self.rules.iter().enumerate() {
68            // Triple-term nesting bound — checked before the
69            // safety analyses because deeper nesting indicates a
70            // structural problem unrelated to variable binding.
71            let head_depth = rule.head.nesting_depth();
72            let body_depth = rule
73                .body
74                .iter()
75                .filter_map(Literal::atom)
76                .map(Atom::nesting_depth)
77                .max()
78                .unwrap_or(0);
79            let depth = head_depth.max(body_depth);
80            if depth > MAX_TRIPLE_TERM_NESTING {
81                return Err(ProgramValidationError::TripleTermNestingExceeded {
82                    rule_index: index,
83                    depth,
84                    limit: MAX_TRIPLE_TERM_NESTING,
85                });
86            }
87            let unsafe_head = rule.unsafe_head_variables();
88            if !unsafe_head.is_empty() {
89                return Err(ProgramValidationError::UnsafeRule {
90                    rule_index: index,
91                    variables: unsafe_head,
92                });
93            }
94            let unsafe_neg = rule.unsafe_negative_variables();
95            if !unsafe_neg.is_empty() {
96                return Err(ProgramValidationError::UnsafeNegation {
97                    rule_index: index,
98                    variables: unsafe_neg,
99                });
100            }
101            let unsafe_filter = rule.unsafe_filter_variables();
102            if !unsafe_filter.is_empty() {
103                return Err(ProgramValidationError::UnsafeFilter {
104                    rule_index: index,
105                    variables: unsafe_filter,
106                });
107            }
108            let unsafe_bind = rule.unsafe_bind_variables();
109            if !unsafe_bind.is_empty() {
110                return Err(ProgramValidationError::UnsafeBind {
111                    rule_index: index,
112                    variables: unsafe_bind,
113                });
114            }
115            if rule.has_skolem_in_body() {
116                return Err(ProgramValidationError::SkolemInBodyAtom { rule_index: index });
117            }
118            if rule.has_nested_aggregate_in_inner_body() {
119                return Err(ProgramValidationError::NestedAggregateInInnerBody {
120                    rule_index: index,
121                });
122            }
123            let unsafe_aggregate = rule.unsafe_aggregate_variables();
124            if !unsafe_aggregate.is_empty() {
125                return Err(ProgramValidationError::UnsafeAggregate {
126                    rule_index: index,
127                    variables: unsafe_aggregate,
128                });
129            }
130        }
131        // Stratification check — reject programs with recursion
132        // through negation.
133        self.stratify()?;
134        Ok(())
135    }
136
137    /// Compute the program's stratification.
138    ///
139    /// Builds the predicate dependency graph (edges from each body
140    /// predicate to the head predicate, tagged with polarity),
141    /// collapses strongly connected components, checks that no SCC
142    /// contains an internal negation edge, and assigns each
143    /// predicate to a stratum such that every negation edge goes
144    /// from a lower stratum to a strictly higher one.
145    ///
146    /// # Errors
147    ///
148    /// Returns [`ProgramValidationError::UnstratifiableNegation`]
149    /// when a cycle in the dependency graph contains a negation
150    /// edge.
151    pub fn stratify(&self) -> Result<Stratification, ProgramValidationError> {
152        stratify(self).map_err(ProgramValidationError::from)
153    }
154}
155
156/// extension — reject negation / aggregation under
157/// [`EqualityMode::SameAs`]. Walks each rule's body and surfaces
158/// the first offending literal as
159/// [`ProgramValidationError::NegationUnderEqualityMode`] or
160/// [`ProgramValidationError::AggregationUnderEqualityMode`].
161fn check_equality_mode_compatibility(rules: &[Rule]) -> Result<(), ProgramValidationError> {
162    for (index, rule) in rules.iter().enumerate() {
163        for lit in &rule.body {
164            match lit {
165                Literal::Negative(_) => {
166                    return Err(ProgramValidationError::NegationUnderEqualityMode {
167                        rule_index: index,
168                    });
169                }
170                Literal::Aggregate(_) => {
171                    return Err(ProgramValidationError::AggregationUnderEqualityMode {
172                        rule_index: index,
173                    });
174                }
175                Literal::Positive(_) | Literal::Filter(_) | Literal::Bind { .. } => {}
176            }
177        }
178    }
179    Ok(())
180}
datalog_structural_model/ir/program.rs

datalog_structural_model/ir/
program.rs
