pub struct Program {
pub rules: Vec<Rule>,
}Expand description
Datalog program as an ordered set of rules.
Fields§
§rules: Vec<Rule>Program rules.
Implementations§
Source§impl Program
impl Program
Sourcepub fn validate(&self) -> Result<(), ProgramValidationError>
pub fn validate(&self) -> Result<(), ProgramValidationError>
Validate all rules in the program for safety and stratifiability.
Runs two checks:
- Safety — every rule must be range-restricted; head variables and variables inside negated body literals must also appear in some positive body literal.
- Stratifiability — the predicate dependency graph must have no
cycle that includes a negation edge (see
Program::stratify).
§Errors
Returns ProgramValidationError::UnsafeRule on a safety
failure, ProgramValidationError::UnsafeNegation when a
negated body literal references a variable that no positive
literal binds, or
ProgramValidationError::UnstratifiableNegation when the
program contains a recursive cycle through negation.
Sourcepub fn validate_with_equality_mode(
&self,
equality_mode: EqualityMode,
) -> Result<(), ProgramValidationError>
pub fn validate_with_equality_mode( &self, equality_mode: EqualityMode, ) -> Result<(), ProgramValidationError>
Validate the program under a specified equality-reasoning mode (extension).
Runs the same safety / stratification / triple-term-nesting
checks as Self::validate and additionally rejects
negation and aggregation when
equality_mode == EqualityMode::SameAs. The two features
interact non-monotonically with owl:sameAs rewriting; see
EqualityMode for the semantic rationale.
§Errors
Returns the same errors as Self::validate plus
ProgramValidationError::NegationUnderEqualityMode or
ProgramValidationError::AggregationUnderEqualityMode
when the corresponding feature is used under
EqualityMode::SameAs.
Sourcepub fn stratify(&self) -> Result<Stratification, ProgramValidationError>
pub fn stratify(&self) -> Result<Stratification, ProgramValidationError>
Compute the program’s stratification.
Builds the predicate dependency graph (edges from each body predicate to the head predicate, tagged with polarity), collapses strongly connected components, checks that no SCC contains an internal negation edge, and assigns each predicate to a stratum such that every negation edge goes from a lower stratum to a strictly higher one.
§Errors
Returns ProgramValidationError::UnstratifiableNegation
when a cycle in the dependency graph contains a negation
edge.