Struct aws_smt_strings::loop_ranges::LoopRange

pub struct LoopRange(/* private fields */);

Loop range

A loop range is either a finite interval [i, j] or an infinite interval [i, ..]

• A finite interval is represented as LoopRange(i, Some(j)) where 0 <= i <= j
• An infinite interval is represented as LoopRange(i, None).

The integers i and j are stored as u32. Operations on loop ranges will panic if results cannot be stored using 32bit unsigned integers.

Implementations

impl LoopRange

pub fn finite(i: u32, j: u32) -> LoopRange

Construct the finite range [i, j]

pub fn infinite(i: u32) -> LoopRange

Construct the infinite range [i, +infinity]

pub fn opt() -> LoopRange

Construct the range [0, 1]

pub fn star() -> LoopRange

Construct the range [0, +infinity]

pub fn plus() -> LoopRange

Construct the range [1, +infinity]

pub fn point(k: u32) -> LoopRange

Construct the range [k, k]

pub fn is_finite(&self) -> bool

Check whether this range is finite

pub fn is_infinite(&self) -> bool

Check whether this range is infinite

pub fn is_point(&self) -> bool

Check whether this range is a singleton

pub fn is_zero(&self) -> bool

Check whether this range is the singleton 0

pub fn is_one(&self) -> bool

Check whether this range is the singleton 1

pub fn is_all(&self) -> bool

Check whether this range is [0, +infinity]

pub fn start(&self) -> u32

Start of the range

pub fn contains(&self, i: u32) -> bool

Check whether an index is in a loop range

pub fn includes(&self, other: &LoopRange) -> bool

Check inclusion

• return true if other is included in self.

pub fn add(&self, other: &LoopRange) -> LoopRange

Add two ranges

The result is the union of both ranges.

This is used to rewrite (concat (loop L a b) (loop L c d)) to (loop L (add [a, b], [c, d])).

Panics

If an arithmetic overflow occurs, that is, the union of the two ranges cannot be represented using 32bit unsigned integers, this method will panic.

pub fn add_point(&self, x: u32) -> LoopRange

Add a point interval

Add the point interval [x, x] to self.

Panics

If there’s an arithmetic overflow. See add.

pub fn scale(&self, k: u32) -> LoopRange

Multiply by a constant k

• If the current range is a finite interval [i, j], return [k * i, k * j]
• If the current range is an infinite interval [i, +infinity] and k is not zero, return [k * i, +infinity]
• If k is zero, return [0, 0] even if the current range is infinite

This corresponds to adding [i, j] to itself k times.

This can be used to rewrite

(loop L i j)^k = (loop L (k * i) (k * j))

Panics

If there’s an arithmetic overflow in k * i or k * j.

pub fn mul(&self, other: &LoopRange) -> LoopRange

Multiply two ranges

The product of the ranges [a, b] and [c, d] (where b or d may be +infinity) is the range [a * c, b * d]. The following rules handle multiplication with infinity:

• 0 * infinity = infinity * 0 = 0
• k * infinity = infinity * k = infinity if k is finite and non-zero
• infinity * infinity = infinity

Note:

The actual product of [a, b] and [c, d] is the set of integers P = { x * y | a <= x <= b and c <= y <= d }.

The interval [a * c, b * d] is an over approximation of P, since P may not be an interval.

For example: if [a, b] = [0, 1] and [c, d] = [3, 4] then P is { 0, 3, 4 } but [0, 1] * [3, 4] is [0, 4].

Method right_mul_is_exact can be used to check whether the product is exact.

Panics

If there’s an arithmetic overflow in the product computation, that is, the result cannot be stored using u32 integers, this method will panic.

pub fn right_mul_is_exact(&self, other: &LoopRange) -> bool

Check whether the product of two ranges is an interval.

Given a range r = [a, b] and s = [c, d], then

r.right_mul_is_exact(s)

returns true if the Union(k * [a, b]) for k in s is equal to [a, b] * [c, d].

If it is, we can rewrite (loop (loop L a b) c d) to (loop L a * c b * d).

Note:

The product of two ranges is commutative but this method is not. For example:

1. Union(k * [0, +infinity], k in [2, 2]) = 2 * [0, +infinity] = [0, +infinity] so

   (loop (loop L 0 +infinity) 2 2) = (L*)^2 = L*

2. Union(k * [2, 2], k in [0, +infinity]) = { 2 * k | k in [0, +infinity] } so

   (loop (loop L 2 2) 0 +infinity) = (L^2)* (not the same as L*)

Example

use aws_smt_strings::loop_ranges::*;

let r = LoopRange::point(2); // range [2, 2]
let s = LoopRange::star();   // range [0, +infinity]

assert!(s.right_mul_is_exact(&r));  // [0, +infinity] * [2, 2] is [0, +infinity] (exact)
assert!(!r.right_mul_is_exact(&s)); // [2, 2] * [0, +infinity] is not an interval

pub fn shift(&self) -> LoopRange

Shift by one.

If self = [a, b], return [dec(a), dec(b)] where dec(x) decrements x by 1:

• dec(0) = 0
• dec(+infinity) = +infinity
• dec(x) = x-1 otherwise

Trait Implementations

impl Clone for LoopRange

fn clone(&self) -> LoopRange

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for LoopRange

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for LoopRange

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Hash for LoopRange

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for LoopRange

fn eq(&self, other: &LoopRange) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

This method tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Copy for LoopRange

impl Eq for LoopRange

impl StructuralEq for LoopRange

impl StructuralPartialEq for LoopRange