From e7b544f11151f09a4a3fbe39b4a176795a82f677 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 13 Feb 2011 13:42:25 -0800 Subject: Upgrade to the latest CUDD 2.4.2. --- src/bdd/cudd/cuddZddSymm.c | 1829 ++++++++++++++++++++++---------------------- 1 file changed, 927 insertions(+), 902 deletions(-) (limited to 'src/bdd/cudd/cuddZddSymm.c') diff --git a/src/bdd/cudd/cuddZddSymm.c b/src/bdd/cudd/cuddZddSymm.c index 644673cd..52e26d88 100644 --- a/src/bdd/cudd/cuddZddSymm.c +++ b/src/bdd/cudd/cuddZddSymm.c @@ -7,45 +7,73 @@ Synopsis [Functions for symmetry-based ZDD variable reordering.] Description [External procedures included in this module: - - Internal procedures included in this module: - - Static procedures included in this module: - - ] + + Internal procedures included in this module: + + Static procedures included in this module: + + ] SeeAlso [cuddSymmetry.c] Author [Hyong-Kyoon Shin, In-Ho Moon] - 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.] ******************************************************************************/ -#include "util_hack.h" -#include "cuddInt.h" +#include "util_hack.h" +#include "cuddInt.h" ABC_NAMESPACE_IMPL_START + /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ @@ -65,14 +93,14 @@ ABC_NAMESPACE_IMPL_START /*---------------------------------------------------------------------------*/ #ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddZddSymm.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $"; +static char rcsid[] DD_UNUSED = "$Id: cuddZddSymm.c,v 1.29 2004/08/13 18:04:54 fabio Exp $"; #endif -extern int *zdd_entry; +extern int *zdd_entry; -extern int zddTotalNumberSwapping; +extern int zddTotalNumberSwapping; -static DdNode *empty; +static DdNode *empty; /*---------------------------------------------------------------------------*/ /* Macro declarations */ @@ -85,14 +113,14 @@ static DdNode *empty; /* Static function prototypes */ /*---------------------------------------------------------------------------*/ -static int cuddZddSymmSiftingAux ARGS((DdManager *table, int x, int x_low, int x_high)); -static int cuddZddSymmSiftingConvAux ARGS((DdManager *table, int x, int x_low, int x_high)); -static Move * cuddZddSymmSifting_up ARGS((DdManager *table, int x, int x_low, int initial_size)); -static Move * cuddZddSymmSifting_down ARGS((DdManager *table, int x, int x_high, int initial_size)); -static int cuddZddSymmSiftingBackward ARGS((DdManager *table, Move *moves, int size)); -static int zdd_group_move ARGS((DdManager *table, int x, int y, Move **moves)); -static int zdd_group_move_backward ARGS((DdManager *table, int x, int y)); -static void cuddZddSymmSummary ARGS((DdManager *table, int lower, int upper, int *symvars, int *symgroups)); +static int cuddZddSymmSiftingAux (DdManager *table, int x, int x_low, int x_high); +static int cuddZddSymmSiftingConvAux (DdManager *table, int x, int x_low, int x_high); +static Move * cuddZddSymmSifting_up (DdManager *table, int x, int x_low, int initial_size); +static Move * cuddZddSymmSifting_down (DdManager *table, int x, int x_high, int initial_size); +static int cuddZddSymmSiftingBackward (DdManager *table, Move *moves, int size); +static int zdd_group_move (DdManager *table, int x, int y, Move **moves); +static int zdd_group_move_backward (DdManager *table, int x, int y); +static void cuddZddSymmSummary (DdManager *table, int lower, int upper, int *symvars, int *symgroups); /**AutomaticEnd***************************************************************/ @@ -119,30 +147,27 @@ Cudd_zddSymmProfile( int lower, int upper) { - int i, x, gbot; - int TotalSymm = 0; - int TotalSymmGroups = 0; - int nvars; - - nvars = table->sizeZ; + int i, x, gbot; + int TotalSymm = 0; + int TotalSymmGroups = 0; for (i = lower; i < upper; i++) { - if (table->subtableZ[i].next != (unsigned) i) { - x = i; - (void) fprintf(table->out,"Group:"); - do { - (void) fprintf(table->out," %d", table->invpermZ[x]); - TotalSymm++; - gbot = x; - x = table->subtableZ[x].next; - } while (x != i); - TotalSymmGroups++; + if (table->subtableZ[i].next != (unsigned) i) { + x = i; + (void) fprintf(table->out,"Group:"); + do { + (void) fprintf(table->out," %d", table->invpermZ[x]); + TotalSymm++; + gbot = x; + x = table->subtableZ[x].next; + } while (x != i); + TotalSymmGroups++; #ifdef DD_DEBUG - assert(table->subtableZ[gbot].next == (unsigned) i); + assert(table->subtableZ[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); @@ -174,75 +199,75 @@ cuddZddSymmCheck( int x, int y) { - int i; - DdNode *f, *f0, *f1, *f01, *f00, *f11, *f10; - int yindex; - int xsymmy = 1; - int xsymmyp = 1; - int arccount = 0; - int TotalRefCount = 0; - int symm_found; + int i; + DdNode *f, *f0, *f1, *f01, *f00, *f11, *f10; + int yindex; + int xsymmy = 1; + int xsymmyp = 1; + int arccount = 0; + int TotalRefCount = 0; + int symm_found; empty = table->zero; yindex = table->invpermZ[y]; for (i = table->subtableZ[x].slots - 1; i >= 0; i--) { - f = table->subtableZ[x].nodelist[i]; - while (f != NULL) { - /* Find f1, f0, f11, f10, f01, f00 */ - f1 = cuddT(f); - f0 = cuddE(f); - if ((int) f1->index == yindex) { - f11 = cuddT(f1); - f10 = cuddE(f1); - if (f10 != empty) - arccount++; - } else { - if ((int) f0->index != yindex) { - return(0); /* f bypasses layer y */ - } - f11 = empty; - f10 = f1; - } - if ((int) f0->index == yindex) { - f01 = cuddT(f0); - f00 = cuddE(f0); - if (f00 != empty) - arccount++; - } else { - f01 = empty; - f00 = f0; - } - if (f01 != f10) - xsymmy = 0; - if (f11 != f00) - xsymmyp = 0; - if ((xsymmy == 0) && (xsymmyp == 0)) - return(0); - - f = f->next; - } /* for each element of the collision list */ + f = table->subtableZ[x].nodelist[i]; + while (f != NULL) { + /* Find f1, f0, f11, f10, f01, f00 */ + f1 = cuddT(f); + f0 = cuddE(f); + if ((int) f1->index == yindex) { + f11 = cuddT(f1); + f10 = cuddE(f1); + if (f10 != empty) + arccount++; + } else { + if ((int) f0->index != yindex) { + return(0); /* f bypasses layer y */ + } + f11 = empty; + f10 = f1; + } + if ((int) f0->index == yindex) { + f01 = cuddT(f0); + f00 = cuddE(f0); + if (f00 != empty) + arccount++; + } else { + f01 = empty; + f00 = f0; + } + if (f01 != f10) + xsymmy = 0; + if (f11 != f00) + xsymmyp = 0; + if ((xsymmy == 0) && (xsymmyp == 0)) + return(0); + + f = f->next; + } /* for each element of the collision list */ } /* for each slot of the subtable */ /* Calculate the total reference counts of y ** whose else arc is not empty. */ for (i = table->subtableZ[y].slots - 1; i >= 0; i--) { - f = table->subtableZ[y].nodelist[i]; - while (f != NIL(DdNode)) { - if (cuddE(f) != empty) - TotalRefCount += f->ref; - f = f->next; - } + f = table->subtableZ[y].nodelist[i]; + while (f != NIL(DdNode)) { + if (cuddE(f) != empty) + TotalRefCount += f->ref; + f = f->next; + } } symm_found = (arccount == TotalRefCount); #if defined(DD_DEBUG) && defined(DD_VERBOSE) if (symm_found) { - int xindex = table->invpermZ[x]; - (void) fprintf(table->out, - "Found symmetry! x =%d\ty = %d\tPos(%d,%d)\n", - xindex,yindex,x,y); + int xindex = table->invpermZ[x]; + (void) fprintf(table->out, + "Found symmetry! x =%d\ty = %d\tPos(%d,%d)\n", + xindex,yindex,x,y); } #endif @@ -279,16 +304,16 @@ cuddZddSymmSifting( int lower, int upper) { - int i; - int *var; - int nvars; - int x; - int result; - int symvars; - int symgroups; - int iteration; + int i; + int *var; + int nvars; + int x; + int result; + int symvars; + int symgroups; + int iteration; #ifdef DD_STATS - int previousSize; + int previousSize; #endif nvars = table->sizeZ; @@ -297,54 +322,54 @@ cuddZddSymmSifting( var = NULL; zdd_entry = ABC_ALLOC(int, nvars); if (zdd_entry == NULL) { - table->errorCode = CUDD_MEMORY_OUT; - goto cuddZddSymmSiftingOutOfMem; + table->errorCode = CUDD_MEMORY_OUT; + goto cuddZddSymmSiftingOutOfMem; } var = ABC_ALLOC(int, nvars); if (var == NULL) { - table->errorCode = CUDD_MEMORY_OUT; - goto cuddZddSymmSiftingOutOfMem; + table->errorCode = CUDD_MEMORY_OUT; + goto cuddZddSymmSiftingOutOfMem; } for (i = 0; i < nvars; i++) { - x = table->permZ[i]; - zdd_entry[i] = table->subtableZ[x].keys; - var[i] = i; + x = table->permZ[i]; + zdd_entry[i] = table->subtableZ[x].keys; + var[i] = i; } - qsort((void *)var, nvars, sizeof(int), (int (*)(const void *, const void *))cuddZddUniqueCompare); + qsort((void *)var, nvars, sizeof(int), (DD_QSFP)cuddZddUniqueCompare); /* Initialize the symmetry of each subtable to itself. */ for (i = lower; i <= upper; i++) - table->subtableZ[i].next = i; + table->subtableZ[i].next = i; iteration = ddMin(table->siftMaxVar, nvars); for (i = 0; i < iteration; i++) { - if (zddTotalNumberSwapping >= table->siftMaxSwap) - break; - x = table->permZ[var[i]]; + if (zddTotalNumberSwapping >= table->siftMaxSwap) + break; + x = table->permZ[var[i]]; #ifdef DD_STATS - previousSize = table->keysZ; + previousSize = table->keysZ; #endif - if (x < lower || x > upper) continue; - if (table->subtableZ[x].next == (unsigned) x) { - result = cuddZddSymmSiftingAux(table, x, lower, upper); - if (!result) - goto cuddZddSymmSiftingOutOfMem; + if (x < lower || x > upper) continue; + if (table->subtableZ[x].next == (unsigned) x) { + result = cuddZddSymmSiftingAux(table, x, lower, upper); + if (!result) + goto cuddZddSymmSiftingOutOfMem; #ifdef DD_STATS - if (table->keysZ < (unsigned) previousSize) { - (void) fprintf(table->out,"-"); - } else if (table->keysZ > (unsigned) previousSize) { - (void) fprintf(table->out,"+"); + if (table->keysZ < (unsigned) previousSize) { + (void) fprintf(table->out,"-"); + } else if (table->keysZ > (unsigned) previousSize) { + (void) fprintf(table->out,"+"); #ifdef DD_VERBOSE - (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ, var[i]); + (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ, var[i]); #endif - } else { - (void) fprintf(table->out,"="); - } - fflush(table->out); + } else { + (void) fprintf(table->out,"="); + } + fflush(table->out); #endif - } + } } ABC_FREE(var); @@ -362,9 +387,9 @@ cuddZddSymmSifting( cuddZddSymmSiftingOutOfMem: if (zdd_entry != NULL) - ABC_FREE(zdd_entry); + ABC_FREE(zdd_entry); if (var != NULL) - ABC_FREE(var); + ABC_FREE(var); return(0); @@ -400,16 +425,16 @@ cuddZddSymmSiftingConv( int lower, int upper) { - int i; - int *var; - int nvars; - int initialSize; - int x; - int result; - int symvars; - int symgroups; - int classes; - int iteration; + int i; + int *var; + int nvars; + int initialSize; + int x; + int result; + int symvars; + int symgroups; + int classes; + int iteration; #ifdef DD_STATS int previousSize; #endif @@ -422,117 +447,117 @@ cuddZddSymmSiftingConv( var = NULL; zdd_entry = ABC_ALLOC(int, nvars); if (zdd_entry == NULL) { - table->errorCode = CUDD_MEMORY_OUT; - goto cuddZddSymmSiftingConvOutOfMem; + table->errorCode = CUDD_MEMORY_OUT; + goto cuddZddSymmSiftingConvOutOfMem; } var = ABC_ALLOC(int, nvars); if (var == NULL) { - table->errorCode = CUDD_MEMORY_OUT; - goto cuddZddSymmSiftingConvOutOfMem; + table->errorCode = CUDD_MEMORY_OUT; + goto cuddZddSymmSiftingConvOutOfMem; } for (i = 0; i < nvars; i++) { - x = table->permZ[i]; - zdd_entry[i] = table->subtableZ[x].keys; - var[i] = i; + x = table->permZ[i]; + zdd_entry[i] = table->subtableZ[x].keys; + var[i] = i; } - qsort((void *)var, nvars, sizeof(int), (int (*)(const void *, const void *))cuddZddUniqueCompare); + qsort((void *)var, nvars, sizeof(int), (DD_QSFP)cuddZddUniqueCompare); /* Initialize the symmetry of each subtable to itself ** for first pass of converging symmetric sifting. */ for (i = lower; i <= upper; i++) - table->subtableZ[i].next = i; + table->subtableZ[i].next = i; iteration = ddMin(table->siftMaxVar, table->sizeZ); for (i = 0; i < iteration; i++) { - if (zddTotalNumberSwapping >= table->siftMaxSwap) - break; - x = table->permZ[var[i]]; - if (x < lower || x > upper) continue; - /* Only sift if not in symmetry group already. */ - if (table->subtableZ[x].next == (unsigned) x) { + if (zddTotalNumberSwapping >= table->siftMaxSwap) + break; + x = table->permZ[var[i]]; + if (x < lower || x > upper) continue; + /* Only sift if not in symmetry group already. */ + if (table->subtableZ[x].next == (unsigned) x) { #ifdef DD_STATS - previousSize = table->keysZ; + previousSize = table->keysZ; #endif - result = cuddZddSymmSiftingAux(table, x, lower, upper); - if (!result) - goto cuddZddSymmSiftingConvOutOfMem; + result = cuddZddSymmSiftingAux(table, x, lower, upper); + if (!result) + goto cuddZddSymmSiftingConvOutOfMem; #ifdef DD_STATS - if (table->keysZ < (unsigned) previousSize) { - (void) fprintf(table->out,"-"); - } else if (table->keysZ > (unsigned) previousSize) { - (void) fprintf(table->out,"+"); + if (table->keysZ < (unsigned) previousSize) { + (void) fprintf(table->out,"-"); + } else if (table->keysZ > (unsigned) previousSize) { + (void) fprintf(table->out,"+"); #ifdef DD_VERBOSE - (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ, var[i]); + (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ, var[i]); #endif - } else { - (void) fprintf(table->out,"="); - } - fflush(table->out); + } else { + (void) fprintf(table->out,"="); + } + fflush(table->out); #endif - } + } } /* Sifting now until convergence. */ while ((unsigned) initialSize > table->keysZ) { - initialSize = table->keysZ; + initialSize = table->keysZ; #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->subtableZ[x].next) - x = table->subtableZ[x].next; - /* Here x is the largest index in a group. - ** Groups consists of adjacent variables. - ** Hence, the next increment of x will move it to a new group. - */ - i = table->invpermZ[x]; - zdd_entry[i] = table->subtableZ[x].keys; - var[classes] = i; - } + /* Here we consider only one representative for each symmetry class. */ + for (x = lower, classes = 0; x <= upper; x++, classes++) { + while ((unsigned) x < table->subtableZ[x].next) + x = table->subtableZ[x].next; + /* Here x is the largest index in a group. + ** Groups consists of adjacent variables. + ** Hence, the next increment of x will move it to a new group. + */ + i = table->invpermZ[x]; + zdd_entry[i] = table->subtableZ[x].keys; + var[classes] = i; + } - qsort((void *)var,classes,sizeof(int),(int (*)(const void *, const void *))cuddZddUniqueCompare); + qsort((void *)var,classes,sizeof(int),(DD_QSFP)cuddZddUniqueCompare); - /* Now sift. */ - iteration = ddMin(table->siftMaxVar, nvars); - for (i = 0; i < iteration; i++) { - if (zddTotalNumberSwapping >= table->siftMaxSwap) - break; - x = table->permZ[var[i]]; - if ((unsigned) x >= table->subtableZ[x].next) { + /* Now sift. */ + iteration = ddMin(table->siftMaxVar, nvars); + for (i = 0; i < iteration; i++) { + if (zddTotalNumberSwapping >= table->siftMaxSwap) + break; + x = table->permZ[var[i]]; + if ((unsigned) x >= table->subtableZ[x].next) { #ifdef DD_STATS - previousSize = table->keysZ; + previousSize = table->keysZ; #endif - result = cuddZddSymmSiftingConvAux(table, x, lower, upper); - if (!result) - goto cuddZddSymmSiftingConvOutOfMem; + result = cuddZddSymmSiftingConvAux(table, x, lower, upper); + if (!result) + goto cuddZddSymmSiftingConvOutOfMem; #ifdef DD_STATS - if (table->keysZ < (unsigned) previousSize) { - (void) fprintf(table->out,"-"); - } else if (table->keysZ > (unsigned) previousSize) { - (void) fprintf(table->out,"+"); + if (table->keysZ < (unsigned) previousSize) { + (void) fprintf(table->out,"-"); + } else if (table->keysZ > (unsigned) previousSize) { + (void) fprintf(table->out,"+"); #ifdef DD_VERBOSE - (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ, var[i]); + (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ, var[i]); #endif - } else { - (void) fprintf(table->out,"="); - } - fflush(table->out); + } else { + (void) fprintf(table->out,"="); + } + fflush(table->out); #endif - } - } /* for */ + } + } /* for */ } cuddZddSymmSummary(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\n", - symgroups); + symgroups); #endif ABC_FREE(var); @@ -543,9 +568,9 @@ cuddZddSymmSiftingConv( cuddZddSymmSiftingConvOutOfMem: if (zdd_entry != NULL) - ABC_FREE(zdd_entry); + ABC_FREE(zdd_entry); if (var != NULL) - ABC_FREE(var); + ABC_FREE(var); return(0); @@ -580,13 +605,13 @@ cuddZddSymmSiftingAux( int x_high) { Move *move; - Move *move_up; /* list of up move */ + Move *move_up; /* list of up move */ Move *move_down; /* list of down move */ - int initial_size; - int result; - int i; - int topbot; /* index to either top or bottom of symmetry group */ - int init_group_size, final_group_size; + int initial_size; + int result; + int i; + int topbot; /* index to either top or bottom of symmetry group */ + int init_group_size, final_group_size; initial_size = table->keysZ; @@ -595,300 +620,300 @@ cuddZddSymmSiftingAux( /* Look for consecutive symmetries above x. */ for (i = x; i > x_low; i--) { - if (!cuddZddSymmCheck(table, i - 1, i)) + if (!cuddZddSymmCheck(table, i - 1, i)) break; - /* find top of i-1's symmetry */ - topbot = table->subtableZ[i - 1].next; - table->subtableZ[i - 1].next = i; - table->subtableZ[x].next = topbot; - /* x is bottom of group so its symmetry is top of i-1's - group */ - i = topbot + 1; /* add 1 for i--, new i is top of symm group */ + /* find top of i-1's symmetry */ + topbot = table->subtableZ[i - 1].next; + table->subtableZ[i - 1].next = i; + table->subtableZ[x].next = topbot; + /* x is bottom of group so its symmetry is top of i-1's + group */ + i = topbot + 1; /* add 1 for i--, new i is top of symm group */ } /* Look for consecutive symmetries below x. */ for (i = x; i < x_high; i++) { - if (!cuddZddSymmCheck(table, i, i + 1)) + if (!cuddZddSymmCheck(table, i, i + 1)) break; - /* find bottom of i+1's symm group */ - topbot = i + 1; - while ((unsigned) topbot < table->subtableZ[topbot].next) - topbot = table->subtableZ[topbot].next; - - table->subtableZ[topbot].next = table->subtableZ[i].next; - table->subtableZ[i].next = i + 1; - i = topbot - 1; /* add 1 for i++, - new i is bottom of symm group */ + /* find bottom of i+1's symm group */ + topbot = i + 1; + while ((unsigned) topbot < table->subtableZ[topbot].next) + topbot = table->subtableZ[topbot].next; + + table->subtableZ[topbot].next = table->subtableZ[i].next; + table->subtableZ[i].next = i + 1; + i = topbot - 1; /* add 1 for i++, + new i is bottom of symm group */ } /* Now x maybe in the middle of a symmetry group. */ if (x == x_low) { /* Sift down */ - /* Find bottom of x's symm group */ - while ((unsigned) x < table->subtableZ[x].next) - x = table->subtableZ[x].next; - - i = table->subtableZ[x].next; - init_group_size = x - i + 1; + /* Find bottom of x's symm group */ + while ((unsigned) x < table->subtableZ[x].next) + x = table->subtableZ[x].next; - move_down = cuddZddSymmSifting_down(table, x, x_high, - initial_size); - /* after that point x --> x_high, unless early term */ - if (move_down == ZDD_MV_OOM) - goto cuddZddSymmSiftingAuxOutOfMem; + i = table->subtableZ[x].next; + init_group_size = x - i + 1; - if (move_down == NULL || - table->subtableZ[move_down->y].next != move_down->y) { - /* symmetry detected may have to make another complete - pass */ + move_down = cuddZddSymmSifting_down(table, x, x_high, + initial_size); + /* after that point x --> x_high, unless early term */ + if (move_down == ZDD_MV_OOM) + goto cuddZddSymmSiftingAuxOutOfMem; + + if (move_down == NULL || + table->subtableZ[move_down->y].next != move_down->y) { + /* symmetry detected may have to make another complete + pass */ if (move_down != NULL) - x = move_down->y; - else - x = table->subtableZ[x].next; - i = x; - while ((unsigned) i < table->subtableZ[i].next) { - i = table->subtableZ[i].next; - } - final_group_size = i - x + 1; + x = move_down->y; + else + x = table->subtableZ[x].next; + i = x; + while ((unsigned) i < table->subtableZ[i].next) { + i = table->subtableZ[i].next; + } + final_group_size = i - x + 1; - if (init_group_size == final_group_size) { - /* No new symmetry groups detected, - return to best position */ - result = cuddZddSymmSiftingBackward(table, - move_down, initial_size); + if (init_group_size == final_group_size) { + /* No new symmetry groups detected, + return to best position */ + result = cuddZddSymmSiftingBackward(table, + move_down, initial_size); + } + else { + initial_size = table->keysZ; + move_up = cuddZddSymmSifting_up(table, x, x_low, + initial_size); + result = cuddZddSymmSiftingBackward(table, move_up, + initial_size); + } } else { - initial_size = table->keysZ; - move_up = cuddZddSymmSifting_up(table, x, x_low, - initial_size); - result = cuddZddSymmSiftingBackward(table, move_up, - initial_size); + result = cuddZddSymmSiftingBackward(table, move_down, + initial_size); + /* move backward and stop at best position */ } - } - else { - result = cuddZddSymmSiftingBackward(table, move_down, - initial_size); - /* move backward and stop at best position */ - } - if (!result) - goto cuddZddSymmSiftingAuxOutOfMem; + if (!result) + goto cuddZddSymmSiftingAuxOutOfMem; } else if (x == x_high) { /* Sift up */ - /* Find top of x's symm group */ - while ((unsigned) x < table->subtableZ[x].next) + /* Find top of x's symm group */ + while ((unsigned) x < table->subtableZ[x].next) + x = table->subtableZ[x].next; x = table->subtableZ[x].next; - x = table->subtableZ[x].next; - i = x; - while ((unsigned) i < table->subtableZ[i].next) { - i = table->subtableZ[i].next; - } - init_group_size = i - x + 1; + i = x; + while ((unsigned) i < table->subtableZ[i].next) { + i = table->subtableZ[i].next; + } + init_group_size = i - x + 1; - move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size); - /* after that point x --> x_low, unless early term */ - if (move_up == ZDD_MV_OOM) - goto cuddZddSymmSiftingAuxOutOfMem; + move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size); + /* after that point x --> x_low, unless early term */ + if (move_up == ZDD_MV_OOM) + goto cuddZddSymmSiftingAuxOutOfMem; - if (move_up == NULL || - table->subtableZ[move_up->x].next != move_up->x) { - /* symmetry detected may have to make another complete - pass */ + if (move_up == NULL || + table->subtableZ[move_up->x].next != move_up->x) { + /* symmetry detected may have to make another complete + pass */ if (move_up != NULL) - x = move_up->x; - else { - while ((unsigned) x < table->subtableZ[x].next) - x = table->subtableZ[x].next; - } - i = table->subtableZ[x].next; - final_group_size = x - i + 1; + x = move_up->x; + else { + while ((unsigned) x < table->subtableZ[x].next) + x = table->subtableZ[x].next; + } + i = table->subtableZ[x].next; + final_group_size = x - i + 1; - if (init_group_size == final_group_size) { - /* No new symmetry groups detected, - return to best position */ - result = cuddZddSymmSiftingBackward(table, move_up, - initial_size); + if (init_group_size == final_group_size) { + /* No new symmetry groups detected, + return to best position */ + result = cuddZddSymmSiftingBackward(table, move_up, + initial_size); + } + else { + initial_size = table->keysZ; + move_down = cuddZddSymmSifting_down(table, x, x_high, + initial_size); + result = cuddZddSymmSiftingBackward(table, move_down, + initial_size); + } } else { - initial_size = table->keysZ; - move_down = cuddZddSymmSifting_down(table, x, x_high, - initial_size); - result = cuddZddSymmSiftingBackward(table, move_down, - initial_size); + result = cuddZddSymmSiftingBackward(table, move_up, + initial_size); + /* move backward and stop at best position */ } - } - else { - result = cuddZddSymmSiftingBackward(table, move_up, - initial_size); - /* move backward and stop at best position */ - } - if (!result) - goto cuddZddSymmSiftingAuxOutOfMem; + if (!result) + goto cuddZddSymmSiftingAuxOutOfMem; } else if ((x - x_low) > (x_high - x)) { /* must go down first: - shorter */ - /* Find bottom of x's symm group */ - while ((unsigned) x < table->subtableZ[x].next) - x = table->subtableZ[x].next; - - move_down = cuddZddSymmSifting_down(table, x, x_high, - initial_size); - /* after that point x --> x_high, unless early term */ - if (move_down == ZDD_MV_OOM) - goto cuddZddSymmSiftingAuxOutOfMem; - - if (move_down != NULL) { - x = move_down->y; - } - else { - x = table->subtableZ[x].next; - } - i = x; - while ((unsigned) i < table->subtableZ[i].next) { - i = table->subtableZ[i].next; - } - init_group_size = i - x + 1; + shorter */ + /* Find bottom of x's symm group */ + while ((unsigned) x < table->subtableZ[x].next) + x = table->subtableZ[x].next; - move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size); - if (move_up == ZDD_MV_OOM) - goto cuddZddSymmSiftingAuxOutOfMem; + move_down = cuddZddSymmSifting_down(table, x, x_high, + initial_size); + /* after that point x --> x_high, unless early term */ + if (move_down == ZDD_MV_OOM) + goto cuddZddSymmSiftingAuxOutOfMem; - if (move_up == NULL || - table->subtableZ[move_up->x].next != move_up->x) { - /* symmetry detected may have to make another complete - pass */ - if (move_up != NULL) { - x = move_up->x; + if (move_down != NULL) { + x = move_down->y; } else { - while ((unsigned) x < table->subtableZ[x].next) x = table->subtableZ[x].next; } - i = table->subtableZ[x].next; - final_group_size = x - i + 1; + i = x; + while ((unsigned) i < table->subtableZ[i].next) { + i = table->subtableZ[i].next; + } + init_group_size = i - x + 1; + + move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size); + if (move_up == ZDD_MV_OOM) + goto cuddZddSymmSiftingAuxOutOfMem; + + if (move_up == NULL || + table->subtableZ[move_up->x].next != move_up->x) { + /* symmetry detected may have to make another complete + pass */ + if (move_up != NULL) { + x = move_up->x; + } + else { + while ((unsigned) x < table->subtableZ[x].next) + x = table->subtableZ[x].next; + } + i = table->subtableZ[x].next; + final_group_size = x - i + 1; - if (init_group_size == final_group_size) { - /* No new symmetry groups detected, - return to best position */ - result = cuddZddSymmSiftingBackward(table, move_up, - initial_size); + if (init_group_size == final_group_size) { + /* No new symmetry groups detected, + return to best position */ + result = cuddZddSymmSiftingBackward(table, move_up, + initial_size); + } + else { + while (move_down != NULL) { + move = move_down->next; + cuddDeallocMove(table, move_down); + move_down = move; + } + initial_size = table->keysZ; + move_down = cuddZddSymmSifting_down(table, x, x_high, + initial_size); + result = cuddZddSymmSiftingBackward(table, move_down, + initial_size); + } } else { - while (move_down != NULL) { - move = move_down->next; - cuddDeallocNode(table, (DdNode *)move_down); - move_down = move; + result = cuddZddSymmSiftingBackward(table, move_up, + initial_size); + /* move backward and stop at best position */ } - initial_size = table->keysZ; - move_down = cuddZddSymmSifting_down(table, x, x_high, - initial_size); - result = cuddZddSymmSiftingBackward(table, move_down, - initial_size); - } - } - else { - result = cuddZddSymmSiftingBackward(table, move_up, - initial_size); - /* move backward and stop at best position */ - } - if (!result) - goto cuddZddSymmSiftingAuxOutOfMem; + if (!result) + goto cuddZddSymmSiftingAuxOutOfMem; } else { /* moving up first:shorter */ /* Find top of x's symmetry group */ - while ((unsigned) x < table->subtableZ[x].next) + while ((unsigned) x < table->subtableZ[x].next) + x = table->subtableZ[x].next; x = table->subtableZ[x].next; - x = table->subtableZ[x].next; - move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size); - /* after that point x --> x_high, unless early term */ - if (move_up == ZDD_MV_OOM) - goto cuddZddSymmSiftingAuxOutOfMem; + move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size); + /* after that point x --> x_high, unless early term */ + if (move_up == ZDD_MV_OOM) + goto cuddZddSymmSiftingAuxOutOfMem; - if (move_up != NULL) { - x = move_up->x; - } - else { - while ((unsigned) x < table->subtableZ[x].next) - x = table->subtableZ[x].next; - } - i = table->subtableZ[x].next; - init_group_size = x - i + 1; - - move_down = cuddZddSymmSifting_down(table, x, x_high, - initial_size); - if (move_down == ZDD_MV_OOM) - goto cuddZddSymmSiftingAuxOutOfMem; - - if (move_down == NULL || - table->subtableZ[move_down->y].next != move_down->y) { - /* symmetry detected may have to make another complete - pass */ - if (move_down != NULL) { - x = move_down->y; + if (move_up != NULL) { + x = move_up->x; } else { - x = table->subtableZ[x].next; + while ((unsigned) x < table->subtableZ[x].next) + x = table->subtableZ[x].next; } - i = x; - while ((unsigned) i < table->subtableZ[i].next) { - i = table->subtableZ[i].next; - } - final_group_size = i - x + 1; + i = table->subtableZ[x].next; + init_group_size = x - i + 1; - if (init_group_size == final_group_size) { - /* No new symmetries detected, - go back to best position */ - result = cuddZddSymmSiftingBackward(table, move_down, + move_down = cuddZddSymmSifting_down(table, x, x_high, initial_size); + if (move_down == ZDD_MV_OOM) + goto cuddZddSymmSiftingAuxOutOfMem; + + if (move_down == NULL || + table->subtableZ[move_down->y].next != move_down->y) { + /* symmetry detected may have to make another complete + pass */ + if (move_down != NULL) { + x = move_down->y; + } + else { + x = table->subtableZ[x].next; + } + i = x; + while ((unsigned) i < table->subtableZ[i].next) { + i = table->subtableZ[i].next; + } + final_group_size = i - x + 1; + + if (init_group_size == final_group_size) { + /* No new symmetries detected, + go back to best position */ + result = cuddZddSymmSiftingBackward(table, move_down, + initial_size); + } + else { + while (move_up != NULL) { + move = move_up->next; + cuddDeallocMove(table, move_up); + move_up = move; + } + initial_size = table->keysZ; + move_up = cuddZddSymmSifting_up(table, x, x_low, + initial_size); + result = cuddZddSymmSiftingBackward(table, move_up, + initial_size); + } } else { - while (move_up != NULL) { - move = move_up->next; - cuddDeallocNode(table, (DdNode *)move_up); - move_up = move; - } - initial_size = table->keysZ; - move_up = cuddZddSymmSifting_up(table, x, x_low, - initial_size); - result = cuddZddSymmSiftingBackward(table, move_up, - initial_size); + result = cuddZddSymmSiftingBackward(table, move_down, + initial_size); + /* move backward and stop at best position */ } - } - else { - result = cuddZddSymmSiftingBackward(table, move_down, - initial_size); - /* move backward and stop at best position */ - } - if (!result) - goto cuddZddSymmSiftingAuxOutOfMem; + if (!result) + goto cuddZddSymmSiftingAuxOutOfMem; } while (move_down != NULL) { - move = move_down->next; - cuddDeallocNode(table, (DdNode *)move_down); - move_down = move; + move = move_down->next; + cuddDeallocMove(table, move_down); + move_down = move; } while (move_up != NULL) { - move = move_up->next; - cuddDeallocNode(table, (DdNode *)move_up); - move_up = move; + move = move_up->next; + cuddDeallocMove(table, move_up); + move_up = move; } return(1); cuddZddSymmSiftingAuxOutOfMem: if (move_down != ZDD_MV_OOM) { - while (move_down != NULL) { - move = move_down->next; - cuddDeallocNode(table, (DdNode *)move_down); - move_down = move; - } + while (move_down != NULL) { + move = move_down->next; + cuddDeallocMove(table, move_down); + move_down = move; + } } if (move_up != ZDD_MV_OOM) { - while (move_up != NULL) { - move = move_up->next; - cuddDeallocNode(table, (DdNode *)move_up); - move_up = move; - } + while (move_up != NULL) { + move = move_up->next; + cuddDeallocMove(table, move_up); + move_up = move; + } } return(0); @@ -919,13 +944,13 @@ cuddZddSymmSiftingConvAux( int x_low, int x_high) { - Move *move; - Move *move_up; /* list of up move */ - Move *move_down; /* list of down move */ - int initial_size; - int result; - int i; - int init_group_size, final_group_size; + Move *move; + Move *move_up; /* list of up move */ + Move *move_down; /* list of down move */ + int initial_size; + int result; + int i; + int init_group_size, final_group_size; initial_size = table->keysZ; @@ -934,269 +959,269 @@ cuddZddSymmSiftingConvAux( if (x == x_low) { /* Sift down */ i = table->subtableZ[x].next; - init_group_size = x - i + 1; - - move_down = cuddZddSymmSifting_down(table, x, x_high, - initial_size); - /* after that point x --> x_high, unless early term */ - if (move_down == ZDD_MV_OOM) - goto cuddZddSymmSiftingConvAuxOutOfMem; - - if (move_down == NULL || - table->subtableZ[move_down->y].next != move_down->y) { - /* symmetry detected may have to make another complete - pass */ - if (move_down != NULL) - x = move_down->y; - else { - while ((unsigned) x < table->subtableZ[x].next); - x = table->subtableZ[x].next; - x = table->subtableZ[x].next; - } - i = x; - while ((unsigned) i < table->subtableZ[i].next) { - i = table->subtableZ[i].next; - } - final_group_size = i - x + 1; + init_group_size = x - i + 1; - if (init_group_size == final_group_size) { - /* No new symmetries detected, - go back to best position */ - result = cuddZddSymmSiftingBackward(table, move_down, + move_down = cuddZddSymmSifting_down(table, x, x_high, initial_size); + /* after that point x --> x_high, unless early term */ + if (move_down == ZDD_MV_OOM) + goto cuddZddSymmSiftingConvAuxOutOfMem; + + if (move_down == NULL || + table->subtableZ[move_down->y].next != move_down->y) { + /* symmetry detected may have to make another complete + pass */ + if (move_down != NULL) + x = move_down->y; + else { + while ((unsigned) x < table->subtableZ[x].next) + x = table->subtableZ[x].next; + x = table->subtableZ[x].next; + } + i = x; + while ((unsigned) i < table->subtableZ[i].next) { + i = table->subtableZ[i].next; + } + final_group_size = i - x + 1; + + if (init_group_size == final_group_size) { + /* No new symmetries detected, + go back to best position */ + result = cuddZddSymmSiftingBackward(table, move_down, + initial_size); + } + else { + initial_size = table->keysZ; + move_up = cuddZddSymmSifting_up(table, x, x_low, + initial_size); + result = cuddZddSymmSiftingBackward(table, move_up, + initial_size); + } } else { - initial_size = table->keysZ; - move_up = cuddZddSymmSifting_up(table, x, x_low, - initial_size); - result = cuddZddSymmSiftingBackward(table, move_up, - initial_size); + result = cuddZddSymmSiftingBackward(table, move_down, + initial_size); + /* move backward and stop at best position */ } - } - else { - result = cuddZddSymmSiftingBackward(table, move_down, - initial_size); - /* move backward and stop at best position */ - } - if (!result) - goto cuddZddSymmSiftingConvAuxOutOfMem; + if (!result) + goto cuddZddSymmSiftingConvAuxOutOfMem; } else if (x == x_high) { /* Sift up */ - /* Find top of x's symm group */ - while ((unsigned) x < table->subtableZ[x].next) + /* Find top of x's symm group */ + while ((unsigned) x < table->subtableZ[x].next) + x = table->subtableZ[x].next; x = table->subtableZ[x].next; - x = table->subtableZ[x].next; - i = x; - while ((unsigned) i < table->subtableZ[i].next) { - i = table->subtableZ[i].next; - } - init_group_size = i - x + 1; + i = x; + while ((unsigned) i < table->subtableZ[i].next) { + i = table->subtableZ[i].next; + } + init_group_size = i - x + 1; - move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size); - /* after that point x --> x_low, unless early term */ - if (move_up == ZDD_MV_OOM) - goto cuddZddSymmSiftingConvAuxOutOfMem; + move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size); + /* after that point x --> x_low, unless early term */ + if (move_up == ZDD_MV_OOM) + goto cuddZddSymmSiftingConvAuxOutOfMem; - if (move_up == NULL || - table->subtableZ[move_up->x].next != move_up->x) { - /* symmetry detected may have to make another complete - pass */ + if (move_up == NULL || + table->subtableZ[move_up->x].next != move_up->x) { + /* symmetry detected may have to make another complete + pass */ if (move_up != NULL) - x = move_up->x; - else { - while ((unsigned) x < table->subtableZ[x].next) - x = table->subtableZ[x].next; - } - i = table->subtableZ[x].next; - final_group_size = x - i + 1; + x = move_up->x; + else { + while ((unsigned) x < table->subtableZ[x].next) + x = table->subtableZ[x].next; + } + i = table->subtableZ[x].next; + final_group_size = x - i + 1; - if (init_group_size == final_group_size) { - /* No new symmetry groups detected, - return to best position */ - result = cuddZddSymmSiftingBackward(table, move_up, - initial_size); + if (init_group_size == final_group_size) { + /* No new symmetry groups detected, + return to best position */ + result = cuddZddSymmSiftingBackward(table, move_up, + initial_size); + } + else { + initial_size = table->keysZ; + move_down = cuddZddSymmSifting_down(table, x, x_high, + initial_size); + result = cuddZddSymmSiftingBackward(table, move_down, + initial_size); + } } else { - initial_size = table->keysZ; - move_down = cuddZddSymmSifting_down(table, x, x_high, - initial_size); - result = cuddZddSymmSiftingBackward(table, move_down, - initial_size); + result = cuddZddSymmSiftingBackward(table, move_up, + initial_size); + /* move backward and stop at best position */ } - } - else { - result = cuddZddSymmSiftingBackward(table, move_up, - initial_size); - /* move backward and stop at best position */ - } - if (!result) - goto cuddZddSymmSiftingConvAuxOutOfMem; + if (!result) + goto cuddZddSymmSiftingConvAuxOutOfMem; } else if ((x - x_low) > (x_high - x)) { /* must go down first: - shorter */ - move_down = cuddZddSymmSifting_down(table, x, x_high, - initial_size); - /* after that point x --> x_high */ - if (move_down == ZDD_MV_OOM) - goto cuddZddSymmSiftingConvAuxOutOfMem; - - if (move_down != NULL) { - x = move_down->y; - } - else { - while ((unsigned) x < table->subtableZ[x].next) - x = table->subtableZ[x].next; - x = table->subtableZ[x].next; - } - i = x; - while ((unsigned) i < table->subtableZ[i].next) { - i = table->subtableZ[i].next; - } - init_group_size = i - x + 1; - - move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size); - if (move_up == ZDD_MV_OOM) - goto cuddZddSymmSiftingConvAuxOutOfMem; + shorter */ + move_down = cuddZddSymmSifting_down(table, x, x_high, + initial_size); + /* after that point x --> x_high */ + if (move_down == ZDD_MV_OOM) + goto cuddZddSymmSiftingConvAuxOutOfMem; - if (move_up == NULL || - table->subtableZ[move_up->x].next != move_up->x) { - /* symmetry detected may have to make another complete - pass */ - if (move_up != NULL) { - x = move_up->x; + if (move_down != NULL) { + x = move_down->y; } else { - while ((unsigned) x < table->subtableZ[x].next) + while ((unsigned) x < table->subtableZ[x].next) + x = table->subtableZ[x].next; x = table->subtableZ[x].next; } + i = x; + while ((unsigned) i < table->subtableZ[i].next) { + i = table->subtableZ[i].next; + } + init_group_size = i - x + 1; + + move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size); + if (move_up == ZDD_MV_OOM) + goto cuddZddSymmSiftingConvAuxOutOfMem; + + if (move_up == NULL || + table->subtableZ[move_up->x].next != move_up->x) { + /* symmetry detected may have to make another complete + pass */ + if (move_up != NULL) { + x = move_up->x; + } + else { + while ((unsigned) x < table->subtableZ[x].next) + x = table->subtableZ[x].next; + } i = table->subtableZ[x].next; final_group_size = x - i + 1; if (init_group_size == final_group_size) { - /* No new symmetry groups detected, - return to best position */ + /* No new symmetry groups detected, + return to best position */ result = cuddZddSymmSiftingBackward(table, move_up, - initial_size); + initial_size); + } + else { + while (move_down != NULL) { + move = move_down->next; + cuddDeallocMove(table, move_down); + move_down = move; + } + initial_size = table->keysZ; + move_down = cuddZddSymmSifting_down(table, x, x_high, + initial_size); + result = cuddZddSymmSiftingBackward(table, move_down, + initial_size); } - else { - while (move_down != NULL) { - move = move_down->next; - cuddDeallocNode(table, (DdNode *)move_down); - move_down = move; } - initial_size = table->keysZ; - move_down = cuddZddSymmSifting_down(table, x, x_high, - initial_size); - result = cuddZddSymmSiftingBackward(table, move_down, - initial_size); + else { + result = cuddZddSymmSiftingBackward(table, move_up, + initial_size); + /* move backward and stop at best position */ } - } - else { - result = cuddZddSymmSiftingBackward(table, move_up, - initial_size); - /* move backward and stop at best position */ - } - if (!result) - goto cuddZddSymmSiftingConvAuxOutOfMem; + if (!result) + goto cuddZddSymmSiftingConvAuxOutOfMem; } else { /* moving up first:shorter */ - /* Find top of x's symmetry group */ - x = table->subtableZ[x].next; + /* Find top of x's symmetry group */ + x = table->subtableZ[x].next; - move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size); - /* after that point x --> x_high, unless early term */ - if (move_up == ZDD_MV_OOM) - goto cuddZddSymmSiftingConvAuxOutOfMem; + move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size); + /* after that point x --> x_high, unless early term */ + if (move_up == ZDD_MV_OOM) + goto cuddZddSymmSiftingConvAuxOutOfMem; - if (move_up != NULL) { - x = move_up->x; - } - else { - while ((unsigned) x < table->subtableZ[x].next) - x = table->subtableZ[x].next; - } + if (move_up != NULL) { + x = move_up->x; + } + else { + while ((unsigned) x < table->subtableZ[x].next) + x = table->subtableZ[x].next; + } i = table->subtableZ[x].next; init_group_size = x - i + 1; - move_down = cuddZddSymmSifting_down(table, x, x_high, - initial_size); - if (move_down == ZDD_MV_OOM) - goto cuddZddSymmSiftingConvAuxOutOfMem; + move_down = cuddZddSymmSifting_down(table, x, x_high, + initial_size); + if (move_down == ZDD_MV_OOM) + goto cuddZddSymmSiftingConvAuxOutOfMem; - if (move_down == NULL || - table->subtableZ[move_down->y].next != move_down->y) { - /* symmetry detected may have to make another complete - pass */ + if (move_down == NULL || + table->subtableZ[move_down->y].next != move_down->y) { + /* symmetry detected may have to make another complete + pass */ if (move_down != NULL) { - x = move_down->y; - } - else { - while ((unsigned) x < table->subtableZ[x].next) - x = table->subtableZ[x].next; - x = table->subtableZ[x].next; - } + x = move_down->y; + } + else { + while ((unsigned) x < table->subtableZ[x].next) + x = table->subtableZ[x].next; + x = table->subtableZ[x].next; + } i = x; while ((unsigned) i < table->subtableZ[i].next) { i = table->subtableZ[i].next; } - final_group_size = i - x + 1; + final_group_size = i - x + 1; if (init_group_size == final_group_size) { - /* No new symmetries detected, - go back to best position */ + /* No new symmetries detected, + go back to best position */ result = cuddZddSymmSiftingBackward(table, move_down, - initial_size); + initial_size); + } + else { + while (move_up != NULL) { + move = move_up->next; + cuddDeallocMove(table, move_up); + move_up = move; + } + initial_size = table->keysZ; + move_up = cuddZddSymmSifting_up(table, x, x_low, + initial_size); + result = cuddZddSymmSiftingBackward(table, move_up, + initial_size); } - else { - while (move_up != NULL) { - move = move_up->next; - cuddDeallocNode(table, (DdNode *)move_up); - move_up = move; } - initial_size = table->keysZ; - move_up = cuddZddSymmSifting_up(table, x, x_low, - initial_size); - result = cuddZddSymmSiftingBackward(table, move_up, - initial_size); + else { + result = cuddZddSymmSiftingBackward(table, move_down, + initial_size); + /* move backward and stop at best position */ } - } - else { - result = cuddZddSymmSiftingBackward(table, move_down, - initial_size); - /* move backward and stop at best position */ - } - if (!result) - goto cuddZddSymmSiftingConvAuxOutOfMem; + if (!result) + goto cuddZddSymmSiftingConvAuxOutOfMem; } while (move_down != NULL) { - move = move_down->next; - cuddDeallocNode(table, (DdNode *)move_down); - move_down = move; + move = move_down->next; + cuddDeallocMove(table, move_down); + move_down = move; } while (move_up != NULL) { - move = move_up->next; - cuddDeallocNode(table, (DdNode *)move_up); - move_up = move; + move = move_up->next; + cuddDeallocMove(table, move_up); + move_up = move; } return(1); cuddZddSymmSiftingConvAuxOutOfMem: if (move_down != ZDD_MV_OOM) { - while (move_down != NULL) { - move = move_down->next; - cuddDeallocNode(table, (DdNode *)move_down); - move_down = move; - } + while (move_down != NULL) { + move = move_down->next; + cuddDeallocMove(table, move_down); + move_down = move; + } } if (move_up != ZDD_MV_OOM) { - while (move_up != NULL) { - move = move_up->next; - cuddDeallocNode(table, (DdNode *)move_up); - move_up = move; - } + while (move_up != NULL) { + move = move_up->next; + cuddDeallocMove(table, move_up); + move_up = move; + } } return(0); @@ -1228,64 +1253,64 @@ cuddZddSymmSifting_up( int x_low, int initial_size) { - Move *moves; - Move *move; - int y; - int size; - int limit_size = initial_size; - int i, gytop; + Move *moves; + Move *move; + int y; + int size; + int limit_size = initial_size; + int i, gytop; moves = NULL; y = cuddZddNextLow(table, x); while (y >= x_low) { - gytop = table->subtableZ[y].next; - if (cuddZddSymmCheck(table, y, x)) { - /* Symmetry found, attach symm groups */ - table->subtableZ[y].next = x; - i = table->subtableZ[x].next; - while (table->subtableZ[i].next != (unsigned) x) - i = table->subtableZ[i].next; - table->subtableZ[i].next = gytop; - } - else if ((table->subtableZ[x].next == (unsigned) x) && - (table->subtableZ[y].next == (unsigned) y)) { - /* x and y have self symmetry */ - size = cuddZddSwapInPlace(table, y, x); - if (size == 0) - goto cuddZddSymmSifting_upOutOfMem; - move = (Move *)cuddDynamicAllocNode(table); - if (move == NULL) - goto cuddZddSymmSifting_upOutOfMem; - move->x = y; - move->y = x; - move->size = size; - move->next = moves; - moves = move; - if ((double)size > - (double)limit_size * table->maxGrowth) - return(moves); - if (size < limit_size) - limit_size = size; - } - else { /* Group move */ - size = zdd_group_move(table, y, x, &moves); - if ((double)size > - (double)limit_size * table->maxGrowth) - return(moves); - if (size < limit_size) - limit_size = size; - } - x = gytop; - y = cuddZddNextLow(table, x); + gytop = table->subtableZ[y].next; + if (cuddZddSymmCheck(table, y, x)) { + /* Symmetry found, attach symm groups */ + table->subtableZ[y].next = x; + i = table->subtableZ[x].next; + while (table->subtableZ[i].next != (unsigned) x) + i = table->subtableZ[i].next; + table->subtableZ[i].next = gytop; + } + else if ((table->subtableZ[x].next == (unsigned) x) && + (table->subtableZ[y].next == (unsigned) y)) { + /* x and y have self symmetry */ + size = cuddZddSwapInPlace(table, y, x); + if (size == 0) + goto cuddZddSymmSifting_upOutOfMem; + move = (Move *)cuddDynamicAllocNode(table); + if (move == NULL) + goto cuddZddSymmSifting_upOutOfMem; + move->x = y; + move->y = x; + move->size = size; + move->next = moves; + moves = move; + if ((double)size > + (double)limit_size * table->maxGrowth) + return(moves); + if (size < limit_size) + limit_size = size; + } + else { /* Group move */ + size = zdd_group_move(table, y, x, &moves); + if ((double)size > + (double)limit_size * table->maxGrowth) + return(moves); + if (size < limit_size) + limit_size = size; + } + x = gytop; + y = cuddZddNextLow(table, x); } return(moves); cuddZddSymmSifting_upOutOfMem: while (moves != NULL) { - move = moves->next; - cuddDeallocNode(table, (DdNode *)moves); - moves = move; + move = moves->next; + cuddDeallocMove(table, moves); + moves = move; } return(ZDD_MV_OOM); @@ -1316,69 +1341,69 @@ cuddZddSymmSifting_down( int x_high, int initial_size) { - Move *moves; - Move *move; - int y; - int size; - int limit_size = initial_size; - int i, gxtop, gybot; + Move *moves; + Move *move; + int y; + int size; + int limit_size = initial_size; + int i, gxtop, gybot; moves = NULL; y = cuddZddNextHigh(table, x); while (y <= x_high) { - gybot = table->subtableZ[y].next; - while (table->subtableZ[gybot].next != (unsigned) y) - gybot = table->subtableZ[gybot].next; - if (cuddZddSymmCheck(table, x, y)) { - /* Symmetry found, attach symm groups */ - gxtop = table->subtableZ[x].next; - table->subtableZ[x].next = y; - i = table->subtableZ[y].next; - while (table->subtableZ[i].next != (unsigned) y) - i = table->subtableZ[i].next; - table->subtableZ[i].next = gxtop; - } - else if ((table->subtableZ[x].next == (unsigned) x) && - (table->subtableZ[y].next == (unsigned) y)) { - /* x and y have self symmetry */ - size = cuddZddSwapInPlace(table, x, y); - if (size == 0) - goto cuddZddSymmSifting_downOutOfMem; - move = (Move *)cuddDynamicAllocNode(table); - if (move == NULL) - goto cuddZddSymmSifting_downOutOfMem; - move->x = x; - move->y = y; - move->size = size; - move->next = moves; - moves = move; - if ((double)size > - (double)limit_size * table->maxGrowth) - return(moves); - if (size < limit_size) - limit_size = size; - x = y; + gybot = table->subtableZ[y].next; + while (table->subtableZ[gybot].next != (unsigned) y) + gybot = table->subtableZ[gybot].next; + if (cuddZddSymmCheck(table, x, y)) { + /* Symmetry found, attach symm groups */ + gxtop = table->subtableZ[x].next; + table->subtableZ[x].next = y; + i = table->subtableZ[y].next; + while (table->subtableZ[i].next != (unsigned) y) + i = table->subtableZ[i].next; + table->subtableZ[i].next = gxtop; + } + else if ((table->subtableZ[x].next == (unsigned) x) && + (table->subtableZ[y].next == (unsigned) y)) { + /* x and y have self symmetry */ + size = cuddZddSwapInPlace(table, x, y); + if (size == 0) + goto cuddZddSymmSifting_downOutOfMem; + move = (Move *)cuddDynamicAllocNode(table); + if (move == NULL) + goto cuddZddSymmSifting_downOutOfMem; + move->x = x; + move->y = y; + move->size = size; + move->next = moves; + moves = move; + if ((double)size > + (double)limit_size * table->maxGrowth) + return(moves); + if (size < limit_size) + limit_size = size; + x = y; + y = cuddZddNextHigh(table, x); + } + else { /* Group move */ + size = zdd_group_move(table, x, y, &moves); + if ((double)size > + (double)limit_size * table->maxGrowth) + return(moves); + if (size < limit_size) + limit_size = size; + } + x = gybot; y = cuddZddNextHigh(table, x); } - else { /* Group move */ - size = zdd_group_move(table, x, y, &moves); - if ((double)size > - (double)limit_size * table->maxGrowth) - return(moves); - if (size < limit_size) - limit_size = size; - } - x = gybot; - y = cuddZddNextHigh(table, x); - } return(moves); cuddZddSymmSifting_downOutOfMem: while (moves != NULL) { - move = moves->next; - cuddDeallocNode(table, (DdNode *)moves); - moves = move; + move = moves->next; + cuddDeallocMove(table, moves); + moves = move; } return(ZDD_MV_OOM); @@ -1406,31 +1431,31 @@ cuddZddSymmSiftingBackward( Move * moves, int size) { - int i; - int i_best; - Move *move; - int res; + int i; + int i_best; + Move *move; + int res; i_best = -1; for (move = moves, i = 0; move != NULL; move = move->next, i++) { - if (move->size < size) { - i_best = i; - size = move->size; - } + if (move->size < size) { + i_best = i; + size = move->size; + } } for (move = moves, i = 0; move != NULL; move = move->next, i++) { - if (i == i_best) break; - if ((table->subtableZ[move->x].next == move->x) && - (table->subtableZ[move->y].next == move->y)) { - res = cuddZddSwapInPlace(table, move->x, move->y); - if (!res) return(0); - } - else { /* Group move necessary */ - res = zdd_group_move_backward(table, move->x, move->y); - } - if (i_best == -1 && res == size) - break; + if (i == i_best) break; + if ((table->subtableZ[move->x].next == move->x) && + (table->subtableZ[move->y].next == move->y)) { + res = cuddZddSwapInPlace(table, move->x, move->y); + if (!res) return(0); + } + else { /* Group move necessary */ + res = zdd_group_move_backward(table, move->x, move->y); + } + if (i_best == -1 && res == size) + break; } return(1); @@ -1459,75 +1484,74 @@ zdd_group_move( int y, Move ** moves) { - Move *move; - int size; - int i, temp, gxtop, gxbot, gytop, gybot, yprev; - int swapx = 0, swapy = 0; // Suppress "might be used uninitialized" + Move *move; + int size; + int i, temp, gxtop, gxbot, gybot, yprev; + int swapx, swapy; #ifdef DD_DEBUG - assert(x < y); /* we assume that x < y */ + assert(x < y); /* we assume that x < y */ #endif /* Find top and bottom for the two groups. */ gxtop = table->subtableZ[x].next; - gytop = y; gxbot = x; gybot = table->subtableZ[y].next; while (table->subtableZ[gybot].next != (unsigned) y) - gybot = table->subtableZ[gybot].next; + gybot = table->subtableZ[gybot].next; yprev = gybot; while (x <= y) { - while (y > gxtop) { - /* Set correct symmetries. */ - temp = table->subtableZ[x].next; - if (temp == x) - temp = y; - i = gxtop; - for (;;) { - if (table->subtableZ[i].next == (unsigned) x) { - table->subtableZ[i].next = y; - break; - } else { - i = table->subtableZ[i].next; - } - } - if (table->subtableZ[y].next != (unsigned) y) { - table->subtableZ[x].next = table->subtableZ[y].next; - } else { - table->subtableZ[x].next = x; - } + while (y > gxtop) { + /* Set correct symmetries. */ + temp = table->subtableZ[x].next; + if (temp == x) + temp = y; + i = gxtop; + for (;;) { + if (table->subtableZ[i].next == (unsigned) x) { + table->subtableZ[i].next = y; + break; + } else { + i = table->subtableZ[i].next; + } + } + if (table->subtableZ[y].next != (unsigned) y) { + table->subtableZ[x].next = table->subtableZ[y].next; + } else { + table->subtableZ[x].next = x; + } - if (yprev != y) { - table->subtableZ[yprev].next = x; - } else { - yprev = x; - } - table->subtableZ[y].next = temp; + if (yprev != y) { + table->subtableZ[yprev].next = x; + } else { + yprev = x; + } + table->subtableZ[y].next = temp; - size = cuddZddSwapInPlace(table, x, y); - if (size == 0) - goto zdd_group_moveOutOfMem; + size = cuddZddSwapInPlace(table, x, y); + if (size == 0) + goto zdd_group_moveOutOfMem; swapx = x; - swapy = y; - y = x; - x--; - } /* while y > gxtop */ - - /* Trying to find the next y. */ - if (table->subtableZ[y].next <= (unsigned) y) { - gybot = y; - } else { - y = table->subtableZ[y].next; - } + swapy = y; + y = x; + x--; + } /* while y > gxtop */ + + /* Trying to find the next y. */ + if (table->subtableZ[y].next <= (unsigned) y) { + gybot = y; + } else { + y = table->subtableZ[y].next; + } - yprev = gxtop; - gxtop++; - gxbot++; - x = gxbot; + yprev = gxtop; + gxtop++; + gxbot++; + x = gxbot; } /* while x <= y, end of group movement */ move = (Move *)cuddDynamicAllocNode(table); if (move == NULL) - goto zdd_group_moveOutOfMem; + goto zdd_group_moveOutOfMem; move->x = swapx; move->y = swapy; move->size = table->keysZ; @@ -1538,9 +1562,9 @@ zdd_group_move( zdd_group_moveOutOfMem: while (*moves != NULL) { - move = (*moves)->next; - cuddDeallocNode(table, (DdNode *)(*moves)); - *moves = move; + move = (*moves)->next; + cuddDeallocMove(table, *moves); + *moves = move; } return(0); @@ -1566,67 +1590,66 @@ zdd_group_move_backward( int x, int y) { - int size = -1; // Suppress "might be used uninitialized" - int i, temp, gxtop, gxbot, gytop, gybot, yprev; + int size; + int i, temp, gxtop, gxbot, gybot, yprev; #ifdef DD_DEBUG - assert(x < y); /* we assume that x < y */ + assert(x < y); /* we assume that x < y */ #endif /* Find top and bottom of the two groups. */ gxtop = table->subtableZ[x].next; - gytop = y; gxbot = x; gybot = table->subtableZ[y].next; while (table->subtableZ[gybot].next != (unsigned) y) - gybot = table->subtableZ[gybot].next; + gybot = table->subtableZ[gybot].next; yprev = gybot; while (x <= y) { - while (y > gxtop) { - /* Set correct symmetries. */ - temp = table->subtableZ[x].next; - if (temp == x) - temp = y; - i = gxtop; - for (;;) { - if (table->subtableZ[i].next == (unsigned) x) { - table->subtableZ[i].next = y; - break; - } else { - i = table->subtableZ[i].next; - } - } - if (table->subtableZ[y].next != (unsigned) y) { - table->subtableZ[x].next = table->subtableZ[y].next; - } else { - table->subtableZ[x].next = x; - } + while (y > gxtop) { + /* Set correct symmetries. */ + temp = table->subtableZ[x].next; + if (temp == x) + temp = y; + i = gxtop; + for (;;) { + if (table->subtableZ[i].next == (unsigned) x) { + table->subtableZ[i].next = y; + break; + } else { + i = table->subtableZ[i].next; + } + } + if (table->subtableZ[y].next != (unsigned) y) { + table->subtableZ[x].next = table->subtableZ[y].next; + } else { + table->subtableZ[x].next = x; + } - if (yprev != y) { - table->subtableZ[yprev].next = x; + if (yprev != y) { + table->subtableZ[yprev].next = x; + } else { + yprev = x; + } + table->subtableZ[y].next = temp; + + size = cuddZddSwapInPlace(table, x, y); + if (size == 0) + return(0); + y = x; + x--; + } /* while y > gxtop */ + + /* Trying to find the next y. */ + if (table->subtableZ[y].next <= (unsigned) y) { + gybot = y; } else { - yprev = x; + y = table->subtableZ[y].next; } - table->subtableZ[y].next = temp; - - size = cuddZddSwapInPlace(table, x, y); - if (size == 0) - return(0); - y = x; - x--; - } /* while y > gxtop */ - - /* Trying to find the next y. */ - if (table->subtableZ[y].next <= (unsigned) y) { - gybot = y; - } else { - y = table->subtableZ[y].next; - } - yprev = gxtop; - gxtop++; - gxbot++; - x = gxbot; + yprev = gxtop; + gxtop++; + gxbot++; + x = gxbot; } /* while x <= y, end of group movement backward */ return(size); @@ -1657,19 +1680,19 @@ cuddZddSymmSummary( int TotalSymmGroups = 0; for (i = lower; i <= upper; i++) { - if (table->subtableZ[i].next != (unsigned) i) { - TotalSymmGroups++; - x = i; - do { - TotalSymm++; - gbot = x; - x = table->subtableZ[x].next; - } while (x != i); + if (table->subtableZ[i].next != (unsigned) i) { + TotalSymmGroups++; + x = i; + do { + TotalSymm++; + gbot = x; + x = table->subtableZ[x].next; + } while (x != i); #ifdef DD_DEBUG - assert(table->subtableZ[gbot].next == (unsigned) i); + assert(table->subtableZ[gbot].next == (unsigned) i); #endif - i = gbot; - } + i = gbot; + } } *symvars = TotalSymm; *symgroups = TotalSymmGroups; @@ -1678,5 +1701,7 @@ cuddZddSymmSummary( } /* end of cuddZddSymmSummary */ + ABC_NAMESPACE_IMPL_END + -- cgit v1.2.3