source: vis_dev/glu-2.3/src/calBdd/calBddSize.c @ 100

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

library glu 2.3
File size: 17.4 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [calBddSize.c]
4
5  PackageName [cal]
6
7  Synopsis    [BDD size and profile routines]
8             
9
10  Description [ ]
11
12  SeeAlso     [optional]
13
14  Author      [Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)
15               Rajeev Ranjan   (rajeev@eecs.berkeley.edu)
16               Originally written by David Long.
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: calBddSize.c,v 1.3 2002/09/21 20:39:24 fabio Exp $]
38
39******************************************************************************/
40#include "calInt.h"
41
42/*---------------------------------------------------------------------------*/
43/* Constant declarations                                                     */
44/*---------------------------------------------------------------------------*/
45
46/*---------------------------------------------------------------------------*/
47/* Type declarations                                                         */
48/*---------------------------------------------------------------------------*/
49typedef int (*CountFn_t)(Cal_Bdd_t);
50
51/*---------------------------------------------------------------------------*/
52/* Stucture declarations                                                     */
53/*---------------------------------------------------------------------------*/
54
55/*---------------------------------------------------------------------------*/
56/* Variable declarations                                                     */
57/*---------------------------------------------------------------------------*/
58
59
60/*---------------------------------------------------------------------------*/
61/* Macro declarations                                                        */
62/*---------------------------------------------------------------------------*/
63
64/**AutomaticStart*************************************************************/
65
66/*---------------------------------------------------------------------------*/
67/* Static function prototypes                                                */
68/*---------------------------------------------------------------------------*/
69
70static void BddMarkBdd(Cal_Bdd_t f);
71static int BddCountNoNodes(Cal_Bdd_t f);
72static int BddCountNodes(Cal_Bdd_t f);
73static long BddSizeStep(Cal_Bdd_t f, CountFn_t countFn);
74static void BddProfileStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, long * levelCounts, CountFn_t countFn);
75static void BddHighestRefStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, CalHashTable_t * h);
76static void BddDominatedStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, long * funcCounts, CalHashTable_t * h);
77
78/**AutomaticEnd***************************************************************/
79
80static
81int (*(countingFns[]))(Cal_Bdd_t) = 
82{
83  BddCountNoNodes,
84  BddCountNodes,
85};
86
87/*---------------------------------------------------------------------------*/
88/* Definition of exported functions                                          */
89/*---------------------------------------------------------------------------*/
90
91/**Function********************************************************************
92
93  Synopsis    [Returns the number of nodes in f when negout is nonzero. If
94  negout is zero, we pretend that the BDDs don't have negative-output pointers.]
95
96  Description [optional]
97
98  SideEffects [None]
99
100  SeeAlso     [optional]
101
102******************************************************************************/
103long
104Cal_BddSize(Cal_BddManager bddManager, Cal_Bdd fUserBdd, int  negout)
105{
106  Cal_Bdd_t f, g;
107
108  if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
109    f = CalBddGetInternalBdd(bddManager, fUserBdd);
110    g =  CalBddOne(bddManager);
111    CalBddPutMark(g, 0);
112    BddMarkBdd(f);
113    return BddSizeStep(f, countingFns[!negout]);
114  }
115  return (0l);
116}
117
118
119/**Function********************************************************************
120
121  Synopsis    [The routine is like Cal_BddSize, but takes a null-terminated
122               array of BDDs and accounts for sharing of nodes.]
123
124  Description [optional]
125
126  SideEffects [None]
127
128  SeeAlso     [optional]
129
130******************************************************************************/
131long
132Cal_BddSizeMultiple(Cal_BddManager bddManager, Cal_Bdd *fUserBddArray,
133                    int  negout)
134{
135  long size;
136  Cal_Bdd_t *f;
137  Cal_Bdd_t g;
138  Cal_Bdd_t *fArray;
139  int i, j;
140 
141  if (CalBddArrayPreProcessing(bddManager, fUserBddArray) == 0){
142    return -1;
143  }
144 
145  for(i = 0; fUserBddArray[i]; ++i);
146
147  fArray = Cal_MemAlloc(Cal_Bdd_t, i+1);
148  for (j=0; j < i; j++){
149    fArray[j] = CalBddGetInternalBdd(bddManager,fUserBddArray[j]);
150  }
151  fArray[j] = bddManager->bddNull;
152 
153  g  =  CalBddOne(bddManager);
154  CalBddPutMark(g, 0);
155  for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
156    BddMarkBdd(*f);
157  }
158  size  =  0l;
159  for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
160    size +=  BddSizeStep(*f, countingFns[!negout]);
161  }
162  Cal_MemFree(fArray);
163  return size;
164}
165
166/**Function********************************************************************
167
168  Synopsis    [Returns a "node profile" of f, i.e., the number of nodes at each
169  level in f.]
170
171  Description [negout is as in Cal_BddSize. levelCounts should be an array of
172  size Cal_BddVars(bddManager)+1 to hold the profile.]
173
174  SideEffects [None]
175
176  SeeAlso     [optional]
177
178******************************************************************************/
179void
180Cal_BddProfile(Cal_BddManager bddManager, Cal_Bdd fUserBdd,
181               long * levelCounts, int  negout)
182{
183  Cal_BddIndex_t i;
184  Cal_Bdd_t f, g;
185  if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
186    f = CalBddGetInternalBdd(bddManager, fUserBdd);
187    for(i = 0; i <=  bddManager->numVars; i++){
188      levelCounts[i] = 0l;
189    }
190    g = CalBddOne(bddManager);
191    CalBddPutMark(g, 0);
192    BddMarkBdd(f);
193    BddProfileStep(bddManager, f, levelCounts, countingFns[!negout]);
194  }
195}
196
197
198/**Function********************************************************************
199
200  Synopsis    []
201
202  Description [optional]
203
204  SideEffects [None]
205
206  SeeAlso     [optional]
207
208******************************************************************************/
209void
210Cal_BddProfileMultiple(Cal_BddManager bddManager, Cal_Bdd *fUserBddArray,
211                       long * levelCounts, int  negout)
212{
213  Cal_Bdd_t *f, *fArray;
214  Cal_Bdd_t g;
215  int i, j;
216 
217  CalBddArrayPreProcessing(bddManager, fUserBddArray);
218
219  for(i = 0; fUserBddArray[i]; ++i);
220
221  fArray = Cal_MemAlloc(Cal_Bdd_t, i+1);
222  for (j=0; j < i; j++){
223    fArray[j] = CalBddGetInternalBdd(bddManager,fUserBddArray[j]);
224  }
225  fArray[j] = bddManager->bddNull;
226   
227  for(i = 0; i <=  bddManager->numVars; i++){
228    levelCounts[i] = 0l;
229  }
230  g = CalBddOne(bddManager);
231  CalBddPutMark(g, 0);
232  for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
233    BddMarkBdd(*f);
234  }
235  for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
236    BddProfileStep(bddManager, *f, levelCounts, countingFns[!negout]);
237  }
238  Cal_MemFree(fArray);
239}
240
241
242/**Function********************************************************************
243
244  Synopsis    [Returns a "function profile" for f.]
245
246  Description [The nth entry of the function
247  profile array is the number of subfunctions of f which may be obtained by
248  restricting the variables whose index is less than n.  An entry of zero
249  indicates that f is independent of the variable with the corresponding index.]
250
251  SideEffects []
252
253  SeeAlso     [optional]
254
255******************************************************************************/
256void
257Cal_BddFunctionProfile(Cal_BddManager bddManager, Cal_Bdd fUserBdd,
258                       long * funcCounts) 
259{
260  long i;
261  Cal_BddIndex_t j;
262  CalHashTable_t *h;
263  Cal_Bdd_t f;
264 
265  /* The number of subfunctions obtainable by restricting the */
266  /* variables of index < n is the number of subfunctions whose top */
267  /* variable has index n plus the number of subfunctions obtainable */
268  /* by restricting the variables of index < n+1 minus the number of */
269  /* these latter subfunctions whose highest reference is by a node at */
270  /* level n. */
271  /* The strategy will be to start with the number of subfunctions */
272  /* whose top variable has index n.  We compute the highest level at */
273  /* which each subfunction is referenced.  Then we work bottom up; at */
274  /* level n we add in the result from level n+1 and subtract the */
275  /* number of subfunctions whose highest reference is at level n. */
276
277  Cal_BddProfile(bddManager, fUserBdd, funcCounts, 0);
278  if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
279    f = CalBddGetInternalBdd(bddManager, fUserBdd);
280    /* Encode the profile.  The low bit of a count will be zero for */
281    /* those levels where f actually has a node. */
282    for(j = 0; j < bddManager->numVars; ++j){
283      if(!funcCounts[j]){
284        funcCounts[j] = 1;
285      }
286      else{
287        funcCounts[j] <<= 1;
288      }
289    }
290    h = CalHashTableOneInit(bddManager, sizeof(int));
291    /* For each subfunction in f, compute the highest level where it is */
292    /* referenced.  f itself is conceptually referenced at the highest */
293    /* possible level, which we represent by -1. */
294    i =  -1;
295    CalHashTableOneInsert(h, f, (char *)&i);
296    BddHighestRefStep(bddManager, f, h);
297    /* Walk through these results.  For each subfunction, decrement the */
298    /* count at the highest level where it is referenced. */
299    BddDominatedStep(bddManager, f, funcCounts, h);
300    CalHashTableOneQuit(h);
301    /* Now add each level n+1 result to that of level n. */
302    for(i = bddManager->numVars-1, j = i+1; i>=  0; --i){
303      if(funcCounts[i] !=  1){
304        funcCounts[i] = (funcCounts[i] >> 1) + funcCounts[j];
305        j = i;
306      }
307      else{
308          funcCounts[i] = 0;
309      }
310    }
311  }
312}
313
314/**Function********************************************************************
315
316  Synopsis    [Returns a "function profile" for fArray.]
317
318  Description [optional]
319
320  SideEffects [None]
321
322  SeeAlso     [optional]
323
324******************************************************************************/
325void
326Cal_BddFunctionProfileMultiple(Cal_BddManager bddManager, Cal_Bdd
327                               *fUserBddArray, long * funcCounts)
328{
329  long i;
330  Cal_BddIndex_t j;
331  Cal_Bdd_t *f, *fArray;
332  CalHashTable_t *h;
333
334  CalBddArrayPreProcessing(bddManager, fUserBddArray);
335
336  for(i = 0; fUserBddArray[i]; ++i);
337
338  fArray = Cal_MemAlloc(Cal_Bdd_t, i+1);
339  for (j=0; j < i; j++){
340    fArray[j] = CalBddGetInternalBdd(bddManager,fUserBddArray[j]);
341  }
342  fArray[j] = bddManager->bddNull;
343
344  /* See cmu_bdd_function_profile for the strategy involved here. */
345  Cal_BddProfileMultiple(bddManager, fUserBddArray, funcCounts, 0);
346  for(j = 0; j < bddManager->numVars; ++j){
347    if(!funcCounts[j]){
348      funcCounts[j] = 1;
349    }
350    else{
351      funcCounts[j] <<= 1;
352    }
353  }
354  h = CalHashTableOneInit(bddManager, sizeof(int));
355  for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
356    BddHighestRefStep(bddManager, *f, h);
357  }
358  i = -1;
359  for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
360    CalHashTableOneInsert(h, *f, (char *)&i);
361  }
362  for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
363    BddDominatedStep(bddManager, *f, funcCounts, h);
364  }
365  CalHashTableOneQuit(h);
366  for(i = bddManager->numVars-1, j = i+1; i >=  0; --i){
367    if(funcCounts[i] !=  1){
368      funcCounts[i] = (funcCounts[i] >> 1) + funcCounts[j];
369      j = i;
370    }
371    else{
372      funcCounts[i] = 0;
373    }
374  }
375  Cal_MemFree(fArray);
376}
377
378/*---------------------------------------------------------------------------*/
379/* Definition of internal functions                                          */
380/*---------------------------------------------------------------------------*/
381
382/*---------------------------------------------------------------------------*/
383/* Definition of static functions                                            */
384/*---------------------------------------------------------------------------*/
385
386
387/**Function********************************************************************
388
389  Synopsis    []
390
391  Description [optional]
392
393  SideEffects [required]
394
395  SeeAlso     [optional]
396
397******************************************************************************/
398static void
399BddMarkBdd(Cal_Bdd_t  f)
400{
401  int currMarking, thisMarking;
402  Cal_Bdd_t thenBdd, elseBdd;
403
404  currMarking = CalBddGetMark(f);
405  thisMarking = (1 << CalBddIsComplement(f));
406  if(currMarking & thisMarking){
407    return;
408  }
409  CalBddPutMark(f, currMarking | thisMarking);
410  if(CalBddIsBddConst(f)){
411    return;
412  }
413  CalBddGetThenBdd(f, thenBdd);
414  BddMarkBdd(thenBdd);
415  CalBddGetElseBdd(f, elseBdd);
416  BddMarkBdd(elseBdd);
417}
418
419
420/**Function********************************************************************
421
422  Synopsis    []
423
424  Description [optional]
425
426  SideEffects [required]
427
428  SeeAlso     [optional]
429
430******************************************************************************/
431static int
432BddCountNoNodes(
433  Cal_Bdd_t  f)
434{
435  return (CalBddGetMark(f) > 0);
436}
437
438
439/**Function********************************************************************
440
441  Synopsis    []
442
443  Description [optional]
444
445  SideEffects [required]
446
447  SeeAlso     [optional]
448
449******************************************************************************/
450static int
451BddCountNodes(
452  Cal_Bdd_t  f)
453{
454  int mark;
455
456  mark = CalBddGetMark(f);
457  return (((mark & 0x1) !=  0) + ((mark & 0x2) !=  0));
458}
459
460
461
462/**Function********************************************************************
463
464  Synopsis    []
465
466  Description [optional]
467
468  SideEffects [required]
469
470  SeeAlso     [optional]
471
472******************************************************************************/
473static long
474BddSizeStep(
475  Cal_Bdd_t  f,
476  CountFn_t countFn)
477{
478  long result;
479  Cal_Bdd_t thenBdd, elseBdd;
480
481  if(!CalBddGetMark(f)){
482    return (0l);
483  }
484  result = (*countFn)(f);
485  if(!CalBddIsBddConst(f)){
486    CalBddGetThenBdd(f, thenBdd);
487    CalBddGetElseBdd(f, elseBdd);
488    result +=
489        BddSizeStep(thenBdd, countFn) +
490        BddSizeStep(elseBdd, countFn);
491  }
492  CalBddPutMark(f, 0);
493  return result;
494}
495
496
497
498/**Function********************************************************************
499
500  Synopsis    []
501
502  Description [optional]
503
504  SideEffects [required]
505
506  SeeAlso     [optional]
507
508******************************************************************************/
509static void
510BddProfileStep(
511  Cal_BddManager_t * bddManager,
512  Cal_Bdd_t  f,
513  long * levelCounts,
514  CountFn_t countFn)
515{
516  Cal_Bdd_t thenBdd, elseBdd;
517  if(!CalBddGetMark(f)){
518    return;
519  }
520  if(CalBddIsBddConst(f)){
521    levelCounts[bddManager->numVars] += (*countFn)(f);
522  }
523  else{
524    levelCounts[CalBddGetBddIndex(bddManager, f)] += (*countFn)(f);
525    CalBddGetThenBdd(f, thenBdd);
526    BddProfileStep(bddManager, thenBdd, levelCounts, countFn);
527    CalBddGetElseBdd(f, elseBdd);
528    BddProfileStep(bddManager, elseBdd, levelCounts, countFn);
529  }
530  CalBddPutMark(f, 0);
531}
532
533
534
535/**Function********************************************************************
536
537  Synopsis    []
538
539  Description [optional]
540
541  SideEffects [required]
542
543  SeeAlso     [optional]
544
545******************************************************************************/
546static void
547BddHighestRefStep(
548  Cal_BddManager_t * bddManager,
549  Cal_Bdd_t  f,
550  CalHashTable_t * h)
551{
552  int fIndex;
553  Cal_Bdd_t keyBdd;
554  int *dataPtr;
555
556  if(CalBddIsBddConst(f)){
557    return;
558  }
559  fIndex = CalBddGetBddIndex(bddManager, f);
560  CalBddGetThenBdd(f, keyBdd);
561  if(CalHashTableOneLookup(h, keyBdd, (char **)&dataPtr)){
562    if(*dataPtr > fIndex){
563      *dataPtr = fIndex;
564    }
565  }
566  else{
567    CalHashTableOneInsert(h, keyBdd, (char *)&fIndex);
568    BddHighestRefStep(bddManager, keyBdd, h);
569  }
570  CalBddGetElseBdd(f, keyBdd);
571  if(CalHashTableOneLookup(h, keyBdd, (char **)&dataPtr)){
572    if(*dataPtr > fIndex){
573      *dataPtr = fIndex;
574    }
575  }
576  else{
577    CalHashTableOneInsert(h, keyBdd, (char *)&fIndex);
578    BddHighestRefStep(bddManager, keyBdd, h);
579  }
580}
581
582/**Function********************************************************************
583
584  Synopsis    []
585
586  Description [optional]
587
588  SideEffects [required]
589
590  SeeAlso     [optional]
591
592******************************************************************************/
593static void
594BddDominatedStep(
595  Cal_BddManager_t * bddManager,
596  Cal_Bdd_t  f,
597  long * funcCounts,
598  CalHashTable_t * h)
599{
600  Cal_Bdd_t thenBdd, elseBdd;
601  int *dataPtr;
602
603  CalHashTableOneLookup(h, f, (char **)&dataPtr);
604  if(*dataPtr >=  0)
605    funcCounts[*dataPtr] -= 2;
606  if(*dataPtr > -2){
607    *dataPtr = -2;
608    if(!CalBddIsBddConst(f)){
609      CalBddGetThenBdd(f, thenBdd);
610      BddDominatedStep(bddManager, thenBdd, funcCounts, h);
611      CalBddGetElseBdd(f, elseBdd);
612      BddDominatedStep(bddManager, elseBdd, funcCounts, h);
613    }
614  }
615}
616
617
618
619
620
621
622
623
624
Note: See TracBrowser for help on using the repository browser.