isl_basic_map_drop_redundant_divs: handle more cases
commit164f3c956e9b3e3e25e545ebbb4dbe90d0eb1a80
authorSven Verdoolaege <skimo@kotnet.org>
Sun, 22 May 2016 16:08:10 +0000 (22 18:08 +0200)
committerSven Verdoolaege <skimo@kotnet.org>
Wed, 25 May 2016 16:56:07 +0000 (25 18:56 +0200)
treec2df9584a3bd09a90207ef1b4a2cbc7219029b6f
parentfb3c30e0133c37a1e7bccbf1b29d91b2bc2f2887
isl_basic_map_drop_redundant_divs: handle more cases

In particular, when looking for redundant existentially quantified variables
by checking that each pair of lower and upper bounds admits an intermediate
integer value, scale down the test inequality if its coefficients have
a common divisor.  This can eliminate some negative rational values
for the test inequality.

For example, for the new test case
{ [m, w] : exists a : w - 2m - 5 <= 3a <= m - 2w }
the originally constructed constraint is -3w + 3m + 3 >= 0,
which can attain the negative integer value -2 (on rational values
-10/3 and -5/3 of w and m), while the scaled down constraint is
-w + m + 1 >= 0, which does not admit any negative (integer) values.

Note that the Omega test can also detect that this existentially
quantified variable can be eliminated, without explicitly evaluating
the test inequality.  This will be addressed in the next commit.

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