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
00028
00029
00030
00031
00032
00033
00034
00035
00036
00037
00038
00039
00040
00041
00042
00043 #include <stdio.h>
00044 #include <stdlib.h>
00045 #include <string.h>
00046 #include <assert.h>
00047 #ifdef DEBUGPP
00048 #include <time.h>
00049 #endif
00050
00051 #include <polylib/polylib.h>
00052
00053 static void traite_m_face(Polyhedron *, unsigned int *, unsigned int *);
00054 static void scan_m_face(int,int,Polyhedron *,unsigned int *);
00055
00056
00057
00058
00059
00060
00061
00062 Polyhedron *PDomainIntersection(Polyhedron *Pol1,Polyhedron *Pol2,unsigned NbMaxRays) {
00063
00064 Polyhedron *p1, *p2, *p3, *d;
00065
00066 if (!Pol1 || !Pol2) return (Polyhedron*) 0;
00067 if((Pol1->Dimension != Pol2->Dimension) || (Pol1->NbEq != Pol2->NbEq)) {
00068 fprintf(stderr,
00069 "? PDomainIntersection: operation on different dimensions\n");
00070 return (Polyhedron*) 0;
00071 }
00072
00073 POL_ENSURE_FACETS(Pol1);
00074 POL_ENSURE_VERTICES(Pol1);
00075 POL_ENSURE_FACETS(Pol2);
00076 POL_ENSURE_VERTICES(Pol2);
00077
00078 d = (Polyhedron *)0;
00079 for (p1=Pol1; p1; p1=p1->next) {
00080 for (p2=Pol2; p2; p2=p2->next) {
00081 p3 = AddConstraints(p2->Constraint[0],
00082 p2->NbConstraints,p1,NbMaxRays);
00083 if (!p3) continue;
00084
00085
00086 if (p3->NbEq!=Pol1->NbEq)
00087 Polyhedron_Free(p3) ;
00088
00089
00090 else
00091 d = AddPolyToDomain(p3,d);
00092 }
00093 }
00094 return d;
00095 }
00096
00097
00098
00099
00100
00101
00102
00103 Polyhedron *PDomainDifference(Polyhedron *Pol1,Polyhedron *Pol2,unsigned NbMaxRays) {
00104
00105 Polyhedron *p1, *p2, *p3, *d;
00106 int i;
00107
00108 if (!Pol1 || !Pol2)
00109 return (Polyhedron*) 0;
00110 if((Pol1->Dimension != Pol2->Dimension) || (Pol1->NbEq != Pol2->NbEq)) {
00111 fprintf(stderr,
00112 "? PDomainDifference: operation on different dimensions\n");
00113 return (Polyhedron*) 0;
00114 }
00115
00116 POL_ENSURE_FACETS(Pol1);
00117 POL_ENSURE_VERTICES(Pol1);
00118 POL_ENSURE_FACETS(Pol2);
00119 POL_ENSURE_VERTICES(Pol2);
00120
00121 d = (Polyhedron *)0;
00122 for (p2=Pol2; p2; p2=p2->next) {
00123 for (p1=Pol1; p1; p1=p1->next) {
00124 for (i=0; i<p2->NbConstraints; i++) {
00125
00126
00127 p3 = SubConstraint(p2->Constraint[i],p1,NbMaxRays,2);
00128 if (!p3) continue;
00129
00130
00131
00132 if (emptyQ(p3) || p3->NbEq!=Pol1->NbEq)
00133 Polyhedron_Free(p3);
00134
00135
00136 else
00137 d = AddPolyToDomain(p3,d);
00138 }
00139 }
00140 if (p2 != Pol2)
00141 Domain_Free(Pol1);
00142 Pol1 = d;
00143 d = (Polyhedron *)0;
00144 }
00145 return Pol1;
00146 }
00147
00148
00149
00150
00151 static int TestRank(Matrix *Mat) {
00152
00153 int i,j,k;
00154 Value m1,m2,m3,gcd,tmp;
00155
00156
00157 value_init(m1); value_init(m2);
00158 value_init(m3); value_init(gcd); value_init(tmp);
00159
00160 for(k=0;k<Mat->NbColumns;++k) {
00161
00162
00163
00164 if(value_zero_p(Mat->p[k][k])) {
00165 for(j=k+1;j<Mat->NbRows;++j) {
00166
00167
00168 if(value_notzero_p(Mat->p[j][k])) {
00169
00170
00171 for(i=k;i<Mat->NbColumns;++i) {
00172 value_assign(tmp,Mat->p[j][i]);
00173 value_assign(Mat->p[j][i],Mat->p[k][i]);
00174 value_assign(Mat->p[k][i],tmp);
00175 }
00176 break;
00177 }
00178 }
00179
00180
00181
00182 if(j>=Mat->NbRows) {
00183
00184
00185 value_clear(m1); value_clear(m2);
00186 value_clear(m3); value_clear(gcd); value_clear(tmp);
00187 return 0;
00188 }
00189 }
00190
00191
00192 for(j=k+1;j<Mat->NbRows;++j) {
00193
00194
00195 value_gcd(gcd, Mat->p[j][k], Mat->p[k][k]);
00196 for(i=k+1;i<Mat->NbColumns;++i) {
00197
00198
00199 value_multiply(m1,Mat->p[j][i],Mat->p[k][k]);
00200 value_multiply(m2,Mat->p[j][k],Mat->p[k][i]);
00201 value_subtract(m3,m1,m2);
00202 value_division(Mat->p[j][i],m3,gcd);
00203 }
00204 }
00205 }
00206
00207
00208 value_clear(m1); value_clear(m2);
00209 value_clear(m3); value_clear(gcd); value_clear(tmp);
00210
00211
00212 return 1;
00213 }
00214
00215
00216
00217
00218
00219
00220
00221
00222 typedef struct {
00223 unsigned int NbRows;
00224 unsigned int NbColumns;
00225 unsigned int **p;
00226 unsigned int *p_init;
00227 } SatMatrix;
00228
00229 static SatMatrix *SMAlloc(int rows,int cols) {
00230
00231 unsigned int **q, *p;
00232 int i;
00233
00234 SatMatrix *result = (SatMatrix *)malloc(sizeof(SatMatrix));
00235 assert (result != NULL);
00236
00237 result->NbRows = rows;
00238 result->NbColumns = cols;
00239 result->p = q = (unsigned int **)malloc(rows * sizeof(unsigned int *));
00240 assert (result->p != NULL);
00241 result->p_init = p = (unsigned int *)malloc(rows * cols * sizeof(unsigned int));
00242 assert (result->p_init != NULL);
00243
00244 for (i=0;i<rows;i++) {
00245 *q++ = p;
00246 p += cols;
00247 }
00248
00249 return result;
00250 }
00251
00252 static void SMPrint (SatMatrix *matrix) {
00253
00254 unsigned int *p;
00255 int i, j;
00256 unsigned NbRows, NbColumns;
00257
00258 fprintf(stderr,"%d %d\n",NbRows=matrix->NbRows, NbColumns=matrix->NbColumns);
00259 for (i=0;i<NbRows;i++) {
00260 p = *(matrix->p+i);
00261 for (j=0;j<NbColumns;j++)
00262 fprintf(stderr, " %10X ", *p++);
00263 fprintf(stderr, "\n");
00264 }
00265 }
00266
00267
00268 static void SMFree (SatMatrix *matrix) {
00269
00270 free ((char *) matrix->p_init);
00271 free ((char *) matrix->p);
00272 free ((char *) matrix);
00273 return;
00274 }
00275
00276
00277
00278
00279
00280
00281
00282 static int m;
00283 static int m_dim;
00284 static int n;
00285 static int ws;
00286 static int nr;
00287
00288 static Polyhedron *CEqualities;
00289 static SatMatrix *Sat;
00290 static unsigned int *egalite;
00291 static Matrix *Xi, *Pi;
00292 static Matrix *PiTest;
00293 static Matrix *CTest;
00294 static Matrix *PiInv;
00295
00296 static Matrix *RaysDi;
00297
00298 static int KD;
00299
00300
00301 static int nbPV;
00302 static Param_Vertices *PV_Result;
00303 static Param_Domain *PDomains;
00304
00305 #ifdef DEBUGPP
00306 static int nbfaces;
00307 #endif
00308
00309
00310
00311
00312
00313
00314 static Polyhedron *Add_CEqualities(Polyhedron *D) {
00315
00316 Polyhedron *d,*r,*tmp;
00317
00318 if(!CEqualities)
00319 return D;
00320 else {
00321 if(!D || emptyQ(D)) {
00322 if(D)
00323 Domain_Free(D);
00324 return(Polyhedron_Copy(CEqualities));
00325 }
00326 r = AddConstraints(D->Constraint[0],D->NbConstraints,
00327 CEqualities,ws);
00328 tmp = r;
00329 for(d=D->next;d;d=d->next) {
00330 tmp->next = AddConstraints(d->Constraint[0],d->NbConstraints,
00331 CEqualities,ws);
00332 tmp = tmp->next;
00333 }
00334 Domain_Free(D);
00335 return(r);
00336 }
00337 }
00338
00339 #define INT_BITS (sizeof(unsigned) * 8)
00340
00341 unsigned int *int_array2bit_vector(unsigned int *array, int n)
00342 {
00343 int i, ix;
00344 unsigned bx;
00345 int words = (n+INT_BITS-1)/INT_BITS;
00346 unsigned int *bv = (unsigned int *)calloc(words, sizeof(unsigned));
00347 assert(bv);
00348 for (i = 0, ix = 0, bx = MSB; i < n; ++i) {
00349 if (array[i])
00350 bv[ix] |= bx;
00351 NEXT(ix, bx);
00352 }
00353 return bv;
00354 }
00355
00356
00357
00358
00359
00360
00361
00362
00363 static void traite_m_face(Polyhedron *D, unsigned int *mf,
00364 unsigned int *egalite)
00365 {
00366 Matrix *Si;
00367 Polyhedron *PDi;
00368 Param_Vertices *PV;
00369 int j,k,c,r;
00370 unsigned kx, bx;
00371
00372 #ifdef DEBUGPP
00373 ++nbfaces;
00374 #endif
00375
00376
00377 RaysDi->NbRows = 0;
00378 for(k=0,c=0,kx=0,bx=MSB;k<D->NbRays;++k) {
00379 if(mf[kx]&bx) {
00380 if(c<m+1) {
00381 int i;
00382
00383
00384
00385
00386
00387
00388 for(j=0;j<m+1;++j) {
00389 for(i=0;i<c;++i)
00390
00391
00392 value_assign(PiTest->p[j][i],Pi->p[j][i]);
00393
00394
00395 value_assign(PiTest->p[j][c],D->Ray[k][j+1+n]);
00396 }
00397 PiTest->NbColumns = c+1;
00398 r = TestRank(PiTest);
00399 if(r ) {
00400
00401
00402 for (j=0;j<n;j++)
00403 value_assign(Xi->p[j][c],D->Ray[k][j+1]);
00404 for (j=0;j<m;j++)
00405 value_assign(Pi->p[j][c],D->Ray[k][j+1+n]);
00406 value_assign(Xi->p[n][c],D->Ray[k][n+m+1]);
00407 value_assign(Pi->p[m][c],D->Ray[k][n+m+1]);
00408 c++;
00409 }
00410 }
00411
00412
00413 value_assign(RaysDi->p[RaysDi->NbRows][0],D->Ray[k][0]);
00414 Vector_Copy(&D->Ray[k][n+1],&RaysDi->p[RaysDi->NbRows][1],(m+1));
00415 ++RaysDi->NbRows;
00416 }
00417 NEXT(kx,bx);
00418 }
00419
00420 #ifdef DEBUGPP41
00421 fprintf(stderr, "\nRaysDi=\n");
00422 Matrix_Print(stderr,P_VALUE_FMT,RaysDi);
00423 if(c < m+1)
00424 fprintf(stderr, "Invalid ");
00425 fprintf(stderr, "Pi=\n");
00426 Matrix_Print(stderr,P_VALUE_FMT,Pi);
00427 #endif
00428
00429 #ifdef DEBUGPP4
00430 if(c < m+1)
00431 fprintf(stderr,"Eliminated because of no vertex\n");
00432 #endif
00433
00434 if(c < m+1)
00435 return;
00436
00437
00438
00439
00440
00441
00442
00443
00444 #ifdef DEBUGPP4
00445 fprintf(stderr,"Xi = ");
00446 Matrix_Print(stderr,P_VALUE_FMT,Xi);
00447 fprintf(stderr,"Pi = ");
00448 Matrix_Print(stderr,P_VALUE_FMT,Pi);
00449 #endif
00450
00451
00452
00453 if(!MatInverse(Pi,PiInv)) {
00454
00455 #ifdef DEBUGPP4
00456 fprintf(stderr, "Eliminated because of no inverse Pi\n");
00457 #endif
00458
00459 return;
00460 }
00461
00462 #ifdef DEBUGPP4
00463 fprintf(stderr,"FACE GENERATED!\n");
00464 fprintf(stderr,"PiInv = ");
00465 Matrix_Print(stderr,P_VALUE_FMT,PiInv);
00466 #endif
00467
00468
00469 Si = Matrix_Alloc(Xi->NbRows,PiInv->NbColumns);
00470 rat_prodmat(Si,Xi,PiInv);
00471
00472 #ifdef DEBUGPP4
00473 fprintf(stderr,"Si = ");
00474 Matrix_Print(stderr,P_VALUE_FMT,Si);
00475 #endif
00476
00477 Si->NbRows--;
00478
00479
00480 PV = (Param_Vertices *) malloc(sizeof(Param_Vertices));
00481 PV->next = PV_Result;
00482 PV->Vertex = Si;
00483 PV->Domain = NULL;
00484 PV->Facets = int_array2bit_vector(egalite, D->NbConstraints);
00485 PV_Result = PV;
00486 nbPV++;
00487
00488
00489 PDi = Rays2Polyhedron(RaysDi,ws);
00490
00491 #ifdef DEBUGPP3
00492 fprintf(stderr,"RaysDi = ");
00493 Matrix_Print(stderr,P_VALUE_FMT,RaysDi);
00494 fprintf(stderr,"PDi = ");
00495 Polyhedron_Print(stderr,P_VALUE_FMT,PDi);
00496 #endif
00497
00498 if(KD==0) {
00499
00500
00501 PDi = Add_CEqualities(PDi);
00502 PV->Domain = Polyhedron2Constraints(PDi);
00503 Polyhedron_Free(PDi);
00504 }
00505 else {
00506 Param_Domain *PD;
00507 PD = (Param_Domain *) malloc(sizeof(Param_Domain));
00508 PD->Domain = PDi;
00509 PD->F = NULL;
00510 PD->next = PDomains;
00511 PDomains = PD;
00512 }
00513 return;
00514 }
00515
00516
00517
00518
00519
00520
00521 int cntbit[256] = {
00522 0, 1, 1, 2, 1, 2, 2, 3, 1, 2, 2, 3, 2, 3, 3, 4,
00523 1, 2, 2, 3, 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5,
00524 1, 2, 2, 3, 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5,
00525 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6,
00526
00527 1, 2, 2, 3, 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5,
00528 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6,
00529 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6,
00530 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7,
00531
00532 1, 2, 2, 3, 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5,
00533 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6,
00534 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6,
00535 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7,
00536
00537 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6,
00538 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7,
00539 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7,
00540 4, 5, 5, 6, 5, 6, 6, 7, 5, 6, 6, 7, 6, 7, 7, 8 };
00541
00542 static int count_sat (unsigned int *mf) {
00543
00544 register unsigned int i, tmp, cnt=0;
00545
00546 for (i=0; i<nr; i++) {
00547 tmp = mf[i];
00548 cnt = cnt
00549 + cntbit[ tmp & 0xff ]
00550 + cntbit[ (tmp>>8) & 0xff ]
00551 + cntbit[ (tmp>>16) & 0xff ]
00552 + cntbit[ (tmp>>24) & 0xff ]
00553 ;
00554 }
00555 return cnt;
00556 }
00557
00558
00559 static int bit_vector_includes(unsigned int *bv, int len, unsigned int *part)
00560 {
00561 int j;
00562
00563 for (j = 0; j < len; j++) {
00564 #ifdef DEBUGPP4
00565 fprintf(stderr, "mf=%08X Sat=%08X &=%08X\n",
00566 part[j],bv[j], (part[j] & bv[j]));
00567 #endif
00568 if ((part[j] & bv[j]) != part[j])
00569 return 0;
00570 }
00571 return 1;
00572 }
00573
00574
00575
00576
00577
00578
00579
00580
00581
00582
00583
00584
00585
00586
00587
00588
00589
00590
00591
00592
00593
00594
00595
00596
00597
00598
00599
00600
00601
00602
00603
00604
00605
00606
00607
00608
00609
00610
00611
00612
00613
00614
00615 static void scan_m_face(int pos,int nb_un,Polyhedron *D,unsigned int *mf) {
00616
00617
00618
00619
00620
00621 unsigned int *new_mf;
00622
00623 #ifdef DEBUGPP4
00624 fprintf(stderr,"Start scan_m_face(pos=%d, nb_un=%d, n=%d, m=%d\n",
00625 pos,nb_un,n,m);
00626 fprintf(stderr,"mf = ");
00627 {
00628 int i;
00629 for(i=0;i<nr;i++)
00630 fprintf(stderr,"%08X", mf[i]);
00631 fprintf(stderr,"\nequality = [");
00632 for(i=0;i<D->NbConstraints;i++)
00633 fprintf(stderr," %1d",egalite[i]);
00634 fprintf(stderr,"]\n");
00635 }
00636 #endif
00637
00638 if(nb_un == 0) {
00639 int i;
00640
00641
00642
00643
00644
00645 for(i=0;i<pos-1;i++)
00646 {
00647 if(egalite[i])
00648 continue;
00649
00650
00651 #ifdef DEBUGPP4
00652 fprintf(stderr, "Sat[%d]\n", i);
00653 #endif
00654 if (bit_vector_includes(Sat->p[i], nr, mf)) {
00655 #ifdef DEBUGPP4
00656 fprintf(stderr, "Redundant with constraint %d\n", i);
00657 #endif
00658 return;
00659 }
00660 }
00661
00662
00663 for (i = pos; i < D->NbConstraints; ++i) {
00664 if (bit_vector_includes(Sat->p[i], nr, mf))
00665 egalite[i] = 1;
00666 }
00667
00668
00669 traite_m_face(D, mf, egalite);
00670 for (i = pos; i < D->NbConstraints; ++i)
00671 egalite[i] = 0;
00672 return;
00673 }
00674
00675
00676 if((pos+nb_un)>D->NbConstraints) return;
00677
00678
00679
00680 {
00681 int k;
00682 new_mf = (unsigned int *)malloc(nr*sizeof(unsigned int));
00683 for (k=0; k<nr; k++)
00684 new_mf[k] = mf[k] & Sat->p[pos][k];
00685 }
00686 #ifdef DEBUGPP4
00687 fprintf(stderr,"new_mf = ");
00688 {
00689 int i;
00690 for(i=0;i<nr;i++) {
00691 fprintf(stderr,"%08X", new_mf[i]);
00692 }
00693 fprintf(stderr,"\ncount(new_mf) = %d\n",count_sat(new_mf));
00694 }
00695 #endif
00696
00697 {
00698 int c;
00699 c = count_sat(new_mf);
00700
00701 if (c>m_dim )
00702 {
00703 int redundant = 0;
00704
00705 egalite[pos]=1;
00706
00707
00708
00709
00710
00711
00712
00713 if( c==count_sat(mf) ) {
00714 int i, c, j;
00715
00716 for (i = 0, c = 0; i < D->NbConstraints; ++i) {
00717 if (egalite[i] == 0 || egalite[i] == -1)
00718 continue;
00719 for (j = 0; j < D->Dimension+1; ++j)
00720 value_assign(CTest->p[j][c],
00721 D->Constraint[i][j+1]);
00722 ++c;
00723 }
00724 CTest->NbColumns = c;
00725 #ifdef DEBUGPP41
00726 Matrix_Print(stderr,P_VALUE_FMT,CTest);
00727 #endif
00728 redundant = !TestRank(CTest);
00729 }
00730
00731
00732 if( redundant )
00733 {
00734 egalite[pos]=-1;
00735
00736 scan_m_face(pos+1,nb_un,D,new_mf);
00737 }
00738 else
00739 {
00740 scan_m_face(pos+1,nb_un-1,D,new_mf);
00741 }
00742 }
00743 }
00744 free(new_mf);
00745 egalite[pos]=0;
00746 if ((pos+nb_un)>=D->NbConstraints) return;
00747 scan_m_face(pos+1,nb_un,D,mf);
00748 return;
00749 }
00750
00751
00752
00753
00754
00755
00756 static SatMatrix *Poly2Sat(Polyhedron *Pol,unsigned int **L) {
00757
00758 SatMatrix *Sat;
00759 int i, j, k, kx;
00760 unsigned int *Temp;
00761 Value *p1, *p2, p3,tmp;
00762 unsigned Dimension, NbRay, NbCon, bx;
00763
00764
00765 value_init(p3); value_init(tmp);
00766
00767 NbRay = Pol->NbRays;
00768 NbCon = Pol->NbConstraints;
00769 Dimension = Pol->Dimension+1;
00770
00771
00772 nr = (NbRay - 1)/(sizeof(int)*8) + 1;
00773 Sat = SMAlloc(NbCon,nr);
00774 Temp = (unsigned int *)malloc(nr*sizeof(unsigned int));
00775 memset(Sat->p_init,0,nr*NbCon*sizeof(int));
00776 memset(Temp,0,nr*sizeof(unsigned int));
00777 kx=0; bx=MSB;
00778 for (k=0; k<NbRay; k++) {
00779 for (i=0; i<NbCon; i++) {
00780 p1 = &Pol->Constraint[i][1];
00781 p2 = &Pol->Ray[k][1];
00782 value_set_si(p3,0);
00783 for (j=0;j<Dimension;j++) {
00784 value_multiply(tmp,*p1,*p2);
00785 value_addto(p3,p3,tmp);
00786 p1++; p2++;
00787 }
00788 if (value_zero_p(p3))
00789 Sat->p[i][kx]|=bx;
00790 }
00791 Temp[kx] |= bx;
00792 NEXT(kx, bx);
00793 }
00794
00795
00796
00797 *L = Temp;
00798
00799
00800 value_clear(p3); value_clear(tmp);
00801
00802 return Sat;
00803 }
00804
00805
00806
00807
00808
00809 Param_Polyhedron *GenParamPolyhedron(Polyhedron *Pol, Matrix *Rays)
00810 {
00811 Param_Polyhedron *result;
00812 int nbRows, nbColumns;
00813 int i, size, rays;
00814
00815 nbRows=Pol->NbRays;
00816 nbColumns=Pol->Dimension+2;
00817
00818
00819 for(i=0, rays=0; i<nbRows; i++)
00820 if(value_notone_p(Pol->Ray[i][0]) ||
00821 value_zero_p(Pol->Ray[i][nbColumns-1]))
00822 ++rays;
00823
00824
00825 result=(Param_Polyhedron *)malloc(sizeof(Param_Polyhedron));
00826 result->nbV=nbRows-rays;
00827 result->V=NULL;
00828 result->Constraints = Polyhedron2Constraints(Pol);
00829 result->Rays = Rays;
00830
00831
00832 for(i=0;i<nbRows;i++) {
00833 Matrix *vertex;
00834 Param_Vertices *paramVertex;
00835 int j;
00836
00837 if (value_notone_p(Pol->Ray[i][0]) ||
00838 value_zero_p(Pol->Ray[i][nbColumns-1]))
00839 continue;
00840
00841 vertex=Matrix_Alloc(nbColumns-2,2);
00842 for(j=1;j<nbColumns-1;j++) {
00843 value_assign(vertex->p[j-1][0],Pol->Ray[i][j]);
00844 value_assign(vertex->p[j-1][1],Pol->Ray[i][nbColumns-1]);
00845 }
00846 paramVertex=(Param_Vertices *)malloc(sizeof(Param_Vertices));
00847 paramVertex->Vertex=vertex;
00848
00849
00850 paramVertex->Domain=Matrix_Alloc(1,2);
00851 value_set_si(paramVertex->Domain->p[0][0],1);
00852 value_set_si(paramVertex->Domain->p[0][1],1);
00853 paramVertex->Facets = NULL;
00854 paramVertex->next=result->V;
00855 result->V=paramVertex;
00856 }
00857
00858
00859 if (nbRows > 1)
00860 size=(nbRows-1)/(8*sizeof(int))+1;
00861 else
00862 size = 1;
00863 result->D=(Param_Domain *)malloc(sizeof(Param_Domain));
00864 result->D->next=NULL;
00865 result->D->Domain=Universe_Polyhedron(0);
00866 result->D->F=(unsigned int *)malloc(size*sizeof(int));
00867 memset(&result->D->F[0],0xFF,size*sizeof(int));
00868
00869 return result;
00870 }
00871
00872
00873
00874
00875
00876
00877
00878
00879
00880
00881
00882 Matrix *PreElim_Columns(Polyhedron *E,int *p,int *ref,int m) {
00883
00884 int i,j,l;
00885 Matrix *T;
00886
00887
00888
00889
00890
00891 memset(p,0,sizeof(int)*(E->NbEq));
00892
00893 #ifdef DEBUGPP32
00894 fprintf(stderr,"\n\nPreElim_Columns starting\n");
00895 fprintf(stderr,"E =\n");
00896 Polyhedron_Print(stderr,P_VALUE_FMT,E);
00897 #endif
00898
00899 for(l=0;l<E->NbEq;++l) {
00900 if(value_notzero_p(E->Constraint[l][0])) {
00901 fprintf(stderr,"Internal error: Elim_Columns (polyparam.c), expecting equalities first in E.\n");
00902 free(p);
00903 return(NULL);
00904 }
00905 for(i=1;value_zero_p(E->Constraint[l][i]);++i) {
00906 if(i==E->Dimension+1) {
00907 fprintf(stderr,"Internal error: Elim_Columns (polyparam.c), expecting non-empty constraint in E.\n");
00908 free(p);
00909 return( NULL );
00910 }
00911 }
00912 p[l] = i;
00913
00914 #ifdef DEBUGPP32
00915 fprintf(stderr,"p[%d] = %d,",l,p[l]);
00916 #endif
00917 }
00918
00919
00920 for(i=0;i<E->Dimension+2-E->NbEq;++i) {
00921 ref[i]=i;
00922 for(j=0;j<E->NbEq;++j)
00923 if(p[j]<=ref[i])
00924 ref[i]++;
00925
00926 #ifdef DEBUGPP32
00927 fprintf(stderr,"ref[%d] = %d,",i,ref[i]);
00928 #endif
00929 }
00930
00931
00932 T = Matrix_Alloc(m+1-E->NbEq,m+1);
00933 for(i=0;i<T->NbColumns;i++)
00934 for(j=0;j<T->NbRows;j++)
00935 if(ref[E->Dimension-m+j+1] == E->Dimension-m+i+1)
00936 value_set_si(T->p[j][i],1);
00937 else
00938 value_set_si(T->p[j][i],0);
00939
00940 #ifdef DEBUGPP32
00941 fprintf(stderr,"\nTransMatrix =\n");
00942 Matrix_Print(stderr,P_VALUE_FMT,T);
00943 #endif
00944
00945 return(T);
00946
00947 }
00948
00949
00950
00951
00952
00953
00954
00955 Polyhedron *Elim_Columns(Polyhedron *A,Polyhedron *E,int *p,int *ref) {
00956
00957 int i,l,c;
00958 Matrix *M, *C;
00959 Polyhedron *R;
00960 Value tmp1,tmp2;
00961
00962
00963 value_init(tmp1); value_init(tmp2);
00964
00965 #ifdef DEBUGPP32
00966 fprintf(stderr,"\nElim_Columns starting\n");
00967 fprintf(stderr,"A =\n" );
00968 Polyhedron_Print(stderr,P_VALUE_FMT,A);
00969 #endif
00970
00971
00972 M = Polyhedron2Constraints(A);
00973 for(l=0;l<E->NbEq;++l) {
00974 for(c=0;c<M->NbRows;++c) {
00975 if(value_notzero_p(M->p[c][p[l]])) {
00976
00977
00978 for(i=1;i<M->NbColumns;++i) {
00979 value_multiply(tmp1,M->p[c][i],E->Constraint[l][p[l]]);
00980 value_multiply(tmp2,E->Constraint[l][i],M->p[c][p[l]]);
00981 value_subtract(M->p[c][i],tmp1,tmp2);
00982 }
00983 }
00984 }
00985 }
00986
00987 #ifdef DEBUGPP32
00988 fprintf(stderr,"\nElim_Columns after zeroing columns of A.\n");
00989 fprintf(stderr,"M =\n");
00990 Matrix_Print(stderr,P_VALUE_FMT,M);
00991 #endif
00992
00993
00994 C = Matrix_Alloc(M->NbRows,M->NbColumns - E->NbEq);
00995 for(l=0;l<C->NbRows;++l)
00996 for(c=0;c<C->NbColumns;++c) {
00997 value_assign(C->p[l][c],M->p[l][ref[c]]);
00998 }
00999
01000 #ifdef DEBUGPP32
01001 fprintf(stderr,"\nElim_Columns after eliminating columns of A.\n");
01002 fprintf(stderr,"C =\n");
01003 Matrix_Print(stderr,P_VALUE_FMT,C);
01004 #endif
01005
01006 R = Constraints2Polyhedron(C,ws);
01007 Matrix_Free(C);
01008 Matrix_Free(M);
01009 value_clear(tmp1); value_clear(tmp2);
01010 return(R);
01011 }
01012
01013
01014 static Polyhedron *Recession_Cone(Polyhedron *P, unsigned nvar, unsigned MaxRays)
01015 {
01016 int i;
01017 Matrix *M = Matrix_Alloc(P->NbConstraints, 1 + nvar + 1);
01018 Polyhedron *R;
01019 for (i = 0; i < P->NbConstraints; ++i)
01020 Vector_Copy(P->Constraint[i], M->p[i], 1+nvar);
01021 R = Constraints2Polyhedron(M, MaxRays);
01022 Matrix_Free(M);
01023 return R;
01024 }
01025
01026
01027
01028
01029
01030
01031
01032
01033 static int ComputeNPLinesRays(int n, Polyhedron *D1, Matrix **Rays)
01034 {
01035 int i, j, nbr, dimfaces;
01036 Polyhedron *RC;
01037
01038 RC = Recession_Cone(D1, n, ws);
01039
01040
01041 nbr = 0;
01042 for (i = 0; i < RC->NbRays ;i++)
01043 if (value_zero_p(RC->Ray[i][n+1]))
01044 nbr++;
01045 *Rays=Matrix_Alloc(nbr, n+2);
01046 for (i = 0, j = 0; j < nbr ;i++)
01047 if (value_zero_p(RC->Ray[i][n+1]))
01048 Vector_Copy(RC->Ray[i], (*Rays)->p[j++], n+2);
01049
01050 dimfaces = RC->NbBid;
01051 Polyhedron_Free(RC);
01052
01053 #ifdef DEBUGPP31
01054 fprintf(stderr, "Rays = ");
01055 Matrix_Print(stderr, P_VALUE_FMT, *Rays);
01056 fprintf(stderr, "dimfaces = %d\n", dimfaces);
01057 #endif
01058
01059 return dimfaces;
01060 }
01061
01062
01063
01064
01065
01066
01067
01068 Param_Polyhedron *Find_m_faces(Polyhedron **Di,Polyhedron *C,int keep_dom,int working_space,Polyhedron **CEq,Matrix **CT) {
01069
01070 unsigned int *mf;
01071 int i, j, dimfaces;
01072 Polyhedron *D=*Di,
01073 *C1,
01074 *D1;
01075 Matrix *Rays,
01076 *M;
01077 Param_Polyhedron *res;
01078 int *p, *ref;
01079
01080 CEqualities = NULL;
01081
01082 if(CT) {
01083 *CEq = NULL;
01084 *CT = NULL;
01085 }
01086
01087 if(!D || !C)
01088 return (Param_Polyhedron *) 0;
01089
01090 ws = working_space;
01091 m = C->Dimension;
01092 n = D->Dimension - m;
01093 if(n<0) {
01094 fprintf(stderr,
01095 "Find_m_faces: ?%d parameters of a %d-polyhedron !\n",m,n);
01096 return (Param_Polyhedron *) 0;
01097 }
01098 if (m==0)
01099 return GenParamPolyhedron(D,Matrix_Alloc(0,2));
01100
01101
01102 C1 = align_context(C,D->Dimension,ws);
01103
01104 #ifdef DEBUGPP31
01105 fprintf(stderr,"m = %d\n",m);
01106 fprintf(stderr, "D = ");
01107 Polyhedron_Print(stderr,P_VALUE_FMT,D);
01108 fprintf(stderr,"C1 = ");
01109 Polyhedron_Print(stderr,P_VALUE_FMT,C1);
01110 #endif
01111
01112 D1 = DomainIntersection(D,C1,ws);
01113
01114 #ifdef DEBUGPP31
01115 fprintf(stderr,"D1 = ");
01116 Polyhedron_Print(stderr,P_VALUE_FMT,D1);
01117 #endif
01118
01119 Domain_Free(C1);
01120
01121 if (!D1)
01122 return(NULL);
01123 if (emptyQ(D1)) {
01124 Polyhedron_Free(D1);
01125 return(NULL);
01126 }
01127
01128
01129
01130 M = Matrix_Alloc(n, D1->Dimension+2);
01131 for (i=0; i<n; i++)
01132 value_set_si(M->p[i][i+1],1);
01133 C1 = DomainAddRays(D1,M,ws);
01134 Matrix_Free(M);
01135
01136 #ifdef DEBUGPP31
01137 fprintf(stderr,"True context C1 = ");
01138 Polyhedron_Print(stderr,P_VALUE_FMT,C1);
01139 #endif
01140
01141 dimfaces = ComputeNPLinesRays(n, D1, &Rays);
01142
01143
01144
01145 if(!CT) {
01146 if (C1->NbEq == 0) {
01147 Polyhedron_Free(C1);
01148 C1 = NULL;
01149 } else {
01150 Polyhedron *CEq1,
01151 *D2;
01152
01153
01154
01155
01156 M = Matrix_Alloc(C1->NbEq,m+2);
01157 for(j=0,i=0;i<C1->NbEq;++i,++j) {
01158 while(value_notzero_p(C1->Constraint[j][0]))
01159 ++j;
01160 value_assign(M->p[i][0],C1->Constraint[j][0]);
01161 Vector_Copy(&C1->Constraint[j][D->Dimension-m+1],&M->p[i][1],(m+1));
01162 }
01163 CEqualities = Constraints2Polyhedron(M,ws);
01164 Matrix_Free(M);
01165 CEq1 = align_context(CEqualities,D->Dimension,ws);
01166
01167
01168 D2 = DomainSimplify(D1,CEq1,ws);
01169 Polyhedron_Free(D1);
01170 Polyhedron_Free(C1);
01171 Polyhedron_Free(CEq1);
01172 D1 = D2;
01173 C1 = NULL;
01174 }
01175 }
01176 else {
01177 Polyhedron *CEq1,
01178 *D2;
01179
01180
01181
01182
01183 CEq1 = C1;
01184 M = Matrix_Alloc(C1->NbConstraints,m+2);
01185 for(i=0;i<C1->NbConstraints;++i) {
01186 value_assign(M->p[i][0],C1->Constraint[i][0]);
01187 Vector_Copy(&C1->Constraint[i][D->Dimension-m+1],&M->p[i][1],(m+1));
01188 }
01189 CEqualities = Constraints2Polyhedron( M, ws );
01190 Matrix_Free(M);
01191
01192 D2 = DomainSimplify(D1,CEq1,ws);
01193 Polyhedron_Free(D1);
01194 D1 = D2;
01195 C1 = Universe_Polyhedron(D2->Dimension);
01196
01197
01198
01199
01200 if( CEq1->NbEq )
01201 {
01202 m -= CEq1->NbEq;
01203 p = (int *)malloc(sizeof(int)*(CEq1->NbEq));
01204 }
01205 else
01206 p = NULL;
01207 ref = (int*) malloc(sizeof(int)*
01208 (CEq1->Dimension+2-CEq1->NbEq));
01209 *CT = PreElim_Columns(CEq1,p,ref,CEqualities->Dimension);
01210 D2 = Elim_Columns(D1,CEq1,p,ref);
01211 if (p)
01212 free(p);
01213 free(ref);
01214
01215 #ifdef DEBUGPP3
01216 fprintf(stderr,"D2\t Dim = %3d\tNbEq = %3d\tLines = %3d\n",
01217 D2->Dimension,D2->NbEq,D2->NbBid);
01218 C2 = Elim_Columns(C1,CEq1,p,ref);
01219 fprintf(stderr,"C2\t Dim = %3d\tNbEq = %3d\tLines = %3d\n",
01220 C2->Dimension,C2->NbEq,C2->NbBid);
01221 Polyhedron_Free(C2);
01222 #endif
01223
01224 Polyhedron_Free(D1);
01225 Polyhedron_Free(C1);
01226 D1 = D2;
01227 C1 = NULL;
01228 *CEq = CEqualities;
01229
01230 #ifdef DEBUGPP3
01231 fprintf(stderr,"Polyhedron CEq = ");
01232 Polyhedron_Print(stderr,P_VALUE_FMT,*CEq);
01233 fprintf(stderr,"Matrix CT = ");
01234 Matrix_Print(stderr,P_VALUE_FMT,*CT);
01235 #endif
01236
01237 Polyhedron_Free(CEq1);
01238 CEqualities = NULL;
01239
01240
01241 if(m==0) {
01242
01243 *Di = D1;
01244
01245 return GenParamPolyhedron(D1, Rays);
01246 }
01247 }
01248
01249 #ifdef DEBUGPP3
01250 fprintf(stderr,"Polyhedron D1 (D AND C) = ");
01251 Polyhedron_Print(stderr,P_VALUE_FMT, D1);
01252 fprintf(stderr,"Polyhedron CEqualities = ");
01253 if(CEqualities) Polyhedron_Print(stderr,P_VALUE_FMT, CEqualities);
01254 else fprintf(stderr,"NULL\n");
01255 #endif
01256
01257 KD = keep_dom;
01258 PDomains = NULL;
01259 PV_Result = NULL;
01260 nbPV = 0;
01261
01262 if (emptyQ(D1)) {
01263 Polyhedron_Free(D1);
01264 Matrix_Free(Rays);
01265 return NULL;
01266 }
01267
01268
01269
01270
01271 Sat = Poly2Sat(D1,&mf);
01272
01273 #ifdef DEBUGPP4
01274 fprintf(stderr,"Sat = ");
01275 SMPrint(Sat);
01276
01277 fprintf(stderr,"mf = ");
01278 for (i=0; i<nr; i++)
01279 fprintf(stderr,"%08X", mf[i]);
01280 fprintf(stderr, "\n");
01281 #endif
01282
01283
01284 egalite = (unsigned int *)malloc(sizeof(int)*D1->NbConstraints);
01285 memset(egalite,0, sizeof(int)*D1->NbConstraints);
01286
01287 for (i=0; i<D1->NbEq; i++)
01288 egalite[i] = 1;
01289
01290 Xi = Matrix_Alloc(n+1,m+1);
01291 Pi = Matrix_Alloc(m+1,m+1);
01292 PiTest = Matrix_Alloc(m+1,m+1);
01293 CTest = Matrix_Alloc(D->Dimension+1,D->NbConstraints);
01294 PiInv = Matrix_Alloc(m+1,m+2);
01295 RaysDi = Matrix_Alloc(D1->NbRays,m+2);
01296 m_dim = m;
01297
01298
01299
01300
01301 m_dim += dimfaces;
01302
01303
01304
01305
01306 #ifdef DEBUGPP3
01307 if (m_dim < D1->NbBid)
01308 fprintf(stderr, "m_dim (%d) < D1->NbBid (%d)\n", m_dim, D1->NbBid );
01309 #endif
01310 if (m_dim < D1->NbBid)
01311 m_dim = D1->NbBid;
01312
01313 #ifdef DEBUGPP
01314 nbfaces=0;
01315 #endif
01316 #ifdef DEBUGPP3
01317 fprintf(stderr, "m_dim = %d\n", m_dim);
01318 fprintf(stderr,
01319 "Target: find faces that saturate %d constraints and %d rays/lines\n",
01320 D1->Dimension - m_dim,m_dim+1);
01321 #endif
01322
01323
01324 scan_m_face(D1->NbEq,(D1->Dimension - m_dim - D1->NbEq),D1,mf);
01325
01326
01327
01328 #ifdef DEBUGPP
01329 fprintf( stderr, "Number of m-faces: %d\n", nbfaces );
01330 #endif
01331
01332 Matrix_Free(RaysDi);
01333 Matrix_Free(PiInv);
01334 Matrix_Free(PiTest);
01335 Matrix_Free(CTest);
01336 Matrix_Free(Pi);
01337 Matrix_Free(Xi);
01338 free(egalite);
01339 free(mf);
01340 SMFree(Sat);
01341
01342
01343
01344
01345
01346
01347 res = (Param_Polyhedron *) malloc (sizeof(Param_Polyhedron));
01348 res->nbV = nbPV;
01349 res->V = PV_Result;
01350 res->D = PDomains;
01351 res->Constraints = Polyhedron2Constraints(D1);
01352 res->Rays = Rays;
01353
01354 if(CT)
01355 *Di = D1;
01356 else
01357 Domain_Free(D1);
01358
01359 return(res);
01360 }
01361
01362
01363
01364
01365
01366 void Compute_PDomains(Param_Domain *PD,int nb_domains,int working_space) {
01367
01368 unsigned bx;
01369 int i, ix, nv;
01370 Polyhedron *dx, *d1, *d2;
01371 Param_Domain *p1, *p2, *p2prev, *PDNew;
01372
01373 if (nb_domains==0) {
01374
01375 #ifdef DEBUGPP5
01376 fprintf(stderr,"No domains\n");
01377 #endif
01378
01379 return;
01380 }
01381
01382
01383 if (!PD->next && PD->F)
01384 return;
01385
01386
01387 nv = (nb_domains - 1)/(8*sizeof(int)) + 1;
01388
01389 #ifdef DEBUGPP5
01390 fprintf(stderr,"nv = %d\n",nv);
01391 #endif
01392
01393 for(p1=PD,i=0,ix=0,bx=MSB;p1;p1=p1->next,i++) {
01394
01395
01396 p1->F = (unsigned *) malloc (nv * sizeof(unsigned));
01397
01398
01399 memset(p1->F,0,nv * sizeof(unsigned));
01400 p1->F[ix] |= bx;
01401 NEXT(ix, bx);
01402 }
01403
01404 #ifdef DEBUGPP5
01405 fprintf(stderr,"nb of vertices=%d\n",i);
01406 #endif
01407
01408
01409 ix = 0; bx=MSB;
01410 for (p1=PD;p1;p1=p1->next) {
01411 for (p2prev=p1,p2=p1->next;p2;p2prev=p2,p2=p2->next) {
01412
01413
01414 dx = PDomainIntersection(p1->Domain,p2->Domain,working_space);
01415
01416 if (!dx || emptyQ(dx)) {
01417
01418 #ifdef DEBUGPP5
01419 fprintf( stderr, "Empty dx (p1 inter p2). Continuing\n");
01420 #endif
01421 if(dx)
01422 Domain_Free(dx);
01423 continue;
01424 }
01425
01426 #ifdef DEBUGPP5
01427 fprintf(stderr,"Begin PDomainDifference\n");
01428 fprintf(stderr, "p1=");
01429 Polyhedron_Print(stderr,P_VALUE_FMT,p1->Domain);
01430 fprintf(stderr,"p2=");
01431 Polyhedron_Print(stderr,P_VALUE_FMT,p2->Domain);
01432 #endif
01433 d1 = PDomainDifference(p1->Domain,p2->Domain,working_space);
01434 d2 = PDomainDifference(p2->Domain,p1->Domain,working_space);
01435
01436 #ifdef DEBUGPP5
01437 fprintf(stderr,"p1\\p2=");
01438 Polyhedron_Print(stderr,P_VALUE_FMT,d1);
01439 fprintf(stderr,"p2\\p1=");
01440 Polyhedron_Print(stderr,P_VALUE_FMT,d2);
01441 fprintf(stderr,"END PDomainDifference\n\n");
01442 #endif
01443 if (!d1 || emptyQ(d1) || d1->NbEq!=0) {
01444
01445 #ifdef DEBUGPP5
01446 fprintf(stderr,"Empty d1\n");
01447 #endif
01448 if (d1)
01449 Domain_Free(d1);
01450 Domain_Free(dx);
01451
01452 if (!d2 || emptyQ(d2) || d2->NbEq!=0) {
01453
01454 #ifdef DEBUGPP5
01455 fprintf( stderr, "Empty d2 (deleting)\n");
01456 #endif
01457
01458 if (d2) Domain_Free(d2);
01459
01460
01461 for (i=0;i<nv;i++)
01462 p1->F[i] |= p2->F[i];
01463
01464
01465 p2prev->next = p2->next;
01466 Domain_Free(p2->Domain);
01467 free(p2->F);
01468 free(p2);
01469 p2 = p2prev;
01470 }
01471 else {
01472
01473 #ifdef DEBUGPP5
01474 fprintf( stderr, "p2 replaced by d2\n");
01475 #endif
01476
01477 for(i=0;i<nv;i++)
01478 p1->F[i] |= p2->F[i];
01479
01480
01481 Domain_Free( p2->Domain );
01482 p2->Domain = d2;
01483 }
01484 }
01485 else {
01486 if (!d2 || emptyQ(d2) || d2->NbEq!=0) {
01487
01488 #ifdef DEBUGPP5
01489 fprintf( stderr, "p1 replaced by d1\n");
01490 #endif
01491 if (d2) Domain_Free(d2);
01492
01493
01494 Domain_Free(dx);
01495
01496
01497 for(i=0;i<nv;i++)
01498 p2->F[i] |= p1->F[i];
01499
01500
01501 Domain_Free(p1->Domain);
01502 p1->Domain = d1;
01503 }
01504 else {
01505
01506 #ifdef DEBUGPP5
01507 fprintf(stderr,"Non-empty d1 and d2\nNew node created\n");
01508 #endif
01509
01510 PDNew = (Param_Domain *) malloc( sizeof(Param_Domain) );
01511 PDNew->F = (unsigned int *)malloc( nv*sizeof(int) );
01512 memset(PDNew->F,0,nv*sizeof(int));
01513 PDNew->Domain = dx;
01514
01515 for (i=0;i<nv;i++)
01516 PDNew->F[i] = p1->F[i] | p2->F[i];
01517
01518
01519 Domain_Free( p1->Domain );
01520 p1->Domain = d1;
01521
01522
01523 Domain_Free( p2->Domain );
01524 p2->Domain = d2;
01525
01526
01527 PDNew->next = p1->next;
01528 p1->next = PDNew;
01529 }
01530 }
01531 }
01532 if (p1->Domain->next) {
01533 Polyhedron *C = DomainConvex(p1->Domain, working_space);
01534 Domain_Free(p1->Domain);
01535 p1->Domain = C;
01536 }
01537 }
01538 }
01539
01540
01541
01542
01543
01544
01545
01546 Param_Polyhedron *Polyhedron2Param_Vertices(Polyhedron *Din,Polyhedron *Cin,int working_space) {
01547
01548 Param_Polyhedron *result;
01549
01550 POL_ENSURE_FACETS(Din);
01551 POL_ENSURE_VERTICES(Din);
01552 POL_ENSURE_FACETS(Cin);
01553 POL_ENSURE_VERTICES(Cin);
01554
01555 #ifdef DEBUGPP
01556 fprintf(stderr,"Polyhedron2Param_Vertices algorithm starting at : %.2fs\n",
01557 (float)clock()/CLOCKS_PER_SEC);
01558 #endif
01559
01560
01561 result = Find_m_faces(&Din,Cin,0,working_space,NULL,NULL);
01562
01563 #ifdef DEBUGPP
01564 fprintf(stderr, "nb of points : %d\n",result->nbV);
01565 #endif
01566
01567 #ifdef DEBUGPP
01568 fprintf(stderr, "end main loop : %.2fs\n", (float)clock()/CLOCKS_PER_SEC);
01569 #endif
01570
01571 return(result);
01572 }
01573
01574
01575
01576
01577 void Param_Vertices_Free(Param_Vertices *PV) {
01578
01579 Param_Vertices *next_pv;
01580
01581 while(PV) {
01582 next_pv = PV->next;
01583 if (PV->Vertex) Matrix_Free(PV->Vertex);
01584 if (PV->Domain) Matrix_Free(PV->Domain);
01585 if (PV->Facets) free(PV->Facets);
01586 free(PV);
01587 PV = next_pv;
01588 }
01589 }
01590
01591
01592
01593
01594 void Print_Vertex(FILE *DST, Matrix *V, const char **param_names)
01595 {
01596 int l, v;
01597 int first;
01598 Value gcd,tmp;
01599
01600 value_init(gcd); value_init(tmp);
01601
01602 fprintf(DST, "[" );
01603 for(l=0;l<V->NbRows;++l){
01604
01605
01606 first=1;
01607 fprintf(DST, " " );
01608 for(v=0;v < V->NbColumns-2;++v) {
01609 if(value_notzero_p(V->p[l][v])) {
01610 value_gcd(gcd, V->p[l][v], V->p[l][V->NbColumns-1]);
01611 value_divexact(tmp, V->p[l][v], gcd);
01612 if(value_posz_p(tmp)) {
01613 if(!first)
01614 fprintf(DST, "+");
01615 if(value_notone_p(tmp)) {
01616 value_print(DST,VALUE_FMT,tmp);
01617 }
01618 }
01619 else {
01620 if(value_mone_p(tmp))
01621 fprintf(DST, "-" );
01622 else {
01623 value_print(DST,VALUE_FMT,tmp);
01624 }
01625 }
01626 value_divexact(tmp, V->p[l][V->NbColumns-1], gcd);
01627 if(value_notone_p(tmp)) {
01628 fprintf(DST, "%s/", param_names[v]);
01629 value_print(DST,VALUE_FMT,tmp);
01630 }
01631 else
01632 fprintf(DST, "%s", param_names[v]);
01633 first=0;
01634 }
01635 }
01636
01637
01638 if(value_notzero_p(V->p[l][v]) || first) {
01639 if(value_posz_p(V->p[l][v]) && !first)
01640 fprintf(DST,"+");
01641 value_gcd(gcd, V->p[l][v], V->p[l][V->NbColumns-1]);
01642 value_divexact(tmp, V->p[l][v], gcd);
01643 value_print(DST,VALUE_FMT,tmp);
01644 value_divexact(tmp, V->p[l][V->NbColumns-1], gcd);
01645 if(value_notone_p(tmp)) {
01646 fprintf(DST,"/");
01647 value_print(DST,VALUE_FMT,tmp);
01648 fprintf(DST," ");
01649 }
01650 }
01651 if (l<V->NbRows-1)
01652 fprintf(DST, ", ");
01653 }
01654 fprintf(DST, " ]");
01655 value_clear(gcd); value_clear(tmp);
01656 return;
01657 }
01658
01659
01660
01661
01662
01663 Matrix *VertexCT(Matrix *V,Matrix *CT) {
01664
01665 Matrix *Vt;
01666 int i,j,k;
01667
01668 if(CT) {
01669
01670
01671 Vt = Matrix_Alloc(V->NbRows,CT->NbColumns+1);
01672 for(i=0;i<V->NbRows;++i) {
01673 value_assign(Vt->p[i][CT->NbColumns],V->p[i][V->NbColumns-1]);
01674 for(j=0;j<CT->NbColumns;j++) {
01675 for(k=0;k<CT->NbRows;k++)
01676 if(value_notzero_p(CT->p[k][j]))
01677 break;
01678 if(k<CT->NbRows)
01679 value_assign(Vt->p[i][j],V->p[i][k]);
01680 else
01681 value_set_si(Vt->p[i][j],0);
01682 }
01683 }
01684 return(Vt);
01685 }
01686 else
01687 return(NULL);
01688 }
01689
01690
01691
01692
01693 void Print_Domain(FILE *DST, Polyhedron *D, const char **pname)
01694 {
01695 int l, v;
01696 int first;
01697
01698 POL_ENSURE_FACETS(D);
01699 POL_ENSURE_VERTICES(D);
01700
01701 for(l=0;l<D->NbConstraints;++l) {
01702 fprintf(DST, " ");
01703 first = 1;
01704 for(v=1;v<=D->Dimension;++v) {
01705 if(value_notzero_p(D->Constraint[l][v])) {
01706 if(value_one_p(D->Constraint[l][v])) {
01707 if(first)
01708 fprintf(DST, "%s ", pname[v-1]);
01709 else
01710 fprintf(DST, "+ %s ", pname[v-1] );
01711 }
01712 else if(value_mone_p(D->Constraint[l][v]))
01713 fprintf(DST, "- %s ", pname[v-1] );
01714 else {
01715 if(value_pos_p(D->Constraint[l][v]) && !first )
01716 fprintf(DST, "+ " );
01717 value_print(DST,VALUE_FMT,D->Constraint[l][v]);
01718 fprintf(DST,"%s ",pname[v-1]);
01719 }
01720 first = 0;
01721 }
01722 }
01723 if(value_notzero_p(D->Constraint[l][v])) {
01724 if(value_pos_p(D->Constraint[l][v]) && !first)
01725 fprintf(DST,"+");
01726 fprintf(DST," ");
01727 value_print(DST,VALUE_FMT,D->Constraint[l][v]);
01728 }
01729 fprintf(DST,(value_notzero_p(D->Constraint[l][0])) ?" >= 0":" = 0");
01730 fprintf(DST, "\n" );
01731 }
01732 fprintf(DST, "\n");
01733
01734 if( D->next )
01735 {
01736 fprintf( DST, "UNION\n" );
01737 Print_Domain( DST, D->next, pname );
01738 }
01739 return;
01740 }
01741
01742
01743
01744
01745
01746 void Param_Vertices_Print(FILE *DST, Param_Vertices *PV, const char **param_names)
01747 {
01748 Polyhedron *poly;
01749
01750 while(PV) {
01751 fprintf(DST, "Vertex :\n" );
01752 Print_Vertex(DST,PV->Vertex,param_names);
01753
01754
01755 fprintf(DST, " If :\n" );
01756 poly = Constraints2Polyhedron(PV->Domain,200);
01757 Print_Domain(DST,poly,param_names);
01758 Domain_Free(poly);
01759 PV = PV->next;
01760 }
01761 return;
01762 }
01763
01764
01765
01766
01767
01768
01769
01770
01771 Param_Polyhedron *Polyhedron2Param_Domain(Polyhedron *Din,Polyhedron *Cin,int working_space) {
01772
01773 Param_Polyhedron *result;
01774 Param_Domain *D;
01775
01776 POL_ENSURE_FACETS(Din);
01777 POL_ENSURE_VERTICES(Din);
01778 POL_ENSURE_FACETS(Cin);
01779 POL_ENSURE_VERTICES(Cin);
01780
01781 if (emptyQ(Din) || emptyQ(Cin))
01782 return NULL;
01783
01784 #ifdef DEBUGPP
01785 fprintf(stderr,"Polyhedron2Param_Polyhedron algorithm starting at : %.2fs\n",
01786 (float)clock()/CLOCKS_PER_SEC);
01787 #endif
01788
01789
01790
01791 result = Find_m_faces(&Din,Cin,1,working_space,NULL,NULL);
01792
01793 #ifdef DEBUGPP
01794 if(result) fprintf(stderr, "Number of vertices : %d\n",result->nbV);
01795 fprintf(stderr,"Vertices found at : %.2fs\n",(float)clock()/CLOCKS_PER_SEC);
01796 #endif
01797
01798
01799 if(result && Cin->Dimension>0)
01800 Compute_PDomains(result->D,result->nbV,working_space);
01801 if(result && CEqualities)
01802 for(D=result->D;D;D=D->next)
01803 D->Domain = Add_CEqualities(D->Domain);
01804 Polyhedron_Free(CEqualities);
01805
01806 #ifdef DEBUGPP
01807 fprintf(stderr, "domains found at : %.2fs\n", (float)clock()/CLOCKS_PER_SEC);
01808 #endif
01809
01810 return(result);
01811 }
01812
01813
01814
01815
01816 Param_Polyhedron *Polyhedron2Param_SimplifiedDomain(Polyhedron **Din,Polyhedron *Cin,int working_space,Polyhedron **CEq,Matrix **CT) {
01817
01818 Param_Polyhedron *result;
01819
01820 assert(CEq != NULL);
01821 assert(CT != NULL);
01822
01823 POL_ENSURE_FACETS(*Din);
01824 POL_ENSURE_VERTICES(*Din);
01825 POL_ENSURE_FACETS(Cin);
01826 POL_ENSURE_VERTICES(Cin);
01827
01828 #ifdef DEBUGPP
01829 fprintf(stderr,"Polyhedron2Param_Polyhedron algorithm starting at : %.2fs\n",
01830 (float)clock()/CLOCKS_PER_SEC);
01831 #endif
01832
01833
01834
01835 result = Find_m_faces(Din,Cin,1,working_space,CEq,CT);
01836
01837 #ifdef DEBUGPP
01838 if(result) fprintf(stderr, "Number of vertices : %d\n",result->nbV);
01839 fprintf(stderr,"Vertices found at : %.2fs\n",(float)clock()/CLOCKS_PER_SEC);
01840 #endif
01841
01842
01843 if(result && Cin->Dimension>0)
01844 Compute_PDomains(result->D,result->nbV,working_space);
01845
01846
01847
01848
01849
01850
01851
01852 #ifdef DEBUGPP
01853 fprintf(stderr, "domains found at : %.2fs\n", (float)clock()/CLOCKS_PER_SEC);
01854 #endif
01855
01856 return(result);
01857 }
01858
01859
01860
01861
01862
01863 void Param_Domain_Free(Param_Domain *PD) {
01864
01865 Param_Domain *next_pd;
01866
01867 while(PD) {
01868 free(PD->F);
01869 Domain_Free(PD->Domain);
01870 next_pd = PD->next;
01871 free(PD);
01872 PD = next_pd;
01873 }
01874 return;
01875 }
01876
01877
01878
01879
01880 void Param_Polyhedron_Free(Param_Polyhedron *P) {
01881
01882 if (!P) return;
01883 Param_Vertices_Free(P->V);
01884 Param_Domain_Free(P->D);
01885 if (P->Constraints)
01886 Matrix_Free(P->Constraints);
01887 if (P->Rays)
01888 Matrix_Free(P->Rays);
01889 free(P);
01890 return;
01891 }
01892
01893
01894
01895
01896 void Param_Polyhedron_Scale_Integer(Param_Polyhedron *PP, Polyhedron **P,
01897 Value *det, unsigned MaxRays)
01898 {
01899 int i;
01900 int nb_param, nb_vars;
01901 Vector *denoms;
01902 Param_Vertices *V;
01903 Value global_var_lcm;
01904 Matrix *expansion;
01905
01906 value_set_si(*det, 1);
01907 if (!PP->nbV)
01908 return;
01909
01910 nb_param = PP->D->Domain->Dimension;
01911 nb_vars = PP->V->Vertex->NbRows;
01912
01913
01914
01915
01916 denoms = Vector_Alloc(nb_vars);
01917 value_init(global_var_lcm);
01918
01919
01920 for (V = PP->V; V; V = V->next)
01921 for (i = 0; i < nb_vars; i++)
01922 value_lcm(denoms->p[i], denoms->p[i], V->Vertex->p[i][nb_param+1]);
01923
01924 value_set_si(global_var_lcm, 1);
01925 for (i = 0; i < nb_vars; i++) {
01926 value_multiply(*det, *det, denoms->p[i]);
01927 value_lcm(global_var_lcm, global_var_lcm, denoms->p[i]);
01928 }
01929
01930
01931 for (V = PP->V; V; V = V->next)
01932 for (i = 0; i < nb_vars; i++) {
01933 Vector_Scale(V->Vertex->p[i], V->Vertex->p[i], denoms->p[i], nb_param+1);
01934 Vector_Normalize(V->Vertex->p[i], nb_param+2);
01935 }
01936
01937
01938
01939 for (i = 0; i < nb_vars; i++)
01940 value_division(denoms->p[i], global_var_lcm, denoms->p[i]);
01941
01942
01943
01944 expansion = Matrix_Alloc(nb_vars+nb_param+1, nb_vars+nb_param+1);
01945 for (i = 0; i < nb_vars; i++)
01946 value_assign(expansion->p[i][i], denoms->p[i]);
01947 for (i = nb_vars; i < nb_vars+nb_param+1; i++)
01948 value_assign(expansion->p[i][i], global_var_lcm);
01949
01950
01951 if (P)
01952 *P = Polyhedron_Preimage(*P, expansion, MaxRays);
01953
01954 Matrix_Free(expansion);
01955 value_clear(global_var_lcm);
01956 Vector_Free(denoms);
01957 }