#include "util_hack.h"
#include "cuddInt.h"
Go to the source code of this file.
Defines | |
#define | MV_OOM (Move *)1 |
Functions | |
static int ddSymmUniqueCompare | ARGS ((int *ptrX, int *ptrY)) |
static int ddSymmSiftingAux | 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)) |
void | Cudd_SymmProfile (DdManager *table, int lower, int upper) |
int | cuddSymmCheck (DdManager *table, int x, int y) |
int | cuddSymmSifting (DdManager *table, int lower, int upper) |
int | cuddSymmSiftingConv (DdManager *table, int lower, int upper) |
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) |
Variables | |
static char rcsid[] | DD_UNUSED = "$Id: cuddSymmetry.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $" |
static int * | entry |
int | ddTotalNumberSwapping |
#define MV_OOM (Move *)1 |
CFile***********************************************************************
FileName [cuddSymmetry.c]
PackageName [cudd]
Synopsis [Functions for symmetry-based variable reordering.]
Description [External procedures included in this file:
Internal procedures included in this module:
Static procedures included in this module:
]
Author [Shipra Panda, Fabio Somenzi]
Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]
Definition at line 48 of file cuddSymmetry.c.
static void ddSymmSummary ARGS | ( | (DdManager *table, int lower, int upper, int *symvars, int *symgroups) | ) | [static] |
static int ddSymmGroupMoveBackward ARGS | ( | (DdManager *table, int x, int y) | ) | [static] |
static int ddSymmSiftingConvAux ARGS | ( | (DdManager *table, int x, int xLow, int xHigh) | ) | [static] |
static int ddSymmUniqueCompare ARGS | ( | (int *ptrX, int *ptrY) | ) | [static] |
AutomaticStart
void Cudd_SymmProfile | ( | DdManager * | table, | |
int | lower, | |||
int | upper | |||
) |
AutomaticEnd Function********************************************************************
Synopsis [Prints statistics on symmetric variables.]
Description []
SideEffects [None]
Definition at line 111 of file cuddSymmetry.c.
00115 { 00116 int i,x,gbot; 00117 int TotalSymm = 0; 00118 int TotalSymmGroups = 0; 00119 00120 for (i = lower; i <= upper; i++) { 00121 if (table->subtables[i].next != (unsigned) i) { 00122 x = i; 00123 (void) fprintf(table->out,"Group:"); 00124 do { 00125 (void) fprintf(table->out," %d",table->invperm[x]); 00126 TotalSymm++; 00127 gbot = x; 00128 x = table->subtables[x].next; 00129 } while (x != i); 00130 TotalSymmGroups++; 00131 #ifdef DD_DEBUG 00132 assert(table->subtables[gbot].next == (unsigned) i); 00133 #endif 00134 i = gbot; 00135 (void) fprintf(table->out,"\n"); 00136 } 00137 } 00138 (void) fprintf(table->out,"Total Symmetric = %d\n",TotalSymm); 00139 (void) fprintf(table->out,"Total Groups = %d\n",TotalSymmGroups); 00140 00141 } /* end of Cudd_SymmProfile */
int cuddSymmCheck | ( | DdManager * | table, | |
int | x, | |||
int | y | |||
) |
Function********************************************************************
Synopsis [Checks for symmetry of x and y.]
Description [Checks for symmetry of x and y. Ignores projection functions, unless they are isolated. Returns 1 in case of symmetry; 0 otherwise.]
SideEffects [None]
Definition at line 161 of file cuddSymmetry.c.
00165 { 00166 DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10; 00167 int comple; /* f0 is complemented */ 00168 int xsymmy; /* x and y may be positively symmetric */ 00169 int xsymmyp; /* x and y may be negatively symmetric */ 00170 int arccount; /* number of arcs from layer x to layer y */ 00171 int TotalRefCount; /* total reference count of layer y minus 1 */ 00172 int yindex; 00173 int i; 00174 DdNodePtr *list; 00175 int slots; 00176 DdNode *sentinel = &(table->sentinel); 00177 #ifdef DD_DEBUG 00178 int xindex; 00179 #endif 00180 00181 /* Checks that x and y are not the projection functions. 00182 ** For x it is sufficient to check whether there is only one 00183 ** node; indeed, if there is one node, it is the projection function 00184 ** and it cannot point to y. Hence, if y isn't just the projection 00185 ** function, it has one arc coming from a layer different from x. 00186 */ 00187 if (table->subtables[x].keys == 1) { 00188 return(0); 00189 } 00190 yindex = table->invperm[y]; 00191 if (table->subtables[y].keys == 1) { 00192 if (table->vars[yindex]->ref == 1) 00193 return(0); 00194 } 00195 00196 xsymmy = xsymmyp = 1; 00197 arccount = 0; 00198 slots = table->subtables[x].slots; 00199 list = table->subtables[x].nodelist; 00200 for (i = 0; i < slots; i++) { 00201 f = list[i]; 00202 while (f != sentinel) { 00203 /* Find f1, f0, f11, f10, f01, f00. */ 00204 f1 = cuddT(f); 00205 f0 = Cudd_Regular(cuddE(f)); 00206 comple = Cudd_IsComplement(cuddE(f)); 00207 if ((int) f1->index == yindex) { 00208 arccount++; 00209 f11 = cuddT(f1); f10 = cuddE(f1); 00210 } else { 00211 if ((int) f0->index != yindex) { 00212 /* If f is an isolated projection function it is 00213 ** allowed to bypass layer y. 00214 */ 00215 if (f1 != DD_ONE(table) || f0 != DD_ONE(table) || f->ref != 1) 00216 return(0); /* f bypasses layer y */ 00217 } 00218 f11 = f10 = f1; 00219 } 00220 if ((int) f0->index == yindex) { 00221 arccount++; 00222 f01 = cuddT(f0); f00 = cuddE(f0); 00223 } else { 00224 f01 = f00 = f0; 00225 } 00226 if (comple) { 00227 f01 = Cudd_Not(f01); 00228 f00 = Cudd_Not(f00); 00229 } 00230 00231 if (f1 != DD_ONE(table) || f0 != DD_ONE(table) || f->ref != 1) { 00232 xsymmy &= f01 == f10; 00233 xsymmyp &= f11 == f00; 00234 if ((xsymmy == 0) && (xsymmyp == 0)) 00235 return(0); 00236 } 00237 00238 f = f->next; 00239 } /* while */ 00240 } /* for */ 00241 00242 /* Calculate the total reference counts of y */ 00243 TotalRefCount = -1; /* -1 for projection function */ 00244 slots = table->subtables[y].slots; 00245 list = table->subtables[y].nodelist; 00246 for (i = 0; i < slots; i++) { 00247 f = list[i]; 00248 while (f != sentinel) { 00249 TotalRefCount += f->ref; 00250 f = f->next; 00251 } 00252 } 00253 00254 #if defined(DD_DEBUG) && defined(DD_VERBOSE) 00255 if (arccount == TotalRefCount) { 00256 xindex = table->invperm[x]; 00257 (void) fprintf(table->out, 00258 "Found symmetry! x =%d\ty = %d\tPos(%d,%d)\n", 00259 xindex,yindex,x,y); 00260 } 00261 #endif 00262 00263 return(arccount == TotalRefCount); 00264 00265 } /* end of cuddSymmCheck */
int cuddSymmSifting | ( | DdManager * | table, | |
int | lower, | |||
int | upper | |||
) |
Function********************************************************************
Synopsis [Symmetric sifting algorithm.]
Description [Symmetric sifting algorithm. Assumes that no dead nodes are present.
Returns 1 plus the number of symmetric variables if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [cuddSymmSiftingConv]
Definition at line 291 of file cuddSymmetry.c.
00295 { 00296 int i; 00297 int *var; 00298 int size; 00299 int x; 00300 int result; 00301 int symvars; 00302 int symgroups; 00303 #ifdef DD_STATS 00304 int previousSize; 00305 #endif 00306 00307 size = table->size; 00308 00309 /* Find order in which to sift variables. */ 00310 var = NULL; 00311 entry = ALLOC(int,size); 00312 if (entry == NULL) { 00313 table->errorCode = CUDD_MEMORY_OUT; 00314 goto ddSymmSiftingOutOfMem; 00315 } 00316 var = ALLOC(int,size); 00317 if (var == NULL) { 00318 table->errorCode = CUDD_MEMORY_OUT; 00319 goto ddSymmSiftingOutOfMem; 00320 } 00321 00322 for (i = 0; i < size; i++) { 00323 x = table->perm[i]; 00324 entry[i] = table->subtables[x].keys; 00325 var[i] = i; 00326 } 00327 00328 qsort((void *)var,size,sizeof(int),(int (*)(const void *, const void *))ddSymmUniqueCompare); 00329 00330 /* Initialize the symmetry of each subtable to itself. */ 00331 for (i = lower; i <= upper; i++) { 00332 table->subtables[i].next = i; 00333 } 00334 00335 for (i = 0; i < ddMin(table->siftMaxVar,size); i++) { 00336 if (ddTotalNumberSwapping >= table->siftMaxSwap) 00337 break; 00338 x = table->perm[var[i]]; 00339 #ifdef DD_STATS 00340 previousSize = table->keys - table->isolated; 00341 #endif 00342 if (x < lower || x > upper) continue; 00343 if (table->subtables[x].next == (unsigned) x) { 00344 result = ddSymmSiftingAux(table,x,lower,upper); 00345 if (!result) goto ddSymmSiftingOutOfMem; 00346 #ifdef DD_STATS 00347 if (table->keys < (unsigned) previousSize + table->isolated) { 00348 (void) fprintf(table->out,"-"); 00349 } else if (table->keys > (unsigned) previousSize + 00350 table->isolated) { 00351 (void) fprintf(table->out,"+"); /* should never happen */ 00352 } else { 00353 (void) fprintf(table->out,"="); 00354 } 00355 fflush(table->out); 00356 #endif 00357 } 00358 } 00359 00360 FREE(var); 00361 FREE(entry); 00362 00363 ddSymmSummary(table, lower, upper, &symvars, &symgroups); 00364 00365 #ifdef DD_STATS 00366 (void) fprintf(table->out, "\n#:S_SIFTING %8d: symmetric variables\n", 00367 symvars); 00368 (void) fprintf(table->out, "#:G_SIFTING %8d: symmetric groups", 00369 symgroups); 00370 #endif 00371 00372 return(1+symvars); 00373 00374 ddSymmSiftingOutOfMem: 00375 00376 if (entry != NULL) FREE(entry); 00377 if (var != NULL) FREE(var); 00378 00379 return(0); 00380 00381 } /* end of cuddSymmSifting */
int cuddSymmSiftingConv | ( | DdManager * | table, | |
int | lower, | |||
int | upper | |||
) |
Function********************************************************************
Synopsis [Symmetric sifting to convergence algorithm.]
Description [Symmetric sifting to convergence algorithm. Assumes that no dead nodes are present.
Returns 1 plus the number of symmetric variables if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [cuddSymmSifting]
Definition at line 408 of file cuddSymmetry.c.
00412 { 00413 int i; 00414 int *var; 00415 int size; 00416 int x; 00417 int result; 00418 int symvars; 00419 int symgroups; 00420 int classes; 00421 int initialSize; 00422 #ifdef DD_STATS 00423 int previousSize; 00424 #endif 00425 00426 initialSize = table->keys - table->isolated; 00427 00428 size = table->size; 00429 00430 /* Find order in which to sift variables. */ 00431 var = NULL; 00432 entry = ALLOC(int,size); 00433 if (entry == NULL) { 00434 table->errorCode = CUDD_MEMORY_OUT; 00435 goto ddSymmSiftingConvOutOfMem; 00436 } 00437 var = ALLOC(int,size); 00438 if (var == NULL) { 00439 table->errorCode = CUDD_MEMORY_OUT; 00440 goto ddSymmSiftingConvOutOfMem; 00441 } 00442 00443 for (i = 0; i < size; i++) { 00444 x = table->perm[i]; 00445 entry[i] = table->subtables[x].keys; 00446 var[i] = i; 00447 } 00448 00449 qsort((void *)var,size,sizeof(int),(int (*)(const void *, const void *))ddSymmUniqueCompare); 00450 00451 /* Initialize the symmetry of each subtable to itself 00452 ** for first pass of converging symmetric sifting. 00453 */ 00454 for (i = lower; i <= upper; i++) { 00455 table->subtables[i].next = i; 00456 } 00457 00458 for (i = 0; i < ddMin(table->siftMaxVar, table->size); i++) { 00459 if (ddTotalNumberSwapping >= table->siftMaxSwap) 00460 break; 00461 x = table->perm[var[i]]; 00462 if (x < lower || x > upper) continue; 00463 /* Only sift if not in symmetry group already. */ 00464 if (table->subtables[x].next == (unsigned) x) { 00465 #ifdef DD_STATS 00466 previousSize = table->keys - table->isolated; 00467 #endif 00468 result = ddSymmSiftingAux(table,x,lower,upper); 00469 if (!result) goto ddSymmSiftingConvOutOfMem; 00470 #ifdef DD_STATS 00471 if (table->keys < (unsigned) previousSize + table->isolated) { 00472 (void) fprintf(table->out,"-"); 00473 } else if (table->keys > (unsigned) previousSize + 00474 table->isolated) { 00475 (void) fprintf(table->out,"+"); 00476 } else { 00477 (void) fprintf(table->out,"="); 00478 } 00479 fflush(table->out); 00480 #endif 00481 } 00482 } 00483 00484 /* Sifting now until convergence. */ 00485 while ((unsigned) initialSize > table->keys - table->isolated) { 00486 initialSize = table->keys - table->isolated; 00487 #ifdef DD_STATS 00488 (void) fprintf(table->out,"\n"); 00489 #endif 00490 /* Here we consider only one representative for each symmetry class. */ 00491 for (x = lower, classes = 0; x <= upper; x++, classes++) { 00492 while ((unsigned) x < table->subtables[x].next) { 00493 x = table->subtables[x].next; 00494 } 00495 /* Here x is the largest index in a group. 00496 ** Groups consist of adjacent variables. 00497 ** Hence, the next increment of x will move it to a new group. 00498 */ 00499 i = table->invperm[x]; 00500 entry[i] = table->subtables[x].keys; 00501 var[classes] = i; 00502 } 00503 00504 qsort((void *)var,classes,sizeof(int),(int (*)(const void *, const void *))ddSymmUniqueCompare); 00505 00506 /* Now sift. */ 00507 for (i = 0; i < ddMin(table->siftMaxVar,classes); i++) { 00508 if (ddTotalNumberSwapping >= table->siftMaxSwap) 00509 break; 00510 x = table->perm[var[i]]; 00511 if ((unsigned) x >= table->subtables[x].next) { 00512 #ifdef DD_STATS 00513 previousSize = table->keys - table->isolated; 00514 #endif 00515 result = ddSymmSiftingConvAux(table,x,lower,upper); 00516 if (!result ) goto ddSymmSiftingConvOutOfMem; 00517 #ifdef DD_STATS 00518 if (table->keys < (unsigned) previousSize + table->isolated) { 00519 (void) fprintf(table->out,"-"); 00520 } else if (table->keys > (unsigned) previousSize + 00521 table->isolated) { 00522 (void) fprintf(table->out,"+"); 00523 } else { 00524 (void) fprintf(table->out,"="); 00525 } 00526 fflush(table->out); 00527 #endif 00528 } 00529 } /* for */ 00530 } 00531 00532 ddSymmSummary(table, lower, upper, &symvars, &symgroups); 00533 00534 #ifdef DD_STATS 00535 (void) fprintf(table->out, "\n#:S_SIFTING %8d: symmetric variables\n", 00536 symvars); 00537 (void) fprintf(table->out, "#:G_SIFTING %8d: symmetric groups", 00538 symgroups); 00539 #endif 00540 00541 FREE(var); 00542 FREE(entry); 00543 00544 return(1+symvars); 00545 00546 ddSymmSiftingConvOutOfMem: 00547 00548 if (entry != NULL) FREE(entry); 00549 if (var != NULL) FREE(var); 00550 00551 return(0); 00552 00553 } /* end of cuddSymmSiftingConv */
Function********************************************************************
Synopsis [Swaps two groups.]
Description [Swaps two groups. x is assumed to be the bottom variable of the first group. y is assumed to be the top variable of the second group. Updates the list of moves. Returns the number of keys in the table if successful; 0 otherwise.]
SideEffects [None]
Definition at line 1441 of file cuddSymmetry.c.
01446 { 01447 Move *move; 01448 int size; 01449 int i,j; 01450 int xtop,xbot,xsize,ytop,ybot,ysize,newxtop; 01451 int swapx,swapy; 01452 01453 #if DD_DEBUG 01454 assert(x < y); /* we assume that x < y */ 01455 #endif 01456 /* Find top, bottom, and size for the two groups. */ 01457 xbot = x; 01458 xtop = table->subtables[x].next; 01459 xsize = xbot - xtop + 1; 01460 ybot = y; 01461 while ((unsigned) ybot < table->subtables[ybot].next) 01462 ybot = table->subtables[ybot].next; 01463 ytop = y; 01464 ysize = ybot - ytop + 1; 01465 01466 /* Sift the variables of the second group up through the first group. */ 01467 for (i = 1; i <= ysize; i++) { 01468 for (j = 1; j <= xsize; j++) { 01469 size = cuddSwapInPlace(table,x,y); 01470 if (size == 0) return(0); 01471 swapx = x; swapy = y; 01472 y = x; 01473 x = y - 1; 01474 } 01475 y = ytop + i; 01476 x = y - 1; 01477 } 01478 01479 /* fix symmetries */ 01480 y = xtop; /* ytop is now where xtop used to be */ 01481 for (i = 0; i < ysize-1 ; i++) { 01482 table->subtables[y].next = y + 1; 01483 y = y + 1; 01484 } 01485 table->subtables[y].next = xtop; /* y is bottom of its group, join */ 01486 /* its symmetry to top of its group */ 01487 x = y + 1; 01488 newxtop = x; 01489 for (i = 0; i < xsize - 1 ; i++) { 01490 table->subtables[x].next = x + 1; 01491 x = x + 1; 01492 } 01493 table->subtables[x].next = newxtop; /* x is bottom of its group, join */ 01494 /* its symmetry to top of its group */ 01495 /* Store group move */ 01496 move = (Move *) cuddDynamicAllocNode(table); 01497 if (move == NULL) return(0); 01498 move->x = swapx; 01499 move->y = swapy; 01500 move->size = size; 01501 move->next = *moves; 01502 *moves = move; 01503 01504 return(size); 01505 01506 } /* end of ddSymmGroupMove */
static int ddSymmGroupMoveBackward | ( | DdManager * | table, | |
int | x, | |||
int | y | |||
) | [static] |
Function********************************************************************
Synopsis [Undoes the swap of two groups.]
Description [Undoes the swap of two groups. x is assumed to be the bottom variable of the first group. y is assumed to be the top variable of the second group. Returns the number of keys in the table if successful; 0 otherwise.]
SideEffects [None]
Definition at line 1522 of file cuddSymmetry.c.
01526 { 01527 int size; 01528 int i,j; 01529 int xtop,xbot,xsize,ytop,ybot,ysize,newxtop; 01530 01531 #if DD_DEBUG 01532 assert(x < y); /* We assume that x < y */ 01533 #endif 01534 01535 /* Find top, bottom, and size for the two groups. */ 01536 xbot = x; 01537 xtop = table->subtables[x].next; 01538 xsize = xbot - xtop + 1; 01539 ybot = y; 01540 while ((unsigned) ybot < table->subtables[ybot].next) 01541 ybot = table->subtables[ybot].next; 01542 ytop = y; 01543 ysize = ybot - ytop + 1; 01544 01545 /* Sift the variables of the second group up through the first group. */ 01546 for (i = 1; i <= ysize; i++) { 01547 for (j = 1; j <= xsize; j++) { 01548 size = cuddSwapInPlace(table,x,y); 01549 if (size == 0) return(0); 01550 y = x; 01551 x = cuddNextLow(table,y); 01552 } 01553 y = ytop + i; 01554 x = y - 1; 01555 } 01556 01557 /* Fix symmetries. */ 01558 y = xtop; 01559 for (i = 0; i < ysize-1 ; i++) { 01560 table->subtables[y].next = y + 1; 01561 y = y + 1; 01562 } 01563 table->subtables[y].next = xtop; /* y is bottom of its group, join */ 01564 /* its symmetry to top of its group */ 01565 x = y + 1; 01566 newxtop = x; 01567 for (i = 0; i < xsize-1 ; i++) { 01568 table->subtables[x].next = x + 1; 01569 x = x + 1; 01570 } 01571 table->subtables[x].next = newxtop; /* x is bottom of its group, join */ 01572 /* its symmetry to top of its group */ 01573 01574 return(size); 01575 01576 } /* end of ddSymmGroupMoveBackward */
static int ddSymmSiftingAux | ( | DdManager * | table, | |
int | x, | |||
int | xLow, | |||
int | xHigh | |||
) | [static] |
Function********************************************************************
Synopsis [Given xLow <= x <= xHigh moves x up and down between the boundaries.]
Description [Given xLow <= x <= xHigh moves x up and down between the boundaries. Finds the best position and does the required changes. Assumes that x is not part of a symmetry group. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
Definition at line 602 of file cuddSymmetry.c.
00607 { 00608 Move *move; 00609 Move *moveUp; /* list of up moves */ 00610 Move *moveDown; /* list of down moves */ 00611 int initialSize; 00612 int result; 00613 int i; 00614 int topbot; /* index to either top or bottom of symmetry group */ 00615 int initGroupSize, finalGroupSize; 00616 00617 00618 #ifdef DD_DEBUG 00619 /* check for previously detected symmetry */ 00620 assert(table->subtables[x].next == (unsigned) x); 00621 #endif 00622 00623 initialSize = table->keys - table->isolated; 00624 00625 moveDown = NULL; 00626 moveUp = NULL; 00627 00628 if ((x - xLow) > (xHigh - x)) { 00629 /* Will go down first, unless x == xHigh: 00630 ** Look for consecutive symmetries above x. 00631 */ 00632 for (i = x; i > xLow; i--) { 00633 if (!cuddSymmCheck(table,i-1,i)) 00634 break; 00635 topbot = table->subtables[i-1].next; /* find top of i-1's group */ 00636 table->subtables[i-1].next = i; 00637 table->subtables[x].next = topbot; /* x is bottom of group so its */ 00638 /* next is top of i-1's group */ 00639 i = topbot + 1; /* add 1 for i--; new i is top of symm group */ 00640 } 00641 } else { 00642 /* Will go up first unless x == xlow: 00643 ** Look for consecutive symmetries below x. 00644 */ 00645 for (i = x; i < xHigh; i++) { 00646 if (!cuddSymmCheck(table,i,i+1)) 00647 break; 00648 /* find bottom of i+1's symm group */ 00649 topbot = i + 1; 00650 while ((unsigned) topbot < table->subtables[topbot].next) { 00651 topbot = table->subtables[topbot].next; 00652 } 00653 table->subtables[topbot].next = table->subtables[i].next; 00654 table->subtables[i].next = i + 1; 00655 i = topbot - 1; /* subtract 1 for i++; new i is bottom of group */ 00656 } 00657 } 00658 00659 /* Now x may be in the middle of a symmetry group. 00660 ** Find bottom of x's symm group. 00661 */ 00662 while ((unsigned) x < table->subtables[x].next) 00663 x = table->subtables[x].next; 00664 00665 if (x == xLow) { /* Sift down */ 00666 00667 #ifdef DD_DEBUG 00668 /* x must be a singleton */ 00669 assert((unsigned) x == table->subtables[x].next); 00670 #endif 00671 if (x == xHigh) return(1); /* just one variable */ 00672 00673 initGroupSize = 1; 00674 00675 moveDown = ddSymmSiftingDown(table,x,xHigh); 00676 /* after this point x --> xHigh, unless early term */ 00677 if (moveDown == MV_OOM) goto ddSymmSiftingAuxOutOfMem; 00678 if (moveDown == NULL) return(1); 00679 00680 x = moveDown->y; 00681 /* Find bottom of x's group */ 00682 i = x; 00683 while ((unsigned) i < table->subtables[i].next) { 00684 i = table->subtables[i].next; 00685 } 00686 #ifdef DD_DEBUG 00687 /* x should be the top of the symmetry group and i the bottom */ 00688 assert((unsigned) i >= table->subtables[i].next); 00689 assert((unsigned) x == table->subtables[i].next); 00690 #endif 00691 finalGroupSize = i - x + 1; 00692 00693 if (initGroupSize == finalGroupSize) { 00694 /* No new symmetry groups detected, return to best position */ 00695 result = ddSymmSiftingBackward(table,moveDown,initialSize); 00696 } else { 00697 initialSize = table->keys - table->isolated; 00698 moveUp = ddSymmSiftingUp(table,x,xLow); 00699 result = ddSymmSiftingBackward(table,moveUp,initialSize); 00700 } 00701 if (!result) goto ddSymmSiftingAuxOutOfMem; 00702 00703 } else if (cuddNextHigh(table,x) > xHigh) { /* Sift up */ 00704 /* Find top of x's symm group */ 00705 i = x; /* bottom */ 00706 x = table->subtables[x].next; /* top */ 00707 00708 if (x == xLow) return(1); /* just one big group */ 00709 00710 initGroupSize = i - x + 1; 00711 00712 moveUp = ddSymmSiftingUp(table,x,xLow); 00713 /* after this point x --> xLow, unless early term */ 00714 if (moveUp == MV_OOM) goto ddSymmSiftingAuxOutOfMem; 00715 if (moveUp == NULL) return(1); 00716 00717 x = moveUp->x; 00718 /* Find top of x's group */ 00719 i = table->subtables[x].next; 00720 #ifdef DD_DEBUG 00721 /* x should be the bottom of the symmetry group and i the top */ 00722 assert((unsigned) x >= table->subtables[x].next); 00723 assert((unsigned) i == table->subtables[x].next); 00724 #endif 00725 finalGroupSize = x - i + 1; 00726 00727 if (initGroupSize == finalGroupSize) { 00728 /* No new symmetry groups detected, return to best position */ 00729 result = ddSymmSiftingBackward(table,moveUp,initialSize); 00730 } else { 00731 initialSize = table->keys - table->isolated; 00732 moveDown = ddSymmSiftingDown(table,x,xHigh); 00733 result = ddSymmSiftingBackward(table,moveDown,initialSize); 00734 } 00735 if (!result) goto ddSymmSiftingAuxOutOfMem; 00736 00737 } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */ 00738 00739 moveDown = ddSymmSiftingDown(table,x,xHigh); 00740 /* at this point x == xHigh, unless early term */ 00741 if (moveDown == MV_OOM) goto ddSymmSiftingAuxOutOfMem; 00742 00743 if (moveDown != NULL) { 00744 x = moveDown->y; /* x is top here */ 00745 i = x; 00746 while ((unsigned) i < table->subtables[i].next) { 00747 i = table->subtables[i].next; 00748 } 00749 } else { 00750 i = x; 00751 while ((unsigned) i < table->subtables[i].next) { 00752 i = table->subtables[i].next; 00753 } 00754 x = table->subtables[i].next; 00755 } 00756 #ifdef DD_DEBUG 00757 /* x should be the top of the symmetry group and i the bottom */ 00758 assert((unsigned) i >= table->subtables[i].next); 00759 assert((unsigned) x == table->subtables[i].next); 00760 #endif 00761 initGroupSize = i - x + 1; 00762 00763 moveUp = ddSymmSiftingUp(table,x,xLow); 00764 if (moveUp == MV_OOM) goto ddSymmSiftingAuxOutOfMem; 00765 00766 if (moveUp != NULL) { 00767 x = moveUp->x; 00768 i = table->subtables[x].next; 00769 } else { 00770 i = x; 00771 while ((unsigned) x < table->subtables[x].next) 00772 x = table->subtables[x].next; 00773 } 00774 #ifdef DD_DEBUG 00775 /* x should be the bottom of the symmetry group and i the top */ 00776 assert((unsigned) x >= table->subtables[x].next); 00777 assert((unsigned) i == table->subtables[x].next); 00778 #endif 00779 finalGroupSize = x - i + 1; 00780 00781 if (initGroupSize == finalGroupSize) { 00782 /* No new symmetry groups detected, return to best position */ 00783 result = ddSymmSiftingBackward(table,moveUp,initialSize); 00784 } else { 00785 while (moveDown != NULL) { 00786 move = moveDown->next; 00787 cuddDeallocNode(table, (DdNode *) moveDown); 00788 moveDown = move; 00789 } 00790 initialSize = table->keys - table->isolated; 00791 moveDown = ddSymmSiftingDown(table,x,xHigh); 00792 result = ddSymmSiftingBackward(table,moveDown,initialSize); 00793 } 00794 if (!result) goto ddSymmSiftingAuxOutOfMem; 00795 00796 } else { /* moving up first: shorter */ 00797 /* Find top of x's symmetry group */ 00798 x = table->subtables[x].next; 00799 00800 moveUp = ddSymmSiftingUp(table,x,xLow); 00801 /* at this point x == xHigh, unless early term */ 00802 if (moveUp == MV_OOM) goto ddSymmSiftingAuxOutOfMem; 00803 00804 if (moveUp != NULL) { 00805 x = moveUp->x; 00806 i = table->subtables[x].next; 00807 } else { 00808 while ((unsigned) x < table->subtables[x].next) 00809 x = table->subtables[x].next; 00810 i = table->subtables[x].next; 00811 } 00812 #ifdef DD_DEBUG 00813 /* x is bottom of the symmetry group and i is top */ 00814 assert((unsigned) x >= table->subtables[x].next); 00815 assert((unsigned) i == table->subtables[x].next); 00816 #endif 00817 initGroupSize = x - i + 1; 00818 00819 moveDown = ddSymmSiftingDown(table,x,xHigh); 00820 if (moveDown == MV_OOM) goto ddSymmSiftingAuxOutOfMem; 00821 00822 if (moveDown != NULL) { 00823 x = moveDown->y; 00824 i = x; 00825 while ((unsigned) i < table->subtables[i].next) { 00826 i = table->subtables[i].next; 00827 } 00828 } else { 00829 i = x; 00830 x = table->subtables[x].next; 00831 } 00832 #ifdef DD_DEBUG 00833 /* x should be the top of the symmetry group and i the bottom */ 00834 assert((unsigned) i >= table->subtables[i].next); 00835 assert((unsigned) x == table->subtables[i].next); 00836 #endif 00837 finalGroupSize = i - x + 1; 00838 00839 if (initGroupSize == finalGroupSize) { 00840 /* No new symmetries detected, go back to best position */ 00841 result = ddSymmSiftingBackward(table,moveDown,initialSize); 00842 } else { 00843 while (moveUp != NULL) { 00844 move = moveUp->next; 00845 cuddDeallocNode(table, (DdNode *) moveUp); 00846 moveUp = move; 00847 } 00848 initialSize = table->keys - table->isolated; 00849 moveUp = ddSymmSiftingUp(table,x,xLow); 00850 result = ddSymmSiftingBackward(table,moveUp,initialSize); 00851 } 00852 if (!result) goto ddSymmSiftingAuxOutOfMem; 00853 } 00854 00855 while (moveDown != NULL) { 00856 move = moveDown->next; 00857 cuddDeallocNode(table, (DdNode *) moveDown); 00858 moveDown = move; 00859 } 00860 while (moveUp != NULL) { 00861 move = moveUp->next; 00862 cuddDeallocNode(table, (DdNode *) moveUp); 00863 moveUp = move; 00864 } 00865 00866 return(1); 00867 00868 ddSymmSiftingAuxOutOfMem: 00869 if (moveDown != MV_OOM) { 00870 while (moveDown != NULL) { 00871 move = moveDown->next; 00872 cuddDeallocNode(table, (DdNode *) moveDown); 00873 moveDown = move; 00874 } 00875 } 00876 if (moveUp != MV_OOM) { 00877 while (moveUp != NULL) { 00878 move = moveUp->next; 00879 cuddDeallocNode(table, (DdNode *) moveUp); 00880 moveUp = move; 00881 } 00882 } 00883 00884 return(0); 00885 00886 } /* end of ddSymmSiftingAux */
Function********************************************************************
Synopsis [Given a set of moves, returns the DD heap to the position giving the minimum size.]
Description [Given a set of moves, returns the DD heap to the position giving the minimum size. In case of ties, returns to the closest position giving the minimum size. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 1593 of file cuddSymmetry.c.
01597 { 01598 Move *move; 01599 int res; 01600 01601 for (move = moves; move != NULL; move = move->next) { 01602 if (move->size < size) { 01603 size = move->size; 01604 } 01605 } 01606 01607 for (move = moves; move != NULL; move = move->next) { 01608 if (move->size == size) return(1); 01609 if (table->subtables[move->x].next == move->x && table->subtables[move->y].next == move->y) { 01610 res = cuddSwapInPlace(table,(int)move->x,(int)move->y); 01611 #ifdef DD_DEBUG 01612 assert(table->subtables[move->x].next == move->x); 01613 assert(table->subtables[move->y].next == move->y); 01614 #endif 01615 } else { /* Group move necessary */ 01616 res = ddSymmGroupMoveBackward(table,(int)move->x,(int)move->y); 01617 } 01618 if (!res) return(0); 01619 } 01620 01621 return(1); 01622 01623 } /* end of ddSymmSiftingBackward */
static int ddSymmSiftingConvAux | ( | DdManager * | table, | |
int | x, | |||
int | xLow, | |||
int | xHigh | |||
) | [static] |
Function********************************************************************
Synopsis [Given xLow <= x <= xHigh moves x up and down between the boundaries.]
Description [Given xLow <= x <= xHigh moves x up and down between the boundaries. Finds the best position and does the required changes. Assumes that x is either an isolated variable, or it is the bottom of a symmetry group. All symmetries may not have been found, because of exceeded growth limit. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
Definition at line 904 of file cuddSymmetry.c.
00909 { 00910 Move *move; 00911 Move *moveUp; /* list of up moves */ 00912 Move *moveDown; /* list of down moves */ 00913 int initialSize; 00914 int result; 00915 int i; 00916 int initGroupSize, finalGroupSize; 00917 00918 00919 initialSize = table->keys - table->isolated; 00920 00921 moveDown = NULL; 00922 moveUp = NULL; 00923 00924 if (x == xLow) { /* Sift down */ 00925 #ifdef DD_DEBUG 00926 /* x is bottom of symmetry group */ 00927 assert((unsigned) x >= table->subtables[x].next); 00928 #endif 00929 i = table->subtables[x].next; 00930 initGroupSize = x - i + 1; 00931 00932 moveDown = ddSymmSiftingDown(table,x,xHigh); 00933 /* at this point x == xHigh, unless early term */ 00934 if (moveDown == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem; 00935 if (moveDown == NULL) return(1); 00936 00937 x = moveDown->y; 00938 i = x; 00939 while ((unsigned) i < table->subtables[i].next) { 00940 i = table->subtables[i].next; 00941 } 00942 #ifdef DD_DEBUG 00943 /* x should be the top of the symmetric group and i the bottom */ 00944 assert((unsigned) i >= table->subtables[i].next); 00945 assert((unsigned) x == table->subtables[i].next); 00946 #endif 00947 finalGroupSize = i - x + 1; 00948 00949 if (initGroupSize == finalGroupSize) { 00950 /* No new symmetries detected, go back to best position */ 00951 result = ddSymmSiftingBackward(table,moveDown,initialSize); 00952 } else { 00953 initialSize = table->keys - table->isolated; 00954 moveUp = ddSymmSiftingUp(table,x,xLow); 00955 result = ddSymmSiftingBackward(table,moveUp,initialSize); 00956 } 00957 if (!result) goto ddSymmSiftingConvAuxOutOfMem; 00958 00959 } else if (cuddNextHigh(table,x) > xHigh) { /* Sift up */ 00960 /* Find top of x's symm group */ 00961 while ((unsigned) x < table->subtables[x].next) 00962 x = table->subtables[x].next; 00963 i = x; /* bottom */ 00964 x = table->subtables[x].next; /* top */ 00965 00966 if (x == xLow) return(1); 00967 00968 initGroupSize = i - x + 1; 00969 00970 moveUp = ddSymmSiftingUp(table,x,xLow); 00971 /* at this point x == xLow, unless early term */ 00972 if (moveUp == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem; 00973 if (moveUp == NULL) return(1); 00974 00975 x = moveUp->x; 00976 i = table->subtables[x].next; 00977 #ifdef DD_DEBUG 00978 /* x should be the bottom of the symmetry group and i the top */ 00979 assert((unsigned) x >= table->subtables[x].next); 00980 assert((unsigned) i == table->subtables[x].next); 00981 #endif 00982 finalGroupSize = x - i + 1; 00983 00984 if (initGroupSize == finalGroupSize) { 00985 /* No new symmetry groups detected, return to best position */ 00986 result = ddSymmSiftingBackward(table,moveUp,initialSize); 00987 } else { 00988 initialSize = table->keys - table->isolated; 00989 moveDown = ddSymmSiftingDown(table,x,xHigh); 00990 result = ddSymmSiftingBackward(table,moveDown,initialSize); 00991 } 00992 if (!result) 00993 goto ddSymmSiftingConvAuxOutOfMem; 00994 00995 } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */ 00996 moveDown = ddSymmSiftingDown(table,x,xHigh); 00997 /* at this point x == xHigh, unless early term */ 00998 if (moveDown == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem; 00999 01000 if (moveDown != NULL) { 01001 x = moveDown->y; 01002 i = x; 01003 while ((unsigned) i < table->subtables[i].next) { 01004 i = table->subtables[i].next; 01005 } 01006 } else { 01007 while ((unsigned) x < table->subtables[x].next) 01008 x = table->subtables[x].next; 01009 i = x; 01010 x = table->subtables[x].next; 01011 } 01012 #ifdef DD_DEBUG 01013 /* x should be the top of the symmetry group and i the bottom */ 01014 assert((unsigned) i >= table->subtables[i].next); 01015 assert((unsigned) x == table->subtables[i].next); 01016 #endif 01017 initGroupSize = i - x + 1; 01018 01019 moveUp = ddSymmSiftingUp(table,x,xLow); 01020 if (moveUp == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem; 01021 01022 if (moveUp != NULL) { 01023 x = moveUp->x; 01024 i = table->subtables[x].next; 01025 } else { 01026 i = x; 01027 while ((unsigned) x < table->subtables[x].next) 01028 x = table->subtables[x].next; 01029 } 01030 #ifdef DD_DEBUG 01031 /* x should be the bottom of the symmetry group and i the top */ 01032 assert((unsigned) x >= table->subtables[x].next); 01033 assert((unsigned) i == table->subtables[x].next); 01034 #endif 01035 finalGroupSize = x - i + 1; 01036 01037 if (initGroupSize == finalGroupSize) { 01038 /* No new symmetry groups detected, return to best position */ 01039 result = ddSymmSiftingBackward(table,moveUp,initialSize); 01040 } else { 01041 while (moveDown != NULL) { 01042 move = moveDown->next; 01043 cuddDeallocNode(table, (DdNode *) moveDown); 01044 moveDown = move; 01045 } 01046 initialSize = table->keys - table->isolated; 01047 moveDown = ddSymmSiftingDown(table,x,xHigh); 01048 result = ddSymmSiftingBackward(table,moveDown,initialSize); 01049 } 01050 if (!result) goto ddSymmSiftingConvAuxOutOfMem; 01051 01052 } else { /* moving up first: shorter */ 01053 /* Find top of x's symmetry group */ 01054 x = table->subtables[x].next; 01055 01056 moveUp = ddSymmSiftingUp(table,x,xLow); 01057 /* at this point x == xHigh, unless early term */ 01058 if (moveUp == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem; 01059 01060 if (moveUp != NULL) { 01061 x = moveUp->x; 01062 i = table->subtables[x].next; 01063 } else { 01064 i = x; 01065 while ((unsigned) x < table->subtables[x].next) 01066 x = table->subtables[x].next; 01067 } 01068 #ifdef DD_DEBUG 01069 /* x is bottom of the symmetry group and i is top */ 01070 assert((unsigned) x >= table->subtables[x].next); 01071 assert((unsigned) i == table->subtables[x].next); 01072 #endif 01073 initGroupSize = x - i + 1; 01074 01075 moveDown = ddSymmSiftingDown(table,x,xHigh); 01076 if (moveDown == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem; 01077 01078 if (moveDown != NULL) { 01079 x = moveDown->y; 01080 i = x; 01081 while ((unsigned) i < table->subtables[i].next) { 01082 i = table->subtables[i].next; 01083 } 01084 } else { 01085 i = x; 01086 x = table->subtables[x].next; 01087 } 01088 #ifdef DD_DEBUG 01089 /* x should be the top of the symmetry group and i the bottom */ 01090 assert((unsigned) i >= table->subtables[i].next); 01091 assert((unsigned) x == table->subtables[i].next); 01092 #endif 01093 finalGroupSize = i - x + 1; 01094 01095 if (initGroupSize == finalGroupSize) { 01096 /* No new symmetries detected, go back to best position */ 01097 result = ddSymmSiftingBackward(table,moveDown,initialSize); 01098 } else { 01099 while (moveUp != NULL) { 01100 move = moveUp->next; 01101 cuddDeallocNode(table, (DdNode *) moveUp); 01102 moveUp = move; 01103 } 01104 initialSize = table->keys - table->isolated; 01105 moveUp = ddSymmSiftingUp(table,x,xLow); 01106 result = ddSymmSiftingBackward(table,moveUp,initialSize); 01107 } 01108 if (!result) goto ddSymmSiftingConvAuxOutOfMem; 01109 } 01110 01111 while (moveDown != NULL) { 01112 move = moveDown->next; 01113 cuddDeallocNode(table, (DdNode *) moveDown); 01114 moveDown = move; 01115 } 01116 while (moveUp != NULL) { 01117 move = moveUp->next; 01118 cuddDeallocNode(table, (DdNode *) moveUp); 01119 moveUp = move; 01120 } 01121 01122 return(1); 01123 01124 ddSymmSiftingConvAuxOutOfMem: 01125 if (moveDown != MV_OOM) { 01126 while (moveDown != NULL) { 01127 move = moveDown->next; 01128 cuddDeallocNode(table, (DdNode *) moveDown); 01129 moveDown = move; 01130 } 01131 } 01132 if (moveUp != MV_OOM) { 01133 while (moveUp != NULL) { 01134 move = moveUp->next; 01135 cuddDeallocNode(table, (DdNode *) moveUp); 01136 moveUp = move; 01137 } 01138 } 01139 01140 return(0); 01141 01142 } /* end of ddSymmSiftingConvAux */
Function********************************************************************
Synopsis [Moves x down until either it reaches the bound (xHigh) or the size of the DD heap increases too much.]
Description [Moves x down until either it reaches the bound (xHigh) or the size of the DD heap increases too much. Assumes that x is the bottom of a symmetry group. Checks x for symmetry to the adjacent variables. If symmetry is found, the symmetry group of x is merged with the symmetry group of the other variable. Returns the set of moves in case of success; MV_OOM if memory is full.]
SideEffects [None]
Definition at line 1303 of file cuddSymmetry.c.
01307 { 01308 Move *moves; 01309 Move *move; 01310 int y; 01311 int size; 01312 int limitSize; 01313 int gxtop,gybot; 01314 int R; /* upper bound on node decrease */ 01315 int xindex, yindex; 01316 int isolated; 01317 int z; 01318 int zindex; 01319 #ifdef DD_DEBUG 01320 int checkR; 01321 #endif 01322 01323 moves = NULL; 01324 /* Initialize R */ 01325 xindex = table->invperm[x]; 01326 gxtop = table->subtables[x].next; 01327 limitSize = size = table->keys - table->isolated; 01328 R = 0; 01329 for (z = xHigh; z > gxtop; z--) { 01330 zindex = table->invperm[z]; 01331 if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) { 01332 isolated = table->vars[zindex]->ref == 1; 01333 R += table->subtables[z].keys - isolated; 01334 } 01335 } 01336 01337 y = cuddNextHigh(table,x); 01338 while (y <= xHigh && size - R < limitSize) { 01339 #ifdef DD_DEBUG 01340 gxtop = table->subtables[x].next; 01341 checkR = 0; 01342 for (z = xHigh; z > gxtop; z--) { 01343 zindex = table->invperm[z]; 01344 if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) { 01345 isolated = table->vars[zindex]->ref == 1; 01346 checkR += table->subtables[z].keys - isolated; 01347 } 01348 } 01349 assert(R == checkR); 01350 #endif 01351 gybot = table->subtables[y].next; 01352 while (table->subtables[gybot].next != (unsigned) y) 01353 gybot = table->subtables[gybot].next; 01354 if (cuddSymmCheck(table,x,y)) { 01355 /* Symmetry found, attach symm groups */ 01356 gxtop = table->subtables[x].next; 01357 table->subtables[x].next = y; 01358 table->subtables[gybot].next = gxtop; 01359 } else if (table->subtables[x].next == (unsigned) x && 01360 table->subtables[y].next == (unsigned) y) { 01361 /* x and y have self symmetry */ 01362 /* Update upper bound on node decrease. */ 01363 yindex = table->invperm[y]; 01364 if (cuddTestInteract(table,xindex,yindex)) { 01365 isolated = table->vars[yindex]->ref == 1; 01366 R -= table->subtables[y].keys - isolated; 01367 } 01368 size = cuddSwapInPlace(table,x,y); 01369 #ifdef DD_DEBUG 01370 assert(table->subtables[x].next == (unsigned) x); 01371 assert(table->subtables[y].next == (unsigned) y); 01372 #endif 01373 if (size == 0) goto ddSymmSiftingDownOutOfMem; 01374 move = (Move *) cuddDynamicAllocNode(table); 01375 if (move == NULL) goto ddSymmSiftingDownOutOfMem; 01376 move->x = x; 01377 move->y = y; 01378 move->size = size; 01379 move->next = moves; 01380 moves = move; 01381 if ((double) size > (double) limitSize * table->maxGrowth) 01382 return(moves); 01383 if (size < limitSize) limitSize = size; 01384 } else { /* Group move */ 01385 /* Update upper bound on node decrease: first phase. */ 01386 gxtop = table->subtables[x].next; 01387 z = gxtop + 1; 01388 do { 01389 zindex = table->invperm[z]; 01390 if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) { 01391 isolated = table->vars[zindex]->ref == 1; 01392 R -= table->subtables[z].keys - isolated; 01393 } 01394 z++; 01395 } while (z <= gybot); 01396 size = ddSymmGroupMove(table,x,y,&moves); 01397 if (size == 0) goto ddSymmSiftingDownOutOfMem; 01398 if ((double) size > (double) limitSize * table->maxGrowth) 01399 return(moves); 01400 if (size < limitSize) limitSize = size; 01401 /* Update upper bound on node decrease: second phase. */ 01402 gxtop = table->subtables[gybot].next; 01403 for (z = gxtop + 1; z <= gybot; z++) { 01404 zindex = table->invperm[z]; 01405 if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) { 01406 isolated = table->vars[zindex]->ref == 1; 01407 R += table->subtables[z].keys - isolated; 01408 } 01409 } 01410 } 01411 x = gybot; 01412 y = cuddNextHigh(table,x); 01413 } 01414 01415 return(moves); 01416 01417 ddSymmSiftingDownOutOfMem: 01418 while (moves != NULL) { 01419 move = moves->next; 01420 cuddDeallocNode(table, (DdNode *) moves); 01421 moves = move; 01422 } 01423 return(MV_OOM); 01424 01425 } /* end of ddSymmSiftingDown */
Function********************************************************************
Synopsis [Moves x up until either it reaches the bound (xLow) or the size of the DD heap increases too much.]
Description [Moves x up until either it reaches the bound (xLow) or the size of the DD heap increases too much. Assumes that x is the top of a symmetry group. Checks x for symmetry to the adjacent variables. If symmetry is found, the symmetry group of x is merged with the symmetry group of the other variable. Returns the set of moves in case of success; MV_OOM if memory is full.]
SideEffects [None]
Definition at line 1161 of file cuddSymmetry.c.
01165 { 01166 Move *moves; 01167 Move *move; 01168 int x; 01169 int size; 01170 int i; 01171 int gxtop,gybot; 01172 int limitSize; 01173 int xindex, yindex; 01174 int zindex; 01175 int z; 01176 int isolated; 01177 int L; /* lower bound on DD size */ 01178 #ifdef DD_DEBUG 01179 int checkL; 01180 #endif 01181 01182 01183 moves = NULL; 01184 yindex = table->invperm[y]; 01185 01186 /* Initialize the lower bound. 01187 ** The part of the DD below the bottom of y' group will not change. 01188 ** The part of the DD above y that does not interact with y will not 01189 ** change. The rest may vanish in the best case, except for 01190 ** the nodes at level xLow, which will not vanish, regardless. 01191 */ 01192 limitSize = L = table->keys - table->isolated; 01193 gybot = y; 01194 while ((unsigned) gybot < table->subtables[gybot].next) 01195 gybot = table->subtables[gybot].next; 01196 for (z = xLow + 1; z <= gybot; z++) { 01197 zindex = table->invperm[z]; 01198 if (zindex == yindex || cuddTestInteract(table,zindex,yindex)) { 01199 isolated = table->vars[zindex]->ref == 1; 01200 L -= table->subtables[z].keys - isolated; 01201 } 01202 } 01203 01204 x = cuddNextLow(table,y); 01205 while (x >= xLow && L <= limitSize) { 01206 #ifdef DD_DEBUG 01207 gybot = y; 01208 while ((unsigned) gybot < table->subtables[gybot].next) 01209 gybot = table->subtables[gybot].next; 01210 checkL = table->keys - table->isolated; 01211 for (z = xLow + 1; z <= gybot; z++) { 01212 zindex = table->invperm[z]; 01213 if (zindex == yindex || cuddTestInteract(table,zindex,yindex)) { 01214 isolated = table->vars[zindex]->ref == 1; 01215 checkL -= table->subtables[z].keys - isolated; 01216 } 01217 } 01218 assert(L == checkL); 01219 #endif 01220 gxtop = table->subtables[x].next; 01221 if (cuddSymmCheck(table,x,y)) { 01222 /* Symmetry found, attach symm groups */ 01223 table->subtables[x].next = y; 01224 i = table->subtables[y].next; 01225 while (table->subtables[i].next != (unsigned) y) 01226 i = table->subtables[i].next; 01227 table->subtables[i].next = gxtop; 01228 } else if (table->subtables[x].next == (unsigned) x && 01229 table->subtables[y].next == (unsigned) y) { 01230 /* x and y have self symmetry */ 01231 xindex = table->invperm[x]; 01232 size = cuddSwapInPlace(table,x,y); 01233 #ifdef DD_DEBUG 01234 assert(table->subtables[x].next == (unsigned) x); 01235 assert(table->subtables[y].next == (unsigned) y); 01236 #endif 01237 if (size == 0) goto ddSymmSiftingUpOutOfMem; 01238 /* Update the lower bound. */ 01239 if (cuddTestInteract(table,xindex,yindex)) { 01240 isolated = table->vars[xindex]->ref == 1; 01241 L += table->subtables[y].keys - isolated; 01242 } 01243 move = (Move *) cuddDynamicAllocNode(table); 01244 if (move == NULL) goto ddSymmSiftingUpOutOfMem; 01245 move->x = x; 01246 move->y = y; 01247 move->size = size; 01248 move->next = moves; 01249 moves = move; 01250 if ((double) size > (double) limitSize * table->maxGrowth) 01251 return(moves); 01252 if (size < limitSize) limitSize = size; 01253 } else { /* Group move */ 01254 size = ddSymmGroupMove(table,x,y,&moves); 01255 if (size == 0) goto ddSymmSiftingUpOutOfMem; 01256 /* Update the lower bound. */ 01257 z = moves->y; 01258 do { 01259 zindex = table->invperm[z]; 01260 if (cuddTestInteract(table,zindex,yindex)) { 01261 isolated = table->vars[zindex]->ref == 1; 01262 L += table->subtables[z].keys - isolated; 01263 } 01264 z = table->subtables[z].next; 01265 } while (z != (int) moves->y); 01266 if ((double) size > (double) limitSize * table->maxGrowth) 01267 return(moves); 01268 if (size < limitSize) limitSize = size; 01269 } 01270 y = gxtop; 01271 x = cuddNextLow(table,y); 01272 } 01273 01274 return(moves); 01275 01276 ddSymmSiftingUpOutOfMem: 01277 while (moves != NULL) { 01278 move = moves->next; 01279 cuddDeallocNode(table, (DdNode *) moves); 01280 moves = move; 01281 } 01282 return(MV_OOM); 01283 01284 } /* end of ddSymmSiftingUp */
static void ddSymmSummary | ( | DdManager * | table, | |
int | lower, | |||
int | upper, | |||
int * | symvars, | |||
int * | symgroups | |||
) | [static] |
Function********************************************************************
Synopsis [Counts numbers of symmetric variables and symmetry groups.]
Description []
SideEffects [None]
Definition at line 1637 of file cuddSymmetry.c.
01643 { 01644 int i,x,gbot; 01645 int TotalSymm = 0; 01646 int TotalSymmGroups = 0; 01647 01648 for (i = lower; i <= upper; i++) { 01649 if (table->subtables[i].next != (unsigned) i) { 01650 TotalSymmGroups++; 01651 x = i; 01652 do { 01653 TotalSymm++; 01654 gbot = x; 01655 x = table->subtables[x].next; 01656 } while (x != i); 01657 #ifdef DD_DEBUG 01658 assert(table->subtables[gbot].next == (unsigned) i); 01659 #endif 01660 i = gbot; 01661 } 01662 } 01663 *symvars = TotalSymm; 01664 *symgroups = TotalSymmGroups; 01665 01666 return; 01667 01668 } /* end of ddSymmSummary */
static int ddSymmUniqueCompare | ( | int * | ptrX, | |
int * | ptrY | |||
) | [static] |
Function********************************************************************
Synopsis [Comparison function used by qsort.]
Description [Comparison function used by qsort to order the variables according to the number of keys in the subtables. Returns the difference in number of keys between the two variables being compared.]
SideEffects [None]
Definition at line 574 of file cuddSymmetry.c.
char rcsid [] DD_UNUSED = "$Id: cuddSymmetry.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $" [static] |
Definition at line 63 of file cuddSymmetry.c.
Definition at line 76 of file cuddReorder.c.
int* entry [static] |
Definition at line 66 of file cuddSymmetry.c.