taco_interval_ta/
interval.rs

1//! Interval module defining intervals and interval order functionality
2//!
3//! This module defines the `Interval` struct representing an interval and the
4//! `IntervalOrder` trait for accessing an interval order.
5
6use std::fmt::Debug;
7use std::fmt::{self};
8
9use taco_threshold_automaton::expressions::{
10    Atomic, BooleanConnective, BooleanExpression, ComparisonOp, Parameter, fraction::Fraction,
11};
12use taco_threshold_automaton::lia_threshold_automaton::integer_thresholds::{
13    IntoNoDivBooleanExpr, Threshold, ThresholdConstraint, WeightedSum,
14};
15
16use super::HasAssociatedIntervals;
17
18/// Trait for types that define an order among intervals
19///
20/// This trait is implemented by types that define an order among intervals.
21/// This trait provides functions to access the order, e.g., to check if one
22/// interval is before another in the order, get the next interval, etc.
23pub trait IntervalOrderFor<T>: IntervalOrder
24where
25    T: HasAssociatedIntervals,
26{
27    /// Check if in the interval order for `t` the intervals are
28    /// ordered `i1 < i2`
29    ///
30    /// Return `true` if `i1` is before `i2` in the order, `false` otherwise.
31    ///
32    /// The function returns an error if the `t` is not found, or any of the
33    /// intervals `i1`, `i2` do not appear in the interval order for `t`
34    fn lt(&self, t: &T, i1: &Interval, i2: &Interval) -> Result<bool, IntervalOrderError<T>>;
35
36    /// Check if in the interval order for `t` it holds that `i1 > i2`
37    ///
38    /// Return `true` if `i1` appears after `i2` in the order, `false`
39    /// otherwise.
40    ///
41    /// The function returns an error if the `t` is not found, or any of the
42    /// intervals `i1`, `i2` do not appear in the interval order for `t`.
43    fn gt(&self, t: &T, i1: &Interval, i2: &Interval) -> Result<bool, IntervalOrderError<T>>;
44
45    /// Get the zero interval of `t`
46    fn get_zero_interval(&self, t: &T) -> Result<&Interval, IntervalOrderError<T>>;
47
48    /// Get the next interval appearing after `i`  in the order for `t`
49    ///
50    /// Return `None` if `i` is the last interval, or `i` is not in the order
51    /// for `var`
52    fn get_next_interval<'a>(
53        &'a self,
54        t: &T,
55        i: &Interval,
56    ) -> Result<Option<&'a Interval>, IntervalOrderError<T>>;
57
58    /// Get the previous interval of `i` for variable `var`
59    ///
60    /// Return `None` if `i` is the first interval, or `i` is not in the order
61    /// for `var`
62    fn get_previous_interval<'a>(
63        &'a self,
64        var: &T,
65        i: &Interval,
66    ) -> Result<Option<&'a Interval>, IntervalOrderError<T>>;
67
68    /// Get all intervals associated with `t`
69    ///
70    /// Return an error if the variable `t` is not found in the interval order,
71    /// otherwise returns the intervals associated with `t`
72    fn get_all_intervals_of_t(&self, t: &T) -> Result<&Vec<Interval>, IntervalOrderError<T>>;
73
74    /// Get the number of intervals associated with `t`
75    fn get_number_of_intervals(&self, t: &T) -> Result<usize, IntervalOrderError<T>>;
76
77    /// Get the intervals of `t` where `thr` is enabled
78    fn compute_enabled_intervals_of_threshold(
79        &self,
80        t: &T,
81        thr: &ThresholdConstraint,
82    ) -> Result<Vec<Interval>, IntervalOrderError<T>>;
83
84    /// Check whether the interval order replaces the interval boundary
85    ///
86    /// This method checks if the interval boundary `ib` is replaced by the
87    /// interval order. If the interval boundary is replaced, the method returns
88    /// the new interval boundary that replaces `ib`. If the interval boundary
89    /// is not replaced, the method returns the original interval boundary.
90    ///
91    /// An interval might have been replaced if the interval boundary is
92    /// considered equal to another boundary in the order.
93    fn check_interval_replaced(&self, ib: IntervalBoundary) -> IntervalBoundary;
94}
95
96/// Common trait of interval orders
97pub trait IntervalOrder {
98    /// Convert the order to a boolean expression
99    ///
100    /// This method converts the interval order to a boolean expression. This
101    /// constraint can for example be appended to the resilience condition of a
102    /// threshold automaton to ensure that the assumed order is satisfied.
103    fn order_to_boolean_expr<T: Atomic>(&self) -> Vec<BooleanExpression<T>>;
104}
105
106/// Error that can occur when accessing interval order
107#[derive(Debug, Clone, PartialEq)]
108pub enum IntervalOrderError<T>
109where
110    T: HasAssociatedIntervals,
111{
112    /// Interval was not found in the interval order for variable
113    IntervalNotFound {
114        /// Variable for which the lookup failed
115        var: T,
116        /// Interval for which the lookup failed
117        interval: Interval,
118    },
119    /// Variable was not found in the interval order
120    VariableNotFound {
121        /// Variable for which the lookup failed
122        var: T,
123    },
124
125    /// Error while extracting intervals from threshold, the associated interval has not been found in the order
126    ThresholdExtractionError {
127        /// Variable for which the lookup failed
128        var: T,
129        /// Threshold for which the lookup failed
130        thr: ThresholdConstraint,
131    },
132}
133
134impl<T: HasAssociatedIntervals> std::error::Error for IntervalOrderError<T> {}
135
136impl<T: HasAssociatedIntervals> fmt::Display for IntervalOrderError<T> {
137    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
138        write!(f, "Error when accessing interval order: ")?;
139
140        match self {
141            IntervalOrderError::IntervalNotFound { var, interval } => write!(
142                f,
143                "The interval {interval} has not been found in the interval order for {var}"
144            ),
145            IntervalOrderError::VariableNotFound { var } => write!(
146                f,
147                "The variable {var} has not been found in the interval order"
148            ),
149            IntervalOrderError::ThresholdExtractionError { var, thr } => write!(
150                f,
151                "Extraction of threshold from order failed: For variable {var} and threshold {thr} no interval matches the threshold"
152            ),
153        }
154    }
155}
156
157/// Interval
158#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
159pub struct Interval {
160    /// Lower / left boundary of the interval
161    lb: IntervalBoundary,
162    /// Lower / left boundary of the interval is open / closed
163    lb_open: bool,
164    /// Upper / right boundary of the interval
165    ub: IntervalBoundary,
166    /// Upper / right boundary of the interval is open / closed
167    ub_open: bool,
168}
169
170impl Interval {
171    /// Create a new interval
172    pub fn new(
173        lb: IntervalBoundary,
174        mut lb_open: bool,
175        ub: IntervalBoundary,
176        mut ub_open: bool,
177    ) -> Self {
178        if lb == IntervalBoundary::Infty {
179            lb_open = true;
180        }
181
182        if ub == IntervalBoundary::Infty {
183            ub_open = true;
184        }
185
186        Self {
187            lb,
188            lb_open,
189            ub,
190            ub_open,
191        }
192    }
193
194    /// Check if the interval is left open, i.e., the lower boundary is not included
195    pub fn is_left_open(&self) -> bool {
196        self.lb_open
197    }
198
199    /// Check if the interval is right open, i.e., the upper boundary is not included
200    pub fn is_right_open(&self) -> bool {
201        self.ub_open
202    }
203
204    /// Returns the left IntervalBoundary
205    pub fn lb(&self) -> &IntervalBoundary {
206        &self.lb
207    }
208
209    /// Returns the right IntervalBoundary
210    pub fn ub(&self) -> &IntervalBoundary {
211        &self.ub
212    }
213
214    /// Return the interval `[0, 1[`
215    pub fn zero() -> Self {
216        Self::new_constant(0, 1)
217    }
218
219    /// Create a new interval of the form `[ c_lower_bound, c_upper_bound [` where `c_lower_bound` and `c_upper_bound`
220    /// are constants
221    pub fn new_constant<T: Into<Fraction>, U: Into<Fraction>>(
222        c_lower_bound: T,
223        c_upper_bound: U,
224    ) -> Self {
225        Self {
226            lb: IntervalBoundary::from_const(c_lower_bound),
227            lb_open: false,
228            ub: IntervalBoundary::from_const(c_upper_bound),
229            ub_open: true,
230        }
231    }
232
233    /// Check if the given interval boundary is contained in the interval
234    ///
235    /// This method *does not* do any mathematical / symbolical
236    /// checks to determine if the interval boundary is contained in the
237    /// interval. It only checks if the one of the boundaries of the interval is
238    /// equal to the given interval boundary and that this boundary is not open.
239    pub fn check_is_contained(&self, ib: &IntervalBoundary) -> bool {
240        (self.lb == *ib && !self.lb_open) || (self.ub == *ib && !self.ub_open)
241    }
242
243    /// Checks whether an addition of `c` to the interval must always leave the
244    /// interval
245    ///
246    /// This function will first check whether both intervals are constants, if
247    /// this is not the case, it returns false, as we cannot statically
248    /// determine the size of the interval.
249    /// If both are constant, it will check whether adding `c` to the lower
250    /// bound will be sufficient to move past the upper bound.
251    pub fn check_add_always_out_of_interval(&self, c: u32) -> bool {
252        if let (Some(lc), Some(uc)) = (self.lb.try_is_constant(), self.ub.try_is_constant()) {
253            let res = lc + c.into();
254            if self.ub_open || self.lb_open {
255                return res >= uc;
256            }
257
258            return res > uc;
259        }
260        false
261    }
262
263    /// Checks whether an addition of `c` from the interval must always leave
264    /// the interval
265    ///
266    /// This function will first check whether both intervals are constants, if
267    /// this is not the case, it returns false, as we cannot statically
268    /// determine the size of the interval.
269    /// If both are constant, it will check whether subtracting `c` from the
270    /// upper bound will be sufficient to move below the lower bound.
271    pub fn check_sub_always_out_of_interval(&self, c: u32) -> bool {
272        self.check_add_always_out_of_interval(c)
273    }
274
275    /// Encode the interval as a boolean expression on a variable
276    ///
277    /// This method encodes the interval as a boolean expression on a variable
278    /// `var`. The boolean expression is true if the variable is in the interval
279    /// and false otherwise.
280    pub fn encode_into_boolean_expr<S, T>(&self, var: &S) -> BooleanExpression<T>
281    where
282        S: IntoNoDivBooleanExpr<T> + Clone,
283        T: Atomic,
284    {
285        // encode the lower bound of the interval
286        let lb = match &self.lb {
287            IntervalBoundary::Bound(lb) => {
288                let op = if self.lb_open {
289                    ComparisonOp::Gt
290                } else {
291                    ComparisonOp::Geq
292                };
293
294                var.encode_comparison_to_boolean_expression(op, lb)
295            }
296            IntervalBoundary::Infty => return BooleanExpression::False,
297        };
298
299        // encode the upper bound of the interval
300        let ub = match &self.ub {
301            IntervalBoundary::Bound(ub) => {
302                let op = if self.ub_open {
303                    ComparisonOp::Lt
304                } else {
305                    ComparisonOp::Leq
306                };
307
308                var.encode_comparison_to_boolean_expression(op, ub)
309            }
310            IntervalBoundary::Infty => BooleanExpression::True,
311        };
312
313        BooleanExpression::BinaryExpression(Box::new(lb), BooleanConnective::And, Box::new(ub))
314    }
315}
316
317/// Boundary of an interval
318#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
319pub enum IntervalBoundary {
320    /// Infinite boundary
321    Infty,
322    /// Bound of an interval
323    Bound(Threshold),
324}
325
326impl IntervalBoundary {
327    /// Create a new interval boundary representing the unbounded interval
328    /// border `∞`
329    pub fn new_infty() -> IntervalBoundary {
330        IntervalBoundary::Infty
331    }
332
333    /// Create a new interval boundary representing a bound
334    /// `param * x + constant`
335    pub fn new_bound<T: Into<WeightedSum<Parameter>>, U: Into<Fraction>>(
336        param: T,
337        constant: U,
338    ) -> IntervalBoundary {
339        IntervalBoundary::Bound(Threshold::new(param, constant))
340    }
341
342    /// Create a new interval boundary representing a constant
343    pub fn from_const<T: Into<Fraction>>(constant: T) -> IntervalBoundary {
344        IntervalBoundary::Bound(Threshold::from_const(constant))
345    }
346
347    /// If the interval boundary is a constant without parameters, this
348    /// function returns the constant
349    pub fn try_is_constant(&self) -> Option<Fraction> {
350        match self {
351            IntervalBoundary::Infty => None,
352            IntervalBoundary::Bound(thr) => thr.get_const(),
353        }
354    }
355
356    /// Get the integer expression of the interval boundary
357    ///
358    /// Returns `None` if the boundary is infinite, otherwise returns the
359    /// threshold
360    pub fn get_threshold(&self) -> Option<&Threshold> {
361        match self {
362            IntervalBoundary::Infty => None,
363            IntervalBoundary::Bound(threshold) => Some(threshold),
364        }
365    }
366
367    /// Extract the interval boundary from a threshold
368    pub fn from_threshold_constraint(trc: &ThresholdConstraint) -> IntervalBoundary {
369        let tr = trc.get_threshold().clone();
370
371        IntervalBoundary::Bound(tr)
372    }
373}
374
375impl fmt::Display for Interval {
376    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
377        if self.lb_open {
378            write!(f, "]")?;
379        } else {
380            write!(f, "[")?;
381        }
382
383        write!(f, "{}, {}", self.lb, self.ub)?;
384
385        if self.ub_open {
386            write!(f, "[")
387        } else {
388            write!(f, "]")
389        }
390    }
391}
392
393impl fmt::Display for IntervalBoundary {
394    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
395        match self {
396            IntervalBoundary::Infty => write!(f, "∞"),
397            IntervalBoundary::Bound(tr) => {
398                write!(f, "{tr}")
399            }
400        }
401    }
402}
403
404#[cfg(test)]
405mod tests {
406
407    use taco_threshold_automaton::{
408        expressions::{
409            BooleanExpression, ComparisonOp, IntegerExpression, Parameter, Variable,
410            fraction::Fraction,
411        },
412        lia_threshold_automaton::integer_thresholds::{
413            Threshold, ThresholdCompOp, ThresholdConstraint, WeightedSum,
414        },
415    };
416
417    use crate::interval::{Interval, IntervalBoundary, IntervalOrderError};
418
419    #[allow(clippy::cognitive_complexity)]
420    #[test]
421    fn test_check_add_always_out_of_interval() {
422        let lb = IntervalBoundary::from_const(1);
423        let ub = IntervalBoundary::from_const(42);
424
425        let i = Interval::new(lb.clone(), false, ub.clone(), false);
426        assert!(!i.check_add_always_out_of_interval(0));
427        assert!(!i.check_add_always_out_of_interval(1));
428        assert!(!i.check_add_always_out_of_interval(41));
429        assert!(i.check_add_always_out_of_interval(42));
430        assert!(i.check_add_always_out_of_interval(43));
431        assert!(i.check_add_always_out_of_interval(100));
432
433        let i = Interval::new(lb.clone(), true, ub.clone(), false);
434        assert!(!i.check_add_always_out_of_interval(0));
435        assert!(!i.check_add_always_out_of_interval(1));
436        assert!(i.check_add_always_out_of_interval(41));
437        assert!(i.check_add_always_out_of_interval(42));
438        assert!(i.check_add_always_out_of_interval(43));
439        assert!(i.check_add_always_out_of_interval(100));
440
441        let i = Interval::new(lb.clone(), false, ub.clone(), true);
442        assert!(!i.check_add_always_out_of_interval(0));
443        assert!(!i.check_add_always_out_of_interval(1));
444        assert!(i.check_add_always_out_of_interval(41));
445        assert!(i.check_add_always_out_of_interval(42));
446        assert!(i.check_add_always_out_of_interval(43));
447        assert!(i.check_add_always_out_of_interval(100));
448
449        let i = Interval::new(lb.clone(), true, ub.clone(), true);
450        assert!(!i.check_add_always_out_of_interval(0));
451        assert!(!i.check_add_always_out_of_interval(1));
452        assert!(i.check_add_always_out_of_interval(41));
453        assert!(i.check_add_always_out_of_interval(42));
454        assert!(i.check_add_always_out_of_interval(43));
455        assert!(i.check_add_always_out_of_interval(100));
456
457        let ub = IntervalBoundary::from_threshold_constraint(&ThresholdConstraint::new(
458            ThresholdCompOp::Lt,
459            WeightedSum::new([(Parameter::new("n"), 1)]),
460            0,
461        ));
462        let i = Interval::new(lb.clone(), true, ub.clone(), true);
463        assert!(!i.check_add_always_out_of_interval(0));
464        assert!(!i.check_add_always_out_of_interval(1));
465        assert!(!i.check_add_always_out_of_interval(41));
466        assert!(!i.check_add_always_out_of_interval(42));
467        assert!(!i.check_add_always_out_of_interval(43));
468        assert!(!i.check_add_always_out_of_interval(100));
469    }
470
471    #[allow(clippy::cognitive_complexity)]
472    #[test]
473    fn test_check_sub_always_out_of_interval() {
474        let lb = IntervalBoundary::from_const(1);
475        let ub = IntervalBoundary::from_const(42);
476
477        let i = Interval::new(lb.clone(), false, ub.clone(), false);
478        assert!(!i.check_sub_always_out_of_interval(0));
479        assert!(!i.check_sub_always_out_of_interval(1));
480        assert!(!i.check_sub_always_out_of_interval(41));
481        assert!(i.check_sub_always_out_of_interval(42));
482        assert!(i.check_sub_always_out_of_interval(43));
483        assert!(i.check_sub_always_out_of_interval(100));
484
485        let i = Interval::new(lb.clone(), true, ub.clone(), false);
486        assert!(!i.check_sub_always_out_of_interval(0));
487        assert!(!i.check_sub_always_out_of_interval(1));
488        assert!(i.check_sub_always_out_of_interval(41));
489        assert!(i.check_sub_always_out_of_interval(42));
490        assert!(i.check_sub_always_out_of_interval(43));
491        assert!(i.check_sub_always_out_of_interval(100));
492
493        let i = Interval::new(lb.clone(), false, ub.clone(), true);
494        assert!(!i.check_sub_always_out_of_interval(0));
495        assert!(!i.check_sub_always_out_of_interval(1));
496        assert!(i.check_sub_always_out_of_interval(41));
497        assert!(i.check_sub_always_out_of_interval(42));
498        assert!(i.check_sub_always_out_of_interval(43));
499        assert!(i.check_sub_always_out_of_interval(100));
500
501        let i = Interval::new(lb.clone(), true, ub.clone(), true);
502        assert!(!i.check_sub_always_out_of_interval(0));
503        assert!(!i.check_sub_always_out_of_interval(1));
504        assert!(i.check_sub_always_out_of_interval(41));
505        assert!(i.check_sub_always_out_of_interval(42));
506        assert!(i.check_sub_always_out_of_interval(43));
507        assert!(i.check_sub_always_out_of_interval(100));
508
509        let ub = IntervalBoundary::from_threshold_constraint(&ThresholdConstraint::new(
510            ThresholdCompOp::Lt,
511            WeightedSum::new([(Parameter::new("n"), 1)]),
512            0,
513        ));
514        let i = Interval::new(lb.clone(), true, ub.clone(), true);
515        assert!(!i.check_sub_always_out_of_interval(0));
516        assert!(!i.check_sub_always_out_of_interval(1));
517        assert!(!i.check_sub_always_out_of_interval(41));
518        assert!(!i.check_sub_always_out_of_interval(42));
519        assert!(!i.check_sub_always_out_of_interval(43));
520        assert!(!i.check_sub_always_out_of_interval(100));
521
522        let lb = IntervalBoundary::from_const(1);
523        let ub = IntervalBoundary::from_const(3);
524        let i = Interval::new(lb.clone(), false, ub.clone(), true);
525        assert!(!i.check_sub_always_out_of_interval(1));
526    }
527
528    #[test]
529    fn test_new_interval() {
530        let lb = IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1));
531        let ub = IntervalBoundary::Infty;
532
533        let interval = Interval::new(lb.clone(), false, ub.clone(), true);
534        assert_eq!(interval.lb, lb);
535        assert!(!interval.lb_open);
536        assert_eq!(interval.ub, ub);
537        assert!(interval.ub_open);
538
539        let interval = Interval::new(lb.clone(), true, ub.clone(), false);
540        assert_eq!(interval.lb, lb);
541        assert!(interval.lb_open);
542        assert_eq!(interval.ub, ub);
543        assert!(interval.ub_open);
544    }
545
546    #[test]
547    fn test_get_threshold_interval() {
548        let lb = IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 42));
549        let ub = IntervalBoundary::Infty;
550
551        assert_eq!(lb.get_threshold(), Some(&Threshold::from_const(42)));
552        assert_eq!(ub.get_threshold(), None);
553    }
554
555    #[test]
556    fn test_is_open_methods() {
557        let interval = Interval::new_constant(0, 1);
558        assert!(!interval.is_left_open());
559        assert!(interval.is_right_open());
560
561        let interval = Interval::new_constant(0, 1);
562        assert!(!interval.is_left_open());
563        assert!(interval.is_right_open());
564
565        let interval = Interval::new_constant(0, 1);
566        assert!(!interval.is_left_open());
567        assert!(interval.is_right_open());
568
569        let interval = Interval::new_constant(0, 1);
570        assert!(!interval.is_left_open());
571        assert!(interval.is_right_open());
572    }
573
574    #[test]
575    fn test_interval_lookup_error_display() {
576        let var = Variable::new("x");
577        let interval = Interval {
578            lb: IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
579            lb_open: false,
580            ub: IntervalBoundary::Infty,
581            ub_open: true,
582        };
583
584        let error = IntervalOrderError::IntervalNotFound {
585            var: var.clone(),
586            interval: interval.clone(),
587        };
588        assert!(error.to_string().contains(&var.to_string()));
589        assert!(error.to_string().contains(&interval.to_string()));
590
591        let error = IntervalOrderError::VariableNotFound { var: var.clone() };
592        assert!(error.to_string().contains(&var.to_string()));
593
594        let thr =
595            ThresholdConstraint::new(ThresholdCompOp::Geq, Vec::<(Parameter, Fraction)>::new(), 2);
596        let error = IntervalOrderError::ThresholdExtractionError {
597            var: var.clone(),
598            thr: thr.clone(),
599        };
600        assert!(error.to_string().contains(&var.to_string()));
601        assert!(error.to_string().contains(&thr.to_string()));
602    }
603
604    #[test]
605    fn test_interval_display() {
606        let interval1 = Interval {
607            lb: IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1)),
608            lb_open: false,
609            ub: IntervalBoundary::Infty,
610            ub_open: true,
611        };
612        let interval2 = Interval {
613            lb: IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 2)),
614            lb_open: true,
615            ub: IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 3)),
616            ub_open: false,
617        };
618
619        assert_eq!(interval1.to_string(), "[1, ∞[");
620        assert_eq!(interval2.to_string(), "]2, 3]");
621    }
622
623    #[test]
624    fn test_interval_boundary_display() {
625        let boundary1 = IntervalBoundary::Infty;
626        let boundary2 = IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 5));
627        let boundary3 = IntervalBoundary::Bound(Threshold::new(
628            WeightedSum::new_empty(),
629            -(Fraction::from(3)),
630        ));
631        let boundary4 = IntervalBoundary::Bound(Threshold::new(
632            WeightedSum::new([(Parameter::new("x"), 1)]),
633            0,
634        ));
635        let boundary5 = IntervalBoundary::Bound(Threshold::new(
636            WeightedSum::new([(Parameter::new("x"), 2)]),
637            5,
638        ));
639
640        assert_eq!(boundary1.to_string(), "∞");
641        assert_eq!(boundary2.to_string(), "5");
642        assert_eq!(boundary3.to_string(), "-3");
643        assert_eq!(boundary4.to_string(), "x");
644        assert_eq!(boundary5.to_string(), "2 * x + 5")
645    }
646
647    #[test]
648    fn test_new_methods() {
649        let ifty = IntervalBoundary::new_infty();
650        assert_eq!(ifty, IntervalBoundary::Infty);
651
652        let b = IntervalBoundary::new_bound(WeightedSum::new_empty(), 1);
653        assert_eq!(
654            b,
655            IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1,))
656        );
657
658        let c_i = Interval::new_constant(0, 1);
659        assert_eq!(
660            c_i,
661            Interval {
662                lb: IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 0)),
663                lb_open: false,
664                ub: IntervalBoundary::Bound(Threshold::new(WeightedSum::new_empty(), 1,)),
665                ub_open: true
666            }
667        );
668    }
669
670    #[test]
671    fn test_encode_interval_as_boolean_expr() {
672        let interval = Interval::new_constant(0, 1);
673        let var = Variable::new("x");
674        let expr = interval.encode_into_boolean_expr(&var);
675
676        let expected = BooleanExpression::ComparisonExpression(
677            Box::new(IntegerExpression::Atom(var.clone())),
678            ComparisonOp::Geq,
679            Box::new(IntegerExpression::Const(0)),
680        ) & BooleanExpression::ComparisonExpression(
681            Box::new(IntegerExpression::Atom(var.clone())),
682            ComparisonOp::Lt,
683            Box::new(IntegerExpression::Const(1)),
684        );
685        assert_eq!(expr, expected);
686
687        let interval = Interval::new(
688            IntervalBoundary::from_const(0),
689            false,
690            IntervalBoundary::new_infty(),
691            true,
692        );
693        let var = Variable::new("x");
694        let expr = interval.encode_into_boolean_expr(&var);
695
696        let expected = BooleanExpression::ComparisonExpression(
697            Box::new(IntegerExpression::Atom(var.clone())),
698            ComparisonOp::Geq,
699            Box::new(IntegerExpression::Const(0)),
700        ) & BooleanExpression::True;
701        assert_eq!(expr, expected);
702
703        let interval = Interval::new(
704            IntervalBoundary::from_const(0),
705            true,
706            IntervalBoundary::from_const(1),
707            false,
708        );
709        let var = Variable::new("x");
710        let expr = interval.encode_into_boolean_expr(&var);
711
712        let expected = BooleanExpression::ComparisonExpression(
713            Box::new(IntegerExpression::Atom(var.clone())),
714            ComparisonOp::Gt,
715            Box::new(IntegerExpression::Const(0)),
716        ) & BooleanExpression::ComparisonExpression(
717            Box::new(IntegerExpression::Atom(var.clone())),
718            ComparisonOp::Leq,
719            Box::new(IntegerExpression::Const(1)),
720        );
721        assert_eq!(expr, expected);
722    }
723
724    #[test]
725    fn test_is_contained() {
726        let interval = Interval::new_constant(0, 1);
727        assert!(interval.check_is_contained(&IntervalBoundary::from_const(0)));
728        assert!(!interval.check_is_contained(&IntervalBoundary::from_const(1)));
729        assert!(!interval.check_is_contained(&IntervalBoundary::from_const(2)));
730
731        let interval = Interval::new(
732            IntervalBoundary::new_bound(
733                WeightedSum::new([
734                    (Parameter::new("F"), -Fraction::from(4)),
735                    (Parameter::new("N"), 2.into()),
736                    (Parameter::new("T"), 6.into()),
737                ]),
738                2,
739            ),
740            false,
741            IntervalBoundary::new_infty(),
742            true,
743        );
744
745        let ib = IntervalBoundary::new_bound(
746            WeightedSum::new([
747                (Parameter::new("F"), -Fraction::from(4)),
748                (Parameter::new("N"), Fraction::from(2)),
749                (Parameter::new("T"), Fraction::from(6)),
750            ]),
751            2,
752        );
753
754        assert!(interval.check_is_contained(&ib));
755    }
756}
taco_interval_ta/interval.rs

taco_interval_ta/
interval.rs
