/**CFile***********************************************************************
FileName [cuddGroup.c]
PackageName [cudd]
Synopsis [Functions for group sifting.]
Description [External procedures included in this file:
<ul>
<li> Cudd_MakeTreeNode()
</ul>
Internal procedures included in this file:
<ul>
<li> cuddTreeSifting()
</ul>
Static procedures included in this module:
<ul>
<li> ddTreeSiftingAux()
<li> ddCountInternalMtrNodes()
<li> ddReorderChildren()
<li> ddFindNodeHiLo()
<li> ddUniqueCompareGroup()
<li> ddGroupSifting()
<li> ddCreateGroup()
<li> ddGroupSiftingAux()
<li> ddGroupSiftingUp()
<li> ddGroupSiftingDown()
<li> ddGroupMove()
<li> ddGroupMoveBackward()
<li> ddGroupSiftingBackward()
<li> ddMergeGroups()
<li> ddDissolveGroup()
<li> ddNoCheck()
<li> ddSecDiffCheck()
<li> ddExtSymmCheck()
<li> ddVarGroupCheck()
<li> ddSetVarHandled()
<li> ddResetVarHandled()
<li> ddIsVarHandled()
</ul>]
Author [Shipra Panda, Fabio Somenzi]
Copyright [This file was created at the University of Colorado at
Boulder. The University of Colorado at Boulder makes no warranty
about the suitability of this software for any purpose. It is
presented on an AS IS basis.]
******************************************************************************/
#include "util_hack.h"
#include "cuddInt.h"
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 */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
/* 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, int TimeStop));
#ifdef DD_STATS
static int ddCountInternalMtrNodes ARGS((DdManager *table, MtrNode *treenode));
#endif
static int ddReorderChildren ARGS((DdManager *table, MtrNode *treenode, Cudd_ReorderingType method, int TimeStop));
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 TimeStop)
{
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, TimeStop);
#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,
int TimeStop)
{
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, TimeStop))
return(0);
saveCheck = table->groupcheck;
table->groupcheck = CUDD_NO_CHECK;
if (method != CUDD_REORDER_LAZY_SIFT)
res = ddReorderChildren(table, auxnode, CUDD_REORDER_GROUP_SIFT, TimeStop);
else
res = ddReorderChildren(table, auxnode, CUDD_REORDER_LAZY_SIFT, TimeStop);
table->groupcheck = saveCheck;
if (res == 0)
return(0);
} else if (auxnode->size > 1) {
if (!ddReorderChildren(table, auxnode, method, TimeStop))
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 TimeStop)
{
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,TimeStop);
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 = 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),
(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 */
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,
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=-1,swapy=-1; // Suppress "might be used uninitialized"
#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 = NULL;
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 <= (unsigned)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