add isl_pw_qpolynomial_foreach_lifted_piece

diff --git a/doc/user.pod b/doc/user.pod
index 3f9129d..49506d2 100644 (file)
--- a/doc/user.pod
+++ b/doc/user.pod
@@ -1192,16 +1192,31 @@ functions.
 =head3 Inspecting (Piecewise) Quasipolynomials
 
 To iterate over the cells in a piecewise quasipolynomial,
-use the following function
+use either of the following two functions
 
        int isl_pw_qpolynomial_foreach_piece(
                __isl_keep isl_pw_qpolynomial *pwqp,
                int (*fn)(__isl_take isl_set *set,
                          __isl_take isl_qpolynomial *qp,
                          void *user), void *user);
+       int isl_pw_qpolynomial_foreach_lifted_piece(
+               __isl_keep isl_pw_qpolynomial *pwqp,
+               int (*fn)(__isl_take isl_set *set,
+                         __isl_take isl_qpolynomial *qp,
+                         void *user), void *user);
 
 As usual, the function C<fn> should return C<0> on success
-and C<-1> on failure.
+and C<-1> on failure.  The difference between
+C<isl_pw_qpolynomial_foreach_piece> and
+C<isl_pw_qpolynomial_foreach_lifted_piece> is that
+C<isl_pw_qpolynomial_foreach_lifted_piece> will first
+compute unique representations for all existentially quantified
+variables and then turn these existentially quantified variables
+into extra set variables, adapting the associated quasipolynomial
+accordingly.  This means that the C<set> passed to C<fn>
+will not have any existentially quantified variables, but that
+the dimensions of the sets may be different for different
+invocations of C<fn>.
 
 To iterate over all terms in a quasipolynomial,
 use

diff --git a/include/isl_polynomial.h b/include/isl_polynomial.h
index 8677e7a..7820ce0 100644 (file)
--- a/include/isl_polynomial.h
+++ b/include/isl_polynomial.h
@@ -95,6 +95,9 @@ __isl_give isl_qpolynomial *isl_pw_qpolynomial_eval(
 int isl_pw_qpolynomial_foreach_piece(__isl_keep isl_pw_qpolynomial *pwqp,
        int (*fn)(__isl_take isl_set *set, __isl_take isl_qpolynomial *qp,
                    void *user), void *user);
+int isl_pw_qpolynomial_foreach_lifted_piece(__isl_keep isl_pw_qpolynomial *pwqp,
+       int (*fn)(__isl_take isl_set *set, __isl_take isl_qpolynomial *qp,
+                   void *user), void *user);
 
 void isl_pw_qpolynomial_print(__isl_keep isl_pw_qpolynomial *pwqp, FILE *out,
        unsigned output_format);

diff --git a/isl_polynomial.c b/isl_polynomial.c
index 1a9bcc2..0b2e3c0 100644 (file)
--- a/isl_polynomial.c
+++ b/isl_polynomial.c
@@ -2098,3 +2098,128 @@ int isl_pw_qpolynomial_foreach_piece(__isl_keep isl_pw_qpolynomial *pwqp,
 
        return 0;
 }
+
+static int any_divs(__isl_keep isl_set *set)
+{
+       int i;
+
+       if (!set)
+               return -1;
+
+       for (i = 0; i < set->n; ++i)
+               if (set->p[i]->n_div > 0)
+                       return 1;
+
+       return 0;
+}
+
+__isl_give isl_qpolynomial *isl_qpolynomial_lift(__isl_take isl_qpolynomial *qp,
+       __isl_take isl_dim *dim)
+{
+       if (!qp || !dim)
+               goto error;
+
+       if (isl_dim_equal(qp->dim, dim)) {
+               isl_dim_free(dim);
+               return qp;
+       }
+
+       qp = isl_qpolynomial_cow(qp);
+       if (!qp)
+               goto error;
+
+       if (qp->div->n_row) {
+               int i;
+               int extra;
+               unsigned total;
+               int *exp;
+
+               extra = isl_dim_size(dim, isl_dim_set) -
+                               isl_dim_size(qp->dim, isl_dim_set);
+               total = isl_dim_total(qp->dim);
+               exp = isl_alloc_array(qp->div->ctx, int, qp->div->n_row);
+               if (!exp)
+                       goto error;
+               for (i = 0; i < qp->div->n_row; ++i)
+                       exp[i] = extra + i;
+               qp->upoly = expand(qp->upoly, exp, total);
+               free(exp);
+               if (!qp->upoly)
+                       goto error;
+               qp->div = isl_mat_insert_cols(qp->div, 2 + total, extra);
+               if (!qp->div)
+                       goto error;
+               for (i = 0; i < qp->div->n_row; ++i)
+                       isl_seq_clr(qp->div->row[i] + 2 + total, extra);
+       }
+
+       isl_dim_free(qp->dim);
+       qp->dim = dim;
+
+       return qp;
+error:
+       isl_dim_free(dim);
+       isl_qpolynomial_free(qp);
+       return NULL;
+}
+
+static int foreach_lifted_subset(__isl_take isl_set *set,
+       __isl_take isl_qpolynomial *qp,
+       int (*fn)(__isl_take isl_set *set, __isl_take isl_qpolynomial *qp,
+                   void *user), void *user)
+{
+       int i;
+
+       if (!set || !qp)
+               goto error;
+
+       for (i = 0; i < set->n; ++i) {
+               isl_set *lift;
+               isl_qpolynomial *copy;
+
+               lift = isl_set_from_basic_set(isl_basic_set_copy(set->p[i]));
+               lift = isl_set_lift(lift);
+
+               copy = isl_qpolynomial_copy(qp);
+               copy = isl_qpolynomial_lift(copy, isl_set_get_dim(lift));
+
+               if (fn(lift, copy, user) < 0)
+                       goto error;
+       }
+
+       isl_set_free(set);
+       isl_qpolynomial_free(qp);
+
+       return 0;
+error:
+       isl_set_free(set);
+       isl_qpolynomial_free(qp);
+       return -1;
+}
+
+int isl_pw_qpolynomial_foreach_lifted_piece(__isl_keep isl_pw_qpolynomial *pwqp,
+       int (*fn)(__isl_take isl_set *set, __isl_take isl_qpolynomial *qp,
+                   void *user), void *user)
+{
+       int i;
+
+       if (!pwqp)
+               return -1;
+
+       for (i = 0; i < pwqp->n; ++i) {
+               isl_set *set;
+               isl_qpolynomial *qp;
+
+               set = isl_set_copy(pwqp->p[i].set);
+               qp = isl_qpolynomial_copy(pwqp->p[i].qp);
+               if (!any_divs(set)) {
+                       if (fn(set, qp, user) < 0)
+                               return -1;
+                       continue;
+               }
+               if (foreach_lifted_subset(set, qp, fn, user) < 0)
+                       return -1;
+       }
+
+       return 0;
+}