source: vis_dev/glu-2.3/src/calBdd/calBddManager.c @ 43

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

library glu 2.3
File size: 27.2 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [calBddManager.c]
4
5  PackageName [cal]
6
7  Synopsis    [Routines for maintaing the manager and creating
8  variables etc.]
9
10  Description []
11
12  SeeAlso     [optional]
13
14  Author      [Rajeev K. Ranjan (rajeev@eecs.berkeley.edu)
15               Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)
16               ]
17
18  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
19  All rights reserved.
20
21  Permission is hereby granted, without written agreement and without license
22  or royalty fees, to use, copy, modify, and distribute this software and its
23  documentation for any purpose, provided that the above copyright notice and
24  the following two paragraphs appear in all copies of this software.
25
26  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
27  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
28  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
29  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
30
31  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
32  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
33  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
34  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
35  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
36
37  Revision    [$Id: calBddManager.c,v 1.9 2002/09/21 20:39:24 fabio Exp $]
38
39******************************************************************************/
40
41#include "calInt.h"
42
43/*---------------------------------------------------------------------------*/
44/* Constant declarations                                                     */
45/*---------------------------------------------------------------------------*/
46
47/*---------------------------------------------------------------------------*/
48/* Type declarations                                                         */
49/*---------------------------------------------------------------------------*/
50
51/*---------------------------------------------------------------------------*/
52/* Stucture declarations                                                     */
53/*---------------------------------------------------------------------------*/
54
55
56/*---------------------------------------------------------------------------*/
57/* Variable declarations                                                     */
58/*---------------------------------------------------------------------------*/
59unsigned long calPrimes[] = 
60{
61  1,
62  2,
63  3,
64  7,
65  13,
66  23,
67  59,
68  113,
69  241,
70  503,
71  1019,
72  2039,
73  4091,
74  8179,
75  11587,
76  16369,
77  23143,
78  32749,
79  46349,
80  65521,
81  92683,
82  131063,
83  185363,
84  262139,
85  330287,
86  416147,
87  524269,
88  660557,
89  832253,
90  1048571,
91  1321109,
92  1664501,
93  2097143,
94  2642201,
95  3328979,
96  4194287,
97  5284393,
98  6657919,
99  8388593,
100  10568797,
101  13315831,
102  16777199,
103  33554393,
104  67108859,
105  134217689,
106  268435399,
107  536870879,
108  1073741789,
109  2147483629
110};
111
112/*---------------------------------------------------------------------------*/
113/* Macro declarations                                                        */
114/*---------------------------------------------------------------------------*/
115#define CalBddManagerGetNodeManager(bddManager, id) \
116    bddManager->nodeManagerArray[id]
117
118
119/**AutomaticStart*************************************************************/
120
121/*---------------------------------------------------------------------------*/
122/* Static function prototypes                                                */
123/*---------------------------------------------------------------------------*/
124
125static void BddDefaultTransformFn(Cal_BddManager_t * bddManager, CalAddress_t value1, CalAddress_t value2, CalAddress_t * result1, CalAddress_t * result2, Cal_Pointer_t pointer);
126#ifdef CALBDDMANAGER
127static int CalBddManagerPrint(Cal_BddManager_t *bddManager);
128#endif /* CALBDDMANAGER */
129
130/**AutomaticEnd***************************************************************/
131
132
133/*---------------------------------------------------------------------------*/
134/* Definition of exported functions                                          */
135/*---------------------------------------------------------------------------*/
136/**Function********************************************************************
137
138  Synopsis    [Creates and initializes a new BDD manager.]
139
140  Description [Initializes and allocates fields of the BDD manager. Some of the
141  fields are initialized for maxNumVars+1 or numVars+1, whereas some of them are
142  initialized for maxNumVars or numVars. The first kind of fields are associated
143  with the id of a variable and the second ones are with the index of the
144  variable.]
145
146  SideEffects [None]
147
148  SeeAlso     [Cal_BddManagerQuit]
149
150******************************************************************************/
151Cal_BddManager
152Cal_BddManagerInit(void)
153{
154  Cal_BddManager_t *bddManager;
155  int i;
156  CalBddNode_t *bddNode;
157  Cal_Bdd_t resultBdd;
158 
159   
160  bddManager = Cal_MemAlloc(Cal_BddManager_t, 1);
161
162  bddManager->numVars = 0;
163
164  bddManager->maxNumVars = 30;
165 
166  bddManager->varBdds = Cal_MemAlloc(Cal_Bdd_t, bddManager->maxNumVars+1);
167 
168  bddManager->pageManager1 = CalPageManagerInit(4);
169  bddManager->pageManager2 = CalPageManagerInit(NUM_PAGES_PER_SEGMENT);
170
171  bddManager->nodeManagerArray = Cal_MemAlloc(CalNodeManager_t*, bddManager->maxNumVars+1);
172
173  bddManager->nodeManagerArray[0] = CalNodeManagerInit(bddManager->pageManager1);
174  bddManager->uniqueTable = Cal_MemAlloc(CalHashTable_t *,
175                                         bddManager->maxNumVars+1);
176  bddManager->uniqueTable[0] = CalHashTableInit(bddManager, 0);
177 
178  /* Constant One */
179  CalBddPutBddId(bddManager->bddOne, CAL_BDD_CONST_ID);
180  CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], bddNode);
181  CalBddPutBddNode(bddManager->bddOne, bddNode);
182  /* ~0x0 put so that the node is not mistaken for forwarded node */
183  CalBddPutThenBddNode(bddManager->bddOne, (CalBddNode_t *)~0x0);
184  CalBddPutElseBddNode(bddManager->bddOne, (CalBddNode_t *)~0x0);
185  CalBddPutRefCount(bddManager->bddOne, CAL_MAX_REF_COUNT);
186  CalBddNot(bddManager->bddOne, bddManager->bddZero);
187
188  /* Create a user BDD */
189  CalHashTableAddDirectAux(bddManager->uniqueTable[0], bddManager->bddOne,
190                           bddManager->bddOne, &resultBdd);
191  CalBddPutRefCount(resultBdd, CAL_MAX_REF_COUNT);
192  bddManager->userOneBdd =  CalBddGetBddNode(resultBdd);
193  bddManager->userZeroBdd = CalBddNodeNot(bddManager->userOneBdd);
194 
195  /* Null BDD */
196  CalBddPutBddId(bddManager->bddNull, CAL_BDD_NULL_ID);
197  CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], bddNode);
198  CalBddPutBddNode(bddManager->bddNull, bddNode);
199  /* ~0x10 put so that the node is not mistaken for forwarded node or
200     the constant nodes. */
201  CalBddPutThenBddNode(bddManager->bddNull, (CalBddNode_t *)~0x10);
202  CalBddPutElseBddNode(bddManager->bddNull, (CalBddNode_t *)~0x10);
203  CalBddPutRefCount(bddManager->bddNull, CAL_MAX_REF_COUNT);
204  /* Put in the unique table, so that it gets locked */
205  /*CalHashTableAddDirect(bddManager->uniqueTable[0], bddNode);*/
206
207  bddManager->indexToId = Cal_MemAlloc(Cal_BddId_t, bddManager->maxNumVars);
208  bddManager->idToIndex = Cal_MemAlloc(Cal_BddIndex_t, bddManager->maxNumVars+1);
209  bddManager->idToIndex[CAL_BDD_CONST_ID] = CAL_BDD_CONST_INDEX;
210
211  bddManager->depth = DEFAULT_DEPTH;
212  bddManager->maxDepth = DEFAULT_MAX_DEPTH;
213  bddManager->pipelineState = READY;
214  bddManager->pipelineDepth = PIPELINE_EXECUTION_DEPTH;
215  bddManager->currentPipelineDepth = 0;
216  bddManager->pipelineFn = CalOpAnd;
217
218
219  bddManager->reqQue = Cal_MemAlloc(CalHashTable_t **, bddManager->maxDepth);
220  bddManager->cacheTable = CalCacheTableTwoInit(bddManager);
221 
222  for (i=0; i < bddManager->maxDepth; i++){
223    bddManager->reqQue[i] = Cal_MemAlloc(CalHashTable_t *,
224                                         bddManager->maxNumVars+1);
225    bddManager->reqQue[i][0] = CalHashTableInit(bddManager, 0);
226  }
227
228  bddManager->requestNodeListArray = Cal_MemAlloc(CalRequestNode_t*,
229                                                  MAX_INSERT_DEPTH);
230  for(i = 0; i < MAX_INSERT_DEPTH; i++){
231    bddManager->requestNodeListArray[i] = Cal_Nil(CalRequestNode_t);
232  }
233  bddManager->userProvisionalNodeList = Cal_Nil(CalRequestNode_t);
234
235  /* Garbage collection related information */
236  bddManager->numNodes = bddManager->numPeakNodes = 1;
237  bddManager->numNodesFreed = 0;
238  bddManager->gcCheck = CAL_GC_CHECK;
239  bddManager->uniqueTableGCLimit =  CAL_MIN_GC_LIMIT;
240  bddManager->numGC = 0;
241  bddManager->gcMode = 1;
242  bddManager->nodeLimit = 0;
243  bddManager->overflow = 0;
244  bddManager->repackAfterGCThreshold = CAL_REPACK_AFTER_GC_THRESHOLD;
245 
246
247  /* Special functions */
248  bddManager->TransformFn = BddDefaultTransformFn;
249  bddManager->transformEnv = 0;
250
251
252  /* Association related information */
253  bddManager->associationList = Cal_Nil(CalAssociation_t);
254  /*bddManager->tempAssociation = CAL_BDD_NEW_REC(bddManager, CalAssociation_t);*/
255  bddManager->tempAssociation = Cal_MemAlloc(CalAssociation_t, 1);
256  bddManager->tempAssociation->id = -1;
257  bddManager->tempAssociation->lastBddIndex = -1;
258  bddManager->tempAssociation->varAssociation =
259      Cal_MemAlloc(Cal_Bdd_t, bddManager->maxNumVars+1);
260  for(i = 0; i < bddManager->maxNumVars+1; i++){
261     bddManager->tempAssociation->varAssociation[i] = bddManager->bddNull;
262  }
263  bddManager->tempOpCode = -1;
264  bddManager->currentAssociation = bddManager->tempAssociation;
265
266  /* BDD reordering related information */
267  bddManager->dynamicReorderingEnableFlag = 1;
268  bddManager->reorderMethod = CAL_REORDER_METHOD_DF;
269  bddManager->reorderTechnique = CAL_REORDER_NONE;
270  bddManager->numForwardedNodes = 0;
271  bddManager->numReorderings = 0;
272  bddManager->maxNumVarsSiftedPerReordering = 1000;
273  bddManager->maxNumSwapsPerReordering = 2000000;
274  bddManager->numSwaps = 0;
275  bddManager->numTrivialSwaps = 0;
276  bddManager->maxSiftingGrowth = 2.0;
277  bddManager->reorderingThreshold = CAL_BDD_REORDER_THRESHOLD;
278  bddManager->maxForwardedNodes = CAL_NUM_FORWARDED_NODES_LIMIT;
279  bddManager->tableRepackThreshold = CAL_TABLE_REPACK_THRESHOLD;
280 
281
282  /*bddManager->superBlock = CAL_BDD_NEW_REC(bddManager, Cal_Block_t);*/
283  bddManager->superBlock = Cal_MemAlloc(Cal_Block_t, 1);
284  bddManager->superBlock->numChildren=0;
285  bddManager->superBlock->children=0;
286  bddManager->superBlock->reorderable=1;
287  bddManager->superBlock->firstIndex= -1;
288  bddManager->superBlock->lastIndex=0;
289 
290  bddManager->hooks = Cal_Nil(void);
291 
292  return bddManager;
293}
294
295/**Function********************************************************************
296
297  Synopsis    [Frees the BDD manager and all the associated allocations]
298
299  Description [Frees the BDD manager and all the associated allocations]
300
301  SideEffects [None]
302
303  SeeAlso     [Cal_BddManagerInit]
304
305******************************************************************************/
306int
307Cal_BddManagerQuit(Cal_BddManager bddManager)
308{
309  int i, j;
310
311  if(bddManager == Cal_Nil(Cal_BddManager_t)) return 1;
312
313  for (i=0; i < bddManager->maxDepth; i++){
314    for (j=0; j <= bddManager->numVars; j++){
315      CalHashTableQuit(bddManager, bddManager->reqQue[i][j]);
316    }
317    Cal_MemFree(bddManager->reqQue[i]);
318  }
319 
320  for (i=0; i <= bddManager->numVars; i++){
321    CalHashTableQuit(bddManager, bddManager->uniqueTable[i]);
322    CalNodeManagerQuit(bddManager->nodeManagerArray[i]);
323  }
324
325  CalCacheTableTwoQuit(bddManager->cacheTable);
326  Cal_MemFree(bddManager->tempAssociation->varAssociation);
327  /*CAL_BDD_FREE_REC(bddManager, bddManager->tempAssociation, CalAssociation_t);*/
328  Cal_MemFree(bddManager->tempAssociation);
329  /*CAL_BDD_FREE_REC(bddManager, bddManager->superBlock, Cal_Block_t);*/
330  CalFreeBlockRecursively(bddManager->superBlock);
331  CalAssociationListFree(bddManager);
332  Cal_MemFree(bddManager->varBdds);
333  Cal_MemFree(bddManager->indexToId);
334  Cal_MemFree(bddManager->idToIndex);
335  Cal_MemFree(bddManager->uniqueTable);
336  Cal_MemFree(bddManager->reqQue);
337  Cal_MemFree(bddManager->requestNodeListArray);
338  Cal_MemFree(bddManager->nodeManagerArray);
339  CalPageManagerQuit(bddManager->pageManager1);
340  CalPageManagerQuit(bddManager->pageManager2);
341  Cal_MemFree(bddManager);
342
343  return 0;
344}
345
346/**Function********************************************************************
347
348  Synopsis    [Sets appropriate fields of BDD Manager.]
349
350  Description [This function is used to set the parameters which are
351  used to control the reordering process. "reorderingThreshold"
352  determines the number of nodes below which reordering will NOT be
353  invoked, "maxForwardedNodes" determines the maximum number of
354  forwarded nodes which are allowed (at that point the cleanup must be
355  done), and "repackingThreshold" determines the fraction of the page
356  utilized below which repacking has to be invoked. These parameters
357  have different effect on the computational and memory usage aspects
358  of reordeing. For instance, higher value of "maxForwardedNodes" will
359  result in process consuming more memory, and a lower value on the
360  other hand would invoke the cleanup process repeatedly resulting in
361  increased computation.]
362
363  SideEffects [Sets appropriate fields of BDD Manager]
364
365  SeeAlso     []
366
367******************************************************************************/
368void
369Cal_BddManagerSetParameters(Cal_BddManager bddManager,
370                            long reorderingThreshold,
371                            long maxForwardedNodes,
372                            double repackAfterGCThreshold,
373                            double tableRepackThreshold)
374{
375  if (reorderingThreshold >= 0){
376    bddManager->reorderingThreshold = reorderingThreshold;
377  }
378  if (maxForwardedNodes >= 0){
379    bddManager->maxForwardedNodes = maxForwardedNodes;
380  }
381  if (repackAfterGCThreshold >= 0.0){
382    bddManager->repackAfterGCThreshold = (float) repackAfterGCThreshold;
383  }
384  if (tableRepackThreshold >= 0.0){
385    bddManager->tableRepackThreshold = (float) tableRepackThreshold;
386  }
387}
388
389
390/**Function********************************************************************
391
392  Synopsis    [Returns the number of BDD nodes]
393
394  Description [Returns the number of BDD nodes]
395
396  SideEffects [None]
397
398  SeeAlso     [Cal_BddTotalSize]
399
400******************************************************************************/
401unsigned long
402Cal_BddManagerGetNumNodes(Cal_BddManager bddManager)
403{
404  return  bddManager->numNodes;
405}
406
407
408
409/**Function********************************************************************
410
411  Synopsis    [Creates and returns a new variable at the start of the variable
412  order.]
413
414  Description [Creates and returns a new variable at the start of the
415  variable order.]
416
417  SideEffects [None]
418
419******************************************************************************/
420Cal_Bdd
421Cal_BddManagerCreateNewVarFirst(Cal_BddManager bddManager)
422{
423  return CalBddGetExternalBdd(bddManager, CalBddManagerCreateNewVar(bddManager,
424                                                        (Cal_BddIndex_t)0));
425}
426
427/**Function********************************************************************
428
429  Synopsis    [Creates and returns a new variable at the end of the variable
430  order.]
431
432  Description [Creates and returns a new variable at the end of the variable
433  order.]
434
435  SideEffects [None]
436
437******************************************************************************/
438Cal_Bdd
439Cal_BddManagerCreateNewVarLast(Cal_BddManager bddManager)
440{
441  return CalBddGetExternalBdd(bddManager,
442                              CalBddManagerCreateNewVar(bddManager,
443                                                        (Cal_BddIndex_t)
444                                                        bddManager->numVars));
445}
446
447
448
449/**Function********************************************************************
450
451  Synopsis    [Creates and returns a new variable before the specified one in
452  the variable order.]
453
454  Description [Creates and returns a new variable before the specified one in
455  the variable order.]
456
457  SideEffects [None]
458
459******************************************************************************/
460Cal_Bdd
461Cal_BddManagerCreateNewVarBefore(Cal_BddManager bddManager,
462                                 Cal_Bdd userBdd)
463{
464  Cal_Bdd_t calBdd = CalBddGetInternalBdd(bddManager, userBdd);
465  if (CalBddIsBddConst(calBdd)){
466    return Cal_BddManagerCreateNewVarLast(bddManager);
467  }
468  else{
469    return CalBddGetExternalBdd(bddManager,
470                                CalBddManagerCreateNewVar(bddManager,
471                                                          CalBddGetBddIndex(bddManager, 
472                                                  calBdd)));
473  }
474}
475
476/**Function********************************************************************
477
478  Synopsis    [Creates and returns a new variable after the specified one in
479  the variable  order.]
480
481  Description [Creates and returns a new variable after the specified one in
482  the variable  order.]
483
484  SideEffects [None]
485
486******************************************************************************/
487Cal_Bdd
488Cal_BddManagerCreateNewVarAfter(Cal_BddManager bddManager,
489                                Cal_Bdd userBdd)
490{
491  Cal_Bdd_t calBdd = CalBddGetInternalBdd(bddManager, userBdd);
492  if (CalBddIsBddConst(calBdd)){
493    return Cal_BddManagerCreateNewVarLast(bddManager);
494  }
495  else{
496    return CalBddGetExternalBdd(bddManager,
497                                CalBddManagerCreateNewVar(bddManager,
498                                                          CalBddGetBddIndex(bddManager, calBdd)+1));
499  }
500}
501
502
503/**Function********************************************************************
504
505  Synopsis    [Returns the variable with the specified index, null if no
506  such variable exists]
507
508  Description [Returns the variable with the specified index, null if no
509  such variable exists]
510
511  SideEffects [None]
512
513******************************************************************************/
514Cal_Bdd
515Cal_BddManagerGetVarWithIndex(Cal_BddManager bddManager, Cal_BddIndex_t  index)
516{
517  if (index >= bddManager->numVars){
518    CalBddWarningMessage("Index out of range");
519    return (Cal_Bdd) 0;
520  }
521  return CalBddGetExternalBdd(bddManager,
522                              bddManager->varBdds[bddManager->indexToId[index]]); 
523}
524
525/**Function********************************************************************
526
527  Synopsis    [Returns the variable with the specified id, null if no
528  such variable exists]
529
530  Description [Returns the variable with the specified id, null if no
531  such variable exists]
532
533  SideEffects [None]
534
535  SeeAlso     [optional]
536
537******************************************************************************/
538Cal_Bdd
539Cal_BddManagerGetVarWithId(Cal_BddManager bddManager,  Cal_BddId_t  id)
540{
541  if (id <= 0 || id > bddManager->numVars){
542    CalBddWarningMessage("Id out of range");
543    return (Cal_Bdd) 0;
544  }
545  return CalBddGetExternalBdd(bddManager, bddManager->varBdds[id]);
546}
547
548/*---------------------------------------------------------------------------*/
549/* Definition of internal functions                                          */
550/*---------------------------------------------------------------------------*/
551/**Function********************************************************************
552
553  Synopsis    [This function creates and returns a new variable with given
554  index value.]
555
556  Description [Right now this function does not handle the case when the
557  package is working in multiprocessor mode. We need to put in the necessary
558  code later.]
559
560  SideEffects [If the number of variables in the manager exceeds that of value
561  of numMaxVars, then we need to reallocate various fields of the manager. Also
562  depending upon the value of "index", idToIndex and indexToId tables would
563  change.]
564
565******************************************************************************/
566Cal_Bdd_t
567CalBddManagerCreateNewVar(Cal_BddManager_t * bddManager, Cal_BddIndex_t  index)
568{
569  Cal_Bdd_t calBdd;
570  Cal_BddId_t varId;
571  int totalNumVars, maxNumVars, i;
572  CalAssociation_t *association;
573 
574  if (bddManager->numVars == CAL_MAX_VAR_ID){
575    CalBddFatalMessage("Cannot create any new variable, no more Id left."); 
576  }
577
578  /*
579   * Get the total number of variables. If the index is more than the total
580   * number of variables, then report error.
581   */
582  totalNumVars = bddManager->numVars;
583 
584  if (index > totalNumVars){
585    CalBddFatalMessage("The variable index out of range");
586  }
587 
588
589  /*
590   * Create a new variable in the manager which contains this index.
591   * This might lead to change in the id->index, and index->id
592   * for other managers.
593   */
594
595  /*
596   * If the number of variables is equal to the maximum number of variables
597   * then reallocate memory.
598   */
599  if (bddManager->numVars == bddManager->maxNumVars){
600    int oldMaxNumVars;
601    CalAssociation_t *p;
602   
603    oldMaxNumVars = bddManager->maxNumVars;
604    if ((maxNumVars = 2*oldMaxNumVars) > CAL_MAX_VAR_ID){
605      maxNumVars = CAL_MAX_VAR_ID;
606    }
607    bddManager->maxNumVars = maxNumVars;
608    bddManager->varBdds = Cal_MemRealloc(Cal_Bdd_t,
609                                         bddManager->varBdds, maxNumVars+1); 
610   
611    bddManager->nodeManagerArray = Cal_MemRealloc(CalNodeManager_t *,
612                                                  bddManager->nodeManagerArray, 
613                                                  maxNumVars+1);
614
615    bddManager->idToIndex = Cal_MemRealloc(Cal_BddIndex_t, bddManager->idToIndex,
616                                        maxNumVars+1);
617
618    bddManager->indexToId = Cal_MemRealloc(Cal_BddIndex_t, bddManager->indexToId,
619                                        maxNumVars);
620
621    bddManager->uniqueTable = Cal_MemRealloc(CalHashTable_t *,
622                                          bddManager->uniqueTable, maxNumVars+1);
623   
624    for (i=0; i<bddManager->maxDepth; i++){
625      bddManager->reqQue[i] = Cal_MemRealloc(CalHashTable_t *, bddManager->reqQue[i],
626                                          maxNumVars+1);
627    }
628    bddManager->tempAssociation->varAssociation = 
629        Cal_MemRealloc(Cal_Bdd_t, bddManager->tempAssociation->varAssociation,
630        maxNumVars+1);
631    /* CHECK LOOP INDICES */
632    for(i = oldMaxNumVars+1; i < maxNumVars+1; i++){
633      bddManager->tempAssociation->varAssociation[i] = bddManager->bddNull;
634    }
635    for(p = bddManager->associationList; p; p = p->next){
636      p->varAssociation = 
637          Cal_MemRealloc(Cal_Bdd_t, p->varAssociation, maxNumVars+1);
638      /* CHECK LOOP INDICES */
639      for(i = oldMaxNumVars+1; i < maxNumVars+1; i++){
640        p->varAssociation[i] = bddManager->bddNull;
641      }
642    }
643  }
644
645  /* If the variable has been created in the middle, shift the indices. */
646  if (index != bddManager->numVars){
647    for (i=0; i<bddManager->numVars; i++){
648      if (bddManager->idToIndex[i+1] >= index){
649        bddManager->idToIndex[i+1]++;
650      }
651    }
652  }
653
654  /* Fix indexToId table */
655  for (i=bddManager->numVars; i>index; i--){
656    bddManager->indexToId[i] = bddManager->indexToId[i-1];
657  }
658
659  for(association = bddManager->associationList; association;
660                                              association =
661                                                  association->next){
662    if (association->lastBddIndex >= index){
663      association->lastBddIndex++;
664    }
665  }
666  if (bddManager->tempAssociation->lastBddIndex >= index){
667    bddManager->tempAssociation->lastBddIndex++;
668  }
669 
670  bddManager->numVars++;
671  varId = bddManager->numVars;
672
673  bddManager->idToIndex[varId] = index;
674  bddManager->indexToId[index] = varId;
675 
676  bddManager->nodeManagerArray[varId] =
677      CalNodeManagerInit(bddManager->pageManager2); 
678  bddManager->uniqueTable[varId] =
679      CalHashTableInit(bddManager, varId);
680   
681  /* insert node in the uniqueTableForId */
682  CalHashTableAddDirectAux(bddManager->uniqueTable[varId],
683                           bddManager->bddOne, bddManager->bddZero, &calBdd);
684  CalBddPutRefCount(calBdd, CAL_MAX_REF_COUNT);
685  bddManager->varBdds[varId] = calBdd;
686
687  bddManager->numNodes++;
688 
689#ifdef __OLD__
690  /* initialize req_que_for_id */
691  bddManager->reqQue[varId] = Cal_MemAlloc(CalHashTable_t*, bddManager->maxDepth);
692  for (i=0; i<manager->maxDepth; i++){
693    bddManager->reqQue[varId][i] = CalHashTableInit(bddManager, varId);
694  }
695#endif
696 
697  /* initialize req_que_for_id */
698  for (i=0; i<bddManager->maxDepth; i++){
699    bddManager->reqQue[i][varId] =
700        CalHashTableInit(bddManager, varId);
701  }
702  CalBddShiftBlock(bddManager, bddManager->superBlock, (long)index);
703  return calBdd;
704}
705
706 
707/*---------------------------------------------------------------------------*/
708/* Definition of static functions                                            */
709/*---------------------------------------------------------------------------*/
710/**Function********************************************************************
711
712  Synopsis    [required]
713
714  Description [optional]
715
716  SideEffects [required]
717
718  SeeAlso     [optional]
719
720******************************************************************************/
721static void
722BddDefaultTransformFn(
723  Cal_BddManager_t * bddManager,
724  CalAddress_t  value1,
725  CalAddress_t  value2,
726  CalAddress_t * result1,
727  CalAddress_t * result2,
728  Cal_Pointer_t  pointer)
729{
730  if (!value2)
731    /* Will be a carry when taking 2's complement of value2.  Thus, */
732    /* take 2's complement of high part. */
733    value1= -(long)value1;
734  else
735    {
736      value2= -(long)value2;
737      value1= ~value1;
738    }
739  *result1=value1;
740  *result2=value2;
741}
742
743#ifdef CALBDDMANAGER
744
745/**Function********************************************************************
746
747  Synopsis    [required]
748
749  Description [optional]
750
751  SideEffects [required]
752
753  SeeAlso     [optional]
754
755******************************************************************************/
756static int
757CalBddManagerPrint(Cal_BddManager_t *bddManager)
758{
759  int i;
760  CalHashTable_t *uniqueTableForId;
761  printf("#####################   BDD MANAGER   #####################\n");
762  for(i = 1; i < bddManager->numVars; i++){
763    uniqueTableForId = bddManager->uniqueTable[i];
764    CalHashTablePrint(uniqueTableForId);
765  }
766  fflush(stdout);
767  return 0;
768}
769
770
771main(argc, argv)
772int argc;
773char **argv;
774{
775        Cal_Bdd_t n;
776        Cal_BddManager_t *manager;
777
778        manager = CalBddManagerInit(argc, argv);
779        n = CalBddManagerCreateVariable(bddManager);
780        CalBddFunctionPrint(n);
781        n = CalBddManagerGetVariable(bddManager, 0);
782        CalBddFunctionPrint(n);
783}
784#endif /* CALBDDMANAGER */
785
786#ifdef __GC__
787main(argc, argv)
788int argc;
789char **argv;
790{
791  Cal_BddManager_t *manager;
792  Cal_Bdd_t vars[256];
793  Cal_Bdd_t function, tempFunction;
794  int i;
795  int numVars;
796 
797  if (argc >= 2)
798        numVars = atoi(argv[1]);
799  else
800    numVars = 3;
801 
802  manager = Cal_BddManagerInit();
803 
804  for (i = 0; i < numVars; i++){
805    vars[i] = Cal_BddManagerCreateNewVarLast(bddManager);
806  }
807 
808  function = vars[0];
809  for (i = 1; i < numVars - 1; i++){
810    tempFunction = Cal_BddITE(bddManager, vars[i], vars[i+1], function);
811    Cal_BddFree(function);
812    function = tempFunction;
813            /*fprintf(stdout, "i = %d\n", i);
814              unique_table_write(stdout, CalBddManager->unique_table);
815              */
816  }
817  fprintf(stdout, "\n******************Before Free****************\n");
818  for (i = 1; i <= numVars; i++){
819    CalHashTablePrint(bddManager->uniqueTable[i]);
820  }
821  Cal_BddFree(function);
822  fprintf(stdout, "\n****************After Free****************\n");
823  for (i = 1; i <= numVars; i++){
824    CalHashTablePrint(bddManager->uniqueTable[i]);
825  }
826  Cal_BddManagerGC(bddManager);
827  fprintf(stdout, "\n****************After GC****************\n");
828  for (i = 1; i <= numVars; i++){
829    CalHashTablePrint(bddManager->uniqueTable[i]);
830  }
831}
832#endif
Note: See TracBrowser for help on using the repository browser.