1 /**CFile***********************************************************************
2
3 FileName [cuddRead.c]
4
5 PackageName [cudd]
6
7 Synopsis [Functions to read in a matrix]
8
9 Description [External procedures included in this module:
10 <ul>
11 <li> Cudd_addRead()
12 <li> Cudd_bddRead()
13 </ul>]
14
15 SeeAlso [cudd_addHarwell.c]
16
17 Author [Fabio Somenzi]
18
19 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
20
21 All rights reserved.
22
23 Redistribution and use in source and binary forms, with or without
24 modification, are permitted provided that the following conditions
25 are met:
26
27 Redistributions of source code must retain the above copyright
28 notice, this list of conditions and the following disclaimer.
29
30 Redistributions in binary form must reproduce the above copyright
31 notice, this list of conditions and the following disclaimer in the
32 documentation and/or other materials provided with the distribution.
33
34 Neither the name of the University of Colorado nor the names of its
35 contributors may be used to endorse or promote products derived from
36 this software without specific prior written permission.
37
38 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
39 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
40 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
41 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
42 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
43 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
44 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
45 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
46 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
47 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
48 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
49 POSSIBILITY OF SUCH DAMAGE.]
50
51 ******************************************************************************/
52
53 #include "misc/util/util_hack.h"
54 #include "cuddInt.h"
55
56 ABC_NAMESPACE_IMPL_START
57
58
59
60
61 /*---------------------------------------------------------------------------*/
62 /* Constant declarations */
63 /*---------------------------------------------------------------------------*/
64
65
66 /*---------------------------------------------------------------------------*/
67 /* Stucture declarations */
68 /*---------------------------------------------------------------------------*/
69
70
71 /*---------------------------------------------------------------------------*/
72 /* Type declarations */
73 /*---------------------------------------------------------------------------*/
74
75
76 /*---------------------------------------------------------------------------*/
77 /* Variable declarations */
78 /*---------------------------------------------------------------------------*/
79
80 #ifndef lint
81 static char rcsid[] DD_UNUSED = "$Id: cuddRead.c,v 1.6 2004/08/13 18:04:50 fabio Exp $";
82 #endif
83
84 /*---------------------------------------------------------------------------*/
85 /* Macro declarations */
86 /*---------------------------------------------------------------------------*/
87
88
89 /**AutomaticStart*************************************************************/
90
91 /*---------------------------------------------------------------------------*/
92 /* Static function prototypes */
93 /*---------------------------------------------------------------------------*/
94
95
96 /**AutomaticEnd***************************************************************/
97
98
99 /*---------------------------------------------------------------------------*/
100 /* Definition of exported functions */
101 /*---------------------------------------------------------------------------*/
102
103
104 /**Function********************************************************************
105
106 Synopsis [Reads in a sparse matrix.]
107
108 Description [Reads in a sparse matrix specified in a simple format.
109 The first line of the input contains the numbers of rows and columns.
110 The remaining lines contain the elements of the matrix, one per line.
111 Given a background value
112 (specified by the background field of the manager), only the values
113 different from it are explicitly listed. Each foreground element is
114 described by two integers, i.e., the row and column number, and a
115 real number, i.e., the value.<p>
116 Cudd_addRead produces an ADD that depends on two sets of variables: x
117 and y. The x variables (x\[0\] ... x\[nx-1\]) encode the row index and
118 the y variables (y\[0\] ... y\[ny-1\]) encode the column index.
119 x\[0\] and y\[0\] are the most significant bits in the indices.
120 The variables may already exist or may be created by the function.
121 The index of x\[i\] is bx+i*sx, and the index of y\[i\] is by+i*sy.<p>
122 On input, nx and ny hold the numbers
123 of row and column variables already in existence. On output, they
124 hold the numbers of row and column variables actually used by the
125 matrix. When Cudd_addRead creates the variable arrays,
126 the index of x\[i\] is bx+i*sx, and the index of y\[i\] is by+i*sy.
127 When some variables already exist Cudd_addRead expects the indices
128 of the existing x variables to be bx+i*sx, and the indices of the
129 existing y variables to be by+i*sy.<p>
130 m and n are set to the numbers of rows and columns of the
131 matrix. Their values on input are immaterial.
132 The ADD for the
133 sparse matrix is returned in E, and its reference count is > 0.
134 Cudd_addRead returns 1 in case of success; 0 otherwise.]
135
136 SideEffects [nx and ny are set to the numbers of row and column
137 variables. m and n are set to the numbers of rows and columns. x and y
138 are possibly extended to represent the array of row and column
139 variables. Similarly for xn and yn_, which hold on return from
140 Cudd_addRead the complements of the row and column variables.]
141
142 SeeAlso [Cudd_addHarwell Cudd_bddRead]
143
144 ******************************************************************************/
145 int
Cudd_addRead(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)146 Cudd_addRead(
147 FILE * fp /* input file pointer */,
148 DdManager * dd /* DD manager */,
149 DdNode ** E /* characteristic function of the graph */,
150 DdNode *** x /* array of row variables */,
151 DdNode *** y /* array of column variables */,
152 DdNode *** xn /* array of complemented row variables */,
153 DdNode *** yn_ /* array of complemented column variables */,
154 int * nx /* number or row variables */,
155 int * ny /* number or column variables */,
156 int * m /* number of rows */,
157 int * n /* number of columns */,
158 int bx /* first index of row variables */,
159 int sx /* step of row variables */,
160 int by /* first index of column variables */,
161 int sy /* step of column variables */)
162 {
163 DdNode *one, *zero;
164 DdNode *w, *neW;
165 DdNode *minterm1;
166 int u, v, err, i, nv;
167 int lnx, lny;
168 CUDD_VALUE_TYPE val;
169 DdNode **lx, **ly, **lxn, **lyn;
170
171 one = DD_ONE(dd);
172 zero = DD_ZERO(dd);
173
174 err = fscanf(fp, "%d %d", &u, &v);
175 if (err == EOF) {
176 return(0);
177 } else if (err != 2) {
178 return(0);
179 }
180
181 *m = u;
182 /* Compute the number of x variables. */
183 lx = *x; lxn = *xn;
184 u--; /* row and column numbers start from 0 */
185 for (lnx=0; u > 0; lnx++) {
186 u >>= 1;
187 }
188 /* Here we rely on the fact that REALLOC of a null pointer is
189 ** translates to an ALLOC.
190 */
191 if (lnx > *nx) {
192 *x = lx = ABC_REALLOC(DdNode *, *x, lnx);
193 if (lx == NULL) {
194 dd->errorCode = CUDD_MEMORY_OUT;
195 return(0);
196 }
197 *xn = lxn = ABC_REALLOC(DdNode *, *xn, lnx);
198 if (lxn == NULL) {
199 dd->errorCode = CUDD_MEMORY_OUT;
200 return(0);
201 }
202 }
203
204 *n = v;
205 /* Compute the number of y variables. */
206 ly = *y; lyn = *yn_;
207 v--; /* row and column numbers start from 0 */
208 for (lny=0; v > 0; lny++) {
209 v >>= 1;
210 }
211 /* Here we rely on the fact that REALLOC of a null pointer is
212 ** translates to an ALLOC.
213 */
214 if (lny > *ny) {
215 *y = ly = ABC_REALLOC(DdNode *, *y, lny);
216 if (ly == NULL) {
217 dd->errorCode = CUDD_MEMORY_OUT;
218 return(0);
219 }
220 *yn_ = lyn = ABC_REALLOC(DdNode *, *yn_, lny);
221 if (lyn == NULL) {
222 dd->errorCode = CUDD_MEMORY_OUT;
223 return(0);
224 }
225 }
226
227 /* Create all new variables. */
228 for (i = *nx, nv = bx + (*nx) * sx; i < lnx; i++, nv += sx) {
229 do {
230 dd->reordered = 0;
231 lx[i] = cuddUniqueInter(dd, nv, one, zero);
232 } while (dd->reordered == 1);
233 if (lx[i] == NULL) return(0);
234 cuddRef(lx[i]);
235 do {
236 dd->reordered = 0;
237 lxn[i] = cuddUniqueInter(dd, nv, zero, one);
238 } while (dd->reordered == 1);
239 if (lxn[i] == NULL) return(0);
240 cuddRef(lxn[i]);
241 }
242 for (i = *ny, nv = by + (*ny) * sy; i < lny; i++, nv += sy) {
243 do {
244 dd->reordered = 0;
245 ly[i] = cuddUniqueInter(dd, nv, one, zero);
246 } while (dd->reordered == 1);
247 if (ly[i] == NULL) return(0);
248 cuddRef(ly[i]);
249 do {
250 dd->reordered = 0;
251 lyn[i] = cuddUniqueInter(dd, nv, zero, one);
252 } while (dd->reordered == 1);
253 if (lyn[i] == NULL) return(0);
254 cuddRef(lyn[i]);
255 }
256 *nx = lnx;
257 *ny = lny;
258
259 *E = dd->background; /* this call will never cause reordering */
260 cuddRef(*E);
261
262 while (! feof(fp)) {
263 err = fscanf(fp, "%d %d %lf", &u, &v, &val);
264 if (err == EOF) {
265 break;
266 } else if (err != 3) {
267 return(0);
268 } else if (u >= *m || v >= *n || u < 0 || v < 0) {
269 return(0);
270 }
271
272 minterm1 = one; cuddRef(minterm1);
273
274 /* Build minterm1 corresponding to this arc */
275 for (i = lnx - 1; i>=0; i--) {
276 if (u & 1) {
277 w = Cudd_addApply(dd, Cudd_addTimes, minterm1, lx[i]);
278 } else {
279 w = Cudd_addApply(dd, Cudd_addTimes, minterm1, lxn[i]);
280 }
281 if (w == NULL) {
282 Cudd_RecursiveDeref(dd, minterm1);
283 return(0);
284 }
285 cuddRef(w);
286 Cudd_RecursiveDeref(dd, minterm1);
287 minterm1 = w;
288 u >>= 1;
289 }
290 for (i = lny - 1; i>=0; i--) {
291 if (v & 1) {
292 w = Cudd_addApply(dd, Cudd_addTimes, minterm1, ly[i]);
293 } else {
294 w = Cudd_addApply(dd, Cudd_addTimes, minterm1, lyn[i]);
295 }
296 if (w == NULL) {
297 Cudd_RecursiveDeref(dd, minterm1);
298 return(0);
299 }
300 cuddRef(w);
301 Cudd_RecursiveDeref(dd, minterm1);
302 minterm1 = w;
303 v >>= 1;
304 }
305 /* Create new constant node if necessary.
306 ** This call will never cause reordering.
307 */
308 neW = cuddUniqueConst(dd, val);
309 if (neW == NULL) {
310 Cudd_RecursiveDeref(dd, minterm1);
311 return(0);
312 }
313 cuddRef(neW);
314
315 w = Cudd_addIte(dd, minterm1, neW, *E);
316 if (w == NULL) {
317 Cudd_RecursiveDeref(dd, minterm1);
318 Cudd_RecursiveDeref(dd, neW);
319 return(0);
320 }
321 cuddRef(w);
322 Cudd_RecursiveDeref(dd, minterm1);
323 Cudd_RecursiveDeref(dd, neW);
324 Cudd_RecursiveDeref(dd, *E);
325 *E = w;
326 }
327 return(1);
328
329 } /* end of Cudd_addRead */
330
331
332 /**Function********************************************************************
333
334 Synopsis [Reads in a graph (without labels) given as a list of arcs.]
335
336 Description [Reads in a graph (without labels) given as an adjacency
337 matrix. The first line of the input contains the numbers of rows and
338 columns of the adjacency matrix. The remaining lines contain the arcs
339 of the graph, one per line. Each arc is described by two integers,
340 i.e., the row and column number, or the indices of the two endpoints.
341 Cudd_bddRead produces a BDD that depends on two sets of variables: x
342 and y. The x variables (x\[0\] ... x\[nx-1\]) encode
343 the row index and the y variables (y\[0\] ... y\[ny-1\]) encode the
344 column index. x\[0\] and y\[0\] are the most significant bits in the
345 indices.
346 The variables may already exist or may be created by the function.
347 The index of x\[i\] is bx+i*sx, and the index of y\[i\] is by+i*sy.<p>
348 On input, nx and ny hold the numbers of row and column variables already
349 in existence. On output, they hold the numbers of row and column
350 variables actually used by the matrix. When Cudd_bddRead creates the
351 variable arrays, the index of x\[i\] is bx+i*sx, and the index of
352 y\[i\] is by+i*sy. When some variables already exist, Cudd_bddRead
353 expects the indices of the existing x variables to be bx+i*sx, and the
354 indices of the existing y variables to be by+i*sy.<p>
355 m and n are set to the numbers of rows and columns of the
356 matrix. Their values on input are immaterial. The BDD for the graph
357 is returned in E, and its reference count is > 0. Cudd_bddRead returns
358 1 in case of success; 0 otherwise.]
359
360 SideEffects [nx and ny are set to the numbers of row and column
361 variables. m and n are set to the numbers of rows and columns. x and y
362 are possibly extended to represent the array of row and column
363 variables.]
364
365 SeeAlso [Cudd_addHarwell Cudd_addRead]
366
367 ******************************************************************************/
368 int
Cudd_bddRead(FILE * fp,DdManager * dd,DdNode ** E,DdNode *** x,DdNode *** y,int * nx,int * ny,int * m,int * n,int bx,int sx,int by,int sy)369 Cudd_bddRead(
370 FILE * fp /* input file pointer */,
371 DdManager * dd /* DD manager */,
372 DdNode ** E /* characteristic function of the graph */,
373 DdNode *** x /* array of row variables */,
374 DdNode *** y /* array of column variables */,
375 int * nx /* number or row variables */,
376 int * ny /* number or column variables */,
377 int * m /* number of rows */,
378 int * n /* number of columns */,
379 int bx /* first index of row variables */,
380 int sx /* step of row variables */,
381 int by /* first index of column variables */,
382 int sy /* step of column variables */)
383 {
384 DdNode *one, *zero;
385 DdNode *w;
386 DdNode *minterm1;
387 int u, v, err, i, nv;
388 int lnx, lny;
389 DdNode **lx, **ly;
390
391 one = DD_ONE(dd);
392 zero = Cudd_Not(one);
393
394 err = fscanf(fp, "%d %d", &u, &v);
395 if (err == EOF) {
396 return(0);
397 } else if (err != 2) {
398 return(0);
399 }
400
401 *m = u;
402 /* Compute the number of x variables. */
403 lx = *x;
404 u--; /* row and column numbers start from 0 */
405 for (lnx=0; u > 0; lnx++) {
406 u >>= 1;
407 }
408 if (lnx > *nx) {
409 *x = lx = ABC_REALLOC(DdNode *, *x, lnx);
410 if (lx == NULL) {
411 dd->errorCode = CUDD_MEMORY_OUT;
412 return(0);
413 }
414 }
415
416 *n = v;
417 /* Compute the number of y variables. */
418 ly = *y;
419 v--; /* row and column numbers start from 0 */
420 for (lny=0; v > 0; lny++) {
421 v >>= 1;
422 }
423 if (lny > *ny) {
424 *y = ly = ABC_REALLOC(DdNode *, *y, lny);
425 if (ly == NULL) {
426 dd->errorCode = CUDD_MEMORY_OUT;
427 return(0);
428 }
429 }
430
431 /* Create all new variables. */
432 for (i = *nx, nv = bx + (*nx) * sx; i < lnx; i++, nv += sx) {
433 do {
434 dd->reordered = 0;
435 lx[i] = cuddUniqueInter(dd, nv, one, zero);
436 } while (dd->reordered == 1);
437 if (lx[i] == NULL) return(0);
438 cuddRef(lx[i]);
439 }
440 for (i = *ny, nv = by + (*ny) * sy; i < lny; i++, nv += sy) {
441 do {
442 dd->reordered = 0;
443 ly[i] = cuddUniqueInter(dd, nv, one, zero);
444 } while (dd->reordered == 1);
445 if (ly[i] == NULL) return(0);
446 cuddRef(ly[i]);
447 }
448 *nx = lnx;
449 *ny = lny;
450
451 *E = zero; /* this call will never cause reordering */
452 cuddRef(*E);
453
454 while (! feof(fp)) {
455 err = fscanf(fp, "%d %d", &u, &v);
456 if (err == EOF) {
457 break;
458 } else if (err != 2) {
459 return(0);
460 } else if (u >= *m || v >= *n || u < 0 || v < 0) {
461 return(0);
462 }
463
464 minterm1 = one; cuddRef(minterm1);
465
466 /* Build minterm1 corresponding to this arc. */
467 for (i = lnx - 1; i>=0; i--) {
468 if (u & 1) {
469 w = Cudd_bddAnd(dd, minterm1, lx[i]);
470 } else {
471 w = Cudd_bddAnd(dd, minterm1, Cudd_Not(lx[i]));
472 }
473 if (w == NULL) {
474 Cudd_RecursiveDeref(dd, minterm1);
475 return(0);
476 }
477 cuddRef(w);
478 Cudd_RecursiveDeref(dd,minterm1);
479 minterm1 = w;
480 u >>= 1;
481 }
482 for (i = lny - 1; i>=0; i--) {
483 if (v & 1) {
484 w = Cudd_bddAnd(dd, minterm1, ly[i]);
485 } else {
486 w = Cudd_bddAnd(dd, minterm1, Cudd_Not(ly[i]));
487 }
488 if (w == NULL) {
489 Cudd_RecursiveDeref(dd, minterm1);
490 return(0);
491 }
492 cuddRef(w);
493 Cudd_RecursiveDeref(dd, minterm1);
494 minterm1 = w;
495 v >>= 1;
496 }
497
498 w = Cudd_bddAnd(dd, Cudd_Not(minterm1), Cudd_Not(*E));
499 if (w == NULL) {
500 Cudd_RecursiveDeref(dd, minterm1);
501 return(0);
502 }
503 w = Cudd_Not(w);
504 cuddRef(w);
505 Cudd_RecursiveDeref(dd, minterm1);
506 Cudd_RecursiveDeref(dd, *E);
507 *E = w;
508 }
509 return(1);
510
511 } /* end of Cudd_bddRead */
512
513 /*---------------------------------------------------------------------------*/
514 /* Definition of internal functions */
515 /*---------------------------------------------------------------------------*/
516
517
518 /*---------------------------------------------------------------------------*/
519 /* Definition of static functions */
520 /*---------------------------------------------------------------------------*/
521
522
523 ABC_NAMESPACE_IMPL_END
524
525
526