source: vis_dev/glu-2.3/src/calBdd/calHashTable.c @ 21

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

library glu 2.3
File size: 33.3 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [calHashTable.c]
4
5  PackageName [cal]
6
7  Synopsis    [Functions to manage the hash tables that are a part of
8                  1. unique table
9                  2. request queue
10               ]
11
12  Author      [Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)
13                Rajeev Ranjan   (rajeev@eecs.berkeley.edu)
14              ]
15  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
16  All rights reserved.
17
18  Permission is hereby granted, without written agreement and without license
19  or royalty fees, to use, copy, modify, and distribute this software and its
20  documentation for any purpose, provided that the above copyright notice and
21  the following two paragraphs appear in all copies of this software.
22
23  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
24  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
25  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
26  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
27
28  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
29  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
30  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
31  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
32  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
33
34  Revision    [$Id: calHashTable.c,v 1.9 2002/09/21 20:39:25 fabio Exp $]
35
36******************************************************************************/
37
38#include "calInt.h"
39
40/*---------------------------------------------------------------------------*/
41/* Constant declarations                                                     */
42/*---------------------------------------------------------------------------*/
43
44
45/*---------------------------------------------------------------------------*/
46/* Type declarations                                                         */
47/*---------------------------------------------------------------------------*/
48
49
50/*---------------------------------------------------------------------------*/
51/* Stucture declarations                                                     */
52/*---------------------------------------------------------------------------*/
53
54
55/*---------------------------------------------------------------------------*/
56/* Variable declarations                                                     */
57/*---------------------------------------------------------------------------*/
58
59/*---------------------------------------------------------------------------*/
60/* Macro declarations                                                        */
61/*---------------------------------------------------------------------------*/
62
63/**AutomaticStart*************************************************************/
64
65/*---------------------------------------------------------------------------*/
66/* Static function prototypes                                                */
67/*---------------------------------------------------------------------------*/
68
69static int CeilLog2(int number);
70
71/**AutomaticEnd***************************************************************/
72
73
74/*---------------------------------------------------------------------------*/
75/* Definition of exported functions                                          */
76/*---------------------------------------------------------------------------*/
77
78
79/*---------------------------------------------------------------------------*/
80/* Definition of internal functions                                          */
81/*---------------------------------------------------------------------------*/
82
83/**Function********************************************************************
84
85  Synopsis    [Initialize a hash table using default parameters.]
86
87  Description [optional]
88
89  SideEffects [required]
90
91  SeeAlso     [optional]
92
93******************************************************************************/
94CalHashTable_t *
95CalHashTableInit(Cal_BddManager_t *bddManager, Cal_BddId_t  bddId)
96{
97  CalHashTable_t *hashTable;
98
99  hashTable = Cal_MemAlloc(CalHashTable_t, 1);
100  /*hashTable = CAL_BDD_NEW_REC(bddManager, CalHashTable_t);*/
101  if(hashTable == Cal_Nil(CalHashTable_t)){
102    CalBddFatalMessage("out of memory");
103  }
104  hashTable->sizeIndex = HASH_TABLE_DEFAULT_SIZE_INDEX;
105  hashTable->numBins = TABLE_SIZE(hashTable->sizeIndex);
106  hashTable->maxCapacity = hashTable->numBins*HASH_TABLE_DEFAULT_MAX_DENSITY;
107  hashTable->bins = Cal_MemAlloc(CalBddNode_t *, hashTable->numBins);
108  if(hashTable->bins == Cal_Nil(CalBddNode_t *)){
109    CalBddFatalMessage("out of memory");
110  }
111  memset((char *)hashTable->bins, 0,
112         hashTable->numBins*sizeof(CalBddNode_t *)); 
113  hashTable->bddId = bddId;
114  hashTable->nodeManager = bddManager->nodeManagerArray[bddId];
115  hashTable->requestNodeList = Cal_Nil(CalRequestNode_t);
116  memset((char *)(&(hashTable->startNode)), 0, sizeof(CalBddNode_t));
117  hashTable->endNode = &(hashTable->startNode);
118  hashTable->numEntries = 0;
119  return hashTable;
120}
121
122
123/**Function********************************************************************
124
125  Synopsis    [Free a hash table along with the associated storage.]
126
127  Description [optional]
128
129  SideEffects [required]
130
131  SeeAlso     [optional]
132
133******************************************************************************/
134int
135CalHashTableQuit(Cal_BddManager_t *bddManager, CalHashTable_t * hashTable)
136{
137  if(hashTable == Cal_Nil(CalHashTable_t))return 1;
138  /*
139  for(i = 0; i < hashTable->numBins; i++){
140    ptr = hashTable->bins[i];
141    while(ptr != Cal_Nil(CalBddNode_t)){
142      next = CalBddNodeGetNextBddNode(ptr);
143      CalNodeManagerFreeNode(hashTable->nodeManager, ptr);
144      ptr = next;
145    }
146  }
147  There is no need to free the nodes individually. They will be taken
148  care of by the PageManagerQuit.
149  We need to make sure that this function is called only during the global quitting.
150  If it need be called at some intermediate point, we need to free the BDD nodes
151  appropriately.
152  */
153 
154  Cal_MemFree(hashTable->bins);
155  Cal_MemFree(hashTable);
156  /*CAL_BDD_FREE_REC(bddManager, hashTable, CalHashTable_t);*/
157  return 0;
158}
159
160
161
162/**Function********************************************************************
163
164  Synopsis    [Directly insert a BDD node in the hash table.]
165
166  Description [optional]
167
168  SideEffects [required]
169
170  SeeAlso     [optional]
171
172******************************************************************************/
173void
174CalHashTableAddDirect(CalHashTable_t * hashTable, CalBddNode_t * bddNode)
175{
176  int hashValue;
177  CalBddNode_t *thenBddNode, *elseBddNode;
178
179  hashTable->numEntries++;
180  if(hashTable->numEntries >= hashTable->maxCapacity){
181    CalHashTableRehash(hashTable, 1);
182  }
183  thenBddNode = CalBddNodeGetThenBddNode(bddNode);
184  elseBddNode = CalBddNodeGetElseBddNode(bddNode);
185  hashValue = CalDoHash2(thenBddNode, elseBddNode, hashTable);
186  CalBddNodePutNextBddNode(bddNode, hashTable->bins[hashValue]);
187  hashTable->bins[hashValue] = bddNode;
188}
189
190
191/**Function********************************************************************
192
193  Synopsis    [required]
194
195  Description [optional]
196
197  SideEffects [required]
198
199  SeeAlso     [optional]
200
201******************************************************************************/
202int
203CalHashTableFindOrAdd(CalHashTable_t * hashTable,
204                      Cal_Bdd_t  thenBdd,
205                      Cal_Bdd_t  elseBdd,
206                      Cal_Bdd_t * bddPtr)
207{
208  CalBddNode_t *ptr;
209  Cal_Bdd_t tmpBdd;
210  int hashValue;
211 
212  hashValue = CalDoHash2(CalBddGetBddNode(thenBdd), 
213      CalBddGetBddNode(elseBdd), hashTable);
214  ptr = hashTable->bins[hashValue];
215  while(ptr != Cal_Nil(CalBddNode_t)){
216    CalBddNodeGetThenBdd(ptr, tmpBdd);
217    if(CalBddIsEqual(thenBdd, tmpBdd)){
218      CalBddNodeGetElseBdd(ptr, tmpBdd);
219      if(CalBddIsEqual(elseBdd, tmpBdd)){
220        CalBddPutBddId(*bddPtr, hashTable->bddId);
221        CalBddPutBddNode(*bddPtr, ptr);
222        return 1;
223      }
224    }
225    ptr = CalBddNodeGetNextBddNode(ptr);
226  }
227  hashTable->numEntries++;
228  if(hashTable->numEntries > hashTable->maxCapacity){
229    CalHashTableRehash(hashTable,1);
230    hashValue = CalDoHash2(CalBddGetBddNode(thenBdd),
231        CalBddGetBddNode(elseBdd), hashTable);
232  }
233  CalNodeManagerInitBddNode(hashTable->nodeManager, thenBdd, elseBdd, 
234      hashTable->bins[hashValue], ptr);
235  hashTable->bins[hashValue] = ptr;
236  CalBddPutBddId(*bddPtr, hashTable->bddId);
237  CalBddPutBddNode(*bddPtr, ptr);
238  return 0;
239}
240
241/**Function********************************************************************
242
243  Synopsis    [required]
244
245  Description [optional]
246
247  SideEffects [required]
248
249  SeeAlso     [optional]
250
251******************************************************************************/
252int
253CalHashTableAddDirectAux(CalHashTable_t * hashTable, Cal_Bdd_t
254                         thenBdd, Cal_Bdd_t  elseBdd, Cal_Bdd_t *
255                         bddPtr) 
256{
257  CalBddNode_t *ptr;
258  int hashValue;
259 
260  hashTable->numEntries++;
261  if(hashTable->numEntries >= hashTable->maxCapacity){
262    CalHashTableRehash(hashTable, 1);
263  }
264  hashValue = CalDoHash2(CalBddGetBddNode(thenBdd), CalBddGetBddNode(elseBdd),
265                         hashTable); 
266  CalNodeManagerInitBddNode(hashTable->nodeManager, thenBdd, elseBdd, 
267      hashTable->bins[hashValue], ptr);
268  hashTable->bins[hashValue] = ptr;
269  CalBddPutBddId(*bddPtr, hashTable->bddId);
270  CalBddPutBddNode(*bddPtr, ptr);
271  return 0;
272}
273
274/**Function********************************************************************
275
276  Synopsis    [required]
277
278  Description [optional]
279
280  SideEffects [required]
281
282  SeeAlso     [optional]
283
284******************************************************************************/
285void
286CalHashTableCleanUp(CalHashTable_t * hashTable)
287{
288  CalNodeManager_t *nodeManager;
289
290  nodeManager = hashTable->nodeManager;
291  hashTable->endNode->nextBddNode = nodeManager->freeNodeList;
292  nodeManager->freeNodeList = hashTable->startNode.nextBddNode;
293  hashTable->endNode = &(hashTable->startNode);
294  hashTable->numEntries = 0;
295  hashTable->startNode.nextBddNode = NULL;
296  Cal_Assert(!(hashTable->requestNodeList));
297  hashTable->requestNodeList = Cal_Nil(CalRequestNode_t);
298  return;
299}
300
301
302/**Function********************************************************************
303
304  Synopsis    [required]
305
306  Description [optional]
307
308  SideEffects [required]
309
310  SeeAlso     [optional]
311
312******************************************************************************/
313int
314CalHashTableLookup(
315  CalHashTable_t * hashTable,
316  Cal_Bdd_t  thenBdd,
317  Cal_Bdd_t  elseBdd,
318  Cal_Bdd_t * bddPtr)
319{
320  CalBddNode_t *ptr;
321  Cal_Bdd_t tmpBdd;
322  int hashValue;
323 
324  hashValue = CalDoHash2(CalBddGetBddNode(thenBdd),
325      CalBddGetBddNode(elseBdd), hashTable);
326  ptr = hashTable->bins[hashValue];
327  while(ptr != Cal_Nil(CalBddNode_t)){
328    CalBddNodeGetThenBdd(ptr, tmpBdd);
329    if(CalBddIsEqual(thenBdd, tmpBdd)){
330      CalBddNodeGetElseBdd(ptr, tmpBdd);
331      if(CalBddIsEqual(elseBdd, tmpBdd)){
332        CalBddPutBddId(*bddPtr, hashTable->bddId);
333        CalBddPutBddNode(*bddPtr, ptr);
334        return 1;
335      }
336    }
337    ptr = CalBddNodeGetNextBddNode(ptr);
338  }
339  return 0;
340}
341
342/**Function********************************************************************
343
344  Synopsis    [Deletes a BDD node in the hash table.]
345
346  Description [optional]
347
348  SideEffects [required]
349
350  SeeAlso     [optional]
351
352******************************************************************************/
353void
354CalHashTableDelete(CalHashTable_t * hashTable, CalBddNode_t * bddNode)
355{
356  int hashValue;
357  Cal_Bdd_t thenBdd, elseBdd;
358  CalBddNode_t  *ptr, *last;
359
360  CalBddNodeGetThenBdd(bddNode, thenBdd);
361  CalBddNodeGetElseBdd(bddNode, elseBdd);
362  hashValue =
363      CalDoHash2(CalBddGetBddNode(thenBdd), CalBddGetBddNode(elseBdd), hashTable);
364
365  last = Cal_Nil(CalBddNode_t);
366  ptr = hashTable->bins[hashValue];
367  while(ptr != Cal_Nil(CalBddNode_t)){
368    if(ptr == bddNode){
369      if(last == Cal_Nil(CalBddNode_t)){
370        hashTable->bins[hashValue] = CalBddNodeGetNextBddNode(ptr);
371      }
372      else{
373        CalBddNodePutNextBddNode(last, CalBddNodeGetNextBddNode(ptr));
374      }
375      hashTable->numEntries--;
376      CalNodeManagerFreeNode(hashTable->nodeManager, ptr);
377      return;
378    }
379    last = ptr;
380    ptr = CalBddNodeGetNextBddNode(ptr);
381  }
382  CalBddWarningMessage("Trying to delete a non-existent node\n");
383}
384
385
386/**Function********************************************************************
387
388  Synopsis    [Lookup unique table for id.]
389
390  Description [optional]
391
392  SideEffects [required]
393
394  SeeAlso     [optional]
395
396******************************************************************************/
397int
398CalUniqueTableForIdLookup(
399  Cal_BddManager_t * bddManager,
400  CalHashTable_t * hashTable,
401  Cal_Bdd_t  thenBdd,
402  Cal_Bdd_t  elseBdd,
403  Cal_Bdd_t * bddPtr)
404{
405  CalBddNode_t *ptr;
406  Cal_Bdd_t tmpBdd;
407  int hashValue;
408 
409  hashValue = CalDoHash2(CalBddGetBddNode(thenBdd),
410      CalBddGetBddNode(elseBdd), hashTable);
411  ptr = hashTable->bins[hashValue];
412  if(CalBddIsOutPos(thenBdd)){
413    while(ptr != Cal_Nil(CalBddNode_t)){
414      CalBddNodeGetThenBdd(ptr, tmpBdd);
415      if(CalBddIsEqual(thenBdd, tmpBdd)){
416        CalBddNodeGetElseBdd(ptr, tmpBdd);
417        if(CalBddIsEqual(elseBdd, tmpBdd)){
418          CalBddPutBddId(*bddPtr, hashTable->bddId);
419          CalBddPutBddNode(*bddPtr, ptr);
420          return 1;
421        }
422      }
423      ptr = CalBddNodeGetNextBddNode(ptr);
424    }
425  }
426  else{
427    CalBddNot(thenBdd, thenBdd);
428    CalBddNot(elseBdd, elseBdd);
429    while(ptr != Cal_Nil(CalBddNode_t)){
430      CalBddNodeGetThenBdd(ptr, tmpBdd);
431      if(CalBddIsEqual(thenBdd, tmpBdd)){
432        CalBddNodeGetElseBdd(ptr, tmpBdd);
433        if(CalBddIsEqual(elseBdd, tmpBdd)){
434          CalBddPutBddId(*bddPtr, hashTable->bddId);
435          CalBddPutBddNode(*bddPtr, CalBddNodeNot(ptr));
436          return 1;
437        }
438      }
439      ptr = CalBddNodeGetNextBddNode(ptr);
440    }
441  }
442  return 0;
443}
444
445
446/**Function********************************************************************
447
448  Synopsis    [find or add in the unique table for id.]
449
450  Description [optional]
451
452  SideEffects [If a new BDD node is created (found == false), then the
453  numNodes field of the manager needs to be incremented.]
454
455  SeeAlso     [optional]
456
457******************************************************************************/
458int
459CalUniqueTableForIdFindOrAdd(
460  Cal_BddManager_t * bddManager,
461  CalHashTable_t * hashTable,
462  Cal_Bdd_t  thenBdd,
463  Cal_Bdd_t  elseBdd,
464  Cal_Bdd_t * bddPtr)
465{
466  int found = 0; 
467  if (CalBddIsEqual(thenBdd, elseBdd)){
468    *bddPtr = thenBdd;
469    found = 1;
470  }
471  else if(CalBddIsOutPos(thenBdd)){
472    found = CalHashTableFindOrAdd(hashTable, thenBdd, elseBdd, bddPtr);
473  }
474  else{
475    CalBddNot(thenBdd, thenBdd);
476    CalBddNot(elseBdd, elseBdd);
477    found = CalHashTableFindOrAdd(hashTable, thenBdd, elseBdd, bddPtr);
478    CalBddNot(*bddPtr, *bddPtr);
479  }
480  if (!found) bddManager->numNodes++;
481  return found;
482}
483
484
485/**Function********************************************************************
486
487  Synopsis    [required]
488
489  Description [optional]
490
491  SideEffects [required]
492
493  SeeAlso     [optional]
494
495******************************************************************************/
496
497void
498CalHashTableRehash(CalHashTable_t *hashTable,int grow)
499{
500  CalBddNode_t *ptr, *next;
501  CalBddNode_t **oldBins = hashTable->bins;
502  int i, hashValue;
503  int oldNumBins = hashTable->numBins;
504
505  if(grow){
506    hashTable->sizeIndex++;
507  }
508  else{
509    if (hashTable->sizeIndex <= HASH_TABLE_DEFAULT_SIZE_INDEX){/* No need to rehash */
510      return;
511    }
512    hashTable->sizeIndex--;
513  }
514
515  hashTable->numBins = TABLE_SIZE(hashTable->sizeIndex);
516  hashTable->maxCapacity = hashTable->numBins * HASH_TABLE_DEFAULT_MAX_DENSITY;
517  hashTable->bins = Cal_MemAlloc(CalBddNode_t *, hashTable->numBins);
518  if(hashTable->bins == Cal_Nil(CalBddNode_t *)){
519    CalBddFatalMessage("out of memory");
520  }
521  /*
522  for(i = 0; i < hashTable->numBins; i++){
523    hashTable->bins[i] = Cal_Nil(CalBddNode_t);
524  }
525  */
526  memset((char *)hashTable->bins, 0,
527         hashTable->numBins*sizeof(CalBddNode_t *));
528
529  for(i = 0; i < oldNumBins; i++){
530    ptr = oldBins[i];
531    while(ptr != Cal_Nil(CalBddNode_t)){
532      next = CalBddNodeGetNextBddNode(ptr);
533      hashValue = CalDoHash2(CalBddNodeGetThenBddNode(ptr),
534          CalBddNodeGetElseBddNode(ptr), hashTable);
535      CalBddNodePutNextBddNode(ptr, hashTable->bins[hashValue]);
536      hashTable->bins[hashValue] = ptr;
537      ptr = next;
538    }
539  }
540  Cal_MemFree(oldBins);
541}
542
543/**Function********************************************************************
544
545  Synopsis    [required]
546
547  Description [optional]
548
549  SideEffects [required]
550
551  SeeAlso     [optional]
552
553******************************************************************************/
554void
555CalUniqueTableForIdRehashNode(CalHashTable_t *hashTable, CalBddNode_t *bddNode,
556                              CalBddNode_t *thenBddNode,
557                              CalBddNode_t *elseBddNode)
558
559{
560  CalBddNode_t *nextBddNode;
561  CalBddNode_t *ptr;
562  int found;
563  int hashValue;
564  int oldHashValue;
565  Cal_Bdd_t thenBdd;
566
567  oldHashValue = CalDoHash2(thenBddNode, elseBddNode, hashTable);
568  hashValue = CalDoHash2(CalBddNodeGetThenBddNode(bddNode),
569                         CalBddNodeGetElseBddNode(bddNode),
570                         hashTable);
571  CalBddNodeGetThenBdd(bddNode, thenBdd);
572  if (CalBddIsComplement(thenBdd)) {
573    CalBddFatalMessage("Complement edge on then pointer");
574  }
575  if (oldHashValue == hashValue) {
576    return;
577  }
578
579  found = 0;
580  ptr = hashTable->bins[oldHashValue];
581  if ((ptr != Cal_Nil(CalBddNode_t)) && (ptr == bddNode)) {
582    hashTable->bins[oldHashValue] = CalBddNodeGetNextBddNode(bddNode);
583    found = 1;
584  } else {
585    while (ptr != Cal_Nil(CalBddNode_t)) {
586      nextBddNode = CalBddNodeGetNextBddNode(ptr);
587      if (nextBddNode == bddNode) {
588        CalBddNodePutNextBddNode(ptr, CalBddNodeGetNextBddNode(bddNode));
589        found = 1;
590        break;
591      }
592      ptr = nextBddNode;
593    }
594  }
595
596  if (!found) {
597    CalBddFatalMessage("Node not found in the unique table");
598  } else {
599    CalBddNodePutNextBddNode(bddNode, hashTable->bins[hashValue]);
600    hashTable->bins[hashValue] = bddNode;
601  }
602}
603
604/**Function********************************************************************
605
606  Synopsis           [required]
607
608  Description        [optional]
609
610  SideEffects        [required]
611
612  SeeAlso            [optional]
613
614******************************************************************************/
615 
616unsigned long
617CalBddUniqueTableNumLockedNodes(Cal_BddManager_t *bddManager,
618                                CalHashTable_t *uniqueTableForId)
619{
620  CalBddNode_t *bddNode;
621  long i;
622  unsigned long numLockedNodes = 0;
623 
624  for(i=0; i<uniqueTableForId->numBins; i++){
625    bddNode = uniqueTableForId->bins[i];
626    while (bddNode){
627      numLockedNodes += CalBddNodeIsRefCountMax(bddNode);
628      bddNode = CalBddNodeGetNextBddNode(bddNode);
629    }
630  }
631  return numLockedNodes;
632}
633
634/**Function********************************************************************
635
636  Synopsis           [required]
637
638  Description        [optional]
639
640  SideEffects        [required]
641
642  SeeAlso            [optional]
643
644******************************************************************************/
645void
646CalPackNodes(Cal_BddManager_t *bddManager)
647{
648  int index, id;
649 
650  for (index = bddManager->numVars-1; index >= 0; index--){
651    id = bddManager->indexToId[index];
652    CalBddPackNodesForSingleId(bddManager, id);
653  }
654}
655
656/**Function********************************************************************
657
658  Synopsis           [required]
659
660  Description        [optional]
661
662  SideEffects        [required]
663
664  SeeAlso            [optional]
665
666******************************************************************************/
667void
668CalBddPackNodesForSingleId(Cal_BddManager_t *bddManager,
669                           Cal_BddId_t id)
670{
671  /* Need to copy the one for "AfterReorder" and suitably modify. */
672}
673
674/**Function********************************************************************
675
676  Synopsis           [Packs the nodes if the variables which has just
677  been sifted.]
678 
679  Description        [fixForwardedNodesFlag: Whether we need to fix
680  the forwarded nodes of variables corresponding to bestIndex through
681  bottomIndex. If this flag is set, then the forwarded nodes of these
682  variables are traversed and updated after the nodes of the bestIndex
683  have been copied. At the end the forwarded nodes are freed. If this
684  flag is not set, it is assumed that the cleanup pass has already
685  been performed.]
686
687  SideEffects        [required]
688
689  SeeAlso            [optional]
690
691******************************************************************************/
692void
693CalBddPackNodesAfterReorderForSingleId(Cal_BddManager_t *bddManager,
694                                       int fixForwardedNodesFlag,
695                                       int bestIndex, 
696                                       int bottomIndex) 
697{
698  /* We need to pack the nodes for this id and fix the cofactors of
699     the upper indices.
700     */
701  CalBddNode_t *node, *nextBddNode, *dupNode, **oldBins;
702  CalBddNode_t *thenBddNode, *elseBddNode, *bddNode;
703  Cal_Bdd_t thenBdd;
704  CalAddress_t *page;
705  int id = bddManager->indexToId[bestIndex];
706  CalNodeManager_t *nodeManager = bddManager->nodeManagerArray[id];
707  CalAddress_t **oldPageList = nodeManager->pageList;
708  int oldNumPages = nodeManager->numPages;
709  CalHashTable_t *uniqueTableForId = bddManager->uniqueTable[id];
710  int numPagesRequired, newSizeIndex, index, i;
711  long oldNumBins, hashValue;
712 
713 
714#ifdef _CAL_VERBOSE
715  fprintf(stdout,"Repacking id %3d\n", id);
716#endif
717 
718
719  nodeManager->freeNodeList = Cal_Nil(CalBddNode_t);
720  nodeManager->numPages = 0;
721  numPagesRequired = uniqueTableForId->numEntries/NUM_NODES_PER_PAGE;
722  nodeManager->maxNumPages =
723      2*(numPagesRequired ? numPagesRequired : 1);
724
725  nodeManager->pageList = Cal_MemAlloc(CalAddress_t *,
726                                       nodeManager->maxNumPages); 
727 
728  oldBins = uniqueTableForId->bins;
729  oldNumBins = uniqueTableForId->numBins;
730  /* Create the new set of bins */
731  newSizeIndex =
732      CeilLog2(uniqueTableForId->numEntries/HASH_TABLE_DEFAULT_MAX_DENSITY);
733
734  if (newSizeIndex < HASH_TABLE_DEFAULT_SIZE_INDEX){
735    newSizeIndex = HASH_TABLE_DEFAULT_SIZE_INDEX;
736  }
737
738  uniqueTableForId->sizeIndex = newSizeIndex;
739  uniqueTableForId->numBins =  TABLE_SIZE(uniqueTableForId->sizeIndex);
740  uniqueTableForId->maxCapacity =
741      uniqueTableForId->numBins * HASH_TABLE_DEFAULT_MAX_DENSITY; 
742
743  uniqueTableForId->bins = Cal_MemAlloc(CalBddNode_t *,
744                                        uniqueTableForId->numBins); 
745  if(uniqueTableForId->bins == Cal_Nil(CalBddNode_t *)){
746    CalBddFatalMessage("out of memory");
747  }
748
749  memset((char *)uniqueTableForId->bins, 0, 
750        uniqueTableForId->numBins*sizeof(CalBddNode_t *)); 
751
752  for (i = 0; i < oldNumBins; i++){
753    node = oldBins[i];
754    while (node){
755      nextBddNode = CalBddNodeGetNextBddNode(node);
756      CalNodeManagerCreateAndDupBddNode(nodeManager, node, dupNode);
757      thenBddNode = CalBddNodeGetThenBddNode(dupNode);
758      elseBddNode = CalBddNodeGetElseBddNode(dupNode);
759      hashValue = CalDoHash2(thenBddNode, elseBddNode, uniqueTableForId);
760      CalBddNodePutNextBddNode(dupNode, uniqueTableForId->bins[hashValue]);
761      uniqueTableForId->bins[hashValue] = dupNode;
762      CalBddNodePutThenBddNode(node, dupNode);
763      CalBddNodePutThenBddId(node, id);
764      CalBddNodePutElseBddNode(node, FORWARD_FLAG);
765      node = nextBddNode;
766      Cal_Assert(!(CalBddNodeIsRefCountZero(dupNode)));
767    }
768  }
769 
770  if (fixForwardedNodesFlag){
771      CalBddNode_t *requestNodeList =
772          bddManager->uniqueTable[id]->startNode.nextBddNode; 
773      for (bddNode = requestNodeList; bddNode; bddNode = nextBddNode){
774        Cal_Assert(CalBddNodeIsForwarded(bddNode));
775        nextBddNode = CalBddNodeGetNextBddNode(bddNode);
776        CalBddNodeGetThenBdd(bddNode, thenBdd);
777        if (CalBddGetBddId(thenBdd) == id){
778          if (CalBddIsForwarded(thenBdd)) {
779            CalBddForward(thenBdd);
780            Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
781            CalBddNodePutThenBdd(bddNode, thenBdd);
782          }
783        }
784        Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
785      }
786      for (index = bestIndex+1; index <= bottomIndex; index++){   
787      int varId = bddManager->indexToId[index];
788      requestNodeList =
789          bddManager->uniqueTable[varId]->startNode.nextBddNode;   
790      for (bddNode = requestNodeList; bddNode; bddNode = nextBddNode){
791        Cal_Assert(CalBddNodeIsForwarded(bddNode));
792        nextBddNode = CalBddNodeGetNextBddNode(bddNode);
793        CalBddNodeGetThenBdd(bddNode, thenBdd);
794        if (CalBddIsForwarded(thenBdd)) {
795          CalBddForward(thenBdd);
796          Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
797          CalBddNodePutThenBdd(bddNode, thenBdd);
798        }
799        Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
800      }
801    }
802  }
803 
804/* Traverse the upper indices fixing the cofactors */
805  for (index = bestIndex-1; index >= 0; index--){
806    CalBddReorderFixCofactors(bddManager,
807                           bddManager->indexToId[index]); 
808  }
809
810  if (bddManager->pipelineState == CREATE){
811    /* There are some results computed in pipeline */
812    CalBddReorderFixProvisionalNodes(bddManager);
813  }
814 
815  /* Fix the user BDDs */
816  CalBddReorderFixUserBddPtrs(bddManager);
817
818  CalBddIsForwardedTo(bddManager->varBdds[id]);
819
820  /* Fix the association */
821  CalReorderAssociationFix(bddManager);
822 
823  /* Free the old bins */
824  Cal_MemFree(oldBins);
825
826  uniqueTableForId->endNode = &(uniqueTableForId->startNode);
827  uniqueTableForId->startNode.nextBddNode = NULL;
828  if (fixForwardedNodesFlag){
829    CalBddReorderReclaimForwardedNodes(bddManager, bestIndex+1,
830                                    bottomIndex);
831  }
832  /* Free the old pages */
833  for (i = 0; i < oldNumPages; i++){
834    page = oldPageList[i]; 
835    CalPageManagerFreePage(nodeManager->pageManager, page);
836  }
837  Cal_MemFree(oldPageList);
838  Cal_Assert(CalCheckAllValidity(bddManager));
839}
840
841/**Function********************************************************************
842
843  Synopsis           [required]
844
845  Description        [optional]
846
847  SideEffects        [required]
848
849  SeeAlso            [optional]
850
851******************************************************************************/
852void
853CalBddPackNodesForMultipleIds(Cal_BddManager_t *bddManager,
854                              Cal_BddId_t beginId, int numLevels)
855{
856  /* We need to pack the nodes for this id and fix the cofactors of
857     the upper indices.
858     */
859  int index = bddManager->idToIndex[beginId];
860  int level, id;
861  long i, j;
862  CalBddNode_t *node, *nextBddNode, *dupNode, *thenBddNode;
863  CalBddNode_t *elseBddNode, **oldBins;
864  Cal_Bdd_t thenBdd, elseBdd;
865  CalNodeManager_t *nodeManager;
866  CalHashTable_t *uniqueTableForId;
867  int someRepackingDone = 0;
868  long oldNumBins, hashValue;
869  int newSizeIndex;
870
871
872  CalAddress_t *page, ***oldPageListArray, **oldPageList;
873  int *oldNumPagesArray;
874  int numPagesRequired;
875 
876  oldPageListArray = Cal_MemAlloc(CalAddress_t **, numLevels);
877
878  oldNumPagesArray = Cal_MemAlloc(int, numLevels);
879 
880  for (level = numLevels-1; level >= 0; level--){
881    id = bddManager->indexToId[index+level];
882    oldNumPagesArray[level] = 0;
883    oldPageListArray[level] = Cal_Nil(CalAddress_t *);
884    if (CalBddIdNeedsRepacking(bddManager, id)){
885      nodeManager = bddManager->nodeManagerArray[id];
886      uniqueTableForId = bddManager->uniqueTable[id];
887      oldPageListArray[level] = nodeManager->pageList;
888      oldNumPagesArray[level] = nodeManager->numPages;
889      nodeManager->freeNodeList = Cal_Nil(CalBddNode_t);
890      nodeManager->numPages = 0;
891      numPagesRequired = uniqueTableForId->numEntries/NUM_NODES_PER_PAGE;
892      nodeManager->maxNumPages =
893          2*(numPagesRequired ? numPagesRequired : 1);
894      nodeManager->pageList = Cal_MemAlloc(CalAddress_t *,
895                                           nodeManager->maxNumPages); 
896      oldBins = uniqueTableForId->bins;
897      oldNumBins = uniqueTableForId->numBins;
898      /* Create the new set of bins */
899      newSizeIndex =
900          CeilLog2(uniqueTableForId->numEntries /
901                   HASH_TABLE_DEFAULT_MAX_DENSITY); 
902      if (newSizeIndex < HASH_TABLE_DEFAULT_SIZE_INDEX){
903        newSizeIndex = HASH_TABLE_DEFAULT_SIZE_INDEX;
904      }
905      uniqueTableForId->sizeIndex = newSizeIndex;
906      uniqueTableForId->numBins =  TABLE_SIZE(uniqueTableForId->sizeIndex);
907      uniqueTableForId->maxCapacity =
908          uniqueTableForId->numBins * HASH_TABLE_DEFAULT_MAX_DENSITY; 
909     
910      uniqueTableForId->bins = Cal_MemAlloc(CalBddNode_t *,
911                                            uniqueTableForId->numBins); 
912      if(uniqueTableForId->bins == Cal_Nil(CalBddNode_t *)){
913        CalBddFatalMessage("out of memory");
914      }
915      memset((char *)uniqueTableForId->bins, 0, 
916            uniqueTableForId->numBins*sizeof(CalBddNode_t *)); 
917     
918      for (i = 0; i < oldNumBins; i++){
919        node = oldBins[i];
920        while (node){
921          nextBddNode = CalBddNodeGetNextBddNode(node);
922          CalBddNodeGetThenBdd(node, thenBdd);
923          CalBddNodeGetElseBdd(node, elseBdd);
924          if (CalBddIsForwarded(thenBdd)){
925            CalBddForward(thenBdd);
926            CalBddNodePutThenBdd(node, thenBdd);
927          }
928          if (CalBddIsForwarded(elseBdd)){
929            CalBddForward(elseBdd);
930            CalBddNodePutElseBdd(node, elseBdd);
931          }
932          CalNodeManagerCreateAndDupBddNode(nodeManager, node, dupNode);
933          thenBddNode = CalBddNodeGetThenBddNode(dupNode);
934          elseBddNode = CalBddNodeGetElseBddNode(dupNode);
935          hashValue = CalDoHash2(thenBddNode, elseBddNode, uniqueTableForId);
936          CalBddNodePutNextBddNode(dupNode, uniqueTableForId->bins[hashValue]);
937          uniqueTableForId->bins[hashValue] = dupNode;
938          CalBddNodePutThenBddNode(node, dupNode);
939          CalBddNodePutThenBddId(node, id);
940          CalBddNodePutElseBddNode(node, FORWARD_FLAG);
941          node = nextBddNode;
942          Cal_Assert(!(CalBddNodeIsRefCountZero(dupNode)));
943        }
944      }
945
946#ifdef __FOO__
947      /*fprintf(stdout,"Repacking id = %d, index = %d\n", id, index+level);*/
948      /* First put all the nodes in that list */
949      nodeList = Cal_Nil(CalBddNode_t);
950      for (i = 0; i < uniqueTableForId->numBins; i++){
951        node = uniqueTableForId->bins[i];
952        while (node){
953          nextBddNode = CalBddNodeGetNextBddNode(node);
954          /* The "then" and "else" pointers could be forwarded */
955          CalBddNodeGetThenBdd(node, thenBdd);
956          CalBddNodeGetElseBdd(node, elseBdd);
957          if (CalBddIsForwarded(thenBdd)){
958            CalBddForward(thenBdd);
959            CalBddNodePutThenBdd(node, thenBdd);
960          }
961          if (CalBddIsForwarded(elseBdd)){
962            CalBddForward(elseBdd);
963            CalBddNodePutElseBdd(node, elseBdd);
964          }
965          CalBddNodePutNextBddNode(node, nodeList);
966          nodeList = node;
967          node = nextBddNode;
968        }
969        uniqueTableForId->bins[i] = Cal_Nil(CalBddNode_t);
970      }
971      uniqueTableForId->numEntries = 0;
972     
973      for (node = nodeList; node; node = nextBddNode){
974        nextBddNode = CalBddNodeGetNextBddNode(node);
975        CalNodeManagerCreateAndDupBddNode(nodeManager, node, dupNode);
976        /* Hash the dupNode */
977        CalHashTableAddDirect(uniqueTableForId, dupNode);
978        /* Make the original node a forwarding node */
979        CalBddNodePutThenBddNode(node, dupNode);
980        CalBddNodePutThenBddId(node, id);
981        CalBddNodePutElseBddNode(node, FORWARD_FLAG);
982      }
983#endif
984      someRepackingDone = 1;
985    }
986    else if (someRepackingDone){ /* Still need to fix the cofactors */
987      CalBddReorderFixCofactors(bddManager, id);
988    }
989  }
990 
991
992  /* Traverse the upper indices fixing the cofactors */
993  for (i = index-1; i >= 0; i--){
994    CalBddReorderFixCofactors(bddManager,
995                              bddManager->indexToId[i]);
996  }
997
998  /* Fix the user BDDs */
999  CalBddReorderFixUserBddPtrs(bddManager);
1000  if (bddManager->pipelineState == CREATE){
1001    /* There are some results computed in pipeline */
1002    CalBddReorderFixProvisionalNodes(bddManager);
1003  }
1004  /* Fix Cache Tables */
1005  (void)CalCacheTableTwoRepackUpdate(bddManager->cacheTable);
1006 
1007  for (level = numLevels - 1 ; level >= 0; level--){
1008    id = bddManager->indexToId[index+level];
1009    /* Update varBdd field of bdd manager */
1010    CalBddIsForwardedTo(bddManager->varBdds[id]);
1011    /* Fix associations */
1012    CalVarAssociationRepackUpdate(bddManager, id);
1013    /* Free the old pages */
1014    nodeManager = bddManager->nodeManagerArray[id];
1015    oldPageList = oldPageListArray[level];
1016    for (j = 0; j < oldNumPagesArray[level]; j++){
1017      page = oldPageList[j]; 
1018      CalPageManagerFreePage(nodeManager->pageManager, page);
1019    }
1020    if ((unsigned long)oldPageList) Cal_MemFree(oldPageList);
1021  }
1022  Cal_MemFree(oldPageListArray);
1023  Cal_MemFree(oldNumPagesArray);
1024}
1025
1026/*---------------------------------------------------------------------------*/
1027/* Definition of static functions                                            */
1028/*---------------------------------------------------------------------------*/
1029/**Function********************************************************************
1030
1031  Synopsis    [Returns the smallest integer greater than or equal to log2 of a
1032  number]
1033
1034  Description [Returns the smallest integer greater than or equal to log2 of a
1035  number (The assumption is that the number is >= 1)]
1036
1037  SideEffects [None]
1038
1039******************************************************************************/
1040static int
1041CeilLog2(
1042  int  number)
1043{
1044  int num, count;
1045  for (num=number, count=0; num > 1; num >>= 1, count++);
1046  if ((1 << count) != number) count++;
1047  return count;
1048}
Note: See TracBrowser for help on using the repository browser.