summaryrefslogtreecommitdiffstats
path: root/src/bdd/cudd/cuddSymmetry.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/bdd/cudd/cuddSymmetry.c')
-rw-r--r--src/bdd/cudd/cuddSymmetry.c1594
1 files changed, 812 insertions, 782 deletions
diff --git a/src/bdd/cudd/cuddSymmetry.c b/src/bdd/cudd/cuddSymmetry.c
index 535ba978..a7ef7845 100644
--- a/src/bdd/cudd/cuddSymmetry.c
+++ b/src/bdd/cudd/cuddSymmetry.c
@@ -7,34 +7,61 @@
Synopsis [Functions for symmetry-based variable reordering.]
Description [External procedures included in this file:
- <ul>
- <li> Cudd_SymmProfile()
- </ul>
- Internal procedures included in this module:
- <ul>
- <li> cuddSymmCheck()
- <li> cuddSymmSifting()
- <li> cuddSymmSiftingConv()
- </ul>
- Static procedures included in this module:
- <ul>
- <li> ddSymmUniqueCompare()
- <li> ddSymmSiftingAux()
- <li> ddSymmSiftingConvAux()
- <li> ddSymmSiftingUp()
- <li> ddSymmSiftingDown()
- <li> ddSymmGroupMove()
- <li> ddSymmGroupMoveBackward()
- <li> ddSymmSiftingBackward()
- <li> ddSymmSummary()
- </ul>]
+ <ul>
+ <li> Cudd_SymmProfile()
+ </ul>
+ Internal procedures included in this module:
+ <ul>
+ <li> cuddSymmCheck()
+ <li> cuddSymmSifting()
+ <li> cuddSymmSiftingConv()
+ </ul>
+ Static procedures included in this module:
+ <ul>
+ <li> ddSymmUniqueCompare()
+ <li> ddSymmSiftingAux()
+ <li> ddSymmSiftingConvAux()
+ <li> ddSymmSiftingUp()
+ <li> ddSymmSiftingDown()
+ <li> ddSymmGroupMove()
+ <li> ddSymmGroupMoveBackward()
+ <li> ddSymmSiftingBackward()
+ <li> ddSymmSummary()
+ </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.]
+ Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
+
+ All rights reserved.
+
+ Redistribution and use in source and binary forms, with or without
+ modification, are permitted provided that the following conditions
+ are met:
+
+ Redistributions of source code must retain the above copyright
+ notice, this list of conditions and the following disclaimer.
+
+ Redistributions in binary form must reproduce the above copyright
+ notice, this list of conditions and the following disclaimer in the
+ documentation and/or other materials provided with the distribution.
+
+ Neither the name of the University of Colorado nor the names of its
+ contributors may be used to endorse or promote products derived from
+ this software without specific prior written permission.
+
+ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
+ FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
+ COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
+ INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
+ BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+ LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+ CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+ LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
+ ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ POSSIBILITY OF SUCH DAMAGE.]
******************************************************************************/
@@ -44,6 +71,7 @@
ABC_NAMESPACE_IMPL_START
+
/*---------------------------------------------------------------------------*/
/* Constant declarations */
/*---------------------------------------------------------------------------*/
@@ -63,14 +91,14 @@ ABC_NAMESPACE_IMPL_START
/*---------------------------------------------------------------------------*/
#ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddSymmetry.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $";
+static char rcsid[] DD_UNUSED = "$Id: cuddSymmetry.c,v 1.26 2009/02/19 16:23:54 fabio Exp $";
#endif
-static int *entry;
+static int *entry;
-extern int ddTotalNumberSwapping;
+extern int ddTotalNumberSwapping;
#ifdef DD_STATS
-extern int ddTotalNISwaps;
+extern int ddTotalNISwaps;
#endif
/*---------------------------------------------------------------------------*/
@@ -83,15 +111,15 @@ extern int ddTotalNISwaps;
/* Static function prototypes */
/*---------------------------------------------------------------------------*/
-static int ddSymmUniqueCompare ARGS((int *ptrX, int *ptrY));
-static int ddSymmSiftingAux ARGS((DdManager *table, int x, int xLow, int xHigh));
-static int ddSymmSiftingConvAux ARGS((DdManager *table, int x, int xLow, int xHigh));
-static Move * ddSymmSiftingUp ARGS((DdManager *table, int y, int xLow));
-static Move * ddSymmSiftingDown ARGS((DdManager *table, int x, int xHigh));
-static int ddSymmGroupMove ARGS((DdManager *table, int x, int y, Move **moves));
-static int ddSymmGroupMoveBackward ARGS((DdManager *table, int x, int y));
-static int ddSymmSiftingBackward ARGS((DdManager *table, Move *moves, int size));
-static void ddSymmSummary ARGS((DdManager *table, int lower, int upper, int *symvars, int *symgroups));
+static int ddSymmUniqueCompare (int *ptrX, int *ptrY);
+static int ddSymmSiftingAux (DdManager *table, int x, int xLow, int xHigh);
+static int ddSymmSiftingConvAux (DdManager *table, int x, int xLow, int xHigh);
+static Move * ddSymmSiftingUp (DdManager *table, int y, int xLow);
+static Move * ddSymmSiftingDown (DdManager *table, int x, int xHigh);
+static int ddSymmGroupMove (DdManager *table, int x, int y, Move **moves);
+static int ddSymmGroupMoveBackward (DdManager *table, int x, int y);
+static int ddSymmSiftingBackward (DdManager *table, Move *moves, int size);
+static void ddSymmSummary (DdManager *table, int lower, int upper, int *symvars, int *symgroups);
/**AutomaticEnd***************************************************************/
@@ -121,22 +149,22 @@ Cudd_SymmProfile(
int TotalSymmGroups = 0;
for (i = lower; i <= upper; i++) {
- if (table->subtables[i].next != (unsigned) i) {
- x = i;
- (void) fprintf(table->out,"Group:");
- do {
- (void) fprintf(table->out," %d",table->invperm[x]);
- TotalSymm++;
- gbot = x;
- x = table->subtables[x].next;
- } while (x != i);
- TotalSymmGroups++;
+ if (table->subtables[i].next != (unsigned) i) {
+ x = i;
+ (void) fprintf(table->out,"Group:");
+ do {
+ (void) fprintf(table->out," %d",table->invperm[x]);
+ TotalSymm++;
+ gbot = x;
+ x = table->subtables[x].next;
+ } while (x != i);
+ TotalSymmGroups++;
#ifdef DD_DEBUG
- assert(table->subtables[gbot].next == (unsigned) i);
+ assert(table->subtables[gbot].next == (unsigned) i);
#endif
- i = gbot;
- (void) fprintf(table->out,"\n");
- }
+ i = gbot;
+ (void) fprintf(table->out,"\n");
+ }
}
(void) fprintf(table->out,"Total Symmetric = %d\n",TotalSymm);
(void) fprintf(table->out,"Total Groups = %d\n",TotalSymmGroups);
@@ -167,11 +195,11 @@ cuddSymmCheck(
int y)
{
DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10;
- int comple; /* f0 is complemented */
- int xsymmy; /* x and y may be positively symmetric */
- int xsymmyp; /* x and y may be negatively symmetric */
- int arccount; /* number of arcs from layer x to layer y */
- int TotalRefCount; /* total reference count of layer y minus 1 */
+ int comple; /* f0 is complemented */
+ int xsymmy; /* x and y may be positively symmetric */
+ int xsymmyp; /* x and y may be negatively symmetric */
+ int arccount; /* number of arcs from layer x to layer y */
+ int TotalRefCount; /* total reference count of layer y minus 1 */
int yindex;
int i;
DdNodePtr *list;
@@ -188,12 +216,12 @@ cuddSymmCheck(
** function, it has one arc coming from a layer different from x.
*/
if (table->subtables[x].keys == 1) {
- return(0);
+ return(0);
}
yindex = table->invperm[y];
if (table->subtables[y].keys == 1) {
- if (table->vars[yindex]->ref == 1)
- return(0);
+ if (table->vars[yindex]->ref == 1)
+ return(0);
}
xsymmy = xsymmyp = 1;
@@ -201,45 +229,45 @@ cuddSymmCheck(
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));
- if ((int) 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 (f1 != DD_ONE(table) || f0 != DD_ONE(table) || f->ref != 1)
- return(0); /* 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);
- }
-
- if (f1 != DD_ONE(table) || f0 != DD_ONE(table) || f->ref != 1) {
- xsymmy &= f01 == f10;
- xsymmyp &= f11 == f00;
- if ((xsymmy == 0) && (xsymmyp == 0))
- return(0);
- }
-
- f = f->next;
- } /* while */
+ 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));
+ if ((int) 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 (f1 != DD_ONE(table) || f0 != DD_ONE(table) || f->ref != 1)
+ return(0); /* 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);
+ }
+
+ if (f1 != DD_ONE(table) || f0 != DD_ONE(table) || f->ref != 1) {
+ xsymmy &= f01 == f10;
+ xsymmyp &= f11 == f00;
+ if ((xsymmy == 0) && (xsymmyp == 0))
+ return(0);
+ }
+
+ f = f->next;
+ } /* while */
} /* for */
/* Calculate the total reference counts of y */
@@ -247,19 +275,19 @@ cuddSymmCheck(
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;
- }
+ f = list[i];
+ while (f != sentinel) {
+ TotalRefCount += f->ref;
+ f = f->next;
+ }
}
#if defined(DD_DEBUG) && defined(DD_VERBOSE)
if (arccount == TotalRefCount) {
- xindex = table->invperm[x];
- (void) fprintf(table->out,
- "Found symmetry! x =%d\ty = %d\tPos(%d,%d)\n",
- xindex,yindex,x,y);
+ xindex = table->invperm[x];
+ (void) fprintf(table->out,
+ "Found symmetry! x =%d\ty = %d\tPos(%d,%d)\n",
+ xindex,yindex,x,y);
}
#endif
@@ -294,18 +322,17 @@ int
cuddSymmSifting(
DdManager * table,
int lower,
- int upper,
- int TimeStop)
+ int upper)
{
- int i;
- int *var;
- int size;
- int x;
- int result;
- int symvars;
- int symgroups;
+ int i;
+ int *var;
+ int size;
+ int x;
+ int result;
+ int symvars;
+ int symgroups;
#ifdef DD_STATS
- int previousSize;
+ int previousSize;
#endif
size = table->size;
@@ -314,53 +341,54 @@ cuddSymmSifting(
var = NULL;
entry = ABC_ALLOC(int,size);
if (entry == NULL) {
- table->errorCode = CUDD_MEMORY_OUT;
- goto ddSymmSiftingOutOfMem;
+ table->errorCode = CUDD_MEMORY_OUT;
+ goto ddSymmSiftingOutOfMem;
}
var = ABC_ALLOC(int,size);
if (var == NULL) {
- table->errorCode = CUDD_MEMORY_OUT;
- goto ddSymmSiftingOutOfMem;
+ table->errorCode = CUDD_MEMORY_OUT;
+ goto ddSymmSiftingOutOfMem;
}
for (i = 0; i < size; i++) {
- x = table->perm[i];
- entry[i] = table->subtables[x].keys;
- var[i] = i;
+ x = table->perm[i];
+ entry[i] = table->subtables[x].keys;
+ var[i] = i;
}
- qsort((void *)var,size,sizeof(int),(int (*)(const void *, const void *))ddSymmUniqueCompare);
+ qsort((void *)var,size,sizeof(int),(DD_QSFP)ddSymmUniqueCompare);
/* Initialize the symmetry of each subtable to itself. */
for (i = lower; i <= upper; i++) {
- table->subtables[i].next = i;
+ table->subtables[i].next = i;
}
for (i = 0; i < ddMin(table->siftMaxVar,size); i++) {
- if (ddTotalNumberSwapping >= table->siftMaxSwap)
- break;
- if ( TimeStop && TimeStop < clock() )
- break;
- x = table->perm[var[i]];
+ if (ddTotalNumberSwapping >= table->siftMaxSwap)
+ break;
+ // enable timeout during variable reodering - alanmi 2/13/11
+ if ( table->TimeStop && table->TimeStop < clock() )
+ break;
+ x = table->perm[var[i]];
#ifdef DD_STATS
- previousSize = table->keys - table->isolated;
+ previousSize = table->keys - table->isolated;
#endif
- if (x < lower || x > upper) continue;
- if (table->subtables[x].next == (unsigned) x) {
- result = ddSymmSiftingAux(table,x,lower,upper);
- if (!result) goto ddSymmSiftingOutOfMem;
+ if (x < lower || x > upper) continue;
+ if (table->subtables[x].next == (unsigned) x) {
+ result = ddSymmSiftingAux(table,x,lower,upper);
+ if (!result) goto ddSymmSiftingOutOfMem;
#ifdef DD_STATS
- if (table->keys < (unsigned) previousSize + table->isolated) {
- (void) fprintf(table->out,"-");
- } else if (table->keys > (unsigned) previousSize +
- table->isolated) {
- (void) fprintf(table->out,"+"); /* should never happen */
- } else {
- (void) fprintf(table->out,"=");
- }
- fflush(table->out);
+ if (table->keys < (unsigned) previousSize + table->isolated) {
+ (void) fprintf(table->out,"-");
+ } else if (table->keys > (unsigned) previousSize +
+ table->isolated) {
+ (void) fprintf(table->out,"+"); /* should never happen */
+ } else {
+ (void) fprintf(table->out,"=");
+ }
+ fflush(table->out);
#endif
- }
+ }
}
ABC_FREE(var);
@@ -370,9 +398,9 @@ cuddSymmSifting(
#ifdef DD_STATS
(void) fprintf(table->out, "\n#:S_SIFTING %8d: symmetric variables\n",
- symvars);
+ symvars);
(void) fprintf(table->out, "#:G_SIFTING %8d: symmetric groups",
- symgroups);
+ symgroups);
#endif
return(1+symvars);
@@ -416,17 +444,17 @@ cuddSymmSiftingConv(
int lower,
int upper)
{
- int i;
- int *var;
- int size;
- int x;
- int result;
- int symvars;
- int symgroups;
- int classes;
- int initialSize;
+ int i;
+ int *var;
+ int size;
+ int x;
+ int result;
+ int symvars;
+ int symgroups;
+ int classes;
+ int initialSize;
#ifdef DD_STATS
- int previousSize;
+ int previousSize;
#endif
initialSize = table->keys - table->isolated;
@@ -437,111 +465,111 @@ cuddSymmSiftingConv(
var = NULL;
entry = ABC_ALLOC(int,size);
if (entry == NULL) {
- table->errorCode = CUDD_MEMORY_OUT;
- goto ddSymmSiftingConvOutOfMem;
+ table->errorCode = CUDD_MEMORY_OUT;
+ goto ddSymmSiftingConvOutOfMem;
}
var = ABC_ALLOC(int,size);
if (var == NULL) {
- table->errorCode = CUDD_MEMORY_OUT;
- goto ddSymmSiftingConvOutOfMem;
+ table->errorCode = CUDD_MEMORY_OUT;
+ goto ddSymmSiftingConvOutOfMem;
}
for (i = 0; i < size; i++) {
- x = table->perm[i];
- entry[i] = table->subtables[x].keys;
- var[i] = i;
+ x = table->perm[i];
+ entry[i] = table->subtables[x].keys;
+ var[i] = i;
}
- qsort((void *)var,size,sizeof(int),(int (*)(const void *, const void *))ddSymmUniqueCompare);
+ qsort((void *)var,size,sizeof(int),(DD_QSFP)ddSymmUniqueCompare);
/* Initialize the symmetry of each subtable to itself
** for first pass of converging symmetric sifting.
*/
for (i = lower; i <= upper; i++) {
- table->subtables[i].next = i;
+ table->subtables[i].next = i;
}
for (i = 0; i < ddMin(table->siftMaxVar, table->size); i++) {
- if (ddTotalNumberSwapping >= table->siftMaxSwap)
- break;
- x = table->perm[var[i]];
- if (x < lower || x > upper) continue;
- /* Only sift if not in symmetry group already. */
- if (table->subtables[x].next == (unsigned) x) {
+ if (ddTotalNumberSwapping >= table->siftMaxSwap)
+ break;
+ x = table->perm[var[i]];
+ if (x < lower || x > upper) continue;
+ /* Only sift if not in symmetry group already. */
+ if (table->subtables[x].next == (unsigned) x) {
#ifdef DD_STATS
- previousSize = table->keys - table->isolated;
+ previousSize = table->keys - table->isolated;
#endif
- result = ddSymmSiftingAux(table,x,lower,upper);
- if (!result) goto ddSymmSiftingConvOutOfMem;
+ result = ddSymmSiftingAux(table,x,lower,upper);
+ if (!result) goto ddSymmSiftingConvOutOfMem;
#ifdef DD_STATS
- if (table->keys < (unsigned) previousSize + table->isolated) {
- (void) fprintf(table->out,"-");
- } else if (table->keys > (unsigned) previousSize +
- table->isolated) {
- (void) fprintf(table->out,"+");
- } else {
- (void) fprintf(table->out,"=");
- }
- fflush(table->out);
+ if (table->keys < (unsigned) previousSize + table->isolated) {
+ (void) fprintf(table->out,"-");
+ } else if (table->keys > (unsigned) previousSize +
+ table->isolated) {
+ (void) fprintf(table->out,"+");
+ } else {
+ (void) fprintf(table->out,"=");
+ }
+ fflush(table->out);
#endif
- }
+ }
}
/* Sifting now until convergence. */
while ((unsigned) initialSize > table->keys - table->isolated) {
- initialSize = table->keys - table->isolated;
+ initialSize = table->keys - table->isolated;
#ifdef DD_STATS
- (void) fprintf(table->out,"\n");
+ (void) fprintf(table->out,"\n");
#endif
/* Here we consider only one representative for each symmetry class. */
- for (x = lower, classes = 0; x <= upper; x++, classes++) {
- while ((unsigned) x < table->subtables[x].next) {
- x = table->subtables[x].next;
+ for (x = lower, classes = 0; x <= upper; x++, classes++) {
+ while ((unsigned) x < table->subtables[x].next) {
+ x = table->subtables[x].next;
+ }
+ /* Here x is the largest index in a group.
+ ** Groups consist of adjacent variables.
+ ** Hence, the next increment of x will move it to a new group.
+ */
+ i = table->invperm[x];
+ entry[i] = table->subtables[x].keys;
+ var[classes] = i;
}
- /* Here x is the largest index in a group.
- ** Groups consist of adjacent variables.
- ** Hence, the next increment of x will move it to a new group.
- */
- i = table->invperm[x];
- entry[i] = table->subtables[x].keys;
- var[classes] = i;
- }
- qsort((void *)var,classes,sizeof(int),(int (*)(const void *, const void *))ddSymmUniqueCompare);
+ qsort((void *)var,classes,sizeof(int),(DD_QSFP)ddSymmUniqueCompare);
- /* Now sift. */
- for (i = 0; i < ddMin(table->siftMaxVar,classes); i++) {
- if (ddTotalNumberSwapping >= table->siftMaxSwap)
- break;
- x = table->perm[var[i]];
- if ((unsigned) x >= table->subtables[x].next) {
+ /* Now sift. */
+ for (i = 0; i < ddMin(table->siftMaxVar,classes); i++) {
+ if (ddTotalNumberSwapping >= table->siftMaxSwap)
+ break;
+ x = table->perm[var[i]];
+ if ((unsigned) x >= table->subtables[x].next) {
#ifdef DD_STATS
- previousSize = table->keys - table->isolated;
+ previousSize = table->keys - table->isolated;
#endif
- result = ddSymmSiftingConvAux(table,x,lower,upper);
- if (!result ) goto ddSymmSiftingConvOutOfMem;
+ result = ddSymmSiftingConvAux(table,x,lower,upper);
+ if (!result ) goto ddSymmSiftingConvOutOfMem;
#ifdef DD_STATS
- if (table->keys < (unsigned) previousSize + table->isolated) {
- (void) fprintf(table->out,"-");
- } else if (table->keys > (unsigned) previousSize +
- table->isolated) {
- (void) fprintf(table->out,"+");
- } else {
- (void) fprintf(table->out,"=");
- }
- fflush(table->out);
+ if (table->keys < (unsigned) previousSize + table->isolated) {
+ (void) fprintf(table->out,"-");
+ } else if (table->keys > (unsigned) previousSize +
+ table->isolated) {
+ (void) fprintf(table->out,"+");
+ } else {
+ (void) fprintf(table->out,"=");
+ }
+ fflush(table->out);
#endif
- }
- } /* for */
+ }
+ } /* for */
}
ddSymmSummary(table, lower, upper, &symvars, &symgroups);
#ifdef DD_STATS
(void) fprintf(table->out, "\n#:S_SIFTING %8d: symmetric variables\n",
- symvars);
+ symvars);
(void) fprintf(table->out, "#:G_SIFTING %8d: symmetric groups",
- symgroups);
+ symgroups);
#endif
ABC_FREE(var);
@@ -583,7 +611,7 @@ ddSymmUniqueCompare(
{
#if 0
if (entry[*ptrY] == entry[*ptrX]) {
- return((*ptrX) - (*ptrY));
+ return((*ptrX) - (*ptrY));
}
#endif
return(entry[*ptrY] - entry[*ptrX]);
@@ -612,12 +640,12 @@ ddSymmSiftingAux(
int xHigh)
{
Move *move;
- Move *moveUp; /* list of up moves */
- Move *moveDown; /* list of down moves */
- int initialSize;
- int result;
+ Move *moveUp; /* list of up moves */
+ Move *moveDown; /* list of down moves */
+ int initialSize;
+ int result;
int i;
- int topbot; /* index to either top or bottom of symmetry group */
+ int topbot; /* index to either top or bottom of symmetry group */
int initGroupSize, finalGroupSize;
@@ -632,259 +660,259 @@ ddSymmSiftingAux(
moveUp = NULL;
if ((x - xLow) > (xHigh - x)) {
- /* Will go down first, unless x == xHigh:
- ** Look for consecutive symmetries above x.
- */
- for (i = x; i > xLow; i--) {
- if (!cuddSymmCheck(table,i-1,i))
- break;
- topbot = table->subtables[i-1].next; /* find top of i-1's group */
- table->subtables[i-1].next = i;
- table->subtables[x].next = topbot; /* x is bottom of group so its */
- /* next is top of i-1's group */
- i = topbot + 1; /* add 1 for i--; new i is top of symm group */
- }
+ /* Will go down first, unless x == xHigh:
+ ** Look for consecutive symmetries above x.
+ */
+ for (i = x; i > xLow; i--) {
+ if (!cuddSymmCheck(table,i-1,i))
+ break;
+ topbot = table->subtables[i-1].next; /* find top of i-1's group */
+ table->subtables[i-1].next = i;
+ table->subtables[x].next = topbot; /* x is bottom of group so its */
+ /* next is top of i-1's group */
+ i = topbot + 1; /* add 1 for i--; new i is top of symm group */
+ }
} else {
- /* Will go up first unless x == xlow:
- ** Look for consecutive symmetries below x.
- */
- for (i = x; i < xHigh; i++) {
- if (!cuddSymmCheck(table,i,i+1))
- break;
- /* find bottom of i+1's symm group */
- topbot = i + 1;
- while ((unsigned) topbot < table->subtables[topbot].next) {
- topbot = table->subtables[topbot].next;
+ /* Will go up first unless x == xlow:
+ ** Look for consecutive symmetries below x.
+ */
+ for (i = x; i < xHigh; i++) {
+ if (!cuddSymmCheck(table,i,i+1))
+ break;
+ /* find bottom of i+1's symm group */
+ topbot = i + 1;
+ while ((unsigned) topbot < table->subtables[topbot].next) {
+ topbot = table->subtables[topbot].next;
+ }
+ table->subtables[topbot].next = table->subtables[i].next;
+ table->subtables[i].next = i + 1;
+ i = topbot - 1; /* subtract 1 for i++; new i is bottom of group */
}
- table->subtables[topbot].next = table->subtables[i].next;
- table->subtables[i].next = i + 1;
- i = topbot - 1; /* subtract 1 for i++; new i is bottom of group */
- }
}
/* Now x may be in the middle of a symmetry group.
** Find bottom of x's symm group.
*/
while ((unsigned) x < table->subtables[x].next)
- x = table->subtables[x].next;
+ x = table->subtables[x].next;
if (x == xLow) { /* Sift down */
#ifdef DD_DEBUG
- /* x must be a singleton */
- assert((unsigned) x == table->subtables[x].next);
+ /* x must be a singleton */
+ assert((unsigned) x == table->subtables[x].next);
#endif
- if (x == xHigh) return(1); /* just one variable */
+ if (x == xHigh) return(1); /* just one variable */
- initGroupSize = 1;
+ initGroupSize = 1;
- moveDown = ddSymmSiftingDown(table,x,xHigh);
- /* after this point x --> xHigh, unless early term */
- if (moveDown == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
- if (moveDown == NULL) return(1);
+ moveDown = ddSymmSiftingDown(table,x,xHigh);
+ /* after this point x --> xHigh, unless early term */
+ if (moveDown == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
+ if (moveDown == NULL) return(1);
- x = moveDown->y;
- /* Find bottom of x's group */
- i = x;
- while ((unsigned) i < table->subtables[i].next) {
- i = table->subtables[i].next;
- }
+ x = moveDown->y;
+ /* Find bottom of x's group */
+ i = x;
+ while ((unsigned) i < table->subtables[i].next) {
+ i = table->subtables[i].next;
+ }
#ifdef DD_DEBUG
- /* x should be the top of the symmetry group and i the bottom */
- assert((unsigned) i >= table->subtables[i].next);
- assert((unsigned) x == table->subtables[i].next);
+ /* x should be the top of the symmetry group and i the bottom */
+ assert((unsigned) i >= table->subtables[i].next);
+ assert((unsigned) x == table->subtables[i].next);
#endif
- finalGroupSize = i - x + 1;
+ finalGroupSize = i - x + 1;
- if (initGroupSize == finalGroupSize) {
- /* No new symmetry groups detected, return to best position */
- result = ddSymmSiftingBackward(table,moveDown,initialSize);
- } else {
- initialSize = table->keys - table->isolated;
- moveUp = ddSymmSiftingUp(table,x,xLow);
- result = ddSymmSiftingBackward(table,moveUp,initialSize);
- }
- if (!result) goto ddSymmSiftingAuxOutOfMem;
+ if (initGroupSize == finalGroupSize) {
+ /* No new symmetry groups detected, return to best position */
+ result = ddSymmSiftingBackward(table,moveDown,initialSize);
+ } else {
+ initialSize = table->keys - table->isolated;
+ moveUp = ddSymmSiftingUp(table,x,xLow);
+ result = ddSymmSiftingBackward(table,moveUp,initialSize);
+ }
+ if (!result) goto ddSymmSiftingAuxOutOfMem;
} else if (cuddNextHigh(table,x) > xHigh) { /* Sift up */
- /* Find top of x's symm group */
- i = x; /* bottom */
- x = table->subtables[x].next; /* top */
+ /* Find top of x's symm group */
+ i = x; /* bottom */
+ x = table->subtables[x].next; /* top */
- if (x == xLow) return(1); /* just one big group */
+ if (x == xLow) return(1); /* just one big group */
- initGroupSize = i - x + 1;
+ initGroupSize = i - x + 1;
- moveUp = ddSymmSiftingUp(table,x,xLow);
- /* after this point x --> xLow, unless early term */
- if (moveUp == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
- if (moveUp == NULL) return(1);
+ moveUp = ddSymmSiftingUp(table,x,xLow);
+ /* after this point x --> xLow, unless early term */
+ if (moveUp == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
+ if (moveUp == NULL) return(1);
- x = moveUp->x;
- /* Find top of x's group */
- i = table->subtables[x].next;
+ x = moveUp->x;
+ /* Find top of x's group */
+ i = table->subtables[x].next;
#ifdef DD_DEBUG
- /* x should be the bottom of the symmetry group and i the top */
- assert((unsigned) x >= table->subtables[x].next);
- assert((unsigned) i == table->subtables[x].next);
+ /* x should be the bottom of the symmetry group and i the top */
+ assert((unsigned) x >= table->subtables[x].next);
+ assert((unsigned) i == table->subtables[x].next);
#endif
- finalGroupSize = x - i + 1;
+ finalGroupSize = x - i + 1;
- if (initGroupSize == finalGroupSize) {
- /* No new symmetry groups detected, return to best position */
- result = ddSymmSiftingBackward(table,moveUp,initialSize);
- } else {
- initialSize = table->keys - table->isolated;
- moveDown = ddSymmSiftingDown(table,x,xHigh);
- result = ddSymmSiftingBackward(table,moveDown,initialSize);
- }
- if (!result) goto ddSymmSiftingAuxOutOfMem;
+ if (initGroupSize == finalGroupSize) {
+ /* No new symmetry groups detected, return to best position */
+ result = ddSymmSiftingBackward(table,moveUp,initialSize);
+ } else {
+ initialSize = table->keys - table->isolated;
+ moveDown = ddSymmSiftingDown(table,x,xHigh);
+ result = ddSymmSiftingBackward(table,moveDown,initialSize);
+ }
+ if (!result) goto ddSymmSiftingAuxOutOfMem;
} else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */
- moveDown = ddSymmSiftingDown(table,x,xHigh);
- /* at this point x == xHigh, unless early term */
- if (moveDown == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
-
- if (moveDown != NULL) {
- x = moveDown->y; /* x is top here */
- i = x;
- while ((unsigned) i < table->subtables[i].next) {
- i = table->subtables[i].next;
- }
- } else {
- i = x;
- while ((unsigned) i < table->subtables[i].next) {
- i = table->subtables[i].next;
+ moveDown = ddSymmSiftingDown(table,x,xHigh);
+ /* at this point x == xHigh, unless early term */
+ if (moveDown == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
+
+ if (moveDown != NULL) {
+ x = moveDown->y; /* x is top here */
+ i = x;
+ while ((unsigned) i < table->subtables[i].next) {
+ i = table->subtables[i].next;
+ }
+ } else {
+ i = x;
+ while ((unsigned) i < table->subtables[i].next) {
+ i = table->subtables[i].next;
+ }
+ x = table->subtables[i].next;
}
- x = table->subtables[i].next;
- }
#ifdef DD_DEBUG
/* x should be the top of the symmetry group and i the bottom */
- assert((unsigned) i >= table->subtables[i].next);
- assert((unsigned) x == table->subtables[i].next);
+ assert((unsigned) i >= table->subtables[i].next);
+ assert((unsigned) x == table->subtables[i].next);
#endif
- initGroupSize = i - x + 1;
+ initGroupSize = i - x + 1;
- moveUp = ddSymmSiftingUp(table,x,xLow);
- if (moveUp == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
+ moveUp = ddSymmSiftingUp(table,x,xLow);
+ if (moveUp == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
- if (moveUp != NULL) {
- x = moveUp->x;
- i = table->subtables[x].next;
- } else {
- i = x;
- while ((unsigned) x < table->subtables[x].next)
- x = table->subtables[x].next;
- }
+ if (moveUp != NULL) {
+ x = moveUp->x;
+ i = table->subtables[x].next;
+ } else {
+ i = x;
+ while ((unsigned) x < table->subtables[x].next)
+ x = table->subtables[x].next;
+ }
#ifdef DD_DEBUG
- /* x should be the bottom of the symmetry group and i the top */
- assert((unsigned) x >= table->subtables[x].next);
- assert((unsigned) i == table->subtables[x].next);
+ /* x should be the bottom of the symmetry group and i the top */
+ assert((unsigned) x >= table->subtables[x].next);
+ assert((unsigned) i == table->subtables[x].next);
#endif
- finalGroupSize = x - i + 1;
+ finalGroupSize = x - i + 1;
- if (initGroupSize == finalGroupSize) {
- /* No new symmetry groups detected, return to best position */
- result = ddSymmSiftingBackward(table,moveUp,initialSize);
- } else {
- while (moveDown != NULL) {
- move = moveDown->next;
- cuddDeallocNode(table, (DdNode *) moveDown);
- moveDown = move;
+ if (initGroupSize == finalGroupSize) {
+ /* No new symmetry groups detected, return to best position */
+ result = ddSymmSiftingBackward(table,moveUp,initialSize);
+ } else {
+ while (moveDown != NULL) {
+ move = moveDown->next;
+ cuddDeallocMove(table, moveDown);
+ moveDown = move;
+ }
+ initialSize = table->keys - table->isolated;
+ moveDown = ddSymmSiftingDown(table,x,xHigh);
+ result = ddSymmSiftingBackward(table,moveDown,initialSize);
}
- initialSize = table->keys - table->isolated;
- moveDown = ddSymmSiftingDown(table,x,xHigh);
- result = ddSymmSiftingBackward(table,moveDown,initialSize);
- }
- if (!result) goto ddSymmSiftingAuxOutOfMem;
+ if (!result) goto ddSymmSiftingAuxOutOfMem;
} else { /* moving up first: shorter */
/* Find top of x's symmetry group */
- x = table->subtables[x].next;
+ x = table->subtables[x].next;
- moveUp = ddSymmSiftingUp(table,x,xLow);
- /* at this point x == xHigh, unless early term */
- if (moveUp == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
+ moveUp = ddSymmSiftingUp(table,x,xLow);
+ /* at this point x == xHigh, unless early term */
+ if (moveUp == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
- if (moveUp != NULL) {
- x = moveUp->x;
- i = table->subtables[x].next;
- } else {
- while ((unsigned) x < table->subtables[x].next)
- x = table->subtables[x].next;
- i = table->subtables[x].next;
- }
+ if (moveUp != NULL) {
+ x = moveUp->x;
+ i = table->subtables[x].next;
+ } else {
+ while ((unsigned) x < table->subtables[x].next)
+ x = table->subtables[x].next;
+ i = table->subtables[x].next;
+ }
#ifdef DD_DEBUG
/* x is bottom of the symmetry group and i is top */
- assert((unsigned) x >= table->subtables[x].next);
- assert((unsigned) i == table->subtables[x].next);
+ assert((unsigned) x >= table->subtables[x].next);
+ assert((unsigned) i == table->subtables[x].next);
#endif
- initGroupSize = x - i + 1;
-
- moveDown = ddSymmSiftingDown(table,x,xHigh);
- if (moveDown == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
+ initGroupSize = x - i + 1;
- if (moveDown != NULL) {
- x = moveDown->y;
- i = x;
- while ((unsigned) i < table->subtables[i].next) {
- i = table->subtables[i].next;
+ moveDown = ddSymmSiftingDown(table,x,xHigh);
+ if (moveDown == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
+
+ if (moveDown != NULL) {
+ x = moveDown->y;
+ i = x;
+ while ((unsigned) i < table->subtables[i].next) {
+ i = table->subtables[i].next;
+ }
+ } else {
+ i = x;
+ x = table->subtables[x].next;
}
- } else {
- i = x;
- x = table->subtables[x].next;
- }
#ifdef DD_DEBUG
- /* x should be the top of the symmetry group and i the bottom */
- assert((unsigned) i >= table->subtables[i].next);
- assert((unsigned) x == table->subtables[i].next);
+ /* x should be the top of the symmetry group and i the bottom */
+ assert((unsigned) i >= table->subtables[i].next);
+ assert((unsigned) x == table->subtables[i].next);
#endif
- finalGroupSize = i - x + 1;
+ finalGroupSize = i - x + 1;
- if (initGroupSize == finalGroupSize) {
- /* No new symmetries detected, go back to best position */
- result = ddSymmSiftingBackward(table,moveDown,initialSize);
- } else {
- while (moveUp != NULL) {
- move = moveUp->next;
- cuddDeallocNode(table, (DdNode *) moveUp);
- moveUp = move;
+ if (initGroupSize == finalGroupSize) {
+ /* No new symmetries detected, go back to best position */
+ result = ddSymmSiftingBackward(table,moveDown,initialSize);
+ } else {
+ while (moveUp != NULL) {
+ move = moveUp->next;
+ cuddDeallocMove(table, moveUp);
+ moveUp = move;
+ }
+ initialSize = table->keys - table->isolated;
+ moveUp = ddSymmSiftingUp(table,x,xLow);
+ result = ddSymmSiftingBackward(table,moveUp,initialSize);
}
- initialSize = table->keys - table->isolated;
- moveUp = ddSymmSiftingUp(table,x,xLow);
- result = ddSymmSiftingBackward(table,moveUp,initialSize);
- }
- if (!result) goto ddSymmSiftingAuxOutOfMem;
+ if (!result) goto ddSymmSiftingAuxOutOfMem;
}
while (moveDown != NULL) {
- move = moveDown->next;
- cuddDeallocNode(table, (DdNode *) moveDown);
- moveDown = move;
+ move = moveDown->next;
+ cuddDeallocMove(table, moveDown);
+ moveDown = move;
}
while (moveUp != NULL) {
- move = moveUp->next;
- cuddDeallocNode(table, (DdNode *) moveUp);
- moveUp = move;
+ move = moveUp->next;
+ cuddDeallocMove(table, moveUp);
+ moveUp = move;
}
return(1);
ddSymmSiftingAuxOutOfMem:
if (moveDown != MV_OOM) {
- while (moveDown != NULL) {
- move = moveDown->next;
- cuddDeallocNode(table, (DdNode *) moveDown);
- moveDown = move;
- }
+ while (moveDown != NULL) {
+ move = moveDown->next;
+ cuddDeallocMove(table, moveDown);
+ moveDown = move;
+ }
}
if (moveUp != MV_OOM) {
- while (moveUp != NULL) {
- move = moveUp->next;
- cuddDeallocNode(table, (DdNode *) moveUp);
- moveUp = move;
- }
+ while (moveUp != NULL) {
+ move = moveUp->next;
+ cuddDeallocMove(table, moveUp);
+ moveUp = move;
+ }
}
return(0);
@@ -914,10 +942,10 @@ ddSymmSiftingConvAux(
int xHigh)
{
Move *move;
- Move *moveUp; /* list of up moves */
- Move *moveDown; /* list of down moves */
- int initialSize;
- int result;
+ Move *moveUp; /* list of up moves */
+ Move *moveDown; /* list of down moves */
+ int initialSize;
+ int result;
int i;
int initGroupSize, finalGroupSize;
@@ -929,148 +957,148 @@ ddSymmSiftingConvAux(
if (x == xLow) { /* Sift down */
#ifdef DD_DEBUG
- /* x is bottom of symmetry group */
- assert((unsigned) x >= table->subtables[x].next);
+ /* x is bottom of symmetry group */
+ assert((unsigned) x >= table->subtables[x].next);
#endif
i = table->subtables[x].next;
- initGroupSize = x - i + 1;
+ initGroupSize = x - i + 1;
- moveDown = ddSymmSiftingDown(table,x,xHigh);
- /* at this point x == xHigh, unless early term */
- if (moveDown == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
- if (moveDown == NULL) return(1);
+ moveDown = ddSymmSiftingDown(table,x,xHigh);
+ /* at this point x == xHigh, unless early term */
+ if (moveDown == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
+ if (moveDown == NULL) return(1);
- x = moveDown->y;
- i = x;
- while ((unsigned) i < table->subtables[i].next) {
- i = table->subtables[i].next;
- }
+ x = moveDown->y;
+ i = x;
+ while ((unsigned) i < table->subtables[i].next) {
+ i = table->subtables[i].next;
+ }
#ifdef DD_DEBUG
- /* x should be the top of the symmetric group and i the bottom */
- assert((unsigned) i >= table->subtables[i].next);
- assert((unsigned) x == table->subtables[i].next);
+ /* x should be the top of the symmetric group and i the bottom */
+ assert((unsigned) i >= table->subtables[i].next);
+ assert((unsigned) x == table->subtables[i].next);
#endif
- finalGroupSize = i - x + 1;
+ finalGroupSize = i - x + 1;
- if (initGroupSize == finalGroupSize) {
- /* No new symmetries detected, go back to best position */
- result = ddSymmSiftingBackward(table,moveDown,initialSize);
- } else {
- initialSize = table->keys - table->isolated;
- moveUp = ddSymmSiftingUp(table,x,xLow);
- result = ddSymmSiftingBackward(table,moveUp,initialSize);
- }
- if (!result) goto ddSymmSiftingConvAuxOutOfMem;
+ if (initGroupSize == finalGroupSize) {
+ /* No new symmetries detected, go back to best position */
+ result = ddSymmSiftingBackward(table,moveDown,initialSize);
+ } else {
+ initialSize = table->keys - table->isolated;
+ moveUp = ddSymmSiftingUp(table,x,xLow);
+ result = ddSymmSiftingBackward(table,moveUp,initialSize);
+ }
+ if (!result) goto ddSymmSiftingConvAuxOutOfMem;
} else if (cuddNextHigh(table,x) > xHigh) { /* Sift up */
- /* Find top of x's symm group */
- while ((unsigned) x < table->subtables[x].next)
- x = table->subtables[x].next;
- i = x; /* bottom */
- x = table->subtables[x].next; /* top */
+ /* Find top of x's symm group */
+ while ((unsigned) x < table->subtables[x].next)
+ x = table->subtables[x].next;
+ i = x; /* bottom */
+ x = table->subtables[x].next; /* top */
- if (x == xLow) return(1);
+ if (x == xLow) return(1);
- initGroupSize = i - x + 1;
+ initGroupSize = i - x + 1;
- moveUp = ddSymmSiftingUp(table,x,xLow);
- /* at this point x == xLow, unless early term */
- if (moveUp == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
- if (moveUp == NULL) return(1);
+ moveUp = ddSymmSiftingUp(table,x,xLow);
+ /* at this point x == xLow, unless early term */
+ if (moveUp == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
+ if (moveUp == NULL) return(1);
- x = moveUp->x;
- i = table->subtables[x].next;
+ x = moveUp->x;
+ i = table->subtables[x].next;
#ifdef DD_DEBUG
- /* x should be the bottom of the symmetry group and i the top */
- assert((unsigned) x >= table->subtables[x].next);
- assert((unsigned) i == table->subtables[x].next);
+ /* x should be the bottom of the symmetry group and i the top */
+ assert((unsigned) x >= table->subtables[x].next);
+ assert((unsigned) i == table->subtables[x].next);
#endif
- finalGroupSize = x - i + 1;
+ finalGroupSize = x - i + 1;
- if (initGroupSize == finalGroupSize) {
- /* No new symmetry groups detected, return to best position */
- result = ddSymmSiftingBackward(table,moveUp,initialSize);
- } else {
- initialSize = table->keys - table->isolated;
- moveDown = ddSymmSiftingDown(table,x,xHigh);
- result = ddSymmSiftingBackward(table,moveDown,initialSize);
- }
- if (!result)
- goto ddSymmSiftingConvAuxOutOfMem;
+ if (initGroupSize == finalGroupSize) {
+ /* No new symmetry groups detected, return to best position */
+ result = ddSymmSiftingBackward(table,moveUp,initialSize);
+ } else {
+ initialSize = table->keys - table->isolated;
+ moveDown = ddSymmSiftingDown(table,x,xHigh);
+ result = ddSymmSiftingBackward(table,moveDown,initialSize);
+ }
+ if (!result)
+ goto ddSymmSiftingConvAuxOutOfMem;
} else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */
- moveDown = ddSymmSiftingDown(table,x,xHigh);
- /* at this point x == xHigh, unless early term */
- if (moveDown == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
-
- if (moveDown != NULL) {
- x = moveDown->y;
- i = x;
- while ((unsigned) i < table->subtables[i].next) {
- i = table->subtables[i].next;
+ moveDown = ddSymmSiftingDown(table,x,xHigh);
+ /* at this point x == xHigh, unless early term */
+ if (moveDown == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
+
+ if (moveDown != NULL) {
+ x = moveDown->y;
+ i = x;
+ while ((unsigned) i < table->subtables[i].next) {
+ i = table->subtables[i].next;
+ }
+ } else {
+ while ((unsigned) x < table->subtables[x].next)
+ x = table->subtables[x].next;
+ i = x;
+ x = table->subtables[x].next;
}
- } else {
- while ((unsigned) x < table->subtables[x].next)
- x = table->subtables[x].next;
- i = x;
- x = table->subtables[x].next;
- }
#ifdef DD_DEBUG
/* x should be the top of the symmetry group and i the bottom */
- assert((unsigned) i >= table->subtables[i].next);
- assert((unsigned) x == table->subtables[i].next);
+ assert((unsigned) i >= table->subtables[i].next);
+ assert((unsigned) x == table->subtables[i].next);
#endif
- initGroupSize = i - x + 1;
+ initGroupSize = i - x + 1;
- moveUp = ddSymmSiftingUp(table,x,xLow);
- if (moveUp == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
+ moveUp = ddSymmSiftingUp(table,x,xLow);
+ if (moveUp == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
- if (moveUp != NULL) {
- x = moveUp->x;
- i = table->subtables[x].next;
- } else {
- i = x;
- while ((unsigned) x < table->subtables[x].next)
- x = table->subtables[x].next;
- }
+ if (moveUp != NULL) {
+ x = moveUp->x;
+ i = table->subtables[x].next;
+ } else {
+ i = x;
+ while ((unsigned) x < table->subtables[x].next)
+ x = table->subtables[x].next;
+ }
#ifdef DD_DEBUG
- /* x should be the bottom of the symmetry group and i the top */
- assert((unsigned) x >= table->subtables[x].next);
- assert((unsigned) i == table->subtables[x].next);
+ /* x should be the bottom of the symmetry group and i the top */
+ assert((unsigned) x >= table->subtables[x].next);
+ assert((unsigned) i == table->subtables[x].next);
#endif
- finalGroupSize = x - i + 1;
+ finalGroupSize = x - i + 1;
- if (initGroupSize == finalGroupSize) {
- /* No new symmetry groups detected, return to best position */
- result = ddSymmSiftingBackward(table,moveUp,initialSize);
- } else {
- while (moveDown != NULL) {
- move = moveDown->next;
- cuddDeallocNode(table, (DdNode *) moveDown);
- moveDown = move;
+ if (initGroupSize == finalGroupSize) {
+ /* No new symmetry groups detected, return to best position */
+ result = ddSymmSiftingBackward(table,moveUp,initialSize);
+ } else {
+ while (moveDown != NULL) {
+ move = moveDown->next;
+ cuddDeallocMove(table, moveDown);
+ moveDown = move;
+ }
+ initialSize = table->keys - table->isolated;
+ moveDown = ddSymmSiftingDown(table,x,xHigh);
+ result = ddSymmSiftingBackward(table,moveDown,initialSize);
}
- initialSize = table->keys - table->isolated;
- moveDown = ddSymmSiftingDown(table,x,xHigh);
- result = ddSymmSiftingBackward(table,moveDown,initialSize);
- }
- if (!result) goto ddSymmSiftingConvAuxOutOfMem;
+ if (!result) goto ddSymmSiftingConvAuxOutOfMem;
} else { /* moving up first: shorter */
- /* Find top of x's symmetry group */
- x = table->subtables[x].next;
+ /* Find top of x's symmetry group */
+ x = table->subtables[x].next;
- moveUp = ddSymmSiftingUp(table,x,xLow);
- /* at this point x == xHigh, unless early term */
- if (moveUp == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
+ moveUp = ddSymmSiftingUp(table,x,xLow);
+ /* at this point x == xHigh, unless early term */
+ if (moveUp == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
- if (moveUp != NULL) {
- x = moveUp->x;
- i = table->subtables[x].next;
- } else {
- i = x;
- while ((unsigned) x < table->subtables[x].next)
- x = table->subtables[x].next;
- }
+ if (moveUp != NULL) {
+ x = moveUp->x;
+ i = table->subtables[x].next;
+ } else {
+ i = x;
+ while ((unsigned) x < table->subtables[x].next)
+ x = table->subtables[x].next;
+ }
#ifdef DD_DEBUG
/* x is bottom of the symmetry group and i is top */
assert((unsigned) x >= table->subtables[x].next);
@@ -1078,69 +1106,69 @@ ddSymmSiftingConvAux(
#endif
initGroupSize = x - i + 1;
- moveDown = ddSymmSiftingDown(table,x,xHigh);
- if (moveDown == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
-
- if (moveDown != NULL) {
- x = moveDown->y;
- i = x;
- while ((unsigned) i < table->subtables[i].next) {
- i = table->subtables[i].next;
+ moveDown = ddSymmSiftingDown(table,x,xHigh);
+ if (moveDown == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
+
+ if (moveDown != NULL) {
+ x = moveDown->y;
+ i = x;
+ while ((unsigned) i < table->subtables[i].next) {
+ i = table->subtables[i].next;
+ }
+ } else {
+ i = x;
+ x = table->subtables[x].next;
}
- } else {
- i = x;
- x = table->subtables[x].next;
- }
#ifdef DD_DEBUG
- /* x should be the top of the symmetry group and i the bottom */
- assert((unsigned) i >= table->subtables[i].next);
- assert((unsigned) x == table->subtables[i].next);
+ /* x should be the top of the symmetry group and i the bottom */
+ assert((unsigned) i >= table->subtables[i].next);
+ assert((unsigned) x == table->subtables[i].next);
#endif
- finalGroupSize = i - x + 1;
+ finalGroupSize = i - x + 1;
- if (initGroupSize == finalGroupSize) {
- /* No new symmetries detected, go back to best position */
- result = ddSymmSiftingBackward(table,moveDown,initialSize);
- } else {
- while (moveUp != NULL) {
- move = moveUp->next;
- cuddDeallocNode(table, (DdNode *) moveUp);
- moveUp = move;
+ if (initGroupSize == finalGroupSize) {
+ /* No new symmetries detected, go back to best position */
+ result = ddSymmSiftingBackward(table,moveDown,initialSize);
+ } else {
+ while (moveUp != NULL) {
+ move = moveUp->next;
+ cuddDeallocMove(table, moveUp);
+ moveUp = move;
+ }
+ initialSize = table->keys - table->isolated;
+ moveUp = ddSymmSiftingUp(table,x,xLow);
+ result = ddSymmSiftingBackward(table,moveUp,initialSize);
}
- initialSize = table->keys - table->isolated;
- moveUp = ddSymmSiftingUp(table,x,xLow);
- result = ddSymmSiftingBackward(table,moveUp,initialSize);
- }
- if (!result) goto ddSymmSiftingConvAuxOutOfMem;
+ if (!result) goto ddSymmSiftingConvAuxOutOfMem;
}
while (moveDown != NULL) {
- move = moveDown->next;
- cuddDeallocNode(table, (DdNode *) moveDown);
- moveDown = move;
+ move = moveDown->next;
+ cuddDeallocMove(table, moveDown);
+ moveDown = move;
}
while (moveUp != NULL) {
- move = moveUp->next;
- cuddDeallocNode(table, (DdNode *) moveUp);
- moveUp = move;
+ move = moveUp->next;
+ cuddDeallocMove(table, moveUp);
+ moveUp = move;
}
return(1);
ddSymmSiftingConvAuxOutOfMem:
if (moveDown != MV_OOM) {
- while (moveDown != NULL) {
- move = moveDown->next;
- cuddDeallocNode(table, (DdNode *) moveDown);
- moveDown = move;
- }
+ while (moveDown != NULL) {
+ move = moveDown->next;
+ cuddDeallocMove(table, moveDown);
+ moveDown = move;
+ }
}
if (moveUp != MV_OOM) {
- while (moveUp != NULL) {
- move = moveUp->next;
- cuddDeallocNode(table, (DdNode *) moveUp);
- moveUp = move;
- }
+ while (moveUp != NULL) {
+ move = moveUp->next;
+ cuddDeallocMove(table, moveUp);
+ moveUp = move;
+ }
}
return(0);
@@ -1171,8 +1199,8 @@ ddSymmSiftingUp(
{
Move *moves;
Move *move;
- int x;
- int size;
+ int x;
+ int size;
int i;
int gxtop,gybot;
int limitSize;
@@ -1180,7 +1208,7 @@ ddSymmSiftingUp(
int zindex;
int z;
int isolated;
- int L; /* lower bound on DD size */
+ int L; /* lower bound on DD size */
#ifdef DD_DEBUG
int checkL;
#endif
@@ -1198,92 +1226,92 @@ ddSymmSiftingUp(
limitSize = L = table->keys - table->isolated;
gybot = y;
while ((unsigned) gybot < table->subtables[gybot].next)
- 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;
- }
+ zindex = table->invperm[z];
+ if (zindex == yindex || cuddTestInteract(table,zindex,yindex)) {
+ isolated = table->vars[zindex]->ref == 1;
+ L -= table->subtables[z].keys - isolated;
+ }
}
x = cuddNextLow(table,y);
while (x >= xLow && L <= limitSize) {
#ifdef DD_DEBUG
- gybot = y;
- while ((unsigned) gybot < table->subtables[gybot].next)
- gybot = table->subtables[gybot].next;
- checkL = table->keys - table->isolated;
- for (z = xLow + 1; z <= gybot; z++) {
- zindex = table->invperm[z];
- if (zindex == yindex || cuddTestInteract(table,zindex,yindex)) {
- isolated = table->vars[zindex]->ref == 1;
- checkL -= table->subtables[z].keys - isolated;
+ 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;
+ }
}
- }
- assert(L == checkL);
+ assert(L == checkL);
#endif
- gxtop = table->subtables[x].next;
- if (cuddSymmCheck(table,x,y)) {
- /* Symmetry found, attach symm 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;
- } else if (table->subtables[x].next == (unsigned) x &&
- table->subtables[y].next == (unsigned) y) {
- /* x and y have self symmetry */
- xindex = table->invperm[x];
- size = cuddSwapInPlace(table,x,y);
+ gxtop = table->subtables[x].next;
+ if (cuddSymmCheck(table,x,y)) {
+ /* Symmetry found, attach symm 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;
+ } else if (table->subtables[x].next == (unsigned) x &&
+ table->subtables[y].next == (unsigned) y) {
+ /* x and y have self symmetry */
+ 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);
+ assert(table->subtables[x].next == (unsigned) x);
+ assert(table->subtables[y].next == (unsigned) y);
#endif
- if (size == 0) goto ddSymmSiftingUpOutOfMem;
- /* 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 ddSymmSiftingUpOutOfMem;
- move->x = x;
- move->y = y;
- move->size = size;
- move->next = moves;
- moves = move;
- if ((double) size > (double) limitSize * table->maxGrowth)
- return(moves);
- if (size < limitSize) limitSize = size;
- } else { /* Group move */
- size = ddSymmGroupMove(table,x,y,&moves);
- if (size == 0) goto ddSymmSiftingUpOutOfMem;
- /* 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;
+ if (size == 0) goto ddSymmSiftingUpOutOfMem;
+ /* 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 ddSymmSiftingUpOutOfMem;
+ move->x = x;
+ move->y = y;
+ move->size = size;
+ move->next = moves;
+ moves = move;
+ if ((double) size > (double) limitSize * table->maxGrowth)
+ return(moves);
+ if (size < limitSize) limitSize = size;
+ } else { /* Group move */
+ size = ddSymmGroupMove(table,x,y,&moves);
+ if (size == 0) goto ddSymmSiftingUpOutOfMem;
+ /* 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(moves);
+ if (size < limitSize) limitSize = size;
}
- z = table->subtables[z].next;
- } while (z != (int) moves->y);
- if ((double) size > (double) limitSize * table->maxGrowth)
- return(moves);
- if (size < limitSize) limitSize = size;
- }
- y = gxtop;
- x = cuddNextLow(table,y);
+ y = gxtop;
+ x = cuddNextLow(table,y);
}
return(moves);
ddSymmSiftingUpOutOfMem:
while (moves != NULL) {
- move = moves->next;
- cuddDeallocNode(table, (DdNode *) moves);
- moves = move;
+ move = moves->next;
+ cuddDeallocMove(table, moves);
+ moves = move;
}
return(MV_OOM);
@@ -1313,11 +1341,11 @@ ddSymmSiftingDown(
{
Move *moves;
Move *move;
- int y;
- int size;
+ int y;
+ int size;
int limitSize;
int gxtop,gybot;
- int R; /* upper bound on node decrease */
+ int R; /* upper bound on node decrease */
int xindex, yindex;
int isolated;
int z;
@@ -1333,98 +1361,98 @@ ddSymmSiftingDown(
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;
- }
+ zindex = table->invperm[z];
+ if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
+ isolated = table->vars[zindex]->ref == 1;
+ R += table->subtables[z].keys - isolated;
+ }
}
y = cuddNextHigh(table,x);
while (y <= xHigh && size - R < limitSize) {
#ifdef DD_DEBUG
- gxtop = table->subtables[x].next;
- checkR = 0;
- for (z = xHigh; z > gxtop; z--) {
- zindex = table->invperm[z];
- if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
- isolated = table->vars[zindex]->ref == 1;
- checkR += table->subtables[z].keys - isolated;
- }
- }
- assert(R == checkR);
-#endif
- gybot = table->subtables[y].next;
- while (table->subtables[gybot].next != (unsigned) y)
- gybot = table->subtables[gybot].next;
- if (cuddSymmCheck(table,x,y)) {
- /* Symmetry found, attach symm groups */
gxtop = table->subtables[x].next;
- table->subtables[x].next = y;
- table->subtables[gybot].next = gxtop;
- } else if (table->subtables[x].next == (unsigned) x &&
- table->subtables[y].next == (unsigned) y) {
- /* x and y have self symmetry */
- /* 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;
+ 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;
+ }
}
- size = cuddSwapInPlace(table,x,y);
+ assert(R == checkR);
+#endif
+ gybot = table->subtables[y].next;
+ while (table->subtables[gybot].next != (unsigned) y)
+ gybot = table->subtables[gybot].next;
+ if (cuddSymmCheck(table,x,y)) {
+ /* Symmetry found, attach symm groups */
+ gxtop = table->subtables[x].next;
+ table->subtables[x].next = y;
+ table->subtables[gybot].next = gxtop;
+ } else if (table->subtables[x].next == (unsigned) x &&
+ table->subtables[y].next == (unsigned) y) {
+ /* x and y have self symmetry */
+ /* 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);
+ assert(table->subtables[x].next == (unsigned) x);
+ assert(table->subtables[y].next == (unsigned) y);
#endif
- if (size == 0) goto ddSymmSiftingDownOutOfMem;
- move = (Move *) cuddDynamicAllocNode(table);
- if (move == NULL) goto ddSymmSiftingDownOutOfMem;
- move->x = x;
- move->y = y;
- move->size = size;
- move->next = moves;
- moves = move;
- if ((double) size > (double) limitSize * table->maxGrowth)
- return(moves);
- if (size < limitSize) limitSize = size;
- } 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 = ddSymmGroupMove(table,x,y,&moves);
- if (size == 0) goto ddSymmSiftingDownOutOfMem;
- if ((double) size > (double) limitSize * table->maxGrowth)
- return(moves);
- 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;
- }
+ if (size == 0) goto ddSymmSiftingDownOutOfMem;
+ move = (Move *) cuddDynamicAllocNode(table);
+ if (move == NULL) goto ddSymmSiftingDownOutOfMem;
+ move->x = x;
+ move->y = y;
+ move->size = size;
+ move->next = moves;
+ moves = move;
+ if ((double) size > (double) limitSize * table->maxGrowth)
+ return(moves);
+ if (size < limitSize) limitSize = size;
+ } 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 = ddSymmGroupMove(table,x,y,&moves);
+ if (size == 0) goto ddSymmSiftingDownOutOfMem;
+ if ((double) size > (double) limitSize * table->maxGrowth)
+ return(moves);
+ 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);
+ x = gybot;
+ y = cuddNextHigh(table,x);
}
return(moves);
ddSymmSiftingDownOutOfMem:
while (moves != NULL) {
- move = moves->next;
- cuddDeallocNode(table, (DdNode *) moves);
- moves = move;
+ move = moves->next;
+ cuddDeallocMove(table, moves);
+ moves = move;
}
return(MV_OOM);
@@ -1451,13 +1479,13 @@ ddSymmGroupMove(
Move ** moves)
{
Move *move;
- int size = 0; // Suppress "might be used uninitialized"
+ int size;
int i,j;
int xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
- int swapx = 0,swapy = 0; // Suppress "might be used uninitialized"
+ int swapx,swapy;
-#if DD_DEBUG
- assert(x < y); /* we assume that x < y */
+#ifdef DD_DEBUG
+ assert(x < y); /* we assume that x < y */
#endif
/* Find top, bottom, and size for the two groups. */
xbot = x;
@@ -1465,39 +1493,39 @@ ddSymmGroupMove(
xsize = xbot - xtop + 1;
ybot = y;
while ((unsigned) ybot < table->subtables[ybot].next)
- 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);
- swapx = x; swapy = y;
- y = x;
+ size = cuddSwapInPlace(table,x,y);
+ if (size == 0) return(0);
+ swapx = x; swapy = y;
+ y = x;
+ x = y - 1;
+ }
+ y = ytop + i;
x = y - 1;
}
- y = ytop + i;
- x = y - 1;
- }
/* fix symmetries */
y = xtop; /* ytop is now where xtop used to be */
for (i = 0; i < ysize-1 ; i++) {
- table->subtables[y].next = y + 1;
- y = y + 1;
+ table->subtables[y].next = y + 1;
+ y = y + 1;
}
table->subtables[y].next = xtop; /* y is bottom of its group, join */
- /* its symmetry to top of its group */
+ /* its symmetry to top of its group */
x = y + 1;
newxtop = x;
for (i = 0; i < xsize - 1 ; i++) {
- table->subtables[x].next = x + 1;
- x = x + 1;
+ table->subtables[x].next = x + 1;
+ x = x + 1;
}
table->subtables[x].next = newxtop; /* x is bottom of its group, join */
- /* its symmetry to top of its group */
+ /* its symmetry to top of its group */
/* Store group move */
move = (Move *) cuddDynamicAllocNode(table);
if (move == NULL) return(0);
@@ -1530,11 +1558,11 @@ ddSymmGroupMoveBackward(
int x,
int y)
{
- int size = 0; // Suppress "might be used uninitialized"
+ int size;
int i,j;
- int xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
+ int xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
-#if DD_DEBUG
+#ifdef DD_DEBUG
assert(x < y); /* We assume that x < y */
#endif
@@ -1544,38 +1572,38 @@ ddSymmGroupMoveBackward(
xsize = xbot - xtop + 1;
ybot = y;
while ((unsigned) ybot < table->subtables[ybot].next)
- 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 = y - 1;
+ size = cuddSwapInPlace(table,x,y);
+ if (size == 0) return(0);
+ y = x;
+ x = cuddNextLow(table,y);
+ }
+ y = ytop + i;
+ x = y - 1;
}
/* Fix symmetries. */
y = xtop;
for (i = 0; i < ysize-1 ; i++) {
- table->subtables[y].next = y + 1;
- y = y + 1;
+ table->subtables[y].next = y + 1;
+ y = y + 1;
}
table->subtables[y].next = xtop; /* y is bottom of its group, join */
- /* its symmetry to top of its group */
+ /* its symmetry to top of its group */
x = y + 1;
newxtop = x;
for (i = 0; i < xsize-1 ; i++) {
- table->subtables[x].next = x + 1;
- x = x + 1;
+ table->subtables[x].next = x + 1;
+ x = x + 1;
}
table->subtables[x].next = newxtop; /* x is bottom of its group, join */
- /* its symmetry to top of its group */
+ /* its symmetry to top of its group */
return(size);
@@ -1605,23 +1633,23 @@ ddSymmSiftingBackward(
int res;
for (move = moves; move != NULL; move = move->next) {
- if (move->size < size) {
- size = move->size;
- }
+ if (move->size < size) {
+ size = move->size;
+ }
}
for (move = moves; move != NULL; move = move->next) {
- 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 (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);
#ifdef DD_DEBUG
- assert(table->subtables[move->x].next == move->x);
- assert(table->subtables[move->y].next == move->y);
+ assert(table->subtables[move->x].next == move->x);
+ assert(table->subtables[move->y].next == move->y);
#endif
- } else { /* Group move necessary */
- res = ddSymmGroupMoveBackward(table,(int)move->x,(int)move->y);
- }
- if (!res) return(0);
+ } else { /* Group move necessary */
+ res = ddSymmGroupMoveBackward(table,(int)move->x,(int)move->y);
+ }
+ if (!res) return(0);
}
return(1);
@@ -1652,19 +1680,19 @@ ddSymmSummary(
int TotalSymmGroups = 0;
for (i = lower; i <= upper; i++) {
- if (table->subtables[i].next != (unsigned) i) {
- TotalSymmGroups++;
- x = i;
- do {
- TotalSymm++;
- gbot = x;
- x = table->subtables[x].next;
- } while (x != i);
+ if (table->subtables[i].next != (unsigned) i) {
+ TotalSymmGroups++;
+ x = i;
+ do {
+ TotalSymm++;
+ gbot = x;
+ x = table->subtables[x].next;
+ } while (x != i);
#ifdef DD_DEBUG
- assert(table->subtables[gbot].next == (unsigned) i);
+ assert(table->subtables[gbot].next == (unsigned) i);
#endif
- i = gbot;
- }
+ i = gbot;
+ }
}
*symvars = TotalSymm;
*symgroups = TotalSymmGroups;
@@ -1672,5 +1700,7 @@ ddSymmSummary(
return;
} /* end of ddSymmSummary */
+
+
ABC_NAMESPACE_IMPL_END
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 20:06:46 +0000