1 /**CFile**********************************************************************
3 FileName [dddmpDdNodeBdd.c]
7 Synopsis [Functions to handle BDD node infos and numbering]
9 Description [Functions to handle BDD node infos and numbering.
12 Author [Gianpiero Cabodi and Stefano Quer]
15 Copyright (c) 2004 by Politecnico di Torino.
16 All Rights Reserved. This software is for educational purposes only.
17 Permission is given to academic institutions to use, copy, and modify
18 this software and its documentation provided that this introductory
19 message is not removed, that this software and its documentation is
20 used for the institutions' internal research and educational purposes,
21 and that no monies are exchanged. No guarantee is expressed or implied
22 by the distribution of this code.
23 Send bug-reports and/or questions to:
24 {gianpiero.cabodi,stefano.quer}@polito.it.
27 ******************************************************************************/
31 /*---------------------------------------------------------------------------*/
32 /* Stucture declarations */
33 /*---------------------------------------------------------------------------*/
35 /*---------------------------------------------------------------------------*/
36 /* Type declarations */
37 /*---------------------------------------------------------------------------*/
39 /*---------------------------------------------------------------------------*/
40 /* Variable declarations */
41 /*---------------------------------------------------------------------------*/
43 /*---------------------------------------------------------------------------*/
44 /* Macro declarations */
45 /*---------------------------------------------------------------------------*/
47 /**AutomaticStart*************************************************************/
49 /*---------------------------------------------------------------------------*/
50 /* Static function prototypes */
51 /*---------------------------------------------------------------------------*/
53 static int NumberNodeRecur(DdNode
*f
, int id
);
54 static void RemoveFromUniqueRecur(DdManager
*ddMgr
, DdNode
*f
);
55 static void RestoreInUniqueRecur(DdManager
*ddMgr
, DdNode
*f
);
57 /**AutomaticEnd***************************************************************/
59 /*---------------------------------------------------------------------------*/
60 /* Definition of exported functions */
61 /*---------------------------------------------------------------------------*/
63 /*---------------------------------------------------------------------------*/
64 /* Definition of internal functions */
65 /*---------------------------------------------------------------------------*/
67 /**Function********************************************************************
69 Synopsis [Removes nodes from unique table and number them]
71 Description [Node numbering is required to convert pointers to integers.
72 Since nodes are removed from unique table, no new nodes should
73 be generated before re-inserting nodes in the unique table
74 (DddmpUnnumberDdNodes()).
77 SideEffects [Nodes are temporarily removed from unique table]
79 SeeAlso [RemoveFromUniqueRecur(), NumberNodeRecur(),
80 DddmpUnnumberDdNodes()]
82 ******************************************************************************/
86 DdManager
*ddMgr
/* IN: DD Manager */,
87 DdNode
**f
/* IN: array of BDDs */,
88 int n
/* IN: number of BDD roots in the array of BDDs */
94 RemoveFromUniqueRecur (ddMgr
, f
[i
]);
98 id
= NumberNodeRecur (f
[i
], id
);
105 /**Function********************************************************************
107 Synopsis [Restores nodes in unique table, loosing numbering]
109 Description [Node indexes are no more needed. Nodes are re-linked in the
115 SeeAlso [DddmpNumberDdNode()]
117 ******************************************************************************/
120 DddmpUnnumberDdNodes(
121 DdManager
*ddMgr
/* IN: DD Manager */,
122 DdNode
**f
/* IN: array of BDDs */,
123 int n
/* IN: number of BDD roots in the array of BDDs */
128 for (i
=0; i
<n
; i
++) {
129 RestoreInUniqueRecur (ddMgr
, f
[i
]);
135 /**Function********************************************************************
137 Synopsis [Write index to node]
139 Description [The index of the node is written in the "next" field of
140 a DdNode struct. LSB is not used (set to 0). It is used as
141 "visited" flag in DD traversals.
146 SeeAlso [DddmpReadNodeIndex(), DddmpSetVisited (), DddmpVisited ()]
148 ******************************************************************************/
151 DddmpWriteNodeIndex (
152 DdNode
*f
/* IN: BDD node */,
153 int id
/* IN: index to be written */
157 if (1 || !Cudd_IsConstant (f
)) {
159 if (!Cudd_IsConstant (f
)) {
161 f
->next
= (struct DdNode
*)((ptruint
)((id
)<<1));
167 /**Function********************************************************************
169 Synopsis [Reads the index of a node]
171 Description [Reads the index of a node. LSB is skipped (used as visited
177 SeeAlso [DddmpWriteNodeIndex(), DddmpSetVisited (), DddmpVisited ()]
179 ******************************************************************************/
183 DdNode
*f
/* IN: BDD node */
188 if (1 || !Cudd_IsConstant (f
)) {
190 if (!Cudd_IsConstant (f
)) {
192 return ((int)(((ptruint
)(f
->next
))>>1));
198 /**Function********************************************************************
200 Synopsis [Returns true if node is visited]
202 Description [Returns true if node is visited]
206 SeeAlso [DddmpSetVisited (), DddmpClearVisited ()]
208 ******************************************************************************/
212 DdNode
*f
/* IN: BDD node to be tested */
216 return ((int)((ptruint
)(f
->next
)) & (01));
219 /**Function********************************************************************
221 Synopsis [Marks a node as visited]
223 Description [Marks a node as visited]
227 SeeAlso [DddmpVisited (), DddmpClearVisited ()]
229 ******************************************************************************/
233 DdNode
*f
/* IN: BDD node to be marked (as visited) */
238 f
->next
= (DdNode
*)(ptruint
)((int)((ptruint
)(f
->next
))|01);
243 /**Function********************************************************************
245 Synopsis [Marks a node as not visited]
247 Description [Marks a node as not visited]
251 SeeAlso [DddmpVisited (), DddmpSetVisited ()]
253 ******************************************************************************/
257 DdNode
*f
/* IN: BDD node to be marked (as not visited) */
260 f
= Cudd_Regular (f
);
262 f
->next
= (DdNode
*)(ptruint
)((int)((ptruint
)(f
->next
)) & (~01));
267 /*---------------------------------------------------------------------------*/
268 /* Definition of static functions */
269 /*---------------------------------------------------------------------------*/
271 /**Function********************************************************************
273 Synopsis [Number nodes recursively in post-order]
275 Description [Number nodes recursively in post-order.
276 The "visited" flag is used with inverse polarity, because all nodes
277 were set "visited" when removing them from unique.
280 SideEffects ["visited" flags are reset.]
284 ******************************************************************************/
288 DdNode
*f
/* IN: root of the BDD to be numbered */,
289 int id
/* IN/OUT: index to be assigned to the node */
294 if (!DddmpVisited (f
)) {
298 if (!cuddIsConstant (f
)) {
299 id
= NumberNodeRecur (cuddT (f
), id
);
300 id
= NumberNodeRecur (cuddE (f
), id
);
303 DddmpWriteNodeIndex (f
, ++id
);
304 DddmpClearVisited (f
);
309 /**Function********************************************************************
311 Synopsis [Removes a node from unique table]
313 Description [Removes a node from the unique table by locating the proper
314 subtable and unlinking the node from it. It recurs on the
315 children of the node.
318 SideEffects [Nodes are left with the "visited" flag true.]
320 SeeAlso [RestoreInUniqueRecur()]
322 ******************************************************************************/
325 RemoveFromUniqueRecur (
326 DdManager
*ddMgr
/* IN: DD Manager */,
327 DdNode
*f
/* IN: root of the BDD to be extracted */
330 DdNode
*node
, *last
, *next
;
331 DdNode
*sentinel
= &(ddMgr
->sentinel
);
333 DdSubtable
*subtable
;
336 f
= Cudd_Regular (f
);
338 if (DddmpVisited (f
)) {
342 if (!cuddIsConstant (f
)) {
344 RemoveFromUniqueRecur (ddMgr
, cuddT (f
));
345 RemoveFromUniqueRecur (ddMgr
, cuddE (f
));
347 level
= ddMgr
->perm
[f
->index
];
348 subtable
= &(ddMgr
->subtables
[level
]);
350 nodelist
= subtable
->nodelist
;
352 pos
= ddHash (cuddT (f
), cuddE (f
), subtable
->shift
);
353 node
= nodelist
[pos
];
355 while (node
!= sentinel
) {
361 nodelist
[pos
] = next
;
378 /**Function********************************************************************
380 Synopsis [Restores a node in unique table]
382 Description [Restores a node in unique table (recursively)]
384 SideEffects [Nodes are not restored in the same order as before removal]
386 SeeAlso [RemoveFromUnique()]
388 ******************************************************************************/
391 RestoreInUniqueRecur (
392 DdManager
*ddMgr
/* IN: DD Manager */,
393 DdNode
*f
/* IN: root of the BDD to be restored */
397 DdNode
*T
, *E
, *looking
;
398 DdNodePtr
*previousP
;
399 DdSubtable
*subtable
;
403 DdNode
*sentinel
= &(ddMgr
->sentinel
);
408 if (!Cudd_IsComplement (f
->next
)) {
412 if (cuddIsConstant (f
)) {
413 DddmpClearVisited (f
);
418 RestoreInUniqueRecur (ddMgr
, cuddT (f
));
419 RestoreInUniqueRecur (ddMgr
, cuddE (f
));
421 level
= ddMgr
->perm
[f
->index
];
422 subtable
= &(ddMgr
->subtables
[level
]);
424 nodelist
= subtable
->nodelist
;
426 pos
= ddHash (cuddT (f
), cuddE (f
), subtable
->shift
);
429 /* verify uniqueness to avoid duplicate nodes in unique table */
430 for (node
=nodelist
[pos
]; node
!= sentinel
; node
=node
->next
)
436 previousP
= &(nodelist
[pos
]);
437 looking
= *previousP
;
439 while (T
< cuddT (looking
)) {
440 previousP
= &(looking
->next
);
441 looking
= *previousP
;
444 while (T
== cuddT (looking
) && E
< cuddE (looking
)) {
445 previousP
= &(looking
->next
);
446 looking
= *previousP
;
449 f
->next
= *previousP
;