isl_map_coalesce: avoid ignoring constraints redundant wrt implicit equalitiesmaint
commit11c6e46cb2936b265362527f45f00a9cace4c790
authorSven Verdoolaege <sven@cerebras.net>
Tue, 11 Apr 2023 14:09:57 +0000 (11 16:09 +0200)
committerSven Verdoolaege <sven@cerebras.net>
Fri, 14 Apr 2023 20:10:37 +0000 (14 22:10 +0200)
treececa18bde6bb58cd9ed3e269de09214477c06356
parent5841bfaf35df1da19d19d73c09bbbae3919b7d2f
isl_map_coalesce: avoid ignoring constraints redundant wrt implicit equalities

Commit isl-0.18-26-g8ffc8160df (isl_map_coalesce: detect constants among
expanded divs, Tue Jun 21 13:00:06 2016 +0200) introduced a mechanism
for detecting integer divisions of one disjunct that have a constant value
in the other disjunct.
This constant value is then encoded in the tableau of the other disjunct
by introducing two inequality constraints and selecting
the facet corresponding to one of those two constraints.

However, the (implicit) equality constraint may render
some other constraints in the second disjunct redundant.
These redundant constraints therefore get completely ignored,
while only one side of the implicit equality constraint itself
is taken into account during some parts of the coalescing.
In particular, when wrapping constraints, only the inequality constraint
forming the facet is considered for potential wrapping and
not the implicit opposite inequality constraint.
Since neither this opposite constraint nor the original constraints
that are redundant with respect to this constraint are considered
for wrapping, the final result may be missing some constraints.

This happens in particular with the 701 variant of the new test case, i.e.,
{ [a] : 0 < a <= 341 or (0 < a <= 701 and 360*floor(a/360) >= -340 + a) }.
The integer division floor(a/360) of the second disjunct has
fixed value 0 in the first disjunct, with the constraint floor(a/360) >= 0
turned into an implicit equality.
The constraint 360*floor(a/360) >= -340 + a is a cut constraint
for the first disjunct.  Since the first disjunct sticks out by one,
the constraint is relaxed and an attempt is made to wrap the constraints
of the intersection of the relaxed constraint with the first disjunct
around the second disjunct.
This intersection is
{ [a, y = floor(a/360)] : 0 < a <= 341 and 0 <= y <= 0 and
                          360*y = -341 + a }
i.e., { [341, 0] }
Given 360*y = -341 + a and the implicit equality y = 0,
both a <= 341 and y <= 0 are redundant in this intersection,
so neither is getting wrapped around the second disjunct.
The extension appears successful and the result consists of only
the valid constraints in both disjuncts, i.e., { [a] : 0 < a <= 701 }.
This is not equal to the input set since it has an extra element { [701] }.

It would be possible to explicitly consider the opposites
of implicit equality constraints, but it is safer
to make the implicit equality constraints explicit, similarly
to what was done in isl-0.11.1-19-g9ce5772769 (isl_map_coalesce:
avoid dropping constraints redundant wrt implicit equalities,
Sat Mar 16 14:40:56 2013 +0100).

Since both sides of an equality constraint are already considered
for wrapping, the constraint floor(a/360) <= 0 is now considered
for wrapping in the example.  The wrapping succeeds, but is rejected
by default because the coefficients in the result are too large.
Note that the two variants of the added test cases are equal to each other
since 701 - 340 = 361 > 360*floor(701/360).
The coalesced result of the 700 variant of the test could therefore
in theory also be used for the 701 variant, but there is currently
no mechanism for detecting this.

Note that this fix may also prevent some coalescings
that just happened to produce a correct result.

Signed-off-by: Sven Verdoolaege <sven@cerebras.net>
isl_coalesce.c
isl_test.c