From 65a9c140ffc2b1f0009a4d641e5410e81c9e1666 Mon Sep 17 00:00:00 2001 From: NullWitnessZK <312565654+NullWitnessZK@users.noreply.github.com> Date: Mon, 3 Aug 2026 22:57:31 +0800 Subject: [PATCH] fix: fold boolean OR complements to true --- src/ir/opt/cfold.rs | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/ir/opt/cfold.rs b/src/ir/opt/cfold.rs index acd6ffbb8..7c94399e7 100644 --- a/src/ir/opt/cfold.rs +++ b/src/ir/opt/cfold.rs @@ -132,11 +132,10 @@ pub fn fold_cache(node: &Term, cache: &mut TermCache, ignore: &[Op]) -> T Some(if *flattened.op() == OR { let mut dedup_children = TermSet::default(); for t in flattened.cs().iter() { - if dedup_children.contains(&term![Op::Not; t.clone()]) { - dedup_children.remove(&term![Op::Not; t.clone()]); - } else { - dedup_children.insert(t.clone()); + if dedup_children.contains(&neg_bool(t.clone())) { + return bool_lit(true); } + dedup_children.insert(t.clone()); } match dedup_children.len().cmp(&1) { @@ -737,6 +736,13 @@ mod test { assert_eq!(fold(&term![OR; bool(false), bool(true)], &[]), bool(true),); } + #[test] + fn b_or_complement() { + let a = var("a".to_owned(), Sort::Bool); + assert_eq!(fold(&term![OR; a.clone(), term![NOT; a.clone()]], &[]), bool(true)); + assert_eq!(fold(&term![OR; term![NOT; a.clone()], a], &[]), bool(true)); + } + #[test] fn b_and() { assert_eq!(fold(&term![AND; bool(false), bool(true)], &[]), bool(false),);