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(Clone, Copy, Debug, Default, Eq, Hash, PartialEq)]
29pub enum EqualityMode {
30 /// No special equality-reasoning regime. All Datalog
31 /// features — including negation and aggregation — are
32 /// allowed.
33 #[default]
34 Default,
35 /// The evaluator rewrites terms across equality classes. Negation
36 /// and aggregation are rejected at validation time because
37 /// they interact non-monotonically with the rewrite — see
38 /// the module-level docs.
39 SameAs,
40}