source: icGREP/icgrep-devel/cudd-2.5.1/dddmp/dddmpLoad.c @ 4597

Last change on this file since 4597 was 4597, checked in by nmedfort, 4 years ago

Upload of the CUDD library.

File size: 43.7 KB
Line 
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
65static 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);
66static Dddmp_Hdr_t * DddmpBddReadHeader(char *file, FILE *fp);
67static 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
93DdNode *
94Dddmp_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
186int
187Dddmp_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
256DdNode *
257Dddmp_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
306int
307Dddmp_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
383int
384Dddmp_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
601static int
602DddmpCuddDdArrayLoad (
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
1176load_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
1199failure:
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
1228static Dddmp_Hdr_t *
1229DddmpBddReadHeader (
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
1439failure:
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
1465static void
1466DddmpFreeHeader (
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
Note: See TracBrowser for help on using the repository browser.