1 /**CFile**********************************************************************
3 FileName [dddmpStoreCnf.c]
7 Synopsis [Functions to write out BDDs to file in a CNF format]
9 Description [Functions to write out BDDs to file in a CNF format.]
11 Author [Gianpiero Cabodi and Stefano Quer]
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.
26 ******************************************************************************/
31 /*-------------------------------1--------------------------------------------*/
32 /* Stucture declarations */
33 /*---------------------------------------------------------------------------*/
35 /*---------------------------------------------------------------------------*/
36 /* Type declarations */
37 /*---------------------------------------------------------------------------*/
39 /*---------------------------------------------------------------------------*/
40 /* Variable declarations */
41 /*---------------------------------------------------------------------------*/
43 #define DDDMP_DEBUG_CNF 0
45 /*---------------------------------------------------------------------------*/
46 /* Macro declarations */
47 /*---------------------------------------------------------------------------*/
49 #define GET_MAX(x,y) (x>y?x:y)
51 /**AutomaticStart*************************************************************/
53 /*---------------------------------------------------------------------------*/
54 /* Static function prototypes */
55 /*---------------------------------------------------------------------------*/
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
);
68 /**AutomaticEnd***************************************************************/
70 /*---------------------------------------------------------------------------*/
71 /* Definition of exported functions */
72 /*---------------------------------------------------------------------------*/
74 /**Function********************************************************************
76 Synopsis [Writes a dump file representing the argument BDD in
80 Description [Dumps the argument BDD to file.
81 This task is performed by calling the function
82 Dddmp_cuddBddArrayStoreCnf.
85 SideEffects [Nodes are temporarily removed from unique hash. They are
86 re-linked after the store operation in a modified order.
89 SeeAlso [Dddmp_cuddBddArrayStoreCnf]
91 ******************************************************************************/
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 */
117 retValue
= Dddmp_cuddBddArrayStoreCnf (ddMgr
, tmpArray
, 1, mode
,
118 noHeader
, varNames
, bddIds
, bddAuxIds
, cnfIds
, idInitial
, edgeInTh
,
119 pathLengthTh
, fname
, fp
, clauseNPtr
, varNewNPtr
);
121 Dddmp_CheckAndReturn (retValue
==DDDMP_FAILURE
, "Failure.");
123 return (DDDMP_SUCCESS
);
126 /**Function********************************************************************
128 Synopsis [Writes a dump file representing the argument array of BDDs
132 Description [Dumps the argument array of BDDs to file.]
134 SideEffects [Nodes are temporarily removed from the unique hash
135 table. They are re-linked after the store operation in a
137 Three methods are allowed:
138 * NodeByNode method: Insert a cut-point for each BDD node (but the
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
146 indicates the maximum number of incoming edges up to which
147 no cut point (auxiliary variable) is inserted.
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)
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
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
165 * is equal to n a cut point is inserted on path whose length is
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.
179 ******************************************************************************/
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 */
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.");
217 retValue2
= DddmpCuddBddArrayStoreCnf (ddMgr
, f
, rootN
, mode
, noHeader
,
218 varNames
, bddIds
, bddAuxIds
, cnfIds
, idInitial
, edgeInTh
, pathLengthTh
,
219 fname
, fp
, clauseNPtr
, varNewNPtr
);
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.");
236 /*---------------------------------------------------------------------------*/
237 /* Definition of internal functions */
238 /*---------------------------------------------------------------------------*/
240 /**Function********************************************************************
242 Synopsis [Writes a dump file representing the argument Array of
243 BDDs in the CNF standard format.
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
253 Iff idInitial is <= 0 its value is selected as the number of internal
255 Auxiliary variables, i.e., cut points are inserted following these
258 indicates the maximum number of incoming edges up to which
259 no cut point (auxiliary variable) is inserted.
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)
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
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
277 * is equal to n a cut point is inserted on path whose length is
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.
285 SideEffects [Nodes are temporarily removed from the unique hash table.
286 They are re-linked after the store operation in a modified
290 SeeAlso [Dddmp_cuddBddStore]
292 ******************************************************************************/
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 */
314 DdNode
*support
= 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
;
329 /*---------------------------- Set Initial Values -------------------------*/
331 support
= scan
= NULL
;
332 bddIdsInSupport
= permIdsInSupport
= rootStartLine
= NULL
;
335 sprintf (intString
, "%d", INT_MAX
);
336 intStringLength
= strlen (intString
);
338 /*---------- Check if File needs to be opened in the proper mode ----------*/
341 fp
= fopen (fname
, "w");
342 Dddmp_CheckAndGotoLabel (fp
==NULL
, "Error opening file.",
347 /*--------- Generate Bdd LOCAL IDs and Perm IDs and count them ------------*/
350 bddIdsInSupport
= DDDMP_ALLOC (int, nVar
);
351 Dddmp_CheckAndGotoLabel (bddIdsInSupport
==NULL
, "Error allocating memory.",
354 permIdsInSupport
= DDDMP_ALLOC (int, nVar
);
355 Dddmp_CheckAndGotoLabel (permIdsInSupport
==NULL
, "Error allocating memory.",
357 /* Support Size (Number of BDD Ids-PermIds */
360 for (i
=0; i
<nVar
; i
++) {
361 bddIdsInSupport
[i
] = permIdsInSupport
[i
] = (-1);
365 * Take the union of the supports of each output function.
366 * Skip NULL functions.
370 for (i
=0; i
<rootN
; i
++) {
374 support
= Cudd_Support (ddMgr
, f
[i
]);
375 Dddmp_CheckAndGotoLabel (support
==NULL
, "NULL support returned.",
379 while (!cuddIsConstant(scan
)) {
380 /* Count Number of Variable in the Support */
382 /* Set Ids and Perm-Ids */
383 bddIdsInSupport
[scan
->index
] = scan
->index
;
384 permIdsInSupport
[scan
->index
] = ddMgr
->perm
[scan
->index
];
387 Cudd_RecursiveDeref (ddMgr
, support
);
389 /* so that we do not try to free it in case of failure */
392 /*---------------------------- Start HEADER -------------------------------*/
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.",
400 fprintf (fp
, "c #\n");
403 /*-------------------- Generate Bdd IDs IFF necessary ---------------------*/
405 if (bddIds
== NULL
) {
407 fprintf (fp
, "c # Warning: BDD IDs missing ... evaluating them.\n");
408 fprintf (fp
, "c # \n");
413 bddIds
= DDDMP_ALLOC (int, nVar
);
414 Dddmp_CheckAndGotoLabel (bddIds
==NULL
, "Error allocating memory.",
417 /* Get BDD-IDs Directly from Cudd Manager */
418 for (i
=0; i
<nVar
; i
++) {
421 } /* end if bddIds == NULL */
423 /*------------------ Generate AUX BDD IDs IF necessary --------------------*/
425 if (bddAuxIds
== NULL
) {
427 fprintf (fp
, "c # Warning: AUX IDs missing ... equal to BDD IDs.\n");
428 fprintf (fp
, "c #\n");
433 bddAuxIds
= DDDMP_ALLOC (int, nVar
);
434 Dddmp_CheckAndGotoLabel (bddAuxIds
==NULL
, "Error allocating memory.",
437 for (i
=0; i
<nVar
; i
++) {
438 bddAuxIds
[i
] = bddIds
[i
];
440 } /* end if cnfIds == NULL */
442 /*------------------- Generate CNF IDs IF necessary -----------------------*/
444 if (cnfIds
== NULL
) {
446 fprintf (fp
, "c # Warning: CNF IDs missing ... equal to BDD IDs.\n");
447 fprintf (fp
, "c #\n");
452 cnfIds
= DDDMP_ALLOC (int, nVar
);
453 Dddmp_CheckAndGotoLabel (cnfIds
==NULL
, "Error allocating memory.",
456 for (i
=0; i
<nVar
; i
++) {
457 cnfIds
[i
] = bddIds
[i
] + 1;
459 } /* end if cnfIds == NULL */
461 /*------------------ Generate Var Names IF necessary ----------------------*/
464 if (varNames
== NULL
) {
467 "c # Warning: null variable names ... create DUMMY names.\n");
468 fprintf (fp
, "c #\n");
473 varNames
= DDDMP_ALLOC (char *, nVar
);
474 for (i
=0; i
<nVar
; i
++) {
477 Dddmp_CheckAndGotoLabel (varNames
==NULL
, "Error allocating memory.",
482 /* Protect the user also from partially loaded varNames array !!! */
483 for (i
=0; i
<nVar
&& flagVar
==0; i
++) {
484 if (varNames
[i
] == NULL
) {
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
);
500 /*----------------------- Set Initial ID IF necessary --------------------*/
502 if (idInitial
<= 0) {
503 idInitial
= nVar
+ 1;
506 /*--------------------------- Continue HEADER -----------------------------*/
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
);
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
]);
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
]);
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
]);
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
]);
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
]);
562 fprintf (fp
, "c .cnfids ");
563 for (i
=0; i
<nVar
; i
++) {
564 if (bddIdsInSupport
[i
] >= 0) {
565 fprintf (fp
, " %d", cnfIds
[i
]);
570 /* Number of Roots */
571 fprintf (fp
, "c .nroots %d", rootN
);
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
, " ");
582 retValue
= fprintf (fp
, "\n");
585 } /* End of noHeader check */
587 /*------------ Select Mode and Print Number of Tmp Var Created ------------*/
590 case DDDMP_CNF_MODE_NODE
:
591 *varNewNPtr
= idInitial
;
592 *varNewNPtr
= DddmpNumberDdNodesCnf (ddMgr
, f
, rootN
, cnfIds
, idInitial
)
595 case DDDMP_CNF_MODE_MAXTERM
:
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
;
607 /*------------ Print Space for Number of Variable and Clauses -------------*/
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
, " ");
619 retValue
= fprintf (fp
, "\n");
623 /*---------------------- Select Mode and Do the Job -----------------------*/
627 rootStartLine
= DDDMP_ALLOC (int, rootN
);
628 Dddmp_CheckAndGotoLabel (rootStartLine
==NULL
, "Error allocating memory.",
630 for (i
=0; i
<rootN
; i
++) {
631 rootStartLine
[i
] = (-1);
635 case DDDMP_CNF_MODE_NODE
:
636 StoreCnfNodeByNode (ddMgr
, f
, rootN
, bddIds
, cnfIds
, fp
, &clauseN
,
637 &varMax
, rootStartLine
);
638 DddmpUnnumberDdNodesCnf (ddMgr
, f
, rootN
);
640 case DDDMP_CNF_MODE_MAXTERM
:
641 StoreCnfMaxtermByMaxterm (ddMgr
, f
, rootN
, bddIds
, cnfIds
, idInitial
,
642 fp
, &varMax
, &clauseN
, rootStartLine
);
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
);
653 /*------------------------------ Write trailer ----------------------------*/
656 retValue
= fprintf (fp
, "c # End of Cnf From dddmp-2.0\n");
657 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
662 * Write Root Starting Line
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
, " ");
675 retValue
= fprintf (fp
, "%s", tmpString
);
677 retValue
= fprintf (fp
, "\n");
682 * Write Number of clauses and variable in the header
685 *clauseNPtr
= clauseN
;
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
, " ");
694 retValue
= fprintf (fp
, "%s\n", tmpString
);
698 /*-------------------------- Close file and return ------------------------*/
704 DDDMP_FREE (bddIdsInSupport
);
705 DDDMP_FREE (permIdsInSupport
);
706 DDDMP_FREE (rootStartLine
);
707 if (bddIdsToFree
== 1) {
710 if (bddAuxIdsToFree
== 1) {
711 DDDMP_FREE (bddAuxIds
);
713 if (cnfIdsToFree
== 1) {
716 if (varNamesToFree
== 1) {
717 for (i
=0; i
<nVar
; i
++) {
718 DDDMP_FREE (varNames
[i
]);
720 DDDMP_FREE (varNames
);
723 return (DDDMP_SUCCESS
);
727 if (support
!= NULL
) {
728 Cudd_RecursiveDeref (ddMgr
, support
);
730 DDDMP_FREE (bddIdsInSupport
);
731 DDDMP_FREE (permIdsInSupport
);
732 DDDMP_FREE (rootStartLine
);
733 if (bddIdsToFree
== 1) {
736 if (bddAuxIdsToFree
== 1) {
737 DDDMP_FREE (bddAuxIds
);
739 if (cnfIdsToFree
== 1) {
742 if (varNamesToFree
== 1) {
743 for (i
=0; i
<nVar
; i
++) {
744 DDDMP_FREE (varNames
[i
]);
746 DDDMP_FREE (varNames
);
749 return (DDDMP_FAILURE
);
752 /*---------------------------------------------------------------------------*/
753 /* Definition of static functions */
754 /*---------------------------------------------------------------------------*/
756 /**Function********************************************************************
758 Synopsis [Store the BDD as CNF clauses.]
760 Description [Store the BDD as CNF clauses.
761 Use a multiplexer description for each BDD node.
768 ******************************************************************************/
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 */
786 for (i
=0; i
<rootN
; i
++) {
788 if (!cuddIsConstant(Cudd_Regular (f
[i
]))) {
790 * Set Starting Line for this Root
793 rootStartLine
[i
] = *clauseN
+ 1;
799 retValue
= StoreCnfNodeByNodeRecur (ddMgr
, Cudd_Regular(f
[i
]),
800 bddIds
, cnfIds
, fp
, clauseN
, varMax
);
802 (void) fprintf (stderr
,
803 "DdStoreCnf: Error in recursive node store\n");
808 * Store CNF for the root if necessary
811 idf
= DddmpReadNodeIndexCnf (Cudd_Regular (f
[i
]));
813 retValue
= fprintf (fp
, "root %d --> \n", i
);
815 if (Cudd_IsComplement (f
[i
])) {
816 retValue
= fprintf (fp
, "-%d 0\n", idf
);
818 retValue
= fprintf (fp
, "%d 0\n", idf
);
820 *varMax
= GET_MAX (*varMax
, idf
);
821 *clauseN
= *clauseN
+ 1;
823 if (retValue
== EOF
) {
824 (void) fprintf (stderr
,
825 "DdStoreCnf: Error in recursive node store\n");
835 /**Function********************************************************************
837 Synopsis [Performs the recursive step of Dddmp_bddStore.]
839 Description [Performs the recursive step of Dddmp_bddStore.
840 Traverse the BDD and store a CNF formula for each "terminal" node.
847 ******************************************************************************/
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 */
861 int idf
, idT
, idE
, vf
;
865 assert(!Cudd_IsComplement(f
));
869 /* If constant, nothing to do. */
870 if (Cudd_IsConstant(f
)) {
874 /* If already visited, nothing to do. */
875 if (DddmpVisitedCnf (f
)) {
879 /* Mark node as visited. */
880 DddmpSetVisitedCnf (f
);
882 /*------------------ Non Terminal Node -------------------------------*/
885 /* BDDs! Only one constant supported */
886 assert (!cuddIsConstant(f
));
890 * Recursive call for Then edge
895 /* ROBDDs! No complemented Then edge */
896 assert (!Cudd_IsComplement(T
));
899 retValue
= StoreCnfNodeByNodeRecur (ddMgr
, T
, bddIds
, cnfIds
, fp
,
906 * Recursive call for Else edge
909 E
= Cudd_Regular (cuddE (f
));
910 retValue
= StoreCnfNodeByNodeRecur (ddMgr
, E
, bddIds
, cnfIds
, fp
,
917 * Obtain nodeids and variable ids of f, T, E
920 idf
= DddmpReadNodeIndexCnf (f
);
923 if (bddIds
[vf
] != vf
) {
924 (void) fprintf (stderr
, "DdStoreCnf: Error writing to file\n");
929 idT
= DddmpReadNodeIndexCnf (T
);
931 idE
= DddmpReadNodeIndexCnf (E
);
932 if (Cudd_IsComplement (cuddE (f
))) {
936 retValue
= StoreCnfOneNode (f
, idf
, cnfIds
[vf
], idT
, idE
, fp
,
939 if (retValue
== EOF
) {
946 /**Function********************************************************************
948 Synopsis [Store One Single BDD Node.]
950 Description [Store One Single BDD Node translating it as a multiplexer.]
956 ******************************************************************************/
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 */
971 int idfAbs
, idTAbs
, idEAbs
;
977 /*----------------------------- Check for Constant ------------------------*/
979 assert(!Cudd_IsConstant(f
));
981 /*------------------------- Check for terminal nodes ----------------------*/
983 if ((idTAbs
==1) && (idEAbs
==1)) {
987 /*------------------------------ Internal Node ----------------------------*/
990 retValue
= fprintf (fp
, "id=%d var=%d idT=%d idE=%d\n",
998 if ((idTAbs
==1) && (idEAbs
!=1)) {
1000 retValue
= fprintf (fp
, "CASE 1 -->\n");
1002 retValue
= fprintf (fp
, "%d %d 0\n",
1004 retValue
= fprintf (fp
, "%d %d 0\n",
1006 retValue
= fprintf (fp
, "%d %d %d 0\n",
1008 *clauseN
= *clauseN
+ 3;
1010 *varMax
= GET_MAX (*varMax
, idfAbs
);
1011 *varMax
= GET_MAX (*varMax
, vf
);
1012 *varMax
= GET_MAX (*varMax
, idEAbs
);
1019 if ((idTAbs
!=1) && (idEAbs
==1)) {
1022 retValue
= fprintf (fp
, "CASE 2 -->\n");
1024 retValue
= fprintf (fp
, "%d %d 0\n",
1026 retValue
= fprintf (fp
, "%d %d 0\n",
1028 retValue
= fprintf (fp
, "%d %d %d 0\n",
1032 retValue
= fprintf (fp
, "CASE 3 -->\n");
1034 retValue
= fprintf (fp
, "%d %d 0\n",
1036 retValue
= fprintf (fp
, "%d %d 0\n",
1038 retValue
= fprintf (fp
, "%d %d %d 0\n",
1042 *varMax
= GET_MAX (*varMax
, idfAbs
);
1043 *varMax
= GET_MAX (*varMax
, vf
);
1044 *varMax
= GET_MAX (*varMax
, idTAbs
);
1046 *clauseN
= *clauseN
+ 3;
1050 * Nor Then or Else to terminal
1053 if ((idTAbs
!=1) && (idEAbs
!=1)) {
1055 retValue
= fprintf (fp
, "CASE 4 -->\n");
1057 retValue
= fprintf (fp
, "%d %d %d 0\n",
1059 retValue
= fprintf (fp
, "%d %d %d 0\n",
1061 retValue
= fprintf (fp
, "%d %d %d 0\n",
1063 retValue
= fprintf (fp
, "%d %d %d 0\n",
1066 *varMax
= GET_MAX (*varMax
, idfAbs
);
1067 *varMax
= GET_MAX (*varMax
, vf
);
1068 *varMax
= GET_MAX (*varMax
, idTAbs
);
1069 *varMax
= GET_MAX (*varMax
, idEAbs
);
1071 *clauseN
= *clauseN
+ 4;
1077 /**Function********************************************************************
1079 Synopsis [Prints a disjoint sum of products.]
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.
1090 SeeAlso [StoreCnfBest]
1092 ******************************************************************************/
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 */
1110 list
= DDDMP_ALLOC (int, ddMgr
->size
);
1112 ddMgr
->errorCode
= CUDD_MEMORY_OUT
;
1113 return (DDDMP_FAILURE
);
1116 for (i
=0; i
<rootN
; i
++) {
1118 if (!cuddIsConstant(Cudd_Regular (f
[i
]))) {
1119 for (j
=0; j
<ddMgr
->size
; j
++) {
1124 * Set Starting Line for this Root
1127 rootStartLine
[i
] = *clauseN
+ 1;
1129 StoreCnfMaxtermByMaxtermRecur (ddMgr
, f
[i
], bddIds
, cnfIds
, fp
,
1130 list
, clauseN
, varMax
);
1140 /**Function********************************************************************
1142 Synopsis [Prints a disjoint sum of products with intermediate
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.
1155 SeeAlso [StoreCnfMaxtermByMaxterm]
1157 ******************************************************************************/
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 */
1175 list
= DDDMP_ALLOC (int, ddMgr
->size
);
1177 ddMgr
->errorCode
= CUDD_MEMORY_OUT
;
1178 return (DDDMP_FAILURE
);
1181 for (i
=0; i
<rootN
; i
++) {
1183 if (!cuddIsConstant(Cudd_Regular (f
[i
]))) {
1184 for (j
=0; j
<ddMgr
->size
; j
++) {
1189 * Set Starting Line for this Root
1192 rootStartLine
[i
] = *clauseN
+ 1;
1195 fprintf (fp
, "root NOT shared BDDs %d --> \n", i
);
1197 StoreCnfBestNotSharedRecur (ddMgr
, f
[i
], 0, bddIds
, cnfIds
, fp
, list
,
1201 fprintf (fp
, "root SHARED BDDs %d --> \n", i
);
1203 StoreCnfBestSharedRecur (ddMgr
, Cudd_Regular (f
[i
]), bddIds
, cnfIds
,
1204 fp
, list
, clauseN
, varMax
);
1210 fprintf (stdout
, "###---> BDDs After the Storing Process:\n");
1211 DddmpPrintBddAndNext (ddMgr
, f
, rootN
);
1216 return (DDDMP_SUCCESS
);
1219 /**Function********************************************************************
1221 Synopsis [Performs the recursive step of Print Maxterm.]
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
1232 ******************************************************************************/
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 */
1246 DdNode
*N
, *Nv
, *Nnv
;
1247 int retValue
, index
;
1249 N
= Cudd_Regular (node
);
1252 * Terminal case: Print one cube based on the current recursion
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;
1265 * NON Terminal case: Recur
1270 if (Cudd_IsComplement (node
)) {
1272 Nnv
= Cudd_Not (Nnv
);
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
1283 if (cuddIsConstant (Cudd_Regular (Nv
)) && Nv
!= ddMgr
->one
) {
1288 StoreCnfMaxtermByMaxtermRecur (ddMgr
, Nnv
, bddIds
, cnfIds
, fp
, list
,
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
1298 if (cuddIsConstant (Cudd_Regular (Nnv
)) && Nnv
!= ddMgr
->one
) {
1303 StoreCnfMaxtermByMaxtermRecur (ddMgr
, Nv
, bddIds
, cnfIds
, fp
, list
,
1310 /**Function********************************************************************
1312 Synopsis [Performs the recursive step of Print Best on Not Shared
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).
1324 ******************************************************************************/
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 */
1339 DdNode
*N
, *Nv
, *Nnv
;
1340 int index
, retValue
;
1345 N
= Cudd_Regular (node
);
1348 * Terminal case or Already Visited:
1349 * Print one cube based on the current recursion
1352 if (cuddIsConstant (N
)) {
1353 retValue
= printCubeCnf (ddMgr
, node
, cnfIds
, fp
, list
, varMax
);
1354 if (retValue
== DDDMP_SUCCESS
) {
1356 fprintf (fp
, "%d ", idf
);
1358 fprintf (fp
, "0\n");
1359 *varMax
= GET_MAX (*varMax
, abs(idf
));
1360 *clauseN
= *clauseN
+ 1;
1362 return (DDDMP_SUCCESS
);
1366 * Shared Sub-Tree: Print Cube
1369 index
= DddmpReadNodeIndexCnf (N
);
1372 fprintf (fp
, "%d ", idf
);
1374 if (Cudd_IsComplement (node
)) {
1375 retValue
= fprintf (fp
, "-%d ", index
);
1377 retValue
= fprintf (fp
, "%d ", index
);
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
);
1387 * NON Terminal case: Recur
1392 if (Cudd_IsComplement (node
)) {
1394 Nnv
= Cudd_Not (Nnv
);
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
1405 if (cuddIsConstant (Cudd_Regular (Nv
)) && Nv
!= ddMgr
->one
) {
1410 StoreCnfBestNotSharedRecur (ddMgr
, Nnv
, idf
, bddIds
, cnfIds
, fp
, list
,
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
1420 if (cuddIsConstant (Cudd_Regular (Nnv
)) && Nnv
!= ddMgr
->one
) {
1425 StoreCnfBestNotSharedRecur (ddMgr
, Nv
, idf
, bddIds
, cnfIds
, fp
, list
,
1429 return (DDDMP_SUCCESS
);
1432 /**Function********************************************************************
1434 Synopsis [Performs the recursive step of Print Best on Shared
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).
1447 ******************************************************************************/
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 */
1461 DdNode
*nodeThen
, *nodeElse
;
1467 Dddmp_Assert (node
==Cudd_Regular(node
),
1468 "Inverted Edge during Shared Printing.");
1470 /* If constant, nothing to do. */
1471 if (cuddIsConstant (node
)) {
1472 return (DDDMP_SUCCESS
);
1475 /* If already visited, nothing to do. */
1476 if (DddmpVisitedCnf (node
)) {
1477 return (DDDMP_SUCCESS
);
1481 * Shared Sub-Tree: Print Cube
1484 idf
= DddmpReadNodeIndexCnf (node
);
1486 /* Cheat the Recur Function about the Index of the Current Node */
1487 DddmpWriteNodeIndexCnf (node
, 0);
1490 fprintf (fp
, "Else of XNOR\n");
1492 for (i
=0; i
<ddMgr
->size
; i
++) {
1495 StoreCnfBestNotSharedRecur (ddMgr
, Cudd_Not (node
), idf
, bddIds
, cnfIds
,
1496 fp
, list
, clauseN
, varMax
);
1499 fprintf (fp
, "Then of XNOR\n");
1501 for (i
=0; i
<ddMgr
->size
; i
++) {
1504 StoreCnfBestNotSharedRecur (ddMgr
, node
, -idf
, bddIds
, cnfIds
,
1505 fp
, list
, clauseN
, varMax
);
1507 /* Set Back Index of Current Node */
1508 DddmpWriteNodeIndexCnf (node
, idf
);
1511 /* Mark node as visited. */
1512 DddmpSetVisitedCnf (node
);
1518 nodeThen
= cuddT (node
);
1519 nodeElse
= cuddE (node
);
1520 index
= node
->index
;
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
);
1527 return (DDDMP_SUCCESS
);
1530 /**Function********************************************************************
1532 Synopsis [Print One Cube in CNF Format.]
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.
1543 ******************************************************************************/
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 */
1558 retValue
= DDDMP_FAILURE
;
1562 for (i
=0; i
<ddMgr
->size
; i
++) {
1564 retValue
= DDDMP_SUCCESS
;
1565 (void) fprintf (fp
, "%d ", cnfIds
[i
]);
1566 *varMax
= GET_MAX(*varMax
, cnfIds
[i
]);
1569 retValue
= DDDMP_SUCCESS
;
1570 (void) fprintf (fp
, "-%d ", cnfIds
[i
]);
1571 *varMax
= GET_MAX(*varMax
, cnfIds
[i
]);