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

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

library glu 2.3
File size: 52.9 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [calReorderDF.c]
4
5  PackageName [cal]
6
7  Synopsis    [Routines for dynamic reordering of variables.]
8
9  Description [This method is based on traditional dynamic reordering
10  technique found in depth-first based packages. The data structure is
11  first converted to conform to traditional one and then reordering is
12  performed. At the end the nodes are arranged back on the pages. The
13  computational overheads are in terms of converting the data
14  structure back and forth and the memory overhead due to the extra
15  space needed to arrange the nodes. This overhead can be eliminated
16  by proper implementation. For details, please refer to the work by
17  Rajeev K. Ranjan et al - "Dynamic variable reordering in a
18  breadth-first manipulation based package: Challenges and Solutions"-
19  Proceedings of ICCD'97.]
20
21  SeeAlso     [calReorderBF.c calReorderUtil.c]
22
23  Author      [Rajeev K. Ranjan   (rajeev@@ic. eecs.berkeley.edu)]
24
25  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
26  All rights reserved.
27
28  Permission is hereby granted, without written agreement and without license
29  or royalty fees, to use, copy, modify, and distribute this software and its
30  documentation for any purpose, provided that the above copyright notice and
31  the following two paragraphs appear in all copies of this software.
32
33  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
34  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
35  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
36  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
37
38  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
39  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
40  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
41  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
42  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
43
44******************************************************************************/
45
46#include "calInt.h"
47
48/*---------------------------------------------------------------------------*/
49/* Constant declarations                                                     */
50/*---------------------------------------------------------------------------*/
51
52/*---------------------------------------------------------------------------*/
53/* Type declarations                                                         */
54/*---------------------------------------------------------------------------*/
55
56/*---------------------------------------------------------------------------*/
57/* Stucture declarations                                                     */
58/*---------------------------------------------------------------------------*/
59
60/*---------------------------------------------------------------------------*/
61/* Variable declarations                                                     */
62/*---------------------------------------------------------------------------*/
63static   CalNodeManager_t *nodeManager; 
64static   int freeListId;
65
66
67/*---------------------------------------------------------------------------*/
68/* Macro declarations                                                        */
69/*---------------------------------------------------------------------------*/
70/* These macros are needed because we are dealing with a new data
71   structures of the BDD nodes */
72
73#define BddNodeIcrRefCount(f)                   \
74{                                               \
75  CalBddNode_t *_bddNode = CAL_BDD_POINTER(f);  \
76  if (_bddNode->elseBddId < CAL_MAX_REF_COUNT){ \
77    _bddNode->elseBddId++;                      \
78  }                                             \
79}
80
81#define BddNodeDcrRefCount(f) \
82{ \
83  CalBddNode_t *_bddNode = CAL_BDD_POINTER(f); \
84  if ((_bddNode->elseBddId < CAL_MAX_REF_COUNT) && (_bddNode->elseBddId)){ \
85    _bddNode->elseBddId--; \
86  } \
87  else if (_bddNode->elseBddId == 0){ \
88    CalBddWarningMessage("Trying to decrement reference count below zero"); \
89  } \
90}
91
92#define BddGetCofactors(bddManager, f, id, fThen, fElse)                \
93{                                                                       \
94  CalBddNode_t *_bddNode = CAL_BDD_POINTER(f);                          \
95  Cal_Assert(bddManager->idToIndex[_bddNode->thenBddId] <=              \
96             bddManager->idToIndex[id]);                                \
97  if (bddManager->idToIndex[_bddNode->thenBddId] ==                     \
98      bddManager->idToIndex[id]){                                       \
99    fThen = _bddNode->thenBddNode;                                      \
100    fElse = _bddNode->elseBddNode;                                      \
101  }                                                                     \
102  else{                                                                 \
103    fThen = fElse = f;                                                  \
104  }                                                                     \
105}
106
107#define BddNodeGetThenBddNode(bddNode)                    \
108((CalBddNode_t*) ((CalAddress_t)                          \
109                  (CAL_BDD_POINTER(bddNode)->thenBddNode) \
110                  ^ (CAL_TAG0(bddNode))))
111
112#define BddNodeGetElseBddNode(bddNode)                    \
113((CalBddNode_t*) ((CalAddress_t)                          \
114                  (CAL_BDD_POINTER(bddNode)->elseBddNode) \
115                  ^ (CAL_TAG0(bddNode))))
116 
117   
118   
119/**AutomaticStart*************************************************************/
120
121/*---------------------------------------------------------------------------*/
122/* Static function prototypes                                                */
123/*---------------------------------------------------------------------------*/
124
125static int UniqueTableForIdFindOrAdd(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, CalBddNode_t *thenBdd, CalBddNode_t *elseBdd, CalBddNode_t **bddPtr);
126static void HashTableAddDirect(CalHashTable_t * hashTable, CalBddNode_t *bddNode);
127static int HashTableFindOrAdd(Cal_BddManager_t *bddManager, CalHashTable_t *hashTable, CalBddNode_t *thenBdd, CalBddNode_t *elseBdd, CalBddNode_t **bddPtr);
128static void BddConvertDataStruct(Cal_BddManager_t *bddManager);
129static void BddConvertDataStructBack(Cal_BddManager_t *bddManager);
130static void BddReallocateNodes(Cal_BddManager_t *bddManager);
131static void BddExchangeAux(Cal_BddManager_t *bddManager, CalBddNode_t *f, int id, int nextId);
132static int CheckValidityOfNodes(Cal_BddManager_t *bddManager, long id);
133static void SweepVarTable(Cal_BddManager_t *bddManager, long id);
134static void BddExchange(Cal_BddManager_t *bddManager, long id);
135static void BddExchangeVarBlocks(Cal_BddManager_t *bddManager, Cal_Block parent, long blockIndex);
136static int BddReorderWindow2(Cal_BddManager_t *bddManager, Cal_Block block, long i);
137static int BddReorderWindow3(Cal_BddManager_t *bddManager, Cal_Block block, long i);
138static void BddReorderStableWindow3Aux(Cal_BddManager_t *bddManager, Cal_Block block, char *levels);
139static void BddReorderStableWindow3(Cal_BddManager_t *bddManager);
140static void BddSiftBlock(Cal_BddManager_t *bddManager, Cal_Block block, long startPosition, double maxSizeFactor);
141static void BddReorderSiftAux(Cal_BddManager_t *bddManager, Cal_Block block, Cal_Block *toSift, double maxSizeFactor);
142static void BddReorderSift(Cal_BddManager_t *bddManager, double maxSizeFactor);
143static int CeilLog2(int number);
144
145/**AutomaticEnd***************************************************************/
146
147/*---------------------------------------------------------------------------*/
148/* Definition of exported functions                                          */
149/*---------------------------------------------------------------------------*/
150
151/**Function********************************************************************
152
153  Synopsis           [required]
154
155  Description        [optional]
156
157  SideEffects        [required]
158
159  SeeAlso            [optional]
160
161******************************************************************************/
162void
163CalBddReorderAuxDF(Cal_BddManager_t *bddManager)
164{
165  CalHashTableGC(bddManager, bddManager->uniqueTable[0]);
166  /*Cal_BddManagerGC(bddManager);Cal_Assert(CalCheckAllValidity(bddManager));*/
167  /* If we want to check the validity, we need to garbage collect */
168  CalInitInteract(bddManager); /* Initialize the interaction matrix
169                                  before changing the data structure */
170  nodeManager = CalNodeManagerInit(bddManager->pageManager2);
171  freeListId = 1;
172#ifdef _CAL_QUANTIFY_
173  quantify_start_recording_data();
174#endif
175  BddConvertDataStruct(bddManager);
176  if (bddManager->reorderTechnique == CAL_REORDER_WINDOW){
177    BddReorderStableWindow3(bddManager);
178  }
179  else {
180    BddReorderSift(bddManager, bddManager->maxSiftingGrowth);
181  }
182  BddReallocateNodes(bddManager);
183  BddConvertDataStructBack(bddManager);
184#ifdef _CAL_QUANTIFY_
185  quantify_stop_recording_data();
186#endif
187  nodeManager->numPages = 0; /* Since these pages have already been
188                                freed */
189  CalNodeManagerQuit(nodeManager);
190  Cal_Assert(CalCheckAllValidity(bddManager));
191  Cal_MemFree(bddManager->interact);
192  bddManager->numReorderings++;
193}
194
195
196/*---------------------------------------------------------------------------*/
197/* Definition of internal functions                                          */
198/*---------------------------------------------------------------------------*/
199/*---------------------------------------------------------------------------*/
200/* Definition of static functions                                          */
201/*---------------------------------------------------------------------------*/
202static void
203NodeManagerAllocNode(Cal_BddManager_t *bddManager, CalBddNode_t **nodePtr) 
204{
205  /* First check the free list of bddManager */
206  if (nodeManager->freeNodeList){
207    *nodePtr = nodeManager->freeNodeList;
208    nodeManager->freeNodeList =
209        ((CalBddNode_t *)(*nodePtr))->nextBddNode;
210  }
211  else{
212    if (freeListId < bddManager->numVars){
213      /* Find the next id with free list */
214      for (; freeListId <= bddManager->numVars; freeListId++){
215        CalNodeManager_t *nodeManagerForId =
216            bddManager->nodeManagerArray[freeListId]; 
217        if (nodeManagerForId->freeNodeList){
218          *nodePtr = nodeManagerForId->freeNodeList;
219          nodeManagerForId->freeNodeList = (CalBddNode_t *)0;
220          nodeManager->freeNodeList =
221              ((CalBddNode_t *)(*nodePtr))->nextBddNode;
222          break;
223        }
224      }
225    }
226  }
227  if (!(*nodePtr)){
228    /* Create a new page */
229    CalBddNode_t *_freeNodeList, *_nextNode, *_node;                       
230    _freeNodeList =                                                         
231        (CalBddNode_t *)CalPageManagerAllocPage(nodeManager->pageManager); 
232    for(_node = _freeNodeList + NUM_NODES_PER_PAGE - 1, _nextNode =0;       
233        _node != _freeNodeList; _nextNode = _node--){                       
234      _node->nextBddNode = _nextNode;                                       
235    }                                                                       
236    nodeManager->freeNodeList = _freeNodeList + 1;                         
237    *nodePtr = _node;
238    if (nodeManager->numPages == nodeManager->maxNumPages){             
239      nodeManager->maxNumPages *= 2;                                     
240      nodeManager->pageList =                                           
241          Cal_MemRealloc(CalAddress_t *, nodeManager->pageList, 
242                         nodeManager->maxNumPages);                       
243    }                                                                       
244    nodeManager->pageList[nodeManager->numPages++] =
245        (CalAddress_t *)_freeNodeList;     
246  }
247}
248
249/**Function********************************************************************
250
251  Synopsis    [find or add in the unique table for id.]
252
253  Description [optional]
254
255  SideEffects [If a new BDD node is created (found == false), then the
256  numNodes field of the manager needs to be incremented.]
257
258  SeeAlso     [optional]
259
260******************************************************************************/
261static int
262UniqueTableForIdFindOrAdd(Cal_BddManager_t * bddManager,
263                          CalHashTable_t * hashTable,
264                          CalBddNode_t *thenBdd,
265                          CalBddNode_t *elseBdd,
266                          CalBddNode_t **bddPtr)
267{
268  int found = 0; 
269  if (thenBdd == elseBdd){
270    *bddPtr = thenBdd;
271    found = 1;
272  }
273  else if(CalBddNodeIsOutPos(thenBdd)){
274    found = HashTableFindOrAdd(bddManager, hashTable, thenBdd, elseBdd, bddPtr);
275  }
276  else{
277    found = HashTableFindOrAdd(bddManager, hashTable,
278                               CalBddNodeNot(thenBdd),
279                               CalBddNodeNot(elseBdd), bddPtr); 
280    *bddPtr = CalBddNodeNot(*bddPtr);
281  }
282  if (!found) bddManager->numNodes++;
283  return found;
284}
285
286/**Function********************************************************************
287
288  Synopsis    [Directly insert a BDD node in the hash table.]
289
290  Description [optional]
291
292  SideEffects [required]
293
294  SeeAlso     [optional]
295
296******************************************************************************/
297static void
298HashTableAddDirect(CalHashTable_t * hashTable, CalBddNode_t *bddNode)
299{
300  int hashValue;
301  CalBddNode_t *thenBddNode, *elseBddNode;
302
303  hashTable->numEntries++;
304  if(hashTable->numEntries >= hashTable->maxCapacity){
305    CalHashTableRehash(hashTable, 1);
306  }
307  thenBddNode = bddNode->thenBddNode;
308  Cal_Assert(CalBddNodeIsOutPos(thenBddNode));
309  elseBddNode = bddNode->elseBddNode;
310  hashValue = CalDoHash2(thenBddNode, elseBddNode, hashTable);
311  bddNode->nextBddNode = hashTable->bins[hashValue];
312  hashTable->bins[hashValue] = bddNode;
313}
314
315
316/**Function********************************************************************
317
318  Synopsis    [required]
319
320  Description [optional]
321
322  SideEffects [required]
323
324  SeeAlso     [optional]
325
326******************************************************************************/
327static int
328HashTableFindOrAdd(Cal_BddManager_t *bddManager, CalHashTable_t
329                   *hashTable,  CalBddNode_t *thenBdd,
330                   CalBddNode_t *elseBdd, CalBddNode_t **bddPtr) 
331{
332  CalBddNode_t *ptr;
333  int hashValue;
334 
335  Cal_Assert(CalBddNodeIsOutPos(thenBdd));
336  hashValue = CalDoHash2(thenBdd, elseBdd, hashTable);
337  for (ptr = hashTable->bins[hashValue]; ptr; ptr = ptr->nextBddNode){
338    if ((ptr->thenBddNode == thenBdd) &&
339        (ptr->elseBddNode == elseBdd)){
340      *bddPtr = ptr;
341      return 1;
342    }
343  }
344  hashTable->numEntries++;
345  if(hashTable->numEntries > hashTable->maxCapacity){
346    CalHashTableRehash(hashTable,1);
347    hashValue = CalDoHash2(thenBdd, elseBdd, hashTable);
348  }
349
350  NodeManagerAllocNode(bddManager, &ptr);
351
352  ptr->thenBddNode = thenBdd;
353  ptr->elseBddNode = elseBdd;
354  ptr->nextBddNode = hashTable->bins[hashValue];
355  ptr->thenBddId = hashTable->bddId;
356  ptr->elseBddId = 0;
357  hashTable->bins[hashValue] = ptr;
358  *bddPtr = ptr;
359  return 0;
360}
361
362
363/**Function********************************************************************
364
365  Synopsis           [Changes the data structure of the bdd nodes.]
366
367  Description        [New data structure: thenBddId -> id
368                                          elseBddId -> ref count]
369
370  SideEffects        [required]
371
372  SeeAlso            [optional]
373
374******************************************************************************/
375static void
376BddConvertDataStruct(Cal_BddManager_t *bddManager)
377{
378  CalBddNode_t *bddNode, *thenBddNode, *elseBddNode,
379      *next = Cal_Nil(CalBddNode_t); 
380  CalBddNode_t *last;
381  long numBins;
382  int i, refCount, id, index;
383  long oldNumEntries;
384  CalHashTable_t *uniqueTableForId;
385
386  if (bddManager->numPeakNodes < bddManager->numNodes){
387    bddManager->numPeakNodes = bddManager->numNodes;
388  }
389
390  for(index = 0; index < bddManager->numVars; index++){
391    id = bddManager->indexToId[index];
392    uniqueTableForId = bddManager->uniqueTable[id];
393    oldNumEntries = uniqueTableForId->numEntries;
394    numBins = uniqueTableForId->numBins;
395    for(i = 0; i < numBins; i++){
396      last = NULL;
397      bddNode = uniqueTableForId->bins[i];
398      while(bddNode != Cal_Nil(CalBddNode_t)){
399        next = CalBddNodeGetNextBddNode(bddNode);
400        CalBddNodeGetRefCount(bddNode, refCount);
401        thenBddNode = CalBddNodeGetThenBddNode(bddNode);
402        elseBddNode = CalBddNodeGetElseBddNode(bddNode);
403        if(refCount == 0){
404          if (last == NULL){
405            uniqueTableForId->bins[i] = next;
406          }
407          else{
408            last->nextBddNode = next;
409          }
410          CalBddNodeDcrRefCount(CAL_BDD_POINTER(thenBddNode));
411          CalBddNodeDcrRefCount(CAL_BDD_POINTER(elseBddNode));
412          CalNodeManagerFreeNode(nodeManager, bddNode);
413          uniqueTableForId->numEntries--;
414        }
415        else {
416          bddNode->thenBddId = id;
417          bddNode->elseBddId = refCount;
418          bddNode->nextBddNode = next;
419          bddNode->thenBddNode = thenBddNode;
420          bddNode->elseBddNode = elseBddNode;
421          last = bddNode; 
422        }
423        bddNode = next;
424      }
425    }
426    if ((uniqueTableForId->numBins > uniqueTableForId->numEntries) &&
427        (uniqueTableForId->sizeIndex > HASH_TABLE_DEFAULT_SIZE_INDEX)){
428      CalHashTableRehash(uniqueTableForId, 0);
429    }
430    bddManager->numNodes -= oldNumEntries - uniqueTableForId->numEntries;
431    bddManager->numNodesFreed += oldNumEntries - uniqueTableForId->numEntries;
432  }
433  id = 0;
434  uniqueTableForId = bddManager->uniqueTable[id];
435  numBins = uniqueTableForId->numBins;
436  for(i = 0; i < numBins; i++){
437    bddNode = uniqueTableForId->bins[i];
438    while(bddNode != Cal_Nil(CalBddNode_t)){
439      next = CalBddNodeGetNextBddNode(bddNode);
440      CalBddNodeGetRefCount(bddNode, refCount);
441      Cal_Assert(refCount);
442      thenBddNode = CalBddNodeGetThenBddNode(bddNode);
443      elseBddNode = CalBddNodeGetElseBddNode(bddNode);
444      bddNode->thenBddId = id;
445      bddNode->elseBddId = refCount;
446      bddNode->nextBddNode = next;
447      bddNode->thenBddNode = thenBddNode;
448      bddNode->elseBddNode = elseBddNode;
449      bddNode = next;
450    }
451  }
452  bddNode = bddManager->bddOne.bddNode;
453  CalBddNodeGetRefCount(bddNode, refCount);
454  Cal_Assert(refCount);
455  thenBddNode = CalBddNodeGetThenBddNode(bddNode);
456  elseBddNode = CalBddNodeGetElseBddNode(bddNode);
457  bddNode->thenBddId = id;
458  bddNode->elseBddId = refCount;
459  bddNode->nextBddNode = next;
460  bddNode->thenBddNode = thenBddNode;
461  bddNode->elseBddNode = elseBddNode;
462}
463
464
465/**Function********************************************************************
466
467  Synopsis           [Changes the data structure of the bdd nodes to
468  the original one.]
469
470  Description        [Data structure conversion: thenBddId -> id
471  elseBddId -> ref count]
472  SideEffects        [required]
473
474  SeeAlso            [optional]
475
476******************************************************************************/
477static void
478BddConvertDataStructBack(Cal_BddManager_t *bddManager)
479{
480  Cal_Bdd_t thenBdd, elseBdd;
481 
482  CalBddNode_t *bddNode, *nextBddNode, **bins;
483  long numBins;
484  int i, id, index;
485  CalHashTable_t *uniqueTableForId;
486  uniqueTableForId = bddManager->uniqueTable[0];
487  numBins = uniqueTableForId->numBins;
488  bins = uniqueTableForId->bins;
489  for(i = 0; i < numBins; i++) {
490    for(bddNode = bins[i];
491        bddNode != Cal_Nil(CalBddNode_t);
492        bddNode = nextBddNode) {
493      nextBddNode = CalBddNodeGetNextBddNode(bddNode);
494      CalBddNodePutRefCount(bddNode, bddNode->elseBddId);
495      bddNode->thenBddId = CAL_BDD_POINTER(bddNode->thenBddNode)->thenBddId;
496      bddNode->elseBddId = CAL_BDD_POINTER(bddNode->elseBddNode)->thenBddId;
497    }
498  }
499  for(index = 0; index < bddManager->numVars; index++){
500    id = bddManager->indexToId[index];
501    uniqueTableForId = bddManager->uniqueTable[id];
502    numBins = uniqueTableForId->numBins;
503    bins = uniqueTableForId->bins;
504    for(i = 0; i < numBins; i++) {
505      for(bddNode = bins[i];
506          bddNode != Cal_Nil(CalBddNode_t);
507          bddNode = nextBddNode) {
508        nextBddNode = CalBddNodeGetNextBddNode(bddNode);
509        CalBddNodePutRefCount(bddNode, bddNode->elseBddId);
510        bddNode->thenBddId = CAL_BDD_POINTER(bddNode->thenBddNode)->thenBddId;
511        bddNode->elseBddId = CAL_BDD_POINTER(bddNode->elseBddNode)->thenBddId;
512      Cal_Assert(!CalBddNodeIsForwarded(bddNode));
513      Cal_Assert(!CalBddNodeIsRefCountZero(bddNode));
514      CalBddNodeGetThenBdd(bddNode, thenBdd);
515      CalBddNodeGetElseBdd(bddNode, elseBdd);
516      Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
517      Cal_Assert(CalBddIsForwarded(elseBdd) == 0);
518      }
519    }
520  }
521  bddNode = bddManager->bddOne.bddNode;
522  CalBddNodePutRefCount(bddNode, bddNode->elseBddId);
523  bddNode->thenBddId = 0;
524  bddNode->elseBddId = 0;
525}
526
527#ifdef _FOO_
528/**Function********************************************************************
529
530  Synopsis           [required]
531
532  Description        [optional]
533
534  SideEffects        [required]
535
536  SeeAlso            [optional]
537
538******************************************************************************/
539static void
540BddReallocateNodesInPlace(Cal_BddManager_t *bddManager)
541{
542  Cal_Address_t  *pageSegment;
543  CalPageManager_t *pageManager;
544  CalHashTable_t *uniqueTable;
545  CalNodeManager_t *nodeManager;
546  int index, id, i, pageCounter, numUsefulSegments, segmentCounter;
547 
548  /* Initialize and set up few things */
549  pageManager = bddManager->pageManager;
550  uniqueTable = bddManager->uniqueTable;
551  for (id = 1; id <= bddManager->numVars; id++){
552    numPagesRequired =
553        uniqueTable[id]->numEntries/NUM_NODES_PER_PAGE+1;
554    nodeManager = uniqueTable[id]->nodeManager;
555    /* Clear out the page list of the node manager */
556    for (i=0; i<nodeManager->maxNumPages; i++){
557      nodeManager->pageList[i] = 0;
558    }
559    nodeManager->freeNodeList = (CalBddNode_t *)0;
560    nodeManager->numPages = numPagesRequired;
561    Cal_Assert(nodeManager->maxNumPages >= numPagesRequired);
562    for (i = 0; i<numPagesRequired; i++){
563      if (++pageCounter ==
564              pageManager->numPagesArray[segmentCounter]){
565        pageCounter = 0;
566        segmentCounter++;
567        pageSegment = pageManager->pageSegmentArray[segmentCounter];
568      }
569      nodeManager->pageList[i] = pageSegment[pageCounter];
570    }
571  }
572  numUsefulSegments = segmentCounter+1;
573  numUsefulPagesInLastSegment = pageCounter+1;
574 
575  /* Traverse all the nodes belonging in each page */
576  /* Put the destination addresses in the next pointer */
577  for (numSegment=0; numSegment < pageManager->numSegments; 
578       numSegment++){
579    for (numPage = 0, page = pageManager->pageSegmentArray[numSegment]; 
580         numPage < pageManager->numPagesArray[numSegment];
581         page += PAGE_SIZE, numPage++){
582      for (bddNode = (CalBddNode_t*) page, numNode = 0;
583           numNode < NUM_NODES_PER_PAGE; numNode++, bddNode += 1){
584        /* If the node is not useful, continue */
585        if (bddNode->elseBddId == 0) continue; 
586        /* Find out the destination address */
587        bddId = bddNode->thenBddId;
588        nodeCounter[bddId]++;
589        if (nodeCounter[bddId] == NUM_NODES_PER_PAGE){
590          pageCounter[bddId]++;
591          nodePointerArray[bddId] =
592              pageListArray[bddId][pageCounter[bddId]];
593          nodeCounter[bddId] = 0;
594        }
595        bddNode->nextBddNode = nodePointerArray[bddId];
596        nodePointerArray[bddId] += 1;
597      }
598    }
599  }
600  /* Traverse all the nodes belonging in each page */
601  /* Update the contents */
602  for (numSegment=0; numSegment < pageManager->totalNumSegments; 
603       numSegment++){
604    for (numPage = 0, page = pageManager->pageSegmentArray[numSegment]; 
605         numPage < pageManager->numPagesArray[numSegment];
606         page += PAGE_SIZE, numPage++){
607      for (bddNode = (CalBddNode_t*) page, numNode = 0;
608           numNode < NUM_NODES_PER_PAGE; numNode++, bddNode += 1){
609        /* If the node is not useful, continue */
610        if (bddNode->elseBddId == 0) continue; 
611        /* If the node has been visited, continue */
612        if ((CalAddress_t)bddNode->nextBddNode & 01) continue;
613        /* If the nodes is supposed to remain at the same place,
614           update the then and else pointers and continue */
615        if (((CalAddress_t) bddNode->nextBddNode &~01) ==
616            ((CalAddress_t) bddNode & ~01)){
617          CalBddNodeUpdatebddNode(bddNode);
618          continue;
619        }
620        origNode = bddNode; /* Remember the address */
621        /* Update the contents */
622        thenBddNode = bddNode->thenBddNode;
623        elseBddNode = bddNode->elseBddNode;
624        thenBddId = bddNode->thenBddId;
625        elseBddId = bddNode->elseBddId;
626        do{
627          thenBddNode = UpdateThenBddNode(thenBddNode);
628          elseBddNode = UpdateElseBddNode(elseBddNode);
629          destinationNode = bddNode->nextBddNode;
630          /* Mark the node visited */
631          bddNode->nextBddNode = (CalBddNode_t *)
632              ((CalAddress_t)bddNode->nextBddNode | 01);
633          thenBddNode2 = destinationNode->thenBddNode;
634          elseBddNode2 = destinationNode->elseBddNode;
635          thenBddId2 = destinationNode->thenBddId;
636          elseBddId2 = destinationNode->elseBddId;
637          destinationNode->thenBddNode = thenBddNode;
638          destinationNode->elseBddNode = elseBddNode;
639          destinationNode->thenBddId = thenBddId;
640          destinationNode->elseBddId = elseBddId;
641          bddNode = destinationNode;
642          thenBddNode = thenBddNode2;
643          elseBddNode = elseBddNode2;
644          thenBddId = thenBddId2;
645          elseBddId = elseBddId2;
646        } while ((elseBddId != 0) && (bddNode != origNode) &&
647                 !((CalAddress_t)(bddNode->nextBddNode) & 01));
648      }
649    }
650  }
651  /* Fix the handles to the nodes being moved */
652  for (id = 1; id <= bddManager->numVars; id++){
653    /* Fix the varBdd array */
654  }
655/* Need to update the handles to the nodes being moved */
656  if (bddManager->pipelineState == CREATE){
657    /* There are some results computed in pipeline */
658    CalBddReorderFixProvisionalNodesAfterReallocation(bddManager);
659  }
660 
661  /* Fix the user BDDs */
662  CalBddReorderFixUserBddPtrsAfterReallocation(bddManager);
663
664  /* Fix the association */
665  CalReorderAssociationFixAfterReallocation(bddManager);
666
667  Cal_Assert(CalCheckAssoc(bddManager));
668 
669
670  /* Update the next pointers */
671  /* Since the pages for the ids are distributed in the uniform
672     manner, we can scan the pages on id by id basis without any
673     disadvantage */
674  for (id = 1; id <= bddManager->numVars; id++){
675    nodeManager = uniqueTable[id]->nodeManager;
676    freeNodeList = Cal_Nil(CalBddNode_t);
677    for (i=0; i<nodeManager->numPages; i++){
678      page = nodeManager->pageList[i];
679      for (bddNode = (CalBddNode_t*) page, numNode = 0;
680           numNode < NUM_NODES_PER_PAGE; numNode++, bddNode += 1){
681        /* If the node is not useful, put it in the free list */
682        if ((bddNode->elseBddId == 0) || (bddNode->elseBddNode == 0)){
683          bddNode->nextBddNode = freeNodeList;
684          freeNodeList = bddNode;
685        }
686      }
687    }
688    nodeManager->freeNodeList = freeNodeList;
689  }
690  /* We should put the unused pages in the free page list */
691  pageSegment = pageManager->pageSegmentArray[numUsefulSegments-1];
692  for (pageCounter = numUsefulPagesInLastSegment;
693       pageCounter < pageSegment->numPages ; pageCounter++){
694    CalPageManagerFreePage(pageManager, pageSegment[pageCounter]);
695  }
696  /* We have to free up the unnecessary page segments;*/
697  for (i = numUsefulSegments; i < pageManager->numSegments; i++){
698    free(pageManager->pageSegmentArray[i]);
699    pageManager->pageSegmentArray[i] = 0;
700  }
701  pageManager->numSegments = numUsefulSegments;
702}
703/**Function********************************************************************
704
705  Synopsis           [required]
706
707  Description        [optional]
708
709  SideEffects        [required]
710
711  SeeAlso            [optional]
712
713******************************************************************************/
714void
715CalAlignCollisionChains(Cal_BddManager_t *bddManager)
716{
717  /* First find out the pages corresponding to each variable */
718  Cal_Address_t ***pageListArray = Cal_MemAlloc(Cal_Address_t **,
719                                                bddManager->numVars+1);
720  for (id = 1; id <= bddManager->numVars; id++){
721    nodeManager = bddManager->nodeManagerArray[id];
722    numPages = nodeManager->numPages;
723    pageListArray[id] = Cal_MemAlloc(Cal_Address_t *, numPages);
724    for (i=0; i<numPages; i++){
725      pageListArray[id][i] = nodeManager->pageList[i];
726    }
727  }
728   
729  /* Bottom up traversal */
730  for (index = bddManager->numVars-1; index >= 0; index--){
731    id = bddManager->indexToId[index];
732    uniqueTableForId = bddManager->uniqueTable[id];
733    nodeManager = uniqueTableForId->nodeManager;
734    /* Calculate the collision lengths */
735    collisionLengthArray = CalculateCollisionLength(uniqueTableForId);
736    /* Initialize the bins */
737    bins = uniqueTableForId->bins;
738    numBins = uniqueTableForId->numBins;
739    numNodes = 0;
740    pageNum = 0;
741    for (i=0; i<numBins; i++){
742      numNodes += collisionLengthArray[i];
743      if (numNodes < NUM_NODES_PER_PAGE){
744        nodePointer[i] += collisionLengthArray[i];
745      }
746      else if (numNodes == NUM_NODES_PER_PAGE){
747        nodePointer[i] = pageListArray[id][++pageNum];
748        numNodes = 0;
749      }
750      else {
751        /* put the rest of the nodes from this page in a free list */
752        nodePointer[i]->nextBddNode = nodeManager->freeNodeList;
753        nodeManager->freeNodeList = nodePointer;
754        nodePointer[i] = pageListArray[id][++pageNum]+collisionLengthArray[i];
755        numNodes = collisionLengthArray[i];
756      }
757    }
758  }
759}
760#endif
761
762/**Function********************************************************************
763
764  Synopsis           [required]
765
766  Description        [optional]
767
768  SideEffects        [required]
769
770  SeeAlso            [optional]
771
772******************************************************************************/
773static void
774BddReallocateNodes(Cal_BddManager_t *bddManager)
775{
776  int i;
777  int index;
778  CalNodeManager_t *nodeManager;
779  CalPageManager_t *pageManager;
780  int numSegments;
781  CalAddress_t **pageSegmentArray;
782 
783  pageManager = bddManager->pageManager2;
784  numSegments = pageManager->numSegments;
785  pageSegmentArray = pageManager->pageSegmentArray;
786 
787  /* Reinitialize the page manager */
788  pageManager->totalNumPages = 0;
789  pageManager->numSegments = 0;
790  pageManager->maxNumSegments = MAX_NUM_SEGMENTS;
791  pageManager->pageSegmentArray
792      = Cal_MemAlloc(CalAddress_t *, pageManager->maxNumSegments);
793  pageManager->freePageList = Cal_Nil(CalAddress_t);
794 
795  /* Do a bottom up traversal */
796
797  for (index = bddManager->numVars-1; index >= 0; index--){
798    int id;
799    CalHashTable_t *uniqueTableForId;
800    int numPagesRequired, newSizeIndex;
801    CalBddNode_t *bddNode, *dupNode, *thenNode, *elseNode, **oldBins;
802    long hashValue, oldNumBins;
803   
804    id = bddManager->indexToId[index];
805    uniqueTableForId = bddManager->uniqueTable[id];
806    nodeManager = bddManager->nodeManagerArray[id];
807    oldBins = uniqueTableForId->bins;
808    oldNumBins = uniqueTableForId->numBins;
809    nodeManager->freeNodeList = Cal_Nil(CalBddNode_t);
810    nodeManager->numPages = 0;
811    numPagesRequired =
812        uniqueTableForId->numEntries/NUM_NODES_PER_PAGE;
813    nodeManager->maxNumPages =
814        2*(numPagesRequired ? numPagesRequired : 1);
815    Cal_MemFree(nodeManager->pageList);
816    nodeManager->pageList = Cal_MemAlloc(CalAddress_t *,
817                                         nodeManager->maxNumPages); 
818    /* Create the new set of bins */
819    newSizeIndex =
820        CeilLog2(uniqueTableForId->numEntries/HASH_TABLE_DEFAULT_MAX_DENSITY);
821    if (newSizeIndex < HASH_TABLE_DEFAULT_SIZE_INDEX){
822      newSizeIndex = HASH_TABLE_DEFAULT_SIZE_INDEX;
823    }
824    uniqueTableForId->sizeIndex = newSizeIndex;
825    uniqueTableForId->numBins =  TABLE_SIZE(uniqueTableForId->sizeIndex);
826    uniqueTableForId->maxCapacity =
827        uniqueTableForId->numBins * HASH_TABLE_DEFAULT_MAX_DENSITY; 
828   
829    uniqueTableForId->bins = Cal_MemAlloc(CalBddNode_t *,
830                                          uniqueTableForId->numBins); 
831    memset((char *)uniqueTableForId->bins, 0, 
832           uniqueTableForId->numBins*sizeof(CalBddNode_t *)); 
833    for (i=0; i<oldNumBins; i++){
834      for (bddNode = oldBins[i]; bddNode; bddNode = bddNode->nextBddNode){ 
835        CalNodeManagerAllocNode(nodeManager, dupNode);
836        thenNode = bddNode->thenBddNode;
837        CalBddNodeIsForwardedTo(thenNode);
838        Cal_Assert(thenNode);
839        Cal_Assert(!CalBddNodeIsForwarded(thenNode));
840        elseNode = bddNode->elseBddNode;
841        CalBddNodeIsForwardedTo(elseNode);
842        Cal_Assert(elseNode);
843        Cal_Assert(!CalBddNodeIsForwarded(CAL_BDD_POINTER(elseNode)));
844        Cal_Assert(bddManager->idToIndex[bddNode->thenBddId] <
845                   bddManager->idToIndex[thenNode->thenBddId]); 
846        Cal_Assert(bddManager->idToIndex[bddNode->thenBddId] <
847                   bddManager->idToIndex[CAL_BDD_POINTER(elseNode)->thenBddId]);
848        dupNode->thenBddNode = thenNode;
849        dupNode->elseBddNode = elseNode;
850        dupNode->thenBddId = bddNode->thenBddId;
851        dupNode->elseBddId = bddNode->elseBddId;
852        hashValue = CalDoHash2(thenNode, elseNode, uniqueTableForId);
853        dupNode->nextBddNode = uniqueTableForId->bins[hashValue];
854        uniqueTableForId->bins[hashValue] = dupNode;
855        bddNode->thenBddNode = dupNode;
856        bddNode->elseBddNode = (CalBddNode_t *)0;
857        bddNode->thenBddId = id;
858        Cal_Assert(bddManager->idToIndex[dupNode->thenBddId] <
859                   bddManager->idToIndex[thenNode->thenBddId]); 
860        Cal_Assert(bddManager->idToIndex[dupNode->thenBddId] <
861                   bddManager->idToIndex[CAL_BDD_POINTER(elseNode)->thenBddId]);
862      }
863    }
864    Cal_MemFree(oldBins);
865    CalBddIsForwardedTo(bddManager->varBdds[id]);
866  }
867
868  if (bddManager->pipelineState == CREATE){
869    /* There are some results computed in pipeline */
870    CalBddReorderFixProvisionalNodes(bddManager);
871  }
872 
873  /* Fix the user BDDs */
874  CalBddReorderFixUserBddPtrs(bddManager);
875
876  /* Fix the association */
877  CalReorderAssociationFix(bddManager);
878
879  Cal_Assert(CalCheckAssoc(bddManager));
880 
881  /* Free the page manager related stuff*/
882  for(i = 0; i < numSegments; i++){
883    free(pageSegmentArray[i]);
884  }
885  Cal_MemFree(pageSegmentArray);
886}
887
888
889/**Function********************************************************************
890
891  Synopsis           [required]
892
893  Description        [optional]
894
895  SideEffects        [required]
896
897  SeeAlso            [optional]
898
899******************************************************************************/
900static void
901BddExchangeAux(Cal_BddManager_t *bddManager, CalBddNode_t *f,
902               int id, int nextId)
903{
904  CalBddNode_t *f0, *f1;
905  CalBddNode_t *f00, *f01, *f10, *f11;
906  CalBddNode_t *newF0, *newF1;
907  int f0Found, f1Found;
908  int fIndex;
909 
910  f0 = f->elseBddNode;
911  f1 = f->thenBddNode;
912
913  if (CAL_BDD_POINTER(f0)->thenBddId == nextId){
914    f00 = BddNodeGetElseBddNode(f0);
915    f01 = BddNodeGetThenBddNode(f0);
916  }
917  else {
918    f00 = f01 = f0;
919  }
920  if (CAL_BDD_POINTER(f1)->thenBddId == nextId){
921    f10 = BddNodeGetElseBddNode(f1);
922    f11 = BddNodeGetThenBddNode(f1);
923  }
924  else {
925    f10 = f11 = f1;
926  }
927 
928  if (f00 == f10){
929    newF0 = f00;
930    f0Found = 1;
931  }
932  else{
933    f0Found = UniqueTableForIdFindOrAdd(bddManager,
934                                        bddManager->uniqueTable[id], f10,
935                                        f00, &newF0);
936  }
937  BddNodeIcrRefCount(newF0);
938  if (f01 == f11){
939    newF1 = f11;
940    f1Found = 1;
941  }
942  else{
943    f1Found = UniqueTableForIdFindOrAdd(bddManager,
944                                        bddManager->uniqueTable[id], f11,
945                                        f01, &newF1);
946  }
947  BddNodeIcrRefCount(newF1);
948
949  f->thenBddId = nextId;
950  f->elseBddNode = newF0;
951  f->thenBddNode = newF1;
952
953  fIndex = bddManager->idToIndex[id];
954  Cal_Assert(fIndex <
955             bddManager->idToIndex[CAL_BDD_POINTER(f00)->thenBddId]);
956  Cal_Assert(fIndex <
957             bddManager->idToIndex[CAL_BDD_POINTER(f10)->thenBddId]);
958  Cal_Assert(fIndex <
959             bddManager->idToIndex[CAL_BDD_POINTER(f01)->thenBddId]);
960  Cal_Assert(fIndex <
961             bddManager->idToIndex[CAL_BDD_POINTER(f11)->thenBddId]);
962  Cal_Assert(CAL_BDD_POINTER(f00)->thenBddId != nextId);
963  Cal_Assert(CAL_BDD_POINTER(f01)->thenBddId != nextId);
964  Cal_Assert(CAL_BDD_POINTER(f10)->thenBddId != nextId);
965  Cal_Assert(CAL_BDD_POINTER(f11)->thenBddId != nextId);
966 
967  if (!f0Found){
968    BddNodeIcrRefCount(f00);
969    BddNodeIcrRefCount(f10);
970  }
971
972  if (!f1Found){
973    BddNodeIcrRefCount(f01);
974    BddNodeIcrRefCount(f11);
975  }
976
977  BddNodeDcrRefCount(f0);
978  BddNodeDcrRefCount(f1);
979}
980
981/**Function********************************************************************
982
983  Synopsis           [required]
984
985  Description        [optional]
986
987  SideEffects        [required]
988
989  SeeAlso            [optional]
990
991******************************************************************************/
992static int
993CheckValidityOfNodes(Cal_BddManager_t *bddManager, long id)
994{
995#ifndef NDEBUG
996  CalHashTable_t *table = bddManager->uniqueTable[id];
997  int i;
998  CalBddNode_t *bddNode;
999  int index = bddManager->idToIndex[id];
1000  for(i = 0; i < table->numBins; ++i){
1001    for (bddNode = table->bins[i]; bddNode; bddNode = bddNode->nextBddNode){
1002      int thenIndex = bddManager->idToIndex[bddNode->thenBddNode->thenBddId];
1003      int elseIndex =
1004        bddManager->idToIndex[CAL_BDD_POINTER(bddNode->elseBddNode)->thenBddId]; 
1005      assert((thenIndex > index) && (elseIndex > index));
1006    }
1007  }
1008#endif
1009  return 1;
1010}
1011
1012/**Function********************************************************************
1013
1014  Synopsis           [required]
1015
1016  Description        [optional]
1017
1018  SideEffects        [required]
1019
1020  SeeAlso            [optional]
1021
1022******************************************************************************/
1023static void
1024SweepVarTable(Cal_BddManager_t *bddManager, long id)
1025{
1026  CalHashTable_t *table = bddManager->uniqueTable[id];
1027  long numNodesFreed, oldNumEntries;
1028  CalBddNode_t **ptr, *bddNode;
1029  int i;
1030 
1031  oldNumEntries = table->numEntries;
1032  for(i = 0; i < table->numBins; ++i){
1033    for (ptr = &table->bins[i], bddNode = *ptr; bddNode;
1034         bddNode = *ptr){
1035      if (bddNode->elseBddId == 0){
1036        *ptr = bddNode->nextBddNode;
1037        CalNodeManagerFreeNode(nodeManager, bddNode);
1038        BddNodeDcrRefCount(bddNode->thenBddNode);
1039        BddNodeDcrRefCount(bddNode->elseBddNode);
1040        table->numEntries--;
1041      }
1042      else{
1043        ptr = &bddNode->nextBddNode;
1044      }
1045    }
1046  }
1047  numNodesFreed = oldNumEntries - table->numEntries;
1048  bddManager->numNodes -= numNodesFreed;
1049  bddManager->numNodesFreed += numNodesFreed;
1050}
1051
1052
1053/**Function********************************************************************
1054
1055  Synopsis           [required]
1056
1057  Description        [optional]
1058
1059  SideEffects        [required]
1060
1061  SeeAlso            [optional]
1062
1063******************************************************************************/
1064static void
1065BddExchange(Cal_BddManager_t *bddManager, long id)
1066{
1067  Cal_BddId_t  nextId;
1068  CalBddNode_t **ptr, *bddNode, *nodeList;
1069  CalHashTable_t *table, *nextTable;
1070  Cal_BddIndex_t index, nextIndex;
1071  int i;
1072  CalBddNode_t  *f1, *f2;
1073  CalAssociation_t *p;
1074  CalNodeManager_t *nodeManager;
1075 
1076  index = bddManager->idToIndex[id];
1077  nextIndex = index+1;
1078  nextId = bddManager->indexToId[nextIndex];
1079
1080  if (CalTestInteract(bddManager, id, nextId)){
1081    bddManager->numSwaps++;
1082    nodeManager = bddManager->nodeManagerArray[id];
1083    table = bddManager->uniqueTable[id];
1084    nextTable = bddManager->uniqueTable[nextId];
1085    nodeList = (CalBddNode_t*)0;
1086    for(i = 0; i < table->numBins; i++){
1087      for (ptr = &table->bins[i], bddNode = *ptr; bddNode;
1088           bddNode = *ptr){
1089        Cal_Assert(bddNode->elseBddId != 0);
1090        f1 = bddNode->elseBddNode;
1091        f2 = bddNode->thenBddNode;
1092        if ((CAL_BDD_POINTER(f1)->thenBddId != nextId) &&
1093            (CAL_BDD_POINTER(f2)->thenBddId != nextId)){ 
1094          ptr = &bddNode->nextBddNode;
1095        }
1096        else{
1097          *ptr = bddNode->nextBddNode;
1098          bddNode->nextBddNode = nodeList;
1099          nodeList = bddNode;
1100        }
1101      }
1102    }
1103    for (bddNode = nodeList; bddNode ; bddNode = nodeList){
1104      BddExchangeAux(bddManager, bddNode, id, nextId);
1105      nodeList = bddNode->nextBddNode;
1106      HashTableAddDirect(nextTable, bddNode);
1107      table->numEntries--;
1108    }
1109    SweepVarTable(bddManager, nextId);
1110  }
1111  else {
1112    bddManager->numTrivialSwaps++;
1113  }
1114 
1115  CalFixupAssoc(bddManager, id, nextId, bddManager->tempAssociation);
1116  for(p = bddManager->associationList; p; p = p->next){
1117    CalFixupAssoc(bddManager, id, nextId, p);
1118  }
1119
1120  bddManager->idToIndex[id] = nextIndex;
1121  bddManager->idToIndex[nextId] = index;
1122  bddManager->indexToId[index] = nextId;
1123  bddManager->indexToId[nextIndex] = id;
1124
1125  Cal_Assert(CheckValidityOfNodes(bddManager, id));
1126  Cal_Assert(CheckValidityOfNodes(bddManager, nextId));
1127  Cal_Assert(CalCheckAssoc(bddManager));
1128#ifdef _CAL_VERBOSE
1129  /*fprintf(stdout,"Variable order after swap:\n");*/
1130  for (i=0; i<bddManager->numVars; i++){
1131    fprintf(stdout, "%3d ", bddManager->indexToId[i]);
1132  }
1133  fprintf(stdout, "%8d\n", bddManager->numNodes);
1134#endif
1135}
1136
1137
1138/**Function********************************************************************
1139
1140  Synopsis           [required]
1141
1142  Description        [optional]
1143
1144  SideEffects        [required]
1145
1146  SeeAlso            [optional]
1147
1148******************************************************************************/
1149static void
1150BddExchangeVarBlocks(Cal_BddManager_t *bddManager, Cal_Block parent,
1151                     long blockIndex)
1152{
1153  Cal_Block b1, b2, temp;
1154  long i, j, k, l, firstBlockWidth, secondBlockWidth;
1155
1156  b1 = parent->children[blockIndex];
1157  b2 = parent->children[blockIndex+1];
1158  /* This slides the blocks past each other in a kind of interleaving */
1159  /* fashion. */
1160  firstBlockWidth = b1->lastIndex - b1->firstIndex;
1161  secondBlockWidth = b2->lastIndex - b2->firstIndex;
1162 
1163  for (i=0; i <= firstBlockWidth + secondBlockWidth; i++){
1164    j = i - firstBlockWidth;
1165    if (j < 0) j=0;
1166    k = ((i > secondBlockWidth) ? secondBlockWidth : i);
1167    while (j <= k) {
1168          l = b2->firstIndex + j - i + j;
1169          BddExchange(bddManager, bddManager->indexToId[l-1]);
1170          ++j;
1171        }
1172  }
1173  CalBddBlockDelta(b1, secondBlockWidth+1);
1174  CalBddBlockDelta(b2, -(firstBlockWidth+1));
1175  temp = parent->children[blockIndex];
1176  parent->children[blockIndex] = parent->children[blockIndex+1];
1177  parent->children[blockIndex+1] = temp;
1178}
1179
1180/**Function********************************************************************
1181
1182  Synopsis           [required]
1183
1184  Description        [optional]
1185
1186  SideEffects        [required]
1187
1188  SeeAlso            [optional]
1189
1190******************************************************************************/
1191static int
1192BddReorderWindow2(Cal_BddManager_t *bddManager, Cal_Block block, long i)
1193{
1194  long size, bestSize;
1195
1196  /* 1 2 */
1197  bestSize = bddManager->numNodes;
1198  BddExchangeVarBlocks(bddManager, block, i);
1199  /* 2 1 */
1200  size = bddManager->numNodes;
1201  if (size < bestSize) return (1);
1202  BddExchangeVarBlocks(bddManager, block, i);
1203  return (0);
1204}
1205
1206
1207/**Function********************************************************************
1208
1209  Synopsis           [required]
1210
1211  Description        [optional]
1212
1213  SideEffects        [required]
1214
1215  SeeAlso            [optional]
1216
1217******************************************************************************/
1218static int
1219BddReorderWindow3(Cal_BddManager_t *bddManager, Cal_Block block, long i)
1220{
1221  int best;
1222  long size, bestSize;
1223  long origSize;
1224 
1225  origSize = bddManager->numNodes;
1226  best = 0;
1227  /* 1 2 3 */
1228  bestSize = bddManager->numNodes;
1229  BddExchangeVarBlocks(bddManager, block, i);
1230  /* 2 1 3 */
1231  size=bddManager->numNodes;
1232  if (size < bestSize) {
1233    best=1;
1234    bestSize=size;
1235  }
1236  BddExchangeVarBlocks(bddManager, block, i+1);
1237  /* 2 3 1 */
1238  size=bddManager->numNodes;
1239  if (size < bestSize) {
1240    best=2;
1241    bestSize=size;
1242  }
1243  BddExchangeVarBlocks(bddManager, block, i);
1244  /* 3 2 1 */
1245  size=bddManager->numNodes;
1246  if (size <= bestSize) {
1247    best=3;
1248    bestSize=size;
1249  }
1250  BddExchangeVarBlocks(bddManager, block, i+1);
1251  /* 3 1 2 */
1252  size=bddManager->numNodes;
1253  if (size <= bestSize) {
1254    best=4;
1255    bestSize=size;
1256  }
1257  BddExchangeVarBlocks(bddManager, block, i);
1258  /* 1 3 2 */
1259  size=bddManager->numNodes;
1260  if (size <= bestSize) {
1261    best=5;
1262    bestSize=size;
1263  }
1264  switch (best){
1265      case 0:
1266        BddExchangeVarBlocks(bddManager, block, i+1);
1267        break;
1268      case 1:
1269        BddExchangeVarBlocks(bddManager, block, i+1);
1270        BddExchangeVarBlocks(bddManager, block, i);
1271        break;
1272      case 2:
1273        BddExchangeVarBlocks(bddManager, block, i+1);
1274        BddExchangeVarBlocks(bddManager, block, i);
1275        BddExchangeVarBlocks(bddManager, block, i+1);
1276        break;
1277      case 3:
1278        BddExchangeVarBlocks(bddManager, block, i);
1279        BddExchangeVarBlocks(bddManager, block, i+1);
1280        break;
1281      case 4:
1282        BddExchangeVarBlocks(bddManager, block, i);
1283        break;
1284      case 5:
1285        break;
1286  }
1287  return ((best > 0) && (origSize > bestSize));
1288}
1289
1290/**Function********************************************************************
1291
1292  Synopsis           [required]
1293
1294  Description        [optional]
1295
1296  SideEffects        [required]
1297
1298  SeeAlso            [optional]
1299
1300******************************************************************************/
1301static void
1302BddReorderStableWindow3Aux(Cal_BddManager_t *bddManager, Cal_Block block,
1303                           char *levels) 
1304{
1305  long i;
1306  int moved;
1307  int anySwapped;
1308
1309  if (block->reorderable) {
1310    for (i=0; i < block->numChildren-1; ++i) levels[i]=1;
1311    do {
1312          anySwapped=0;
1313          for (i=0; i < block->numChildren-1; i++){
1314            if (levels[i]){
1315#ifdef _CAL_VERBOSE
1316          fprintf(stdout,"Moving block %3d -- %3d\n",
1317                  bddManager->indexToId[block->children[i]-> firstIndex],
1318                  bddManager->indexToId[block->children[i]->lastIndex]);
1319          fflush(stdout);
1320          for (j=0; j<bddManager->numVars; j++){
1321            fprintf(stdout, "%3d ", bddManager->indexToId[j]);
1322          }
1323          fprintf(stdout, "%8d\n", bddManager->numNodes);
1324#endif
1325          if (i < block->numChildren-2){
1326            moved = BddReorderWindow3(bddManager, block, i);
1327          }
1328          else{
1329            moved = BddReorderWindow2(bddManager, block, i);
1330          }
1331          if (moved){
1332                    if (i > 0) {
1333              levels[i-1]=1;
1334              if (i > 1)
1335                levels[i-2]=1;
1336            }
1337                    levels[i]=1;
1338                    levels[i+1]=1;
1339                    if (i < block->numChildren-2){
1340              levels[i+2]=1;
1341              if (i < block->numChildren-3) {
1342                            levels[i+3]=1;
1343                            if (i < block->numChildren-4) levels[i+4]=1;
1344                          }
1345            }
1346                    anySwapped=1;
1347          }
1348          else levels[i]=0;
1349        }
1350      }
1351    } while (anySwapped);
1352  }
1353  for (i=0; i < block->numChildren; ++i){
1354    BddReorderStableWindow3Aux(bddManager, block->children[i], levels);
1355  }
1356}
1357
1358/**Function********************************************************************
1359
1360  Synopsis           [required]
1361
1362  Description        [optional]
1363
1364  SideEffects        [required]
1365
1366  SeeAlso            [optional]
1367
1368******************************************************************************/
1369static void
1370BddReorderStableWindow3(Cal_BddManager_t *bddManager)
1371{
1372  char *levels;
1373  levels =  Cal_MemAlloc(char, bddManager->numVars);
1374  bddManager->numSwaps = 0;
1375  BddReorderStableWindow3Aux(bddManager, bddManager->superBlock, levels);
1376  Cal_MemFree(levels);
1377}
1378
1379/**Function********************************************************************
1380
1381  Synopsis           [required]
1382
1383  Description        [optional]
1384
1385  SideEffects        [required]
1386
1387  SeeAlso            [optional]
1388
1389******************************************************************************/
1390static void
1391BddSiftBlock(Cal_BddManager_t *bddManager, Cal_Block block, long
1392             startPosition, double maxSizeFactor)
1393{
1394  long startSize;
1395  long bestSize;
1396  long bestPosition;
1397  long currentSize;
1398  long currentPosition;
1399  long maxSize;
1400 
1401  startSize = bddManager->numNodes;
1402  bestSize = startSize;
1403  bestPosition = startPosition;
1404  currentSize = startSize;
1405  currentPosition = startPosition;
1406  maxSize = maxSizeFactor*startSize;
1407  if (bddManager->nodeLimit && maxSize > bddManager->nodeLimit)
1408    maxSize = bddManager->nodeLimit;
1409
1410  /* Need to do optimization here */
1411  if (startPosition > (block->numChildren >> 1)){
1412    while (currentPosition < block->numChildren-1 && currentSize <= maxSize){
1413      BddExchangeVarBlocks(bddManager, block, currentPosition);
1414      ++currentPosition;
1415      currentSize = bddManager->numNodes;
1416      if (currentSize < bestSize){
1417        bestSize = currentSize;
1418        bestPosition=currentPosition;
1419      }
1420    }
1421    while (currentPosition != startPosition){
1422      --currentPosition;
1423      BddExchangeVarBlocks(bddManager, block, currentPosition);
1424    }
1425    currentSize = startSize;
1426    while (currentPosition && currentSize <= maxSize){
1427      --currentPosition;
1428      BddExchangeVarBlocks(bddManager, block, currentPosition);
1429      currentSize = bddManager->numNodes;
1430      if (currentSize <= bestSize){
1431        bestSize = currentSize;
1432        bestPosition = currentPosition;
1433      }
1434    }
1435    while (currentPosition != bestPosition){
1436      BddExchangeVarBlocks(bddManager, block, currentPosition);
1437      ++currentPosition;
1438    }
1439  }
1440  else{
1441    while (currentPosition && currentSize <= maxSize){
1442      --currentPosition;
1443      BddExchangeVarBlocks(bddManager, block, currentPosition);
1444      currentSize = bddManager->numNodes;
1445      if (currentSize < bestSize){
1446        bestSize = currentSize;
1447        bestPosition = currentPosition;
1448      }
1449    }
1450    while (currentPosition != startPosition){
1451      BddExchangeVarBlocks(bddManager, block, currentPosition);
1452      ++currentPosition;
1453    }
1454    currentSize = startSize;
1455    while (currentPosition < block->numChildren-1 && currentSize <= maxSize){
1456      BddExchangeVarBlocks(bddManager, block, currentPosition);
1457      currentSize = bddManager->numNodes;
1458      ++currentPosition;
1459      if (currentSize <= bestSize){
1460        bestSize = currentSize;
1461        bestPosition = currentPosition;
1462      }
1463    }
1464    while (currentPosition != bestPosition){
1465      --currentPosition;
1466      BddExchangeVarBlocks(bddManager, block, currentPosition);
1467    }
1468  }
1469}
1470
1471
1472
1473/**Function********************************************************************
1474
1475  Synopsis    [Reorder variables using "sift" algorithm.]
1476
1477  Description [Reorder variables using "sift" algorithm.]
1478
1479  SideEffects [None]
1480
1481******************************************************************************/
1482static void
1483BddReorderSiftAux(Cal_BddManager_t *bddManager, Cal_Block block,
1484                     Cal_Block *toSift, double maxSizeFactor) 
1485{
1486  long i, j, k;
1487  long width;
1488  long maxWidth;
1489  long widest;
1490  long numVarsShifted = 0;
1491  bddManager->numSwaps = 0;
1492  if (block->reorderable) {
1493    for (i=0; i < block->numChildren; ++i){
1494      toSift[i] = block->children[i];
1495    }
1496    while (i &&
1497           (numVarsShifted <=
1498            bddManager->maxNumVarsSiftedPerReordering) &&
1499           (bddManager->numSwaps <=
1500            bddManager->maxNumSwapsPerReordering)){ 
1501          i--;
1502      numVarsShifted++;
1503          maxWidth = 0;
1504          widest = 0;
1505          for (j=0; j <= i; ++j) {
1506        for (width=0, k=toSift[j]->firstIndex; k <= toSift[j]->lastIndex; ++k){
1507          width +=
1508              bddManager->uniqueTable[bddManager->indexToId[k]]->numEntries; 
1509        }
1510        width /= toSift[j]->lastIndex - toSift[j]->firstIndex+1;
1511        if (width > maxWidth) {
1512                  maxWidth = width;
1513                  widest = j;
1514                }
1515      }
1516          if (maxWidth > 1) {
1517        for (j=0; block->children[j] != toSift[widest]; ++j);
1518#ifdef _CAL_VERBOSE
1519        fprintf(stdout,"Moving block %3d -- %3d\n",
1520                bddManager->indexToId[block->children[j]-> firstIndex],
1521                bddManager->indexToId[block->children[j]->lastIndex]);
1522        fflush(stdout);
1523        for (l=0; l<bddManager->numVars; l++){
1524          fprintf(stdout, "%3d ", bddManager->indexToId[l]);
1525        }
1526        fprintf(stdout, "%8d\n", bddManager->numNodes);
1527#endif
1528        BddSiftBlock(bddManager, block, j, maxSizeFactor);
1529        toSift[widest] = toSift[i];
1530      }
1531          else {
1532        break;
1533      }
1534        }
1535  }
1536  for (i=0; i < block->numChildren; ++i)
1537    BddReorderSiftAux(bddManager, block->children[i], toSift,
1538                      maxSizeFactor); 
1539}
1540
1541/**Function********************************************************************
1542
1543  Synopsis           [required]
1544
1545  Description        [optional]
1546
1547  SideEffects        [required]
1548
1549  SeeAlso            [optional]
1550
1551******************************************************************************/
1552static void
1553BddReorderSift(Cal_BddManager_t *bddManager, double maxSizeFactor)
1554{
1555  Cal_Block *toSift;
1556
1557  toSift = Cal_MemAlloc(Cal_Block, bddManager->numVars);
1558  BddReorderSiftAux(bddManager, bddManager->superBlock, toSift,
1559                       maxSizeFactor); 
1560  Cal_MemFree(toSift);
1561}
1562
1563
1564
1565
1566/**Function********************************************************************
1567
1568  Synopsis    [Returns the smallest integer greater than or equal to log2 of a
1569  number]
1570
1571  Description [Returns the smallest integer greater than or equal to log2 of a
1572  number (The assumption is that the number is >= 1)]
1573
1574  SideEffects [None]
1575
1576******************************************************************************/
1577static int
1578CeilLog2(int  number)
1579{
1580  int num, count;
1581  for (num=number, count=0; num > 1; num >>= 1, count++);
1582  if ((1 << count) != number) count++;
1583  return count;
1584}
Note: See TracBrowser for help on using the repository browser.