isl_equalities.c 24 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808809810811812813814815816817818819820821822823824825826827828829830831832833834835836837838839840841842843844845846847848849850851852853854855856857858859860861862863864865866867868869870871872873874875876877878879880881882883884885886887888889890891892893894895896897
  1. /*
  2. * Copyright 2008-2009 Katholieke Universiteit Leuven
  3. * Copyright 2010 INRIA Saclay
  4. *
  5. * Use of this software is governed by the MIT license
  6. *
  7. * Written by Sven Verdoolaege, K.U.Leuven, Departement
  8. * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium
  9. * and INRIA Saclay - Ile-de-France, Parc Club Orsay Universite,
  10. * ZAC des vignes, 4 rue Jacques Monod, 91893 Orsay, France
  11. */
  12. #include <isl_mat_private.h>
  13. #include <isl_vec_private.h>
  14. #include <isl_seq.h>
  15. #include "isl_map_private.h"
  16. #include "isl_equalities.h"
  17. #include <isl_val_private.h>
  18. /* Given a set of modulo constraints
  19. *
  20. * c + A y = 0 mod d
  21. *
  22. * this function computes a particular solution y_0
  23. *
  24. * The input is given as a matrix B = [ c A ] and a vector d.
  25. *
  26. * The output is matrix containing the solution y_0 or
  27. * a zero-column matrix if the constraints admit no integer solution.
  28. *
  29. * The given set of constrains is equivalent to
  30. *
  31. * c + A y = -D x
  32. *
  33. * with D = diag d and x a fresh set of variables.
  34. * Reducing both c and A modulo d does not change the
  35. * value of y in the solution and may lead to smaller coefficients.
  36. * Let M = [ D A ] and [ H 0 ] = M U, the Hermite normal form of M.
  37. * Then
  38. * [ x ]
  39. * M [ y ] = - c
  40. * and so
  41. * [ x ]
  42. * [ H 0 ] U^{-1} [ y ] = - c
  43. * Let
  44. * [ A ] [ x ]
  45. * [ B ] = U^{-1} [ y ]
  46. * then
  47. * H A + 0 B = -c
  48. *
  49. * so B may be chosen arbitrarily, e.g., B = 0, and then
  50. *
  51. * [ x ] = [ -c ]
  52. * U^{-1} [ y ] = [ 0 ]
  53. * or
  54. * [ x ] [ -c ]
  55. * [ y ] = U [ 0 ]
  56. * specifically,
  57. *
  58. * y = U_{2,1} (-c)
  59. *
  60. * If any of the coordinates of this y are non-integer
  61. * then the constraints admit no integer solution and
  62. * a zero-column matrix is returned.
  63. */
  64. static __isl_give isl_mat *particular_solution(__isl_keep isl_mat *B,
  65. __isl_keep isl_vec *d)
  66. {
  67. int i, j;
  68. struct isl_mat *M = NULL;
  69. struct isl_mat *C = NULL;
  70. struct isl_mat *U = NULL;
  71. struct isl_mat *H = NULL;
  72. struct isl_mat *cst = NULL;
  73. struct isl_mat *T = NULL;
  74. M = isl_mat_alloc(B->ctx, B->n_row, B->n_row + B->n_col - 1);
  75. C = isl_mat_alloc(B->ctx, 1 + B->n_row, 1);
  76. if (!M || !C)
  77. goto error;
  78. isl_int_set_si(C->row[0][0], 1);
  79. for (i = 0; i < B->n_row; ++i) {
  80. isl_seq_clr(M->row[i], B->n_row);
  81. isl_int_set(M->row[i][i], d->block.data[i]);
  82. isl_int_neg(C->row[1 + i][0], B->row[i][0]);
  83. isl_int_fdiv_r(C->row[1+i][0], C->row[1+i][0], M->row[i][i]);
  84. for (j = 0; j < B->n_col - 1; ++j)
  85. isl_int_fdiv_r(M->row[i][B->n_row + j],
  86. B->row[i][1 + j], M->row[i][i]);
  87. }
  88. M = isl_mat_left_hermite(M, 0, &U, NULL);
  89. if (!M || !U)
  90. goto error;
  91. H = isl_mat_sub_alloc(M, 0, B->n_row, 0, B->n_row);
  92. H = isl_mat_lin_to_aff(H);
  93. C = isl_mat_inverse_product(H, C);
  94. if (!C)
  95. goto error;
  96. for (i = 0; i < B->n_row; ++i) {
  97. if (!isl_int_is_divisible_by(C->row[1+i][0], C->row[0][0]))
  98. break;
  99. isl_int_divexact(C->row[1+i][0], C->row[1+i][0], C->row[0][0]);
  100. }
  101. if (i < B->n_row)
  102. cst = isl_mat_alloc(B->ctx, B->n_row, 0);
  103. else
  104. cst = isl_mat_sub_alloc(C, 1, B->n_row, 0, 1);
  105. T = isl_mat_sub_alloc(U, B->n_row, B->n_col - 1, 0, B->n_row);
  106. cst = isl_mat_product(T, cst);
  107. isl_mat_free(M);
  108. isl_mat_free(C);
  109. isl_mat_free(U);
  110. return cst;
  111. error:
  112. isl_mat_free(M);
  113. isl_mat_free(C);
  114. isl_mat_free(U);
  115. return NULL;
  116. }
  117. /* Compute and return the matrix
  118. *
  119. * U_1^{-1} diag(d_1, 1, ..., 1)
  120. *
  121. * with U_1 the unimodular completion of the first (and only) row of B.
  122. * The columns of this matrix generate the lattice that satisfies
  123. * the single (linear) modulo constraint.
  124. */
  125. static __isl_take isl_mat *parameter_compression_1(__isl_keep isl_mat *B,
  126. __isl_keep isl_vec *d)
  127. {
  128. struct isl_mat *U;
  129. U = isl_mat_alloc(B->ctx, B->n_col - 1, B->n_col - 1);
  130. if (!U)
  131. return NULL;
  132. isl_seq_cpy(U->row[0], B->row[0] + 1, B->n_col - 1);
  133. U = isl_mat_unimodular_complete(U, 1);
  134. U = isl_mat_right_inverse(U);
  135. if (!U)
  136. return NULL;
  137. isl_mat_col_mul(U, 0, d->block.data[0], 0);
  138. U = isl_mat_lin_to_aff(U);
  139. return U;
  140. }
  141. /* Compute a common lattice of solutions to the linear modulo
  142. * constraints specified by B and d.
  143. * See also the documentation of isl_mat_parameter_compression.
  144. * We put the matrix
  145. *
  146. * A = [ L_1^{-T} L_2^{-T} ... L_k^{-T} ]
  147. *
  148. * on a common denominator. This denominator D is the lcm of modulos d.
  149. * Since L_i = U_i^{-1} diag(d_i, 1, ... 1), we have
  150. * L_i^{-T} = U_i^T diag(d_i, 1, ... 1)^{-T} = U_i^T diag(1/d_i, 1, ..., 1).
  151. * Putting this on the common denominator, we have
  152. * D * L_i^{-T} = U_i^T diag(D/d_i, D, ..., D).
  153. */
  154. static __isl_give isl_mat *parameter_compression_multi(__isl_keep isl_mat *B,
  155. __isl_keep isl_vec *d)
  156. {
  157. int i, j, k;
  158. isl_int D;
  159. struct isl_mat *A = NULL, *U = NULL;
  160. struct isl_mat *T;
  161. unsigned size;
  162. isl_int_init(D);
  163. isl_vec_lcm(d, &D);
  164. size = B->n_col - 1;
  165. A = isl_mat_alloc(B->ctx, size, B->n_row * size);
  166. U = isl_mat_alloc(B->ctx, size, size);
  167. if (!U || !A)
  168. goto error;
  169. for (i = 0; i < B->n_row; ++i) {
  170. isl_seq_cpy(U->row[0], B->row[i] + 1, size);
  171. U = isl_mat_unimodular_complete(U, 1);
  172. if (!U)
  173. goto error;
  174. isl_int_divexact(D, D, d->block.data[i]);
  175. for (k = 0; k < U->n_col; ++k)
  176. isl_int_mul(A->row[k][i*size+0], D, U->row[0][k]);
  177. isl_int_mul(D, D, d->block.data[i]);
  178. for (j = 1; j < U->n_row; ++j)
  179. for (k = 0; k < U->n_col; ++k)
  180. isl_int_mul(A->row[k][i*size+j],
  181. D, U->row[j][k]);
  182. }
  183. A = isl_mat_left_hermite(A, 0, NULL, NULL);
  184. T = isl_mat_sub_alloc(A, 0, A->n_row, 0, A->n_row);
  185. T = isl_mat_lin_to_aff(T);
  186. if (!T)
  187. goto error;
  188. isl_int_set(T->row[0][0], D);
  189. T = isl_mat_right_inverse(T);
  190. if (!T)
  191. goto error;
  192. isl_assert(T->ctx, isl_int_is_one(T->row[0][0]), goto error);
  193. T = isl_mat_transpose(T);
  194. isl_mat_free(A);
  195. isl_mat_free(U);
  196. isl_int_clear(D);
  197. return T;
  198. error:
  199. isl_mat_free(A);
  200. isl_mat_free(U);
  201. isl_int_clear(D);
  202. return NULL;
  203. }
  204. /* Given a set of modulo constraints
  205. *
  206. * c + A y = 0 mod d
  207. *
  208. * this function returns an affine transformation T,
  209. *
  210. * y = T y'
  211. *
  212. * that bijectively maps the integer vectors y' to integer
  213. * vectors y that satisfy the modulo constraints.
  214. *
  215. * This function is inspired by Section 2.5.3
  216. * of B. Meister, "Stating and Manipulating Periodicity in the Polytope
  217. * Model. Applications to Program Analysis and Optimization".
  218. * However, the implementation only follows the algorithm of that
  219. * section for computing a particular solution and not for computing
  220. * a general homogeneous solution. The latter is incomplete and
  221. * may remove some valid solutions.
  222. * Instead, we use an adaptation of the algorithm in Section 7 of
  223. * B. Meister, S. Verdoolaege, "Polynomial Approximations in the Polytope
  224. * Model: Bringing the Power of Quasi-Polynomials to the Masses".
  225. *
  226. * The input is given as a matrix B = [ c A ] and a vector d.
  227. * Each element of the vector d corresponds to a row in B.
  228. * The output is a lower triangular matrix.
  229. * If no integer vector y satisfies the given constraints then
  230. * a matrix with zero columns is returned.
  231. *
  232. * We first compute a particular solution y_0 to the given set of
  233. * modulo constraints in particular_solution. If no such solution
  234. * exists, then we return a zero-columned transformation matrix.
  235. * Otherwise, we compute the generic solution to
  236. *
  237. * A y = 0 mod d
  238. *
  239. * That is we want to compute G such that
  240. *
  241. * y = G y''
  242. *
  243. * with y'' integer, describes the set of solutions.
  244. *
  245. * We first remove the common factors of each row.
  246. * In particular if gcd(A_i,d_i) != 1, then we divide the whole
  247. * row i (including d_i) by this common factor. If afterwards gcd(A_i) != 1,
  248. * then we divide this row of A by the common factor, unless gcd(A_i) = 0.
  249. * In the later case, we simply drop the row (in both A and d).
  250. *
  251. * If there are no rows left in A, then G is the identity matrix. Otherwise,
  252. * for each row i, we now determine the lattice of integer vectors
  253. * that satisfies this row. Let U_i be the unimodular extension of the
  254. * row A_i. This unimodular extension exists because gcd(A_i) = 1.
  255. * The first component of
  256. *
  257. * y' = U_i y
  258. *
  259. * needs to be a multiple of d_i. Let y' = diag(d_i, 1, ..., 1) y''.
  260. * Then,
  261. *
  262. * y = U_i^{-1} diag(d_i, 1, ..., 1) y''
  263. *
  264. * for arbitrary integer vectors y''. That is, y belongs to the lattice
  265. * generated by the columns of L_i = U_i^{-1} diag(d_i, 1, ..., 1).
  266. * If there is only one row, then G = L_1.
  267. *
  268. * If there is more than one row left, we need to compute the intersection
  269. * of the lattices. That is, we need to compute an L such that
  270. *
  271. * L = L_i L_i' for all i
  272. *
  273. * with L_i' some integer matrices. Let A be constructed as follows
  274. *
  275. * A = [ L_1^{-T} L_2^{-T} ... L_k^{-T} ]
  276. *
  277. * and computed the Hermite Normal Form of A = [ H 0 ] U
  278. * Then,
  279. *
  280. * L_i^{-T} = H U_{1,i}
  281. *
  282. * or
  283. *
  284. * H^{-T} = L_i U_{1,i}^T
  285. *
  286. * In other words G = L = H^{-T}.
  287. * To ensure that G is lower triangular, we compute and use its Hermite
  288. * normal form.
  289. *
  290. * The affine transformation matrix returned is then
  291. *
  292. * [ 1 0 ]
  293. * [ y_0 G ]
  294. *
  295. * as any y = y_0 + G y' with y' integer is a solution to the original
  296. * modulo constraints.
  297. */
  298. __isl_give isl_mat *isl_mat_parameter_compression(__isl_take isl_mat *B,
  299. __isl_take isl_vec *d)
  300. {
  301. int i;
  302. struct isl_mat *cst = NULL;
  303. struct isl_mat *T = NULL;
  304. isl_int D;
  305. if (!B || !d)
  306. goto error;
  307. isl_assert(B->ctx, B->n_row == d->size, goto error);
  308. cst = particular_solution(B, d);
  309. if (!cst)
  310. goto error;
  311. if (cst->n_col == 0) {
  312. T = isl_mat_alloc(B->ctx, B->n_col, 0);
  313. isl_mat_free(cst);
  314. isl_mat_free(B);
  315. isl_vec_free(d);
  316. return T;
  317. }
  318. isl_int_init(D);
  319. /* Replace a*g*row = 0 mod g*m by row = 0 mod m */
  320. for (i = 0; i < B->n_row; ++i) {
  321. isl_seq_gcd(B->row[i] + 1, B->n_col - 1, &D);
  322. if (isl_int_is_one(D))
  323. continue;
  324. if (isl_int_is_zero(D)) {
  325. B = isl_mat_drop_rows(B, i, 1);
  326. d = isl_vec_cow(d);
  327. if (!B || !d)
  328. goto error2;
  329. isl_seq_cpy(d->block.data+i, d->block.data+i+1,
  330. d->size - (i+1));
  331. d->size--;
  332. i--;
  333. continue;
  334. }
  335. B = isl_mat_cow(B);
  336. if (!B)
  337. goto error2;
  338. isl_seq_scale_down(B->row[i] + 1, B->row[i] + 1, D, B->n_col-1);
  339. isl_int_gcd(D, D, d->block.data[i]);
  340. d = isl_vec_cow(d);
  341. if (!d)
  342. goto error2;
  343. isl_int_divexact(d->block.data[i], d->block.data[i], D);
  344. }
  345. isl_int_clear(D);
  346. if (B->n_row == 0)
  347. T = isl_mat_identity(B->ctx, B->n_col);
  348. else if (B->n_row == 1)
  349. T = parameter_compression_1(B, d);
  350. else
  351. T = parameter_compression_multi(B, d);
  352. T = isl_mat_left_hermite(T, 0, NULL, NULL);
  353. if (!T)
  354. goto error;
  355. isl_mat_sub_copy(T->ctx, T->row + 1, cst->row, cst->n_row, 0, 0, 1);
  356. isl_mat_free(cst);
  357. isl_mat_free(B);
  358. isl_vec_free(d);
  359. return T;
  360. error2:
  361. isl_int_clear(D);
  362. error:
  363. isl_mat_free(cst);
  364. isl_mat_free(B);
  365. isl_vec_free(d);
  366. return NULL;
  367. }
  368. /* Given a set of equalities
  369. *
  370. * B(y) + A x = 0 (*)
  371. *
  372. * compute and return an affine transformation T,
  373. *
  374. * y = T y'
  375. *
  376. * that bijectively maps the integer vectors y' to integer
  377. * vectors y that satisfy the modulo constraints for some value of x.
  378. *
  379. * Let [H 0] be the Hermite Normal Form of A, i.e.,
  380. *
  381. * A = [H 0] Q
  382. *
  383. * Then y is a solution of (*) iff
  384. *
  385. * H^-1 B(y) (= - [I 0] Q x)
  386. *
  387. * is an integer vector. Let d be the common denominator of H^-1.
  388. * We impose
  389. *
  390. * d H^-1 B(y) = 0 mod d
  391. *
  392. * and compute the solution using isl_mat_parameter_compression.
  393. */
  394. __isl_give isl_mat *isl_mat_parameter_compression_ext(__isl_take isl_mat *B,
  395. __isl_take isl_mat *A)
  396. {
  397. isl_ctx *ctx;
  398. isl_vec *d;
  399. int n_row, n_col;
  400. if (!A)
  401. return isl_mat_free(B);
  402. ctx = isl_mat_get_ctx(A);
  403. n_row = A->n_row;
  404. n_col = A->n_col;
  405. A = isl_mat_left_hermite(A, 0, NULL, NULL);
  406. A = isl_mat_drop_cols(A, n_row, n_col - n_row);
  407. A = isl_mat_lin_to_aff(A);
  408. A = isl_mat_right_inverse(A);
  409. d = isl_vec_alloc(ctx, n_row);
  410. if (A)
  411. d = isl_vec_set(d, A->row[0][0]);
  412. A = isl_mat_drop_rows(A, 0, 1);
  413. A = isl_mat_drop_cols(A, 0, 1);
  414. B = isl_mat_product(A, B);
  415. return isl_mat_parameter_compression(B, d);
  416. }
  417. /* Return a compression matrix that indicates that there are no solutions
  418. * to the original constraints. In particular, return a zero-column
  419. * matrix with 1 + dim rows. If "T2" is not NULL, then assign *T2
  420. * the inverse of this matrix. *T2 may already have been assigned
  421. * matrix, so free it first.
  422. * "free1", "free2" and "free3" are temporary matrices that are
  423. * not useful when an empty compression is returned. They are
  424. * simply freed.
  425. */
  426. static __isl_give isl_mat *empty_compression(isl_ctx *ctx, unsigned dim,
  427. __isl_give isl_mat **T2, __isl_take isl_mat *free1,
  428. __isl_take isl_mat *free2, __isl_take isl_mat *free3)
  429. {
  430. isl_mat_free(free1);
  431. isl_mat_free(free2);
  432. isl_mat_free(free3);
  433. if (T2) {
  434. isl_mat_free(*T2);
  435. *T2 = isl_mat_alloc(ctx, 0, 1 + dim);
  436. }
  437. return isl_mat_alloc(ctx, 1 + dim, 0);
  438. }
  439. /* Given a matrix that maps a (possibly) parametric domain to
  440. * a parametric domain, add in rows that map the "nparam" parameters onto
  441. * themselves.
  442. */
  443. static __isl_give isl_mat *insert_parameter_rows(__isl_take isl_mat *mat,
  444. unsigned nparam)
  445. {
  446. int i;
  447. if (nparam == 0)
  448. return mat;
  449. if (!mat)
  450. return NULL;
  451. mat = isl_mat_insert_rows(mat, 1, nparam);
  452. if (!mat)
  453. return NULL;
  454. for (i = 0; i < nparam; ++i) {
  455. isl_seq_clr(mat->row[1 + i], mat->n_col);
  456. isl_int_set(mat->row[1 + i][1 + i], mat->row[0][0]);
  457. }
  458. return mat;
  459. }
  460. /* Given a set of equalities
  461. *
  462. * -C(y) + M x = 0
  463. *
  464. * this function computes a unimodular transformation from a lower-dimensional
  465. * space to the original space that bijectively maps the integer points x'
  466. * in the lower-dimensional space to the integer points x in the original
  467. * space that satisfy the equalities.
  468. *
  469. * The input is given as a matrix B = [ -C M ] and the output is a
  470. * matrix that maps [1 x'] to [1 x].
  471. * The number of equality constraints in B is assumed to be smaller than
  472. * or equal to the number of variables x.
  473. * "first" is the position of the first x variable.
  474. * The preceding variables are considered to be y-variables.
  475. * If T2 is not NULL, then *T2 is set to a matrix mapping [1 x] to [1 x'].
  476. *
  477. * First compute the (left) Hermite normal form of M,
  478. *
  479. * M [U1 U2] = M U = H = [H1 0]
  480. * or
  481. * M = H Q = [H1 0] [Q1]
  482. * [Q2]
  483. *
  484. * with U, Q unimodular, Q = U^{-1} (and H lower triangular).
  485. * Define the transformed variables as
  486. *
  487. * x = [U1 U2] [ x1' ] = [U1 U2] [Q1] x
  488. * [ x2' ] [Q2]
  489. *
  490. * The equalities then become
  491. *
  492. * -C(y) + H1 x1' = 0 or x1' = H1^{-1} C(y) = C'(y)
  493. *
  494. * If the denominator of the constant term does not divide the
  495. * the common denominator of the coefficients of y, then every
  496. * integer point is mapped to a non-integer point and then the original set
  497. * has no integer solutions (since the x' are a unimodular transformation
  498. * of the x). In this case, a zero-column matrix is returned.
  499. * Otherwise, the transformation is given by
  500. *
  501. * x = U1 H1^{-1} C(y) + U2 x2'
  502. *
  503. * The inverse transformation is simply
  504. *
  505. * x2' = Q2 x
  506. */
  507. __isl_give isl_mat *isl_mat_final_variable_compression(__isl_take isl_mat *B,
  508. int first, __isl_give isl_mat **T2)
  509. {
  510. int i, n;
  511. isl_ctx *ctx;
  512. isl_mat *H = NULL, *C, *H1, *U = NULL, *U1, *U2;
  513. unsigned dim;
  514. if (T2)
  515. *T2 = NULL;
  516. if (!B)
  517. goto error;
  518. ctx = isl_mat_get_ctx(B);
  519. dim = B->n_col - 1;
  520. n = dim - first;
  521. if (n < B->n_row)
  522. isl_die(ctx, isl_error_invalid, "too many equality constraints",
  523. goto error);
  524. H = isl_mat_sub_alloc(B, 0, B->n_row, 1 + first, n);
  525. H = isl_mat_left_hermite(H, 0, &U, T2);
  526. if (!H || !U || (T2 && !*T2))
  527. goto error;
  528. if (T2) {
  529. *T2 = isl_mat_drop_rows(*T2, 0, B->n_row);
  530. *T2 = isl_mat_diagonal(isl_mat_identity(ctx, 1 + first), *T2);
  531. if (!*T2)
  532. goto error;
  533. }
  534. C = isl_mat_alloc(ctx, 1 + B->n_row, 1 + first);
  535. if (!C)
  536. goto error;
  537. isl_int_set_si(C->row[0][0], 1);
  538. isl_seq_clr(C->row[0] + 1, first);
  539. isl_mat_sub_neg(ctx, C->row + 1, B->row, B->n_row, 0, 0, 1 + first);
  540. H1 = isl_mat_sub_alloc(H, 0, H->n_row, 0, H->n_row);
  541. H1 = isl_mat_lin_to_aff(H1);
  542. C = isl_mat_inverse_product(H1, C);
  543. if (!C)
  544. goto error;
  545. isl_mat_free(H);
  546. if (!isl_int_is_one(C->row[0][0])) {
  547. isl_int g;
  548. isl_int_init(g);
  549. for (i = 0; i < B->n_row; ++i) {
  550. isl_seq_gcd(C->row[1 + i] + 1, first, &g);
  551. isl_int_gcd(g, g, C->row[0][0]);
  552. if (!isl_int_is_divisible_by(C->row[1 + i][0], g))
  553. break;
  554. }
  555. isl_int_clear(g);
  556. if (i < B->n_row)
  557. return empty_compression(ctx, dim, T2, B, C, U);
  558. C = isl_mat_normalize(C);
  559. }
  560. U1 = isl_mat_sub_alloc(U, 0, U->n_row, 0, B->n_row);
  561. U1 = isl_mat_lin_to_aff(U1);
  562. U2 = isl_mat_sub_alloc(U, 0, U->n_row, B->n_row, U->n_row - B->n_row);
  563. U2 = isl_mat_lin_to_aff(U2);
  564. isl_mat_free(U);
  565. C = isl_mat_product(U1, C);
  566. C = isl_mat_aff_direct_sum(C, U2);
  567. C = insert_parameter_rows(C, first);
  568. isl_mat_free(B);
  569. return C;
  570. error:
  571. isl_mat_free(B);
  572. isl_mat_free(H);
  573. isl_mat_free(U);
  574. if (T2) {
  575. isl_mat_free(*T2);
  576. *T2 = NULL;
  577. }
  578. return NULL;
  579. }
  580. /* Given a set of equalities
  581. *
  582. * M x - c = 0
  583. *
  584. * this function computes a unimodular transformation from a lower-dimensional
  585. * space to the original space that bijectively maps the integer points x'
  586. * in the lower-dimensional space to the integer points x in the original
  587. * space that satisfy the equalities.
  588. *
  589. * The input is given as a matrix B = [ -c M ] and the output is a
  590. * matrix that maps [1 x'] to [1 x].
  591. * The number of equality constraints in B is assumed to be smaller than
  592. * or equal to the number of variables x.
  593. * If T2 is not NULL, then *T2 is set to a matrix mapping [1 x] to [1 x'].
  594. */
  595. __isl_give isl_mat *isl_mat_variable_compression(__isl_take isl_mat *B,
  596. __isl_give isl_mat **T2)
  597. {
  598. return isl_mat_final_variable_compression(B, 0, T2);
  599. }
  600. /* Return "bset" and set *T and *T2 to the identity transformation
  601. * on "bset" (provided T and T2 are not NULL).
  602. */
  603. static __isl_give isl_basic_set *return_with_identity(
  604. __isl_take isl_basic_set *bset, __isl_give isl_mat **T,
  605. __isl_give isl_mat **T2)
  606. {
  607. isl_size dim;
  608. isl_mat *id;
  609. dim = isl_basic_set_dim(bset, isl_dim_set);
  610. if (dim < 0)
  611. return isl_basic_set_free(bset);
  612. if (!T && !T2)
  613. return bset;
  614. id = isl_mat_identity(isl_basic_map_get_ctx(bset), 1 + dim);
  615. if (T)
  616. *T = isl_mat_copy(id);
  617. if (T2)
  618. *T2 = isl_mat_copy(id);
  619. isl_mat_free(id);
  620. return bset;
  621. }
  622. /* Use the n equalities of bset to unimodularly transform the
  623. * variables x such that n transformed variables x1' have a constant value
  624. * and rewrite the constraints of bset in terms of the remaining
  625. * transformed variables x2'. The matrix pointed to by T maps
  626. * the new variables x2' back to the original variables x, while T2
  627. * maps the original variables to the new variables.
  628. */
  629. static __isl_give isl_basic_set *compress_variables(
  630. __isl_take isl_basic_set *bset,
  631. __isl_give isl_mat **T, __isl_give isl_mat **T2)
  632. {
  633. struct isl_mat *B, *TC;
  634. isl_size dim;
  635. if (T)
  636. *T = NULL;
  637. if (T2)
  638. *T2 = NULL;
  639. if (isl_basic_set_check_no_params(bset) < 0 ||
  640. isl_basic_set_check_no_locals(bset) < 0)
  641. return isl_basic_set_free(bset);
  642. dim = isl_basic_set_dim(bset, isl_dim_set);
  643. if (dim < 0)
  644. return isl_basic_set_free(bset);
  645. isl_assert(bset->ctx, bset->n_eq <= dim, goto error);
  646. if (bset->n_eq == 0)
  647. return return_with_identity(bset, T, T2);
  648. B = isl_mat_sub_alloc6(bset->ctx, bset->eq, 0, bset->n_eq, 0, 1 + dim);
  649. TC = isl_mat_variable_compression(B, T2);
  650. if (!TC)
  651. goto error;
  652. if (TC->n_col == 0) {
  653. isl_mat_free(TC);
  654. if (T2) {
  655. isl_mat_free(*T2);
  656. *T2 = NULL;
  657. }
  658. bset = isl_basic_set_set_to_empty(bset);
  659. return return_with_identity(bset, T, T2);
  660. }
  661. bset = isl_basic_set_preimage(bset, T ? isl_mat_copy(TC) : TC);
  662. if (T)
  663. *T = TC;
  664. return bset;
  665. error:
  666. isl_basic_set_free(bset);
  667. return NULL;
  668. }
  669. __isl_give isl_basic_set *isl_basic_set_remove_equalities(
  670. __isl_take isl_basic_set *bset, __isl_give isl_mat **T,
  671. __isl_give isl_mat **T2)
  672. {
  673. if (T)
  674. *T = NULL;
  675. if (T2)
  676. *T2 = NULL;
  677. if (isl_basic_set_check_no_params(bset) < 0)
  678. return isl_basic_set_free(bset);
  679. bset = isl_basic_set_gauss(bset, NULL);
  680. if (ISL_F_ISSET(bset, ISL_BASIC_SET_EMPTY))
  681. return return_with_identity(bset, T, T2);
  682. bset = compress_variables(bset, T, T2);
  683. return bset;
  684. }
  685. /* Check if dimension dim belongs to a residue class
  686. * i_dim \equiv r mod m
  687. * with m != 1 and if so return m in *modulo and r in *residue.
  688. * As a special case, when i_dim has a fixed value v, then
  689. * *modulo is set to 0 and *residue to v.
  690. *
  691. * If i_dim does not belong to such a residue class, then *modulo
  692. * is set to 1 and *residue is set to 0.
  693. */
  694. isl_stat isl_basic_set_dim_residue_class(__isl_keep isl_basic_set *bset,
  695. int pos, isl_int *modulo, isl_int *residue)
  696. {
  697. isl_bool fixed;
  698. struct isl_ctx *ctx;
  699. struct isl_mat *H = NULL, *U = NULL, *C, *H1, *U1;
  700. isl_size total;
  701. isl_size nparam;
  702. if (!bset || !modulo || !residue)
  703. return isl_stat_error;
  704. fixed = isl_basic_set_plain_dim_is_fixed(bset, pos, residue);
  705. if (fixed < 0)
  706. return isl_stat_error;
  707. if (fixed) {
  708. isl_int_set_si(*modulo, 0);
  709. return isl_stat_ok;
  710. }
  711. ctx = isl_basic_set_get_ctx(bset);
  712. total = isl_basic_set_dim(bset, isl_dim_all);
  713. nparam = isl_basic_set_dim(bset, isl_dim_param);
  714. if (total < 0 || nparam < 0)
  715. return isl_stat_error;
  716. H = isl_mat_sub_alloc6(ctx, bset->eq, 0, bset->n_eq, 1, total);
  717. H = isl_mat_left_hermite(H, 0, &U, NULL);
  718. if (!H)
  719. return isl_stat_error;
  720. isl_seq_gcd(U->row[nparam + pos]+bset->n_eq,
  721. total-bset->n_eq, modulo);
  722. if (isl_int_is_zero(*modulo))
  723. isl_int_set_si(*modulo, 1);
  724. if (isl_int_is_one(*modulo)) {
  725. isl_int_set_si(*residue, 0);
  726. isl_mat_free(H);
  727. isl_mat_free(U);
  728. return isl_stat_ok;
  729. }
  730. C = isl_mat_alloc(ctx, 1 + bset->n_eq, 1);
  731. if (!C)
  732. goto error;
  733. isl_int_set_si(C->row[0][0], 1);
  734. isl_mat_sub_neg(ctx, C->row + 1, bset->eq, bset->n_eq, 0, 0, 1);
  735. H1 = isl_mat_sub_alloc(H, 0, H->n_row, 0, H->n_row);
  736. H1 = isl_mat_lin_to_aff(H1);
  737. C = isl_mat_inverse_product(H1, C);
  738. isl_mat_free(H);
  739. U1 = isl_mat_sub_alloc(U, nparam+pos, 1, 0, bset->n_eq);
  740. U1 = isl_mat_lin_to_aff(U1);
  741. isl_mat_free(U);
  742. C = isl_mat_product(U1, C);
  743. if (!C)
  744. return isl_stat_error;
  745. if (!isl_int_is_divisible_by(C->row[1][0], C->row[0][0])) {
  746. bset = isl_basic_set_copy(bset);
  747. bset = isl_basic_set_set_to_empty(bset);
  748. isl_basic_set_free(bset);
  749. isl_int_set_si(*modulo, 1);
  750. isl_int_set_si(*residue, 0);
  751. return isl_stat_ok;
  752. }
  753. isl_int_divexact(*residue, C->row[1][0], C->row[0][0]);
  754. isl_int_fdiv_r(*residue, *residue, *modulo);
  755. isl_mat_free(C);
  756. return isl_stat_ok;
  757. error:
  758. isl_mat_free(H);
  759. isl_mat_free(U);
  760. return isl_stat_error;
  761. }
  762. /* Check if dimension dim belongs to a residue class
  763. * i_dim \equiv r mod m
  764. * with m != 1 and if so return m in *modulo and r in *residue.
  765. * As a special case, when i_dim has a fixed value v, then
  766. * *modulo is set to 0 and *residue to v.
  767. *
  768. * If i_dim does not belong to such a residue class, then *modulo
  769. * is set to 1 and *residue is set to 0.
  770. */
  771. isl_stat isl_set_dim_residue_class(__isl_keep isl_set *set,
  772. int pos, isl_int *modulo, isl_int *residue)
  773. {
  774. isl_int m;
  775. isl_int r;
  776. int i;
  777. if (!set || !modulo || !residue)
  778. return isl_stat_error;
  779. if (set->n == 0) {
  780. isl_int_set_si(*modulo, 0);
  781. isl_int_set_si(*residue, 0);
  782. return isl_stat_ok;
  783. }
  784. if (isl_basic_set_dim_residue_class(set->p[0], pos, modulo, residue)<0)
  785. return isl_stat_error;
  786. if (set->n == 1)
  787. return isl_stat_ok;
  788. if (isl_int_is_one(*modulo))
  789. return isl_stat_ok;
  790. isl_int_init(m);
  791. isl_int_init(r);
  792. for (i = 1; i < set->n; ++i) {
  793. if (isl_basic_set_dim_residue_class(set->p[i], pos, &m, &r) < 0)
  794. goto error;
  795. isl_int_gcd(*modulo, *modulo, m);
  796. isl_int_sub(m, *residue, r);
  797. isl_int_gcd(*modulo, *modulo, m);
  798. if (!isl_int_is_zero(*modulo))
  799. isl_int_fdiv_r(*residue, *residue, *modulo);
  800. if (isl_int_is_one(*modulo))
  801. break;
  802. }
  803. isl_int_clear(m);
  804. isl_int_clear(r);
  805. return isl_stat_ok;
  806. error:
  807. isl_int_clear(m);
  808. isl_int_clear(r);
  809. return isl_stat_error;
  810. }
  811. /* Check if dimension "dim" belongs to a residue class
  812. * i_dim \equiv r mod m
  813. * with m != 1 and if so return m in *modulo and r in *residue.
  814. * As a special case, when i_dim has a fixed value v, then
  815. * *modulo is set to 0 and *residue to v.
  816. *
  817. * If i_dim does not belong to such a residue class, then *modulo
  818. * is set to 1 and *residue is set to 0.
  819. */
  820. isl_stat isl_set_dim_residue_class_val(__isl_keep isl_set *set,
  821. int pos, __isl_give isl_val **modulo, __isl_give isl_val **residue)
  822. {
  823. *modulo = NULL;
  824. *residue = NULL;
  825. if (!set)
  826. return isl_stat_error;
  827. *modulo = isl_val_alloc(isl_set_get_ctx(set));
  828. *residue = isl_val_alloc(isl_set_get_ctx(set));
  829. if (!*modulo || !*residue)
  830. goto error;
  831. if (isl_set_dim_residue_class(set, pos,
  832. &(*modulo)->n, &(*residue)->n) < 0)
  833. goto error;
  834. isl_int_set_si((*modulo)->d, 1);
  835. isl_int_set_si((*residue)->d, 1);
  836. return isl_stat_ok;
  837. error:
  838. isl_val_free(*modulo);
  839. isl_val_free(*residue);
  840. return isl_stat_error;
  841. }