taco_threshold_automaton/lia_threshold_automaton/general_to_lia/
classify_into_lia.rs

1//! This module contains the logic to transform a general boolean expression
2//! over variables into a [`super::LIAVariableConstraint`].
3//!
4//! The conversion generally works as described in
5//! [`../general_to_lia.rs`](general_to_lia.rs).
6//!
7//! This module implements the logic that after successfully splitting the
8//! expression into pairs of atoms and rational factors, brings all variables to
9//! the left and collects all parameter factor pairs and constants on the right.
10//!
11//! Then the module converts them into the appropriate [`LIAVariableConstraint`]
12//! type, i.e., either a [`SingleAtomConstraint`], [`SumAtomConstraint`] or
13//! [`ComparisonConstraint`].
14
15use std::{collections::HashMap, hash::Hash};
16
17use crate::{
18    BooleanVarConstraint,
19    expressions::{
20        Atomic, BooleanConnective, BooleanExpression, ComparisonOp, IntegerExpression, Variable,
21        fraction::Fraction,
22    },
23    lia_threshold_automaton::{
24        ComparisonConstraint, LIAVariableConstraint, SingleAtomConstraint, SumAtomConstraint,
25        integer_thresholds::{
26            IntoNoDivBooleanExpr, Threshold, ThresholdCompOp, ThresholdConstraint,
27        },
28    },
29};
30
31use super::{ConstraintRewriteError, remove_boolean_neg::NonNegatedBooleanExpression};
32
33impl TryFrom<&BooleanVarConstraint> for LIAVariableConstraint {
34    type Error = ConstraintRewriteError;
35
36    fn try_from(expr: &BooleanExpression<Variable>) -> Result<Self, Self::Error> {
37        let non_negated = expr.remove_boolean_negations();
38        non_negated.try_into()
39    }
40}
41
42impl TryFrom<BooleanVarConstraint> for LIAVariableConstraint {
43    type Error = ConstraintRewriteError;
44
45    fn try_from(expr: BooleanExpression<Variable>) -> Result<Self, Self::Error> {
46        (&expr).try_into()
47    }
48}
49
50impl TryFrom<NonNegatedBooleanExpression<Variable>> for LIAVariableConstraint {
51    type Error = ConstraintRewriteError;
52    /// Parse the `NonNegatedBooleanExpression` into a LIAVariableConstraint by
53    /// converting into weighted sums of parameters and variables
54    fn try_from(value: NonNegatedBooleanExpression<Variable>) -> Result<Self, Self::Error> {
55        match value {
56            NonNegatedBooleanExpression::True => Ok(LIAVariableConstraint::True),
57            NonNegatedBooleanExpression::False => Ok(LIAVariableConstraint::False),
58            NonNegatedBooleanExpression::BinaryExpression(lhs, op, rhs) => {
59                let lhs = (*lhs).try_into()?;
60                let rhs = (*rhs).try_into()?;
61
62                Ok(LIAVariableConstraint::BinaryGuard(
63                    Box::new(lhs),
64                    op,
65                    Box::new(rhs),
66                ))
67            }
68            NonNegatedBooleanExpression::ComparisonExpression(lhs, op, rhs) => {
69                canonicalize_comp_op(*lhs, op, *rhs)
70            }
71        }
72    }
73}
74
75/// Translate the constraints into constraints over the canonical thresholds
76fn canonicalize_comp_op(
77    lhs: IntegerExpression<Variable>,
78    op: ComparisonOp,
79    rhs: IntegerExpression<Variable>,
80) -> Result<LIAVariableConstraint, ConstraintRewriteError> {
81    // Catch trivially true or false constraints and replace them
82    if let Ok(res) =
83        BooleanExpression::ComparisonExpression(Box::new(lhs.clone()), op, Box::new(rhs.clone()))
84            .check_satisfied(&HashMap::new(), &HashMap::new())
85    {
86        if res {
87            return Ok(LIAVariableConstraint::True);
88        }
89        return Ok(LIAVariableConstraint::False);
90    }
91
92    match op {
93        ComparisonOp::Gt => {
94            let op = ThresholdCompOp::Geq;
95            let lhs = lhs - IntegerExpression::Const(1);
96
97            let (variables, thr) = split_pairs_into_atom_and_threshold(lhs, rhs)?;
98            let thr_c = ThresholdConstraint::new_from_thr(op, thr);
99            parse_guard_type(variables, thr_c)
100        }
101        ComparisonOp::Geq => {
102            let (variables, thr) = split_pairs_into_atom_and_threshold(lhs, rhs)?;
103            let thr_c = ThresholdConstraint::new_from_thr(ThresholdCompOp::Geq, thr);
104            parse_guard_type(variables, thr_c)
105        }
106        ComparisonOp::Leq => {
107            let op = ThresholdCompOp::Lt;
108            let rhs = rhs + IntegerExpression::Const(1);
109
110            let (variables, thr) = split_pairs_into_atom_and_threshold(lhs, rhs)?;
111            let thr_c = ThresholdConstraint::new_from_thr(op, thr);
112
113            parse_guard_type(variables, thr_c)
114        }
115        ComparisonOp::Lt => {
116            let (variables, thr) = split_pairs_into_atom_and_threshold(lhs, rhs)?;
117            let thr_c = ThresholdConstraint::new_from_thr(ThresholdCompOp::Lt, thr);
118            parse_guard_type(variables, thr_c)
119        }
120        ComparisonOp::Eq => {
121            let lower_constr = canonicalize_comp_op(lhs.clone(), ComparisonOp::Leq, rhs.clone())?;
122            let upper_constr = canonicalize_comp_op(lhs.clone(), ComparisonOp::Geq, rhs.clone())?;
123
124            Ok(LIAVariableConstraint::BinaryGuard(
125                Box::new(lower_constr),
126                BooleanConnective::And,
127                Box::new(upper_constr),
128            ))
129        }
130        ComparisonOp::Neq => {
131            let lower_constr = canonicalize_comp_op(lhs.clone(), ComparisonOp::Lt, rhs.clone())?;
132            let upper_constr = canonicalize_comp_op(lhs.clone(), ComparisonOp::Gt, rhs.clone())?;
133
134            Ok(LIAVariableConstraint::BinaryGuard(
135                Box::new(lower_constr),
136                BooleanConnective::Or,
137                Box::new(upper_constr),
138            ))
139        }
140    }
141}
142
143/// This function is designed to rewrite an comparison expression into a form
144/// where the returned `HashMap<T, Fraction>` forms the new lhs of the equation
145/// and the returned threshold is the right hand side of the equation
146///
147// TODO: Refactor: remove the pub(crate)
148pub(crate) fn split_pairs_into_atom_and_threshold<T: Atomic>(
149    lhs: IntegerExpression<T>,
150    rhs: IntegerExpression<T>,
151) -> Result<(HashMap<T, Fraction>, Threshold), ConstraintRewriteError> {
152    let lhs = lhs
153        .remove_unary_neg_and_sub()
154        .remove_div()?
155        .split_into_factor_pairs()?;
156
157    let rhs = rhs
158        .remove_unary_neg_and_sub()
159        .remove_div()?
160        .split_into_factor_pairs()?;
161
162    let atoms = combine_pair_iterators(lhs.get_atom_factor_pairs(), rhs.get_atom_factor_pairs());
163
164    let params = combine_pair_iterators(rhs.get_param_factor_pairs(), lhs.get_param_factor_pairs());
165
166    let c = rhs.get_const_factor() - lhs.get_const_factor();
167    let t = Threshold::new(params, c);
168
169    Ok((atoms, t))
170}
171
172fn parse_guard_type(
173    vars: HashMap<Variable, Fraction>,
174    thr_c: ThresholdConstraint,
175) -> Result<LIAVariableConstraint, ConstraintRewriteError> {
176    if vars.is_empty() {
177        // We have caught expressions over only constants in `canonicalize_comp_op`
178        //
179        // The evaluation will fail if the constraint contains parameters
180        // This would mean that the variable expression constraints the
181        // parameters which is not permitted !
182        return Err(ConstraintRewriteError::ParameterConstraint(Box::new(
183            BooleanExpression::ComparisonExpression(
184                Box::new(IntegerExpression::Const(0)),
185                thr_c.get_op().into(),
186                Box::new(thr_c.get_threshold().get_scaled_integer_expression(1)),
187            ),
188        )));
189    }
190
191    if vars.len() == 1 {
192        let (var, factor) = vars.into_iter().next().unwrap();
193        let mut thr = thr_c;
194        thr.scale(factor.inverse());
195
196        let svar_guard = SingleAtomConstraint::new(var, thr);
197
198        return Ok(LIAVariableConstraint::SingleVarConstraint(svar_guard));
199    }
200
201    if let Ok(g) = SumAtomConstraint::try_new(vars.clone(), thr_c.clone()) {
202        return Ok(LIAVariableConstraint::SumVarConstraint(g));
203    }
204
205    Ok(LIAVariableConstraint::ComparisonConstraint(
206        ComparisonConstraint::try_new(vars, thr_c).expect("Failed to categorize guard type."),
207    ))
208}
209
210/// Combine two iterators over pairs of tuples over (T, Fraction) into a single
211/// map from T to [`Fraction`], where all entries from `negated_it` are inserted
212/// negated
213fn combine_pair_iterators<'a, T: Clone + Eq + Hash + 'a>(
214    reg_it: impl Iterator<Item = (&'a T, &'a Fraction)>,
215    negated_it: impl Iterator<Item = (&'a T, &'a Fraction)>,
216) -> HashMap<T, Fraction> {
217    reg_it
218        .map(|(t, f)| (t.clone(), *f))
219        // negate the all factors from `negated_it` and add them to the chain
220        .chain(negated_it.map(|(t, f)| (t.clone(), -*f)))
221        .fold(HashMap::new(), |mut acc, (p, f)| {
222            // if key exists, add the factor, otherwise insert it
223            acc.entry(p).and_modify(|e| *e += f).or_insert(f);
224
225            acc
226        })
227}
228
229#[cfg(test)]
230mod tests {
231    use std::collections::BTreeMap;
232
233    use crate::{
234        expressions::{
235            BooleanConnective, ComparisonOp, IntegerExpression, Parameter, Variable,
236            fraction::Fraction,
237        },
238        lia_threshold_automaton::{
239            ConstraintRewriteError, LIAVariableConstraint, SingleAtomConstraint, SumAtomConstraint,
240            general_to_lia::remove_boolean_neg::NonNegatedBooleanExpression,
241            integer_thresholds::{ThresholdCompOp, ThresholdConstraint},
242        },
243    };
244
245    #[test]
246    fn test_try_into_single_var() {
247        let expr = NonNegatedBooleanExpression::ComparisonExpression(
248            Box::new(IntegerExpression::Atom(Variable::new("var"))),
249            ComparisonOp::Gt,
250            Box::new(IntegerExpression::Const(0)),
251        );
252
253        let expected_expr = LIAVariableConstraint::SingleVarConstraint(SingleAtomConstraint::new(
254            Variable::new("var"),
255            ThresholdConstraint::new(ThresholdCompOp::Geq, Vec::<(Parameter, Fraction)>::new(), 1),
256        ));
257        let got = LIAVariableConstraint::try_from(expr).unwrap();
258        assert_eq!(got, expected_expr);
259    }
260
261    #[test]
262    fn test_try_into_single_var_eq() {
263        let expr = NonNegatedBooleanExpression::ComparisonExpression(
264            Box::new(IntegerExpression::Atom(Variable::new("var"))),
265            ComparisonOp::Eq,
266            Box::new(IntegerExpression::Const(0)),
267        );
268
269        let expected_expr = LIAVariableConstraint::BinaryGuard(
270            Box::new(LIAVariableConstraint::SingleVarConstraint(
271                SingleAtomConstraint::new(
272                    Variable::new("var"),
273                    ThresholdConstraint::new(
274                        ThresholdCompOp::Lt,
275                        Vec::<(Parameter, Fraction)>::new(),
276                        1,
277                    ),
278                ),
279            )),
280            BooleanConnective::And,
281            Box::new(LIAVariableConstraint::SingleVarConstraint(
282                SingleAtomConstraint::new(
283                    Variable::new("var"),
284                    ThresholdConstraint::new(
285                        ThresholdCompOp::Geq,
286                        Vec::<(Parameter, Fraction)>::new(),
287                        0,
288                    ),
289                ),
290            )),
291        );
292        let got = LIAVariableConstraint::try_from(expr).unwrap();
293        assert_eq!(got, expected_expr);
294    }
295
296    #[test]
297    fn test_try_into_single_var_neq() {
298        let expr = NonNegatedBooleanExpression::ComparisonExpression(
299            Box::new(IntegerExpression::Atom(Variable::new("var"))),
300            ComparisonOp::Neq,
301            Box::new(IntegerExpression::Const(1)),
302        );
303
304        let expected_expr = LIAVariableConstraint::BinaryGuard(
305            Box::new(LIAVariableConstraint::SingleVarConstraint(
306                SingleAtomConstraint::new(
307                    Variable::new("var"),
308                    ThresholdConstraint::new(
309                        ThresholdCompOp::Lt,
310                        Vec::<(Parameter, Fraction)>::new(),
311                        1,
312                    ),
313                ),
314            )),
315            BooleanConnective::Or,
316            Box::new(LIAVariableConstraint::SingleVarConstraint(
317                SingleAtomConstraint::new(
318                    Variable::new("var"),
319                    ThresholdConstraint::new(
320                        ThresholdCompOp::Geq,
321                        Vec::<(Parameter, Fraction)>::new(),
322                        2,
323                    ),
324                ),
325            )),
326        );
327        let got = LIAVariableConstraint::try_from(expr).unwrap();
328        assert_eq!(got, expected_expr);
329    }
330
331    #[test]
332    fn test_try_into_single_var_scale_factor_correct() {
333        let expr = NonNegatedBooleanExpression::ComparisonExpression(
334            Box::new(IntegerExpression::Const(2) * IntegerExpression::Atom(Variable::new("var"))),
335            ComparisonOp::Gt,
336            Box::new(IntegerExpression::Const(7)),
337        );
338
339        let expected_expr = LIAVariableConstraint::SingleVarConstraint(SingleAtomConstraint::new(
340            Variable::new("var"),
341            ThresholdConstraint::new(ThresholdCompOp::Geq, Vec::<(Parameter, Fraction)>::new(), 4),
342        ));
343        let got = LIAVariableConstraint::try_from(expr).unwrap();
344        assert_eq!(got, expected_expr);
345    }
346
347    #[test]
348    fn test_simple_guards() {
349        let expr: NonNegatedBooleanExpression<Variable> = NonNegatedBooleanExpression::True;
350        let expected = LIAVariableConstraint::True;
351
352        let result = LIAVariableConstraint::try_from(expr).unwrap();
353        assert_eq!(result, expected);
354
355        let expr: NonNegatedBooleanExpression<Variable> = NonNegatedBooleanExpression::False;
356        let expected = LIAVariableConstraint::False;
357
358        let result = LIAVariableConstraint::try_from(expr).unwrap();
359        assert_eq!(result, expected);
360    }
361
362    #[test]
363    fn test_binary_guard() {
364        // top && top
365        let expr = NonNegatedBooleanExpression::BinaryExpression(
366            Box::new(NonNegatedBooleanExpression::True),
367            BooleanConnective::And,
368            Box::new(NonNegatedBooleanExpression::True),
369        );
370
371        let expected_expr = LIAVariableConstraint::BinaryGuard(
372            Box::new(LIAVariableConstraint::True),
373            BooleanConnective::And,
374            Box::new(LIAVariableConstraint::True),
375        );
376        let got = LIAVariableConstraint::try_from(expr).unwrap();
377        assert_eq!(got, expected_expr);
378
379        //bot || top
380        let expr = NonNegatedBooleanExpression::BinaryExpression(
381            Box::new(NonNegatedBooleanExpression::False),
382            BooleanConnective::Or,
383            Box::new(NonNegatedBooleanExpression::True),
384        );
385
386        let expected_expr = LIAVariableConstraint::BinaryGuard(
387            Box::new(LIAVariableConstraint::False),
388            BooleanConnective::Or,
389            Box::new(LIAVariableConstraint::True),
390        );
391        let got = LIAVariableConstraint::try_from(expr).unwrap();
392        assert_eq!(got, expected_expr);
393    }
394
395    #[test]
396    fn test_try_into_single_var_double_var_lhs() {
397        let expr = NonNegatedBooleanExpression::ComparisonExpression(
398            Box::new(
399                IntegerExpression::Atom(Variable::new("var"))
400                    + IntegerExpression::Atom(Variable::new("var")),
401            ),
402            ComparisonOp::Gt,
403            Box::new(IntegerExpression::Const(1)),
404        );
405
406        let expected_expr = LIAVariableConstraint::SingleVarConstraint(SingleAtomConstraint::new(
407            Variable::new("var"),
408            ThresholdConstraint::new(
409                ThresholdCompOp::Geq,
410                Vec::<(Parameter, Fraction)>::new(),
411                Fraction::new(2, 2, false),
412            ),
413        ));
414        // TODO: consider whether this is fine
415        let got = LIAVariableConstraint::try_from(expr).unwrap();
416        assert_eq!(got, expected_expr);
417    }
418
419    #[test]
420    fn test_try_into_single_var_double_var_rhs() {
421        let expr = NonNegatedBooleanExpression::ComparisonExpression(
422            Box::new(IntegerExpression::Const(1)),
423            ComparisonOp::Leq,
424            Box::new(
425                IntegerExpression::Atom(Variable::new("var"))
426                    + IntegerExpression::Atom(Variable::new("var")),
427            ),
428        );
429        let expected_expr = LIAVariableConstraint::SingleVarConstraint(SingleAtomConstraint::new(
430            Variable::new("var"),
431            ThresholdConstraint::new(
432                ThresholdCompOp::Geq,
433                Vec::<(Parameter, Fraction)>::new(),
434                Fraction::new(1, 2, false),
435            ),
436        ));
437        let got = LIAVariableConstraint::try_from(expr).unwrap();
438        assert_eq!(got, expected_expr);
439
440        // TODO: consider whether this is fine
441        // 1 < 2 var --> 2var > 1 --> var >= 1
442        let expr = NonNegatedBooleanExpression::ComparisonExpression(
443            Box::new(IntegerExpression::Const(1)),
444            ComparisonOp::Lt,
445            Box::new(
446                IntegerExpression::Atom(Variable::new("var"))
447                    + IntegerExpression::Atom(Variable::new("var")),
448            ),
449        );
450        let expected_expr = LIAVariableConstraint::SingleVarConstraint(SingleAtomConstraint::new(
451            Variable::new("var"),
452            ThresholdConstraint::new(
453                ThresholdCompOp::Geq,
454                Vec::<(Parameter, Fraction)>::new(),
455                Fraction::new(1, 1, false),
456            ),
457        ));
458        let got = LIAVariableConstraint::try_from(expr).unwrap();
459        assert_eq!(got, expected_expr);
460
461        let expr = NonNegatedBooleanExpression::ComparisonExpression(
462            Box::new(IntegerExpression::Const(6) - IntegerExpression::Atom(Variable::new("var"))),
463            ComparisonOp::Leq,
464            Box::new(
465                IntegerExpression::Atom(Variable::new("var"))
466                    + IntegerExpression::Atom(Variable::new("var")),
467            ),
468        );
469        let expected_expr = LIAVariableConstraint::SingleVarConstraint(SingleAtomConstraint::new(
470            Variable::new("var"),
471            ThresholdConstraint::new(
472                ThresholdCompOp::Geq,
473                Vec::<(Parameter, Fraction)>::new(),
474                Fraction::new(2, 1, false),
475            ),
476        ));
477        let got = LIAVariableConstraint::try_from(expr).unwrap();
478        assert_eq!(got, expected_expr);
479    }
480
481    #[test]
482    fn test_try_into_multi_var() {
483        let expr = NonNegatedBooleanExpression::ComparisonExpression(
484            Box::new(
485                IntegerExpression::Atom(Variable::new("var1"))
486                    + IntegerExpression::Atom(Variable::new("var2")),
487            ),
488            ComparisonOp::Lt,
489            Box::new(IntegerExpression::Const(0)),
490        );
491
492        let expected_expr = LIAVariableConstraint::SumVarConstraint(
493            SumAtomConstraint::try_new(
494                BTreeMap::from([(Variable::new("var1"), 1), (Variable::new("var2"), 1)]),
495                ThresholdConstraint::new(
496                    ThresholdCompOp::Lt,
497                    Vec::<(Parameter, Fraction)>::new(),
498                    0,
499                ),
500            )
501            .unwrap(),
502        );
503
504        let got = LIAVariableConstraint::try_from(expr).unwrap();
505        assert_eq!(got, expected_expr);
506    }
507
508    #[test]
509    fn test_try_into_multi_var_double_var_lhs() {
510        let expr = NonNegatedBooleanExpression::ComparisonExpression(
511            Box::new(
512                IntegerExpression::Atom(Variable::new("var1"))
513                    + IntegerExpression::Atom(Variable::new("var2"))
514                    + IntegerExpression::Atom(Variable::new("var1")) * IntegerExpression::Const(2),
515            ),
516            ComparisonOp::Lt,
517            Box::new(IntegerExpression::Const(0)),
518        );
519
520        let expected_expr = LIAVariableConstraint::SumVarConstraint(
521            SumAtomConstraint::try_new(
522                BTreeMap::from([(Variable::new("var1"), 3), (Variable::new("var2"), 1)]),
523                ThresholdConstraint::new(
524                    ThresholdCompOp::Lt,
525                    Vec::<(Parameter, Fraction)>::new(),
526                    0,
527                ),
528            )
529            .unwrap(),
530        );
531
532        let got = LIAVariableConstraint::try_from(expr).unwrap();
533        assert_eq!(got, expected_expr);
534    }
535
536    #[test]
537    fn test_try_into_multi_var_double_var_rhs() {
538        // var1 + var2 + 5 * var1 <  0 + 2 * var1
539        let expr = NonNegatedBooleanExpression::ComparisonExpression(
540            Box::new(
541                IntegerExpression::Atom(Variable::new("var1"))
542                    + IntegerExpression::Atom(Variable::new("var2"))
543                    + IntegerExpression::Atom(Variable::new("var1")) * IntegerExpression::Const(5),
544            ),
545            ComparisonOp::Lt,
546            Box::new(
547                IntegerExpression::Const(0)
548                    + (IntegerExpression::Atom(Variable::new("var1"))
549                        * IntegerExpression::Const(2)),
550            ),
551        );
552
553        let expected_expr = LIAVariableConstraint::SumVarConstraint(
554            SumAtomConstraint::try_new(
555                BTreeMap::from([(Variable::new("var1"), 4), (Variable::new("var2"), 1)]),
556                ThresholdConstraint::new(
557                    ThresholdCompOp::Lt,
558                    Vec::<(Parameter, Fraction)>::new(),
559                    0,
560                ),
561            )
562            .unwrap(),
563        );
564
565        let got = LIAVariableConstraint::try_from(expr).unwrap();
566        assert_eq!(got, expected_expr);
567    }
568
569    #[test]
570    fn test_try_into_comp_guard() {
571        // var1 + var2 + 2 * var1 <  0 + 5 * var1
572        let expr = NonNegatedBooleanExpression::ComparisonExpression(
573            Box::new(
574                IntegerExpression::Atom(Variable::new("var1"))
575                    + IntegerExpression::Atom(Variable::new("var2"))
576                    + IntegerExpression::Atom(Variable::new("var1")) * IntegerExpression::Const(2),
577            ),
578            ComparisonOp::Lt,
579            Box::new(
580                IntegerExpression::Const(0)
581                    + (IntegerExpression::Atom(Variable::new("var1"))
582                        * IntegerExpression::Const(5)),
583            ),
584        );
585
586        let expected_expr = LIAVariableConstraint::ComparisonConstraint(
587            crate::lia_threshold_automaton::ComparisonConstraint::try_new(
588                BTreeMap::from([
589                    (Variable::new("var1"), -Fraction::from(2)),
590                    (Variable::new("var2"), 1.into()),
591                ]),
592                ThresholdConstraint::new(
593                    ThresholdCompOp::Lt,
594                    Vec::<(Parameter, Fraction)>::new(),
595                    0,
596                ),
597            )
598            .unwrap(),
599        );
600
601        let got = LIAVariableConstraint::try_from(expr).unwrap();
602        assert_eq!(got, expected_expr);
603    }
604
605    #[test]
606    fn test_try_into_only_const() {
607        // 0 == 0
608        let expr = NonNegatedBooleanExpression::ComparisonExpression(
609            Box::new(IntegerExpression::Const(0)),
610            ComparisonOp::Eq,
611            Box::new(IntegerExpression::Const(0)),
612        );
613
614        let expected_expr = LIAVariableConstraint::True;
615
616        let got = LIAVariableConstraint::try_from(expr).unwrap();
617        assert_eq!(got, expected_expr);
618
619        // 0 < 0
620        let expr = NonNegatedBooleanExpression::ComparisonExpression(
621            Box::new(IntegerExpression::Const(0)),
622            ComparisonOp::Lt,
623            Box::new(IntegerExpression::Const(0)),
624        );
625
626        let expected_expr = LIAVariableConstraint::False;
627
628        let got = LIAVariableConstraint::try_from(expr).unwrap();
629        assert_eq!(got, expected_expr);
630    }
631
632    #[test]
633    fn test_error_on_parameter_constraint() {
634        let expr = NonNegatedBooleanExpression::ComparisonExpression(
635            Box::new(IntegerExpression::Param(Parameter::new("n"))),
636            ComparisonOp::Gt,
637            Box::new(IntegerExpression::Const(0)),
638        );
639
640        let got = LIAVariableConstraint::try_from(expr);
641        assert!(got.is_err(), "Got {got:?}");
642        assert!(matches!(
643            got,
644            Err(ConstraintRewriteError::ParameterConstraint(_))
645        ));
646    }
647}
taco_threshold_automaton/lia_threshold_automaton/general_to_lia/classify_into_lia.rs

taco_threshold_automaton/lia_threshold_automaton/general_to_lia/
classify_into_lia.rs
