[13] | 1 | /**CFile*********************************************************************** |
---|
| 2 | |
---|
| 3 | FileName [cuddHarwell.c] |
---|
| 4 | |
---|
| 5 | PackageName [cudd] |
---|
| 6 | |
---|
| 7 | Synopsis [Function to read a matrix in Harwell format.] |
---|
| 8 | |
---|
| 9 | Description [External procedures included in this module: |
---|
| 10 | <ul> |
---|
| 11 | <li> Cudd_addHarwell() |
---|
| 12 | </ul> |
---|
| 13 | ] |
---|
| 14 | |
---|
| 15 | Author [Fabio Somenzi] |
---|
| 16 | |
---|
| 17 | Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado |
---|
| 18 | |
---|
| 19 | All rights reserved. |
---|
| 20 | |
---|
| 21 | Redistribution and use in source and binary forms, with or without |
---|
| 22 | modification, are permitted provided that the following conditions |
---|
| 23 | are met: |
---|
| 24 | |
---|
| 25 | Redistributions of source code must retain the above copyright |
---|
| 26 | notice, this list of conditions and the following disclaimer. |
---|
| 27 | |
---|
| 28 | Redistributions in binary form must reproduce the above copyright |
---|
| 29 | notice, this list of conditions and the following disclaimer in the |
---|
| 30 | documentation and/or other materials provided with the distribution. |
---|
| 31 | |
---|
| 32 | Neither the name of the University of Colorado nor the names of its |
---|
| 33 | contributors may be used to endorse or promote products derived from |
---|
| 34 | this software without specific prior written permission. |
---|
| 35 | |
---|
| 36 | THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS |
---|
| 37 | "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT |
---|
| 38 | LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS |
---|
| 39 | FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE |
---|
| 40 | COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, |
---|
| 41 | INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, |
---|
| 42 | BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; |
---|
| 43 | LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER |
---|
| 44 | CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT |
---|
| 45 | LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN |
---|
| 46 | ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE |
---|
| 47 | POSSIBILITY OF SUCH DAMAGE.] |
---|
| 48 | |
---|
| 49 | ******************************************************************************/ |
---|
| 50 | |
---|
| 51 | #include "util.h" |
---|
| 52 | #include "cuddInt.h" |
---|
| 53 | |
---|
| 54 | /*---------------------------------------------------------------------------*/ |
---|
| 55 | /* Constant declarations */ |
---|
| 56 | /*---------------------------------------------------------------------------*/ |
---|
| 57 | |
---|
| 58 | |
---|
| 59 | /*---------------------------------------------------------------------------*/ |
---|
| 60 | /* Stucture declarations */ |
---|
| 61 | /*---------------------------------------------------------------------------*/ |
---|
| 62 | |
---|
| 63 | |
---|
| 64 | /*---------------------------------------------------------------------------*/ |
---|
| 65 | /* Type declarations */ |
---|
| 66 | /*---------------------------------------------------------------------------*/ |
---|
| 67 | |
---|
| 68 | |
---|
| 69 | /*---------------------------------------------------------------------------*/ |
---|
| 70 | /* Variable declarations */ |
---|
| 71 | /*---------------------------------------------------------------------------*/ |
---|
| 72 | |
---|
| 73 | #ifndef lint |
---|
| 74 | static char rcsid[] DD_UNUSED = "$Id: cuddHarwell.c,v 1.9 2004/08/13 18:04:49 fabio Exp $"; |
---|
| 75 | #endif |
---|
| 76 | |
---|
| 77 | /*---------------------------------------------------------------------------*/ |
---|
| 78 | /* Macro declarations */ |
---|
| 79 | /*---------------------------------------------------------------------------*/ |
---|
| 80 | |
---|
| 81 | |
---|
| 82 | /**AutomaticStart*************************************************************/ |
---|
| 83 | |
---|
| 84 | /*---------------------------------------------------------------------------*/ |
---|
| 85 | /* Static function prototypes */ |
---|
| 86 | /*---------------------------------------------------------------------------*/ |
---|
| 87 | |
---|
| 88 | |
---|
| 89 | /**AutomaticEnd***************************************************************/ |
---|
| 90 | |
---|
| 91 | |
---|
| 92 | /*---------------------------------------------------------------------------*/ |
---|
| 93 | /* Definition of exported functions */ |
---|
| 94 | /*---------------------------------------------------------------------------*/ |
---|
| 95 | |
---|
| 96 | /**Function******************************************************************** |
---|
| 97 | |
---|
| 98 | Synopsis [Reads in a matrix in the format of the Harwell-Boeing |
---|
| 99 | benchmark suite.] |
---|
| 100 | |
---|
| 101 | Description [Reads in a matrix in the format of the Harwell-Boeing |
---|
| 102 | benchmark suite. The variables are ordered as follows: |
---|
| 103 | <blockquote> |
---|
| 104 | x\[0\] y\[0\] x\[1\] y\[1\] ... |
---|
| 105 | </blockquote> |
---|
| 106 | 0 is the most significant bit. On input, nx and ny hold the numbers |
---|
| 107 | of row and column variables already in existence. On output, they |
---|
| 108 | hold the numbers of row and column variables actually used by the |
---|
| 109 | matrix. m and n are set to the numbers of rows and columns of the |
---|
| 110 | matrix. Their values on input are immaterial. Returns 1 on |
---|
| 111 | success; 0 otherwise. The ADD for the sparse matrix is returned in |
---|
| 112 | E, and its reference count is > 0.] |
---|
| 113 | |
---|
| 114 | SideEffects [None] |
---|
| 115 | |
---|
| 116 | SeeAlso [Cudd_addRead Cudd_bddRead] |
---|
| 117 | |
---|
| 118 | ******************************************************************************/ |
---|
| 119 | int |
---|
| 120 | Cudd_addHarwell( |
---|
| 121 | FILE * fp /* pointer to the input file */, |
---|
| 122 | DdManager * dd /* DD manager */, |
---|
| 123 | DdNode ** E /* characteristic function of the graph */, |
---|
| 124 | DdNode *** x /* array of row variables */, |
---|
| 125 | DdNode *** y /* array of column variables */, |
---|
| 126 | DdNode *** xn /* array of complemented row variables */, |
---|
| 127 | DdNode *** yn_ /* array of complemented column variables */, |
---|
| 128 | int * nx /* number or row variables */, |
---|
| 129 | int * ny /* number or column variables */, |
---|
| 130 | int * m /* number of rows */, |
---|
| 131 | int * n /* number of columns */, |
---|
| 132 | int bx /* first index of row variables */, |
---|
| 133 | int sx /* step of row variables */, |
---|
| 134 | int by /* first index of column variables */, |
---|
| 135 | int sy /* step of column variables */, |
---|
| 136 | int pr /* verbosity level */) |
---|
| 137 | { |
---|
| 138 | DdNode *one, *zero; |
---|
| 139 | DdNode *w; |
---|
| 140 | DdNode *cubex, *cubey, *minterm1; |
---|
| 141 | int u, v, err, i, j, nv; |
---|
| 142 | double val; |
---|
| 143 | DdNode **lx, **ly, **lxn, **lyn; /* local copies of x, y, xn, yn_ */ |
---|
| 144 | int lnx, lny; /* local copies of nx and ny */ |
---|
| 145 | char title[73], key[9], mxtype[4], rhstyp[4]; |
---|
| 146 | int totcrd, ptrcrd, indcrd, valcrd, rhscrd, |
---|
| 147 | nrow, ncol, nnzero, neltvl, |
---|
| 148 | nrhs, nrhsix; |
---|
| 149 | int *colptr, *rowind; |
---|
| 150 | #if 0 |
---|
| 151 | int nguess, nexact; |
---|
| 152 | int *rhsptr, *rhsind; |
---|
| 153 | #endif |
---|
| 154 | |
---|
| 155 | if (*nx < 0 || *ny < 0) return(0); |
---|
| 156 | |
---|
| 157 | one = DD_ONE(dd); |
---|
| 158 | zero = DD_ZERO(dd); |
---|
| 159 | |
---|
| 160 | /* Read the header */ |
---|
| 161 | err = fscanf(fp, "%72c %8c", title, key); |
---|
| 162 | if (err == EOF) { |
---|
| 163 | return(0); |
---|
| 164 | } else if (err != 2) { |
---|
| 165 | return(0); |
---|
| 166 | } |
---|
| 167 | title[72] = (char) 0; |
---|
| 168 | key[8] = (char) 0; |
---|
| 169 | |
---|
| 170 | err = fscanf(fp, "%d %d %d %d %d", &totcrd, &ptrcrd, &indcrd, |
---|
| 171 | &valcrd, &rhscrd); |
---|
| 172 | if (err == EOF) { |
---|
| 173 | return(0); |
---|
| 174 | } else if (err != 5) { |
---|
| 175 | return(0); |
---|
| 176 | } |
---|
| 177 | |
---|
| 178 | err = fscanf(fp, "%3s %d %d %d %d", mxtype, &nrow, &ncol, |
---|
| 179 | &nnzero, &neltvl); |
---|
| 180 | if (err == EOF) { |
---|
| 181 | return(0); |
---|
| 182 | } else if (err != 5) { |
---|
| 183 | return(0); |
---|
| 184 | } |
---|
| 185 | |
---|
| 186 | /* Skip FORTRAN formats */ |
---|
| 187 | if (rhscrd == 0) { |
---|
| 188 | err = fscanf(fp, "%*s %*s %*s \n"); |
---|
| 189 | } else { |
---|
| 190 | err = fscanf(fp, "%*s %*s %*s %*s \n"); |
---|
| 191 | } |
---|
| 192 | if (err == EOF) { |
---|
| 193 | return(0); |
---|
| 194 | } else if (err != 0) { |
---|
| 195 | return(0); |
---|
| 196 | } |
---|
| 197 | |
---|
| 198 | /* Print out some stuff if requested to be verbose */ |
---|
| 199 | if (pr>0) { |
---|
| 200 | (void) fprintf(dd->out,"%s: type %s, %d rows, %d columns, %d entries\n", key, |
---|
| 201 | mxtype, nrow, ncol, nnzero); |
---|
| 202 | if (pr>1) (void) fprintf(dd->out,"%s\n", title); |
---|
| 203 | } |
---|
| 204 | |
---|
| 205 | /* Check matrix type */ |
---|
| 206 | if (mxtype[0] != 'R' || mxtype[1] != 'U' || mxtype[2] != 'A') { |
---|
| 207 | (void) fprintf(dd->err,"%s: Illegal matrix type: %s\n", |
---|
| 208 | key, mxtype); |
---|
| 209 | return(0); |
---|
| 210 | } |
---|
| 211 | if (neltvl != 0) return(0); |
---|
| 212 | |
---|
| 213 | /* Read optional 5-th line */ |
---|
| 214 | if (rhscrd != 0) { |
---|
| 215 | err = fscanf(fp, "%3c %d %d", rhstyp, &nrhs, &nrhsix); |
---|
| 216 | if (err == EOF) { |
---|
| 217 | return(0); |
---|
| 218 | } else if (err != 3) { |
---|
| 219 | return(0); |
---|
| 220 | } |
---|
| 221 | rhstyp[3] = (char) 0; |
---|
| 222 | if (rhstyp[0] != 'F') { |
---|
| 223 | (void) fprintf(dd->err, |
---|
| 224 | "%s: Sparse right-hand side not yet supported\n", key); |
---|
| 225 | return(0); |
---|
| 226 | } |
---|
| 227 | if (pr>0) (void) fprintf(dd->out,"%d right-hand side(s)\n", nrhs); |
---|
| 228 | } else { |
---|
| 229 | nrhs = 0; |
---|
| 230 | } |
---|
| 231 | |
---|
| 232 | /* Compute the number of variables */ |
---|
| 233 | |
---|
| 234 | /* row and column numbers start from 0 */ |
---|
| 235 | u = nrow - 1; |
---|
| 236 | for (i=0; u > 0; i++) { |
---|
| 237 | u >>= 1; |
---|
| 238 | } |
---|
| 239 | lnx = i; |
---|
| 240 | if (nrhs == 0) { |
---|
| 241 | v = ncol - 1; |
---|
| 242 | } else { |
---|
| 243 | v = 2* (ddMax(ncol, nrhs) - 1); |
---|
| 244 | } |
---|
| 245 | for (i=0; v > 0; i++) { |
---|
| 246 | v >>= 1; |
---|
| 247 | } |
---|
| 248 | lny = i; |
---|
| 249 | |
---|
| 250 | /* Allocate or reallocate arrays for variables as needed */ |
---|
| 251 | if (*nx == 0) { |
---|
| 252 | if (lnx > 0) { |
---|
| 253 | *x = lx = ALLOC(DdNode *,lnx); |
---|
| 254 | if (lx == NULL) { |
---|
| 255 | dd->errorCode = CUDD_MEMORY_OUT; |
---|
| 256 | return(0); |
---|
| 257 | } |
---|
| 258 | *xn = lxn = ALLOC(DdNode *,lnx); |
---|
| 259 | if (lxn == NULL) { |
---|
| 260 | dd->errorCode = CUDD_MEMORY_OUT; |
---|
| 261 | return(0); |
---|
| 262 | } |
---|
| 263 | } else { |
---|
| 264 | *x = *xn = NULL; |
---|
| 265 | } |
---|
| 266 | } else if (lnx > *nx) { |
---|
| 267 | *x = lx = REALLOC(DdNode *, *x, lnx); |
---|
| 268 | if (lx == NULL) { |
---|
| 269 | dd->errorCode = CUDD_MEMORY_OUT; |
---|
| 270 | return(0); |
---|
| 271 | } |
---|
| 272 | *xn = lxn = REALLOC(DdNode *, *xn, lnx); |
---|
| 273 | if (lxn == NULL) { |
---|
| 274 | dd->errorCode = CUDD_MEMORY_OUT; |
---|
| 275 | return(0); |
---|
| 276 | } |
---|
| 277 | } else { |
---|
| 278 | lx = *x; |
---|
| 279 | lxn = *xn; |
---|
| 280 | } |
---|
| 281 | if (*ny == 0) { |
---|
| 282 | if (lny >0) { |
---|
| 283 | *y = ly = ALLOC(DdNode *,lny); |
---|
| 284 | if (ly == NULL) { |
---|
| 285 | dd->errorCode = CUDD_MEMORY_OUT; |
---|
| 286 | return(0); |
---|
| 287 | } |
---|
| 288 | *yn_ = lyn = ALLOC(DdNode *,lny); |
---|
| 289 | if (lyn == NULL) { |
---|
| 290 | dd->errorCode = CUDD_MEMORY_OUT; |
---|
| 291 | return(0); |
---|
| 292 | } |
---|
| 293 | } else { |
---|
| 294 | *y = *yn_ = NULL; |
---|
| 295 | } |
---|
| 296 | } else if (lny > *ny) { |
---|
| 297 | *y = ly = REALLOC(DdNode *, *y, lny); |
---|
| 298 | if (ly == NULL) { |
---|
| 299 | dd->errorCode = CUDD_MEMORY_OUT; |
---|
| 300 | return(0); |
---|
| 301 | } |
---|
| 302 | *yn_ = lyn = REALLOC(DdNode *, *yn_, lny); |
---|
| 303 | if (lyn == NULL) { |
---|
| 304 | dd->errorCode = CUDD_MEMORY_OUT; |
---|
| 305 | return(0); |
---|
| 306 | } |
---|
| 307 | } else { |
---|
| 308 | ly = *y; |
---|
| 309 | lyn = *yn_; |
---|
| 310 | } |
---|
| 311 | |
---|
| 312 | /* Create new variables as needed */ |
---|
| 313 | for (i= *nx,nv=bx+(*nx)*sx; i < lnx; i++,nv+=sx) { |
---|
| 314 | do { |
---|
| 315 | dd->reordered = 0; |
---|
| 316 | lx[i] = cuddUniqueInter(dd, nv, one, zero); |
---|
| 317 | } while (dd->reordered == 1); |
---|
| 318 | if (lx[i] == NULL) return(0); |
---|
| 319 | cuddRef(lx[i]); |
---|
| 320 | do { |
---|
| 321 | dd->reordered = 0; |
---|
| 322 | lxn[i] = cuddUniqueInter(dd, nv, zero, one); |
---|
| 323 | } while (dd->reordered == 1); |
---|
| 324 | if (lxn[i] == NULL) return(0); |
---|
| 325 | cuddRef(lxn[i]); |
---|
| 326 | } |
---|
| 327 | for (i= *ny,nv=by+(*ny)*sy; i < lny; i++,nv+=sy) { |
---|
| 328 | do { |
---|
| 329 | dd->reordered = 0; |
---|
| 330 | ly[i] = cuddUniqueInter(dd, nv, one, zero); |
---|
| 331 | } while (dd->reordered == 1); |
---|
| 332 | if (ly[i] == NULL) return(0); |
---|
| 333 | cuddRef(ly[i]); |
---|
| 334 | do { |
---|
| 335 | dd->reordered = 0; |
---|
| 336 | lyn[i] = cuddUniqueInter(dd, nv, zero, one); |
---|
| 337 | } while (dd->reordered == 1); |
---|
| 338 | if (lyn[i] == NULL) return(0); |
---|
| 339 | cuddRef(lyn[i]); |
---|
| 340 | } |
---|
| 341 | |
---|
| 342 | /* Update matrix parameters */ |
---|
| 343 | *nx = lnx; |
---|
| 344 | *ny = lny; |
---|
| 345 | *m = nrow; |
---|
| 346 | if (nrhs == 0) { |
---|
| 347 | *n = ncol; |
---|
| 348 | } else { |
---|
| 349 | *n = (1 << (lny - 1)) + nrhs; |
---|
| 350 | } |
---|
| 351 | |
---|
| 352 | /* Read structure data */ |
---|
| 353 | colptr = ALLOC(int, ncol+1); |
---|
| 354 | if (colptr == NULL) { |
---|
| 355 | dd->errorCode = CUDD_MEMORY_OUT; |
---|
| 356 | return(0); |
---|
| 357 | } |
---|
| 358 | rowind = ALLOC(int, nnzero); |
---|
| 359 | if (rowind == NULL) { |
---|
| 360 | dd->errorCode = CUDD_MEMORY_OUT; |
---|
| 361 | return(0); |
---|
| 362 | } |
---|
| 363 | |
---|
| 364 | for (i=0; i<ncol+1; i++) { |
---|
| 365 | err = fscanf(fp, " %d ", &u); |
---|
| 366 | if (err == EOF){ |
---|
| 367 | FREE(colptr); |
---|
| 368 | FREE(rowind); |
---|
| 369 | return(0); |
---|
| 370 | } else if (err != 1) { |
---|
| 371 | FREE(colptr); |
---|
| 372 | FREE(rowind); |
---|
| 373 | return(0); |
---|
| 374 | } |
---|
| 375 | colptr[i] = u - 1; |
---|
| 376 | } |
---|
| 377 | if (colptr[0] != 0) { |
---|
| 378 | (void) fprintf(dd->err,"%s: Unexpected colptr[0] (%d)\n", |
---|
| 379 | key,colptr[0]); |
---|
| 380 | FREE(colptr); |
---|
| 381 | FREE(rowind); |
---|
| 382 | return(0); |
---|
| 383 | } |
---|
| 384 | for (i=0; i<nnzero; i++) { |
---|
| 385 | err = fscanf(fp, " %d ", &u); |
---|
| 386 | if (err == EOF){ |
---|
| 387 | FREE(colptr); |
---|
| 388 | FREE(rowind); |
---|
| 389 | return(0); |
---|
| 390 | } else if (err != 1) { |
---|
| 391 | FREE(colptr); |
---|
| 392 | FREE(rowind); |
---|
| 393 | return(0); |
---|
| 394 | } |
---|
| 395 | rowind[i] = u - 1; |
---|
| 396 | } |
---|
| 397 | |
---|
| 398 | *E = zero; cuddRef(*E); |
---|
| 399 | |
---|
| 400 | for (j=0; j<ncol; j++) { |
---|
| 401 | v = j; |
---|
| 402 | cubey = one; cuddRef(cubey); |
---|
| 403 | for (nv = lny - 1; nv>=0; nv--) { |
---|
| 404 | if (v & 1) { |
---|
| 405 | w = Cudd_addApply(dd, Cudd_addTimes, cubey, ly[nv]); |
---|
| 406 | } else { |
---|
| 407 | w = Cudd_addApply(dd, Cudd_addTimes, cubey, lyn[nv]); |
---|
| 408 | } |
---|
| 409 | if (w == NULL) { |
---|
| 410 | Cudd_RecursiveDeref(dd, cubey); |
---|
| 411 | FREE(colptr); |
---|
| 412 | FREE(rowind); |
---|
| 413 | return(0); |
---|
| 414 | } |
---|
| 415 | cuddRef(w); |
---|
| 416 | Cudd_RecursiveDeref(dd, cubey); |
---|
| 417 | cubey = w; |
---|
| 418 | v >>= 1; |
---|
| 419 | } |
---|
| 420 | for (i=colptr[j]; i<colptr[j+1]; i++) { |
---|
| 421 | u = rowind[i]; |
---|
| 422 | err = fscanf(fp, " %lf ", &val); |
---|
| 423 | if (err == EOF || err != 1){ |
---|
| 424 | Cudd_RecursiveDeref(dd, cubey); |
---|
| 425 | FREE(colptr); |
---|
| 426 | FREE(rowind); |
---|
| 427 | return(0); |
---|
| 428 | } |
---|
| 429 | /* Create new Constant node if necessary */ |
---|
| 430 | cubex = cuddUniqueConst(dd, (CUDD_VALUE_TYPE) val); |
---|
| 431 | if (cubex == NULL) { |
---|
| 432 | Cudd_RecursiveDeref(dd, cubey); |
---|
| 433 | FREE(colptr); |
---|
| 434 | FREE(rowind); |
---|
| 435 | return(0); |
---|
| 436 | } |
---|
| 437 | cuddRef(cubex); |
---|
| 438 | |
---|
| 439 | for (nv = lnx - 1; nv>=0; nv--) { |
---|
| 440 | if (u & 1) { |
---|
| 441 | w = Cudd_addApply(dd, Cudd_addTimes, cubex, lx[nv]); |
---|
| 442 | } else { |
---|
| 443 | w = Cudd_addApply(dd, Cudd_addTimes, cubex, lxn[nv]); |
---|
| 444 | } |
---|
| 445 | if (w == NULL) { |
---|
| 446 | Cudd_RecursiveDeref(dd, cubey); |
---|
| 447 | Cudd_RecursiveDeref(dd, cubex); |
---|
| 448 | FREE(colptr); |
---|
| 449 | FREE(rowind); |
---|
| 450 | return(0); |
---|
| 451 | } |
---|
| 452 | cuddRef(w); |
---|
| 453 | Cudd_RecursiveDeref(dd, cubex); |
---|
| 454 | cubex = w; |
---|
| 455 | u >>= 1; |
---|
| 456 | } |
---|
| 457 | minterm1 = Cudd_addApply(dd, Cudd_addTimes, cubey, cubex); |
---|
| 458 | if (minterm1 == NULL) { |
---|
| 459 | Cudd_RecursiveDeref(dd, cubey); |
---|
| 460 | Cudd_RecursiveDeref(dd, cubex); |
---|
| 461 | FREE(colptr); |
---|
| 462 | FREE(rowind); |
---|
| 463 | return(0); |
---|
| 464 | } |
---|
| 465 | cuddRef(minterm1); |
---|
| 466 | Cudd_RecursiveDeref(dd, cubex); |
---|
| 467 | w = Cudd_addApply(dd, Cudd_addPlus, *E, minterm1); |
---|
| 468 | if (w == NULL) { |
---|
| 469 | Cudd_RecursiveDeref(dd, cubey); |
---|
| 470 | FREE(colptr); |
---|
| 471 | FREE(rowind); |
---|
| 472 | return(0); |
---|
| 473 | } |
---|
| 474 | cuddRef(w); |
---|
| 475 | Cudd_RecursiveDeref(dd, minterm1); |
---|
| 476 | Cudd_RecursiveDeref(dd, *E); |
---|
| 477 | *E = w; |
---|
| 478 | } |
---|
| 479 | Cudd_RecursiveDeref(dd, cubey); |
---|
| 480 | } |
---|
| 481 | FREE(colptr); |
---|
| 482 | FREE(rowind); |
---|
| 483 | |
---|
| 484 | /* Read right-hand sides */ |
---|
| 485 | for (j=0; j<nrhs; j++) { |
---|
| 486 | v = j + (1<< (lny-1)); |
---|
| 487 | cubey = one; cuddRef(cubey); |
---|
| 488 | for (nv = lny - 1; nv>=0; nv--) { |
---|
| 489 | if (v & 1) { |
---|
| 490 | w = Cudd_addApply(dd, Cudd_addTimes, cubey, ly[nv]); |
---|
| 491 | } else { |
---|
| 492 | w = Cudd_addApply(dd, Cudd_addTimes, cubey, lyn[nv]); |
---|
| 493 | } |
---|
| 494 | if (w == NULL) { |
---|
| 495 | Cudd_RecursiveDeref(dd, cubey); |
---|
| 496 | return(0); |
---|
| 497 | } |
---|
| 498 | cuddRef(w); |
---|
| 499 | Cudd_RecursiveDeref(dd, cubey); |
---|
| 500 | cubey = w; |
---|
| 501 | v >>= 1; |
---|
| 502 | } |
---|
| 503 | for (i=0; i<nrow; i++) { |
---|
| 504 | u = i; |
---|
| 505 | err = fscanf(fp, " %lf ", &val); |
---|
| 506 | if (err == EOF || err != 1){ |
---|
| 507 | Cudd_RecursiveDeref(dd, cubey); |
---|
| 508 | return(0); |
---|
| 509 | } |
---|
| 510 | /* Create new Constant node if necessary */ |
---|
| 511 | if (val == (double) 0.0) continue; |
---|
| 512 | cubex = cuddUniqueConst(dd, (CUDD_VALUE_TYPE) val); |
---|
| 513 | if (cubex == NULL) { |
---|
| 514 | Cudd_RecursiveDeref(dd, cubey); |
---|
| 515 | return(0); |
---|
| 516 | } |
---|
| 517 | cuddRef(cubex); |
---|
| 518 | |
---|
| 519 | for (nv = lnx - 1; nv>=0; nv--) { |
---|
| 520 | if (u & 1) { |
---|
| 521 | w = Cudd_addApply(dd, Cudd_addTimes, cubex, lx[nv]); |
---|
| 522 | } else { |
---|
| 523 | w = Cudd_addApply(dd, Cudd_addTimes, cubex, lxn[nv]); |
---|
| 524 | } |
---|
| 525 | if (w == NULL) { |
---|
| 526 | Cudd_RecursiveDeref(dd, cubey); |
---|
| 527 | Cudd_RecursiveDeref(dd, cubex); |
---|
| 528 | return(0); |
---|
| 529 | } |
---|
| 530 | cuddRef(w); |
---|
| 531 | Cudd_RecursiveDeref(dd, cubex); |
---|
| 532 | cubex = w; |
---|
| 533 | u >>= 1; |
---|
| 534 | } |
---|
| 535 | minterm1 = Cudd_addApply(dd, Cudd_addTimes, cubey, cubex); |
---|
| 536 | if (minterm1 == NULL) { |
---|
| 537 | Cudd_RecursiveDeref(dd, cubey); |
---|
| 538 | Cudd_RecursiveDeref(dd, cubex); |
---|
| 539 | return(0); |
---|
| 540 | } |
---|
| 541 | cuddRef(minterm1); |
---|
| 542 | Cudd_RecursiveDeref(dd, cubex); |
---|
| 543 | w = Cudd_addApply(dd, Cudd_addPlus, *E, minterm1); |
---|
| 544 | if (w == NULL) { |
---|
| 545 | Cudd_RecursiveDeref(dd, cubey); |
---|
| 546 | return(0); |
---|
| 547 | } |
---|
| 548 | cuddRef(w); |
---|
| 549 | Cudd_RecursiveDeref(dd, minterm1); |
---|
| 550 | Cudd_RecursiveDeref(dd, *E); |
---|
| 551 | *E = w; |
---|
| 552 | } |
---|
| 553 | Cudd_RecursiveDeref(dd, cubey); |
---|
| 554 | } |
---|
| 555 | |
---|
| 556 | return(1); |
---|
| 557 | |
---|
| 558 | } /* end of Cudd_addHarwell */ |
---|
| 559 | |
---|
| 560 | |
---|
| 561 | /*---------------------------------------------------------------------------*/ |
---|
| 562 | /* Definition of internal functions */ |
---|
| 563 | /*---------------------------------------------------------------------------*/ |
---|
| 564 | |
---|
| 565 | /*---------------------------------------------------------------------------*/ |
---|
| 566 | /* Definition of static functions */ |
---|
| 567 | /*---------------------------------------------------------------------------*/ |
---|
| 568 | |
---|