datalog_structural_model/ir/
atom.rs

1//! Datalog [`Atom`] — predicate applied to an ordered term list.
2
3use std::collections::BTreeSet;
4use std::fmt;
5
6use super::symbols::{PredicateSymbol, VariableSymbol};
7use super::term::Term;
8
9/// Datalog atom: `predicate(term_1, ..., term_n)`.
10#[derive(Clone, Debug, Eq, Hash, PartialEq)]
11pub struct Atom {
12    /// Predicate identifier.
13    pub predicate: PredicateSymbol,
14    /// Ordered list of terms.
15    pub terms: Vec<Term>,
16}
17
18impl Atom {
19    /// Arity of the atom.
20    #[must_use]
21    pub fn arity(&self) -> usize {
22        self.terms.len()
23    }
24
25    /// All variables that appear anywhere in this atom, including
26    /// variables nested inside [`Term::TripleTerm`] arguments
27    /// (recursively).
28    #[must_use]
29    pub(super) fn variables(&self) -> BTreeSet<VariableSymbol> {
30        let mut acc = BTreeSet::new();
31        self.collect_variables(&mut acc);
32        acc
33    }
34
35    fn collect_variables(&self, acc: &mut BTreeSet<VariableSymbol>) {
36        for term in &self.terms {
37            collect_term_variables(term, acc);
38        }
39    }
40
41    /// Returns `true` when any argument (including those nested
42    /// inside a [`Term::TripleTerm`]) is a `SKOLEM(...)` term.
43    /// Used by validation to reject `SKOLEM` outside head atoms —
44    /// a SKOLEM term has no pattern semantics, so it can't appear
45    /// in a body literal.
46    #[must_use]
47    pub(super) fn contains_skolem(&self) -> bool {
48        self.terms.iter().any(term_contains_skolem)
49    }
50
51    /// Maximum [`Term::TripleTerm`] nesting depth observed
52    /// anywhere in this atom's argument tree. `0` for a
53    /// plain-term atom; otherwise the depth of the deepest
54    /// nested triple-term.
55    #[must_use]
56    pub(super) fn nesting_depth(&self) -> usize {
57        self.terms
58            .iter()
59            .map(Term::nesting_depth)
60            .max()
61            .unwrap_or(0)
62    }
63}
64
65fn collect_term_variables(term: &Term, acc: &mut BTreeSet<VariableSymbol>) {
66    match term {
67        Term::Variable(var) => {
68            acc.insert(var.clone());
69        }
70        Term::Constant(_) => {}
71        Term::TripleTerm(inner) => {
72            for child in &inner.terms {
73                collect_term_variables(child, acc);
74            }
75        }
76        Term::Skolem { args, .. } => {
77            for arg in args {
78                collect_term_variables(arg, acc);
79            }
80        }
81    }
82}
83
84fn term_contains_skolem(term: &Term) -> bool {
85    match term {
86        Term::Skolem { .. } => true,
87        Term::TripleTerm(inner) => inner.terms.iter().any(term_contains_skolem),
88        Term::Variable(_) | Term::Constant(_) => false,
89    }
90}
91
92/// Display an [`Atom`] as `predicate(term_1, term_2, …)`. Used
93/// directly by [`Term`]'s [`std::fmt::Display`] impl for non-2-arity
94/// triple terms and available to error messages / debugging.
95impl fmt::Display for Atom {
96    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
97        write!(f, "{}(", self.predicate.as_str())?;
98        for (idx, term) in self.terms.iter().enumerate() {
99            if idx > 0 {
100                write!(f, ", ")?;
101            }
102            write!(f, "{term}")?;
103        }
104        write!(f, ")")
105    }
106}
datalog_structural_model/ir/atom.rs

datalog_structural_model/ir/
atom.rs
