source: vis_dev/glu-2.3/src/calBdd/calUtil.c @ 13

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

library glu 2.3
File size: 20.4 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [calUtil.c]
4
5  PackageName [cal]
6
7  Synopsis    [Utility functions for the Cal package.]
8
9  Description [Utility functions used in the Cal package.]
10
11  SeeAlso     [optional]
12
13  Author      [Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)
14               Rajeev K. Ranjan   (rajeev@eecs.berkeley.edu)
15              ]
16  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
17  All rights reserved.
18
19  Permission is hereby granted, without written agreement and without license
20  or royalty fees, to use, copy, modify, and distribute this software and its
21  documentation for any purpose, provided that the above copyright notice and
22  the following two paragraphs appear in all copies of this software.
23
24  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
25  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
26  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
27  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
28
29  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
30  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
31  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
32  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
33  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
34
35  Revision    [$Id: calUtil.c,v 1.4 2002/09/10 00:10:37 fabio Exp $]
36
37******************************************************************************/
38
39#include "calInt.h"
40
41/*---------------------------------------------------------------------------*/
42/* Constant declarations                                                     */
43/*---------------------------------------------------------------------------*/
44/* Random generator constants. */
45#define CAL_MODULUS1 2147483563
46#define CAL_LEQA1 40014
47#define CAL_LEQQ1 53668
48#define CAL_LEQR1 12211
49#define CAL_MODULUS2 2147483399
50#define CAL_LEQA2 40692
51#define CAL_LEQQ2 52774
52#define CAL_LEQR2 3791
53#define CAL_STAB_SIZE 64
54#define CAL_STAB_DIV (1 + (CAL_MODULUS1 - 1) / CAL_STAB_SIZE)
55
56/*---------------------------------------------------------------------------*/
57/* Type declarations                                                         */
58/*---------------------------------------------------------------------------*/
59
60
61/*---------------------------------------------------------------------------*/
62/* Stucture declarations                                                     */
63/*---------------------------------------------------------------------------*/
64
65/*---------------------------------------------------------------------------*/
66/* Variable declarations                                                     */
67/*---------------------------------------------------------------------------*/
68static long utilRand = 0;
69static long utilRand2;
70static long shuffleSelect;
71static long shuffleTable[CAL_STAB_SIZE];
72
73/*---------------------------------------------------------------------------*/
74/* Macro declarations                                                        */
75/*---------------------------------------------------------------------------*/
76
77
78/**AutomaticStart*************************************************************/
79
80/*---------------------------------------------------------------------------*/
81/* Static function prototypes                                                */
82/*---------------------------------------------------------------------------*/
83
84
85/**AutomaticEnd***************************************************************/
86
87/*---------------------------------------------------------------------------*/
88/* Definition of exported functions                                          */
89/*---------------------------------------------------------------------------*/
90void
91Cal_ImageDump(Cal_BddManager_t *bddManager, FILE *fp)
92{
93
94  CalPageManager_t *pageManager;
95  int i, j;
96  char *segment, c;
97  int count = NUM_PAGES_PER_SEGMENT * PAGE_SIZE;
98
99  pageManager = bddManager->pageManager1;
100  for(i = 0; i < pageManager->numSegments; i++){
101    segment = (char *) pageManager->pageSegmentArray[i];
102    for(j = 1; j <= count; j++){
103      c = segment[j];
104      fprintf(fp, "%c", j%64?c:'\n');
105    }
106  }
107  pageManager = bddManager->pageManager2;
108  for(i = 0; i < pageManager->numSegments; i++){
109    segment = (char *) pageManager->pageSegmentArray[i];
110    for(j = 1; j <= count; j++){
111      c = segment[j];
112      fprintf(fp, "%c", j%64?c:'\n');
113    }
114  }
115}
116
117
118/**Function********************************************************************
119
120  Synopsis    [Prints the function implemented by the argument BDD]
121
122  Description [Prints the function implemented by the argument BDD]
123
124  SideEffects [None]
125
126******************************************************************************/
127void
128Cal_BddFunctionPrint(Cal_BddManager bddManager, Cal_Bdd  userBdd,
129                     char *name)
130{
131  Cal_Bdd_t calBdd;
132  calBdd = CalBddGetInternalBdd(bddManager, userBdd);
133  CalBddFunctionPrint(bddManager, calBdd, name);
134}
135
136/*---------------------------------------------------------------------------*/
137/* Definition of internal functions                                          */
138/*---------------------------------------------------------------------------*/
139/**Function********************************************************************
140
141  Synopsis    [required]
142
143  Description [optional]
144
145  SideEffects [required]
146
147  SeeAlso     [optional]
148
149******************************************************************************/
150void
151CalUniqueTablePrint(Cal_BddManager_t *bddManager)
152{
153  int i;
154  for(i = 0; i <= bddManager->numVars; i++){
155    CalHashTablePrint(bddManager->uniqueTable[i]);
156  }
157}
158
159/**Function********************************************************************
160
161  Synopsis    [Prints the function implemented by the argument BDD]
162
163  Description [Prints the function implemented by the argument BDD]
164
165  SideEffects [None]
166
167******************************************************************************/
168void
169CalBddFunctionPrint(Cal_BddManager_t * bddManager,
170                    Cal_Bdd_t  calBdd,
171                    char * name)
172{
173  Cal_Bdd_t T,E;
174  Cal_BddId_t id;
175  char c;
176  static int level;
177
178  if(level == 0)printf("%s = ",name);
179  level++;
180  printf("( ");
181  if(CalBddIsBddZero(bddManager, calBdd)){
182    printf("0 ");
183  }
184  else if(CalBddIsBddOne(bddManager, calBdd)){
185    printf("1 ");
186  }
187  else{
188    id = CalBddGetBddId(calBdd);
189    c = (char)((int)'a' + id - 1);
190    printf("%c ", c);
191    CalBddGetCofactors(calBdd, id, T, E);
192    CalBddFunctionPrint(bddManager, T, " ");
193    printf("+ %c' ", c);
194    CalBddFunctionPrint(bddManager, E, " ");
195  }
196  level--;
197  printf(") ");
198  if(level == 0)printf("\n");
199}
200
201/**Function********************************************************************
202 
203  Synopsis    [required]
204 
205  Description [optional]
206 
207  SideEffects [required]
208 
209  SeeAlso     [optional]
210 
211******************************************************************************/
212#if HAVE_STDARG_H
213int
214CalBddPreProcessing(Cal_BddManager_t *bddManager, int count, ...)
215{
216  int allValid;
217  va_list ap;
218  Cal_Bdd fUserBdd;
219  Cal_Bdd_t f;
220 
221  va_start(ap, count);
222#else
223#  if HAVE_VARARGS_H
224int
225CalBddPreProcessing(va_alist)
226va_dcl
227{
228  int allValid;
229  va_list ap;
230  Cal_Bdd *fUserBdd;
231  int count;
232  Cal_BddManager_t *bddManager;
233  Cal_Bdd_t f;
234 
235  va_start(ap);
236  bddManager = va_arg(ap, Cal_BddManager_t *);
237  count = va_arg(ap, int);
238#  endif
239#endif 
240
241  allValid=1;
242  while (count){
243    fUserBdd = va_arg(ap, Cal_Bdd);
244        if (fUserBdd == 0){
245          allValid=0;
246    }
247        else {
248      f = CalBddGetInternalBdd(bddManager, fUserBdd);
249      if (CalBddIsRefCountZero(f)){
250        CalBddFatalMessage("Bdd With Zero Reference Count Used.");
251      }
252    }
253    --count;
254  }
255  if (allValid) {
256    CalBddPostProcessing(bddManager);
257  }
258  va_end(ap);
259  return (allValid);
260}
261
262
263/**Function********************************************************************
264
265  Synopsis    [required]
266
267  Description [optional]
268
269  SideEffects [required]
270
271  SeeAlso     [optional]
272
273******************************************************************************/
274int
275CalBddPostProcessing(Cal_BddManager_t *bddManager)
276{
277  if (bddManager->gcCheck > 0) return CAL_BDD_OK;
278  bddManager->gcCheck = CAL_GC_CHECK;
279  if(bddManager->numNodes > bddManager->uniqueTableGCLimit){
280    long origNodes = bddManager->numNodes;
281    Cal_BddManagerGC(bddManager);
282    if ((bddManager->numNodes > bddManager->reorderingThreshold) &&
283        (3*bddManager->numNodes > 2* bddManager->uniqueTableGCLimit) &&
284        (bddManager->dynamicReorderingEnableFlag) &&
285        (bddManager->reorderTechnique != CAL_REORDER_NONE)){
286      CalCacheTableTwoFlush(bddManager->cacheTable);
287      if (bddManager->reorderMethod == CAL_REORDER_METHOD_BF){
288        CalBddReorderAuxBF(bddManager);
289      }
290      else{
291        CalBddReorderAuxDF(bddManager);
292      }
293    }
294    else {
295      /* Check if we should repack */
296      Cal_Assert(CalCheckAllValidity(bddManager));
297      if (bddManager->numNodes <
298          bddManager->repackAfterGCThreshold*origNodes){
299        CalRepackNodesAfterGC(bddManager);
300      }
301      Cal_Assert(CalCheckAllValidity(bddManager));
302    }
303    Cal_BddManagerSetGCLimit(bddManager);
304    if (bddManager->nodeLimit && (bddManager->numNodes >
305                                  bddManager->nodeLimit)){ 
306      CalBddWarningMessage("Overflow: Node Limit Exceeded");
307      bddManager->overflow = 1;
308      return CAL_BDD_OVERFLOWED;
309    }
310    /*
311     * Check to see if the cache table needs to be rehashed.
312     */
313    CalCacheTableRehash(bddManager);
314  }
315  return CAL_BDD_OK;
316}
317
318/**Function********************************************************************
319 
320  Synopsis    [required]
321 
322  Description [optional]
323 
324  SideEffects [required]
325 
326  SeeAlso     [optional]
327 
328******************************************************************************/
329int
330CalBddArrayPreProcessing(Cal_BddManager_t *bddManager, Cal_Bdd *userBddArray) 
331{
332  int i = 0;
333  Cal_Bdd userBdd;
334  while ((userBdd = userBddArray[i++])){
335    if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
336      return 0;
337    }
338  }
339  return 1;
340}
341   
342                       
343/**Function********************************************************************
344
345  Name        [CalBddFatalMessage]
346
347  Synopsis    [Prints fatal message and exits.]
348
349  Description [optional]
350
351  SideEffects [required]
352
353  SeeAlso     [optional]
354
355******************************************************************************/
356Cal_Bdd_t
357CalBddGetInternalBdd(Cal_BddManager bddManager, Cal_Bdd userBdd)
358{
359  Cal_Bdd_t resultBdd;
360  if (CalBddNodeIsOutPos(userBdd)){
361    CalBddNodeGetThenBdd(userBdd, resultBdd);
362  }
363  else {
364    Cal_Bdd userBddNot = CalBddNodeNot(userBdd);
365    Cal_Bdd_t internalBdd;
366        CalBddNodeGetThenBdd(userBddNot,internalBdd);
367    CalBddNot(internalBdd, resultBdd);
368  }
369  return resultBdd;
370}
371
372/**Function********************************************************************
373
374  Name        [CalBddFatalMessage]
375
376  Synopsis    [Prints fatal message and exits.]
377
378  Description [optional]
379
380  SideEffects [required]
381
382  SeeAlso     [optional]
383
384******************************************************************************/
385Cal_Bdd
386CalBddGetExternalBdd(Cal_BddManager_t *bddManager, Cal_Bdd_t internalBdd)
387{
388  CalHashTable_t *hashTableForUserBdd = bddManager->uniqueTable[0];
389  Cal_Bdd_t resultBdd;
390  int found;
391 
392  if(CalBddIsOutPos(internalBdd)){
393    found = CalHashTableFindOrAdd(hashTableForUserBdd, internalBdd,
394                          bddManager->bddOne, &resultBdd);
395  }
396  else {
397    Cal_Bdd_t internalBddNot;
398    CalBddNot(internalBdd, internalBddNot);
399    found = CalHashTableFindOrAdd(hashTableForUserBdd, internalBddNot,
400                          bddManager->bddOne, &resultBdd);
401    CalBddNot(resultBdd, resultBdd);
402  }
403  if (found == 0){
404    CalBddIcrRefCount(internalBdd);
405  }
406  CalBddIcrRefCount(resultBdd);
407  return CalBddGetBddNode(resultBdd);
408}
409
410
411/**Function********************************************************************
412
413  Name        [CalBddFatalMessage]
414
415  Synopsis    [Prints fatal message and exits.]
416
417  Description [optional]
418
419  SideEffects [required]
420
421  SeeAlso     [optional]
422
423******************************************************************************/
424void
425CalBddFatalMessage(char *string)
426{
427  (void) fprintf(stderr,"Fatal: %s\n", string);
428  exit(-1);
429}
430/**Function********************************************************************
431
432  Name        [CalBddWarningMessage]
433
434  Synopsis    [Prints warning message.]
435
436  Description [optional]
437
438  SideEffects [required]
439
440  SeeAlso     [optional]
441
442******************************************************************************/
443void
444CalBddWarningMessage(char *string)
445{
446  (void) fprintf(stderr,"Warning: %s\n", string);
447}
448
449/**Function********************************************************************
450
451  Synopsis    [required]
452
453  Description [optional]
454
455  SideEffects [required]
456
457  SeeAlso     [optional]
458
459******************************************************************************/
460void
461CalBddNodePrint(CalBddNode_t *bddNode)
462{
463  int refCount;
464  CalBddNodeGetRefCount(bddNode, refCount);
465  printf("Node (%lx) thenBdd(%2d %lx)  elseBdd(%2d %lx) ref_count (%d) next (%lx)\n",
466         (CalAddress_t)bddNode,
467         CalBddNodeGetThenBddId(bddNode),
468         (CalAddress_t) CalBddNodeGetThenBddNode(bddNode), 
469         CalBddNodeGetElseBddId(bddNode),
470         (CalAddress_t) CalBddNodeGetElseBddNode(bddNode),
471         refCount, (CalAddress_t)bddNode->nextBddNode);
472}
473
474/**Function********************************************************************
475
476  Synopsis    [required]
477
478  Description [optional]
479
480  SideEffects [required]
481
482  SeeAlso     [optional]
483
484******************************************************************************/
485
486void
487CalBddPrint(Cal_Bdd_t calBdd)
488{
489  printf("Id(%2d) node(%lx) ",
490      CalBddGetBddId(calBdd), (CalAddress_t) CalBddGetBddNode(calBdd));
491  printf("thenBdd(%2d %lx)  elseBdd(%2d %lx)\n",
492         CalBddGetThenBddId(calBdd),
493         (CalAddress_t) CalBddGetThenBddNode(calBdd), 
494         CalBddGetElseBddId(calBdd),
495         (CalAddress_t) CalBddGetElseBddNode(calBdd));
496}
497
498#ifdef TEST_CALBDDNODE
499main(int argc, char **argv)
500{
501  CalBddNode_t *bddNode, *thenBddNode, *elseBddNode;
502
503  bddNode = Cal_MemAlloc(CalBddNode_t, 1);
504  thenBddNode = Cal_MemAlloc(CalBddNode_t, 1);
505  elseBddNode = Cal_MemAlloc(CalBddNode_t, 1);
506
507  CalBddNodePutThenBddId(bddNode, 1);
508  CalBddNodePutThenBddNode(bddNode, thenBddNode);
509  CalBddNodePutElseBddId(bddNode, 2);
510  CalBddNodePutElseBddNode(bddNode, elseBddNode);
511
512  printf("then( 1 %x) else( 2 %x)\n", thenBddNode, elseBddNode);
513  CalBddNodePrint(bddNode);
514}
515#endif
516
517
518/**Function********************************************************************
519
520  Synopsis    [Prints a hash table.]
521
522  Description [optional]
523
524  SideEffects [required]
525
526  SeeAlso     [optional]
527
528******************************************************************************/
529void
530CalHashTablePrint(CalHashTable_t *hashTable)
531{
532  int i;
533  CalBddNode_t *ptr;
534  Cal_Bdd_t calBdd, T, E;
535  int refCount, firstFlag;
536
537  printf("HashTable bddId(%d) entries(%ld) bins(%ld) capacity(%ld)\n",
538         hashTable->bddId, hashTable->numEntries, hashTable->numBins,
539         hashTable->maxCapacity);
540  for(i = 0; i < hashTable->numBins; i++){
541    ptr = hashTable->bins[i];
542    firstFlag = 1;
543    while(ptr != Cal_Nil(CalBddNode_t)){
544      CalBddPutBddNode(calBdd, ptr);
545      CalBddNodeGetThenBdd(ptr, T);
546      CalBddNodeGetElseBdd(ptr, E);
547      if (firstFlag){
548        printf("\tbin = (%d) ", i);
549        firstFlag = 0;
550      }
551      printf("\t\tbddNode(%lx) ", (CalAddress_t)ptr);
552      printf("thenId(%d) ", CalBddGetBddId(T)); 
553      printf("thenBddNode(%lx) ", (CalAddress_t) CalBddGetBddNode(T));
554      printf("elseId(%d) ", CalBddGetBddId(E)); 
555      printf("elseBddNode(%lx) ", (unsigned long)CalBddGetBddNode(E));
556      CalBddGetRefCount(calBdd, refCount);
557      printf("refCount(%d)\n", refCount);
558      ptr = CalBddNodeGetNextBddNode(ptr);
559    }
560  }
561}
562
563/**Function********************************************************************
564
565  Synopsis    [required]
566
567  Description [optional]
568
569  SideEffects [required]
570
571  SeeAlso     [optional]
572
573******************************************************************************/
574void
575CalHashTableOnePrint(CalHashTable_t *hashTable, int flag)
576{
577  int i;
578  CalBddNode_t *ptr, *node;
579  Cal_Bdd_t keyBdd;
580
581  printf("*************************************************\n");
582  for(i = 0; i < hashTable->numBins; i++){
583    ptr = hashTable->bins[i];
584    while(ptr != Cal_Nil(CalBddNode_t)){
585      CalBddNodeGetThenBdd(ptr, keyBdd);
586      node = CalBddNodeGetElseBddNode(ptr);
587      if(flag == 1){
588        printf("Key(%d %lx) Value(%f)\n", 
589            CalBddGetBddId(keyBdd), (CalAddress_t)CalBddGetBddNode(keyBdd), *(double *)node); 
590      }
591      else{
592        printf("Key(%d %lx) Value(%d)\n",
593            CalBddGetBddId(keyBdd), (CalAddress_t)CalBddGetBddNode(keyBdd),  *(int *)node); 
594      }
595      ptr = CalBddNodeGetNextBddNode(ptr);
596    }
597  }
598}
599
600/**Function********************************************************************
601
602  Synopsis    [Initializer for the portable random number generator.]
603
604  Description [Initializer for the portable number generator based on
605  ran2 in "Numerical Recipes in C." The input is the seed for the
606  generator. If it is negative, its absolute value is taken as seed.
607  If it is 0, then 1 is taken as seed. The initialized sets up the two
608  recurrences used to generate a long-period stream, and sets up the
609  shuffle table.]
610
611  SideEffects [None]
612
613  SeeAlso     [CalUtilRandom]
614
615******************************************************************************/
616void
617CalUtilSRandom(long seed)
618{
619    int i;
620
621    if (seed < 0)       utilRand = -seed;
622    else if (seed == 0) utilRand = 1;
623    else                utilRand = seed;
624    utilRand2 = utilRand;
625    /* Load the shuffle table (after 11 warm-ups). */
626    for (i = 0; i < CAL_STAB_SIZE + 11; i++) {
627        long int w;
628        w = utilRand / CAL_LEQQ1;
629        utilRand = CAL_LEQA1 * (utilRand - w * CAL_LEQQ1) - w * CAL_LEQR1;
630        utilRand += (utilRand < 0) * CAL_MODULUS1;
631        shuffleTable[i % CAL_STAB_SIZE] = utilRand;
632    }
633    shuffleSelect = shuffleTable[1 % CAL_STAB_SIZE];
634} /* end of CalUtilSRandom */
635
636/**Function********************************************************************
637
638  Synopsis    [Portable random number generator.]
639
640  Description [Portable number generator based on ran2 from "Numerical
641  Recipes in C." It is a long period (> 2 * 10^18) random number generator
642  of L'Ecuyer with Bays-Durham shuffle. Returns a long integer uniformly
643  distributed between 0 and 2147483561 (inclusive of the endpoint values).
644  The random generator can be explicitly initialized by calling
645  CalUtilSRandom. If no explicit initialization is performed, then the
646  seed 1 is assumed.]
647
648  SideEffects []
649
650  SeeAlso     [CalUtilSRandom]
651
652******************************************************************************/
653long
654CalUtilRandom(void)
655{
656    int i;      /* index in the shuffle table */
657    long int w; /* work variable */
658
659    /* utilRand == 0 if the geneartor has not been initialized yet. */
660    if (utilRand == 0) CalUtilSRandom((long)1);
661
662    /* Compute utilRand = (utilRand * CAL_LEQA1) % CAL_MODULUS1 avoiding
663    ** overflows by Schrage's method.
664    */
665    w          = utilRand / CAL_LEQQ1;
666    utilRand   = CAL_LEQA1 * (utilRand - w * CAL_LEQQ1) - w * CAL_LEQR1;
667    utilRand  += (utilRand < 0) * CAL_MODULUS1;
668
669    /* Compute utilRand2 = (utilRand2 * CAL_LEQA2) % CAL_MODULUS2 avoiding
670    ** overflows by Schrage's method.
671    */
672    w          = utilRand2 / CAL_LEQQ2;
673    utilRand2  = CAL_LEQA2 * (utilRand2 - w * CAL_LEQQ2) - w * CAL_LEQR2;
674    utilRand2 += (utilRand2 < 0) * CAL_MODULUS2;
675
676    /* utilRand is shuffled with the Bays-Durham algorithm.
677    ** shuffleSelect and utilRand2 are combined to generate the output.
678    */
679
680    /* Pick one element from the shuffle table; "i" will be in the range
681    ** from 0 to CAL_STAB_SIZE-1.
682    */
683    i = shuffleSelect / CAL_STAB_DIV;
684    /* Mix the element of the shuffle table with the current iterate of
685    ** the second sub-generator, and replace the chosen element of the
686    ** shuffle table with the current iterate of the first sub-generator.
687    */
688    shuffleSelect   = shuffleTable[i] - utilRand2;
689    shuffleTable[i] = utilRand;
690    shuffleSelect  += (shuffleSelect < 1) * (CAL_MODULUS1 - 1);
691    /* Since shuffleSelect != 0, and we want to be able to return 0,
692    ** here we subtract 1 before returning.
693    */
694    return(shuffleSelect - 1);
695
696} /* end of CalUtilRandom */
697
698
Note: See TracBrowser for help on using the repository browser.