From a7766d248c52a468f50144b505986091e7627ed7 Mon Sep 17 00:00:00 2001
From: Alex Ivliev <Alex.Ivliev@mailbox.tu-dresden.de>
Date: Wed, 3 Apr 2024 17:09:36 +0200
Subject: [PATCH] Throw error message if negated literal uses derived variable
 or complex term (#461)

---
 nemo/src/io/parser/types.rs       |  6 ++++
 nemo/src/model/rule_model/rule.rs | 57 ++++++++++++++++++++++++-------
 2 files changed, 51 insertions(+), 12 deletions(-)

diff --git a/nemo/src/io/parser/types.rs b/nemo/src/io/parser/types.rs
index fa9d6c04b..0f490d213 100644
--- a/nemo/src/io/parser/types.rs
+++ b/nemo/src/io/parser/types.rs
@@ -149,6 +149,12 @@ 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),
+    /// Negated literal uses a complex term.
+    #[error(r#"negated literal "{0}" uses the complex term "{1}""#)]
+    NegatedLiteralComplex(String, String),
+    /// Negated literal uses a derived variable.
+    #[error(r#"negated literal "{0}" uses a derived variable "{1}""#)]
+    NegatedLiteralDerived(String, Variable),
     /// Complex term uses a derived variable.
     #[error(r#"complex term "{0}" uses a derived variable "{1}""#)]
     ComplexTermDerived(String, Variable),
diff --git a/nemo/src/model/rule_model/rule.rs b/nemo/src/model/rule_model/rule.rs
index a94b2b3e8..f3eeb07d3 100644
--- a/nemo/src/model/rule_model/rule.rs
+++ b/nemo/src/model/rule_model/rule.rs
@@ -161,19 +161,52 @@ impl Rule {
         for negative_literal in negative {
             let mut current_unsafe = HashSet::<Variable>::new();
 
-            for primitive_term in negative_literal.primitive_terms() {
-                if let PrimitiveTerm::Variable(variable) = primitive_term {
-                    if derived_variables.contains(&variable) || safe_variables.contains(variable) {
-                        continue;
+            for negative_term in negative_literal.terms() {
+                if let Term::Primitive(primitive_term) = negative_term {
+                    if let PrimitiveTerm::Variable(variable) = primitive_term {
+                        if safe_variables.contains(variable) {
+                            continue;
+                        }
+
+                        if derived_variables.contains(variable) {
+                            return Err(ParseError::NegatedLiteralDerived(
+                                negative_literal.to_string(),
+                                variable.clone(),
+                            ));
+                        }
+
+                        if unsafe_negative_variables.contains(variable) {
+                            return Err(ParseError::UnsafeVariableInMultipleNegativeLiterals(
+                                variable.clone(),
+                            ));
+                        }
+                        if let PrimitiveTerm::Variable(variable) = primitive_term {
+                            if safe_variables.contains(variable) {
+                                continue;
+                            }
+
+                            if derived_variables.contains(variable) {
+                                return Err(ParseError::NegatedLiteralDerived(
+                                    negative_literal.to_string(),
+                                    variable.clone(),
+                                ));
+                            }
+
+                            if unsafe_negative_variables.contains(variable) {
+                                return Err(ParseError::UnsafeVariableInMultipleNegativeLiterals(
+                                    variable.clone(),
+                                ));
+                            }
+
+                            current_unsafe.insert(variable.clone());
+                        }
+                        current_unsafe.insert(variable.clone());
                     }
-
-                    if unsafe_negative_variables.contains(variable) {
-                        return Err(ParseError::UnsafeVariableInMultipleNegativeLiterals(
-                            variable.clone(),
-                        ));
-                    }
-
-                    current_unsafe.insert(variable.clone());
+                } else {
+                    return Err(ParseError::NegatedLiteralComplex(
+                        negative_literal.to_string(),
+                        negative_term.to_string(),
+                    ));
                 }
             }