isl_map_gist: try and exploit implicit constraints in multi-disjunct contexts
commitecafffade5c2c60f5bd13c6699b675245c2c3797
authorSven Verdoolaege <skimo@kotnet.org>
Fri, 21 Nov 2014 11:23:57 +0000 (21 12:23 +0100)
committerSven Verdoolaege <skimo@kotnet.org>
Tue, 2 Dec 2014 21:37:48 +0000 (2 22:37 +0100)
tree2b5f54ea39dcdedba5df5ae5502ae86799856c0d
parent8b2a206704a9738837e01512139853787d4bd359
isl_map_gist: try and exploit implicit constraints in multi-disjunct contexts

If the context is a multi-disjunct set, then we first compute
a single-disjunct approximation and compute the gist with respect
to this approximation.  The approximation may however drop some
constraints that are only implicitly available in the disjuncts
of the context.
Check which of the constraints in the input map are also valid
for the context so that they can be used to simplify away
those constraints of the input.

For example, the constraint a <= 2147 + n is
implied by the set

{ [m, n, a, b] : (n >= 1 and a >= 0 and b <= 2148 - n - a and b >= 0) or
  (m >= 1 and n >= 1 and a <= 2148 - m and b <= 2148 - n and b >= 0 and
   b >= 2149 - n - a) }

but it is not implied by the simple hull of this set, i.e.,

{ [m, n, a, b] : n >= 1 and a >= 0 and b <= 4295 - n - a and
 b >= 0 and b <= 2148 - n }

When also considering the constraint a <= 2147 + n while building
the simple hull, we obtain

{ [m, n, a, b] : b <= 2148 - n and b >= 0 and a >= 0 and
a <= 2147 + n and n >= 1 }

instead, which can be used to simplify away the original
"a <= 2147 + n" constraint.

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