diff --git a/src/uniqueness/boolean_algebra.rs b/src/uniqueness/boolean_algebra.rs index ecb0a7b71d..c89dde35c0 100644 --- a/src/uniqueness/boolean_algebra.rs +++ b/src/uniqueness/boolean_algebra.rs @@ -38,10 +38,11 @@ pub fn or(left: Bool, right: Bool) -> Bool { Or(Box::new(left), Box::new(right)) } -pub fn any(mut it: I) -> Bool +pub fn any(iterable: I) -> Bool where - I: Iterator, + I: IntoIterator, { + let mut it = iterable.into_iter(); if let Some(first) = it.next() { it.fold(first, |x, y| or(y, x)) } else { @@ -49,20 +50,11 @@ where } } -pub fn all(terms: Product) -> Bool { - let mut it = terms.into_iter(); - - if let Some(first) = it.next() { - it.fold(first, and) - } else { - One - } -} - -pub fn all_iterator(mut it: I) -> Bool +pub fn all(iterable: I) -> Bool where - I: Iterator, + I: IntoIterator, { + let mut it = iterable.into_iter(); if let Some(first) = it.next() { it.fold(first, and) } else { @@ -179,50 +171,27 @@ pub fn sop_to_term(sop: Sop) -> Bool { accum.sort_by(|x, y| (y.len().cmp(&x.len()))); - println!("{:?}", &accum); - - any(accum.into_iter().map(|v| all_iterator(v.into_iter()))) + any(accum.into_iter().map(all)) } #[inline(always)] pub fn sop_to_term_vector(sop: Vec>) -> Bool { - any(sop.into_iter().rev().map(|v| all_iterator(v.into_iter()))) -} - -pub fn simplify_sop(sop: Sop) -> Sop { - // sort by length longest to shortest (proxy for how many variables there are) - let mut sorted: Vec> = sop.clone().into_iter().collect(); - - sorted.sort_by(|x, y| y.len().cmp(&x.len())); - - // filter out anything that is included in the remaining elements - let mut active = sop; - let mut result = ImSet::default(); - for t in sorted { - if !(active.remove(&t).is_some() && included(all(t.clone()), sop_to_term(active.clone()))) { - result.insert(t); - } - } - - result + any(sop.into_iter().rev().map(all)) } pub fn simplify_sop_vector(sorted: Vec>) -> Vec> { // sort by length longest to shortest (proxy for how many variables there are) // sorted.sort_by(|x, y| y.len().cmp(&x.len())); - let sorted2 = sorted.clone(); + let backup = sorted.clone(); let mut p: Vec> = Vec::new(); for (i, t) in sorted.into_iter().enumerate() { - let ts = &sorted2[i + 1..]; + let ts = &backup[i + 1..]; ts.to_vec().extend(p.clone()); - if included( - all_iterator(t.clone().into_iter()).clone(), - sop_to_term_vector(ts.to_vec()), - ) { + if included(all(t.clone()), sop_to_term_vector(ts.to_vec())) { // do nothing } else { p.insert(0, t.into_iter().collect()); @@ -232,21 +201,6 @@ pub fn simplify_sop_vector(sorted: Vec>) -> Vec> { p } -/* -simplify_sop :: BooleanAlgebra a => Sum (Product a) -> Sum (Product a) -simplify_sop terms = - let - sorted = (sortBy (\x y -> compare (length y) (length x)) terms) - in - f sorted [] - where - f [] p = p - f (t:ts) p = - if list_to_conj t `included` sop_to_term (ts ++ p) - then f ts p - else f ts (t:p) -*/ - /// Blake canonical form pub fn bcf(sop: Sop) -> Vec> { absorptive(syllogistic(sop)) @@ -275,16 +229,8 @@ pub fn syllogistic(terms: Sop) -> Sop { } } -/* -absorptive :: BooleanAlgebra a => Sum (Product a) -> Sum (Product a) -absorptive p = f p p - where - f [] p = p - f (t:ts) p = f ts (t : filter (not . absorbs t) p) -*/ - /// Absorption (apply the identify p + pq = p) -pub fn absorptive(sop: Sop) -> Vec> { +fn absorptive(sop: Sop) -> Vec> { let mut accum: Vec> = Vec::new(); for s in sop { @@ -302,8 +248,6 @@ pub fn absorptive_vector(mut accum: Vec>) -> Vec> { accum.insert(0, product.clone()); } - // accum.reverse(); - accum } @@ -311,12 +255,6 @@ pub fn absorbs_vector(p: &[Bool], q: &[Bool]) -> bool { p.iter().all(|x| q.contains(x)) } -/// Does p absorb q? (can we replace p + q by p?) -/// TODO investigate: either the comment or the implementation is wrong I think? -pub fn absorbs(p: &Product, q: &Product) -> bool { - p.iter().all(|x| q.contains(x)) -} - fn consensus(p: &Product, q: &Product) -> Option> { let mut it = oppositions(p, q).into_iter(); diff --git a/tests/test_boolean_algebra.rs b/tests/test_boolean_algebra.rs index 4a0455249c..1f942825e6 100644 --- a/tests/test_boolean_algebra.rs +++ b/tests/test_boolean_algebra.rs @@ -39,7 +39,9 @@ mod test_boolean_algebra { } fn absorbs_eq(a: ImSet, b: ImSet, expected: bool) { - assert_eq!(boolean_algebra::absorbs(&a, &b), expected); + let x: Vec = a.into_iter().collect(); + let y: Vec = b.into_iter().collect(); + assert_eq!(boolean_algebra::absorbs_vector(&x, &y), expected); } fn vecs_to_sets(input: Vec>) -> ImSet> { @@ -53,7 +55,8 @@ mod test_boolean_algebra { } fn absorptive_eq(actual: Vec>, expected: Vec>) { - let actual_vec: ImSet> = vecs_to_sets(actual); + let result = boolean_algebra::absorptive_vector(actual); + let actual_vec: ImSet> = vecs_to_sets(result); let expected_vec: ImSet> = vecs_to_sets(expected); assert_eq!(actual_vec, expected_vec); } @@ -640,7 +643,7 @@ mod test_boolean_algebra { ); assert_eq!( - boolean_algebra::simplify_sop( + boolean_algebra::simplify_sop_vector( vec![ vec![Variable(a), Variable(d)].into(), vec![Variable(a), Variable(c)].into(), @@ -652,12 +655,11 @@ mod test_boolean_algebra { .into() ), vec![ - vec![Bool::not(Variable(b)), Variable(c)].into(), - vec![Bool::not(Variable(b)), Variable(d)].into(), - vec![Variable(a), Variable(c)].into(), - vec![Variable(a), Variable(d)].into() + vec![Bool::not(Variable(b)), Variable(c)], + vec![Bool::not(Variable(b)), Variable(d)], + vec![Variable(a), Variable(c)], + vec![Variable(a), Variable(d)] ] - .into() ); assert_eq!( @@ -684,33 +686,27 @@ mod test_boolean_algebra { ); absorptive_eq( - boolean_algebra::absorptive( - vec![vec![Bool::not(Variable(b)), Variable(c)].into()].into(), - ), + vec![vec![Bool::not(Variable(b)), Variable(c)].into()].into(), vec![vec![Bool::not(Variable(b)), Variable(c)]], ); absorptive_eq( - boolean_algebra::absorptive( - vec![ - vec![Bool::not(Variable(b)), Variable(c)].into(), - vec![Bool::not(Variable(b)), Variable(d)].into(), - ] - .into(), - ), + vec![ + vec![Bool::not(Variable(b)), Variable(c)].into(), + vec![Bool::not(Variable(b)), Variable(d)].into(), + ] + .into(), vec![ vec![Bool::not(Variable(b)), Variable(d)], vec![Bool::not(Variable(b)), Variable(c)], ], ); absorptive_eq( - boolean_algebra::absorptive( - vec![ - vec![Bool::not(Variable(b)), Variable(c)].into(), - vec![Bool::not(Variable(b)), Variable(d)].into(), - vec![Bool::not(Variable(b)), Bool::not(Variable(d)), Variable(c)].into(), - ] - .into(), - ), + vec![ + vec![Bool::not(Variable(b)), Variable(c)].into(), + vec![Bool::not(Variable(b)), Variable(d)].into(), + vec![Bool::not(Variable(b)), Bool::not(Variable(d)), Variable(c)].into(), + ] + .into(), vec![ vec![Bool::not(Variable(b)), Bool::not(Variable(d)), Variable(c)], vec![Bool::not(Variable(b)), Variable(d)], @@ -718,15 +714,13 @@ mod test_boolean_algebra { ], ); absorptive_eq( - boolean_algebra::absorptive( - vec![ - vec![Bool::not(Variable(b)), Variable(c)].into(), - vec![Bool::not(Variable(b)), Variable(d)].into(), - vec![Bool::not(Variable(b)), Bool::not(Variable(d)), Variable(c)].into(), - vec![Bool::not(Variable(c)), Bool::not(Variable(b)), Variable(d)].into(), - ] - .into(), - ), + vec![ + vec![Bool::not(Variable(b)), Variable(c)].into(), + vec![Bool::not(Variable(b)), Variable(d)].into(), + vec![Bool::not(Variable(b)), Bool::not(Variable(d)), Variable(c)].into(), + vec![Bool::not(Variable(c)), Bool::not(Variable(b)), Variable(d)].into(), + ] + .into(), vec![ vec![Bool::not(Variable(c)), Bool::not(Variable(b)), Variable(d)], vec![Bool::not(Variable(b)), Bool::not(Variable(d)), Variable(c)], @@ -735,16 +729,14 @@ mod test_boolean_algebra { ], ); absorptive_eq( - boolean_algebra::absorptive( - vec![ - vec![Bool::not(Variable(b)), Variable(c)].into(), - vec![Bool::not(Variable(b)), Variable(d)].into(), - vec![Bool::not(Variable(b)), Bool::not(Variable(d)), Variable(c)].into(), - vec![Bool::not(Variable(c)), Bool::not(Variable(b)), Variable(d)].into(), - vec![Variable(a), Variable(c)].into(), - ] - .into(), - ), + vec![ + vec![Bool::not(Variable(b)), Variable(c)].into(), + vec![Bool::not(Variable(b)), Variable(d)].into(), + vec![Bool::not(Variable(b)), Bool::not(Variable(d)), Variable(c)].into(), + vec![Bool::not(Variable(c)), Bool::not(Variable(b)), Variable(d)].into(), + vec![Variable(a), Variable(c)].into(), + ] + .into(), vec![ vec![Variable(a), Variable(c)].into(), vec![Bool::not(Variable(c)), Bool::not(Variable(b)), Variable(d)],