1 /**CFile**********************************************************************
3 FileName [dddmpStoreBdd.c]
7 Synopsis [Functions to write BDDs to file.]
9 Description [Functions to write BDDs to file.
10 BDDs are represended on file either in text or binary format under the
11 following rules. A file contains a forest of BDDs (a vector of
12 Boolean functions). BDD nodes are numbered with contiguous numbers,
13 from 1 to NNodes (total number of nodes on a file). 0 is not used to
14 allow negative node indexes for complemented edges. A file contains
15 a header, including information about variables and roots to BDD
16 functions, followed by the list of nodes. BDD nodes are listed
17 according to their numbering, and in the present implementation
18 numbering follows a post-order strategy, in such a way that a node
19 is never listed before its Then/Else children.
22 Author [Gianpiero Cabodi and Stefano Quer]
25 Copyright (c) 2004 by Politecnico di Torino.
26 All Rights Reserved. This software is for educational purposes only.
27 Permission is given to academic institutions to use, copy, and modify
28 this software and its documentation provided that this introductory
29 message is not removed, that this software and its documentation is
30 used for the institutions' internal research and educational purposes,
31 and that no monies are exchanged. No guarantee is expressed or implied
32 by the distribution of this code.
33 Send bug-reports and/or questions to:
34 {gianpiero.cabodi,stefano.quer}@polito.it.
37 ******************************************************************************/
41 /*---------------------------------------------------------------------------*/
42 /* Stucture declarations */
43 /*---------------------------------------------------------------------------*/
45 /*---------------------------------------------------------------------------*/
46 /* Type declarations */
47 /*---------------------------------------------------------------------------*/
49 /*---------------------------------------------------------------------------*/
50 /* Variable declarations */
51 /*---------------------------------------------------------------------------*/
53 /*---------------------------------------------------------------------------*/
54 /* Macro declarations */
55 /*---------------------------------------------------------------------------*/
57 /**AutomaticStart*************************************************************/
59 /*---------------------------------------------------------------------------*/
60 /* Static function prototypes */
61 /*---------------------------------------------------------------------------*/
63 static int NodeStoreRecurBdd(DdManager
*ddMgr
, DdNode
*f
, int mode
, int *supportids
, char **varnames
, int *outids
, FILE *fp
);
64 static int NodeTextStoreBdd(DdManager
*ddMgr
, DdNode
*f
, int mode
, int *supportids
, char **varnames
, int *outids
, FILE *fp
, int idf
, int vf
, int idT
, int idE
);
65 static int NodeBinaryStoreBdd(DdManager
*ddMgr
, DdNode
*f
, int mode
, int *supportids
, char **varnames
, int *outids
, FILE *fp
, int idf
, int vf
, int idT
, int idE
, int vT
, int vE
, DdNode
*T
, DdNode
*E
);
67 /**AutomaticEnd***************************************************************/
69 /*---------------------------------------------------------------------------*/
70 /* Definition of exported functions */
71 /*---------------------------------------------------------------------------*/
73 /**Function********************************************************************
75 Synopsis [Writes a dump file representing the argument BDD.]
77 Description [Dumps the argument BDD to file. Dumping is done through
78 Dddmp_cuddBddArrayStore. A dummy array of 1 BDD root is
79 used for this purpose.
82 SideEffects [Nodes are temporarily removed from unique hash. They are
83 re-linked after the store operation in a modified order.
86 SeeAlso [Dddmp_cuddBddLoad Dddmp_cuddBddArrayLoad]
88 ******************************************************************************/
92 DdManager
*ddMgr
/* IN: DD Manager */,
93 char *ddname
/* IN: DD name (or NULL) */,
94 DdNode
*f
/* IN: BDD root to be stored */,
95 char **varnames
/* IN: array of variable names (or NULL) */,
96 int *auxids
/* IN: array of converted var ids */,
97 int mode
/* IN: storing mode selector */,
98 Dddmp_VarInfoType varinfo
/* IN: extra info for variables in text mode */,
99 char *fname
/* IN: File name */,
100 FILE *fp
/* IN: File pointer to the store file */
108 retValue
= Dddmp_cuddBddArrayStore (ddMgr
,ddname
,1,tmpArray
,NULL
,
109 varnames
, auxids
, mode
, varinfo
, fname
, fp
);
114 /**Function********************************************************************
116 Synopsis [Writes a dump file representing the argument Array of BDDs.]
118 Description [Dumps the argument array of BDDs to file. Dumping is either
119 in text or binary form. BDDs are stored to the fp (already
120 open) file if not NULL. Otherwise the file whose name is
121 fname is opened in write mode. The header has the same format
122 for both textual and binary dump. Names are allowed for input
123 variables (vnames) and for represented functions (rnames).
124 For sake of generality and because of dynamic variable
125 ordering both variable IDs and permuted IDs are included.
126 New IDs are also supported (auxids). Variables are identified
127 with incremental numbers. according with their positiom in
128 the support set. In text mode, an extra info may be added,
129 chosen among the following options: name, ID, PermID, or an
130 auxiliary id. Since conversion from DD pointers to integers
131 is required, DD nodes are temporarily removed from the unique
132 hash table. This allows the use of the next field to store
136 SideEffects [Nodes are temporarily removed from the unique hash
137 table. They are re-linked after the store operation in a
141 SeeAlso [Dddmp_cuddBddStore, Dddmp_cuddBddLoad,
142 Dddmp_cuddBddArrayLoad
145 ******************************************************************************/
148 Dddmp_cuddBddArrayStore (
149 DdManager
*ddMgr
/* IN: DD Manager */,
150 char *ddname
/* IN: dd name (or NULL) */,
151 int nRoots
/* IN: number of output BDD roots to be stored */,
152 DdNode
**f
/* IN: array of BDD roots to be stored */,
153 char **rootnames
/* IN: array of root names (or NULL) */,
154 char **varnames
/* IN: array of variable names (or NULL) */,
155 int *auxids
/* IN: array of converted var IDs */,
156 int mode
/* IN: storing mode selector */,
157 Dddmp_VarInfoType varinfo
/* IN: extra info for variables in text mode */,
158 char *fname
/* IN: File name */,
159 FILE *fp
/* IN: File pointer to the store file */
168 retValueBis
= Cudd_DebugCheck (ddMgr
);
169 if (retValueBis
== 1) {
170 fprintf (stderr
, "Inconsistency Found During BDD Store.\n");
173 if (retValueBis
== CUDD_OUT_OF_MEM
) {
174 fprintf (stderr
, "Out of Memory During BDD Store.\n");
181 retValue
= DddmpCuddBddArrayStore (DDDMP_BDD
, ddMgr
, ddname
, nRoots
, f
,
182 rootnames
, varnames
, auxids
, mode
, varinfo
, fname
, fp
);
186 retValueBis
= Cudd_DebugCheck (ddMgr
);
187 if (retValueBis
== 1) {
188 fprintf (stderr
, "Inconsistency Found During BDD Store.\n");
191 if (retValueBis
== CUDD_OUT_OF_MEM
) {
192 fprintf (stderr
, "Out of Memory During BDD Store.\n");
202 /*---------------------------------------------------------------------------*/
203 /* Definition of internal functions */
204 /*---------------------------------------------------------------------------*/
206 /**Function********************************************************************
208 Synopsis [Writes a dump file representing the argument Array of
212 Description [Dumps the argument array of BDDs to file.
213 Internal function doing inner steps of store for BDDs.
216 SideEffects [Nodes are temporarily removed from the unique hash
217 table. They are re-linked after the store operation in a
221 SeeAlso [Dddmp_cuddBddStore, Dddmp_cuddBddLoad,
222 Dddmp_cuddBddArrayLoad
225 ******************************************************************************/
228 DddmpCuddBddArrayStore (
229 Dddmp_DecompType ddType
/* IN: Selects the decomp type BDD */,
230 DdManager
*ddMgr
/* IN: DD Manager */,
231 char *ddname
/* IN: DD name (or NULL) */,
232 int nRoots
/* IN: number of output BDD roots to be stored */,
233 DdNode
**f
/* IN: array of DD roots to be stored */,
234 char **rootnames
/* IN: array of root names (or NULL) */,
235 char **varnames
/* IN: array of variable names (or NULL) */,
236 int *auxids
/* IN: array of converted var IDs */,
237 int mode
/* IN: storing mode selector */,
238 Dddmp_VarInfoType varinfo
/* IN: extra info for variables in text mode */,
239 char *fname
/* IN: File name */,
240 FILE *fp
/* IN: File pointer to the store file */
243 DdNode
*support
= NULL
;
247 int *invpermids
= NULL
;
248 int *supportids
= NULL
;
250 char **outvarnames
= NULL
;
251 int nVars
= ddMgr
->size
;
261 Dddmp_CheckAndGotoLabel (ddType
==DDDMP_ADD
,
262 "Error writing to file: ADD Type.", failure
);
265 * Check if File needs to be opened in the proper mode.
269 fp
= fopen (fname
, "w");
270 Dddmp_CheckAndGotoLabel (fp
==NULL
, "Error opening file.",
276 * Force binary mode if automatic.
280 case DDDMP_MODE_TEXT
:
281 case DDDMP_MODE_BINARY
:
283 case DDDMP_MODE_DEFAULT
:
284 mode
= DDDMP_MODE_BINARY
;
287 mode
= DDDMP_MODE_BINARY
;
292 * Alloc vectors for variable IDs, perm IDs and support IDs.
293 * +1 to include a slot for terminals.
296 ids
= DDDMP_ALLOC (int, nVars
);
297 Dddmp_CheckAndGotoLabel (ids
==NULL
, "Error allocating memory.", failure
);
298 permids
= DDDMP_ALLOC (int, nVars
);
299 Dddmp_CheckAndGotoLabel (permids
==NULL
, "Error allocating memory.", failure
);
300 invpermids
= DDDMP_ALLOC (int, nVars
);
301 Dddmp_CheckAndGotoLabel (invpermids
==NULL
, "Error allocating memory.",
303 supportids
= DDDMP_ALLOC (int, nVars
+1);
304 Dddmp_CheckAndGotoLabel (supportids
==NULL
, "Error allocating memory.",
307 for (i
=0; i
<nVars
; i
++) {
308 ids
[i
] = permids
[i
] = invpermids
[i
] = supportids
[i
] = (-1);
311 supportids
[nVars
] = -1;
314 * Take the union of the supports of each output function.
315 * skip NULL functions.
316 * Set permids and invpermids of support variables to the proper values.
319 for (i
=0; i
<nRoots
; i
++) {
323 support
= Cudd_Support (ddMgr
, f
[i
]);
324 Dddmp_CheckAndGotoLabel (support
==NULL
, "NULL support returned.",
328 while (!cuddIsConstant(scan
)) {
329 ids
[scan
->index
] = scan
->index
;
330 permids
[scan
->index
] = ddMgr
->perm
[scan
->index
];
331 invpermids
[ddMgr
->perm
[scan
->index
]] = scan
->index
;
334 Cudd_RecursiveDeref (ddMgr
, support
);
336 /* so that we do not try to free it in case of failure */
340 * Set supportids to incremental (shrinked) values following the ordering.
343 for (i
=0, var
=0; i
<nVars
; i
++) {
344 if (invpermids
[i
] >= 0) {
345 supportids
[invpermids
[i
]] = var
++;
348 /* set a dummy id for terminal nodes */
349 supportids
[nVars
] = var
;
352 * Select conversion array for extra var info
356 case DDDMP_MODE_TEXT
:
361 case DDDMP_VARPERMIDS
:
364 case DDDMP_VARAUXIDS
:
368 outvarnames
= varnames
;
370 case DDDMP_VARDEFAULT
:
374 case DDDMP_MODE_BINARY
:
380 * Number dd nodes and count them (numbering is from 1 to nnodes)
383 nnodes
= DddmpNumberBddNodes (ddMgr
, f
, nRoots
);
390 retValue
= fprintf (fp
, ".ver %s\n", DDDMP_VERSION
);
391 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
395 retValue
= fprintf (fp
, ".mode %c\n", mode
);
396 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
399 if (mode
== DDDMP_MODE_TEXT
) {
400 retValue
= fprintf (fp
, ".varinfo %d\n", varinfo
);
401 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
405 if (ddname
!= NULL
) {
406 retValue
= fprintf (fp
, ".dd %s\n",ddname
);
407 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
411 retValue
= fprintf (fp
, ".nnodes %d\n", nnodes
);
412 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
415 retValue
= fprintf (fp
, ".nvars %d\n", nVars
);
416 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
419 retValue
= fprintf (fp
, ".nsuppvars %d\n", var
);
420 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
423 /*------------ Write the Var Names by scanning the ids array -------------*/
425 if (varnames
!= NULL
) {
427 retValue
= fprintf (fp
, ".suppvarnames");
428 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
431 for (i
=0; i
<nVars
; i
++) {
433 if (varnames
[ids
[i
]] == NULL
) {
434 (void) fprintf (stderr
,
435 "DdStore Warning: null variable name. DUMMY%d generated\n", i
);
437 varnames
[ids
[i
]] = DDDMP_ALLOC (char, 10);
438 Dddmp_CheckAndGotoLabel (varnames
[ids
[i
]] == NULL
,
439 "Error allocating memory.", failure
);
440 sprintf (varnames
[ids
[i
]], "DUMMY%d", i
);
442 retValue
= fprintf (fp
, " %s", varnames
[ids
[i
]]);
443 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
448 retValue
= fprintf (fp
, "\n");
449 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
453 /*--------- Write the Var SUPPORT Names by scanning the ids array ---------*/
455 if (varnames
!= NULL
) {
456 retValue
= fprintf (fp
, ".orderedvarnames");
457 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
460 for (i
=0; i
<nVars
; i
++) {
461 if (varnames
[ddMgr
->invperm
[i
]] == NULL
) {
462 (void) fprintf (stderr
,
463 "DdStore Warning: null variable name. DUMMY%d generated\n", i
);
465 varnames
[ddMgr
->invperm
[i
]] = DDDMP_ALLOC (char, 10);
466 Dddmp_CheckAndGotoLabel (varnames
[ddMgr
->invperm
[i
]] == NULL
,
467 "Error allocating memory.", failure
);
468 sprintf (varnames
[ddMgr
->invperm
[i
]], "DUMMY%d", i
);
471 retValue
= fprintf (fp
, " %s", varnames
[ddMgr
->invperm
[i
]]);
472 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
476 retValue
= fprintf (fp
, "\n");
477 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
481 /*------------ Write the var ids by scanning the ids array ---------------*/
483 retValue
= fprintf (fp
, ".ids");
484 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
487 for (i
=0; i
<nVars
; i
++) {
489 retValue
= fprintf (fp
, " %d", i
);
490 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
494 retValue
= fprintf (fp
, "\n");
495 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
499 * Write the var permids by scanning the permids array.
502 retValue
= fprintf (fp
, ".permids");
503 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
505 for (i
= 0; i
< nVars
; i
++) {
506 if (permids
[i
] >= 0) {
507 retValue
= fprintf (fp
, " %d", permids
[i
]);
508 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
513 retValue
= fprintf (fp
, "\n");
514 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
517 if (auxids
!= NULL
) {
520 * Write the var auxids by scanning the ids array.
523 retValue
= fprintf (fp
, ".auxids");
524 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
526 for (i
= 0; i
< nVars
; i
++) {
528 retValue
= fprintf (fp
, " %d", auxids
[i
]);
529 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
533 retValue
= fprintf (fp
, "\n");
534 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
539 * Write the roots info.
542 retValue
= fprintf (fp
, ".nroots %d\n", nRoots
);
543 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
546 if (rootnames
!= NULL
) {
549 * Write the root names.
552 retValue
= fprintf (fp
, ".rootnames");
553 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
556 for (i
= 0; i
< nRoots
; i
++) {
557 if (rootnames
[i
] == NULL
) {
558 (void) fprintf (stderr
,
559 "DdStore Warning: null variable name. ROOT%d generated\n",i
);
561 rootnames
[i
] = DDDMP_ALLOC(char,10);
562 Dddmp_CheckAndGotoLabel (rootnames
[i
]==NULL
,
563 "Error writing to file.", failure
);
564 sprintf(rootnames
[ids
[i
]], "ROOT%d",i
);
566 retValue
= fprintf (fp
, " %s", rootnames
[i
]);
567 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
571 retValue
= fprintf (fp
, "\n");
572 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
576 retValue
= fprintf (fp
, ".rootids");
577 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
581 * Write BDD indexes of function roots.
582 * Use negative integers for complemented edges.
585 for (i
= 0; i
< nRoots
; i
++) {
587 (void) fprintf (stderr
, "DdStore Warning: %d-th root is NULL\n",i
);
589 retValue
= fprintf (fp
, " 0");
591 if (Cudd_IsComplement(f
[i
])) {
592 retValue
= fprintf (fp
, " -%d",
593 DddmpReadNodeIndexBdd (Cudd_Regular (f
[i
])));
595 retValue
= fprintf (fp
, " %d",
596 DddmpReadNodeIndexBdd (Cudd_Regular (f
[i
])));
598 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
602 retValue
= fprintf (fp
, "\n");
603 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
606 retValue
= fprintf (fp
, ".nodes\n");
607 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
615 * Call the function that really gets the job done.
618 for (i
= 0; i
< nRoots
; i
++) {
620 retValue
= NodeStoreRecurBdd (ddMgr
, Cudd_Regular(f
[i
]),
621 mode
, supportids
, outvarnames
, outids
, fp
);
622 Dddmp_CheckAndGotoLabel (retValue
==DDDMP_FAILURE
,
623 "Error writing to file.", failure
);
628 * Write trailer and return.
631 retValue
= fprintf (fp
, ".end\n");
632 Dddmp_CheckAndGotoLabel (retValue
==EOF
, "Error writing to file.",
639 DddmpUnnumberBddNodes (ddMgr
, f
, nRoots
);
641 DDDMP_FREE (permids
);
642 DDDMP_FREE (invpermids
);
643 DDDMP_FREE (supportids
);
645 return (DDDMP_SUCCESS
);
652 if (permids
!= NULL
) {
653 DDDMP_FREE (permids
);
655 if (invpermids
!= NULL
) {
656 DDDMP_FREE (invpermids
);
658 if (supportids
!= NULL
) {
659 DDDMP_FREE (supportids
);
661 if (support
!= NULL
) {
662 Cudd_RecursiveDeref (ddMgr
, support
);
665 return (DDDMP_FAILURE
);
668 /*---------------------------------------------------------------------------*/
669 /* Definition of static functions */
670 /*---------------------------------------------------------------------------*/
672 /**Function********************************************************************
674 Synopsis [Performs the recursive step of Dddmp_bddStore.]
676 Description [Stores a node to file in either test or binary mode.<l>
677 In text mode a node is represented (on a text line basis) as
679 <LI> node-index \[var-extrainfo\] var-index Then-index Else-index
682 where all indexes are integer numbers and var-extrainfo
683 (optional redundant field) is either an integer or a string
684 (variable name). Node-index is redundant (due to the node
685 ordering) but we keep it for readability.<p>
687 In binary mode nodes are represented as a sequence of bytes,
688 representing var-index, Then-index, and Else-index in an
689 optimized way. Only the first byte (code) is mandatory.
690 Integer indexes are represented in absolute or relative mode,
691 where relative means offset wrt. a Then/Else node info.
692 Suppose Var(NodeId), Then(NodeId) and Else(NodeId) represent
693 infos about a given node.<p>
695 The generic "NodeId" node is stored as
704 where code-byte contains bit fields
708 <LI>Variable: 2 bits, one of the following codes
710 <LI>DDDMP_ABSOLUTE_ID var-info = Var(NodeId) follows
711 <LI>DDDMP_RELATIVE_ID Var(NodeId) is represented in relative form as
712 var-info = Min(Var(Then(NodeId)),Var(Else(NodeId))) -Var(NodeId)
713 <LI>DDDMP_RELATIVE_1 No var-info follows, because
714 Var(NodeId) = Min(Var(Then(NodeId)),Var(Else(NodeId)))-1
715 <LI>DDDMP_TERMINAL Node is a terminal, no var info required
717 <LI>T : 2 bits, with codes similar to V
719 <LI>DDDMP_ABSOLUTE_ID Then-info = Then(NodeId) follows
720 <LI>DDDMP_RELATIVE_ID Then(NodeId) is represented in relative form as
721 Then-info = Nodeid-Then(NodeId)
722 <LI>DDDMP_RELATIVE_1 No info on Then(NodeId) follows, because
723 Then(NodeId) = NodeId-1
724 <LI>DDDMP_TERMINAL Then Node is a terminal, no info required (for BDDs)
726 <LI>Ecompl : 1 bit, if 1 means complemented edge
727 <LI>E : 2 bits, with codes and meanings as for the Then edge
729 var-info, Then-info, Else-info (if required) are represented as unsigned
730 integer values on a sufficient set of bytes (MSByte first).
737 ******************************************************************************/
741 DdManager
*ddMgr
/* IN: DD Manager */,
742 DdNode
*f
/* IN: DD node to be stored */,
743 int mode
/* IN: store mode */,
744 int *supportids
/* IN: internal ids for variables */,
745 char **varnames
/* IN: names of variables: to be stored with nodes */,
746 int *outids
/* IN: output ids for variables */,
747 FILE *fp
/* IN: store file */
763 idf
= idT
= idE
= (-1);
766 assert(!Cudd_IsComplement(f
));
768 assert(supportids
!=NULL
);
771 /* If already visited, nothing to do. */
772 if (DddmpVisitedBdd (f
)) {
773 return (DDDMP_SUCCESS
);
776 /* Mark node as visited. */
777 DddmpSetVisitedBdd (f
);
779 if (Cudd_IsConstant(f
)) {
780 /* Check for special case: don't recur */
781 idf
= DddmpReadNodeIndexBdd (f
);
785 /* BDDs! Only one constant supported */
786 assert (!cuddIsConstant(f
));
790 * Recursive call for Then edge
795 /* ROBDDs! No complemented Then edge */
796 assert (!Cudd_IsComplement(T
));
799 retValue
= NodeStoreRecurBdd (ddMgr
, T
, mode
, supportids
, varnames
, outids
,
801 if (retValue
!= DDDMP_SUCCESS
) {
806 * Recursive call for Else edge
809 E
= Cudd_Regular (cuddE (f
));
810 retValue
= NodeStoreRecurBdd (ddMgr
, E
, mode
, supportids
, varnames
, outids
,
812 if (retValue
!= DDDMP_SUCCESS
) {
817 * Obtain nodeids and variable ids of f, T, E
820 idf
= DddmpReadNodeIndexBdd (f
);
823 idT
= DddmpReadNodeIndexBdd (T
);
824 if (Cudd_IsConstant(T
)) {
830 idE
= DddmpReadNodeIndexBdd (E
);
831 if (Cudd_IsConstant(E
)) {
839 case DDDMP_MODE_TEXT
:
840 retValue
= NodeTextStoreBdd (ddMgr
, f
, mode
, supportids
, varnames
,
841 outids
, fp
, idf
, vf
, idT
, idE
);
843 case DDDMP_MODE_BINARY
:
844 retValue
= NodeBinaryStoreBdd (ddMgr
, f
, mode
, supportids
, varnames
,
845 outids
, fp
, idf
, vf
, idT
, idE
, vT
, vE
, T
, E
);
848 return (DDDMP_FAILURE
);
854 /**Function********************************************************************
856 Synopsis [Store One Single Node in Text Format.]
858 Description [Store 1 0 0 for the terminal node.
859 Store id, left child pointer, right pointer for all the other nodes.
864 SeeAlso [NodeBinaryStoreBdd]
866 ******************************************************************************/
870 DdManager
*ddMgr
/* IN: DD Manager */,
871 DdNode
*f
/* IN: DD node to be stored */,
872 int mode
/* IN: store mode */,
873 int *supportids
/* IN: internal ids for variables */,
874 char **varnames
/* IN: names of variables: to be stored with nodes */,
875 int *outids
/* IN: output ids for variables */,
876 FILE *fp
/* IN: Store file */,
877 int idf
/* IN: index of the current node */,
878 int vf
/* IN: variable of the current node */,
879 int idT
/* IN: index of the Then node */,
880 int idE
/* IN: index of the Else node */
889 if (Cudd_IsConstant(f
)) {
891 if (f
== Cudd_ReadOne(ddMgr
)) {
892 if ((varnames
!= NULL
) || (outids
!= NULL
)) {
893 retValue
= fprintf (fp
, "%d T 1 0 0\n", idf
);
895 retValue
= fprintf (fp
, "%d 1 0 0\n", idf
);
898 if (retValue
== EOF
) {
899 return (DDDMP_FAILURE
);
901 return (DDDMP_SUCCESS
);
905 if (f
== Cudd_ReadZero(ddMgr
)) {
906 if ((varnames
!= NULL
) || (outids
!= NULL
)) {
907 retValue
= fprintf (fp
, "%d T 0 0 0\n", idf
);
909 retValue
= fprintf (fp
, "%d 0 0 0\n", idf
);
912 if (retValue
== EOF
) {
913 return (DDDMP_FAILURE
);
915 return (DDDMP_SUCCESS
);
920 * A constant node different from 1: an ADD constant
923 Dddmp_CheckAndReturn (((varnames
!=NULL
)||(outids
!=NULL
)),
924 "Error writing to file: ADD Type.");
926 if (retValue
== EOF
) {
927 return (DDDMP_FAILURE
);
929 return (DDDMP_SUCCESS
);
937 if (Cudd_IsComplement (cuddE(f
))) {
941 if (varnames
!= NULL
) {
942 retValue
= fprintf (fp
, "%d %s %d %d %d\n",
943 idf
, varnames
[vf
], supportids
[vf
], idT
, idE
);
945 if (retValue
== EOF
) {
946 return (DDDMP_FAILURE
);
948 return (DDDMP_SUCCESS
);
952 if (outids
!= NULL
) {
953 retValue
= fprintf (fp
, "%d %d %d %d %d\n",
954 idf
, outids
[vf
], supportids
[vf
], idT
, idE
);
956 if (retValue
== EOF
) {
957 return (DDDMP_FAILURE
);
959 return (DDDMP_SUCCESS
);
963 retValue
= fprintf (fp
, "%d %d %d %d\n",
964 idf
, supportids
[vf
], idT
, idE
);
966 if (retValue
== EOF
) {
967 return (DDDMP_FAILURE
);
969 return (DDDMP_SUCCESS
);
973 /**Function********************************************************************
975 Synopsis [Store One Single Node in Binary Format.]
977 Description [Store 1 0 0 for the terminal node.
978 Store id, left child pointer, right pointer for all the other nodes.
979 Store every information as coded binary values.]
983 SeeAlso [NodeTextStoreBdd]
985 ******************************************************************************/
989 DdManager
*ddMgr
/* IN: DD Manager */,
990 DdNode
*f
/* IN: DD node to be stored */,
991 int mode
/* IN: store mode */,
992 int *supportids
/* IN: internal ids for variables */,
993 char **varnames
/* IN: names of variables: to be stored with nodes */,
994 int *outids
/* IN: output ids for variables */,
995 FILE *fp
/* IN: store file */,
996 int idf
/* IN: index of the node */,
997 int vf
/* IN: variable of the node */,
998 int idT
/* IN: index of the Then node */,
999 int idE
/* IN: index of the Else node */,
1000 int vT
/* IN: variable of the Then node */,
1001 int vE
/* IN: variable of the Else node */,
1002 DdNode
*T
/* IN: Then node */,
1003 DdNode
*E
/* IN: Else node */
1006 int retValue
, diff
, var
;
1007 struct binary_dd_code code
;
1010 * Check for Constant
1013 /* only integer ids used, varnames ignored */
1014 /* Terminal one is coded as DDDMP_TERMINAL, all other fields are 0 */
1015 if (Cudd_IsConstant(f
)) {
1017 code
.V
= DDDMP_TERMINAL
;
1021 retValue
= DddmpWriteCode (fp
,code
);
1022 if (retValue
== EOF
) {
1023 return (DDDMP_FAILURE
);
1025 return (DDDMP_SUCCESS
);
1030 * Non terminal: output variable id
1033 var
= supportids
[vf
];
1034 diff
= (supportids
[vT
]<supportids
[vE
]) ?
1035 (supportids
[vT
]-var
) : (supportids
[vE
]-var
);
1036 code
.V
= DDDMP_ABSOLUTE_ID
;
1040 code
.V
= DDDMP_RELATIVE_1
;
1042 code
.V
= DDDMP_RELATIVE_ID
;
1047 if (T
== DD_ONE(ddMgr
)) {
1048 code
.T
= DDDMP_TERMINAL
;
1050 /* compute displacement */
1052 code
.T
= DDDMP_ABSOLUTE_ID
;
1055 code
.T
= DDDMP_RELATIVE_1
;
1057 code
.T
= DDDMP_RELATIVE_ID
;
1063 if (E
== DD_ONE(ddMgr
)) {
1064 code
.E
= DDDMP_TERMINAL
;
1066 /* compute displacement */
1068 code
.E
= DDDMP_ABSOLUTE_ID
;
1071 code
.E
= DDDMP_RELATIVE_1
;
1073 code
.E
= DDDMP_RELATIVE_ID
;
1079 if (Cudd_IsComplement(cuddE(f
))) {
1085 retValue
= DddmpWriteCode (fp
,code
);
1087 if (retValue
== EOF
) {
1088 return (DDDMP_FAILURE
);
1091 if ((code
.V
== DDDMP_ABSOLUTE_ID
) || (code
.V
== DDDMP_RELATIVE_ID
)) {
1092 retValue
= DddmpWriteInt (fp
, var
);
1093 if (retValue
== EOF
) {
1094 return (DDDMP_FAILURE
);
1098 if ((code
.T
== DDDMP_ABSOLUTE_ID
) || (code
.T
== DDDMP_RELATIVE_ID
)) {
1099 retValue
= DddmpWriteInt(fp
,idT
);
1100 if (retValue
== EOF
) {
1101 return (DDDMP_FAILURE
);
1105 if ((code
.E
== DDDMP_ABSOLUTE_ID
) || (code
.E
== DDDMP_RELATIVE_ID
)) {
1106 retValue
= DddmpWriteInt(fp
,idE
);
1107 if (retValue
== EOF
) {
1108 return (DDDMP_FAILURE
);