src/calBdd/calBddSize.c File Reference

#include "calInt.h"

Include dependency graph for calBddSize.c:

Typedefs
typedef int(*	CountFn_t )(Cal_Bdd_t)
Functions
static void	BddMarkBdd (Cal_Bdd_t f)
static int	BddCountNoNodes (Cal_Bdd_t f)
static int	BddCountNodes (Cal_Bdd_t f)
static long	BddSizeStep (Cal_Bdd_t f, CountFn_t countFn)
static void	BddProfileStep (Cal_BddManager_t bddManager, Cal_Bdd_t f, long levelCounts, CountFn_t countFn)
static void	BddHighestRefStep (Cal_BddManager_t bddManager, Cal_Bdd_t f, CalHashTable_t h)
static void	BddDominatedStep (Cal_BddManager_t bddManager, Cal_Bdd_t f, long funcCounts, CalHashTable_t *h)
static int	countingFns (Cal_Bdd_t)
long	Cal_BddSize (Cal_BddManager bddManager, Cal_Bdd fUserBdd, int negout)
long	Cal_BddSizeMultiple (Cal_BddManager bddManager, Cal_Bdd *fUserBddArray, int negout)
void	Cal_BddProfile (Cal_BddManager bddManager, Cal_Bdd fUserBdd, long *levelCounts, int negout)
void	Cal_BddProfileMultiple (Cal_BddManager bddManager, Cal_Bdd fUserBddArray, long levelCounts, int negout)
void	Cal_BddFunctionProfile (Cal_BddManager bddManager, Cal_Bdd fUserBdd, long *funcCounts)
void	Cal_BddFunctionProfileMultiple (Cal_BddManager bddManager, Cal_Bdd fUserBddArray, long funcCounts)

Typedef Documentation

typedef int(* CountFn_t)(Cal_Bdd_t)

CFile***********************************************************************

FileName [calBddSize.c]

PackageName [cal]

Synopsis [BDD size and profile routines]

Description [ ]

SeeAlso [optional]

Author [Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@eecs.berkeley.edu) Originally written by David Long. ] Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved.

Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

Revision [

Id: calBddSize.c,v 1.3 2002/09/21 20:39:24 fabio Exp

]

Definition at line 49 of file calBddSize.c.

Function Documentation

static int BddCountNodes ( Cal_Bdd_t f ) [static]

Function********************************************************************

Synopsis []

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 451 of file calBddSize.c.

00453 {
00454   int mark;
00455 
00456   mark = CalBddGetMark(f);
00457   return (((mark & 0x1) !=  0) + ((mark & 0x2) !=  0));
00458 }

static int BddCountNoNodes ( Cal_Bdd_t f ) [static]

Function********************************************************************

Synopsis []

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 432 of file calBddSize.c.

00434 {
00435   return (CalBddGetMark(f) > 0);
00436 }

static void BddDominatedStep	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd_t	f,
		long *	funcCounts,
		CalHashTable_t *	h
	)			`[static]`

Function********************************************************************

Synopsis []

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 594 of file calBddSize.c.

00599 {
00600   Cal_Bdd_t thenBdd, elseBdd;
00601   int *dataPtr;
00602 
00603   CalHashTableOneLookup(h, f, (char **)&dataPtr);
00604   if(*dataPtr >=  0)
00605     funcCounts[*dataPtr] -= 2;
00606   if(*dataPtr > -2){
00607     *dataPtr = -2;
00608     if(!CalBddIsBddConst(f)){
00609       CalBddGetThenBdd(f, thenBdd);
00610       BddDominatedStep(bddManager, thenBdd, funcCounts, h);
00611       CalBddGetElseBdd(f, elseBdd);
00612       BddDominatedStep(bddManager, elseBdd, funcCounts, h);
00613     }
00614   }
00615 }

static void BddHighestRefStep	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd_t	f,
		CalHashTable_t *	h
	)			`[static]`

Function********************************************************************

Synopsis []

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 547 of file calBddSize.c.

00551 {
00552   int fIndex;
00553   Cal_Bdd_t keyBdd;
00554   int *dataPtr;
00555 
00556   if(CalBddIsBddConst(f)){
00557     return;
00558   }
00559   fIndex = CalBddGetBddIndex(bddManager, f);
00560   CalBddGetThenBdd(f, keyBdd);
00561   if(CalHashTableOneLookup(h, keyBdd, (char **)&dataPtr)){
00562     if(*dataPtr > fIndex){
00563       *dataPtr = fIndex;
00564     }
00565   }
00566   else{
00567     CalHashTableOneInsert(h, keyBdd, (char *)&fIndex);
00568     BddHighestRefStep(bddManager, keyBdd, h);
00569   }
00570   CalBddGetElseBdd(f, keyBdd);
00571   if(CalHashTableOneLookup(h, keyBdd, (char **)&dataPtr)){
00572     if(*dataPtr > fIndex){
00573       *dataPtr = fIndex;
00574     }
00575   }
00576   else{
00577     CalHashTableOneInsert(h, keyBdd, (char *)&fIndex);
00578     BddHighestRefStep(bddManager, keyBdd, h);
00579   }
00580 }

static void BddMarkBdd ( Cal_Bdd_t f ) [static]

AutomaticStart

Function********************************************************************

Synopsis []

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 399 of file calBddSize.c.

00400 {
00401   int currMarking, thisMarking;
00402   Cal_Bdd_t thenBdd, elseBdd;
00403 
00404   currMarking = CalBddGetMark(f);
00405   thisMarking = (1 << CalBddIsComplement(f));
00406   if(currMarking & thisMarking){
00407     return;
00408   }
00409   CalBddPutMark(f, currMarking | thisMarking);
00410   if(CalBddIsBddConst(f)){
00411     return;
00412   }
00413   CalBddGetThenBdd(f, thenBdd);
00414   BddMarkBdd(thenBdd);
00415   CalBddGetElseBdd(f, elseBdd);
00416   BddMarkBdd(elseBdd);
00417 }

static void BddProfileStep	(	Cal_BddManager_t *	bddManager,
		Cal_Bdd_t	f,
		long *	levelCounts,
		CountFn_t	countFn
	)			`[static]`

Function********************************************************************

Synopsis []

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 510 of file calBddSize.c.

00515 {
00516   Cal_Bdd_t thenBdd, elseBdd;
00517   if(!CalBddGetMark(f)){
00518     return;
00519   }
00520   if(CalBddIsBddConst(f)){
00521     levelCounts[bddManager->numVars] += (*countFn)(f);
00522   }
00523   else{
00524     levelCounts[CalBddGetBddIndex(bddManager, f)] += (*countFn)(f);
00525     CalBddGetThenBdd(f, thenBdd);
00526     BddProfileStep(bddManager, thenBdd, levelCounts, countFn);
00527     CalBddGetElseBdd(f, elseBdd);
00528     BddProfileStep(bddManager, elseBdd, levelCounts, countFn);
00529   }
00530   CalBddPutMark(f, 0);
00531 }

static long BddSizeStep	(	Cal_Bdd_t	f,
		CountFn_t	countFn
	)			`[static]`

Function********************************************************************

Synopsis []

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 474 of file calBddSize.c.

00477 {
00478   long result;
00479   Cal_Bdd_t thenBdd, elseBdd;
00480 
00481   if(!CalBddGetMark(f)){
00482     return (0l);
00483   }
00484   result = (*countFn)(f);
00485   if(!CalBddIsBddConst(f)){
00486     CalBddGetThenBdd(f, thenBdd);
00487     CalBddGetElseBdd(f, elseBdd);
00488     result +=
00489         BddSizeStep(thenBdd, countFn) +
00490         BddSizeStep(elseBdd, countFn);
00491   }
00492   CalBddPutMark(f, 0);
00493   return result;
00494 }

void Cal_BddFunctionProfile	(	Cal_BddManager	bddManager,
		Cal_Bdd	fUserBdd,
		long *	funcCounts
	)

Function********************************************************************

Synopsis [Returns a "function profile" for f.]

Description [The nth entry of the function profile array is the number of subfunctions of f which may be obtained by restricting the variables whose index is less than n. An entry of zero indicates that f is independent of the variable with the corresponding index.]

SideEffects []

SeeAlso [optional]

Definition at line 257 of file calBddSize.c.

00259 {
00260   long i;
00261   Cal_BddIndex_t j;
00262   CalHashTable_t *h;
00263   Cal_Bdd_t f;
00264   
00265   /* The number of subfunctions obtainable by restricting the */
00266   /* variables of index < n is the number of subfunctions whose top */
00267   /* variable has index n plus the number of subfunctions obtainable */
00268   /* by restricting the variables of index < n+1 minus the number of */
00269   /* these latter subfunctions whose highest reference is by a node at */
00270   /* level n. */
00271   /* The strategy will be to start with the number of subfunctions */
00272   /* whose top variable has index n.  We compute the highest level at */
00273   /* which each subfunction is referenced.  Then we work bottom up; at */
00274   /* level n we add in the result from level n+1 and subtract the */
00275   /* number of subfunctions whose highest reference is at level n. */
00276 
00277   Cal_BddProfile(bddManager, fUserBdd, funcCounts, 0);
00278   if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
00279     f = CalBddGetInternalBdd(bddManager, fUserBdd);
00280     /* Encode the profile.  The low bit of a count will be zero for */
00281     /* those levels where f actually has a node. */
00282     for(j = 0; j < bddManager->numVars; ++j){
00283       if(!funcCounts[j]){
00284         funcCounts[j] = 1;
00285       }
00286       else{
00287         funcCounts[j] <<= 1;
00288       }
00289     }
00290     h = CalHashTableOneInit(bddManager, sizeof(int));
00291     /* For each subfunction in f, compute the highest level where it is */
00292     /* referenced.  f itself is conceptually referenced at the highest */
00293     /* possible level, which we represent by -1. */
00294     i =  -1;
00295     CalHashTableOneInsert(h, f, (char *)&i);
00296     BddHighestRefStep(bddManager, f, h);
00297     /* Walk through these results.  For each subfunction, decrement the */
00298     /* count at the highest level where it is referenced. */
00299     BddDominatedStep(bddManager, f, funcCounts, h);
00300     CalHashTableOneQuit(h);
00301     /* Now add each level n+1 result to that of level n. */
00302     for(i = bddManager->numVars-1, j = i+1; i>=  0; --i){
00303       if(funcCounts[i] !=  1){
00304         funcCounts[i] = (funcCounts[i] >> 1) + funcCounts[j];
00305         j = i;
00306       }
00307       else{
00308           funcCounts[i] = 0;
00309       }
00310     }
00311   }
00312 }

void Cal_BddFunctionProfileMultiple	(	Cal_BddManager	bddManager,
		Cal_Bdd *	fUserBddArray,
		long *	funcCounts
	)

Function********************************************************************

Synopsis [Returns a "function profile" for fArray.]

Description [optional]

SideEffects [None]

SeeAlso [optional]

Definition at line 326 of file calBddSize.c.

00328 {
00329   long i;
00330   Cal_BddIndex_t j;
00331   Cal_Bdd_t *f, *fArray;
00332   CalHashTable_t *h;
00333 
00334   CalBddArrayPreProcessing(bddManager, fUserBddArray);
00335 
00336   for(i = 0; fUserBddArray[i]; ++i);
00337 
00338   fArray = Cal_MemAlloc(Cal_Bdd_t, i+1);
00339   for (j=0; j < i; j++){
00340     fArray[j] = CalBddGetInternalBdd(bddManager,fUserBddArray[j]);
00341   }
00342   fArray[j] = bddManager->bddNull;
00343 
00344   /* See cmu_bdd_function_profile for the strategy involved here. */
00345   Cal_BddProfileMultiple(bddManager, fUserBddArray, funcCounts, 0);
00346   for(j = 0; j < bddManager->numVars; ++j){
00347     if(!funcCounts[j]){
00348       funcCounts[j] = 1;
00349     }
00350     else{
00351       funcCounts[j] <<= 1;
00352     }
00353   }
00354   h = CalHashTableOneInit(bddManager, sizeof(int));
00355   for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
00356     BddHighestRefStep(bddManager, *f, h);
00357   }
00358   i = -1;
00359   for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
00360     CalHashTableOneInsert(h, *f, (char *)&i);
00361   }
00362   for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
00363     BddDominatedStep(bddManager, *f, funcCounts, h);
00364   }
00365   CalHashTableOneQuit(h);
00366   for(i = bddManager->numVars-1, j = i+1; i >=  0; --i){
00367     if(funcCounts[i] !=  1){
00368       funcCounts[i] = (funcCounts[i] >> 1) + funcCounts[j];
00369       j = i;
00370     }
00371     else{
00372       funcCounts[i] = 0;
00373     }
00374   }
00375   Cal_MemFree(fArray);
00376 }

void Cal_BddProfile	(	Cal_BddManager	bddManager,
		Cal_Bdd	fUserBdd,
		long *	levelCounts,
		int	negout
	)

Function********************************************************************

Synopsis [Returns a "node profile" of f, i.e., the number of nodes at each level in f.]

Description [negout is as in Cal_BddSize. levelCounts should be an array of size Cal_BddVars(bddManager)+1 to hold the profile.]

SideEffects [None]

SeeAlso [optional]

Definition at line 180 of file calBddSize.c.

00182 {
00183   Cal_BddIndex_t i;
00184   Cal_Bdd_t f, g;
00185   if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
00186     f = CalBddGetInternalBdd(bddManager, fUserBdd);
00187     for(i = 0; i <=  bddManager->numVars; i++){
00188       levelCounts[i] = 0l;
00189     }
00190     g = CalBddOne(bddManager);
00191     CalBddPutMark(g, 0);
00192     BddMarkBdd(f);
00193     BddProfileStep(bddManager, f, levelCounts, countingFns[!negout]);
00194   }
00195 }

void Cal_BddProfileMultiple	(	Cal_BddManager	bddManager,
		Cal_Bdd *	fUserBddArray,
		long *	levelCounts,
		int	negout
	)

Function********************************************************************

Synopsis []

Description [optional]

SideEffects [None]

SeeAlso [optional]

Definition at line 210 of file calBddSize.c.

00212 {
00213   Cal_Bdd_t *f, *fArray;
00214   Cal_Bdd_t g;
00215   int i, j;
00216   
00217   CalBddArrayPreProcessing(bddManager, fUserBddArray);
00218 
00219   for(i = 0; fUserBddArray[i]; ++i);
00220 
00221   fArray = Cal_MemAlloc(Cal_Bdd_t, i+1);
00222   for (j=0; j < i; j++){
00223     fArray[j] = CalBddGetInternalBdd(bddManager,fUserBddArray[j]);
00224   }
00225   fArray[j] = bddManager->bddNull;
00226     
00227   for(i = 0; i <=  bddManager->numVars; i++){
00228     levelCounts[i] = 0l;
00229   }
00230   g = CalBddOne(bddManager);
00231   CalBddPutMark(g, 0);
00232   for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
00233     BddMarkBdd(*f);
00234   }
00235   for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
00236     BddProfileStep(bddManager, *f, levelCounts, countingFns[!negout]);
00237   }
00238   Cal_MemFree(fArray);
00239 }

long Cal_BddSize	(	Cal_BddManager	bddManager,
		Cal_Bdd	fUserBdd,
		int	negout
	)

Function********************************************************************

Synopsis [Returns the number of nodes in f when negout is nonzero. If negout is zero, we pretend that the BDDs don't have negative-output pointers.]

Description [optional]

SideEffects [None]

SeeAlso [optional]

Definition at line 104 of file calBddSize.c.

00105 {
00106   Cal_Bdd_t f, g;
00107 
00108   if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
00109     f = CalBddGetInternalBdd(bddManager, fUserBdd);
00110     g =  CalBddOne(bddManager);
00111     CalBddPutMark(g, 0);
00112     BddMarkBdd(f);
00113     return BddSizeStep(f, countingFns[!negout]);
00114   }
00115   return (0l);
00116 }

long Cal_BddSizeMultiple	(	Cal_BddManager	bddManager,
		Cal_Bdd *	fUserBddArray,
		int	negout
	)

Function********************************************************************

Synopsis [The routine is like Cal_BddSize, but takes a null-terminated array of BDDs and accounts for sharing of nodes.]

Description [optional]

SideEffects [None]

SeeAlso [optional]

Definition at line 132 of file calBddSize.c.

00134 {
00135   long size;
00136   Cal_Bdd_t *f;
00137   Cal_Bdd_t g;
00138   Cal_Bdd_t *fArray;
00139   int i, j;
00140   
00141   if (CalBddArrayPreProcessing(bddManager, fUserBddArray) == 0){
00142     return -1;
00143   }
00144   
00145   for(i = 0; fUserBddArray[i]; ++i);
00146 
00147   fArray = Cal_MemAlloc(Cal_Bdd_t, i+1);
00148   for (j=0; j < i; j++){
00149     fArray[j] = CalBddGetInternalBdd(bddManager,fUserBddArray[j]);
00150   }
00151   fArray[j] = bddManager->bddNull;
00152   
00153   g  =  CalBddOne(bddManager);
00154   CalBddPutMark(g, 0);
00155   for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
00156     BddMarkBdd(*f);
00157   }
00158   size  =  0l;
00159   for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
00160     size +=  BddSizeStep(*f, countingFns[!negout]);
00161   }
00162   Cal_MemFree(fArray);
00163   return size;
00164 }

static int countingFns ( Cal_Bdd_t ) [static]

AutomaticEnd

src/calBdd/calBddSize.c File Reference

Typedefs

Functions

Typedef Documentation

Function Documentation