From 89288359c74bb8172af9c04574314c084d4ec2f9 Mon Sep 17 00:00:00 2001 From: Zachary Bonagura Date: Tue, 10 Dec 2024 14:34:02 -0500 Subject: [PATCH] Fixed glitches for complement Fixed glitches for complement, now properly handles preserving non-complement terms --- aris/src/expr.rs | 59 ++++++++++++++++++++-------------- aris/src/proofs/proof_tests.rs | 7 ++-- 2 files changed, 39 insertions(+), 27 deletions(-) diff --git a/aris/src/expr.rs b/aris/src/expr.rs index 20bc162f..0e6a9775 100644 --- a/aris/src/expr.rs +++ b/aris/src/expr.rs @@ -786,6 +786,17 @@ impl Expr { Expr::Assoc { op: Op::Or, exprs } => (demorgans(Op::And, exprs), true), _ => (Expr::not(*operand), false), }, + Expr::Assoc { op, exprs } if op == Op::Or || op == Op::And => { + let flattened_exprs: Vec = exprs + .into_iter() + .flat_map(|e| match e { + Expr::Assoc { op: inner_op, exprs: inner_exprs } if inner_op == op => inner_exprs, + _ => vec![e], + }) + .collect(); + + (Expr::Assoc { op, exprs: flattened_exprs }, false) + } _ => (expr, false), } }) @@ -1148,10 +1159,8 @@ impl Expr { match expr { Expr::Assoc { op: expr_op, exprs } if *expr_op == op => exprs.iter().fold(false, |found_complement, sub_expr| Expr::collect_unique_exprs_complement(sub_expr, op, unique_exprs) || found_complement), Expr::Not { operand } => { - if let Expr::Quant { kind: QuantKind::Forall, .. } = **operand { - if operand.is_universal_tautology() { - return true; - } + if operand.is_universal_tautology() { + return true; } if unique_exprs.contains(&**operand) { unique_exprs.remove(&**operand); @@ -1161,6 +1170,7 @@ impl Expr { false } } + expr if expr.is_universal_tautology() => false, _ => { let negated = Expr::Not { operand: Box::new(expr.clone()) }; if unique_exprs.contains(&negated) { @@ -1182,29 +1192,30 @@ impl Expr { match self { Expr::Assoc { op, exprs } if op == Op::And || op == Op::Or => { let mut unique_exprs = HashSet::new(); - let has_complement = exprs.iter().any(|expr| Expr::collect_unique_exprs_complement(expr, op, &mut unique_exprs)); - - if has_complement { - match op { - Op::And => { - let remaining_terms: Vec = unique_exprs.into_iter().collect(); - if remaining_terms.is_empty() { - Expr::Contra - } else { - Expr::Assoc { op, exprs: vec![Expr::Contra].into_iter().chain(remaining_terms).collect() } - } - } - Op::Or => Expr::Taut, - _ => unreachable!(), + let mut complements_found = false; + + for expr in exprs { + if Expr::collect_unique_exprs_complement(&expr, op, &mut unique_exprs) { + complements_found = true; } - } else { - let unique_exprs: Vec = unique_exprs.into_iter().map(|e| e.normalize_complement()).collect(); - if unique_exprs.len() == 1 { - unique_exprs.into_iter().next().unwrap() - } else { - Expr::Assoc { op, exprs: unique_exprs } + } + + unique_exprs.retain(|e| !e.is_universal_tautology()); + let mut result_exprs: Vec = unique_exprs.into_iter().collect(); + + if complements_found { + if op == Op::Or { + result_exprs.push(Expr::Taut); + } else if op == Op::And { + result_exprs.push(Expr::Contra); } } + + if result_exprs.len() == 1 { + result_exprs.into_iter().next().unwrap() + } else { + Expr::Assoc { op, exprs: result_exprs } + } } other => other, } diff --git a/aris/src/proofs/proof_tests.rs b/aris/src/proofs/proof_tests.rs index 8532d448..a40df43f 100644 --- a/aris/src/proofs/proof_tests.rs +++ b/aris/src/proofs/proof_tests.rs @@ -964,7 +964,6 @@ pub fn test_reduction() -> (P, Vec>, Vec>) { let p2 = prf.add_premise(p("(~~A | B) & ~A")); let p3 = prf.add_premise(p("(B & ~A) | A")); let p4 = prf.add_premise(p("~B | (A & ~~B)")); - // let p5 = prf.add_premise(p("(forall A (A & (~A | B))) | (~(forall A (A & (~A | B))) & C)")); let p6 = prf.add_premise(p("B & (C | (~C & ~A))")); let p7 = prf.add_premise(p("A | (~A & (~~A | B))")); let p8 = prf.add_premise(p("D | (~A & (~~A | B))")); @@ -975,11 +974,12 @@ pub fn test_reduction() -> (P, Vec>, Vec>) { let p12 = prf.add_premise(p("P & M & (~(P & M) | Q)")); let p13 = prf.add_premise(p("(forall A (A & B)) | (~(forall A (A & B)) & C)")); + let p14 = prf.add_premise(p("¬A | (A & B) | ¬C | (C & D)")); + let r1 = prf.add_step(Justification(p("A & B"), RuleM::Reduction, vec![i(p1.clone())], vec![])); let r2 = prf.add_step(Justification(p("~A & B"), RuleM::Reduction, vec![i(p2.clone())], vec![])); let r3 = prf.add_step(Justification(p("A | B"), RuleM::Reduction, vec![i(p3.clone())], vec![])); let r4 = prf.add_step(Justification(p("~B | A"), RuleM::Reduction, vec![i(p4.clone())], vec![])); - // let r5 = prf.add_step(Justification(p("(forall A (A & B)) | (~(forall A (A & B)) & C)"), RuleM::Reduction, vec![i(p5)], vec![])); let r6 = prf.add_step(Justification(p("A"), RuleM::Reduction, vec![i(p1)], vec![])); let r7 = prf.add_step(Justification(p("A | B"), RuleM::Reduction, vec![i(p2)], vec![])); @@ -1000,7 +1000,8 @@ pub fn test_reduction() -> (P, Vec>, Vec>) { let r19 = prf.add_step(Justification(p("P & M & Q"), RuleM::Reduction, vec![i(p12.clone())], vec![])); let r20 = prf.add_step(Justification(p("(forall A (A & B)) | C"), RuleM::Reduction, vec![i(p13)], vec![])); - (prf, vec![i(r1), i(r2), i(r3), i(r4), i(r19), i(r18), i(r10), i(r12), i(r13), i(r14), i(r16), i(r20)], vec![i(r6), i(r7), i(r8), i(r9), i(r11), i(r15), i(r17)]) + let r21 = prf.add_step(Justification(p("¬A ∨ B ∨ ¬C ∨ D"), RuleM::Reduction, vec![i(p14.clone())], vec![])); + (prf, vec![i(r1), i(r2), i(r3), i(r4), i(r19), i(r18), i(r10), i(r12), i(r13), i(r14), i(r16), i(r20), i(r21)], vec![i(r6), i(r7), i(r8), i(r9), i(r11), i(r15), i(r17)]) } pub fn test_adjacency() -> (P, Vec>, Vec>) {