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

/**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 $]

******************************************************************************/
#include "calInt.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/
typedef int (*CountFn_t)(Cal_Bdd_t);

/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

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);

/**AutomaticEnd***************************************************************/

static
int (*(countingFns[]))(Cal_Bdd_t) = 
{
  BddCountNoNodes,
  BddCountNodes,
};

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

/**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]

******************************************************************************/
long
Cal_BddSize(Cal_BddManager bddManager, Cal_Bdd fUserBdd, int  negout)
{
  Cal_Bdd_t f, g;

  if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
    f = CalBddGetInternalBdd(bddManager, fUserBdd);
    g =  CalBddOne(bddManager);
    CalBddPutMark(g, 0);
    BddMarkBdd(f);
    return BddSizeStep(f, countingFns[!negout]);
  }
  return (0l);
}


/**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]

******************************************************************************/
long
Cal_BddSizeMultiple(Cal_BddManager bddManager, Cal_Bdd *fUserBddArray,
                    int  negout)
{
  long size;
  Cal_Bdd_t *f;
  Cal_Bdd_t g;
  Cal_Bdd_t *fArray;
  int i, j;
  
  if (CalBddArrayPreProcessing(bddManager, fUserBddArray) == 0){
    return -1;
  }
  
  for(i = 0; fUserBddArray[i]; ++i);

  fArray = Cal_MemAlloc(Cal_Bdd_t, i+1);
  for (j=0; j < i; j++){
    fArray[j] = CalBddGetInternalBdd(bddManager,fUserBddArray[j]);
  }
  fArray[j] = bddManager->bddNull;
  
  g  =  CalBddOne(bddManager);
  CalBddPutMark(g, 0);
  for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
    BddMarkBdd(*f);
  }
  size  =  0l;
  for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
    size +=  BddSizeStep(*f, countingFns[!negout]);
  }
  Cal_MemFree(fArray);
  return size;
}

/**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]

******************************************************************************/
void
Cal_BddProfile(Cal_BddManager bddManager, Cal_Bdd fUserBdd,
               long * levelCounts, int  negout)
{
  Cal_BddIndex_t i;
  Cal_Bdd_t f, g;
  if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
    f = CalBddGetInternalBdd(bddManager, fUserBdd);
    for(i = 0; i <=  bddManager->numVars; i++){
      levelCounts[i] = 0l;
    }
    g = CalBddOne(bddManager);
    CalBddPutMark(g, 0);
    BddMarkBdd(f);
    BddProfileStep(bddManager, f, levelCounts, countingFns[!negout]);
  }
}


/**Function********************************************************************

  Synopsis    []

  Description [optional]

  SideEffects [None]

  SeeAlso     [optional]

******************************************************************************/
void
Cal_BddProfileMultiple(Cal_BddManager bddManager, Cal_Bdd *fUserBddArray,
                       long * levelCounts, int  negout)
{
  Cal_Bdd_t *f, *fArray;
  Cal_Bdd_t g;
  int i, j;
  
  CalBddArrayPreProcessing(bddManager, fUserBddArray);

  for(i = 0; fUserBddArray[i]; ++i);

  fArray = Cal_MemAlloc(Cal_Bdd_t, i+1);
  for (j=0; j < i; j++){
    fArray[j] = CalBddGetInternalBdd(bddManager,fUserBddArray[j]);
  }
  fArray[j] = bddManager->bddNull;
    
  for(i = 0; i <=  bddManager->numVars; i++){
    levelCounts[i] = 0l;
  }
  g = CalBddOne(bddManager);
  CalBddPutMark(g, 0);
  for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
    BddMarkBdd(*f);
  }
  for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
    BddProfileStep(bddManager, *f, levelCounts, countingFns[!negout]);
  }
  Cal_MemFree(fArray);
}


/**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]

******************************************************************************/
void
Cal_BddFunctionProfile(Cal_BddManager bddManager, Cal_Bdd fUserBdd,
                       long * funcCounts) 
{
  long i;
  Cal_BddIndex_t j;
  CalHashTable_t *h;
  Cal_Bdd_t f;
  
  /* The number of subfunctions obtainable by restricting the */
  /* variables of index < n is the number of subfunctions whose top */
  /* variable has index n plus the number of subfunctions obtainable */
  /* by restricting the variables of index < n+1 minus the number of */
  /* these latter subfunctions whose highest reference is by a node at */
  /* level n. */
  /* The strategy will be to start with the number of subfunctions */
  /* whose top variable has index n.  We compute the highest level at */
  /* which each subfunction is referenced.  Then we work bottom up; at */
  /* level n we add in the result from level n+1 and subtract the */
  /* number of subfunctions whose highest reference is at level n. */

  Cal_BddProfile(bddManager, fUserBdd, funcCounts, 0);
  if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
    f = CalBddGetInternalBdd(bddManager, fUserBdd);
    /* Encode the profile.  The low bit of a count will be zero for */
    /* those levels where f actually has a node. */
    for(j = 0; j < bddManager->numVars; ++j){
      if(!funcCounts[j]){
        funcCounts[j] = 1;
      }
      else{
        funcCounts[j] <<= 1;
      }
    }
    h = CalHashTableOneInit(bddManager, sizeof(int));
    /* For each subfunction in f, compute the highest level where it is */
    /* referenced.  f itself is conceptually referenced at the highest */
    /* possible level, which we represent by -1. */
    i =  -1;
    CalHashTableOneInsert(h, f, (char *)&i);
    BddHighestRefStep(bddManager, f, h);
    /* Walk through these results.  For each subfunction, decrement the */
    /* count at the highest level where it is referenced. */
    BddDominatedStep(bddManager, f, funcCounts, h);
    CalHashTableOneQuit(h);
    /* Now add each level n+1 result to that of level n. */
    for(i = bddManager->numVars-1, j = i+1; i>=  0; --i){
      if(funcCounts[i] !=  1){
        funcCounts[i] = (funcCounts[i] >> 1) + funcCounts[j];
        j = i;
      }
      else{
          funcCounts[i] = 0;
      }
    }
  }
}

/**Function********************************************************************

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

  Description [optional]

  SideEffects [None]

  SeeAlso     [optional]

******************************************************************************/
void
Cal_BddFunctionProfileMultiple(Cal_BddManager bddManager, Cal_Bdd
                               *fUserBddArray, long * funcCounts)
{
  long i;
  Cal_BddIndex_t j;
  Cal_Bdd_t *f, *fArray;
  CalHashTable_t *h;

  CalBddArrayPreProcessing(bddManager, fUserBddArray);

  for(i = 0; fUserBddArray[i]; ++i);

  fArray = Cal_MemAlloc(Cal_Bdd_t, i+1);
  for (j=0; j < i; j++){
    fArray[j] = CalBddGetInternalBdd(bddManager,fUserBddArray[j]);
  }
  fArray[j] = bddManager->bddNull;

  /* See cmu_bdd_function_profile for the strategy involved here. */
  Cal_BddProfileMultiple(bddManager, fUserBddArray, funcCounts, 0);
  for(j = 0; j < bddManager->numVars; ++j){
    if(!funcCounts[j]){
      funcCounts[j] = 1;
    }
    else{
      funcCounts[j] <<= 1;
    }
  }
  h = CalHashTableOneInit(bddManager, sizeof(int));
  for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
    BddHighestRefStep(bddManager, *f, h);
  }
  i = -1;
  for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
    CalHashTableOneInsert(h, *f, (char *)&i);
  }
  for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
    BddDominatedStep(bddManager, *f, funcCounts, h);
  }
  CalHashTableOneQuit(h);
  for(i = bddManager->numVars-1, j = i+1; i >=  0; --i){
    if(funcCounts[i] !=  1){
      funcCounts[i] = (funcCounts[i] >> 1) + funcCounts[j];
      j = i;
    }
    else{
      funcCounts[i] = 0;
    }
  }
  Cal_MemFree(fArray);
}

/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


/**Function********************************************************************

  Synopsis    []

  Description [optional]

  SideEffects [required]

  SeeAlso     [optional]

******************************************************************************/
static void
BddMarkBdd(Cal_Bdd_t  f)
{
  int currMarking, thisMarking;
  Cal_Bdd_t thenBdd, elseBdd;

  currMarking = CalBddGetMark(f);
  thisMarking = (1 << CalBddIsComplement(f));
  if(currMarking & thisMarking){
    return;
  }
  CalBddPutMark(f, currMarking | thisMarking);
  if(CalBddIsBddConst(f)){
    return;
  }
  CalBddGetThenBdd(f, thenBdd);
  BddMarkBdd(thenBdd);
  CalBddGetElseBdd(f, elseBdd);
  BddMarkBdd(elseBdd);
}


/**Function********************************************************************

  Synopsis    []

  Description [optional]

  SideEffects [required]

  SeeAlso     [optional]

******************************************************************************/
static int
BddCountNoNodes(
  Cal_Bdd_t  f)
{
  return (CalBddGetMark(f) > 0);
}


/**Function********************************************************************

  Synopsis    []

  Description [optional]

  SideEffects [required]

  SeeAlso     [optional]

******************************************************************************/
static int
BddCountNodes(
  Cal_Bdd_t  f)
{
  int mark;

  mark = CalBddGetMark(f);
  return (((mark & 0x1) !=  0) + ((mark & 0x2) !=  0));
}



/**Function********************************************************************

  Synopsis    []

  Description [optional]

  SideEffects [required]

  SeeAlso     [optional]

******************************************************************************/
static long
BddSizeStep(
  Cal_Bdd_t  f,
  CountFn_t countFn)
{
  long result;
  Cal_Bdd_t thenBdd, elseBdd;

  if(!CalBddGetMark(f)){
    return (0l);
  }
  result = (*countFn)(f);
  if(!CalBddIsBddConst(f)){
    CalBddGetThenBdd(f, thenBdd);
    CalBddGetElseBdd(f, elseBdd);
    result +=
        BddSizeStep(thenBdd, countFn) +
        BddSizeStep(elseBdd, countFn);
  }
  CalBddPutMark(f, 0);
  return result;
}



/**Function********************************************************************

  Synopsis    []

  Description [optional]

  SideEffects [required]

  SeeAlso     [optional]

******************************************************************************/
static void
BddProfileStep(
  Cal_BddManager_t * bddManager,
  Cal_Bdd_t  f,
  long * levelCounts,
  CountFn_t countFn)
{
  Cal_Bdd_t thenBdd, elseBdd;
  if(!CalBddGetMark(f)){
    return;
  }
  if(CalBddIsBddConst(f)){
    levelCounts[bddManager->numVars] += (*countFn)(f);
  }
  else{
    levelCounts[CalBddGetBddIndex(bddManager, f)] += (*countFn)(f);
    CalBddGetThenBdd(f, thenBdd);
    BddProfileStep(bddManager, thenBdd, levelCounts, countFn);
    CalBddGetElseBdd(f, elseBdd);
    BddProfileStep(bddManager, elseBdd, levelCounts, countFn);
  }
  CalBddPutMark(f, 0);
}



/**Function********************************************************************

  Synopsis    []

  Description [optional]

  SideEffects [required]

  SeeAlso     [optional]

******************************************************************************/
static void
BddHighestRefStep(
  Cal_BddManager_t * bddManager,
  Cal_Bdd_t  f,
  CalHashTable_t * h)
{
  int fIndex;
  Cal_Bdd_t keyBdd;
  int *dataPtr;

  if(CalBddIsBddConst(f)){
    return;
  }
  fIndex = CalBddGetBddIndex(bddManager, f);
  CalBddGetThenBdd(f, keyBdd);
  if(CalHashTableOneLookup(h, keyBdd, (char **)&dataPtr)){
    if(*dataPtr > fIndex){
      *dataPtr = fIndex;
    }
  }
  else{
    CalHashTableOneInsert(h, keyBdd, (char *)&fIndex);
    BddHighestRefStep(bddManager, keyBdd, h);
  }
  CalBddGetElseBdd(f, keyBdd);
  if(CalHashTableOneLookup(h, keyBdd, (char **)&dataPtr)){
    if(*dataPtr > fIndex){
      *dataPtr = fIndex;
    }
  }
  else{
    CalHashTableOneInsert(h, keyBdd, (char *)&fIndex);
    BddHighestRefStep(bddManager, keyBdd, h);
  }
}

/**Function********************************************************************

  Synopsis    []

  Description [optional]

  SideEffects [required]

  SeeAlso     [optional]

******************************************************************************/
static void
BddDominatedStep(
  Cal_BddManager_t * bddManager,
  Cal_Bdd_t  f,
  long * funcCounts,
  CalHashTable_t * h)
{
  Cal_Bdd_t thenBdd, elseBdd;
  int *dataPtr;

  CalHashTableOneLookup(h, f, (char **)&dataPtr);
  if(*dataPtr >=  0)
    funcCounts[*dataPtr] -= 2;
  if(*dataPtr > -2){
    *dataPtr = -2;
    if(!CalBddIsBddConst(f)){
      CalBddGetThenBdd(f, thenBdd);
      BddDominatedStep(bddManager, thenBdd, funcCounts, h);
      CalBddGetElseBdd(f, elseBdd);
      BddDominatedStep(bddManager, elseBdd, funcCounts, h);
    }
  }
}