isl_map_coalesce: tighten constraints of potential extension
While checking whether basic map A is an extension of basic map B,
a constraint of B is first relaxed by one and then turned into
an equality. If the resulting facet is a subset of A, then the constraint
of B can simply be relaxed to include exactly A.
The test whether the facet next to B is a subset of A is performed
on the tableau, which does not fully exploit the fact that only the integer
points in the facet need to be a subset of A.
In particular, some of the constraints of B could possibly be tightened
on the facet.
For example, for the test case
{ [y, x] : (x - y) mod 3 = 2 and 2 <= y <= 200 and 0 <= x <= 2; [1, 0] }
the first disjunct is reformulated internally as
{ [y, x] : exists a : 3a = -2 - y + x and 4 <= x - 3a <= 202 and 0 <= x <= 2 }
The constraint 4 <= x - 3a is determined to be adjacent to
the other basic map (with a = -1).
The facet next to the first disjunct is
{ [y, x, a] : x = 3a + 3 and y = 1 and 0 <= x <= 2 }
which on the surface does not look like it is included in { [1, 0, -1] }.
However, by applying a compression of the variables, the constraint
x <= 2 can be tightened to x <= 0, i.e.,
{ [y, x, a] : x = 3a + 3 and y = 1 and x = 0 }, which is a subset
of { [1, 0, -1] }.
In general, construct a compression from the equality constraint
defining the facet that is checked for being a subset of the other
disjunct. See if any of the constraints can be tightened based
on the compression and, if so, add extra constraints to the tableau
to impose this tightening. Perform the inclusion test on
this tightened tableau.
Requested-by: Sven Wuytack <Sven.Wuytack@synopsys.com>
Signed-off-by: Sven Verdoolaege <skimo@kotnet.org>