src/cuBdd/cuddRead.c File Reference

#include "util.h"
#include "cuddInt.h"

Include dependency graph for cuddRead.c:

Functions
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)
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)
Variables
static char rcsid[]	DD_UNUSED = "$Id: cuddRead.c,v 1.6 2004/08/13 18:04:50 fabio Exp $"

Function Documentation

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
	)

AutomaticStart AutomaticEnd Function********************************************************************

Synopsis [Reads in a sparse matrix.]

Description [Reads in a sparse matrix specified in a simple format. The first line of the input contains the numbers of rows and columns. The remaining lines contain the elements of the matrix, one per line. Given a background value (specified by the background field of the manager), only the values different from it are explicitly listed. Each foreground element is described by two integers, i.e., the row and column number, and a real number, i.e., the value.

Cudd_addRead produces an ADD that depends on two sets of variables: x and y. The x variables (x\[0\] ... x\[nx-1\]) encode the row index and the y variables (y\[0\] ... y\[ny-1\]) encode the column index. x\[0\] and y\[0\] are the most significant bits in the indices. The variables may already exist or may be created by the function. The index of x\[i\] is bx+i*sx, and the index of y\[i\] is by+i*sy.

On input, nx and ny hold the numbers of row and column variables already in existence. On output, they hold the numbers of row and column variables actually used by the matrix. When Cudd_addRead creates the variable arrays, the index of x\[i\] is bx+i*sx, and the index of y\[i\] is by+i*sy. When some variables already exist Cudd_addRead expects the indices of the existing x variables to be bx+i*sx, and the indices of the existing y variables to be by+i*sy.

m and n are set to the numbers of rows and columns of the matrix. Their values on input are immaterial. The ADD for the sparse matrix is returned in E, and its reference count is > 0. Cudd_addRead returns 1 in case of success; 0 otherwise.]

SideEffects [nx and ny are set to the numbers of row and column variables. m and n are set to the numbers of rows and columns. x and y are possibly extended to represent the array of row and column variables. Similarly for xn and yn_, which hold on return from Cudd_addRead the complements of the row and column variables.]

SeeAlso [Cudd_addHarwell Cudd_bddRead]

Definition at line 142 of file cuddRead.c.

00159 00160 00161 00162 00163 00164 00165 00166 00167 00168 00169 00170 00171 00172 00173 00174 00175     } 00176 00177     *m = u; 00178 00179 00180 00181 00182 00183     } 00184 00185 00186 00187 00188 00189 00190 00191 00192         } 00193 00194 00195 00196 00197         } 00198     } 00199 00200     *n = v; 00201 00202 00203 00204 00205 00206     } 00207 00208 00209 00210 00211 00212 00213 00214 00215         } 00216 00217 00218 00219 00220         } 00221     } 00222 00223 00224 00225 00226 00227 00228 00229 00230 00231 00232 00233 00234 00235 00236 00237     } 00238 00239 00240 00241 00242 00243 00244 00245 00246 00247 00248 00249 00250 00251     } 00252 00253 00254 00255 00256 00257 00258 00259 00260 00261 00262 00263 00264 00265 00266         } 00267 00268 00269 00270 00271 00272 00273 00274 00275 00276 00277 00278 00279 00280 00281 00282 00283 00284 00285         } 00286 00287 00288 00289 00290 00291 00292 00293 00294 00295 00296 00297 00298 00299 00300         } 00301 00302 00303 00304 00305 00306 00307 00308         } 00309 00310 00311 00312 00313 00314 00315 00316         } 00317 00318 00319 00320 00321 00322     } 00323 00324 00325

class="fragment">00158 { DdNode *one, *zero; DdNode *w, *neW; DdNode *minterm1; int u, v, err, i, nv; int lnx, lny; CUDD_VALUE_TYPE val; DdNode **lx, **ly, **lxn, **lyn; one = DD_ONE(dd); zero = DD_ZERO(dd); err = fscanf(fp, "%d %d", &u, &v); if (err == EOF) { return(0); } else if (err != 2) { return(0); /* Compute the number of x variables. */ lx = *x; lxn = *xn; u--; /* row and column numbers start from 0 */ for (lnx=0; u > 0; lnx++) { u >>= 1; /* Here we rely on the fact that REALLOC of a null pointer is ** translates to an ALLOC. */ if (lnx > *nx) { *x = lx = REALLOC(DdNode *, *x, lnx); if (lx == NULL) { dd->errorCode = CUDD_MEMORY_OUT; return(0); *xn = lxn = REALLOC(DdNode *, *xn, lnx); if (lxn == NULL) { dd->errorCode = CUDD_MEMORY_OUT; return(0); /* Compute the number of y variables. */ ly = *y; lyn = *yn_; v--; /* row and column numbers start from 0 */ for (lny=0; v > 0; lny++) { v >>= 1; /* Here we rely on the fact that REALLOC of a null pointer is ** translates to an ALLOC. */ if (lny > *ny) { *y = ly = REALLOC(DdNode *, *y, lny); if (ly == NULL) { dd->errorCode = CUDD_MEMORY_OUT; return(0); *yn_ = lyn = REALLOC(DdNode *, *yn_, lny); if (lyn == NULL) { dd->errorCode = CUDD_MEMORY_OUT; return(0); /* Create all new variables. */ for (i = *nx, nv = bx + (*nx) * sx; i < lnx; i++, nv += sx) { do { dd->reordered = 0; lx[i] = cuddUniqueInter(dd, nv, one, zero); } while (dd->reordered == 1); if (lx[i] == NULL) return(0); cuddRef(lx[i]); do { dd->reordered = 0; lxn[i] = cuddUniqueInter(dd, nv, zero, one); } while (dd->reordered == 1); if (lxn[i] == NULL) return(0); cuddRef(lxn[i]); for (i = *ny, nv = by + (*ny) * sy; i < lny; i++, nv += sy) { do { dd->reordered = 0; ly[i] = cuddUniqueInter(dd, nv, one, zero); } while (dd->reordered == 1); if (ly[i] == NULL) return(0); cuddRef(ly[i]); do { dd->reordered = 0; lyn[i] = cuddUniqueInter(dd, nv, zero, one); } while (dd->reordered == 1); if (lyn[i] == NULL) return(0); cuddRef(lyn[i]); *nx = lnx; *ny = lny; *E = dd->background; /* this call will never cause reordering */ cuddRef(*E); while (! feof(fp)) { err = fscanf(fp, "%d %d %lf", &u, &v, &val); if (err == EOF) { break; } else if (err != 3) { return(0); } else if (u >= *m || v >= *n || u < 0 || v < 0) { return(0); minterm1 = one; cuddRef(minterm1); /* Build minterm1 corresponding to this arc */ for (i = lnx - 1; i>=0; i--) { if (u & 1) { w = Cudd_addApply(dd, Cudd_addTimes, minterm1, lx[i]); } else { w = Cudd_addApply(dd, Cudd_addTimes, minterm1, lxn[i]); } if (w == NULL) { Cudd_RecursiveDeref(dd, minterm1); return(0); } cuddRef(w); Cudd_RecursiveDeref(dd, minterm1); minterm1 = w; u >>= 1; for (i = lny - 1; i>=0; i--) { if (v & 1) { w = Cudd_addApply(dd, Cudd_addTimes, minterm1, ly[i]); } else { w = Cudd_addApply(dd, Cudd_addTimes, minterm1, lyn[i]); } if (w == NULL) { Cudd_RecursiveDeref(dd, minterm1); return(0); } cuddRef(w); Cudd_RecursiveDeref(dd, minterm1); minterm1 = w; v >>= 1; /* Create new constant node if necessary. ** This call will never cause reordering. */ neW = cuddUniqueConst(dd, val); if (neW == NULL) { Cudd_RecursiveDeref(dd, minterm1); return(0); cuddRef(neW); w = Cudd_addIte(dd, minterm1, neW, *E); if (w == NULL) { Cudd_RecursiveDeref(dd, minterm1); Cudd_RecursiveDeref(dd, neW); return(0); cuddRef(w); Cudd_RecursiveDeref(dd, minterm1); Cudd_RecursiveDeref(dd, neW); Cudd_RecursiveDeref(dd, *E); *E = w; return(1); } /* end of Cudd_addRead */

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
	)

Function********************************************************************

Synopsis [Reads in a graph (without labels) given as a list of arcs.]

Description [Reads in a graph (without labels) given as an adjacency matrix. The first line of the input contains the numbers of rows and columns of the adjacency matrix. The remaining lines contain the arcs of the graph, one per line. Each arc is described by two integers, i.e., the row and column number, or the indices of the two endpoints. Cudd_bddRead produces a BDD that depends on two sets of variables: x and y. The x variables (x\[0\] ... x\[nx-1\]) encode the row index and the y variables (y\[0\] ... y\[ny-1\]) encode the column index. x\[0\] and y\[0\] are the most significant bits in the indices. The variables may already exist or may be created by the function. The index of x\[i\] is bx+i*sx, and the index of y\[i\] is by+i*sy.

On input, nx and ny hold the numbers of row and column variables already in existence. On output, they hold the numbers of row and column variables actually used by the matrix. When Cudd_bddRead creates the variable arrays, the index of x\[i\] is bx+i*sx, and the index of y\[i\] is by+i*sy. When some variables already exist, Cudd_bddRead expects the indices of the existing x variables to be bx+i*sx, and the indices of the existing y variables to be by+i*sy.

m and n are set to the numbers of rows and columns of the matrix. Their values on input are immaterial. The BDD for the graph is returned in E, and its reference count is > 0. Cudd_bddRead returns 1 in case of success; 0 otherwise.]

SideEffects [nx and ny are set to the numbers of row and column variables. m and n are set to the numbers of rows and columns. x and y are possibly extended to represent the array of row and column variables.]

SeeAlso [Cudd_addHarwell Cudd_addRead]

Definition at line 365 of file cuddRead.c.

00379 {
00380     DdNode *one, *zero;
00381     DdNode *w;
00382     DdNode *minterm1;
00383     int u, v, err, i, nv;
00384     int lnx, lny;
00385     DdNode **lx, **ly;
00386 
00387     one = DD_ONE(dd);
00388     zero = Cudd_Not(one);
00389 
00390     err = fscanf(fp, "%d %d", &u, &v);
00391     if (err == EOF) {
00392         return(0);
00393     } else if (err != 2) {
00394         return(0);
00395     }
00396 
00397     *m = u;
00398     /* Compute the number of x variables. */
00399     lx = *x;
00400     u--;        /* row and column numbers start from 0 */
00401     for (lnx=0; u > 0; lnx++) {
00402         u >>= 1;
00403     }
00404     if (lnx > *nx) {
00405         *x = lx = REALLOC(DdNode *, *x, lnx);
00406         if (lx == NULL) {
00407             dd->errorCode = CUDD_MEMORY_OUT;
00408             return(0);
00409         }
00410     }
00411 
00412     *n = v;
00413     /* Compute the number of y variables. */
00414     ly = *y;
00415     v--;        /* row and column numbers start from 0 */
00416     for (lny=0; v > 0; lny++) {
00417         v >>= 1;
00418     }
00419     if (lny > *ny) {
00420         *y = ly = REALLOC(DdNode *, *y, lny);
00421         if (ly == NULL) {
00422             dd->errorCode = CUDD_MEMORY_OUT;
00423             return(0);
00424         }
00425     }
00426 
00427     /* Create all new variables. */
00428     for (i = *nx, nv = bx + (*nx) * sx; i < lnx; i++, nv += sx) {
00429         do {
00430             dd->reordered = 0;
00431             lx[i] = cuddUniqueInter(dd, nv, one, zero);
00432         } while (dd->reordered == 1);
00433         if (lx[i] == NULL) return(0);
00434         cuddRef(lx[i]);
00435     }
00436     for (i = *ny, nv = by + (*ny) * sy; i < lny; i++, nv += sy) {
00437         do {
00438             dd->reordered = 0;
00439             ly[i] = cuddUniqueInter(dd, nv, one, zero);
00440         } while (dd->reordered == 1);
00441         if (ly[i] == NULL) return(0);
00442         cuddRef(ly[i]);
00443     }
00444     *nx = lnx;
00445     *ny = lny;
00446 
00447     *E = zero; /* this call will never cause reordering */
00448     cuddRef(*E);
00449 
00450     while (! feof(fp)) {
00451         err = fscanf(fp, "%d %d", &u, &v);
00452         if (err == EOF) {
00453             break;
00454         } else if (err != 2) {
00455             return(0);
00456         } else if (u >= *m || v >= *n || u < 0 || v < 0) {
00457             return(0);
00458         }
00459  
00460         minterm1 = one; cuddRef(minterm1);
00461 
00462         /* Build minterm1 corresponding to this arc. */
00463         for (i = lnx - 1; i>=0; i--) {
00464             if (u & 1) {
00465                 w = Cudd_bddAnd(dd, minterm1, lx[i]);
00466             } else {
00467                 w = Cudd_bddAnd(dd, minterm1, Cudd_Not(lx[i]));
00468             }
00469             if (w == NULL) {
00470                 Cudd_RecursiveDeref(dd, minterm1);
00471                 return(0);
00472             }
00473             cuddRef(w);
00474             Cudd_RecursiveDeref(dd,minterm1);
00475             minterm1 = w;
00476             u >>= 1;
00477         }
00478         for (i = lny - 1; i>=0; i--) {
00479             if (v & 1) {
00480                 w = Cudd_bddAnd(dd, minterm1, ly[i]);
00481             } else {
00482                 w = Cudd_bddAnd(dd, minterm1, Cudd_Not(ly[i]));
00483             }
00484             if (w == NULL) {
00485                 Cudd_RecursiveDeref(dd, minterm1);
00486                 return(0);
00487             }
00488             cuddRef(w);
00489             Cudd_RecursiveDeref(dd, minterm1);
00490             minterm1 = w;
00491             v >>= 1;
00492         }
00493 
00494         w = Cudd_bddAnd(dd, Cudd_Not(minterm1), Cudd_Not(*E));
00495         if (w == NULL) {
00496             Cudd_RecursiveDeref(dd, minterm1);
00497             return(0);
00498         }
00499         w = Cudd_Not(w);
00500         cuddRef(w);
00501         Cudd_RecursiveDeref(dd, minterm1);
00502         Cudd_RecursiveDeref(dd, *E);
00503         *E = w;
00504     }
00505     return(1);
00506 
00507 } /* end of Cudd_bddRead */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddRead.c,v 1.6 2004/08/13 18:04:50 fabio Exp $" [static]

CFile***********************************************************************

FileName [cuddRead.c]

PackageName [cudd]

Synopsis [Functions to read in a matrix]

Description [External procedures included in this module:

]

SeeAlso [cudd_addHarwell.c]

Author [Fabio Somenzi]

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]

Definition at line 77 of file cuddRead.c.

src/cuBdd/cuddRead.c File Reference

Functions

Variables

Function Documentation

Variable Documentation