distr/cudd/cuddZddUtil.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddZddUtil.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Utility functions for ZDDs.]
   8
   9   Description [External procedures included in this module:
  10                     <ul>
  11                     <li> Cudd_zddPrintMinterm()
  12                     <li> Cudd_zddPrintCover()
  13                     <li> Cudd_zddPrintDebug()
  14                     <li> Cudd_zddFirstPath()
  15                     <li> Cudd_zddNextPath()
  16                     <li> Cudd_zddCoverPathToString()
  17                     <li> Cudd_zddDumpDot()
  18                     </ul>
  19                Internal procedures included in this module:
  20                     <ul>
  21                     <li> cuddZddP()
  22                     </ul>
  23                Static procedures included in this module:
  24                     <ul>
  25                     <li> zp2()
  26                     <li> zdd_print_minterm_aux()
  27                     <li> zddPrintCoverAux()
  28                     </ul>
  29               ]
  30
  31   SeeAlso     []
  32
  33   Author      [Hyong-Kyoon Shin, In-Ho Moon, Fabio Somenzi]
  34
  35   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  36
  37   All rights reserved.
  38
  39   Redistribution and use in source and binary forms, with or without
  40   modification, are permitted provided that the following conditions
  41   are met:
  42
  43   Redistributions of source code must retain the above copyright
  44   notice, this list of conditions and the following disclaimer.
  45
  46   Redistributions in binary form must reproduce the above copyright
  47   notice, this list of conditions and the following disclaimer in the
  48   documentation and/or other materials provided with the distribution.
  49
  50   Neither the name of the University of Colorado nor the names of its
  51   contributors may be used to endorse or promote products derived from
  52   this software without specific prior written permission.
  53
  54   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  55   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  56   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  57   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  58   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  59   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  60   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  61   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  62   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  63   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  64   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  65   POSSIBILITY OF SUCH DAMAGE.]
  66
  67 ******************************************************************************/
  68
  69 #include "util.h"
  70 #include "cuddInt.h"
  71
  72 /*---------------------------------------------------------------------------*/
  73 /* Constant declarations                                                     */
  74 /*---------------------------------------------------------------------------*/
  75
  76
  77 /*---------------------------------------------------------------------------*/
  78 /* Stucture declarations                                                     */
  79 /*---------------------------------------------------------------------------*/
  80
  81
  82 /*---------------------------------------------------------------------------*/
  83 /* Type declarations                                                         */
  84 /*---------------------------------------------------------------------------*/
  85
  86
  87 /*---------------------------------------------------------------------------*/
  88 /* Variable declarations                                                     */
  89 /*---------------------------------------------------------------------------*/
  90
  91 #ifndef lint
  92 static char rcsid[] DD_UNUSED = "$Id: cuddZddUtil.c,v 1.27 2009/03/08 02:49:02 fabio Exp $";
  93 #endif
  94
  95 /*---------------------------------------------------------------------------*/
  96 /* Macro declarations                                                        */
  97 /*---------------------------------------------------------------------------*/
  98
  99
 100 /**AutomaticStart*************************************************************/
 101
 102 /*---------------------------------------------------------------------------*/
 103 /* Static function prototypes                                                */
 104 /*---------------------------------------------------------------------------*/
 105
 106 static int zp2 (DdManager *zdd, DdNode *f, st_table *t);
 107 static void zdd_print_minterm_aux (DdManager *zdd, DdNode *node, int level, int *list);
 108 static void zddPrintCoverAux (DdManager *zdd, DdNode *node, int level, int *list);
 109
 110 /**AutomaticEnd***************************************************************/
 111
 112
 113 /*---------------------------------------------------------------------------*/
 114 /* Definition of exported functions                                          */
 115 /*---------------------------------------------------------------------------*/
 116
 117
 118 /**Function********************************************************************
 119
 120   Synopsis    [Prints a disjoint sum of product form for a ZDD.]
 121
 122   Description [Prints a disjoint sum of product form for a ZDD. Returns 1
 123   if successful; 0 otherwise.]
 124
 125   SideEffects [None]
 126
 127   SeeAlso     [Cudd_zddPrintDebug Cudd_zddPrintCover]
 128
 129 ******************************************************************************/
 130 int
 131 Cudd_zddPrintMinterm(
 132   DdManager * zdd,
 133   DdNode * node)
 134 {
 135     int         i, size;
 136     int         *list;
 137
 138     size = (int)zdd->sizeZ;
 139     list = ALLOC(int, size);
 140     if (list == NULL) {
 141         zdd->errorCode = CUDD_MEMORY_OUT;
 142         return(0);
 143     }
 144     for (i = 0; i < size; i++) list[i] = 3; /* bogus value should disappear */
 145     zdd_print_minterm_aux(zdd, node, 0, list);
 146     FREE(list);
 147     return(1);
 148
 149 } /* end of Cudd_zddPrintMinterm */
 150
 151
 152 /**Function********************************************************************
 153
 154   Synopsis    [Prints a sum of products from a ZDD representing a cover.]
 155
 156   Description [Prints a sum of products from a ZDD representing a cover.
 157   Returns 1 if successful; 0 otherwise.]
 158
 159   SideEffects [None]
 160
 161   SeeAlso     [Cudd_zddPrintMinterm]
 162
 163 ******************************************************************************/
 164 int
 165 Cudd_zddPrintCover(
 166   DdManager * zdd,
 167   DdNode * node)
 168 {
 169     int         i, size;
 170     int         *list;
 171
 172     size = (int)zdd->sizeZ;
 173     if (size % 2 != 0) return(0); /* number of variables should be even */
 174     list = ALLOC(int, size);
 175     if (list == NULL) {
 176         zdd->errorCode = CUDD_MEMORY_OUT;
 177         return(0);
 178     }
 179     for (i = 0; i < size; i++) list[i] = 3; /* bogus value should disappear */
 180     zddPrintCoverAux(zdd, node, 0, list);
 181     FREE(list);
 182     return(1);
 183
 184 } /* end of Cudd_zddPrintCover */
 185
 186
 187 /**Function********************************************************************
 188
 189   Synopsis [Prints to the standard output a ZDD and its statistics.]
 190
 191   Description [Prints to the standard output a DD and its statistics.
 192   The statistics include the number of nodes and the number of minterms.
 193   (The number of minterms is also the number of combinations in the set.)
 194   The statistics are printed if pr &gt; 0.  Specifically:
 195   <ul>
 196   <li> pr = 0 : prints nothing
 197   <li> pr = 1 : prints counts of nodes and minterms
 198   <li> pr = 2 : prints counts + disjoint sum of products
 199   <li> pr = 3 : prints counts + list of nodes
 200   <li> pr &gt; 3 : prints counts + disjoint sum of products + list of nodes
 201   </ul>
 202   Returns 1 if successful; 0 otherwise.
 203   ]
 204
 205   SideEffects [None]
 206
 207   SeeAlso     []
 208
 209 ******************************************************************************/
 210 int
 211 Cudd_zddPrintDebug(
 212   DdManager * zdd,
 213   DdNode * f,
 214   int  n,
 215   int  pr)
 216 {
 217     DdNode      *empty = DD_ZERO(zdd);
 218     int         nodes;
 219     double      minterms;
 220     int         retval = 1;
 221
 222     if (f == empty && pr > 0) {
 223         (void) fprintf(zdd->out,": is the empty ZDD\n");
 224         (void) fflush(zdd->out);
 225         return(1);
 226     }
 227
 228     if (pr > 0) {
 229         nodes = Cudd_zddDagSize(f);
 230         if (nodes == CUDD_OUT_OF_MEM) retval = 0;
 231         minterms = Cudd_zddCountMinterm(zdd, f, n);
 232         if (minterms == (double)CUDD_OUT_OF_MEM) retval = 0;
 233         (void) fprintf(zdd->out,": %d nodes %g minterms\n",
 234                        nodes, minterms);
 235         if (pr > 2)
 236             if (!cuddZddP(zdd, f)) retval = 0;
 237         if (pr == 2 || pr > 3) {
 238             if (!Cudd_zddPrintMinterm(zdd, f)) retval = 0;
 239             (void) fprintf(zdd->out,"\n");
 240         }
 241         (void) fflush(zdd->out);
 242     }
 243     return(retval);
 244
 245 } /* end of Cudd_zddPrintDebug */
 246
 247
 248
 249 /**Function********************************************************************
 250
 251   Synopsis    [Finds the first path of a ZDD.]
 252
 253   Description [Defines an iterator on the paths of a ZDD
 254   and finds its first path. Returns a generator that contains the
 255   information necessary to continue the enumeration if successful; NULL
 256   otherwise.<p>
 257   A path is represented as an array of literals, which are integers in
 258   {0, 1, 2}; 0 represents an else arc out of a node, 1 represents a then arc
 259   out of a node, and 2 stands for the absence of a node.
 260   The size of the array equals the number of variables in the manager at
 261   the time Cudd_zddFirstCube is called.<p>
 262   The paths that end in the empty terminal are not enumerated.]
 263
 264   SideEffects [The first path is returned as a side effect.]
 265
 266   SeeAlso     [Cudd_zddForeachPath Cudd_zddNextPath Cudd_GenFree
 267   Cudd_IsGenEmpty]
 268
 269 ******************************************************************************/
 270 DdGen *
 271 Cudd_zddFirstPath(
 272   DdManager * zdd,
 273   DdNode * f,
 274   int ** path)
 275 {
 276     DdGen *gen;
 277     DdNode *top, *next, *prev;
 278     int i;
 279     int nvars;
 280
 281     /* Sanity Check. */
 282     if (zdd == NULL || f == NULL) return(NULL);
 283
 284     /* Allocate generator an initialize it. */
 285     gen = ALLOC(DdGen,1);
 286     if (gen == NULL) {
 287         zdd->errorCode = CUDD_MEMORY_OUT;
 288         return(NULL);
 289     }
 290
 291     gen->manager = zdd;
 292     gen->type = CUDD_GEN_ZDD_PATHS;
 293     gen->status = CUDD_GEN_EMPTY;
 294     gen->gen.cubes.cube = NULL;
 295     gen->gen.cubes.value = DD_ZERO_VAL;
 296     gen->stack.sp = 0;
 297     gen->stack.stack = NULL;
 298     gen->node = NULL;
 299
 300     nvars = zdd->sizeZ;
 301     gen->gen.cubes.cube = ALLOC(int,nvars);
 302     if (gen->gen.cubes.cube == NULL) {
 303         zdd->errorCode = CUDD_MEMORY_OUT;
 304         FREE(gen);
 305         return(NULL);
 306     }
 307     for (i = 0; i < nvars; i++) gen->gen.cubes.cube[i] = 2;
 308
 309     /* The maximum stack depth is one plus the number of variables.
 310     ** because a path may have nodes at all levels, including the
 311     ** constant level.
 312     */
 313     gen->stack.stack = ALLOC(DdNodePtr, nvars+1);
 314     if (gen->stack.stack == NULL) {
 315         zdd->errorCode = CUDD_MEMORY_OUT;
 316         FREE(gen->gen.cubes.cube);
 317         FREE(gen);
 318         return(NULL);
 319     }
 320     for (i = 0; i <= nvars; i++) gen->stack.stack[i] = NULL;
 321
 322     /* Find the first path of the ZDD. */
 323     gen->stack.stack[gen->stack.sp] = f; gen->stack.sp++;
 324
 325     while (1) {
 326         top = gen->stack.stack[gen->stack.sp-1];
 327         if (!cuddIsConstant(Cudd_Regular(top))) {
 328             /* Take the else branch first. */
 329             gen->gen.cubes.cube[Cudd_Regular(top)->index] = 0;
 330             next = cuddE(Cudd_Regular(top));
 331             gen->stack.stack[gen->stack.sp] = Cudd_Not(next); gen->stack.sp++;
 332         } else if (Cudd_Regular(top) == DD_ZERO(zdd)) {
 333             /* Backtrack. */
 334             while (1) {
 335                 if (gen->stack.sp == 1) {
 336                     /* The current node has no predecessor. */
 337                     gen->status = CUDD_GEN_EMPTY;
 338                     gen->stack.sp--;
 339                     goto done;
 340                 }
 341                 prev = Cudd_Regular(gen->stack.stack[gen->stack.sp-2]);
 342                 next = cuddT(prev);
 343                 if (next != top) { /* follow the then branch next */
 344                     gen->gen.cubes.cube[prev->index] = 1;
 345                     gen->stack.stack[gen->stack.sp-1] = next;
 346                     break;
 347                 }
 348                 /* Pop the stack and try again. */
 349                 gen->gen.cubes.cube[prev->index] = 2;
 350                 gen->stack.sp--;
 351                 top = gen->stack.stack[gen->stack.sp-1];
 352             }
 353         } else {
 354             gen->status = CUDD_GEN_NONEMPTY;
 355             gen->gen.cubes.value = cuddV(Cudd_Regular(top));
 356             goto done;
 357         }
 358     }
 359
 360 done:
 361     *path = gen->gen.cubes.cube;
 362     return(gen);
 363
 364 } /* end of Cudd_zddFirstPath */
 365
 366
 367 /**Function********************************************************************
 368
 369   Synopsis    [Generates the next path of a ZDD.]
 370
 371   Description [Generates the next path of a ZDD onset,
 372   using generator gen. Returns 0 if the enumeration is completed; 1
 373   otherwise.]
 374
 375   SideEffects [The path is returned as a side effect. The
 376   generator is modified.]
 377
 378   SeeAlso     [Cudd_zddForeachPath Cudd_zddFirstPath Cudd_GenFree
 379   Cudd_IsGenEmpty]
 380
 381 ******************************************************************************/
 382 int
 383 Cudd_zddNextPath(
 384   DdGen * gen,
 385   int ** path)
 386 {
 387     DdNode *top, *next, *prev;
 388     DdManager *zdd = gen->manager;
 389
 390     /* Backtrack from previously reached terminal node. */
 391     while (1) {
 392         if (gen->stack.sp == 1) {
 393             /* The current node has no predecessor. */
 394             gen->status = CUDD_GEN_EMPTY;
 395             gen->stack.sp--;
 396             goto done;
 397         }
 398         top = gen->stack.stack[gen->stack.sp-1];
 399         prev = Cudd_Regular(gen->stack.stack[gen->stack.sp-2]);
 400         next = cuddT(prev);
 401         if (next != top) { /* follow the then branch next */
 402             gen->gen.cubes.cube[prev->index] = 1;
 403             gen->stack.stack[gen->stack.sp-1] = next;
 404             break;
 405         }
 406         /* Pop the stack and try again. */
 407         gen->gen.cubes.cube[prev->index] = 2;
 408         gen->stack.sp--;
 409     }
 410
 411     while (1) {
 412         top = gen->stack.stack[gen->stack.sp-1];
 413         if (!cuddIsConstant(Cudd_Regular(top))) {
 414             /* Take the else branch first. */
 415             gen->gen.cubes.cube[Cudd_Regular(top)->index] = 0;
 416             next = cuddE(Cudd_Regular(top));
 417             gen->stack.stack[gen->stack.sp] = Cudd_Not(next); gen->stack.sp++;
 418         } else if (Cudd_Regular(top) == DD_ZERO(zdd)) {
 419             /* Backtrack. */
 420             while (1) {
 421                 if (gen->stack.sp == 1) {
 422                     /* The current node has no predecessor. */
 423                     gen->status = CUDD_GEN_EMPTY;
 424                     gen->stack.sp--;
 425                     goto done;
 426                 }
 427                 prev = Cudd_Regular(gen->stack.stack[gen->stack.sp-2]);
 428                 next = cuddT(prev);
 429                 if (next != top) { /* follow the then branch next */
 430                     gen->gen.cubes.cube[prev->index] = 1;
 431                     gen->stack.stack[gen->stack.sp-1] = next;
 432                     break;
 433                 }
 434                 /* Pop the stack and try again. */
 435                 gen->gen.cubes.cube[prev->index] = 2;
 436                 gen->stack.sp--;
 437                 top = gen->stack.stack[gen->stack.sp-1];
 438             }
 439         } else {
 440             gen->status = CUDD_GEN_NONEMPTY;
 441             gen->gen.cubes.value = cuddV(Cudd_Regular(top));
 442             goto done;
 443         }
 444     }
 445
 446 done:
 447     if (gen->status == CUDD_GEN_EMPTY) return(0);
 448     *path = gen->gen.cubes.cube;
 449     return(1);
 450
 451 } /* end of Cudd_zddNextPath */
 452
 453
 454 /**Function********************************************************************
 455
 456   Synopsis    [Converts a path of a ZDD representing a cover to a string.]
 457
 458   Description [Converts a path of a ZDD representing a cover to a
 459   string.  The string represents an implicant of the cover.  The path
 460   is typically produced by Cudd_zddForeachPath.  Returns a pointer to
 461   the string if successful; NULL otherwise.  If the str input is NULL,
 462   it allocates a new string.  The string passed to this function must
 463   have enough room for all variables and for the terminator.]
 464
 465   SideEffects [None]
 466
 467   SeeAlso     [Cudd_zddForeachPath]
 468
 469 ******************************************************************************/
 470 char *
 471 Cudd_zddCoverPathToString(
 472   DdManager *zdd                /* DD manager */,
 473   int *path                     /* path of ZDD representing a cover */,
 474   char *str                     /* pointer to string to use if != NULL */
 475   )
 476 {
 477     int nvars = zdd->sizeZ;
 478     int i;
 479     char *res;
 480
 481     if (nvars & 1) return(NULL);
 482     nvars >>= 1;
 483     if (str == NULL) {
 484         res = ALLOC(char, nvars+1);
 485         if (res == NULL) return(NULL);
 486     } else {
 487         res = str;
 488     }
 489     for (i = 0; i < nvars; i++) {
 490         int v = (path[2*i] << 2) | path[2*i+1];
 491         switch (v) {
 492         case 0:
 493         case 2:
 494         case 8:
 495         case 10:
 496             res[i] = '-';
 497             break;
 498         case 1:
 499         case 9:
 500             res[i] = '0';
 501             break;
 502         case 4:
 503         case 6:
 504             res[i] = '1';
 505             break;
 506         default:
 507             res[i] = '?';
 508         }
 509     }
 510     res[nvars] = 0;
 511
 512     return(res);
 513
 514 } /* end of Cudd_zddCoverPathToString */
 515
 516
 517 /**Function********************************************************************
 518
 519   Synopsis    [Writes a dot file representing the argument ZDDs.]
 520
 521   Description [Writes a file representing the argument ZDDs in a format
 522   suitable for the graph drawing program dot.
 523   It returns 1 in case of success; 0 otherwise (e.g., out-of-memory,
 524   file system full).
 525   Cudd_zddDumpDot does not close the file: This is the caller
 526   responsibility. Cudd_zddDumpDot uses a minimal unique subset of the
 527   hexadecimal address of a node as name for it.
 528   If the argument inames is non-null, it is assumed to hold the pointers
 529   to the names of the inputs. Similarly for onames.
 530   Cudd_zddDumpDot uses the following convention to draw arcs:
 531     <ul>
 532     <li> solid line: THEN arcs;
 533     <li> dashed line: ELSE arcs.
 534     </ul>
 535   The dot options are chosen so that the drawing fits on a letter-size
 536   sheet.
 537   ]
 538
 539   SideEffects [None]
 540
 541   SeeAlso     [Cudd_DumpDot Cudd_zddPrintDebug]
 542
 543 ******************************************************************************/
 544 int
 545 Cudd_zddDumpDot(
 546   DdManager * dd /* manager */,
 547   int  n /* number of output nodes to be dumped */,
 548   DdNode ** f /* array of output nodes to be dumped */,
 549   char ** inames /* array of input names (or NULL) */,
 550   char ** onames /* array of output names (or NULL) */,
 551   FILE * fp /* pointer to the dump file */)
 552 {
 553     DdNode      *support = NULL;
 554     DdNode      *scan;
 555     int         *sorted = NULL;
 556     int         nvars = dd->sizeZ;
 557     st_table    *visited = NULL;
 558     st_generator *gen;
 559     int         retval;
 560     int         i, j;
 561     int         slots;
 562     DdNodePtr   *nodelist;
 563     long        refAddr, diff, mask;
 564
 565     /* Build a bit array with the support of f. */
 566     sorted = ALLOC(int,nvars);
 567     if (sorted == NULL) {
 568         dd->errorCode = CUDD_MEMORY_OUT;
 569         goto failure;
 570     }
 571     for (i = 0; i < nvars; i++) sorted[i] = 0;
 572
 573     /* Take the union of the supports of each output function. */
 574     for (i = 0; i < n; i++) {
 575         support = Cudd_Support(dd,f[i]);
 576         if (support == NULL) goto failure;
 577         cuddRef(support);
 578         scan = support;
 579         while (!cuddIsConstant(scan)) {
 580             sorted[scan->index] = 1;
 581             scan = cuddT(scan);
 582         }
 583         Cudd_RecursiveDeref(dd,support);
 584     }
 585     support = NULL; /* so that we do not try to free it in case of failure */
 586
 587     /* Initialize symbol table for visited nodes. */
 588     visited = st_init_table(st_ptrcmp, st_ptrhash);
 589     if (visited == NULL) goto failure;
 590
 591     /* Collect all the nodes of this DD in the symbol table. */
 592     for (i = 0; i < n; i++) {
 593         retval = cuddCollectNodes(f[i],visited);
 594         if (retval == 0) goto failure;
 595     }
 596
 597     /* Find how many most significant hex digits are identical
 598     ** in the addresses of all the nodes. Build a mask based
 599     ** on this knowledge, so that digits that carry no information
 600     ** will not be printed. This is done in two steps.
 601     **  1. We scan the symbol table to find the bits that differ
 602     **     in at least 2 addresses.
 603     **  2. We choose one of the possible masks. There are 8 possible
 604     **     masks for 32-bit integer, and 16 possible masks for 64-bit
 605     **     integers.
 606     */
 607
 608     /* Find the bits that are different. */
 609     refAddr = (long) f[0];
 610     diff = 0;
 611     gen = st_init_gen(visited);
 612     while (st_gen(gen, &scan, NULL)) {
 613         diff |= refAddr ^ (long) scan;
 614     }
 615     st_free_gen(gen);
 616
 617     /* Choose the mask. */
 618     for (i = 0; (unsigned) i < 8 * sizeof(long); i += 4) {
 619         mask = (1 << i) - 1;
 620         if (diff <= mask) break;
 621     }
 622
 623     /* Write the header and the global attributes. */
 624     retval = fprintf(fp,"digraph \"ZDD\" {\n");
 625     if (retval == EOF) return(0);
 626     retval = fprintf(fp,
 627         "size = \"7.5,10\"\ncenter = true;\nedge [dir = none];\n");
 628     if (retval == EOF) return(0);
 629
 630     /* Write the input name subgraph by scanning the support array. */
 631     retval = fprintf(fp,"{ node [shape = plaintext];\n");
 632     if (retval == EOF) goto failure;
 633     retval = fprintf(fp,"  edge [style = invis];\n");
 634     if (retval == EOF) goto failure;
 635     /* We use a name ("CONST NODES") with an embedded blank, because
 636     ** it is unlikely to appear as an input name.
 637     */
 638     retval = fprintf(fp,"  \"CONST NODES\" [style = invis];\n");
 639     if (retval == EOF) goto failure;
 640     for (i = 0; i < nvars; i++) {
 641         if (sorted[dd->invpermZ[i]]) {
 642             if (inames == NULL) {
 643                 retval = fprintf(fp,"\" %d \" -> ", dd->invpermZ[i]);
 644             } else {
 645                 retval = fprintf(fp,"\" %s \" -> ", inames[dd->invpermZ[i]]);
 646             }
 647             if (retval == EOF) goto failure;
 648         }
 649     }
 650     retval = fprintf(fp,"\"CONST NODES\"; \n}\n");
 651     if (retval == EOF) goto failure;
 652
 653     /* Write the output node subgraph. */
 654     retval = fprintf(fp,"{ rank = same; node [shape = box]; edge [style = invis];\n");
 655     if (retval == EOF) goto failure;
 656     for (i = 0; i < n; i++) {
 657         if (onames == NULL) {
 658             retval = fprintf(fp,"\"F%d\"", i);
 659         } else {
 660             retval = fprintf(fp,"\"  %s  \"", onames[i]);
 661         }
 662         if (retval == EOF) goto failure;
 663         if (i == n - 1) {
 664             retval = fprintf(fp,"; }\n");
 665         } else {
 666             retval = fprintf(fp," -> ");
 667         }
 668         if (retval == EOF) goto failure;
 669     }
 670
 671     /* Write rank info: All nodes with the same index have the same rank. */
 672     for (i = 0; i < nvars; i++) {
 673         if (sorted[dd->invpermZ[i]]) {
 674             retval = fprintf(fp,"{ rank = same; ");
 675             if (retval == EOF) goto failure;
 676             if (inames == NULL) {
 677                 retval = fprintf(fp,"\" %d \";\n", dd->invpermZ[i]);
 678             } else {
 679                 retval = fprintf(fp,"\" %s \";\n", inames[dd->invpermZ[i]]);
 680             }
 681             if (retval == EOF) goto failure;
 682             nodelist = dd->subtableZ[i].nodelist;
 683             slots = dd->subtableZ[i].slots;
 684             for (j = 0; j < slots; j++) {
 685                 scan = nodelist[j];
 686                 while (scan != NULL) {
 687                     if (st_is_member(visited,(char *) scan)) {
 688                         retval = fprintf(fp,"\"%p\";\n", (void *)
 689                                          ((mask & (ptrint) scan) /
 690                                           sizeof(DdNode)));
 691                         if (retval == EOF) goto failure;
 692                     }
 693                     scan = scan->next;
 694                 }
 695             }
 696             retval = fprintf(fp,"}\n");
 697             if (retval == EOF) goto failure;
 698         }
 699     }
 700
 701     /* All constants have the same rank. */
 702     retval = fprintf(fp,
 703         "{ rank = same; \"CONST NODES\";\n{ node [shape = box]; ");
 704     if (retval == EOF) goto failure;
 705     nodelist = dd->constants.nodelist;
 706     slots = dd->constants.slots;
 707     for (j = 0; j < slots; j++) {
 708         scan = nodelist[j];
 709         while (scan != NULL) {
 710             if (st_is_member(visited,(char *) scan)) {
 711                 retval = fprintf(fp,"\"%p\";\n", (void *)
 712                                  ((mask & (ptrint) scan) / sizeof(DdNode)));
 713                 if (retval == EOF) goto failure;
 714             }
 715             scan = scan->next;
 716         }
 717     }
 718     retval = fprintf(fp,"}\n}\n");
 719     if (retval == EOF) goto failure;
 720
 721     /* Write edge info. */
 722     /* Edges from the output nodes. */
 723     for (i = 0; i < n; i++) {
 724         if (onames == NULL) {
 725             retval = fprintf(fp,"\"F%d\"", i);
 726         } else {
 727             retval = fprintf(fp,"\"  %s  \"", onames[i]);
 728         }
 729         if (retval == EOF) goto failure;
 730         retval = fprintf(fp," -> \"%p\" [style = solid];\n",
 731                          (void *) ((mask & (ptrint) f[i]) /
 732                                           sizeof(DdNode)));
 733         if (retval == EOF) goto failure;
 734     }
 735
 736     /* Edges from internal nodes. */
 737     for (i = 0; i < nvars; i++) {
 738         if (sorted[dd->invpermZ[i]]) {
 739             nodelist = dd->subtableZ[i].nodelist;
 740             slots = dd->subtableZ[i].slots;
 741             for (j = 0; j < slots; j++) {
 742                 scan = nodelist[j];
 743                 while (scan != NULL) {
 744                     if (st_is_member(visited,(char *) scan)) {
 745                         retval = fprintf(fp,
 746                             "\"%p\" -> \"%p\";\n",
 747                             (void *) ((mask & (ptrint) scan) / sizeof(DdNode)),
 748                             (void *) ((mask & (ptrint) cuddT(scan)) /
 749                                       sizeof(DdNode)));
 750                         if (retval == EOF) goto failure;
 751                         retval = fprintf(fp,
 752                                          "\"%p\" -> \"%p\" [style = dashed];\n",
 753                                          (void *) ((mask & (ptrint) scan)
 754                                                    / sizeof(DdNode)),
 755                                          (void *) ((mask & (ptrint)
 756                                                     cuddE(scan)) /
 757                                                    sizeof(DdNode)));
 758                         if (retval == EOF) goto failure;
 759                     }
 760                     scan = scan->next;
 761                 }
 762             }
 763         }
 764     }
 765
 766     /* Write constant labels. */
 767     nodelist = dd->constants.nodelist;
 768     slots = dd->constants.slots;
 769     for (j = 0; j < slots; j++) {
 770         scan = nodelist[j];
 771         while (scan != NULL) {
 772             if (st_is_member(visited,(char *) scan)) {
 773                 retval = fprintf(fp,"\"%p\" [label = \"%g\"];\n",
 774                                  (void *) ((mask & (ptrint) scan) /
 775                                            sizeof(DdNode)),
 776                                  cuddV(scan));
 777                 if (retval == EOF) goto failure;
 778             }
 779             scan = scan->next;
 780         }
 781     }
 782
 783     /* Write trailer and return. */
 784     retval = fprintf(fp,"}\n");
 785     if (retval == EOF) goto failure;
 786
 787     st_free_table(visited);
 788     FREE(sorted);
 789     return(1);
 790
 791 failure:
 792     if (sorted != NULL) FREE(sorted);
 793     if (visited != NULL) st_free_table(visited);
 794     return(0);
 795
 796 } /* end of Cudd_zddDumpBlif */
 797
 798
 799 /*---------------------------------------------------------------------------*/
 800 /* Definition of internal functions                                          */
 801 /*---------------------------------------------------------------------------*/
 802
 803
 804 /**Function********************************************************************
 805
 806   Synopsis [Prints a ZDD to the standard output. One line per node is
 807   printed.]
 808
 809   Description [Prints a ZDD to the standard output. One line per node is
 810   printed. Returns 1 if successful; 0 otherwise.]
 811
 812   SideEffects [None]
 813
 814   SeeAlso     [Cudd_zddPrintDebug]
 815
 816 ******************************************************************************/
 817 int
 818 cuddZddP(
 819   DdManager * zdd,
 820   DdNode * f)
 821 {
 822     int retval;
 823     st_table *table = st_init_table(st_ptrcmp, st_ptrhash);
 824
 825     if (table == NULL) return(0);
 826
 827     retval = zp2(zdd, f, table);
 828     st_free_table(table);
 829     (void) fputc('\n', zdd->out);
 830     return(retval);
 831
 832 } /* end of cuddZddP */
 833
 834
 835 /*---------------------------------------------------------------------------*/
 836 /* Definition of static functions                                            */
 837 /*---------------------------------------------------------------------------*/
 838
 839
 840 /**Function********************************************************************
 841
 842   Synopsis [Performs the recursive step of cuddZddP.]
 843
 844   Description [Performs the recursive step of cuddZddP. Returns 1 in
 845   case of success; 0 otherwise.]
 846
 847   SideEffects [None]
 848
 849   SeeAlso     []
 850
 851 ******************************************************************************/
 852 static int
 853 zp2(
 854   DdManager * zdd,
 855   DdNode * f,
 856   st_table * t)
 857 {
 858     DdNode      *n;
 859     int         T, E;
 860     DdNode      *base = DD_ONE(zdd);
 861
 862     if (f == NULL)
 863         return(0);
 864
 865     if (Cudd_IsConstant(f)) {
 866         (void)fprintf(zdd->out, "ID = %d\n", (f == base));
 867         return(1);
 868     }
 869     if (st_is_member(t, (char *)f) == 1)
 870         return(1);
 871
 872     if (st_insert(t, (char *) f, NULL) == ST_OUT_OF_MEM)
 873         return(0);
 874
 875 #if SIZEOF_VOID_P == 8
 876     (void) fprintf(zdd->out, "ID = 0x%lx\tindex = %u\tr = %u\t",
 877         (ptruint)f / (ptruint) sizeof(DdNode), f->index, f->ref);
 878 #else
 879     (void) fprintf(zdd->out, "ID = 0x%x\tindex = %hu\tr = %hu\t",
 880         (ptruint)f / (ptruint) sizeof(DdNode), f->index, f->ref);
 881 #endif
 882
 883     n = cuddT(f);
 884     if (Cudd_IsConstant(n)) {
 885         (void) fprintf(zdd->out, "T = %d\t\t", (n == base));
 886         T = 1;
 887     } else {
 888 #if SIZEOF_VOID_P == 8
 889         (void) fprintf(zdd->out, "T = 0x%lx\t", (ptruint) n /
 890                        (ptruint) sizeof(DdNode));
 891 #else
 892         (void) fprintf(zdd->out, "T = 0x%x\t", (ptruint) n /
 893                        (ptruint) sizeof(DdNode));
 894 #endif
 895         T = 0;
 896     }
 897
 898     n = cuddE(f);
 899     if (Cudd_IsConstant(n)) {
 900         (void) fprintf(zdd->out, "E = %d\n", (n == base));
 901         E = 1;
 902     } else {
 903 #if SIZEOF_VOID_P == 8
 904         (void) fprintf(zdd->out, "E = 0x%lx\n", (ptruint) n /
 905                       (ptruint) sizeof(DdNode));
 906 #else
 907         (void) fprintf(zdd->out, "E = 0x%x\n", (ptruint) n /
 908                        (ptruint) sizeof(DdNode));
 909 #endif
 910         E = 0;
 911     }
 912
 913     if (E == 0)
 914         if (zp2(zdd, cuddE(f), t) == 0) return(0);
 915     if (T == 0)
 916         if (zp2(zdd, cuddT(f), t) == 0) return(0);
 917     return(1);
 918
 919 } /* end of zp2 */
 920
 921
 922 /**Function********************************************************************
 923
 924   Synopsis    [Performs the recursive step of Cudd_zddPrintMinterm.]
 925
 926   Description []
 927
 928   SideEffects [None]
 929
 930   SeeAlso     []
 931
 932 ******************************************************************************/
 933 static void
 934 zdd_print_minterm_aux(
 935   DdManager * zdd /* manager */,
 936   DdNode * node /* current node */,
 937   int  level /* depth in the recursion */,
 938   int * list /* current recursion path */)
 939 {
 940     DdNode      *Nv, *Nnv;
 941     int         i, v;
 942     DdNode      *base = DD_ONE(zdd);
 943
 944     if (Cudd_IsConstant(node)) {
 945         if (node == base) {
 946             /* Check for missing variable. */
 947             if (level != zdd->sizeZ) {
 948                 list[zdd->invpermZ[level]] = 0;
 949                 zdd_print_minterm_aux(zdd, node, level + 1, list);
 950                 return;
 951             }
 952             /* Terminal case: Print one cube based on the current recursion
 953             ** path.
 954             */
 955             for (i = 0; i < zdd->sizeZ; i++) {
 956                 v = list[i];
 957                 if (v == 0)
 958                     (void) fprintf(zdd->out,"0");
 959                 else if (v == 1)
 960                     (void) fprintf(zdd->out,"1");
 961                 else if (v == 3)
 962                     (void) fprintf(zdd->out,"@");       /* should never happen */
 963                 else
 964                     (void) fprintf(zdd->out,"-");
 965             }
 966             (void) fprintf(zdd->out," 1\n");
 967         }
 968     } else {
 969         /* Check for missing variable. */
 970         if (level != cuddIZ(zdd,node->index)) {
 971             list[zdd->invpermZ[level]] = 0;
 972             zdd_print_minterm_aux(zdd, node, level + 1, list);
 973             return;
 974         }
 975
 976         Nnv = cuddE(node);
 977         Nv = cuddT(node);
 978         if (Nv == Nnv) {
 979             list[node->index] = 2;
 980             zdd_print_minterm_aux(zdd, Nnv, level + 1, list);
 981             return;
 982         }
 983
 984         list[node->index] = 1;
 985         zdd_print_minterm_aux(zdd, Nv, level + 1, list);
 986         list[node->index] = 0;
 987         zdd_print_minterm_aux(zdd, Nnv, level + 1, list);
 988     }
 989     return;
 990
 991 } /* end of zdd_print_minterm_aux */
 992
 993
 994 /**Function********************************************************************
 995
 996   Synopsis    [Performs the recursive step of Cudd_zddPrintCover.]
 997
 998   Description []
 999
1000   SideEffects [None]
1001
1002   SeeAlso     []
1003
1004 ******************************************************************************/
1005 static void
1006 zddPrintCoverAux(
1007   DdManager * zdd /* manager */,
1008   DdNode * node /* current node */,
1009   int  level /* depth in the recursion */,
1010   int * list /* current recursion path */)
1011 {
1012     DdNode      *Nv, *Nnv;
1013     int         i, v;
1014     DdNode      *base = DD_ONE(zdd);
1015
1016     if (Cudd_IsConstant(node)) {
1017         if (node == base) {
1018             /* Check for missing variable. */
1019             if (level != zdd->sizeZ) {
1020                 list[zdd->invpermZ[level]] = 0;
1021                 zddPrintCoverAux(zdd, node, level + 1, list);
1022                 return;
1023             }
1024             /* Terminal case: Print one cube based on the current recursion
1025             ** path.
1026             */
1027             for (i = 0; i < zdd->sizeZ; i += 2) {
1028                 v = list[i] * 4 + list[i+1];
1029                 if (v == 0)
1030                     (void) putc('-',zdd->out);
1031                 else if (v == 4)
1032                     (void) putc('1',zdd->out);
1033                 else if (v == 1)
1034                     (void) putc('0',zdd->out);
1035                 else
1036                     (void) putc('@',zdd->out); /* should never happen */
1037             }
1038             (void) fprintf(zdd->out," 1\n");
1039         }
1040     } else {
1041         /* Check for missing variable. */
1042         if (level != cuddIZ(zdd,node->index)) {
1043             list[zdd->invpermZ[level]] = 0;
1044             zddPrintCoverAux(zdd, node, level + 1, list);
1045             return;
1046         }
1047
1048         Nnv = cuddE(node);
1049         Nv = cuddT(node);
1050         if (Nv == Nnv) {
1051             list[node->index] = 2;
1052             zddPrintCoverAux(zdd, Nnv, level + 1, list);
1053             return;
1054         }
1055
1056         list[node->index] = 1;
1057         zddPrintCoverAux(zdd, Nv, level + 1, list);
1058         list[node->index] = 0;
1059         zddPrintCoverAux(zdd, Nnv, level + 1, list);
1060     }
1061     return;
1062
1063 } /* end of zddPrintCoverAux */