2 #include "isl_map_private.h"
3 #include "isl_equalities.h"
5 /* Use the n equalities of bset to unimodularly transform the
6 * variables x such that n transformed variables x1' have a constant value
7 * and rewrite the constraints of bset in terms of the remaining
8 * transformed variables x2'. The matrix pointed to by T maps
9 * the new variables x2' back to the original variables x, while T2
10 * maps the original variables to the new variables.
12 * Let the equalities of bset be
16 * Compute the (left) Hermite normal form of M,
18 * M [U1 U2] = M U = H = [H1 0]
20 * M = H Q = [H1 0] [Q1]
23 * with U, Q unimodular, Q = U^{-1} (and H lower triangular).
24 * Define the transformed variables as
26 * x = [U1 U2] [ x1' ] = [U1 U2] [Q1] x
29 * The equalities then become
31 * H1 x1' - c = 0 or x1' = H1^{-1} c = c'
33 * If any of the c' is non-integer, then the original set has no
34 * integer solutions (since the x' are a unimodular transformation
36 * Otherwise, the transformation is given by
38 * x = U1 H1^{-1} c + U2 x2'
40 * The inverse transformation is simply
44 static struct isl_basic_set *compress_variables(struct isl_ctx *ctx,
45 struct isl_basic_set *bset, struct isl_mat **T, struct isl_mat **T2)
48 struct isl_mat *H = NULL, *C = NULL, *H1, *U = NULL, *U1, *U2, *TC;
56 isl_assert(ctx, bset->nparam == 0, goto error);
57 isl_assert(ctx, bset->n_div == 0, goto error);
58 isl_assert(ctx, bset->n_eq <= bset->dim, goto error);
62 H = isl_mat_sub_alloc(ctx, bset->eq, 0, bset->n_eq, 1, bset->dim);
63 H = isl_mat_left_hermite(ctx, H, &U, T2);
64 if (!H || !U || (T2 && !*T2))
67 *T2 = isl_mat_drop_rows(ctx, *T2, 0, bset->n_eq);
68 *T2 = isl_mat_lin_to_aff(ctx, *T2);
72 C = isl_mat_alloc(ctx, 1+bset->n_eq, 1);
75 isl_int_set_si(C->row[0][0], 1);
76 isl_mat_sub_neg(ctx, C->row+1, bset->eq, bset->n_eq, 0, 0, 1);
77 H1 = isl_mat_sub_alloc(ctx, H->row, 0, H->n_row, 0, H->n_row);
78 H1 = isl_mat_lin_to_aff(ctx, H1);
79 TC = isl_mat_inverse_product(ctx, H1, C);
83 if (!isl_int_is_one(TC->row[0][0])) {
84 for (i = 0; i < bset->n_eq; ++i) {
85 if (!isl_int_is_divisible_by(TC->row[1+i][0], TC->row[0][0])) {
86 isl_mat_free(ctx, TC);
89 isl_mat_free(ctx, *T2);
92 return isl_basic_set_set_to_empty(ctx, bset);
94 isl_seq_scale_down(TC->row[1+i], TC->row[1+i], TC->row[0][0], 1);
96 isl_int_set_si(TC->row[0][0], 1);
98 U1 = isl_mat_sub_alloc(ctx, U->row, 0, U->n_row, 0, bset->n_eq);
99 U1 = isl_mat_lin_to_aff(ctx, U1);
100 U2 = isl_mat_sub_alloc(ctx, U->row, 0, U->n_row,
101 bset->n_eq, U->n_row - bset->n_eq);
102 U2 = isl_mat_lin_to_aff(ctx, U2);
103 isl_mat_free(ctx, U);
104 TC = isl_mat_product(ctx, U1, TC);
105 TC = isl_mat_aff_direct_sum(ctx, TC, U2);
106 bset = isl_basic_set_preimage(ctx, bset, T ? isl_mat_copy(ctx, TC) : TC);
111 isl_mat_free(ctx, H);
112 isl_mat_free(ctx, U);
114 isl_mat_free(ctx, *T2);
115 isl_basic_set_free(ctx, bset);
123 struct isl_basic_set *isl_basic_set_remove_equalities(struct isl_ctx *ctx,
124 struct isl_basic_set *bset, struct isl_mat **T, struct isl_mat **T2)
126 isl_assert(ctx, bset->nparam == 0, goto error);
131 bset = isl_basic_set_gauss(ctx, bset, NULL);
132 if (F_ISSET(bset, ISL_BASIC_SET_EMPTY))
134 bset = compress_variables(ctx, bset, T, T2);
137 isl_basic_set_free(ctx, bset);