From abad6181cb583baa6f678249bbfc276187a313b3 Mon Sep 17 00:00:00 2001
From: Martin Berg Alstad <600878@stud.hvl.no>
Date: Sun, 14 Jul 2024 19:08:58 +0200
Subject: [PATCH] format with rustfmt

---
 src/expressions/simplify.rs | 554 ++++++++++++++++++++++++++----------
 1 file changed, 399 insertions(+), 155 deletions(-)

diff --git a/src/expressions/simplify.rs b/src/expressions/simplify.rs
index e8961f0..d09eae9 100644
--- a/src/expressions/simplify.rs
+++ b/src/expressions/simplify.rs
@@ -24,91 +24,171 @@ pub enum Law {
 // TODO refactor
 #[macro_export]
 macro_rules! absorption_law_opposites {
-    ($left:expr, $right:expr, $operations:expr, $this_op:pat, $op:pat, $func:expr, $ignore_case:expr) => {
-        {
-            let before = $func($left.clone(), $right.clone());
-            match ($left.as_ref(), $right.as_ref()) {
-                (_, Expression::Binary { left: right_left, operator: $op, right: right_right }) => {
-                    let result = evaluate_equals_or_opposites($left.as_ref(), right_left, right_right, $func, $ignore_case, $operations).unwrap_or(
-                        $func($left.absorption_law($operations, $ignore_case), $right.absorption_law($operations, $ignore_case))
-                    );
-                    if let Some(operation) = Operation::new(&before, &result, Law::AbsorptionLaw) {
-                        $operations.push(operation);
-                    }
-                    result
+    ($left:expr, $right:expr, $operations:expr, $this_op:pat, $op:pat, $func:expr, $ignore_case:expr) => {{
+        let before = $func($left.clone(), $right.clone());
+        match ($left.as_ref(), $right.as_ref()) {
+            (
+                _,
+                Expression::Binary {
+                    left: right_left,
+                    operator: $op,
+                    right: right_right,
+                },
+            ) => {
+                let result = evaluate_equals_or_opposites(
+                    $left.as_ref(),
+                    right_left,
+                    right_right,
+                    $func,
+                    $ignore_case,
+                    $operations,
+                )
+                .unwrap_or($func(
+                    $left.absorption_law($operations, $ignore_case),
+                    $right.absorption_law($operations, $ignore_case),
+                ));
+                if let Some(operation) = Operation::new(&before, &result, Law::AbsorptionLaw) {
+                    $operations.push(operation);
                 }
-                (_, Expression::Binary { left: right_left, operator: $this_op, .. })
-                if $left.opposite_eq(right_left, $ignore_case) => {
-                    let result = $func($left.clone(), right_left.clone());
-                    if let Some(operation) = Operation::new(&before, &result, Law::AbsorptionLaw) {
-                        $operations.push(operation);
-                    }
-                    result
-                }
-                (_, Expression::Binary { right: right_right, operator: $this_op, .. })
-                if $left.opposite_eq(right_right, $ignore_case) => {
-                    let result = $func($left.clone(), right_right.clone());
-                    if let Some(operation) = Operation::new(&before, &result, Law::AbsorptionLaw) {
-                        $operations.push(operation);
-                    }
-                    result
-                }
-                (Expression::Binary { left: left_left, operator: $op, right: left_right }, _) => {
-                    let result = evaluate_equals_or_opposites($right.as_ref(), left_left, left_right, $func, $ignore_case, $operations).unwrap_or(
-                        $func($left.absorption_law($operations, $ignore_case), $right.absorption_law($operations, $ignore_case))
-                    );
-                    if let Some(operation) = Operation::new(&before, &result, Law::AbsorptionLaw) {
-                        $operations.push(operation);
-                    }
-                    result
-                }
-                (Expression::Binary { left: left_left, operator: $this_op, .. }, _)
-                if $right.opposite_eq(left_left, $ignore_case) => {
-                    let result = $func($right.clone(), left_left.clone());
-                    if let Some(operation) = Operation::new(&before, &result, Law::AbsorptionLaw) {
-                        $operations.push(operation);
-                    }
-                    result
-                }
-                (Expression::Binary { right: left_right, operator: $this_op, .. }, _)
-                if $right.opposite_eq(left_right, $ignore_case) => {
-                    let result = $func($right.clone(), left_right.clone());
-                    if let Some(operation) = Operation::new(&before, &result, Law::AbsorptionLaw) {
-                        $operations.push(operation);
-                    }
-                    result
-                }
-                (left, right) => $func(left.absorption_law($operations, $ignore_case), right.absorption_law($operations, $ignore_case))
+                result
             }
+            (
+                _,
+                Expression::Binary {
+                    left: right_left,
+                    operator: $this_op,
+                    ..
+                },
+            ) if $left.opposite_eq(right_left, $ignore_case) => {
+                let result = $func($left.clone(), right_left.clone());
+                if let Some(operation) = Operation::new(&before, &result, Law::AbsorptionLaw) {
+                    $operations.push(operation);
+                }
+                result
+            }
+            (
+                _,
+                Expression::Binary {
+                    right: right_right,
+                    operator: $this_op,
+                    ..
+                },
+            ) if $left.opposite_eq(right_right, $ignore_case) => {
+                let result = $func($left.clone(), right_right.clone());
+                if let Some(operation) = Operation::new(&before, &result, Law::AbsorptionLaw) {
+                    $operations.push(operation);
+                }
+                result
+            }
+            (
+                Expression::Binary {
+                    left: left_left,
+                    operator: $op,
+                    right: left_right,
+                },
+                _,
+            ) => {
+                let result = evaluate_equals_or_opposites(
+                    $right.as_ref(),
+                    left_left,
+                    left_right,
+                    $func,
+                    $ignore_case,
+                    $operations,
+                )
+                .unwrap_or($func(
+                    $left.absorption_law($operations, $ignore_case),
+                    $right.absorption_law($operations, $ignore_case),
+                ));
+                if let Some(operation) = Operation::new(&before, &result, Law::AbsorptionLaw) {
+                    $operations.push(operation);
+                }
+                result
+            }
+            (
+                Expression::Binary {
+                    left: left_left,
+                    operator: $this_op,
+                    ..
+                },
+                _,
+            ) if $right.opposite_eq(left_left, $ignore_case) => {
+                let result = $func($right.clone(), left_left.clone());
+                if let Some(operation) = Operation::new(&before, &result, Law::AbsorptionLaw) {
+                    $operations.push(operation);
+                }
+                result
+            }
+            (
+                Expression::Binary {
+                    right: left_right,
+                    operator: $this_op,
+                    ..
+                },
+                _,
+            ) if $right.opposite_eq(left_right, $ignore_case) => {
+                let result = $func($right.clone(), left_right.clone());
+                if let Some(operation) = Operation::new(&before, &result, Law::AbsorptionLaw) {
+                    $operations.push(operation);
+                }
+                result
+            }
+            (left, right) => $func(
+                left.absorption_law($operations, $ignore_case),
+                right.absorption_law($operations, $ignore_case),
+            ),
         }
-    };
+    }};
 }
 
 #[macro_export]
 macro_rules! distributive_law_atomic_vs_binary {
     ($left:expr, $right:expr, $operations:expr, $op:pat, $func1:expr, $func2:expr) => {
         match ($left.as_ref(), $right.as_ref()) {
-            (Expression::Atomic(_), Expression::Binary { left: right_left, operator: $op, right: right_right }) => {
+            (
+                Expression::Atomic(_),
+                Expression::Binary {
+                    left: right_left,
+                    operator: $op,
+                    right: right_right,
+                },
+            ) => {
                 let right_left = right_left.distributive_law($operations);
                 let right_right = right_right.distributive_law($operations);
                 let before = $func2($left.clone(), $right.clone());
-                let after = $func1($func2($left.clone(), right_left), $func2($left.clone(), right_right));
+                let after = $func1(
+                    $func2($left.clone(), right_left),
+                    $func2($left.clone(), right_right),
+                );
                 if let Some(operation) = Operation::new(&before, &after, Law::DistributiveLaw) {
                     $operations.push(operation);
                 }
                 after
             }
-            (Expression::Binary { left: left_left, operator: $op, right: left_right }, Expression::Atomic(_)) => {
+            (
+                Expression::Binary {
+                    left: left_left,
+                    operator: $op,
+                    right: left_right,
+                },
+                Expression::Atomic(_),
+            ) => {
                 let left_left = left_left.distributive_law($operations);
                 let left_right = left_right.distributive_law($operations);
                 let before = $func2($left.clone(), $right.clone());
-                let after = $func1($func2(left_left, $right.clone()), $func2(left_right, $right.clone()));
+                let after = $func1(
+                    $func2(left_left, $right.clone()),
+                    $func2(left_right, $right.clone()),
+                );
                 if let Some(operation) = Operation::new(&before, &after, Law::DistributiveLaw) {
                     $operations.push(operation);
                 }
                 after
             }
-            (left, right) => $func2(left.distributive_law($operations), right.distributive_law($operations))
+            (left, right) => $func2(
+                left.distributive_law($operations),
+                right.distributive_law($operations),
+            ),
         }
     };
 }
@@ -120,7 +200,9 @@ pub struct Options {
 
 impl From<SimplifyOptions> for Options {
     fn from(options: SimplifyOptions) -> Self {
-        Self { ignore_case: options.ignore_case }
+        Self {
+            ignore_case: options.ignore_case,
+        }
     }
 }
 
@@ -129,7 +211,8 @@ impl Expression {
     // TODO better track of operations
     pub fn simplify(&self, options: Options) -> (Self, Vec<Operation>) {
         let mut operations: Vec<Operation> = vec![];
-        let expression = self.elimination_of_implication(&mut operations)
+        let expression = self
+            .elimination_of_implication(&mut operations)
             .de_morgans_laws(&mut operations)
             .absorb_opposites(&mut operations, options.ignore_case)
             // .associative_law(&mut operations)
@@ -144,17 +227,21 @@ impl Expression {
     /// This is done by replacing `a ➔ b` with `¬a ⋁ b`.
     fn elimination_of_implication(&self, operations: &mut Vec<Operation>) -> Self {
         match self {
-            Expression::Not(expr) => {
-                not(expr.elimination_of_implication(operations))
-            }
-            Expression::Binary { left, operator, right } => {
+            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 {
                     let after = or(not(l_result.clone()), r_result.clone());
-                    if let Some(operation) = Operation::new(&before, &after, Law::EliminationOfImplication) {
+                    if let Some(operation) =
+                        Operation::new(&before, &after, Law::EliminationOfImplication)
+                    {
                         operations.push(operation);
                     }
                     after
@@ -173,7 +260,9 @@ impl Expression {
         match self {
             Expression::Not(expr) => {
                 if let Expression::Not(after) = expr.deref() {
-                    if let Some(operation) = Operation::new(self, after, Law::DoubleNegationElimination) {
+                    if let Some(operation) =
+                        Operation::new(self, after, Law::DoubleNegationElimination)
+                    {
                         operations.push(operation);
                     }
                     after.double_negation_elimination(operations)
@@ -181,7 +270,11 @@ impl Expression {
                     self.clone()
                 }
             }
-            Expression::Binary { left, operator, right } => {
+            Expression::Binary {
+                left,
+                operator,
+                right,
+            } => {
                 let left = left.double_negation_elimination(operations);
                 let right = right.double_negation_elimination(operations);
                 binary(left, *operator, right)
@@ -192,25 +285,31 @@ impl Expression {
 
     fn de_morgans_laws(&self, operations: &mut Vec<Operation>) -> Self {
         match self {
-            Expression::Not(expr) => {
-                match expr.deref() {
-                    Expression::Binary { left, operator: operator @ (BinaryOperator::And | BinaryOperator::Or), right } => {
-                        let left = not(left.de_morgans_laws(operations));
-                        let right = not(right.de_morgans_laws(operations));
-                        let result = if let BinaryOperator::And = operator {
-                            or(left, right)
-                        } else {
-                            and(left, right)
-                        };
-                        if let Some(operation) = Operation::new(self, &result, Law::DeMorgansLaws) {
-                            operations.push(operation);
-                        }
-                        result.de_morgans_laws(operations)
+            Expression::Not(expr) => match expr.deref() {
+                Expression::Binary {
+                    left,
+                    operator: operator @ (BinaryOperator::And | BinaryOperator::Or),
+                    right,
+                } => {
+                    let left = not(left.de_morgans_laws(operations));
+                    let right = not(right.de_morgans_laws(operations));
+                    let result = if let BinaryOperator::And = operator {
+                        or(left, right)
+                    } else {
+                        and(left, right)
+                    };
+                    if let Some(operation) = Operation::new(self, &result, Law::DeMorgansLaws) {
+                        operations.push(operation);
                     }
-                    _ => not(expr.de_morgans_laws(operations)),
+                    result.de_morgans_laws(operations)
                 }
-            }
-            Expression::Binary { left, operator, right } => {
+                _ => not(expr.de_morgans_laws(operations)),
+            },
+            Expression::Binary {
+                left,
+                operator,
+                right,
+            } => {
                 let left = left.de_morgans_laws(operations);
                 let right = right.de_morgans_laws(operations);
                 binary(left, *operator, right)
@@ -222,42 +321,68 @@ impl Expression {
     // TODO merge some branches?
     fn absorption_law(&self, operations: &mut Vec<Operation>, ignore_case: bool) -> Self {
         match self {
-            Expression::Binary { left, operator: BinaryOperator::And | BinaryOperator::Or, right }
-            if Expression::eq(left, right, ignore_case) => {
+            Expression::Binary {
+                left,
+                operator: BinaryOperator::And | BinaryOperator::Or,
+                right,
+            } if Expression::eq(left, right, ignore_case) => {
                 if let Some(operation) = Operation::new(self, left, Law::AbsorptionLaw) {
                     operations.push(operation);
                 }
                 left.absorption_law(operations, ignore_case)
             }
-            Expression::Binary { left, operator, right }
-            if operator.is_and() && (right.is_in(left) && left.is_and() || left.is_in(right) && right.is_or()) => {
+            Expression::Binary {
+                left,
+                operator,
+                right,
+            } if operator.is_and()
+                && (right.is_in(left) && left.is_and() || left.is_in(right) && right.is_or()) =>
+            {
                 if let Some(operation) = Operation::new(self, left, Law::AbsorptionLaw) {
                     operations.push(operation);
                 }
                 left.absorption_law(operations, ignore_case)
             }
-            Expression::Binary { left, operator, right }
-            if operator.is_and() && (right.is_in(left) && left.is_or() || left.is_in(right) && right.is_and()) => {
+            Expression::Binary {
+                left,
+                operator,
+                right,
+            } if operator.is_and()
+                && (right.is_in(left) && left.is_or() || left.is_in(right) && right.is_and()) =>
+            {
                 if let Some(operation) = Operation::new(self, right, Law::AbsorptionLaw) {
                     operations.push(operation);
                 }
                 right.absorption_law(operations, ignore_case)
             }
-            Expression::Binary { left, operator, right }
-            if operator.is_or() && (right.is_in(left) && (left.is_and() || left.is_or()) || left.is_in(right) && right.is_or()) => {
+            Expression::Binary {
+                left,
+                operator,
+                right,
+            } if operator.is_or()
+                && (right.is_in(left) && (left.is_and() || left.is_or())
+                    || left.is_in(right) && right.is_or()) =>
+            {
                 if let Some(operation) = Operation::new(self, right, Law::AbsorptionLaw) {
                     operations.push(operation);
                 }
                 right.absorption_law(operations, ignore_case)
             }
-            Expression::Binary { left, operator: BinaryOperator::Or, right }
-            if left.is_in(right) && right.is_and() => {
+            Expression::Binary {
+                left,
+                operator: BinaryOperator::Or,
+                right,
+            } if left.is_in(right) && right.is_and() => {
                 if let Some(operation) = Operation::new(self, left, Law::AbsorptionLaw) {
                     operations.push(operation);
                 }
                 left.absorption_law(operations, ignore_case)
             }
-            Expression::Binary { left, operator, right } => binary(
+            Expression::Binary {
+                left,
+                operator,
+                right,
+            } => binary(
                 left.absorption_law(operations, ignore_case),
                 *operator,
                 right.absorption_law(operations, ignore_case),
@@ -269,14 +394,42 @@ impl Expression {
 
     fn absorb_opposites(&self, operations: &mut Vec<Operation>, ignore_case: bool) -> Self {
         match self {
-            Expression::Binary { left, operator: BinaryOperator::And, right } => {
+            Expression::Binary {
+                left,
+                operator: BinaryOperator::And,
+                right,
+            } => {
                 // TODO Refactor duplicate code with absorption_law!
-                absorption_law_opposites!(left, right, operations, BinaryOperator::And, BinaryOperator::Or, and, ignore_case)
+                absorption_law_opposites!(
+                    left,
+                    right,
+                    operations,
+                    BinaryOperator::And,
+                    BinaryOperator::Or,
+                    and,
+                    ignore_case
+                )
             }
-            Expression::Binary { left, operator: BinaryOperator::Or, right } => {
-                absorption_law_opposites!(left, right, operations, BinaryOperator::Or, BinaryOperator::And, or, ignore_case)
+            Expression::Binary {
+                left,
+                operator: BinaryOperator::Or,
+                right,
+            } => {
+                absorption_law_opposites!(
+                    left,
+                    right,
+                    operations,
+                    BinaryOperator::Or,
+                    BinaryOperator::And,
+                    or,
+                    ignore_case
+                )
             }
-            Expression::Binary { left, operator, right } => binary(
+            Expression::Binary {
+                left,
+                operator,
+                right,
+            } => binary(
                 left.absorb_opposites(operations, ignore_case),
                 *operator,
                 right.absorb_opposites(operations, ignore_case),
@@ -294,13 +447,39 @@ impl Expression {
     // A & (B | C) <=> A & B | A & C
     fn distributive_law(&self, operations: &mut Vec<Operation>) -> Self {
         match self {
-            Expression::Binary { left, operator: BinaryOperator::And, right } => {
-                distributive_law_atomic_vs_binary!(left, right, operations, BinaryOperator::Or, or, and)
+            Expression::Binary {
+                left,
+                operator: BinaryOperator::And,
+                right,
+            } => {
+                distributive_law_atomic_vs_binary!(
+                    left,
+                    right,
+                    operations,
+                    BinaryOperator::Or,
+                    or,
+                    and
+                )
             }
-            Expression::Binary { left, operator: BinaryOperator::Or, right } => {
-                distributive_law_atomic_vs_binary!(left, right, operations, BinaryOperator::And, and, or)
+            Expression::Binary {
+                left,
+                operator: BinaryOperator::Or,
+                right,
+            } => {
+                distributive_law_atomic_vs_binary!(
+                    left,
+                    right,
+                    operations,
+                    BinaryOperator::And,
+                    and,
+                    or
+                )
             }
-            Expression::Binary { left, operator, right } => binary(
+            Expression::Binary {
+                left,
+                operator,
+                right,
+            } => binary(
                 left.distributive_law(operations),
                 *operator,
                 right.distributive_law(operations),
@@ -327,9 +506,15 @@ fn evaluate_equals_or_opposites<F: Fn(Expression, Expression) -> Expression>(
         return Some(this.absorption_law(operations, ignore_case));
     } else if left.is_atomic() && right.is_atomic() {
         if this.opposite_eq(left, ignore_case) {
-            return Some(op_func(right.absorption_law(operations, ignore_case), this.absorption_law(operations, ignore_case)));
+            return Some(op_func(
+                right.absorption_law(operations, ignore_case),
+                this.absorption_law(operations, ignore_case),
+            ));
         } else if this.opposite_eq(right, ignore_case) {
-            return Some(op_func(left.absorption_law(operations, ignore_case), this.absorption_law(operations, ignore_case)));
+            return Some(op_func(
+                left.absorption_law(operations, ignore_case),
+                this.absorption_law(operations, ignore_case),
+            ));
         }
     }
     None
@@ -342,7 +527,8 @@ mod tests {
 
     #[test]
     fn test_simplify() {
-        let (expression, operations) = implies(atomic("a"), atomic("b")).simplify(Default::default());
+        let (expression, operations) =
+            implies(atomic("a"), atomic("b")).simplify(Default::default());
         assert_eq!(expression, or(not(atomic("a")), atomic("b")));
         assert_eq!(operations.len(), 1);
         assert_eq!(operations[0].law, Law::EliminationOfImplication);
@@ -358,14 +544,20 @@ mod tests {
 
     #[test]
     fn test_implication_and_de_morgans() {
-        let expression = implies(and(not(atomic("a")), atomic("b")), atomic("c")).simplify(Default::default()).0;
-        assert_eq!(expression, or(or(atomic("a"), not(atomic("b"))), atomic("c")));
+        let expression = implies(and(not(atomic("a")), atomic("b")), atomic("c"))
+            .simplify(Default::default())
+            .0;
+        assert_eq!(
+            expression,
+            or(or(atomic("a"), not(atomic("b"))), atomic("c"))
+        );
     }
 
     #[test]
     fn test_elimination_of_implication() {
         let mut operations = vec![];
-        let expression = implies(atomic("a"), atomic("b")).elimination_of_implication(&mut operations);
+        let expression =
+            implies(atomic("a"), atomic("b")).elimination_of_implication(&mut operations);
         assert_eq!(expression, or(not(atomic("a")), atomic("b")));
         assert_eq!(operations.len(), 1);
         assert_eq!(operations[0].law, Law::EliminationOfImplication);
@@ -376,8 +568,12 @@ mod tests {
     #[test]
     fn test_elimination_of_implication_nested() {
         let mut operations = vec![];
-        let expression = implies(atomic("a"), implies(atomic("b"), atomic("c"))).elimination_of_implication(&mut operations);
-        assert_eq!(expression, or(not(atomic("a")), or(not(atomic("b")), atomic("c"))));
+        let expression = implies(atomic("a"), implies(atomic("b"), atomic("c")))
+            .elimination_of_implication(&mut operations);
+        assert_eq!(
+            expression,
+            or(not(atomic("a")), or(not(atomic("b")), atomic("c")))
+        );
         assert_eq!(operations.len(), 2);
         assert_eq!(operations[0].law, Law::EliminationOfImplication);
         assert_eq!(operations[0].before, "b ➔ c");
@@ -398,7 +594,8 @@ mod tests {
     #[test]
     fn test_elimination_of_implication_nested_none() {
         let mut operations = vec![];
-        let expression = or(atomic("a"), and(atomic("b"), atomic("c"))).elimination_of_implication(&mut operations);
+        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);
     }
@@ -428,7 +625,8 @@ mod tests {
     #[test]
     fn test_five_negation_elimination() {
         let mut operations = vec![];
-        let expression = not(not(not(not(not(atomic("a")))))).double_negation_elimination(&mut operations);
+        let expression =
+            not(not(not(not(not(atomic("a")))))).double_negation_elimination(&mut operations);
         assert_eq!(expression, not(atomic("a")));
         assert_eq!(operations.len(), 2);
         assert_eq!(operations[0].law, Law::DoubleNegationElimination);
@@ -449,7 +647,11 @@ mod tests {
     #[test]
     fn test_double_negation_nested_elimination() {
         let mut operations = vec![];
-        let expression = and(or(not(not(atomic("a"))), atomic("b")), not(not(atomic("c")))).double_negation_elimination(&mut operations);
+        let expression = and(
+            or(not(not(atomic("a"))), atomic("b")),
+            not(not(atomic("c"))),
+        )
+        .double_negation_elimination(&mut operations);
         assert_eq!(expression, and(or(atomic("a"), atomic("b")), atomic("c")));
         assert_eq!(operations.len(), 2);
         assert_eq!(operations[0].law, Law::DoubleNegationElimination);
@@ -485,8 +687,12 @@ mod tests {
     #[test]
     fn test_de_morgans_laws_nested_or() {
         let mut operations = vec![];
-        let expression = not(or(and(atomic("a"), atomic("b")), atomic("c"))).de_morgans_laws(&mut operations); // ¬(a ⋀ b ⋁ c)
-        assert_eq!(expression, and(or(not(atomic("a")), not(atomic("b"))), not(atomic("c")))); // ¬(a ⋀ b) ⋀ ¬c == (¬a ⋁ ¬b) ⋀ ¬c
+        let expression =
+            not(or(and(atomic("a"), atomic("b")), atomic("c"))).de_morgans_laws(&mut operations); // ¬(a ⋀ b ⋁ c)
+        assert_eq!(
+            expression,
+            and(or(not(atomic("a")), not(atomic("b"))), not(atomic("c")))
+        ); // ¬(a ⋀ b) ⋀ ¬c == (¬a ⋁ ¬b) ⋀ ¬c
         assert_eq!(operations.len(), 2);
         assert_eq!(operations[0].law, Law::DeMorgansLaws);
         assert_eq!(operations[0].before, "¬(a ⋀ b ⋁ c)");
@@ -499,8 +705,12 @@ mod tests {
     #[test]
     fn test_de_morgans_laws_nested_and() {
         let mut operations = vec![];
-        let expression = not(and(or(atomic("a"), atomic("b")), atomic("c"))).de_morgans_laws(&mut operations); // ¬((a ⋁ b) ⋀ c)
-        assert_eq!(expression, or(and(not(atomic("a")), not(atomic("b"))), not(atomic("c")))); // ¬(a ⋁ b) ⋀ ¬c == (¬a ⋀ ¬b) ⋁ ¬c
+        let expression =
+            not(and(or(atomic("a"), atomic("b")), atomic("c"))).de_morgans_laws(&mut operations); // ¬((a ⋁ b) ⋀ c)
+        assert_eq!(
+            expression,
+            or(and(not(atomic("a")), not(atomic("b"))), not(atomic("c")))
+        ); // ¬(a ⋁ b) ⋀ ¬c == (¬a ⋀ ¬b) ⋁ ¬c
         assert_eq!(operations.len(), 2);
         assert_eq!(operations[0].law, Law::DeMorgansLaws);
         assert_eq!(operations[0].before, "¬((a ⋁ b) ⋀ c)");
@@ -513,8 +723,18 @@ mod tests {
     #[test]
     fn test_de_morgans_laws_nested_and_or() {
         let mut operations = vec![];
-        let expression = not(and(or(atomic("a"), atomic("b")), or(atomic("c"), atomic("d")))).de_morgans_laws(&mut operations); // ¬(a ⋁ b ⋀ c ⋁ d)
-        assert_eq!(expression, or(and(not(atomic("a")), not(atomic("b"))), and(not(atomic("c")), not(atomic("d"))))); // ¬(a ⋁ b) ⋀ ¬(c ⋁ d) == (¬a ⋀ ¬b) ⋁ (¬c ⋀ ¬d)
+        let expression = not(and(
+            or(atomic("a"), atomic("b")),
+            or(atomic("c"), atomic("d")),
+        ))
+        .de_morgans_laws(&mut operations); // ¬(a ⋁ b ⋀ c ⋁ d)
+        assert_eq!(
+            expression,
+            or(
+                and(not(atomic("a")), not(atomic("b"))),
+                and(not(atomic("c")), not(atomic("d")))
+            )
+        ); // ¬(a ⋁ b) ⋀ ¬(c ⋁ d) == (¬a ⋀ ¬b) ⋁ (¬c ⋀ ¬d)
         assert_eq!(operations.len(), 3);
     }
 
@@ -522,7 +742,8 @@ mod tests {
     #[test]
     fn test_absorption_law_and() {
         let mut operations = vec![];
-        let expression = and(atomic("a"), or(atomic("a"), atomic("b"))).absorption_law(&mut operations, false);
+        let expression =
+            and(atomic("a"), or(atomic("a"), atomic("b"))).absorption_law(&mut operations, false);
         assert_eq!(expression, atomic("a"));
         assert_eq!(operations.len(), 1);
     }
@@ -530,7 +751,8 @@ mod tests {
     #[test]
     fn test_absorption_law_or() {
         let mut operations = vec![];
-        let expression = or(atomic("a"), and(atomic("a"), atomic("b"))).absorption_law(&mut operations, false);
+        let expression =
+            or(atomic("a"), and(atomic("a"), atomic("b"))).absorption_law(&mut operations, false);
         assert_eq!(expression, atomic("a"));
         assert_eq!(operations.len(), 1);
     }
@@ -541,24 +763,22 @@ mod tests {
         let mut operations = vec![];
         let expression = or(
             not(atomic("a")),
-            or(
-                not(atomic("a")),
-                or(
-                    atomic("a"),
-                    atomic("b"),
-                ),
-            ),
-        ).absorption_law(&mut operations, false);
-        assert_eq!(expression, or(not(atomic("a")), or(atomic("a"), atomic("b"))));
+            or(not(atomic("a")), or(atomic("a"), atomic("b"))),
+        )
+        .absorption_law(&mut operations, false);
+        assert_eq!(
+            expression,
+            or(not(atomic("a")), or(atomic("a"), atomic("b")))
+        );
         assert_eq!(operations.len(), 1);
     }
 
-
     // !A & B | A <=> B | A
     #[test]
     fn test_absorption_law_not() {
         let mut operations = vec![];
-        let expression = or(and(not(atomic("a")), atomic("b")), atomic("a")).absorb_opposites(&mut operations, Default::default());
+        let expression = or(and(not(atomic("a")), atomic("b")), atomic("a"))
+            .absorb_opposites(&mut operations, Default::default());
         assert_eq!(expression, or(atomic("b"), atomic("a")));
         assert_eq!(operations.len(), 1);
         assert_eq!(operations[0].law, Law::AbsorptionLaw);
@@ -570,7 +790,8 @@ mod tests {
     #[test]
     fn test_absorption_law_duplicate_a_or_not_b() {
         let mut operations = vec![];
-        let expression = atomic("a").or(not(atomic("b")).or(atomic("a")))
+        let expression = atomic("a")
+            .or(not(atomic("b")).or(atomic("a")))
             .absorption_law(&mut operations, Default::default())
             .absorb_opposites(&mut operations, Default::default());
         assert_eq!(expression, or(not(atomic("b")), atomic("a")));
@@ -582,9 +803,12 @@ mod tests {
 
     // A ⋁ ¬B ⋁ A <=> ¬B ⋁ A
     #[test]
-    fn test_absorption_law_duplicate_a_or_not_b_flipped() { // TODO works on master
+    fn test_absorption_law_duplicate_a_or_not_b_flipped() {
+        // TODO works on master
         let mut operations = vec![];
-        let expression = atomic("a").or(not(atomic("b"))).or(atomic("a"))
+        let expression = atomic("a")
+            .or(not(atomic("b")))
+            .or(atomic("a"))
             .absorption_law(&mut operations, Default::default())
             .absorb_opposites(&mut operations, Default::default());
         assert_eq!(expression, or(not(atomic("b")), atomic("a")));
@@ -610,7 +834,8 @@ mod tests {
     #[test]
     fn test_absorption_law_not_reversed() {
         let mut operations = vec![];
-        let expression = or(and(atomic("a"), atomic("b")), not(atomic("a"))).absorb_opposites(&mut operations, Default::default());
+        let expression = or(and(atomic("a"), atomic("b")), not(atomic("a")))
+            .absorb_opposites(&mut operations, Default::default());
         assert_eq!(expression, or(atomic("b"), not(atomic("a"))));
         assert_eq!(operations.len(), 1);
     }
@@ -619,7 +844,8 @@ mod tests {
     #[test]
     fn test_absorption_law_not_duplicate() {
         let mut operations = vec![];
-        let expression = or(atomic("a"), or(not(atomic("a")), atomic("b"))).absorb_opposites(&mut operations, Default::default());
+        let expression = or(atomic("a"), or(not(atomic("a")), atomic("b")))
+            .absorb_opposites(&mut operations, Default::default());
         assert_eq!(expression, or(atomic("a"), not(atomic("a"))));
         assert_eq!(operations.len(), 1);
     }
@@ -628,7 +854,8 @@ mod tests {
     #[test]
     fn test_absorption_law_double_not() {
         let mut operations = vec![];
-        let expression = or(and(not(atomic("a")), atomic("b")), not(atomic("a"))).absorption_law(&mut operations, Default::default());
+        let expression = or(and(not(atomic("a")), atomic("b")), not(atomic("a")))
+            .absorption_law(&mut operations, Default::default());
         assert_eq!(expression, not(atomic("a")));
         assert_eq!(operations.len(), 1);
     }
@@ -664,7 +891,8 @@ mod tests {
     #[test]
     fn test_in_parenthesis() {
         let mut operations = vec![];
-        let expression = and(or(atomic("a"), atomic("b")), not(atomic("a"))).absorb_opposites(&mut operations, Default::default());
+        let expression = and(or(atomic("a"), atomic("b")), not(atomic("a")))
+            .absorb_opposites(&mut operations, Default::default());
         assert_eq!(expression, and(atomic("b"), not(atomic("a"))));
         assert_eq!(operations.len(), 1);
         assert_eq!(operations[0].law, Law::AbsorptionLaw);
@@ -675,8 +903,12 @@ mod tests {
     #[test]
     fn test_distributive_law_and() {
         let mut operations = vec![];
-        let expression = and(atomic("a"), or(atomic("b"), atomic("c"))).distributive_law(&mut operations);
-        assert_eq!(expression, or(and(atomic("a"), atomic("b")), and(atomic("a"), atomic("c"))));
+        let expression =
+            and(atomic("a"), or(atomic("b"), atomic("c"))).distributive_law(&mut operations);
+        assert_eq!(
+            expression,
+            or(and(atomic("a"), atomic("b")), and(atomic("a"), atomic("c")))
+        );
         assert_eq!(operations.len(), 1);
         assert_eq!(operations[0].law, Law::DistributiveLaw);
         assert_eq!(operations[0].before, "a ⋀ (b ⋁ c)");
@@ -686,8 +918,12 @@ mod tests {
     #[test]
     fn test_distributive_law_or() {
         let mut operations = vec![];
-        let expression = or(atomic("a"), and(atomic("b"), atomic("c"))).distributive_law(&mut operations);
-        assert_eq!(expression, and(or(atomic("a"), atomic("b")), or(atomic("a"), atomic("c"))));
+        let expression =
+            or(atomic("a"), and(atomic("b"), atomic("c"))).distributive_law(&mut operations);
+        assert_eq!(
+            expression,
+            and(or(atomic("a"), atomic("b")), or(atomic("a"), atomic("c")))
+        );
         assert_eq!(operations.len(), 1);
         assert_eq!(operations[0].law, Law::DistributiveLaw);
         assert_eq!(operations[0].before, "a ⋁ b ⋀ c");
@@ -697,8 +933,12 @@ mod tests {
     #[test]
     fn test_distributive_law_nested_not() {
         let mut operations = vec![];
-        let expression = and(atomic("a"), not(or(atomic("b"), atomic("c")))).distributive_law(&mut operations);
-        assert_eq!(expression, and(atomic("a"), not(or(atomic("b"), atomic("c")))));
+        let expression =
+            and(atomic("a"), not(or(atomic("b"), atomic("c")))).distributive_law(&mut operations);
+        assert_eq!(
+            expression,
+            and(atomic("a"), not(or(atomic("b"), atomic("c"))))
+        );
         assert_eq!(operations.len(), 0);
     }
 
@@ -708,11 +948,15 @@ mod tests {
         let expression = and(
             and(atomic("A"), or(atomic("B"), atomic("C"))),
             and(atomic("A"), or(atomic("B"), atomic("C"))),
-        ).distributive_law(&mut operations);
-        assert_eq!(expression, and(
-            or(and(atomic("A"), atomic("B")), and(atomic("A"), atomic("C"))),
-            or(and(atomic("A"), atomic("B")), and(atomic("A"), atomic("C"))),
-        ));
+        )
+        .distributive_law(&mut operations);
+        assert_eq!(
+            expression,
+            and(
+                or(and(atomic("A"), atomic("B")), and(atomic("A"), atomic("C"))),
+                or(and(atomic("A"), atomic("B")), and(atomic("A"), atomic("C"))),
+            )
+        );
         assert_eq!(operations.len(), 2);
         assert_eq!(operations[0].law, Law::DistributiveLaw);
         assert_eq!(operations[0].before, "A ⋀ (B ⋁ C)");