abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cuddSymmetry.c File Reference
#include "misc/util/util_hack.h"
#include "cuddInt.h"

Go to the source code of this file.

Macros

#define MV_OOM   (Move *)1
 

Functions

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 MoveddSymmSiftingUp (DdManager *table, int y, int xLow)
 
static MoveddSymmSiftingDown (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)
 
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)
 

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddSymmetry.c,v 1.26 2009/02/19 16:23:54 fabio Exp $"
 
static int * entry
 
int ddTotalNumberSwapping
 

Macro Definition Documentation

#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 [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.]

Definition at line 79 of file cuddSymmetry.c.

Function Documentation

void Cudd_SymmProfile ( DdManager table,
int  lower,
int  upper 
)

AutomaticEnd Function********************************************************************

Synopsis [Prints statistics on symmetric variables.]

Description []

SideEffects [None]

Definition at line 142 of file cuddSymmetry.c.

146 {
147  int i,x,gbot;
148  int TotalSymm = 0;
149  int TotalSymmGroups = 0;
150 
151  for (i = lower; i <= upper; i++) {
152  if (table->subtables[i].next != (unsigned) i) {
153  x = i;
154  (void) fprintf(table->out,"Group:");
155  do {
156  (void) fprintf(table->out," %d",table->invperm[x]);
157  TotalSymm++;
158  gbot = x;
159  x = table->subtables[x].next;
160  } while (x != i);
161  TotalSymmGroups++;
162 #ifdef DD_DEBUG
163  assert(table->subtables[gbot].next == (unsigned) i);
164 #endif
165  i = gbot;
166  (void) fprintf(table->out,"\n");
167  }
168  }
169  (void) fprintf(table->out,"Total Symmetric = %d\n",TotalSymm);
170  (void) fprintf(table->out,"Total Groups = %d\n",TotalSymmGroups);
171 
172 } /* end of Cudd_SymmProfile */
DdSubtable * subtables
Definition: cuddInt.h:365
FILE * out
Definition: cuddInt.h:441
unsigned int next
Definition: cuddInt.h:333
#define assert(ex)
Definition: util_old.h:213
int * invperm
Definition: cuddInt.h:388
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 192 of file cuddSymmetry.c.

196 {
197  DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10;
198  int comple; /* f0 is complemented */
199  int xsymmy; /* x and y may be positively symmetric */
200  int xsymmyp; /* x and y may be negatively symmetric */
201  int arccount; /* number of arcs from layer x to layer y */
202  int TotalRefCount; /* total reference count of layer y minus 1 */
203  int yindex;
204  int i;
205  DdNodePtr *list;
206  int slots;
207  DdNode *sentinel = &(table->sentinel);
208 #ifdef DD_DEBUG
209  int xindex;
210 #endif
211 
212  /* Checks that x and y are not the projection functions.
213  ** For x it is sufficient to check whether there is only one
214  ** node; indeed, if there is one node, it is the projection function
215  ** and it cannot point to y. Hence, if y isn't just the projection
216  ** function, it has one arc coming from a layer different from x.
217  */
218  if (table->subtables[x].keys == 1) {
219  return(0);
220  }
221  yindex = table->invperm[y];
222  if (table->subtables[y].keys == 1) {
223  if (table->vars[yindex]->ref == 1)
224  return(0);
225  }
226 
227  xsymmy = xsymmyp = 1;
228  arccount = 0;
229  slots = table->subtables[x].slots;
230  list = table->subtables[x].nodelist;
231  for (i = 0; i < slots; i++) {
232  f = list[i];
233  while (f != sentinel) {
234  /* Find f1, f0, f11, f10, f01, f00. */
235  f1 = cuddT(f);
236  f0 = Cudd_Regular(cuddE(f));
237  comple = Cudd_IsComplement(cuddE(f));
238  if ((int) f1->index == yindex) {
239  arccount++;
240  f11 = cuddT(f1); f10 = cuddE(f1);
241  } else {
242  if ((int) f0->index != yindex) {
243  /* If f is an isolated projection function it is
244  ** allowed to bypass layer y.
245  */
246  if (f1 != DD_ONE(table) || f0 != DD_ONE(table) || f->ref != 1)
247  return(0); /* f bypasses layer y */
248  }
249  f11 = f10 = f1;
250  }
251  if ((int) f0->index == yindex) {
252  arccount++;
253  f01 = cuddT(f0); f00 = cuddE(f0);
254  } else {
255  f01 = f00 = f0;
256  }
257  if (comple) {
258  f01 = Cudd_Not(f01);
259  f00 = Cudd_Not(f00);
260  }
261 
262  if (f1 != DD_ONE(table) || f0 != DD_ONE(table) || f->ref != 1) {
263  xsymmy &= f01 == f10;
264  xsymmyp &= f11 == f00;
265  if ((xsymmy == 0) && (xsymmyp == 0))
266  return(0);
267  }
268 
269  f = f->next;
270  } /* while */
271  } /* for */
272 
273  /* Calculate the total reference counts of y */
274  TotalRefCount = -1; /* -1 for projection function */
275  slots = table->subtables[y].slots;
276  list = table->subtables[y].nodelist;
277  for (i = 0; i < slots; i++) {
278  f = list[i];
279  while (f != sentinel) {
280  TotalRefCount += f->ref;
281  f = f->next;
282  }
283  }
284 
285 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
286  if (arccount == TotalRefCount) {
287  xindex = table->invperm[x];
288  (void) fprintf(table->out,
289  "Found symmetry! x =%d\ty = %d\tPos(%d,%d)\n",
290  xindex,yindex,x,y);
291  }
292 #endif
293 
294  return(arccount == TotalRefCount);
295 
296 } /* end of cuddSymmCheck */
DdHalfWord ref
Definition: cudd.h:280
unsigned int keys
Definition: cuddInt.h:330
Definition: cudd.h:278
#define Cudd_Not(node)
Definition: cudd.h:367
#define Cudd_Regular(node)
Definition: cudd.h:397
DdSubtable * subtables
Definition: cuddInt.h:365
#define Cudd_IsComplement(node)
Definition: cudd.h:425
DdNode sentinel
Definition: cuddInt.h:344
FILE * out
Definition: cuddInt.h:441
DdNode * next
Definition: cudd.h:281
DdNode ** nodelist
Definition: cuddInt.h:327
#define cuddT(node)
Definition: cuddInt.h:636
DdHalfWord index
Definition: cudd.h:279
unsigned int slots
Definition: cuddInt.h:329
DdNode ** vars
Definition: cuddInt.h:390
#define cuddE(node)
Definition: cuddInt.h:652
int * invperm
Definition: cuddInt.h:388
#define DD_ONE(dd)
Definition: cuddInt.h:911
int cuddSymmSifting ( DdManager table,
int  lower,
int  upper 
)

Function********************************************************************

Synopsis [Symmetric sifting algorithm.]

Description [Symmetric sifting algorithm. Assumes that no dead nodes are present.

  1. Order all the variables according to the number of entries in each unique subtable.
  2. Sift the variable up and down, remembering each time the total size of the DD heap and grouping variables that are symmetric.
  3. Select the best permutation.
  4. Repeat 3 and 4 for all variables.

Returns 1 plus the number of symmetric variables if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [cuddSymmSiftingConv]

Definition at line 322 of file cuddSymmetry.c.

326 {
327  int i;
328  int *var;
329  int size;
330  int x;
331  int result;
332  int symvars;
333  int symgroups;
334 #ifdef DD_STATS
335  int previousSize;
336 #endif
337 
338  size = table->size;
339 
340  /* Find order in which to sift variables. */
341  var = NULL;
342  entry = ABC_ALLOC(int,size);
343  if (entry == NULL) {
344  table->errorCode = CUDD_MEMORY_OUT;
345  goto ddSymmSiftingOutOfMem;
346  }
347  var = ABC_ALLOC(int,size);
348  if (var == NULL) {
349  table->errorCode = CUDD_MEMORY_OUT;
350  goto ddSymmSiftingOutOfMem;
351  }
352 
353  for (i = 0; i < size; i++) {
354  x = table->perm[i];
355  entry[i] = table->subtables[x].keys;
356  var[i] = i;
357  }
358 
359  qsort((void *)var,size,sizeof(int),(DD_QSFP)ddSymmUniqueCompare);
360 
361  /* Initialize the symmetry of each subtable to itself. */
362  for (i = lower; i <= upper; i++) {
363  table->subtables[i].next = i;
364  }
365 
366  for (i = 0; i < ddMin(table->siftMaxVar,size); i++) {
367  if (ddTotalNumberSwapping >= table->siftMaxSwap)
368  break;
369  // enable timeout during variable reodering - alanmi 2/13/11
370  if ( table->TimeStop && Abc_Clock() > table->TimeStop )
371  break;
372  x = table->perm[var[i]];
373 #ifdef DD_STATS
374  previousSize = table->keys - table->isolated;
375 #endif
376  if (x < lower || x > upper) continue;
377  if (table->subtables[x].next == (unsigned) x) {
378  result = ddSymmSiftingAux(table,x,lower,upper);
379  if (!result) goto ddSymmSiftingOutOfMem;
380 #ifdef DD_STATS
381  if (table->keys < (unsigned) previousSize + table->isolated) {
382  (void) fprintf(table->out,"-");
383  } else if (table->keys > (unsigned) previousSize +
384  table->isolated) {
385  (void) fprintf(table->out,"+"); /* should never happen */
386  } else {
387  (void) fprintf(table->out,"=");
388  }
389  fflush(table->out);
390 #endif
391  }
392  }
393 
394  ABC_FREE(var);
395  ABC_FREE(entry);
396 
397  ddSymmSummary(table, lower, upper, &symvars, &symgroups);
398 
399 #ifdef DD_STATS
400  (void) fprintf(table->out, "\n#:S_SIFTING %8d: symmetric variables\n",
401  symvars);
402  (void) fprintf(table->out, "#:G_SIFTING %8d: symmetric groups",
403  symgroups);
404 #endif
405 
406  return(1+symvars);
407 
408 ddSymmSiftingOutOfMem:
409 
410  if (entry != NULL) ABC_FREE(entry);
411  if (var != NULL) ABC_FREE(var);
412 
413  return(0);
414 
415 } /* end of cuddSymmSifting */
unsigned int keys
Definition: cuddInt.h:330
abctime TimeStop
Definition: cuddInt.h:489
static int * entry
Definition: cuddSymmetry.c:97
int siftMaxSwap
Definition: cuddInt.h:412
int(* DD_QSFP)(const void *, const void *)
Definition: cudd.h:326
int size
Definition: cuddInt.h:361
int var(Lit p)
Definition: SolverTypes.h:62
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
DdSubtable * subtables
Definition: cuddInt.h:365
static abctime Abc_Clock()
Definition: abc_global.h:279
unsigned int keys
Definition: cuddInt.h:369
FILE * out
Definition: cuddInt.h:441
static void ddSymmSummary(DdManager *table, int lower, int upper, int *symvars, int *symgroups)
static int size
Definition: cuddSign.c:86
#define ddMin(x, y)
Definition: cuddInt.h:818
int siftMaxVar
Definition: cuddInt.h:411
#define ABC_FREE(obj)
Definition: abc_global.h:232
int ddTotalNumberSwapping
Definition: cuddReorder.c:107
unsigned int next
Definition: cuddInt.h:333
static int result
Definition: cuddGenetic.c:125
int isolated
Definition: cuddInt.h:385
static int ddSymmUniqueCompare(int *ptrX, int *ptrY)
Definition: cuddSymmetry.c:608
int * perm
Definition: cuddInt.h:386
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
static int ddSymmSiftingAux(DdManager *table, int x, int xLow, int xHigh)
Definition: cuddSymmetry.c:636
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.

  1. Order all the variables according to the number of entries in each unique subtable.
  2. Sift the variable up and down, remembering each time the total size of the DD heap and grouping variables that are symmetric.
  3. Select the best permutation.
  4. Repeat 3 and 4 for all variables.
  5. Repeat 1-4 until no further improvement.

Returns 1 plus the number of symmetric variables if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [cuddSymmSifting]

Definition at line 442 of file cuddSymmetry.c.

446 {
447  int i;
448  int *var;
449  int size;
450  int x;
451  int result;
452  int symvars;
453  int symgroups;
454  int classes;
455  int initialSize;
456 #ifdef DD_STATS
457  int previousSize;
458 #endif
459 
460  initialSize = table->keys - table->isolated;
461 
462  size = table->size;
463 
464  /* Find order in which to sift variables. */
465  var = NULL;
466  entry = ABC_ALLOC(int,size);
467  if (entry == NULL) {
468  table->errorCode = CUDD_MEMORY_OUT;
469  goto ddSymmSiftingConvOutOfMem;
470  }
471  var = ABC_ALLOC(int,size);
472  if (var == NULL) {
473  table->errorCode = CUDD_MEMORY_OUT;
474  goto ddSymmSiftingConvOutOfMem;
475  }
476 
477  for (i = 0; i < size; i++) {
478  x = table->perm[i];
479  entry[i] = table->subtables[x].keys;
480  var[i] = i;
481  }
482 
483  qsort((void *)var,size,sizeof(int),(DD_QSFP)ddSymmUniqueCompare);
484 
485  /* Initialize the symmetry of each subtable to itself
486  ** for first pass of converging symmetric sifting.
487  */
488  for (i = lower; i <= upper; i++) {
489  table->subtables[i].next = i;
490  }
491 
492  for (i = 0; i < ddMin(table->siftMaxVar, table->size); i++) {
493  if (ddTotalNumberSwapping >= table->siftMaxSwap)
494  break;
495  x = table->perm[var[i]];
496  if (x < lower || x > upper) continue;
497  /* Only sift if not in symmetry group already. */
498  if (table->subtables[x].next == (unsigned) x) {
499 #ifdef DD_STATS
500  previousSize = table->keys - table->isolated;
501 #endif
502  result = ddSymmSiftingAux(table,x,lower,upper);
503  if (!result) goto ddSymmSiftingConvOutOfMem;
504 #ifdef DD_STATS
505  if (table->keys < (unsigned) previousSize + table->isolated) {
506  (void) fprintf(table->out,"-");
507  } else if (table->keys > (unsigned) previousSize +
508  table->isolated) {
509  (void) fprintf(table->out,"+");
510  } else {
511  (void) fprintf(table->out,"=");
512  }
513  fflush(table->out);
514 #endif
515  }
516  }
517 
518  /* Sifting now until convergence. */
519  while ((unsigned) initialSize > table->keys - table->isolated) {
520  initialSize = table->keys - table->isolated;
521 #ifdef DD_STATS
522  (void) fprintf(table->out,"\n");
523 #endif
524  /* Here we consider only one representative for each symmetry class. */
525  for (x = lower, classes = 0; x <= upper; x++, classes++) {
526  while ((unsigned) x < table->subtables[x].next) {
527  x = table->subtables[x].next;
528  }
529  /* Here x is the largest index in a group.
530  ** Groups consist of adjacent variables.
531  ** Hence, the next increment of x will move it to a new group.
532  */
533  i = table->invperm[x];
534  entry[i] = table->subtables[x].keys;
535  var[classes] = i;
536  }
537 
538  qsort((void *)var,classes,sizeof(int),(DD_QSFP)ddSymmUniqueCompare);
539 
540  /* Now sift. */
541  for (i = 0; i < ddMin(table->siftMaxVar,classes); i++) {
542  if (ddTotalNumberSwapping >= table->siftMaxSwap)
543  break;
544  x = table->perm[var[i]];
545  if ((unsigned) x >= table->subtables[x].next) {
546 #ifdef DD_STATS
547  previousSize = table->keys - table->isolated;
548 #endif
549  result = ddSymmSiftingConvAux(table,x,lower,upper);
550  if (!result ) goto ddSymmSiftingConvOutOfMem;
551 #ifdef DD_STATS
552  if (table->keys < (unsigned) previousSize + table->isolated) {
553  (void) fprintf(table->out,"-");
554  } else if (table->keys > (unsigned) previousSize +
555  table->isolated) {
556  (void) fprintf(table->out,"+");
557  } else {
558  (void) fprintf(table->out,"=");
559  }
560  fflush(table->out);
561 #endif
562  }
563  } /* for */
564  }
565 
566  ddSymmSummary(table, lower, upper, &symvars, &symgroups);
567 
568 #ifdef DD_STATS
569  (void) fprintf(table->out, "\n#:S_SIFTING %8d: symmetric variables\n",
570  symvars);
571  (void) fprintf(table->out, "#:G_SIFTING %8d: symmetric groups",
572  symgroups);
573 #endif
574 
575  ABC_FREE(var);
576  ABC_FREE(entry);
577 
578  return(1+symvars);
579 
580 ddSymmSiftingConvOutOfMem:
581 
582  if (entry != NULL) ABC_FREE(entry);
583  if (var != NULL) ABC_FREE(var);
584 
585  return(0);
586 
587 } /* end of cuddSymmSiftingConv */
unsigned int keys
Definition: cuddInt.h:330
static int * entry
Definition: cuddSymmetry.c:97
int siftMaxSwap
Definition: cuddInt.h:412
int(* DD_QSFP)(const void *, const void *)
Definition: cudd.h:326
int size
Definition: cuddInt.h:361
int var(Lit p)
Definition: SolverTypes.h:62
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
DdSubtable * subtables
Definition: cuddInt.h:365
unsigned int keys
Definition: cuddInt.h:369
FILE * out
Definition: cuddInt.h:441
static void ddSymmSummary(DdManager *table, int lower, int upper, int *symvars, int *symgroups)
static int size
Definition: cuddSign.c:86
#define ddMin(x, y)
Definition: cuddInt.h:818
static int ddSymmSiftingConvAux(DdManager *table, int x, int xLow, int xHigh)
Definition: cuddSymmetry.c:938
int siftMaxVar
Definition: cuddInt.h:411
#define ABC_FREE(obj)
Definition: abc_global.h:232
int ddTotalNumberSwapping
Definition: cuddReorder.c:107
unsigned int next
Definition: cuddInt.h:333
int * invperm
Definition: cuddInt.h:388
static int result
Definition: cuddGenetic.c:125
int isolated
Definition: cuddInt.h:385
static int ddSymmUniqueCompare(int *ptrX, int *ptrY)
Definition: cuddSymmetry.c:608
int * perm
Definition: cuddInt.h:386
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
static int ddSymmSiftingAux(DdManager *table, int x, int xLow, int xHigh)
Definition: cuddSymmetry.c:636
static int ddSymmGroupMove ( DdManager table,
int  x,
int  y,
Move **  moves 
)
static

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 1475 of file cuddSymmetry.c.

1480 {
1481  Move *move;
1482  int size = -1;
1483  int i,j;
1484  int xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
1485  int swapx = -1,swapy = -1;
1486 
1487 #ifdef DD_DEBUG
1488  assert(x < y); /* we assume that x < y */
1489 #endif
1490  /* Find top, bottom, and size for the two groups. */
1491  xbot = x;
1492  xtop = table->subtables[x].next;
1493  xsize = xbot - xtop + 1;
1494  ybot = y;
1495  while ((unsigned) ybot < table->subtables[ybot].next)
1496  ybot = table->subtables[ybot].next;
1497  ytop = y;
1498  ysize = ybot - ytop + 1;
1499 
1500  /* Sift the variables of the second group up through the first group. */
1501  for (i = 1; i <= ysize; i++) {
1502  for (j = 1; j <= xsize; j++) {
1503  size = cuddSwapInPlace(table,x,y);
1504  if (size == 0) return(0);
1505  swapx = x; swapy = y;
1506  y = x;
1507  x = y - 1;
1508  }
1509  y = ytop + i;
1510  x = y - 1;
1511  }
1512 
1513  /* fix symmetries */
1514  y = xtop; /* ytop is now where xtop used to be */
1515  for (i = 0; i < ysize-1 ; i++) {
1516  table->subtables[y].next = y + 1;
1517  y = y + 1;
1518  }
1519  table->subtables[y].next = xtop; /* y is bottom of its group, join */
1520  /* its symmetry to top of its group */
1521  x = y + 1;
1522  newxtop = x;
1523  for (i = 0; i < xsize - 1 ; i++) {
1524  table->subtables[x].next = x + 1;
1525  x = x + 1;
1526  }
1527  table->subtables[x].next = newxtop; /* x is bottom of its group, join */
1528  /* its symmetry to top of its group */
1529  /* Store group move */
1530  move = (Move *) cuddDynamicAllocNode(table);
1531  if (move == NULL) return(0);
1532  move->x = swapx;
1533  move->y = swapy;
1534  move->size = size;
1535  move->next = *moves;
1536  *moves = move;
1537 
1538  return(size);
1539 
1540 } /* end of ddSymmGroupMove */
Definition: cuddInt.h:492
DdSubtable * subtables
Definition: cuddInt.h:365
DdHalfWord x
Definition: cuddInt.h:493
static int size
Definition: cuddSign.c:86
DdNode * cuddDynamicAllocNode(DdManager *table)
Definition: cuddReorder.c:406
int cuddSwapInPlace(DdManager *table, int x, int y)
Definition: cuddReorder.c:761
DdHalfWord y
Definition: cuddInt.h:494
unsigned int next
Definition: cuddInt.h:333
struct Move * next
Definition: cuddInt.h:497
#define assert(ex)
Definition: util_old.h:213
int size
Definition: cuddInt.h:496
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 1556 of file cuddSymmetry.c.

1560 {
1561  int size = -1;
1562  int i,j;
1563  int xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
1564 
1565 #ifdef DD_DEBUG
1566  assert(x < y); /* We assume that x < y */
1567 #endif
1568 
1569  /* Find top, bottom, and size for the two groups. */
1570  xbot = x;
1571  xtop = table->subtables[x].next;
1572  xsize = xbot - xtop + 1;
1573  ybot = y;
1574  while ((unsigned) ybot < table->subtables[ybot].next)
1575  ybot = table->subtables[ybot].next;
1576  ytop = y;
1577  ysize = ybot - ytop + 1;
1578 
1579  /* Sift the variables of the second group up through the first group. */
1580  for (i = 1; i <= ysize; i++) {
1581  for (j = 1; j <= xsize; j++) {
1582  size = cuddSwapInPlace(table,x,y);
1583  if (size == 0) return(0);
1584  y = x;
1585  x = cuddNextLow(table,y);
1586  }
1587  y = ytop + i;
1588  x = y - 1;
1589  }
1590 
1591  /* Fix symmetries. */
1592  y = xtop;
1593  for (i = 0; i < ysize-1 ; i++) {
1594  table->subtables[y].next = y + 1;
1595  y = y + 1;
1596  }
1597  table->subtables[y].next = xtop; /* y is bottom of its group, join */
1598  /* its symmetry to top of its group */
1599  x = y + 1;
1600  newxtop = x;
1601  for (i = 0; i < xsize-1 ; i++) {
1602  table->subtables[x].next = x + 1;
1603  x = x + 1;
1604  }
1605  table->subtables[x].next = newxtop; /* x is bottom of its group, join */
1606  /* its symmetry to top of its group */
1607 
1608  return(size);
1609 
1610 } /* end of ddSymmGroupMoveBackward */
int cuddNextLow(DdManager *table, int x)
Definition: cuddReorder.c:738
DdSubtable * subtables
Definition: cuddInt.h:365
static int size
Definition: cuddSign.c:86
int cuddSwapInPlace(DdManager *table, int x, int y)
Definition: cuddReorder.c:761
unsigned int next
Definition: cuddInt.h:333
#define assert(ex)
Definition: util_old.h:213
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 636 of file cuddSymmetry.c.

641 {
642  Move *move;
643  Move *moveUp; /* list of up moves */
644  Move *moveDown; /* list of down moves */
645  int initialSize;
646  int result;
647  int i;
648  int topbot; /* index to either top or bottom of symmetry group */
649  int initGroupSize, finalGroupSize;
650 
651 
652 #ifdef DD_DEBUG
653  /* check for previously detected symmetry */
654  assert(table->subtables[x].next == (unsigned) x);
655 #endif
656 
657  initialSize = table->keys - table->isolated;
658 
659  moveDown = NULL;
660  moveUp = NULL;
661 
662  if ((x - xLow) > (xHigh - x)) {
663  /* Will go down first, unless x == xHigh:
664  ** Look for consecutive symmetries above x.
665  */
666  for (i = x; i > xLow; i--) {
667  if (!cuddSymmCheck(table,i-1,i))
668  break;
669  topbot = table->subtables[i-1].next; /* find top of i-1's group */
670  table->subtables[i-1].next = i;
671  table->subtables[x].next = topbot; /* x is bottom of group so its */
672  /* next is top of i-1's group */
673  i = topbot + 1; /* add 1 for i--; new i is top of symm group */
674  }
675  } else {
676  /* Will go up first unless x == xlow:
677  ** Look for consecutive symmetries below x.
678  */
679  for (i = x; i < xHigh; i++) {
680  if (!cuddSymmCheck(table,i,i+1))
681  break;
682  /* find bottom of i+1's symm group */
683  topbot = i + 1;
684  while ((unsigned) topbot < table->subtables[topbot].next) {
685  topbot = table->subtables[topbot].next;
686  }
687  table->subtables[topbot].next = table->subtables[i].next;
688  table->subtables[i].next = i + 1;
689  i = topbot - 1; /* subtract 1 for i++; new i is bottom of group */
690  }
691  }
692 
693  /* Now x may be in the middle of a symmetry group.
694  ** Find bottom of x's symm group.
695  */
696  while ((unsigned) x < table->subtables[x].next)
697  x = table->subtables[x].next;
698 
699  if (x == xLow) { /* Sift down */
700 
701 #ifdef DD_DEBUG
702  /* x must be a singleton */
703  assert((unsigned) x == table->subtables[x].next);
704 #endif
705  if (x == xHigh) return(1); /* just one variable */
706 
707  initGroupSize = 1;
708 
709  moveDown = ddSymmSiftingDown(table,x,xHigh);
710  /* after this point x --> xHigh, unless early term */
711  if (moveDown == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
712  if (moveDown == NULL) return(1);
713 
714  x = moveDown->y;
715  /* Find bottom of x's group */
716  i = x;
717  while ((unsigned) i < table->subtables[i].next) {
718  i = table->subtables[i].next;
719  }
720 #ifdef DD_DEBUG
721  /* x should be the top of the symmetry group and i the bottom */
722  assert((unsigned) i >= table->subtables[i].next);
723  assert((unsigned) x == table->subtables[i].next);
724 #endif
725  finalGroupSize = i - x + 1;
726 
727  if (initGroupSize == finalGroupSize) {
728  /* No new symmetry groups detected, return to best position */
729  result = ddSymmSiftingBackward(table,moveDown,initialSize);
730  } else {
731  initialSize = table->keys - table->isolated;
732  moveUp = ddSymmSiftingUp(table,x,xLow);
733  result = ddSymmSiftingBackward(table,moveUp,initialSize);
734  }
735  if (!result) goto ddSymmSiftingAuxOutOfMem;
736 
737  } else if (cuddNextHigh(table,x) > xHigh) { /* Sift up */
738  /* Find top of x's symm group */
739  i = x; /* bottom */
740  x = table->subtables[x].next; /* top */
741 
742  if (x == xLow) return(1); /* just one big group */
743 
744  initGroupSize = i - x + 1;
745 
746  moveUp = ddSymmSiftingUp(table,x,xLow);
747  /* after this point x --> xLow, unless early term */
748  if (moveUp == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
749  if (moveUp == NULL) return(1);
750 
751  x = moveUp->x;
752  /* Find top of x's group */
753  i = table->subtables[x].next;
754 #ifdef DD_DEBUG
755  /* x should be the bottom of the symmetry group and i the top */
756  assert((unsigned) x >= table->subtables[x].next);
757  assert((unsigned) i == table->subtables[x].next);
758 #endif
759  finalGroupSize = x - i + 1;
760 
761  if (initGroupSize == finalGroupSize) {
762  /* No new symmetry groups detected, return to best position */
763  result = ddSymmSiftingBackward(table,moveUp,initialSize);
764  } else {
765  initialSize = table->keys - table->isolated;
766  moveDown = ddSymmSiftingDown(table,x,xHigh);
767  result = ddSymmSiftingBackward(table,moveDown,initialSize);
768  }
769  if (!result) goto ddSymmSiftingAuxOutOfMem;
770 
771  } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */
772 
773  moveDown = ddSymmSiftingDown(table,x,xHigh);
774  /* at this point x == xHigh, unless early term */
775  if (moveDown == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
776 
777  if (moveDown != NULL) {
778  x = moveDown->y; /* x is top here */
779  i = x;
780  while ((unsigned) i < table->subtables[i].next) {
781  i = table->subtables[i].next;
782  }
783  } else {
784  i = x;
785  while ((unsigned) i < table->subtables[i].next) {
786  i = table->subtables[i].next;
787  }
788  x = table->subtables[i].next;
789  }
790 #ifdef DD_DEBUG
791  /* x should be the top of the symmetry group and i the bottom */
792  assert((unsigned) i >= table->subtables[i].next);
793  assert((unsigned) x == table->subtables[i].next);
794 #endif
795  initGroupSize = i - x + 1;
796 
797  moveUp = ddSymmSiftingUp(table,x,xLow);
798  if (moveUp == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
799 
800  if (moveUp != NULL) {
801  x = moveUp->x;
802  i = table->subtables[x].next;
803  } else {
804  i = x;
805  while ((unsigned) x < table->subtables[x].next)
806  x = table->subtables[x].next;
807  }
808 #ifdef DD_DEBUG
809  /* x should be the bottom of the symmetry group and i the top */
810  assert((unsigned) x >= table->subtables[x].next);
811  assert((unsigned) i == table->subtables[x].next);
812 #endif
813  finalGroupSize = x - i + 1;
814 
815  if (initGroupSize == finalGroupSize) {
816  /* No new symmetry groups detected, return to best position */
817  result = ddSymmSiftingBackward(table,moveUp,initialSize);
818  } else {
819  while (moveDown != NULL) {
820  move = moveDown->next;
821  cuddDeallocMove(table, moveDown);
822  moveDown = move;
823  }
824  initialSize = table->keys - table->isolated;
825  moveDown = ddSymmSiftingDown(table,x,xHigh);
826  result = ddSymmSiftingBackward(table,moveDown,initialSize);
827  }
828  if (!result) goto ddSymmSiftingAuxOutOfMem;
829 
830  } else { /* moving up first: shorter */
831  /* Find top of x's symmetry group */
832  x = table->subtables[x].next;
833 
834  moveUp = ddSymmSiftingUp(table,x,xLow);
835  /* at this point x == xHigh, unless early term */
836  if (moveUp == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
837 
838  if (moveUp != NULL) {
839  x = moveUp->x;
840  i = table->subtables[x].next;
841  } else {
842  while ((unsigned) x < table->subtables[x].next)
843  x = table->subtables[x].next;
844  i = table->subtables[x].next;
845  }
846 #ifdef DD_DEBUG
847  /* x is bottom of the symmetry group and i is top */
848  assert((unsigned) x >= table->subtables[x].next);
849  assert((unsigned) i == table->subtables[x].next);
850 #endif
851  initGroupSize = x - i + 1;
852 
853  moveDown = ddSymmSiftingDown(table,x,xHigh);
854  if (moveDown == MV_OOM) goto ddSymmSiftingAuxOutOfMem;
855 
856  if (moveDown != NULL) {
857  x = moveDown->y;
858  i = x;
859  while ((unsigned) i < table->subtables[i].next) {
860  i = table->subtables[i].next;
861  }
862  } else {
863  i = x;
864  x = table->subtables[x].next;
865  }
866 #ifdef DD_DEBUG
867  /* x should be the top of the symmetry group and i the bottom */
868  assert((unsigned) i >= table->subtables[i].next);
869  assert((unsigned) x == table->subtables[i].next);
870 #endif
871  finalGroupSize = i - x + 1;
872 
873  if (initGroupSize == finalGroupSize) {
874  /* No new symmetries detected, go back to best position */
875  result = ddSymmSiftingBackward(table,moveDown,initialSize);
876  } else {
877  while (moveUp != NULL) {
878  move = moveUp->next;
879  cuddDeallocMove(table, moveUp);
880  moveUp = move;
881  }
882  initialSize = table->keys - table->isolated;
883  moveUp = ddSymmSiftingUp(table,x,xLow);
884  result = ddSymmSiftingBackward(table,moveUp,initialSize);
885  }
886  if (!result) goto ddSymmSiftingAuxOutOfMem;
887  }
888 
889  while (moveDown != NULL) {
890  move = moveDown->next;
891  cuddDeallocMove(table, moveDown);
892  moveDown = move;
893  }
894  while (moveUp != NULL) {
895  move = moveUp->next;
896  cuddDeallocMove(table, moveUp);
897  moveUp = move;
898  }
899 
900  return(1);
901 
902 ddSymmSiftingAuxOutOfMem:
903  if (moveDown != MV_OOM) {
904  while (moveDown != NULL) {
905  move = moveDown->next;
906  cuddDeallocMove(table, moveDown);
907  moveDown = move;
908  }
909  }
910  if (moveUp != MV_OOM) {
911  while (moveUp != NULL) {
912  move = moveUp->next;
913  cuddDeallocMove(table, moveUp);
914  moveUp = move;
915  }
916  }
917 
918  return(0);
919 
920 } /* end of ddSymmSiftingAux */
#define MV_OOM
Definition: cuddSymmetry.c:79
#define cuddDeallocMove(unique, node)
Definition: cuddInt.h:564
static Move * ddSymmSiftingDown(DdManager *table, int x, int xHigh)
int cuddSymmCheck(DdManager *table, int x, int y)
Definition: cuddSymmetry.c:192
Definition: cuddInt.h:492
DdSubtable * subtables
Definition: cuddInt.h:365
unsigned int keys
Definition: cuddInt.h:369
DdHalfWord x
Definition: cuddInt.h:493
static int ddSymmSiftingBackward(DdManager *table, Move *moves, int size)
static Move * ddSymmSiftingUp(DdManager *table, int y, int xLow)
int cuddNextHigh(DdManager *table, int x)
Definition: cuddReorder.c:716
DdHalfWord y
Definition: cuddInt.h:494
unsigned int next
Definition: cuddInt.h:333
struct Move * next
Definition: cuddInt.h:497
#define assert(ex)
Definition: util_old.h:213
static int result
Definition: cuddGenetic.c:125
int isolated
Definition: cuddInt.h:385
static int ddSymmSiftingBackward ( DdManager table,
Move moves,
int  size 
)
static

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 1627 of file cuddSymmetry.c.

1631 {
1632  Move *move;
1633  int res = -1;
1634 
1635  for (move = moves; move != NULL; move = move->next) {
1636  if (move->size < size) {
1637  size = move->size;
1638  }
1639  }
1640 
1641  for (move = moves; move != NULL; move = move->next) {
1642  if (move->size == size) return(1);
1643  if (table->subtables[move->x].next == move->x && table->subtables[move->y].next == move->y) {
1644  res = cuddSwapInPlace(table,(int)move->x,(int)move->y);
1645 #ifdef DD_DEBUG
1646  assert(table->subtables[move->x].next == move->x);
1647  assert(table->subtables[move->y].next == move->y);
1648 #endif
1649  } else { /* Group move necessary */
1650  res = ddSymmGroupMoveBackward(table,(int)move->x,(int)move->y);
1651  }
1652  if (!res) return(0);
1653  }
1654 
1655  return(1);
1656 
1657 } /* end of ddSymmSiftingBackward */
static int ddSymmGroupMoveBackward(DdManager *table, int x, int y)
Definition: cuddInt.h:492
DdSubtable * subtables
Definition: cuddInt.h:365
DdHalfWord x
Definition: cuddInt.h:493
static int size
Definition: cuddSign.c:86
int cuddSwapInPlace(DdManager *table, int x, int y)
Definition: cuddReorder.c:761
DdHalfWord y
Definition: cuddInt.h:494
unsigned int next
Definition: cuddInt.h:333
struct Move * next
Definition: cuddInt.h:497
#define assert(ex)
Definition: util_old.h:213
int size
Definition: cuddInt.h:496
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 938 of file cuddSymmetry.c.

943 {
944  Move *move;
945  Move *moveUp; /* list of up moves */
946  Move *moveDown; /* list of down moves */
947  int initialSize;
948  int result;
949  int i;
950  int initGroupSize, finalGroupSize;
951 
952 
953  initialSize = table->keys - table->isolated;
954 
955  moveDown = NULL;
956  moveUp = NULL;
957 
958  if (x == xLow) { /* Sift down */
959 #ifdef DD_DEBUG
960  /* x is bottom of symmetry group */
961  assert((unsigned) x >= table->subtables[x].next);
962 #endif
963  i = table->subtables[x].next;
964  initGroupSize = x - i + 1;
965 
966  moveDown = ddSymmSiftingDown(table,x,xHigh);
967  /* at this point x == xHigh, unless early term */
968  if (moveDown == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
969  if (moveDown == NULL) return(1);
970 
971  x = moveDown->y;
972  i = x;
973  while ((unsigned) i < table->subtables[i].next) {
974  i = table->subtables[i].next;
975  }
976 #ifdef DD_DEBUG
977  /* x should be the top of the symmetric group and i the bottom */
978  assert((unsigned) i >= table->subtables[i].next);
979  assert((unsigned) x == table->subtables[i].next);
980 #endif
981  finalGroupSize = i - x + 1;
982 
983  if (initGroupSize == finalGroupSize) {
984  /* No new symmetries detected, go back to best position */
985  result = ddSymmSiftingBackward(table,moveDown,initialSize);
986  } else {
987  initialSize = table->keys - table->isolated;
988  moveUp = ddSymmSiftingUp(table,x,xLow);
989  result = ddSymmSiftingBackward(table,moveUp,initialSize);
990  }
991  if (!result) goto ddSymmSiftingConvAuxOutOfMem;
992 
993  } else if (cuddNextHigh(table,x) > xHigh) { /* Sift up */
994  /* Find top of x's symm group */
995  while ((unsigned) x < table->subtables[x].next)
996  x = table->subtables[x].next;
997  i = x; /* bottom */
998  x = table->subtables[x].next; /* top */
999 
1000  if (x == xLow) return(1);
1001 
1002  initGroupSize = i - x + 1;
1003 
1004  moveUp = ddSymmSiftingUp(table,x,xLow);
1005  /* at this point x == xLow, unless early term */
1006  if (moveUp == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
1007  if (moveUp == NULL) return(1);
1008 
1009  x = moveUp->x;
1010  i = table->subtables[x].next;
1011 #ifdef DD_DEBUG
1012  /* x should be the bottom of the symmetry group and i the top */
1013  assert((unsigned) x >= table->subtables[x].next);
1014  assert((unsigned) i == table->subtables[x].next);
1015 #endif
1016  finalGroupSize = x - i + 1;
1017 
1018  if (initGroupSize == finalGroupSize) {
1019  /* No new symmetry groups detected, return to best position */
1020  result = ddSymmSiftingBackward(table,moveUp,initialSize);
1021  } else {
1022  initialSize = table->keys - table->isolated;
1023  moveDown = ddSymmSiftingDown(table,x,xHigh);
1024  result = ddSymmSiftingBackward(table,moveDown,initialSize);
1025  }
1026  if (!result)
1027  goto ddSymmSiftingConvAuxOutOfMem;
1028 
1029  } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */
1030  moveDown = ddSymmSiftingDown(table,x,xHigh);
1031  /* at this point x == xHigh, unless early term */
1032  if (moveDown == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
1033 
1034  if (moveDown != NULL) {
1035  x = moveDown->y;
1036  i = x;
1037  while ((unsigned) i < table->subtables[i].next) {
1038  i = table->subtables[i].next;
1039  }
1040  } else {
1041  while ((unsigned) x < table->subtables[x].next)
1042  x = table->subtables[x].next;
1043  i = x;
1044  x = table->subtables[x].next;
1045  }
1046 #ifdef DD_DEBUG
1047  /* x should be the top of the symmetry group and i the bottom */
1048  assert((unsigned) i >= table->subtables[i].next);
1049  assert((unsigned) x == table->subtables[i].next);
1050 #endif
1051  initGroupSize = i - x + 1;
1052 
1053  moveUp = ddSymmSiftingUp(table,x,xLow);
1054  if (moveUp == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
1055 
1056  if (moveUp != NULL) {
1057  x = moveUp->x;
1058  i = table->subtables[x].next;
1059  } else {
1060  i = x;
1061  while ((unsigned) x < table->subtables[x].next)
1062  x = table->subtables[x].next;
1063  }
1064 #ifdef DD_DEBUG
1065  /* x should be the bottom of the symmetry group and i the top */
1066  assert((unsigned) x >= table->subtables[x].next);
1067  assert((unsigned) i == table->subtables[x].next);
1068 #endif
1069  finalGroupSize = x - i + 1;
1070 
1071  if (initGroupSize == finalGroupSize) {
1072  /* No new symmetry groups detected, return to best position */
1073  result = ddSymmSiftingBackward(table,moveUp,initialSize);
1074  } else {
1075  while (moveDown != NULL) {
1076  move = moveDown->next;
1077  cuddDeallocMove(table, moveDown);
1078  moveDown = move;
1079  }
1080  initialSize = table->keys - table->isolated;
1081  moveDown = ddSymmSiftingDown(table,x,xHigh);
1082  result = ddSymmSiftingBackward(table,moveDown,initialSize);
1083  }
1084  if (!result) goto ddSymmSiftingConvAuxOutOfMem;
1085 
1086  } else { /* moving up first: shorter */
1087  /* Find top of x's symmetry group */
1088  x = table->subtables[x].next;
1089 
1090  moveUp = ddSymmSiftingUp(table,x,xLow);
1091  /* at this point x == xHigh, unless early term */
1092  if (moveUp == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
1093 
1094  if (moveUp != NULL) {
1095  x = moveUp->x;
1096  i = table->subtables[x].next;
1097  } else {
1098  i = x;
1099  while ((unsigned) x < table->subtables[x].next)
1100  x = table->subtables[x].next;
1101  }
1102 #ifdef DD_DEBUG
1103  /* x is bottom of the symmetry group and i is top */
1104  assert((unsigned) x >= table->subtables[x].next);
1105  assert((unsigned) i == table->subtables[x].next);
1106 #endif
1107  initGroupSize = x - i + 1;
1108 
1109  moveDown = ddSymmSiftingDown(table,x,xHigh);
1110  if (moveDown == MV_OOM) goto ddSymmSiftingConvAuxOutOfMem;
1111 
1112  if (moveDown != NULL) {
1113  x = moveDown->y;
1114  i = x;
1115  while ((unsigned) i < table->subtables[i].next) {
1116  i = table->subtables[i].next;
1117  }
1118  } else {
1119  i = x;
1120  x = table->subtables[x].next;
1121  }
1122 #ifdef DD_DEBUG
1123  /* x should be the top of the symmetry group and i the bottom */
1124  assert((unsigned) i >= table->subtables[i].next);
1125  assert((unsigned) x == table->subtables[i].next);
1126 #endif
1127  finalGroupSize = i - x + 1;
1128 
1129  if (initGroupSize == finalGroupSize) {
1130  /* No new symmetries detected, go back to best position */
1131  result = ddSymmSiftingBackward(table,moveDown,initialSize);
1132  } else {
1133  while (moveUp != NULL) {
1134  move = moveUp->next;
1135  cuddDeallocMove(table, moveUp);
1136  moveUp = move;
1137  }
1138  initialSize = table->keys - table->isolated;
1139  moveUp = ddSymmSiftingUp(table,x,xLow);
1140  result = ddSymmSiftingBackward(table,moveUp,initialSize);
1141  }
1142  if (!result) goto ddSymmSiftingConvAuxOutOfMem;
1143  }
1144 
1145  while (moveDown != NULL) {
1146  move = moveDown->next;
1147  cuddDeallocMove(table, moveDown);
1148  moveDown = move;
1149  }
1150  while (moveUp != NULL) {
1151  move = moveUp->next;
1152  cuddDeallocMove(table, moveUp);
1153  moveUp = move;
1154  }
1155 
1156  return(1);
1157 
1158 ddSymmSiftingConvAuxOutOfMem:
1159  if (moveDown != MV_OOM) {
1160  while (moveDown != NULL) {
1161  move = moveDown->next;
1162  cuddDeallocMove(table, moveDown);
1163  moveDown = move;
1164  }
1165  }
1166  if (moveUp != MV_OOM) {
1167  while (moveUp != NULL) {
1168  move = moveUp->next;
1169  cuddDeallocMove(table, moveUp);
1170  moveUp = move;
1171  }
1172  }
1173 
1174  return(0);
1175 
1176 } /* end of ddSymmSiftingConvAux */
#define MV_OOM
Definition: cuddSymmetry.c:79
#define cuddDeallocMove(unique, node)
Definition: cuddInt.h:564
static Move * ddSymmSiftingDown(DdManager *table, int x, int xHigh)
Definition: cuddInt.h:492
DdSubtable * subtables
Definition: cuddInt.h:365
unsigned int keys
Definition: cuddInt.h:369
DdHalfWord x
Definition: cuddInt.h:493
static int ddSymmSiftingBackward(DdManager *table, Move *moves, int size)
static Move * ddSymmSiftingUp(DdManager *table, int y, int xLow)
int cuddNextHigh(DdManager *table, int x)
Definition: cuddReorder.c:716
DdHalfWord y
Definition: cuddInt.h:494
unsigned int next
Definition: cuddInt.h:333
struct Move * next
Definition: cuddInt.h:497
#define assert(ex)
Definition: util_old.h:213
static int result
Definition: cuddGenetic.c:125
int isolated
Definition: cuddInt.h:385
static Move * ddSymmSiftingDown ( DdManager table,
int  x,
int  xHigh 
)
static

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 1337 of file cuddSymmetry.c.

1341 {
1342  Move *moves;
1343  Move *move;
1344  int y;
1345  int size;
1346  int limitSize;
1347  int gxtop,gybot;
1348  int R; /* upper bound on node decrease */
1349  int xindex, yindex;
1350  int isolated;
1351  int z;
1352  int zindex;
1353 #ifdef DD_DEBUG
1354  int checkR;
1355 #endif
1356 
1357  moves = NULL;
1358  /* Initialize R */
1359  xindex = table->invperm[x];
1360  gxtop = table->subtables[x].next;
1361  limitSize = size = table->keys - table->isolated;
1362  R = 0;
1363  for (z = xHigh; z > gxtop; z--) {
1364  zindex = table->invperm[z];
1365  if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
1366  isolated = table->vars[zindex]->ref == 1;
1367  R += table->subtables[z].keys - isolated;
1368  }
1369  }
1370 
1371  y = cuddNextHigh(table,x);
1372  while (y <= xHigh && size - R < limitSize) {
1373 #ifdef DD_DEBUG
1374  gxtop = table->subtables[x].next;
1375  checkR = 0;
1376  for (z = xHigh; z > gxtop; z--) {
1377  zindex = table->invperm[z];
1378  if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
1379  isolated = table->vars[zindex]->ref == 1;
1380  checkR += table->subtables[z].keys - isolated;
1381  }
1382  }
1383  assert(R == checkR);
1384 #endif
1385  gybot = table->subtables[y].next;
1386  while (table->subtables[gybot].next != (unsigned) y)
1387  gybot = table->subtables[gybot].next;
1388  if (cuddSymmCheck(table,x,y)) {
1389  /* Symmetry found, attach symm groups */
1390  gxtop = table->subtables[x].next;
1391  table->subtables[x].next = y;
1392  table->subtables[gybot].next = gxtop;
1393  } else if (table->subtables[x].next == (unsigned) x &&
1394  table->subtables[y].next == (unsigned) y) {
1395  /* x and y have self symmetry */
1396  /* Update upper bound on node decrease. */
1397  yindex = table->invperm[y];
1398  if (cuddTestInteract(table,xindex,yindex)) {
1399  isolated = table->vars[yindex]->ref == 1;
1400  R -= table->subtables[y].keys - isolated;
1401  }
1402  size = cuddSwapInPlace(table,x,y);
1403 #ifdef DD_DEBUG
1404  assert(table->subtables[x].next == (unsigned) x);
1405  assert(table->subtables[y].next == (unsigned) y);
1406 #endif
1407  if (size == 0) goto ddSymmSiftingDownOutOfMem;
1408  move = (Move *) cuddDynamicAllocNode(table);
1409  if (move == NULL) goto ddSymmSiftingDownOutOfMem;
1410  move->x = x;
1411  move->y = y;
1412  move->size = size;
1413  move->next = moves;
1414  moves = move;
1415  if ((double) size > (double) limitSize * table->maxGrowth)
1416  return(moves);
1417  if (size < limitSize) limitSize = size;
1418  } else { /* Group move */
1419  /* Update upper bound on node decrease: first phase. */
1420  gxtop = table->subtables[x].next;
1421  z = gxtop + 1;
1422  do {
1423  zindex = table->invperm[z];
1424  if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
1425  isolated = table->vars[zindex]->ref == 1;
1426  R -= table->subtables[z].keys - isolated;
1427  }
1428  z++;
1429  } while (z <= gybot);
1430  size = ddSymmGroupMove(table,x,y,&moves);
1431  if (size == 0) goto ddSymmSiftingDownOutOfMem;
1432  if ((double) size > (double) limitSize * table->maxGrowth)
1433  return(moves);
1434  if (size < limitSize) limitSize = size;
1435  /* Update upper bound on node decrease: second phase. */
1436  gxtop = table->subtables[gybot].next;
1437  for (z = gxtop + 1; z <= gybot; z++) {
1438  zindex = table->invperm[z];
1439  if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
1440  isolated = table->vars[zindex]->ref == 1;
1441  R += table->subtables[z].keys - isolated;
1442  }
1443  }
1444  }
1445  x = gybot;
1446  y = cuddNextHigh(table,x);
1447  }
1448 
1449  return(moves);
1450 
1451 ddSymmSiftingDownOutOfMem:
1452  while (moves != NULL) {
1453  move = moves->next;
1454  cuddDeallocMove(table, moves);
1455  moves = move;
1456  }
1457  return(MV_OOM);
1458 
1459 } /* end of ddSymmSiftingDown */
DdHalfWord ref
Definition: cudd.h:280
unsigned int keys
Definition: cuddInt.h:330
#define MV_OOM
Definition: cuddSymmetry.c:79
#define cuddDeallocMove(unique, node)
Definition: cuddInt.h:564
int cuddSymmCheck(DdManager *table, int x, int y)
Definition: cuddSymmetry.c:192
Definition: cuddInt.h:492
double maxGrowth
Definition: cuddInt.h:413
DdSubtable * subtables
Definition: cuddInt.h:365
unsigned int keys
Definition: cuddInt.h:369
DdHalfWord x
Definition: cuddInt.h:493
static int size
Definition: cuddSign.c:86
DdNode * cuddDynamicAllocNode(DdManager *table)
Definition: cuddReorder.c:406
int cuddNextHigh(DdManager *table, int x)
Definition: cuddReorder.c:716
int cuddSwapInPlace(DdManager *table, int x, int y)
Definition: cuddReorder.c:761
DdHalfWord y
Definition: cuddInt.h:494
DdNode ** vars
Definition: cuddInt.h:390
unsigned int next
Definition: cuddInt.h:333
struct Move * next
Definition: cuddInt.h:497
#define assert(ex)
Definition: util_old.h:213
int * invperm
Definition: cuddInt.h:388
int isolated
Definition: cuddInt.h:385
int cuddTestInteract(DdManager *table, int x, int y)
Definition: cuddInteract.c:191
static int ddSymmGroupMove(DdManager *table, int x, int y, Move **moves)
int size
Definition: cuddInt.h:496
static Move * ddSymmSiftingUp ( DdManager table,
int  y,
int  xLow 
)
static

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 1195 of file cuddSymmetry.c.

1199 {
1200  Move *moves;
1201  Move *move;
1202  int x;
1203  int size;
1204  int i;
1205  int gxtop,gybot;
1206  int limitSize;
1207  int xindex, yindex;
1208  int zindex;
1209  int z;
1210  int isolated;
1211  int L; /* lower bound on DD size */
1212 #ifdef DD_DEBUG
1213  int checkL;
1214 #endif
1215 
1216 
1217  moves = NULL;
1218  yindex = table->invperm[y];
1219 
1220  /* Initialize the lower bound.
1221  ** The part of the DD below the bottom of y' group will not change.
1222  ** The part of the DD above y that does not interact with y will not
1223  ** change. The rest may vanish in the best case, except for
1224  ** the nodes at level xLow, which will not vanish, regardless.
1225  */
1226  limitSize = L = table->keys - table->isolated;
1227  gybot = y;
1228  while ((unsigned) gybot < table->subtables[gybot].next)
1229  gybot = table->subtables[gybot].next;
1230  for (z = xLow + 1; z <= gybot; z++) {
1231  zindex = table->invperm[z];
1232  if (zindex == yindex || cuddTestInteract(table,zindex,yindex)) {
1233  isolated = table->vars[zindex]->ref == 1;
1234  L -= table->subtables[z].keys - isolated;
1235  }
1236  }
1237 
1238  x = cuddNextLow(table,y);
1239  while (x >= xLow && L <= limitSize) {
1240 #ifdef DD_DEBUG
1241  gybot = y;
1242  while ((unsigned) gybot < table->subtables[gybot].next)
1243  gybot = table->subtables[gybot].next;
1244  checkL = table->keys - table->isolated;
1245  for (z = xLow + 1; z <= gybot; z++) {
1246  zindex = table->invperm[z];
1247  if (zindex == yindex || cuddTestInteract(table,zindex,yindex)) {
1248  isolated = table->vars[zindex]->ref == 1;
1249  checkL -= table->subtables[z].keys - isolated;
1250  }
1251  }
1252  assert(L == checkL);
1253 #endif
1254  gxtop = table->subtables[x].next;
1255  if (cuddSymmCheck(table,x,y)) {
1256  /* Symmetry found, attach symm groups */
1257  table->subtables[x].next = y;
1258  i = table->subtables[y].next;
1259  while (table->subtables[i].next != (unsigned) y)
1260  i = table->subtables[i].next;
1261  table->subtables[i].next = gxtop;
1262  } else if (table->subtables[x].next == (unsigned) x &&
1263  table->subtables[y].next == (unsigned) y) {
1264  /* x and y have self symmetry */
1265  xindex = table->invperm[x];
1266  size = cuddSwapInPlace(table,x,y);
1267 #ifdef DD_DEBUG
1268  assert(table->subtables[x].next == (unsigned) x);
1269  assert(table->subtables[y].next == (unsigned) y);
1270 #endif
1271  if (size == 0) goto ddSymmSiftingUpOutOfMem;
1272  /* Update the lower bound. */
1273  if (cuddTestInteract(table,xindex,yindex)) {
1274  isolated = table->vars[xindex]->ref == 1;
1275  L += table->subtables[y].keys - isolated;
1276  }
1277  move = (Move *) cuddDynamicAllocNode(table);
1278  if (move == NULL) goto ddSymmSiftingUpOutOfMem;
1279  move->x = x;
1280  move->y = y;
1281  move->size = size;
1282  move->next = moves;
1283  moves = move;
1284  if ((double) size > (double) limitSize * table->maxGrowth)
1285  return(moves);
1286  if (size < limitSize) limitSize = size;
1287  } else { /* Group move */
1288  size = ddSymmGroupMove(table,x,y,&moves);
1289  if (size == 0) goto ddSymmSiftingUpOutOfMem;
1290  /* Update the lower bound. */
1291  z = moves->y;
1292  do {
1293  zindex = table->invperm[z];
1294  if (cuddTestInteract(table,zindex,yindex)) {
1295  isolated = table->vars[zindex]->ref == 1;
1296  L += table->subtables[z].keys - isolated;
1297  }
1298  z = table->subtables[z].next;
1299  } while (z != (int) moves->y);
1300  if ((double) size > (double) limitSize * table->maxGrowth)
1301  return(moves);
1302  if (size < limitSize) limitSize = size;
1303  }
1304  y = gxtop;
1305  x = cuddNextLow(table,y);
1306  }
1307 
1308  return(moves);
1309 
1310 ddSymmSiftingUpOutOfMem:
1311  while (moves != NULL) {
1312  move = moves->next;
1313  cuddDeallocMove(table, moves);
1314  moves = move;
1315  }
1316  return(MV_OOM);
1317 
1318 } /* end of ddSymmSiftingUp */
DdHalfWord ref
Definition: cudd.h:280
unsigned int keys
Definition: cuddInt.h:330
#define MV_OOM
Definition: cuddSymmetry.c:79
#define cuddDeallocMove(unique, node)
Definition: cuddInt.h:564
int cuddSymmCheck(DdManager *table, int x, int y)
Definition: cuddSymmetry.c:192
Definition: cuddInt.h:492
int cuddNextLow(DdManager *table, int x)
Definition: cuddReorder.c:738
double maxGrowth
Definition: cuddInt.h:413
DdSubtable * subtables
Definition: cuddInt.h:365
unsigned int keys
Definition: cuddInt.h:369
DdHalfWord x
Definition: cuddInt.h:493
static int size
Definition: cuddSign.c:86
DdNode * cuddDynamicAllocNode(DdManager *table)
Definition: cuddReorder.c:406
int cuddSwapInPlace(DdManager *table, int x, int y)
Definition: cuddReorder.c:761
DdHalfWord y
Definition: cuddInt.h:494
DdNode ** vars
Definition: cuddInt.h:390
unsigned int next
Definition: cuddInt.h:333
struct Move * next
Definition: cuddInt.h:497
#define assert(ex)
Definition: util_old.h:213
int * invperm
Definition: cuddInt.h:388
int isolated
Definition: cuddInt.h:385
int cuddTestInteract(DdManager *table, int x, int y)
Definition: cuddInteract.c:191
static int ddSymmGroupMove(DdManager *table, int x, int y, Move **moves)
int size
Definition: cuddInt.h:496
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 1671 of file cuddSymmetry.c.

1677 {
1678  int i,x,gbot;
1679  int TotalSymm = 0;
1680  int TotalSymmGroups = 0;
1681 
1682  for (i = lower; i <= upper; i++) {
1683  if (table->subtables[i].next != (unsigned) i) {
1684  TotalSymmGroups++;
1685  x = i;
1686  do {
1687  TotalSymm++;
1688  gbot = x;
1689  x = table->subtables[x].next;
1690  } while (x != i);
1691 #ifdef DD_DEBUG
1692  assert(table->subtables[gbot].next == (unsigned) i);
1693 #endif
1694  i = gbot;
1695  }
1696  }
1697  *symvars = TotalSymm;
1698  *symgroups = TotalSymmGroups;
1699 
1700  return;
1701 
1702 } /* end of ddSymmSummary */
DdSubtable * subtables
Definition: cuddInt.h:365
unsigned int next
Definition: cuddInt.h:333
#define assert(ex)
Definition: util_old.h:213
static int ddSymmUniqueCompare ( int *  ptrX,
int *  ptrY 
)
static

AutomaticStart

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 608 of file cuddSymmetry.c.

611 {
612 #if 0
613  if (entry[*ptrY] == entry[*ptrX]) {
614  return((*ptrX) - (*ptrY));
615  }
616 #endif
617  return(entry[*ptrY] - entry[*ptrX]);
618 
619 } /* end of ddSymmUniqueCompare */
static int * entry
Definition: cuddSymmetry.c:97

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddSymmetry.c,v 1.26 2009/02/19 16:23:54 fabio Exp $"
static

Definition at line 94 of file cuddSymmetry.c.

int ddTotalNumberSwapping

Definition at line 107 of file cuddReorder.c.

int* entry
static

Definition at line 97 of file cuddSymmetry.c.