cuddzddgroup.c

主要进行大规模的电路综合

/**CFile***********************************************************************

  FileName    [cuddZddGroup.c]

  PackageName [cudd]

  Synopsis    [Functions for ZDD group sifting.]

  Description [External procedures included in this file:
		<ul>
		<li> Cudd_MakeZddTreeNode()
		</ul>
	Internal procedures included in this file:
		<ul>
		<li> cuddZddTreeSifting()
		</ul>
	Static procedures included in this module:
		<ul>
		<li> zddTreeSiftingAux()
		<li> zddCountInternalMtrNodes()
		<li> zddReorderChildren()
		<li> zddFindNodeHiLo()
		<li> zddUniqueCompareGroup()
		<li> zddGroupSifting()
		<li> zddGroupSiftingAux()
		<li> zddGroupSiftingUp()
		<li> zddGroupSiftingDown()
		<li> zddGroupMove()
		<li> zddGroupMoveBackward()
		<li> zddGroupSiftingBackward()
		<li> zddMergeGroups()
		</ul>]

  Author      [Fabio Somenzi]

  Copyright   [This file was created at the University of Colorado at
  Boulder.  The University of Colorado at Boulder makes no warranty
  about the suitability of this software for any purpose.  It is
  presented on an AS IS basis.]

******************************************************************************/

#include "util.h"
#include "cuddInt.h"

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

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

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

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

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddZddGroup.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $";
#endif

static	int	*entry;
extern	int	zddTotalNumberSwapping;
#ifdef DD_STATS
static  int     extsymmcalls;
static  int     extsymm;
static  int     secdiffcalls;
static  int     secdiff;
static  int     secdiffmisfire;
#endif
#ifdef DD_DEBUG
static	int	pr = 0;	/* flag to enable printing while debugging */
			/* by depositing a 1 into it */
#endif

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

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

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

static int zddTreeSiftingAux ARGS((DdManager *table, MtrNode *treenode, Cudd_ReorderingType method));
#ifdef DD_STATS
static int zddCountInternalMtrNodes ARGS((DdManager *table, MtrNode *treenode));
#endif
static int zddReorderChildren ARGS((DdManager *table, MtrNode *treenode, Cudd_ReorderingType method));
static void zddFindNodeHiLo ARGS((DdManager *table, MtrNode *treenode, int *lower, int *upper));
static int zddUniqueCompareGroup ARGS((int *ptrX, int *ptrY));
static int zddGroupSifting ARGS((DdManager *table, int lower, int upper));
static int zddGroupSiftingAux ARGS((DdManager *table, int x, int xLow, int xHigh));
static int zddGroupSiftingUp ARGS((DdManager *table, int y, int xLow, Move **moves));
static int zddGroupSiftingDown ARGS((DdManager *table, int x, int xHigh, Move **moves));
static int zddGroupMove ARGS((DdManager *table, int x, int y, Move **moves));
static int zddGroupMoveBackward ARGS((DdManager *table, int x, int y));
static int zddGroupSiftingBackward ARGS((DdManager *table, Move *moves, int size));
static void zddMergeGroups ARGS((DdManager *table, MtrNode *treenode, int low, int high));

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


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


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

  Synopsis    [Creates a new ZDD variable group.]

  Description [Creates a new ZDD variable group. The group starts at
  variable and contains size variables. The parameter low is the index
  of the first variable. If the variable already exists, its current
  position in the order is known to the manager. If the variable does
  not exist yet, the position is assumed to be the same as the index.
  The group tree is created if it does not exist yet.
  Returns a pointer to the group if successful; NULL otherwise.]

  SideEffects [The ZDD variable tree is changed.]

  SeeAlso     [Cudd_MakeTreeNode]

******************************************************************************/
MtrNode *
Cudd_MakeZddTreeNode(
  DdManager * dd /* manager */,
  unsigned int  low /* index of the first group variable */,
  unsigned int  size /* number of variables in the group */,
  unsigned int  type /* MTR_DEFAULT or MTR_FIXED */)
{
    MtrNode *group;
    MtrNode *tree;
    unsigned int level;

    /* If the variable does not exist yet, the position is assumed to be
    ** the same as the index. Therefore, applications that rely on
    ** Cudd_bddNewVarAtLevel or Cudd_addNewVarAtLevel to create new
    ** variables have to create the variables before they group them.
    */
    level = (low < (unsigned int) dd->sizeZ) ? dd->permZ[low] : low;

    if (level + size - 1> (int) MTR_MAXHIGH)
	return(NULL);

    /* If the tree does not exist yet, create it. */
    tree = dd->treeZ;
    if (tree == NULL) {
	dd->treeZ = tree = Mtr_InitGroupTree(0, dd->sizeZ);
	if (tree == NULL)
	    return(NULL);
	tree->index = dd->invpermZ[0];
    }

    /* Extend the upper bound of the tree if necessary. This allows the
    ** application to create groups even before the variables are created.
    */
    tree->size = ddMax(tree->size, level + size);

    /* Create the group. */
    group = Mtr_MakeGroup(tree, level, size, type);
    if (group == NULL)
	return(NULL);

    /* Initialize the index field to the index of the variable currently
    ** in position low. This field will be updated by the reordering
    ** procedure to provide a handle to the group once it has been moved.
    */
    group->index = (MtrHalfWord) low;

    return(group);

} /* end of Cudd_MakeZddTreeNode */


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


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

  Synopsis    [Tree sifting algorithm for ZDDs.]

  Description [Tree sifting algorithm for ZDDs. Assumes that a tree
  representing a group hierarchy is passed as a parameter. It then
  reorders each group in postorder fashion by calling
  zddTreeSiftingAux.  Assumes that no dead nodes are present.  Returns
  1 if successful; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
int
cuddZddTreeSifting(
  DdManager * table /* DD table */,
  Cudd_ReorderingType method /* reordering method for the groups of leaves */)
{
    int i;
    int nvars;
    int result;
    int tempTree;

    /* If no tree is provided we create a temporary one in which all
    ** variables are in a single group. After reordering this tree is
    ** destroyed.
    */
    tempTree = table->treeZ == NULL;
    if (tempTree) {
	table->treeZ = Mtr_InitGroupTree(0,table->sizeZ);
	table->treeZ->index = table->invpermZ[0];
    }
    nvars = table->sizeZ;

#ifdef DD_DEBUG
    if (pr > 0 && !tempTree)
	(void) fprintf(table->out,"cuddZddTreeSifting:");
    Mtr_PrintGroups(table->treeZ,pr <= 0);
#endif
#if 0
    /* Debugging code. */
    if (table->tree && table->treeZ) {
	(void) fprintf(table->out,"\n");
	Mtr_PrintGroups(table->tree, 0);
	cuddPrintVarGroups(table,table->tree,0,0);
	for (i = 0; i < table->size; i++) {
	    (void) fprintf(table->out,"%s%d",
			   (i == 0) ? "" : ",", table->invperm[i]);
	}
	(void) fprintf(table->out,"\n");
	for (i = 0; i < table->size; i++) {
	    (void) fprintf(table->out,"%s%d",
			   (i == 0) ? "" : ",", table->perm[i]);
	}
	(void) fprintf(table->out,"\n\n");
	Mtr_PrintGroups(table->treeZ,0);
	cuddPrintVarGroups(table,table->treeZ,1,0);
	for (i = 0; i < table->sizeZ; i++) {
	    (void) fprintf(table->out,"%s%d",
			   (i == 0) ? "" : ",", table->invpermZ[i]);
	}
	(void) fprintf(table->out,"\n");
	for (i = 0; i < table->sizeZ; i++) {
	    (void) fprintf(table->out,"%s%d",
			   (i == 0) ? "" : ",", table->permZ[i]);
	}
	(void) fprintf(table->out,"\n");
    }
    /* End of debugging code. */
#endif
#ifdef DD_STATS
    extsymmcalls = 0;
    extsymm = 0;
    secdiffcalls = 0;
    secdiff = 0;
    secdiffmisfire = 0;

    (void) fprintf(table->out,"\n");
    if (!tempTree)
	(void) fprintf(table->out,"#:IM_NODES  %8d: group tree nodes\n",
		       zddCountInternalMtrNodes(table,table->treeZ));
#endif

    /* Initialize the group of each subtable to itself. Initially
    ** there are no groups. Groups are created according to the tree
    ** structure in postorder fashion.
    */
    for (i = 0; i < nvars; i++)
        table->subtableZ[i].next = i;

    /* Reorder. */
    result = zddTreeSiftingAux(table, table->treeZ, method);

#ifdef DD_STATS		/* print stats */
    if (!tempTree && method == CUDD_REORDER_GROUP_SIFT &&
	(table->groupcheck == CUDD_GROUP_CHECK7 ||
	 table->groupcheck == CUDD_GROUP_CHECK5)) {
	(void) fprintf(table->out,"\nextsymmcalls = %d\n",extsymmcalls);
	(void) fprintf(table->out,"extsymm = %d",extsymm);
    }
    if (!tempTree && method == CUDD_REORDER_GROUP_SIFT &&
	table->groupcheck == CUDD_GROUP_CHECK7) {
	(void) fprintf(table->out,"\nsecdiffcalls = %d\n",secdiffcalls);
	(void) fprintf(table->out,"secdiff = %d\n",secdiff);
	(void) fprintf(table->out,"secdiffmisfire = %d",secdiffmisfire);
    }
#endif

    if (tempTree)
	Cudd_FreeZddTree(table);
    return(result);

} /* end of cuddZddTreeSifting */


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


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

  Synopsis    [Visits the group tree and reorders each group.]

  Description [Recursively visits the group tree and reorders each
  group in postorder fashion.  Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
static int
zddTreeSiftingAux(
  DdManager * table,
  MtrNode * treenode,
  Cudd_ReorderingType method)
{
    MtrNode  *auxnode;
    int res;

#ifdef DD_DEBUG
    Mtr_PrintGroups(treenode,1);
#endif

    auxnode = treenode;
    while (auxnode != NULL) {
	if (auxnode->child != NULL) {
	    if (!zddTreeSiftingAux(table, auxnode->child, method))
		return(0);
	    res = zddReorderChildren(table, auxnode, CUDD_REORDER_GROUP_SIFT);
	    if (res == 0)
		return(0);
	} else if (auxnode->size > 1) {
	    if (!zddReorderChildren(table, auxnode, method))
		return(0);
	}
	auxnode = auxnode->younger;
    }

    return(1);

} /* end of zddTreeSiftingAux */


#ifdef DD_STATS
/**Function********************************************************************

  Synopsis    [Counts the number of internal nodes of the group tree.]

  Description [Counts the number of internal nodes of the group tree.
  Returns the count.]

  SideEffects [None]

******************************************************************************/
static int
zddCountInternalMtrNodes(
  DdManager * table,
  MtrNode * treenode)
{
    MtrNode *auxnode;
    int     count,nodeCount;


    nodeCount = 0;
    auxnode = treenode;
    while (auxnode != NULL) {
	if (!(MTR_TEST(auxnode,MTR_TERMINAL))) {
	    nodeCount++;
	    count = zddCountInternalMtrNodes(table,auxnode->child);
	    nodeCount += count;
	}
	auxnode = auxnode->younger;
    }

    return(nodeCount);

} /* end of zddCountInternalMtrNodes */
#endif


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

  Synopsis    [Reorders the children of a group tree node according to
  the options.]

  Description [Reorders the children of a group tree node according to
  the options. After reordering puts all the variables in the group
  and/or its descendents in a single group. This allows hierarchical
  reordering.  If the variables in the group do not exist yet, simply
  does nothing. Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

******************************************************************************/
static int
zddReorderChildren(
  DdManager * table,
  MtrNode * treenode,
  Cudd_ReorderingType method)
{
    int lower;
    int upper;
    int result;
    unsigned int initialSize;

    zddFindNodeHiLo(table,treenode,&lower,&upper);
    /* If upper == -1 these variables do not exist yet. */
    if (upper == -1)
	return(1);

    if (treenode->flags == MTR_FIXED) {
	result = 1;
    } else {
#ifdef DD_STATS
	(void) fprintf(table->out," ");
#endif
	switch (method) {
	case CUDD_REORDER_RANDOM:
	case CUDD_REORDER_RANDOM_PIVOT:
	    result = cuddZddSwapping(table,lower,upper,method);
	    break;
	case CUDD_REORDER_SIFT:
	    result = cuddZddSifting(table,lower,upper);
	    break;
	case CUDD_REORDER_SIFT_CONVERGE:
	    do {
		initialSize = table->keysZ;
		result = cuddZddSifting(table,lower,upper);
		if (initialSize <= table->keysZ)
		    break;
#ifdef DD_STATS
		else
		    (void) fprintf(table->out,"\n");
#endif