From 21f66d9409808edc99595c018472334b8501cac4 Mon Sep 17 00:00:00 2001 From: Martin Berg Alstad Date: Tue, 25 Jun 2024 19:57:23 +0200 Subject: [PATCH] Fixed bug surrounding implies with parentheses when unnecessary. Fixed correct saving of operation in elimination of implication. Must use macro on helpers --- src/expressions/expression.rs | 2 +- src/expressions/helpers.rs | 6 +++++ src/expressions/simplify.rs | 42 ++++++++++++++++++++++------------ src/expressions/truth_table.rs | 2 +- 4 files changed, 35 insertions(+), 17 deletions(-) diff --git a/src/expressions/expression.rs b/src/expressions/expression.rs index 63692f8..ef8ec57 100644 --- a/src/expressions/expression.rs +++ b/src/expressions/expression.rs @@ -93,7 +93,7 @@ impl Display for Expression { format!("{} ⋀ {}", fmt_helper(left, Some(expression)), fmt_helper(right, Some(expression))) } Expression::Binary { left, operator: BinaryOperator::Or, right } => { - if parent.is_none() || matches!(parent, Some(Expression::Binary { operator: BinaryOperator::Or, .. })) { + if parent.is_none() || matches!(parent, Some(Expression::Binary { operator: BinaryOperator::Or | BinaryOperator::Implication, .. })) { format!("{} ⋁ {}", fmt_helper(left, Some(expression)), fmt_helper(right, Some(expression))) } else { format!("({} ⋁ {})", fmt_helper(left, Some(expression)), fmt_helper(right, Some(expression))) diff --git a/src/expressions/helpers.rs b/src/expressions/helpers.rs index 2af5533..1aaa6e3 100644 --- a/src/expressions/helpers.rs +++ b/src/expressions/helpers.rs @@ -3,6 +3,7 @@ use crate::expressions::expression::Expression; use crate::expressions::operator::BinaryOperator; #[inline] +#[must_use] pub fn and(left: L, right: R) -> Expression where L: Into>, @@ -12,6 +13,7 @@ where } #[inline] +#[must_use] pub fn or(left: L, right: R) -> Expression where L: Into>, @@ -21,6 +23,7 @@ where } #[inline] +#[must_use] pub fn implies(left: L, right: R) -> Expression where L: Into>, @@ -30,6 +33,7 @@ where } #[inline] +#[must_use] pub fn binary(left: L, operator: BinaryOperator, right: R) -> Expression where L: Into>, @@ -39,11 +43,13 @@ where } #[inline] +#[must_use] pub fn not>>(value: T) -> Expression { Expression::Not(value.into()) } #[inline] +#[must_use] pub fn atomic>(value: T) -> Expression { Expression::Atomic(value.into()) } diff --git a/src/expressions/simplify.rs b/src/expressions/simplify.rs index 7420161..2460041 100644 --- a/src/expressions/simplify.rs +++ b/src/expressions/simplify.rs @@ -10,6 +10,7 @@ use crate::routing::response::Operation; #[derive(Debug, PartialEq, Serialize)] #[serde(rename_all = "SCREAMING_SNAKE_CASE")] +#[allow(clippy::enum_variant_names)] pub enum Law { EliminationOfImplication, DeMorgansLaws, @@ -86,24 +87,27 @@ impl Expression { /// Eliminate the implication operator from the expression. /// This is done by replacing `a ➔ b` with `¬a ⋁ b`. fn elimination_of_implication(&self, operations: &mut Vec) -> Self { - let result = match self { - Expression::Not(expr) => not(expr.elimination_of_implication(operations)), + match self { + Expression::Not(expr) => { + not(expr.elimination_of_implication(operations)) + } Expression::Binary { left, operator, right } => { let l_result = left.elimination_of_implication(operations); let r_result = right.elimination_of_implication(operations); + let before = binary(l_result.clone(), *operator, r_result.clone()); if let BinaryOperator::Implication = *operator { - or(not(l_result), r_result) + let after = or(not(l_result.clone()), r_result.clone()); + if let Some(operation) = Operation::new(&before, &after, Law::EliminationOfImplication) { + operations.push(operation); + } + after } else { - binary(l_result, *operator, r_result) + before } } atomic @ Expression::Atomic(_) => atomic.clone(), - }; - if let Some(operation) = Operation::new(self, &result, Law::EliminationOfImplication) { - operations.push(operation); } - result } /// Eliminate double negations from the expression. @@ -112,10 +116,16 @@ impl Expression { fn double_negation_elimination(&self, operations: &mut Vec) -> Self { let result = match self { Expression::Not(expr) => { + let before = not(expr.double_negation_elimination(operations)); if let Expression::Not(inner) = expr.deref() { - inner.double_negation_elimination(operations) + let after = inner.double_negation_elimination(operations); + dbg!(before.to_string(), after.to_string()); + if let Some(operation) = Operation::new(&before, &after, Law::DoubleNegationElimination) { + operations.push(operation); + } + after } else { - not(expr.double_negation_elimination(operations)) + before } } Expression::Binary { left, operator, right } => { @@ -125,9 +135,9 @@ impl Expression { } atomic @ Expression::Atomic(_) => atomic.clone(), }; - if let Some(operation) = Operation::new(self, &result, Law::DoubleNegationElimination) { - operations.push(operation); - } + // if let Some(operation) = Operation::new(self, &result, Law::DoubleNegationElimination) { + // operations.push(operation); + // } result } @@ -285,7 +295,7 @@ mod tests { assert_eq!(operations[0].before, "b ➔ c"); assert_eq!(operations[0].after, "¬b ⋁ c"); assert_eq!(operations[1].law, Law::EliminationOfImplication); - assert_eq!(operations[1].before, "a ➔ b ➔ c"); + assert_eq!(operations[1].before, "a ➔ ¬b ⋁ c"); assert_eq!(operations[1].after, "¬a ⋁ ¬b ⋁ c"); } @@ -294,6 +304,7 @@ mod tests { let mut operations = vec![]; let expression = and(atomic("a"), atomic("b")).elimination_of_implication(&mut operations); assert_eq!(expression, and(atomic("a"), atomic("b"))); + assert_eq!(operations.len(), 0); } #[test] @@ -301,6 +312,7 @@ mod tests { let mut operations = vec![]; let expression = or(atomic("a"), and(atomic("b"), atomic("c"))).elimination_of_implication(&mut operations); assert_eq!(expression, or(atomic("a"), and(atomic("b"), atomic("c")))); + assert_eq!(operations.len(), 0); } #[test] @@ -336,7 +348,7 @@ mod tests { assert_eq!(operations[0].after, "¬a"); assert_eq!(operations[1].law, Law::DoubleNegationElimination); assert_eq!(operations[1].before, "¬¬¬¬¬a"); - assert_eq!(operations[1].after, "¬a"); + assert_eq!(operations[1].after, "¬¬¬a"); } #[test] diff --git a/src/expressions/truth_table.rs b/src/expressions/truth_table.rs index 4c09a6a..74e3afc 100644 --- a/src/expressions/truth_table.rs +++ b/src/expressions/truth_table.rs @@ -501,7 +501,7 @@ mod tests { fn test_complex_expression() { let expression = implies(and(atomic("A"), atomic("B")), or(atomic("C"), atomic("D"))); let header = TruthTable::extract_header(&expression); - assert_eq!(header, vec!["A", "B", "A ⋀ B", "C", "D", "C ⋁ D", "A ⋀ B ➔ (C ⋁ D)"]); + assert_eq!(header, vec!["A", "B", "A ⋀ B", "C", "D", "C ⋁ D", "A ⋀ B ➔ C ⋁ D"]); } #[test]