isl_ast_build_expr.c: extract_modulo: consider simple sums of constraints
Modulo expressions are detected by looking at expressions
of the form
f * m * floor(a / m)
and checking that some variation of a is non-negative.
In particular, a and -a + m - 1 are tested for being non-negative,
but first the constraints are scanned for constraints that are
equal or opposite to a mod m up to a constant.
Also check if a happens to be equal (up to a constant)
to a positively weighted sum of constraints with disjoint sets of variables.
Since each constraint in non-negative, a positive combination
is non-negative as well.
Note that sum is required to be equal to a itself and not just a mod m
to make it easier to find the coefficients with which each constraint
should be multiplied.
The extra check allows for some extra cases to be discovered
on some inputs because the basic check only checks whether a itself
is non-negative, while the sum of constraints may have a different
constant term.
On other inputs, the extra check simply results in a different
modulo expression being detected.
Signed-off-by: Sven Verdoolaege <sven@cerebras.net>