distr/dddmp/dddmpLoad.c

   1 /**CFile**********************************************************************
   2
   3   FileName     [dddmpLoad.c]
   4
   5   PackageName  [dddmp]
   6
   7   Synopsis     [Functions to read in bdds to file]
   8
   9   Description  [Functions to read in bdds to file.  BDDs
  10     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 #define matchkeywd(str,key) (strncmp(str,key,strlen(key))==0)
  58
  59 /**AutomaticStart*************************************************************/
  60
  61 /*---------------------------------------------------------------------------*/
  62 /* Static function prototypes                                                */
  63 /*---------------------------------------------------------------------------*/
  64
  65 static int DddmpCuddDdArrayLoad(Dddmp_DecompType ddType, DdManager *ddMgr, Dddmp_RootMatchType rootMatchMode, char **rootmatchnames, Dddmp_VarMatchType varMatchMode, char **varmatchnames, int *varmatchauxids, int *varcomposeids, int mode, char *file, FILE *fp, DdNode ***pproots);
  66 static Dddmp_Hdr_t * DddmpBddReadHeader(char *file, FILE *fp);
  67 static void DddmpFreeHeader(Dddmp_Hdr_t *Hdr);
  68
  69 /**AutomaticEnd***************************************************************/
  70
  71 /*---------------------------------------------------------------------------*/
  72 /* Definition of exported functions                                          */
  73 /*---------------------------------------------------------------------------*/
  74
  75 /**Function********************************************************************
  76
  77   Synopsis     [Reads a dump file representing the argument BDD.]
  78
  79   Description  [Reads a dump file representing the argument BDD.
  80     Dddmp_cuddBddArrayLoad is used through a dummy array (see this
  81     function's description for more details).
  82     Mode, the requested input file format, is checked against
  83     the file format.
  84     The loaded BDDs is referenced before returning it.
  85     ]
  86
  87   SideEffects  [A vector of pointers to DD nodes is allocated and freed.]
  88
  89   SeeAlso      [Dddmp_cuddBddStore, Dddmp_cuddBddArrayLoad]
  90
  91 ******************************************************************************/
  92
  93 DdNode *
  94 Dddmp_cuddBddLoad (
  95   DdManager *ddMgr                /* IN: DD Manager */,
  96   Dddmp_VarMatchType varMatchMode /* IN: storing mode selector */,
  97   char **varmatchnames            /* IN: array of variable names - by IDs */,
  98   int *varmatchauxids             /* IN: array of variable auxids - by IDs */,
  99   int *varcomposeids              /* IN: array of new ids accessed - by IDs */,
 100   int mode                        /* IN: requested input file format */,
 101   char *file                      /* IN: file name */,
 102   FILE *fp                        /* IN: file pointer */
 103   )
 104 {
 105   DdNode *f , **tmpArray;
 106   int i, nRoots;
 107
 108   nRoots = Dddmp_cuddBddArrayLoad(ddMgr,DDDMP_ROOT_MATCHLIST,NULL,
 109     varMatchMode,varmatchnames,varmatchauxids,varcomposeids,
 110     mode,file,fp,&tmpArray);
 111
 112   if (nRoots == 0) {
 113     return (NULL);
 114   } else {
 115     f = tmpArray[0];
 116     if (nRoots > 1) {
 117       fprintf (stderr,
 118         "Warning: %d BDD roots found in file. Only first retrieved.\n",
 119          nRoots);
 120       for (i=1; i<nRoots; i++) {
 121         Cudd_RecursiveDeref (ddMgr, tmpArray[i]);
 122       }
 123     }
 124     DDDMP_FREE (tmpArray);
 125     return (f);
 126   }
 127 }
 128
 129 /**Function********************************************************************
 130
 131   Synopsis    [Reads a dump file representing the argument BDDs.]
 132
 133   Description [Reads a dump file representing the argument BDDs. The header is
 134     common to both text and binary mode. The node list is either
 135     in text or binary format. A dynamic vector of DD pointers
 136     is allocated to support conversion from DD indexes to pointers.
 137     Several criteria are supported for variable match between file
 138     and dd manager. Several changes/permutations/compositions are allowed
 139     for variables while loading DDs. Variable of the dd manager are allowed
 140     to match with variables on file on ids, permids, varnames,
 141     varauxids; also direct composition between ids and
 142     composeids is supported. More in detail:
 143     <ol>
 144     <li> varMatchMode=DDDMP_VAR_MATCHIDS <p>
 145     allows the loading of a DD keeping variable IDs unchanged
 146     (regardless of the variable ordering of the reading manager); this
 147     is useful, for example, when swapping DDs to file and restoring them
 148     later from file, after possible variable reordering activations.
 149
 150     <li> varMatchMode=DDDMP_VAR_MATCHPERMIDS <p>
 151     is used to allow variable match according to the position in the
 152     ordering.
 153
 154     <li> varMatchMode=DDDMP_VAR_MATCHNAMES <p>
 155     requires a non NULL varmatchnames parameter; this is a vector of
 156     strings in one-to-one correspondence with variable IDs of the
 157     reading manager. Variables in the DD file read are matched with
 158     manager variables according to their name (a non NULL varnames
 159     parameter was required while storing the DD file).
 160
 161     <li> varMatchMode=DDDMP_VAR_MATCHIDS <p>
 162     has a meaning similar to DDDMP_VAR_MATCHNAMES, but integer auxiliary
 163     IDs are used instead of strings; the additional non NULL
 164     varmatchauxids parameter is needed.
 165
 166     <li> varMatchMode=DDDMP_VAR_COMPOSEIDS <p>
 167     uses the additional varcomposeids parameter is used as array of
 168     variable ids to be composed with ids stored in file.
 169     </ol>
 170
 171     In the present implementation, the array varnames (3), varauxids (4)
 172     and composeids (5) need to have one entry for each variable in the
 173     DD manager (NULL pointers are allowed for unused variables
 174     in varnames). Hence variables need to be already present in the
 175     manager. All arrays are sorted according to IDs.
 176
 177     All the loaded BDDs are referenced before returning them.
 178     ]
 179
 180   SideEffects [A vector of pointers to DD nodes is allocated and freed.]
 181
 182   SeeAlso     [Dddmp_cuddBddArrayStore]
 183
 184 ******************************************************************************/
 185
 186 int
 187 Dddmp_cuddBddArrayLoad (
 188   DdManager *ddMgr                  /* IN: DD Manager */,
 189   Dddmp_RootMatchType rootMatchMode /* IN: storing mode selector */,
 190   char **rootmatchnames             /* IN: sorted names for loaded roots */,
 191   Dddmp_VarMatchType varMatchMode   /* IN: storing mode selector */,
 192   char **varmatchnames              /* IN: array of variable names, by ids */,
 193   int *varmatchauxids               /* IN: array of variable auxids, by ids */,
 194   int *varcomposeids                /* IN: array of new ids, by ids */,
 195   int mode                          /* IN: requested input file format */,
 196   char *file                        /* IN: file name */,
 197   FILE *fp                          /* IN: file pointer */,
 198   DdNode ***pproots                 /* OUT: array of returned BDD roots */
 199   )
 200 {
 201   int retValue;
 202
 203 #ifdef DDDMP_DEBUG
 204 #ifndef __alpha__
 205   int retValueBis;
 206
 207   retValueBis = Cudd_DebugCheck (ddMgr);
 208   if (retValueBis == 1) {
 209     fprintf (stderr, "Inconsistency Found During BDD Load.\n");
 210     fflush (stderr);
 211   } else {
 212     if (retValueBis == CUDD_OUT_OF_MEM) {
 213       fprintf (stderr, "Out of Memory During BDD Load.\n");
 214       fflush (stderr);
 215     }
 216   }
 217 #endif
 218 #endif
 219
 220   retValue = DddmpCuddDdArrayLoad (DDDMP_BDD, ddMgr, rootMatchMode,
 221      rootmatchnames, varMatchMode, varmatchnames, varmatchauxids,
 222      varcomposeids, mode, file, fp, pproots);
 223
 224 #ifdef DDDMP_DEBUG
 225 #ifndef __alpha__
 226   retValueBis = Cudd_DebugCheck (ddMgr);
 227   if (retValueBis == 1) {
 228     fprintf (stderr, "Inconsistency Found During BDD Load.\n");
 229     fflush (stderr);
 230   } else {
 231     if (retValueBis == CUDD_OUT_OF_MEM) {
 232       fprintf (stderr, "Out of Memory During BDD Load.\n");
 233       fflush (stderr);
 234     }
 235   }
 236 #endif
 237 #endif
 238
 239   return (retValue);
 240 }
 241
 242 /**Function********************************************************************
 243
 244   Synopsis    [Reads a dump file representing the argument ADD.]
 245
 246   Description [Reads a dump file representing the argument ADD.
 247     Dddmp_cuddAddArrayLoad is used through a dummy array.
 248     ]
 249
 250   SideEffects [A vector of pointers to DD nodes is allocated and freed.]
 251
 252   SeeAlso     [Dddmp_cuddAddStore, Dddmp_cuddAddArrayLoad]
 253
 254 ******************************************************************************/
 255
 256 DdNode *
 257 Dddmp_cuddAddLoad (
 258   DdManager *ddMgr                /* IN: Manager */,
 259   Dddmp_VarMatchType varMatchMode /* IN: storing mode selector */,
 260   char **varmatchnames            /* IN: array of variable names by IDs */,
 261   int  *varmatchauxids            /* IN: array of variable auxids by IDs */,
 262   int  *varcomposeids             /* IN: array of new ids by IDs */,
 263   int mode                        /* IN: requested input file format */,
 264   char *file                      /* IN: file name */,
 265   FILE *fp                        /* IN: file pointer */
 266   )
 267 {
 268   DdNode *f , **tmpArray;
 269   int i, nRoots;
 270
 271   nRoots = Dddmp_cuddAddArrayLoad (ddMgr, DDDMP_ROOT_MATCHLIST,NULL,
 272     varMatchMode, varmatchnames, varmatchauxids, varcomposeids,
 273     mode, file, fp, &tmpArray);
 274
 275   if (nRoots == 0) {
 276     return (NULL);
 277   } else {
 278     f = tmpArray[0];
 279     if (nRoots > 1) {
 280       fprintf (stderr,
 281         "Warning: %d BDD roots found in file. Only first retrieved.\n",
 282         nRoots);
 283       for (i=1; i<nRoots; i++) {
 284         Cudd_RecursiveDeref (ddMgr, tmpArray[i]);
 285       }
 286     }
 287     DDDMP_FREE (tmpArray);
 288     return (f);
 289   }
 290 }
 291
 292 /**Function********************************************************************
 293
 294   Synopsis    [Reads a dump file representing the argument ADDs.]
 295
 296   Description [Reads a dump file representing the argument ADDs. See
 297     BDD load functions for detailed explanation.
 298     ]
 299
 300   SideEffects [A vector of pointers to DD nodes is allocated and freed.]
 301
 302   SeeAlso     [Dddmp_cuddBddArrayStore]
 303
 304 ******************************************************************************/
 305
 306 int
 307 Dddmp_cuddAddArrayLoad (
 308   DdManager *ddMgr                  /* IN: DD Manager */,
 309   Dddmp_RootMatchType rootMatchMode /* IN: storing mode selector */,
 310   char **rootmatchnames             /* IN: sorted names for loaded roots */,
 311   Dddmp_VarMatchType varMatchMode   /* IN: storing mode selector */,
 312   char **varmatchnames              /* IN: array of variable names, by ids */,
 313   int *varmatchauxids               /* IN: array of variable auxids, by ids */,
 314   int *varcomposeids                /* IN: array of new ids, by ids */,
 315   int mode                          /* IN: requested input file format */,
 316   char *file                        /* IN: file name */,
 317   FILE *fp                          /* IN: file pointer */,
 318   DdNode ***pproots                 /* OUT: array of returned BDD roots */
 319   )
 320 {
 321
 322   int retValue;
 323
 324 #if 0
 325 #ifdef DDDMP_DEBUG
 326 #ifndef __alpha__
 327   int retValueBis;
 328
 329   retValueBis = Cudd_DebugCheck (ddMgr);
 330   if (retValueBis == 1) {
 331     fprintf (stderr, "Inconsistency Found During ADD Load.\n");
 332     fflush (stderr);
 333   } else {
 334     if (retValueBis == CUDD_OUT_OF_MEM) {
 335       fprintf (stderr, "Out of Memory During ADD Load.\n");
 336       fflush (stderr);
 337     }
 338   }
 339 #endif
 340 #endif
 341 #endif
 342
 343   retValue = DddmpCuddDdArrayLoad (DDDMP_ADD, ddMgr, rootMatchMode,
 344     rootmatchnames, varMatchMode, varmatchnames, varmatchauxids,
 345     varcomposeids, mode, file, fp, pproots);
 346
 347 #if 0
 348 #ifdef DDDMP_DEBUG
 349 #ifndef __alpha__
 350   retValueBis = Cudd_DebugCheck (ddMgr);
 351   if (retValueBis == 1) {
 352     fprintf (stderr, "Inconsistency Found During ADD Load.\n");
 353     fflush (stderr);
 354   } else {
 355     if (retValueBis == CUDD_OUT_OF_MEM) {
 356       fprintf (stderr, "Out of Memory During ADD Load.\n");
 357       fflush (stderr);
 358     }
 359   }
 360 #endif
 361 #endif
 362 #endif
 363
 364   return (retValue);
 365 }
 366
 367 /**Function********************************************************************
 368
 369   Synopsis    [Reads the header of a dump file representing the argument BDDs]
 370
 371   Description [Reads the header of a dump file representing the argument BDDs.
 372     Returns main information regarding DD type stored in the file,
 373     the variable ordering used, the number of variables, etc.
 374     It reads only the header of the file NOT the BDD/ADD section.
 375     ]
 376
 377   SideEffects []
 378
 379   SeeAlso     [Dddmp_cuddBddArrayLoad]
 380
 381 ******************************************************************************/
 382
 383 int
 384 Dddmp_cuddHeaderLoad (
 385   Dddmp_DecompType *ddType  /* OUT: selects the proper decomp type */,
 386   int *nVars                /* OUT: number of DD variables */,
 387   int *nsuppvars            /* OUT: number of support variables */,
 388   char ***suppVarNames      /* OUT: array of support variable names */,
 389   char ***orderedVarNames   /* OUT: array of variable names */,
 390   int **varIds              /* OUT: array of variable ids */,
 391   int **varComposeIds       /* OUT: array of permids ids */,
 392   int **varAuxIds           /* OUT: array of variable aux ids */,
 393   int *nRoots               /* OUT: number of root in the file */,
 394   char *file                 /* IN: file name */,
 395   FILE *fp                   /* IN: file pointer */
 396   )
 397 {
 398   Dddmp_Hdr_t *Hdr;
 399   int i, fileToClose;
 400   int *tmpVarIds = NULL;
 401   int *tmpVarComposeIds = NULL;
 402   int *tmpVarAuxIds = NULL;
 403
 404   fileToClose = 0;
 405   if (fp == NULL) {
 406     fp = fopen (file, "r");
 407     Dddmp_CheckAndGotoLabel (fp==NULL, "Error opening file.",
 408       failure);
 409     fileToClose = 1;
 410   }
 411
 412   Hdr = DddmpBddReadHeader (NULL, fp);
 413
 414   Dddmp_CheckAndGotoLabel (Hdr->nnodes==0, "Zero number of nodes.",
 415     failure);
 416
 417   /*
 418    *  Type, number of variables (tot and support)
 419    */
 420
 421   *ddType = Hdr->ddType;
 422   *nVars = Hdr->nVars;
 423   *nsuppvars = Hdr->nsuppvars;
 424
 425   /*
 426    *  Support Varnames
 427    */
 428
 429   if (Hdr->suppVarNames != NULL) {
 430     *suppVarNames = DDDMP_ALLOC (char *, *nsuppvars);
 431     Dddmp_CheckAndGotoLabel (*suppVarNames==NULL,
 432       "Error allocating memory.", failure);
 433
 434     for (i=0; i<*nsuppvars; i++) {
 435       (*suppVarNames)[i] = DDDMP_ALLOC (char,
 436         (strlen (Hdr->suppVarNames[i]) + 1));
 437       Dddmp_CheckAndGotoLabel (Hdr->suppVarNames[i]==NULL,
 438         "Support Variable Name Missing in File.", failure);
 439       strcpy ((*suppVarNames)[i], Hdr->suppVarNames[i]);
 440     }
 441   } else {
 442     *suppVarNames = NULL;
 443   }
 444
 445   /*
 446    *  Ordered Varnames
 447    */
 448
 449   if (Hdr->orderedVarNames != NULL) {
 450     *orderedVarNames = DDDMP_ALLOC (char *, *nVars);
 451     Dddmp_CheckAndGotoLabel (*orderedVarNames==NULL,
 452       "Error allocating memory.", failure);
 453
 454     for (i=0; i<*nVars; i++) {
 455       (*orderedVarNames)[i]  = DDDMP_ALLOC (char,
 456         (strlen (Hdr->orderedVarNames[i]) + 1));
 457       Dddmp_CheckAndGotoLabel (Hdr->orderedVarNames[i]==NULL,
 458         "Support Variable Name Missing in File.", failure);
 459       strcpy ((*orderedVarNames)[i], Hdr->orderedVarNames[i]);
 460     }
 461   } else {
 462     *orderedVarNames = NULL;
 463   }
 464
 465   /*
 466    *  Variable Ids
 467    */
 468
 469   if (Hdr->ids != NULL) {
 470     tmpVarIds = DDDMP_ALLOC (int, *nsuppvars);
 471     Dddmp_CheckAndGotoLabel (tmpVarIds==NULL, "Error allocating memory.",
 472       failure);
 473     for (i=0; i<*nsuppvars; i++) {
 474       tmpVarIds[i] = Hdr->ids[i];
 475     }
 476
 477     *varIds = tmpVarIds;
 478   } else {
 479     *varIds = NULL;
 480   }
 481
 482   /*
 483    *  Variable Compose Ids
 484    */
 485
 486   if (Hdr->permids != NULL) {
 487     tmpVarComposeIds = DDDMP_ALLOC (int, *nsuppvars);
 488     Dddmp_CheckAndGotoLabel (tmpVarComposeIds==NULL,
 489       "Error allocating memory.", failure);
 490     for (i=0; i<*nsuppvars; i++) {
 491       tmpVarComposeIds[i] = Hdr->permids[i];
 492     }
 493
 494     *varComposeIds = tmpVarComposeIds;
 495   } else {
 496     *varComposeIds = NULL;
 497   }
 498
 499   /*
 500    *  Variable Auxiliary Ids
 501    */
 502
 503   if (Hdr->auxids != NULL) {
 504     tmpVarAuxIds = DDDMP_ALLOC (int, *nsuppvars);
 505     Dddmp_CheckAndGotoLabel (tmpVarAuxIds==NULL,
 506       "Error allocating memory.", failure);
 507     for (i=0; i<*nsuppvars; i++) {
 508       tmpVarAuxIds[i] = Hdr->auxids[i];
 509     }
 510
 511     *varAuxIds = tmpVarAuxIds;
 512   } else {
 513     *varAuxIds = NULL;
 514   }
 515
 516   /*
 517    *  Number of roots
 518    */
 519
 520   *nRoots = Hdr->nRoots;
 521
 522  /*
 523    *  Free and Return
 524    */
 525
 526   if (fileToClose == 1) {
 527     fclose (fp);
 528   }
 529
 530   DddmpFreeHeader(Hdr);
 531
 532   return (DDDMP_SUCCESS);
 533
 534   failure:
 535     return (DDDMP_FAILURE);
 536 }
 537
 538
 539 /*---------------------------------------------------------------------------*/
 540 /* Definition of internal functions                                          */
 541 /*---------------------------------------------------------------------------*/
 542
 543 /*---------------------------------------------------------------------------*/
 544 /* Definition of static functions                                            */
 545 /*---------------------------------------------------------------------------*/
 546
 547 /**Function********************************************************************
 548
 549   Synopsis    [Reads a dump file representing the argument BDDs.]
 550
 551   Description [Reads a dump file representing the argument BDDs. The header is
 552     common to both text and binary mode. The node list is either
 553     in text or binary format. A dynamic vector of DD pointers
 554     is allocated to support conversion from DD indexes to pointers.
 555     Several criteria are supported for variable match between file
 556     and dd manager. Several changes/permutations/compositions are allowed
 557     for variables while loading DDs. Variable of the dd manager are allowed
 558     to match with variables on file on ids, permids, varnames,
 559     varauxids; also direct composition between ids and
 560     composeids is supported. More in detail:
 561     <ol>
 562     <li> varMatchMode=DDDMP_VAR_MATCHIDS <p>
 563     allows the loading of a DD keeping variable IDs unchanged
 564     (regardless of the variable ordering of the reading manager); this
 565     is useful, for example, when swapping DDs to file and restoring them
 566     later from file, after possible variable reordering activations.
 567
 568     <li> varMatchMode=DDDMP_VAR_MATCHPERMIDS <p>
 569     is used to allow variable match according to the position in the ordering.
 570
 571     <li> varMatchMode=DDDMP_VAR_MATCHNAMES <p>
 572     requires a non NULL varmatchnames parameter; this is a vector of
 573     strings in one-to-one correspondence with variable IDs of the
 574     reading manager. Variables in the DD file read are matched with
 575     manager variables according to their name (a non NULL varnames
 576     parameter was required while storing the DD file).
 577
 578     <li> varMatchMode=DDDMP_VAR_MATCHIDS <p>
 579     has a meaning similar to DDDMP_VAR_MATCHNAMES, but integer auxiliary
 580     IDs are used instead of strings; the additional non NULL
 581     varmatchauxids parameter is needed.
 582
 583     <li> varMatchMode=DDDMP_VAR_COMPOSEIDS <p>
 584     uses the additional varcomposeids parameter is used as array of
 585     variable ids to be composed with ids stored in file.
 586     </ol>
 587
 588     In the present implementation, the array varnames (3), varauxids (4)
 589     and composeids (5) need to have one entry for each variable in the
 590     DD manager (NULL pointers are allowed for unused variables
 591     in varnames). Hence variables need to be already present in the
 592     manager. All arrays are sorted according to IDs.
 593     ]
 594
 595   SideEffects [A vector of pointers to DD nodes is allocated and freed.]
 596
 597   SeeAlso     [Dddmp_cuddBddArrayStore]
 598
 599 ******************************************************************************/
 600
 601 static int
 602 DddmpCuddDdArrayLoad (
 603   Dddmp_DecompType ddType           /* IN: Selects decomp type */,
 604   DdManager *ddMgr                  /* IN: DD Manager */,
 605   Dddmp_RootMatchType rootMatchMode /* IN: storing mode selector */,
 606   char **rootmatchnames             /* IN: sorted names for loaded roots */,
 607   Dddmp_VarMatchType varMatchMode   /* IN: storing mode selector */,
 608   char **varmatchnames              /* IN: array of variable names, by ids */,
 609   int *varmatchauxids               /* IN: array of variable auxids, by ids */,
 610   int *varcomposeids                /* IN: array of new ids, by ids */,
 611   int mode                          /* IN: requested input file format */,
 612   char *file                        /* IN: file name */,
 613   FILE *fp                          /* IN: file pointer */,
 614   DdNode ***pproots                 /* OUT: array BDD roots (by reference) */
 615   )
 616 {
 617   Dddmp_Hdr_t *Hdr = NULL;
 618   DdNode *f = NULL;
 619   DdNode *T = NULL;
 620   DdNode *E = NULL;
 621   struct binary_dd_code code;
 622   char buf[DDDMP_MAXSTRLEN];
 623   int retValue, id, size, maxv;
 624   int i, j, k, maxaux, var, vT, vE, idT, idE;
 625   double addConstant;
 626   int *permsupport = NULL;
 627   int *convertids = NULL;
 628   int *invconvertids = NULL;
 629   int *invauxids = NULL;
 630   char **sortedvarnames = NULL;
 631   int  nddvars, nRoots;
 632   DdNode **pnodes = NULL;
 633   unsigned char *pvars1byte = NULL;
 634   unsigned short *pvars2byte = NULL;
 635   DdNode **proots = NULL;
 636   int fileToClose = 0;
 637
 638   *pproots = NULL;
 639
 640   if (fp == NULL) {
 641     fp = fopen (file, "r");
 642     Dddmp_CheckAndGotoLabel (fp==NULL, "Error opening file.",
 643       failure);
 644     fileToClose = 1;
 645   }
 646
 647   nddvars = ddMgr->size;
 648
 649   Hdr = DddmpBddReadHeader (NULL, fp);
 650
 651   Dddmp_CheckAndGotoLabel (Hdr->nnodes==0, "Zero number of nodes.",
 652     failure);
 653
 654   nRoots = Hdr->nRoots;
 655
 656   if (Hdr->ddType != ddType) {
 657     (void) fprintf (stderr, "DdLoad Error: ddType mismatch\n");
 658
 659    if (Hdr->ddType == DDDMP_BDD)
 660       (void) fprintf (stderr, "BDD found\n");
 661     if (Hdr->ddType == DDDMP_ADD)
 662       (void) fprintf (stderr, "ADD found\n");
 663     if (ddType == DDDMP_BDD)
 664       (void) fprintf (stderr, "when loading a BDD\n");
 665     if (ddType == DDDMP_ADD)
 666       (void) fprintf (stderr, "when loading an ADD\n");
 667
 668     fflush (stderr);
 669     goto failure;
 670   }
 671
 672   if (Hdr->mode != mode) {
 673     Dddmp_CheckAndGotoLabel (mode!=DDDMP_MODE_DEFAULT,
 674       "Mode Mismatch.", failure);
 675     mode = Hdr->mode;
 676   }
 677
 678   /*
 679    *  For each variable in the support
 680    *  compute the relative position in the ordering
 681    *  (within the support only)
 682    */
 683
 684   permsupport = DDDMP_ALLOC (int, Hdr->nsuppvars);
 685   Dddmp_CheckAndGotoLabel (permsupport==NULL, "Error allocating memory.",
 686     failure);
 687   for (i=0,k=0; i < Hdr->nVars; i++) {
 688     for (j=0; j < Hdr->nsuppvars; j++) {
 689       if (Hdr->permids[j] == i) {
 690         permsupport[j] = k++;
 691       }
 692     }
 693   }
 694   Dddmp_Assert (k==Hdr->nsuppvars, "k==Hdr->nsuppvars");
 695
 696   if (Hdr->suppVarNames != NULL) {
 697     /*
 698      *  Varnames are sorted for binary search
 699      */
 700
 701     sortedvarnames = DDDMP_ALLOC(char *, Hdr->nsuppvars);
 702     Dddmp_CheckAndGotoLabel (sortedvarnames==NULL, "Error allocating memory.",
 703       failure);
 704     for (i=0; i<Hdr->nsuppvars; i++) {
 705       Dddmp_CheckAndGotoLabel (Hdr->suppVarNames[i]==NULL,
 706         "Support Variable Name Missing in File.", failure);
 707       sortedvarnames[i] = Hdr->suppVarNames[i];
 708     }
 709
 710     qsort ((void *) sortedvarnames, Hdr->nsuppvars,
 711       sizeof(char *), QsortStrcmp);
 712
 713   }
 714
 715   /*
 716    *  Convertids is the array used to convert variable ids from positional
 717    *  (shrinked) ids used within the DD file.
 718    *  Positions in the file are from 0 to nsuppvars-1.
 719    */
 720
 721   convertids = DDDMP_ALLOC (int, Hdr->nsuppvars);
 722   Dddmp_CheckAndGotoLabel (convertids==NULL, "Error allocating memory.",
 723     failure);
 724
 725   again_matchmode:
 726   switch (varMatchMode) {
 727     case DDDMP_VAR_MATCHIDS:
 728       for (i=0; i<Hdr->nsuppvars; i++) {
 729         convertids[permsupport[i]] = Hdr->ids[i];
 730       }
 731       break;
 732     case DDDMP_VAR_MATCHPERMIDS:
 733       for (i=0; i<Hdr->nsuppvars; i++) {
 734         convertids[permsupport[i]] = Cudd_ReadInvPerm (ddMgr,
 735           Hdr->permids[i]);
 736       }
 737       break;
 738     case DDDMP_VAR_MATCHAUXIDS:
 739       if (Hdr->auxids == NULL) {
 740         (void) fprintf (stderr,
 741            "DdLoad Error: variable auxids matching requested\n");
 742         (void) fprintf (stderr, "but .auxids not found in BDD file\n");
 743         (void) fprintf (stderr, "Matching IDs forced.\n");
 744         fflush (stderr);
 745         varMatchMode = DDDMP_VAR_MATCHIDS;
 746         goto again_matchmode;
 747       }
 748       /* find max auxid value to alloc invaux array */
 749       for (i=0,maxaux= -1; i<nddvars; i++) {
 750         if (varmatchauxids[i]>maxaux) {
 751           maxaux = varmatchauxids[i];
 752         }
 753       }
 754       /* generate invaux array */
 755       invauxids = DDDMP_ALLOC (int, maxaux+1);
 756       Dddmp_CheckAndGotoLabel (invauxids==NULL, "Error allocating memory.",
 757         failure);
 758
 759       for (i=0; i<=maxaux; i++) {
 760         invauxids[i] = -1;
 761       }
 762
 763       for (i=0; i<Hdr->nsuppvars; i++) {
 764         invauxids[varmatchauxids[Hdr->ids[i]]] = Hdr->ids[i];
 765       }
 766
 767       /* generate convertids array */
 768       for (i=0; i<Hdr->nsuppvars; i++) {
 769         if ((Hdr->auxids[i]>maxaux) || (invauxids[Hdr->auxids[i]]<0)) {
 770           (void) fprintf (stderr,
 771             "DdLoad Error: auxid %d not found in DD manager.\n",
 772             Hdr->auxids[i]);
 773           (void) fprintf (stderr, "ID matching forced (%d).\n", i);
 774           (void) fprintf (stderr,
 775             "Beware of possible overlappings with other variables\n");
 776           fflush (stderr);
 777           convertids[permsupport[i]] = i;
 778         } else {
 779           convertids[permsupport[i]] = invauxids[Hdr->auxids[i]];
 780         }
 781       }
 782       break;
 783     case DDDMP_VAR_MATCHNAMES:
 784       if (Hdr->suppVarNames == NULL) {
 785         (void) fprintf (stderr,
 786           "DdLoad Error: variable names matching requested\n");
 787         (void) fprintf (stderr, "but .suppvarnames not found in BDD file\n");
 788         (void) fprintf (stderr, "Matching IDs forced.\n");
 789         fflush (stderr);
 790         varMatchMode = DDDMP_VAR_MATCHIDS;
 791         goto again_matchmode;
 792       }
 793
 794       /* generate invaux array */
 795       invauxids = DDDMP_ALLOC (int, Hdr->nsuppvars);
 796       Dddmp_CheckAndGotoLabel (invauxids==NULL, "Error allocating memory.",
 797         failure);
 798
 799       for (i=0; i<Hdr->nsuppvars; i++) {
 800         invauxids[i] = -1;
 801       }
 802
 803       for (i=0; i<nddvars; i++) {
 804         if (varmatchnames[i]==NULL) {
 805           (void) fprintf (stderr,
 806             "DdLoad Warning: NULL match variable name (id: %d). Ignored.\n",
 807             i);
 808           fflush (stderr);
 809         }
 810         else
 811           if ((j=FindVarname(varmatchnames[i],sortedvarnames,Hdr->nsuppvars))
 812                >=0) {
 813             Dddmp_Assert (j<Hdr->nsuppvars, "j<Hdr->nsuppvars");
 814             invauxids[j] = i;
 815           }
 816       }
 817       /* generate convertids array */
 818       for (i=0; i<Hdr->nsuppvars; i++) {
 819         Dddmp_Assert (Hdr->suppVarNames[i]!=NULL,
 820           "Hdr->suppVarNames[i] != NULL");
 821         j=FindVarname(Hdr->suppVarNames[i],sortedvarnames,Hdr->nsuppvars);
 822         Dddmp_Assert ((j>=0) && (j<Hdr->nsuppvars),
 823           "(j>=0) && (j<Hdr->nsuppvars)");
 824         if (invauxids[j]<0) {
 825           fprintf (stderr,
 826             "DdLoad Error: varname %s not found in DD manager.",
 827              Hdr->suppVarNames[i]);
 828           fprintf (stderr, "ID matching forced (%d)\n", i);
 829           fflush (stderr);
 830           convertids[permsupport[i]]=i;
 831         } else {
 832           convertids[permsupport[i]] = invauxids[j];
 833         }
 834       }
 835       break;
 836     case DDDMP_VAR_COMPOSEIDS:
 837       for (i=0; i<Hdr->nsuppvars; i++) {
 838         convertids[permsupport[i]] = varcomposeids[Hdr->ids[i]];
 839       }
 840       break;
 841   }
 842
 843   maxv = (-1);
 844   for (i=0; i<Hdr->nsuppvars; i++) {
 845     if (convertids[i] > maxv) {
 846       maxv = convertids[i];
 847     }
 848   }
 849
 850   invconvertids = DDDMP_ALLOC (int, maxv+1);
 851   Dddmp_CheckAndGotoLabel (invconvertids==NULL, "Error allocating memory.",
 852     failure);
 853
 854   for (i=0; i<=maxv; i++) {
 855     invconvertids[i]= -1;
 856   }
 857
 858   for (i=0; i<Hdr->nsuppvars; i++) {
 859     invconvertids[convertids[i]] = i;
 860   }
 861
 862   pnodes = DDDMP_ALLOC(DdNode *,(Hdr->nnodes+1));
 863   Dddmp_CheckAndGotoLabel (pnodes==NULL, "Error allocating memory.",
 864     failure);
 865
 866   if (Hdr->nsuppvars < 256) {
 867     pvars1byte = DDDMP_ALLOC(unsigned char,(Hdr->nnodes+1));
 868     Dddmp_CheckAndGotoLabel (pvars1byte==NULL, "Error allocating memory.",
 869       failure);
 870   }
 871   else if (Hdr->nsuppvars < 0xffff) {
 872     pvars2byte = DDDMP_ALLOC(unsigned short,(Hdr->nnodes+1));
 873     Dddmp_CheckAndGotoLabel (pvars2byte==NULL, "Error allocating memory.",
 874       failure);
 875   } else {
 876     (void) fprintf (stderr,
 877        "DdLoad Error: more than %d variables. Not supported.\n", 0xffff);
 878     fflush (stderr);
 879     goto failure;
 880   }
 881
 882   /*-------------- Deal With Nodes ... One Row File at a Time --------------*/
 883
 884   for (i=1; i<=Hdr->nnodes; i++) {
 885
 886     Dddmp_CheckAndGotoLabel (feof(fp),
 887       "Unexpected EOF While Reading DD Nodes.", failure);
 888
 889     switch (mode) {
 890
 891       /*
 892        *  Text FORMAT
 893        */
 894
 895       case DDDMP_MODE_TEXT:
 896
 897         switch (Hdr->varinfo) {
 898           case DDDMP_VARIDS:
 899           case DDDMP_VARPERMIDS:
 900           case DDDMP_VARAUXIDS:
 901           case DDDMP_VARNAMES:
 902             retValue = fscanf(fp, "%d %*s %s %d %d\n", &id, buf, &idT, &idE);
 903             Dddmp_CheckAndGotoLabel (retValue<4,
 904               "Error Reading Nodes in Text Mode.", failure);
 905             break;
 906           case DDDMP_VARDEFAULT:
 907             retValue = fscanf(fp, "%d %s %d %d\n", &id, buf, &idT, &idE);
 908             Dddmp_CheckAndGotoLabel (retValue<4,
 909               "Error Reading Nodes in Text Mode.", failure);
 910             break;
 911         }
 912 #ifdef DDDMP_DEBUG
 913         Dddmp_Assert (id==i, "id == i");
 914 #endif
 915         if (idT==0 && idE==0) {
 916           /* leaf node: a constant */
 917           if (strcmp(buf, "1") == 0) {
 918             pnodes[i] = Cudd_ReadOne (ddMgr);
 919           } else {
 920             /* this is an ADD constant ! */
 921             if (strcmp(buf, "0") == 0) {
 922               pnodes[i] = Cudd_ReadZero (ddMgr);
 923             } else {
 924               addConstant = atof(buf);
 925               pnodes[i] = Cudd_addConst (ddMgr,
 926                 (CUDD_VALUE_TYPE) addConstant);
 927             }
 928           }
 929
 930           /* StQ 11.02.2004:
 931              Bug fixed --> Reference All Nodes for ADD */
 932           Cudd_Ref (pnodes[i]);
 933           Dddmp_CheckAndGotoLabel (pnodes[i]==NULL, "NULL pnodes.",
 934             failure);
 935           continue;
 936         } else {
 937 #ifdef DDDMP_DEBUG
 938           Dddmp_Assert (idT>0, "id > 0");
 939 #endif
 940           var = atoi(buf);
 941           T = pnodes[idT];
 942           if(idE<0) {
 943             idE = -idE;
 944             E = pnodes[idE];
 945             E = Cudd_Not(E);
 946           } else {
 947             E = pnodes[idE];
 948           }
 949         }
 950
 951         break;
 952
 953       /*
 954        *  Binary FORMAT
 955        */
 956
 957       case DDDMP_MODE_BINARY:
 958
 959         Dddmp_CheckAndGotoLabel (DddmpReadCode(fp,&code) == 0,
 960           "Error Reading witn ReadCode.", failure);
 961
 962         switch (code.V) {
 963         case DDDMP_TERMINAL:
 964           /* only 1 terminal presently supported */
 965           pnodes[i] = Cudd_ReadOne (ddMgr);
 966           continue;
 967           break;
 968         case DDDMP_RELATIVE_1:
 969           break;
 970         case DDDMP_RELATIVE_ID:
 971         case DDDMP_ABSOLUTE_ID:
 972           size = DddmpReadInt (fp, &var);
 973           Dddmp_CheckAndGotoLabel (size==0, "Error reading size.",
 974             failure);
 975           break;
 976         }
 977
 978         switch (code.T) {
 979         case DDDMP_TERMINAL:
 980           idT = 1;
 981           break;
 982         case DDDMP_RELATIVE_1:
 983           idT = i-1;
 984           break;
 985         case DDDMP_RELATIVE_ID:
 986           size = DddmpReadInt (fp, &id);
 987           Dddmp_CheckAndGotoLabel (size==0, "Error reading size.",
 988             failure);
 989           idT = i-id;
 990           break;
 991         case DDDMP_ABSOLUTE_ID:
 992           size = DddmpReadInt (fp, &idT);
 993           Dddmp_CheckAndGotoLabel (size==0, "Error reading size.",
 994             failure);
 995           break;
 996         }
 997
 998         switch (code.E) {
 999         case DDDMP_TERMINAL:
1000           idE = 1;
1001           break;
1002         case DDDMP_RELATIVE_1:
1003           idE = i-1;
1004           break;
1005         case DDDMP_RELATIVE_ID:
1006           size = DddmpReadInt (fp, &id);
1007           Dddmp_CheckAndGotoLabel (size==0, "Error reading size.",
1008             failure);
1009           idE = i-id;
1010           break;
1011         case DDDMP_ABSOLUTE_ID:
1012           size = DddmpReadInt (fp, &idE);
1013           Dddmp_CheckAndGotoLabel (size==0, "Error reading size.",
1014             failure);
1015           break;
1016         }
1017
1018 #ifdef DDDMP_DEBUG
1019       Dddmp_Assert (idT<i, "id<i");
1020 #endif
1021       T = pnodes[idT];
1022       if (cuddIsConstant(T))
1023         vT = Hdr->nsuppvars;
1024       else {
1025         if (pvars1byte != NULL)
1026           vT = pvars1byte[idT];
1027         else if (pvars2byte != NULL)
1028           vT = pvars2byte[idT];
1029         else
1030           vT = invconvertids[T->index];
1031       }
1032 #ifdef DDDMP_DEBUG
1033       Dddmp_Assert (vT>0, "vT > 0");
1034       Dddmp_Assert (vT<=Hdr->nsuppvars, "vT <= Hdr->nsuppvars");
1035 #endif
1036
1037 #ifdef DDDMP_DEBUG
1038       Dddmp_Assert (idE<i, "idE < i");
1039 #endif
1040       E = pnodes[idE];
1041       if (cuddIsConstant(E))
1042         vE = Hdr->nsuppvars;
1043       else {
1044         if (pvars1byte != NULL)
1045           vE = pvars1byte[idE];
1046         else if (pvars2byte != NULL)
1047           vE = pvars2byte[idE];
1048         else
1049           vE = invconvertids[E->index];
1050       }
1051 #ifdef DDDMP_DEBUG
1052       Dddmp_Assert (vE>0, "vE > 0");
1053       Dddmp_Assert (vE<=Hdr->nsuppvars, "vE <= Hdr->nsuppvars");
1054 #endif
1055
1056       switch (code.V) {
1057         case DDDMP_TERMINAL:
1058         case DDDMP_ABSOLUTE_ID:
1059           break;
1060         case DDDMP_RELATIVE_1:
1061           var = (vT<vE) ? vT-1 : vE-1;
1062           break;
1063         case DDDMP_RELATIVE_ID:
1064           var = (vT<vE) ? vT-var : vE-var;
1065           break;
1066       }
1067
1068       if (code.Ecompl) {
1069         E = Cudd_Not(E);
1070       }
1071
1072 #ifdef DDDMP_DEBUG
1073       Dddmp_Assert (var<Hdr->nsuppvars, "var < Hdr->nsuppvars");
1074 #endif
1075
1076       break;
1077     }
1078
1079     if (pvars1byte != NULL) {
1080       pvars1byte[i] = (unsigned char) var;
1081     } else {
1082       if (pvars2byte != NULL) {
1083         pvars2byte[i] = (unsigned short) var;
1084       }
1085     }
1086
1087     var = convertids[var];
1088     switch (ddType) {
1089       case DDDMP_BDD:
1090         pnodes[i] = Cudd_bddIte (ddMgr, Cudd_bddIthVar (ddMgr, var),
1091           T, E);
1092         break;
1093       case DDDMP_ADD:
1094         {
1095         DdNode *tmp = Cudd_addIthVar (ddMgr, var);
1096         Cudd_Ref (tmp);
1097         pnodes[i] = Cudd_addIte (ddMgr, tmp, T, E);
1098         Cudd_RecursiveDeref (ddMgr, tmp);
1099         break;
1100         }
1101       case DDDMP_CNF:
1102       case DDDMP_NONE:
1103         Dddmp_Warning (1, "Wrong DD Type.");
1104         break;
1105      }
1106
1107     cuddRef (pnodes[i]);
1108   }
1109
1110   /*------------------------ Deal With the File Tail -----------------------*/
1111
1112   fgets (buf, DDDMP_MAXSTRLEN-1,fp);
1113   Dddmp_CheckAndGotoLabel (!matchkeywd(buf, ".end"),
1114     "Error .end not found.", failure);
1115
1116   /* Close File IFF Necessary */
1117   if (fileToClose) {
1118     fclose (fp);
1119   }
1120
1121   /* BDD Roots */
1122   proots = DDDMP_ALLOC(DdNode *,nRoots);
1123   Dddmp_CheckAndGotoLabel (proots==NULL, "Error allocating memory.",
1124     failure);
1125
1126   for(i=0; i<nRoots; ++i) {
1127     switch (rootMatchMode) {
1128       case DDDMP_ROOT_MATCHNAMES:
1129         for (j=0; j<nRoots; j++) {
1130           if (strcmp(rootmatchnames[i], Hdr->rootnames[j]) == 0)
1131             break;
1132         }
1133         if (j>=nRoots) {
1134           /* rootname not found */
1135           fprintf (stderr, "Warning: unable to match root name <%s>\n",
1136             rootmatchnames[i]);
1137         }
1138         break;
1139       case DDDMP_ROOT_MATCHLIST:
1140         j = i;
1141         break;
1142     }
1143
1144     id = Hdr->rootids[i];
1145     if (id==0) {
1146       (void) fprintf (stderr, "DdLoad Warning: NULL root found in file\n");
1147       fflush (stderr);
1148       f = NULL;
1149     } else {
1150       if (id<0) {
1151         f = Cudd_Not(pnodes[-id]);
1152       } else {
1153         f = pnodes[id];
1154       }
1155     }
1156     proots[i] = f;
1157
1158     cuddRef (f);
1159   } /* end for i = 0..nRoots */
1160
1161   /*
1162    *  Decrease Reference for all Nodes
1163    */
1164
1165   /* StQ 11.02.2004:
1166      Bug fixed --> De-Reference All Nodes for ADD */
1167   for (i=1; i<=Hdr->nnodes; i++) {
1168     f = pnodes[i];
1169     Cudd_RecursiveDeref (ddMgr, f);
1170   }
1171
1172   /*
1173    *  Free Memory: load_end label
1174    */
1175
1176 load_end:
1177
1178   DddmpFreeHeader(Hdr);
1179
1180   DDDMP_FREE (pnodes);
1181   DDDMP_FREE (pvars1byte);
1182   DDDMP_FREE (pvars2byte);
1183
1184   /* variable names are not freed because they were shared with varnames */
1185   DDDMP_FREE (sortedvarnames);
1186
1187   DDDMP_FREE (permsupport);
1188   DDDMP_FREE (convertids);
1189   DDDMP_FREE (invconvertids);
1190   DDDMP_FREE (invauxids);
1191
1192   *pproots = proots;
1193   return (nRoots);
1194
1195   /*
1196    *  Failure Condition
1197    */
1198
1199 failure:
1200
1201   if (fileToClose) {
1202     fclose (fp);
1203   }
1204
1205   nRoots = 0; /* return 0 on error ! */
1206
1207   DDDMP_FREE (proots);
1208
1209   goto load_end; /* this is done to free memory */
1210 }
1211
1212 /**Function********************************************************************
1213
1214   Synopsis    [Reads a the header of a dump file representing the
1215     argument BDDs.
1216     ]
1217
1218   Description [Reads the header of a dump file. Builds a Dddmp_Hdr_t struct
1219     containing all infos in the header, for next manipulations.
1220     ]
1221
1222   SideEffects [none]
1223
1224   SeeAlso     []
1225
1226 ******************************************************************************/
1227
1228 static Dddmp_Hdr_t *
1229 DddmpBddReadHeader (
1230   char *file        /* IN: file name */,
1231   FILE *fp          /* IN: file pointer */
1232   )
1233 {
1234   Dddmp_Hdr_t *Hdr = NULL;
1235   char buf[DDDMP_MAXSTRLEN];
1236   int retValue, fileToClose = 0;
1237
1238   if (fp == NULL) {
1239     fp = fopen (file, "r");
1240     Dddmp_CheckAndGotoLabel (fp==NULL, "Error opening file.",
1241       failure);
1242     fileToClose = 1;
1243   }
1244
1245   /* START HEADER */
1246
1247   Hdr = DDDMP_ALLOC (Dddmp_Hdr_t,1);
1248   if (Hdr == NULL) {
1249     return NULL;
1250   }
1251   Hdr->ver = NULL;
1252   Hdr->mode = 0;
1253   Hdr->ddType = DDDMP_BDD;
1254   Hdr->varinfo = DDDMP_VARIDS;
1255   Hdr->dd = NULL;
1256   Hdr->nnodes = 0;
1257   Hdr->nVars = 0;
1258   Hdr->nsuppvars = 0;
1259   Hdr->suppVarNames = NULL;
1260   Hdr->orderedVarNames = NULL;
1261   Hdr->ids = NULL;
1262   Hdr->permids = NULL;
1263   Hdr->auxids = NULL;
1264   Hdr->cnfids = NULL;
1265   Hdr->nRoots = 0;
1266   Hdr->rootids = NULL;
1267   Hdr->rootnames = NULL;
1268   Hdr->nAddedCnfVar = 0;
1269   Hdr->nVarsCnf = 0;
1270   Hdr->nClausesCnf = 0;
1271
1272   while (fscanf(fp, "%s", buf)!=EOF) {
1273
1274     /* comment */
1275     if (buf[0] == '#') {
1276       fgets(buf,DDDMP_MAXSTRLEN,fp);
1277       continue;
1278     }
1279
1280     Dddmp_CheckAndGotoLabel (buf[0] != '.',
1281       "Error; line must begin with '.' or '#'.",
1282         failure);
1283
1284     if (matchkeywd(buf, ".ver")) {
1285       /* this not checked so far: only read */
1286       retValue = fscanf (fp, "%s", buf);
1287       Dddmp_CheckAndGotoLabel (retValue==EOF, "Error reading from file.",
1288         failure);
1289
1290       Hdr->ver=DddmpStrDup(buf);
1291       Dddmp_CheckAndGotoLabel (Hdr->ver==NULL,
1292         "Error allocating memory.", failure);
1293
1294       continue;
1295     }
1296
1297     if (matchkeywd(buf, ".add")) {
1298       Hdr->ddType = DDDMP_ADD;
1299       continue;
1300     }
1301
1302     if (matchkeywd(buf, ".bdd")) {
1303       Hdr->ddType = DDDMP_BDD;
1304       continue;
1305     }
1306
1307     if (matchkeywd(buf, ".mode")) {
1308       retValue = fscanf (fp, "%s", buf);
1309       Dddmp_CheckAndGotoLabel (retValue==EOF, "Error reading to file.",
1310         failure);
1311
1312       Hdr->mode = buf[0];
1313       continue;
1314     }
1315
1316     if (matchkeywd(buf, ".varinfo")) {
1317       int readMe;
1318       retValue = fscanf (fp, "%d", &readMe);
1319       Dddmp_CheckAndGotoLabel (retValue==EOF, "Error reading file.",
1320         failure);
1321       Hdr->varinfo = (Dddmp_VarInfoType) readMe;
1322
1323       continue;
1324     }
1325
1326     if (matchkeywd(buf, ".dd")) {
1327       retValue = fscanf (fp, "%s", buf);
1328       Dddmp_CheckAndGotoLabel (retValue==EOF, "Error reading file.",
1329         failure);
1330
1331       Hdr->dd = DddmpStrDup (buf);
1332       Dddmp_CheckAndGotoLabel (Hdr->dd==NULL, "Error allocating memory.",
1333         failure);
1334
1335       continue;
1336     }
1337
1338     if (matchkeywd(buf, ".nnodes")) {
1339       retValue = fscanf (fp, "%d", &(Hdr->nnodes));
1340       Dddmp_CheckAndGotoLabel (retValue==EOF, "Error reading file.",
1341         failure);
1342
1343       continue;
1344     }
1345
1346     if (matchkeywd(buf, ".nvars")) {
1347       retValue = fscanf (fp, "%d", &(Hdr->nVars));
1348       Dddmp_CheckAndGotoLabel (retValue==EOF, "Error reading file.",
1349         failure);
1350
1351       continue;
1352     }
1353
1354     if (matchkeywd(buf, ".nsuppvars")) {
1355       retValue = fscanf (fp, "%d", &(Hdr->nsuppvars));
1356       Dddmp_CheckAndGotoLabel (retValue==EOF, "Error reading file.",
1357         failure);
1358
1359       continue;
1360     }
1361
1362     if (matchkeywd(buf, ".orderedvarnames")) {
1363       Hdr->orderedVarNames = DddmpStrArrayRead (fp, Hdr->nVars);
1364       Dddmp_CheckAndGotoLabel (Hdr->orderedVarNames==NULL,
1365         "Error allocating memory.", failure);
1366
1367       continue;
1368     }
1369
1370     if (matchkeywd(buf, ".suppvarnames") ||
1371       ((strcmp (Hdr->ver, "DDDMP-1.0") == 0) &&
1372       matchkeywd (buf, ".varnames"))) {
1373       Hdr->suppVarNames = DddmpStrArrayRead (fp, Hdr->nsuppvars);
1374       Dddmp_CheckAndGotoLabel (Hdr->suppVarNames==NULL,
1375         "Error allocating memory.", failure);
1376
1377       continue;
1378     }
1379
1380     if matchkeywd(buf, ".ids") {
1381       Hdr->ids = DddmpIntArrayRead(fp,Hdr->nsuppvars);
1382       Dddmp_CheckAndGotoLabel (Hdr->ids==NULL,
1383         "Error allocating memory.", failure);
1384
1385       continue;
1386     }
1387
1388     if (matchkeywd(buf, ".permids")) {
1389       Hdr->permids = DddmpIntArrayRead(fp,Hdr->nsuppvars);
1390       Dddmp_CheckAndGotoLabel (Hdr->permids==NULL,
1391         "Error allocating memory.", failure);
1392
1393       continue;
1394     }
1395
1396     if (matchkeywd(buf, ".auxids")) {
1397       Hdr->auxids = DddmpIntArrayRead(fp,Hdr->nsuppvars);
1398       Dddmp_CheckAndGotoLabel (Hdr->auxids==NULL,
1399         "Error allocating memory.", failure);
1400
1401       continue;
1402     }
1403
1404     if (matchkeywd(buf, ".nroots")) {
1405       retValue = fscanf (fp, "%d", &(Hdr->nRoots));
1406       Dddmp_CheckAndGotoLabel (retValue==EOF, "Error reading file.",
1407         failure);
1408
1409       continue;
1410     }
1411
1412     if (matchkeywd(buf, ".rootids")) {
1413       Hdr->rootids = DddmpIntArrayRead(fp,Hdr->nRoots);
1414       Dddmp_CheckAndGotoLabel (Hdr->rootids==NULL,
1415         "Error allocating memory.", failure);
1416
1417       continue;
1418     }
1419
1420     if (matchkeywd(buf, ".rootnames")) {
1421       Hdr->rootnames = DddmpStrArrayRead(fp,Hdr->nRoots);
1422       Dddmp_CheckAndGotoLabel (Hdr->rootnames==NULL,
1423         "Error allocating memory.", failure);
1424
1425       continue;
1426     }
1427
1428     if (matchkeywd(buf, ".nodes")) {
1429       fgets(buf,DDDMP_MAXSTRLEN,fp);
1430       break;
1431     }
1432
1433   }
1434
1435   /* END HEADER */
1436
1437   return (Hdr);
1438
1439 failure:
1440
1441   if (fileToClose == 1) {
1442     fclose (fp);
1443   }
1444
1445   DddmpFreeHeader(Hdr);
1446
1447   return (NULL);
1448 }
1449
1450
1451 /**Function********************************************************************
1452
1453   Synopsis    [Frees the internal header structure.]
1454
1455   Description [Frees the internal header structureby freeing all internal
1456     fields first.
1457     ]
1458
1459   SideEffects []
1460
1461   SeeAlso     []
1462
1463 ******************************************************************************/
1464
1465 static void
1466 DddmpFreeHeader (
1467   Dddmp_Hdr_t *Hdr   /* IN: pointer to header */
1468   )
1469 {
1470   DDDMP_FREE (Hdr->ver);
1471   DDDMP_FREE (Hdr->dd);
1472   DddmpStrArrayFree (Hdr->orderedVarNames, Hdr->nVars);
1473   DddmpStrArrayFree (Hdr->suppVarNames, Hdr->nsuppvars);
1474   DDDMP_FREE (Hdr->ids);
1475   DDDMP_FREE (Hdr->permids);
1476   DDDMP_FREE (Hdr->auxids);
1477   DDDMP_FREE (Hdr->rootids);
1478   DddmpStrArrayFree (Hdr->rootnames, Hdr->nRoots);
1479
1480   DDDMP_FREE (Hdr);
1481
1482   return;
1483 }
1484
1485
1486