taco_threshold_automaton/lia_threshold_automaton/general_to_lia/
remove_boolean_neg.rs

1//! Logic to remove boolean negations from an expression
2//!
3//! This module defines the new type [`NonNegatedBooleanExpression`] which is a
4//! restricted variant of boolean expressions, as it does not allow for boolean
5//! negations, that is the `!` operator is not allowed.
6//!
7//! Every [`BooleanExpression`] can be converted into a
8//! `NonNegatedBooleanExpression`, as the negations can be removed by pushing
9//! them into the formula, potentially negating inner comparison expressions.
10
11use std::fmt::{Debug, Display};
12
13use crate::expressions::{
14    Atomic, BooleanConnective, BooleanExpression, ComparisonOp, IntegerExpression,
15};
16
17impl<T: Atomic> BooleanExpression<T> {
18    /// Remove boolean negations from an expression, transforming the expression
19    /// into a `NonNegatedBooleanExpression`.
20    ///
21    /// This function removes a boolean negation by pushing it inwards and
22    /// transforming the expression accordingly.
23    ///
24    /// # Example
25    ///
26    /// ```rust, ignore
27    /// // !(x > 0)
28    /// let expr = BooleanExpression::Not(Box::new(BooleanExpression::ComparisonExpression(
29    ///    Box::new(IntegerExpression::Atom(Variable::new("x"))),
30    ///    ComparisonOp::Gt,
31    ///    Box::new(IntegerExpression::Const(0)),
32    /// )));
33    ///
34    /// // !(x > 0) -> x <= 0
35    /// let transformed_expr = expr.remove_boolean_negations();
36    ///
37    /// assert_eq!(
38    ///    transformed_expr,
39    ///    NonNegatedBooleanExpression::ComparisonExpression(
40    ///         Box::new(IntegerExpression::Atom(Variable::new("x"))),
41    ///         ComparisonOp::Leq,
42    ///         Box::new(IntegerExpression::Const(0)),
43    ///    ),
44    /// );
45    /// ```
46    ///
47    /// # Implementation
48    ///
49    /// The goal of this function is to remove all boolean negations from an
50    /// expression. This is done by recursively traversing the expression, if a
51    /// negation i.e. `Not` is encountered, the negation is pushed inwards using
52    /// the helper function `negate_expression`.
53    ///
54    /// The helper function then:
55    ///     - replaces a [`BooleanExpression::True`] constant with a
56    ///       [`BooleanExpression::False`] and vice versa
57    ///     - calls [`BooleanExpression::remove_boolean_negations`] again if
58    ///       another [`BooleanExpression::Not`] is encountered (double negation)
59    ///     - inverts the comparison operator if a comparison expression is
60    ///       encountered
61    ///     - inverts the boolean connective if a binary expression is encountered
62    ///       and continues recursively on the left and right side of the
63    ///       binary expression
64    pub fn remove_boolean_negations(&self) -> NonNegatedBooleanExpression<T> {
65        match self {
66            BooleanExpression::ComparisonExpression(lhs, comparison_op, rhs) => {
67                NonNegatedBooleanExpression::ComparisonExpression(
68                    lhs.clone(),
69                    *comparison_op,
70                    rhs.clone(),
71                )
72            }
73            BooleanExpression::True => NonNegatedBooleanExpression::True,
74            BooleanExpression::False => NonNegatedBooleanExpression::False,
75            BooleanExpression::BinaryExpression(lhs, op, rhs) => {
76                NonNegatedBooleanExpression::BinaryExpression(
77                    Box::new(lhs.remove_boolean_negations()),
78                    *op,
79                    Box::new(rhs.remove_boolean_negations()),
80                )
81            }
82            BooleanExpression::Not(inner_expr) => inner_expr.negate_expression(),
83        }
84    }
85
86    /// Computes the negation of an expression and removes any inner negations.
87    ///
88    /// Helper function for [`BooleanExpression::remove_boolean_negations`],
89    /// called when a negation is encountered to remove it by pushing it
90    /// inwards.
91    fn negate_expression(&self) -> NonNegatedBooleanExpression<T> {
92        match self {
93            BooleanExpression::ComparisonExpression(lhs, op, rhs) => {
94                NonNegatedBooleanExpression::ComparisonExpression(
95                    lhs.clone(),
96                    op.invert(),
97                    rhs.clone(),
98                )
99            }
100            BooleanExpression::BinaryExpression(lhs, op, rhs) => {
101                NonNegatedBooleanExpression::BinaryExpression(
102                    Box::new(lhs.negate_expression()),
103                    op.invert(),
104                    Box::new(rhs.negate_expression()),
105                )
106            }
107            BooleanExpression::Not(ex) => ex.remove_boolean_negations(),
108            BooleanExpression::True => NonNegatedBooleanExpression::False,
109            BooleanExpression::False => NonNegatedBooleanExpression::True,
110        }
111    }
112}
113
114impl<T: Atomic> From<BooleanExpression<T>> for NonNegatedBooleanExpression<T> {
115    fn from(val: BooleanExpression<T>) -> Self {
116        val.remove_boolean_negations()
117    }
118}
119
120/// Boolean expressions that do not contain a `Not`
121#[derive(Debug, PartialEq, Clone)]
122pub enum NonNegatedBooleanExpression<T: Atomic> {
123    /// Comparison between two integer expressions
124    ComparisonExpression(
125        Box<IntegerExpression<T>>,
126        ComparisonOp,
127        Box<IntegerExpression<T>>,
128    ),
129    /// Boolean expressions combined through boolean connective
130    BinaryExpression(
131        Box<NonNegatedBooleanExpression<T>>,
132        BooleanConnective,
133        Box<NonNegatedBooleanExpression<T>>,
134    ),
135    /// true
136    True,
137    /// false
138    False,
139}
140
141impl<T: Atomic> Display for NonNegatedBooleanExpression<T> {
142    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
143        match self {
144            NonNegatedBooleanExpression::ComparisonExpression(lhs, op, rhs) => {
145                write!(f, "{lhs} {op} {rhs}")
146            }
147            NonNegatedBooleanExpression::BinaryExpression(lhs, op, rhs) => {
148                write!(f, "({lhs}) {op} ({rhs})")
149            }
150            NonNegatedBooleanExpression::True => write!(f, "true"),
151            NonNegatedBooleanExpression::False => write!(f, "false"),
152        }
153    }
154}
155
156#[cfg(test)]
157mod test {
158    // This set of tests uses a private interface, therefore might be removed
159    // However, they are extremely useful for debugging.
160    mod tests_remove_boolean_negations {
161
162        use crate::{
163            expressions::{
164                BooleanConnective, BooleanExpression, ComparisonOp, IntegerExpression, Variable,
165            },
166            lia_threshold_automaton::general_to_lia::remove_boolean_neg::NonNegatedBooleanExpression,
167        };
168
169        #[test]
170        fn test_remove_negation_comparison_expression1() {
171            let expr = BooleanExpression::Not(Box::new(BooleanExpression::ComparisonExpression(
172                Box::new(IntegerExpression::Atom(Variable::new("x"))),
173                ComparisonOp::Eq,
174                Box::new(IntegerExpression::Atom(Variable::new("y"))),
175            )));
176            let expected_expr = NonNegatedBooleanExpression::ComparisonExpression(
177                Box::new(IntegerExpression::Atom(Variable::new("x"))),
178                ComparisonOp::Neq,
179                Box::new(IntegerExpression::Atom(Variable::new("y"))),
180            );
181
182            let got_expr = expr.remove_boolean_negations();
183
184            assert_eq!(got_expr, expected_expr);
185        }
186
187        #[test]
188        fn test_remove_negation_comparison_expression2() {
189            let expr = BooleanExpression::Not(Box::new(BooleanExpression::ComparisonExpression(
190                Box::new(IntegerExpression::Atom(Variable::new("x"))),
191                ComparisonOp::Neq,
192                Box::new(IntegerExpression::Const(1)),
193            )));
194            let expected_expr = NonNegatedBooleanExpression::ComparisonExpression(
195                Box::new(IntegerExpression::Atom(Variable::new("x"))),
196                ComparisonOp::Eq,
197                Box::new(IntegerExpression::Const(1)),
198            );
199
200            let got_expr = expr.remove_boolean_negations();
201
202            assert_eq!(got_expr, expected_expr);
203        }
204
205        #[test]
206        fn test_remove_negation_boolean_con_inner() {
207            let expr = BooleanExpression::BinaryExpression(
208                Box::new(BooleanExpression::Not(Box::new(
209                    BooleanExpression::ComparisonExpression(
210                        Box::new(IntegerExpression::Atom(Variable::new("x"))),
211                        ComparisonOp::Gt,
212                        Box::new(IntegerExpression::Const(5)),
213                    ),
214                ))),
215                BooleanConnective::And,
216                Box::new(BooleanExpression::ComparisonExpression(
217                    Box::new(IntegerExpression::Atom(Variable::new("y"))),
218                    ComparisonOp::Leq,
219                    Box::new(IntegerExpression::Atom(Variable::new("z"))),
220                )),
221            );
222
223            let expected_expr = NonNegatedBooleanExpression::BinaryExpression(
224                Box::new(NonNegatedBooleanExpression::ComparisonExpression(
225                    Box::new(IntegerExpression::Atom(Variable::new("x"))),
226                    ComparisonOp::Leq,
227                    Box::new(IntegerExpression::Const(5)),
228                )),
229                BooleanConnective::And,
230                Box::new(NonNegatedBooleanExpression::ComparisonExpression(
231                    Box::new(IntegerExpression::Atom(Variable::new("y"))),
232                    ComparisonOp::Leq,
233                    Box::new(IntegerExpression::Atom(Variable::new("z"))),
234                )),
235            );
236
237            let got_expr = expr.remove_boolean_negations();
238
239            assert_eq!(got_expr, expected_expr);
240        }
241
242        #[test]
243        fn test_remove_negation_boolean_con_outer() {
244            let expr = BooleanExpression::Not(Box::new(BooleanExpression::BinaryExpression(
245                Box::new(BooleanExpression::ComparisonExpression(
246                    Box::new(IntegerExpression::Atom(Variable::new("x"))),
247                    ComparisonOp::Geq,
248                    Box::new(IntegerExpression::Const(5)),
249                )),
250                BooleanConnective::Or,
251                Box::new(BooleanExpression::ComparisonExpression(
252                    Box::new(IntegerExpression::Atom(Variable::new("y"))),
253                    ComparisonOp::Lt,
254                    Box::new(IntegerExpression::Atom(Variable::new("z"))),
255                )),
256            )));
257
258            let expected_expr = NonNegatedBooleanExpression::BinaryExpression(
259                Box::new(NonNegatedBooleanExpression::ComparisonExpression(
260                    Box::new(IntegerExpression::Atom(Variable::new("x"))),
261                    ComparisonOp::Lt,
262                    Box::new(IntegerExpression::Const(5)),
263                )),
264                BooleanConnective::And,
265                Box::new(NonNegatedBooleanExpression::ComparisonExpression(
266                    Box::new(IntegerExpression::Atom(Variable::new("y"))),
267                    ComparisonOp::Geq,
268                    Box::new(IntegerExpression::Atom(Variable::new("z"))),
269                )),
270            );
271
272            let got_expr = expr.remove_boolean_negations();
273
274            assert_eq!(got_expr, expected_expr);
275        }
276
277        #[test]
278        fn test_remove_negation_boolean_con_outer_and_inner() {
279            let expr = BooleanExpression::Not(Box::new(BooleanExpression::BinaryExpression(
280                Box::new(BooleanExpression::Not(Box::new(BooleanExpression::Not(
281                    Box::new(BooleanExpression::Not(Box::new(
282                        BooleanExpression::ComparisonExpression(
283                            Box::new(IntegerExpression::Atom(Variable::new("x"))),
284                            ComparisonOp::Neq,
285                            Box::new(IntegerExpression::Const(5)),
286                        ),
287                    ))),
288                )))),
289                BooleanConnective::And,
290                Box::new(BooleanExpression::Not(Box::new(BooleanExpression::Not(
291                    Box::new(BooleanExpression::ComparisonExpression(
292                        Box::new(IntegerExpression::Atom(Variable::new("y"))),
293                        ComparisonOp::Leq,
294                        Box::new(IntegerExpression::Atom(Variable::new("z"))),
295                    )),
296                )))),
297            )));
298
299            let expected_expr = NonNegatedBooleanExpression::BinaryExpression(
300                Box::new(NonNegatedBooleanExpression::ComparisonExpression(
301                    Box::new(IntegerExpression::Atom(Variable::new("x"))),
302                    ComparisonOp::Neq,
303                    Box::new(IntegerExpression::Const(5)),
304                )),
305                BooleanConnective::Or,
306                Box::new(NonNegatedBooleanExpression::ComparisonExpression(
307                    Box::new(IntegerExpression::Atom(Variable::new("y"))),
308                    ComparisonOp::Gt,
309                    Box::new(IntegerExpression::Atom(Variable::new("z"))),
310                )),
311            );
312
313            let got_expr = NonNegatedBooleanExpression::<Variable>::from(expr);
314
315            assert_eq!(got_expr, expected_expr);
316        }
317
318        #[test]
319        fn test_remove_negation_constants() {
320            let expr: BooleanExpression<Variable> = BooleanExpression::True;
321            assert_eq!(
322                NonNegatedBooleanExpression::<Variable>::from(expr),
323                NonNegatedBooleanExpression::True
324            );
325
326            let expr = BooleanExpression::<Variable>::False;
327            assert_eq!(
328                NonNegatedBooleanExpression::<Variable>::from(expr),
329                NonNegatedBooleanExpression::False
330            );
331
332            let expr = BooleanExpression::Not(Box::new(BooleanExpression::<Variable>::True));
333            assert_eq!(
334                NonNegatedBooleanExpression::<Variable>::from(expr),
335                NonNegatedBooleanExpression::False
336            );
337
338            let expr = BooleanExpression::Not(Box::new(BooleanExpression::<Variable>::False));
339            assert_eq!(
340                NonNegatedBooleanExpression::<Variable>::from(expr),
341                NonNegatedBooleanExpression::True
342            );
343        }
344
345        #[test]
346        fn test_display_non_negated_boolean_expression() {
347            let expr = NonNegatedBooleanExpression::ComparisonExpression(
348                Box::new(IntegerExpression::Atom(Variable::new("x"))),
349                ComparisonOp::Eq,
350                Box::new(IntegerExpression::Const(5)),
351            );
352
353            let expected_str = "x == 5";
354            assert_eq!(expr.to_string(), expected_str);
355
356            let expr = NonNegatedBooleanExpression::BinaryExpression(
357                Box::new(NonNegatedBooleanExpression::ComparisonExpression(
358                    Box::new(IntegerExpression::Atom(Variable::new("x"))),
359                    ComparisonOp::Eq,
360                    Box::new(IntegerExpression::Const(5)),
361                )),
362                BooleanConnective::And,
363                Box::new(NonNegatedBooleanExpression::ComparisonExpression(
364                    Box::new(IntegerExpression::Atom(Variable::new("y"))),
365                    ComparisonOp::Neq,
366                    Box::new(IntegerExpression::Const(3)),
367                )),
368            );
369
370            let expected_str = "(x == 5) && (y != 3)";
371            assert_eq!(expr.to_string(), expected_str);
372
373            let expr: NonNegatedBooleanExpression<Variable> = NonNegatedBooleanExpression::True;
374            let expected_str = "true";
375            assert_eq!(expr.to_string(), expected_str);
376
377            let expr: NonNegatedBooleanExpression<Variable> = NonNegatedBooleanExpression::False;
378            let expected_str = "false";
379            assert_eq!(expr.to_string(), expected_str);
380        }
381    }
382}
taco_threshold_automaton/lia_threshold_automaton/general_to_lia/remove_boolean_neg.rs

taco_threshold_automaton/lia_threshold_automaton/general_to_lia/
remove_boolean_neg.rs
