Feature/nemo changes for static checks

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),

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<Item = &Term> {
         self.terms.iter()
@@ -116,6 +121,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<Item = &Variable> {
+        self.variables().filter(|variable| variable.is_universal())
+    }
 }
 
 impl Index<usize> for Atom {

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 {

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},
@@ -164,6 +165,24 @@ impl Rule {
         &mut self.head
     }
 
+    /// Return an iterator over all existential variables in this rule.
+    pub fn existential_variables(&self) -> impl Iterator<Item = &Variable> {
+        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<Item = &Variable> {
+        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<Item = &Atom> {
@@ -179,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<Item = &ImportLiteral> {
@@ -196,32 +224,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<Item = &Variable> {
+        let positive_variables = self.positive_variables().collect::<HashSet<_>>();
+        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<Item = &Variable> {
+        self.head
             .iter()
-            .flat_map(|import| import.variables())
-            .collect::<HashSet<_>>()
+            .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<Item = &Variable> {
+        self.imports.iter().flat_map(|import| import.variables())
     }
 
     /// Return a set of "safe" variables.
@@ -233,8 +253,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::<HashSet<_>>();
 
         loop {

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<std::cmp::Ordering> {
-        self.tag.partial_cmp(&other.tag)
+        Some(self.cmp(other))
     }
 }
 

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<Terms: IntoIterator<Item = Term>>(tag: Tag, subterms: Terms) -> Self {
+    pub fn new_tagged<Terms: IntoIterator<Item = Term>>(tag: Tag, subterms: Terms) -> Self {
         Self {
             origin: Origin::default(),
             id: ProgramComponentId::default(),

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),

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<std::cmp::Ordering> {
-        self.name.partial_cmp(&other.name)
+        Some(self.cmp(other))
     }
 }
 

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<std::cmp::Ordering> {
-        self.name.partial_cmp(&other.name)
+        Some(self.cmp(other))
     }
 }
 

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<std::cmp::Ordering> {
-        self.name.partial_cmp(&other.name)
+        Some(self.cmp(other))
     }
 }
 

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),

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),
 

nemo/src/rule_model/pipeline/transformations.rs

@@ -1,13 +1,16 @@
 //! 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;

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<Item = (&Tag, usize)> {
+    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<Item = (&'a Tag, usize)> {
+    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<Fact> {
+    (0..arity)
+        .map(|_| constants.iter().cloned())
+        .multi_cartesian_product()
+        .map(|terms| Fact::new(predicate.clone(), terms))
+        .collect()
+}
+
+fn critical_instance(rules: &[&Rule]) -> impl Iterator<Item = Fact> {
+    let mut constants = rules
+        .iter()
+        .flat_map(|rule| rule.primitive_terms())
+        .filter(|primitive| primitive.is_ground())
+        .cloned()
+        .map(Term::from)
+        .collect::<Vec<_>>();
+    constants.push(Term::from("__STAR__"));
+
+    let predicates_and_arities = preds_and_lens_of_rules(rules).collect::<HashSet<_>>();
+
+    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<ProgramHandle, ValidationReport> {
+        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::<Vec<_>>();
+
+        for fact in critical_instance(&rules) {
+            commit.add_fact(fact);
+        }
+
+        commit.submit()
+    }
+}