isl_equalities.c: extract and export isl_mat_variable_compression

diff --git a/isl_equalities.c b/isl_equalities.c
index 8835fdf..c8489a0 100644 (file)
--- a/isl_equalities.c
+++ b/isl_equalities.c
@@ -3,18 +3,20 @@
 #include "isl_map_private.h"
 #include "isl_equalities.h"
 
-/* Use the n equalities of bset to unimodularly transform the
- * variables x such that n transformed variables x1' have a constant value
- * and rewrite the constraints of bset in terms of the remaining
- * transformed variables x2'.  The matrix pointed to by T maps
- * the new variables x2' back to the original variables x, while T2
- * maps the original variables to the new variables.
- *
- * Let the equalities of bset be
+/* Given a set of equalities
  *
  *             M x - c = 0
  *
- * Compute the (left) Hermite normal form of M,
+ * this function computes unimodular transformation from a lower-dimensional
+ * space to the original space that bijectively maps the integer points x'
+ * in the lower-dimensional space to the integer points x in the original
+ * space that satisfy the equalities.
+ *
+ * The input is given as a matrix B = [ -c M ] and the out is a
+ * matrix that maps [1 x'] to [1 x].
+ * If T2 is not NULL, then *T2 is set to a matrix mapping [1 x] to [1 x'].
+ *
+ * First compute the (left) Hermite normal form of M,
  *
  *             M [U1 U2] = M U = H = [H1 0]
  * or
@@ -42,41 +44,34 @@
  *
  *             x2' = Q2 x
  */
-static struct isl_basic_set *compress_variables(struct isl_ctx *ctx,
-       struct isl_basic_set *bset, struct isl_mat **T, struct isl_mat **T2)
+struct isl_mat *isl_mat_variable_compression(struct isl_ctx *ctx,
+                       struct isl_mat *B, struct isl_mat **T2)
 {
        int i;
        struct isl_mat *H = NULL, *C = NULL, *H1, *U = NULL, *U1, *U2, *TC;
        unsigned dim;
 
-       if (T)
-               *T = NULL;
        if (T2)
                *T2 = NULL;
-       if (!bset)
+       if (!B)
                goto error;
-       isl_assert(ctx, isl_basic_set_n_param(bset) == 0, goto error);
-       isl_assert(ctx, bset->n_div == 0, goto error);
-       dim = isl_basic_set_n_dim(bset);
-       isl_assert(ctx, bset->n_eq <= dim, goto error);
-       if (bset->n_eq == 0)
-               return bset;
 
-       H = isl_mat_sub_alloc(ctx, bset->eq, 0, bset->n_eq, 1, dim);
+       dim = B->n_col - 1;
+       H = isl_mat_sub_alloc(ctx, B->row, 0, B->n_row, 1, dim);
        H = isl_mat_left_hermite(ctx, H, 0, &U, T2);
        if (!H || !U || (T2 && !*T2))
                goto error;
        if (T2) {
-               *T2 = isl_mat_drop_rows(ctx, *T2, 0, bset->n_eq);
+               *T2 = isl_mat_drop_rows(ctx, *T2, 0, B->n_row);
                *T2 = isl_mat_lin_to_aff(ctx, *T2);
                if (!*T2)
                        goto error;
        }
-       C = isl_mat_alloc(ctx, 1+bset->n_eq, 1);
+       C = isl_mat_alloc(ctx, 1+B->n_row, 1);
        if (!C)
                goto error;
        isl_int_set_si(C->row[0][0], 1);
-       isl_mat_sub_neg(ctx, C->row+1, bset->eq, bset->n_eq, 0, 0, 1);
+       isl_mat_sub_neg(ctx, C->row+1, B->row, B->n_row, 0, 0, 1);
        H1 = isl_mat_sub_alloc(ctx, H->row, 0, H->n_row, 0, H->n_row);
        H1 = isl_mat_lin_to_aff(ctx, H1);
        TC = isl_mat_inverse_product(ctx, H1, C);
@@ -84,42 +79,89 @@ static struct isl_basic_set *compress_variables(struct isl_ctx *ctx,
                goto error;
        isl_mat_free(ctx, H);
        if (!isl_int_is_one(TC->row[0][0])) {
-               for (i = 0; i < bset->n_eq; ++i) {
+               for (i = 0; i < B->n_row; ++i) {
                        if (!isl_int_is_divisible_by(TC->row[1+i][0], TC->row[0][0])) {
+                               isl_mat_free(ctx, B);
                                isl_mat_free(ctx, TC);
                                isl_mat_free(ctx, U);
                                if (T2) {
                                        isl_mat_free(ctx, *T2);
                                        *T2 = NULL;
                                }
-                               return isl_basic_set_set_to_empty(bset);
+                               return isl_mat_alloc(ctx, 1 + B->n_col, 0);
                        }
                        isl_seq_scale_down(TC->row[1+i], TC->row[1+i], TC->row[0][0], 1);
                }
                isl_int_set_si(TC->row[0][0], 1);
        }
-       U1 = isl_mat_sub_alloc(ctx, U->row, 0, U->n_row, 0, bset->n_eq);
+       U1 = isl_mat_sub_alloc(ctx, U->row, 0, U->n_row, 0, B->n_row);
        U1 = isl_mat_lin_to_aff(ctx, U1);
        U2 = isl_mat_sub_alloc(ctx, U->row, 0, U->n_row,
-                               bset->n_eq, U->n_row - bset->n_eq);
+                               B->n_row, U->n_row - B->n_row);
        U2 = isl_mat_lin_to_aff(ctx, U2);
        isl_mat_free(ctx, U);
        TC = isl_mat_product(ctx, U1, TC);
        TC = isl_mat_aff_direct_sum(ctx, TC, U2);
-       bset = isl_basic_set_preimage(ctx, bset, T ? isl_mat_copy(ctx, TC) : TC);
-       if (T)
-               *T = TC;
-       return bset;
+
+       isl_mat_free(ctx, B);
+
+       return TC;
 error:
+       isl_mat_free(ctx, B);
        isl_mat_free(ctx, H);
        isl_mat_free(ctx, U);
-       if (T2)
+       if (T2) {
                isl_mat_free(ctx, *T2);
-       isl_basic_set_free(bset);
+               *T2 = NULL;
+       }
+       return NULL;
+}
+
+/* Use the n equalities of bset to unimodularly transform the
+ * variables x such that n transformed variables x1' have a constant value
+ * and rewrite the constraints of bset in terms of the remaining
+ * transformed variables x2'.  The matrix pointed to by T maps
+ * the new variables x2' back to the original variables x, while T2
+ * maps the original variables to the new variables.
+ */
+static struct isl_basic_set *compress_variables(struct isl_ctx *ctx,
+       struct isl_basic_set *bset, struct isl_mat **T, struct isl_mat **T2)
+{
+       struct isl_mat *B, *TC;
+       unsigned dim;
+
        if (T)
                *T = NULL;
        if (T2)
                *T2 = NULL;
+       if (!bset)
+               goto error;
+       isl_assert(ctx, isl_basic_set_n_param(bset) == 0, goto error);
+       isl_assert(ctx, bset->n_div == 0, goto error);
+       dim = isl_basic_set_n_dim(bset);
+       isl_assert(ctx, bset->n_eq <= dim, goto error);
+       if (bset->n_eq == 0)
+               return bset;
+
+       B = isl_mat_sub_alloc(ctx, bset->eq, 0, bset->n_eq, 0, 1 + dim);
+       TC = isl_mat_variable_compression(ctx, B, T2);
+       if (!TC)
+               goto error;
+       if (TC->n_col == 0) {
+               isl_mat_free(ctx, TC);
+               if (T2) {
+                       isl_mat_free(ctx, *T2);
+                       *T2 = NULL;
+               }
+               return isl_basic_set_set_to_empty(bset);
+       }
+
+       bset = isl_basic_set_preimage(ctx, bset, T ? isl_mat_copy(ctx, TC) : TC);
+       if (T)
+               *T = TC;
+       return bset;
+error:
+       isl_basic_set_free(bset);
        return NULL;
 }
 

diff --git a/isl_equalities.h b/isl_equalities.h
index 47fa6da..88489aa 100644 (file)
--- a/isl_equalities.h
+++ b/isl_equalities.h
@@ -8,6 +8,8 @@
 extern "C" {
 #endif
 
+struct isl_mat *isl_mat_variable_compression(struct isl_ctx *ctx,
+                       struct isl_mat *B, struct isl_mat **T2);
 struct isl_basic_set *isl_basic_set_remove_equalities(
        struct isl_basic_set *bset, struct isl_mat **T, struct isl_mat **T2);