From 4812c90424dfc40d26725244723887a2d16ddfd9 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 1 Oct 2007 08:01:00 -0700 Subject: Version abc71001 --- src/bdd/cudd/cuddGroup.c | 2142 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 2142 insertions(+) create mode 100644 src/bdd/cudd/cuddGroup.c (limited to 'src/bdd/cudd/cuddGroup.c') diff --git a/src/bdd/cudd/cuddGroup.c b/src/bdd/cudd/cuddGroup.c new file mode 100644 index 00000000..81c05d2c --- /dev/null +++ b/src/bdd/cudd/cuddGroup.c @@ -0,0 +1,2142 @@ +/**CFile*********************************************************************** + + FileName [cuddGroup.c] + + PackageName [cudd] + + Synopsis [Functions for group sifting.] + + Description [External procedures included in this file: + + Internal procedures included in this file: + + Static procedures included in this module: + ] + + 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 */ -- cgit v1.2.3