glu-2.2: src/cuBdd/cuddHarwell.c Source File

00001 
00051 #include "util.h"
00052 #include "cuddInt.h"
00053 
00054 /*---------------------------------------------------------------------------*/
00055 /* Constant declarations                                                     */
00056 /*---------------------------------------------------------------------------*/
00057 
00058 
00059 /*---------------------------------------------------------------------------*/
00060 /* Stucture declarations                                                     */
00061 /*---------------------------------------------------------------------------*/
00062 
00063 
00064 /*---------------------------------------------------------------------------*/
00065 /* Type declarations                                                         */
00066 /*---------------------------------------------------------------------------*/
00067 
00068 
00069 /*---------------------------------------------------------------------------*/
00070 /* Variable declarations                                                     */
00071 /*---------------------------------------------------------------------------*/
00072 
00073 #ifndef lint
00074 static char rcsid[] DD_UNUSED = "$Id: cuddHarwell.c,v 1.9 2004/08/13 18:04:49 fabio Exp $";
00075 #endif
00076 
00077 /*---------------------------------------------------------------------------*/
00078 /* Macro declarations                                                        */
00079 /*---------------------------------------------------------------------------*/
00080 
00081 
00084 /*---------------------------------------------------------------------------*/
00085 /* Static function prototypes                                                */
00086 /*---------------------------------------------------------------------------*/
00087 
00088 
00092 /*---------------------------------------------------------------------------*/
00093 /* Definition of exported functions                                          */
00094 /*---------------------------------------------------------------------------*/
00095 
00119 int
00120 Cudd_addHarwell(
00121   FILE * fp /* pointer to the input file */,
00122   DdManager * dd /* DD manager */,
00123   DdNode ** E /* characteristic function of the graph */,
00124   DdNode *** x /* array of row variables */,
00125   DdNode *** y /* array of column variables */,
00126   DdNode *** xn /* array of complemented row variables */,
00127   DdNode *** yn_ /* array of complemented column variables */,
00128   int * nx /* number or row variables */,
00129   int * ny /* number or column variables */,
00130   int * m /* number of rows */,
00131   int * n /* number of columns */,
00132   int  bx /* first index of row variables */,
00133   int  sx /* step of row variables */,
00134   int  by /* first index of column variables */,
00135   int  sy /* step of column variables */,
00136   int  pr /* verbosity level */)
00137 {
00138     DdNode *one, *zero;
00139     DdNode *w;
00140     DdNode *cubex, *cubey, *minterm1;
00141     int u, v, err, i, j, nv;
00142     double val;
00143     DdNode **lx, **ly, **lxn, **lyn;    /* local copies of x, y, xn, yn_ */
00144     int lnx, lny;                       /* local copies of nx and ny */
00145     char title[73], key[9], mxtype[4], rhstyp[4];
00146     int totcrd, ptrcrd, indcrd, valcrd, rhscrd,
00147         nrow, ncol, nnzero, neltvl,
00148         nrhs, nrhsix;
00149     int *colptr, *rowind;
00150 #if 0
00151     int nguess, nexact;
00152     int *rhsptr, *rhsind;
00153 #endif
00154 
00155     if (*nx < 0 || *ny < 0) return(0);
00156 
00157     one = DD_ONE(dd);
00158     zero = DD_ZERO(dd);
00159 
00160     /* Read the header */
00161     err = fscanf(fp, "%72c %8c", title, key);
00162     if (err == EOF) {
00163         return(0);
00164     } else if (err != 2) {
00165         return(0);
00166     }
00167     title[72] = (char) 0;
00168     key[8] = (char) 0;
00169 
00170     err = fscanf(fp, "%d %d %d %d %d", &totcrd, &ptrcrd, &indcrd,
00171     &valcrd, &rhscrd);
00172     if (err == EOF) {
00173         return(0);
00174     } else if (err != 5) {
00175         return(0);
00176     }
00177 
00178     err = fscanf(fp, "%3s %d %d %d %d", mxtype, &nrow, &ncol,
00179     &nnzero, &neltvl);
00180     if (err == EOF) {
00181         return(0);
00182     } else if (err != 5) {
00183         return(0);
00184     }
00185 
00186     /* Skip FORTRAN formats */
00187     if (rhscrd == 0) {
00188         err = fscanf(fp, "%*s %*s %*s \n");
00189     } else {
00190         err = fscanf(fp, "%*s %*s %*s %*s \n");
00191     }
00192     if (err == EOF) {
00193         return(0);
00194     } else if (err != 0) {
00195         return(0);
00196     }
00197 
00198     /* Print out some stuff if requested to be verbose */
00199     if (pr>0) {
00200         (void) fprintf(dd->out,"%s: type %s, %d rows, %d columns, %d entries\n", key,
00201         mxtype, nrow, ncol, nnzero);
00202         if (pr>1) (void) fprintf(dd->out,"%s\n", title);
00203     }
00204 
00205     /* Check matrix type */
00206     if (mxtype[0] != 'R' || mxtype[1] != 'U' || mxtype[2] != 'A') {
00207         (void) fprintf(dd->err,"%s: Illegal matrix type: %s\n",
00208                        key, mxtype);
00209         return(0);
00210     }
00211     if (neltvl != 0) return(0);
00212 
00213     /* Read optional 5-th line */
00214     if (rhscrd != 0) {
00215         err = fscanf(fp, "%3c %d %d", rhstyp, &nrhs, &nrhsix);
00216         if (err == EOF) {
00217             return(0);
00218         } else if (err != 3) {
00219             return(0);
00220         }
00221         rhstyp[3] = (char) 0;
00222         if (rhstyp[0] != 'F') {
00223             (void) fprintf(dd->err,
00224             "%s: Sparse right-hand side not yet supported\n", key);
00225             return(0);
00226         }
00227         if (pr>0) (void) fprintf(dd->out,"%d right-hand side(s)\n", nrhs);
00228     } else {
00229         nrhs = 0;
00230     }
00231 
00232     /* Compute the number of variables */
00233 
00234     /* row and column numbers start from 0 */
00235     u = nrow - 1;
00236     for (i=0; u > 0; i++) {
00237         u >>= 1;
00238     }
00239     lnx = i;
00240     if (nrhs == 0) {
00241         v = ncol - 1;
00242     } else {
00243         v = 2* (ddMax(ncol, nrhs) - 1);
00244     }
00245     for (i=0; v > 0; i++) {
00246         v >>= 1;
00247     }
00248     lny = i;
00249 
00250     /* Allocate or reallocate arrays for variables as needed */
00251     if (*nx == 0) {
00252         if (lnx > 0) {
00253             *x = lx = ALLOC(DdNode *,lnx);
00254             if (lx == NULL) {
00255                 dd->errorCode = CUDD_MEMORY_OUT;
00256                 return(0);
00257             }
00258             *xn = lxn =  ALLOC(DdNode *,lnx);
00259             if (lxn == NULL) {
00260                 dd->errorCode = CUDD_MEMORY_OUT;
00261                 return(0);
00262             }
00263         } else {
00264             *x = *xn = NULL;
00265         }
00266     } else if (lnx > *nx) {
00267         *x = lx = REALLOC(DdNode *, *x, lnx);
00268         if (lx == NULL) {
00269             dd->errorCode = CUDD_MEMORY_OUT;
00270             return(0);
00271         }
00272         *xn = lxn =  REALLOC(DdNode *, *xn, lnx);
00273         if (lxn == NULL) {
00274             dd->errorCode = CUDD_MEMORY_OUT;
00275             return(0);
00276         }
00277     } else {
00278         lx = *x;
00279         lxn = *xn;
00280     }
00281     if (*ny == 0) {
00282         if (lny >0) {
00283             *y = ly = ALLOC(DdNode *,lny);
00284             if (ly == NULL) {
00285                 dd->errorCode = CUDD_MEMORY_OUT;
00286                 return(0);
00287             }
00288             *yn_ = lyn = ALLOC(DdNode *,lny);
00289             if (lyn == NULL) {
00290                 dd->errorCode = CUDD_MEMORY_OUT;
00291                 return(0);
00292             }
00293         } else {
00294             *y = *yn_ = NULL;
00295         }
00296     } else if (lny > *ny) {
00297         *y = ly = REALLOC(DdNode *, *y, lny);
00298         if (ly == NULL) {
00299             dd->errorCode = CUDD_MEMORY_OUT;
00300             return(0);
00301         }
00302         *yn_ = lyn = REALLOC(DdNode *, *yn_, lny);
00303         if (lyn == NULL) {
00304             dd->errorCode = CUDD_MEMORY_OUT;
00305             return(0);
00306         }
00307     } else {
00308         ly = *y;
00309         lyn = *yn_;
00310     }
00311 
00312     /* Create new variables as needed */
00313     for (i= *nx,nv=bx+(*nx)*sx; i < lnx; i++,nv+=sx) {
00314         do {
00315             dd->reordered = 0;
00316             lx[i] = cuddUniqueInter(dd, nv, one, zero);
00317         } while (dd->reordered == 1);
00318         if (lx[i] == NULL) return(0);
00319         cuddRef(lx[i]);
00320         do {
00321             dd->reordered = 0;
00322             lxn[i] = cuddUniqueInter(dd, nv, zero, one);
00323         } while (dd->reordered == 1);
00324         if (lxn[i] == NULL) return(0);
00325         cuddRef(lxn[i]);
00326     }
00327     for (i= *ny,nv=by+(*ny)*sy; i < lny; i++,nv+=sy) {
00328         do {
00329             dd->reordered = 0;
00330             ly[i] = cuddUniqueInter(dd, nv, one, zero);
00331         } while (dd->reordered == 1);
00332         if (ly[i] == NULL) return(0);
00333         cuddRef(ly[i]);
00334         do {
00335             dd->reordered = 0;
00336             lyn[i] = cuddUniqueInter(dd, nv, zero, one);
00337         } while (dd->reordered == 1);
00338         if (lyn[i] == NULL) return(0);
00339         cuddRef(lyn[i]);
00340     }
00341 
00342     /* Update matrix parameters */
00343     *nx = lnx;
00344     *ny = lny;
00345     *m = nrow;
00346     if (nrhs == 0) {
00347         *n = ncol;
00348     } else {
00349         *n = (1 << (lny - 1)) + nrhs;
00350     }
00351     
00352     /* Read structure data */
00353     colptr = ALLOC(int, ncol+1);
00354     if (colptr == NULL) {
00355         dd->errorCode = CUDD_MEMORY_OUT;
00356         return(0);
00357     }
00358     rowind = ALLOC(int, nnzero);
00359     if (rowind == NULL) {
00360         dd->errorCode = CUDD_MEMORY_OUT;
00361         return(0);
00362     }
00363 
00364     for (i=0; i<ncol+1; i++) {
00365         err = fscanf(fp, " %d ", &u);
00366         if (err == EOF){ 
00367             FREE(colptr);
00368             FREE(rowind);
00369             return(0);
00370         } else if (err != 1) {
00371             FREE(colptr);
00372             FREE(rowind);
00373             return(0);
00374         }
00375         colptr[i] = u - 1;
00376     }
00377     if (colptr[0] != 0) {
00378         (void) fprintf(dd->err,"%s: Unexpected colptr[0] (%d)\n",
00379                        key,colptr[0]);
00380         FREE(colptr);
00381         FREE(rowind);
00382         return(0);
00383     }
00384     for (i=0; i<nnzero; i++) {
00385         err = fscanf(fp, " %d ", &u);
00386         if (err == EOF){ 
00387             FREE(colptr);
00388             FREE(rowind);
00389             return(0);
00390         } else if (err != 1) {
00391             FREE(colptr);
00392             FREE(rowind);
00393             return(0);
00394         }
00395         rowind[i] = u - 1;
00396     }
00397 
00398     *E = zero; cuddRef(*E);
00399 
00400     for (j=0; j<ncol; j++) {
00401         v = j;
00402         cubey = one; cuddRef(cubey);
00403         for (nv = lny - 1; nv>=0; nv--) {
00404             if (v & 1) {
00405                 w = Cudd_addApply(dd, Cudd_addTimes, cubey, ly[nv]);
00406             } else {
00407                 w = Cudd_addApply(dd, Cudd_addTimes, cubey, lyn[nv]);
00408             }
00409             if (w == NULL) {
00410                 Cudd_RecursiveDeref(dd, cubey);
00411                 FREE(colptr);
00412                 FREE(rowind);
00413                 return(0);
00414             }
00415             cuddRef(w);
00416             Cudd_RecursiveDeref(dd, cubey);
00417             cubey = w;
00418             v >>= 1;
00419         }
00420         for (i=colptr[j]; i<colptr[j+1]; i++) {
00421             u = rowind[i];
00422             err = fscanf(fp, " %lf ", &val);
00423             if (err == EOF || err != 1){ 
00424                 Cudd_RecursiveDeref(dd, cubey);
00425                 FREE(colptr);
00426                 FREE(rowind);
00427                 return(0);
00428             }
00429             /* Create new Constant node if necessary */
00430             cubex = cuddUniqueConst(dd, (CUDD_VALUE_TYPE) val);
00431             if (cubex == NULL) {
00432                 Cudd_RecursiveDeref(dd, cubey);
00433                 FREE(colptr);
00434                 FREE(rowind);
00435                 return(0);
00436             }
00437             cuddRef(cubex);
00438 
00439             for (nv = lnx - 1; nv>=0; nv--) {
00440                 if (u & 1) {
00441                     w = Cudd_addApply(dd, Cudd_addTimes, cubex, lx[nv]);
00442                 } else { 
00443                     w = Cudd_addApply(dd, Cudd_addTimes, cubex, lxn[nv]);
00444                 }
00445                 if (w == NULL) {
00446                     Cudd_RecursiveDeref(dd, cubey);
00447                     Cudd_RecursiveDeref(dd, cubex);
00448                     FREE(colptr);
00449                     FREE(rowind);
00450                     return(0);
00451                 }
00452                 cuddRef(w);
00453                 Cudd_RecursiveDeref(dd, cubex);
00454                 cubex = w;
00455                 u >>= 1;
00456             }
00457             minterm1 = Cudd_addApply(dd, Cudd_addTimes, cubey, cubex);
00458             if (minterm1 == NULL) {
00459                 Cudd_RecursiveDeref(dd, cubey);
00460                 Cudd_RecursiveDeref(dd, cubex);
00461                 FREE(colptr);
00462                 FREE(rowind);
00463                 return(0);
00464             }
00465             cuddRef(minterm1);
00466             Cudd_RecursiveDeref(dd, cubex);
00467             w = Cudd_addApply(dd, Cudd_addPlus, *E, minterm1);
00468             if (w == NULL) {
00469                 Cudd_RecursiveDeref(dd, cubey);
00470                 FREE(colptr);
00471                 FREE(rowind);
00472                 return(0);
00473             }
00474             cuddRef(w);
00475             Cudd_RecursiveDeref(dd, minterm1);
00476             Cudd_RecursiveDeref(dd, *E);
00477             *E = w;
00478         }
00479         Cudd_RecursiveDeref(dd, cubey);
00480     }
00481     FREE(colptr);
00482     FREE(rowind);
00483 
00484     /* Read right-hand sides */
00485     for (j=0; j<nrhs; j++) {
00486         v = j + (1<< (lny-1));
00487         cubey = one; cuddRef(cubey);
00488         for (nv = lny - 1; nv>=0; nv--) {
00489             if (v & 1) {
00490                 w = Cudd_addApply(dd, Cudd_addTimes, cubey, ly[nv]);
00491             } else {
00492                 w = Cudd_addApply(dd, Cudd_addTimes, cubey, lyn[nv]);
00493             }
00494             if (w == NULL) {
00495                 Cudd_RecursiveDeref(dd, cubey);
00496                 return(0);
00497             }
00498             cuddRef(w);
00499             Cudd_RecursiveDeref(dd, cubey);
00500             cubey = w;
00501             v >>= 1;
00502         }
00503         for (i=0; i<nrow; i++) {
00504             u = i;
00505             err = fscanf(fp, " %lf ", &val);
00506             if (err == EOF || err != 1){ 
00507                 Cudd_RecursiveDeref(dd, cubey);
00508                 return(0);
00509             }
00510             /* Create new Constant node if necessary */
00511             if (val == (double) 0.0) continue;
00512             cubex = cuddUniqueConst(dd, (CUDD_VALUE_TYPE) val);
00513             if (cubex == NULL) {
00514                 Cudd_RecursiveDeref(dd, cubey);
00515                 return(0);
00516             }
00517             cuddRef(cubex);
00518 
00519             for (nv = lnx - 1; nv>=0; nv--) {
00520                 if (u & 1) {
00521                    w = Cudd_addApply(dd, Cudd_addTimes, cubex, lx[nv]);
00522                 } else { 
00523                     w = Cudd_addApply(dd, Cudd_addTimes, cubex, lxn[nv]);
00524                 }
00525                 if (w == NULL) {
00526                     Cudd_RecursiveDeref(dd, cubey);
00527                     Cudd_RecursiveDeref(dd, cubex);
00528                     return(0);
00529                 }
00530                 cuddRef(w);
00531                 Cudd_RecursiveDeref(dd, cubex);
00532                 cubex = w;
00533                 u >>= 1;
00534             }
00535             minterm1 = Cudd_addApply(dd, Cudd_addTimes, cubey, cubex);
00536             if (minterm1 == NULL) {
00537                 Cudd_RecursiveDeref(dd, cubey);
00538                 Cudd_RecursiveDeref(dd, cubex);
00539                 return(0);
00540             }
00541             cuddRef(minterm1);
00542             Cudd_RecursiveDeref(dd, cubex);
00543             w = Cudd_addApply(dd, Cudd_addPlus, *E, minterm1);
00544             if (w == NULL) {
00545                 Cudd_RecursiveDeref(dd, cubey);
00546                 return(0);
00547             }
00548             cuddRef(w);
00549             Cudd_RecursiveDeref(dd, minterm1);
00550             Cudd_RecursiveDeref(dd, *E);
00551             *E = w;
00552         }
00553         Cudd_RecursiveDeref(dd, cubey);
00554     }
00555 
00556     return(1);
00557 
00558 } /* end of Cudd_addHarwell */
00559 
00560 
00561 /*---------------------------------------------------------------------------*/
00562 /* Definition of internal functions                                          */
00563 /*---------------------------------------------------------------------------*/
00564 
00565 /*---------------------------------------------------------------------------*/
00566 /* Definition of static functions                                            */
00567 /*---------------------------------------------------------------------------*/
00568