#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
*
* 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);
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;
}