distr/dddmp/dddmpStoreMisc.c

   1 /**CFile**********************************************************************
   2
   3   FileName     [dddmpStoreMisc.c]
   4
   5   PackageName  [dddmp]
   6
   7   Synopsis     [Functions to write out bdds to file in prefixed
   8     and in Blif form.]
   9
  10   Description  [Functions to write out bdds to file.
  11     BDDs are represended on file in text format.
  12     Each node is stored as a multiplexer in a prefix notation format for
  13     the prefix notation file or in PLA format for the blif file.
  14   ]
  15
  16   Author       [Gianpiero Cabodi and Stefano Quer]
  17
  18   Copyright    [
  19     Copyright (c) 2004 by Politecnico di Torino.
  20     All Rights Reserved. This software is for educational purposes only.
  21     Permission is given to academic institutions to use, copy, and modify
  22     this software and its documentation provided that this introductory
  23     message is not removed, that this software and its documentation is
  24     used for the institutions' internal research and educational purposes,
  25     and that no monies are exchanged. No guarantee is expressed or implied
  26     by the distribution of this code.
  27     Send bug-reports and/or questions to:
  28     {gianpiero.cabodi,stefano.quer}@polito.it.
  29     ]
  30
  31 ******************************************************************************/
  32
  33 #include "dddmpInt.h"
  34
  35 /*---------------------------------------------------------------------------*/
  36 /* Stucture declarations                                                     */
  37 /*---------------------------------------------------------------------------*/
  38
  39 /*---------------------------------------------------------------------------*/
  40 /* Type declarations                                                         */
  41 /*---------------------------------------------------------------------------*/
  42
  43 /*---------------------------------------------------------------------------*/
  44 /* Variable declarations                                                     */
  45 /*---------------------------------------------------------------------------*/
  46
  47 /*---------------------------------------------------------------------------*/
  48 /* Macro declarations                                                        */
  49 /*---------------------------------------------------------------------------*/
  50
  51 /**AutomaticStart*************************************************************/
  52
  53 /*---------------------------------------------------------------------------*/
  54 /* Static function prototypes                                                */
  55 /*---------------------------------------------------------------------------*/
  56
  57 static int DddmpCuddDdArrayStorePrefix(DdManager *ddMgr, int n, DdNode **f, char **inputNames, char **outputNames, char *modelName, FILE *fp);
  58 static int DddmpCuddDdArrayStorePrefixBody(DdManager *ddMgr, int n, DdNode **f, char **inputNames, char **outputNames, FILE *fp);
  59 static int DddmpCuddDdArrayStorePrefixStep(DdManager * ddMgr, DdNode * f, FILE * fp, st_table * visited, char ** names);
  60 static int DddmpCuddDdArrayStoreBlif(DdManager *ddMgr, int n, DdNode **f, char **inputNames, char **outputNames, char *modelName, FILE *fp);
  61 static int DddmpCuddDdArrayStoreBlifBody(DdManager *ddMgr, int n, DdNode **f, char **inputNames, char **outputNames, FILE *fp);
  62 static int DddmpCuddDdArrayStoreBlifStep(DdManager *ddMgr, DdNode *f, FILE *fp, st_table *visited, char **names);
  63 static int DddmpCuddDdArrayStoreSmv(DdManager *ddMgr, int n, DdNode **f, char **inputNames, char **outputNames, char *modelName, FILE *fp);
  64 static int DddmpCuddDdArrayStoreSmvBody(DdManager *ddMgr, int n, DdNode **f, char **inputNames, char **outputNames, FILE *fp);
  65 static int DddmpCuddDdArrayStoreSmvStep(DdManager * ddMgr, DdNode * f, FILE * fp, st_table * visited, char ** names);
  66
  67 /**AutomaticEnd***************************************************************/
  68
  69 /*---------------------------------------------------------------------------*/
  70 /* Definition of exported functions                                          */
  71 /*---------------------------------------------------------------------------*/
  72
  73 /**Function********************************************************************
  74
  75   Synopsis     [Writes a dump file representing the argument BDD in
  76     a prefix notation.]
  77
  78   Description  [Dumps the argument BDD to file.
  79     Dumping is done through Dddmp_cuddBddArrayStorePrefix.
  80     A dummy array of 1 BDD root is used for this purpose.
  81     ]
  82
  83   SideEffects  []
  84
  85   SeeAlso      [Dddmp_cuddBddStore]
  86
  87 ******************************************************************************/
  88
  89 int
  90 Dddmp_cuddBddStorePrefix (
  91   DdManager *ddMgr     /* IN: DD Manager */,
  92   int nRoots           /* IN: Number of BDD roots */,
  93   DdNode *f            /* IN: BDD root to be stored */,
  94   char **inputNames    /* IN: Array of variable names */,
  95   char **outputNames   /* IN: Array of root names */,
  96   char *modelName      /* IN: Model Name */,
  97   char *fileName       /* IN: File name */,
  98   FILE *fp             /* IN: File pointer to the store file */
  99   )
 100 {
 101   int retValue;
 102   DdNode *tmpArray[1];
 103
 104   tmpArray[0] = f;
 105
 106   retValue = Dddmp_cuddBddArrayStorePrefix (ddMgr, 1, tmpArray,
 107     inputNames, outputNames, modelName, fileName, fp);
 108
 109   return (retValue);
 110 }
 111
 112 /**Function********************************************************************
 113
 114   Synopsis     [Writes a dump file representing the argument BDD in
 115     a prefix notation.]
 116
 117   Description  [Dumps the argument BDD to file.
 118     Dumping is done through Dddmp_cuddBddArrayStorePrefix.
 119     A dummy array of 1 BDD root is used for this purpose.
 120     ]
 121
 122   SideEffects  []
 123
 124   SeeAlso      [Dddmp_cuddBddArrayStore]
 125
 126 ******************************************************************************/
 127
 128 int
 129 Dddmp_cuddBddArrayStorePrefix (
 130   DdManager *ddMgr       /* IN: DD Manager */,
 131   int nroots             /* IN: number of output BDD roots to be stored */,
 132   DdNode **f             /* IN: array of BDD roots to be stored */,
 133   char **inputNames      /* IN: array of variable names (or NULL) */,
 134   char **outputNames     /* IN: array of root names (or NULL) */,
 135   char *modelName        /* IN: Model Name */,
 136   char *fname            /* IN: File name */,
 137   FILE *fp               /* IN: File pointer to the store file */
 138   )
 139 {
 140   int retValue;
 141   int fileToClose = 0;
 142
 143 #ifdef DDDMP_DEBUG
 144 #ifndef __alpha__
 145   int retValueBis;
 146
 147   retValueBis = Cudd_DebugCheck (ddMgr);
 148   if (retValueBis == 1) {
 149     fprintf (stderr, "Inconsistency Found During BDD Store.\n");
 150     fflush (stderr);
 151   } else {
 152     if (retValueBis == CUDD_OUT_OF_MEM) {
 153       fprintf (stderr, "Out of Memory During BDD Store.\n");
 154       fflush (stderr);
 155     }
 156   }
 157 #endif
 158 #endif
 159
 160   /*
 161    *  Check if File needs to be opened in the proper mode.
 162    */
 163
 164   if (fp == NULL) {
 165     fp = fopen (fname, "w");
 166     Dddmp_CheckAndGotoLabel (fp==NULL, "Error opening file.",
 167       failure);
 168     fileToClose = 1;
 169   }
 170
 171   retValue = DddmpCuddDdArrayStorePrefix (ddMgr, nroots, f,
 172     inputNames, outputNames, modelName, fp);
 173
 174   if (fileToClose) {
 175     fclose (fp);
 176   }
 177
 178 #ifdef DDDMP_DEBUG
 179 #ifndef __alpha__
 180   retValueBis = Cudd_DebugCheck (ddMgr);
 181   if (retValueBis == 1) {
 182     fprintf (stderr, "Inconsistency Found During BDD Store.\n");
 183     fflush (stderr);
 184   } else {
 185     if (retValueBis == CUDD_OUT_OF_MEM) {
 186       fprintf (stderr, "Out of Memory During BDD Store.\n");
 187       fflush (stderr);
 188     }
 189   }
 190 #endif
 191 #endif
 192
 193   return (retValue);
 194
 195   failure:
 196     return (DDDMP_FAILURE);
 197 }
 198
 199 /**Function********************************************************************
 200
 201   Synopsis     [Writes a dump file representing the argument BDD in
 202     a Blif/Exlif notation.]
 203
 204   Description  [Dumps the argument BDD to file.
 205     Dumping is done through Dddmp_cuddBddArrayStoreBlif.
 206     A dummy array of 1 BDD root is used for this purpose.
 207     ]
 208
 209   SideEffects  []
 210
 211   SeeAlso      [Dddmp_cuddBddStorePrefix]
 212
 213 ******************************************************************************/
 214
 215 int
 216 Dddmp_cuddBddStoreBlif (
 217   DdManager *ddMgr     /* IN: DD Manager */,
 218   int nRoots           /* IN: Number of BDD roots */,
 219   DdNode *f            /* IN: BDD root to be stored */,
 220   char **inputNames    /* IN: Array of variable names */,
 221   char **outputNames   /* IN: Array of root names */,
 222   char *modelName      /* IN: Model Name */,
 223   char *fileName       /* IN: File name */,
 224   FILE *fp             /* IN: File pointer to the store file */
 225   )
 226 {
 227   int retValue;
 228   DdNode *tmpArray[1];
 229
 230   tmpArray[0] = f;
 231
 232   retValue = Dddmp_cuddBddArrayStoreBlif (ddMgr, 1, tmpArray,
 233     inputNames, outputNames, modelName, fileName, fp);
 234
 235   return (retValue);
 236 }
 237
 238 /**Function********************************************************************
 239
 240   Synopsis     [Writes a dump file representing the argument BDD in
 241     a Blif/Exlif notation.]
 242
 243   Description  [Dumps the argument BDD to file.
 244     Dumping is done through Dddmp_cuddBddArrayStoreBLif.
 245     A dummy array of 1 BDD root is used for this purpose.
 246     ]
 247
 248   SideEffects  []
 249
 250   SeeAlso      [Dddmp_cuddBddArrayStorePrefix]
 251
 252 ******************************************************************************/
 253
 254 int
 255 Dddmp_cuddBddArrayStoreBlif (
 256   DdManager *ddMgr       /* IN: DD Manager */,
 257   int nroots             /* IN: number of output BDD roots to be stored */,
 258   DdNode **f             /* IN: array of BDD roots to be stored */,
 259   char **inputNames      /* IN: array of variable names (or NULL) */,
 260   char **outputNames     /* IN: array of root names (or NULL) */,
 261   char *modelName        /* IN: Model Name */,
 262   char *fname            /* IN: File name */,
 263   FILE *fp               /* IN: File pointer to the store file */
 264   )
 265 {
 266   int retValue;
 267   int fileToClose = 0;
 268
 269 #ifdef DDDMP_DEBUG
 270 #ifndef __alpha__
 271   int retValueBis;
 272
 273   retValueBis = Cudd_DebugCheck (ddMgr);
 274   if (retValueBis == 1) {
 275     fprintf (stderr, "Inconsistency Found During BDD Store.\n");
 276     fflush (stderr);
 277   } else {
 278     if (retValueBis == CUDD_OUT_OF_MEM) {
 279       fprintf (stderr, "Out of Memory During BDD Store.\n");
 280       fflush (stderr);
 281     }
 282   }
 283 #endif
 284 #endif
 285
 286   /*
 287    *  Check if File needs to be opened in the proper mode.
 288    */
 289
 290   if (fp == NULL) {
 291     fp = fopen (fname, "w");
 292     Dddmp_CheckAndGotoLabel (fp==NULL, "Error opening file.",
 293       failure);
 294     fileToClose = 1;
 295   }
 296
 297   retValue = DddmpCuddDdArrayStoreBlif (ddMgr, nroots, f,
 298     inputNames, outputNames, modelName, fp);
 299
 300   if (fileToClose) {
 301     fclose (fp);
 302   }
 303
 304 #ifdef DDDMP_DEBUG
 305 #ifndef __alpha__
 306   retValueBis = Cudd_DebugCheck (ddMgr);
 307   if (retValueBis == 1) {
 308     fprintf (stderr, "Inconsistency Found During BDD Store.\n");
 309     fflush (stderr);
 310   } else {
 311     if (retValueBis == CUDD_OUT_OF_MEM) {
 312       fprintf (stderr, "Out of Memory During BDD Store.\n");
 313       fflush (stderr);
 314     }
 315   }
 316 #endif
 317 #endif
 318
 319   return (retValue);
 320
 321   failure:
 322     return (DDDMP_FAILURE);
 323 }
 324
 325 /**Function********************************************************************
 326
 327   Synopsis     [Writes a dump file representing the argument BDD in
 328     a prefix notation.]
 329
 330   Description  [Dumps the argument BDD to file.
 331     Dumping is done through Dddmp_cuddBddArrayStorePrefix.
 332     A dummy array of 1 BDD root is used for this purpose.
 333     ]
 334
 335   SideEffects  []
 336
 337   SeeAlso      [Dddmp_cuddBddStore]
 338
 339 ******************************************************************************/
 340
 341 int
 342 Dddmp_cuddBddStoreSmv (
 343   DdManager *ddMgr     /* IN: DD Manager */,
 344   int nRoots           /* IN: Number of BDD roots */,
 345   DdNode *f            /* IN: BDD root to be stored */,
 346   char **inputNames    /* IN: Array of variable names */,
 347   char **outputNames   /* IN: Array of root names */,
 348   char *modelName      /* IN: Model Name */,
 349   char *fileName       /* IN: File name */,
 350   FILE *fp             /* IN: File pointer to the store file */
 351   )
 352 {
 353   int retValue;
 354   DdNode *tmpArray[1];
 355
 356   tmpArray[0] = f;
 357
 358   retValue = Dddmp_cuddBddArrayStoreSmv (ddMgr, 1, tmpArray,
 359     inputNames, outputNames, modelName, fileName, fp);
 360
 361   return (retValue);
 362 }
 363
 364 /**Function********************************************************************
 365
 366   Synopsis     [Writes a dump file representing the argument BDD in
 367     a prefix notation.]
 368
 369   Description  [Dumps the argument BDD to file.
 370     Dumping is done through Dddmp_cuddBddArrayStorePrefix.
 371     A dummy array of 1 BDD root is used for this purpose.
 372     ]
 373
 374   SideEffects  []
 375
 376   SeeAlso      [Dddmp_cuddBddArrayStore]
 377
 378 ******************************************************************************/
 379
 380 int
 381 Dddmp_cuddBddArrayStoreSmv (
 382   DdManager *ddMgr       /* IN: DD Manager */,
 383   int nroots             /* IN: number of output BDD roots to be stored */,
 384   DdNode **f             /* IN: array of BDD roots to be stored */,
 385   char **inputNames      /* IN: array of variable names (or NULL) */,
 386   char **outputNames     /* IN: array of root names (or NULL) */,
 387   char *modelName        /* IN: Model Name */,
 388   char *fname            /* IN: File name */,
 389   FILE *fp               /* IN: File pointer to the store file */
 390   )
 391 {
 392   int retValue;
 393   int fileToClose = 0;
 394
 395 #ifdef DDDMP_DEBUG
 396 #ifndef __alpha__
 397   int retValueBis;
 398
 399   retValueBis = Cudd_DebugCheck (ddMgr);
 400   if (retValueBis == 1) {
 401     fprintf (stderr, "Inconsistency Found During BDD Store.\n");
 402     fflush (stderr);
 403   } else {
 404     if (retValueBis == CUDD_OUT_OF_MEM) {
 405       fprintf (stderr, "Out of Memory During BDD Store.\n");
 406       fflush (stderr);
 407     }
 408   }
 409 #endif
 410 #endif
 411
 412   /*
 413    *  Check if File needs to be opened in the proper mode.
 414    */
 415
 416   if (fp == NULL) {
 417     fp = fopen (fname, "w");
 418     Dddmp_CheckAndGotoLabel (fp==NULL, "Error opening file.",
 419       failure);
 420     fileToClose = 1;
 421   }
 422
 423   retValue = DddmpCuddDdArrayStoreSmv (ddMgr, nroots, f,
 424     inputNames, outputNames, modelName, fp);
 425
 426   if (fileToClose) {
 427     fclose (fp);
 428   }
 429
 430 #ifdef DDDMP_DEBUG
 431 #ifndef __alpha__
 432   retValueBis = Cudd_DebugCheck (ddMgr);
 433   if (retValueBis == 1) {
 434     fprintf (stderr, "Inconsistency Found During BDD Store.\n");
 435     fflush (stderr);
 436   } else {
 437     if (retValueBis == CUDD_OUT_OF_MEM) {
 438       fprintf (stderr, "Out of Memory During BDD Store.\n");
 439       fflush (stderr);
 440     }
 441   }
 442 #endif
 443 #endif
 444
 445   return (retValue);
 446
 447   failure:
 448     return (DDDMP_FAILURE);
 449 }
 450
 451 /*---------------------------------------------------------------------------*/
 452 /* Definition of static functions                                            */
 453 /*---------------------------------------------------------------------------*/
 454
 455 /**Function********************************************************************
 456
 457   Synopsis     [Internal function to writes a dump file representing the
 458     argument BDD in a prefix notation.]
 459
 460   Description  [One multiplexer is written for each BDD node.
 461     It returns 1 in case of success; 0 otherwise (e.g., out-of-memory, file
 462     system full, or an ADD with constants different from 0 and 1).
 463     It does not close the file: This is the caller responsibility.
 464     It uses a minimal unique subset of the hexadecimal address of a node as
 465     name for it.
 466     If the argument inputNames is non-null, it is assumed to hold the
 467     pointers to the names of the inputs. Similarly for outputNames.
 468     For each BDD node of function f, variable v, then child T, and else
 469     child E it stores:
 470     f = v * T + v' * E
 471     that is
 472     (OR f (AND v T) (AND (NOT v) E))
 473     If E is a complemented child this results in the following
 474     (OR f (AND v T) (AND (NOT v) (NOT E)))
 475     Comments (COMMENT) are added at the beginning of the description to
 476     describe inputs and outputs of the design.
 477     A buffer (BUF) is add on the output to cope with complemented functions.
 478     ]
 479
 480   SideEffects [None]
 481
 482   SeeAlso     [DddmpCuddDdArrayStoreBlif]
 483
 484 ******************************************************************************/
 485
 486 static int
 487 DddmpCuddDdArrayStorePrefix (
 488   DdManager *ddMgr    /* IN: Manager */,
 489   int n               /* IN: Number of output nodes to be dumped */,
 490   DdNode **f          /* IN: Array of output nodes to be dumped */,
 491   char **inputNames   /* IN: Array of input names (or NULL) */,
 492   char **outputNames  /* IN: Array of output names (or NULL) */,
 493   char *modelName     /* IN: Model name (or NULL) */,
 494   FILE *fp            /* IN: Pointer to the dump file */
 495   )
 496 {
 497   DdNode *support = NULL;
 498   DdNode *scan;
 499   int *sorted = NULL;
 500   int nVars = ddMgr->size;
 501   int retValue;
 502   int i;
 503
 504   /* Build a bit array with the support of f. */
 505   sorted = ALLOC(int, nVars);
 506   if (sorted == NULL) {
 507     ddMgr->errorCode = CUDD_MEMORY_OUT;
 508     Dddmp_CheckAndGotoLabel (1, "Allocation Error.", failure);
 509   }
 510   for (i = 0; i < nVars; i++) {
 511     sorted[i] = 0;
 512   }
 513
 514   /* Take the union of the supports of each output function. */
 515   support = Cudd_VectorSupport(ddMgr,f,n);
 516   Dddmp_CheckAndGotoLabel (support==NULL,
 517     "Error in function Cudd_VectorSupport.", failure);
 518   cuddRef(support);
 519   scan = support;
 520   while (!cuddIsConstant(scan)) {
 521     sorted[scan->index] = 1;
 522     scan = cuddT(scan);
 523   }
 524   Cudd_RecursiveDeref(ddMgr,support);
 525   /* so that we do not try to free it in case of failure */
 526   support = NULL;
 527
 528   /* Write the header (.model .inputs .outputs). */
 529   if (modelName == NULL) {
 530     retValue = fprintf (fp, "(COMMENT - model name: Unknown )\n");
 531   } else {
 532     retValue = fprintf (fp, "(COMMENT - model name: %s )\n", modelName);
 533   }
 534   if (retValue == EOF) {
 535     return(0);
 536   }
 537
 538   retValue = fprintf(fp, "(COMMENT - input names: ");
 539   if (retValue == EOF) {
 540     return(0);
 541   }
 542   /* Write the input list by scanning the support array. */
 543   for (i = 0; i < nVars; i++) {
 544     if (sorted[i]) {
 545       if (inputNames == NULL) {
 546         retValue = fprintf(fp," inNode%d", i);
 547       } else {
 548         retValue = fprintf(fp," %s", inputNames[i]);
 549       }
 550       Dddmp_CheckAndGotoLabel (retValue==EOF,
 551         "Error during file store.", failure);
 552     }
 553   }
 554   FREE(sorted);
 555   sorted = NULL;
 556   retValue = fprintf(fp, " )\n");
 557   if (retValue == EOF) {
 558     return(0);
 559   }
 560
 561   /* Write the .output line. */
 562   retValue = fprintf(fp,"(COMMENT - output names: ");
 563   if (retValue == EOF) {
 564     return(0);
 565   }
 566   for (i = 0; i < n; i++) {
 567     if (outputNames == NULL) {
 568       retValue = fprintf (fp," outNode%d", i);
 569     } else {
 570       retValue = fprintf (fp," %s", outputNames[i]);
 571     }
 572     Dddmp_CheckAndGotoLabel (retValue==EOF,
 573       "Error during file store.", failure);
 574   }
 575   retValue = fprintf(fp, " )\n");
 576   Dddmp_CheckAndGotoLabel (retValue==EOF,
 577     "Error during file store.", failure);
 578
 579   retValue = DddmpCuddDdArrayStorePrefixBody (ddMgr, n, f, inputNames,
 580     outputNames, fp);
 581   Dddmp_CheckAndGotoLabel (retValue==0,
 582     "Error in function DddmpCuddDdArrayStorePrefixBody.", failure);
 583
 584   return(1);
 585
 586 failure:
 587     if (sorted != NULL) {
 588       FREE(sorted);
 589     }
 590     if (support != NULL) {
 591       Cudd_RecursiveDeref(ddMgr,support);
 592     }
 593     return(0);
 594 }
 595
 596 /**Function********************************************************************
 597
 598   Synopsis     [Internal function to writes a dump file representing the
 599     argument BDD in a prefix notation. Writes the body of the file.]
 600
 601   Description  [One multiplexer is written for each BDD node.
 602     It returns 1 in case of success; 0 otherwise (e.g., out-of-memory, file
 603     system full, or an ADD with constants different from 0 and 1).
 604     It does not close the file: This is the caller responsibility.
 605     It uses a minimal unique subset of the hexadecimal address of a node as
 606     name for it.
 607     If the argument inputNames is non-null, it is assumed to hold the
 608     pointers to the names of the inputs. Similarly for outputNames.
 609     For each BDD node of function f, variable v, then child T, and else
 610     child E it stores:
 611     f = v * T + v' * E
 612     that is
 613     (OR f (AND v T) (AND (NOT v) E))
 614     If E is a complemented child this results in the following
 615     (OR f (AND v T) (AND (NOT v) (NOT E)))
 616     ]
 617
 618   SideEffects [None]
 619
 620   SeeAlso     [DddmpCuddDdArrayStoreBlif]
 621
 622 ******************************************************************************/
 623
 624 static int
 625 DddmpCuddDdArrayStorePrefixBody (
 626   DdManager *ddMgr      /* IN: Manager */,
 627   int n                 /* IN: Number of output nodes to be dumped */,
 628   DdNode **f            /* IN: Array of output nodes to be dumped */,
 629   char **inputNames     /* IN: Array of input names (or NULL) */,
 630   char **outputNames    /* IN: Array of output names (or NULL) */,
 631   FILE *fp              /* IN: Pointer to the dump file */
 632   )
 633 {
 634   st_table *visited = NULL;
 635   int retValue;
 636   int i;
 637
 638   /* Initialize symbol table for visited nodes. */
 639   visited = st_init_table(st_ptrcmp, st_ptrhash);
 640   Dddmp_CheckAndGotoLabel (visited==NULL,
 641     "Error if function st_init_table.", failure);
 642
 643   /* Call the function that really gets the job done. */
 644   for (i = 0; i < n; i++) {
 645     retValue = DddmpCuddDdArrayStorePrefixStep (ddMgr, Cudd_Regular(f[i]),
 646       fp, visited, inputNames);
 647     Dddmp_CheckAndGotoLabel (retValue==0,
 648       "Error if function DddmpCuddDdArrayStorePrefixStep.", failure);
 649   }
 650
 651   /* To account for the possible complement on the root,
 652    ** we put either a buffer or an inverter at the output of
 653    ** the multiplexer representing the top node.
 654    */
 655   for (i=0; i<n; i++) {
 656     if (outputNames == NULL) {
 657       retValue = fprintf (fp,  "(BUF outNode%d ", i);
 658     } else {
 659       retValue = fprintf (fp,  "(BUF %s ", outputNames[i]);
 660     }
 661     Dddmp_CheckAndGotoLabel (retValue==EOF,
 662       "Error during file store.", failure);
 663
 664     if (Cudd_IsComplement(f[i])) {
 665 #if SIZEOF_VOID_P == 8
 666       retValue = fprintf (fp, "(NOT node%lx))\n",
 667         (unsigned long) f[i] / (unsigned long) sizeof(DdNode));
 668 #else
 669       retValue = fprintf (fp, "(NOT node%x))\n",
 670         (unsigned) f[i] / (unsigned) sizeof(DdNode));
 671 #endif
 672     } else {
 673 #if SIZEOF_VOID_P == 8
 674       retValue = fprintf (fp, "node%lx)\n",
 675         (unsigned long) f[i] / (unsigned long) sizeof(DdNode));
 676 #else
 677       retValue = fprintf (fp, "node%x)\n",
 678         (unsigned) f[i] / (unsigned) sizeof(DdNode));
 679 #endif
 680     }
 681     Dddmp_CheckAndGotoLabel (retValue==EOF,
 682       "Error during file store.", failure);
 683   }
 684
 685   st_free_table (visited);
 686
 687   return(1);
 688
 689 failure:
 690     if (visited != NULL) st_free_table(visited);
 691     return(0);
 692
 693 }
 694
 695 /**Function********************************************************************
 696
 697   Synopsis    [Performs the recursive step of
 698     DddmpCuddDdArrayStorePrefixBody.]
 699
 700   Description [Performs the recursive step of
 701     DddmpCuddDdArrayStorePrefixBody.
 702     Traverses the BDD f and writes a multiplexer-network description to the
 703     file pointed by fp.
 704     For each BDD node of function f, variable v, then child T, and else
 705     child E it stores:
 706     f = v * T + v' * E
 707     that is
 708     (OR f (AND v T) (AND (NOT v) E))
 709     If E is a complemented child this results in the following
 710     (OR f (AND v T) (AND (NOT v) (NOT E)))
 711     f is assumed to be a regular pointer and the function guarantees this
 712     assumption in the recursive calls.
 713     ]
 714
 715   SideEffects [None]
 716
 717   SeeAlso     []
 718
 719 ******************************************************************************/
 720
 721 static int
 722 DddmpCuddDdArrayStorePrefixStep (
 723   DdManager * ddMgr,
 724   DdNode * f,
 725   FILE * fp,
 726   st_table * visited,
 727   char ** names
 728   )
 729 {
 730   DdNode *T, *E;
 731   int retValue;
 732
 733 #ifdef DDDMP_DEBUG
 734   assert(!Cudd_IsComplement(f));
 735 #endif
 736
 737   /* If already visited, nothing to do. */
 738   if (st_is_member(visited, (char *) f) == 1) {
 739     return(1);
 740   }
 741
 742   /* Check for abnormal condition that should never happen. */
 743   if (f == NULL) {
 744     return(0);
 745   }
 746
 747   /* Mark node as visited. */
 748   if (st_insert(visited, (char *) f, NULL) == ST_OUT_OF_MEM) {
 749     return(0);
 750   }
 751
 752   /* Check for special case: If constant node, generate constant 1. */
 753   if (f == DD_ONE (ddMgr)) {
 754 #if SIZEOF_VOID_P == 8
 755     retValue = fprintf (fp,
 756       "(OR node%lx vss vdd)\n",
 757       (unsigned long) f / (unsigned long) sizeof(DdNode));
 758 #else
 759     retValue = fprintf (fp,
 760       "(OR node%x vss vdd)\n",
 761       (unsigned) f / (unsigned) sizeof(DdNode));
 762 #endif
 763     if (retValue == EOF) {
 764        return(0);
 765     } else {
 766        return(1);
 767     }
 768   }
 769
 770   /*
 771    *  Check whether this is an ADD. We deal with 0-1 ADDs, but not
 772    *  with the general case.
 773    */
 774
 775   if (f == DD_ZERO(ddMgr)) {
 776 #if SIZEOF_VOID_P == 8
 777     retValue = fprintf (fp,
 778       "(AND node%lx vss vdd)\n",
 779        (unsigned long) f / (unsigned long) sizeof(DdNode));
 780 #else
 781     retValue = fprintf (fp,
 782       "(AND node%x vss vdd)\n",
 783       (unsigned) f / (unsigned) sizeof(DdNode));
 784 #endif
 785    if (retValue == EOF) {
 786      return(0);
 787    } else {
 788      return(1);
 789    }
 790   }
 791
 792   if (cuddIsConstant(f)) {
 793     return(0);
 794   }
 795
 796   /* Recursive calls. */
 797   T = cuddT(f);
 798   retValue = DddmpCuddDdArrayStorePrefixStep (ddMgr,T,fp,visited,names);
 799   if (retValue != 1) {
 800     return(retValue);
 801   }
 802   E = Cudd_Regular(cuddE(f));
 803   retValue = DddmpCuddDdArrayStorePrefixStep (ddMgr,E,fp,visited,names);
 804   if (retValue != 1) {
 805     return(retValue);
 806   }
 807
 808   /* Write multiplexer taking complement arc into account. */
 809 #if SIZEOF_VOID_P == 8
 810   retValue = fprintf (fp, "(OR node%lx (AND ",
 811     (unsigned long) f / (unsigned long) sizeof(DdNode));
 812 #else
 813   retValue = fprintf (fp, "(OR node%x (AND ",
 814     (unsigned) f / (unsigned) sizeof(DdNode));
 815 #endif
 816   if (retValue == EOF) {
 817     return(0);
 818   }
 819
 820   if (names != NULL) {
 821     retValue = fprintf(fp, "%s ", names[f->index]);
 822   } else {
 823     retValue = fprintf(fp, "inNode%d ", f->index);
 824   }
 825   if (retValue == EOF) {
 826     return(0);
 827   }
 828
 829 #if SIZEOF_VOID_P == 8
 830   retValue = fprintf (fp, "node%lx) (AND (NOT ",
 831     (unsigned long) T / (unsigned long) sizeof(DdNode));
 832 #else
 833   retValue = fprintf (fp, "node%x) (AND (NOT ",
 834     (unsigned) T / (unsigned) sizeof(DdNode));
 835 #endif
 836   if (retValue == EOF) {
 837     return(0);
 838   }
 839
 840   if (names != NULL) {
 841     retValue = fprintf (fp, "%s", names[f->index]);
 842   } else {
 843     retValue = fprintf (fp, "inNode%d", f->index);
 844   }
 845   if (retValue == EOF) {
 846     return(0);
 847   }
 848
 849 #if SIZEOF_VOID_P == 8
 850   if (Cudd_IsComplement(cuddE(f))) {
 851     retValue = fprintf (fp, ") (NOT node%lx)))\n",
 852       (unsigned long) E / (unsigned long) sizeof(DdNode));
 853   } else {
 854     retValue = fprintf (fp, ") node%lx))\n",
 855       (unsigned long) E / (unsigned long) sizeof(DdNode));
 856   }
 857 #else
 858   if (Cudd_IsComplement(cuddE(f))) {
 859     retValue = fprintf (fp, ") (NOT node%x)))\n",
 860       (unsigned) E / (unsigned) sizeof(DdNode));
 861   } else {
 862     retValue = fprintf (fp, ") node%x))\n",
 863       (unsigned) E / (unsigned) sizeof(DdNode));
 864   }
 865 #endif
 866
 867   if (retValue == EOF) {
 868     return(0);
 869   } else {
 870     return(1);
 871   }
 872 }
 873
 874 /**Function********************************************************************
 875
 876   Synopsis    [Writes a blif file representing the argument BDDs.]
 877
 878   Description [Writes a blif file representing the argument BDDs as a
 879     network of multiplexers. One multiplexer is written for each BDD
 880     node. It returns 1 in case of success; 0 otherwise (e.g.,
 881     out-of-memory, file system full, or an ADD with constants different
 882     from 0 and 1).
 883     DddmpCuddDdArrayStoreBlif does not close the file: This is the
 884     caller responsibility.
 885     DddmpCuddDdArrayStoreBlif uses a minimal unique subset of
 886     the hexadecimal address of a node as name for it.  If the argument
 887     inames is non-null, it is assumed to hold the pointers to the names
 888     of the inputs. Similarly for outputNames.
 889     It prefixes the string "NODE" to each nome to have "regular" names
 890     for each elements.
 891     ]
 892
 893   SideEffects [None]
 894
 895   SeeAlso     [DddmpCuddDdArrayStoreBlifBody,Cudd_DumpBlif]
 896
 897 ******************************************************************************/
 898
 899 static int
 900 DddmpCuddDdArrayStoreBlif (
 901   DdManager *ddMgr    /* IN: Manager */,
 902   int n               /* IN: Number of output nodes to be dumped */,
 903   DdNode **f          /* IN: Array of output nodes to be dumped */,
 904   char **inputNames   /* IN: Array of input names (or NULL) */,
 905   char **outputNames  /* IN: Array of output names (or NULL) */,
 906   char *modelName     /* IN: Model name (or NULL) */,
 907   FILE *fp            /* IN: Pointer to the dump file */
 908   )
 909 {
 910   DdNode *support = NULL;
 911   DdNode *scan;
 912   int *sorted = NULL;
 913   int nVars = ddMgr->size;
 914   int retValue;
 915   int i;
 916
 917   /* Build a bit array with the support of f. */
 918   sorted = ALLOC (int, nVars);
 919   if (sorted == NULL) {
 920     ddMgr->errorCode = CUDD_MEMORY_OUT;
 921     Dddmp_CheckAndGotoLabel (1, "Allocation Error.", failure);
 922   }
 923   for (i = 0; i < nVars; i++) {
 924     sorted[i] = 0;
 925   }
 926
 927   /* Take the union of the supports of each output function. */
 928   support = Cudd_VectorSupport(ddMgr,f,n);
 929   Dddmp_CheckAndGotoLabel (support==NULL,
 930     "Error in function Cudd_VectorSupport.", failure);
 931   cuddRef(support);
 932   scan = support;
 933   while (!cuddIsConstant(scan)) {
 934     sorted[scan->index] = 1;
 935     scan = cuddT(scan);
 936   }
 937   Cudd_RecursiveDeref(ddMgr,support);
 938   support = NULL;
 939   /* so that we do not try to free it in case of failure */
 940
 941   /* Write the header (.model .inputs .outputs). */
 942   if (modelName == NULL) {
 943     retValue = fprintf(fp,".model DD\n.inputs");
 944   } else {
 945     retValue = fprintf(fp,".model %s\n.inputs", modelName);
 946   }
 947   if (retValue == EOF) {
 948     return(0);
 949   }
 950
 951   /* Write the input list by scanning the support array. */
 952   for (i = 0; i < nVars; i++) {
 953     if (sorted[i]) {
 954       if (inputNames == NULL || (inputNames[i] == NULL)) {
 955         retValue = fprintf(fp," inNode%d", i);
 956       } else {
 957         retValue = fprintf(fp," %s", inputNames[i]);
 958       }
 959       Dddmp_CheckAndGotoLabel (retValue==EOF,
 960         "Error during file store.", failure);
 961     }
 962   }
 963   FREE(sorted);
 964   sorted = NULL;
 965
 966   /* Write the .output line. */
 967   retValue = fprintf(fp,"\n.outputs");
 968   Dddmp_CheckAndGotoLabel (retValue==EOF,
 969     "Error during file store.", failure);
 970   for (i = 0; i < n; i++) {
 971     if (outputNames == NULL || (outputNames[i] == NULL)) {
 972       retValue = fprintf(fp," outNode%d", i);
 973     } else {
 974       retValue = fprintf(fp," %s", outputNames[i]);
 975     }
 976     Dddmp_CheckAndGotoLabel (retValue==EOF,
 977       "Error during file store.", failure);
 978   }
 979   retValue = fprintf(fp,"\n");
 980   Dddmp_CheckAndGotoLabel (retValue==EOF,
 981     "Error during file store.", failure);
 982
 983   retValue = DddmpCuddDdArrayStoreBlifBody(ddMgr, n, f, inputNames,
 984     outputNames, fp);
 985   Dddmp_CheckAndGotoLabel (retValue==0,
 986     "Error if function DddmpCuddDdArrayStoreBlifBody.", failure);
 987
 988   /* Write trailer and return. */
 989   retValue = fprintf (fp, ".end\n");
 990   Dddmp_CheckAndGotoLabel (retValue==EOF,
 991     "Error during file store.", failure);
 992
 993   return(1);
 994
 995 failure:
 996   if (sorted != NULL) {
 997     FREE(sorted);
 998   }
 999   if (support != NULL) {
1000     Cudd_RecursiveDeref(ddMgr,support);
1001   }
1002
1003   return(0);
1004 }
1005
1006
1007 /**Function********************************************************************
1008
1009   Synopsis    [Writes a blif body representing the argument BDDs.]
1010
1011   Description [Writes a blif body representing the argument BDDs as a
1012     network of multiplexers. One multiplexer is written for each BDD
1013     node. It returns 1 in case of success; 0 otherwise (e.g.,
1014     out-of-memory, file system full, or an ADD with constants different
1015     from 0 and 1).
1016     DddmpCuddDdArrayStoreBlif does not close the file: This is the
1017     caller responsibility.
1018     DddmpCuddDdArrayStoreBlif uses a minimal unique subset of
1019     the hexadecimal address of a node as name for it.  If the argument
1020     inputNames is non-null, it is assumed to hold the pointers to the names
1021     of the inputs. Similarly for outputNames. This function prints out only
1022     .names part.
1023   ]
1024
1025   SideEffects [None]
1026
1027   SeeAlso     []
1028
1029 ******************************************************************************/
1030
1031 static int
1032 DddmpCuddDdArrayStoreBlifBody (
1033   DdManager *ddMgr      /* IN: Manager */,
1034   int n                 /* IN: Number of output nodes to be dumped */,
1035   DdNode **f            /* IN: Array of output nodes to be dumped */,
1036   char **inputNames     /* IN: Array of input names (or NULL) */,
1037   char **outputNames    /* IN: Array of output names (or NULL) */,
1038   FILE *fp              /* IN: Pointer to the dump file */
1039   )
1040 {
1041   st_table *visited = NULL;
1042   int retValue;
1043   int i;
1044
1045   /* Initialize symbol table for visited nodes. */
1046   visited = st_init_table(st_ptrcmp, st_ptrhash);
1047   Dddmp_CheckAndGotoLabel (visited==NULL,
1048     "Error if function st_init_table.", failure);
1049
1050   /* Call the function that really gets the job done. */
1051   for (i = 0; i < n; i++) {
1052     retValue = DddmpCuddDdArrayStoreBlifStep (ddMgr, Cudd_Regular(f[i]),
1053       fp, visited, inputNames);
1054     Dddmp_CheckAndGotoLabel (retValue==0,
1055       "Error if function DddmpCuddDdArrayStoreBlifStep.", failure);
1056   }
1057
1058   /*
1059    *  To account for the possible complement on the root,
1060    *  we put either a buffer or an inverter at the output of
1061    *  the multiplexer representing the top node.
1062    */
1063
1064   for (i = 0; i < n; i++) {
1065     if (outputNames == NULL) {
1066       retValue = fprintf(fp,
1067 #if SIZEOF_VOID_P == 8
1068         ".names node%lx outNode%d\n",
1069         (unsigned long) f[i] / (unsigned long) sizeof(DdNode), i);
1070 #else
1071         ".names node%x outNode%d\n",
1072         (unsigned) f[i] / (unsigned) sizeof(DdNode), i);
1073 #endif
1074     } else {
1075       retValue = fprintf(fp,
1076 #if SIZEOF_VOID_P == 8
1077         ".names node%lx %s\n",
1078         (unsigned long) f[i] / (unsigned long) sizeof(DdNode), outputNames[i]);
1079 #else
1080         ".names node%x %s\n",
1081         (unsigned) f[i] / (unsigned) sizeof(DdNode), outputNames[i]);
1082 #endif
1083     }
1084     Dddmp_CheckAndGotoLabel (retValue==EOF,
1085       "Error during file store.", failure);
1086     if (Cudd_IsComplement(f[i])) {
1087       retValue = fprintf(fp,"0 1\n");
1088     } else {
1089       retValue = fprintf(fp,"1 1\n");
1090     }
1091     Dddmp_CheckAndGotoLabel (retValue==EOF,
1092       "Error during file store.", failure);
1093   }
1094
1095   st_free_table(visited);
1096   return(1);
1097
1098 failure:
1099   if (visited != NULL) {
1100     st_free_table(visited);
1101   }
1102   return(0);
1103 }
1104
1105 /**Function********************************************************************
1106
1107   Synopsis    [Performs the recursive step of DddmpCuddDdArrayStoreBlif.]
1108
1109   Description [Performs the recursive step of DddmpCuddDdArrayStoreBlif.
1110     Traverses the BDD f and writes a multiplexer-network description to
1111     the file pointed by fp in blif format.
1112     f is assumed to be a regular pointer and DddmpCuddDdArrayStoreBlifStep
1113     guarantees this assumption in the recursive calls.
1114     ]
1115
1116   SideEffects [None]
1117
1118   SeeAlso     []
1119
1120 ******************************************************************************/
1121
1122 static int
1123 DddmpCuddDdArrayStoreBlifStep (
1124   DdManager *ddMgr,
1125   DdNode *f,
1126   FILE *fp,
1127   st_table *visited,
1128   char **names
1129   )
1130 {
1131   DdNode *T, *E;
1132   int retValue;
1133
1134 #ifdef DDDMP_DEBUG
1135   assert(!Cudd_IsComplement(f));
1136 #endif
1137
1138   /* If already visited, nothing to do. */
1139   if (st_is_member(visited, (char *) f) == 1) {
1140     return(1);
1141   }
1142
1143   /* Check for abnormal condition that should never happen. */
1144   if (f == NULL) {
1145     return(0);
1146   }
1147
1148   /* Mark node as visited. */
1149   if (st_insert(visited, (char *) f, NULL) == ST_OUT_OF_MEM) {
1150     return(0);
1151   }
1152
1153   /* Check for special case: If constant node, generate constant 1. */
1154   if (f == DD_ONE(ddMgr)) {
1155 #if SIZEOF_VOID_P == 8
1156     retValue = fprintf(fp, ".names node%lx\n1\n",
1157       (unsigned long) f / (unsigned long) sizeof(DdNode));
1158 #else
1159     retValue = fprintf(fp, ".names node%x\n1\n",
1160       (unsigned) f / (unsigned) sizeof(DdNode));
1161 #endif
1162      if (retValue == EOF) {
1163        return(0);
1164      } else {
1165        return(1);
1166     }
1167   }
1168
1169   /* Check whether this is an ADD. We deal with 0-1 ADDs, but not
1170   ** with the general case.
1171   */
1172   if (f == DD_ZERO(ddMgr)) {
1173 #if SIZEOF_VOID_P == 8
1174     retValue = fprintf(fp, ".names node%lx\n",
1175       (unsigned long) f / (unsigned long) sizeof(DdNode));
1176 #else
1177     retValue = fprintf(fp, ".names node%x\n",
1178       (unsigned) f / (unsigned) sizeof(DdNode));
1179 #endif
1180     if (retValue == EOF) {
1181       return(0);
1182     } else {
1183       return(1);
1184     }
1185   }
1186   if (cuddIsConstant(f)) {
1187     return(0);
1188   }
1189
1190   /* Recursive calls. */
1191   T = cuddT(f);
1192   retValue = DddmpCuddDdArrayStoreBlifStep(ddMgr,T,fp,visited,names);
1193   if (retValue != 1) return(retValue);
1194   E = Cudd_Regular(cuddE(f));
1195   retValue = DddmpCuddDdArrayStoreBlifStep(ddMgr,E,fp,visited,names);
1196   if (retValue != 1) return(retValue);
1197
1198   /* Write multiplexer taking complement arc into account. */
1199   if (names != NULL) {
1200     retValue = fprintf(fp,".names %s", names[f->index]);
1201   } else {
1202     retValue = fprintf(fp,".names inNode%d", f->index);
1203   }
1204   if (retValue == EOF) {
1205     return(0);
1206   }
1207
1208 #if SIZEOF_VOID_P == 8
1209   if (Cudd_IsComplement(cuddE(f))) {
1210     retValue = fprintf(fp," node%lx node%lx node%lx\n11- 1\n0-0 1\n",
1211       (unsigned long) T / (unsigned long) sizeof(DdNode),
1212       (unsigned long) E / (unsigned long) sizeof(DdNode),
1213       (unsigned long) f / (unsigned long) sizeof(DdNode));
1214   } else {
1215     retValue = fprintf(fp," node%lx node%lx node%lx\n11- 1\n0-1 1\n",
1216       (unsigned long) T / (unsigned long) sizeof(DdNode),
1217       (unsigned long) E / (unsigned long) sizeof(DdNode),
1218       (unsigned long) f / (unsigned long) sizeof(DdNode));
1219   }
1220 #else
1221   if (Cudd_IsComplement(cuddE(f))) {
1222     retValue = fprintf(fp," node%x node%x node%x\n11- 1\n0-0 1\n",
1223       (unsigned) T / (unsigned) sizeof(DdNode),
1224       (unsigned) E / (unsigned) sizeof(DdNode),
1225       (unsigned) f / (unsigned) sizeof(DdNode));
1226   } else {
1227     retValue = fprintf(fp," node%x node%x node%x\n11- 1\n0-1 1\n",
1228       (unsigned) T / (unsigned) sizeof(DdNode),
1229       (unsigned) E / (unsigned) sizeof(DdNode),
1230       (unsigned) f / (unsigned) sizeof(DdNode));
1231   }
1232 #endif
1233   if (retValue == EOF) {
1234     return(0);
1235   } else {
1236     return(1);
1237   }
1238 }
1239
1240 /**Function********************************************************************
1241
1242   Synopsis     [Internal function to writes a dump file representing the
1243     argument BDD in a SMV notation.]
1244
1245   Description  [One multiplexer is written for each BDD node.
1246     It returns 1 in case of success; 0 otherwise (e.g., out-of-memory, file
1247     system full, or an ADD with constants different from 0 and 1).
1248     It does not close the file: This is the caller responsibility.
1249     It uses a minimal unique subset of the hexadecimal address of a node as
1250     name for it.
1251     If the argument inputNames is non-null, it is assumed to hold the
1252     pointers to the names of the inputs. Similarly for outputNames.
1253     For each BDD node of function f, variable v, then child T, and else
1254     child E it stores:
1255     f = v * T + v' * E
1256     that is
1257     (OR f (AND v T) (AND (NOT v) E))
1258     If E is a complemented child this results in the following
1259     (OR f (AND v T) (AND (NOT v) (NOT E)))
1260     Comments (COMMENT) are added at the beginning of the description to
1261     describe inputs and outputs of the design.
1262     A buffer (BUF) is add on the output to cope with complemented functions.
1263     ]
1264
1265   SideEffects [None]
1266
1267   SeeAlso     [DddmpCuddDdArrayStoreBlif]
1268
1269 ******************************************************************************/
1270
1271 static int
1272 DddmpCuddDdArrayStoreSmv (
1273   DdManager *ddMgr    /* IN: Manager */,
1274   int n               /* IN: Number of output nodes to be dumped */,
1275   DdNode **f          /* IN: Array of output nodes to be dumped */,
1276   char **inputNames   /* IN: Array of input names (or NULL) */,
1277   char **outputNames  /* IN: Array of output names (or NULL) */,
1278   char *modelName     /* IN: Model name (or NULL) */,
1279   FILE *fp            /* IN: Pointer to the dump file */
1280   )
1281 {
1282   DdNode *support = NULL;
1283   DdNode *scan;
1284   int *sorted = NULL;
1285   int nVars = ddMgr->size;
1286   int retValue;
1287   int i;
1288
1289   /* Build a bit array with the support of f. */
1290   sorted = ALLOC(int, nVars);
1291   if (sorted == NULL) {
1292     ddMgr->errorCode = CUDD_MEMORY_OUT;
1293     Dddmp_CheckAndGotoLabel (1, "Allocation Error.", failure);
1294   }
1295   for (i = 0; i < nVars; i++) {
1296     sorted[i] = 0;
1297   }
1298
1299   /* Take the union of the supports of each output function. */
1300   support = Cudd_VectorSupport(ddMgr,f,n);
1301   Dddmp_CheckAndGotoLabel (support==NULL,
1302     "Error in function Cudd_VectorSupport.", failure);
1303   cuddRef(support);
1304   scan = support;
1305   while (!cuddIsConstant(scan)) {
1306     sorted[scan->index] = 1;
1307     scan = cuddT(scan);
1308   }
1309   Cudd_RecursiveDeref(ddMgr,support);
1310   /* so that we do not try to free it in case of failure */
1311   support = NULL;
1312
1313   /* Write the header */
1314   if (modelName == NULL) {
1315     retValue = fprintf (fp, "MODULE main -- Unknown\n");
1316   } else {
1317     retValue = fprintf (fp, "MODULE main -- %s\n", modelName);
1318   }
1319   if (retValue == EOF) {
1320     return(0);
1321   }
1322
1323   retValue = fprintf(fp, "IVAR\n");
1324   if (retValue == EOF) {
1325     return(0);
1326   }
1327
1328   /* Write the input list by scanning the support array. */
1329   for (i=0; i<nVars; i++) {
1330     if (sorted[i]) {
1331       if (inputNames == NULL) {
1332         retValue = fprintf (fp, " inNode%d : boolean;\n", i);
1333       } else {
1334         retValue = fprintf (fp, " %s : boolean;\n", inputNames[i]);
1335       }
1336       Dddmp_CheckAndGotoLabel (retValue==EOF,
1337         "Error during file store.", failure);
1338     }
1339   }
1340   FREE(sorted);
1341   sorted = NULL;
1342
1343   retValue = fprintf (fp, "\nDEFINE\n");
1344
1345   retValue = DddmpCuddDdArrayStoreSmvBody (ddMgr, n, f, inputNames,
1346     outputNames, fp);
1347   Dddmp_CheckAndGotoLabel (retValue==0,
1348     "Error in function DddmpCuddDdArrayStoreSmvBody.", failure);
1349
1350   return(1);
1351
1352 failure:
1353     if (sorted != NULL) {
1354       FREE(sorted);
1355     }
1356     if (support != NULL) {
1357       Cudd_RecursiveDeref(ddMgr,support);
1358     }
1359     return(0);
1360 }
1361
1362 /**Function********************************************************************
1363
1364   Synopsis     [Internal function to writes a dump file representing the
1365     argument BDD in a SMV notation. Writes the body of the file.]
1366
1367   Description  [One multiplexer is written for each BDD node.
1368     It returns 1 in case of success; 0 otherwise (e.g., out-of-memory, file
1369     system full, or an ADD with constants different from 0 and 1).
1370     It does not close the file: This is the caller responsibility.
1371     It uses a minimal unique subset of the hexadecimal address of a node as
1372     name for it.
1373     If the argument inputNames is non-null, it is assumed to hold the
1374     pointers to the names of the inputs. Similarly for outputNames.
1375     For each BDD node of function f, variable v, then child T, and else
1376     child E it stores:
1377     f = v * T + v' * E
1378     that is
1379     (OR f (AND v T) (AND (NOT v) E))
1380     If E is a complemented child this results in the following
1381     (OR f (AND v T) (AND (NOT v) (NOT E)))
1382     ]
1383
1384   SideEffects [None]
1385
1386   SeeAlso     [DddmpCuddDdArrayStoreBlif]
1387
1388 ******************************************************************************/
1389
1390 static int
1391 DddmpCuddDdArrayStoreSmvBody (
1392   DdManager *ddMgr      /* IN: Manager */,
1393   int n                 /* IN: Number of output nodes to be dumped */,
1394   DdNode **f            /* IN: Array of output nodes to be dumped */,
1395   char **inputNames     /* IN: Array of input names (or NULL) */,
1396   char **outputNames    /* IN: Array of output names (or NULL) */,
1397   FILE *fp              /* IN: Pointer to the dump file */
1398   )
1399 {
1400   st_table *visited = NULL;
1401   int retValue;
1402   int i;
1403
1404   /* Initialize symbol table for visited nodes. */
1405   visited = st_init_table(st_ptrcmp, st_ptrhash);
1406   Dddmp_CheckAndGotoLabel (visited==NULL,
1407     "Error if function st_init_table.", failure);
1408
1409   /* Call the function that really gets the job done. */
1410   for (i = 0; i < n; i++) {
1411     retValue = DddmpCuddDdArrayStoreSmvStep (ddMgr, Cudd_Regular(f[i]),
1412       fp, visited, inputNames);
1413     Dddmp_CheckAndGotoLabel (retValue==0,
1414       "Error if function DddmpCuddDdArrayStoreSmvStep.", failure);
1415   }
1416
1417   /*
1418    *  To account for the possible complement on the root,
1419    *  we put either a buffer or an inverter at the output of
1420    *  the multiplexer representing the top node.
1421    */
1422
1423   for (i=0; i<n; i++) {
1424     if (outputNames == NULL) {
1425       retValue = fprintf (fp,  "outNode%d := ", i);
1426     } else {
1427       retValue = fprintf (fp,  "%s := ", outputNames[i]);
1428     }
1429     Dddmp_CheckAndGotoLabel (retValue==EOF,
1430       "Error during file store.", failure);
1431
1432     if (Cudd_IsComplement(f[i])) {
1433 #if SIZEOF_VOID_P == 8
1434       retValue = fprintf (fp, "!node%lx\n",
1435         (unsigned long) f[i] / (unsigned long) sizeof(DdNode));
1436 #else
1437       retValue = fprintf (fp, "!node%x\n",
1438         (unsigned) f[i] / (unsigned) sizeof(DdNode));
1439 #endif
1440     } else {
1441 #if SIZEOF_VOID_P == 8
1442       retValue = fprintf (fp, "node%lx\n",
1443         (unsigned long) f[i] / (unsigned long) sizeof(DdNode));
1444 #else
1445       retValue = fprintf (fp, "node%x\n",
1446         (unsigned) f[i] / (unsigned) sizeof(DdNode));
1447 #endif
1448     }
1449     Dddmp_CheckAndGotoLabel (retValue==EOF,
1450       "Error during file store.", failure);
1451   }
1452
1453   st_free_table (visited);
1454
1455   return(1);
1456
1457 failure:
1458     if (visited != NULL) st_free_table(visited);
1459     return(0);
1460
1461 }
1462
1463 /**Function********************************************************************
1464
1465   Synopsis    [Performs the recursive step of
1466     DddmpCuddDdArrayStoreSmvBody.]
1467
1468   Description [Performs the recursive step of
1469     DddmpCuddDdArrayStoreSmvBody.
1470     Traverses the BDD f and writes a multiplexer-network description to the
1471     file pointed by fp.
1472     For each BDD node of function f, variable v, then child T, and else
1473     child E it stores:
1474     f = v * T + v' * E
1475     that is
1476     (OR f (AND v T) (AND (NOT v) E))
1477     If E is a complemented child this results in the following
1478     (OR f (AND v T) (AND (NOT v) (NOT E)))
1479     f is assumed to be a regular pointer and the function guarantees this
1480     assumption in the recursive calls.
1481     ]
1482
1483   SideEffects [None]
1484
1485   SeeAlso     []
1486
1487 ******************************************************************************/
1488
1489 static int
1490 DddmpCuddDdArrayStoreSmvStep (
1491   DdManager * ddMgr,
1492   DdNode * f,
1493   FILE * fp,
1494   st_table * visited,
1495   char ** names
1496   )
1497 {
1498   DdNode *T, *E;
1499   int retValue;
1500
1501 #ifdef DDDMP_DEBUG
1502   assert(!Cudd_IsComplement(f));
1503 #endif
1504
1505   /* If already visited, nothing to do. */
1506   if (st_is_member(visited, (char *) f) == 1) {
1507     return(1);
1508   }
1509
1510   /* Check for abnormal condition that should never happen. */
1511   if (f == NULL) {
1512     return(0);
1513   }
1514
1515   /* Mark node as visited. */
1516   if (st_insert(visited, (char *) f, NULL) == ST_OUT_OF_MEM) {
1517     return(0);
1518   }
1519
1520   /* Check for special case: If constant node, generate constant 1. */
1521   if (f == DD_ONE (ddMgr)) {
1522 #if SIZEOF_VOID_P == 8
1523     retValue = fprintf (fp,
1524       "node%lx := 1;\n",
1525       (unsigned long) f / (unsigned long) sizeof(DdNode));
1526 #else
1527     retValue = fprintf (fp,
1528       "node%x := 1;\n",
1529       (unsigned) f / (unsigned) sizeof(DdNode));
1530 #endif
1531     if (retValue == EOF) {
1532        return(0);
1533     } else {
1534        return(1);
1535     }
1536   }
1537
1538   /*
1539    *  Check whether this is an ADD. We deal with 0-1 ADDs, but not
1540    *  with the general case.
1541    */
1542
1543   if (f == DD_ZERO(ddMgr)) {
1544 #if SIZEOF_VOID_P == 8
1545     retValue = fprintf (fp,
1546       "node%lx := 0;\n",
1547        (unsigned long) f / (unsigned long) sizeof(DdNode));
1548 #else
1549     retValue = fprintf (fp,
1550       "node%x := 0;\n",
1551       (unsigned) f / (unsigned) sizeof(DdNode));
1552 #endif
1553    if (retValue == EOF) {
1554      return(0);
1555    } else {
1556      return(1);
1557    }
1558   }
1559
1560   if (cuddIsConstant(f)) {
1561     return(0);
1562   }
1563
1564   /* Recursive calls. */
1565   T = cuddT(f);
1566   retValue = DddmpCuddDdArrayStoreSmvStep (ddMgr,T,fp,visited,names);
1567   if (retValue != 1) {
1568     return(retValue);
1569   }
1570   E = Cudd_Regular(cuddE(f));
1571   retValue = DddmpCuddDdArrayStoreSmvStep (ddMgr,E,fp,visited,names);
1572   if (retValue != 1) {
1573     return(retValue);
1574   }
1575
1576   /* Write multiplexer taking complement arc into account. */
1577 #if SIZEOF_VOID_P == 8
1578   retValue = fprintf (fp, "node%lx := ",
1579     (unsigned long) f / (unsigned long) sizeof(DdNode));
1580 #else
1581   retValue = fprintf (fp, "node%x := ",
1582     (unsigned) f / (unsigned) sizeof(DdNode));
1583 #endif
1584   if (retValue == EOF) {
1585     return(0);
1586   }
1587
1588   if (names != NULL) {
1589     retValue = fprintf(fp, "%s ", names[f->index]);
1590   } else {
1591     retValue = fprintf(fp, "inNode%d ", f->index);
1592   }
1593   if (retValue == EOF) {
1594     return(0);
1595   }
1596
1597 #if SIZEOF_VOID_P == 8
1598   retValue = fprintf (fp, "& node%lx | ",
1599     (unsigned long) T / (unsigned long) sizeof(DdNode));
1600 #else
1601   retValue = fprintf (fp, "& node%x | ",
1602     (unsigned) T / (unsigned) sizeof(DdNode));
1603 #endif
1604   if (retValue == EOF) {
1605     return(0);
1606   }
1607
1608   if (names != NULL) {
1609     retValue = fprintf (fp, "!%s ", names[f->index]);
1610   } else {
1611     retValue = fprintf (fp, "!inNode%d ", f->index);
1612   }
1613   if (retValue == EOF) {
1614     return(0);
1615   }
1616
1617 #if SIZEOF_VOID_P == 8
1618   if (Cudd_IsComplement(cuddE(f))) {
1619     retValue = fprintf (fp, "& !node%lx\n",
1620       (unsigned long) E / (unsigned long) sizeof(DdNode));
1621   } else {
1622     retValue = fprintf (fp, "& node%lx\n",
1623       (unsigned long) E / (unsigned long) sizeof(DdNode));
1624   }
1625 #else
1626   if (Cudd_IsComplement(cuddE(f))) {
1627     retValue = fprintf (fp, "& !node%x\n",
1628       (unsigned) E / (unsigned) sizeof(DdNode));
1629   } else {
1630     retValue = fprintf (fp, "& node%x\n",
1631       (unsigned) E / (unsigned) sizeof(DdNode));
1632   }
1633 #endif
1634
1635   if (retValue == EOF) {
1636     return(0);
1637   } else {
1638     return(1);
1639   }
1640 }
1641