source: icGREP/icgrep-devel/cudd-2.5.1/dddmp/dddmpStoreCnf.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: 46.9 KB
Line 
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
57static 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);
58static int StoreCnfNodeByNode(DdManager *ddMgr, DdNode **f, int rootN, int *bddIds, int *cnfIds, FILE *fp, int *clauseN, int *varMax, int *rootStartLine);
59static int StoreCnfNodeByNodeRecur(DdManager *ddMgr, DdNode *f, int *bddIds, int *cnfIds, FILE *fp, int *clauseN, int *varMax);
60static int StoreCnfOneNode(DdNode *f, int idf, int vf, int idT, int idE, FILE *fp, int *clauseN, int *varMax);
61static int StoreCnfMaxtermByMaxterm(DdManager *ddMgr, DdNode **f, int rootN, int *bddIds, int *cnfIds, int idInitial, FILE *fp, int *varMax, int *clauseN, int *rootStartLine);
62static int StoreCnfBest(DdManager *ddMgr, DdNode **f, int rootN, int *bddIds, int *cnfIds, int idInitial, FILE *fp, int *varMax, int *clauseN, int *rootStartLine);
63static void StoreCnfMaxtermByMaxtermRecur(DdManager *ddMgr, DdNode *node, int *bddIds, int *cnfIds, FILE *fp, int *list, int *clauseN, int *varMax);
64static int StoreCnfBestNotSharedRecur(DdManager *ddMgr, DdNode *node, int idf, int *bddIds, int *cnfIds, FILE *fp, int *list, int *clauseN, int *varMax);
65static int StoreCnfBestSharedRecur(DdManager *ddMgr, DdNode *node, int *bddIds, int *cnfIds, FILE *fp, int *list, int *clauseN, int *varMax);
66static 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
93int
94Dddmp_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
181int
182Dddmp_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
294static int
295DddmpCuddBddArrayStoreCnf (
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
770static int
771StoreCnfNodeByNode (
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
849static int
850StoreCnfNodeByNodeRecur (
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
958static int
959StoreCnfOneNode (
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
1094static int
1095StoreCnfMaxtermByMaxterm (
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
1159static int
1160StoreCnfBest (
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
1234static void
1235StoreCnfMaxtermByMaxtermRecur (
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
1326static int
1327StoreCnfBestNotSharedRecur (
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
1449static int
1450StoreCnfBestSharedRecur (
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
1545static int
1546printCubeCnf (
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
Note: See TracBrowser for help on using the repository browser.