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

taco_interval_ta/
interval.rs
