source: icGREP/icgrep-devel/cudd-2.5.1/dddmp/dddmpNodeBdd.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: 11.9 KB
Line 
1/**CFile**********************************************************************
2
3  FileName     [dddmpNodeBdd.c]
4
5  PackageName  [dddmp]
6
7  Synopsis     [Functions to handle BDD node infos and numbering]
8
9  Description  [Functions to handle BDD node infos and numbering.
10    ]
11
12  Author       [Gianpiero Cabodi and Stefano Quer]
13
14  Copyright    [
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.
25    ]
26
27******************************************************************************/
28
29#include "dddmpInt.h"
30
31/*---------------------------------------------------------------------------*/
32/* Stucture declarations                                                     */
33/*---------------------------------------------------------------------------*/
34
35/*---------------------------------------------------------------------------*/
36/* Type declarations                                                         */
37/*---------------------------------------------------------------------------*/
38
39/*---------------------------------------------------------------------------*/
40/* Variable declarations                                                     */
41/*---------------------------------------------------------------------------*/
42
43/*---------------------------------------------------------------------------*/
44/* Macro declarations                                                        */
45/*---------------------------------------------------------------------------*/
46
47/**AutomaticStart*************************************************************/
48
49/*---------------------------------------------------------------------------*/
50/* Static function prototypes                                                */
51/*---------------------------------------------------------------------------*/
52
53static int NumberNodeRecurBdd(DdNode *f, int id);
54static void RemoveFromUniqueRecurBdd(DdManager *ddMgr, DdNode *f);
55static void RestoreInUniqueRecurBdd(DdManager *ddMgr, DdNode *f);
56
57/**AutomaticEnd***************************************************************/
58
59/*---------------------------------------------------------------------------*/
60/* Definition of exported functions                                          */
61/*---------------------------------------------------------------------------*/
62
63/*---------------------------------------------------------------------------*/
64/* Definition of internal functions                                          */
65/*---------------------------------------------------------------------------*/
66
67/**Function********************************************************************
68
69  Synopsis    [Removes nodes from unique table and number them]
70
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    (DddmpUnnumberBddNodes ()).
75    ]
76
77  SideEffects [Nodes are temporarily removed from unique table]
78
79  SeeAlso     [RemoveFromUniqueRecur(), NumberNodeRecur(),
80    DddmpUnnumberBddNodes ()]
81
82******************************************************************************/
83
84int
85DddmpNumberBddNodes (
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 */
89  )
90{
91  int id=0, i;
92
93  for (i=0; i<n; i++) {
94    RemoveFromUniqueRecurBdd (ddMgr, f[i]);
95  }
96
97  for (i=0; i<n; i++) {
98    id = NumberNodeRecurBdd (f[i], id);
99  }
100
101  return (id);
102}
103
104
105/**Function********************************************************************
106
107  Synopsis     [Restores nodes in unique table, loosing numbering]
108
109  Description  [Node indexes are no more needed. Nodes are re-linked in the
110    unique table.
111    ]
112
113  SideEffects  [None]
114
115  SeeAlso      [DddmpNumberBddNode ()]
116
117******************************************************************************/
118
119void
120DddmpUnnumberBddNodes(
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 */
124  )
125{
126  int i;
127
128  for (i=0; i<n; i++) {
129    RestoreInUniqueRecurBdd (ddMgr, f[i]);
130  }
131
132  return;
133}
134
135/**Function********************************************************************
136
137  Synopsis     [Write index to node]
138
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.
142    ]
143
144  SideEffects  [None]
145
146  SeeAlso      [DddmpReadNodeIndexBdd(), DddmpSetVisitedBdd (),
147    DddmpVisitedBdd ()]
148
149******************************************************************************/
150
151void 
152DddmpWriteNodeIndexBdd (
153  DdNode *f   /* IN: BDD node */,
154  int id       /* IN: index to be written */
155  )
156{
157  if (!Cudd_IsConstant (f)) {
158    f->next = (struct DdNode *)((ptruint)((id)<<1));
159  }
160
161  return;
162}
163
164/**Function********************************************************************
165
166  Synopsis     [Reads the index of a node]
167
168  Description  [Reads the index of a node. LSB is skipped (used as visited
169    flag).
170    ]
171
172  SideEffects  [None]
173
174  SeeAlso      [DddmpWriteNodeIndexBdd (), DddmpSetVisitedBdd (),
175    DddmpVisitedBdd ()]
176
177******************************************************************************/
178
179int
180DddmpReadNodeIndexBdd (
181  DdNode *f    /* IN: BDD node */
182  )
183{
184  if (!Cudd_IsConstant (f)) {
185    return ((int)(((ptruint)(f->next))>>1));
186  } else {
187    return (1);
188  }
189}
190
191/**Function********************************************************************
192
193  Synopsis     [Returns true if node is visited]
194
195  Description  [Returns true if node is visited]
196
197  SideEffects  [None]
198
199  SeeAlso      [DddmpSetVisitedBdd (), DddmpClearVisitedBdd ()]
200
201******************************************************************************/
202
203int
204DddmpVisitedBdd (
205  DdNode *f    /* IN: BDD node to be tested */
206  )
207{
208  f = Cudd_Regular(f);
209
210  return ((int)((ptruint)(f->next)) & (01));
211}
212
213/**Function********************************************************************
214
215  Synopsis     [Marks a node as visited]
216 
217  Description  [Marks a node as visited]
218
219  SideEffects  [None]
220
221  SeeAlso      [DddmpVisitedBdd (), DddmpClearVisitedBdd ()]
222
223******************************************************************************/
224
225void
226DddmpSetVisitedBdd (
227  DdNode *f   /* IN: BDD node to be marked (as visited) */
228  )
229{
230  f = Cudd_Regular(f);
231
232  f->next = (DdNode *)(ptruint)((int)((ptruint)(f->next))|01);
233
234  return;
235}
236
237/**Function********************************************************************
238
239  Synopsis     [Marks a node as not visited]
240
241  Description  [Marks a node as not visited]
242
243  SideEffects  [None]
244
245  SeeAlso      [DddmpVisited (), DddmpSetVisited ()]
246
247******************************************************************************/
248
249void
250DddmpClearVisitedBdd (
251  DdNode *f    /* IN: BDD node to be marked (as not visited) */
252  )
253{
254  f = Cudd_Regular (f);
255
256  f->next = (DdNode *)(ptruint)((int)((ptruint)(f->next)) & (~01));
257
258  return;
259}
260
261/*---------------------------------------------------------------------------*/
262/* Definition of static functions                                            */
263/*---------------------------------------------------------------------------*/
264
265/**Function********************************************************************
266
267  Synopsis     [Number nodes recursively in post-order]
268
269  Description  [Number nodes recursively in post-order.
270    The "visited" flag is used with inverse polarity, because all nodes
271    were set "visited" when removing them from unique.
272    ]
273
274  SideEffects  ["visited" flags are reset.]
275
276  SeeAlso      []
277
278******************************************************************************/
279
280static int
281NumberNodeRecurBdd (
282  DdNode */*  IN: root of the BDD to be numbered */,
283  int id     /* IN/OUT: index to be assigned to the node */
284  )
285{
286  f = Cudd_Regular (f);
287
288  if (!DddmpVisitedBdd (f)) {
289    return (id);
290  }
291
292  if (!cuddIsConstant (f)) {
293    id = NumberNodeRecurBdd (cuddT (f), id);
294    id = NumberNodeRecurBdd (cuddE (f), id);
295  }
296
297  DddmpWriteNodeIndexBdd (f, ++id);
298  DddmpClearVisitedBdd (f);
299
300  return (id);
301}
302
303/**Function********************************************************************
304
305  Synopsis    [Removes a node from unique table]
306
307  Description [Removes a node from the unique table by locating the proper
308    subtable and unlinking the node from it. It recurs on the
309    children of the node. Constants remain untouched.
310    ]
311
312  SideEffects [Nodes are left with the "visited" flag true.]
313
314  SeeAlso     [RestoreInUniqueRecurBdd ()]
315
316******************************************************************************/
317
318static void
319RemoveFromUniqueRecurBdd (
320  DdManager *ddMgr  /*  IN: DD Manager */,
321  DdNode *f         /*  IN: root of the BDD to be extracted */
322  )
323{
324  DdNode *node, *last, *next;
325  DdNode *sentinel = &(ddMgr->sentinel);
326  DdNodePtr *nodelist;
327  DdSubtable *subtable;
328  int pos, level;
329
330  f = Cudd_Regular (f);
331
332  if (DddmpVisitedBdd (f)) {
333    return;
334  }
335
336  if (!cuddIsConstant (f)) {
337
338    RemoveFromUniqueRecurBdd (ddMgr, cuddT (f));
339    RemoveFromUniqueRecurBdd (ddMgr, cuddE (f));
340
341    level = ddMgr->perm[f->index];
342    subtable = &(ddMgr->subtables[level]);
343
344    nodelist = subtable->nodelist;
345
346    pos = ddHash (cuddT (f), cuddE (f), subtable->shift);
347    node = nodelist[pos];
348    last = NULL;
349    while (node != sentinel) {
350      next = node->next;
351      if (node == f) {
352        if (last != NULL) 
353          last->next = next;
354        else 
355          nodelist[pos] = next;
356        break;
357      } else {
358        last = node;
359        node = next;
360      }
361    }
362
363    f->next = NULL;
364
365  }
366
367  DddmpSetVisitedBdd (f);
368
369  return;
370}
371
372/**Function********************************************************************
373
374  Synopsis     [Restores a node in unique table]
375
376  Description  [Restores a node in unique table (recursively)]
377
378  SideEffects  [Nodes are not restored in the same order as before removal]
379
380  SeeAlso      [RemoveFromUnique()]
381
382******************************************************************************/
383
384static void
385RestoreInUniqueRecurBdd (
386  DdManager *ddMgr /*  IN: DD Manager */,
387  DdNode *f        /*  IN: root of the BDD to be restored */
388  )
389{
390  DdNodePtr *nodelist;
391  DdNode *T, *E, *looking;
392  DdNodePtr *previousP;
393  DdSubtable *subtable;
394  int pos, level;
395#ifdef DDDMP_DEBUG
396  DdNode *node;
397  DdNode *sentinel = &(ddMgr->sentinel);
398#endif
399
400  f = Cudd_Regular(f);
401
402  if (!Cudd_IsComplement (f->next)) {
403    return;
404  }
405
406  if (cuddIsConstant (f)) {
407    /* StQ 11.02.2004:
408       Bug fixed --> restore NULL within the next field */
409    /*DddmpClearVisitedBdd (f);*/   
410    f->next = NULL;
411
412    return;
413  }
414
415  RestoreInUniqueRecurBdd (ddMgr, cuddT (f));
416  RestoreInUniqueRecurBdd (ddMgr, cuddE (f));
417
418  level = ddMgr->perm[f->index];
419  subtable = &(ddMgr->subtables[level]);
420
421  nodelist = subtable->nodelist;
422
423  pos = ddHash (cuddT (f), cuddE (f), subtable->shift);
424
425#ifdef DDDMP_DEBUG
426  /* verify uniqueness to avoid duplicate nodes in unique table */
427  for (node=nodelist[pos]; node != sentinel; node=node->next)
428    assert(node!=f);
429#endif
430
431  T = cuddT (f);
432  E = cuddE (f);
433  previousP = &(nodelist[pos]);
434  looking = *previousP;
435
436  while (T < cuddT (looking)) {
437    previousP = &(looking->next);
438    looking = *previousP;
439  }
440
441  while (T == cuddT (looking) && E < cuddE (looking)) {
442    previousP = &(looking->next);
443    looking = *previousP;
444  }
445
446  f->next = *previousP;
447  *previousP = f;
448
449  return;
450}
451
452
Note: See TracBrowser for help on using the repository browser.