source: vis_dev/glu-2.3/src/cuBdd/cuddRead.c@ 28

Last change on this file since 28 was 13, checked in by cecile, 15 years ago

library glu 2.3
File size: 16.3 KB
Line 
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 "util.h"
54#include "cuddInt.h"
55
56
57/*---------------------------------------------------------------------------*/
58/* Constant declarations */
59/*---------------------------------------------------------------------------*/
60
61
62/*---------------------------------------------------------------------------*/
63/* Stucture declarations */
64/*---------------------------------------------------------------------------*/
65
66
67/*---------------------------------------------------------------------------*/
68/* Type declarations */
69/*---------------------------------------------------------------------------*/
70
71
72/*---------------------------------------------------------------------------*/
73/* Variable declarations */
74/*---------------------------------------------------------------------------*/
75
76#ifndef lint
77static char rcsid[] DD_UNUSED = "$Id: cuddRead.c,v 1.6 2004/08/13 18:04:50 fabio Exp $";
78#endif
79
80/*---------------------------------------------------------------------------*/
81/* Macro declarations */
82/*---------------------------------------------------------------------------*/
83
84
85/**AutomaticStart*************************************************************/
86
87/*---------------------------------------------------------------------------*/
88/* Static function prototypes */
89/*---------------------------------------------------------------------------*/
90
91
92/**AutomaticEnd***************************************************************/
93
94
95/*---------------------------------------------------------------------------*/
96/* Definition of exported functions */
97/*---------------------------------------------------------------------------*/
98
99
100/**Function********************************************************************
101
102 Synopsis [Reads in a sparse matrix.]
103
104 Description [Reads in a sparse matrix specified in a simple format.
105 The first line of the input contains the numbers of rows and columns.
106 The remaining lines contain the elements of the matrix, one per line.
107 Given a background value
108 (specified by the background field of the manager), only the values
109 different from it are explicitly listed. Each foreground element is
110 described by two integers, i.e., the row and column number, and a
111 real number, i.e., the value.<p>
112 Cudd_addRead produces an ADD that depends on two sets of variables: x
113 and y. The x variables (x\[0\] ... x\[nx-1\]) encode the row index and
114 the y variables (y\[0\] ... y\[ny-1\]) encode the column index.
115 x\[0\] and y\[0\] are the most significant bits in the indices.
116 The variables may already exist or may be created by the function.
117 The index of x\[i\] is bx+i*sx, and the index of y\[i\] is by+i*sy.<p>
118 On input, nx and ny hold the numbers
119 of row and column variables already in existence. On output, they
120 hold the numbers of row and column variables actually used by the
121 matrix. When Cudd_addRead creates the variable arrays,
122 the index of x\[i\] is bx+i*sx, and the index of y\[i\] is by+i*sy.
123 When some variables already exist Cudd_addRead expects the indices
124 of the existing x variables to be bx+i*sx, and the indices of the
125 existing y variables to be by+i*sy.<p>
126 m and n are set to the numbers of rows and columns of the
127 matrix. Their values on input are immaterial.
128 The ADD for the
129 sparse matrix is returned in E, and its reference count is > 0.
130 Cudd_addRead returns 1 in case of success; 0 otherwise.]
131
132 SideEffects [nx and ny are set to the numbers of row and column
133 variables. m and n are set to the numbers of rows and columns. x and y
134 are possibly extended to represent the array of row and column
135 variables. Similarly for xn and yn_, which hold on return from
136 Cudd_addRead the complements of the row and column variables.]
137
138 SeeAlso [Cudd_addHarwell Cudd_bddRead]
139
140******************************************************************************/
141int
142Cudd_addRead(
143 FILE * fp /* input file pointer */,
144 DdManager * dd /* DD manager */,
145 DdNode ** E /* characteristic function of the graph */,
146 DdNode *** x /* array of row variables */,
147 DdNode *** y /* array of column variables */,
148 DdNode *** xn /* array of complemented row variables */,
149 DdNode *** yn_ /* array of complemented column variables */,
150 int * nx /* number or row variables */,
151 int * ny /* number or column variables */,
152 int * m /* number of rows */,
153 int * n /* number of columns */,
154 int bx /* first index of row variables */,
155 int sx /* step of row variables */,
156 int by /* first index of column variables */,
157 int sy /* step of column variables */)
158{
159 DdNode *one, *zero;
160 DdNode *w, *neW;
161 DdNode *minterm1;
162 int u, v, err, i, nv;
163 int lnx, lny;
164 CUDD_VALUE_TYPE val;
165 DdNode **lx, **ly, **lxn, **lyn;
166
167 one = DD_ONE(dd);
168 zero = DD_ZERO(dd);
169
170 err = fscanf(fp, "%d %d", &u, &v);
171 if (err == EOF) {
172 return(0);
173 } else if (err != 2) {
174 return(0);
175 }
176
177 *m = u;
178 /* Compute the number of x variables. */
179 lx = *x; lxn = *xn;
180 u--; /* row and column numbers start from 0 */
181 for (lnx=0; u > 0; lnx++) {
182 u >>= 1;
183 }
184 /* Here we rely on the fact that REALLOC of a null pointer is
185 ** translates to an ALLOC.
186 */
187 if (lnx > *nx) {
188 *x = lx = REALLOC(DdNode *, *x, lnx);
189 if (lx == NULL) {
190 dd->errorCode = CUDD_MEMORY_OUT;
191 return(0);
192 }
193 *xn = lxn = REALLOC(DdNode *, *xn, lnx);
194 if (lxn == NULL) {
195 dd->errorCode = CUDD_MEMORY_OUT;
196 return(0);
197 }
198 }
199
200 *n = v;
201 /* Compute the number of y variables. */
202 ly = *y; lyn = *yn_;
203 v--; /* row and column numbers start from 0 */
204 for (lny=0; v > 0; lny++) {
205 v >>= 1;
206 }
207 /* Here we rely on the fact that REALLOC of a null pointer is
208 ** translates to an ALLOC.
209 */
210 if (lny > *ny) {
211 *y = ly = REALLOC(DdNode *, *y, lny);
212 if (ly == NULL) {
213 dd->errorCode = CUDD_MEMORY_OUT;
214 return(0);
215 }
216 *yn_ = lyn = REALLOC(DdNode *, *yn_, lny);
217 if (lyn == NULL) {
218 dd->errorCode = CUDD_MEMORY_OUT;
219 return(0);
220 }
221 }
222
223 /* Create all new variables. */
224 for (i = *nx, nv = bx + (*nx) * sx; i < lnx; i++, nv += sx) {
225 do {
226 dd->reordered = 0;
227 lx[i] = cuddUniqueInter(dd, nv, one, zero);
228 } while (dd->reordered == 1);
229 if (lx[i] == NULL) return(0);
230 cuddRef(lx[i]);
231 do {
232 dd->reordered = 0;
233 lxn[i] = cuddUniqueInter(dd, nv, zero, one);
234 } while (dd->reordered == 1);
235 if (lxn[i] == NULL) return(0);
236 cuddRef(lxn[i]);
237 }
238 for (i = *ny, nv = by + (*ny) * sy; i < lny; i++, nv += sy) {
239 do {
240 dd->reordered = 0;
241 ly[i] = cuddUniqueInter(dd, nv, one, zero);
242 } while (dd->reordered == 1);
243 if (ly[i] == NULL) return(0);
244 cuddRef(ly[i]);
245 do {
246 dd->reordered = 0;
247 lyn[i] = cuddUniqueInter(dd, nv, zero, one);
248 } while (dd->reordered == 1);
249 if (lyn[i] == NULL) return(0);
250 cuddRef(lyn[i]);
251 }
252 *nx = lnx;
253 *ny = lny;
254
255 *E = dd->background; /* this call will never cause reordering */
256 cuddRef(*E);
257
258 while (! feof(fp)) {
259 err = fscanf(fp, "%d %d %lf", &u, &v, &val);
260 if (err == EOF) {
261 break;
262 } else if (err != 3) {
263 return(0);
264 } else if (u >= *m || v >= *n || u < 0 || v < 0) {
265 return(0);
266 }
267
268 minterm1 = one; cuddRef(minterm1);
269
270 /* Build minterm1 corresponding to this arc */
271 for (i = lnx - 1; i>=0; i--) {
272 if (u & 1) {
273 w = Cudd_addApply(dd, Cudd_addTimes, minterm1, lx[i]);
274 } else {
275 w = Cudd_addApply(dd, Cudd_addTimes, minterm1, lxn[i]);
276 }
277 if (w == NULL) {
278 Cudd_RecursiveDeref(dd, minterm1);
279 return(0);
280 }
281 cuddRef(w);
282 Cudd_RecursiveDeref(dd, minterm1);
283 minterm1 = w;
284 u >>= 1;
285 }
286 for (i = lny - 1; i>=0; i--) {
287 if (v & 1) {
288 w = Cudd_addApply(dd, Cudd_addTimes, minterm1, ly[i]);
289 } else {
290 w = Cudd_addApply(dd, Cudd_addTimes, minterm1, lyn[i]);
291 }
292 if (w == NULL) {
293 Cudd_RecursiveDeref(dd, minterm1);
294 return(0);
295 }
296 cuddRef(w);
297 Cudd_RecursiveDeref(dd, minterm1);
298 minterm1 = w;
299 v >>= 1;
300 }
301 /* Create new constant node if necessary.
302 ** This call will never cause reordering.
303 */
304 neW = cuddUniqueConst(dd, val);
305 if (neW == NULL) {
306 Cudd_RecursiveDeref(dd, minterm1);
307 return(0);
308 }
309 cuddRef(neW);
310
311 w = Cudd_addIte(dd, minterm1, neW, *E);
312 if (w == NULL) {
313 Cudd_RecursiveDeref(dd, minterm1);
314 Cudd_RecursiveDeref(dd, neW);
315 return(0);
316 }
317 cuddRef(w);
318 Cudd_RecursiveDeref(dd, minterm1);
319 Cudd_RecursiveDeref(dd, neW);
320 Cudd_RecursiveDeref(dd, *E);
321 *E = w;
322 }
323 return(1);
324
325} /* end of Cudd_addRead */
326
327
328/**Function********************************************************************
329
330 Synopsis [Reads in a graph (without labels) given as a list of arcs.]
331
332 Description [Reads in a graph (without labels) given as an adjacency
333 matrix. The first line of the input contains the numbers of rows and
334 columns of the adjacency matrix. The remaining lines contain the arcs
335 of the graph, one per line. Each arc is described by two integers,
336 i.e., the row and column number, or the indices of the two endpoints.
337 Cudd_bddRead produces a BDD that depends on two sets of variables: x
338 and y. The x variables (x\[0\] ... x\[nx-1\]) encode
339 the row index and the y variables (y\[0\] ... y\[ny-1\]) encode the
340 column index. x\[0\] and y\[0\] are the most significant bits in the
341 indices.
342 The variables may already exist or may be created by the function.
343 The index of x\[i\] is bx+i*sx, and the index of y\[i\] is by+i*sy.<p>
344 On input, nx and ny hold the numbers of row and column variables already
345 in existence. On output, they hold the numbers of row and column
346 variables actually used by the matrix. When Cudd_bddRead creates the
347 variable arrays, the index of x\[i\] is bx+i*sx, and the index of
348 y\[i\] is by+i*sy. When some variables already exist, Cudd_bddRead
349 expects the indices of the existing x variables to be bx+i*sx, and the
350 indices of the existing y variables to be by+i*sy.<p>
351 m and n are set to the numbers of rows and columns of the
352 matrix. Their values on input are immaterial. The BDD for the graph
353 is returned in E, and its reference count is > 0. Cudd_bddRead returns
354 1 in case of success; 0 otherwise.]
355
356 SideEffects [nx and ny are set to the numbers of row and column
357 variables. m and n are set to the numbers of rows and columns. x and y
358 are possibly extended to represent the array of row and column
359 variables.]
360
361 SeeAlso [Cudd_addHarwell Cudd_addRead]
362
363******************************************************************************/
364int
365Cudd_bddRead(
366 FILE * fp /* input file pointer */,
367 DdManager * dd /* DD manager */,
368 DdNode ** E /* characteristic function of the graph */,
369 DdNode *** x /* array of row variables */,
370 DdNode *** y /* array of column variables */,
371 int * nx /* number or row variables */,
372 int * ny /* number or column variables */,
373 int * m /* number of rows */,
374 int * n /* number of columns */,
375 int bx /* first index of row variables */,
376 int sx /* step of row variables */,
377 int by /* first index of column variables */,
378 int sy /* step of column variables */)
379{
380 DdNode *one, *zero;
381 DdNode *w;
382 DdNode *minterm1;
383 int u, v, err, i, nv;
384 int lnx, lny;
385 DdNode **lx, **ly;
386
387 one = DD_ONE(dd);
388 zero = Cudd_Not(one);
389
390 err = fscanf(fp, "%d %d", &u, &v);
391 if (err == EOF) {
392 return(0);
393 } else if (err != 2) {
394 return(0);
395 }
396
397 *m = u;
398 /* Compute the number of x variables. */
399 lx = *x;
400 u--; /* row and column numbers start from 0 */
401 for (lnx=0; u > 0; lnx++) {
402 u >>= 1;
403 }
404 if (lnx > *nx) {
405 *x = lx = REALLOC(DdNode *, *x, lnx);
406 if (lx == NULL) {
407 dd->errorCode = CUDD_MEMORY_OUT;
408 return(0);
409 }
410 }
411
412 *n = v;
413 /* Compute the number of y variables. */
414 ly = *y;
415 v--; /* row and column numbers start from 0 */
416 for (lny=0; v > 0; lny++) {
417 v >>= 1;
418 }
419 if (lny > *ny) {
420 *y = ly = REALLOC(DdNode *, *y, lny);
421 if (ly == NULL) {
422 dd->errorCode = CUDD_MEMORY_OUT;
423 return(0);
424 }
425 }
426
427 /* Create all new variables. */
428 for (i = *nx, nv = bx + (*nx) * sx; i < lnx; i++, nv += sx) {
429 do {
430 dd->reordered = 0;
431 lx[i] = cuddUniqueInter(dd, nv, one, zero);
432 } while (dd->reordered == 1);
433 if (lx[i] == NULL) return(0);
434 cuddRef(lx[i]);
435 }
436 for (i = *ny, nv = by + (*ny) * sy; i < lny; i++, nv += sy) {
437 do {
438 dd->reordered = 0;
439 ly[i] = cuddUniqueInter(dd, nv, one, zero);
440 } while (dd->reordered == 1);
441 if (ly[i] == NULL) return(0);
442 cuddRef(ly[i]);
443 }
444 *nx = lnx;
445 *ny = lny;
446
447 *E = zero; /* this call will never cause reordering */
448 cuddRef(*E);
449
450 while (! feof(fp)) {
451 err = fscanf(fp, "%d %d", &u, &v);
452 if (err == EOF) {
453 break;
454 } else if (err != 2) {
455 return(0);
456 } else if (u >= *m || v >= *n || u < 0 || v < 0) {
457 return(0);
458 }
459
460 minterm1 = one; cuddRef(minterm1);
461
462 /* Build minterm1 corresponding to this arc. */
463 for (i = lnx - 1; i>=0; i--) {
464 if (u & 1) {
465 w = Cudd_bddAnd(dd, minterm1, lx[i]);
466 } else {
467 w = Cudd_bddAnd(dd, minterm1, Cudd_Not(lx[i]));
468 }
469 if (w == NULL) {
470 Cudd_RecursiveDeref(dd, minterm1);
471 return(0);
472 }
473 cuddRef(w);
474 Cudd_RecursiveDeref(dd,minterm1);
475 minterm1 = w;
476 u >>= 1;
477 }
478 for (i = lny - 1; i>=0; i--) {
479 if (v & 1) {
480 w = Cudd_bddAnd(dd, minterm1, ly[i]);
481 } else {
482 w = Cudd_bddAnd(dd, minterm1, Cudd_Not(ly[i]));
483 }
484 if (w == NULL) {
485 Cudd_RecursiveDeref(dd, minterm1);
486 return(0);
487 }
488 cuddRef(w);
489 Cudd_RecursiveDeref(dd, minterm1);
490 minterm1 = w;
491 v >>= 1;
492 }
493
494 w = Cudd_bddAnd(dd, Cudd_Not(minterm1), Cudd_Not(*E));
495 if (w == NULL) {
496 Cudd_RecursiveDeref(dd, minterm1);
497 return(0);
498 }
499 w = Cudd_Not(w);
500 cuddRef(w);
501 Cudd_RecursiveDeref(dd, minterm1);
502 Cudd_RecursiveDeref(dd, *E);
503 *E = w;
504 }
505 return(1);
506
507} /* end of Cudd_bddRead */
508
509/*---------------------------------------------------------------------------*/
510/* Definition of internal functions */
511/*---------------------------------------------------------------------------*/
512
513
514/*---------------------------------------------------------------------------*/
515/* Definition of static functions */
516/*---------------------------------------------------------------------------*/
517
Note: See TracBrowser for help on using the repository browser.