00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027 #include <stdlib.h>
00028 #include<polylib/polylib.h>
00029 #include <polylib/matrix_addon.h>
00030
00031
00032 Matrix * constraintsView(Polyhedron * P) {
00033 Matrix * view = (Matrix *)malloc(sizeof(Matrix));
00034 view->NbRows = P->NbConstraints;
00035 view->NbColumns = P->Dimension+2;
00036 view->p = P->Constraint;
00037 return view;
00038 }
00039
00040
00041 void constraintsView_Free(Matrix * M) {
00042 free(M);
00043 }
00044
00045
00046
00047
00048
00049
00050 void split_constraints(Matrix const * M, Matrix ** Eqs, Matrix **Ineqs) {
00051 unsigned int i, j, k_eq, k_ineq, nb_eqs=0;
00052
00053
00054 for (i=0; i< M->NbRows; i++)
00055 if (value_zero_p(M->p[i][0])) nb_eqs++;
00056
00057
00058 (*Eqs) = Matrix_Alloc(nb_eqs, M->NbColumns);
00059 (*Ineqs) = Matrix_Alloc(M->NbRows-nb_eqs, M->NbColumns);
00060
00061 k_eq = k_ineq = 0;
00062 for(i=0; i< M->NbRows; i++) {
00063 if (value_zero_p(M->p[i][0]))
00064 {
00065 for(j=0; j< M->NbColumns; j++)
00066 value_assign((*Eqs)->p[k_eq][j], M->p[i][j]);
00067 k_eq++;
00068 }
00069 else
00070 {
00071 for(j=0; j< M->NbColumns; j++)
00072 value_assign((*Ineqs)->p[k_ineq][j], M->p[i][j]);
00073 k_ineq++;
00074 }
00075 }
00076 }
00077
00078
00079
00080 Matrix * Identity_Matrix(unsigned int dim) {
00081 Matrix * ret = Matrix_Alloc(dim, dim);
00082 unsigned int i,j;
00083 for (i=0; i< dim; i++) {
00084 for (j=0; j< dim; j++) {
00085 if (i==j)
00086 { value_set_si(ret->p[i][j], 1); }
00087 else value_set_si(ret->p[i][j], 0);
00088 }
00089 }
00090 return ret;
00091 }
00092
00093
00094
00095
00096
00097
00098
00099 void Matrix_identity(unsigned int dim, Matrix ** I) {
00100 int i,j;
00101 if (*I==NULL) {
00102 (*I) = Identity_Matrix(dim);
00103 }
00104 else {
00105 assert((*I)->NbRows>=dim && (*I)->NbColumns>=dim);
00106 for (i=0; i< dim; i++) {
00107 for (j=0; j< dim; j++) {
00108 if (i==j) {
00109 value_set_si((*I)->p[i][j], 1);
00110 }
00111 else {
00112 value_set_si((*I)->p[i][j], 0);
00113 }
00114 }
00115 }
00116 }
00117 }
00118
00119
00120
00121
00122
00123 void mtransformation_inverse(Matrix * transf, Matrix ** inverse, Value * g) {
00124 Value factor;
00125 unsigned int i,j;
00126 Matrix *tmp, *inv;
00127
00128 value_init(*g);
00129 value_set_si(*g,1);
00130
00131
00132 tmp = Matrix_Copy(transf);
00133 inv = Matrix_Alloc(transf->NbRows, transf->NbColumns+1);
00134 MatInverse(tmp, inv);
00135 Matrix_Free(tmp);
00136
00137
00138 (*inverse) = Matrix_Alloc(transf->NbRows, transf->NbRows);
00139 for (i=0; i< inv->NbRows; i++)
00140 value_lcm(*g, *g, inv->p[i][inv->NbColumns-1]);
00141 for (i=0; i< inv->NbRows; i++) {
00142 value_division(factor, *g, inv->p[i][inv->NbColumns-1]);
00143 for (j=0; j< (*inverse)->NbColumns; j++)
00144 value_multiply((*inverse)->p[i][j], inv->p[i][j], factor);
00145 }
00146
00147
00148 value_clear(factor);
00149 Matrix_Free(inv);
00150 }
00151
00152
00153
00154
00155 Matrix * mtransformation_expand_left_to_dim(Matrix * M, int new_dim) {
00156 Matrix * ret = Identity_Matrix(new_dim);
00157 int offset = new_dim-M->NbRows;
00158 unsigned int i,j;
00159
00160 assert(new_dim>=M->NbColumns);
00161 assert(M->NbRows==M->NbColumns);
00162
00163 for (i=0; i< M->NbRows; i++)
00164 for (j=0; j< M->NbRows; j++)
00165 value_assign(ret->p[offset+i][offset+j], M->p[i][j]);
00166 return ret;
00167 }
00168
00169
00170
00171
00172 void mpolyhedron_simplify(Matrix * polyh) {
00173 int i, j;
00174 Value cur_gcd;
00175 value_init(cur_gcd);
00176 for (i=0; i< polyh->NbRows; i++) {
00177 Vector_Gcd(polyh->p[i]+1, polyh->NbColumns-1, &cur_gcd);
00178 printf(" gcd[%d] = ", i);
00179 value_print(stdout, VALUE_FMT, cur_gcd);printf("\n");
00180 Vector_AntiScale(polyh->p[i]+1, polyh->p[i]+1, cur_gcd, polyh->NbColumns-1);
00181 }
00182 value_clear(cur_gcd);
00183 }
00184
00185
00186
00187
00188
00189
00190 void mpolyhedron_inflate(Matrix * polyh, unsigned int nb_parms) {
00191 unsigned int i,j;
00192 unsigned nb_vars = polyh->NbColumns-nb_parms-2;
00193 Value infl;
00194 value_init(infl);
00195
00196 for (i=0; i< polyh->NbRows; i++) {
00197 value_set_si(infl, 0);
00198 for (j=0; j< nb_vars; j++) {
00199 if (value_neg_p(polyh->p[i][1+j]))
00200 value_addto(infl, infl, polyh->p[i][1+j]);
00201 }
00202
00203 value_subtract(polyh->p[i][polyh->NbColumns-1],
00204 polyh->p[i][polyh->NbColumns-1], infl);
00205 }
00206 value_clear(infl);
00207 }
00208
00209
00210
00211
00212
00213 void mpolyhedron_deflate(Matrix * polyh, unsigned int nb_parms) {
00214 unsigned int i,j;
00215 unsigned nb_vars = polyh->NbColumns-nb_parms-2;
00216 Value defl;
00217 value_init(defl);
00218
00219 for (i=0; i< polyh->NbRows; i++) {
00220 value_set_si(defl, 0);
00221 for (j=0; j< nb_vars; j++) {
00222 if (value_pos_p(polyh->p[i][1+j]))
00223 value_addto(defl, defl, polyh->p[i][1+j]);
00224 }
00225
00226 value_subtract(polyh->p[i][polyh->NbColumns-1],
00227 polyh->p[i][polyh->NbColumns-1], defl);
00228 }
00229 value_clear(defl);
00230 }
00231
00232
00233
00234
00235
00236
00237
00238
00239
00240
00241 void eliminate_var_with_constr(Matrix * Eliminator,
00242 unsigned int eliminator_row, Matrix * Victim,
00243 unsigned int victim_row,
00244 unsigned int var_to_elim) {
00245 Value cur_lcm, mul_a, mul_b;
00246 Value tmp, tmp2;
00247 int k;
00248
00249 value_init(cur_lcm);
00250 value_init(mul_a);
00251 value_init(mul_b);
00252 value_init(tmp);
00253 value_init(tmp2);
00254
00255 if (value_notzero_p(Victim->p[victim_row][var_to_elim+1])) {
00256 value_lcm(cur_lcm, Eliminator->p[eliminator_row][var_to_elim+1],
00257 Victim->p[victim_row][var_to_elim+1]);
00258
00259 value_division(mul_a, cur_lcm,
00260 Eliminator->p[eliminator_row][var_to_elim+1]);
00261 value_division(mul_b, cur_lcm,
00262 Victim->p[victim_row][var_to_elim+1]);
00263
00264 if (value_pos_p(mul_b)) {
00265 value_oppose(mul_a, mul_a);
00266 }
00267 else {
00268 value_oppose(mul_b, mul_b);
00269 }
00270 value_clear(cur_lcm);
00271
00272 for (k=1; k<Victim->NbColumns; k++) {
00273 value_multiply(tmp, Eliminator->p[eliminator_row][k], mul_a);
00274 value_multiply(tmp2, Victim->p[victim_row][k], mul_b);
00275 value_addto(Victim->p[victim_row][k], tmp, tmp2);
00276 }
00277 }
00278 value_clear(mul_a);
00279 value_clear(mul_b);
00280 value_clear(tmp);
00281 value_clear(tmp2);
00282 }
00283
00284
00285
00286
00287
00288
00289
00290
00291
00292
00293 void mpolyhedron_compress_last_vars(Matrix * M, Matrix * compression) {
00294 unsigned int i, j, k;
00295 unsigned int offset = M->NbColumns - compression->NbRows;
00296
00297
00298 Matrix * M_tmp = Matrix_Alloc(1, M->NbColumns);
00299 assert(compression->NbRows==compression->NbColumns);
00300
00301
00302 for(i=0; i< M->NbRows; i++) {
00303 for (j=0; j< compression->NbRows; j++) {
00304 value_set_si(M_tmp->p[0][j], 0);
00305 for (k=0; k< compression->NbRows; k++) {
00306 value_addmul(M_tmp->p[0][j], M->p[i][k+offset],compression->p[k][j]);
00307 }
00308 }
00309 for (j=0; j< compression->NbRows; j++)
00310 value_assign(M->p[i][j+offset], M_tmp->p[0][j]);
00311 }
00312 Matrix_Free(M_tmp);
00313 }
00314
00315
00316
00317
00318
00319
00320
00321 unsigned int mpolyhedron_eliminate_first_variables(Matrix * Eqs,
00322 Matrix *Ineqs) {
00323 unsigned int i, j, k;
00324
00325 for (i=0; i< Eqs->NbRows; i++) {
00326
00327 for (j=0; j<Eqs->NbRows && (Eqs->p[j][i+1]==0 ||
00328 ( !value_cmp_si(Eqs->p[j][0],2) ));
00329 j++);
00330
00331
00332 if (j==Eqs->NbRows) return 0;
00333
00334
00335 for (k=j+1; k<Eqs->NbRows; k++)
00336 eliminate_var_with_constr(Eqs, j, Eqs, k, i);
00337 for (k=0; k< Ineqs->NbRows; k++)
00338 eliminate_var_with_constr(Eqs, j, Ineqs, k, i);
00339
00340 value_set_si(Eqs->p[j][0],2);
00341 }
00342
00343 for (i=0; i< Eqs->NbRows; i++) value_set_si(Eqs->p[i][0],0);
00344 return 1;
00345 }
00346
00347
00348
00349
00350
00351
00352
00353
00354
00355
00356
00357 void Matrix_subMatrix(Matrix * M, unsigned int sr, unsigned int sc,
00358 unsigned int er, unsigned int ec, Matrix ** sub) {
00359 int i;
00360 int nbR = er-sr;
00361 int nbC = ec-sc;
00362 assert (er<=M->NbRows && ec<=M->NbColumns);
00363 if ((*sub)==NULL) {
00364 (*sub) = Matrix_Alloc(nbR, nbC);
00365 }
00366 if (nbR==0 || nbC==0) return;
00367 for (i=0; i< nbR; i++) {
00368 Vector_Copy(&(M->p[i+sr][sc]), (*sub)->p[i], nbC);
00369 }
00370 }
00371
00372
00373
00374
00375
00376
00377 void Matrix_clone(Matrix * M, Matrix ** Cl) {
00378 Matrix_subMatrix(M, 0,0, M->NbRows, M->NbColumns, Cl);
00379 }
00380
00381
00382
00383
00384
00385
00386
00387
00388
00389
00390
00391
00392
00393
00394 void Matrix_copySubMatrix(Matrix *M1,
00395 unsigned int sr1, unsigned int sc1,
00396 unsigned int nbR, unsigned int nbC,
00397 Matrix * M2,
00398 unsigned int sr2, unsigned int sc2) {
00399 int i;
00400 for (i=0; i< nbR; i++) {
00401 Vector_Copy(&(M1->p[i+sr1][sc1]), &(M2->p[i+sr2][sc2]), nbC);
00402 }
00403 }
00404
00405
00406
00407
00408
00409 void Matrix_oppose(Matrix * M) {
00410 int i,j;
00411 for (i=0; i<M->NbRows; i++) {
00412 for (j=0; j< M->NbColumns; j++) {
00413 value_oppose(M->p[i][j], M->p[i][j]);
00414 }
00415 }
00416 }