isl_basic_map_drop_redundant_divs: fix div with single constant lower bound
commit5beaa108229bf2a5b247ce3549e72c6328514a7a
authorSven Verdoolaege <skimo@kotnet.org>
Sun, 7 Feb 2016 11:09:41 +0000 (7 12:09 +0100)
committerSven Verdoolaege <skimo@kotnet.org>
Wed, 10 Feb 2016 08:23:12 +0000 (10 09:23 +0100)
tree96733bf2c6dc5b98563f9633fb0d730427c5a723
parenta7d565c5da81a32ede49235e5624763a88b475d9
isl_basic_map_drop_redundant_divs: fix div with single constant lower bound

If an existentially quantified variable has a single lower bound that
does not involve any other existentially quantified variables and that
can be determined to have a constant value, then the variable can be
safely assigned this value, essentially eliminating the existentially
quantified variable.

In particular, if the single lower bound constraint is of the form

    f(x) + n d + c >= 0

then the lower bound ceil((-f(x) - c)/n) is a valid value for
the variable whenever there is any valid value.
If, moreover, there are two constraints

    f(x) + c0 >= 0
    -f(x) + c1 >= 0

such that ceil((-c1 - c)/n) = ceil((c0 - c)/n), then
ceil((-f(x) - c)/n) has a fixed value and the existentially
quantified variable can be assigned this value.

In the omega/m11-0.in test case, the additional lower bound is derived
from the set

    [m] -> { [i0, i1] : exists (e0: i1 > 0 and 2e0 > -i1 and i1 <= 2 and
2e0 <= 6 - i1 and 20e0 <= 26 + 2m - 17i0 - 10i1 and
i0 > 0 and i0 <= 4) }

Before this commit, the existentially quantified would end up
getting rationally eliminated, resulting in the set

    [m] -> { [i0, i1] : 0 < i0 <= 4 and 17i0 <= 16 + 2m and 0 < i1 <= 2 }

After this commit, however, e0 gets assigned its lower bound
ceil((-i1 + 1)/2) = 0, resulting in the set

    [m] -> { [i0, i1] : 0 < i0 <= 4 and 0 < i1 <= 2 and 10i1 <= 26 + 2m - 17i0 }

Signed-off-by: Sven Verdoolaege <skimo@kotnet.org>
isl_map_simplify.c
test_inputs/codegen/omega/m11-0.c