source: vis_dev/glu-2.3/src/calBdd/calReorderUtil.c @ 102

Last change on this file since 102 was 13, checked in by cecile, 13 years ago

library glu 2.3
File size: 20.5 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [calReorderUtil.c]
4
5  PackageName [cal]
6
7  Synopsis    [Some utility routines used by both breadth-first and
8  depth-first reordering techniques.]
9
10  Description []
11
12  SeeAlso     [optional]
13
14  Author      [Rajeev K. Ranjan   (rajeev@ic.eecs.berkeley.edu)
15               Wilsin Gosti (wilsin@ic.eecs.berkeley.edu)]
16  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
17  All rights reserved.
18
19  Permission is hereby granted, without written agreement and without license
20  or royalty fees, to use, copy, modify, and distribute this software and its
21  documentation for any purpose, provided that the above copyright notice and
22  the following two paragraphs appear in all copies of this software.
23
24  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
25  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
26  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
27  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
28
29  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
30  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
31  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
32  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
33  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
34
35  Revision    [$Id: calReorderUtil.c,v 1.3 2002/09/22 00:37:04 fabio Exp $]
36
37******************************************************************************/
38
39#include "calInt.h"
40
41/*---------------------------------------------------------------------------*/
42/* Constant declarations                                                     */
43/*---------------------------------------------------------------------------*/
44
45/*---------------------------------------------------------------------------*/
46/* Type declarations                                                         */
47/*---------------------------------------------------------------------------*/
48
49/*---------------------------------------------------------------------------*/
50/* Stucture declarations                                                     */
51/*---------------------------------------------------------------------------*/
52
53/*---------------------------------------------------------------------------*/
54/* Variable declarations                                                     */
55/*---------------------------------------------------------------------------*/
56
57/*---------------------------------------------------------------------------*/
58/* Macro declarations                                                        */
59/*---------------------------------------------------------------------------*/
60
61/**AutomaticStart*************************************************************/
62
63/*---------------------------------------------------------------------------*/
64/* Static function prototypes                                                */
65/*---------------------------------------------------------------------------*/
66
67
68/**AutomaticEnd***************************************************************/
69
70/*---------------------------------------------------------------------------*/
71/* Definition of exported functions                                          */
72/*---------------------------------------------------------------------------*/
73/*---------------------------------------------------------------------------*/
74/* Definition of internal functions                                          */
75/*---------------------------------------------------------------------------*/
76/**Function********************************************************************
77
78  Synopsis           [required]
79
80  Description        [optional]
81
82  SideEffects        [required]
83
84  SeeAlso            [optional]
85
86******************************************************************************/
87void
88CalBddReorderFixUserBddPtrs(Cal_BddManager bddManager)
89{
90  CalHashTable_t *userBddUniqueTable = bddManager->uniqueTable[0];
91  int i;
92  int numBins;
93  int rehashFlag;
94  CalBddNode_t **bins;
95  CalBddNode_t *bddNode;
96  CalBddNode_t *nextBddNode;
97  CalBddNode_t *thenBddNode;
98  CalBddNode_t *elseBddNode;
99  Cal_Bdd_t internalBdd;
100
101  numBins = userBddUniqueTable->numBins;
102  bins = userBddUniqueTable->bins;
103
104  for(i = 0; i < numBins; i++) {
105    for(bddNode = bins[i];
106        bddNode != Cal_Nil(CalBddNode_t);
107        bddNode = nextBddNode) {
108      /*
109       * Process one bddNode at a time
110       */
111      nextBddNode = CalBddNodeGetNextBddNode(bddNode);
112      rehashFlag = 0;
113
114      thenBddNode = CalBddNodeGetThenBddNode(bddNode);
115      elseBddNode = CalBddNodeGetElseBddNode(bddNode);
116      CalBddNodeGetThenBdd(bddNode, internalBdd);
117      if (CalBddIsForwarded(internalBdd)) {
118        CalBddForward(internalBdd);
119        CalBddNodePutThenBdd(bddNode, internalBdd);
120        rehashFlag = 1;
121      }
122      Cal_Assert(CalBddIsForwarded(internalBdd) == 0);
123      /*Cal_Assert(!CalBddIsRefCountZero(internalBdd));*/
124      /*
125       * Rehash if necessary
126       */
127      if (rehashFlag) {
128        CalUniqueTableForIdRehashNode(userBddUniqueTable, bddNode,
129                                      thenBddNode, elseBddNode);
130      }
131    }
132  }
133}
134
135/**Function********************************************************************
136
137  Synopsis           [required]
138
139  Description        [optional]
140
141  SideEffects        [required]
142
143  SeeAlso            [optional]
144
145******************************************************************************/
146int
147CalCheckAllValidity(Cal_BddManager bddManager)
148{
149  int id;
150  for(id = 0; id <= bddManager->numVars; id++){
151    CalCheckValidityOfNodesForId(bddManager, id);
152  }
153  CalCheckAssociationValidity(bddManager);
154  if (bddManager->pipelineState == CREATE){
155    CalCheckPipelineValidity(bddManager);
156  }
157  CalCheckRefCountValidity(bddManager);
158  CalCheckCacheTableValidity(bddManager);
159  return 1;
160}
161
162
163/**Function********************************************************************
164
165  Synopsis           [required]
166
167  Description        [optional]
168
169  SideEffects        [required]
170
171  SeeAlso            [optional]
172
173******************************************************************************/
174int
175CalCheckValidityOfNodesForId(Cal_BddManager bddManager, int id)
176{
177  int i, numBins;
178  CalHashTable_t *uniqueTableForId;
179  CalBddNode_t *bddNode, *nextBddNode;
180  Cal_Bdd_t thenBdd, elseBdd;
181 
182  uniqueTableForId = bddManager->uniqueTable[id];
183  Cal_Assert(uniqueTableForId->startNode.nextBddNode == NULL);
184  numBins = uniqueTableForId->numBins;
185  for (i = 0; i < numBins; i++){
186    for (bddNode = uniqueTableForId->bins[i]; bddNode;
187         bddNode = nextBddNode){
188      nextBddNode = CalBddNodeGetNextBddNode(bddNode);
189      CalCheckValidityOfANode(bddManager, bddNode, id);
190      CalBddNodeGetThenBdd(bddNode, thenBdd);
191      CalBddNodeGetElseBdd(bddNode, elseBdd);
192      Cal_Assert(CalDoHash2(CalBddGetBddNode(thenBdd),
193                            CalBddGetBddNode(elseBdd), 
194                            uniqueTableForId) == i);
195    }
196  }
197  return 1;
198}
199
200
201/**Function********************************************************************
202
203  Synopsis           [required]
204
205  Description        [optional]
206
207  SideEffects        [required]
208
209  SeeAlso            [optional]
210
211******************************************************************************/
212int
213CalCheckValidityOfNodesForWindow(Cal_BddManager bddManager,
214                                 Cal_BddIndex_t index, int numLevels)
215{
216  int i, numBins, j;
217  CalHashTable_t *uniqueTableForId;
218  CalBddNode_t *bddNode, *nextBddNode;
219  Cal_Bdd_t thenBdd, elseBdd;
220
221  for (i = 0; i < numLevels; i++){
222    uniqueTableForId =
223        bddManager->uniqueTable[bddManager->indexToId[index+i]]; 
224    numBins = uniqueTableForId->numBins;
225    for (j = 0; j < numBins; j++){
226      for (bddNode = uniqueTableForId->bins[j]; bddNode;
227           bddNode = nextBddNode){
228        nextBddNode = CalBddNodeGetNextBddNode(bddNode);
229        Cal_Assert(CalBddNodeIsForwarded(bddNode) == 0);
230        CalBddNodeGetThenBdd(bddNode, thenBdd);
231        CalBddNodeGetElseBdd(bddNode, elseBdd);
232        Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
233        Cal_Assert(CalBddIsForwarded(elseBdd) == 0);
234        Cal_Assert(CalDoHash2(CalBddGetBddNode(thenBdd),
235                              CalBddGetBddNode(elseBdd), 
236                             uniqueTableForId) == j);
237      }
238    }
239    for (bddNode = uniqueTableForId->startNode.nextBddNode; bddNode;
240         bddNode = nextBddNode){ 
241      nextBddNode = CalBddNodeGetNextBddNode(bddNode);
242      CalBddNodeGetThenBdd(bddNode, thenBdd);
243      Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
244    }
245  }
246  return 1;
247}
248
249
250 
251/**Function********************************************************************
252
253  Synopsis           [required]
254
255  Description        [optional]
256
257  SideEffects        [required]
258
259  SeeAlso            [optional]
260
261******************************************************************************/
262int
263CalCheckValidityOfANode(Cal_BddManager_t *bddManager, CalBddNode_t
264                     *bddNode, int id) 
265{
266  Cal_Bdd_t thenBdd, elseBdd, thenBdd_, elseBdd_, bdd;
267  if (id != 0){
268    /* id = 0 corresponds to the constants and the user BDDs */
269    Cal_Assert(bddManager->idToIndex[id] <
270               bddManager->idToIndex[bddNode->thenBddId]);   
271    Cal_Assert(bddManager->idToIndex[id] < 
272               bddManager->idToIndex[bddNode->elseBddId]);
273  }
274  Cal_Assert(!CalBddNodeIsForwarded(bddNode));
275  Cal_Assert(!CalBddNodeIsRefCountZero(bddNode));
276  CalBddNodeGetThenBdd(bddNode, thenBdd);
277  CalBddNodeGetElseBdd(bddNode, elseBdd);
278  Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
279  Cal_Assert(CalBddIsForwarded(elseBdd) == 0);
280  Cal_Assert(!CalBddIsRefCountZero(thenBdd));
281  Cal_Assert(!CalBddIsRefCountZero(elseBdd));
282  /* Make sure that the then and else bdd nodes are part of the
283     respective unique tables */
284  if (bddNode->thenBddId != 0){
285    CalBddGetThenBdd(thenBdd, thenBdd_);
286    CalBddGetElseBdd(thenBdd, elseBdd_);
287    Cal_Assert(
288      CalUniqueTableForIdLookup(bddManager,
289                                bddManager->uniqueTable[bddNode->thenBddId], 
290                                thenBdd_, elseBdd_, &bdd));
291  }
292  if (bddNode->elseBddId != 0){
293    CalBddGetThenBdd(elseBdd, thenBdd_);
294    CalBddGetElseBdd(elseBdd, elseBdd_);
295    Cal_Assert(
296      CalUniqueTableForIdLookup(bddManager,
297                                bddManager->uniqueTable[bddNode->elseBddId],
298                                thenBdd_, elseBdd_, &bdd));
299  }
300  return 1;
301}
302
303/**Function********************************************************************
304
305  Synopsis           [required]
306
307  Description        [optional]
308
309  SideEffects        [required]
310
311  SeeAlso            [optional]
312
313******************************************************************************/
314void
315CalCheckRefCountValidity(Cal_BddManager_t *bddManager)
316{
317  int i, numBins, index;
318  CalHashTable_t *uniqueTableForId;
319  CalBddNode_t *bddNode, *nextBddNode;
320  Cal_Bdd_t thenBdd, elseBdd, internalBdd;
321  CalAssociation_t *assoc, *nextAssoc;
322 
323  /* First traverse the user BDDs */
324  uniqueTableForId = bddManager->uniqueTable[0];
325  numBins = uniqueTableForId->numBins;
326  for (i = 0; i < numBins; i++){
327    for (bddNode = uniqueTableForId->bins[i]; bddNode;
328         bddNode = nextBddNode){
329      nextBddNode = CalBddNodeGetNextBddNode(bddNode);
330      CalBddNodeGetThenBdd(bddNode, internalBdd);
331      CalBddDcrRefCount(internalBdd);
332    }
333  }
334      /* Traverse the associations */
335 
336  for(assoc = bddManager->associationList;
337      assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
338    nextAssoc = assoc->next;
339    for (i=1; i <= bddManager->numVars; i++){
340        if (CalBddGetBddId(assoc->varAssociation[i]) != CAL_BDD_NULL_ID){
341            CalBddDcrRefCount(assoc->varAssociation[i]);
342        }
343    }
344  }
345  /* temporary association */
346  assoc = bddManager->tempAssociation;
347  for (i=1; i <= bddManager->numVars; i++){
348      if (CalBddGetBddId(assoc->varAssociation[i]) != CAL_BDD_NULL_ID){
349          CalBddDcrRefCount(assoc->varAssociation[i]);
350      }
351  }
352
353 
354  /* Now traverse all the nodes in order */
355  for (index = 0; index < bddManager->numVars; index++){
356    uniqueTableForId = bddManager->uniqueTable[bddManager->indexToId[index]];
357    numBins = uniqueTableForId->numBins;
358    for (i = 0; i < numBins; i++){
359      for (bddNode = uniqueTableForId->bins[i]; bddNode;
360           bddNode = nextBddNode){
361        nextBddNode = CalBddNodeGetNextBddNode(bddNode);
362        CalBddNodeGetThenBdd(bddNode, thenBdd);
363        CalBddNodeGetElseBdd(bddNode, elseBdd);
364        CalBddDcrRefCount(thenBdd);
365        CalBddDcrRefCount(elseBdd);
366      }
367    }
368  }
369
370  /* All the reference count must be zero  or max */
371  for (index = 0; index < bddManager->numVars; index++){
372    uniqueTableForId = bddManager->uniqueTable[bddManager->indexToId[index]];
373    numBins = uniqueTableForId->numBins;
374    for (i = 0; i < numBins; i++){
375      for (bddNode = uniqueTableForId->bins[i]; bddNode;
376           bddNode = nextBddNode){
377        nextBddNode = CalBddNodeGetNextBddNode(bddNode);
378        /* If the pipeline execution is going on, the following
379           assertion will not hold */
380        if (bddManager->pipelineState != CREATE){
381          Cal_Assert(CalBddNodeIsRefCountZero(bddNode) ||
382                     CalBddNodeIsRefCountMax(bddNode));
383        }
384      }
385    }
386  }
387
388  /* Put back the ref count */
389  /* traverse all the nodes in order */
390  for (index = 0; index < bddManager->numVars; index++){
391    uniqueTableForId = bddManager->uniqueTable[bddManager->indexToId[index]];
392    numBins = uniqueTableForId->numBins;
393    for (i = 0; i < numBins; i++){
394      for (bddNode = uniqueTableForId->bins[i]; bddNode;
395           bddNode = nextBddNode){
396        nextBddNode = CalBddNodeGetNextBddNode(bddNode);
397        CalBddNodeGetThenBdd(bddNode, thenBdd);
398        CalBddNodeGetElseBdd(bddNode, elseBdd);
399        CalBddIcrRefCount(thenBdd);
400        CalBddIcrRefCount(elseBdd);
401      }
402    }
403  }
404      /* Traverse the associations */
405  for(assoc = bddManager->associationList;
406      assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
407    nextAssoc = assoc->next;
408    for (i=1; i <= bddManager->numVars; i++){
409        if (CalBddGetBddId(assoc->varAssociation[i]) != CAL_BDD_NULL_ID){
410            CalBddIcrRefCount(assoc->varAssociation[i]);
411        }
412    }
413  }
414  /* temporary association */
415  assoc = bddManager->tempAssociation;
416  for (i=1; i <= bddManager->numVars; i++){
417      if (CalBddGetBddId(assoc->varAssociation[i]) != CAL_BDD_NULL_ID){
418          CalBddIcrRefCount(assoc->varAssociation[i]);
419      }
420  }
421
422  /* Traverse the user BDDs */
423  uniqueTableForId = bddManager->uniqueTable[0];
424  numBins = uniqueTableForId->numBins;
425  for (i = 0; i < numBins; i++){
426    for (bddNode = uniqueTableForId->bins[i]; bddNode;
427         bddNode = nextBddNode){
428      nextBddNode = CalBddNodeGetNextBddNode(bddNode);
429      CalBddNodeGetThenBdd(bddNode, internalBdd);
430      CalBddIcrRefCount(internalBdd);
431    }
432  }
433}
434
435/**Function********************************************************************
436
437  Synopsis           [required]
438
439  Description        [optional]
440
441  SideEffects        [required]
442
443  SeeAlso            [optional]
444
445******************************************************************************/
446int
447CalCheckAssoc(Cal_BddManager_t *bddManager)
448{
449  CalAssociation_t *assoc, *nextAssoc;
450  int i;
451  int expectedLastBddIndex, bddIndex;
452
453  for(assoc = bddManager->associationList;
454      assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
455    nextAssoc = assoc->next;
456    expectedLastBddIndex = -1;
457    for (i=1; i <= bddManager->numVars; i++){
458      if (CalBddIsBddNull(bddManager, assoc->varAssociation[i]) == 0){
459        bddIndex = bddManager->idToIndex[i];
460        if (expectedLastBddIndex < bddIndex){
461          expectedLastBddIndex = bddIndex;
462        }
463      }
464    }
465    Cal_Assert(expectedLastBddIndex == assoc->lastBddIndex);
466  }
467  /* fix temporary association */
468  assoc = bddManager->tempAssociation;
469  expectedLastBddIndex = -1;
470  for (i=1; i <= bddManager->numVars; i++){
471    if (CalBddIsBddNull(bddManager, assoc->varAssociation[i]) == 0){
472      bddIndex = bddManager->idToIndex[i];
473      if (expectedLastBddIndex < bddIndex){
474        expectedLastBddIndex = bddIndex;
475      }
476    }
477  }
478  Cal_Assert(expectedLastBddIndex == assoc->lastBddIndex);
479  return 1;
480}
481
482/**Function********************************************************************
483
484  Synopsis           [required]
485
486  Description        [optional]
487
488  SideEffects        [required]
489
490  SeeAlso            [optional]
491
492******************************************************************************/
493void
494CalFixupAssoc(Cal_BddManager_t *bddManager, long id1, long id2,
495           CalAssociation_t *assoc)
496{
497  if (assoc->lastBddIndex == -1) return;
498  /* Variable with id1 is moving down a spot. */
499  if ((CalBddIsBddNull(bddManager, assoc->varAssociation[id1]) == 0)
500      && (assoc->lastBddIndex == bddManager->idToIndex[id1])){
501    assoc->lastBddIndex++;
502  }
503  else if ((CalBddIsBddNull(bddManager, assoc->varAssociation[id1])) &&
504           (CalBddIsBddNull(bddManager, assoc->varAssociation[id2]) ==
505            0) && 
506  (assoc->lastBddIndex == bddManager->idToIndex[id2])){
507    assoc->lastBddIndex--;
508  }
509  Cal_Assert((assoc->lastBddIndex >= 0) && (assoc->lastBddIndex <=
510                                           CAL_BDD_CONST_INDEX));
511   
512}
513/**Function********************************************************************
514
515  Synopsis           [Fixes the cofactors of the nodes belonging to
516  the given index.]
517
518  Description        [This routine traverses the unique table and for
519  each node, looks at the then and else cofactors. If needed fixes the
520  cofactors.]
521
522  SideEffects        [required]
523
524  SeeAlso            [optional]
525
526******************************************************************************/
527void
528CalBddReorderFixCofactors(Cal_BddManager bddManager, Cal_BddId_t id)
529{
530  CalHashTable_t *uniqueTableForId =
531      bddManager->uniqueTable[id];
532  CalBddNode_t *bddNode, *nextBddNode, **bins, *thenBddNode, *elseBddNode;
533  Cal_Bdd_t f0, f1;
534  long numBins;
535  int i, rehashFlag;
536 
537  numBins = uniqueTableForId->numBins;
538  bins = uniqueTableForId->bins;
539
540  for(i = 0; i < numBins; i++) {
541    for(bddNode = bins[i];
542        bddNode != Cal_Nil(CalBddNode_t);
543        bddNode = nextBddNode) {
544      nextBddNode = CalBddNodeGetNextBddNode(bddNode);
545      /*
546       * Process one bddNode at a time
547       */
548      /*
549      ** Because we have kept all the forwarding nodes in the list,
550      ** this should not be a forwarding node.
551      */
552      Cal_Assert(CalBddNodeIsForwarded(bddNode) == 0);
553      Cal_Assert(CalBddNodeIsRefCountZero(bddNode) == 0);
554      thenBddNode = CalBddNodeGetThenBddNode(bddNode);
555      elseBddNode = CalBddNodeGetElseBddNode(bddNode);
556      rehashFlag = 0;
557      CalBddNodeGetThenBdd(bddNode, f1);
558      CalBddNodeGetElseBdd(bddNode, f0);
559      if (CalBddIsForwarded(f1)) {
560        CalBddForward(f1);
561        CalBddNodePutThenBdd(bddNode, f1);
562        rehashFlag = 1;
563      }
564      Cal_Assert(CalBddIsForwarded(f1) == 0);
565      if (CalBddIsForwarded(f0)) {
566        CalBddForward(f0);
567        CalBddNodePutElseBdd(bddNode, f0); 
568        rehashFlag = 1;
569      }
570      Cal_Assert(CalBddIsForwarded(f0) == 0);
571      /* Rehash if necessary */
572      if (rehashFlag) {
573        CalUniqueTableForIdRehashNode(uniqueTableForId, bddNode, thenBddNode,
574                                      elseBddNode);
575      }
576    }
577  }
578}
579
580/**Function********************************************************************
581
582  Synopsis           [required]
583
584  Description        [optional]
585
586  SideEffects        [required]
587
588  SeeAlso            [optional]
589
590******************************************************************************/
591void
592CalBddReorderReclaimForwardedNodes(Cal_BddManager bddManager, int
593                                startIndex, int endIndex)
594{
595  Cal_BddIndex_t index;
596  Cal_BddId_t id;
597  CalHashTable_t *uniqueTableForId;
598  CalNodeManager_t *nodeManager;
599 
600  for(index = startIndex; index <= endIndex; index++){
601    id = bddManager->indexToId[index];
602    uniqueTableForId = bddManager->uniqueTable[id];
603    nodeManager = uniqueTableForId->nodeManager;
604    uniqueTableForId->endNode->nextBddNode = nodeManager->freeNodeList;
605    nodeManager->freeNodeList = uniqueTableForId->startNode.nextBddNode;
606    uniqueTableForId->endNode = &(uniqueTableForId->startNode);
607    uniqueTableForId->startNode.nextBddNode = NULL;
608  }
609  bddManager->numForwardedNodes = 0;
610}
611
612
613
614/*---------------------------------------------------------------------------*/
615/* Definition of static functions                                          */
616/*---------------------------------------------------------------------------*/
617
Note: See TracBrowser for help on using the repository browser.