taco_threshold_automaton/lia_threshold_automaton/general_to_lia/
remove_minus.rs

1//! Remove unary negations and subtractions from integer expressions
2//!
3//! This module defines a new type [`NonMinusIntegerExpr`] that represents a
4//! restricted integer expression which does not contain the sub operator
5//! nor unary negations. However, it does have support for negated constants.
6//!
7//! Any [`IntegerExpression`] can be converted into a [`NonMinusIntegerExpr`],
8//! by pushing the negation inwards until they can be applied to a constant or
9//! until a factor of -1 can be added to an atom.
10
11use std::fmt::{Debug, Display};
12
13use crate::expressions::{Atomic, IntegerExpression, IntegerOp, Parameter};
14
15/// Integer expression that does not contain a minus operator, i.e., no negations
16/// or subtractions, only negated constants are allowed.
17#[derive(Debug, PartialEq, Clone)]
18pub enum NonMinusIntegerExpr<T: Atomic> {
19    /// Atomic of type T
20    Atom(T),
21    /// Integer constant
22    Const(u32),
23    /// Negated integer constant
24    NegConst(u32),
25    /// Parameter
26    Param(Parameter),
27    /// Integer expression combining two Integer expressions through an
28    /// arithmetic operator
29    BinaryExpr(
30        Box<NonMinusIntegerExpr<T>>,
31        NonMinusIntegerOp,
32        Box<NonMinusIntegerExpr<T>>,
33    ),
34}
35
36impl<T: Atomic> From<IntegerExpression<T>> for NonMinusIntegerExpr<T> {
37    fn from(val: IntegerExpression<T>) -> Self {
38        val.remove_unary_neg_and_sub()
39    }
40}
41
42impl<T: Atomic> Display for NonMinusIntegerExpr<T> {
43    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
44        match self {
45            NonMinusIntegerExpr::Atom(atom) => write!(f, "{atom}"),
46            NonMinusIntegerExpr::Const(c) => write!(f, "{c}"),
47            NonMinusIntegerExpr::NegConst(c) => write!(f, "-{c}"),
48            NonMinusIntegerExpr::Param(param) => write!(f, "{param}"),
49            NonMinusIntegerExpr::BinaryExpr(lhs, op, rhs) => {
50                write!(f, "({lhs} {op} {rhs})")
51            }
52        }
53    }
54}
55
56/// Arithmetic operators without -
57#[derive(Debug, PartialEq, Clone, Copy)]
58pub enum NonMinusIntegerOp {
59    /// +
60    Add,
61    /// *
62    Mul,
63    /// /
64    Div,
65}
66
67impl From<IntegerOp> for NonMinusIntegerOp {
68    /// Convert an [`IntegerOp`] to a NonMinusIntegerOp
69    ///
70    /// Panics if the [`IntegerOp`] is a subtraction operator
71    fn from(op: IntegerOp) -> Self {
72        match op {
73            IntegerOp::Add => NonMinusIntegerOp::Add,
74            IntegerOp::Mul => NonMinusIntegerOp::Mul,
75            IntegerOp::Div => NonMinusIntegerOp::Div,
76            IntegerOp::Sub => unreachable!("Subtraction should have been removed"),
77        }
78    }
79}
80
81impl From<NonMinusIntegerOp> for IntegerOp {
82    fn from(op: NonMinusIntegerOp) -> Self {
83        match op {
84            NonMinusIntegerOp::Add => IntegerOp::Add,
85            NonMinusIntegerOp::Mul => IntegerOp::Mul,
86            NonMinusIntegerOp::Div => IntegerOp::Div,
87        }
88    }
89}
90
91impl Display for NonMinusIntegerOp {
92    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
93        match self {
94            NonMinusIntegerOp::Add => write!(f, "+"),
95            NonMinusIntegerOp::Mul => write!(f, "*"),
96            NonMinusIntegerOp::Div => write!(f, "/"),
97        }
98    }
99}
100
101impl<T: Atomic> IntegerExpression<T> {
102    /// Remove unary negations and subtractions from the integer expression
103    /// such that there are only negated constants.
104    ///
105    /// # Implementation
106    ///
107    /// The function recursively traverses the expression tree and pushes
108    /// negations inwards until they are in front of constants, atoms, or
109    /// parameters. In the latter two cases, it adds a `-1 *` in front of the
110    /// atom or parameter.
111    ///
112    /// # Example
113    ///
114    /// ```rust,ignore
115    ///
116    /// // 1 - (n + -5)
117    /// let expr = IntegerExpression::BinaryExpr(
118    ///     Box::new(IntegerExpression::Const(1)),
119    ///     IntegerOp::Sub,
120    ///     Box::new(IntegerExpression::BinaryExpr(
121    ///         Box::new(IntegerExpression::Param(Parameter::new("n"))),
122    ///         IntegerOp::Add,
123    ///         Box::new(IntegerExpression::Neg(Box::new(IntegerExpression::Const(5)))),
124    ///     )),
125    /// );
126    ///
127    /// // 1 + (-1 * n + 5)
128    /// let expected_expr : NonMinusIntegerExpr<Variable> = NonMinusIntegerExpr::BinaryExpr(
129    ///     Box::new(NonMinusIntegerExpr::Const(1)),
130    ///     NonMinusIntegerOp::Add,
131    ///     Box::new(NonMinusIntegerExpr::BinaryExpr(
132    ///         Box::new(
133    ///             NonMinusIntegerExpr::BinaryExpr(
134    ///                 Box::new(NonMinusIntegerExpr::NegConst(1)),
135    ///                 NonMinusIntegerOp::Mul,
136    ///                 Box::new(NonMinusIntegerExpr::Param(Parameter::new("n"))),
137    ///            )
138    ///         ),
139    ///         NonMinusIntegerOp::Add,
140    ///         Box::new(NonMinusIntegerExpr::Const(5)),
141    ///     )),
142    /// );
143    ///     
144    /// let got_expr = expr.remove_unary_neg_and_sub();
145    /// assert_eq!(got_expr, expected_expr);
146    /// ```
147    pub fn remove_unary_neg_and_sub(self) -> NonMinusIntegerExpr<T> {
148        match self {
149            IntegerExpression::Const(c) => NonMinusIntegerExpr::Const(c),
150            IntegerExpression::Param(p) => NonMinusIntegerExpr::Param(p),
151            IntegerExpression::Atom(a) => NonMinusIntegerExpr::Atom(a),
152            IntegerExpression::Neg(ex) => ex.negate_expression(),
153            // Found subtraction, push it inwards on the right hand side
154            IntegerExpression::BinaryExpr(lhs, IntegerOp::Sub, rhs) => {
155                let lhs = lhs.remove_unary_neg_and_sub();
156                let rhs = rhs.negate_expression();
157                NonMinusIntegerExpr::BinaryExpr(
158                    Box::new(lhs),
159                    NonMinusIntegerOp::Add,
160                    Box::new(rhs),
161                )
162            }
163            IntegerExpression::BinaryExpr(lhs, op, rhs) => {
164                let lhs = lhs.remove_unary_neg_and_sub();
165                let rhs = rhs.remove_unary_neg_and_sub();
166                NonMinusIntegerExpr::BinaryExpr(Box::new(lhs), op.into(), Box::new(rhs))
167            }
168        }
169    }
170
171    /// Compute the negation of expression and removes any inner negations or
172    /// subtractions
173    ///
174    /// Helper function for `remove_unary_neg_and_sub`: This function pushes a
175    /// found negation inwards until they are in front of constants, atoms, or
176    /// parameters. In the latter two cases, it adds a -1 * in front of the
177    /// atom or parameter.
178    fn negate_expression(self) -> NonMinusIntegerExpr<T> {
179        match self {
180            IntegerExpression::Const(c) => NonMinusIntegerExpr::NegConst(c),
181            IntegerExpression::Param(p) => NonMinusIntegerExpr::BinaryExpr(
182                Box::new(NonMinusIntegerExpr::NegConst(1)),
183                NonMinusIntegerOp::Mul,
184                Box::new(NonMinusIntegerExpr::Param(p)),
185            ),
186            IntegerExpression::Atom(a) => NonMinusIntegerExpr::BinaryExpr(
187                Box::new(NonMinusIntegerExpr::NegConst(1)),
188                NonMinusIntegerOp::Mul,
189                Box::new(NonMinusIntegerExpr::Atom(a)),
190            ),
191            // Negation found, apply double negation rule and continue eliminating minus from subexpression
192            IntegerExpression::Neg(ex) => ex.remove_unary_neg_and_sub(),
193            // Found inner subtraction: negate left hand side and continue eliminating potential negations from right hand side
194            IntegerExpression::BinaryExpr(lhs, IntegerOp::Sub, rhs) => {
195                let lhs = lhs.negate_expression();
196                let rhs = rhs.remove_unary_neg_and_sub();
197                NonMinusIntegerExpr::BinaryExpr(
198                    Box::new(lhs),
199                    NonMinusIntegerOp::Add,
200                    Box::new(rhs),
201                )
202            }
203            // Addition: continue pushing negation to both subexpressions
204            IntegerExpression::BinaryExpr(lhs, IntegerOp::Add, rhs) => {
205                let lhs = lhs.negate_expression();
206                let rhs = rhs.negate_expression();
207                NonMinusIntegerExpr::BinaryExpr(
208                    Box::new(lhs),
209                    NonMinusIntegerOp::Add,
210                    Box::new(rhs),
211                )
212            }
213            // Multiplication or division: push negation to either lhs or rhs of the expression
214            IntegerExpression::BinaryExpr(lhs, op, rhs) => {
215                // To avoid making the expression more complex (by introducing many `-1 *` factors)
216                // we check whether lhs or rhs has a negation that can be removed by pushing the negation
217                // inwards. If so, we choose the side with the negation.
218                if rhs.has_removable_negation_inside(false) {
219                    NonMinusIntegerExpr::BinaryExpr(
220                        Box::new(lhs.remove_unary_neg_and_sub()),
221                        op.into(),
222                        Box::new(rhs.negate_expression()),
223                    )
224                } else {
225                    NonMinusIntegerExpr::BinaryExpr(
226                        Box::new(lhs.negate_expression()),
227                        op.into(),
228                        Box::new(rhs.remove_unary_neg_and_sub()),
229                    )
230                }
231            }
232        }
233    }
234
235    /// Check whether further down the expression tree there is a negation
236    /// that will be removed if we push the negation inwards.
237    ///
238    /// Helper function for `negate_expression`. To check for a removable
239    /// negation, for expression `ex` call with `has_neg` initially set to
240    /// false, i.e. `ex.has_removable_negation_inside(false)`.
241    fn has_removable_negation_inside(&self, has_neg: bool) -> bool {
242        match self {
243            IntegerExpression::Atom(_)
244            | IntegerExpression::Const(_)
245            | IntegerExpression::Param(_) => has_neg,
246            IntegerExpression::BinaryExpr(lhs, op, rhs) => {
247                if *op == IntegerOp::Sub {
248                    lhs.has_removable_negation_inside(!has_neg)
249                        || rhs.has_removable_negation_inside(!has_neg)
250                } else {
251                    lhs.has_removable_negation_inside(has_neg)
252                        || rhs.has_removable_negation_inside(has_neg)
253                }
254            }
255            IntegerExpression::Neg(ex) => ex.has_removable_negation_inside(!has_neg),
256        }
257    }
258}
259
260impl<T: Atomic> From<NonMinusIntegerExpr<T>> for IntegerExpression<T> {
261    fn from(val: NonMinusIntegerExpr<T>) -> Self {
262        match val {
263            NonMinusIntegerExpr::Atom(a) => IntegerExpression::Atom(a),
264            NonMinusIntegerExpr::Const(c) => IntegerExpression::Const(c),
265            NonMinusIntegerExpr::NegConst(c) => {
266                IntegerExpression::Neg(Box::new(IntegerExpression::Const(c)))
267            }
268            NonMinusIntegerExpr::Param(p) => IntegerExpression::Param(p),
269            NonMinusIntegerExpr::BinaryExpr(lhs, op, rhs) => IntegerExpression::BinaryExpr(
270                Box::new((*lhs).into()),
271                op.into(),
272                Box::new((*rhs).into()),
273            ),
274        }
275    }
276}
277
278#[cfg(test)]
279mod tests {
280
281    use super::*;
282    use crate::expressions::{Location, Variable};
283
284    #[test]
285    fn test_push_neg_to_atomics1() {
286        // -(x - 5)
287        let expr = IntegerExpression::Neg(Box::new(IntegerExpression::BinaryExpr(
288            Box::new(IntegerExpression::Atom(Variable::new("x"))),
289            IntegerOp::Sub,
290            Box::new(IntegerExpression::Const(5)),
291        )));
292
293        // -1 * x + 5
294        let expected_expr = NonMinusIntegerExpr::BinaryExpr(
295            Box::new(NonMinusIntegerExpr::BinaryExpr(
296                Box::new(NonMinusIntegerExpr::NegConst(1)),
297                NonMinusIntegerOp::Mul,
298                Box::new(NonMinusIntegerExpr::Atom(Variable::new("x"))),
299            )),
300            NonMinusIntegerOp::Add,
301            Box::new(NonMinusIntegerExpr::Const(5)),
302        );
303
304        let got_expr = expr.remove_unary_neg_and_sub();
305        assert_eq!(got_expr, expected_expr);
306
307        let got_expr = Into::<IntegerExpression<_>>::into(got_expr);
308        let expected_expr = Into::<IntegerExpression<Variable>>::into(expected_expr);
309        assert_eq!(
310            got_expr.try_to_evaluate_to_const(),
311            expected_expr.try_to_evaluate_to_const()
312        );
313    }
314
315    #[test]
316    fn test_push_neg_to_atomics2() {
317        // -(1 * (3 - 5))
318        let expr: IntegerExpression<Variable> =
319            IntegerExpression::Neg(Box::new(IntegerExpression::BinaryExpr(
320                Box::new(IntegerExpression::Const(1)),
321                IntegerOp::Mul,
322                Box::new(IntegerExpression::BinaryExpr(
323                    Box::new(IntegerExpression::Const(3)),
324                    IntegerOp::Sub,
325                    Box::new(IntegerExpression::Const(5)),
326                )),
327            )));
328
329        // 1 * 3 + 5
330        let expected_expr = NonMinusIntegerExpr::BinaryExpr(
331            Box::new(NonMinusIntegerExpr::Const(1)),
332            NonMinusIntegerOp::Mul,
333            Box::new(NonMinusIntegerExpr::BinaryExpr(
334                Box::new(NonMinusIntegerExpr::NegConst(3)),
335                NonMinusIntegerOp::Add,
336                Box::new(NonMinusIntegerExpr::Const(5)),
337            )),
338        );
339
340        let got_expr = expr.remove_unary_neg_and_sub();
341        assert_eq!(got_expr, expected_expr);
342
343        let got_expr = Into::<IntegerExpression<_>>::into(got_expr);
344        let expected_expr = Into::<IntegerExpression<Variable>>::into(expected_expr);
345        assert_eq!(
346            got_expr.try_to_evaluate_to_const(),
347            expected_expr.try_to_evaluate_to_const()
348        );
349        assert_eq!(got_expr.try_to_evaluate_to_const(), Some(2))
350    }
351
352    #[test]
353    fn test_push_neg_to_atomics3() {
354        // 1 * (3 - 5)
355        let expr: IntegerExpression<Variable> = IntegerExpression::BinaryExpr(
356            Box::new(IntegerExpression::Const(1)),
357            IntegerOp::Mul,
358            Box::new(IntegerExpression::BinaryExpr(
359                Box::new(IntegerExpression::Const(3)),
360                IntegerOp::Sub,
361                Box::new(IntegerExpression::Const(5)),
362            )),
363        );
364
365        // 1 * 3 + -5
366        let expected_expr = NonMinusIntegerExpr::BinaryExpr(
367            Box::new(NonMinusIntegerExpr::Const(1)),
368            NonMinusIntegerOp::Mul,
369            Box::new(NonMinusIntegerExpr::BinaryExpr(
370                Box::new(NonMinusIntegerExpr::Const(3)),
371                NonMinusIntegerOp::Add,
372                Box::new(NonMinusIntegerExpr::NegConst(5)),
373            )),
374        );
375
376        let got_expr = expr.remove_unary_neg_and_sub();
377        assert_eq!(got_expr, expected_expr);
378
379        let got_expr = Into::<IntegerExpression<_>>::into(got_expr);
380        let expected_expr = Into::<IntegerExpression<Variable>>::into(expected_expr);
381        assert_eq!(
382            got_expr.try_to_evaluate_to_const(),
383            expected_expr.try_to_evaluate_to_const()
384        );
385        assert_eq!(got_expr.try_to_evaluate_to_const(), Some(-2))
386    }
387
388    #[test]
389    fn test_push_neg_to_atomics4() {
390        // 42 + -(-3 * 9)
391        let expr: IntegerExpression<Variable> = IntegerExpression::BinaryExpr(
392            Box::new(IntegerExpression::Const(42)),
393            IntegerOp::Add,
394            Box::new(IntegerExpression::Neg(Box::new(
395                IntegerExpression::BinaryExpr(
396                    Box::new(IntegerExpression::Neg(Box::new(IntegerExpression::Const(
397                        3,
398                    )))),
399                    IntegerOp::Mul,
400                    Box::new(IntegerExpression::Const(9)),
401                ),
402            ))),
403        );
404
405        // 42 + 3 * 9
406        let expected_expr = NonMinusIntegerExpr::BinaryExpr(
407            Box::new(NonMinusIntegerExpr::Const(42)),
408            NonMinusIntegerOp::Add,
409            Box::new(NonMinusIntegerExpr::BinaryExpr(
410                Box::new(NonMinusIntegerExpr::Const(3)),
411                NonMinusIntegerOp::Mul,
412                Box::new(NonMinusIntegerExpr::Const(9)),
413            )),
414        );
415
416        let got_expr = expr.remove_unary_neg_and_sub();
417        assert_eq!(got_expr, expected_expr);
418
419        let got_expr: IntegerExpression<_> = got_expr.into();
420        let expected_expr: IntegerExpression<Variable> = expected_expr.into();
421        assert_eq!(
422            got_expr.try_to_evaluate_to_const(),
423            expected_expr.try_to_evaluate_to_const()
424        );
425        assert_eq!(got_expr.try_to_evaluate_to_const(), Some(69))
426    }
427
428    #[test]
429    fn test_push_neg_to_atomics5() {
430        // - (42 + 9 * -3)
431        let expr: IntegerExpression<Variable> =
432            IntegerExpression::Neg(Box::new(IntegerExpression::BinaryExpr(
433                Box::new(IntegerExpression::Const(42)),
434                IntegerOp::Add,
435                Box::new(IntegerExpression::BinaryExpr(
436                    Box::new(IntegerExpression::Const(9)),
437                    IntegerOp::Mul,
438                    Box::new(IntegerExpression::Neg(Box::new(IntegerExpression::Param(
439                        Parameter::new("n"),
440                    )))),
441                )),
442            )));
443
444        // -42 + 9 * 3
445        let expected_expr = NonMinusIntegerExpr::BinaryExpr(
446            Box::new(NonMinusIntegerExpr::NegConst(42)),
447            NonMinusIntegerOp::Add,
448            Box::new(NonMinusIntegerExpr::BinaryExpr(
449                Box::new(NonMinusIntegerExpr::Const(9)),
450                NonMinusIntegerOp::Mul,
451                Box::new(NonMinusIntegerExpr::Param(Parameter::new("n"))),
452            )),
453        );
454
455        let got_expr: NonMinusIntegerExpr<_> = expr.remove_unary_neg_and_sub();
456        assert_eq!(got_expr, expected_expr);
457
458        let got_expr: IntegerExpression<_> = got_expr.into();
459        let expected_expr: IntegerExpression<Variable> = expected_expr.into();
460        assert_eq!(
461            got_expr.try_to_evaluate_to_const(),
462            expected_expr.try_to_evaluate_to_const()
463        );
464        assert_eq!(got_expr.try_to_evaluate_to_const(), None)
465    }
466
467    #[test]
468    fn test_push_neg_to_atomics6() {
469        // - (42  + (9 / 3 * -9))
470        let expr: IntegerExpression<Variable> =
471            IntegerExpression::Neg(Box::new(IntegerExpression::BinaryExpr(
472                Box::new(IntegerExpression::Const(42)),
473                IntegerOp::Add,
474                Box::new(IntegerExpression::BinaryExpr(
475                    Box::new(IntegerExpression::Const(9)),
476                    IntegerOp::Div,
477                    Box::new(IntegerExpression::BinaryExpr(
478                        Box::new(IntegerExpression::Const(3)),
479                        IntegerOp::Mul,
480                        Box::new(IntegerExpression::Neg(Box::new(IntegerExpression::Const(
481                            9,
482                        )))),
483                    )),
484                )),
485            )));
486
487        // -42 + 9 / 3 * 9
488        let expected_expr = NonMinusIntegerExpr::BinaryExpr(
489            Box::new(NonMinusIntegerExpr::NegConst(42)),
490            NonMinusIntegerOp::Add,
491            Box::new(NonMinusIntegerExpr::BinaryExpr(
492                Box::new(NonMinusIntegerExpr::Const(9)),
493                NonMinusIntegerOp::Div,
494                Box::new(NonMinusIntegerExpr::BinaryExpr(
495                    Box::new(NonMinusIntegerExpr::Const(3)),
496                    NonMinusIntegerOp::Mul,
497                    Box::new(NonMinusIntegerExpr::Const(9)),
498                )),
499            )),
500        );
501
502        let got_expr = expr.remove_unary_neg_and_sub();
503        assert_eq!(got_expr, expected_expr);
504
505        let got_expr: IntegerExpression<_> = got_expr.into();
506        let expected_expr: IntegerExpression<Variable> = expected_expr.into();
507        assert_eq!(
508            got_expr.try_to_evaluate_to_const(),
509            expected_expr.try_to_evaluate_to_const()
510        );
511        assert_eq!(got_expr.try_to_evaluate_to_const(), Some(-42))
512    }
513
514    #[test]
515    fn test_push_neg_to_atomics7() {
516        // -1 * - (3 - 5)
517        let expr: IntegerExpression<Variable> = IntegerExpression::BinaryExpr(
518            Box::new(IntegerExpression::Neg(Box::new(IntegerExpression::Const(
519                1,
520            )))),
521            IntegerOp::Mul,
522            Box::new(IntegerExpression::Neg(Box::new(
523                IntegerExpression::BinaryExpr(
524                    Box::new(IntegerExpression::Const(3)),
525                    IntegerOp::Sub,
526                    Box::new(IntegerExpression::Const(5)),
527                ),
528            ))),
529        );
530
531        // -1 * (3 + 5)
532        let expected_expr = NonMinusIntegerExpr::BinaryExpr(
533            Box::new(NonMinusIntegerExpr::NegConst(1)),
534            NonMinusIntegerOp::Mul,
535            Box::new(NonMinusIntegerExpr::BinaryExpr(
536                Box::new(NonMinusIntegerExpr::NegConst(3)),
537                NonMinusIntegerOp::Add,
538                Box::new(NonMinusIntegerExpr::Const(5)),
539            )),
540        );
541
542        let got_expr = expr.remove_unary_neg_and_sub();
543        assert_eq!(got_expr, expected_expr);
544
545        let got_expr: IntegerExpression<_> = got_expr.into();
546        let expected_expr: IntegerExpression<Variable> = expected_expr.into();
547        assert_eq!(
548            got_expr.try_to_evaluate_to_const(),
549            expected_expr.try_to_evaluate_to_const()
550        );
551        assert_eq!(got_expr.try_to_evaluate_to_const(), Some(-2))
552    }
553
554    #[test]
555    fn test_push_neg_to_atomics8() {
556        // - (42 + 9 * (-3 - 5)) )
557        let expr: IntegerExpression<Variable> =
558            IntegerExpression::Neg(Box::new(IntegerExpression::BinaryExpr(
559                Box::new(IntegerExpression::Const(42)),
560                IntegerOp::Add,
561                Box::new(IntegerExpression::BinaryExpr(
562                    Box::new(IntegerExpression::Const(9)),
563                    IntegerOp::Mul,
564                    Box::new(-IntegerExpression::Const(3) - IntegerExpression::Const(5)),
565                )),
566            )));
567
568        // -42 + 9 * (3 + -5)
569        let expected_expr = NonMinusIntegerExpr::BinaryExpr(
570            Box::new(NonMinusIntegerExpr::NegConst(42)),
571            NonMinusIntegerOp::Add,
572            Box::new(NonMinusIntegerExpr::BinaryExpr(
573                Box::new(NonMinusIntegerExpr::Const(9)),
574                NonMinusIntegerOp::Mul,
575                Box::new(NonMinusIntegerExpr::BinaryExpr(
576                    Box::new(NonMinusIntegerExpr::Const(3)),
577                    NonMinusIntegerOp::Add,
578                    Box::new(NonMinusIntegerExpr::Const(5)),
579                )),
580            )),
581        );
582
583        let got_expr = expr.remove_unary_neg_and_sub();
584        assert_eq!(got_expr, expected_expr);
585    }
586
587    #[test]
588    fn test_into_neg_param() {
589        // -n
590        let expr: IntegerExpression<Location> =
591            IntegerExpression::Neg(Box::new(IntegerExpression::Param(Parameter::new("n"))));
592
593        let expected: NonMinusIntegerExpr<Location> = NonMinusIntegerExpr::BinaryExpr(
594            Box::new(NonMinusIntegerExpr::NegConst(1)),
595            NonMinusIntegerOp::Mul,
596            Box::new(NonMinusIntegerExpr::Param(Parameter::new("n"))),
597        );
598
599        assert_eq!(NonMinusIntegerExpr::from(expr), expected);
600
601        let got: IntegerExpression<Location> = Into::<IntegerExpression<_>>::into(expected);
602        let expected: IntegerExpression<Location> =
603            -IntegerExpression::Const(1) * IntegerExpression::Param(Parameter::new("n"));
604        assert_eq!(got, expected);
605
606        // n
607        let expr = IntegerExpression::Atom(Parameter::new("n"));
608
609        let expected = NonMinusIntegerExpr::Atom(Parameter::new("n"));
610
611        assert_eq!(NonMinusIntegerExpr::from(expr), expected);
612    }
613
614    #[test]
615    fn test_display_non_minus_integer_expression() {
616        // 1 / (n + -5)
617        let expr = NonMinusIntegerExpr::BinaryExpr(
618            Box::new(NonMinusIntegerExpr::Const(1)),
619            NonMinusIntegerOp::Div,
620            Box::new(NonMinusIntegerExpr::BinaryExpr(
621                Box::new(NonMinusIntegerExpr::Atom(Parameter::new("n"))),
622                NonMinusIntegerOp::Add,
623                Box::new(NonMinusIntegerExpr::NegConst(5)),
624            )),
625        );
626        assert_eq!(expr.to_string(), "(1 / (n + -5))");
627
628        // 1 + (-1 * n + 5)
629        let expr: NonMinusIntegerExpr<Variable> = NonMinusIntegerExpr::BinaryExpr(
630            Box::new(NonMinusIntegerExpr::Const(1)),
631            NonMinusIntegerOp::Add,
632            Box::new(NonMinusIntegerExpr::BinaryExpr(
633                Box::new(NonMinusIntegerExpr::BinaryExpr(
634                    Box::new(NonMinusIntegerExpr::NegConst(1)),
635                    NonMinusIntegerOp::Mul,
636                    Box::new(NonMinusIntegerExpr::Param(Parameter::new("n"))),
637                )),
638                NonMinusIntegerOp::Add,
639                Box::new(NonMinusIntegerExpr::Const(5)),
640            )),
641        );
642        assert_eq!(expr.to_string(), "(1 + ((-1 * n) + 5))");
643    }
644
645    #[test]
646    #[should_panic]
647    fn test_non_minus_op() {
648        let _ = NonMinusIntegerOp::from(IntegerOp::Sub);
649    }
650}
taco_threshold_automaton/lia_threshold_automaton/general_to_lia/remove_minus.rs

taco_threshold_automaton/lia_threshold_automaton/general_to_lia/
remove_minus.rs
