Go to the previous, next section.

Linear Inequality Math

i = ~A
Check if there does not exist an integer solution to the given system of inequalities. i is set to TRUE if NO SOLUTION and returns FALSE if a solution exists to the system of inequalities.

i = (A == B)
i is set to TRUE if both systems of inequalities represent the same set of integer points.

i = (A >> B)
This is the subset or "is contained?" operator. It checks if all the integer points given by the set of inequalities of B are also included in the polyhedron defined by the system of inequalities A.

i = col_lcm(j);
Find the least common multiplier of all the numbers in the j-th column.

i = col_gcd(j);
Find the greatest common divider of all the numbers in the j-th column.

normalize();
Normalize the inequalities by dividing each inequality by the gcd. In normalize(TRUE) the constant term of each inequality is adjusted to make the bounds tight without changing the integer solution.

del_zeros();
Remove the rows that have all zero values. If the coefficient values and the constant of a constraint are all zeros, it represents 0 >= 0, thus void of any information.

del_unused_var();
Each column (other than the first) represents coefficients of a variable. If no non-zero coefficient exists for a variable (the column is all zeros) remove that variable from the system. Since no inequality uses this variable, getting rid of that variable does not change the problem.

del_repetition();
If the same inequality is repeated multiple times, get rid of all the copies but one.

del_loose();
If two inequalities have similar coefficients but have different constant terms, eliminate the slacker inequality.

min_constant();
...

max_rank();
Position of the rightmost column that has a non-zero element.

A = B.filter(a, i, j);
A = B.filter_thru(a, i);
A = B.filter_away(a, i);
`Filter' functions are used to filter a subset of inequalities from a given set of inequalities. The filter kernel a has an entry for each column of B. If a[x] is 0 the column x does not affect the results while a 1 makes that column active. The variable i is the sign of the participating coefficients. If i is 0, all active columns with non-zero coefficients participate; if i is 1, only the active columns with positive coefficients participate; i is -1, only the active columns with negative coefficient participate. Finally the variable j in the function filter determines the filter operation. If j is 1 the operation is filter_thru and when j is -1 the operation is filter_away.
Let's look at an example loop nest.
for i1 = 0 to N do       
    for i2 = 0 to MIN(i1, N) do       
        for i3 = 1 to MIN(i2, N-1) do       
            for i4 = 0 to 100 do       
                ...

The set of inequalities representing this loop nest is:

//              N  i1  i2  i3  i4
        [   0   0   1   0   0   0 ]
        [   0   1  -1   0   0   0 ]
        [   0   0   0   1   0   0 ]
    A = [   0   0   1  -1   0   0 ]
        [   0   1   0  -1   0   0 ]
        [  -1   0   0   0   1   0 ]
        [   0   0   0   1  -1   0 ]
        [   1   1   0   0  -1   0 ]
        [   0   0   0   0   0   1 ]
        [ 100   0   0   0   0  -1 ]

Let's see how to extract the lower and upper bounds of the loop i2 from the system of inequalities A.

constraint c(6);

// First remove all the inequalities representing 
// the bounds of inner loops (i3 and i4). This step
// will remove the 7th inequality where i2 is in
// the bounds of i3.
c = 0;
c[4] = 1
c[5] = 1
//   c =[   0   0   0   0   1   1 ]

B = A.filter_away(c, 0);
//      [   0   0   1   0   0   0 ]
//      [   0   1  -1   0   0   0 ]
//  B = [   0   0   0   1   0   0 ]
//      [   0   0   1  -1   0   0 ]
//      [   0   1   0  -1   0   0 ]

// Now get the inequalities that represent the bounds 
// of i2. After the previous step, all the inequalities 
// with a non-zero coefficient for i2 represents a 
// bound for the i2 loop.
c = 0;
c[3] = 1
//  c = [   0   0   0   1   0   0 ]

LB = B.filter_thru(c,  1);
// The lower bound of the loop i2 is:
// LB = [   0   0   0   1   0   0 ]

UB = B.filter_thru(c, -1);
// The upper bound of the loop i2 is:
// UB = [   0   0   1  -1   0   0 ]
//      [   0   1   0  -1   0   0 ]

Go to the previous, next section.