/* Remove divs that are not strictly needed.
* In particular, if a div only occurs positively (or negatively)
* in constraints, then it can simply be dropped.
- * Also, if a div occurs only occurs in two constraints and if moreover
+ * Also, if a div occurs in only two constraints and if moreover
* those two constraints are opposite to each other, except for the constant
* term and if the sum of the constant terms is such that for any value
* of the other values, there is always at least one integer value of the
* the (absolute value) of the coefficent of the div in the constraints,
* then we can also simply drop the div.
*
+ * We skip divs that appear in equalities or in the definition of other divs.
+ * Divs that appear in the definition of other divs usually occur in at least
+ * 4 constraints, but the constraints may have been simplified.
+ *
* If any divs are left after these simple checks then we move on
* to more complicated cases in drop_more_redundant_divs.
*/
int defined;
defined = !isl_int_is_zero(bmap->div[i][0]);
+ for (j = i; j < bmap->n_div; ++j)
+ if (!isl_int_is_zero(bmap->div[j][1 + 1 + off + i]))
+ break;
+ if (j < bmap->n_div)
+ continue;
for (j = 0; j < bmap->n_eq; ++j)
if (!isl_int_is_zero(bmap->eq[j][1 + off + i]))
break;
"{ [i0, i1] : exists (e0 = [(i0 - i1)/16], e1: "
"16e0 <= i0 - i1 and 16e0 >= -15 + i0 - i1 and "
"16e1 <= i1 and 16e0 >= -i1 and 16e1 >= -i0 + i1) }", 1 },
+ { "{ [65] }",
+ "{ [i] : exists (e0 = [(255i)/256], e1 = [(127i + 65e0)/191], "
+ "e2 = [(3i + 61e1)/65], e3 = [(52i + 12e2)/61], "
+ "e4 = [(2i + e3)/3], e5 = [(4i + e3)/4], e6 = [(8i + e3)/12]: "
+ "3e4 = 2i + e3 and 4e5 = 4i + e3 and 12e6 = 8i + e3 and "
+ "i <= 255 and 64e3 >= -45 + 67i and i >= 0 and "
+ "256e0 <= 255i and 256e0 >= -255 + 255i and "
+ "191e1 <= 127i + 65e0 and 191e1 >= -190 + 127i + 65e0 and "
+ "65e2 <= 3i + 61e1 and 65e2 >= -64 + 3i + 61e1 and "
+ "61e3 <= 52i + 12e2 and 61e3 >= -60 + 52i + 12e2) }", 1 },
};
static int test_subset(isl_ctx *ctx)