Rule Set Classification

nemo/Cargo.toml

@@ -54,6 +54,8 @@ bytecount = "0.6.8"
 colored = "2"
 
 [dev-dependencies]
+assert_cmd = "2.0"
+dir-test = "0.2.1"
 env_logger = "*"
 assert_fs = "1.0"
 test-log = "0.2"

nemo/src/lib.rs

@@ -32,6 +32,8 @@ pub mod execution;
 pub mod rule_model;
 pub mod util;
 
+pub mod static_checks;
+
 pub mod chase_model; // TODO: Make private
 pub(crate) mod table_manager;
 

nemo/src/rule_model/components/atom.rs

@@ -80,6 +80,10 @@ impl Atom {
         self.predicate.clone()
     }
 
+    pub fn predicate_ref(&self) -> &Tag {
+        &self.predicate
+    }
+
     /// Return an iterator over the arguments of this atom.
     pub fn arguments(&self) -> impl Iterator<Item = &Term> {
         self.terms.iter()

nemo/src/rule_model/components/rule.rs

@@ -147,6 +147,24 @@ impl Rule {
         result
     }
 
+    pub fn positive_variables_as_vec(&self) -> Vec<&Variable> {
+        let mut result = Vec::new();
+
+        for literal in &self.body {
+            if let Literal::Positive(atom) = literal {
+                for term in atom.arguments() {
+                    if let Term::Primitive(Primitive::Variable(variable)) = term {
+                        if variable.is_universal() && variable.name().is_some() {
+                            result.push(variable);
+                        }
+                    }
+                }
+            }
+        }
+
+        result
+    }
+
     /// Return a set of "safe" variables.
     ///
     /// A variable is considered safe,

nemo/src/rule_model/components/tag.rs

@@ -5,7 +5,7 @@ use std::{fmt::Display, hash::Hash};
 use crate::rule_model::origin::Origin;
 
 /// Name of a term or predicate
-#[derive(Debug, Clone, Eq)]
+#[derive(Clone, Debug, Eq)]
 pub struct Tag {
     /// Origin of this component.
     origin: Origin,
@@ -53,6 +53,12 @@ impl Display for Tag {
     }
 }
 
+impl Ord for Tag {
+    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
+        self.tag.cmp(&other.tag)
+    }
+}
+
 impl PartialEq for Tag {
     fn eq(&self, other: &Self) -> bool {
         self.tag == other.tag
@@ -61,7 +67,7 @@ impl PartialEq for Tag {
 
 impl PartialOrd for Tag {
     fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
-        self.tag.partial_cmp(&other.tag)
+        Some(self.tag.cmp(&other.tag))
     }
 }
 

nemo/src/rule_model/components/term/primitive/variable.rs

@@ -40,7 +40,7 @@ impl Display for VariableName {
 ///
 /// 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

@@ -56,7 +56,13 @@ impl PartialEq for ExistentialVariable {
 
 impl PartialOrd for ExistentialVariable {
     fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
-        self.name.partial_cmp(&other.name)
+        Some(self.cmp(other))
+    }
+}
+
+impl Ord for ExistentialVariable {
+    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
+        self.name.cmp(&other.name)
     }
 }
 

nemo/src/rule_model/components/term/primitive/variable/universal.rs

@@ -79,7 +79,13 @@ impl PartialEq for UniversalVariable {
 
 impl PartialOrd for UniversalVariable {
     fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
-        self.name.partial_cmp(&other.name)
+        Some(self.cmp(other))
+    }
+}
+
+impl Ord for UniversalVariable {
+    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
+        self.name.cmp(&other.name)
     }
 }
 

nemo/src/rule_model/origin.rs

@@ -5,7 +5,7 @@ use std::hash::Hash;
 pub(crate) type ExternalReference = usize;
 
 /// Origin of a program component
-#[derive(Debug, Copy, Clone, Eq, PartialEq, Hash)]
+#[derive(Debug, Copy, Clone, Eq, PartialEq, Hash, Ord, PartialOrd)]
 pub enum Origin {
     /// Component was created via a constructor
     Created,

nemo/src/static_checks.rs

@@ -0,0 +1,8 @@
+//! Functionality to give static checks for a RuleSet.
+pub mod acyclicity_graph_constructor;
+pub mod acyclicity_graphs;
+pub mod collection_traits;
+pub mod positions;
+pub mod rule_properties;
+pub mod rule_set;
+pub mod rules_properties;

nemo/src/static_checks/acyclicity_graph_constructor.rs

@@ -0,0 +1,25 @@
+//! Functionality that provides methods to build the (JointAcyclicityGraph / WeakAcyclicityGraph) of a
+/// RuleSet.
+use crate::static_checks::acyclicity_graphs::{
+    AcyclicityGraphBuilder, JointAcyclicityGraph, WeakAcyclicityGraph,
+};
+use crate::static_checks::rule_set::RuleSet;
+
+/// This Trait provides methods of some RuleSet to build the (WeakAcyclicityGraph /
+/// JointAcyclicityGraph).
+pub trait AcyclicityGraphConstructor<'a> {
+    /// Builds the JointAcyclicityGraph.
+    fn joint_acyclicity_graph(&'a self) -> JointAcyclicityGraph<'a>;
+    /// Builds the WeakAcyclicityGraph.
+    fn weak_acyclicity_graph(&'a self) -> WeakAcyclicityGraph<'a>;
+}
+
+impl<'a> AcyclicityGraphConstructor<'a> for RuleSet {
+    fn joint_acyclicity_graph(&'a self) -> JointAcyclicityGraph<'a> {
+        JointAcyclicityGraph::build_graph(self)
+    }
+
+    fn weak_acyclicity_graph(&'a self) -> WeakAcyclicityGraph<'a> {
+        WeakAcyclicityGraph::build_graph(self)
+    }
+}