taco_threshold_automaton/lia_threshold_automaton/
integer_thresholds.rs

1//! This module defines abstract types for linear arithmetic constraints over
2//! parameters, variables and other [`Atomic`] values, that can be safely
3//! encoded into integer arithmetic SMT constraints.
4//!
5//! A type that can be safely encoded into integer constraints will implement
6//! the [`IntoNoDivBooleanExpr`] trait. Expressions implementing this trait will
7//! always be expanded to the least common multiple of the denominators
8//! appearing in the expression, thus removing the rational constants in the
9//! encoded expression while preserving the satisfying assignments-
10//!
11//! This is important as SMTLIB-2 defines integer division analog to how integer
12//! division is usually implemented on a computer
13//! (see [Theory of `Ints`](https://smt-lib.org/theories-Ints.shtml)).
14//!
15//! This means for example that the expressions `1 / 2 == 0` is `True`. In our
16//! case, this is not the intended definition. Therefore, if fractions appear as
17//! part of boolean expressions, these expressions are expanded until all
18//! fractions can be represented as an integer.
19//!
20//! For example, an expression of the form `x = 1/3 * n` will be encoded as
21//! `3 * x = n`.
22
23use std::{
24    collections::{BTreeMap, HashMap},
25    error::Error,
26    fmt::{self},
27    hash::Hash,
28    ops,
29};
30
31use crate::{
32    expressions::{
33        And, Atomic, BooleanExpression, ComparisonOp, IntegerExpression, Location, Or, Parameter,
34        Variable, fraction::Fraction,
35    },
36    lia_threshold_automaton::ConstraintRewriteError,
37    lia_threshold_automaton::general_to_lia::classify_into_lia::split_pairs_into_atom_and_threshold,
38};
39
40/// Weighted sum of [`Atomic`] values
41///
42/// A weighted sum is an expression of the form `c_1 * v_1 + ... + c_n * v_n`
43/// where `v_1, ..., v_n` are atomic values and `c_1, ..., c_n` are real
44/// valued coefficients to these variables.
45#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
46pub struct WeightedSum<T>
47where
48    T: Atomic,
49{
50    /// Map of atomic values and their weights
51    weight_map: BTreeMap<T, Fraction>,
52}
53
54impl<T: Atomic> WeightedSum<T> {
55    /// Check if the weighted sum is empty / equal to 0
56    pub fn is_zero(&self) -> bool {
57        self.weight_map.is_empty()
58    }
59
60    /// Check whether all coefficients are already integers
61    ///
62    /// This checks whether all coefficients in the weighted sum are integers,
63    /// i.e., they can be converted to integer values without a loss in
64    /// precision.
65    ///
66    /// # Example
67    ///
68    ///
69    /// ```rust
70    /// use taco_threshold_automaton::{
71    ///     expressions::{Variable, fraction::Fraction},
72    ///     lia_threshold_automaton::integer_thresholds::WeightedSum
73    /// };
74    ///
75    /// let ws : WeightedSum<Variable> = WeightedSum::new([
76    ///     (Variable::new("var2"), 1),
77    /// ]);
78    /// assert!(ws.is_integer_form());
79    ///
80    /// let ws : WeightedSum<Variable> = WeightedSum::new([
81    ///     (Variable::new("var2"), Fraction::new(1, 2, false)),
82    /// ]);
83    /// assert!(!ws.is_integer_form());
84    /// ```
85    pub fn is_integer_form(&self) -> bool {
86        self.weight_map.values().all(|coef| coef.is_integer())
87    }
88
89    /// Create a new [`WeightedSum`]
90    ///
91    /// Creates a new [`WeightedSum`], filtering all components with a factor of `0`
92    pub fn new<F, I, V>(weight_map: I) -> Self
93    where
94        F: Into<Fraction>,
95        V: Into<T>,
96        I: IntoIterator<Item = (V, F)>,
97    {
98        // remove all entries with a coefficient of zero
99        let weight_map = weight_map
100            .into_iter()
101            .map(|(v, c)| (v.into(), c.into()))
102            .filter(|(_, coef)| *coef != Fraction::from(0))
103            .collect();
104
105        Self { weight_map }
106    }
107
108    /// Create a new empty [`WeightedSum`]
109    pub fn new_empty() -> Self {
110        Self {
111            weight_map: BTreeMap::new(),
112        }
113    }
114
115    /// Get the factor for `v` if it exists
116    ///
117    /// # Example
118    ///
119    /// ```
120    /// use taco_threshold_automaton::{
121    ///     expressions::{Variable, fraction::Fraction},
122    ///     lia_threshold_automaton::integer_thresholds::WeightedSum
123    /// };
124    ///
125    /// let ws : WeightedSum<Variable> = WeightedSum::new([
126    ///     (Variable::new("var1"), 1),
127    /// ]);
128    /// assert_eq!(ws.get_factor(&Variable::new("var1")), Some(&Fraction::from(1)));
129    /// ```
130    pub fn get_factor(&self, v: &T) -> Option<&Fraction> {
131        self.weight_map.get(v)
132    }
133
134    /// Get the least common multiple across all denominators of the
135    /// coefficients
136    ///
137    /// The least common multiple is computed across all denominators of the
138    /// coefficients in the [`WeightedSum`].
139    ///
140    /// This can be useful for scaling such that all coefficients are integers.
141    ///
142    /// # Example
143    ///
144    /// ```
145    /// use taco_threshold_automaton::{
146    ///     expressions::{Variable, fraction::Fraction},
147    ///     lia_threshold_automaton::integer_thresholds::WeightedSum
148    /// };
149    ///
150    /// let ws : WeightedSum<Variable> = WeightedSum::new([
151    ///     (Variable::new("var1"), 1),
152    /// ]);
153    /// assert_eq!(ws.get_lcm_of_denominators(), 1);
154    ///
155    /// let ws : WeightedSum<Variable> = WeightedSum::new([
156    ///     (Variable::new("var1"), Fraction::from(1)),
157    ///     (Variable::new("var2"), Fraction::new(1, 2, false)),
158    /// ]);
159    /// assert_eq!(ws.get_lcm_of_denominators(), 2);
160    /// ```
161    pub fn get_lcm_of_denominators(&self) -> u32 {
162        self.weight_map
163            .values()
164            .fold(1, |acc, coef| num::Integer::lcm(&acc, &coef.denominator()))
165    }
166
167    /// Scale the weighted sum by a factor
168    ///
169    /// # Example
170    ///
171    /// ```rust
172    /// use taco_threshold_automaton::{
173    ///     expressions::Variable,
174    ///     lia_threshold_automaton::integer_thresholds::WeightedSum
175    /// };
176    ///
177    /// let mut ws : WeightedSum<Variable> = WeightedSum::new([
178    ///     (Variable::new("var2"), 1),
179    ///     (Variable::new("var2"), 3),
180    /// ]);
181    /// let scaled_ws = WeightedSum::new([
182    ///     (Variable::new("var2"), 3),
183    ///     (Variable::new("var2"), 9),
184    /// ]);
185    ///
186    /// ws.scale(3.into());
187    ///
188    /// assert_eq!(ws, scaled_ws);
189    /// ```
190    pub fn scale(&mut self, factor: Fraction) {
191        if factor == Fraction::from(0) {
192            self.weight_map.clear();
193            return;
194        }
195
196        for coef in self.weight_map.values_mut() {
197            *coef *= factor;
198        }
199    }
200
201    /// Check whether `t` is part of the [`WeightedSum`] (and the factor is not 0)
202    ///
203    /// # Example
204    ///
205    /// ```rust
206    /// use taco_threshold_automaton::{
207    ///     expressions::Variable,
208    ///     lia_threshold_automaton::integer_thresholds::WeightedSum
209    /// };
210    ///
211    /// let ws = WeightedSum::new([
212    ///     (Variable::new("var"), 1),
213    ///     (Variable::new("zvar"), 0),
214    /// ]);
215    ///
216    /// assert!(ws.contains(&Variable::new("var")));
217    /// assert!(!ws.contains(&Variable::new("unknown")));
218    /// assert!(!ws.contains(&Variable::new("zvar")));
219    /// ```
220    pub fn contains(&self, t: &T) -> bool {
221        self.weight_map.contains_key(t)
222    }
223
224    /// Encode the weighted sum into an [`IntegerExpression`]
225    ///
226    /// This method will return the [`WeightedSum`] encoded as an
227    /// [`IntegerExpression`]. In case the weighted sum contains a fraction that
228    /// is not in an integer form this function **will encode the fraction**
229    /// without panicking or returning an error
230    fn get_integer_expression<S>(&self) -> IntegerExpression<S>
231    where
232        T: Into<IntegerExpression<S>>,
233        S: Atomic,
234    {
235        self.weight_map
236            .iter()
237            .fold(IntegerExpression::Const(0), |acc, (v, c)| {
238                debug_assert!(c != &Fraction::from(0));
239                debug_assert!(c.is_integer());
240
241                let mut expr = v.clone().into();
242                if *c != Fraction::from(1) {
243                    expr = IntegerExpression::from(*c) * expr;
244                }
245
246                // remove initial accumulator value
247                if acc == IntegerExpression::Const(0) {
248                    return expr;
249                }
250                acc + expr
251            })
252    }
253
254    /// Returns an iterator over all atoms in the weighted sum
255    pub fn get_atoms_appearing(&self) -> impl Iterator<Item = &T> {
256        self.weight_map.keys()
257    }
258}
259
260impl<T, F, I> From<I> for WeightedSum<T>
261where
262    T: Atomic,
263    F: Into<Fraction> + Clone,
264    I: IntoIterator<Item = (T, F)>,
265{
266    fn from(value: I) -> Self {
267        Self::new(value)
268    }
269}
270
271impl<T: Atomic> fmt::Display for WeightedSum<T> {
272    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
273        //? This works but is not very nice: we make the string representation
274        //? deterministic by sorting by their string representation.
275        let mut it = self.weight_map.iter().collect::<Vec<_>>();
276        it.sort_by_key(|(v, _)| v.to_string());
277        let mut it = it.into_iter();
278
279        if let Some((v, coef)) = it.next() {
280            display_factor_pair_omit_one(f, coef, v)?;
281        }
282
283        it.try_for_each(|(v, coef)| {
284            write!(f, " + ")?;
285            display_factor_pair_omit_one(f, coef, v)
286        })?;
287
288        Ok(())
289    }
290}
291
292impl<'a, T: Atomic> IntoIterator for &'a WeightedSum<T> {
293    type Item = (&'a T, &'a Fraction);
294
295    type IntoIter = std::collections::btree_map::Iter<'a, T, Fraction>;
296
297    fn into_iter(self) -> Self::IntoIter {
298        self.weight_map.iter()
299    }
300}
301
302/// Display a scaled pair but omit factor if it is one
303///
304/// This function converts the pair `factor` * `x` to the string `factor * x`
305/// but will omit `factor *` if factor is equal to one
306fn display_factor_pair_omit_one<T: fmt::Display>(
307    f: &mut std::fmt::Formatter<'_>,
308    factor: &Fraction,
309    x: &T,
310) -> std::fmt::Result {
311    if factor == &1.into() {
312        write!(f, "{x}")
313    } else {
314        write!(f, "{factor} * {x}")
315    }
316}
317
318/// [`WeightedSum`] of [`Parameter`]s with additional constant summand
319///
320/// This struct represents a sum over [`Parameter`] of the form
321/// `c_1 * p_1 + ... + c_n * p_n + c`
322/// where p_1, ..., p_n are [`Parameter`] and c_1,..,c_n, c are rational numbers
323/// represented by [`Fraction`]s.
324#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
325pub struct Threshold {
326    weighted_parameters: WeightedSum<Parameter>,
327    constant: Fraction,
328}
329
330impl Threshold {
331    /// Create a new [`Threshold`]
332    pub fn new<S, T>(weighted_parameters: S, constant: T) -> Self
333    where
334        S: Into<WeightedSum<Parameter>>,
335        T: Into<Fraction>,
336    {
337        Self {
338            weighted_parameters: weighted_parameters.into(),
339            constant: constant.into(),
340        }
341    }
342
343    /// Create a new [`Threshold`] from a constant without any parameters
344    pub fn from_const<T: Into<Fraction>>(c: T) -> Self {
345        Self {
346            weighted_parameters: WeightedSum::new_empty(),
347            constant: c.into(),
348        }
349    }
350
351    /// Scale the [`Threshold`] by a rational factor
352    pub fn scale<T: Into<Fraction>>(&mut self, factor: T) {
353        let factor = factor.into();
354        self.weighted_parameters.scale(factor);
355        self.constant *= factor;
356    }
357
358    /// Check whether the [`Threshold`] only contains a constant
359    pub fn is_constant(&self) -> bool {
360        self.weighted_parameters.is_zero()
361    }
362
363    /// Check whether the [`Threshold`] always evaluates to 0, i.e. there are no
364    /// scaled [`Parameter`] and the constant is 0
365    pub fn is_zero(&self) -> bool {
366        self.weighted_parameters.is_zero() && self.constant == Fraction::from(0)
367    }
368
369    /// If the threshold is constant, return the constant
370    ///
371    /// Returns `None` otherwise
372    pub fn get_const(&self) -> Option<Fraction> {
373        if self.weighted_parameters.is_zero() {
374            return Some(self.constant);
375        }
376
377        None
378    }
379
380    /// Add a constant to the threshold
381    pub fn add_const<F: Into<Fraction>>(&mut self, c: F) {
382        self.constant += c.into()
383    }
384
385    /// Subtract a constant from the threshold
386    pub fn sub_const<F: Into<Fraction>>(&mut self, c: F) {
387        self.constant -= c.into()
388    }
389}
390
391impl ops::Add for Threshold {
392    type Output = Threshold;
393
394    fn add(self, rhs: Self) -> Self::Output {
395        let constant = self.constant + rhs.constant;
396        let mut ws = self.weighted_parameters;
397
398        rhs.weighted_parameters
399            .weight_map
400            .into_iter()
401            .for_each(|(p, s)| {
402                ws.weight_map
403                    .entry(p)
404                    .and_modify(|existing| *existing += s)
405                    .or_insert(s);
406            });
407
408        ws.weight_map.retain(|_, f| !f.is_zero());
409
410        Self {
411            weighted_parameters: ws,
412            constant,
413        }
414    }
415}
416
417impl ops::Sub for Threshold {
418    type Output = Threshold;
419
420    fn sub(self, rhs: Self) -> Self::Output {
421        let constant = self.constant - rhs.constant;
422        let mut ws = self.weighted_parameters;
423
424        rhs.weighted_parameters
425            .weight_map
426            .into_iter()
427            .for_each(|(p, s)| {
428                ws.weight_map
429                    .entry(p)
430                    .and_modify(|existing| *existing -= s)
431                    .or_insert(-s);
432            });
433
434        ws.weight_map.retain(|_, f| !f.is_zero());
435
436        Self {
437            weighted_parameters: ws,
438            constant,
439        }
440    }
441}
442
443impl fmt::Display for Threshold {
444    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
445        if self.weighted_parameters.is_zero() {
446            return write!(f, "{}", self.constant);
447        }
448
449        write!(f, "{}", self.weighted_parameters)?;
450        if self.constant != Fraction::from(0) {
451            write!(f, " + {}", self.constant)?;
452        }
453
454        Ok(())
455    }
456}
457
458/// Restricted form of [`ComparisonOp`]
459#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
460pub enum ThresholdCompOp {
461    /// >=
462    Geq,
463    /// >
464    Gt,
465    /// <
466    Lt,
467    /// <=
468    Leq,
469}
470
471impl ThresholdCompOp {
472    /// Check whether the operator is not satisfied exactly at the threshold
473    /// but at its neighbors (`>` and `<=`), i.e., whether an interval
474    /// abstraction needs an exact interval `[t, t]` for the threshold `t`
475    pub fn needs_exact_interval(&self) -> bool {
476        matches!(self, ThresholdCompOp::Gt | ThresholdCompOp::Leq)
477    }
478}
479
480impl From<ThresholdCompOp> for ComparisonOp {
481    fn from(value: ThresholdCompOp) -> Self {
482        match value {
483            ThresholdCompOp::Geq => ComparisonOp::Geq,
484            ThresholdCompOp::Lt => ComparisonOp::Lt,
485            ThresholdCompOp::Gt => ComparisonOp::Gt,
486            ThresholdCompOp::Leq => ComparisonOp::Leq,
487        }
488    }
489}
490
491impl fmt::Display for ThresholdCompOp {
492    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
493        match self {
494            ThresholdCompOp::Geq => write!(f, ">="),
495            ThresholdCompOp::Lt => write!(f, "<"),
496            ThresholdCompOp::Gt => write!(f, ">"),
497            ThresholdCompOp::Leq => write!(f, "<="),
498        }
499    }
500}
501
502/// [`Threshold`] in combination with a comparison operator
503///
504/// A [`ThresholdConstraint`] represents a [`Threshold`] in combination with a
505/// comparison operator. Thus it can be used to represent equations of the form
506///  `<COMPOP> c_1 * p_1 + ... + c_n * p_n + c`
507/// where `<COMPOP>` is one of the comparison operators `==`, `!=`, `<`, `>`,
508/// `<=`, `>=` (represented by [`ComparisonOp`]).
509///
510/// Most importantly, this struct implements operations like scaling by a
511/// negative number faithfully. Thus it can be useful when transforming
512/// threshold guards.
513#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
514pub struct ThresholdConstraint(ThresholdCompOp, Threshold);
515
516impl ThresholdConstraint {
517    /// Create a new threshold constraint
518    pub fn new<S, T>(op: ThresholdCompOp, weighted_parameters: S, constant: T) -> Self
519    where
520        S: Into<WeightedSum<Parameter>>,
521        T: Into<Fraction>,
522    {
523        let thr = Threshold::new(weighted_parameters, constant);
524        Self(op, thr)
525    }
526
527    /// Create a new threshold constraint
528    pub fn new_from_thr(op: ThresholdCompOp, thr: Threshold) -> Self {
529        Self(op, thr)
530    }
531
532    /// Scale the threshold constraint by a fraction
533    pub fn scale<T: Into<Fraction>>(&mut self, factor: T) {
534        let factor = factor.into();
535        // first execute * -1, then scale
536        if factor.is_negative() {
537            match self.0 {
538                ThresholdCompOp::Geq => {
539                    self.0 = ThresholdCompOp::Leq;
540                }
541                ThresholdCompOp::Lt => {
542                    self.0 = ThresholdCompOp::Gt;
543                }
544                ThresholdCompOp::Gt => {
545                    self.0 = ThresholdCompOp::Lt;
546                }
547                ThresholdCompOp::Leq => {
548                    self.0 = ThresholdCompOp::Geq;
549                }
550            }
551        }
552
553        self.1.scale(factor);
554    }
555
556    /// Get the [`ComparisonOp`] used in the threshold
557    pub fn get_op(&self) -> ThresholdCompOp {
558        self.0
559    }
560
561    /// Get the [`Threshold`] of the threshold constraint
562    pub fn get_threshold(&self) -> &Threshold {
563        &self.1
564    }
565}
566
567impl fmt::Display for ThresholdConstraint {
568    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
569        write!(f, "{} {}", self.0, self.1)
570    }
571}
572
573/// Trait that needs to implemented by expressions which can be derived from
574/// thresholds and scaled expressions of type `T`
575pub trait DeriveFromIntegerComp<T: Atomic, E: Error + From<ConstraintRewriteError>>
576where
577    Self: Sized + And + Or,
578{
579    /// Derive from threshold and map scaled values of `T`
580    fn form_ordered_constr(
581        scaled_t: HashMap<T, Fraction>,
582        thr_c: ThresholdConstraint,
583    ) -> Result<Self, E>;
584
585    /// Derive the the type T from the integer expression
586    fn from_integer_expr(
587        lhs: IntegerExpression<T>,
588        op: ComparisonOp,
589        rhs: IntegerExpression<T>,
590    ) -> Result<Self, E> {
591        match op {
592            ComparisonOp::Gt => {
593                let op = ThresholdCompOp::Gt;
594
595                let (variables, thr) = split_pairs_into_atom_and_threshold(lhs, rhs)?;
596                let thr_c = ThresholdConstraint::new_from_thr(op, thr);
597                Self::form_ordered_constr(variables, thr_c)
598            }
599            ComparisonOp::Geq => {
600                let (variables, thr) = split_pairs_into_atom_and_threshold(lhs, rhs)?;
601                let thr_c = ThresholdConstraint::new_from_thr(ThresholdCompOp::Geq, thr);
602                Self::form_ordered_constr(variables, thr_c)
603            }
604            ComparisonOp::Leq => {
605                let op = ThresholdCompOp::Leq;
606
607                let (variables, thr) = split_pairs_into_atom_and_threshold(lhs, rhs)?;
608                let thr_c = ThresholdConstraint::new_from_thr(op, thr);
609
610                Self::form_ordered_constr(variables, thr_c)
611            }
612            ComparisonOp::Lt => {
613                let (variables, thr) = split_pairs_into_atom_and_threshold(lhs, rhs)?;
614                let thr_c = ThresholdConstraint::new_from_thr(ThresholdCompOp::Lt, thr);
615                Self::form_ordered_constr(variables, thr_c)
616            }
617            ComparisonOp::Eq => {
618                let lower_constr =
619                    Self::from_integer_expr(lhs.clone(), ComparisonOp::Leq, rhs.clone())?;
620                let upper_constr =
621                    Self::from_integer_expr(lhs.clone(), ComparisonOp::Geq, rhs.clone())?;
622
623                Ok(lower_constr.and(upper_constr))
624            }
625            ComparisonOp::Neq => {
626                let lower_constr =
627                    Self::from_integer_expr(lhs.clone(), ComparisonOp::Lt, rhs.clone())?;
628                let upper_constr =
629                    Self::from_integer_expr(lhs.clone(), ComparisonOp::Gt, rhs.clone())?;
630
631                Ok(lower_constr.or(upper_constr))
632            }
633        }
634    }
635}
636
637/// This struct represents a [`Threshold`] constraint over an object of type T
638///
639/// It is used to, for example, represent a threshold guard over a variable
640#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
641pub(crate) struct ThresholdConstraintOver<T> {
642    t: T,
643    thr_constr: ThresholdConstraint,
644}
645
646impl<T> ThresholdConstraintOver<T> {
647    /// Create a new symbolic constraint over an object of type `T`
648    pub fn new(t: T, thr_constr: ThresholdConstraint) -> Self {
649        Self { t, thr_constr }
650    }
651
652    /// Check whether the constraint is an upper guard
653    ///
654    /// An upper guard is a guard of the form `< t` or `<= t` or `!= t` or
655    /// `== t`, as it can become disabled when the threshold is reached.
656    pub fn is_upper_guard(&self) -> bool {
657        matches!(
658            self.thr_constr.get_op(),
659            ThresholdCompOp::Lt | ThresholdCompOp::Leq
660        )
661    }
662
663    /// Check whether the constraint is a lower guard
664    ///
665    /// A lower guard is a guard of the form `> t` or `>= t` or `!= t` or
666    /// `== t`, as it can become enabled when the threshold is reached.
667    pub fn is_lower_guard(&self) -> bool {
668        matches!(
669            self.thr_constr.get_op(),
670            ThresholdCompOp::Geq | ThresholdCompOp::Gt
671        )
672    }
673
674    /// Get the subject of the constraint
675    pub fn get_t(&self) -> &T {
676        &self.t
677    }
678
679    /// Get the threshold of the constraint
680    pub fn get_threshold(&self) -> &Threshold {
681        self.thr_constr.get_threshold()
682    }
683
684    /// Get the threshold constraint of this constraint
685    pub fn get_threshold_constraint(&self) -> &ThresholdConstraint {
686        &self.thr_constr
687    }
688
689    /// Encode the constraint into a BooleanExpression
690    ///
691    /// This encoding will be guaranteed to not include rational constants
692    pub fn encode_to_boolean_expr<S>(&self) -> BooleanExpression<S>
693    where
694        S: Atomic,
695        T: IntoNoDivBooleanExpr<S>,
696        Threshold: IntoNoDivBooleanExpr<S>,
697    {
698        self.t.encode_comparison_to_boolean_expression(
699            self.thr_constr.get_op().into(),
700            self.thr_constr.get_threshold(),
701        )
702    }
703}
704
705impl<S, T> From<ThresholdConstraintOver<T>> for BooleanExpression<S>
706where
707    S: Atomic,
708    T: IntoNoDivBooleanExpr<S>,
709    Threshold: IntoNoDivBooleanExpr<S>,
710{
711    fn from(val: ThresholdConstraintOver<T>) -> Self {
712        val.encode_to_boolean_expr()
713    }
714}
715
716impl<T> fmt::Display for ThresholdConstraintOver<T>
717where
718    T: fmt::Display,
719{
720    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
721        write!(f, "{} {}", self.t, self.thr_constr)
722    }
723}
724
725/// Trait for objects that can be encoded into boolean expressions that
726/// do not contain any integer divisions or real numbers.
727///
728/// When using this trait all expressions will be scaled such that there are no
729/// longer real coefficients appearing in the expression, but the set of
730/// satisfying (integer) solutions will stay the same.
731///
732/// This is done by computing the least common multiple (LCM) of all
733/// denominators of rational coefficients and then scaling both sides of a
734/// `ComparisonExpr` to obtain an equivalent expression only containing integers.
735///
736/// Note that using this trait might result in a lot of LCM computations.
737pub trait IntoNoDivBooleanExpr<T>
738where
739    T: Atomic,
740{
741    /// Get the scaled integer expression
742    ///
743    /// **Important:** The scaling factor supplied will be a multiple of the
744    /// least common multiple (LCM) of the expression. That is the relation
745    /// `scaling_factor % self.get_lcm_of_denominators() == 0` must hold.
746    ///
747    /// This function converts the object into an integer expression without any
748    /// divisions or real numbers. To eliminate rational coefficients, the
749    /// expression is therefore scaled by the given factor.    
750    fn get_scaled_integer_expression(&self, scaling_factor: u32) -> IntegerExpression<T>;
751
752    /// Get the lcm across all denominators in the object
753    ///
754    /// This is useful to determine the (least) scaling factor needed to scale
755    /// this expressions such that it does not contain any real numbers.
756    fn get_lcm_of_denominators(&self) -> u32;
757
758    /// Encode the comparison of two expressions into a boolean expression with a
759    /// that does not contain any real numbers.
760    ///
761    /// This functions scales the given thresholds such that in both thresholds
762    /// all factors are integers. The scaling is done by computing the least
763    /// common multiple (LCM) of the denominators.
764    ///
765    /// Resulting comparison: `self <OP> other`
766    fn encode_comparison_to_boolean_expression<Q>(
767        &self,
768        comparison_op: ComparisonOp,
769        other: &Q,
770    ) -> BooleanExpression<T>
771    where
772        Q: IntoNoDivBooleanExpr<T>,
773    {
774        let lcm_self = self.get_lcm_of_denominators();
775        let lcm_other = other.get_lcm_of_denominators();
776        let lcm = num::integer::lcm(lcm_self, lcm_other);
777
778        let self_s = self.get_scaled_integer_expression(lcm);
779        let other_s = other.get_scaled_integer_expression(lcm);
780
781        BooleanExpression::ComparisonExpression(Box::new(self_s), comparison_op, Box::new(other_s))
782    }
783}
784
785impl<T> IntoNoDivBooleanExpr<T> for Parameter
786where
787    Self: Into<IntegerExpression<T>>,
788    T: Atomic,
789{
790    fn get_scaled_integer_expression(&self, scaling_factor: u32) -> IntegerExpression<T> {
791        if scaling_factor == 0 {
792            return IntegerExpression::Const(0);
793        }
794        if scaling_factor == 1 {
795            return IntegerExpression::from(self.clone());
796        }
797
798        IntegerExpression::from(scaling_factor) * IntegerExpression::from(self.clone())
799    }
800
801    fn get_lcm_of_denominators(&self) -> u32 {
802        1 // Parameters do not have denominators
803    }
804}
805
806impl<T> IntoNoDivBooleanExpr<T> for Location
807where
808    T: Atomic,
809    IntegerExpression<T>: From<Self>,
810    IntegerExpression<T>: From<u32>,
811{
812    fn get_scaled_integer_expression(&self, scaling_factor: u32) -> IntegerExpression<T> {
813        if scaling_factor == 0 {
814            return IntegerExpression::Const(0);
815        }
816        if scaling_factor == 1 {
817            return IntegerExpression::from(self.clone());
818        }
819
820        IntegerExpression::<T>::from(scaling_factor) * IntegerExpression::<T>::from(self.clone())
821    }
822
823    fn get_lcm_of_denominators(&self) -> u32 {
824        1 // Locations do not have denominators
825    }
826}
827
828impl<T> IntoNoDivBooleanExpr<T> for Variable
829where
830    T: Atomic,
831    IntegerExpression<T>: From<Self>,
832    IntegerExpression<T>: From<u32>,
833{
834    fn get_scaled_integer_expression(&self, scaling_factor: u32) -> IntegerExpression<T> {
835        if scaling_factor == 0 {
836            return IntegerExpression::Const(0);
837        }
838        if scaling_factor == 1 {
839            return IntegerExpression::from(self.clone());
840        }
841
842        IntegerExpression::<T>::from(scaling_factor) * IntegerExpression::<T>::from(self.clone())
843    }
844
845    fn get_lcm_of_denominators(&self) -> u32 {
846        1 // Variables do not have denominators
847    }
848}
849
850impl<T, S> IntoNoDivBooleanExpr<S> for WeightedSum<T>
851where
852    T: Atomic + IntoNoDivBooleanExpr<S>,
853    S: Atomic,
854    IntegerExpression<S>: From<T>,
855{
856    fn get_scaled_integer_expression(&self, scaling_factor: u32) -> IntegerExpression<S> {
857        let mut scaled = self.clone();
858        scaled.scale(Fraction::from(scaling_factor));
859        debug_assert!(
860            scaled.is_integer_form(),
861            "Scaled weighted sum is not in integer form"
862        );
863
864        scaled.get_integer_expression()
865    }
866
867    fn get_lcm_of_denominators(&self) -> u32 {
868        self.get_lcm_of_denominators()
869    }
870}
871
872impl<T> IntoNoDivBooleanExpr<T> for Threshold
873where
874    WeightedSum<Parameter>: IntoNoDivBooleanExpr<T>,
875    T: Atomic,
876{
877    fn get_scaled_integer_expression(&self, scaling_factor: u32) -> IntegerExpression<T> {
878        let scaled_constant = self.constant * Fraction::from(scaling_factor);
879        debug_assert!(
880            scaled_constant.is_integer(),
881            "Scaled constant is not an integer"
882        );
883
884        if self.weighted_parameters.is_zero() {
885            return IntegerExpression::from(scaled_constant);
886        }
887
888        let intexpr_ws = self
889            .weighted_parameters
890            .get_scaled_integer_expression(scaling_factor);
891
892        if scaled_constant == Fraction::from(0) {
893            return intexpr_ws;
894        }
895
896        intexpr_ws + IntegerExpression::from(scaled_constant)
897    }
898
899    fn get_lcm_of_denominators(&self) -> u32 {
900        let lcm_ws = self.weighted_parameters.get_lcm_of_denominators();
901        let lcm_const = self.constant.denominator();
902        num::integer::lcm(lcm_ws, lcm_const)
903    }
904}
905
906#[cfg(test)]
907mod tests {
908    use std::collections::{BTreeMap, HashSet};
909
910    use crate::{
911        expressions::{
912            BooleanExpression, ComparisonOp, IntegerExpression, Location, Parameter, Variable,
913            fraction::Fraction,
914        },
915        lia_threshold_automaton::integer_thresholds::{
916            IntoNoDivBooleanExpr, Threshold, ThresholdCompOp, ThresholdConstraint,
917            ThresholdConstraintOver, WeightedSum,
918        },
919    };
920
921    #[test]
922    fn test_threshold_is_zero() {
923        let thr = Threshold::new(Vec::<(Parameter, Fraction)>::new(), 0);
924        assert!(thr.is_zero());
925
926        let thr = Threshold::new(BTreeMap::from([(Parameter::new("n"), 1)]), 0);
927        assert!(!thr.is_zero());
928
929        let thr = Threshold::new(Vec::<(Parameter, Fraction)>::new(), 1);
930        assert!(!thr.is_zero());
931
932        let thr = Threshold::new(
933            BTreeMap::from([(Parameter::new("n"), 1)]),
934            -Fraction::from(1),
935        );
936        assert!(!thr.is_zero());
937    }
938
939    #[test]
940    fn test_threshold_is_constant() {
941        let thr = Threshold::new(Vec::<(Parameter, Fraction)>::new(), 0);
942        assert!(thr.is_constant());
943
944        let thr = Threshold::new(BTreeMap::from([(Parameter::new("n"), 1)]), 0);
945        assert!(!thr.is_constant());
946
947        let thr = Threshold::new(Vec::<(Parameter, Fraction)>::new(), 1);
948        assert!(thr.is_constant());
949
950        let thr = Threshold::new(
951            BTreeMap::from([(Parameter::new("n"), 1)]),
952            -Fraction::from(1),
953        );
954        assert!(!thr.is_constant());
955    }
956
957    #[test]
958    fn test_threshold_scale() {
959        let mut thr = Threshold::new(BTreeMap::from([(Parameter::new("n"), 1)]), 0);
960        thr.scale(2);
961
962        let expected = Threshold::new(BTreeMap::from([(Parameter::new("n"), 2)]), 0);
963        assert_eq!(thr, expected);
964
965        let mut thr = Threshold::new(BTreeMap::from([(Parameter::new("n"), 0)]), 1);
966        thr.scale(-Fraction::from(2));
967
968        let expected = Threshold::new(
969            BTreeMap::from([(Parameter::new("n"), Fraction::from(0))]),
970            -Fraction::from(2),
971        );
972        assert_eq!(thr, expected);
973
974        let mut thr = Threshold::new(BTreeMap::from([(Parameter::new("n"), 1)]), 0);
975        thr.scale(0);
976
977        let expected = Threshold::new(BTreeMap::from([(Parameter::new("n"), 0)]), 0);
978        assert_eq!(thr, expected);
979    }
980
981    #[test]
982    fn test_threshold_add_cons() {
983        let mut thr = Threshold::new(Vec::<(Parameter, Fraction)>::new(), 0);
984        assert!(thr.is_constant());
985
986        thr.add_const(1);
987        assert_eq!(thr.get_const().unwrap(), Fraction::from(1));
988
989        thr.sub_const(1);
990        assert_eq!(thr.get_const().unwrap(), Fraction::from(0));
991
992        let mut thr = Threshold::new(BTreeMap::from([(Parameter::new("n"), 1)]), 0);
993        thr.add_const(1);
994        assert_eq!(thr.get_const(), None);
995
996        thr.sub_const(1);
997        assert_eq!(thr.get_const(), None);
998    }
999
1000    #[test]
1001    fn test_threshold_add() {
1002        // disjoint parameters are combined
1003        let thr = Threshold::new(BTreeMap::from([(Parameter::new("n"), 1)]), 1)
1004            + Threshold::new(BTreeMap::from([(Parameter::new("m"), 2)]), 2);
1005
1006        let expected = Threshold::new(
1007            BTreeMap::from([(Parameter::new("n"), 1), (Parameter::new("m"), 2)]),
1008            3,
1009        );
1010        assert_eq!(thr, expected);
1011
1012        // coefficients of parameters appearing in both summands accumulate
1013        let thr = Threshold::new(BTreeMap::from([(Parameter::new("n"), 2)]), 1)
1014            + Threshold::new(BTreeMap::from([(Parameter::new("n"), 3)]), 2);
1015
1016        let expected = Threshold::new(BTreeMap::from([(Parameter::new("n"), 5)]), 3);
1017        assert_eq!(thr, expected);
1018
1019        // coefficients canceling out to 0 are removed
1020        let thr = Threshold::new(BTreeMap::from([(Parameter::new("n"), 1)]), 1)
1021            + Threshold::new(
1022                BTreeMap::from([(Parameter::new("n"), -Fraction::from(1))]),
1023                2,
1024            );
1025
1026        let expected = Threshold::from_const(3);
1027        assert_eq!(thr, expected);
1028        assert!(thr.is_constant());
1029
1030        // adding pure constants
1031        let thr = Threshold::from_const(1) + Threshold::from_const(2);
1032        assert_eq!(thr.get_const().unwrap(), Fraction::from(3));
1033    }
1034
1035    #[test]
1036    fn test_threshold_sub() {
1037        // disjoint parameters: coefficients of the rhs are subtracted
1038        let thr = Threshold::new(BTreeMap::from([(Parameter::new("n"), 1)]), 1)
1039            - Threshold::new(BTreeMap::from([(Parameter::new("m"), 2)]), 3);
1040
1041        let expected = Threshold::new(
1042            BTreeMap::from([
1043                (Parameter::new("n"), Fraction::from(1)),
1044                (Parameter::new("m"), -Fraction::from(2)),
1045            ]),
1046            -Fraction::from(2),
1047        );
1048        assert_eq!(thr, expected);
1049
1050        // coefficients of parameters appearing in both are subtracted
1051        let thr = Threshold::new(BTreeMap::from([(Parameter::new("n"), 5)]), 3)
1052            - Threshold::new(BTreeMap::from([(Parameter::new("n"), 2)]), 1);
1053
1054        let expected = Threshold::new(BTreeMap::from([(Parameter::new("n"), 3)]), 2);
1055        assert_eq!(thr, expected);
1056
1057        // subtracting a threshold from itself yields 0
1058        let thr = Threshold::new(BTreeMap::from([(Parameter::new("n"), 1)]), 1)
1059            - Threshold::new(BTreeMap::from([(Parameter::new("n"), 1)]), 1);
1060        assert!(thr.is_zero());
1061
1062        // resulting coefficients may become negative
1063        let thr = Threshold::new(BTreeMap::from([(Parameter::new("n"), 1)]), 0)
1064            - Threshold::new(BTreeMap::from([(Parameter::new("n"), 2)]), 0);
1065
1066        let expected = Threshold::new(
1067            BTreeMap::from([(Parameter::new("n"), -Fraction::from(1))]),
1068            0,
1069        );
1070        assert_eq!(thr, expected);
1071    }
1072
1073    #[test]
1074    fn test_threshold_constr_getters() {
1075        let thrc = ThresholdConstraint::new(
1076            ThresholdCompOp::Geq,
1077            BTreeMap::from([
1078                (Parameter::new("n"), Fraction::from(1)),
1079                (Parameter::new("m"), -Fraction::from(2)),
1080            ]),
1081            1,
1082        );
1083
1084        let thr = Threshold::new(
1085            [
1086                (Parameter::new("n"), Fraction::from(1)),
1087                (Parameter::new("m"), -Fraction::from(2)),
1088            ],
1089            1,
1090        );
1091
1092        assert_eq!(thrc.get_threshold(), &thr)
1093    }
1094
1095    #[test]
1096    fn test_threshold_constr_scale() {
1097        let mut thrc = ThresholdConstraint::new(
1098            ThresholdCompOp::Gt,
1099            BTreeMap::from([
1100                (Parameter::new("n"), Fraction::from(1)),
1101                (Parameter::new("m"), -Fraction::from(2)),
1102            ]),
1103            1,
1104        );
1105        thrc.scale(Fraction::from(1));
1106
1107        let expected = ThresholdConstraint::new(
1108            ThresholdCompOp::Gt,
1109            BTreeMap::from([
1110                (Parameter::new("n"), Fraction::from(1)),
1111                (Parameter::new("m"), -Fraction::from(2)),
1112            ]),
1113            Fraction::from(1),
1114        );
1115
1116        assert_eq!(thrc, expected);
1117
1118        thrc.scale(Fraction::from(2));
1119
1120        let expected = ThresholdConstraint::new(
1121            ThresholdCompOp::Gt,
1122            BTreeMap::from([
1123                (Parameter::new("n"), Fraction::from(2)),
1124                (Parameter::new("m"), -Fraction::from(4)),
1125            ]),
1126            Fraction::from(2),
1127        );
1128
1129        assert_eq!(thrc, expected);
1130
1131        thrc.scale(Fraction::new(1, 2, false));
1132
1133        let expected = ThresholdConstraint::new(
1134            ThresholdCompOp::Gt,
1135            BTreeMap::from([
1136                (Parameter::new("n"), Fraction::from(1)),
1137                (Parameter::new("m"), -Fraction::from(2)),
1138            ]),
1139            1,
1140        );
1141
1142        assert_eq!(thrc, expected);
1143    }
1144
1145    #[test]
1146    fn test_threshold_constr_scale_with_negative() {
1147        let mut thrc = ThresholdConstraint::new(
1148            ThresholdCompOp::Gt,
1149            BTreeMap::from([
1150                (Parameter::new("n"), Fraction::from(1)),
1151                (Parameter::new("m"), -Fraction::from(2)),
1152            ]),
1153            1,
1154        );
1155
1156        thrc.scale(-Fraction::from(2));
1157
1158        let expected = ThresholdConstraint::new(
1159            ThresholdCompOp::Lt,
1160            BTreeMap::from([
1161                (Parameter::new("n"), -Fraction::from(2)),
1162                (Parameter::new("m"), Fraction::from(4)),
1163            ]),
1164            -Fraction::from(2),
1165        );
1166
1167        assert_eq!(thrc, expected);
1168
1169        let mut thrc = ThresholdConstraint::new(
1170            ThresholdCompOp::Leq,
1171            BTreeMap::from([
1172                (Parameter::new("n"), Fraction::from(1)),
1173                (Parameter::new("m"), -Fraction::from(2)),
1174            ]),
1175            1,
1176        );
1177
1178        thrc.scale(-Fraction::from(2));
1179
1180        let expected = ThresholdConstraint::new(
1181            ThresholdCompOp::Geq,
1182            BTreeMap::from([
1183                (Parameter::new("n"), -Fraction::from(2)),
1184                (Parameter::new("m"), Fraction::from(4)),
1185            ]),
1186            -Fraction::from(2),
1187        );
1188
1189        assert_eq!(thrc, expected);
1190
1191        let mut thrc = ThresholdConstraint::new(
1192            ThresholdCompOp::Lt,
1193            BTreeMap::from([
1194                (Parameter::new("n"), Fraction::from(1)),
1195                (Parameter::new("m"), -Fraction::from(2)),
1196            ]),
1197            1,
1198        );
1199
1200        thrc.scale(-Fraction::from(2));
1201
1202        let expected = ThresholdConstraint::new(
1203            ThresholdCompOp::Gt,
1204            BTreeMap::from([
1205                (Parameter::new("n"), -Fraction::from(2)),
1206                (Parameter::new("m"), Fraction::from(4)),
1207            ]),
1208            -Fraction::from(2),
1209        );
1210
1211        assert_eq!(thrc, expected);
1212
1213        let mut thrc = ThresholdConstraint::new(
1214            ThresholdCompOp::Leq,
1215            BTreeMap::from([
1216                (Parameter::new("n"), Fraction::from(1)),
1217                (Parameter::new("m"), -Fraction::from(2)),
1218            ]),
1219            1,
1220        );
1221
1222        thrc.scale(-Fraction::from(2));
1223
1224        let expected = ThresholdConstraint::new(
1225            ThresholdCompOp::Geq,
1226            BTreeMap::from([
1227                (Parameter::new("n"), -Fraction::from(2)),
1228                (Parameter::new("m"), Fraction::from(4)),
1229            ]),
1230            -Fraction::from(2),
1231        );
1232
1233        assert_eq!(thrc, expected);
1234    }
1235
1236    #[test]
1237    fn test_threshold_display() {
1238        let thr = ThresholdConstraint::new(
1239            ThresholdCompOp::Geq,
1240            BTreeMap::from([
1241                (Parameter::new("n"), Fraction::from(1)),
1242                (Parameter::new("m"), -Fraction::from(2)),
1243            ]),
1244            1,
1245        );
1246
1247        let expected = ">= -2 * m + n + 1";
1248        assert_eq!(thr.to_string(), expected);
1249
1250        let thr =
1251            ThresholdConstraint::new(ThresholdCompOp::Geq, Vec::<(Parameter, Fraction)>::new(), 0);
1252        assert_eq!(thr.to_string(), ">= 0");
1253    }
1254
1255    #[test]
1256    fn test_contains_weighted_sum() {
1257        let ws = WeightedSum::new(BTreeMap::from([
1258            (Variable::new("var1"), 1),
1259            (Variable::new("var2"), 2),
1260        ]));
1261
1262        assert!(ws.contains(&Variable::new("var1")));
1263        assert!(!ws.contains(&Variable::new("var3")));
1264    }
1265
1266    #[test]
1267    fn test_get_atoms_appearing_ws() {
1268        let ws = WeightedSum::new(BTreeMap::from([
1269            (Variable::new("var1"), 1),
1270            (Variable::new("var2"), 2),
1271        ]));
1272
1273        let got_atoms: HashSet<_> = ws.get_atoms_appearing().cloned().collect();
1274        let expected_atoms = HashSet::from([Variable::new("var1"), Variable::new("var2")]);
1275        assert_eq!(got_atoms, expected_atoms)
1276    }
1277
1278    #[test]
1279    fn test_into_scaled_integer_expression_weighted_sum() {
1280        let ws: WeightedSum<Parameter> = WeightedSum::new(BTreeMap::from([
1281            (Parameter::new("var1"), 1),
1282            (Parameter::new("var2"), 2),
1283            (Parameter::new("var3"), 0),
1284        ]));
1285
1286        let expected: IntegerExpression<Parameter> =
1287            IntegerExpression::Param(Parameter::new("var1"))
1288                + (IntegerExpression::Const(2) * IntegerExpression::Param(Parameter::new("var2")));
1289
1290        let ws = ws.get_scaled_integer_expression(1);
1291
1292        assert_eq!(ws, expected);
1293
1294        let ws: WeightedSum<Parameter> = WeightedSum::new(BTreeMap::from([
1295            (Parameter::new("var1"), 1),
1296            (Parameter::new("var2"), 2),
1297            (Parameter::new("var3"), 0),
1298        ]));
1299
1300        let expected: IntegerExpression<Parameter> = (IntegerExpression::Const(5)
1301            * IntegerExpression::Param(Parameter::new("var1")))
1302            + (IntegerExpression::Const(10) * IntegerExpression::Param(Parameter::new("var2")));
1303
1304        let ws = ws.get_scaled_integer_expression(5);
1305
1306        assert_eq!(ws, expected);
1307    }
1308
1309    #[test]
1310    fn test_weighted_sum_into_iter() {
1311        let ws: WeightedSum<Variable> = WeightedSum::new([
1312            (Variable::new("var1"), 1),
1313            (Variable::new("var2"), 2),
1314            (Variable::new("var3"), 0),
1315        ]);
1316
1317        let expected: Vec<(Variable, Fraction)> = vec![
1318            (Variable::new("var1"), 1.into()),
1319            (Variable::new("var2"), 2.into()),
1320        ];
1321
1322        let result: Vec<(Variable, Fraction)> =
1323            (&ws).into_iter().map(|(a, b)| (a.clone(), *b)).collect();
1324        assert_eq!(result, expected);
1325    }
1326
1327    #[test]
1328    fn test_to_boolean_expr_thr_constr_over_var() {
1329        let constr = ThresholdConstraintOver::new(
1330            Variable::new("v"),
1331            ThresholdConstraint::new(ThresholdCompOp::Geq, [(Parameter::new("n"), 1)], 1),
1332        );
1333
1334        let b_expr = BooleanExpression::from(constr);
1335
1336        let expected_b_expr = BooleanExpression::ComparisonExpression(
1337            Box::new(IntegerExpression::Atom(Variable::new("v"))),
1338            ComparisonOp::Geq,
1339            Box::new(IntegerExpression::Param(Parameter::new("n")) + IntegerExpression::Const(1)),
1340        );
1341
1342        assert_eq!(b_expr, expected_b_expr)
1343    }
1344
1345    #[test]
1346    fn test_into_no_div_for_param() {
1347        let param = Parameter::new("n");
1348
1349        assert_eq!(
1350            <Parameter as IntoNoDivBooleanExpr<Parameter>>::get_lcm_of_denominators(&param),
1351            1
1352        );
1353
1354        let expected_int_expr: IntegerExpression<Parameter> =
1355            IntegerExpression::Const(42) * IntegerExpression::Param(param.clone());
1356        assert_eq!(param.get_scaled_integer_expression(42), expected_int_expr)
1357    }
1358
1359    #[test]
1360    fn test_into_no_div_for_loc() {
1361        let loc = Location::new("n");
1362
1363        assert_eq!(
1364            <Location as IntoNoDivBooleanExpr<Location>>::get_lcm_of_denominators(&loc),
1365            1
1366        );
1367
1368        let expected_int_expr: IntegerExpression<Location> =
1369            IntegerExpression::Const(42) * IntegerExpression::Atom(loc.clone());
1370        assert_eq!(loc.get_scaled_integer_expression(42), expected_int_expr)
1371    }
1372
1373    #[test]
1374    fn test_into_no_div_for_var() {
1375        let var = Variable::new("n");
1376
1377        assert_eq!(
1378            <Variable as IntoNoDivBooleanExpr<Variable>>::get_lcm_of_denominators(&var),
1379            1
1380        );
1381
1382        let expected_int_expr: IntegerExpression<Variable> =
1383            IntegerExpression::Const(42) * IntegerExpression::Atom(var.clone());
1384        assert_eq!(var.get_scaled_integer_expression(42), expected_int_expr)
1385    }
1386}
taco_threshold_automaton/lia_threshold_automaton/integer_thresholds.rs

taco_threshold_automaton/lia_threshold_automaton/
integer_thresholds.rs
