martials/simplify_truths
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

format with rustfmt

Browse Source
This commit is contained in:
Martin Berg Alstad 2024-07-14 19:08:58 +02:00
parent 60b9bdc28a
commit abad6181cb
1 changed files with 399 additions and 155 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

554
src/expressions/simplify.rs
View File

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