datalog_structural_model/ir/equality_mode.rs
1//! Equality-mode flag for Datalog program validation.
2//!
3//! Some Datalog features interact non-monotonically with
4//! equality rewriting. Specifically, when the
5//! reasoner rewrites terms across equality classes (the
6//! `eq-rep-s` / `eq-rep-p` / `eq-rep-o` rules; see
7//! [`crate::ir::Literal::Negative`] for the corresponding
8//! body-literal shape), the set a negated atom is evaluated
9//! against can change shape mid-evaluation, and the multiset an
10//! aggregate folds over likewise shifts. Both lead to
11//! semantically unstable results.
12//!
13//! Programs that combine negation or aggregation with equality mode are
14//! rejected because those operators depend on the complete contents of the
15//! equality classes. This restriction keeps validation explicit and prevents
16//! an evaluator from silently changing results while equality classes merge.
17
18/// Equality-reasoning mode under which a Datalog program is
19/// validated.
20///
21/// Programs are checked under [`Self::Default`] by
22/// [`Program::validate`](super::program::Program::validate); callers that have
23/// an active equality-rewriting regime pass [`Self::SameAs`] through
24/// [`Program::validate_with_equality_mode`](super::program::Program::validate_with_equality_mode)
25/// to additionally reject negation and aggregation. The two
26/// methods share their other checks (safety, stratification,
27/// triple-term nesting).
28#[derive(
29 Clone, Copy, Debug, Default, Eq, Hash, PartialEq, serde::Serialize, serde::Deserialize,
30)]
31#[serde(deny_unknown_fields)]
32pub enum EqualityMode {
33 /// No special equality-reasoning regime. All Datalog
34 /// features — including negation and aggregation — are
35 /// allowed.
36 #[default]
37 Default,
38 /// The evaluator rewrites terms across equality classes. Negation
39 /// and aggregation are rejected at validation time because
40 /// they interact non-monotonically with the rewrite — see
41 /// the module-level docs.
42 SameAs,
43}