| /**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 [Copyright (c) 1995-2004, Regents of the University of Colorado |
| |
| All rights reserved. |
| |
| Redistribution and use in source and binary forms, with or without |
| modification, are permitted provided that the following conditions |
| are met: |
| |
| Redistributions of source code must retain the above copyright |
| notice, this list of conditions and the following disclaimer. |
| |
| Redistributions in binary form must reproduce the above copyright |
| notice, this list of conditions and the following disclaimer in the |
| documentation and/or other materials provided with the distribution. |
| |
| Neither the name of the University of Colorado nor the names of its |
| contributors may be used to endorse or promote products derived from |
| this software without specific prior written permission. |
| |
| THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS |
| "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT |
| LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS |
| FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE |
| COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, |
| INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, |
| BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; |
| LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER |
| CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT |
| LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN |
| ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE |
| POSSIBILITY OF SUCH DAMAGE.] |
| |
| ******************************************************************************/ |
| |
| #include "misc/util/util_hack.h" |
| #include "cuddInt.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| |
| /*---------------------------------------------------------------------------*/ |
| /* 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 */ |
| /*---------------------------------------------------------------------------*/ |
| |
| typedef int (*DD_CHKFP)(DdManager *, int, int); |
| |
| /*---------------------------------------------------------------------------*/ |
| /* Variable declarations */ |
| /*---------------------------------------------------------------------------*/ |
| |
| #ifndef lint |
| static char rcsid[] DD_UNUSED = "$Id: cuddGroup.c,v 1.44 2009/02/21 18:24:10 fabio 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 unsigned int originalSize; |
| |
| /*---------------------------------------------------------------------------*/ |
| /* Macro declarations */ |
| /*---------------------------------------------------------------------------*/ |
| |
| /**AutomaticStart*************************************************************/ |
| |
| /*---------------------------------------------------------------------------*/ |
| /* Static function prototypes */ |
| /*---------------------------------------------------------------------------*/ |
| |
| static int ddTreeSiftingAux (DdManager *table, MtrNode *treenode, Cudd_ReorderingType method); |
| #ifdef DD_STATS |
| static int ddCountInternalMtrNodes (DdManager *table, MtrNode *treenode); |
| #endif |
| static int ddReorderChildren (DdManager *table, MtrNode *treenode, Cudd_ReorderingType method); |
| static void ddFindNodeHiLo (DdManager *table, MtrNode *treenode, int *lower, int *upper); |
| static int ddUniqueCompareGroup (int *ptrX, int *ptrY); |
| static int ddGroupSifting (DdManager *table, int lower, int upper, DD_CHKFP checkFunction, int lazyFlag); |
| static void ddCreateGroup (DdManager *table, int x, int y); |
| static int ddGroupSiftingAux (DdManager *table, int x, int xLow, int xHigh, DD_CHKFP checkFunction, int lazyFlag); |
| static int ddGroupSiftingUp (DdManager *table, int y, int xLow, DD_CHKFP checkFunction, Move **moves); |
| static int ddGroupSiftingDown (DdManager *table, int x, int xHigh, DD_CHKFP checkFunction, Move **moves); |
| static int ddGroupMove (DdManager *table, int x, int y, Move **moves); |
| static int ddGroupMoveBackward (DdManager *table, int x, int y); |
| static int ddGroupSiftingBackward (DdManager *table, Move *moves, int size, int upFlag, int lazyFlag); |
| static void ddMergeGroups (DdManager *table, MtrNode *treenode, int low, int high); |
| static void ddDissolveGroup (DdManager *table, int x, int y); |
| static int ddNoCheck (DdManager *table, int x, int y); |
| static int ddSecDiffCheck (DdManager *table, int x, int y); |
| static int ddExtSymmCheck (DdManager *table, int x, int y); |
| static int ddVarGroupCheck (DdManager * table, int x, int y); |
| static int ddSetVarHandled (DdManager *dd, int index); |
| static int ddResetVarHandled (DdManager *dd, int index); |
| static int ddIsVarHandled (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 = -1; |
| 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, |
| DD_CHKFP checkFunction, |
| 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 = ABC_ALLOC(int,nvars); |
| if (var == NULL) { |
| table->errorCode = CUDD_MEMORY_OUT; |
| goto ddGroupSiftingOutOfMem; |
| } |
| entry = ABC_ALLOC(int,nvars); |
| if (entry == NULL) { |
| table->errorCode = CUDD_MEMORY_OUT; |
| goto ddGroupSiftingOutOfMem; |
| } |
| sifted = ABC_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), |
| (DD_QSFP) 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 */ |
| |
| ABC_FREE(sifted); |
| ABC_FREE(var); |
| ABC_FREE(entry); |
| |
| return(1); |
| |
| ddGroupSiftingOutOfMem: |
| if (entry != NULL) ABC_FREE(entry); |
| if (var != NULL) ABC_FREE(var); |
| if (sifted != NULL) ABC_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, |
| DD_CHKFP checkFunction, |
| 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; |
| |
| 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; |
| cuddDeallocMove(table, moves); |
| moves = move; |
| } |
| |
| return(1); |
| |
| ddGroupSiftingAuxOutOfMem: |
| while (moves != NULL) { |
| move = moves->next; |
| cuddDeallocMove(table, 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, |
| DD_CHKFP checkFunction, |
| 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; |
| } |
| } |
| |
| 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; |
| cuddDeallocMove(table, *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, |
| DD_CHKFP checkFunction, |
| 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; |
| } |
| } |
| |
| 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; |
| cuddDeallocMove(table, *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 = -1,swapy = -1; |
| #if defined(DD_DEBUG) && defined(DD_VERBOSE) |
| int initialSize,bestSize; |
| #endif |
| |
| #ifdef 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; |
| cuddDeallocMove(table, *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; |
| |
| |
| #ifdef 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 = NULL; |
| int diff, tmp_diff; |
| int index; |
| unsigned int 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 = |
| (unsigned) 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; |
| unsigned 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 == (unsigned) 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 */ |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
