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 | |
---|