distr/dddmp/dddmpLoadCnf.c

   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
  62 static 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);
  63 static Dddmp_Hdr_t * DddmpBddReadHeaderCnf(char *file, FILE *fp);
  64 static void DddmpFreeHeaderCnf(Dddmp_Hdr_t *Hdr);
  65 static int DddmpReadCnfClauses(Dddmp_Hdr_t *Hdr, int ***cnfTable, FILE *fp);
  66 static 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
  94 int
  95 Dddmp_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
 144 int
 145 Dddmp_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
 217 int
 218 Dddmp_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
 403 static int
 404 DddmpCuddDdArrayLoadCnf (
 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
 474 failure:
 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
 509 static Dddmp_Hdr_t *
 510 DddmpBddReadHeaderCnf (
 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
 710 failure:
 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
 736 static void
 737 DddmpFreeHeaderCnf (
 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
 778 static int
 779 DddmpReadCnfClauses (
 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
 872 static int
 873 DddmpCnfClauses2Bdd (
 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
1055 failure:
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