isl_ast_expr_from_aff: try harder to use isl_ast_op_pdiv_{q,r}

When generating C code, we prefer to generate "/" (or "%") rather
than "floord" because "floord" has an implicit condition on the
sign of the first argument.
We would already generate isl_ast_op_pdiv_q instead of isl_ast_op_fdiv_q
if we detect that the first argument is non-negative.
Now, we also check if the first argument is smaller than the second.
If so, we can rewrite

	floor(e/d) = -ceil(-e/d) = -floor((-e + d - 1)/d)

and still use isl_ast_op_pdiv_q.

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

diff --git a/isl_ast_build_expr.c b/isl_ast_build_expr.c
index 51f33ce..81688de 100644 (file)
--- a/isl_ast_build_expr.c
+++ b/isl_ast_build_expr.c
@@ -36,9 +36,27 @@ enum isl_lp_result isl_ast_build_max(__isl_keep isl_ast_build *build,
        return isl_set_max(build->domain, obj, opt);
 }
 
+/* Compute the "opposite" of the (numerator of the) argument of a div
+ * with denonimator "d".
+ *
+ * In particular, compute
+ *
+ *     -aff + (d - 1)
+ */
+static __isl_give isl_aff *oppose_div_arg(__isl_take isl_aff *aff, isl_int d)
+{
+       aff = isl_aff_neg(aff);
+       aff = isl_aff_add_constant(aff, d);
+       aff = isl_aff_add_constant_si(aff, -1);
+
+       return aff;
+}
+
 /* Create an isl_ast_expr evaluating the div at position "pos" in "ls".
  * The result is simplified in terms of build->domain.
  *
+ * "v" points to the coefficient of the div in the expression where it
+ * appears and may be updated by this function.
  * "ls" is known to be non-NULL.
  *
  * Let the div be of the form floor(e/d).
@@ -51,8 +69,16 @@ enum isl_lp_result isl_ast_build_max(__isl_keep isl_ast_build *build,
  *
  *     (fdiv_q, expr(e), expr(d))
  *
+ * If the ast_build_prefer_pdiv option is set and
+ * if "e" is not non-negative, then we check if "-e + d - 1" is non-negative.
+ * If so, we can rewrite
+ *
+ *     floor(e/d) = -ceil(-e/d) = -floor((-e + d - 1)/d)
+ *
+ * and still use pdiv_q.
  */
-static __isl_give isl_ast_expr *var_div(__isl_keep isl_local_space *ls,
+static __isl_give isl_ast_expr *var_div(isl_int *v,
+       __isl_keep isl_local_space *ls,
        int pos, __isl_keep isl_ast_build *build)
 {
        isl_ctx *ctx = isl_local_space_get_ctx(ls);
@@ -66,17 +92,27 @@ static __isl_give isl_ast_expr *var_div(__isl_keep isl_local_space *ls,
        isl_aff_get_denominator(aff, &d);
        aff = isl_aff_scale(aff, d);
        den = isl_ast_expr_alloc_int(ctx, d);
-       isl_int_clear(d);
 
        type = isl_ast_op_fdiv_q;
        if (isl_options_get_ast_build_prefer_pdiv(ctx)) {
                int non_neg = isl_ast_build_aff_is_nonneg(build, aff);
+               if (non_neg >= 0 && !non_neg) {
+                       isl_aff *opp = oppose_div_arg(isl_aff_copy(aff), d);
+                       non_neg = isl_ast_build_aff_is_nonneg(build, opp);
+                       if (non_neg >= 0 && non_neg) {
+                               isl_int_neg(*v, *v);
+                               isl_aff_free(aff);
+                               aff = opp;
+                       } else
+                               isl_aff_free(opp);
+               }
                if (non_neg < 0)
                        aff = isl_aff_free(aff);
                else if (non_neg)
                        type = isl_ast_op_pdiv_q;
        }
 
+       isl_int_clear(d);
        num = isl_ast_expr_from_aff(aff, build);
        return isl_ast_expr_alloc_binary(type, num, den);
 }
@@ -84,19 +120,22 @@ static __isl_give isl_ast_expr *var_div(__isl_keep isl_local_space *ls,
 /* Create an isl_ast_expr evaluating the specified dimension of "ls".
  * The result is simplified in terms of build->domain.
  *
+ * "v" points to the coefficient of the specified dimension
+ * in the expression where it appears and may be updated by this function.
+ *
  * The isl_ast_expr is constructed based on the type of the dimension.
  * - divs are constructed by var_div
  * - set variables are constructed from the iterator isl_ids in "build"
  * - parameters are constructed from the isl_ids in "ls"
  */
-static __isl_give isl_ast_expr *var(__isl_keep isl_local_space *ls,
+static __isl_give isl_ast_expr *var(isl_int *v, __isl_keep isl_local_space *ls,
        enum isl_dim_type type, int pos, __isl_keep isl_ast_build *build)
 {
        isl_ctx *ctx = isl_local_space_get_ctx(ls);
        isl_id *id;
 
        if (type == isl_dim_div)
-               return var_div(ls, pos, build);
+               return var_div(v, ls, pos, build);
 
        if (type == isl_dim_set) {
                id = isl_ast_build_get_iterator_id(build, pos);
@@ -212,50 +251,44 @@ static __isl_give isl_ast_expr *isl_ast_expr_mod(isl_int v,
        return expr;
 }
 
-/* Create an isl_ast_expr evaluating "v" times the specified dimension of "ls".
- * The result is simplified in terms of build->domain.
+/* Create an isl_ast_expr that scales "expr" by "v".
  *
- * Let e be the expression for the specified dimension.
- * If v is 1, we simply return e.
+ * If v is 1, we simply return expr.
  * If v is -1, we return
  *
- *     (isl_ast_op_minus, e)
+ *     (isl_ast_op_minus, expr)
  *
  * Otherwise, we return
  *
- *     (isl_ast_op_mul, expr(v), e)
+ *     (isl_ast_op_mul, expr(v), expr)
  */
-static __isl_give isl_ast_expr *isl_ast_expr_term(
-       __isl_keep isl_local_space *ls, enum isl_dim_type type, int pos,
-       isl_int v, __isl_keep isl_ast_build *build)
+static __isl_give isl_ast_expr *scale(__isl_take isl_ast_expr *expr, isl_int v)
 {
        isl_ctx *ctx;
-       isl_ast_expr *expr;
        isl_ast_expr *c;
 
-       if (!ls)
+       if (!expr)
                return NULL;
+       if (isl_int_is_one(v))
+               return expr;
 
-       ctx = isl_local_space_get_ctx(ls);
-       expr = var(ls, type, pos, build);
-
-       if (!isl_int_is_one(v)) {
-               if (isl_int_is_negone(v)) {
-                       expr = isl_ast_expr_neg(expr);
-               } else {
-                       c = isl_ast_expr_alloc_int(ctx, v);
-                       expr = isl_ast_expr_mul(c, expr);
-               }
+       if (isl_int_is_negone(v)) {
+               expr = isl_ast_expr_neg(expr);
+       } else {
+               ctx = isl_ast_expr_get_ctx(expr);
+               c = isl_ast_expr_alloc_int(ctx, v);
+               expr = isl_ast_expr_mul(c, expr);
        }
 
        return expr;
 }
 
-/* Add an expression for "v" times the specified dimension of "ls"
+/* Add an expression for "*v" times the specified dimension of "ls"
  * to expr.
  *
- * Let e be the expression for the specified dimension.
- * If "v" is negative, we create
+ * Let e be the expression for the specified dimension,
+ * multiplied by the absolute value of "*v".
+ * If "*v" is negative, we create
  *
  *     (isl_ast_op_sub, expr, e)
  *
@@ -265,7 +298,7 @@ static __isl_give isl_ast_expr *isl_ast_expr_term(
  *
  * instead.
  *
- * If "v" is positive, we simply create
+ * If "*v" is positive, we simply create
  *
  *     (isl_ast_op_add, expr, e)
  *
@@ -273,19 +306,21 @@ static __isl_give isl_ast_expr *isl_ast_expr_term(
 static __isl_give isl_ast_expr *isl_ast_expr_add_term(
        __isl_take isl_ast_expr *expr,
        __isl_keep isl_local_space *ls, enum isl_dim_type type, int pos,
-       isl_int v, __isl_keep isl_ast_build *build)
+       isl_int *v, __isl_keep isl_ast_build *build)
 {
        isl_ast_expr *term;
 
        if (!expr)
                return NULL;
 
-       if (isl_int_is_neg(v) && !ast_expr_is_zero(expr)) {
-               isl_int_neg(v, v);
-               term = isl_ast_expr_term(ls, type, pos, v, build);
+       term = var(v, ls, type, pos, build);
+
+       if (isl_int_is_neg(*v) && !ast_expr_is_zero(expr)) {
+               isl_int_neg(*v, *v);
+               term = scale(term, *v);
                return ast_expr_sub(expr, term);
        } else {
-               term = isl_ast_expr_term(ls, type, pos, v, build);
+               term = scale(term, *v);
                return ast_expr_add(expr, term);
        }
 }
@@ -338,6 +373,12 @@ static __isl_give isl_ast_expr *isl_ast_expr_add_int(
  *     (isl_ast_op_pdiv_r, a, m)
  *
  * we need to make sure that a is non-negative.
+ * If not, we check if "-a + m - 1" is non-negative.
+ * If so, we can rewrite
+ *
+ *     floor(a/m) = -ceil(-a/m) = -floor((-a + m - 1)/m)
+ *
+ * and still extract a modulo.
  *
  * The caller is responsible for dividing *neg and/or *pos by d.
  */
@@ -355,8 +396,20 @@ static __isl_give isl_aff *extract_modulo(__isl_take isl_aff *aff,
        div = isl_aff_get_div(aff, j);
        isl_aff_get_denominator(div, &d);
        mod = isl_int_is_divisible_by(v, d);
-       if (mod)
+       if (mod) {
+               div = isl_aff_scale(div, d);
                mod = isl_ast_build_aff_is_nonneg(build, div);
+               if (mod >= 0 && !mod) {
+                       isl_aff *opp = oppose_div_arg(isl_aff_copy(div), d);
+                       mod = isl_ast_build_aff_is_nonneg(build, opp);
+                       if (mod >= 0 && mod) {
+                               isl_aff_free(div);
+                               div = opp;
+                               isl_int_neg(v, v);
+                       } else
+                               isl_aff_free(opp);
+               }
+       }
        if (mod < 0) {
                isl_aff_free(div);
                isl_int_clear(d);
@@ -366,7 +419,6 @@ static __isl_give isl_aff *extract_modulo(__isl_take isl_aff *aff,
                isl_int_clear(d);
                return aff;
        }
-       div = isl_aff_scale(div, d);
        isl_int_divexact(v, v, d);
        s = isl_int_sgn(v);
        isl_int_abs(v, v);
@@ -482,7 +534,7 @@ __isl_give isl_ast_expr *isl_ast_expr_from_aff(__isl_take isl_aff *aff,
                        if (isl_int_is_zero(v))
                                continue;
                        expr = isl_ast_expr_add_term(expr,
-                                                       ls, l[i], j, v, build);
+                                                       ls, l[i], j, &v, build);
                }
        }
 
@@ -526,7 +578,7 @@ static __isl_give isl_ast_expr *add_signed_terms(__isl_take isl_ast_expr *expr,
                                continue;
                        isl_int_abs(v, v);
                        expr = isl_ast_expr_add_term(expr,
-                                               ls, l[i], j, v, build);
+                                               ls, l[i], j, &v, build);
                }
        }
 

diff --git a/test_inputs/codegen/cloog/jacobi-shared.c b/test_inputs/codegen/cloog/jacobi-shared.c
index fda697d..6314bc3 100644 (file)
--- a/test_inputs/codegen/cloog/jacobi-shared.c
+++ b/test_inputs/codegen/cloog/jacobi-shared.c
@@ -1,3 +1,3 @@
-if (2 * floord(h0 - 1, 2) + 1 == h0 && t1 >= 32 * floord(-g2 + t1 - 1, 32) + 3 && N + 32 * floord(-g2 + t1 - 1, 32) >= t1 + 1)
-  for (int c0 = max(t0 - 16 * floord(t0 - 1, 16), t0 - 16 * floord(g1 + t0 - 3, 16)); c0 <= min(32, N - g1 - 1); c0 += 16)
-    S1(g1 + c0 - 1, g2 + t1 + 32 * floord(-t1, 32) + 31);
+if (2 * floord(h0 - 1, 2) + 1 == h0 && g2 + 29 >= (g2 - t1 + 32) % 32 && ((g2 - t1 + 32) % 32) + N >= g2 + 33)
+  for (int c0 = max(-((-t0 + 16) % 16) + 16, t0 - 16 * floord(g1 + t0 - 3, 16)); c0 <= min(32, N - g1 - 1); c0 += 16)
+    S1(g1 + c0 - 1, ((t1 + 31) % 32) + g2);

diff --git a/test_inputs/codegen/cloog/nul_complex1.c b/test_inputs/codegen/cloog/nul_complex1.c
index cdf5425..750e331 100644 (file)
--- a/test_inputs/codegen/cloog/nul_complex1.c
+++ b/test_inputs/codegen/cloog/nul_complex1.c
@@ -1,3 +1,3 @@
 for (int c0 = 0; c0 <= 5 * n; c0 += 1)
-  for (int c1 = max(((n + c0) % 2) - n + c0, ((c0 + c0 / 3) % 2) + c0 - c0 / 3); c1 <= min(n + c0 + floord(-n - c0, 3), c0); c1 += 2)
+  for (int c1 = max(((n + c0) % 2) - n + c0, ((c0 + c0 / 3) % 2) + c0 - c0 / 3); c1 <= min(n + c0 - (n + c0 + 2) / 3, c0); c1 += 2)
     S1((-2 * c0 + 3 * c1) / 2, c0 - c1);

diff --git a/test_inputs/codegen/cloog/reservoir-cholesky2.c b/test_inputs/codegen/cloog/reservoir-cholesky2.c
index c4d9185..d497524 100644 (file)
--- a/test_inputs/codegen/cloog/reservoir-cholesky2.c
+++ b/test_inputs/codegen/cloog/reservoir-cholesky2.c
@@ -1,10 +1,10 @@
 for (int c1 = 2; c1 <= 3 * M - 1; c1 += 1) {
   if ((c1 - 2) % 3 == 0)
     S1((c1 + 1) / 3);
-  for (int c3 = -floord(-c1 + 1, 3) + 1; c3 <= min(c1 - 2, M); c3 += 1)
+  for (int c3 = (c1 + 1) / 3 + 1; c3 <= min(c1 - 2, M); c3 += 1)
     for (int c5 = c1 - (c1 + c3) / 2 + 1; c5 <= min(c1 - c3, c3); c5 += 1)
       S3(c1 - c3 - c5 + 1, c3, c5);
-  if (c1 + 1 >= 3 * ((c1 + floord(-c1 - 1, 3) + 1) / 2) && 3 * ((c1 + floord(-c1 - 1, 3) + 1) / 2) + 1 >= c1)
-    for (int c3 = ((c1 + floord(-c1 - 1, 3) + 1) % 2) - floord(-c1 - 1, 3) + 1; c3 <= min(c1, M); c3 += 2)
+  if (c1 + 1 >= 3 * ((c1 - (c1 + 3) / 3 + 1) / 2) && 3 * ((c1 - (c1 + 3) / 3 + 1) / 2) + 1 >= c1)
+    for (int c3 = ((c1 - (c1 + 3) / 3 + 1) % 2) + (c1 + 3) / 3 + 1; c3 <= min(c1, M); c3 += 2)
       S2((c1 - c3 + 2) / 2, c3);
 }

diff --git a/test_inputs/codegen/cloog/reservoir-lim-lam3.c b/test_inputs/codegen/cloog/reservoir-lim-lam3.c
index 1d6f994..14475f8 100644 (file)
--- a/test_inputs/codegen/cloog/reservoir-lim-lam3.c
+++ b/test_inputs/codegen/cloog/reservoir-lim-lam3.c
@@ -6,6 +6,6 @@ for (int c1 = 5; c1 <= 5 * M; c1 += 1) {
     S2(c1 - 4 * c3 - 3, c3);
   if (c1 % 5 == 0)
     S4(c1 / 5);
-  for (int c3 = max(-c1 - 3 * floord(-c1, 3) + 1, 2 * c1 - 3 * ((M + c1 + 1) / 2) + 1); c3 <= (c1 + 1) / 5 - 1; c3 += 3)
+  for (int c3 = max(-((c1 + 2) % 3) + 3, 2 * c1 - 3 * ((M + c1 + 1) / 2) + 1); c3 <= (c1 + 1) / 5 - 1; c3 += 3)
     S3((c1 - 2 * c3 - 1) / 3, c3);
 }

diff --git a/test_inputs/codegen/omega/dagstuhl1-1.c b/test_inputs/codegen/omega/dagstuhl1-1.c
index a725c91..491fada 100644 (file)
--- a/test_inputs/codegen/omega/dagstuhl1-1.c
+++ b/test_inputs/codegen/omega/dagstuhl1-1.c
@@ -1,2 +1,2 @@
 for (int c0 = 0; c0 <= 99; c0 += 1)
-  s0(c0, c0 + 10 * floord(-c0 - 1, 10) + 10, -floord(-c0 - 1, 10) - 1);
+  s0(c0, (c0 + 10) % 10, (c0 + 10) / 10 - 1);

diff --git a/test_inputs/codegen/omega/hpf-0.c b/test_inputs/codegen/omega/hpf-0.c
index 2756b45..8b52b22 100644 (file)
--- a/test_inputs/codegen/omega/hpf-0.c
+++ b/test_inputs/codegen/omega/hpf-0.c
@@ -1,4 +1,4 @@
 if (P1 == P2 && P2 <= 3 && P2 >= 0)
   for (int c0 = 0; c0 <= min(2, -P2 + 4); c0 += 1)
-    for (int c2 = -P2 - c0 - 3 * floord(-P2 - c0, 3); c2 <= 3; c2 += 3)
+    for (int c2 = -((P2 + c0 + 2) % 3) + 2; c2 <= 3; c2 += 3)
       s0(c0, c0, c2, c2);

diff --git a/test_inputs/codegen/omega/lefur00-0.c b/test_inputs/codegen/omega/lefur00-0.c
index 4003e52..b3873c0 100644 (file)
--- a/test_inputs/codegen/omega/lefur00-0.c
+++ b/test_inputs/codegen/omega/lefur00-0.c
@@ -1,5 +1,5 @@
 for (int c0 = 0; c0 <= 15; c0 += 1)
   for (int c1 = max(c0 - (c0 + 1) / 2, 2 * c0 - 15); c1 <= min(c0 + 1, 15); c1 += 1)
-    for (int c2 = max(max(max(67 * c0 - (c0 + 1) / 3, 133 * c0 - 67 * c1 - floord(-c0 - c1 + 1, 3) - 66), 67 * c1 - floord(c1 - 1, 3) - 1), 1); c2 <= min(min(133 * c0 - 67 * c1 + floord(c0 + c1 - 1, 3) + 133, 100 * c0 + 99), 1000); c2 += 1)
+    for (int c2 = max(max(max(67 * c0 - (c0 + 1) / 3, 133 * c0 - 67 * c1 + (c0 + c1 + 1) / 3 - 66), 67 * c1 - floord(c1 - 1, 3) - 1), 1); c2 <= min(min(133 * c0 - 67 * c1 + floord(c0 + c1 - 1, 3) + 133, 100 * c0 + 99), 1000); c2 += 1)
       for (int c3 = max(max(200 * c0 - c2, 100 * c1 + c2 - c2 / 2), c2); c3 <= min(min(100 * c1 + (c2 + 1) / 2 + 99, 2 * c2 + 1), 200 * c0 - c2 + 199); c3 += 1)
         s0(c0, c1, c2, c3);

diff --git a/test_inputs/codegen/omega/lefur01-0.c b/test_inputs/codegen/omega/lefur01-0.c
index 4003e52..b3873c0 100644 (file)
--- a/test_inputs/codegen/omega/lefur01-0.c
+++ b/test_inputs/codegen/omega/lefur01-0.c
@@ -1,5 +1,5 @@
 for (int c0 = 0; c0 <= 15; c0 += 1)
   for (int c1 = max(c0 - (c0 + 1) / 2, 2 * c0 - 15); c1 <= min(c0 + 1, 15); c1 += 1)
-    for (int c2 = max(max(max(67 * c0 - (c0 + 1) / 3, 133 * c0 - 67 * c1 - floord(-c0 - c1 + 1, 3) - 66), 67 * c1 - floord(c1 - 1, 3) - 1), 1); c2 <= min(min(133 * c0 - 67 * c1 + floord(c0 + c1 - 1, 3) + 133, 100 * c0 + 99), 1000); c2 += 1)
+    for (int c2 = max(max(max(67 * c0 - (c0 + 1) / 3, 133 * c0 - 67 * c1 + (c0 + c1 + 1) / 3 - 66), 67 * c1 - floord(c1 - 1, 3) - 1), 1); c2 <= min(min(133 * c0 - 67 * c1 + floord(c0 + c1 - 1, 3) + 133, 100 * c0 + 99), 1000); c2 += 1)
       for (int c3 = max(max(200 * c0 - c2, 100 * c1 + c2 - c2 / 2), c2); c3 <= min(min(100 * c1 + (c2 + 1) / 2 + 99, 2 * c2 + 1), 200 * c0 - c2 + 199); c3 += 1)
         s0(c0, c1, c2, c3);

diff --git a/test_inputs/codegen/omega/lefur01-1.c b/test_inputs/codegen/omega/lefur01-1.c
index 6dd8625..804a9ef 100644 (file)
--- a/test_inputs/codegen/omega/lefur01-1.c
+++ b/test_inputs/codegen/omega/lefur01-1.c
@@ -1,5 +1,5 @@
 for (int c0 = 0; c0 <= 15; c0 += 1)
   for (int c1 = max(c0 - (c0 + 1) / 2, 2 * c0 - 15); c1 <= min(c0 + 1, 15); c1 += 1)
-    for (int c2 = max(max(max(133 * c0 - 67 * c1 - floord(-c0 - c1 + 1, 3) - 66, 67 * c1 - floord(c1 - 1, 3) - 1), 67 * c0 - (c0 + 1) / 3), 1); c2 <= min(min(133 * c0 - 67 * c1 + floord(c0 + c1 - 1, 3) + 133, 100 * c0 + 99), 1000); c2 += 1)
+    for (int c2 = max(max(max(133 * c0 - 67 * c1 + (c0 + c1 + 1) / 3 - 66, 67 * c1 - floord(c1 - 1, 3) - 1), 67 * c0 - (c0 + 1) / 3), 1); c2 <= min(min(133 * c0 - 67 * c1 + floord(c0 + c1 - 1, 3) + 133, 100 * c0 + 99), 1000); c2 += 1)
       for (int c3 = max(max(200 * c0 - c2, 100 * c1 + c2 - c2 / 2), c2); c3 <= min(min(100 * c1 + (c2 + 1) / 2 + 99, 2 * c2 + 1), 200 * c0 - c2 + 199); c3 += 1)
         s0(c0, c1, c2, c3);

diff --git a/test_inputs/codegen/omega/lefur03-0.c b/test_inputs/codegen/omega/lefur03-0.c
index 2560ade..3e58184 100644 (file)
--- a/test_inputs/codegen/omega/lefur03-0.c
+++ b/test_inputs/codegen/omega/lefur03-0.c
@@ -1,7 +1,7 @@
 for (int c0 = 0; c0 <= 3; c0 += 1)
   for (int c1 = max(0, 2 * c0 - 3); c1 <= min(c0 + c0 / 2 + 1, 3); c1 += 1)
     for (int c2 = c0; c2 <= min(min(3, 3 * c1 + 2), 2 * c0 - c1 + 1); c2 += 1)
-      for (int c3 = max(max(max(c1 - floord(-c1, 3) - 1, 0), c1 + c2 - (3 * c1 + c2) / 6 - 1), 2 * c0 - (c0 + c1 + 1) / 3 - 1); c3 <= min(c0 + 1, 3); c3 += 1)
-        for (int c4 = max(max(max(max(-200 * c1 + 400 * c3 - 199, 333 * c1 - floord(-c1 - 1, 3) - 1), 333 * c2 - floord(-c2 + 1, 3)), 667 * c0 - 333 * c1 - (c0 + c1) / 3 - 333), 250 * c3 + 1); c4 <= min(min(min(min(500 * c0 + 499, -200 * c1 + 400 * c3 + 400), 333 * c3 + floord(c3 - 1, 3) + 334), 1000), 333 * c2 + floord(c2 - 1, 3) + 333); c4 += 1)
+      for (int c3 = max(max(max(c1 + (c1 + 2) / 3 - 1, 0), c1 + c2 - (3 * c1 + c2) / 6 - 1), 2 * c0 - (c0 + c1 + 1) / 3 - 1); c3 <= min(c0 + 1, 3); c3 += 1)
+        for (int c4 = max(max(max(max(-200 * c1 + 400 * c3 - 199, 333 * c1 + (c1 + 3) / 3 - 1), 333 * c2 + (c2 + 1) / 3), 667 * c0 - 333 * c1 - (c0 + c1) / 3 - 333), 250 * c3 + 1); c4 <= min(min(min(min(500 * c0 + 499, -200 * c1 + 400 * c3 + 400), 333 * c3 - (-c3 + 3) / 3 + 334), 1000), 333 * c2 - (-c2 + 3) / 3 + 333); c4 += 1)
           for (int c5 = max(max(max(1000 * c3 - 2 * c4 + 2, 1000 * c0 - c4), 500 * c1 + c4 - c4 / 2), c4); c5 <= min(min(min(1000 * c3 - 2 * c4 + 1001, 1000 * c0 - c4 + 999), 500 * c1 + (c4 + 1) / 2 + 499), 2 * c4 + 1); c5 += 1)
             s0(c0, c1, c2, c3, c4, c5);

diff --git a/test_inputs/codegen/omega/lefur04-0.c b/test_inputs/codegen/omega/lefur04-0.c
index 91463e6..b531bf6 100644 (file)
--- a/test_inputs/codegen/omega/lefur04-0.c
+++ b/test_inputs/codegen/omega/lefur04-0.c
@@ -1,8 +1,8 @@
 for (int c0 = 0; c0 <= 3; c0 += 1)
   for (int c1 = max(0, 2 * c0 - 3); c1 <= min(c0 + 1, 3); c1 += 1)
     for (int c2 = c0; c2 <= min(min(3, 3 * c1 + 2), 2 * c0 - c1 + 1); c2 += 1)
-      for (int c3 = max(max(max(c2 - floord(c2 - 1, 3) - 1, c1 + c2 - (3 * c1 + c2) / 6 - 1), c1 - floord(-c1, 3) - 1), c0 - floord(-c2, 3) - 1); c3 <= min(c0 + c0 / 2 + 1, 3); c3 += 1)
-        for (int c5 = max(max(max(max(c1 - floord(-c1, 3) - 1, 0), 2 * c3 - 4), c3 - c3 / 3 - 1), c2 - c2 / 3 - 1); c5 <= min(min(-c2 + 2 * c3 + floord(-c2 - 1, 3) + 2, c1 + 1), c3); c5 += 1)
-          for (int c6 = max(max(max(max(max(250 * c3 + 1, 667 * c0 - 333 * c1 - (c0 + c1) / 3 - 333), -200 * c1 + 400 * c3 - 199), 333 * c1 - floord(-c1 - 1, 3) - 1), 1000 * c0 - 500 * c5 - 501), 333 * c2 - floord(-c2 + 1, 3)); c6 <= min(min(min(min(min(min(333 * c3 + floord(c3 - 1, 3) + 334, 1000), 333 * c2 + floord(c2 - 1, 3) + 333), 1000 * c0 - 500 * c5 + 997), 500 * c5 + 501), 500 * c0 + 499), -200 * c1 + 400 * c3 + 400); c6 += 1)
+      for (int c3 = max(max(max(c2 + (-c2 + 3) / 3 - 1, c1 + c2 - (3 * c1 + c2) / 6 - 1), c1 + (c1 + 2) / 3 - 1), c0 + (c2 + 2) / 3 - 1); c3 <= min(c0 + c0 / 2 + 1, 3); c3 += 1)
+        for (int c5 = max(max(max(max(c1 + (c1 + 2) / 3 - 1, 0), 2 * c3 - 4), c3 - c3 / 3 - 1), c2 - c2 / 3 - 1); c5 <= min(min(-c2 + 2 * c3 - (c2 + 3) / 3 + 2, c1 + 1), c3); c5 += 1)
+          for (int c6 = max(max(max(max(max(250 * c3 + 1, 667 * c0 - 333 * c1 - (c0 + c1) / 3 - 333), -200 * c1 + 400 * c3 - 199), 333 * c1 + (c1 + 3) / 3 - 1), 1000 * c0 - 500 * c5 - 501), 333 * c2 + (c2 + 1) / 3); c6 <= min(min(min(min(min(min(333 * c3 - (-c3 + 3) / 3 + 334, 1000), 333 * c2 - (-c2 + 3) / 3 + 333), 1000 * c0 - 500 * c5 + 997), 500 * c5 + 501), 500 * c0 + 499), -200 * c1 + 400 * c3 + 400); c6 += 1)
             for (int c7 = max(max(max(max(c6, 500 * c1 + c6 - c6 / 2), 1000 * c0 - c6), 500 * c5 + 2), 1000 * c3 - 2 * c6 + 2); c7 <= min(min(min(min(500 * c5 + 501, 2 * c6 + 1), 1000 * c3 - 2 * c6 + 1001), 1000 * c0 - c6 + 999), 500 * c1 + (c6 + 1) / 2 + 499); c7 += 1)
               s0(c0, c1, c2, c3, c2 / 3, c5, c6, c7);

diff --git a/test_inputs/codegen/omega/p.delft-0.c b/test_inputs/codegen/omega/p.delft-0.c
index 2756b45..8b52b22 100644 (file)
--- a/test_inputs/codegen/omega/p.delft-0.c
+++ b/test_inputs/codegen/omega/p.delft-0.c
@@ -1,4 +1,4 @@
 if (P1 == P2 && P2 <= 3 && P2 >= 0)
   for (int c0 = 0; c0 <= min(2, -P2 + 4); c0 += 1)
-    for (int c2 = -P2 - c0 - 3 * floord(-P2 - c0, 3); c2 <= 3; c2 += 3)
+    for (int c2 = -((P2 + c0 + 2) % 3) + 2; c2 <= 3; c2 += 3)
       s0(c0, c0, c2, c2);

diff --git a/test_inputs/codegen/omega/p.delft2-0.c b/test_inputs/codegen/omega/p.delft2-0.c
index 3b0a246..99d4005 100644 (file)
--- a/test_inputs/codegen/omega/p.delft2-0.c
+++ b/test_inputs/codegen/omega/p.delft2-0.c
@@ -1,11 +1,11 @@
 if ((2 * floord(P2, 2) == P2 && 2 * floord(P1, 2) == P1 && P2 >= 0 && P2 <= 3 && P1 >= 0 && P1 <= 3) || (2 * floord(P2, 2) == P2 && 2 * floord(P1 - 1, 2) + 1 == P1 && P2 >= 0 && P2 <= 3 && P1 >= 0 && P1 <= 3) || (2 * floord(P2 - 1, 2) + 1 == P2 && 2 * floord(P1, 2) == P1 && P2 >= 0 && P2 <= 3 && P1 >= 0 && P1 <= 3) || (2 * floord(P2 - 1, 2) + 1 == P2 && 2 * floord(P1 - 1, 2) + 1 == P1 && P2 >= 0 && P2 <= 3 && P1 >= 0 && P1 <= 3))
   for (int c0 = P1 - 1; c0 <= 3; c0 += 1)
     if ((2 * floord(c0, 2) == c0 && P2 % 2 == 0 && 2 * floord(P1 - 1, 2) + 1 == P1) || (2 * floord(c0, 2) == c0 && 2 * floord(P2 - 1, 2) + 1 == P2 && 2 * floord(P1 - 1, 2) + 1 == P1) || (2 * floord(c0 - 1, 2) + 1 == c0 && P2 % 2 == 0 && P1 % 2 == 0) || (2 * floord(c0 - 1, 2) + 1 == c0 && 2 * floord(P2 - 1, 2) + 1 == P2 && P1 % 2 == 0))
-      for (int c2 = 0; c2 <= floord(-P1 - 1, 4) + 8; c2 += 1)
-        if ((2 * floord(P2 - 1, 4) + 2 * (P2 / 4) + 2 == P2 && 2 * floord(P2 - 1, 2) + 2 == P2 && P2 <= 6 && 18 * floord(9 * P1 + 17 * c0 + 14 * c2 + 3, 18) + 1 >= 9 * P1 + 17 * c0 + 14 * c2) || (2 * floord(P2 - 1, 2) + 1 == P2 && P2 + 1 >= 0 && 18 * floord(9 * P1 + 17 * c0 + 14 * c2 + 3, 18) + 1 >= 9 * P1 + 17 * c0 + 14 * c2 && 4 * floord(P2 - 1, 4) + 3 >= P2))
-          for (int c3 = 0; c3 <= floord(-P2 - 1, 4) + 8; c3 += 1)
+      for (int c2 = 0; c2 <= -((P1 + 4) / 4) + 8; c2 += 1)
+        if ((-2 * ((-P2 + 4) / 4) + 2 * (P2 / 4) + 2 == P2 && 2 * floord(P2 - 1, 2) + 2 == P2 && P2 <= 6 && 18 * floord(9 * P1 + 17 * c0 + 14 * c2 + 3, 18) + 1 >= 9 * P1 + 17 * c0 + 14 * c2) || (2 * floord(P2 - 1, 2) + 1 == P2 && P2 + 1 >= 0 && 18 * floord(9 * P1 + 17 * c0 + 14 * c2 + 3, 18) + 1 >= 9 * P1 + 17 * c0 + 14 * c2 && (-P2 + 4) % 4 >= 1))
+          for (int c3 = 0; c3 <= -((P2 + 4) / 4) + 8; c3 += 1)
             if ((5 * P2 + 2 * c3) % 9 <= 3 && 9 * ((4 * P2 + 3) / 9 / 2) + 7 >= 2 * P2 && 2 * P2 + 1 >= 9 * ((4 * P2 + 3) / 9 / 2))
               if (c0 + 1 == P1 && (5 * P1 + 2 * c2) % 9 <= 2 && P1 >= 1) {
-                s0(P1 - 1, P2, c2, c3, ((5 * P1 + 2 * c2) % 9) + 1, -4 * P2 + 2 * c3 + 9 * floord(4 * P2 - 2 * c3 - 1, 9) + 9);
+                s0(P1 - 1, P2, c2, c3, ((5 * P1 + 2 * c2) % 9) + 1, (-4 * P2 + 2 * c3 + 9) % 9);
               } else if (c2 % 4 == 0 && c0 == 3 && P1 == 0)
-                s0(3, P2, c2, c3, (-c2 + 12) / 4, -4 * P2 + 2 * c3 + 9 * floord(4 * P2 - 2 * c3 - 1, 9) + 9);
+                s0(3, P2, c2, c3, (-c2 + 12) / 4, (-4 * P2 + 2 * c3 + 9) % 9);