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        };
272
273        Ok(result)
274    }
275
276    fn get_zero_interval(&self, t: &T) -> Result<&Interval, IntervalOrderError<T>> {
277        Ok(self.get_intervals(t)?.first().unwrap())
278    }
279
280    fn get_all_intervals_of_t(&self, t: &T) -> Result<&Vec<Interval>, IntervalOrderError<T>> {
281        self.get_intervals(t)
282    }
283
284    fn check_interval_replaced(&self, ib: IntervalBoundary) -> IntervalBoundary {
285        self.check_interval_replaced_by_eq(ib)
286    }
287}
288
289impl IntervalOrder for StaticIntervalOrder {
290    fn order_to_boolean_expr<T: Atomic>(&self) -> Vec<BooleanExpression<T>> {
291        let eq_constr = self.equal_boundaries.iter().map(|(ib_1, ib_2)| {
292            let ib_1 = ib_1.get_threshold().expect("Infinite interval in order");
293            let ib_2 = ib_2.get_threshold().expect("Infinite interval in order");
294
295            ib_1.encode_comparison_to_boolean_expression(ComparisonOp::Eq, ib_2)
296        });
297
298        let single_var_constr = self.single_var_order.iter().flat_map(|(_, intervals)| {
299            intervals
300                .iter()
301                .filter(|i| i.ub() != &IntervalBoundary::Infty)
302                .map(|interval| {
303                    if interval.lb() == &IntervalBoundary::Infty {
304                        debug_assert!(false, "Interval with lower bound ∞ found");
305                        return BooleanExpression::False;
306                    }
307
308                    let lb = interval
309                        .lb()
310                        .get_threshold()
311                        .expect("Infinite interval in order");
312                    let ub = interval
313                        .ub()
314                        .get_threshold()
315                        .expect("Infinite interval in order");
316
317                    lb.encode_comparison_to_boolean_expression(ComparisonOp::Lt, ub)
318                })
319        });
320
321        let multi_var_constr = self.multi_var_order.iter().flat_map(|(_, intervals)| {
322            intervals
323                .iter()
324                .filter(|i| i.ub() != &IntervalBoundary::Infty)
325                .map(|interval| {
326                    if interval.lb() == &IntervalBoundary::Infty {
327                        debug_assert!(false, "Interval with lower bound ∞ found");
328                        return BooleanExpression::False;
329                    }
330
331                    let lb = interval
332                        .lb()
333                        .get_threshold()
334                        .expect("Infinite interval in order");
335                    let ub = interval
336                        .ub()
337                        .get_threshold()
338                        .expect("Infinite interval in order");
339
340                    lb.encode_comparison_to_boolean_expression(ComparisonOp::Lt, ub)
341                })
342        });
343
344        eq_constr
345            .chain(single_var_constr)
346            .chain(multi_var_constr)
347            .collect()
348    }
349}
350
351impl fmt::Display for StaticIntervalOrder {
352    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
353        writeln!(f, "intervalOrder {{")?;
354
355        if !self.equal_boundaries.is_empty() {
356            writeln!(
357                f,
358                "    {};",
359                join_iterator(
360                    self.equal_boundaries
361                        .iter()
362                        .map(|(ib1, ib2)| format!("{ib1} == {ib2}")),
363                    " && "
364                )
365            )?;
366        }
367
368        if !self.single_var_order.is_empty() {
369            let mut sorted_single_var = self.single_var_order.iter().collect::<Vec<_>>();
370            sorted_single_var.sort_by_key(|(a, _)| *a);
371
372            for (var, intervals) in sorted_single_var {
373                writeln!(f, "    {}: {};", var, join_iterator(intervals.iter(), ", "))?;
374            }
375        }
376
377        if !self.multi_var_order.is_empty() {
378            for (var, intervals) in &self.multi_var_order {
379                writeln!(f, "    {}: {};", var, join_iterator(intervals.iter(), ", "))?;
380            }
381        }
382
383        write!(f, "}}")
384    }
385}
386
387/// Builder for generating static interval orders
388pub struct StaticIntervalOrderBuilder {
389    order_generator: SimpleOrderGeneratorContext,
390    vars: Vec<Variable>,
391}
392
393impl StaticIntervalOrderBuilder {
394    /// Create a new static interval order builder
395    pub fn new<T: ThresholdAutomaton>(ta: &T, smt_solver_builder: SMTSolverBuilder) -> Self {
396        let orders = SimpleOrderGeneratorContext::new(ta, smt_solver_builder);
397        let vars = ta.variables().cloned().collect::<Vec<_>>();
398
399        StaticIntervalOrderBuilder {
400            order_generator: orders,
401            vars,
402        }
403    }
404
405    /// Add an interval found for a single variable
406    pub fn add_single_variable_interval(self, var: &Variable, interval: &IntervalBoundary) -> Self {
407        let orders = self
408            .order_generator
409            .extend_order_with_interval_for_single_variable(var, interval);
410
411        StaticIntervalOrderBuilder {
412            order_generator: orders,
413            vars: self.vars,
414        }
415    }
416
417    /// Add an interval found for a sum of variables
418    pub fn add_multi_variable_interval(
419        self,
420        sum: &WeightedSum<Variable>,
421        interval: &IntervalBoundary,
422    ) -> Self {
423        let orders = self
424            .order_generator
425            .extend_order_with_interval_for_multi_variable(sum, interval);
426
427        StaticIntervalOrderBuilder {
428            order_generator: orders,
429            vars: self.vars,
430        }
431    }
432
433    /// Generate all possible orders on intervals
434    pub fn build(self) -> Vec<StaticIntervalOrder> {
435        self.order_generator.build_orders(&self.vars)
436    }
437}
438
439#[cfg(test)]
440mod tests {
441
442    use std::collections::{BTreeMap, HashMap};
443
444    use taco_threshold_automaton::expressions::fraction::Fraction;
445    use taco_threshold_automaton::expressions::{
446        BooleanExpression, ComparisonOp, IntegerExpression, Parameter,
447    };
448
449    use taco_threshold_automaton::expressions::Variable;
450    use taco_threshold_automaton::lia_threshold_automaton::integer_thresholds::{
451        Threshold, ThresholdCompOp, ThresholdConstraint, WeightedSum,
452    };
453
454    use crate::builder::static_interval_order::{DefinesStaticIntervalOrder, StaticIntervalOrder};
455    use crate::interval::{
456        Interval, IntervalBoundary, IntervalOrder, IntervalOrderError, IntervalOrderFor,
457    };
458
459    #[test]
460    fn test_get_interval_index_single_var() {
461        let var = Variable::new("x");
462        let interval1 = Interval::new(
463            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
464            false,
465            IntervalBoundary::Infty,
466            false,
467        );
468
469        let mut internal_order = HashMap::new();
470        internal_order.insert(var.clone(), vec![interval1.clone()]);
471
472        let order = StaticIntervalOrder {
473            single_var_order: internal_order,
474            multi_var_order: HashMap::new(),
475            equal_boundaries: HashMap::new(),
476        };
477
478        assert_eq!(order.get_interval_index(&var, &interval1).unwrap(), 0);
479
480        let interval2 = Interval::new(
481            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
482            false,
483            IntervalBoundary::Infty,
484            true,
485        );
486        let err = order.get_interval_index(&var, &interval2);
487        assert!(err.is_err());
488        assert!(matches!(
489            err.unwrap_err(),
490            IntervalOrderError::IntervalNotFound { .. }
491        ));
492    }
493
494    #[test]
495    fn get_interval_index_multi_var() {
496        let var1 = Variable::new("x");
497        let var2 = Variable::new("y");
498        let sum = WeightedSum::new(BTreeMap::from([(var1.clone(), 1), (var2.clone(), 1)]));
499        let interval1 = Interval::new(
500            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
501            false,
502            IntervalBoundary::Infty,
503            true,
504        );
505
506        let mut internal_order = HashMap::new();
507        internal_order.insert(sum.clone(), vec![interval1.clone()]);
508
509        let order = StaticIntervalOrder {
510            single_var_order: HashMap::new(),
511            multi_var_order: internal_order,
512            equal_boundaries: HashMap::new(),
513        };
514
515        assert_eq!(order.get_interval_index(&sum, &interval1).unwrap(), 0);
516
517        let interval2 = Interval::new(
518            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
519            false,
520            IntervalBoundary::Infty,
521            true,
522        );
523        let err = order.get_interval_index(&sum, &interval2);
524        assert!(err.is_err());
525        assert!(matches!(
526            err.unwrap_err(),
527            IntervalOrderError::IntervalNotFound { .. }
528        ));
529    }
530
531    #[test]
532    fn test_get_interval_by_index_single_var() {
533        let var = Variable::new("x");
534        let interval1 = Interval::new(
535            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
536            false,
537            IntervalBoundary::Infty,
538            true,
539        );
540
541        let mut internal_order = HashMap::new();
542        internal_order.insert(var.clone(), vec![interval1.clone()]);
543
544        let order = StaticIntervalOrder {
545            single_var_order: internal_order,
546            multi_var_order: HashMap::new(),
547            equal_boundaries: HashMap::new(),
548        };
549
550        assert_eq!(order.get_interval_by_index(&var, 0).unwrap(), &interval1);
551        assert_eq!(order.get_interval_by_index(&var, 1).unwrap(), &interval1);
552    }
553
554    #[test]
555    fn get_interval_by_index_multi_var() {
556        let var1 = Variable::new("x");
557        let var2 = Variable::new("y");
558        let sum = WeightedSum::new(BTreeMap::from([(var1.clone(), 1), (var2.clone(), 1)]));
559        let interval1 = Interval::new(
560            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
561            false,
562            IntervalBoundary::Infty,
563            true,
564        );
565
566        let mut internal_order = HashMap::new();
567        internal_order.insert(sum.clone(), vec![interval1.clone()]);
568
569        let order = StaticIntervalOrder {
570            single_var_order: HashMap::new(),
571            multi_var_order: internal_order,
572            equal_boundaries: HashMap::new(),
573        };
574
575        assert_eq!(order.get_interval_by_index(&sum, 0).unwrap(), &interval1);
576        assert_eq!(order.get_interval_by_index(&sum, 1).unwrap(), &interval1);
577    }
578
579    #[test]
580    fn test_interval_order_lt() {
581        let var = Variable::new("x");
582        let interval1 = Interval::new(
583            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
584            false,
585            IntervalBoundary::Infty,
586            true,
587        );
588        let interval2 = Interval::new(
589            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
590            false,
591            IntervalBoundary::Infty,
592            true,
593        );
594        let mut internal_order = HashMap::new();
595        internal_order.insert(var.clone(), vec![interval1.clone(), interval2.clone()]);
596        let order = StaticIntervalOrder {
597            single_var_order: internal_order,
598            multi_var_order: HashMap::new(),
599            equal_boundaries: HashMap::new(),
600        };
601
602        assert!(order.lt(&var, &interval1, &interval2).unwrap());
603        assert!(!order.lt(&var, &interval2, &interval1).unwrap());
604    }
605
606    #[test]
607    fn test_interval_order_gt() {
608        let var = Variable::new("x");
609        let interval1 = Interval::new(
610            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
611            false,
612            IntervalBoundary::Infty,
613            true,
614        );
615        let interval2 = Interval::new(
616            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
617            false,
618            IntervalBoundary::Infty,
619            true,
620        );
621        let mut internal_order = HashMap::new();
622        internal_order.insert(var.clone(), vec![interval1.clone(), interval2.clone()]);
623        let order = StaticIntervalOrder {
624            single_var_order: internal_order,
625            multi_var_order: HashMap::new(),
626            equal_boundaries: HashMap::new(),
627        };
628
629        assert!(order.gt(&var, &interval2, &interval1).unwrap());
630        assert!(!order.gt(&var, &interval1, &interval2).unwrap());
631    }
632
633    #[test]
634    fn test_get_next_interval() {
635        let var = Variable::new("x");
636        let interval1 = Interval::new(
637            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
638            false,
639            IntervalBoundary::Infty,
640            true,
641        );
642        let interval2 = Interval::new(
643            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
644            false,
645            IntervalBoundary::Infty,
646            true,
647        );
648        let mut internal_order = HashMap::new();
649        internal_order.insert(var.clone(), vec![interval1.clone(), interval2.clone()]);
650        let order = StaticIntervalOrder {
651            single_var_order: internal_order,
652            multi_var_order: HashMap::new(),
653            equal_boundaries: HashMap::new(),
654        };
655
656        assert_eq!(
657            order.get_next_interval(&var, &interval1).unwrap(),
658            Some(&interval2)
659        );
660        assert_eq!(order.get_next_interval(&var, &interval2).unwrap(), None);
661    }
662
663    #[test]
664    fn test_get_previous_interval() {
665        let var = Variable::new("x");
666        let interval1 = Interval::new(
667            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
668            false,
669            IntervalBoundary::Infty,
670            true,
671        );
672        let interval2 = Interval::new(
673            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
674            false,
675            IntervalBoundary::Infty,
676            true,
677        );
678        let mut internal_order = HashMap::new();
679        internal_order.insert(var.clone(), vec![interval1.clone(), interval2.clone()]);
680        let order = StaticIntervalOrder {
681            single_var_order: internal_order,
682            multi_var_order: HashMap::new(),
683            equal_boundaries: HashMap::new(),
684        };
685
686        assert_eq!(
687            order.get_previous_interval(&var, &interval2).unwrap(),
688            Some(&interval1)
689        );
690        assert_eq!(order.get_previous_interval(&var, &interval1).unwrap(), None);
691    }
692
693    #[test]
694    fn test_get_number_of_intervals() {
695        let var = Variable::new("x");
696        let interval1 = Interval::new(
697            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
698            false,
699            IntervalBoundary::Infty,
700            true,
701        );
702        let interval2 = Interval::new(
703            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
704            false,
705            IntervalBoundary::Infty,
706            true,
707        );
708        let mut internal_order = HashMap::new();
709        internal_order.insert(var.clone(), vec![interval1, interval2]);
710        let order = StaticIntervalOrder {
711            single_var_order: internal_order,
712            multi_var_order: HashMap::new(),
713            equal_boundaries: HashMap::new(),
714        };
715
716        assert_eq!(order.get_number_of_intervals(&var).unwrap(), 2);
717    }
718
719    #[test]
720    fn test_empty_intervals() {
721        let var = Variable::new("x");
722        let mut internal_order = HashMap::new();
723        internal_order.insert(var.clone(), vec![]);
724        let order = StaticIntervalOrder {
725            single_var_order: internal_order,
726            multi_var_order: HashMap::new(),
727            equal_boundaries: HashMap::new(),
728        };
729
730        assert_eq!(order.get_number_of_intervals(&var).unwrap(), 0);
731    }
732
733    #[test]
734    fn test_variable_not_found() {
735        let var = Variable::new("x");
736        let order = StaticIntervalOrder {
737            single_var_order: HashMap::new(),
738            multi_var_order: HashMap::new(),
739            equal_boundaries: HashMap::new(),
740        };
741
742        assert!(order.get_number_of_intervals(&var).is_err());
743    }
744
745    #[test]
746    fn test_interval_order_with_multiple_variables() {
747        let var1 = Variable::new("x");
748        let var2 = Variable::new("y");
749        let interval1 = Interval::new(
750            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
751            false,
752            IntervalBoundary::Infty,
753            true,
754        );
755        let interval2 = Interval::new(
756            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
757            false,
758            IntervalBoundary::Infty,
759            true,
760        );
761
762        let mut internal_order = HashMap::new();
763        internal_order.insert(var1.clone(), vec![interval1.clone()]);
764        internal_order.insert(var2.clone(), vec![interval2.clone()]);
765
766        let order = StaticIntervalOrder {
767            single_var_order: internal_order,
768            multi_var_order: HashMap::new(),
769            equal_boundaries: HashMap::new(),
770        };
771
772        assert_eq!(order.get_number_of_intervals(&var1).unwrap(), 1);
773        assert_eq!(order.get_number_of_intervals(&var2).unwrap(), 1);
774        assert!(
775            order
776                .get_next_interval(&var1, &interval1)
777                .unwrap()
778                .is_none()
779        );
780        assert!(
781            order
782                .get_next_interval(&var2, &interval2)
783                .unwrap()
784                .is_none()
785        );
786        assert!(
787            order
788                .get_previous_interval(&var1, &interval1)
789                .unwrap()
790                .is_none()
791        );
792        assert!(
793            order
794                .get_previous_interval(&var2, &interval2)
795                .unwrap()
796                .is_none()
797        );
798    }
799
800    #[test]
801    fn test_get_intervals_of_threshold() {
802        let var = Variable::new("x");
803        let interval1 = Interval::new(
804            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
805            false,
806            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
807            false,
808        );
809        let interval2 = Interval::new(
810            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
811            false,
812            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
813            false,
814        );
815        let interval3 = Interval::new(
816            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 3)),
817            false,
818            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 3)),
819            false,
820        );
821
822        let mut internal_order = HashMap::new();
823        internal_order.insert(
824            var.clone(),
825            vec![interval1.clone(), interval2.clone(), interval3.clone()],
826        );
827
828        let order = StaticIntervalOrder {
829            single_var_order: internal_order,
830            multi_var_order: HashMap::new(),
831            equal_boundaries: HashMap::new(),
832        };
833
834        // Test GEQ threshold
835        let threshold_geq =
836            ThresholdConstraint::new(ThresholdCompOp::Geq, Vec::<(Parameter, Fraction)>::new(), 2);
837        let intervals_geq = order
838            .compute_enabled_intervals_of_threshold(&var, &threshold_geq)
839            .unwrap();
840        assert_eq!(intervals_geq.len(), 2);
841        assert_eq!(intervals_geq, vec![interval2.clone(), interval3.clone()]);
842
843        // Test LT threshold
844        let threshold_lt =
845            ThresholdConstraint::new(ThresholdCompOp::Lt, Vec::<(Parameter, Fraction)>::new(), 3);
846        let intervals_lt = order
847            .compute_enabled_intervals_of_threshold(&var, &threshold_lt)
848            .unwrap();
849        assert_eq!(intervals_lt.len(), 2);
850        assert_eq!(intervals_lt, vec![interval1.clone(), interval2.clone()]);
851    }
852
853    #[test]
854    fn test_get_intervals_of_threshold_err() {
855        let var = Variable::new("x");
856        let interval1 = Interval::new(
857            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
858            false,
859            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
860            false,
861        );
862        let interval2 = Interval::new(
863            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
864            false,
865            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
866            false,
867        );
868        let interval3 = Interval::new(
869            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 3)),
870            false,
871            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 3)),
872            false,
873        );
874
875        let mut internal_order = HashMap::new();
876        internal_order.insert(
877            var.clone(),
878            vec![interval1.clone(), interval2.clone(), interval3.clone()],
879        );
880
881        let order = StaticIntervalOrder {
882            single_var_order: internal_order,
883            multi_var_order: HashMap::new(),
884            equal_boundaries: HashMap::new(),
885        };
886
887        // Test threshold not found
888        let threshold =
889            ThresholdConstraint::new(ThresholdCompOp::Geq, Vec::<(Parameter, Fraction)>::new(), 4);
890        let err = order.compute_enabled_intervals_of_threshold(&var, &threshold);
891        assert!(err.is_err());
892        assert!(matches!(
893            err.unwrap_err(),
894            IntervalOrderError::ThresholdExtractionError { .. }
895        ));
896    }
897
898    #[test]
899    fn test_get_zero_interval() {
900        let var = Variable::new("x");
901        let interval1 = Interval::new(
902            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
903            false,
904            IntervalBoundary::Infty,
905            false,
906        );
907        let interval2 = Interval::new(
908            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
909            false,
910            IntervalBoundary::Infty,
911            false,
912        );
913        let mut internal_order = HashMap::new();
914        internal_order.insert(var.clone(), vec![interval1.clone(), interval2.clone()]);
915        let order = StaticIntervalOrder {
916            single_var_order: internal_order,
917            multi_var_order: HashMap::new(),
918            equal_boundaries: HashMap::new(),
919        };
920
921        assert_eq!(order.get_zero_interval(&var).unwrap(), &interval1);
922    }
923
924    #[test]
925    fn test_order_to_boolean_expr() {
926        let var = Variable::new("x");
927        let interval1 = Interval::new(
928            IntervalBoundary::from_const(1),
929            false,
930            IntervalBoundary::from_const(2),
931            true,
932        );
933        let interval2 = Interval::new(
934            IntervalBoundary::from_const(2),
935            false,
936            IntervalBoundary::Infty,
937            true,
938        );
939
940        let ib1 = IntervalBoundary::new_bound(WeightedSum::new([(Parameter::new("n"), 1)]), 0);
941        let ib2 = IntervalBoundary::new_bound(WeightedSum::new([(Parameter::new("n"), 2)]), 0);
942
943        let mut internal_order = HashMap::new();
944        internal_order.insert(var.clone(), vec![interval1.clone(), interval2.clone()]);
945        let order = StaticIntervalOrder {
946            single_var_order: HashMap::from([(
947                var.clone(),
948                vec![interval1.clone(), interval2.clone()],
949            )]),
950            multi_var_order: HashMap::new(),
951            equal_boundaries: HashMap::from([(ib2, ib1)]),
952        };
953
954        let exprs = order.order_to_boolean_expr::<Parameter>();
955
956        assert_eq!(exprs.len(), 2);
957
958        let expected_expr_1 = BooleanExpression::ComparisonExpression(
959            Box::new(IntegerExpression::Const(1)),
960            ComparisonOp::Lt,
961            Box::new(IntegerExpression::Const(2)),
962        );
963        assert!(exprs.contains(&expected_expr_1));
964
965        let expected_expr_2 = BooleanExpression::ComparisonExpression(
966            Box::new(IntegerExpression::Const(2) * IntegerExpression::Param(Parameter::new("n"))),
967            ComparisonOp::Eq,
968            Box::new(IntegerExpression::Param(Parameter::new("n"))),
969        );
970        assert!(exprs.contains(&expected_expr_2));
971    }
972
973    #[test]
974    fn test_display_static_interval_order() {
975        let var1 = Variable::new("x");
976        let var2 = Variable::new("y");
977        let sum = WeightedSum::new(BTreeMap::from([(var1.clone(), 1), (var2.clone(), 1)]));
978        let interval1 = Interval::new(
979            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
980            false,
981            IntervalBoundary::Infty,
982            false,
983        );
984        let interval2 = Interval::new(
985            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
986            false,
987            IntervalBoundary::Infty,
988            false,
989        );
990        let ib = IntervalBoundary::Bound(Threshold::new(
991            WeightedSum::new([(Parameter::new("n"), 1)]),
992            0,
993        ));
994
995        let single_var_internal_order = HashMap::from([
996            (var1.clone(), vec![interval1.clone()]),
997            (var2.clone(), vec![interval2.clone()]),
998        ]);
999
1000        let multi_var_internal_order = HashMap::from([(sum.clone(), vec![interval1.clone()])]);
1001
1002        let order = StaticIntervalOrder {
1003            single_var_order: single_var_internal_order,
1004            multi_var_order: multi_var_internal_order,
1005            equal_boundaries: HashMap::from([(IntervalBoundary::from_const(1), ib)]),
1006        };
1007
1008        let expected =
1009            "intervalOrder {\n    1 == n;\n    x: [1, ∞[;\n    y: [2, ∞[;\n    x + y: [1, ∞[;\n}";
1010        assert_eq!(format!("{order}"), expected);
1011    }
1012}
taco_interval_ta/builder/static_interval_order.rs

taco_interval_ta/builder/
static_interval_order.rs
