src/res/resSmartVarUse.c

Go to the documentation of this file.

#include "resInt.h" 
#include "var_set.h"

static char rcsid[] UNUSED = "$Id: resSmartVarUse.c,v 1.15 2002/09/08 23:56:11 fabio Exp $";

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

#define DEFAULT_NUMBER_OF_VARIABLES (sizeof(int)*16)
#define ELEMENTS_PER_WORD (sizeof(int)<<3)

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/


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

static var_set_t *idSet = NIL(var_set_t);
static int numVarsInUse = 0;

/*--------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/
/* based on the fact that var set word size = ELEMENTS_PER_WORD */
#define MaxSizeOfSet(set) ((set)->n_words * ELEMENTS_PER_WORD)

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

static var_set_t * InitializeVariableManager(int numOfVars);
static void ResizeVariableManager(int newSize);

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

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

void
MddCreateVariables(mdd_manager *mgr,     
                   int numVarsToBeAdded) 
{
    array_t *mvar_values;
    array_t *mvar_names = NIL(array_t);
    array_t *mvar_strides = NIL(array_t);
    int i, two_values;

    if (numVarsToBeAdded <= 0) return;
    
    /* Create 2 mvar values 0,1 */
    mvar_values = array_alloc(int, numVarsToBeAdded);    

    /* Assume we create only Bdd variables here */
    two_values = 2;
    for(i = 0; i < numVarsToBeAdded; i++) {
      array_insert(int, mvar_values, i, two_values);
    }

    /* creates the mdd variables and updates the mvar_list field */
    mdd_create_variables(mgr, mvar_values, mvar_names, mvar_strides);
    
    array_free(mvar_values);

} /* End of MddCreateVariables */

int *
ResResidueVarAllocate(bdd_manager *ddManager,  
                         lsList orderList,   
                         array_t *newIdArray)
{
  lsGen listGen;             /* generator to step through a list of nodes */
  Ntk_Node_t *nodePtr;       /* variable to store node pointer */
  int nodeId;                /* mdd id of a node */
  char *flagValue;           /* string to store flag value */
  int newVarsRequired;       /* number of new variables required by layer */
  int verbose;               /* verbosity value */
  var_set_t *assignedSet;    /* var_set of assigned  Ids in this layer */
  var_set_t *idsNotInList;   /* set of assigned Ids not in layer or fanin */
  var_set_t *notAssignedSet; /* var_set of Ids not in this layer */
  int *invPermArray;         /* inverse permutation array for shuffle */
  int invPermIndex, newIdIndex;  /* iterators */
  int i, j, id;              /* iterators */
  int holes;                  /* number of holes filled so far */
  int lastDdId;              /* last variable in dd manager before expansion */
  int numberOfFreeVars;      /* number of free variables */

  /* read verbosity flag */
  verbose = 0;
  flagValue = Cmd_FlagReadByName("residue_verbosity");
  if (flagValue != NIL(char)) {
    verbose = atoi(flagValue);
  }
  /* no work required */
  if (!lsLength(orderList)) {
    error_append("Something wrong order list is empty \n");
    return NIL(int);
  }

  /* if manager not yet initialized, initialize here */
  if (idSet == NIL(var_set_t)) {
    ResResidueInitializeVariableManager(lsLength(orderList));
  }

  /* number of nodes with unassigned Ids */
  newVarsRequired = 0;

  /* for output nodes list, ids are assigned, just set them in the
   * var set
   */
  if (var_set_is_empty(idSet)) {
    invPermArray = ALLOC(int, bdd_num_vars(ddManager));
    for (i = 0; (unsigned) i < bdd_num_vars(ddManager); i++) {
      invPermArray[i] = bdd_get_id_from_level(ddManager, i);
    }  
    invPermIndex = 0;
    lsForEachItem(orderList, listGen, nodePtr) {
      nodeId = Ntk_NodeReadMddId(nodePtr);
      assert(nodeId != NTK_UNASSIGNED_MDD_ID);
      /* mark output node mdd id as in use */
      var_set_set_elt(idSet, nodeId);
      /* increase number of variables in use */
      numVarsInUse++;
      invPermArray[invPermIndex] = nodeId;
      invPermArray[nodeId] = invPermIndex;
      invPermIndex++;
    }
    return(invPermArray);
  }

  /* create a set for already assigned Ids */
  assignedSet = var_set_new(MaxSizeOfSet(idSet));

  /* for each item in the list, check against the set if Id
   * is assigned. Also create a set to isolate assigned Ids
   * that are not in the list. If unassigned Id, increment
   * new variables
   */
  lsForEachItem(orderList, listGen, nodePtr) {
    nodeId = Ntk_NodeReadMddId(nodePtr);
    if (nodeId != NTK_UNASSIGNED_MDD_ID) {
      assert(var_set_get_elt(idSet, nodeId) == 1);
      /* create a var set with assigned ids in list */
      var_set_set_elt(assignedSet, nodeId);
    } else {
      newVarsRequired++;
    }
  }
  
  /* find out from the set, the assigned Ids which are not in
   * this list
   */
  idsNotInList = var_set_new(MaxSizeOfSet(idSet));
  
  /* do the operation idSet - assignedSet */
  notAssignedSet = var_set_new(MaxSizeOfSet(idSet));
  notAssignedSet = var_set_not(notAssignedSet, assignedSet);
  idsNotInList = var_set_and(idsNotInList, notAssignedSet, idSet);
  var_set_free(assignedSet);
  var_set_free(notAssignedSet);
  
  
  /* initialize return value */
  if (newVarsRequired) {
    
    if (verbose >= 3) {
      fprintf(vis_stdout, "Number of new variables to be assigned = %d\n",
              newVarsRequired);
    }
    /* compute number of free variables available in the manager */
    numberOfFreeVars = MaxSizeOfSet(idSet) - numVarsInUse;

    /* if too few free variables available, resize manager */
    if (numberOfFreeVars < newVarsRequired) {
      ResizeVariableManager(numVarsInUse + newVarsRequired);
    }

    invPermArray = ALLOC(int, bdd_num_vars(ddManager));
    /* fill the inverse permutation array */
    for (i = 0; (unsigned) i < bdd_num_vars(ddManager); i++) {
      invPermArray[i] = bdd_get_id_from_level(ddManager, i);
    }
    /* create the array of new ids ; assign them starting from the
     * top(in position) available ID
     */
    /* number of available ids in the variable manager */
    holes = 0;
    /* There could be two cases here: the number of new vars required
     * are filled by holes or new variables are required in the DD
     * manager to fill the requirement
     */
    
    /* assign as many new Ids as required by the list */
    for (i = 0; ((unsigned) i < bdd_num_vars(ddManager)) && (holes < newVarsRequired); i++) {
      /* done when holes fill the new variable requirements or when
       * new variables are needed in the ddManager
       */
      if (!var_set_get_elt(idSet, invPermArray[i])) {
        /* the number of holes filled above are the variables that exist in
         * the ddManager and are not in use
         */
        array_insert_last(int , newIdArray, invPermArray[i]);
        holes++;
      }
    }
    FREE(invPermArray);
    if (verbose >= 4) {
      if (holes) {
        fprintf(vis_stdout, "Holes filled are ids:");
        arrayForEachItem(int, newIdArray, i, nodeId) {
          fprintf(vis_stdout, "%d ", nodeId);
        }
        fprintf(vis_stdout, "\n");
      }
    }

    
    /* newVarsRequired-holes is the number of variables to be added to the
     * mdd manager
     */
    if (holes < newVarsRequired) {
      lastDdId = bdd_num_vars(ddManager);
      /* create mdd variables, dirty stuff needed to add to the mvar_list */
      MddCreateVariables((mdd_manager *)ddManager, newVarsRequired - holes);
      
      /* since all the variables were created in the end, use the ids
       * starting at the size of the manager
       */
      for(i = 0; i < (newVarsRequired-holes); i++) {
        array_insert_last(int, newIdArray, lastDdId+i);
      }
      if (verbose >= 4) {
        fprintf(vis_stdout, "New dd ids assigned are: ");
        for(i = 0; i < (newVarsRequired-holes); i++) {
          fprintf(vis_stdout, "%d ", array_fetch(int, newIdArray, holes+i));
        } 
        fprintf(vis_stdout, "\n");
      }
    } /* end of new vars needed to be assigned in the manager */
  } /* end of new vars need to be assigned to nodes */

  /* Create Inverse Permutation Array for the DD Manager */
  
  /* create inverse permutation array with nodes in list */ 
  invPermArray = ALLOC(int, bdd_num_vars(ddManager));
  invPermIndex = 0;
  newIdIndex = 0;
  if (verbose >= 4) {
    fprintf(vis_stdout, "Final order to shuffle heap is:\n");
  }
  lsForEachItem(orderList, listGen, nodePtr) {
    /* for nodes with assigned ids, get id from node */
    nodeId = Ntk_NodeReadMddId(nodePtr);
    if (nodeId == NTK_UNASSIGNED_MDD_ID) {
      /* for nodes with unassigned ids, get id from array */
      nodeId = array_fetch(int, newIdArray, newIdIndex);
      /* update var set with teh new ids added */
      var_set_set_elt(idSet, nodeId);
      numVarsInUse++;
      newIdIndex++;
    }
    invPermArray[invPermIndex] = nodeId;
    if (verbose >= 4) {
      fprintf(vis_stdout, "%d ", nodeId);
    }
    invPermIndex++;
  }
  /* all new ids been accounted for */
  assert(newIdIndex == array_n(newIdArray));

  /* push nodes  not in list with assigned Ids below those in list */
  /* fill inv Perm array with Ids that are not in the list
   * and not in the idsNotInList. These are ids in the
   * ddManager that are not in idSet. 
   */
  /* if the number of ids in use in residue verification is less
   * than that in the manager
   */
  if (((unsigned) invPermIndex < bdd_num_vars(ddManager)) ||
      (!var_set_is_empty(idsNotInList))) {

    /* collect the ids that are not in use in residue verification */
    for (j = 0; (unsigned) j < bdd_num_vars(ddManager); j++) {
      /* if not idSet, it means that it is not in use by
       * residue verification, hence add to the end of invpermArray.
       * Get id from the invPermArray that was filled in the
       * above lines(where invPermArray was copied in the manager).
       * Nodes already in the list will not get added since idSet
       * was updated as the list was read. The id is read from the
       * invPermArray so as to not disturb the relative order of
       * the ids not in use and those in the manager. The check
       * has the additional clause on the id <
       * MaxSizeOfSet(idsNotInList)since idsNotInList was created
       * before the additional variables were added to the manager.
       */
      id = bdd_get_id_from_level(ddManager, j);
      if ((!var_set_get_elt(idSet, id)) ||
           (((unsigned) id < MaxSizeOfSet(idsNotInList)) &&
            (var_set_get_elt(idsNotInList, id)))) {
        /* add to the inverse permutation array */
        invPermArray[invPermIndex] = id;
        if (verbose >= 4) {
          fprintf(vis_stdout, "%d ", id);
        }
        invPermIndex++;
      } /* end of if not in idSet */
    } /* end of iterating through the ids in the dd manager */
  } /* end of if */ 
  if (verbose >= 4) {
    fprintf(vis_stdout, "\n");
  }

  var_set_free(idsNotInList);
  assert(invPermIndex == bdd_num_vars(ddManager));
  
  return(invPermArray);
}/* End of ResResidueVarAllocate */

void
ResResidueVarDeallocate(array_t *currentLayer)
{
  int i=0;
  int nodeId;
  Ntk_Node_t *nodePtr;
  
  LayerForEachNode(currentLayer, i, nodePtr) {
    nodeId = Ntk_NodeReadMddId(nodePtr);
    var_set_clear_elt(idSet, nodeId);
    numVarsInUse--;
  }

  return;
} /* End of Res_ResidueVarUseDeallocate */

void
ResResidueFreeVariableManager(void)
{

  if (idSet == NIL(var_set_t)) {
    return;
  } /* End of if */

  numVarsInUse = 0;
  var_set_free(idSet);

  idSet = NIL(var_set_t);

  return;
} /* End of ResResidueFreeVariableManager */

void
ResResidueInitializeVariableManager(int numOfVars)
{
  idSet = InitializeVariableManager(numOfVars);
  return;
} /* End of ResResidueInitializeVariableManager */


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

static var_set_t *
InitializeVariableManager(int numOfVars)
{
  if (numOfVars != 0) {
    if (numOfVars % ELEMENTS_PER_WORD != 0) {
      /* round up to the next word length */
      numOfVars = ((numOfVars/ELEMENTS_PER_WORD)+1)*ELEMENTS_PER_WORD;
    } 
  } else {
    numOfVars = DEFAULT_NUMBER_OF_VARIABLES;
  }

  /* default value of number of words = 2 */
  return var_set_new(numOfVars);

} /* End of InitializeVariableManager */

static void
ResizeVariableManager(int newSize)
{
  var_set_t *newSet;
  int i;

  /* resize only if the new size is larger than the previous size */
  assert(newSize > MaxSizeOfSet(idSet));

  /* create a new set with the new size */
  newSet = InitializeVariableManager(newSize);
  
  for (i=0; i < idSet->n_words; i++) {
    newSet->data[i] |= idSet->data[i];
  }
  /* free the old id set, not using ResResidueFreeVariableManager()
   * because it resets the numVarsInUse
   */
  var_set_free(idSet);

  idSet = newSet;
  return;
} /* End of ResizeVariableManager */