distr/dddmp/dddmpStoreBdd.c

   1 /**CFile**********************************************************************
   2
   3   FileName     [dddmpStoreBdd.c]
   4
   5   PackageName  [dddmp]
   6
   7   Synopsis     [Functions to write BDDs to file.]
   8
   9   Description  [Functions to write BDDs to file.
  10     BDDs are represended on file either in text or binary format under the
  11     following rules.  A file contains a forest of BDDs (a vector of
  12     Boolean functions).  BDD nodes are numbered with contiguous numbers,
  13     from 1 to NNodes (total number of nodes on a file). 0 is not used to
  14     allow negative node indexes for complemented edges.  A file contains
  15     a header, including information about variables and roots to BDD
  16     functions, followed by the list of nodes.  BDD nodes are listed
  17     according to their numbering, and in the present implementation
  18     numbering follows a post-order strategy, in such a way that a node
  19     is never listed before its Then/Else children.
  20   ]
  21
  22   Author       [Gianpiero Cabodi and Stefano Quer]
  23
  24   Copyright    [
  25     Copyright (c) 2004 by Politecnico di Torino.
  26     All Rights Reserved. This software is for educational purposes only.
  27     Permission is given to academic institutions to use, copy, and modify
  28     this software and its documentation provided that this introductory
  29     message is not removed, that this software and its documentation is
  30     used for the institutions' internal research and educational purposes,
  31     and that no monies are exchanged. No guarantee is expressed or implied
  32     by the distribution of this code.
  33     Send bug-reports and/or questions to:
  34     {gianpiero.cabodi,stefano.quer}@polito.it.
  35     ]
  36
  37 ******************************************************************************/
  38
  39 #include "dddmpInt.h"
  40
  41 /*---------------------------------------------------------------------------*/
  42 /* Stucture declarations                                                     */
  43 /*---------------------------------------------------------------------------*/
  44
  45 /*---------------------------------------------------------------------------*/
  46 /* Type declarations                                                         */
  47 /*---------------------------------------------------------------------------*/
  48
  49 /*---------------------------------------------------------------------------*/
  50 /* Variable declarations                                                     */
  51 /*---------------------------------------------------------------------------*/
  52
  53 /*---------------------------------------------------------------------------*/
  54 /* Macro declarations                                                        */
  55 /*---------------------------------------------------------------------------*/
  56
  57 /**AutomaticStart*************************************************************/
  58
  59 /*---------------------------------------------------------------------------*/
  60 /* Static function prototypes                                                */
  61 /*---------------------------------------------------------------------------*/
  62
  63 static int NodeStoreRecurBdd(DdManager *ddMgr, DdNode *f, int mode, int *supportids, char **varnames, int *outids, FILE *fp);
  64 static int NodeTextStoreBdd(DdManager *ddMgr, DdNode *f, int mode, int *supportids, char **varnames, int *outids, FILE *fp, int idf, int vf, int idT, int idE);
  65 static int NodeBinaryStoreBdd(DdManager *ddMgr, DdNode *f, int mode, int *supportids, char **varnames, int *outids, FILE *fp, int idf, int vf, int idT, int idE, int vT, int vE, DdNode *T, DdNode *E);
  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.]
  76
  77   Description  [Dumps the argument BDD to file. Dumping is done through
  78     Dddmp_cuddBddArrayStore. A dummy array of 1 BDD root is
  79     used for this purpose.
  80     ]
  81
  82   SideEffects  [Nodes are temporarily removed from unique hash. They are
  83     re-linked after the store operation in a modified order.
  84     ]
  85
  86   SeeAlso      [Dddmp_cuddBddLoad Dddmp_cuddBddArrayLoad]
  87
  88 ******************************************************************************/
  89
  90 int
  91 Dddmp_cuddBddStore (
  92   DdManager *ddMgr           /* IN: DD Manager */,
  93   char *ddname               /* IN: DD name (or NULL) */,
  94   DdNode *f                  /* IN: BDD root to be stored */,
  95   char **varnames            /* IN: array of variable names (or NULL) */,
  96   int *auxids                /* IN: array of converted var ids */,
  97   int mode                   /* IN: storing mode selector */,
  98   Dddmp_VarInfoType varinfo  /* IN: extra info for variables in text mode */,
  99   char *fname                /* IN: File name */,
 100   FILE *fp                   /* IN: File pointer to the store file */
 101   )
 102 {
 103   int retValue;
 104   DdNode *tmpArray[1];
 105
 106   tmpArray[0] = f;
 107
 108   retValue = Dddmp_cuddBddArrayStore (ddMgr,ddname,1,tmpArray,NULL,
 109     varnames, auxids, mode, varinfo, fname, fp);
 110
 111   return (retValue);
 112 }
 113
 114 /**Function********************************************************************
 115
 116   Synopsis     [Writes a dump file representing the argument Array of BDDs.]
 117
 118   Description  [Dumps the argument array of BDDs to file. Dumping is either
 119     in text or binary form.  BDDs are stored to the fp (already
 120     open) file if not NULL. Otherwise the file whose name is
 121     fname is opened in write mode. The header has the same format
 122     for both textual and binary dump. Names are allowed for input
 123     variables (vnames) and for represented functions (rnames).
 124     For sake of generality and because of dynamic variable
 125     ordering both variable IDs and permuted IDs are included.
 126     New IDs are also supported (auxids). Variables are identified
 127     with incremental numbers. according with their positiom in
 128     the support set. In text mode, an extra info may be added,
 129     chosen among the following options: name, ID, PermID, or an
 130     auxiliary id. Since conversion from DD pointers to integers
 131     is required, DD nodes are temporarily removed from the unique
 132     hash table. This allows the use of the next field to store
 133     node IDs.
 134    ]
 135
 136   SideEffects  [Nodes are temporarily removed from the unique hash
 137     table. They are re-linked after the store operation in a
 138     modified order.
 139     ]
 140
 141   SeeAlso      [Dddmp_cuddBddStore, Dddmp_cuddBddLoad,
 142     Dddmp_cuddBddArrayLoad
 143     ]
 144
 145 ******************************************************************************/
 146
 147 int
 148 Dddmp_cuddBddArrayStore (
 149   DdManager *ddMgr           /* IN: DD Manager */,
 150   char *ddname               /* IN: dd name (or NULL) */,
 151   int nRoots                 /* IN: number of output BDD roots to be stored */,
 152   DdNode **f                 /* IN: array of BDD roots to be stored */,
 153   char **rootnames           /* IN: array of root names (or NULL) */,
 154   char **varnames            /* IN: array of variable names (or NULL) */,
 155   int *auxids                /* IN: array of converted var IDs */,
 156   int mode                   /* IN: storing mode selector */,
 157   Dddmp_VarInfoType varinfo  /* IN: extra info for variables in text mode */,
 158   char *fname                /* IN: File name */,
 159   FILE *fp                   /* IN: File pointer to the store file */
 160   )
 161 {
 162   int retValue;
 163
 164 #ifdef DDDMP_DEBUG
 165 #ifndef __alpha__
 166   int retValueBis;
 167
 168   retValueBis = Cudd_DebugCheck (ddMgr);
 169   if (retValueBis == 1) {
 170     fprintf (stderr, "Inconsistency Found During BDD Store.\n");
 171     fflush (stderr);
 172   } else {
 173     if (retValueBis == CUDD_OUT_OF_MEM) {
 174       fprintf (stderr, "Out of Memory During BDD Store.\n");
 175       fflush (stderr);
 176     }
 177   }
 178 #endif
 179 #endif
 180
 181   retValue = DddmpCuddBddArrayStore (DDDMP_BDD, ddMgr, ddname, nRoots, f,
 182     rootnames, varnames, auxids, mode, varinfo, fname, fp);
 183
 184 #ifdef DDDMP_DEBUG
 185 #ifndef __alpha__
 186   retValueBis = Cudd_DebugCheck (ddMgr);
 187   if (retValueBis == 1) {
 188     fprintf (stderr, "Inconsistency Found During BDD Store.\n");
 189     fflush (stderr);
 190   } else {
 191     if (retValueBis == CUDD_OUT_OF_MEM) {
 192       fprintf (stderr, "Out of Memory During BDD Store.\n");
 193       fflush (stderr);
 194     }
 195   }
 196 #endif
 197 #endif
 198
 199   return (retValue);
 200 }
 201
 202 /*---------------------------------------------------------------------------*/
 203 /* Definition of internal functions                                          */
 204 /*---------------------------------------------------------------------------*/
 205
 206 /**Function********************************************************************
 207
 208   Synopsis     [Writes a dump file representing the argument Array of
 209     BDDs.
 210     ]
 211
 212   Description  [Dumps the argument array of BDDs to file.
 213     Internal function doing inner steps of store for BDDs.
 214     ]
 215
 216   SideEffects  [Nodes are temporarily removed from the unique hash
 217     table. They are re-linked after the store operation in a
 218     modified order.
 219     ]
 220
 221   SeeAlso      [Dddmp_cuddBddStore, Dddmp_cuddBddLoad,
 222     Dddmp_cuddBddArrayLoad
 223     ]
 224
 225 ******************************************************************************/
 226
 227 int
 228 DddmpCuddBddArrayStore (
 229   Dddmp_DecompType ddType   /* IN: Selects the decomp type BDD */,
 230   DdManager *ddMgr          /* IN: DD Manager */,
 231   char *ddname              /* IN: DD name (or NULL) */,
 232   int nRoots                /* IN: number of output BDD roots to be stored */,
 233   DdNode **f                /* IN: array of DD roots to be stored */,
 234   char **rootnames          /* IN: array of root names (or NULL) */,
 235   char **varnames           /* IN: array of variable names (or NULL) */,
 236   int *auxids               /* IN: array of converted var IDs */,
 237   int mode                  /* IN: storing mode selector */,
 238   Dddmp_VarInfoType varinfo /* IN: extra info for variables in text mode */,
 239   char *fname               /* IN: File name */,
 240   FILE *fp                  /* IN: File pointer to the store file */
 241   )
 242 {
 243   DdNode *support = NULL;
 244   DdNode *scan;
 245   int *ids = NULL;
 246   int *permids = NULL;
 247   int *invpermids = NULL;
 248   int *supportids = NULL;
 249   int *outids = NULL;
 250   char **outvarnames = NULL;
 251   int nVars = ddMgr->size;
 252   int nnodes;
 253   int retValue;
 254   int i, var;
 255   int fileToClose = 0;
 256
 257   /*
 258    *  Check DD Type
 259    */
 260
 261   Dddmp_CheckAndGotoLabel (ddType==DDDMP_ADD,
 262     "Error writing to file: ADD Type.", failure);
 263
 264   /*
 265    *  Check if File needs to be opened in the proper mode.
 266    */
 267
 268   if (fp == NULL) {
 269     fp = fopen (fname, "w");
 270     Dddmp_CheckAndGotoLabel (fp==NULL, "Error opening file.",
 271       failure);
 272     fileToClose = 1;
 273   }
 274
 275   /*
 276    *  Force binary mode if automatic.
 277    */
 278
 279   switch (mode) {
 280     case DDDMP_MODE_TEXT:
 281     case DDDMP_MODE_BINARY:
 282       break;
 283     case DDDMP_MODE_DEFAULT:
 284       mode = DDDMP_MODE_BINARY;
 285       break;
 286     default:
 287       mode = DDDMP_MODE_BINARY;
 288       break;
 289   }
 290
 291   /*
 292    * Alloc vectors for variable IDs, perm IDs and support IDs.
 293    *  +1 to include a slot for terminals.
 294    */
 295
 296   ids = DDDMP_ALLOC (int, nVars);
 297   Dddmp_CheckAndGotoLabel (ids==NULL, "Error allocating memory.", failure);
 298   permids = DDDMP_ALLOC (int, nVars);
 299   Dddmp_CheckAndGotoLabel (permids==NULL, "Error allocating memory.", failure);
 300   invpermids = DDDMP_ALLOC (int, nVars);
 301   Dddmp_CheckAndGotoLabel (invpermids==NULL, "Error allocating memory.",
 302     failure);
 303   supportids = DDDMP_ALLOC (int, nVars+1);
 304   Dddmp_CheckAndGotoLabel (supportids==NULL, "Error allocating memory.",
 305     failure);
 306
 307   for (i=0; i<nVars; i++) {
 308     ids[i] = permids[i] = invpermids[i] = supportids[i] = (-1);
 309   }
 310   /* StQ */
 311   supportids[nVars] = -1;
 312
 313   /*
 314    *  Take the union of the supports of each output function.
 315    *  skip NULL functions.
 316    *  Set permids and invpermids of support variables to the proper values.
 317    */
 318
 319   for (i=0; i<nRoots; i++) {
 320     if (f[i] == NULL) {
 321       continue;
 322     }
 323     support = Cudd_Support (ddMgr, f[i]);
 324     Dddmp_CheckAndGotoLabel (support==NULL, "NULL support returned.",
 325       failure);
 326     cuddRef (support);
 327     scan = support;
 328     while (!cuddIsConstant(scan)) {
 329       ids[scan->index] = scan->index;
 330       permids[scan->index] = ddMgr->perm[scan->index];
 331       invpermids[ddMgr->perm[scan->index]] = scan->index;
 332       scan = cuddT (scan);
 333     }
 334     Cudd_RecursiveDeref (ddMgr, support);
 335   }
 336   /* so that we do not try to free it in case of failure */
 337   support = NULL;
 338
 339   /*
 340    *  Set supportids to incremental (shrinked) values following the ordering.
 341    */
 342
 343   for (i=0, var=0; i<nVars; i++) {
 344     if (invpermids[i] >= 0) {
 345       supportids[invpermids[i]] = var++;
 346     }
 347   }
 348   /* set a dummy id for terminal nodes */
 349   supportids[nVars] = var;
 350
 351   /*
 352    *  Select conversion array for extra var info
 353    */
 354
 355   switch (mode) {
 356     case DDDMP_MODE_TEXT:
 357       switch (varinfo) {
 358         case DDDMP_VARIDS:
 359           outids = ids;
 360           break;
 361         case DDDMP_VARPERMIDS:
 362           outids = permids;
 363           break;
 364         case DDDMP_VARAUXIDS:
 365           outids = auxids;
 366           break;
 367         case DDDMP_VARNAMES:
 368           outvarnames = varnames;
 369           break;
 370         case DDDMP_VARDEFAULT:
 371           break;
 372       }
 373       break;
 374     case DDDMP_MODE_BINARY:
 375       outids = NULL;
 376       break;
 377   }
 378
 379   /*
 380    *  Number dd nodes and count them (numbering is from 1 to nnodes)
 381    */
 382
 383   nnodes = DddmpNumberBddNodes (ddMgr, f, nRoots);
 384
 385   /*
 386    * Start Header
 387    */
 388
 389 #ifdef DDDMP_VERSION
 390   retValue = fprintf (fp, ".ver %s\n", DDDMP_VERSION);
 391   Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 392     failure);
 393 #endif
 394
 395   retValue = fprintf (fp, ".mode %c\n", mode);
 396   Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 397     failure);
 398
 399   if (mode == DDDMP_MODE_TEXT) {
 400     retValue = fprintf (fp, ".varinfo %d\n", varinfo);
 401     Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 402       failure);
 403   }
 404
 405   if (ddname != NULL) {
 406     retValue = fprintf (fp, ".dd %s\n",ddname);
 407     Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 408       failure);
 409   }
 410
 411   retValue = fprintf (fp, ".nnodes %d\n", nnodes);
 412   Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 413     failure);
 414
 415   retValue = fprintf (fp, ".nvars %d\n", nVars);
 416   Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 417     failure);
 418
 419   retValue = fprintf (fp, ".nsuppvars %d\n", var);
 420   Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 421     failure);
 422
 423   /*------------  Write the Var Names by scanning the ids array -------------*/
 424
 425   if (varnames != NULL) {
 426
 427     retValue = fprintf (fp, ".suppvarnames");
 428     Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 429       failure);
 430
 431     for (i=0; i<nVars; i++) {
 432       if (ids[i] >= 0) {
 433         if (varnames[ids[i]] == NULL) {
 434           (void) fprintf (stderr,
 435              "DdStore Warning: null variable name. DUMMY%d generated\n", i);
 436           fflush (stderr);
 437           varnames[ids[i]] = DDDMP_ALLOC (char, 10);
 438           Dddmp_CheckAndGotoLabel (varnames[ids[i]] == NULL,
 439             "Error allocating memory.", failure);
 440           sprintf (varnames[ids[i]], "DUMMY%d", i);
 441         }
 442         retValue = fprintf (fp, " %s", varnames[ids[i]]);
 443         Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 444           failure);
 445       }
 446     }
 447
 448     retValue = fprintf (fp, "\n");
 449     Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 450       failure);
 451   }
 452
 453   /*--------- Write the Var SUPPORT Names by scanning the ids array ---------*/
 454
 455   if (varnames != NULL) {
 456     retValue = fprintf (fp, ".orderedvarnames");
 457     Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 458       failure);
 459
 460     for (i=0; i<nVars; i++) {
 461       if (varnames[ddMgr->invperm[i]] == NULL) {
 462           (void) fprintf (stderr,
 463            "DdStore Warning: null variable name. DUMMY%d generated\n", i);
 464         fflush (stderr);
 465         varnames[ddMgr->invperm[i]] = DDDMP_ALLOC (char, 10);
 466         Dddmp_CheckAndGotoLabel (varnames[ddMgr->invperm[i]] == NULL,
 467           "Error allocating memory.", failure);
 468         sprintf (varnames[ddMgr->invperm[i]], "DUMMY%d", i);
 469       }
 470
 471       retValue = fprintf (fp, " %s", varnames[ddMgr->invperm[i]]);
 472       Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 473         failure);
 474     }
 475
 476     retValue = fprintf (fp, "\n");
 477     Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 478       failure);
 479   }
 480
 481   /*------------ Write the var ids by scanning the ids array ---------------*/
 482
 483   retValue = fprintf (fp, ".ids");
 484   Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 485     failure);
 486
 487   for (i=0; i<nVars; i++) {
 488     if (ids[i] >= 0) {
 489       retValue = fprintf (fp, " %d", i);
 490       Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 491         failure);
 492     }
 493   }
 494   retValue = fprintf (fp, "\n");
 495   Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 496     failure);
 497
 498   /*
 499    *  Write the var permids by scanning the permids array.
 500    */
 501
 502   retValue = fprintf (fp, ".permids");
 503   Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 504     failure);
 505   for (i = 0; i < nVars; i++) {
 506     if (permids[i] >= 0) {
 507       retValue = fprintf (fp, " %d", permids[i]);
 508       Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 509         failure);
 510     }
 511   }
 512
 513   retValue = fprintf (fp, "\n");
 514   Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 515     failure);
 516
 517   if (auxids != NULL) {
 518
 519     /*
 520      * Write the var auxids by scanning the ids array.
 521      */
 522
 523     retValue = fprintf (fp, ".auxids");
 524     Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 525       failure);
 526     for (i = 0; i < nVars; i++) {
 527       if (ids[i] >= 0) {
 528         retValue = fprintf (fp, " %d", auxids[i]);
 529         Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 530           failure);
 531       }
 532     }
 533     retValue = fprintf (fp, "\n");
 534     Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 535       failure);
 536   }
 537
 538   /*
 539    * Write the roots info.
 540    */
 541
 542   retValue = fprintf (fp, ".nroots %d\n", nRoots);
 543   Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 544     failure);
 545
 546   if (rootnames != NULL) {
 547
 548     /*
 549      * Write the root names.
 550      */
 551
 552     retValue = fprintf (fp, ".rootnames");
 553     Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 554       failure);
 555
 556     for (i = 0; i < nRoots; i++) {
 557       if (rootnames[i] == NULL) {
 558         (void) fprintf (stderr,
 559           "DdStore Warning: null variable name. ROOT%d generated\n",i);
 560         fflush (stderr);
 561         rootnames[i] = DDDMP_ALLOC(char,10);
 562         Dddmp_CheckAndGotoLabel (rootnames[i]==NULL,
 563           "Error writing to file.", failure);
 564         sprintf(rootnames[ids[i]], "ROOT%d",i);
 565       }
 566       retValue = fprintf (fp, " %s", rootnames[i]);
 567       Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 568         failure);
 569     }
 570
 571     retValue = fprintf (fp, "\n");
 572     Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 573       failure);
 574   }
 575
 576   retValue = fprintf (fp, ".rootids");
 577   Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 578     failure);
 579
 580   /*
 581    * Write BDD indexes of function roots.
 582    * Use negative integers for complemented edges.
 583    */
 584
 585   for (i = 0; i < nRoots; i++) {
 586     if (f[i] == NULL) {
 587       (void) fprintf (stderr, "DdStore Warning: %d-th root is NULL\n",i);
 588       fflush (stderr);
 589       retValue = fprintf (fp, " 0");
 590     }
 591     if (Cudd_IsComplement(f[i])) {
 592       retValue = fprintf (fp, " -%d",
 593         DddmpReadNodeIndexBdd (Cudd_Regular (f[i])));
 594     } else {
 595       retValue = fprintf (fp, " %d",
 596         DddmpReadNodeIndexBdd (Cudd_Regular (f[i])));
 597     }
 598     Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 599       failure);
 600   }
 601
 602   retValue = fprintf (fp, "\n");
 603   Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 604     failure);
 605
 606   retValue = fprintf (fp, ".nodes\n");
 607   Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 608     failure);
 609
 610   /*
 611    *  END HEADER
 612    */
 613
 614   /*
 615    *  Call the function that really gets the job done.
 616    */
 617
 618   for (i = 0; i < nRoots; i++) {
 619     if (f[i] != NULL) {
 620       retValue = NodeStoreRecurBdd (ddMgr, Cudd_Regular(f[i]),
 621         mode, supportids, outvarnames, outids, fp);
 622       Dddmp_CheckAndGotoLabel (retValue==DDDMP_FAILURE,
 623         "Error writing to file.", failure);
 624     }
 625   }
 626
 627   /*
 628    *  Write trailer and return.
 629    */
 630
 631   retValue = fprintf (fp, ".end\n");
 632   Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 633     failure);
 634
 635   if (fileToClose) {
 636     fclose (fp);
 637   }
 638
 639   DddmpUnnumberBddNodes (ddMgr, f, nRoots);
 640   DDDMP_FREE (ids);
 641   DDDMP_FREE (permids);
 642   DDDMP_FREE (invpermids);
 643   DDDMP_FREE (supportids);
 644
 645   return (DDDMP_SUCCESS);
 646
 647   failure:
 648
 649     if (ids != NULL) {
 650       DDDMP_FREE (ids);
 651     }
 652     if (permids != NULL) {
 653       DDDMP_FREE (permids);
 654     }
 655     if (invpermids != NULL) {
 656       DDDMP_FREE (invpermids);
 657     }
 658     if (supportids != NULL) {
 659       DDDMP_FREE (supportids);
 660     }
 661     if (support != NULL) {
 662       Cudd_RecursiveDeref (ddMgr, support);
 663     }
 664
 665     return (DDDMP_FAILURE);
 666 }
 667
 668 /*---------------------------------------------------------------------------*/
 669 /* Definition of static functions                                            */
 670 /*---------------------------------------------------------------------------*/
 671
 672 /**Function********************************************************************
 673
 674   Synopsis     [Performs the recursive step of Dddmp_bddStore.]
 675
 676   Description  [Stores a node to file in either test or binary mode.<l>
 677     In text mode a node is represented (on a text line basis) as
 678     <UL>
 679     <LI> node-index \[var-extrainfo\] var-index Then-index Else-index
 680     </UL>
 681
 682     where all indexes are integer numbers and var-extrainfo
 683     (optional redundant field) is either an integer or a string
 684     (variable name). Node-index is redundant (due to the node
 685     ordering) but we keep it for readability.<p>
 686
 687     In binary mode nodes are represented as a sequence of bytes,
 688     representing var-index, Then-index, and Else-index in an
 689     optimized way. Only the first byte (code) is mandatory.
 690     Integer indexes are represented in absolute or relative mode,
 691     where relative means offset wrt. a Then/Else node info.
 692     Suppose Var(NodeId), Then(NodeId) and Else(NodeId) represent
 693     infos about a given node.<p>
 694
 695     The generic "NodeId" node is stored as
 696
 697     <UL>
 698     <LI> code-byte
 699     <LI> \[var-info\]
 700     <LI> \[Then-info\]
 701     <LI> \[Else-info\]
 702     </UL>
 703
 704     where code-byte contains bit fields
 705
 706     <UL>
 707     <LI>Unused  : 1 bit
 708     <LI>Variable: 2 bits, one of the following codes
 709     <UL>
 710     <LI>DDDMP_ABSOLUTE_ID   var-info = Var(NodeId) follows
 711     <LI>DDDMP_RELATIVE_ID   Var(NodeId) is represented in relative form as
 712         var-info = Min(Var(Then(NodeId)),Var(Else(NodeId))) -Var(NodeId)
 713     <LI>DDDMP_RELATIVE_1    No var-info follows, because
 714         Var(NodeId) = Min(Var(Then(NodeId)),Var(Else(NodeId)))-1
 715     <LI>DDDMP_TERMINAL      Node is a terminal, no var info required
 716     </UL>
 717     <LI>T       : 2 bits, with codes similar to V
 718     <UL>
 719     <LI>DDDMP_ABSOLUTE_ID   Then-info = Then(NodeId) follows
 720     <LI>DDDMP_RELATIVE_ID   Then(NodeId) is represented in relative form as
 721           Then-info = Nodeid-Then(NodeId)
 722     <LI>DDDMP_RELATIVE_1    No info on Then(NodeId) follows, because
 723           Then(NodeId) = NodeId-1
 724     <LI>DDDMP_TERMINAL Then Node is a terminal, no info required (for BDDs)
 725     </UL>
 726     <LI>Ecompl  : 1 bit, if 1 means complemented edge
 727     <LI>E       : 2 bits, with codes and meanings as for the Then edge
 728     </UL>
 729     var-info, Then-info, Else-info (if required) are represented as unsigned
 730     integer values on a sufficient set of bytes (MSByte first).
 731     ]
 732
 733   SideEffects  [None]
 734
 735   SeeAlso      []
 736
 737 ******************************************************************************/
 738
 739 static int
 740 NodeStoreRecurBdd (
 741   DdManager *ddMgr  /* IN: DD Manager */,
 742   DdNode *f         /* IN: DD node to be stored */,
 743   int mode          /* IN: store mode */,
 744   int *supportids   /* IN: internal ids for variables */,
 745   char **varnames   /* IN: names of variables: to be stored with nodes */,
 746   int *outids       /* IN: output ids for variables */,
 747   FILE *fp          /* IN: store file */
 748   )
 749 {
 750   DdNode *T = NULL;
 751   DdNode *E = NULL;
 752   int idf = (-1);
 753   int idT = (-1);
 754   int idE = (-1);
 755   int vf = (-1);
 756   int vT = (-1);
 757   int vE = (-1);
 758   int retValue;
 759   int nVars;
 760
 761   nVars = ddMgr->size;
 762   T = E = NULL;
 763   idf = idT =  idE = (-1);
 764
 765 #ifdef DDDMP_DEBUG
 766   assert(!Cudd_IsComplement(f));
 767   assert(f!=NULL);
 768   assert(supportids!=NULL);
 769 #endif
 770
 771   /* If already visited, nothing to do. */
 772   if (DddmpVisitedBdd (f)) {
 773     return (DDDMP_SUCCESS);
 774   }
 775
 776   /* Mark node as visited. */
 777   DddmpSetVisitedBdd (f);
 778
 779   if (Cudd_IsConstant(f)) {
 780     /* Check for special case: don't recur */
 781     idf = DddmpReadNodeIndexBdd (f);
 782   } else {
 783
 784 #ifdef DDDMP_DEBUG
 785     /* BDDs! Only one constant supported */
 786     assert (!cuddIsConstant(f));
 787 #endif
 788
 789     /*
 790      *  Recursive call for Then edge
 791      */
 792
 793     T = cuddT(f);
 794 #ifdef DDDMP_DEBUG
 795     /* ROBDDs! No complemented Then edge */
 796     assert (!Cudd_IsComplement(T));
 797 #endif
 798     /* recur */
 799     retValue = NodeStoreRecurBdd (ddMgr, T, mode, supportids, varnames, outids,
 800       fp);
 801     if (retValue != DDDMP_SUCCESS) {
 802       return (retValue);
 803     }
 804
 805     /*
 806      *  Recursive call for Else edge
 807      */
 808
 809     E = Cudd_Regular (cuddE (f));
 810     retValue = NodeStoreRecurBdd (ddMgr, E, mode, supportids, varnames, outids,
 811       fp);
 812     if (retValue != DDDMP_SUCCESS) {
 813       return (retValue);
 814     }
 815
 816     /*
 817      *  Obtain nodeids and variable ids of f, T, E
 818      */
 819
 820     idf = DddmpReadNodeIndexBdd (f);
 821     vf = f->index;
 822
 823     idT = DddmpReadNodeIndexBdd (T);
 824     if (Cudd_IsConstant(T)) {
 825       vT = nVars;
 826     } else {
 827       vT = T->index;
 828     }
 829
 830     idE = DddmpReadNodeIndexBdd (E);
 831     if (Cudd_IsConstant(E)) {
 832       vE = nVars;
 833     } else {
 834       vE = E->index;
 835     }
 836   }
 837
 838   switch (mode) {
 839     case DDDMP_MODE_TEXT:
 840       retValue = NodeTextStoreBdd (ddMgr, f, mode, supportids, varnames,
 841         outids, fp, idf, vf, idT, idE);
 842       break;
 843     case DDDMP_MODE_BINARY:
 844       retValue = NodeBinaryStoreBdd (ddMgr, f, mode, supportids, varnames,
 845         outids, fp, idf, vf, idT, idE, vT, vE, T, E);
 846       break;
 847     default:
 848       return (DDDMP_FAILURE);
 849   }
 850
 851   return (retValue);
 852 }
 853
 854 /**Function********************************************************************
 855
 856   Synopsis     [Store One Single Node in Text Format.]
 857
 858   Description  [Store 1 0 0 for the terminal node.
 859     Store id, left child pointer, right pointer for all the other nodes.
 860     ]
 861
 862   SideEffects  [None]
 863
 864   SeeAlso      [NodeBinaryStoreBdd]
 865
 866 ******************************************************************************/
 867
 868 static int
 869 NodeTextStoreBdd (
 870   DdManager *ddMgr  /* IN: DD Manager */,
 871   DdNode *f         /* IN: DD node to be stored */,
 872   int mode          /* IN: store mode */,
 873   int *supportids   /* IN: internal ids for variables */,
 874   char **varnames   /* IN: names of variables: to be stored with nodes */,
 875   int *outids       /* IN: output ids for variables */,
 876   FILE *fp          /* IN: Store file */,
 877   int idf           /* IN: index of the current node */,
 878   int vf            /* IN: variable of the current node */,
 879   int idT           /* IN: index of the Then node */,
 880   int idE           /* IN: index of the Else node */
 881   )
 882 {
 883   int retValue = EOF;
 884
 885   /*
 886    *  Check for Constant
 887    */
 888
 889   if (Cudd_IsConstant(f)) {
 890
 891     if (f == Cudd_ReadOne(ddMgr)) {
 892       if ((varnames != NULL) || (outids != NULL)) {
 893         retValue = fprintf (fp, "%d T 1 0 0\n", idf);
 894       } else {
 895         retValue = fprintf (fp, "%d 1 0 0\n", idf);
 896       }
 897
 898       if (retValue == EOF) {
 899         return (DDDMP_FAILURE);
 900       } else {
 901         return (DDDMP_SUCCESS);
 902       }
 903     }
 904
 905     if (f == Cudd_ReadZero(ddMgr)) {
 906       if ((varnames != NULL) || (outids != NULL)) {
 907         retValue = fprintf (fp, "%d T 0 0 0\n", idf);
 908       } else {
 909         retValue = fprintf (fp, "%d 0 0 0\n", idf);
 910       }
 911
 912       if (retValue == EOF) {
 913         return (DDDMP_FAILURE);
 914       } else {
 915         return (DDDMP_SUCCESS);
 916       }
 917     }
 918
 919     /*
 920      *  A constant node different from 1: an ADD constant
 921      */
 922
 923     Dddmp_CheckAndReturn (((varnames!=NULL)||(outids!=NULL)),
 924       "Error writing to file: ADD Type.");
 925
 926     if (retValue == EOF) {
 927       return (DDDMP_FAILURE);
 928     } else {
 929       return (DDDMP_SUCCESS);
 930     }
 931   }
 932
 933   /*
 934    *  ... Not A Constant
 935    */
 936
 937   if (Cudd_IsComplement (cuddE(f))) {
 938     idE = -idE;
 939   }
 940
 941   if (varnames != NULL) {
 942     retValue = fprintf (fp, "%d %s %d %d %d\n",
 943        idf, varnames[vf], supportids[vf], idT, idE);
 944
 945     if (retValue == EOF) {
 946       return (DDDMP_FAILURE);
 947     } else {
 948       return (DDDMP_SUCCESS);
 949     }
 950   }
 951
 952   if (outids != NULL) {
 953     retValue = fprintf (fp, "%d %d %d %d %d\n",
 954        idf, outids[vf], supportids[vf], idT, idE);
 955
 956     if (retValue == EOF) {
 957       return (DDDMP_FAILURE);
 958     } else {
 959       return (DDDMP_SUCCESS);
 960     }
 961     }
 962
 963   retValue = fprintf (fp, "%d %d %d %d\n",
 964     idf, supportids[vf], idT, idE);
 965
 966   if (retValue == EOF) {
 967     return (DDDMP_FAILURE);
 968   } else {
 969     return (DDDMP_SUCCESS);
 970   }
 971 }
 972
 973 /**Function********************************************************************
 974
 975   Synopsis     [Store One Single Node in Binary Format.]
 976
 977   Description  [Store 1 0 0 for the terminal node.
 978     Store id, left child pointer, right pointer for all the other nodes.
 979     Store every information as coded binary values.]
 980
 981   SideEffects  [None]
 982
 983   SeeAlso      [NodeTextStoreBdd]
 984
 985 ******************************************************************************/
 986
 987 static int
 988 NodeBinaryStoreBdd (
 989   DdManager *ddMgr  /* IN: DD Manager */,
 990   DdNode *f         /* IN: DD node to be stored */,
 991   int mode          /* IN: store mode */,
 992   int *supportids   /* IN: internal ids for variables */,
 993   char **varnames   /* IN: names of variables: to be stored with nodes */,
 994   int *outids       /* IN: output ids for variables */,
 995   FILE *fp          /* IN: store file */,
 996   int idf           /* IN: index of the node */,
 997   int vf            /* IN: variable of the node */,
 998   int idT           /* IN: index of the Then node */,
 999   int idE           /* IN: index of the Else node */,
1000   int vT            /* IN: variable of the Then node */,
1001   int vE            /* IN: variable of the Else node */,
1002   DdNode *T         /* IN: Then node */,
1003   DdNode *E         /* IN: Else node */
1004   )
1005 {
1006   int retValue, diff, var;
1007   struct binary_dd_code code;
1008
1009   /*
1010    *  Check for Constant
1011    */
1012
1013   /* only integer ids used, varnames ignored */
1014   /* Terminal one is coded as DDDMP_TERMINAL, all other fields are 0 */
1015   if (Cudd_IsConstant(f)) {
1016     code.Unused = 0;
1017     code.V = DDDMP_TERMINAL;
1018     code.T = 0;
1019     code.E = 0;
1020     code.Ecompl = 0;
1021     retValue = DddmpWriteCode (fp,code);
1022     if (retValue == EOF) {
1023       return (DDDMP_FAILURE);
1024     } else {
1025       return (DDDMP_SUCCESS);
1026     }
1027   }
1028
1029   /*
1030    * Non terminal: output variable id
1031    */
1032
1033   var = supportids[vf];
1034   diff = (supportids[vT]<supportids[vE]) ?
1035     (supportids[vT]-var) : (supportids[vE]-var);
1036   code.V = DDDMP_ABSOLUTE_ID;
1037
1038   if (diff <= var) {
1039     if (diff == 1) {
1040       code.V = DDDMP_RELATIVE_1;
1041     } else {
1042       code.V = DDDMP_RELATIVE_ID;
1043       var = diff;
1044     }
1045   }
1046
1047   if (T == DD_ONE(ddMgr)) {
1048     code.T = DDDMP_TERMINAL;
1049   } else {
1050     /* compute displacement */
1051     diff = idf - idT;
1052     code.T = DDDMP_ABSOLUTE_ID;
1053     if (diff <= idT) {
1054       if (diff == 1) {
1055          code.T = DDDMP_RELATIVE_1;
1056       } else {
1057          code.T = DDDMP_RELATIVE_ID;
1058          idT = diff;
1059       }
1060     }
1061   }
1062
1063   if (E == DD_ONE(ddMgr)) {
1064     code.E = DDDMP_TERMINAL;
1065   } else {
1066     /* compute displacement */
1067     diff = idf - idE;
1068     code.E = DDDMP_ABSOLUTE_ID;
1069     if (diff <= idE) {
1070       if (diff == 1) {
1071         code.E = DDDMP_RELATIVE_1;
1072       } else {
1073         code.E = DDDMP_RELATIVE_ID;
1074         idE = diff;
1075       }
1076     }
1077   }
1078
1079   if (Cudd_IsComplement(cuddE(f))) {
1080     code.Ecompl = 1;
1081   } else {
1082     code.Ecompl = 0;
1083   }
1084
1085   retValue = DddmpWriteCode (fp,code);
1086
1087   if (retValue == EOF) {
1088     return (DDDMP_FAILURE);
1089   }
1090
1091   if ((code.V == DDDMP_ABSOLUTE_ID) || (code.V == DDDMP_RELATIVE_ID)) {
1092     retValue = DddmpWriteInt (fp, var);
1093     if (retValue == EOF) {
1094       return (DDDMP_FAILURE);
1095     }
1096   }
1097
1098   if ((code.T == DDDMP_ABSOLUTE_ID) || (code.T == DDDMP_RELATIVE_ID)) {
1099     retValue = DddmpWriteInt(fp,idT);
1100     if (retValue == EOF) {
1101       return (DDDMP_FAILURE);
1102     }
1103   }
1104
1105   if ((code.E == DDDMP_ABSOLUTE_ID) || (code.E == DDDMP_RELATIVE_ID)) {
1106     retValue = DddmpWriteInt(fp,idE);
1107     if (retValue == EOF) {
1108       return (DDDMP_FAILURE);
1109     }
1110   }
1111
1112   return (retValue);
1113 }
1114