source: icGREP/icgrep-devel/cudd-2.5.1/dddmp/dddmpLoadCnf.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: 28.9 KB
Line 
1/**CFile**********************************************************************
2
3  FileName     [dddmpLoadCnf.c]
4
5  PackageName  [dddmp]
6
7  Synopsis     [Functions to read in CNF from file as BDDs.]
8
9  Description  [Functions to read in CNF from file as BDDs.
10    ]
11
12  Author       [Gianpiero Cabodi and Stefano Quer]
13
14  Copyright    [
15    Copyright (c) 2004 by Politecnico di Torino.
16    All Rights Reserved. This software is for educational purposes only.
17    Permission is given to academic institutions to use, copy, and modify
18    this software and its documentation provided that this introductory
19    message is not removed, that this software and its documentation is
20    used for the institutions' internal research and educational purposes,
21    and that no monies are exchanged. No guarantee is expressed or implied
22    by the distribution of this code.
23    Send bug-reports and/or questions to:
24    {gianpiero.cabodi,stefano.quer}@polito.it.
25    ]
26
27******************************************************************************/
28
29#include "dddmpInt.h"
30
31/*---------------------------------------------------------------------------*/
32/* Constant declarations                                                     */
33/*---------------------------------------------------------------------------*/
34
35#define DDDMP_MAX_CNF_ROW_LENGTH 1000
36#define DDDMP_DEBUG_CNF 0
37
38/*---------------------------------------------------------------------------*/
39/* Stucture declarations                                                     */
40/*---------------------------------------------------------------------------*/
41
42/*---------------------------------------------------------------------------*/
43/* Type declarations                                                         */
44/*---------------------------------------------------------------------------*/
45
46/*---------------------------------------------------------------------------*/
47/* Variable declarations                                                     */
48/*---------------------------------------------------------------------------*/
49
50/*---------------------------------------------------------------------------*/
51/* Macro declarations                                                        */
52/*---------------------------------------------------------------------------*/
53
54#define matchkeywd(str,key) (strncmp(str,key,strlen(key))==0)
55
56/**AutomaticStart*************************************************************/
57
58/*---------------------------------------------------------------------------*/
59/* Static function prototypes                                                */
60/*---------------------------------------------------------------------------*/
61
62static int DddmpCuddDdArrayLoadCnf(DdManager *ddMgr, Dddmp_RootMatchType rootmatchmode, char **rootmatchnames, Dddmp_VarMatchType varmatchmode, char **varmatchnames, int *varmatchauxids, int *varcomposeids, int mode, char *file, FILE *fp, DdNode ***rootsPtrPtr, int *nRoots);
63static Dddmp_Hdr_t * DddmpBddReadHeaderCnf(char *file, FILE *fp);
64static void DddmpFreeHeaderCnf(Dddmp_Hdr_t *Hdr);
65static int DddmpReadCnfClauses(Dddmp_Hdr_t *Hdr, int ***cnfTable, FILE *fp);
66static int DddmpCnfClauses2Bdd(Dddmp_Hdr_t *Hdr, DdManager *ddMgr, int **cnfTable, int mode, DdNode ***rootsPtrPtr);
67
68/**AutomaticEnd***************************************************************/
69
70/*---------------------------------------------------------------------------*/
71/* Definition of exported functions                                          */
72/*---------------------------------------------------------------------------*/
73
74/**Function********************************************************************
75
76  Synopsis     [Reads a dump file in a CNF format.]
77
78  Description  [Reads a dump file representing the argument BDD in a
79    CNF formula.
80    Dddmp_cuddBddArrayLoadCnf is used through a dummy array.
81    The results is returned in different formats depending on the
82    mode selection:
83      IFF mode == 0 Return the Clauses without Conjunction
84      IFF mode == 1 Return the sets of BDDs without Quantification
85      IFF mode == 2 Return the sets of BDDs AFTER Existential Quantification
86   ]
87
88  SideEffects  [A vector of pointers to DD nodes is allocated and freed.]
89
90  SeeAlso      [Dddmp_cuddBddLoad, Dddmp_cuddBddArrayLoad]
91
92******************************************************************************/
93
94int
95Dddmp_cuddBddLoadCnf (
96  DdManager *ddMgr                /* IN: DD Manager */,
97  Dddmp_VarMatchType varmatchmode /* IN: storing mode selector */,
98  char **varmatchnames            /* IN: array of variable names, by IDs */,
99  int *varmatchauxids             /* IN: array of variable auxids, by IDs */,
100  int *varcomposeids              /* IN: array of new ids accessed, by IDs */,
101  int mode                        /* IN: computation mode */,
102  char *file                      /* IN: file name */,
103  FILE *fp                        /* IN: file pointer */,
104  DdNode ***rootsPtrPtr           /* OUT: array of returned BDD roots */,
105  int *nRoots                     /* OUT: number of BDDs returned */
106  )
107{
108  int i, retValue;
109
110  retValue = Dddmp_cuddBddArrayLoadCnf (ddMgr, DDDMP_ROOT_MATCHLIST, NULL,
111    varmatchmode, varmatchnames, varmatchauxids, varcomposeids, mode,
112    file, fp, rootsPtrPtr, nRoots);
113
114  if (retValue == DDDMP_FAILURE) {
115    return (DDDMP_FAILURE);
116  }
117
118  if (*nRoots > 1) {
119    fprintf (stderr,
120      "Warning: %d BDD roots found in file. Only first retrieved.\n",
121      *nRoots);
122    for (i=1; i<*nRoots; i++) {
123      Cudd_RecursiveDeref (ddMgr, *rootsPtrPtr[i]);
124    } 
125  } 
126
127  return (DDDMP_SUCCESS);
128}
129
130/**Function********************************************************************
131
132  Synopsis     [Reads a dump file in a CNF format.]
133
134  Description  [Reads a dump file representing the argument BDD in a
135    CNF formula.
136    ]
137
138  SideEffects  [A vector of pointers to DD nodes is allocated and freed.]
139
140  SeeAlso      [Dddmp_cuddBddArrayLoad]
141
142******************************************************************************/
143
144int
145Dddmp_cuddBddArrayLoadCnf (
146  DdManager *ddMgr                 /* IN: DD Manager */,
147  Dddmp_RootMatchType rootmatchmode/* IN: storing mode selector */,
148  char **rootmatchnames            /* IN: sorted names for loaded roots */,
149  Dddmp_VarMatchType varmatchmode  /* IN: storing mode selector */,
150  char **varmatchnames             /* IN: array of variable names, by IDs */,
151  int *varmatchauxids              /* IN: array of variable auxids, by IDs */,
152  int *varcomposeids               /* IN: array of new ids, by IDs */,
153  int mode                         /* IN: computation Mode */,
154  char *file                       /* IN: file name */,
155  FILE *fp                         /* IN: file pointer */,
156  DdNode ***rootsPtrPtr            /* OUT: array of returned BDD roots */,
157  int *nRoots                      /* OUT: number of BDDs returned */
158  )
159{
160  int retValue;
161
162#ifdef DDDMP_DEBUG
163#ifndef __alpha__ 
164  int retValueBis;
165
166  retValueBis = Cudd_DebugCheck (ddMgr);
167  if (retValueBis == 1) {
168    fprintf (stderr, "Inconsistency Found During CNF Load.\n");
169    fflush (stderr);
170  } else {
171    if (retValueBis == CUDD_OUT_OF_MEM) {
172      fprintf (stderr, "Out of Memory During CNF Load.\n");
173      fflush (stderr);
174    }
175  }
176#endif
177#endif
178
179  retValue = DddmpCuddDdArrayLoadCnf (ddMgr, rootmatchmode,
180    rootmatchnames, varmatchmode, varmatchnames, varmatchauxids,
181    varcomposeids, mode, file, fp, rootsPtrPtr, nRoots);
182
183#ifdef DDDMP_DEBUG
184#ifndef __alpha__ 
185  retValueBis = Cudd_DebugCheck (ddMgr);
186  if (retValueBis == 1) {
187    fprintf (stderr, "Inconsistency Found During CNF Load.\n");
188    fflush (stderr);
189  } else {
190    if (retValueBis == CUDD_OUT_OF_MEM) {
191      fprintf (stderr, "Out of Memory During CNF Load.\n");
192      fflush (stderr);
193    }
194  }
195#endif
196#endif
197
198  return (retValue);
199}
200
201/**Function********************************************************************
202
203  Synopsis    [Reads the header of a dump file representing the argument BDDs]
204
205  Description [Reads the header of a dump file representing the argument BDDs.
206    Returns main information regarding DD type stored in the file,
207    the variable ordering used, the number of variables, etc.
208    It reads only the header of the file NOT the BDD/ADD section.
209    ]
210
211  SideEffects []
212
213  SeeAlso     [Dddmp_cuddBddArrayLoad]
214
215******************************************************************************/
216
217int
218Dddmp_cuddHeaderLoadCnf (
219  int *nVars                /* OUT: number of DD variables */,
220  int *nsuppvars            /* OUT: number of support variables */,
221  char ***suppVarNames      /* OUT: array of support variable names */,
222  char ***orderedVarNames   /* OUT: array of variable names */,
223  int **varIds              /* OUT: array of variable ids */,
224  int **varComposeIds       /* OUT: array of permids ids */,
225  int **varAuxIds           /* OUT: array of variable aux ids */,
226  int *nRoots               /* OUT: number of root in the file */,
227  char *file                 /* IN: file name */,
228  FILE *fp                   /* IN: file pointer */
229  )
230{
231  Dddmp_Hdr_t *Hdr;
232  int i, fileToClose;
233  char **tmpOrderedVarNames = NULL;
234  char **tmpSuppVarNames = NULL;
235  int *tmpVarIds = NULL;
236  int *tmpVarComposeIds = NULL;
237  int *tmpVarAuxIds = NULL; 
238
239  fileToClose = 0;
240  if (fp == NULL) {
241    fp = fopen (file, "r");
242    Dddmp_CheckAndGotoLabel (fp==NULL, "Error opening file.",
243      failure);
244    fileToClose = 1;
245  }
246
247  Hdr = DddmpBddReadHeaderCnf (NULL, fp);
248
249  Dddmp_CheckAndGotoLabel (Hdr->nnodes==0, "Zero number of nodes.",
250    failure);
251
252  /*
253   *  Number of variables (tot and support)
254   */
255
256  *nVars = Hdr->nVars;
257  *nsuppvars = Hdr->nsuppvars;
258
259  /*
260   *  Support Varnames
261   */
262
263  if (Hdr->suppVarNames != NULL) {
264    tmpSuppVarNames = DDDMP_ALLOC (char *, *nsuppvars);
265    Dddmp_CheckAndGotoLabel (tmpSuppVarNames==NULL, "Error allocating memory.",
266      failure);
267
268    for (i=0; i<*nsuppvars; i++) {
269      tmpSuppVarNames[i] = DDDMP_ALLOC (char,
270        (strlen (Hdr->suppVarNames[i]) + 1));
271      Dddmp_CheckAndGotoLabel (Hdr->suppVarNames[i]==NULL,
272        "Support Variable Name Missing in File.", failure);
273      strcpy (tmpSuppVarNames[i], Hdr->suppVarNames[i]);
274    }
275
276    *suppVarNames = tmpSuppVarNames;
277  } else {
278    *suppVarNames = NULL;
279  }
280
281  /*
282   *  Ordered Varnames
283   */
284
285  if (Hdr->orderedVarNames != NULL) {
286    tmpOrderedVarNames = DDDMP_ALLOC (char *, *nVars);
287    Dddmp_CheckAndGotoLabel (tmpOrderedVarNames==NULL,
288      "Error allocating memory.", failure);
289
290    for (i=0; i<*nVars; i++) {
291      tmpOrderedVarNames[i]  = DDDMP_ALLOC (char,
292        (strlen (Hdr->orderedVarNames[i]) + 1));
293      Dddmp_CheckAndGotoLabel (Hdr->orderedVarNames[i]==NULL,
294        "Support Variable Name Missing in File.", failure);
295      strcpy (tmpOrderedVarNames[i], Hdr->orderedVarNames[i]);
296    }
297
298    *orderedVarNames = tmpOrderedVarNames;
299  } else {
300    *orderedVarNames = NULL;
301  }
302
303  /*
304   *  Variable Ids
305   */
306
307  if (Hdr->ids != NULL) {
308    tmpVarIds = DDDMP_ALLOC (int, *nsuppvars);
309    Dddmp_CheckAndGotoLabel (tmpVarIds==NULL, "Error allocating memory.",
310      failure);
311    for (i=0; i<*nsuppvars; i++) {
312      tmpVarIds[i] = Hdr->ids[i];
313    }
314
315    *varIds = tmpVarIds; 
316  } else {
317    *varIds = NULL;
318  }
319
320  /*
321   *  Variable Compose Ids
322   */
323
324  if (Hdr->permids != NULL) {
325    tmpVarComposeIds = DDDMP_ALLOC (int, *nsuppvars);
326    Dddmp_CheckAndGotoLabel (tmpVarComposeIds==NULL,
327      "Error allocating memory.", failure);
328    for (i=0; i<*nsuppvars; i++) {
329      tmpVarComposeIds[i] = Hdr->permids[i];
330    }
331
332    *varComposeIds = tmpVarComposeIds; 
333  } else {
334    *varComposeIds = NULL;
335  }
336
337  /*
338   *  Variable Auxiliary Ids
339   */
340
341  if (Hdr->auxids != NULL) {
342    tmpVarAuxIds = DDDMP_ALLOC (int, *nsuppvars);
343    Dddmp_CheckAndGotoLabel (tmpVarAuxIds==NULL,
344      "Error allocating memory.", failure);
345    for (i=0; i<*nsuppvars; i++) {
346      tmpVarAuxIds[i] = Hdr->auxids[i];
347    }
348
349    *varAuxIds = tmpVarAuxIds; 
350  } else {
351    *varAuxIds = NULL;
352  }
353
354  /*
355   *  Number of roots
356   */
357
358  *nRoots = Hdr->nRoots;
359
360  /*
361   *  Free and Return
362   */
363
364  if (fileToClose == 1) {
365    fclose (fp);
366  }
367       
368  DddmpFreeHeaderCnf (Hdr);
369
370  return (DDDMP_SUCCESS);
371
372  failure:
373    return (DDDMP_FAILURE);
374}
375
376/*---------------------------------------------------------------------------*/
377/* Definition of internal functions                                          */
378/*---------------------------------------------------------------------------*/
379
380/*---------------------------------------------------------------------------*/
381/* Definition of static functions                                            */
382/*---------------------------------------------------------------------------*/
383
384/**Function********************************************************************
385
386  Synopsis    [Reads a dump file representing the argument BDDs in CNF
387     format.
388    ]
389
390  Description [Reads a dump file representing the argument BDDs in CNF
391    format.
392      IFF mode == 0 Return the Clauses without Conjunction
393      IFF mode == 1 Return the sets of BDDs without Quantification
394      IFF mode == 2 Return the sets of BDDs AFTER Existential Quantification
395    ]
396
397  SideEffects [A vector of pointers to DD nodes is allocated and freed.]
398
399  SeeAlso     [Dddmp_cuddBddArrayLoad]
400
401******************************************************************************/
402
403static int
404DddmpCuddDdArrayLoadCnf (
405  DdManager *ddMgr                 /* IN: DD Manager */,
406  Dddmp_RootMatchType rootmatchmode/* IN: storing mode selector */,
407  char **rootmatchnames            /* IN: sorted names for loaded roots */,
408  Dddmp_VarMatchType varmatchmode  /* IN: storing mode selector */,
409  char **varmatchnames             /* IN: array of variable names, by ids */,
410  int *varmatchauxids              /* IN: array of variable auxids, by ids */,
411  int *varcomposeids               /* IN: array of new ids, by ids */,
412  int mode                         /* IN: computation mode */,
413  char *file                       /* IN: file name */,
414  FILE *fp                         /* IN: file pointer */,
415  DdNode ***rootsPtrPtr            /* OUT: array of BDD roots */,
416  int *nRoots                      /* OUT: number of BDDs returned */
417  )
418{
419  Dddmp_Hdr_t *Hdr = NULL;
420  int **cnfTable = NULL;
421  int fileToClose = 0;
422  int retValue, i;
423
424  fileToClose = 0;
425  *rootsPtrPtr = NULL;
426
427  if (fp == NULL) {
428    fp = fopen (file, "r");
429    Dddmp_CheckAndGotoLabel (fp==NULL, "Error opening file.",
430      failure);
431    fileToClose = 1;
432  }
433
434  /*--------------------------- Read the Header -----------------------------*/
435
436  Hdr = DddmpBddReadHeaderCnf (NULL, fp);
437
438  Dddmp_CheckAndGotoLabel (Hdr->nnodes==0, "Zero number of nodes.",
439    failure);
440
441  /*------------------------ Read the CNF Clauses ---------------------------*/
442
443  retValue = DddmpReadCnfClauses (Hdr, &cnfTable, fp);
444
445  Dddmp_CheckAndGotoLabel (retValue==DDDMP_FAILURE,
446    "Read CNF Clauses Failure.",  failure);
447
448  /*------------------------- From Clauses to BDDs --------------------------*/
449
450  retValue = DddmpCnfClauses2Bdd (Hdr, ddMgr, cnfTable, mode, rootsPtrPtr);
451
452  Dddmp_CheckAndGotoLabel (retValue==DDDMP_FAILURE,
453    "CNF Clauses To BDDs Failure.",  failure);
454
455  *nRoots = Hdr->nRoots;
456
457  if (fileToClose) {
458    fclose (fp);
459  }
460
461  for (i=0; i<Hdr->nClausesCnf; i++) {
462    DDDMP_FREE (cnfTable[i]);
463  }
464  DDDMP_FREE (cnfTable);
465
466  DddmpFreeHeaderCnf (Hdr);
467
468  return (DDDMP_SUCCESS);
469
470  /*
471   *  Failure Condition
472   */
473
474failure:
475
476  if (fileToClose) {
477    fclose (fp);
478  }
479
480  for (i=0; i<Hdr->nClausesCnf; i++) {
481    DDDMP_FREE (cnfTable[i]);
482  }
483  DDDMP_FREE (cnfTable);
484
485  DddmpFreeHeaderCnf (Hdr);
486
487  /* return 0 on error ! */
488  nRoots = 0;
489
490  return (DDDMP_FAILURE);
491}
492
493/**Function********************************************************************
494
495  Synopsis    [Reads a the header of a dump file representing the argument
496    BDDs.
497    ]
498
499  Description [Reads the header of a dump file. Builds a Dddmp_Hdr_t struct
500    containing all infos in the header, for next manipulations.
501    ]
502
503  SideEffects [none]
504
505  SeeAlso     []
506
507******************************************************************************/
508
509static Dddmp_Hdr_t *
510DddmpBddReadHeaderCnf (
511  char *file      /* IN: file name */,
512  FILE *fp        /* IN: file pointer */
513  )
514{
515  Dddmp_Hdr_t *Hdr = NULL;
516  char buf[DDDMP_MAXSTRLEN];
517  int nv, nc, retValue, fileToClose = 0;
518
519  if (fp == NULL) {
520    fp = fopen (file, "r");
521    Dddmp_CheckAndGotoLabel (fp==NULL, "Error opening file.",
522      failure);
523    fileToClose = 1;
524  }
525
526  /* Start Header */
527  Hdr = DDDMP_ALLOC (Dddmp_Hdr_t, 1);
528  if (Hdr == NULL) {
529    return NULL;
530  }
531
532  Hdr->ver = NULL;
533  Hdr->mode = 0;
534  Hdr->ddType = DDDMP_CNF;
535  Hdr->varinfo = DDDMP_VARIDS;
536  Hdr->dd = NULL;
537  Hdr->nnodes = 0;
538  Hdr->nVars = 0;
539  Hdr->nsuppvars = 0;
540  Hdr->orderedVarNames = NULL;
541  Hdr->suppVarNames = NULL;
542  Hdr->ids = NULL;
543  Hdr->permids = NULL;
544  Hdr->auxids = NULL;
545  Hdr->cnfids = NULL;
546  Hdr->nRoots = 0;
547  Hdr->rootids = NULL;
548  Hdr->rootnames = NULL;
549  Hdr->nAddedCnfVar = 0;
550  Hdr->nVarsCnf = 0;
551  Hdr->nClausesCnf = 0;
552
553  while (fscanf (fp, "%s", buf) != EOF) {
554
555    /* Init Problem Line */ 
556    if (buf[0] == 'p') {
557      fscanf (fp, "%*s %d %d", &nv, &nc);
558      Hdr->nVarsCnf = nv;
559      Hdr->nClausesCnf = nc;
560      break;
561    }
562
563    /* CNF Comment Line */
564    if (buf[0] == 'c') {
565      if (fscanf (fp, "%s", buf) == EOF) {
566        break;
567      }
568    }
569
570    /* Skip Comment? */
571    if (buf[0] != '.') {
572      fgets (buf, DDDMP_MAXSTRLEN, fp);
573      continue;
574    }
575
576    if (matchkeywd (buf, ".ver")) {   
577      /* this not checked so far: only read */
578      retValue = fscanf (fp, "%s", buf);
579      Dddmp_CheckAndGotoLabel (retValue==EOF, "Error reading from file.",
580        failure);
581
582      Hdr->ver=DddmpStrDup(buf);
583      Dddmp_CheckAndGotoLabel (Hdr->ver==NULL,
584        "Error allocating memory.", failure);
585
586      continue;
587    }
588
589    if (matchkeywd (buf, ".dd")) {   
590      retValue = fscanf (fp, "%s", buf);
591      Dddmp_CheckAndGotoLabel (retValue==EOF, "Error reading file.",
592        failure);
593
594      Hdr->dd = DddmpStrDup (buf);
595      Dddmp_CheckAndGotoLabel (Hdr->dd==NULL, "Error allocating memory.",
596        failure);
597
598      continue;
599    }
600
601    if (matchkeywd (buf, ".nnodes")) {
602      retValue = fscanf (fp, "%d", &(Hdr->nnodes));
603      Dddmp_CheckAndGotoLabel (retValue==EOF, "Error reading file.",
604        failure);
605
606      continue;
607    }
608
609    if (matchkeywd (buf, ".nvars")) {   
610      retValue = fscanf (fp, "%d", &(Hdr->nVars));
611      Dddmp_CheckAndGotoLabel (retValue==EOF, "Error reading file.",
612        failure);
613
614      continue;
615    }
616
617    if (matchkeywd (buf, ".nsuppvars")) {
618      retValue = fscanf (fp, "%d", &(Hdr->nsuppvars));
619      Dddmp_CheckAndGotoLabel (retValue==EOF, "Error reading file.",
620        failure);
621
622      continue;
623    }
624
625    if (matchkeywd (buf, ".orderedvarnames")) {
626      Hdr->orderedVarNames = DddmpStrArrayRead (fp, Hdr->nVars);
627      Dddmp_CheckAndGotoLabel (Hdr->orderedVarNames==NULL,
628        "Error allocating memory.", failure);
629
630      continue;
631    }
632
633    if (matchkeywd (buf, ".suppvarnames")) {
634      Hdr->suppVarNames = DddmpStrArrayRead (fp, Hdr->nsuppvars);
635      Dddmp_CheckAndGotoLabel (Hdr->suppVarNames==NULL,
636        "Error allocating memory.", failure);
637
638      continue;
639    }
640
641    if matchkeywd (buf, ".ids") {
642      Hdr->ids = DddmpIntArrayRead(fp,Hdr->nsuppvars);
643      Dddmp_CheckAndGotoLabel (Hdr->ids==NULL,
644        "Error allocating memory.", failure);
645
646      continue;
647    }
648
649    if (matchkeywd (buf, ".permids")) {
650      Hdr->permids = DddmpIntArrayRead(fp,Hdr->nsuppvars);
651      Dddmp_CheckAndGotoLabel (Hdr->permids==NULL,
652        "Error allocating memory.", failure);
653
654      continue;
655    }
656
657    if (matchkeywd (buf, ".auxids")) {
658      Hdr->auxids = DddmpIntArrayRead(fp,Hdr->nsuppvars);
659      Dddmp_CheckAndGotoLabel (Hdr->auxids==NULL,
660        "Error allocating memory.", failure);
661
662      continue;
663    }
664
665    if (matchkeywd (buf, ".cnfids")) {
666      Hdr->cnfids = DddmpIntArrayRead (fp, Hdr->nsuppvars);
667      Dddmp_CheckAndGotoLabel (Hdr->cnfids==NULL,
668        "Error allocating memory.", failure);
669
670      continue;
671    }
672
673    if (matchkeywd (buf, ".nroots")) {
674      retValue = fscanf (fp, "%d", &(Hdr->nRoots));
675      Dddmp_CheckAndGotoLabel (retValue==EOF, "Error reading file.",
676        failure);
677
678      continue;
679    }
680
681    if (matchkeywd (buf, ".rootids")) {
682      Hdr->rootids = DddmpIntArrayRead(fp,Hdr->nRoots);
683      Dddmp_CheckAndGotoLabel (Hdr->rootids==NULL,
684        "Error allocating memory.", failure);
685
686      continue;
687    }
688
689    if (matchkeywd (buf, ".rootnames")) {
690      Hdr->rootnames = DddmpStrArrayRead(fp,Hdr->nRoots);
691      Dddmp_CheckAndGotoLabel (Hdr->rootnames==NULL,
692        "Error allocating memory.", failure);
693
694      continue;
695    }
696
697
698    if (matchkeywd (buf, ".nAddedCnfVar")) {
699      retValue = fscanf (fp, "%d", &(Hdr->nAddedCnfVar));
700      Dddmp_CheckAndGotoLabel (retValue==EOF, "Error reading file.",
701        failure);
702
703      continue;
704    }
705  }
706
707  /* END HEADER */
708  return (Hdr);
709
710failure:
711
712  if (fileToClose == 1) {
713    fclose (fp);
714  }
715
716  DddmpFreeHeaderCnf (Hdr);
717
718  return (NULL);
719}
720
721
722/**Function********************************************************************
723
724  Synopsis    [Frees the internal header structure.]
725
726  Description [Frees the internal header structure by freeing all internal
727    fields first.
728    ]
729
730  SideEffects []
731
732  SeeAlso     []
733
734******************************************************************************/
735
736static void
737DddmpFreeHeaderCnf (
738  Dddmp_Hdr_t *Hdr   /* IN: pointer to header */
739  )
740{
741  if (Hdr==NULL) {
742    return;
743  }
744
745  DDDMP_FREE (Hdr->ver);
746  DDDMP_FREE (Hdr->dd);
747  DddmpStrArrayFree (Hdr->orderedVarNames, Hdr->nVars);
748  DddmpStrArrayFree (Hdr->suppVarNames, Hdr->nsuppvars);
749  DDDMP_FREE (Hdr->ids);
750  DDDMP_FREE (Hdr->permids);
751  DDDMP_FREE (Hdr->auxids);
752  DDDMP_FREE (Hdr->cnfids);
753  DDDMP_FREE (Hdr->rootids);
754  DddmpStrArrayFree (Hdr->rootnames, Hdr->nRoots);
755
756  DDDMP_FREE (Hdr);
757
758  return;
759}
760
761/**Function********************************************************************
762
763  Synopsis    [Read the CNF clauses from the file in the standard DIMACS
764    format.
765    ]
766
767  Description [Read the CNF clauses from the file in the standard DIMACS
768    format. Store all the clauses in an internal structure for
769    future transformation into BDDs.
770    ]
771
772  SideEffects []
773
774  SeeAlso     []
775
776******************************************************************************/
777
778static int
779DddmpReadCnfClauses (
780  Dddmp_Hdr_t *Hdr  /*  IN: file header */,
781  int ***cnfTable   /* OUT: CNF table for clauses */,
782  FILE *fp          /*  IN: source file */
783  )
784{
785  char word[DDDMP_MAX_CNF_ROW_LENGTH];
786  int i, j, var;
787  int **cnfTableLocal = NULL;
788  int *clause = NULL;
789
790  cnfTableLocal = DDDMP_ALLOC (int *, Hdr->nClausesCnf);
791  clause = DDDMP_ALLOC (int, 2*Hdr->nVarsCnf+1);
792
793  for (i=0; i<Hdr->nClausesCnf; i++) {
794    cnfTableLocal[i] = NULL;
795  }
796
797  for (i=0; i<=2*Hdr->nVarsCnf; i++) {
798    clause[i] = 0;
799  }
800
801  i = j = 0;
802  do { 
803    if (fscanf(fp, "%s", word)==EOF) {
804      if (j>0) {
805        /* force last zero */
806        strcpy(word,"0");
807      }
808      else break;
809    }
810
811    /* Check for Comment */
812    if (word[0] == 'c') {
813      /* Comment Found: Skip line */
814      fgets (word, DDDMP_MAX_CNF_ROW_LENGTH-1, fp);
815      break;
816    }
817
818    var = atoi (word);
819    Dddmp_Assert ((var>=(-Hdr->nVarsCnf))&&(var<=Hdr->nVarsCnf),
820      "Wrong num found");
821    clause[j++] = var;
822    if (var == 0) {
823      cnfTableLocal[i] = DDDMP_ALLOC (int, j);
824      while (--j >=0) {
825        cnfTableLocal[i][j] = clause[j];
826        }
827      i++;
828      j=0;
829    }
830
831  } while (!feof(fp));
832
833  Dddmp_Assert (i==Hdr->nClausesCnf,
834    "Wrong number of clauses in file");
835
836#if DDDMP_DEBUG_CNF
837  for (i=0; i<Hdr->nClausesCnf; i++) {
838    fprintf (stdout, "[%4d] ", i);
839    j=0;
840    while ((var = cnfTableLocal[i][j++]) != 0) {
841      fprintf (stdout, "%d ", var);
842    } 
843    fprintf (stdout, "0\n");
844  }
845#endif
846
847  DDDMP_FREE (clause);
848
849  *cnfTable = cnfTableLocal;
850
851  return (DDDMP_SUCCESS);
852}
853
854/**Function********************************************************************
855
856  Synopsis    [Transforms CNF clauses into BDDs.]
857
858  Description [Transforms CNF clauses into BDDs. Clauses are stored in an
859   internal structure previously read. The results can be given in
860   different format according to the mode selection:
861     IFF mode == 0 Return the Clauses without Conjunction
862     IFF mode == 1 Return the sets of BDDs without Quantification
863     IFF mode == 2 Return the sets of BDDs AFTER Existential Quantification
864   ]
865
866  SideEffects []
867
868  SeeAlso     []
869
870******************************************************************************/
871
872static int
873DddmpCnfClauses2Bdd (
874  Dddmp_Hdr_t *Hdr       /* IN: file header */,
875  DdManager *ddMgr       /* IN: DD Manager */,
876  int **cnfTable         /* IN: CNF table for clauses */,
877  int mode               /* IN: computation mode */,
878  DdNode ***rootsPtrPtr  /* OUT: array of returned BDD roots (by reference) */
879  )
880{
881  DdNode **rel = NULL;
882  DdNode *lit = NULL;
883  DdNode *tmp1 = NULL;
884  DdNode *tmp2 = NULL;
885  DdNode **rootsPtr = NULL;
886  DdNode *cubeAllVar = NULL;
887  DdNode *cubeBddVar = NULL;
888  DdNode *cubeCnfVar = NULL;
889  int i, j, k, n, var1, var2, fromLine, toLine;
890
891  rootsPtr = NULL;
892  *rootsPtrPtr = NULL;
893
894  /*-------------------------- Read The Clauses -----------------------------*/
895
896  rel = DDDMP_ALLOC (DdNode *, Hdr->nClausesCnf);
897
898  cubeBddVar = Cudd_ReadOne (ddMgr);
899  cubeCnfVar = Cudd_ReadOne (ddMgr);
900  cubeAllVar = Cudd_ReadOne (ddMgr);
901  Cudd_Ref (cubeBddVar);
902  Cudd_Ref (cubeCnfVar);
903  Cudd_Ref (cubeAllVar);
904
905  for (i=0; i<Hdr->nClausesCnf; i++) {
906    rel[i] = Cudd_Not (Cudd_ReadOne (ddMgr));
907    Cudd_Ref (rel[i]);
908    j=0;
909    while ((var1 = cnfTable[i][j++]) != 0) {
910
911      /* Deal with the Literal */
912      var2 = abs (var1);
913      n = (-1);
914      for (k=0; k<Hdr->nsuppvars; k++) {
915        if (Hdr->cnfids[k] == var2) {
916          n = k;
917          break;
918        }
919      }
920
921      if (n == (-1)) {
922        lit = Cudd_bddIthVar (ddMgr, var2);
923
924        /* Create the cubes of CNF Variables */
925        tmp1 = Cudd_bddAnd (ddMgr, cubeCnfVar, lit);
926        Cudd_Ref (tmp1);
927        Cudd_RecursiveDeref (ddMgr, cubeCnfVar);
928        cubeCnfVar = tmp1;
929
930      } else {
931        lit = Cudd_bddIthVar (ddMgr, Hdr->ids[n]);
932
933        /* Create the cubes of BDD Variables */
934        tmp1 = Cudd_bddAnd (ddMgr, cubeBddVar, lit);
935        Cudd_Ref (tmp1);
936        Cudd_RecursiveDeref (ddMgr, cubeBddVar);
937        cubeBddVar = tmp1;
938      }
939
940      /* Create the cubes of ALL Variables */
941      tmp1 = Cudd_bddAnd (ddMgr, cubeAllVar, lit);
942      Cudd_Ref (tmp1);
943      Cudd_RecursiveDeref (ddMgr, cubeAllVar);
944      cubeAllVar = tmp1;
945
946      /* Deal with Relations */
947      if (var1<0) {
948        lit = Cudd_Not (lit);
949      }
950      tmp1 = Cudd_bddOr (ddMgr, rel[i], lit);
951      Cudd_Ref (tmp1);
952      Cudd_RecursiveDeref (ddMgr, rel[i]);
953      rel[i] = tmp1;
954    }
955  }
956
957  /*
958   *  Mode == 0 Return the Clauses without Conjunction
959   */
960
961  if (mode == 0) {
962    return (DDDMP_SUCCESS);
963  }
964
965  rootsPtr = DDDMP_ALLOC (DdNode *, Hdr->nRoots);
966  Dddmp_CheckAndGotoLabel (rootsPtr==NULL, "Error allocating memory.",
967    failure);
968
969  for (i=0; i<Hdr->nRoots; i++) {
970    if (i == (Hdr->nRoots-1)) {
971      fromLine = Hdr->rootids[i] - 1;
972      toLine = Hdr->nClausesCnf;
973    } else {
974      fromLine = Hdr->rootids[i] - 1;
975      toLine = Hdr->rootids[i+1];
976    }
977
978    tmp1 = Cudd_ReadOne (ddMgr);
979    Cudd_Ref (tmp1); 
980    for (j=fromLine; j<toLine; j++) {
981      tmp2 = Cudd_bddAnd (ddMgr, rel[j], tmp1);
982      Cudd_Ref (tmp2);
983      Cudd_RecursiveDeref (ddMgr, tmp1);
984      Cudd_RecursiveDeref (ddMgr, rel[j]);
985      tmp1 = tmp2;
986    }
987    rootsPtr[i] = tmp1;
988  }
989
990  DDDMP_FREE (rel);
991
992  /*
993   *  Mode == 1 Return the sets of BDDs without Quantification
994   */
995
996  if (mode == 1) {
997    *rootsPtrPtr = rootsPtr;
998    return (DDDMP_SUCCESS);
999  }
1000
1001  /*
1002   *  Mode == 2 Return the sets of BDDs AFTER Existential Quantification
1003   */
1004
1005#if DDDMP_DEBUG_CNF
1006  cubeBddVar = Cudd_ReadOne (ddMgr);
1007  Cudd_Ref (cubeBddVar);
1008  for (i=0; i<Hdr->nsuppvars; i++) {
1009    lit = Cudd_bddIthVar (ddMgr, Hdr->ids[i]);
1010    tmp1 = Cudd_bddAnd (ddMgr, cubeBddVar, lit);
1011    Cudd_Ref (tmp1);
1012    Cudd_RecursiveDeref (ddMgr, cubeBddVar);
1013    cubeBddVar = tmp1;
1014  }
1015
1016  cubeCnfVar = Cudd_bddExistAbstract (ddMgr, cubeAllVar, cubeBddVar);
1017#endif
1018
1019  for (i=0; i<Hdr->nRoots; i++) {
1020#if DDDMP_DEBUG_CNF
1021    fprintf (stdout, "rootsPtr Before Exist:\n");
1022    Cudd_PrintDebug (ddMgr, rootsPtr[i], 0, 3);
1023#endif
1024
1025    tmp1 = Cudd_bddExistAbstract (ddMgr, rootsPtr[i], cubeCnfVar);
1026    Cudd_RecursiveDeref (ddMgr, rootsPtr[i]);
1027    rootsPtr[i] = tmp1;
1028
1029#if DDDMP_DEBUG_CNF
1030    fprintf (stdout, "rootsPtr After Exist:\n");
1031    Cudd_PrintDebug (ddMgr, rootsPtr[i], 0, 3);
1032#endif
1033  }
1034
1035#if DDDMP_DEBUG_CNF
1036  fprintf (stdout, "cubeAllVar:\n");
1037  Cudd_PrintDebug (ddMgr, cubeAllVar, 0, 3);
1038  fprintf (stdout, "cubeBddVar:\n");
1039  Cudd_PrintDebug (ddMgr, cubeBddVar, 0, 3);
1040  fprintf (stdout, "cubeCnfVar:\n");
1041  Cudd_PrintDebug (ddMgr, cubeCnfVar, 0, 3);
1042#endif
1043   
1044  Cudd_RecursiveDeref (ddMgr, cubeAllVar);
1045  Cudd_RecursiveDeref (ddMgr, cubeBddVar);
1046  Cudd_RecursiveDeref (ddMgr, cubeCnfVar);
1047  *rootsPtrPtr = rootsPtr;
1048
1049  return (DDDMP_SUCCESS);
1050
1051  /*
1052   *  Failure Condition
1053   */
1054
1055failure:
1056
1057  DDDMP_FREE (rel);
1058  DDDMP_FREE (rootsPtrPtr);
1059
1060  return (DDDMP_FAILURE);
1061}
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
Note: See TracBrowser for help on using the repository browser.