isl_basic_map_remove_redundancies: sort constraints

isl_basic_map_remove_redundancies: sort constraints

Since 738e40b (isl_map_*_simple_hull: sort constraints before dropping
redundant constraints, Thu Mar 31 17:50:00 2016 +0200), the constraints
are already sorted when isl_basic_map_remove_redundancies is called
from within isl_map_*_simple_hull, but the sorting should be more
generally useful.  In particular, constraints that involve later variables
should be considered for removal before those that only contain earlier
variables.

This change has an effect on some AST generation outputs.
For example, the effect on unroll6 is as follows:

-  if (nn >= 128 * g + 6 && nn >= ((t1 + 127) % 128) + 128 * g + 3 && ((t1 + 127) % 128) + 128 * g >= 0)
+  if (g >= 0 && nn >= 128 * g + 6 && nn >= ((t1 + 127) % 128) + 128 * g + 3)

This is the desired result.  A constraint involving integer divisions
is removed in favor of a constraint that does not.

In the case of hoist2, the effect is less favorable.
This effect can be explained as follows.
Before this commit, the guard in add_domain looks like

[t1, b] -> { [i0, i1] : exists (e0 = floor((1 + i0)/2), e1 = floor((-t1 + i1)/64), e2: 64e1 = -t1 + i1 and i1 >= 9 - 64b and 2e2 <= 70 - i1 and 2e2 >= -3 + i0 and b <= 1 and t1 >= 5 and i0 > 0 and t1 <= 8 and 2e2 >= 7 - i1 and e2 <= 1 and e2 >= 0 and b >= 0 and i0 <= 5 and i1 >= 5 and i1 <= 70 and i1 <= 73 - i0 and 2e0 <= 1 + i0 and 2e0 >= -72 + 2i0 + i1 and 2e0 >= i0) }

while after the commit, it looks like

[t1, b] -> { [i0, i1] : exists (e0 = floor((71 - t1)/64), e1 = floor((-t1 + i1)/64), e2: 64e1 = -t1 + i1 and t1 >= 5 and t1 <= 8 and 2e2 >= 7 - i1 and b <= 1 and i0 > 0 and 2e2 >= -3 + i0 and i1 >= 9 - 64b and 2e2 <= 70 - i1 and e2 >= 0 and e2 <= 1 and b >= 0 and i0 <= 5 and i1 <= 73 - i0 and i1 >= 5 and i1 <= 70 and 64e0 <= 71 - t1 and 64e0 >= 9 - t1 - 64b and 64e0 >= 8 - t1) }

The main difference is that e0 is now defined in terms of t1 instead of i0,
which makes sense in light of the preference of removing redundant constraints
that involve later variables.
However, dropping all constraints involving the existentially quantified
variable e2 used to result in

[t1, b] -> { [i0, i1] : exists (e0 = floor((1 + i0)/2), e1 = floor((-t1 + i1)/64): 64e1 = -t1 + i1 and i1 >= 9 - 64b and b <= 1 and t1 >= 5 and i0 > 0 and t1 <= 8 and b >= 0 and i0 <= 5 and i1 >= 5 and i1 <= 70 and i1 <= 73 - i0 and 2e0 <= 1 + i0 and 2e0 >= -72 + 2i0 + i1 and 2e0 >= i0) }

and this set is identical to the set with the extra constraints.
isl_set_compute_divs is therefore able to recover this set.

Dropping the constraints involving e2 in the second representation results in

[t1, b] -> { [i0, i1] : exists (e0 = floor((71 - t1)/64), e1 = floor((-t1 + i1)/64): 64e1 = -t1 + i1 and t1 >= 5 and t1 <= 8 and b <= 1 and i0 > 0 and i1 >= 9 - 64b and b >= 0 and i0 <= 5 and i1 <= 73 - i0 and i1 >= 5 and i1 <= 70 and 64e0 <= 71 - t1 and 64e0 >= 9 - t1 - 64b and 64e0 >= 8 - t1) }

which is not the same set.  It is therefore not surprising that
isl_set_compute_divs may need to subdivide the domain.

Since the original result appears to be based on pure luck, the regression
on this test case does not look like a sufficient reason to block this change
since other changes that happen to change the order of the constraints
may result in similar effects.  At least with this change, the result
will be less dependent on the history of the set.

Signed-off-by: Sven Verdoolaege <skimo@kotnet.org>