INTERVAL

Construct an interval specified by a minimum (u) and a maximum (v) integer value. Values u and v are considered to be included in the interval.

IntervalCopy

Return a copy of the given input interval.

IntervalEmpty

Return an empty interval; interval [1,0] is produced.

IntervalUniverse

Returns the entire interval for a given arithmetic representation type (ztyp) and for the specified bitwidth (bw).

IntervalClamp

Return a saturated version of the given interval for the specified lower (lo) and higher (hi) bounds.

IntervalAdd

Return the interval of the result of adding the intervals of two integers.

IntervalSub

Return the interval of the result of performing subtraction on two integer intervals.

IntervalNeg

Return a negated interval by negating the supremum and infimum fields.

IntervalMul

Return the interval of the result of performing multiplication on two integer intervals. The result is not truncated. xtyp, ytyp provide the arithmetic representation type for x and y, respectively.

IntervalDiv

Return the interval of the result of performing division (quotient only) between two integer intervals. xtyp, ytyp provide the arithmetic representation type for x and y, respectively.

IntervalMod

Return the interval of the result of performing the modulus on two integer intervals. xtyp provides the arithmetic representation type for x.

IntervalMux

Return the interval of the result of z = ((a) relop (b) ? (x) : (y)), where relop is a relational operator:

• "==" (muxeq),
• "!=" (muxne),
• "<" (muxlt),
• "<=" (muxle),
• ">" (muxgt),
• ">=" (muxge)

IntervalSet

Return the interval of the result of z = x relop y, where relop is a relational operator:

• "==" (seteq),
• "!=" (setne),
• "<" (setlt),
• "<=" (setle),
• ">" (setgt),
• ">=" (setge)

IntervalAnd

Return the interval of the result of z = x AND y.

IntervalIor

Return the interval of the result of z = x IOR y.

IntervalXor

Return the interval of the result of z = x XOR y.

IntervalNot

Return the interval of the result of z = NOT x.

IntervalExpInteger

Return the interval of the result of z = x ** n (n-th integer power of x). n is an integer and its interval representation is [n,n].

IntervalSqrt

Return the interval of the result of z = sqrt(x).

IntervalAbs

Return the interval of the result of computing the absolute value of interval x: z = abs(x).

IntervalMax

Return the interval of the result of computing the maximum value of intervals x and y: z = max(x, y).

IntervalMin

Return the interval of the result of computing the minimum value of intervals x and y: z = min(x, y).

IntervalUnion

Return the union (actually the so-called "interval hull" which produces a contiguous interval) of intervals x and y. The union operator formally produces two distinct intervals.

IntervalIntersection

Return the intersection of intervals x and y. In case the intersection of x and y is the empty interval, the [1,0] interval (the default empty interval) is returned.

ValueIsInInterval

Query whether the given value v is in interval x or not. Returns 1 if v is in x; 0 otherwise.

IntervalIsEmpty

Query whether the given interval is an empty set (i.e. containing no values). Returns 1 if the interval x is empty; 0 otherwise.

IntervalIsPositive

Query whether the given interval is strictly positive (i.e. lies in the domain of positive integers). The interval may contain integer ZERO. Returns 1 if the interval x is positive; 0 otherwise.

IntervalIsNegative

Query whether the given interval is strictly negative (i.e. lies in the domain of negative integers). The interval may contain integer ZERO. Returns 1 if the interval x is negative; 0 otherwise.

ValueToInterval

Convert a given integer value v to a degenerate interval of the form [v,v]. Returns the computed interval.

IntervalBalanced

Given an "unbalanced" interval (of the form [m,n], where m!=n and m,n>0 or m<0<=n and |m|=n+1), it is converted to a "balanced" interval of the form [0,2^n-1] for unsigned or [-2^(n-1),2^(n-1)+1] for signed integer arithmetic. xtyp provides the arithmetic type for the assumed integer arithmetic.

IntervalIsBalanced

Query whether the given interval is balanced, i.e. [0,2^n-1] for unsigned or [-2^(n-1),2^(n-1)+1] for signed integer arithmetic. Returns 1 if the interval x is balanced; 0 otherwise.

IntervalIsSymmetric

Query whether the given interval is symmetric, i.e. [-n,n] for any given arithmetic (even a non fixed-point one). Returns 1 if the interval x is symmetric; 0 otherwise.

NOTE: For non-exact arithmetic representations, the comparison operation should be carefully designed.

IntegerBitwidthToInterval

Convert the bitwidth of a signed (2's complement) or unsigned integer number to the corresponding interval. A bitwidth of n-bits would be converted to [0,2**n-1] for an unsigned integer or [-2**(n-1),2**(n-1)-1] for a signed integer. xtyp provides the arithmetic type for the assumed integer.

IntervalToIntegerBitwidth

Convert the given interval to the corresponding minimum bitwidth necessary for the representation of signed (2's complement) or unsigned integers. xtyp provides the arithmetic type for the assumed integer representation.

IntervalPrint

Print the specified interval to outfile.