diff options
Diffstat (limited to 'src/bdd/cudd/cuddGroup.c')
| -rw-r--r-- | src/bdd/cudd/cuddGroup.c | 2142 |
1 files changed, 0 insertions, 2142 deletions
diff --git a/src/bdd/cudd/cuddGroup.c b/src/bdd/cudd/cuddGroup.c deleted file mode 100644 index 81c05d2c..00000000 --- a/src/bdd/cudd/cuddGroup.c +++ /dev/null @@ -1,2142 +0,0 @@ -/**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_hack.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 lint -static char rcsid[] DD_UNUSED = "$Id: cuddGroup.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $"; -#endif - -static int *entry; -extern int ddTotalNumberSwapping; -#ifdef DD_STATS -extern int ddTotalNISwaps; -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 -static int originalSize; -static int originalLevel; - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -static int ddTreeSiftingAux ARGS((DdManager *table, MtrNode *treenode, Cudd_ReorderingType method)); -#ifdef DD_STATS -static int ddCountInternalMtrNodes ARGS((DdManager *table, MtrNode *treenode)); -#endif -static 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] - -******************************************************************************/ -int -cuddTreeSifting( - 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 int -ddTreeSiftingAux( - 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 int -ddCountInternalMtrNodes( - 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 int -ddReorderChildren( - 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) { - case CUDD_REORDER_RANDOM: - case CUDD_REORDER_RANDOM_PIVOT: - result = cuddSwapping(table,lower,upper,method); - break; - case CUDD_REORDER_SIFT: - result = cuddSifting(table,lower,upper); - break; - case CUDD_REORDER_SIFT_CONVERGE: - do { - initialSize = table->keys - table->isolated; - result = cuddSifting(table,lower,upper); - if (initialSize <= table->keys - table->isolated) - break; -#ifdef DD_STATS - else - (void) fprintf(table->out,"\n"); -#endif - } while (result != 0); - break; - case CUDD_REORDER_SYMM_SIFT: - result = cuddSymmSifting(table,lower,upper); - break; - case CUDD_REORDER_SYMM_SIFT_CONV: - result = cuddSymmSiftingConv(table,lower,upper); - break; - case CUDD_REORDER_GROUP_SIFT: - if (table->groupcheck == CUDD_NO_CHECK) { - result = ddGroupSifting(table,lower,upper,ddNoCheck, - DD_NORMAL_SIFT); - } else if (table->groupcheck == CUDD_GROUP_CHECK5) { - result = ddGroupSifting(table,lower,upper,ddExtSymmCheck, - DD_NORMAL_SIFT); - } else if (table->groupcheck == CUDD_GROUP_CHECK7) { - result = ddGroupSifting(table,lower,upper,ddExtSymmCheck, - DD_NORMAL_SIFT); - } else { - (void) fprintf(table->err, - "Unknown group ckecking method\n"); - result = 0; - } - break; - case CUDD_REORDER_GROUP_SIFT_CONV: - do { - initialSize = table->keys - table->isolated; - if (table->groupcheck == CUDD_NO_CHECK) { - result = ddGroupSifting(table,lower,upper,ddNoCheck, - DD_NORMAL_SIFT); - } else if (table->groupcheck == CUDD_GROUP_CHECK5) { - result = ddGroupSifting(table,lower,upper,ddExtSymmCheck, - DD_NORMAL_SIFT); - } else if (table->groupcheck == CUDD_GROUP_CHECK7) { - result = ddGroupSifting(table,lower,upper,ddExtSymmCheck, - DD_NORMAL_SIFT); - } else { - (void) fprintf(table->err, - "Unknown group ckecking method\n"); - result = 0; - } -#ifdef DD_STATS - (void) fprintf(table->out,"\n"); -#endif - result = cuddWindowReorder(table,lower,upper, - CUDD_REORDER_WINDOW4); - if (initialSize <= table->keys - table->isolated) - break; -#ifdef DD_STATS - else - (void) fprintf(table->out,"\n"); -#endif - } while (result != 0); - break; - case CUDD_REORDER_WINDOW2: - case CUDD_REORDER_WINDOW3: - case CUDD_REORDER_WINDOW4: - case CUDD_REORDER_WINDOW2_CONV: - case CUDD_REORDER_WINDOW3_CONV: - case CUDD_REORDER_WINDOW4_CONV: - result = cuddWindowReorder(table,lower,upper,method); - break; - case CUDD_REORDER_ANNEALING: - result = cuddAnnealing(table,lower,upper); - break; - case CUDD_REORDER_GENETIC: - result = cuddGa(table,lower,upper); - break; - case CUDD_REORDER_LINEAR: - result = cuddLinearAndSifting(table,lower,upper); - break; - case CUDD_REORDER_LINEAR_CONVERGE: - do { - initialSize = table->keys - table->isolated; - result = cuddLinearAndSifting(table,lower,upper); - if (initialSize <= table->keys - table->isolated) - break; -#ifdef DD_STATS - else - (void) fprintf(table->out,"\n"); -#endif - } while (result != 0); - break; - case CUDD_REORDER_EXACT: - result = cuddExact(table,lower,upper); - break; - case CUDD_REORDER_LAZY_SIFT: - result = ddGroupSifting(table,lower,upper,ddVarGroupCheck, - DD_LAZY_SIFT); - break; - default: - return(0); - } - } - - /* Create a single group for all the variables that were sifted, - ** so that they will be treated as a single block by successive - ** invocations of ddGroupSifting. - */ - ddMergeGroups(table,treenode,lower,upper); - -#ifdef DD_DEBUG - if (pr > 0) (void) fprintf(table->out,"ddReorderChildren:"); -#endif - - return(result); - -} /* end of ddReorderChildren */ - - -/**Function******************************************************************** - - Synopsis [Finds the lower and upper bounds of the group represented - by treenode.] - - Description [Finds the lower and upper bounds of the group - represented by treenode. From the index and size fields we need to - derive the current positions, and find maximum and minimum.] - - SideEffects [The bounds are returned as side effects.] - - SeeAlso [] - -******************************************************************************/ -static void -ddFindNodeHiLo( - DdManager * table, - MtrNode * treenode, - int * lower, - int * upper) -{ - int low; - int high; - - /* Check whether no variables in this group already exist. - ** If so, return immediately. The calling procedure will know from - ** the values of upper that no reordering is needed. - */ - if ((int) treenode->low >= table->size) { - *lower = table->size; - *upper = -1; - return; - } - - *lower = low = (unsigned int) table->perm[treenode->index]; - high = (int) (low + treenode->size - 1); - - if (high >= table->size) { - /* This is the case of a partially existing group. The aim is to - ** reorder as many variables as safely possible. If the tree - ** node is terminal, we just reorder the subset of the group - ** that is currently in existence. If the group has - ** subgroups, then we only reorder those subgroups that are - ** fully instantiated. This way we avoid breaking up a group. - */ - MtrNode *auxnode = treenode->child; - if (auxnode == NULL) { - *upper = (unsigned int) table->size - 1; - } else { - /* Search the subgroup that strands the table->size line. - ** If the first group starts at 0 and goes past table->size - ** upper will get -1, thus correctly signaling that no reordering - ** should take place. - */ - while (auxnode != NULL) { - int thisLower = table->perm[auxnode->low]; - int thisUpper = thisLower + auxnode->size - 1; - if (thisUpper >= table->size && thisLower < table->size) - *upper = (unsigned int) thisLower - 1; - auxnode = auxnode->younger; - } - } - } else { - /* Normal case: All the variables of the group exist. */ - *upper = (unsigned int) high; - } - -#ifdef DD_DEBUG - /* Make sure that all variables in group are contiguous. */ - assert(treenode->size >= *upper - *lower + 1); -#endif - - return; - -} /* end of ddFindNodeHiLo */ - - -/**Function******************************************************************** - - Synopsis [Comparison function used by qsort.] - - Description [Comparison function used by qsort to order the variables - according to the number of keys in the subtables. Returns the - difference in number of keys between the two variables being - compared.] - - SideEffects [None] - -******************************************************************************/ -static int -ddUniqueCompareGroup( - int * ptrX, - int * ptrY) -{ -#if 0 - if (entry[*ptrY] == entry[*ptrX]) { - return((*ptrX) - (*ptrY)); - } -#endif - return(entry[*ptrY] - entry[*ptrX]); - -} /* end of ddUniqueCompareGroup */ - - -/**Function******************************************************************** - - Synopsis [Sifts from treenode->low to treenode->high.] - - Description [Sifts from treenode->low to treenode->high. If - croupcheck == CUDD_GROUP_CHECK7, it checks for group creation at the - end of the initial sifting. If a group is created, it is then sifted - again. After sifting one variable, the group that contains it is - dissolved. Returns 1 in case of success; 0 otherwise.] - - SideEffects [None] - -******************************************************************************/ -static int -ddGroupSifting( - DdManager * table, - int lower, - int upper, - int (*checkFunction)(DdManager *, int, int), - int lazyFlag) -{ - int *var; - int i,j,x,xInit; - int nvars; - int classes; - int result; - int *sifted; - int merged; - int dissolve; -#ifdef DD_STATS - unsigned previousSize; -#endif - int xindex; - - nvars = table->size; - - /* Order variables to sift. */ - entry = NULL; - sifted = NULL; - var = ALLOC(int,nvars); - if (var == NULL) { - table->errorCode = CUDD_MEMORY_OUT; - goto ddGroupSiftingOutOfMem; - } - entry = ALLOC(int,nvars); - if (entry == NULL) { - table->errorCode = CUDD_MEMORY_OUT; - goto ddGroupSiftingOutOfMem; - } - sifted = ALLOC(int,nvars); - if (sifted == NULL) { - table->errorCode = CUDD_MEMORY_OUT; - goto ddGroupSiftingOutOfMem; - } - - /* Here we consider only one representative for each group. */ - for (i = 0, classes = 0; i < nvars; i++) { - sifted[i] = 0; - x = table->perm[i]; - if ((unsigned) x >= table->subtables[x].next) { - entry[i] = table->subtables[x].keys; - var[classes] = i; - classes++; - } - } - - qsort((void *)var,classes,sizeof(int), - (int (*)(const void *, const void *)) ddUniqueCompareGroup); - - if (lazyFlag) { - for (i = 0; i < nvars; i ++) { - ddResetVarHandled(table, i); - } - } - - /* Now sift. */ - for (i = 0; i < ddMin(table->siftMaxVar,classes); i++) { - if (ddTotalNumberSwapping >= table->siftMaxSwap) - break; - xindex = var[i]; - if (sifted[xindex] == 1) /* variable already sifted as part of group */ - continue; - x = table->perm[xindex]; /* find current level of this variable */ - - if (x < lower || x > upper || table->subtables[x].bindVar == 1) - continue; -#ifdef DD_STATS - previousSize = table->keys - table->isolated; -#endif -#ifdef DD_DEBUG - /* x is bottom of group */ - assert((unsigned) x >= table->subtables[x].next); -#endif - if ((unsigned) x == table->subtables[x].next) { - dissolve = 1; - result = ddGroupSiftingAux(table,x,lower,upper,checkFunction, - lazyFlag); - } else { - dissolve = 0; - result = ddGroupSiftingAux(table,x,lower,upper,ddNoCheck,lazyFlag); - } - if (!result) goto ddGroupSiftingOutOfMem; - - /* check for aggregation */ - merged = 0; - if (lazyFlag == 0 && table->groupcheck == CUDD_GROUP_CHECK7) { - x = table->perm[xindex]; /* find current level */ - if ((unsigned) x == table->subtables[x].next) { /* not part of a group */ - if (x != upper && sifted[table->invperm[x+1]] == 0 && - (unsigned) x+1 == table->subtables[x+1].next) { - if (ddSecDiffCheck(table,x,x+1)) { - merged =1; - ddCreateGroup(table,x,x+1); - } - } - if (x != lower && sifted[table->invperm[x-1]] == 0 && - (unsigned) x-1 == table->subtables[x-1].next) { - if (ddSecDiffCheck(table,x-1,x)) { - merged =1; - ddCreateGroup(table,x-1,x); - } - } - } - } - - if (merged) { /* a group was created */ - /* move x to bottom of group */ - while ((unsigned) x < table->subtables[x].next) - x = table->subtables[x].next; - /* sift */ - result = ddGroupSiftingAux(table,x,lower,upper,ddNoCheck,lazyFlag); - if (!result) goto ddGroupSiftingOutOfMem; -#ifdef DD_STATS - if (table->keys < previousSize + table->isolated) { - (void) fprintf(table->out,"_"); - } else if (table->keys > previousSize + table->isolated) { - (void) fprintf(table->out,"^"); - } else { - (void) fprintf(table->out,"*"); - } - fflush(table->out); - } else { - if (table->keys < previousSize + table->isolated) { - (void) fprintf(table->out,"-"); - } else if (table->keys > previousSize + table->isolated) { - (void) fprintf(table->out,"+"); - } else { - (void) fprintf(table->out,"="); - } - fflush(table->out); -#endif - } - - /* Mark variables in the group just sifted. */ - x = table->perm[xindex]; - if ((unsigned) x != table->subtables[x].next) { - xInit = x; - do { - j = table->invperm[x]; - sifted[j] = 1; - x = table->subtables[x].next; - } while (x != xInit); - - /* Dissolve the group if it was created. */ - if (lazyFlag == 0 && dissolve) { - do { - j = table->subtables[x].next; - table->subtables[x].next = x; - x = j; - } while (x != xInit); - } - } - -#ifdef DD_DEBUG - if (pr > 0) (void) fprintf(table->out,"ddGroupSifting:"); -#endif - - if (lazyFlag) ddSetVarHandled(table, xindex); - } /* for */ - - FREE(sifted); - FREE(var); - FREE(entry); - - return(1); - -ddGroupSiftingOutOfMem: - if (entry != NULL) FREE(entry); - if (var != NULL) FREE(var); - if (sifted != NULL) FREE(sifted); - - return(0); - -} /* end of ddGroupSifting */ - - -/**Function******************************************************************** - - Synopsis [Creates a group encompassing variables from x to y in the - DD table.] - - Description [Creates a group encompassing variables from x to y in the - DD table. In the current implementation it must be y == x+1. - Returns 1 in case of success; 0 otherwise.] - - SideEffects [None] - -******************************************************************************/ -static void -ddCreateGroup( - DdManager * table, - int x, - int y) -{ - int gybot; - -#ifdef DD_DEBUG - assert(y == x+1); -#endif - - /* Find bottom of second group. */ - gybot = y; - while ((unsigned) gybot < table->subtables[gybot].next) - gybot = table->subtables[gybot].next; - - /* Link groups. */ - table->subtables[x].next = y; - table->subtables[gybot].next = x; - - return; - -} /* ddCreateGroup */ - - -/**Function******************************************************************** - - Synopsis [Sifts one variable up and down until it has taken all - positions. Checks for aggregation.] - - Description [Sifts one variable up and down until it has taken all - positions. Checks for aggregation. There may be at most two sweeps, - even if the group grows. Assumes that x is either an isolated - variable, or it is the bottom of a group. All groups may not have - been found. The variable being moved is returned to the best position - seen during sifting. Returns 1 in case of success; 0 otherwise.] - - SideEffects [None] - -******************************************************************************/ -static int -ddGroupSiftingAux( - DdManager * table, - int x, - int xLow, - int xHigh, - int (*checkFunction)(DdManager *, int, int), - int lazyFlag) -{ - Move *move; - Move *moves; /* list of moves */ - int initialSize; - int result; - int y; - int topbot; - -#ifdef DD_DEBUG - if (pr > 0) (void) fprintf(table->out, - "ddGroupSiftingAux from %d to %d\n",xLow,xHigh); - assert((unsigned) x >= table->subtables[x].next); /* x is bottom of group */ -#endif - - initialSize = table->keys - table->isolated; - moves = NULL; - - originalSize = initialSize; /* for lazy sifting */ - - /* If we have a singleton, we check for aggregation in both - ** directions before we sift. - */ - if ((unsigned) x == table->subtables[x].next) { - /* Will go down first, unless x == xHigh: - ** Look for aggregation above x. - */ - for (y = x; y > xLow; y--) { - if (!checkFunction(table,y-1,y)) - break; - topbot = table->subtables[y-1].next; /* find top of y-1's group */ - table->subtables[y-1].next = y; - table->subtables[x].next = topbot; /* x is bottom of group so its */ - /* next is top of y-1's group */ - y = topbot + 1; /* add 1 for y--; new y is top of group */ - } - /* Will go up first unless x == xlow: - ** Look for aggregation below x. - */ - for (y = x; y < xHigh; y++) { - if (!checkFunction(table,y,y+1)) - break; - /* find bottom of y+1's group */ - topbot = y + 1; - while ((unsigned) topbot < table->subtables[topbot].next) { - topbot = table->subtables[topbot].next; - } - table->subtables[topbot].next = table->subtables[y].next; - table->subtables[y].next = y + 1; - y = topbot - 1; /* subtract 1 for y++; new y is bottom of group */ - } - } - - /* Now x may be in the middle of a group. - ** Find bottom of x's group. - */ - while ((unsigned) x < table->subtables[x].next) - x = table->subtables[x].next; - - originalLevel = x; /* for lazy sifting */ - - if (x == xLow) { /* Sift down */ -#ifdef DD_DEBUG - /* x must be a singleton */ - assert((unsigned) x == table->subtables[x].next); -#endif - if (x == xHigh) return(1); /* just one variable */ - - if (!ddGroupSiftingDown(table,x,xHigh,checkFunction,&moves)) - goto ddGroupSiftingAuxOutOfMem; - /* at this point x == xHigh, unless early term */ - - /* move backward and stop at best position */ - result = ddGroupSiftingBackward(table,moves,initialSize, - DD_SIFT_DOWN,lazyFlag); -#ifdef DD_DEBUG - assert(table->keys - table->isolated <= (unsigned) initialSize); -#endif - if (!result) goto ddGroupSiftingAuxOutOfMem; - - } else if (cuddNextHigh(table,x) > xHigh) { /* Sift up */ -#ifdef DD_DEBUG - /* x is bottom of group */ - assert((unsigned) x >= table->subtables[x].next); -#endif - /* Find top of x's group */ - x = table->subtables[x].next; - - if (!ddGroupSiftingUp(table,x,xLow,checkFunction,&moves)) - goto ddGroupSiftingAuxOutOfMem; - /* at this point x == xLow, unless early term */ - - /* move backward and stop at best position */ - result = ddGroupSiftingBackward(table,moves,initialSize, - DD_SIFT_UP,lazyFlag); -#ifdef DD_DEBUG - assert(table->keys - table->isolated <= (unsigned) initialSize); -#endif - if (!result) goto ddGroupSiftingAuxOutOfMem; - - } else if (x - xLow > xHigh - x) { /* must go down first: shorter */ - if (!ddGroupSiftingDown(table,x,xHigh,checkFunction,&moves)) - goto ddGroupSiftingAuxOutOfMem; - /* at this point x == xHigh, unless early term */ - - /* Find top of group */ - if (moves) { - x = moves->y; - } - while ((unsigned) x < table->subtables[x].next) - x = table->subtables[x].next; - x = table->subtables[x].next; -#ifdef DD_DEBUG - /* x should be the top of a group */ - assert((unsigned) x <= table->subtables[x].next); -#endif - - if (!ddGroupSiftingUp(table,x,xLow,checkFunction,&moves)) - goto ddGroupSiftingAuxOutOfMem; - - /* move backward and stop at best position */ - result = ddGroupSiftingBackward(table,moves,initialSize, - DD_SIFT_UP,lazyFlag); -#ifdef DD_DEBUG - assert(table->keys - table->isolated <= (unsigned) initialSize); -#endif - if (!result) goto ddGroupSiftingAuxOutOfMem; - - } else { /* moving up first: shorter */ - /* Find top of x's group */ - x = table->subtables[x].next; - - if (!ddGroupSiftingUp(table,x,xLow,checkFunction,&moves)) - goto ddGroupSiftingAuxOutOfMem; - /* at this point x == xHigh, unless early term */ - - if (moves) { - x = moves->x; - } - while ((unsigned) x < table->subtables[x].next) - x = table->subtables[x].next; -#ifdef DD_DEBUG - /* x is bottom of a group */ - assert((unsigned) x >= table->subtables[x].next); -#endif - - if (!ddGroupSiftingDown(table,x,xHigh,checkFunction,&moves)) - goto ddGroupSiftingAuxOutOfMem; - - /* move backward and stop at best position */ - result = ddGroupSiftingBackward(table,moves,initialSize, - DD_SIFT_DOWN,lazyFlag); -#ifdef DD_DEBUG - assert(table->keys - table->isolated <= (unsigned) initialSize); -#endif - if (!result) goto ddGroupSiftingAuxOutOfMem; - } - - while (moves != NULL) { - move = moves->next; - cuddDeallocNode(table, (DdNode *) moves); - moves = move; - } - - return(1); - -ddGroupSiftingAuxOutOfMem: - while (moves != NULL) { - move = moves->next; - cuddDeallocNode(table, (DdNode *) moves); - moves = move; - } - - return(0); - -} /* end of ddGroupSiftingAux */ - - -/**Function******************************************************************** - - Synopsis [Sifts up a variable until either it reaches position xLow - or the size of the DD heap increases too much.] - - Description [Sifts up a variable until either it reaches position - xLow or the size of the DD heap increases too much. Assumes that y is - the top of a group (or a singleton). Checks y for aggregation to the - adjacent variables. Records all the moves that are appended to the - list of moves received as input and returned as a side effect. - Returns 1 in case of success; 0 otherwise.] - - SideEffects [None] - -******************************************************************************/ -static int -ddGroupSiftingUp( - DdManager * table, - int y, - int xLow, - int (*checkFunction)(DdManager *, int, int), - Move ** moves) -{ - Move *move; - int x; - int size; - int i; - int gxtop,gybot; - int limitSize; - int xindex, yindex; - int zindex; - int z; - int isolated; - int L; /* lower bound on DD size */ -#ifdef DD_DEBUG - int checkL; -#endif - - yindex = table->invperm[y]; - - /* Initialize the lower bound. - ** The part of the DD below the bottom of y's group will not change. - ** The part of the DD above y that does not interact with any - ** variable of y's group will not change. - ** The rest may vanish in the best case, except for - ** the nodes at level xLow, which will not vanish, regardless. - ** What we use here is not really a lower bound, because we ignore - ** the interactions with all variables except y. - */ - limitSize = L = table->keys - table->isolated; - gybot = y; - while ((unsigned) gybot < table->subtables[gybot].next) - gybot = table->subtables[gybot].next; - for (z = xLow + 1; z <= gybot; z++) { - zindex = table->invperm[z]; - if (zindex == yindex || cuddTestInteract(table,zindex,yindex)) { - isolated = table->vars[zindex]->ref == 1; - L -= table->subtables[z].keys - isolated; - } - } - - originalLevel = y; /* for lazy sifting */ - - x = cuddNextLow(table,y); - while (x >= xLow && L <= limitSize) { -#ifdef DD_DEBUG - gybot = y; - while ((unsigned) gybot < table->subtables[gybot].next) - gybot = table->subtables[gybot].next; - checkL = table->keys - table->isolated; - for (z = xLow + 1; z <= gybot; z++) { - zindex = table->invperm[z]; - if (zindex == yindex || cuddTestInteract(table,zindex,yindex)) { - isolated = table->vars[zindex]->ref == 1; - checkL -= table->subtables[z].keys - isolated; - } - } - if (pr > 0 && L != checkL) { - (void) fprintf(table->out, - "Inaccurate lower bound: L = %d checkL = %d\n", - L, checkL); - } -#endif - gxtop = table->subtables[x].next; - if (checkFunction(table,x,y)) { - /* Group found, attach groups */ - table->subtables[x].next = y; - i = table->subtables[y].next; - while (table->subtables[i].next != (unsigned) y) - i = table->subtables[i].next; - table->subtables[i].next = gxtop; - move = (Move *)cuddDynamicAllocNode(table); - if (move == NULL) goto ddGroupSiftingUpOutOfMem; - move->x = x; - move->y = y; - move->flags = MTR_NEWNODE; - move->size = table->keys - table->isolated; - move->next = *moves; - *moves = move; - } else if (table->subtables[x].next == (unsigned) x && - table->subtables[y].next == (unsigned) y) { - /* x and y are self groups */ - xindex = table->invperm[x]; - size = cuddSwapInPlace(table,x,y); -#ifdef DD_DEBUG - assert(table->subtables[x].next == (unsigned) x); - assert(table->subtables[y].next == (unsigned) y); -#endif - if (size == 0) goto ddGroupSiftingUpOutOfMem; - /* Update the lower bound. */ - if (cuddTestInteract(table,xindex,yindex)) { - isolated = table->vars[xindex]->ref == 1; - L += table->subtables[y].keys - isolated; - } - move = (Move *)cuddDynamicAllocNode(table); - if (move == NULL) goto ddGroupSiftingUpOutOfMem; - move->x = x; - move->y = y; - move->flags = MTR_DEFAULT; - move->size = size; - move->next = *moves; - *moves = move; - -#ifdef DD_DEBUG - if (pr > 0) (void) fprintf(table->out, - "ddGroupSiftingUp (2 single groups):\n"); -#endif - if ((double) size > (double) limitSize * table->maxGrowth) - return(1); - if (size < limitSize) limitSize = size; - } else { /* Group move */ - size = ddGroupMove(table,x,y,moves); - if (size == 0) goto ddGroupSiftingUpOutOfMem; - /* Update the lower bound. */ - z = (*moves)->y; - do { - zindex = table->invperm[z]; - if (cuddTestInteract(table,zindex,yindex)) { - isolated = table->vars[zindex]->ref == 1; - L += table->subtables[z].keys - isolated; - } - z = table->subtables[z].next; - } while (z != (int) (*moves)->y); - if ((double) size > (double) limitSize * table->maxGrowth) - return(1); - if (size < limitSize) limitSize = size; - } - y = gxtop; - x = cuddNextLow(table,y); - } - - return(1); - -ddGroupSiftingUpOutOfMem: - while (*moves != NULL) { - move = (*moves)->next; - cuddDeallocNode(table, (DdNode *) *moves); - *moves = move; - } - return(0); - -} /* end of ddGroupSiftingUp */ - - -/**Function******************************************************************** - - Synopsis [Sifts down a variable until it reaches position xHigh.] - - Description [Sifts down a variable until it reaches position xHigh. - Assumes that x is the bottom of a group (or a singleton). Records - all the moves. Returns 1 in case of success; 0 otherwise.] - - SideEffects [None] - -******************************************************************************/ -static int -ddGroupSiftingDown( - DdManager * table, - int x, - int xHigh, - int (*checkFunction)(DdManager *, int, int), - Move ** moves) -{ - Move *move; - int y; - int size; - int limitSize; - int gxtop,gybot; - int R; /* upper bound on node decrease */ - int xindex, yindex; - int isolated, allVars; - int z; - int zindex; -#ifdef DD_DEBUG - int checkR; -#endif - - /* If the group consists of simple variables, there is no point in - ** sifting it down. This check is redundant if the projection functions - ** do not have external references, because the computation of the - ** lower bound takes care of the problem. It is necessary otherwise to - ** prevent the sifting down of simple variables. */ - y = x; - allVars = 1; - do { - if (table->subtables[y].keys != 1) { - allVars = 0; - break; - } - y = table->subtables[y].next; - } while (table->subtables[y].next != (unsigned) x); - if (allVars) - return(1); - - /* Initialize R. */ - xindex = table->invperm[x]; - gxtop = table->subtables[x].next; - limitSize = size = table->keys - table->isolated; - R = 0; - for (z = xHigh; z > gxtop; z--) { - zindex = table->invperm[z]; - if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) { - isolated = table->vars[zindex]->ref == 1; - R += table->subtables[z].keys - isolated; - } - } - - originalLevel = x; /* for lazy sifting */ - - y = cuddNextHigh(table,x); - while (y <= xHigh && size - R < limitSize) { -#ifdef DD_DEBUG - gxtop = table->subtables[x].next; - checkR = 0; - for (z = xHigh; z > gxtop; z--) { - zindex = table->invperm[z]; - if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) { - isolated = table->vars[zindex]->ref == 1; - checkR += table->subtables[z].keys - isolated; - } - } - assert(R >= checkR); -#endif - /* Find bottom of y group. */ - gybot = table->subtables[y].next; - while (table->subtables[gybot].next != (unsigned) y) - gybot = table->subtables[gybot].next; - - if (checkFunction(table,x,y)) { - /* Group found: attach groups and record move. */ - gxtop = table->subtables[x].next; - table->subtables[x].next = y; - table->subtables[gybot].next = gxtop; - move = (Move *)cuddDynamicAllocNode(table); - if (move == NULL) goto ddGroupSiftingDownOutOfMem; - move->x = x; - move->y = y; - move->flags = MTR_NEWNODE; - move->size = table->keys - table->isolated; - move->next = *moves; - *moves = move; - } else if (table->subtables[x].next == (unsigned) x && - table->subtables[y].next == (unsigned) y) { - /* x and y are self groups */ - /* Update upper bound on node decrease. */ - yindex = table->invperm[y]; - if (cuddTestInteract(table,xindex,yindex)) { - isolated = table->vars[yindex]->ref == 1; - R -= table->subtables[y].keys - isolated; - } - size = cuddSwapInPlace(table,x,y); -#ifdef DD_DEBUG - assert(table->subtables[x].next == (unsigned) x); - assert(table->subtables[y].next == (unsigned) y); -#endif - if (size == 0) goto ddGroupSiftingDownOutOfMem; - - /* Record move. */ - move = (Move *) cuddDynamicAllocNode(table); - if (move == NULL) goto ddGroupSiftingDownOutOfMem; - move->x = x; - move->y = y; - move->flags = MTR_DEFAULT; - move->size = size; - move->next = *moves; - *moves = move; - -#ifdef DD_DEBUG - if (pr > 0) (void) fprintf(table->out, - "ddGroupSiftingDown (2 single groups):\n"); -#endif - if ((double) size > (double) limitSize * table->maxGrowth) - return(1); - if (size < limitSize) limitSize = size; - - x = y; - y = cuddNextHigh(table,x); - } else { /* Group move */ - /* Update upper bound on node decrease: first phase. */ - gxtop = table->subtables[x].next; - z = gxtop + 1; - do { - zindex = table->invperm[z]; - if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) { - isolated = table->vars[zindex]->ref == 1; - R -= table->subtables[z].keys - isolated; - } - z++; - } while (z <= gybot); - size = ddGroupMove(table,x,y,moves); - if (size == 0) goto ddGroupSiftingDownOutOfMem; - if ((double) size > (double) limitSize * table->maxGrowth) - return(1); - if (size < limitSize) limitSize = size; - - /* Update upper bound on node decrease: second phase. */ - gxtop = table->subtables[gybot].next; - for (z = gxtop + 1; z <= gybot; z++) { - zindex = table->invperm[z]; - if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) { - isolated = table->vars[zindex]->ref == 1; - R += table->subtables[z].keys - isolated; - } - } - } - x = gybot; - y = cuddNextHigh(table,x); - } - - return(1); - -ddGroupSiftingDownOutOfMem: - while (*moves != NULL) { - move = (*moves)->next; - cuddDeallocNode(table, (DdNode *) *moves); - *moves = move; - } - - return(0); - -} /* end of ddGroupSiftingDown */ - - -/**Function******************************************************************** - - Synopsis [Swaps two groups and records the move.] - - Description [Swaps two groups and records the move. Returns the - number of keys in the DD table in case of success; 0 otherwise.] - - SideEffects [None] - -******************************************************************************/ -static int -ddGroupMove( - DdManager * table, - int x, - int y, - Move ** moves) -{ - Move *move; - int size; - int i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop; - int swapx,swapy; -#if defined(DD_DEBUG) && defined(DD_VERBOSE) - int initialSize,bestSize; -#endif - -#if DD_DEBUG - /* We assume that x < y */ - assert(x < y); -#endif - /* Find top, bottom, and size for the two groups. */ - xbot = x; - xtop = table->subtables[x].next; - xsize = xbot - xtop + 1; - ybot = y; - while ((unsigned) ybot < table->subtables[ybot].next) - ybot = table->subtables[ybot].next; - ytop = y; - ysize = ybot - ytop + 1; - -#if defined(DD_DEBUG) && defined(DD_VERBOSE) - initialSize = bestSize = table->keys - table->isolated; -#endif - /* Sift the variables of the second group up through the first group */ - for (i = 1; i <= ysize; i++) { - for (j = 1; j <= xsize; j++) { - size = cuddSwapInPlace(table,x,y); - if (size == 0) goto ddGroupMoveOutOfMem; -#if defined(DD_DEBUG) && defined(DD_VERBOSE) - if (size < bestSize) - bestSize = size; -#endif - swapx = x; swapy = y; - y = x; - x = cuddNextLow(table,y); - } - y = ytop + i; - x = cuddNextLow(table,y); - } -#if defined(DD_DEBUG) && defined(DD_VERBOSE) - if ((bestSize < initialSize) && (bestSize < size)) - (void) fprintf(table->out,"Missed local minimum: initialSize:%d bestSize:%d finalSize:%d\n",initialSize,bestSize,size); -#endif - - /* fix groups */ - y = xtop; /* ytop is now where xtop used to be */ - for (i = 0; i < ysize - 1; i++) { - table->subtables[y].next = cuddNextHigh(table,y); - y = cuddNextHigh(table,y); - } - table->subtables[y].next = xtop; /* y is bottom of its group, join */ - /* it to top of its group */ - x = cuddNextHigh(table,y); - newxtop = x; - for (i = 0; i < xsize - 1; i++) { - table->subtables[x].next = cuddNextHigh(table,x); - x = cuddNextHigh(table,x); - } - table->subtables[x].next = newxtop; /* x is bottom of its group, join */ - /* it to top of its group */ -#ifdef DD_DEBUG - if (pr > 0) (void) fprintf(table->out,"ddGroupMove:\n"); -#endif - - /* Store group move */ - move = (Move *) cuddDynamicAllocNode(table); - if (move == NULL) goto ddGroupMoveOutOfMem; - move->x = swapx; - move->y = swapy; - move->flags = MTR_DEFAULT; - move->size = table->keys - table->isolated; - move->next = *moves; - *moves = move; - - return(table->keys - table->isolated); - -ddGroupMoveOutOfMem: - while (*moves != NULL) { - move = (*moves)->next; - cuddDeallocNode(table, (DdNode *) *moves); - *moves = move; - } - return(0); - -} /* end of ddGroupMove */ - - -/**Function******************************************************************** - - Synopsis [Undoes the swap two groups.] - - Description [Undoes the swap two groups. Returns 1 in case of - success; 0 otherwise.] - - SideEffects [None] - -******************************************************************************/ -static int -ddGroupMoveBackward( - DdManager * table, - int x, - int y) -{ - int size; - int i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop; - - -#if DD_DEBUG - /* We assume that x < y */ - assert(x < y); -#endif - - /* Find top, bottom, and size for the two groups. */ - xbot = x; - xtop = table->subtables[x].next; - xsize = xbot - xtop + 1; - ybot = y; - while ((unsigned) ybot < table->subtables[ybot].next) - ybot = table->subtables[ybot].next; - ytop = y; - ysize = ybot - ytop + 1; - - /* Sift the variables of the second group up through the first group */ - for (i = 1; i <= ysize; i++) { - for (j = 1; j <= xsize; j++) { - size = cuddSwapInPlace(table,x,y); - if (size == 0) - return(0); - y = x; - x = cuddNextLow(table,y); - } - y = ytop + i; - x = cuddNextLow(table,y); - } - - /* fix groups */ - y = xtop; - for (i = 0; i < ysize - 1; i++) { - table->subtables[y].next = cuddNextHigh(table,y); - y = cuddNextHigh(table,y); - } - table->subtables[y].next = xtop; /* y is bottom of its group, join */ - /* to its top */ - x = cuddNextHigh(table,y); - newxtop = x; - for (i = 0; i < xsize - 1; i++) { - table->subtables[x].next = cuddNextHigh(table,x); - x = cuddNextHigh(table,x); - } - table->subtables[x].next = newxtop; /* x is bottom of its group, join */ - /* to its top */ -#ifdef DD_DEBUG - if (pr > 0) (void) fprintf(table->out,"ddGroupMoveBackward:\n"); -#endif - - return(1); - -} /* end of ddGroupMoveBackward */ - - -/**Function******************************************************************** - - Synopsis [Determines the best position for a variables and returns - it there.] - - Description [Determines the best position for a variables and returns - it there. Returns 1 in case of success; 0 otherwise.] - - SideEffects [None] - -******************************************************************************/ -static int -ddGroupSiftingBackward( - DdManager * table, - Move * moves, - int size, - int upFlag, - int lazyFlag) -{ - Move *move; - int res; - Move *end_move; - int diff, tmp_diff; - int index, pairlev; - - if (lazyFlag) { - end_move = NULL; - - /* Find the minimum size, and the earliest position at which it - ** was achieved. */ - for (move = moves; move != NULL; move = move->next) { - if (move->size < size) { - size = move->size; - end_move = move; - } else if (move->size == size) { - if (end_move == NULL) end_move = move; - } - } - - /* Find among the moves that give minimum size the one that - ** minimizes the distance from the corresponding variable. */ - if (moves != NULL) { - diff = Cudd_ReadSize(table) + 1; - index = (upFlag == 1) ? - table->invperm[moves->x] : table->invperm[moves->y]; - pairlev = table->perm[Cudd_bddReadPairIndex(table, index)]; - - for (move = moves; move != NULL; move = move->next) { - if (move->size == size) { - if (upFlag == 1) { - tmp_diff = (move->x > pairlev) ? - move->x - pairlev : pairlev - move->x; - } else { - tmp_diff = (move->y > pairlev) ? - move->y - pairlev : pairlev - move->y; - } - if (tmp_diff < diff) { - diff = tmp_diff; - end_move = move; - } - } - } - } - } else { - /* Find the minimum size. */ - for (move = moves; move != NULL; move = move->next) { - if (move->size < size) { - size = move->size; - } - } - } - - /* In case of lazy sifting, end_move identifies the position at - ** which we want to stop. Otherwise, we stop as soon as we meet - ** the minimum size. */ - for (move = moves; move != NULL; move = move->next) { - if (lazyFlag) { - if (move == end_move) return(1); - } else { - if (move->size == size) return(1); - } - if ((table->subtables[move->x].next == move->x) && - (table->subtables[move->y].next == move->y)) { - res = cuddSwapInPlace(table,(int)move->x,(int)move->y); - if (!res) return(0); -#ifdef DD_DEBUG - if (pr > 0) (void) fprintf(table->out,"ddGroupSiftingBackward:\n"); - assert(table->subtables[move->x].next == move->x); - assert(table->subtables[move->y].next == move->y); -#endif - } else { /* Group move necessary */ - if (move->flags == MTR_NEWNODE) { - ddDissolveGroup(table,(int)move->x,(int)move->y); - } else { - res = ddGroupMoveBackward(table,(int)move->x,(int)move->y); - if (!res) return(0); - } - } - - } - - return(1); - -} /* end of ddGroupSiftingBackward */ - - -/**Function******************************************************************** - - Synopsis [Merges groups in the DD table.] - - Description [Creates a single group from low to high and adjusts the - index field of the tree node.] - - SideEffects [None] - -******************************************************************************/ -static void -ddMergeGroups( - DdManager * table, - MtrNode * treenode, - int low, - int high) -{ - int i; - MtrNode *auxnode; - int saveindex; - int newindex; - - /* Merge all variables from low to high in one group, unless - ** this is the topmost group. In such a case we do not merge lest - ** we lose the symmetry information. */ - if (treenode != table->tree) { - for (i = low; i < high; i++) - table->subtables[i].next = i+1; - table->subtables[high].next = low; - } - - /* Adjust the index fields of the tree nodes. If a node is the - ** first child of its parent, then the parent may also need adjustment. */ - saveindex = treenode->index; - newindex = table->invperm[low]; - auxnode = treenode; - do { - auxnode->index = newindex; - if (auxnode->parent == NULL || - (int) auxnode->parent->index != saveindex) - break; - auxnode = auxnode->parent; - } while (1); - return; - -} /* end of ddMergeGroups */ - - -/**Function******************************************************************** - - Synopsis [Dissolves a group in the DD table.] - - Description [x and y are variables in a group to be cut in two. The cut - is to pass between x and y.] - - SideEffects [None] - -******************************************************************************/ -static void -ddDissolveGroup( - DdManager * table, - int x, - int y) -{ - int topx; - int boty; - - /* find top and bottom of the two groups */ - boty = y; - while ((unsigned) boty < table->subtables[boty].next) - boty = table->subtables[boty].next; - - topx = table->subtables[boty].next; - - table->subtables[boty].next = y; - table->subtables[x].next = topx; - - return; - -} /* end of ddDissolveGroup */ - - -/**Function******************************************************************** - - Synopsis [Pretends to check two variables for aggregation.] - - Description [Pretends to check two variables for aggregation. Always - returns 0.] - - SideEffects [None] - -******************************************************************************/ -static int -ddNoCheck( - DdManager * table, - int x, - int y) -{ - return(0); - -} /* end of ddNoCheck */ - - -/**Function******************************************************************** - - Synopsis [Checks two variables for aggregation.] - - Description [Checks two variables for aggregation. The check is based - on the second difference of the number of nodes as a function of the - layer. If the second difference is lower than a given threshold - (typically negative) then the two variables should be aggregated. - Returns 1 if the two variables pass the test; 0 otherwise.] - - SideEffects [None] - -******************************************************************************/ -static int -ddSecDiffCheck( - DdManager * table, - int x, - int y) -{ - double Nx,Nx_1; - double Sx; - double threshold; - int xindex,yindex; - - if (x==0) return(0); - -#ifdef DD_STATS - secdiffcalls++; -#endif - Nx = (double) table->subtables[x].keys; - Nx_1 = (double) table->subtables[x-1].keys; - Sx = (table->subtables[y].keys/Nx) - (Nx/Nx_1); - - threshold = table->recomb / 100.0; - if (Sx < threshold) { - xindex = table->invperm[x]; - yindex = table->invperm[y]; - if (cuddTestInteract(table,xindex,yindex)) { -#if defined(DD_DEBUG) && defined(DD_VERBOSE) - (void) fprintf(table->out, - "Second difference for %d = %g Pos(%d)\n", - table->invperm[x],Sx,x); -#endif -#ifdef DD_STATS - secdiff++; -#endif - return(1); - } else { -#ifdef DD_STATS - secdiffmisfire++; -#endif - return(0); - } - - } - return(0); - -} /* end of ddSecDiffCheck */ - - -/**Function******************************************************************** - - Synopsis [Checks for extended symmetry of x and y.] - - Description [Checks for extended symmetry of x and y. Returns 1 in - case of extended symmetry; 0 otherwise.] - - SideEffects [None] - -******************************************************************************/ -static int -ddExtSymmCheck( - DdManager * table, - int x, - int y) -{ - DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10; - DdNode *one; - int comple; /* f0 is complemented */ - int notproj; /* f is not a projection function */ - int arccount; /* number of arcs from layer x to layer y */ - int TotalRefCount; /* total reference count of layer y minus 1 */ - int counter; /* number of nodes of layer x that are allowed */ - /* to violate extended symmetry conditions */ - int arccounter; /* number of arcs into layer y that are allowed */ - /* to come from layers other than x */ - int i; - int xindex; - int yindex; - int res; - int slots; - DdNodePtr *list; - DdNode *sentinel = &(table->sentinel); - - xindex = table->invperm[x]; - yindex = table->invperm[y]; - - /* If the two variables do not interact, we do not want to merge them. */ - if (!cuddTestInteract(table,xindex,yindex)) - return(0); - -#ifdef DD_DEBUG - /* Checks that x and y do not contain just the projection functions. - ** With the test on interaction, these test become redundant, - ** because an isolated projection function does not interact with - ** any other variable. - */ - if (table->subtables[x].keys == 1) { - assert(table->vars[xindex]->ref != 1); - } - if (table->subtables[y].keys == 1) { - assert(table->vars[yindex]->ref != 1); - } -#endif - -#ifdef DD_STATS - extsymmcalls++; -#endif - - arccount = 0; - counter = (int) (table->subtables[x].keys * - (table->symmviolation/100.0) + 0.5); - one = DD_ONE(table); - - slots = table->subtables[x].slots; - list = table->subtables[x].nodelist; - for (i = 0; i < slots; i++) { - f = list[i]; - while (f != sentinel) { - /* Find f1, f0, f11, f10, f01, f00. */ - f1 = cuddT(f); - f0 = Cudd_Regular(cuddE(f)); - comple = Cudd_IsComplement(cuddE(f)); - notproj = f1 != one || f0 != one || f->ref != (DdHalfWord) 1; - if (f1->index == yindex) { - arccount++; - f11 = cuddT(f1); f10 = cuddE(f1); - } else { - if ((int) f0->index != yindex) { - /* If f is an isolated projection function it is - ** allowed to bypass layer y. - */ - if (notproj) { - if (counter == 0) - return(0); - counter--; /* f bypasses layer y */ - } - } - f11 = f10 = f1; - } - if ((int) f0->index == yindex) { - arccount++; - f01 = cuddT(f0); f00 = cuddE(f0); - } else { - f01 = f00 = f0; - } - if (comple) { - f01 = Cudd_Not(f01); - f00 = Cudd_Not(f00); - } - - /* Unless we are looking at a projection function - ** without external references except the one from the - ** table, we insist that f01 == f10 or f11 == f00 - */ - if (notproj) { - if (f01 != f10 && f11 != f00) { - if (counter == 0) - return(0); - counter--; - } - } - - f = f->next; - } /* while */ - } /* for */ - - /* Calculate the total reference counts of y */ - TotalRefCount = -1; /* -1 for projection function */ - slots = table->subtables[y].slots; - list = table->subtables[y].nodelist; - for (i = 0; i < slots; i++) { - f = list[i]; - while (f != sentinel) { - TotalRefCount += f->ref; - f = f->next; - } - } - - arccounter = (int) (table->subtables[y].keys * - (table->arcviolation/100.0) + 0.5); - res = arccount >= TotalRefCount - arccounter; - -#if defined(DD_DEBUG) && defined(DD_VERBOSE) - if (res) { - (void) fprintf(table->out, - "Found extended symmetry! x = %d\ty = %d\tPos(%d,%d)\n", - xindex,yindex,x,y); - } -#endif - -#ifdef DD_STATS - if (res) - extsymm++; -#endif - return(res); - -} /* end ddExtSymmCheck */ - - -/**Function******************************************************************** - - Synopsis [Checks for grouping of x and y.] - - Description [Checks for grouping of x and y. Returns 1 in - case of grouping; 0 otherwise. This function is used for lazy sifting.] - - SideEffects [None] - -******************************************************************************/ -static int -ddVarGroupCheck( - DdManager * table, - int x, - int y) -{ - int xindex = table->invperm[x]; - int yindex = table->invperm[y]; - - if (Cudd_bddIsVarToBeUngrouped(table, xindex)) return(0); - - if (Cudd_bddReadPairIndex(table, xindex) == yindex) { - if (ddIsVarHandled(table, xindex) || - ddIsVarHandled(table, yindex)) { - if (Cudd_bddIsVarToBeGrouped(table, xindex) || - Cudd_bddIsVarToBeGrouped(table, yindex) ) { - if (table->keys - table->isolated <= originalSize) { - return(1); - } - } - } - } - - return(0); - -} /* end of ddVarGroupCheck */ - - -/**Function******************************************************************** - - Synopsis [Sets a variable to already handled.] - - Description [Sets a variable to already handled. This function is used - for lazy sifting.] - - SideEffects [none] - - SeeAlso [] - -******************************************************************************/ -static int -ddSetVarHandled( - DdManager *dd, - int index) -{ - if (index >= dd->size || index < 0) return(0); - dd->subtables[dd->perm[index]].varHandled = 1; - return(1); - -} /* end of ddSetVarHandled */ - - -/**Function******************************************************************** - - Synopsis [Resets a variable to be processed.] - - Description [Resets a variable to be processed. This function is used - for lazy sifting.] - - SideEffects [none] - - SeeAlso [] - -******************************************************************************/ -static int -ddResetVarHandled( - DdManager *dd, - int index) -{ - if (index >= dd->size || index < 0) return(0); - dd->subtables[dd->perm[index]].varHandled = 0; - return(1); - -} /* end of ddResetVarHandled */ - - -/**Function******************************************************************** - - Synopsis [Checks whether a variables is already handled.] - - Description [Checks whether a variables is already handled. This - function is used for lazy sifting.] - - SideEffects [none] - - SeeAlso [] - -******************************************************************************/ -static int -ddIsVarHandled( - DdManager *dd, - int index) -{ - if (index >= dd->size || index < 0) return(-1); - return dd->subtables[dd->perm[index]].varHandled; - -} /* end of ddIsVarHandled */ |