taco_interval_ta/builder/
static_interval_order.rs

1//! This module implements a static order on intervals
2//!
3//! A static order on intervals is a fixed order on intervals, which defines
4//! which interval borders are equal and the relative order among interval
5//! borders.
6//!
7
8use core::fmt;
9use std::collections::HashMap;
10
11use taco_display_utils::join_iterator;
12
13use simple_order_generator::SimpleOrderGeneratorContext;
14use taco_smt_encoder::SMTSolverBuilder;
15use taco_threshold_automaton::{
16    ThresholdAutomaton,
17    expressions::{Atomic, BooleanExpression, ComparisonOp, Variable},
18    lia_threshold_automaton::integer_thresholds::{
19        IntoNoDivBooleanExpr, ThresholdCompOp, ThresholdConstraint, WeightedSum,
20    },
21};
22
23use crate::{
24    HasAssociatedIntervals,
25    interval::{Interval, IntervalBoundary, IntervalOrder, IntervalOrderError, IntervalOrderFor},
26};
27
28mod simple_order_generator;
29
30/// Types implementing this trait define a static order on intervals that
31/// associates every interval with an index for each variable
32trait DefinesStaticIntervalOrder<T>: fmt::Display + IntervalOrder
33where
34    T: HasAssociatedIntervals,
35{
36    fn get_intervals<'a>(&'a self, var: &T) -> Result<&'a Vec<Interval>, IntervalOrderError<T>>;
37
38    fn get_interval_index(&self, var: &T, i: &Interval) -> Result<usize, IntervalOrderError<T>>;
39
40    fn get_interval_by_index<'a>(
41        &'a self,
42        var: &T,
43        idx: usize,
44    ) -> Result<&'a Interval, IntervalOrderError<T>>;
45
46    /// Check whether the interval order replaces the interval boundary
47    ///
48    /// This method checks if the interval boundary `ib` is replaced by the
49    /// interval order. If the interval boundary is replaced, the method returns
50    /// the new interval boundary that replaces `ib`. If the interval boundary
51    /// is not replaced, the method returns the original interval boundary.
52    ///
53    /// An interval might have been replaced if the interval boundary is
54    /// considered equal to another boundary in the order.
55    fn check_interval_replaced_by_eq(&self, ib: IntervalBoundary) -> IntervalBoundary;
56}
57
58/// Static order on intervals implementing `IntervalOrder` for variables and
59/// sums of variables
60#[derive(Debug, Clone, PartialEq)]
61pub struct StaticIntervalOrder {
62    /// Order on intervals for each variable
63    single_var_order: HashMap<Variable, Vec<Interval>>,
64    /// Order on intervals multi-variable guards
65    multi_var_order: HashMap<WeightedSum<Variable>, Vec<Interval>>,
66    /// Interval boundaries that are considered equal
67    equal_boundaries: HashMap<IntervalBoundary, IntervalBoundary>,
68}
69impl StaticIntervalOrder {
70    /// returns the underlying single_var_order
71    pub fn single_var_order(&self) -> &HashMap<Variable, Vec<Interval>> {
72        &self.single_var_order
73    }
74}
75
76#[cfg(test)]
77impl StaticIntervalOrder {
78    /// Get a new empty order for test purposes
79    pub fn new(
80        single_var_order: HashMap<Variable, Vec<Interval>>,
81        multi_var_order: HashMap<WeightedSum<Variable>, Vec<Interval>>,
82        equal_boundaries: HashMap<IntervalBoundary, IntervalBoundary>,
83    ) -> StaticIntervalOrder {
84        StaticIntervalOrder {
85            single_var_order,
86            multi_var_order,
87            equal_boundaries,
88        }
89    }
90}
91
92impl DefinesStaticIntervalOrder<Variable> for StaticIntervalOrder {
93    fn get_intervals<'a>(
94        &'a self,
95        var: &Variable,
96    ) -> Result<&'a Vec<Interval>, IntervalOrderError<Variable>> {
97        let intervals = self
98            .single_var_order
99            .get(var)
100            .ok_or_else(|| IntervalOrderError::VariableNotFound { var: var.clone() })?;
101        Ok(intervals)
102    }
103
104    fn get_interval_index(
105        &self,
106        var: &Variable,
107        i: &Interval,
108    ) -> Result<usize, IntervalOrderError<Variable>> {
109        let intervals = self.get_intervals(var)?;
110
111        intervals.iter().position(|x| *x == *i).ok_or_else(|| {
112            IntervalOrderError::IntervalNotFound {
113                var: var.clone(),
114                interval: i.clone(),
115            }
116        })
117    }
118
119    fn get_interval_by_index<'a>(
120        &'a self,
121        var: &Variable,
122        mut idx: usize,
123    ) -> Result<&'a Interval, IntervalOrderError<Variable>> {
124        let intervals = self.get_intervals(var)?;
125
126        if idx >= intervals.len() {
127            idx = intervals.len() - 1;
128        }
129
130        Ok(&intervals[idx])
131    }
132
133    /// This function checks whether the interval needs to be replaced by
134    /// another one because it is considered equal to another boundary in the
135    /// order.
136    ///
137    /// This function must be called when converting thresholds in the order.
138    fn check_interval_replaced_by_eq(&self, ib: IntervalBoundary) -> IntervalBoundary {
139        if let Some(ib) = self.equal_boundaries.get(&ib) {
140            return ib.clone();
141        }
142
143        ib
144    }
145}
146
147impl DefinesStaticIntervalOrder<WeightedSum<Variable>> for StaticIntervalOrder {
148    fn get_intervals<'a>(
149        &'a self,
150        var: &WeightedSum<Variable>,
151    ) -> Result<&'a Vec<Interval>, IntervalOrderError<WeightedSum<Variable>>> {
152        let intervals = self
153            .multi_var_order
154            .get(var)
155            .ok_or_else(|| IntervalOrderError::VariableNotFound { var: var.clone() })?;
156
157        Ok(intervals)
158    }
159
160    fn get_interval_index(
161        &self,
162        var: &WeightedSum<Variable>,
163        i: &Interval,
164    ) -> Result<usize, IntervalOrderError<WeightedSum<Variable>>> {
165        let intervals = self.get_intervals(var)?;
166
167        intervals.iter().position(|x| *x == *i).ok_or_else(|| {
168            IntervalOrderError::IntervalNotFound {
169                var: var.clone(),
170                interval: i.clone(),
171            }
172        })
173    }
174
175    fn get_interval_by_index<'a>(
176        &'a self,
177        var: &WeightedSum<Variable>,
178        mut idx: usize,
179    ) -> Result<&'a Interval, IntervalOrderError<WeightedSum<Variable>>> {
180        let intervals = self.get_intervals(var)?;
181
182        if intervals.is_empty() {
183            unreachable!("Should at least contain one interval!");
184        }
185        if idx >= intervals.len() {
186            idx = intervals.len() - 1;
187        }
188
189        Ok(&intervals[idx])
190    }
191
192    fn check_interval_replaced_by_eq(&self, ib: IntervalBoundary) -> IntervalBoundary {
193        if let Some(ib) = self.equal_boundaries.get(&ib) {
194            return ib.clone();
195        }
196
197        ib
198    }
199}
200
201impl<T: HasAssociatedIntervals, U: DefinesStaticIntervalOrder<T>> IntervalOrderFor<T> for U {
202    fn get_number_of_intervals(&self, var: &T) -> Result<usize, IntervalOrderError<T>> {
203        Ok(self.get_intervals(var)?.len())
204    }
205
206    fn lt(&self, var: &T, i1: &Interval, i2: &Interval) -> Result<bool, IntervalOrderError<T>> {
207        let idx1 = self.get_interval_index(var, i1)?;
208        let idx2 = self.get_interval_index(var, i2)?;
209
210        Ok(idx1 < idx2)
211    }
212
213    fn gt(&self, var: &T, i1: &Interval, i2: &Interval) -> Result<bool, IntervalOrderError<T>> {
214        let idx1 = self.get_interval_index(var, i1)?;
215        let idx2 = self.get_interval_index(var, i2)?;
216
217        Ok(idx1 > idx2)
218    }
219
220    fn get_next_interval<'a>(
221        &'a self,
222        var: &T,
223        i: &Interval,
224    ) -> Result<Option<&'a Interval>, IntervalOrderError<T>> {
225        let idx = self.get_interval_index(var, i)?;
226
227        if idx >= self.get_number_of_intervals(var)? - 1 {
228            return Ok(None);
229        }
230
231        Ok(Some(self.get_interval_by_index(var, idx + 1)?))
232    }
233
234    fn get_previous_interval<'a>(
235        &'a self,
236        var: &T,
237        i: &Interval,
238    ) -> Result<Option<&'a Interval>, IntervalOrderError<T>> {
239        let idx = self.get_interval_index(var, i)?;
240
241        if idx == 0 {
242            return Ok(None);
243        }
244
245        Ok(Some(self.get_interval_by_index(var, idx - 1)?))
246    }
247
248    fn compute_enabled_intervals_of_threshold(
249        &self,
250        t: &T,
251        thr: &ThresholdConstraint,
252    ) -> Result<Vec<Interval>, IntervalOrderError<T>> {
253        let lb = IntervalBoundary::from_threshold_constraint(thr);
254
255        let lb: IntervalBoundary = self.check_interval_replaced_by_eq(lb);
256
257        let intervals = self.get_intervals(t)?;
258
259        let (idx, _) = intervals
260            .iter()
261            .enumerate()
262            .find(|(_index, i)| i.check_is_contained(&lb))
263            .ok_or_else(|| IntervalOrderError::ThresholdExtractionError {
264                var: t.clone(),
265                thr: thr.clone(),
266            })?;
267
268        let result = match thr.get_op() {
269            ThresholdCompOp::Geq => intervals[idx..].to_vec(),
270            ThresholdCompOp::Lt => intervals[..idx].to_vec(),
271            ThresholdCompOp::Gt => {
272                let idx = idx + 1;
273                intervals[idx..].to_vec()
274            }
275            ThresholdCompOp::Leq => {
276                let idx = idx + 1;
277                intervals[..idx].to_vec()
278            }
279        };
280
281        Ok(result)
282    }
283
284    fn get_zero_interval(&self, t: &T) -> Result<&Interval, IntervalOrderError<T>> {
285        Ok(self.get_intervals(t)?.first().unwrap())
286    }
287
288    fn get_all_intervals_of_t(&self, t: &T) -> Result<&Vec<Interval>, IntervalOrderError<T>> {
289        self.get_intervals(t)
290    }
291
292    fn check_interval_replaced(&self, ib: IntervalBoundary) -> IntervalBoundary {
293        self.check_interval_replaced_by_eq(ib)
294    }
295}
296
297impl IntervalOrder for StaticIntervalOrder {
298    fn order_to_boolean_expr<T: Atomic>(&self) -> Vec<BooleanExpression<T>> {
299        let eq_constr = self.equal_boundaries.iter().map(|(ib_1, ib_2)| {
300            let ib_1 = ib_1.get_threshold().expect("Infinite interval in order");
301            let ib_2 = ib_2.get_threshold().expect("Infinite interval in order");
302
303            ib_1.encode_comparison_to_boolean_expression(ComparisonOp::Eq, ib_2)
304        });
305
306        // Exact intervals [b, b] do not impose an order constraint
307        let interval_constr = self
308            .single_var_order
309            .values()
310            .chain(self.multi_var_order.values())
311            .flat_map(|intervals| {
312                intervals
313                    .iter()
314                    .filter(|i| i.ub() != &IntervalBoundary::Infty)
315                    .filter(|i| i.lb() != i.ub() || i.is_left_open() || i.is_right_open())
316                    .map(|interval| {
317                        if interval.lb() == &IntervalBoundary::Infty {
318                            debug_assert!(false, "Interval with lower bound ∞ found");
319                            return BooleanExpression::False;
320                        }
321
322                        let lb = interval
323                            .lb()
324                            .get_threshold()
325                            .expect("Infinite interval in order");
326                        let ub = interval
327                            .ub()
328                            .get_threshold()
329                            .expect("Infinite interval in order");
330
331                        lb.encode_comparison_to_boolean_expression(ComparisonOp::Lt, ub)
332                    })
333            });
334
335        eq_constr.chain(interval_constr).collect()
336    }
337}
338
339impl fmt::Display for StaticIntervalOrder {
340    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
341        writeln!(f, "intervalOrder {{")?;
342
343        if !self.equal_boundaries.is_empty() {
344            writeln!(
345                f,
346                "    {};",
347                join_iterator(
348                    self.equal_boundaries
349                        .iter()
350                        .map(|(ib1, ib2)| format!("{ib1} == {ib2}")),
351                    " && "
352                )
353            )?;
354        }
355
356        if !self.single_var_order.is_empty() {
357            let mut sorted_single_var = self.single_var_order.iter().collect::<Vec<_>>();
358            sorted_single_var.sort_by_key(|(a, _)| *a);
359
360            for (var, intervals) in sorted_single_var {
361                writeln!(f, "    {}: {};", var, join_iterator(intervals.iter(), ", "))?;
362            }
363        }
364
365        if !self.multi_var_order.is_empty() {
366            for (var, intervals) in &self.multi_var_order {
367                writeln!(f, "    {}: {};", var, join_iterator(intervals.iter(), ", "))?;
368            }
369        }
370
371        write!(f, "}}")
372    }
373}
374
375/// Builder for generating static interval orders
376pub struct StaticIntervalOrderBuilder {
377    order_generator: SimpleOrderGeneratorContext,
378    vars: Vec<Variable>,
379}
380
381impl StaticIntervalOrderBuilder {
382    /// Create a new static interval order builder
383    pub fn new<T: ThresholdAutomaton>(ta: &T, smt_solver_builder: SMTSolverBuilder) -> Self {
384        let orders = SimpleOrderGeneratorContext::new(ta, smt_solver_builder);
385        let vars = ta.variables().cloned().collect::<Vec<_>>();
386
387        StaticIntervalOrderBuilder {
388            order_generator: orders,
389            vars,
390        }
391    }
392
393    /// Add an interval found for a single variable
394    pub fn add_single_variable_interval(
395        self,
396        var: &Variable,
397        interval: &IntervalBoundary,
398        needs_exact: bool,
399    ) -> Self {
400        let orders = self
401            .order_generator
402            .extend_order_with_interval_for_single_variable(var, interval, needs_exact);
403
404        StaticIntervalOrderBuilder {
405            order_generator: orders,
406            vars: self.vars,
407        }
408    }
409
410    /// Add an interval found for a sum of variables
411    pub fn add_multi_variable_interval(
412        self,
413        sum: &WeightedSum<Variable>,
414        interval: &IntervalBoundary,
415        needs_exact: bool,
416    ) -> Self {
417        let orders = self
418            .order_generator
419            .extend_order_with_interval_for_multi_variable(sum, interval, needs_exact);
420
421        StaticIntervalOrderBuilder {
422            order_generator: orders,
423            vars: self.vars,
424        }
425    }
426
427    /// Generate all possible orders on intervals
428    pub fn build(self) -> Vec<StaticIntervalOrder> {
429        self.order_generator.build_orders(&self.vars)
430    }
431}
432
433#[cfg(test)]
434mod tests {
435
436    use std::collections::{BTreeMap, HashMap};
437
438    use taco_threshold_automaton::expressions::fraction::Fraction;
439    use taco_threshold_automaton::expressions::{
440        BooleanExpression, ComparisonOp, IntegerExpression, Parameter,
441    };
442
443    use taco_threshold_automaton::expressions::Variable;
444    use taco_threshold_automaton::lia_threshold_automaton::integer_thresholds::{
445        Threshold, ThresholdCompOp, ThresholdConstraint, WeightedSum,
446    };
447
448    use crate::builder::static_interval_order::{DefinesStaticIntervalOrder, StaticIntervalOrder};
449    use crate::interval::{
450        Interval, IntervalBoundary, IntervalOrder, IntervalOrderError, IntervalOrderFor,
451    };
452
453    #[test]
454    fn test_get_interval_index_single_var() {
455        let var = Variable::new("x");
456        let interval1 = Interval::new(
457            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
458            false,
459            IntervalBoundary::Infty,
460            false,
461        );
462
463        let mut internal_order = HashMap::new();
464        internal_order.insert(var.clone(), vec![interval1.clone()]);
465
466        let order = StaticIntervalOrder {
467            single_var_order: internal_order,
468            multi_var_order: HashMap::new(),
469            equal_boundaries: HashMap::new(),
470        };
471
472        assert_eq!(order.get_interval_index(&var, &interval1).unwrap(), 0);
473
474        let interval2 = Interval::new(
475            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
476            false,
477            IntervalBoundary::Infty,
478            true,
479        );
480        let err = order.get_interval_index(&var, &interval2);
481        assert!(err.is_err());
482        assert!(matches!(
483            err.unwrap_err(),
484            IntervalOrderError::IntervalNotFound { .. }
485        ));
486    }
487
488    #[test]
489    fn get_interval_index_multi_var() {
490        let var1 = Variable::new("x");
491        let var2 = Variable::new("y");
492        let sum = WeightedSum::new(BTreeMap::from([(var1.clone(), 1), (var2.clone(), 1)]));
493        let interval1 = Interval::new(
494            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
495            false,
496            IntervalBoundary::Infty,
497            true,
498        );
499
500        let mut internal_order = HashMap::new();
501        internal_order.insert(sum.clone(), vec![interval1.clone()]);
502
503        let order = StaticIntervalOrder {
504            single_var_order: HashMap::new(),
505            multi_var_order: internal_order,
506            equal_boundaries: HashMap::new(),
507        };
508
509        assert_eq!(order.get_interval_index(&sum, &interval1).unwrap(), 0);
510
511        let interval2 = Interval::new(
512            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
513            false,
514            IntervalBoundary::Infty,
515            true,
516        );
517        let err = order.get_interval_index(&sum, &interval2);
518        assert!(err.is_err());
519        assert!(matches!(
520            err.unwrap_err(),
521            IntervalOrderError::IntervalNotFound { .. }
522        ));
523    }
524
525    #[test]
526    fn test_get_interval_by_index_single_var() {
527        let var = Variable::new("x");
528        let interval1 = Interval::new(
529            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
530            false,
531            IntervalBoundary::Infty,
532            true,
533        );
534
535        let mut internal_order = HashMap::new();
536        internal_order.insert(var.clone(), vec![interval1.clone()]);
537
538        let order = StaticIntervalOrder {
539            single_var_order: internal_order,
540            multi_var_order: HashMap::new(),
541            equal_boundaries: HashMap::new(),
542        };
543
544        assert_eq!(order.get_interval_by_index(&var, 0).unwrap(), &interval1);
545        assert_eq!(order.get_interval_by_index(&var, 1).unwrap(), &interval1);
546    }
547
548    #[test]
549    fn get_interval_by_index_multi_var() {
550        let var1 = Variable::new("x");
551        let var2 = Variable::new("y");
552        let sum = WeightedSum::new(BTreeMap::from([(var1.clone(), 1), (var2.clone(), 1)]));
553        let interval1 = Interval::new(
554            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
555            false,
556            IntervalBoundary::Infty,
557            true,
558        );
559
560        let mut internal_order = HashMap::new();
561        internal_order.insert(sum.clone(), vec![interval1.clone()]);
562
563        let order = StaticIntervalOrder {
564            single_var_order: HashMap::new(),
565            multi_var_order: internal_order,
566            equal_boundaries: HashMap::new(),
567        };
568
569        assert_eq!(order.get_interval_by_index(&sum, 0).unwrap(), &interval1);
570        assert_eq!(order.get_interval_by_index(&sum, 1).unwrap(), &interval1);
571    }
572
573    #[test]
574    fn test_interval_order_lt() {
575        let var = Variable::new("x");
576        let interval1 = Interval::new(
577            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
578            false,
579            IntervalBoundary::Infty,
580            true,
581        );
582        let interval2 = Interval::new(
583            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
584            false,
585            IntervalBoundary::Infty,
586            true,
587        );
588        let mut internal_order = HashMap::new();
589        internal_order.insert(var.clone(), vec![interval1.clone(), interval2.clone()]);
590        let order = StaticIntervalOrder {
591            single_var_order: internal_order,
592            multi_var_order: HashMap::new(),
593            equal_boundaries: HashMap::new(),
594        };
595
596        assert!(order.lt(&var, &interval1, &interval2).unwrap());
597        assert!(!order.lt(&var, &interval2, &interval1).unwrap());
598    }
599
600    #[test]
601    fn test_interval_order_gt() {
602        let var = Variable::new("x");
603        let interval1 = Interval::new(
604            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
605            false,
606            IntervalBoundary::Infty,
607            true,
608        );
609        let interval2 = Interval::new(
610            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
611            false,
612            IntervalBoundary::Infty,
613            true,
614        );
615        let mut internal_order = HashMap::new();
616        internal_order.insert(var.clone(), vec![interval1.clone(), interval2.clone()]);
617        let order = StaticIntervalOrder {
618            single_var_order: internal_order,
619            multi_var_order: HashMap::new(),
620            equal_boundaries: HashMap::new(),
621        };
622
623        assert!(order.gt(&var, &interval2, &interval1).unwrap());
624        assert!(!order.gt(&var, &interval1, &interval2).unwrap());
625    }
626
627    #[test]
628    fn test_get_next_interval() {
629        let var = Variable::new("x");
630        let interval1 = Interval::new(
631            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
632            false,
633            IntervalBoundary::Infty,
634            true,
635        );
636        let interval2 = Interval::new(
637            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
638            false,
639            IntervalBoundary::Infty,
640            true,
641        );
642        let mut internal_order = HashMap::new();
643        internal_order.insert(var.clone(), vec![interval1.clone(), interval2.clone()]);
644        let order = StaticIntervalOrder {
645            single_var_order: internal_order,
646            multi_var_order: HashMap::new(),
647            equal_boundaries: HashMap::new(),
648        };
649
650        assert_eq!(
651            order.get_next_interval(&var, &interval1).unwrap(),
652            Some(&interval2)
653        );
654        assert_eq!(order.get_next_interval(&var, &interval2).unwrap(), None);
655    }
656
657    #[test]
658    fn test_get_previous_interval() {
659        let var = Variable::new("x");
660        let interval1 = Interval::new(
661            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
662            false,
663            IntervalBoundary::Infty,
664            true,
665        );
666        let interval2 = Interval::new(
667            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
668            false,
669            IntervalBoundary::Infty,
670            true,
671        );
672        let mut internal_order = HashMap::new();
673        internal_order.insert(var.clone(), vec![interval1.clone(), interval2.clone()]);
674        let order = StaticIntervalOrder {
675            single_var_order: internal_order,
676            multi_var_order: HashMap::new(),
677            equal_boundaries: HashMap::new(),
678        };
679
680        assert_eq!(
681            order.get_previous_interval(&var, &interval2).unwrap(),
682            Some(&interval1)
683        );
684        assert_eq!(order.get_previous_interval(&var, &interval1).unwrap(), None);
685    }
686
687    #[test]
688    fn test_get_number_of_intervals() {
689        let var = Variable::new("x");
690        let interval1 = Interval::new(
691            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
692            false,
693            IntervalBoundary::Infty,
694            true,
695        );
696        let interval2 = Interval::new(
697            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
698            false,
699            IntervalBoundary::Infty,
700            true,
701        );
702        let mut internal_order = HashMap::new();
703        internal_order.insert(var.clone(), vec![interval1, interval2]);
704        let order = StaticIntervalOrder {
705            single_var_order: internal_order,
706            multi_var_order: HashMap::new(),
707            equal_boundaries: HashMap::new(),
708        };
709
710        assert_eq!(order.get_number_of_intervals(&var).unwrap(), 2);
711    }
712
713    #[test]
714    fn test_empty_intervals() {
715        let var = Variable::new("x");
716        let mut internal_order = HashMap::new();
717        internal_order.insert(var.clone(), vec![]);
718        let order = StaticIntervalOrder {
719            single_var_order: internal_order,
720            multi_var_order: HashMap::new(),
721            equal_boundaries: HashMap::new(),
722        };
723
724        assert_eq!(order.get_number_of_intervals(&var).unwrap(), 0);
725    }
726
727    #[test]
728    fn test_variable_not_found() {
729        let var = Variable::new("x");
730        let order = StaticIntervalOrder {
731            single_var_order: HashMap::new(),
732            multi_var_order: HashMap::new(),
733            equal_boundaries: HashMap::new(),
734        };
735
736        assert!(order.get_number_of_intervals(&var).is_err());
737    }
738
739    #[test]
740    fn test_interval_order_with_multiple_variables() {
741        let var1 = Variable::new("x");
742        let var2 = Variable::new("y");
743        let interval1 = Interval::new(
744            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
745            false,
746            IntervalBoundary::Infty,
747            true,
748        );
749        let interval2 = Interval::new(
750            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
751            false,
752            IntervalBoundary::Infty,
753            true,
754        );
755
756        let mut internal_order = HashMap::new();
757        internal_order.insert(var1.clone(), vec![interval1.clone()]);
758        internal_order.insert(var2.clone(), vec![interval2.clone()]);
759
760        let order = StaticIntervalOrder {
761            single_var_order: internal_order,
762            multi_var_order: HashMap::new(),
763            equal_boundaries: HashMap::new(),
764        };
765
766        assert_eq!(order.get_number_of_intervals(&var1).unwrap(), 1);
767        assert_eq!(order.get_number_of_intervals(&var2).unwrap(), 1);
768        assert!(
769            order
770                .get_next_interval(&var1, &interval1)
771                .unwrap()
772                .is_none()
773        );
774        assert!(
775            order
776                .get_next_interval(&var2, &interval2)
777                .unwrap()
778                .is_none()
779        );
780        assert!(
781            order
782                .get_previous_interval(&var1, &interval1)
783                .unwrap()
784                .is_none()
785        );
786        assert!(
787            order
788                .get_previous_interval(&var2, &interval2)
789                .unwrap()
790                .is_none()
791        );
792    }
793
794    #[test]
795    fn test_get_intervals_of_threshold() {
796        let var = Variable::new("x");
797        let interval1 = Interval::new(
798            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
799            false,
800            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
801            false,
802        );
803        let interval2 = Interval::new(
804            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
805            false,
806            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
807            false,
808        );
809        let interval3 = Interval::new(
810            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 3)),
811            false,
812            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 3)),
813            false,
814        );
815
816        let mut internal_order = HashMap::new();
817        internal_order.insert(
818            var.clone(),
819            vec![interval1.clone(), interval2.clone(), interval3.clone()],
820        );
821
822        let order = StaticIntervalOrder {
823            single_var_order: internal_order,
824            multi_var_order: HashMap::new(),
825            equal_boundaries: HashMap::new(),
826        };
827
828        // Test GEQ threshold
829        let threshold_geq =
830            ThresholdConstraint::new(ThresholdCompOp::Geq, Vec::<(Parameter, Fraction)>::new(), 2);
831        let intervals_geq = order
832            .compute_enabled_intervals_of_threshold(&var, &threshold_geq)
833            .unwrap();
834        assert_eq!(intervals_geq.len(), 2);
835        assert_eq!(intervals_geq, vec![interval2.clone(), interval3.clone()]);
836
837        // Test LT threshold
838        let threshold_lt =
839            ThresholdConstraint::new(ThresholdCompOp::Lt, Vec::<(Parameter, Fraction)>::new(), 3);
840        let intervals_lt = order
841            .compute_enabled_intervals_of_threshold(&var, &threshold_lt)
842            .unwrap();
843        assert_eq!(intervals_lt.len(), 2);
844        assert_eq!(intervals_lt, vec![interval1.clone(), interval2.clone()]);
845    }
846
847    #[test]
848    fn test_get_intervals_of_threshold_err() {
849        let var = Variable::new("x");
850        let interval1 = Interval::new(
851            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
852            false,
853            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
854            false,
855        );
856        let interval2 = Interval::new(
857            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
858            false,
859            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
860            false,
861        );
862        let interval3 = Interval::new(
863            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 3)),
864            false,
865            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 3)),
866            false,
867        );
868
869        let mut internal_order = HashMap::new();
870        internal_order.insert(
871            var.clone(),
872            vec![interval1.clone(), interval2.clone(), interval3.clone()],
873        );
874
875        let order = StaticIntervalOrder {
876            single_var_order: internal_order,
877            multi_var_order: HashMap::new(),
878            equal_boundaries: HashMap::new(),
879        };
880
881        // Test threshold not found
882        let threshold =
883            ThresholdConstraint::new(ThresholdCompOp::Geq, Vec::<(Parameter, Fraction)>::new(), 4);
884        let err = order.compute_enabled_intervals_of_threshold(&var, &threshold);
885        assert!(err.is_err());
886        assert!(matches!(
887            err.unwrap_err(),
888            IntervalOrderError::ThresholdExtractionError { .. }
889        ));
890    }
891
892    #[test]
893    fn test_get_zero_interval() {
894        let var = Variable::new("x");
895        let interval1 = Interval::new(
896            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
897            false,
898            IntervalBoundary::Infty,
899            false,
900        );
901        let interval2 = Interval::new(
902            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
903            false,
904            IntervalBoundary::Infty,
905            false,
906        );
907        let mut internal_order = HashMap::new();
908        internal_order.insert(var.clone(), vec![interval1.clone(), interval2.clone()]);
909        let order = StaticIntervalOrder {
910            single_var_order: internal_order,
911            multi_var_order: HashMap::new(),
912            equal_boundaries: HashMap::new(),
913        };
914
915        assert_eq!(order.get_zero_interval(&var).unwrap(), &interval1);
916    }
917
918    #[test]
919    fn test_order_to_boolean_expr() {
920        let var = Variable::new("x");
921        let interval1 = Interval::new(
922            IntervalBoundary::from_const(1),
923            false,
924            IntervalBoundary::from_const(2),
925            true,
926        );
927        let interval2 = Interval::new(
928            IntervalBoundary::from_const(2),
929            false,
930            IntervalBoundary::Infty,
931            true,
932        );
933
934        let ib1 = IntervalBoundary::new_bound(WeightedSum::new([(Parameter::new("n"), 1)]), 0);
935        let ib2 = IntervalBoundary::new_bound(WeightedSum::new([(Parameter::new("n"), 2)]), 0);
936
937        let mut internal_order = HashMap::new();
938        internal_order.insert(var.clone(), vec![interval1.clone(), interval2.clone()]);
939        let order = StaticIntervalOrder {
940            single_var_order: HashMap::from([(
941                var.clone(),
942                vec![interval1.clone(), interval2.clone()],
943            )]),
944            multi_var_order: HashMap::new(),
945            equal_boundaries: HashMap::from([(ib2, ib1)]),
946        };
947
948        let exprs = order.order_to_boolean_expr::<Parameter>();
949
950        assert_eq!(exprs.len(), 2);
951
952        let expected_expr_1 = BooleanExpression::ComparisonExpression(
953            Box::new(IntegerExpression::Const(1)),
954            ComparisonOp::Lt,
955            Box::new(IntegerExpression::Const(2)),
956        );
957        assert!(exprs.contains(&expected_expr_1));
958
959        let expected_expr_2 = BooleanExpression::ComparisonExpression(
960            Box::new(IntegerExpression::Const(2) * IntegerExpression::Param(Parameter::new("n"))),
961            ComparisonOp::Eq,
962            Box::new(IntegerExpression::Param(Parameter::new("n"))),
963        );
964        assert!(exprs.contains(&expected_expr_2));
965    }
966
967    #[test]
968    fn test_order_to_boolean_expr_skips_exact_intervals() {
969        let sum = WeightedSum::new(BTreeMap::from([
970            (Variable::new("x"), 1),
971            (Variable::new("y"), 1),
972        ]));
973        let ib = IntervalBoundary::from_const(2);
974        let intervals = vec![
975            Interval::new(IntervalBoundary::from_const(0), false, ib.clone(), true),
976            Interval::new(ib.clone(), false, ib.clone(), false),
977            Interval::new(ib, true, IntervalBoundary::Infty, true),
978        ];
979
980        let order = StaticIntervalOrder {
981            single_var_order: HashMap::from([(Variable::new("z"), intervals.clone())]),
982            multi_var_order: HashMap::from([(sum, intervals)]),
983            equal_boundaries: HashMap::new(),
984        };
985
986        // `[2, 2]` must not yield the unsatisfiable constraint `2 < 2`
987        let exact = BooleanExpression::ComparisonExpression(
988            Box::new(IntegerExpression::Const(2)),
989            ComparisonOp::Lt,
990            Box::new(IntegerExpression::Const(2)),
991        );
992        let exprs = order.order_to_boolean_expr::<Parameter>();
993        assert_eq!(exprs.len(), 2);
994        assert!(!exprs.contains(&exact));
995    }
996
997    #[test]
998    fn test_display_static_interval_order() {
999        let var1 = Variable::new("x");
1000        let var2 = Variable::new("y");
1001        let sum = WeightedSum::new(BTreeMap::from([(var1.clone(), 1), (var2.clone(), 1)]));
1002        let interval1 = Interval::new(
1003            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
1004            false,
1005            IntervalBoundary::Infty,
1006            false,
1007        );
1008        let interval2 = Interval::new(
1009            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
1010            false,
1011            IntervalBoundary::Infty,
1012            false,
1013        );
1014        let ib = IntervalBoundary::Bound(Threshold::new(
1015            WeightedSum::new([(Parameter::new("n"), 1)]),
1016            0,
1017        ));
1018
1019        let single_var_internal_order = HashMap::from([
1020            (var1.clone(), vec![interval1.clone()]),
1021            (var2.clone(), vec![interval2.clone()]),
1022        ]);
1023
1024        let multi_var_internal_order = HashMap::from([(sum.clone(), vec![interval1.clone()])]);
1025
1026        let order = StaticIntervalOrder {
1027            single_var_order: single_var_internal_order,
1028            multi_var_order: multi_var_internal_order,
1029            equal_boundaries: HashMap::from([(IntervalBoundary::from_const(1), ib)]),
1030        };
1031
1032        let expected =
1033            "intervalOrder {\n    1 == n;\n    x: [1, ∞[;\n    y: [2, ∞[;\n    x + y: [1, ∞[;\n}";
1034        assert_eq!(format!("{order}"), expected);
1035    }
1036}
taco_interval_ta/builder/static_interval_order.rs

taco_interval_ta/builder/
static_interval_order.rs
