From 582598e3c20082d435e93dd7b792974160677765 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Louis=20Gr=C3=B6ger?= Date: Sun, 23 Aug 2026 14:40:43 +0200 Subject: [PATCH 01/13] Track rule origin through skolemization --- nemo/src/execution/tracing/resolve_origin.rs | 1 + nemo/src/rule_model/error.rs | 1 + nemo/src/rule_model/origin.rs | 3 +++ nemo/src/rule_model/pipeline/transformations/skolem.rs | 4 +++- 4 files changed, 8 insertions(+), 1 deletion(-) diff --git a/nemo/src/execution/tracing/resolve_origin.rs b/nemo/src/execution/tracing/resolve_origin.rs index ad050e8e3..834affc9a 100644 --- a/nemo/src/execution/tracing/resolve_origin.rs +++ b/nemo/src/execution/tracing/resolve_origin.rs @@ -40,6 +40,7 @@ pub fn tracing_resolve_origin_id( | Origin::Extern | Origin::Substitution { .. } => id, Origin::Normalization(origin_id) + | Origin::Skolemization(origin_id) | Origin::Global(origin_id) | Origin::Incremental(origin_id) | Origin::MergeSparql(origin_id) => tracing_resolve_origin_id(handle, origin_id), diff --git a/nemo/src/rule_model/error.rs b/nemo/src/rule_model/error.rs index 25a56c278..e3a03d7a5 100644 --- a/nemo/src/rule_model/error.rs +++ b/nemo/src/rule_model/error.rs @@ -407,6 +407,7 @@ impl ValidationReport { None } Origin::Normalization(id) + | Origin::Skolemization(id) | Origin::Global(id) | Origin::Incremental(id) | Origin::MergeSparql(id) => Self::id_to_range(program, *id, error), diff --git a/nemo/src/rule_model/origin.rs b/nemo/src/rule_model/origin.rs index 4e07466ac..eeb55018a 100644 --- a/nemo/src/rule_model/origin.rs +++ b/nemo/src/rule_model/origin.rs @@ -40,6 +40,9 @@ pub enum Origin { /// Rule that was created by normalizing a rule Normalization(ProgramComponentId), + /// Rule that was created by skolemizing a rule + Skolemization(ProgramComponentId), + /// Statement that was created by substituting global variables in a rule Global(ProgramComponentId), diff --git a/nemo/src/rule_model/pipeline/transformations/skolem.rs b/nemo/src/rule_model/pipeline/transformations/skolem.rs index 5205b1a24..5dda7a4f5 100644 --- a/nemo/src/rule_model/pipeline/transformations/skolem.rs +++ b/nemo/src/rule_model/pipeline/transformations/skolem.rs @@ -4,7 +4,7 @@ use std::collections::{HashMap, HashSet}; use crate::rule_model::{ components::{ - IterableVariables, + ComponentIdentity, ComponentSource, IterableVariables, literal::Literal, statement::Statement, term::{ @@ -14,6 +14,7 @@ use crate::rule_model::{ }, }, error::ValidationReport, + origin::Origin, programs::{ProgramRead, ProgramWrite, handle::ProgramHandle}, }; @@ -62,6 +63,7 @@ impl ProgramTransformation for TransformationSkolemize { .collect::>(); let mut new_rule = rule.clone(); + new_rule.set_origin(Origin::Skolemization(rule.id())); let mut sk_terms_by_ex_var = HashMap::new(); for head_atom in new_rule.head_mut() { for term in head_atom.terms_mut() { From bd8e5c9105129cdf54c0100de56cbbbf98370e36 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Louis=20Gr=C3=B6ger?= Date: Sun, 23 Aug 2026 14:41:45 +0200 Subject: [PATCH 02/13] Expose rule variable iterators --- nemo/src/rule_model/components/rule.rs | 59 +++++++++++++++----------- 1 file changed, 34 insertions(+), 25 deletions(-) diff --git a/nemo/src/rule_model/components/rule.rs b/nemo/src/rule_model/components/rule.rs index a23027967..32e60a936 100644 --- a/nemo/src/rule_model/components/rule.rs +++ b/nemo/src/rule_model/components/rule.rs @@ -164,6 +164,24 @@ impl Rule { &mut self.head } + /// Return an iterator over all existential variables in this rule. + pub fn existential_variables(&self) -> impl Iterator { + self.variables() + .filter(|variable| variable.is_existential()) + } + + /// Return an iterator over the variables bound in positive body atoms. + pub fn positive_variables(&self) -> impl Iterator { + self.body_positive().flat_map(|atom| { + atom.terms() + .filter_map(|term| match term { + Term::Primitive(Primitive::Variable(variable)) => Some(variable), + _ => None, + }) + .filter(|variable| variable.is_universal() && variable.name().is_some()) + }) + } + /// Return an iterator over all positive and negative [Atom]s /// contained in the body of this rule. pub fn body_atoms(&self) -> impl Iterator { @@ -196,32 +214,24 @@ impl Rule { self.imports.push(import); } - /// Return the set of variables that are bound in positive body atoms. - pub fn positive_variables(&self) -> HashSet<&Variable> { - let mut result = HashSet::new(); - - for literal in &self.body { - if let Literal::Positive(atom) = literal { - for term in atom.terms() { - if let Term::Primitive(Primitive::Variable(variable)) = term - && variable.is_universal() - && variable.name().is_some() - { - result.insert(variable); - } - } - } - } - - result + /// Return an iterator over the frontier variables of this rule. + pub fn frontier_variables(&self) -> impl Iterator { + let positive_variables = self.positive_variables().collect::>(); + self.universal_head_variables() + .filter(move |variable| positive_variables.contains(variable)) } - /// Return the set of variables that are bound by import statements - pub fn import_variables(&self) -> HashSet<&Variable> { - self.imports + /// Return an iterator over all universal variables in the head of this rule. + fn universal_head_variables(&self) -> impl Iterator { + self.head .iter() - .flat_map(|import| import.variables()) - .collect::>() + .flat_map(|atom| atom.variables()) + .filter(|variable| variable.is_universal()) + } + + /// Return an iterator over the variables bound by import statements. + pub fn import_variables(&self) -> impl Iterator { + self.imports.iter().flat_map(|import| import.variables()) } /// Return a set of "safe" variables. @@ -233,8 +243,7 @@ impl Rule { pub fn safe_variables(&self) -> HashSet<&Variable> { let mut result = self .positive_variables() - .union(&self.import_variables()) - .cloned() + .chain(self.import_variables()) .collect::>(); loop { From bb8cb46d2a5dcfe2804f878e07756bd226f99863 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Louis=20Gr=C3=B6ger?= Date: Sun, 23 Aug 2026 14:42:03 +0200 Subject: [PATCH 03/13] Add universal variable iterator to atoms --- nemo/src/rule_model/components/atom.rs | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/nemo/src/rule_model/components/atom.rs b/nemo/src/rule_model/components/atom.rs index 5d69e756b..78c478c5f 100644 --- a/nemo/src/rule_model/components/atom.rs +++ b/nemo/src/rule_model/components/atom.rs @@ -116,6 +116,11 @@ impl Atom { pub fn remove(&mut self, index: usize) -> Term { self.terms.remove(index) } + + /// Return an iterator over the universal variables in this atom. + pub fn universal_variables(&self) -> impl Iterator { + self.variables().filter(|variable| variable.is_universal()) + } } impl Index for Atom { From d1e586c7cd1f3dd27f7bf700240c001c8ee85fc7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Louis=20Gr=C3=B6ger?= Date: Sun, 23 Aug 2026 14:42:33 +0200 Subject: [PATCH 04/13] Add borrowed predicate accessors --- nemo/src/rule_model/components/atom.rs | 5 +++++ nemo/src/rule_model/components/literal.rs | 9 +++++++++ nemo/src/rule_model/components/rule.rs | 10 ++++++++++ 3 files changed, 24 insertions(+) diff --git a/nemo/src/rule_model/components/atom.rs b/nemo/src/rule_model/components/atom.rs index 78c478c5f..dce8b5d71 100644 --- a/nemo/src/rule_model/components/atom.rs +++ b/nemo/src/rule_model/components/atom.rs @@ -94,6 +94,11 @@ impl Atom { self.predicate.clone() } + /// Return a reference to the predicate of this atom. + pub fn predicate_ref(&self) -> &Tag { + &self.predicate + } + /// Return an iterator over the terms of this atom. pub fn terms(&self) -> impl Iterator { self.terms.iter() diff --git a/nemo/src/rule_model/components/literal.rs b/nemo/src/rule_model/components/literal.rs index 04e0699c2..4098ca213 100644 --- a/nemo/src/rule_model/components/literal.rs +++ b/nemo/src/rule_model/components/literal.rs @@ -52,6 +52,15 @@ impl Literal { Literal::Operation(_) => None, } } + + /// If this literal is not an operation, return a reference to its predicate. + /// Returns `None` otherwise. + pub fn predicate_ref(&self) -> Option<&Tag> { + match self { + Literal::Positive(atom) | Literal::Negative(atom) => Some(atom.predicate_ref()), + Literal::Operation(_) => None, + } + } } impl Display for Literal { diff --git a/nemo/src/rule_model/components/rule.rs b/nemo/src/rule_model/components/rule.rs index 32e60a936..2980bb1ee 100644 --- a/nemo/src/rule_model/components/rule.rs +++ b/nemo/src/rule_model/components/rule.rs @@ -18,6 +18,7 @@ use super::{ atom::Atom, component_iterator, component_iterator_mut, literal::Literal, + tag::Tag, term::{ Term, primitive::{Primitive, variable::Variable}, @@ -197,6 +198,15 @@ impl Rule { self.head.iter().chain(self.body_atoms()) } + /// Return references to the predicates of all atoms in this rule. + pub fn predicates_ref(&self) -> Vec<&Tag> { + self.body + .iter() + .filter_map(Literal::predicate_ref) + .chain(self.head.iter().map(Atom::predicate_ref)) + .collect() + } + /// Return an iterator over all [ImportLiteral]s /// that are evaluated as part of this rule. pub fn imports(&self) -> impl Iterator { From 41ae2c304dfedc1597beb66082dc9e8e96fdb825 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Louis=20Gr=C3=B6ger?= Date: Sun, 23 Aug 2026 14:42:57 +0200 Subject: [PATCH 05/13] Expose tagged function term constructor --- nemo/src/rule_model/components/term/function.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/nemo/src/rule_model/components/term/function.rs b/nemo/src/rule_model/components/term/function.rs index 4639cb645..562336572 100644 --- a/nemo/src/rule_model/components/term/function.rs +++ b/nemo/src/rule_model/components/term/function.rs @@ -73,7 +73,7 @@ impl FunctionTerm { } /// Create a new [FunctionTerm] with a [Tag]. - pub(crate) fn new_tagged>(tag: Tag, subterms: Terms) -> Self { + pub fn new_tagged>(tag: Tag, subterms: Terms) -> Self { Self { origin: Origin::default(), id: ProgramComponentId::default(), From ae4afd0a1af5e77be81d097909cd8cd82f3200bc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Louis=20Gr=C3=B6ger?= Date: Sun, 23 Aug 2026 14:43:43 +0200 Subject: [PATCH 06/13] Implement total ordering for tags and variables --- nemo/src/rule_model/components/tag.rs | 8 +++++++- nemo/src/rule_model/components/term/primitive/variable.rs | 2 +- .../components/term/primitive/variable/existential.rs | 8 +++++++- .../components/term/primitive/variable/global.rs | 8 +++++++- .../components/term/primitive/variable/universal.rs | 8 +++++++- 5 files changed, 29 insertions(+), 5 deletions(-) diff --git a/nemo/src/rule_model/components/tag.rs b/nemo/src/rule_model/components/tag.rs index 1903b5ebb..e2d28c3a8 100644 --- a/nemo/src/rule_model/components/tag.rs +++ b/nemo/src/rule_model/components/tag.rs @@ -62,9 +62,15 @@ impl PartialEq for Tag { impl Eq for Tag {} +impl Ord for Tag { + fn cmp(&self, other: &Self) -> std::cmp::Ordering { + self.tag.cmp(&other.tag) + } +} + impl PartialOrd for Tag { fn partial_cmp(&self, other: &Self) -> Option { - self.tag.partial_cmp(&other.tag) + Some(self.cmp(other)) } } diff --git a/nemo/src/rule_model/components/term/primitive/variable.rs b/nemo/src/rule_model/components/term/primitive/variable.rs index 46cce2d30..53ca43363 100644 --- a/nemo/src/rule_model/components/term/primitive/variable.rs +++ b/nemo/src/rule_model/components/term/primitive/variable.rs @@ -26,7 +26,7 @@ pub mod universal; /// /// A general placeholder that can be bound to any value. /// We distinguish [UniversalVariable] and [ExistentialVariable]. -#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd)] +#[derive(Debug, Clone, PartialEq, Eq, Hash, Ord, PartialOrd)] pub enum Variable { /// Universal variable Universal(UniversalVariable), diff --git a/nemo/src/rule_model/components/term/primitive/variable/existential.rs b/nemo/src/rule_model/components/term/primitive/variable/existential.rs index 44c2ddb0f..cdf2187b8 100644 --- a/nemo/src/rule_model/components/term/primitive/variable/existential.rs +++ b/nemo/src/rule_model/components/term/primitive/variable/existential.rs @@ -76,9 +76,15 @@ impl PartialEq for ExistentialVariable { impl Eq for ExistentialVariable {} +impl Ord for ExistentialVariable { + fn cmp(&self, other: &Self) -> std::cmp::Ordering { + self.name.cmp(&other.name) + } +} + impl PartialOrd for ExistentialVariable { fn partial_cmp(&self, other: &Self) -> Option { - self.name.partial_cmp(&other.name) + Some(self.cmp(other)) } } diff --git a/nemo/src/rule_model/components/term/primitive/variable/global.rs b/nemo/src/rule_model/components/term/primitive/variable/global.rs index 8e6ca8f13..34a9844a6 100644 --- a/nemo/src/rule_model/components/term/primitive/variable/global.rs +++ b/nemo/src/rule_model/components/term/primitive/variable/global.rs @@ -70,9 +70,15 @@ impl PartialEq for GlobalVariable { impl Eq for GlobalVariable {} +impl Ord for GlobalVariable { + fn cmp(&self, other: &Self) -> std::cmp::Ordering { + self.name.cmp(&other.name) + } +} + impl PartialOrd for GlobalVariable { fn partial_cmp(&self, other: &Self) -> Option { - self.name.partial_cmp(&other.name) + Some(self.cmp(other)) } } diff --git a/nemo/src/rule_model/components/term/primitive/variable/universal.rs b/nemo/src/rule_model/components/term/primitive/variable/universal.rs index 8b9893595..4707f8f73 100644 --- a/nemo/src/rule_model/components/term/primitive/variable/universal.rs +++ b/nemo/src/rule_model/components/term/primitive/variable/universal.rs @@ -100,9 +100,15 @@ impl PartialEq for UniversalVariable { impl Eq for UniversalVariable {} +impl Ord for UniversalVariable { + fn cmp(&self, other: &Self) -> std::cmp::Ordering { + self.name.cmp(&other.name) + } +} + impl PartialOrd for UniversalVariable { fn partial_cmp(&self, other: &Self) -> Option { - self.name.partial_cmp(&other.name) + Some(self.cmp(other)) } } From e8031f62fd755284098f84bd9d71ca3efd805cb5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Louis=20Gr=C3=B6ger?= Date: Sun, 23 Aug 2026 14:52:06 +0200 Subject: [PATCH 07/13] Add critical instance transformation --- .../rule_model/pipeline/transformations.rs | 1 + .../pipeline/transformations/crit_instance.rs | 92 +++++++++++++++++++ 2 files changed, 93 insertions(+) create mode 100644 nemo/src/rule_model/pipeline/transformations/crit_instance.rs diff --git a/nemo/src/rule_model/pipeline/transformations.rs b/nemo/src/rule_model/pipeline/transformations.rs index 912b140d3..9ea89f539 100644 --- a/nemo/src/rule_model/pipeline/transformations.rs +++ b/nemo/src/rule_model/pipeline/transformations.rs @@ -1,6 +1,7 @@ //! This module defines [ProgramTransformation]s. pub mod active; +pub mod crit_instance; pub mod default; pub mod empty; pub mod exports; diff --git a/nemo/src/rule_model/pipeline/transformations/crit_instance.rs b/nemo/src/rule_model/pipeline/transformations/crit_instance.rs new file mode 100644 index 000000000..9c01e4c1a --- /dev/null +++ b/nemo/src/rule_model/pipeline/transformations/crit_instance.rs @@ -0,0 +1,92 @@ +//! This module defines [TransformationCriticalInstance]. + +use std::collections::HashSet; + +use itertools::Itertools; + +use super::ProgramTransformation; +use crate::rule_model::{ + components::{ + IterablePrimitives, fact::Fact, literal::Literal, rule::Rule, statement::Statement, + tag::Tag, term::Term, + }, + error::ValidationReport, + programs::{ProgramRead, ProgramWrite, handle::ProgramHandle}, +}; + +/// Program transformation that replaces a program's facts with its critical instance. +#[derive(Debug, Default, Clone, Copy)] +pub struct TransformationCriticalInstance; + +fn predicates_and_arities(rule: &Rule) -> impl Iterator { + rule.body() + .iter() + .filter_map(|literal| match literal { + Literal::Positive(atom) | Literal::Negative(atom) => Some(atom), + Literal::Operation(_) => None, + }) + .chain(rule.head()) + .map(|atom| (atom.predicate_ref(), atom.len())) +} + +/// Return predicate and arity pairs for all atoms in the provided rules. +pub fn preds_and_lens_of_rules<'a>(rules: &[&'a Rule]) -> impl Iterator { + rules.iter().flat_map(|rule| predicates_and_arities(rule)) +} + +/// Return every fact for the given predicate and arity that can be formed +/// from the provided constants. +pub fn facts_for_predicate_and_constants( + predicate: &Tag, + arity: usize, + constants: &[Term], +) -> HashSet { + (0..arity) + .map(|_| constants.iter().cloned()) + .multi_cartesian_product() + .map(|terms| Fact::new(predicate.clone(), terms)) + .collect() +} + +fn critical_instance(rules: &[&Rule]) -> impl Iterator { + let mut constants = rules + .iter() + .flat_map(|rule| rule.primitive_terms()) + .filter(|primitive| primitive.is_ground()) + .cloned() + .map(Term::from) + .collect::>(); + constants.push(Term::from("__STAR__")); + + let predicates_and_arities = preds_and_lens_of_rules(rules).collect::>(); + + predicates_and_arities + .into_iter() + .flat_map(move |(predicate, arity)| { + facts_for_predicate_and_constants(predicate, arity, &constants) + }) +} + +impl ProgramTransformation for TransformationCriticalInstance { + fn apply(self, program: &ProgramHandle) -> Result { + let mut commit = program.fork(); + + let rules = program + .statements() + .filter_map(|statement| { + if let Statement::Rule(rule) = statement { + commit.keep(statement); + Some(rule) + } else { + None + } + }) + .collect::>(); + + for fact in critical_instance(&rules) { + commit.add_fact(fact); + } + + commit.submit() + } +} From 4095705c79e6a95da1241fa2538b37bbe355f35e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Louis=20Gr=C3=B6ger?= Date: Sun, 23 Aug 2026 14:52:36 +0200 Subject: [PATCH 08/13] Add rule filtering transformation --- .../rule_model/pipeline/transformations.rs | 1 + .../pipeline/transformations/filter_rules.rs | 50 +++++++++++++++++++ 2 files changed, 51 insertions(+) create mode 100644 nemo/src/rule_model/pipeline/transformations/filter_rules.rs diff --git a/nemo/src/rule_model/pipeline/transformations.rs b/nemo/src/rule_model/pipeline/transformations.rs index 9ea89f539..24f443d20 100644 --- a/nemo/src/rule_model/pipeline/transformations.rs +++ b/nemo/src/rule_model/pipeline/transformations.rs @@ -6,6 +6,7 @@ pub mod default; pub mod empty; pub mod exports; pub mod filter_imports; +pub mod filter_rules; pub mod global; pub mod incremental; pub mod merge_sparql; diff --git a/nemo/src/rule_model/pipeline/transformations/filter_rules.rs b/nemo/src/rule_model/pipeline/transformations/filter_rules.rs new file mode 100644 index 000000000..edc17e0fc --- /dev/null +++ b/nemo/src/rule_model/pipeline/transformations/filter_rules.rs @@ -0,0 +1,50 @@ +//! This module defines [TransformationFilterRules]. + +use super::ProgramTransformation; +use crate::rule_model::{ + components::statement::Statement, + error::ValidationReport, + programs::{ProgramRead, handle::ProgramHandle}, +}; + +/// Program transformation that retains rules selected by a [RuleSelector]. +#[derive(Debug, Clone, Copy)] +pub struct TransformationFilterRules(pub RuleSelector); + +impl TransformationFilterRules { + fn matches(&self, statement: &Statement) -> bool { + let Statement::Rule(rule) = statement else { + return false; + }; + + let is_existential = rule.existential_variables().next().is_some(); + match self.0 { + RuleSelector::Existential => is_existential, + RuleSelector::NonExistential => !is_existential, + } + } +} + +/// Selects rules based on whether they contain existential variables. +#[derive(Debug, Clone, Copy)] +pub enum RuleSelector { + /// Select rules containing at least one existential variable. + Existential, + /// Select rules containing no existential variables. + NonExistential, +} + +impl ProgramTransformation for TransformationFilterRules { + fn apply(self, program: &ProgramHandle) -> Result { + let mut commit = program.fork(); + + for statement in program + .statements() + .filter(|statement| self.matches(statement)) + { + commit.keep(statement); + } + + commit.submit() + } +} From 4e4e89f0c557f05e0c14eb991b8fb18b10afd4ff Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Louis=20Gr=C3=B6ger?= Date: Sun, 23 Aug 2026 14:53:37 +0200 Subject: [PATCH 09/13] Add MSA transformation --- .../rule_model/pipeline/transformations.rs | 1 + .../pipeline/transformations/msa.rs | 148 ++++++++++++++++++ 2 files changed, 149 insertions(+) create mode 100644 nemo/src/rule_model/pipeline/transformations/msa.rs diff --git a/nemo/src/rule_model/pipeline/transformations.rs b/nemo/src/rule_model/pipeline/transformations.rs index 24f443d20..91c06218c 100644 --- a/nemo/src/rule_model/pipeline/transformations.rs +++ b/nemo/src/rule_model/pipeline/transformations.rs @@ -10,6 +10,7 @@ pub mod filter_rules; pub mod global; pub mod incremental; pub mod merge_sparql; +pub mod msa; pub mod normalize; pub mod set_default_outputs; pub mod skolem; diff --git a/nemo/src/rule_model/pipeline/transformations/msa.rs b/nemo/src/rule_model/pipeline/transformations/msa.rs new file mode 100644 index 000000000..cb7de5f14 --- /dev/null +++ b/nemo/src/rule_model/pipeline/transformations/msa.rs @@ -0,0 +1,148 @@ +//! This module defines [TransformationMSA]. + +use std::collections::HashSet; + +use super::ProgramTransformation; +use crate::rule_model::{ + components::{ + atom::Atom, + literal::Literal, + rule::Rule, + statement::Statement, + tag::Tag, + term::{ + Term, + primitive::{Primitive, variable::Variable}, + }, + }, + error::ValidationReport, + pipeline::commit::ProgramCommit, + programs::{ProgramRead, ProgramWrite, handle::ProgramHandle}, + substitution::Substitution, +}; + +/// Program transformation used to reduce model-summarizing acyclicity to fact entailment. +#[derive(Debug, Default, Clone, Copy)] +pub struct TransformationMSA; + +fn function_predicates(existential_variables: &[&Variable], rule_index: usize) -> Vec { + existential_variables + .iter() + .enumerate() + .map(|(variable_index, _)| Tag::new(format!("_msa_F_{rule_index}_{variable_index}"))) + .collect() +} + +fn modified_msa_rule( + rule: &Rule, + rule_index: usize, + s_predicate: &Tag, + existential_variables: &[&Variable], +) -> (Rule, Vec) { + let mut result = rule.clone(); + let function_predicates = function_predicates(existential_variables, rule_index); + let frontier_variables = rule.frontier_variables().collect::>(); + + for (function_predicate, existential_variable) in + function_predicates.iter().zip(existential_variables.iter()) + { + let existential_term = Term::from((*existential_variable).clone()); + result.head_mut().push(Atom::new( + function_predicate.clone(), + [existential_term.clone()], + )); + + for frontier_variable in &frontier_variables { + result.head_mut().push(Atom::new( + s_predicate.clone(), + [ + Term::from((*frontier_variable).clone()), + existential_term.clone(), + ], + )); + } + } + + let mut substitution = Substitution::default(); + for (variable_index, variable) in existential_variables.iter().enumerate() { + substitution.insert( + Primitive::from((*variable).clone()), + Term::from(format!("_msa_c_{rule_index}_{variable_index}")), + ); + } + substitution.apply(&mut result); + + (result, function_predicates) +} + +fn generic_rules(s_predicate: &Tag, d_predicate: &Tag, x1: &Term, x2: &Term) -> [Rule; 2] { + let x3 = Term::from(Variable::universal("_msa_x3")); + + let s_x1_x2 = Literal::Positive(Atom::new(s_predicate.clone(), [x1.clone(), x2.clone()])); + let s_x2_x3 = Literal::Positive(Atom::new(s_predicate.clone(), [x2.clone(), x3.clone()])); + let d_x1_x2 = Atom::new(d_predicate.clone(), [x1.clone(), x2.clone()]); + let d_x1_x3 = Atom::new(d_predicate.clone(), [x1.clone(), x3]); + + [ + Rule::new([d_x1_x2.clone()].into(), [s_x1_x2].into()), + Rule::new( + [d_x1_x3].into(), + [Literal::Positive(d_x1_x2), s_x2_x3].into(), + ), + ] +} + +fn function_rules( + function_predicates: &[Tag], + d_predicate: &Tag, + x1: &Term, + x2: &Term, +) -> impl Iterator { + let c_atom = Atom::new(Tag::from("_msa_C"), [Term::from("nullaryPredsNotAllowed")]); + + function_predicates.iter().map(move |function_predicate| { + let f_x1 = Literal::Positive(Atom::new(function_predicate.clone(), [x1.clone()])); + let f_x2 = Literal::Positive(Atom::new(function_predicate.clone(), [x2.clone()])); + let d_x1_x2 = Literal::Positive(Atom::new(d_predicate.clone(), [x1.clone(), x2.clone()])); + + Rule::new([c_atom.clone()].into(), [f_x1, d_x1_x2, f_x2].into()) + }) +} + +impl ProgramTransformation for TransformationMSA { + fn apply(self, program: &ProgramHandle) -> Result { + let mut commit: ProgramCommit = program.fork(); + + let s_predicate = Tag::from("_msa_S"); + let d_predicate = Tag::from("_msa_D"); + let x1 = Term::from(Variable::universal("_msa_x1")); + let x2 = Term::from(Variable::universal("_msa_x2")); + + for rule in generic_rules(&s_predicate, &d_predicate, &x1, &x2) { + commit.add_rule(rule); + } + + for (rule_index, statement) in program.statements().enumerate() { + let Statement::Rule(rule) = statement else { + commit.keep(statement); + continue; + }; + + let existential_variables = rule.existential_variables().collect::>(); + if existential_variables.is_empty() { + commit.keep(statement); + continue; + } + + let (modified_rule, function_predicates) = + modified_msa_rule(rule, rule_index, &s_predicate, &existential_variables); + commit.add_rule(modified_rule); + + for rule in function_rules(&function_predicates, &d_predicate, &x1, &x2) { + commit.add_rule(rule); + } + } + + commit.submit() + } +} From f5ff26800f9ae6ea92413035c1dc0644dea5b8d9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Louis=20Gr=C3=B6ger?= Date: Wed, 7 Oct 2026 14:28:21 +0200 Subject: [PATCH 10/13] reworked rule.positive_variables() by using atom.universal_variables() --- .gitignore | 3 +++ nemo/src/rule_model/components/rule.rs | 8 ++------ 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/.gitignore b/.gitignore index 93bd5279a..852b0cf5b 100644 --- a/.gitignore +++ b/.gitignore @@ -34,3 +34,6 @@ flycheck_*.el # ide settings /.vscode + +# macOS specific files +.DS_Store diff --git a/nemo/src/rule_model/components/rule.rs b/nemo/src/rule_model/components/rule.rs index 2980bb1ee..e9859878d 100644 --- a/nemo/src/rule_model/components/rule.rs +++ b/nemo/src/rule_model/components/rule.rs @@ -174,12 +174,8 @@ impl Rule { /// Return an iterator over the variables bound in positive body atoms. pub fn positive_variables(&self) -> impl Iterator { self.body_positive().flat_map(|atom| { - atom.terms() - .filter_map(|term| match term { - Term::Primitive(Primitive::Variable(variable)) => Some(variable), - _ => None, - }) - .filter(|variable| variable.is_universal() && variable.name().is_some()) + atom.universal_variables() + .filter(|var| var.name().is_some()) }) } From b2749bd6d02f1710e3015e8e2e96f5fa2de3f69a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Louis=20Gr=C3=B6ger?= Date: Wed, 7 Oct 2026 15:16:00 +0200 Subject: [PATCH 11/13] rule.predicates_ref() does now return an iterator over &Tag --- nemo/src/rule_model/components/rule.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/nemo/src/rule_model/components/rule.rs b/nemo/src/rule_model/components/rule.rs index e9859878d..dc9d6d83a 100644 --- a/nemo/src/rule_model/components/rule.rs +++ b/nemo/src/rule_model/components/rule.rs @@ -195,12 +195,11 @@ impl Rule { } /// Return references to the predicates of all atoms in this rule. - pub fn predicates_ref(&self) -> Vec<&Tag> { + pub fn predicates_ref(&self) -> impl Iterator { self.body .iter() .filter_map(Literal::predicate_ref) .chain(self.head.iter().map(Atom::predicate_ref)) - .collect() } /// Return an iterator over all [ImportLiteral]s From 80992bce67e62c70b695d8a6638adbe179f684dd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Louis=20Gr=C3=B6ger?= Date: Wed, 7 Oct 2026 15:20:00 +0200 Subject: [PATCH 12/13] rework of rule.universal_head_variables() by using atom.universal_variables() --- nemo/src/rule_model/components/rule.rs | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/nemo/src/rule_model/components/rule.rs b/nemo/src/rule_model/components/rule.rs index dc9d6d83a..05d01fa47 100644 --- a/nemo/src/rule_model/components/rule.rs +++ b/nemo/src/rule_model/components/rule.rs @@ -228,10 +228,7 @@ impl Rule { /// Return an iterator over all universal variables in the head of this rule. fn universal_head_variables(&self) -> impl Iterator { - self.head - .iter() - .flat_map(|atom| atom.variables()) - .filter(|variable| variable.is_universal()) + self.head.iter().flat_map(|atom| atom.universal_variables()) } /// Return an iterator over the variables bound by import statements. From efa774466df29573c049ed3ac17b7bed9f8b4db6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Louis=20Gr=C3=B6ger?= Date: Thu, 8 Oct 2026 15:36:29 +0200 Subject: [PATCH 13/13] removed transformations: msa, filter_rules and crit_instance from nemo as they are only used for nemo-static-checks --- .../rule_model/pipeline/transformations.rs | 3 - .../pipeline/transformations/crit_instance.rs | 92 ----------- .../pipeline/transformations/filter_rules.rs | 50 ------ .../pipeline/transformations/msa.rs | 148 ------------------ 4 files changed, 293 deletions(-) delete mode 100644 nemo/src/rule_model/pipeline/transformations/crit_instance.rs delete mode 100644 nemo/src/rule_model/pipeline/transformations/filter_rules.rs delete mode 100644 nemo/src/rule_model/pipeline/transformations/msa.rs diff --git a/nemo/src/rule_model/pipeline/transformations.rs b/nemo/src/rule_model/pipeline/transformations.rs index 91c06218c..912b140d3 100644 --- a/nemo/src/rule_model/pipeline/transformations.rs +++ b/nemo/src/rule_model/pipeline/transformations.rs @@ -1,16 +1,13 @@ //! This module defines [ProgramTransformation]s. pub mod active; -pub mod crit_instance; pub mod default; pub mod empty; pub mod exports; pub mod filter_imports; -pub mod filter_rules; pub mod global; pub mod incremental; pub mod merge_sparql; -pub mod msa; pub mod normalize; pub mod set_default_outputs; pub mod skolem; diff --git a/nemo/src/rule_model/pipeline/transformations/crit_instance.rs b/nemo/src/rule_model/pipeline/transformations/crit_instance.rs deleted file mode 100644 index 9c01e4c1a..000000000 --- a/nemo/src/rule_model/pipeline/transformations/crit_instance.rs +++ /dev/null @@ -1,92 +0,0 @@ -//! This module defines [TransformationCriticalInstance]. - -use std::collections::HashSet; - -use itertools::Itertools; - -use super::ProgramTransformation; -use crate::rule_model::{ - components::{ - IterablePrimitives, fact::Fact, literal::Literal, rule::Rule, statement::Statement, - tag::Tag, term::Term, - }, - error::ValidationReport, - programs::{ProgramRead, ProgramWrite, handle::ProgramHandle}, -}; - -/// Program transformation that replaces a program's facts with its critical instance. -#[derive(Debug, Default, Clone, Copy)] -pub struct TransformationCriticalInstance; - -fn predicates_and_arities(rule: &Rule) -> impl Iterator { - rule.body() - .iter() - .filter_map(|literal| match literal { - Literal::Positive(atom) | Literal::Negative(atom) => Some(atom), - Literal::Operation(_) => None, - }) - .chain(rule.head()) - .map(|atom| (atom.predicate_ref(), atom.len())) -} - -/// Return predicate and arity pairs for all atoms in the provided rules. -pub fn preds_and_lens_of_rules<'a>(rules: &[&'a Rule]) -> impl Iterator { - rules.iter().flat_map(|rule| predicates_and_arities(rule)) -} - -/// Return every fact for the given predicate and arity that can be formed -/// from the provided constants. -pub fn facts_for_predicate_and_constants( - predicate: &Tag, - arity: usize, - constants: &[Term], -) -> HashSet { - (0..arity) - .map(|_| constants.iter().cloned()) - .multi_cartesian_product() - .map(|terms| Fact::new(predicate.clone(), terms)) - .collect() -} - -fn critical_instance(rules: &[&Rule]) -> impl Iterator { - let mut constants = rules - .iter() - .flat_map(|rule| rule.primitive_terms()) - .filter(|primitive| primitive.is_ground()) - .cloned() - .map(Term::from) - .collect::>(); - constants.push(Term::from("__STAR__")); - - let predicates_and_arities = preds_and_lens_of_rules(rules).collect::>(); - - predicates_and_arities - .into_iter() - .flat_map(move |(predicate, arity)| { - facts_for_predicate_and_constants(predicate, arity, &constants) - }) -} - -impl ProgramTransformation for TransformationCriticalInstance { - fn apply(self, program: &ProgramHandle) -> Result { - let mut commit = program.fork(); - - let rules = program - .statements() - .filter_map(|statement| { - if let Statement::Rule(rule) = statement { - commit.keep(statement); - Some(rule) - } else { - None - } - }) - .collect::>(); - - for fact in critical_instance(&rules) { - commit.add_fact(fact); - } - - commit.submit() - } -} diff --git a/nemo/src/rule_model/pipeline/transformations/filter_rules.rs b/nemo/src/rule_model/pipeline/transformations/filter_rules.rs deleted file mode 100644 index edc17e0fc..000000000 --- a/nemo/src/rule_model/pipeline/transformations/filter_rules.rs +++ /dev/null @@ -1,50 +0,0 @@ -//! This module defines [TransformationFilterRules]. - -use super::ProgramTransformation; -use crate::rule_model::{ - components::statement::Statement, - error::ValidationReport, - programs::{ProgramRead, handle::ProgramHandle}, -}; - -/// Program transformation that retains rules selected by a [RuleSelector]. -#[derive(Debug, Clone, Copy)] -pub struct TransformationFilterRules(pub RuleSelector); - -impl TransformationFilterRules { - fn matches(&self, statement: &Statement) -> bool { - let Statement::Rule(rule) = statement else { - return false; - }; - - let is_existential = rule.existential_variables().next().is_some(); - match self.0 { - RuleSelector::Existential => is_existential, - RuleSelector::NonExistential => !is_existential, - } - } -} - -/// Selects rules based on whether they contain existential variables. -#[derive(Debug, Clone, Copy)] -pub enum RuleSelector { - /// Select rules containing at least one existential variable. - Existential, - /// Select rules containing no existential variables. - NonExistential, -} - -impl ProgramTransformation for TransformationFilterRules { - fn apply(self, program: &ProgramHandle) -> Result { - let mut commit = program.fork(); - - for statement in program - .statements() - .filter(|statement| self.matches(statement)) - { - commit.keep(statement); - } - - commit.submit() - } -} diff --git a/nemo/src/rule_model/pipeline/transformations/msa.rs b/nemo/src/rule_model/pipeline/transformations/msa.rs deleted file mode 100644 index cb7de5f14..000000000 --- a/nemo/src/rule_model/pipeline/transformations/msa.rs +++ /dev/null @@ -1,148 +0,0 @@ -//! This module defines [TransformationMSA]. - -use std::collections::HashSet; - -use super::ProgramTransformation; -use crate::rule_model::{ - components::{ - atom::Atom, - literal::Literal, - rule::Rule, - statement::Statement, - tag::Tag, - term::{ - Term, - primitive::{Primitive, variable::Variable}, - }, - }, - error::ValidationReport, - pipeline::commit::ProgramCommit, - programs::{ProgramRead, ProgramWrite, handle::ProgramHandle}, - substitution::Substitution, -}; - -/// Program transformation used to reduce model-summarizing acyclicity to fact entailment. -#[derive(Debug, Default, Clone, Copy)] -pub struct TransformationMSA; - -fn function_predicates(existential_variables: &[&Variable], rule_index: usize) -> Vec { - existential_variables - .iter() - .enumerate() - .map(|(variable_index, _)| Tag::new(format!("_msa_F_{rule_index}_{variable_index}"))) - .collect() -} - -fn modified_msa_rule( - rule: &Rule, - rule_index: usize, - s_predicate: &Tag, - existential_variables: &[&Variable], -) -> (Rule, Vec) { - let mut result = rule.clone(); - let function_predicates = function_predicates(existential_variables, rule_index); - let frontier_variables = rule.frontier_variables().collect::>(); - - for (function_predicate, existential_variable) in - function_predicates.iter().zip(existential_variables.iter()) - { - let existential_term = Term::from((*existential_variable).clone()); - result.head_mut().push(Atom::new( - function_predicate.clone(), - [existential_term.clone()], - )); - - for frontier_variable in &frontier_variables { - result.head_mut().push(Atom::new( - s_predicate.clone(), - [ - Term::from((*frontier_variable).clone()), - existential_term.clone(), - ], - )); - } - } - - let mut substitution = Substitution::default(); - for (variable_index, variable) in existential_variables.iter().enumerate() { - substitution.insert( - Primitive::from((*variable).clone()), - Term::from(format!("_msa_c_{rule_index}_{variable_index}")), - ); - } - substitution.apply(&mut result); - - (result, function_predicates) -} - -fn generic_rules(s_predicate: &Tag, d_predicate: &Tag, x1: &Term, x2: &Term) -> [Rule; 2] { - let x3 = Term::from(Variable::universal("_msa_x3")); - - let s_x1_x2 = Literal::Positive(Atom::new(s_predicate.clone(), [x1.clone(), x2.clone()])); - let s_x2_x3 = Literal::Positive(Atom::new(s_predicate.clone(), [x2.clone(), x3.clone()])); - let d_x1_x2 = Atom::new(d_predicate.clone(), [x1.clone(), x2.clone()]); - let d_x1_x3 = Atom::new(d_predicate.clone(), [x1.clone(), x3]); - - [ - Rule::new([d_x1_x2.clone()].into(), [s_x1_x2].into()), - Rule::new( - [d_x1_x3].into(), - [Literal::Positive(d_x1_x2), s_x2_x3].into(), - ), - ] -} - -fn function_rules( - function_predicates: &[Tag], - d_predicate: &Tag, - x1: &Term, - x2: &Term, -) -> impl Iterator { - let c_atom = Atom::new(Tag::from("_msa_C"), [Term::from("nullaryPredsNotAllowed")]); - - function_predicates.iter().map(move |function_predicate| { - let f_x1 = Literal::Positive(Atom::new(function_predicate.clone(), [x1.clone()])); - let f_x2 = Literal::Positive(Atom::new(function_predicate.clone(), [x2.clone()])); - let d_x1_x2 = Literal::Positive(Atom::new(d_predicate.clone(), [x1.clone(), x2.clone()])); - - Rule::new([c_atom.clone()].into(), [f_x1, d_x1_x2, f_x2].into()) - }) -} - -impl ProgramTransformation for TransformationMSA { - fn apply(self, program: &ProgramHandle) -> Result { - let mut commit: ProgramCommit = program.fork(); - - let s_predicate = Tag::from("_msa_S"); - let d_predicate = Tag::from("_msa_D"); - let x1 = Term::from(Variable::universal("_msa_x1")); - let x2 = Term::from(Variable::universal("_msa_x2")); - - for rule in generic_rules(&s_predicate, &d_predicate, &x1, &x2) { - commit.add_rule(rule); - } - - for (rule_index, statement) in program.statements().enumerate() { - let Statement::Rule(rule) = statement else { - commit.keep(statement); - continue; - }; - - let existential_variables = rule.existential_variables().collect::>(); - if existential_variables.is_empty() { - commit.keep(statement); - continue; - } - - let (modified_rule, function_predicates) = - modified_msa_rule(rule, rule_index, &s_predicate, &existential_variables); - commit.add_rule(modified_rule); - - for rule in function_rules(&function_predicates, &d_predicate, &x1, &x2) { - commit.add_rule(rule); - } - } - - commit.submit() - } -}