/**CFile***********************************************************************  FileName    [cuddGroup.c]  PackageName [cudd]  Synopsis    [Functions for group sifting.]  Description [External procedures included in this file:		<ul>		<li> Cudd_MakeTreeNode()		</ul>	Internal procedures included in this file:		<ul>		<li> cuddTreeSifting()		</ul>	Static procedures included in this module:		<ul>		<li> ddTreeSiftingAux()		<li> ddCountInternalMtrNodes()		<li> ddReorderChildren()		<li> ddFindNodeHiLo()		<li> ddUniqueCompareGroup()		<li> ddGroupSifting()		<li> ddCreateGroup()		<li> ddGroupSiftingAux()		<li> ddGroupSiftingUp()		<li> ddGroupSiftingDown()		<li> ddGroupMove()		<li> ddGroupMoveBackward()		<li> ddGroupSiftingBackward()		<li> ddMergeGroups()		<li> ddDissolveGroup()		<li> ddNoCheck()		<li> ddSecDiffCheck()		<li> ddExtSymmCheck()		<li> ddVarGroupCheck()		<li> ddSetVarHandled()		<li> ddResetVarHandled()		<li> ddIsVarHandled()		</ul>]  Author      [Shipra Panda, 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                                                     *//*---------------------------------------------------------------------------*//* Constants for lazy sifting */#define	DD_NORMAL_SIFT	0#define	DD_LAZY_SIFT	1/* Constants for sifting up and down */#define	DD_SIFT_DOWN	0#define	DD_SIFT_UP	1/*---------------------------------------------------------------------------*//* Stucture declarations                                                     *//*---------------------------------------------------------------------------*//*---------------------------------------------------------------------------*//* Type declarations                                                         *//*---------------------------------------------------------------------------*//*---------------------------------------------------------------------------*//* Variable declarations                                                     *//*---------------------------------------------------------------------------*/#ifndef lintstatic char rcsid[] DD_UNUSED = "$Id: cuddGroup.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $";#endifstatic	int	*entry;extern	int	ddTotalNumberSwapping;#ifdef DD_STATSextern	int	ddTotalNISwaps;static  int     extsymmcalls;static  int     extsymm;static  int     secdiffcalls;static  int     secdiff;static  int     secdiffmisfire;#endif#ifdef DD_DEBUGstatic	int	pr = 0;	/* flag to enable printing while debugging */			/* by depositing a 1 into it */#endifstatic int originalSize;static int originalLevel;/*---------------------------------------------------------------------------*//* Macro declarations                                                        *//*---------------------------------------------------------------------------*//**AutomaticStart*************************************************************//*---------------------------------------------------------------------------*//* Static function prototypes                                                *//*---------------------------------------------------------------------------*/static int ddTreeSiftingAux ARGS((DdManager *table, MtrNode *treenode, Cudd_ReorderingType method));#ifdef DD_STATSstatic int ddCountInternalMtrNodes ARGS((DdManager *table, MtrNode *treenode));#endifstatic int ddReorderChildren ARGS((DdManager *table, MtrNode *treenode, Cudd_ReorderingType method));static void ddFindNodeHiLo ARGS((DdManager *table, MtrNode *treenode, int *lower, int *upper));static int ddUniqueCompareGroup ARGS((int *ptrX, int *ptrY));static int ddGroupSifting ARGS((DdManager *table, int lower, int upper, int (*checkFunction)(DdManager *, int, int), int lazyFlag));static void ddCreateGroup ARGS((DdManager *table, int x, int y));static int ddGroupSiftingAux ARGS((DdManager *table, int x, int xLow, int xHigh, int (*checkFunction)(DdManager *, int, int), int lazyFlag));static int ddGroupSiftingUp ARGS((DdManager *table, int y, int xLow, int (*checkFunction)(DdManager *, int, int), Move **moves));static int ddGroupSiftingDown ARGS((DdManager *table, int x, int xHigh, int (*checkFunction)(DdManager *, int, int), Move **moves));static int ddGroupMove ARGS((DdManager *table, int x, int y, Move **moves));static int ddGroupMoveBackward ARGS((DdManager *table, int x, int y));static int ddGroupSiftingBackward ARGS((DdManager *table, Move *moves, int size, int upFlag, int lazyFlag));static void ddMergeGroups ARGS((DdManager *table, MtrNode *treenode, int low, int high));static void ddDissolveGroup ARGS((DdManager *table, int x, int y));static int ddNoCheck ARGS((DdManager *table, int x, int y));static int ddSecDiffCheck ARGS((DdManager *table, int x, int y));static int ddExtSymmCheck ARGS((DdManager *table, int x, int y));static int ddVarGroupCheck ARGS((DdManager * table, int x, int y)); static int ddSetVarHandled ARGS((DdManager *dd, int index));static int ddResetVarHandled ARGS((DdManager *dd, int index));static int ddIsVarHandled ARGS((DdManager *dd, int index));/**AutomaticEnd***************************************************************//*---------------------------------------------------------------------------*//* Definition of exported functions                                          *//*---------------------------------------------------------------------------*//**Function********************************************************************  Synopsis    [Creates a new variable group.]  Description [Creates a new 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 variable tree is changed.]  SeeAlso     [Cudd_MakeZddTreeNode]******************************************************************************/MtrNode *Cudd_MakeTreeNode(  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->size) ? dd->perm[low] : low;    if (level + size - 1> (int) MTR_MAXHIGH)	return(NULL);    /* If the tree does not exist yet, create it. */    tree = dd->tree;    if (tree == NULL) {	dd->tree = tree = Mtr_InitGroupTree(0, dd->size);	if (tree == NULL)	    return(NULL);	tree->index = dd->invperm[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, ddMax(level + size, (unsigned) dd->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_MakeTreeNode *//*---------------------------------------------------------------------------*//* Definition of internal functions                                          *//*---------------------------------------------------------------------------*//**Function********************************************************************  Synopsis    [Tree sifting algorithm.]  Description [Tree sifting algorithm. Assumes that a tree representing  a group hierarchy is passed as a parameter. It then reorders each  group in postorder fashion by calling ddTreeSiftingAux.  Assumes that  no dead nodes are present.  Returns 1 if successful; 0 otherwise.]  SideEffects [None]******************************************************************************/intcuddTreeSifting(  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->tree == NULL;    if (tempTree) {	table->tree = Mtr_InitGroupTree(0,table->size);	table->tree->index = table->invperm[0];    }    nvars = table->size;#ifdef DD_DEBUG    if (pr > 0 && !tempTree) (void) fprintf(table->out,"cuddTreeSifting:");    Mtr_PrintGroups(table->tree,pr <= 0);#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",		       ddCountInternalMtrNodes(table,table->tree));#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->subtables[i].next = i;    /* Reorder. */    result = ddTreeSiftingAux(table, table->tree, 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_FreeTree(table);    return(result);} /* end of cuddTreeSifting *//*---------------------------------------------------------------------------*//* 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 intddTreeSiftingAux(  DdManager * table,  MtrNode * treenode,  Cudd_ReorderingType method){    MtrNode  *auxnode;    int res;    Cudd_AggregationType saveCheck;#ifdef DD_DEBUG    Mtr_PrintGroups(treenode,1);#endif    auxnode = treenode;    while (auxnode != NULL) {	if (auxnode->child != NULL) {	    if (!ddTreeSiftingAux(table, auxnode->child, method))		return(0);	    saveCheck = table->groupcheck;	    table->groupcheck = CUDD_NO_CHECK;	    if (method != CUDD_REORDER_LAZY_SIFT)	      res = ddReorderChildren(table, auxnode, CUDD_REORDER_GROUP_SIFT);	    else	      res = ddReorderChildren(table, auxnode, CUDD_REORDER_LAZY_SIFT);	    table->groupcheck = saveCheck;	    if (res == 0)		return(0);	} else if (auxnode->size > 1) {	    if (!ddReorderChildren(table, auxnode, method))		return(0);	}	auxnode = auxnode->younger;    }    return(1);} /* end of ddTreeSiftingAux */#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 intddCountInternalMtrNodes(  DdManager * table,  MtrNode * treenode){    MtrNode *auxnode;    int     count,nodeCount;    nodeCount = 0;    auxnode = treenode;    while (auxnode != NULL) {	if (!(MTR_TEST(auxnode,MTR_TERMINAL))) {	    nodeCount++;	    count = ddCountInternalMtrNodes(table,auxnode->child);	    nodeCount += count;	}	auxnode = auxnode->younger;    }    return(nodeCount);} /* end of ddCountInternalMtrNodes */#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 intddReorderChildren(  DdManager * table,  MtrNode * treenode,  Cudd_ReorderingType method){    int lower;    int upper;    int result;    unsigned int initialSize;    ddFindNodeHiLo(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) {