Skip to content

Commit

Permalink
Merge pull request #143 from zacharybonagura/master
Browse files Browse the repository at this point in the history 
Fixed glitches for complement
  • Loading branch information
@zacharybonagura
zacharybonagura authored Dec 10, 2024
2 parents 3288cd5 + 8928835 commit de8293b
Show file tree
Hide file tree
Showing 2 changed files with 39 additions and 27 deletions.
59 changes: 35 additions & 24 deletions aris/src/expr.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<Expr> = 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),
}
})
Expand Down Expand Up @@ -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);
Expand All @@ -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) {
Expand All @@ -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<Expr> = 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<Expr> = 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<Expr> = 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,
}
Expand Down
7 changes: 4 additions & 3 deletions aris/src/proofs/proof_tests.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -964,7 +964,6 @@ pub fn test_reduction<P: Proof>() -> (P, Vec<PjRef<P>>, Vec<PjRef<P>>) {
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))"));
Expand All @@ -975,11 +974,12 @@ pub fn test_reduction<P: Proof>() -> (P, Vec<PjRef<P>>, Vec<PjRef<P>>) {
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![]));
Expand All @@ -1000,7 +1000,8 @@ pub fn test_reduction<P: Proof>() -> (P, Vec<PjRef<P>>, Vec<PjRef<P>>) {
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: Proof>() -> (P, Vec<PjRef<P>>, Vec<PjRef<P>>) {
Expand Down

0 comments on commit de8293b

Please sign in to comment.