distr/cudd/cuddRead.c

   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
  77 static 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 ******************************************************************************/
 141 int
 142 Cudd_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 ******************************************************************************/
 364 int
 365 Cudd_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