netsblox_stateflow/
condition.rs

1use core::ops::{BitAnd, BitOr, Not};
2use core::fmt;
3
4use alloc::vec::Vec;
5use alloc::boxed::Box;
6use alloc::string::ToString;
7use alloc::collections::BTreeSet;
8
9use netsblox_ast::CompactString;
10
11#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)]
12pub enum RawCondition {
13    Const(bool),
14    Atom(CompactString),
15    Not(Box<RawCondition>),
16    And(Box<RawCondition>, Box<RawCondition>),
17    Or(Box<RawCondition>, Box<RawCondition>),
18}
19
20impl fmt::Display for RawCondition {
21    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
22        match self {
23            RawCondition::Const(x) => write!(f, "{x}"),
24            RawCondition::Atom(x) => write!(f, "{x}"),
25            RawCondition::And(a, b) => {
26                fn single(f: &mut fmt::Formatter<'_>, v: &RawCondition) -> fmt::Result {
27                    match v {
28                        RawCondition::Or(_, _) => write!(f, "({v})"),
29                        _ => write!(f, "{v}"),
30                    }
31                }
32                single(f, a)?;
33                write!(f, " & ")?;
34                single(f, b)
35            }
36            RawCondition::Or(a, b) => {
37                fn single(f: &mut fmt::Formatter<'_>, v: &RawCondition) -> fmt::Result {
38                    match v {
39                        RawCondition::And(_, _) => write!(f, "({v})"),
40                        _ => write!(f, "{v}"),
41                    }
42                }
43                single(f, a)?;
44                write!(f, " | ")?;
45                single(f, b)
46            }
47            RawCondition::Not(x) => {
48                let inside = x.to_string();
49                if inside.chars().all(char::is_alphanumeric) {
50                    write!(f, "~{inside}")
51                } else {
52                    write!(f, "~({inside})")
53                }
54            }
55        }
56    }
57}
58
59impl BitAnd for RawCondition {
60    type Output = Self;
61    fn bitand(self, rhs: Self) -> Self::Output {
62        RawCondition::And(Box::new(self), Box::new(rhs))
63    }
64}
65impl BitOr for RawCondition {
66    type Output = Self;
67    fn bitor(self, rhs: Self) -> Self::Output {
68        RawCondition::Or(Box::new(self), Box::new(rhs))
69    }
70}
71impl Not for RawCondition {
72    type Output = Self;
73    fn not(self) -> Self::Output {
74        RawCondition::Not(Box::new(self))
75    }
76}
77
78#[test]
79fn test_condition() {
80    let a = RawCondition::Atom("a".into());
81    let b = RawCondition::Atom("b".into());
82    let c = RawCondition::Atom("c".into());
83    let d = RawCondition::Atom("d".into());
84    let e = RawCondition::Atom("x < 10".into());
85    let f = RawCondition::Atom("y == x + 10".into());
86
87    let bt = RawCondition::Const(true);
88    let bf = RawCondition::Const(false);
89
90    assert_eq!(a.to_string(), "a");
91    assert_eq!(b.to_string(), "b");
92    assert_eq!(c.to_string(), "c");
93    assert_eq!(d.to_string(), "d");
94    assert_eq!(e.to_string(), "x < 10");
95    assert_eq!(f.to_string(), "y == x + 10");
96    assert_eq!(bt.to_string(), "true");
97    assert_eq!(bf.to_string(), "false");
98
99    assert_eq!((a.clone() & b.clone()).to_string(), "a & b");
100    assert_eq!((a.clone() & b.clone() & c.clone()).to_string(), "a & b & c");
101    assert_eq!((a.clone() & b.clone() & c.clone() & d.clone()).to_string(), "a & b & c & d");
102
103    assert_eq!((a.clone() | b.clone()).to_string(), "a | b");
104    assert_eq!((a.clone() | b.clone() | c.clone()).to_string(), "a | b | c");
105    assert_eq!((a.clone() | b.clone() | c.clone() | d.clone()).to_string(), "a | b | c | d");
106
107    assert_eq!((a.clone() & b.clone() & a.clone()).to_string(), "a & b & a");
108    assert_eq!(((a.clone() & b.clone()) & a.clone()).to_string(), "a & b & a");
109    assert_eq!((a.clone() & (b.clone() & a.clone())).to_string(), "a & b & a");
110
111    assert_eq!(((a.clone() & b.clone()) | c.clone()).to_string(), "(a & b) | c");
112    assert_eq!((c.clone() | (a.clone() & b.clone())).to_string(), "c | (a & b)");
113    assert_eq!(((c.clone() & a.clone()) | (a.clone() & b.clone())).to_string(), "(c & a) | (a & b)");
114
115    assert_eq!(((a.clone() | b.clone()) & c.clone()).to_string(), "(a | b) & c");
116    assert_eq!((c.clone() & (a.clone() | b.clone())).to_string(), "c & (a | b)");
117    assert_eq!(((c.clone() | a.clone()) & (a.clone() | b.clone())).to_string(), "(c | a) & (a | b)");
118
119    assert_eq!(((a.clone() & (c.clone() & b.clone())) & a.clone()).to_string(), "a & c & b & a");
120    assert_eq!(((a.clone() & (c.clone() & b.clone())) & (a.clone() & a.clone() & c.clone())).to_string(), "a & c & b & a & a & c");
121
122    assert_eq!((!a.clone()).to_string(), "~a");
123    assert_eq!((!c.clone()).to_string(), "~c");
124    assert_eq!((!e.clone()).to_string(), "~(x < 10)");
125    assert_eq!((!f.clone()).to_string(), "~(y == x + 10)");
126
127    assert_eq!((!!a.clone()).to_string(), "~(~a)");
128    assert_eq!((!!c.clone()).to_string(), "~(~c)");
129    assert_eq!((!!e.clone()).to_string(), "~(~(x < 10))");
130    assert_eq!((!!f.clone()).to_string(), "~(~(y == x + 10))");
131
132    assert_eq!((bt.clone() & a.clone()).to_string(), "true & a");
133    assert_eq!((a.clone() & bt.clone()).to_string(), "a & true");
134
135    assert_eq!((bf.clone() | a.clone()).to_string(), "false | a");
136    assert_eq!((a.clone() | bf.clone()).to_string(), "a | false");
137
138    assert_eq!((bf.clone() & a.clone()).to_string(), "false & a");
139    assert_eq!((a.clone() & bf.clone()).to_string(), "a & false");
140
141    assert_eq!((bt.clone() | a.clone()).to_string(), "true | a");
142    assert_eq!((a.clone() | bt.clone()).to_string(), "a | true");
143
144    assert_eq!((a.clone() | !a.clone()).to_string(), "a | ~a");
145
146    assert_eq!((!bt.clone()).to_string(), "~true");
147    assert_eq!((!!bt.clone()).to_string(), "~(~true)");
148    assert_eq!((!!!bt.clone()).to_string(), "~(~(~true))");
149    assert_eq!((!!!!bt.clone()).to_string(), "~(~(~(~true)))");
150
151    assert_eq!((!bf.clone()).to_string(), "~false");
152    assert_eq!((!!bf.clone()).to_string(), "~(~false)");
153    assert_eq!((!!!bf.clone()).to_string(), "~(~(~false))");
154    assert_eq!((!!!!bf.clone()).to_string(), "~(~(~(~false)))");
155}
156
157impl RawCondition {
158    fn visit_and<F: FnMut(&RawCondition)>(&self, f: &mut F) {
159        match self {
160            RawCondition::And(x, y) => {
161                x.visit_and(f);
162                y.visit_and(f);
163            }
164            x => f(x),
165        }
166    }
167    fn visit_or<F: FnMut(&RawCondition)>(&self, f: &mut F) {
168        match self {
169            RawCondition::Or(x, y) => {
170                x.visit_or(f);
171                y.visit_or(f);
172            }
173            x => f(x),
174        }
175    }
176    fn simpl(&self) -> Self {
177        macro_rules! hetero_simpl {
178            ($terms:ident : $kind:ident , $visitor:ident) => {{
179                let groups = $terms.iter().filter(|t| if let RawCondition::$kind(_, _) = t { true } else { false }).map(|t| {
180                    let mut sub_terms: BTreeSet<RawCondition> = Default::default();
181                    t.$visitor(&mut |x| { sub_terms.insert(x.clone()); });
182                    (t.clone(), sub_terms)
183                }).collect::<Vec<_>>();
184                for (i, (group, sub_terms)) in groups.iter().enumerate() {
185                    if sub_terms.iter().any(|t| $terms.contains(t)) || groups[..i].iter().chain(&groups[i + 1..]).any(|t| t.1.is_subset(&sub_terms)) {
186                        assert!($terms.remove(group));
187                    }
188                }
189            }};
190        }
191        macro_rules! homo_simpl {
192            ($terms:ident : $kind:ident, $visitor:ident, $identity:literal) => {{
193                let groups = $terms.iter().filter_map(|t| match t { RawCondition::Not(x) => match &**x { RawCondition::$kind(_, _) => Some((t, x)), _ => None }, _ => None }).map(|(src, x)| {
194                    let mut sub_terms: BTreeSet<RawCondition> = Default::default();
195                    x.$visitor(&mut |x| { sub_terms.insert(x.clone()); });
196                    (src.clone(), sub_terms)
197                }).collect::<Vec<_>>();
198                for (src, group) in groups.iter() {
199                    assert!($terms.remove(src));
200                    if !$terms.iter().any(|t| match t { RawCondition::Not(x) => group.contains(x), _ => false }) && !group.iter().any(|t| match t { RawCondition::Not(x) => $terms.contains(x), _ => false }) {
201                        let new_group = group.iter().filter(|t| !$terms.contains(t)).cloned().collect::<BTreeSet<_>>();
202                        $terms.insert(new_group.into_iter().reduce(|a, b| RawCondition::$kind(Box::new(a), Box::new(b))).map(|t| !t).unwrap_or(RawCondition::Const(!$identity)));
203                    }
204                }
205            }};
206        }
207
208        match self {
209            RawCondition::And(_, _) => {
210                let mut terms: BTreeSet<RawCondition> = Default::default();
211                self.visit_and(&mut |x| { terms.insert(x.simpl()); });
212
213                //  a      & (a | b)     ---> a
214                // (a | b) & (a | b | c) ---> a | b
215                hetero_simpl!(terms: Or, visit_or);
216
217                //  a & !( a & b) --->  a & !b
218                //  a & !(!a & b) --->  a
219                // !a & !( a & b) ---> !a
220                homo_simpl!(terms: And, visit_and, true);
221
222                terms.remove(&RawCondition::Const(true));
223                if terms.contains(&RawCondition::Const(false)) || terms.iter().any(|t| if let RawCondition::Not(t) = t { terms.contains(t) } else { false }) {
224                    return RawCondition::Const(false);
225                }
226
227                terms.into_iter().reduce(|a, b| a & b).unwrap_or(RawCondition::Const(true))
228            }
229            RawCondition::Or(_, _) => {
230                let mut terms: BTreeSet<RawCondition> = Default::default();
231                self.visit_or(&mut |x| { terms.insert(x.simpl()); });
232
233                //  a      | (a & b)     ---> a
234                // (a & b) | (a & b & c) ---> a & b
235                hetero_simpl!(terms: And, visit_and);
236
237                //  a | !( a | b) --->  a | !b
238                //  a | !(!a | b) --->  a
239                // !a | !( a | b) ---> !a
240                homo_simpl!(terms: Or, visit_or, false);
241
242                terms.remove(&RawCondition::Const(false));
243                if terms.contains(&RawCondition::Const(true)) || terms.iter().any(|t| if let RawCondition::Not(t) = t { terms.contains(t) } else { false }) {
244                    return RawCondition::Const(true);
245                }
246
247                terms.into_iter().reduce(|a, b| a | b).unwrap_or(RawCondition::Const(false))
248            }
249            RawCondition::Not(x) => match &**x {
250                RawCondition::Const(x) => RawCondition::Const(!x),
251                RawCondition::Not(x) => x.simpl(),
252                x => RawCondition::Not(Box::new(x.simpl())),
253            }
254            x => x.clone(),
255        }
256    }
257}
258
259#[test]
260fn test_simpl() {
261    let a = RawCondition::Atom("a".into());
262    let b = RawCondition::Atom("b".into());
263    let c = RawCondition::Atom("c".into());
264    let d = RawCondition::Atom("d".into());
265    let e = RawCondition::Atom("x < 10".into());
266    let f = RawCondition::Atom("y == x + 10".into());
267
268    let bt = RawCondition::Const(true);
269    let bf = RawCondition::Const(false);
270
271    assert_eq!((a.clone() & a.clone()).simpl().to_string(), "a");
272    assert_eq!((a.clone() & c.clone() & a.clone()).simpl().to_string(), "a & c");
273    assert_eq!((a.clone() & (c.clone() & a.clone())).simpl().to_string(), "a & c");
274    assert_eq!((a.clone() & ((c.clone() | c.clone()) & a.clone())).simpl().to_string(), "a & c");
275    assert_eq!((a.clone() & ((c.clone() | c.clone() | c.clone()) & a.clone())).simpl().to_string(), "a & c");
276
277    assert_eq!((a.clone() | a.clone()).simpl().to_string(), "a");
278    assert_eq!((a.clone() | c.clone() | a.clone()).simpl().to_string(), "a | c");
279    assert_eq!((a.clone() | (c.clone() | a.clone())).simpl().to_string(), "a | c");
280    assert_eq!((a.clone() | ((c.clone() & c.clone()) | a.clone())).simpl().to_string(), "a | c");
281    assert_eq!((a.clone() | ((c.clone() & c.clone() & c.clone()) | a.clone())).simpl().to_string(), "a | c");
282
283    assert_eq!((!f.clone()).simpl().to_string(), "~(y == x + 10)");
284    assert_eq!((!!f.clone()).simpl().to_string(), "y == x + 10");
285    assert_eq!((!!!f.clone()).simpl().to_string(), "~(y == x + 10)");
286    assert_eq!((!!!!f.clone()).simpl().to_string(), "y == x + 10");
287
288    assert_eq!((!(a.clone() | a.clone())).simpl().to_string(), "~a");
289    assert_eq!((!(a.clone() & a.clone())).simpl().to_string(), "~a");
290
291    assert_eq!((bf.clone() & bf.clone()).simpl().to_string(), "false");
292    assert_eq!((bf.clone() & bt.clone()).simpl().to_string(), "false");
293    assert_eq!((bt.clone() & bf.clone()).simpl().to_string(), "false");
294    assert_eq!((bt.clone() & bt.clone()).simpl().to_string(), "true");
295
296    assert_eq!((bf.clone() | bf.clone()).simpl().to_string(), "false");
297    assert_eq!((bf.clone() | bt.clone()).simpl().to_string(), "true");
298    assert_eq!((bt.clone() | bf.clone()).simpl().to_string(), "true");
299    assert_eq!((bt.clone() | bt.clone()).simpl().to_string(), "true");
300
301    assert_eq!((a.clone() & bt.clone()).simpl().to_string(), "a");
302    assert_eq!((bt.clone() & a.clone() & bt.clone()).simpl().to_string(), "a");
303
304    assert_eq!((a.clone() | bf.clone()).simpl().to_string(), "a");
305    assert_eq!((bf.clone() | a.clone() | bf.clone()).simpl().to_string(), "a");
306
307    assert_eq!((a.clone() & bf.clone()).simpl().to_string(), "false");
308    assert_eq!((a.clone() | bt.clone()).simpl().to_string(), "true");
309
310    assert_eq!((a.clone() | (a.clone() & b.clone())).simpl().to_string(), "a");
311    assert_eq!(((a.clone() & b.clone()) | (a.clone() & b.clone())).simpl().to_string(), "a & b");
312    assert_eq!(((a.clone() & b.clone()) | (a.clone() & c.clone() & b.clone())).simpl().to_string(), "a & b");
313    assert_eq!(((a.clone() & c.clone() & b.clone() & c.clone()) | (a.clone() & b.clone())).simpl().to_string(), "a & b");
314    assert_eq!(((a.clone() & c.clone() & b.clone() & c.clone()) | b.clone() | (a.clone() & b.clone())).simpl().to_string(), "b");
315    assert_eq!(((a.clone() & c.clone() & b.clone() & c.clone()) | b.clone() | (a.clone() & d.clone() & b.clone())).simpl().to_string(), "b");
316    assert_eq!(((a.clone() & c.clone() & b.clone() & c.clone()) | (b.clone() & c.clone()) | (a.clone() & d.clone() & b.clone())).simpl().to_string(), "(b & c) | (a & b & d)");
317    assert_eq!(((a.clone() & c.clone() & b.clone() & c.clone()) | (b.clone() & c.clone()) | (a.clone() & c.clone() & b.clone())).simpl().to_string(), "b & c");
318
319    assert_eq!((a.clone() & (a.clone() | b.clone())).simpl().to_string(), "a");
320    assert_eq!(((a.clone() | b.clone()) & (a.clone() | b.clone())).simpl().to_string(), "a | b");
321    assert_eq!(((a.clone() | b.clone()) & (a.clone() | b.clone() | c.clone())).simpl().to_string(), "a | b");
322    assert_eq!(((a.clone() | c.clone() | b.clone() | c.clone()) & (a.clone() | b.clone())).simpl().to_string(), "a | b");
323    assert_eq!(((a.clone() | c.clone() | b.clone() | c.clone()) & b.clone() & (a.clone() | b.clone())).simpl().to_string(), "b");
324    assert_eq!(((a.clone() | c.clone() | b.clone() | c.clone()) & b.clone() & (a.clone() | d.clone() | b.clone())).simpl().to_string(), "b");
325    assert_eq!(((a.clone() | c.clone() | b.clone() | c.clone()) & (b.clone() | c.clone()) & (a.clone() | d.clone() | b.clone())).simpl().to_string(), "(b | c) & (a | b | d)");
326    assert_eq!(((a.clone() | c.clone() | b.clone() | c.clone()) & (b.clone() | c.clone()) & (a.clone() | c.clone() | b.clone())).simpl().to_string(), "b | c");
327
328    assert_eq!((e.clone() | !e.clone()).simpl().to_string(), "true");
329    assert_eq!((!!e.clone() | !e.clone()).simpl().to_string(), "true");
330    assert_eq!((!!e.clone() | !!!e.clone()).simpl().to_string(), "true");
331
332    assert_eq!((e.clone() & !e.clone()).simpl().to_string(), "false");
333    assert_eq!((!!e.clone() & !e.clone()).simpl().to_string(), "false");
334    assert_eq!((!!e.clone() & !!!e.clone()).simpl().to_string(), "false");
335
336    assert_eq!((!bt.clone()).simpl().to_string(), "false");
337    assert_eq!((!!bt.clone()).simpl().to_string(), "true");
338    assert_eq!((!!!bt.clone()).simpl().to_string(), "false");
339    assert_eq!((!!!!bt.clone()).simpl().to_string(), "true");
340
341    assert_eq!((!bf.clone()).simpl().to_string(), "true");
342    assert_eq!((!!bf.clone()).simpl().to_string(), "false");
343    assert_eq!((!!!bf.clone()).simpl().to_string(), "true");
344    assert_eq!((!!!!bf.clone()).simpl().to_string(), "false");
345
346    assert_eq!((a.clone() & !(a.clone() & b.clone())).simpl().to_string(), "a & ~b");
347    assert_eq!((a.clone() | !(a.clone() | b.clone())).simpl().to_string(), "a | ~b");
348
349    assert_eq!((a.clone() & b.clone() & !(a.clone() & b.clone())).simpl().to_string(), "false");
350    assert_eq!((a.clone() | b.clone() | !(a.clone() | b.clone())).simpl().to_string(), "true");
351
352    assert_eq!((!a.clone() & !(a.clone() & b.clone())).simpl().to_string(), "~a");
353    assert_eq!((!a.clone() | !(a.clone() | b.clone())).simpl().to_string(), "~a");
354
355    assert_eq!((a.clone() & !(!a.clone() & b.clone())).simpl().to_string(), "a");
356    assert_eq!((a.clone() | !(!a.clone() | b.clone())).simpl().to_string(), "a");
357}
358
359#[derive(Clone, PartialEq, Eq, PartialOrd, Ord)]
360pub struct Condition(RawCondition);
361impl Condition {
362    pub fn raw(&self) -> &RawCondition {
363        &self.0
364    }
365    pub fn atom(v: CompactString) -> Self {
366        debug_assert!(v != "true" && v != "false" && !v.is_empty());
367        Condition(RawCondition::Atom(v))
368    }
369    pub fn constant(v: bool) -> Self {
370        Condition(RawCondition::Const(v))
371    }
372}
373impl fmt::Display for Condition {
374    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
375        write!(f, "{}", self.0)
376    }
377}
378impl fmt::Debug for Condition {
379    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
380        write!(f, "{}", self.0)
381    }
382}
383impl BitAnd for Condition {
384    type Output = Self;
385    fn bitand(self, rhs: Self) -> Self::Output {
386        let res = (self.0 & rhs.0).simpl();
387        debug_assert_eq!(res, res.simpl());
388        Condition(res)
389    }
390}
391impl BitOr for Condition {
392    type Output = Self;
393    fn bitor(self, rhs: Self) -> Self::Output {
394        let res = (self.0 | rhs.0).simpl();
395        debug_assert_eq!(res, res.simpl());
396        Condition(res)
397    }
398}
399impl Not for Condition {
400    type Output = Self;
401    fn not(self) -> Self::Output {
402        let res = (!self.0).simpl();
403        debug_assert_eq!(res, res.simpl());
404        Condition(res)
405    }
406}
netsblox_stateflow/condition.rs

netsblox_stateflow/
condition.rs
