distr/dddmp/dddmpStoreCnf.c

   1 /**CFile**********************************************************************
   2
   3   FileName     [dddmpStoreCnf.c]
   4
   5   PackageName  [dddmp]
   6
   7   Synopsis     [Functions to write out BDDs to file in a CNF format]
   8
   9   Description  [Functions to write out BDDs to file in a CNF format.]
  10
  11   Author       [Gianpiero Cabodi and Stefano Quer]
  12
  13   Copyright    [
  14     Copyright (c) 2004 by Politecnico di Torino.
  15     All Rights Reserved. This software is for educational purposes only.
  16     Permission is given to academic institutions to use, copy, and modify
  17     this software and its documentation provided that this introductory
  18     message is not removed, that this software and its documentation is
  19     used for the institutions' internal research and educational purposes,
  20     and that no monies are exchanged. No guarantee is expressed or implied
  21     by the distribution of this code.
  22     Send bug-reports and/or questions to:
  23     {gianpiero.cabodi,stefano.quer}@polito.it.
  24     ]
  25
  26 ******************************************************************************/
  27
  28 #include <limits.h>
  29 #include "dddmpInt.h"
  30
  31 /*-------------------------------1--------------------------------------------*/
  32 /* Stucture declarations                                                     */
  33 /*---------------------------------------------------------------------------*/
  34
  35 /*---------------------------------------------------------------------------*/
  36 /* Type declarations                                                         */
  37 /*---------------------------------------------------------------------------*/
  38
  39 /*---------------------------------------------------------------------------*/
  40 /* Variable declarations                                                     */
  41 /*---------------------------------------------------------------------------*/
  42
  43 #define DDDMP_DEBUG_CNF   0
  44
  45 /*---------------------------------------------------------------------------*/
  46 /* Macro declarations                                                        */
  47 /*---------------------------------------------------------------------------*/
  48
  49 #define GET_MAX(x,y) (x>y?x:y)
  50
  51 /**AutomaticStart*************************************************************/
  52
  53 /*---------------------------------------------------------------------------*/
  54 /* Static function prototypes                                                */
  55 /*---------------------------------------------------------------------------*/
  56
  57 static int DddmpCuddBddArrayStoreCnf(DdManager *ddMgr, DdNode **f, int rootN, Dddmp_DecompCnfStoreType mode, int noHeader, char **varNames, int *bddIds, int *bddAuxIds, int *cnfIds, int idInitial, int edgeInTh, int pathLengthTh, char *fname, FILE *fp, int *clauseNPtr, int *varNewNPtr);
  58 static int StoreCnfNodeByNode(DdManager *ddMgr, DdNode **f, int rootN, int *bddIds, int *cnfIds, FILE *fp, int *clauseN, int *varMax, int *rootStartLine);
  59 static int StoreCnfNodeByNodeRecur(DdManager *ddMgr, DdNode *f, int *bddIds, int *cnfIds, FILE *fp, int *clauseN, int *varMax);
  60 static int StoreCnfOneNode(DdNode *f, int idf, int vf, int idT, int idE, FILE *fp, int *clauseN, int *varMax);
  61 static int StoreCnfMaxtermByMaxterm(DdManager *ddMgr, DdNode **f, int rootN, int *bddIds, int *cnfIds, int idInitial, FILE *fp, int *varMax, int *clauseN, int *rootStartLine);
  62 static int StoreCnfBest(DdManager *ddMgr, DdNode **f, int rootN, int *bddIds, int *cnfIds, int idInitial, FILE *fp, int *varMax, int *clauseN, int *rootStartLine);
  63 static void StoreCnfMaxtermByMaxtermRecur(DdManager *ddMgr, DdNode *node, int *bddIds, int *cnfIds, FILE *fp, int *list, int *clauseN, int *varMax);
  64 static int StoreCnfBestNotSharedRecur(DdManager *ddMgr, DdNode *node, int idf, int *bddIds, int *cnfIds, FILE *fp, int *list, int *clauseN, int *varMax);
  65 static int StoreCnfBestSharedRecur(DdManager *ddMgr, DdNode *node, int *bddIds, int *cnfIds, FILE *fp, int *list, int *clauseN, int *varMax);
  66 static int printCubeCnf(DdManager *ddMgr, DdNode *node, int *cnfIds, FILE *fp, int *list, int *varMax);
  67
  68 /**AutomaticEnd***************************************************************/
  69
  70 /*---------------------------------------------------------------------------*/
  71 /* Definition of exported functions                                          */
  72 /*---------------------------------------------------------------------------*/
  73
  74 /**Function********************************************************************
  75
  76   Synopsis     [Writes a dump file representing the argument BDD in
  77     a CNF format.
  78     ]
  79
  80   Description  [Dumps the argument BDD to file.
  81     This task is performed by calling the function
  82     Dddmp_cuddBddArrayStoreCnf.
  83     ]
  84
  85   SideEffects  [Nodes are temporarily removed from unique hash. They are
  86     re-linked after the store operation in a modified order.
  87     ]
  88
  89   SeeAlso      [Dddmp_cuddBddArrayStoreCnf]
  90
  91 ******************************************************************************/
  92
  93 int
  94 Dddmp_cuddBddStoreCnf (
  95   DdManager *ddMgr              /* IN: DD Manager */,
  96   DdNode *f                     /* IN: BDD root to be stored */,
  97   Dddmp_DecompCnfStoreType mode /* IN: format selection */,
  98   int noHeader                  /* IN: do not store header iff 1 */,
  99   char **varNames               /* IN: array of variable names (or NULL) */,
 100   int *bddIds                   /* IN: array of var ids */,
 101   int *bddAuxIds                /* IN: array of BDD node Auxiliary Ids */,
 102   int *cnfIds                   /* IN: array of CNF var ids */,
 103   int idInitial                 /* IN: starting id for cutting variables */,
 104   int edgeInTh                  /* IN: Max # Incoming Edges */,
 105   int pathLengthTh              /* IN: Max Path Length */,
 106   char *fname                   /* IN: file name */,
 107   FILE *fp                      /* IN: pointer to the store file */,
 108   int *clauseNPtr               /* OUT: number of clause stored */,
 109   int *varNewNPtr               /* OUT: number of new variable created */
 110   )
 111 {
 112   int retValue;
 113   DdNode *tmpArray[1];
 114
 115   tmpArray[0] = f;
 116
 117   retValue = Dddmp_cuddBddArrayStoreCnf (ddMgr, tmpArray, 1, mode,
 118     noHeader, varNames, bddIds, bddAuxIds, cnfIds, idInitial, edgeInTh,
 119     pathLengthTh, fname, fp, clauseNPtr, varNewNPtr);
 120
 121   Dddmp_CheckAndReturn (retValue==DDDMP_FAILURE, "Failure.");
 122
 123   return (DDDMP_SUCCESS);
 124 }
 125
 126 /**Function********************************************************************
 127
 128   Synopsis     [Writes a dump file representing the argument array of BDDs
 129     in CNF format.
 130     ]
 131
 132   Description  [Dumps the argument array of BDDs to file.]
 133
 134   SideEffects  [Nodes are temporarily removed from the unique hash
 135     table. They are re-linked after the store operation in a
 136     modified order.
 137     Three methods are allowed:
 138     * NodeByNode method: Insert a cut-point for each BDD node (but the
 139                          terminal nodes)
 140     * MaxtermByMaxterm method: Insert no cut-points, i.e. the off-set of
 141                                trhe function is stored
 142     * Best method: Tradeoff between the previous two methods.
 143       Auxiliary variables, i.e., cut points are inserted following these
 144       criterias:
 145       * edgeInTh
 146         indicates the maximum number of incoming edges up to which
 147         no cut point (auxiliary variable) is inserted.
 148         If edgeInTh:
 149         * is equal to -1 no cut point due to incoming edges are inserted
 150           (MaxtermByMaxterm method.)
 151         * is equal to 0 a cut point is inserted for each node with a single
 152           incoming edge, i.e., each node, (NodeByNode method).
 153         * is equal to n a cut point is inserted for each node with (n+1)
 154           incoming edges.
 155       * pathLengthTh
 156         indicates the maximum length path up to which no cut points
 157         (auxiliary variable) is inserted.
 158         If the path length between two nodes exceeds this value, a cut point
 159         is inserted.
 160         If pathLengthTh:
 161         * is equal to -1 no cut point due path length are inserted
 162           (MaxtermByMaxterm method.)
 163         * is equal to 0 a cut point is inserted for each node (NodeByNode
 164           method).
 165         * is equal to n a cut point is inserted on path whose length is
 166           equal to (n+1).
 167         Notice that the maximum number of literals in a clause is equal
 168         to (pathLengthTh + 2), i.e., for each path we have to keep into
 169         account a CNF variable for each node plus 2 added variables for
 170         the bottom and top-path cut points.
 171     The stored file can contain a file header or not depending on the
 172     noHeader parameter (IFF 0, usual setting, the header is usually stored.
 173     This option can be useful in storing multiple BDDs, as separate BDDs,
 174     on the same file leaving the opening of the file to the caller.
 175     ]
 176
 177   SeeAlso      []
 178
 179 ******************************************************************************/
 180
 181 int
 182 Dddmp_cuddBddArrayStoreCnf (
 183   DdManager *ddMgr              /* IN: DD Manager */,
 184   DdNode **f                    /* IN: array of BDD roots to be stored */,
 185   int rootN                     /* IN: # output BDD roots to be stored */,
 186   Dddmp_DecompCnfStoreType mode /* IN: format selection */,
 187   int noHeader                  /* IN: do not store header iff 1 */,
 188   char **varNames               /* IN: array of variable names (or NULL) */,
 189   int *bddIds                   /* IN: array of converted var IDs */,
 190   int *bddAuxIds                /* IN: array of BDD node Auxiliary Ids */,
 191   int *cnfIds                   /* IN: array of converted var IDs */,
 192   int idInitial                 /* IN: starting id for cutting variables */,
 193   int edgeInTh                  /* IN: Max # Incoming Edges */,
 194   int pathLengthTh              /* IN: Max Path Length */,
 195   char *fname                   /* IN: file name */,
 196   FILE *fp                      /* IN: pointer to the store file */,
 197   int *clauseNPtr               /* OUT: number of clause stored */,
 198   int *varNewNPtr               /* OUT: number of new variable created */
 199   )
 200 {
 201   int retValue2;
 202
 203 #if 0
 204 #ifdef DDDMP_DEBUG
 205 #ifndef __alpha__
 206   int retValue1;
 207
 208   retValue1 = Cudd_DebugCheck (ddMgr);
 209   Dddmp_CheckAndReturn (retValue1==1,
 210     "Inconsistency Found During CNF Store.");
 211   Dddmp_CheckAndReturn (retValue1==CUDD_OUT_OF_MEM,
 212     "Out of Memory During CNF Store.");
 213 #endif
 214 #endif
 215 #endif
 216
 217   retValue2 = DddmpCuddBddArrayStoreCnf (ddMgr, f, rootN, mode, noHeader,
 218     varNames, bddIds, bddAuxIds, cnfIds, idInitial, edgeInTh, pathLengthTh,
 219     fname, fp, clauseNPtr, varNewNPtr);
 220
 221 #if 0
 222 #ifdef DDDMP_DEBUG
 223 #ifndef __alpha__
 224   retValue1 = Cudd_DebugCheck (ddMgr);
 225   Dddmp_CheckAndReturn (retValue1==1,
 226     "Inconsistency Found During CNF Store.");
 227   Dddmp_CheckAndReturn (retValue1==CUDD_OUT_OF_MEM,
 228     "Out of Memory During CNF Store.");
 229 #endif
 230 #endif
 231 #endif
 232
 233   return (retValue2);
 234 }
 235
 236 /*---------------------------------------------------------------------------*/
 237 /* Definition of internal functions                                          */
 238 /*---------------------------------------------------------------------------*/
 239
 240 /**Function********************************************************************
 241
 242   Synopsis     [Writes a dump file representing the argument Array of
 243     BDDs in the CNF standard format.
 244     ]
 245
 246   Description  [Dumps the argument array of BDDs/ADDs to file in CNF format.
 247     The following arrays: varNames, bddIds, bddAuxIds, and cnfIds
 248     fix the correspondence among variable names, BDD ids, BDD
 249     auxiliary ids and the ids used to store the CNF problem.
 250     All these arrays are automatically created iff NULL.
 251     Auxiliary variable, iff necessary, are created starting from value
 252     idInitial.
 253     Iff idInitial is <= 0 its value is selected as the number of internal
 254     CUDD variable + 2.
 255     Auxiliary variables, i.e., cut points are inserted following these
 256     criterias:
 257     * edgeInTh
 258       indicates the maximum number of incoming edges up to which
 259       no cut point (auxiliary variable) is inserted.
 260       If edgeInTh:
 261       * is equal to -1 no cut point due to incoming edges are inserted
 262         (MaxtermByMaxterm method.)
 263         * is equal to 0 a cut point is inserted for each node with a single
 264         incoming edge, i.e., each node, (NodeByNode method).
 265         * is equal to n a cut point is inserted for each node with (n+1)
 266         incoming edges.
 267     * pathLengthTh
 268       indicates the maximum length path up to which no cut points
 269       (auxiliary variable) is inserted.
 270       If the path length between two nodes exceeds this value, a cut point
 271       is inserted.
 272       If pathLengthTh:
 273       * is equal to -1 no cut point due path length are inserted
 274         (MaxtermByMaxterm method.)
 275         * is equal to 0 a cut point is inserted for each node (NodeByNode
 276         method).
 277         * is equal to n a cut point is inserted on path whose length is
 278         equal to (n+1).
 279       Notice that the maximum number of literals in a clause is equal
 280       to (pathLengthTh + 2), i.e., for each path we have to keep into
 281       account a CNF variable for each node plus 2 added variables for
 282       the bottom and top-path cut points.
 283     ]
 284
 285   SideEffects  [Nodes are temporarily removed from the unique hash table.
 286     They are re-linked after the store operation in a modified
 287     order.
 288     ]
 289
 290   SeeAlso      [Dddmp_cuddBddStore]
 291
 292 ******************************************************************************/
 293
 294 static int
 295 DddmpCuddBddArrayStoreCnf (
 296   DdManager *ddMgr               /* IN: DD Manager */,
 297   DdNode **f                     /* IN: array of BDD roots to be stored */,
 298   int rootN                      /* IN: # of output BDD roots to be stored */,
 299   Dddmp_DecompCnfStoreType mode  /* IN: format selection */,
 300   int noHeader                   /* IN: do not store header iff 1 */,
 301   char **varNames                /* IN: array of variable names (or NULL) */,
 302   int *bddIds                    /* IN: array of BDD node Ids (or NULL) */,
 303   int *bddAuxIds                 /* IN: array of BDD Aux Ids (or NULL) */,
 304   int *cnfIds                    /* IN: array of CNF ids (or NULL) */,
 305   int idInitial                  /* IN: starting id for cutting variables */,
 306   int edgeInTh                   /* IN: Max # Incoming Edges */,
 307   int pathLengthTh               /* IN: Max Path Length */,
 308   char *fname                    /* IN: file name */,
 309   FILE *fp                       /* IN: pointer to the store file */,
 310   int *clauseNPtr                /* OUT: number of clause stored */,
 311   int *varNewNPtr                /* OUT: number of new variable created */
 312   )
 313 {
 314   DdNode *support = NULL;
 315   DdNode *scan = NULL;
 316   int *bddIdsInSupport = NULL;
 317   int *permIdsInSupport = NULL;
 318   int *rootStartLine = NULL;
 319   int nVar, nVarInSupport, retValue, i, j, fileToClose;
 320   int varMax, clauseN, flagVar, intStringLength;
 321   int bddIdsToFree = 0;
 322   int bddAuxIdsToFree = 0;
 323   int cnfIdsToFree = 0;
 324   int varNamesToFree = 0;
 325   char intString[DDDMP_MAXSTRLEN];
 326   char tmpString[DDDMP_MAXSTRLEN];
 327   fpos_t posFile1, posFile2;
 328
 329   /*---------------------------- Set Initial Values -------------------------*/
 330
 331   support = scan = NULL;
 332   bddIdsInSupport = permIdsInSupport = rootStartLine = NULL;
 333   nVar = ddMgr->size;
 334   fileToClose = 0;
 335   sprintf (intString, "%d", INT_MAX);
 336   intStringLength = strlen (intString);
 337
 338   /*---------- Check if File needs to be opened in the proper mode ----------*/
 339
 340   if (fp == NULL) {
 341     fp = fopen (fname, "w");
 342     Dddmp_CheckAndGotoLabel (fp==NULL, "Error opening file.",
 343       failure);
 344     fileToClose = 1;
 345   }
 346
 347   /*--------- Generate Bdd LOCAL IDs and Perm IDs and count them ------------*/
 348
 349   /* BDD Ids */
 350   bddIdsInSupport = DDDMP_ALLOC (int, nVar);
 351   Dddmp_CheckAndGotoLabel (bddIdsInSupport==NULL, "Error allocating memory.",
 352     failure);
 353   /* BDD PermIds */
 354   permIdsInSupport = DDDMP_ALLOC (int, nVar);
 355   Dddmp_CheckAndGotoLabel (permIdsInSupport==NULL, "Error allocating memory.",
 356     failure);
 357   /* Support Size (Number of BDD Ids-PermIds */
 358   nVarInSupport = 0;
 359
 360   for (i=0; i<nVar; i++) {
 361     bddIdsInSupport[i] = permIdsInSupport[i] = (-1);
 362   }
 363
 364   /*
 365    *  Take the union of the supports of each output function.
 366    *  Skip NULL functions.
 367    */
 368
 369
 370   for (i=0; i<rootN; i++) {
 371     if (f[i] == NULL) {
 372       continue;
 373     }
 374     support = Cudd_Support (ddMgr, f[i]);
 375     Dddmp_CheckAndGotoLabel (support==NULL, "NULL support returned.",
 376       failure);
 377     cuddRef (support);
 378     scan = support;
 379     while (!cuddIsConstant(scan)) {
 380       /* Count Number of Variable in the Support */
 381       nVarInSupport++;
 382       /* Set Ids and Perm-Ids */
 383       bddIdsInSupport[scan->index] = scan->index;
 384       permIdsInSupport[scan->index] = ddMgr->perm[scan->index];
 385       scan = cuddT (scan);
 386     }
 387     Cudd_RecursiveDeref (ddMgr, support);
 388   }
 389   /* so that we do not try to free it in case of failure */
 390   support = NULL;
 391
 392   /*---------------------------- Start HEADER -------------------------------*/
 393
 394   if (noHeader==0) {
 395
 396     retValue = fprintf (fp,
 397       "c # BDD stored by the DDDMP tool in CNF format\n");
 398     Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing on file.",
 399       failure);
 400     fprintf (fp, "c #\n");
 401   }
 402
 403   /*-------------------- Generate Bdd IDs IFF necessary ---------------------*/
 404
 405   if (bddIds == NULL) {
 406     if (noHeader==0) {
 407       fprintf (fp, "c # Warning: BDD IDs missing ... evaluating them.\n");
 408       fprintf (fp, "c # \n");
 409       fflush (fp);
 410     }
 411
 412     bddIdsToFree = 1;
 413     bddIds = DDDMP_ALLOC (int, nVar);
 414     Dddmp_CheckAndGotoLabel (bddIds==NULL, "Error allocating memory.",
 415       failure);
 416
 417     /* Get BDD-IDs Directly from Cudd Manager */
 418     for (i=0; i<nVar; i++) {
 419       bddIds[i] = i;
 420     }
 421   } /* end if bddIds == NULL */
 422
 423   /*------------------ Generate AUX BDD IDs IF necessary --------------------*/
 424
 425   if (bddAuxIds == NULL) {
 426     if (noHeader==0) {
 427       fprintf (fp, "c # Warning: AUX IDs missing ... equal to BDD IDs.\n");
 428       fprintf (fp, "c #\n");
 429       fflush (fp);
 430     }
 431
 432     bddAuxIdsToFree = 1;
 433     bddAuxIds = DDDMP_ALLOC (int, nVar);
 434     Dddmp_CheckAndGotoLabel (bddAuxIds==NULL, "Error allocating memory.",
 435       failure);
 436
 437     for (i=0; i<nVar; i++) {
 438       bddAuxIds[i] = bddIds[i];
 439     }
 440   } /* end if cnfIds == NULL */
 441
 442   /*------------------- Generate CNF IDs IF necessary -----------------------*/
 443
 444   if (cnfIds == NULL) {
 445     if (noHeader==0) {
 446       fprintf (fp, "c # Warning: CNF IDs missing ... equal to BDD IDs.\n");
 447       fprintf (fp, "c #\n");
 448       fflush (fp);
 449     }
 450
 451     cnfIdsToFree = 1;
 452     cnfIds = DDDMP_ALLOC (int, nVar);
 453     Dddmp_CheckAndGotoLabel (cnfIds==NULL, "Error allocating memory.",
 454       failure);
 455
 456     for (i=0; i<nVar; i++) {
 457       cnfIds[i] = bddIds[i] + 1;
 458     }
 459   } /* end if cnfIds == NULL */
 460
 461   /*------------------ Generate Var Names IF necessary ----------------------*/
 462
 463   flagVar = 0;
 464   if (varNames == NULL) {
 465     if (noHeader==0) {
 466       fprintf (fp,
 467         "c # Warning: null variable names ... create DUMMY names.\n");
 468       fprintf (fp, "c #\n");
 469       fflush (stderr);
 470     }
 471
 472     varNamesToFree = 1;
 473     varNames = DDDMP_ALLOC (char *, nVar);
 474     for (i=0; i<nVar; i++) {
 475        varNames[i] = NULL;
 476     }
 477     Dddmp_CheckAndGotoLabel (varNames==NULL, "Error allocating memory.",
 478       failure);
 479
 480     flagVar = 1;
 481   } else {
 482     /* Protect the user also from partially loaded varNames array !!! */
 483     for (i=0; i<nVar && flagVar==0; i++) {
 484       if (varNames[i] == NULL) {
 485         flagVar = 1;
 486       }
 487     }
 488   }
 489
 490   if (flagVar == 1) {
 491     for (i=0; i<nVar; i++) {
 492       if (varNames[i] == NULL) {
 493         sprintf (tmpString, "DUMMY%d", bddIds[i]);
 494         varNames[i] = DDDMP_ALLOC (char, (strlen (tmpString)+1));
 495         strcpy (varNames[i], tmpString);
 496       }
 497     }
 498   }
 499
 500   /*----------------------- Set Initial ID  IF necessary --------------------*/
 501
 502   if (idInitial <= 0) {
 503     idInitial = nVar + 1;
 504   }
 505
 506   /*--------------------------- Continue HEADER -----------------------------*/
 507
 508   if (noHeader==0) {
 509     fprintf (fp, "c .ver %s\n", DDDMP_VERSION);
 510     fprintf (fp, "c .nnodes %d\n", Cudd_SharingSize (f, rootN));
 511     fprintf (fp, "c .nvars %d\n", nVar);
 512     fprintf (fp, "c .nsuppvars %d\n", nVarInSupport);
 513
 514     /* Support Variable Names */
 515     if (varNames != NULL) {
 516       fprintf (fp, "c .suppvarnames");
 517       for (i=0; i<nVar; i++) {
 518         if (bddIdsInSupport[i] >= 0) {
 519           fprintf (fp, " %s", varNames[i]);
 520         }
 521       }
 522       fprintf (fp, "\n");
 523     }
 524
 525     /* Ordered Variable Names */
 526     if (varNames != NULL) {
 527       fprintf (fp, "c .orderedvarnames");
 528       for (i=0; i<nVar; i++) {
 529         fprintf (fp, " %s", varNames[i]);
 530       }
 531       fprintf (fp, "\n");
 532     }
 533
 534     /* BDD Variable Ids */
 535     fprintf (fp, "c .ids ");
 536     for (i=0; i<nVar; i++) {
 537       if (bddIdsInSupport[i] >= 0) {
 538         fprintf (fp, " %d", bddIdsInSupport[i]);
 539       }
 540     }
 541     fprintf (fp, "\n");
 542
 543     /* BDD Variable Permutation Ids */
 544     fprintf (fp, "c .permids ");
 545     for (i=0; i<nVar; i++) {
 546       if (bddIdsInSupport[i] >= 0) {
 547         fprintf (fp, " %d", permIdsInSupport[i]);
 548       }
 549     }
 550     fprintf (fp, "\n");
 551
 552     /* BDD Variable Auxiliary Ids */
 553     fprintf (fp, "c .auxids ");
 554     for (i=0; i<nVar; i++) {
 555       if (bddIdsInSupport[i] >= 0) {
 556         fprintf (fp, " %d", bddAuxIds[i]);
 557       }
 558     }
 559     fprintf (fp, "\n");
 560
 561     /* CNF Ids */
 562     fprintf (fp, "c .cnfids ");
 563     for (i=0; i<nVar; i++) {
 564       if (bddIdsInSupport[i] >= 0) {
 565         fprintf (fp, " %d", cnfIds[i]);
 566       }
 567     }
 568     fprintf (fp, "\n");
 569
 570     /* Number of Roots */
 571     fprintf (fp, "c .nroots %d", rootN);
 572     fprintf (fp, "\n");
 573
 574     /* Root Starting Line */
 575     fgetpos (fp, &posFile1);
 576     fprintf (fp, "c .rootids");
 577     for (i=0; i<rootN; i++) {
 578       for (j=0; j<intStringLength+1; j++) {
 579         retValue = fprintf (fp, " ");
 580       }
 581     }
 582     retValue = fprintf (fp, "\n");
 583     fflush (fp);
 584
 585   } /* End of noHeader check */
 586
 587   /*------------ Select Mode and Print Number of Tmp Var Created ------------*/
 588
 589   switch (mode) {
 590     case DDDMP_CNF_MODE_NODE:
 591       *varNewNPtr = idInitial;
 592       *varNewNPtr = DddmpNumberDdNodesCnf (ddMgr, f, rootN, cnfIds, idInitial)
 593         - *varNewNPtr;
 594       break;
 595     case DDDMP_CNF_MODE_MAXTERM:
 596       *varNewNPtr = 0;
 597       break;
 598     default:
 599       Dddmp_Warning (1, "Wrong DDDMP Store Mode. Force DDDMP_MODE_BEST.");
 600     case DDDMP_CNF_MODE_BEST:
 601       *varNewNPtr = idInitial;
 602       *varNewNPtr = DddmpDdNodesCountEdgesAndNumber (ddMgr, f, rootN,
 603         edgeInTh, pathLengthTh, cnfIds, idInitial) - *varNewNPtr;
 604       break;
 605   }
 606
 607   /*------------ Print Space for Number of Variable and Clauses -------------*/
 608
 609   if (noHeader==0) {
 610     fprintf (fp, "c .nAddedCnfVar %d\n", *varNewNPtr);
 611     fprintf (fp, "c #\n");
 612     fprintf (fp, "c # Init CNF Clauses\n");
 613     fprintf (fp, "c #\n");
 614     fgetpos (fp, &posFile2);
 615     retValue = fprintf (fp, "p cnf");
 616     for (j=0; j<2*(intStringLength+1); j++) {
 617       retValue = fprintf (fp, " ");
 618     }
 619     retValue = fprintf (fp, "\n");
 620     fflush (fp);
 621   }
 622
 623   /*---------------------- Select Mode and Do the Job -----------------------*/
 624
 625   clauseN = 0;
 626   varMax = -1;
 627   rootStartLine = DDDMP_ALLOC (int, rootN);
 628   Dddmp_CheckAndGotoLabel (rootStartLine==NULL, "Error allocating memory.",
 629     failure);
 630   for (i=0; i<rootN; i++) {
 631     rootStartLine[i] = (-1);
 632   }
 633
 634   switch (mode) {
 635     case DDDMP_CNF_MODE_NODE:
 636       StoreCnfNodeByNode (ddMgr, f, rootN, bddIds, cnfIds, fp, &clauseN,
 637         &varMax, rootStartLine);
 638       DddmpUnnumberDdNodesCnf (ddMgr, f, rootN);
 639       break;
 640     case DDDMP_CNF_MODE_MAXTERM:
 641       StoreCnfMaxtermByMaxterm (ddMgr, f, rootN, bddIds, cnfIds, idInitial,
 642         fp, &varMax, &clauseN, rootStartLine);
 643       break;
 644     default:
 645       Dddmp_Warning (1, "Wrong DDDMP Store Mode. Force DDDMP_MODE_BEST.");
 646     case DDDMP_CNF_MODE_BEST:
 647       StoreCnfBest (ddMgr, f, rootN, bddIds, cnfIds, idInitial,
 648         fp, &varMax, &clauseN, rootStartLine);
 649       DddmpUnnumberDdNodesCnf (ddMgr, f, rootN);
 650       break;
 651   }
 652
 653   /*------------------------------ Write trailer ----------------------------*/
 654
 655   if (noHeader==0) {
 656     retValue = fprintf (fp, "c # End of Cnf From dddmp-2.0\n");
 657     Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
 658       failure);
 659   }
 660
 661   /*
 662    *  Write Root Starting Line
 663    */
 664
 665   if (noHeader==0) {
 666     fsetpos (fp, &posFile1);
 667     fprintf (fp, "c .rootids");
 668     for (i=0; i<rootN; i++) {
 669       Dddmp_Warning (rootStartLine[i]==(-1),
 670         "Init Line for CNF file = (-1) {[(Stored one or zero BDD)]}.");
 671       sprintf (tmpString, " %d", rootStartLine[i]);
 672       for (j=strlen(tmpString); j<intStringLength+1; j++) {
 673         strcat (tmpString, " ");
 674       }
 675       retValue = fprintf (fp, "%s", tmpString);
 676     }
 677     retValue = fprintf (fp, "\n");
 678     fflush (fp);
 679   }
 680
 681   /*
 682    *  Write Number of clauses and variable in the header
 683    */
 684
 685   *clauseNPtr = clauseN;
 686
 687   if (noHeader==0) {
 688     fsetpos (fp, &posFile2);
 689     retValue = fprintf (fp, "p cnf");
 690     sprintf (tmpString, " %d %d", varMax, clauseN);
 691     for (j=strlen(tmpString); j<2*(intStringLength+1); j++) {
 692       strcat (tmpString, " ");
 693     }
 694     retValue = fprintf (fp, "%s\n", tmpString);
 695     fflush (fp);
 696   }
 697
 698   /*-------------------------- Close file and return ------------------------*/
 699
 700   if (fileToClose) {
 701     fclose (fp);
 702   }
 703
 704   DDDMP_FREE (bddIdsInSupport);
 705   DDDMP_FREE (permIdsInSupport);
 706   DDDMP_FREE (rootStartLine);
 707   if (bddIdsToFree == 1) {
 708     DDDMP_FREE (bddIds);
 709   }
 710   if (bddAuxIdsToFree == 1) {
 711     DDDMP_FREE (bddAuxIds);
 712   }
 713   if (cnfIdsToFree == 1) {
 714     DDDMP_FREE (cnfIds);
 715   }
 716   if (varNamesToFree == 1) {
 717     for (i=0; i<nVar; i++) {
 718       DDDMP_FREE (varNames[i]);
 719     }
 720     DDDMP_FREE (varNames);
 721   }
 722
 723   return (DDDMP_SUCCESS);
 724
 725   failure:
 726
 727     if (support != NULL) {
 728       Cudd_RecursiveDeref (ddMgr, support);
 729     }
 730     DDDMP_FREE (bddIdsInSupport);
 731     DDDMP_FREE (permIdsInSupport);
 732     DDDMP_FREE (rootStartLine);
 733     if (bddIdsToFree == 1) {
 734       DDDMP_FREE (bddIds);
 735     }
 736     if (bddAuxIdsToFree == 1) {
 737       DDDMP_FREE (bddAuxIds);
 738     }
 739     if (cnfIdsToFree == 1) {
 740       DDDMP_FREE (cnfIds);
 741     }
 742     if (varNamesToFree == 1) {
 743       for (i=0; i<nVar; i++) {
 744         DDDMP_FREE (varNames[i]);
 745       }
 746       DDDMP_FREE (varNames);
 747     }
 748
 749     return (DDDMP_FAILURE);
 750 }
 751
 752 /*---------------------------------------------------------------------------*/
 753 /* Definition of static functions                                            */
 754 /*---------------------------------------------------------------------------*/
 755
 756 /**Function********************************************************************
 757
 758   Synopsis     [Store the BDD as CNF clauses.]
 759
 760   Description  [Store the BDD as CNF clauses.
 761     Use a multiplexer description for each BDD node.
 762     ]
 763
 764   SideEffects  [None]
 765
 766   SeeAlso      []
 767
 768 ******************************************************************************/
 769
 770 static int
 771 StoreCnfNodeByNode (
 772   DdManager *ddMgr      /* IN: DD Manager */,
 773   DdNode **f            /* IN: BDD array to be stored */,
 774   int rootN             /* IN: number of BDDs in the array */,
 775   int *bddIds           /* IN: BDD ids for variables */,
 776   int *cnfIds           /* IN: CNF ids for variables */,
 777   FILE *fp              /* IN: store file */,
 778   int *clauseN      /* IN/OUT: number of clauses written in the CNF file */,
 779   int *varMax       /* IN/OUT: maximum value of id written in the CNF file */,
 780   int *rootStartLine   /* OUT: CNF line where root starts */
 781   )
 782 {
 783   int retValue = 0;
 784   int i, idf;
 785
 786   for (i=0; i<rootN; i++) {
 787     if (f[i] != NULL) {
 788       if (!cuddIsConstant(Cudd_Regular (f[i]))) {
 789         /*
 790          *  Set Starting Line for this Root
 791          */
 792
 793         rootStartLine[i] = *clauseN + 1;
 794
 795         /*
 796          *  Store the BDD
 797          */
 798
 799         retValue = StoreCnfNodeByNodeRecur (ddMgr, Cudd_Regular(f[i]),
 800           bddIds, cnfIds, fp, clauseN, varMax);
 801         if (retValue == 0) {
 802           (void) fprintf (stderr,
 803             "DdStoreCnf: Error in recursive node store\n");
 804           fflush (stderr);
 805         }
 806
 807         /*
 808          *  Store CNF for the root if necessary
 809          */
 810
 811         idf = DddmpReadNodeIndexCnf (Cudd_Regular (f[i]));
 812 #if DDDMP_DEBUG_CNF
 813         retValue = fprintf (fp, "root %d --> \n", i);
 814 #endif
 815         if (Cudd_IsComplement (f[i])) {
 816           retValue = fprintf (fp, "-%d 0\n", idf);
 817         } else {
 818           retValue = fprintf (fp, "%d 0\n", idf);
 819         }
 820         *varMax = GET_MAX (*varMax, idf);
 821         *clauseN = *clauseN + 1;
 822
 823         if (retValue == EOF) {
 824           (void) fprintf (stderr,
 825             "DdStoreCnf: Error in recursive node store\n");
 826           fflush (stderr);
 827         }
 828       }
 829     }
 830   }
 831
 832   return (retValue);
 833 }
 834
 835 /**Function********************************************************************
 836
 837   Synopsis     [Performs the recursive step of Dddmp_bddStore.]
 838
 839   Description  [Performs the recursive step of Dddmp_bddStore.
 840     Traverse the BDD and store a CNF formula for each "terminal" node.
 841     ]
 842
 843   SideEffects  [None]
 844
 845   SeeAlso      []
 846
 847 ******************************************************************************/
 848
 849 static int
 850 StoreCnfNodeByNodeRecur (
 851   DdManager *ddMgr   /* IN: DD Manager */,
 852   DdNode *f          /* IN: BDD node to be stored */,
 853   int *bddIds        /* IN: BDD ids for variables */,
 854   int *cnfIds        /* IN: CNF ids for variables */,
 855   FILE *fp           /* IN: store file */,
 856   int *clauseN      /* OUT: number of clauses written in the CNF file */,
 857   int *varMax       /* OUT: maximum value of id written in the CNF file */
 858   )
 859 {
 860   DdNode *T, *E;
 861   int idf, idT, idE, vf;
 862   int retValue;
 863
 864 #ifdef DDDMP_DEBUG
 865   assert(!Cudd_IsComplement(f));
 866   assert(f!=NULL);
 867 #endif
 868
 869   /* If constant, nothing to do. */
 870   if (Cudd_IsConstant(f)) {
 871     return (1);
 872   }
 873
 874   /* If already visited, nothing to do. */
 875   if (DddmpVisitedCnf (f)) {
 876     return (1);
 877   }
 878
 879   /* Mark node as visited. */
 880   DddmpSetVisitedCnf (f);
 881
 882   /*------------------ Non Terminal Node -------------------------------*/
 883
 884 #ifdef DDDMP_DEBUG
 885   /* BDDs! Only one constant supported */
 886   assert (!cuddIsConstant(f));
 887 #endif
 888
 889   /*
 890    *  Recursive call for Then edge
 891    */
 892
 893   T = cuddT (f);
 894 #ifdef DDDMP_DEBUG
 895   /* ROBDDs! No complemented Then edge */
 896   assert (!Cudd_IsComplement(T));
 897 #endif
 898   /* recur */
 899   retValue = StoreCnfNodeByNodeRecur (ddMgr, T, bddIds, cnfIds, fp,
 900     clauseN, varMax);
 901   if (retValue != 1) {
 902     return(retValue);
 903   }
 904
 905   /*
 906    *  Recursive call for Else edge
 907    */
 908
 909   E = Cudd_Regular (cuddE (f));
 910   retValue = StoreCnfNodeByNodeRecur (ddMgr, E, bddIds, cnfIds, fp,
 911     clauseN, varMax);
 912   if (retValue != 1) {
 913     return (retValue);
 914   }
 915
 916   /*
 917    *  Obtain nodeids and variable ids of f, T, E
 918    */
 919
 920   idf = DddmpReadNodeIndexCnf (f);
 921   vf = f->index;
 922
 923   if (bddIds[vf] != vf) {
 924     (void) fprintf (stderr, "DdStoreCnf: Error writing to file\n");
 925     fflush (stderr);
 926     return (0);
 927   }
 928
 929   idT = DddmpReadNodeIndexCnf (T);
 930
 931   idE = DddmpReadNodeIndexCnf (E);
 932   if (Cudd_IsComplement (cuddE (f))) {
 933     idE = -idE;
 934   }
 935
 936   retValue = StoreCnfOneNode (f, idf, cnfIds[vf], idT, idE, fp,
 937    clauseN, varMax);
 938
 939   if (retValue == EOF) {
 940     return (0);
 941   } else {
 942     return (1);
 943   }
 944 }
 945
 946 /**Function********************************************************************
 947
 948   Synopsis     [Store One Single BDD Node.]
 949
 950   Description  [Store One Single BDD Node translating it as a multiplexer.]
 951
 952   SideEffects  [None]
 953
 954   SeeAlso      []
 955
 956 ******************************************************************************/
 957
 958 static int
 959 StoreCnfOneNode (
 960   DdNode *f       /* IN: node to be stored */,
 961   int idf         /* IN: node CNF Index  */,
 962   int vf          /* IN: node BDD Index */,
 963   int idT         /* IN: Then CNF Index with sign = inverted edge */,
 964   int idE         /* IN: Else CNF Index with sign = inverted edge */,
 965   FILE *fp        /* IN: store file */,
 966   int *clauseN   /* OUT: number of clauses */,
 967   int *varMax    /* OUT: maximun Index of variable stored */
 968   )
 969 {
 970   int retValue = 0;
 971   int idfAbs, idTAbs, idEAbs;
 972
 973   idfAbs = abs (idf);
 974   idTAbs = abs (idT);
 975   idEAbs = abs (idE);
 976
 977   /*----------------------------- Check for Constant ------------------------*/
 978
 979   assert(!Cudd_IsConstant(f));
 980
 981   /*------------------------- Check for terminal nodes ----------------------*/
 982
 983   if ((idTAbs==1) && (idEAbs==1)) {
 984     return (1);
 985   }
 986
 987   /*------------------------------ Internal Node ----------------------------*/
 988
 989 #if DDDMP_DEBUG_CNF
 990   retValue = fprintf (fp, "id=%d var=%d idT=%d idE=%d\n",
 991     idf, vf, idT, idE);
 992 #endif
 993
 994   /*
 995    *  Then to terminal
 996    */
 997
 998   if ((idTAbs==1) && (idEAbs!=1)) {
 999 #if DDDMP_DEBUG_CNF
1000     retValue = fprintf (fp, "CASE 1 -->\n");
1001 #endif
1002     retValue = fprintf (fp, "%d %d 0\n",
1003       idf, -vf);
1004     retValue = fprintf (fp, "%d %d 0\n",
1005       idf, -idE);
1006     retValue = fprintf (fp, "%d %d %d 0\n",
1007       -idf, vf, idE);
1008     *clauseN = *clauseN + 3;
1009
1010     *varMax = GET_MAX (*varMax, idfAbs);
1011     *varMax = GET_MAX (*varMax, vf);
1012     *varMax = GET_MAX (*varMax, idEAbs);
1013   }
1014
1015   /*
1016    *  Else to terminal
1017    */
1018
1019   if ((idTAbs!=1) && (idEAbs==1)) {
1020     if (idE == 1) {
1021 #if DDDMP_DEBUG_CNF
1022       retValue = fprintf (fp, "CASE 2 -->\n");
1023 #endif
1024       retValue = fprintf (fp, "%d %d 0\n",
1025         idf, vf);
1026       retValue = fprintf (fp, "%d %d 0\n",
1027         idf, -idT);
1028       retValue = fprintf (fp, "%d %d %d 0\n",
1029         -idf, -vf, idT);
1030     } else {
1031 #if DDDMP_DEBUG_CNF
1032       retValue = fprintf (fp, "CASE 3 -->\n");
1033 #endif
1034       retValue = fprintf (fp, "%d %d 0\n",
1035         -idf, vf);
1036       retValue = fprintf (fp, "%d %d 0\n",
1037         -idf, idT);
1038       retValue = fprintf (fp, "%d %d %d 0\n",
1039         idf, -vf, -idT);
1040     }
1041
1042     *varMax = GET_MAX (*varMax, idfAbs);
1043     *varMax = GET_MAX (*varMax, vf);
1044     *varMax = GET_MAX (*varMax, idTAbs);
1045
1046     *clauseN = *clauseN + 3;
1047   }
1048
1049   /*
1050    *  Nor Then or Else to terminal
1051    */
1052
1053   if ((idTAbs!=1) && (idEAbs!=1)) {
1054 #if DDDMP_DEBUG_CNF
1055     retValue = fprintf (fp, "CASE 4 -->\n");
1056 #endif
1057     retValue = fprintf (fp, "%d %d %d 0\n",
1058       idf, vf, -idE);
1059     retValue = fprintf (fp, "%d %d %d 0\n",
1060       -idf, vf, idE);
1061     retValue = fprintf (fp, "%d %d %d 0\n",
1062       idf, -vf, -idT);
1063     retValue = fprintf (fp, "%d %d %d 0\n",
1064       -idf, -vf, idT);
1065
1066     *varMax = GET_MAX (*varMax, idfAbs);
1067     *varMax = GET_MAX (*varMax, vf);
1068     *varMax = GET_MAX (*varMax, idTAbs);
1069     *varMax = GET_MAX (*varMax, idEAbs);
1070
1071     *clauseN = *clauseN + 4;
1072   }
1073
1074   return (retValue);
1075 }
1076
1077 /**Function********************************************************************
1078
1079   Synopsis    [Prints a disjoint sum of products.]
1080
1081   Description [Prints a disjoint sum of product cover for the function
1082     rooted at node. Each product corresponds to a path from node a
1083     leaf node different from the logical zero, and different from
1084     the background value. Uses the standard output.  Returns 1 if
1085     successful, 0 otherwise.
1086     ]
1087
1088   SideEffects [None]
1089
1090   SeeAlso     [StoreCnfBest]
1091
1092 ******************************************************************************/
1093
1094 static int
1095 StoreCnfMaxtermByMaxterm (
1096   DdManager *ddMgr    /* IN: DD Manager */,
1097   DdNode **f          /* IN: array of BDDs to store */,
1098   int rootN           /* IN: number of BDDs in the array */,
1099   int *bddIds         /* IN: BDD Identifiers */,
1100   int *cnfIds         /* IN: corresponding CNF Identifiers */,
1101   int idInitial       /* IN: initial value for numbering new CNF variables */,
1102   FILE *fp            /* IN: file pointer */,
1103   int *varMax        /* OUT: maximum identifier of the variables created */,
1104   int *clauseN       /* OUT: number of stored clauses */,
1105   int *rootStartLine /* OUT: line where root starts */
1106   )
1107 {
1108   int i, j, *list;
1109
1110   list = DDDMP_ALLOC (int, ddMgr->size);
1111   if (list == NULL) {
1112     ddMgr->errorCode = CUDD_MEMORY_OUT;
1113     return (DDDMP_FAILURE);
1114   }
1115
1116   for (i=0; i<rootN; i++) {
1117     if (f[i] != NULL) {
1118       if (!cuddIsConstant(Cudd_Regular (f[i]))) {
1119         for (j=0; j<ddMgr->size; j++) {
1120           list[j] = 2;
1121         }
1122
1123         /*
1124          *  Set Starting Line for this Root
1125          */
1126
1127         rootStartLine[i] = *clauseN + 1;
1128
1129         StoreCnfMaxtermByMaxtermRecur (ddMgr, f[i], bddIds, cnfIds, fp,
1130           list, clauseN, varMax);
1131       }
1132     }
1133   }
1134
1135   FREE (list);
1136
1137   return (1);
1138 }
1139
1140 /**Function********************************************************************
1141
1142   Synopsis    [Prints a disjoint sum of products with intermediate
1143     cutting points.]
1144
1145   Description [Prints a disjoint sum of product cover for the function
1146     rooted at node intorducing cutting points whenever necessary.
1147     Each product corresponds to a path from node a leaf
1148     node different from the logical zero, and different from the
1149     background value. Uses the standard output.  Returns 1 if
1150     successful, 0 otherwise.
1151     ]
1152
1153   SideEffects [None]
1154
1155   SeeAlso     [StoreCnfMaxtermByMaxterm]
1156
1157 ******************************************************************************/
1158
1159 static int
1160 StoreCnfBest (
1161   DdManager *ddMgr    /* IN: DD Manager */,
1162   DdNode **f          /* IN: array of BDDs to store */,
1163   int rootN           /* IN: number of BDD in the array */,
1164   int *bddIds         /* IN: BDD identifiers */,
1165   int *cnfIds         /* IN: corresponding CNF identifiers */,
1166   int idInitial       /* IN: initial value for numbering new CNF variables */,
1167   FILE *fp            /* IN: file pointer */,
1168   int *varMax        /* OUT: maximum identifier of the variables created */,
1169   int *clauseN       /* OUT: number of stored clauses */,
1170   int *rootStartLine /* OUT: line where root starts */
1171   )
1172 {
1173   int i, j, *list;
1174
1175   list = DDDMP_ALLOC (int, ddMgr->size);
1176   if (list == NULL) {
1177     ddMgr->errorCode = CUDD_MEMORY_OUT;
1178     return (DDDMP_FAILURE);
1179   }
1180
1181   for (i=0; i<rootN; i++) {
1182     if (f[i] != NULL) {
1183       if (!cuddIsConstant(Cudd_Regular (f[i]))) {
1184         for (j=0; j<ddMgr->size; j++) {
1185           list[j] = 2;
1186         }
1187
1188         /*
1189          *  Set Starting Line for this Root
1190          */
1191
1192         rootStartLine[i] = *clauseN + 1;
1193
1194 #if DDDMP_DEBUG_CNF
1195         fprintf (fp, "root NOT shared BDDs %d --> \n", i);
1196 #endif
1197         StoreCnfBestNotSharedRecur (ddMgr, f[i], 0, bddIds, cnfIds, fp, list,
1198           clauseN, varMax);
1199
1200 #if DDDMP_DEBUG_CNF
1201         fprintf (fp, "root SHARED BDDs %d --> \n", i);
1202 #endif
1203         StoreCnfBestSharedRecur (ddMgr, Cudd_Regular (f[i]), bddIds, cnfIds,
1204           fp, list, clauseN, varMax);
1205       }
1206     }
1207   }
1208
1209 #if DDDMP_DEBUG_CNF
1210   fprintf (stdout, "###---> BDDs After the Storing Process:\n");
1211   DddmpPrintBddAndNext (ddMgr, f, rootN);
1212 #endif
1213
1214   FREE (list);
1215
1216   return (DDDMP_SUCCESS);
1217 }
1218
1219 /**Function********************************************************************
1220
1221   Synopsis    [Performs the recursive step of Print Maxterm.]
1222
1223   Description [Performs the recursive step of Print Maxterm.
1224     Traverse a BDD a print out a cube in CNF format each time a terminal
1225     node is reached.
1226     ]
1227
1228   SideEffects [None]
1229
1230   SeeAlso     []
1231
1232 ******************************************************************************/
1233
1234 static void
1235 StoreCnfMaxtermByMaxtermRecur (
1236   DdManager *ddMgr  /* IN: DD Manager */,
1237   DdNode *node      /* IN: BDD to store */,
1238   int *bddIds       /* IN: BDD identifiers */,
1239   int *cnfIds       /* IN: corresponding CNF identifiers */,
1240   FILE *fp          /* IN: file pointer */,
1241   int *list         /* IN: temporary array to store cubes */,
1242   int *clauseN     /* OUT: number of stored clauses */,
1243   int *varMax      /* OUT: maximum identifier of the variables created */
1244   )
1245 {
1246   DdNode *N, *Nv, *Nnv;
1247   int retValue, index;
1248
1249   N = Cudd_Regular (node);
1250
1251   /*
1252    *  Terminal case: Print one cube based on the current recursion
1253    */
1254
1255   if (cuddIsConstant (N)) {
1256     retValue = printCubeCnf (ddMgr, node, cnfIds, fp, list, varMax);
1257     if (retValue == DDDMP_SUCCESS) {
1258       fprintf (fp, "0\n");
1259       *clauseN = *clauseN + 1;
1260     }
1261     return;
1262   }
1263
1264   /*
1265    *  NON Terminal case: Recur
1266    */
1267
1268   Nv  = cuddT (N);
1269   Nnv = cuddE (N);
1270   if (Cudd_IsComplement (node)) {
1271     Nv  = Cudd_Not (Nv);
1272     Nnv = Cudd_Not (Nnv);
1273   }
1274   index = N->index;
1275
1276   /*
1277    *  StQ 06.05.2003
1278    *  Perform the optimization:
1279    *  f = (a + b)' = (a') ^ (a + b') = (a') ^ (b')
1280    *  i.e., if the THEN node is the constant ZERO then that variable
1281    *  can be forgotten (list[index] = 2) for subsequent ELSE cubes
1282    */
1283   if (cuddIsConstant (Cudd_Regular (Nv)) &&  Nv != ddMgr->one) {
1284     list[index] = 2;
1285   } else {
1286     list[index] = 0;
1287   }
1288   StoreCnfMaxtermByMaxtermRecur (ddMgr, Nnv, bddIds, cnfIds, fp, list,
1289     clauseN, varMax);
1290
1291   /*
1292    *  StQ 06.05.2003
1293    *  Perform the optimization:
1294    *  f = a ^ b = (a) ^ (a' + b) = (a) ^ (b)
1295    *  i.e., if the ELSE node is the constant ZERO then that variable
1296    *  can be forgotten (list[index] = 2) for subsequent THEN cubes
1297    */
1298   if (cuddIsConstant (Cudd_Regular (Nnv)) &&  Nnv != ddMgr->one) {
1299     list[index] = 2;
1300   } else {
1301     list[index] = 1;
1302   }
1303   StoreCnfMaxtermByMaxtermRecur (ddMgr, Nv, bddIds, cnfIds, fp, list,
1304     clauseN, varMax);
1305   list[index] = 2;
1306
1307   return;
1308 }
1309
1310 /**Function********************************************************************
1311
1312   Synopsis    [Performs the recursive step of Print Best on Not Shared
1313     sub-BDDs.]
1314
1315   Description [Performs the recursive step of Print Best on Not Shared
1316     sub-BDDs, i.e., print out information for the nodes belonging to
1317     BDDs not shared (whose root has just one incoming edge).
1318     ]
1319
1320   SideEffects [None]
1321
1322   SeeAlso     []
1323
1324 ******************************************************************************/
1325
1326 static int
1327 StoreCnfBestNotSharedRecur (
1328   DdManager *ddMgr   /* IN: DD Manager */,
1329   DdNode *node       /* IN: BDD to store */,
1330   int idf            /* IN: Id to store */,
1331   int *bddIds        /* IN: BDD identifiers */,
1332   int *cnfIds        /* IN: corresponding CNF identifiers */,
1333   FILE *fp           /* IN: file pointer */,
1334   int *list          /* IN: temporary array to store cubes */,
1335   int *clauseN      /* OUT: number of stored clauses */,
1336   int *varMax       /* OUT: maximum identifier of the variables created */
1337   )
1338 {
1339   DdNode *N, *Nv, *Nnv;
1340   int index, retValue;
1341   DdNode *one;
1342
1343   one = ddMgr->one;
1344
1345   N = Cudd_Regular (node);
1346
1347   /*
1348    *  Terminal case or Already Visited:
1349    *    Print one cube based on the current recursion
1350    */
1351
1352   if (cuddIsConstant (N)) {
1353     retValue = printCubeCnf (ddMgr, node, cnfIds, fp, list, varMax);
1354     if (retValue == DDDMP_SUCCESS) {
1355       if (idf != 0) {
1356          fprintf (fp, "%d ", idf);
1357       }
1358       fprintf (fp, "0\n");
1359       *varMax = GET_MAX (*varMax, abs(idf));
1360       *clauseN = *clauseN + 1;
1361     }
1362     return (DDDMP_SUCCESS);
1363   }
1364
1365   /*
1366    *  Shared Sub-Tree: Print Cube
1367    */
1368
1369   index = DddmpReadNodeIndexCnf (N);
1370   if (index > 0) {
1371     if (idf != 0) {
1372       fprintf (fp, "%d ", idf);
1373     }
1374     if (Cudd_IsComplement (node)) {
1375       retValue = fprintf (fp, "-%d ", index);
1376     } else {
1377       retValue = fprintf (fp, "%d ", index);
1378     }
1379     retValue = printCubeCnf (ddMgr, node, cnfIds, fp, list, varMax);
1380     fprintf (fp, "0\n");
1381     *varMax = GET_MAX (*varMax, abs(index));
1382     *clauseN = *clauseN + 1;
1383     return (DDDMP_SUCCESS);
1384   }
1385
1386   /*
1387    *  NON Terminal case: Recur
1388    */
1389
1390   Nv  = cuddT (N);
1391   Nnv = cuddE (N);
1392   if (Cudd_IsComplement (node)) {
1393     Nv  = Cudd_Not (Nv);
1394     Nnv = Cudd_Not (Nnv);
1395   }
1396   index = N->index;
1397
1398   /*
1399    *  StQ 06.05.2003
1400    *  Perform the optimization:
1401    *  f = (a + b)' = (a') ^ (a + b') = (a') ^ (b')
1402    *  i.e., if the THEN node is the constant ZERO then that variable
1403    *  can be forgotten (list[index] = 2) for subsequent ELSE cubes
1404    */
1405   if (cuddIsConstant (Cudd_Regular (Nv)) &&  Nv != ddMgr->one) {
1406     list[index] = 2;
1407   } else {
1408     list[index] = 0;
1409   }
1410   StoreCnfBestNotSharedRecur (ddMgr, Nnv, idf, bddIds, cnfIds, fp, list,
1411     clauseN, varMax);
1412
1413   /*
1414    *  StQ 06.05.2003
1415    *  Perform the optimization:
1416    *  f = a ^ b = (a) ^ (a' + b) = (a) ^ (b)
1417    *  i.e., if the ELSE node is the constant ZERO then that variable
1418    *  can be forgotten (list[index] = 2) for subsequent THEN cubes
1419    */
1420   if (cuddIsConstant (Cudd_Regular (Nnv)) &&  Nnv != ddMgr->one) {
1421     list[index] = 2;
1422   } else {
1423     list[index] = 1;
1424   }
1425   StoreCnfBestNotSharedRecur (ddMgr, Nv, idf, bddIds, cnfIds, fp, list,
1426     clauseN, varMax);
1427   list[index] = 2;
1428
1429   return (DDDMP_SUCCESS);
1430 }
1431
1432 /**Function********************************************************************
1433
1434   Synopsis    [Performs the recursive step of Print Best on Shared
1435     sub-BDDs.
1436     ]
1437
1438   Description [Performs the recursive step of Print Best on Not Shared
1439     sub-BDDs, i.e., print out information for the nodes belonging to
1440     BDDs not shared (whose root has just one incoming edge).
1441     ]
1442
1443   SideEffects [None]
1444
1445   SeeAlso      []
1446
1447 ******************************************************************************/
1448
1449 static int
1450 StoreCnfBestSharedRecur (
1451   DdManager *ddMgr  /* IN: DD Manager */,
1452   DdNode *node      /* IN: BDD to store */,
1453   int *bddIds       /* IN: BDD identifiers */,
1454   int *cnfIds       /* IN: corresponding CNF identifiers */,
1455   FILE *fp          /* IN: file pointer */,
1456   int *list         /* IN: temporary array to store cubes */,
1457   int *clauseN     /* OUT: number of stored clauses */,
1458   int *varMax      /* OUT: maximum identifier of the variables created */
1459   )
1460 {
1461   DdNode *nodeThen, *nodeElse;
1462   int i, idf, index;
1463   DdNode *one;
1464
1465   one = ddMgr->one;
1466
1467   Dddmp_Assert (node==Cudd_Regular(node),
1468     "Inverted Edge during Shared Printing.");
1469
1470   /* If constant, nothing to do. */
1471   if (cuddIsConstant (node)) {
1472     return (DDDMP_SUCCESS);
1473   }
1474
1475   /* If already visited, nothing to do. */
1476   if (DddmpVisitedCnf (node)) {
1477     return (DDDMP_SUCCESS);
1478   }
1479
1480   /*
1481    *  Shared Sub-Tree: Print Cube
1482    */
1483
1484   idf = DddmpReadNodeIndexCnf (node);
1485   if (idf > 0) {
1486     /* Cheat the Recur Function about the Index of the Current Node */
1487     DddmpWriteNodeIndexCnf (node, 0);
1488
1489 #if DDDMP_DEBUG_CNF
1490     fprintf (fp, "Else of XNOR\n");
1491 #endif
1492     for (i=0; i<ddMgr->size; i++) {
1493       list[i] = 2;
1494     }
1495     StoreCnfBestNotSharedRecur (ddMgr, Cudd_Not (node), idf, bddIds, cnfIds,
1496       fp, list, clauseN, varMax);
1497
1498 #if DDDMP_DEBUG_CNF
1499     fprintf (fp, "Then of XNOR\n");
1500 #endif
1501     for (i=0; i<ddMgr->size; i++) {
1502       list[i] = 2;
1503     }
1504     StoreCnfBestNotSharedRecur (ddMgr, node, -idf, bddIds, cnfIds,
1505       fp, list, clauseN, varMax);
1506
1507     /* Set Back Index of Current Node */
1508     DddmpWriteNodeIndexCnf (node, idf);
1509   }
1510
1511   /* Mark node as visited. */
1512   DddmpSetVisitedCnf (node);
1513
1514   /*
1515    *  Recur
1516    */
1517
1518   nodeThen  = cuddT (node);
1519   nodeElse = cuddE (node);
1520   index = node->index;
1521
1522   StoreCnfBestSharedRecur (ddMgr, Cudd_Regular (nodeThen), bddIds, cnfIds,
1523     fp, list, clauseN, varMax);
1524   StoreCnfBestSharedRecur (ddMgr, Cudd_Regular (nodeElse), bddIds, cnfIds,
1525     fp, list, clauseN, varMax);
1526
1527   return (DDDMP_SUCCESS);
1528 }
1529
1530 /**Function********************************************************************
1531
1532   Synopsis    [Print One Cube in CNF Format.]
1533
1534   Description [Print One Cube in CNF Format.
1535     Return DDDMP_SUCCESS if something is printed out, DDDMP_FAILURE
1536     is nothing is printed out.
1537     ]
1538
1539   SideEffects [None]
1540
1541   SeeAlso      []
1542
1543 ******************************************************************************/
1544
1545 static int
1546 printCubeCnf (
1547   DdManager *ddMgr /* IN: DD Manager */,
1548   DdNode *node     /* IN: BDD to store */,
1549   int *cnfIds      /* IN: CNF identifiers */,
1550   FILE *fp         /* IN: file pointer */,
1551   int *list        /* IN: temporary array to store cubes */,
1552   int *varMax      /* OUT: maximum identifier of the variables created */
1553   )
1554 {
1555   int i, retValue;
1556   DdNode *one;
1557
1558   retValue = DDDMP_FAILURE;
1559   one = ddMgr->one;
1560
1561   if (node != one) {
1562     for (i=0; i<ddMgr->size; i++) {
1563       if (list[i] == 0) {
1564         retValue = DDDMP_SUCCESS;
1565         (void) fprintf (fp, "%d ", cnfIds[i]);
1566         *varMax = GET_MAX(*varMax, cnfIds[i]);
1567       } else {
1568         if (list[i] == 1) {
1569           retValue = DDDMP_SUCCESS;
1570           (void) fprintf (fp, "-%d ", cnfIds[i]);
1571           *varMax = GET_MAX(*varMax, cnfIds[i]);
1572         }
1573       }
1574     }
1575   }
1576
1577   return (retValue);
1578 }
1579
1580
1581
1582
1583