bool_logic/transforms/
simplify_all_not_any.rs

1use std::slice;
2
3use crate::ast::{All, Any, Expr, Not};
4use crate::utils::remove_if;
5use crate::visit_mut::VisitMut;
6use crate::visit_mut::walk_mut_expr_list;
7
8pub struct SimplifyAllNotAny;
9
10impl<T> VisitMut<T> for SimplifyAllNotAny
11where
12    T: Eq,
13{
14    /// `all(not(any(x0, x1, ...)), any(x0, x2, ...)) => all(not(any(...)), any(x0, ...))`
15    fn visit_mut_all(&mut self, All(all): &mut All<T>) {
16        walk_mut_expr_list(self, all);
17
18        match all.as_mut_slice() {
19            [Expr::Any(Any(pos)), Expr::Not(Not(not))]
20            | [Expr::Not(Not(not)), Expr::Any(Any(pos))] => {
21                let neg = match not.as_mut_any() {
22                    Some(Any(neg)) => neg,
23                    None => slice::from_mut(&mut **not),
24                };
25                remove_if(pos, |x| neg.contains(x));
26            }
27            _ => {}
28        }
29    }
30}
31
32#[cfg(test)]
33mod tests {
34    use super::*;
35    use crate::ast::{all, any, expr, not, var};
36
37    #[test]
38    fn simplify_all_not_any_basic() {
39        let mut x = expr(all((not(any((var(1), var(2)))), any((var(1), var(3))))));
40        let expected = expr(all((not(any((var(1), var(2)))), any((var(3),)))));
41
42        SimplifyAllNotAny.visit_mut_expr(&mut x);
43
44        assert_eq!(x.to_string(), expected.to_string());
45    }
46
47    #[test]
48    fn simplify_all_not_any_reverse_order() {
49        let mut x = expr(all((any((var(1), var(3))), not(any((var(1), var(2)))))));
50        let expected = expr(all((any((var(3),)), not(any((var(1), var(2)))))));
51
52        SimplifyAllNotAny.visit_mut_expr(&mut x);
53
54        assert_eq!(x.to_string(), expected.to_string());
55    }
56
57    #[test]
58    fn simplify_all_not_any_complete_overlap() {
59        let mut x = expr(all((not(any((var(1), var(2)))), any((var(1), var(2))))));
60        let expected = expr(all((not(any((var(1), var(2)))), any(()))));
61
62        SimplifyAllNotAny.visit_mut_expr(&mut x);
63
64        assert_eq!(x.to_string(), expected.to_string());
65    }
66
67    #[test]
68    fn simplify_all_not_any_no_overlap() {
69        let mut x = expr(all((not(any((var(1), var(2)))), any((var(3), var(4))))));
70        let expected = expr(all((not(any((var(1), var(2)))), any((var(3), var(4))))));
71
72        SimplifyAllNotAny.visit_mut_expr(&mut x);
73
74        assert_eq!(x.to_string(), expected.to_string());
75    }
76
77    #[test]
78    fn simplify_all_not_expr_direct() {
79        let mut x = expr(all((not(var(1)), any((var(1), var(2))))));
80        let expected = expr(all((not(var(1)), any((var(2),)))));
81
82        SimplifyAllNotAny.visit_mut_expr(&mut x);
83
84        assert_eq!(x.to_string(), expected.to_string());
85    }
86
87    #[test]
88    fn no_simplify_wrong_pattern() {
89        let mut x = expr(all((var(1), var(2), var(3))));
90        let expected = expr(all((var(1), var(2), var(3))));
91
92        SimplifyAllNotAny.visit_mut_expr(&mut x);
93
94        assert_eq!(x.to_string(), expected.to_string());
95    }
96
97    #[test]
98    fn no_simplify_single_expr() {
99        let mut x = expr(all((not(any((var(1), var(2)))),)));
100        let expected = expr(all((not(any((var(1), var(2)))),)));
101
102        SimplifyAllNotAny.visit_mut_expr(&mut x);
103
104        assert_eq!(x.to_string(), expected.to_string());
105    }
106
107    #[test]
108    fn simplify_partial_overlap() {
109        let mut x = expr(all((
110            not(any((var(1), var(2), var(3)))),
111            any((var(1), var(4), var(5))),
112        )));
113        let expected = expr(all((
114            not(any((var(1), var(2), var(3)))),
115            any((var(4), var(5))),
116        )));
117
118        SimplifyAllNotAny.visit_mut_expr(&mut x);
119
120        assert_eq!(x.to_string(), expected.to_string());
121    }
122}
bool_logic/transforms/simplify_all_not_any.rs

bool_logic/transforms/
simplify_all_not_any.rs
