src/bdd/cudd/cuddHarwell.c File Reference

#include "util_hack.h"
#include "cuddInt.h"
Include dependency graph for cuddHarwell.c:

Go to the source code of this file.

Functions

int Cudd_addHarwell (FILE *fp, DdManager *dd, DdNode **E, DdNode ***x, DdNode ***y, DdNode ***xn, DdNode ***yn_, int *nx, int *ny, int *m, int *n, int bx, int sx, int by, int sy, int pr)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddHarwell.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $"

Function Documentation

int Cudd_addHarwell ( FILE *  fp,
DdManager *  dd,
DdNode **  E,
DdNode ***  x,
DdNode ***  y,
DdNode ***  xn,
DdNode ***  yn_,
int *  nx,
int *  ny,
int *  m,
int *  n,
int  bx,
int  sx,
int  by,
int  sy,
int  pr 
)

AutomaticStart AutomaticEnd Function********************************************************************

Synopsis [Reads in a matrix in the format of the Harwell-Boeing benchmark suite.]

Description [Reads in a matrix in the format of the Harwell-Boeing benchmark suite. The variables are ordered as follows: <blockquote> x\[0\] y\[0\] x\[1\] y\[1\] ... </blockquote> 0 is the most significant bit. On input, nx and ny hold the numbers of row and column variables already in existence. On output, they hold the numbers of row and column variables actually used by the matrix. m and n are set to the numbers of rows and columns of the matrix. Their values on input are immaterial. Returns 1 on success; 0 otherwise. The ADD for the sparse matrix is returned in E, and its reference count is > 0.]

SideEffects [None]

SeeAlso [Cudd_addRead Cudd_bddRead]

Definition at line 93 of file cuddHarwell.c.

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

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddHarwell.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $" [static]

CFile***********************************************************************

FileName [cuddHarwell.c]

PackageName [cudd]

Synopsis [Function to read a matrix in Harwell format.]

Description [External procedures included in this module:

]

Author [Fabio Somenzi]

Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]

Definition at line 47 of file cuddHarwell.c.

Generated on Tue Jan 5 12:18:54 2010 for abc70930 by  doxygen 1.6.1