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

Last change on this file since 27 was 13, checked in by cecile, 13 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.