Module loop_ranges

Loop ranges in regular expressions.

SMT-LIB has a loop construct for regular expressions: Given a language L, (loop i j L) means repetition of L for some number between i and j. So we have:

(loop i j L) = union for k=i to j of L^k (provided i<=j).

We generalize this construct by allowing j to be +infinity. Then we use loop to reduce the number of regular expression primitives that we need:

1. L? is (loop 0 1 L)
2. L⁺ is (loop 1 +infinity L)
3. L^* is (loop 0 +infinity L)
4. L^k is (loop k k L)

This module implements operations on loop ranges. Each range is a pair (i, j) where 0 <= i <= j and j may be infinite.

We limit i and j to u32. The code will panic in case of arithmetic overflow.

Structs

LoopRange

Loop range