Add error message for filtered derived variables (#458)

* Add error message for filtered derived variables * Extend calculation of safe variables --------- Co-authored-by: Alex Ivliev <[email protected]>
knowsys · Apr 2, 2024 · c0515cb · c0515cb
1 parent 7d44277
commit c0515cb
Show file tree

Hide file tree

Showing 2 changed files with 59 additions and 9 deletions.
diff --git a/nemo/src/io/parser/types.rs b/nemo/src/io/parser/types.rs
@@ -149,8 +149,11 @@ pub enum ParseError {
     /// The variable must only depend on variables that occur in a positive body literal.
     #[error(r#"the variable "{0}" must only depend on variables that occur in a positive body literals"#)]
     UnsafeDefinition(Variable),
-    /// Complex term uses an undefined variable.
-    #[error(r#"complex term "{0}" uses an undefined variable "{1}""#)]
+    /// Complex term uses a derived variable.
+    #[error(r#"complex term "{0}" uses a derived variable "{1}""#)]
+    ComplexTermDerived(String, Variable),
+    /// Complex term uses an unsafe variable.
+    #[error(r#"complex term "{0}" uses an unsafe variable "{1}""#)]
     UnsafeComplexTerm(String, Variable),
     /// Variable has been defined multiple times.
     #[error(r#"the variable "{0}" has been used in multiple equalities"#)]

diff --git a/nemo/src/model/rule_model/rule.rs b/nemo/src/model/rule_model/rule.rs
@@ -61,8 +61,13 @@ impl Rule {
             .cloned()
             .partition(|literal| literal.is_positive());
 
-        // Safe variables are considered to be all variables occuring as primitive terms in a positive body literal
-        let safe_variables = Self::safe_variables_literals(&positive);
+        // Safe variables are considered to be
+        // all variables occuring as primitive terms in a positive body literal
+        // or every value that is equal to such a variable
+        let safe_variables = Self::safe_variables_constraints(
+            Self::safe_variables_literals(&positive),
+            &constraints,
+        );
 
         // A derived variable is a variable which is defined in terms of bound variables
         // using a simple equality operation
@@ -110,7 +115,7 @@ impl Rule {
             }
         }
 
-        // Every constraint that is not an assignment must only use derived or safe varaibles
+        // Every constraint that is not an assignment must only use safe varaibles
         for constraint in &constraints {
             if let Some((variable, _)) = constraint.has_form_assignment() {
                 if derived_variables.contains(variable) {
@@ -120,9 +125,16 @@ impl Rule {
 
             for term in [constraint.left(), constraint.right()] {
                 for variable in term.variables() {
-                    if !safe_variables.contains(variable) && !derived_variables.contains(variable) {
+                    if derived_variables.contains(variable) {
+                        return Err(ParseError::ComplexTermDerived(
+                            constraint.to_string(),
+                            variable.clone(),
+                        ));
+                    }
+
+                    if !safe_variables.contains(variable) {
                         return Err(ParseError::UnsafeComplexTerm(
-                            term.to_string(),
+                            constraint.to_string(),
                             variable.clone(),
                         ));
                     }
@@ -201,10 +213,45 @@ impl Rule {
         result
     }
 
+    /// Propagates the safety property to variables that are equal to other safe variables.
+    fn safe_variables_constraints(
+        mut safe_variables: HashSet<Variable>,
+        constraints: &[Constraint],
+    ) -> HashSet<Variable> {
+        let mut changed = true;
+
+        while changed {
+            changed = false;
+
+            for constraint in constraints {
+                if let (
+                    Term::Primitive(PrimitiveTerm::Variable(variable_left)),
+                    Term::Primitive(PrimitiveTerm::Variable(variable_right)),
+                ) = constraint.terms()
+                {
+                    if safe_variables.contains(variable_left)
+                        ^ safe_variables.contains(variable_right)
+                    {
+                        safe_variables.insert(variable_left.clone());
+                        safe_variables.insert(variable_right.clone());
+
+                        changed = true;
+                    }
+                }
+            }
+        }
+
+        safe_variables
+    }
+
     /// Return all variables that are "safe".
-    /// A variable is safe if it occurs in a positive body literal.
+    /// A variable is safe if it occurs in a positive body literal,
+    /// or is equal to such a value.
     pub fn safe_variables(&self) -> HashSet<Variable> {
-        Self::safe_variables_literals(&self.body)
+        Self::safe_variables_constraints(
+            Self::safe_variables_literals(&self.body),
+            self.constraints(),
+        )
     }
 
     /// Return the head atoms of the rule - immutable.