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

Go to the source code of this file.

Macros

#define ZDD_MV_OOM   (Move *)1
 

Functions

static int cuddZddSymmSiftingAux (DdManager *table, int x, int x_low, int x_high)
 
static int cuddZddSymmSiftingConvAux (DdManager *table, int x, int x_low, int x_high)
 
static Move * cuddZddSymmSifting_up (DdManager *table, int x, int x_low, int initial_size)
 
static Move * cuddZddSymmSifting_down (DdManager *table, int x, int x_high, int initial_size)
 
static int cuddZddSymmSiftingBackward (DdManager *table, Move *moves, int size)
 
static int zdd_group_move (DdManager *table, int x, int y, Move **moves)
 
static int zdd_group_move_backward (DdManager *table, int x, int y)
 
static void cuddZddSymmSummary (DdManager *table, int lower, int upper, int *symvars, int *symgroups)
 
void Cudd_zddSymmProfile (DdManager *table, int lower, int upper)
 
int cuddZddSymmCheck (DdManager *table, int x, int y)
 
int cuddZddSymmSifting (DdManager *table, int lower, int upper)
 
int cuddZddSymmSiftingConv (DdManager *table, int lower, int upper)
 

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddZddSymm.c,v 1.29 2004/08/13 18:04:54 fabio Exp $"
 
int * zdd_entry
 
int zddTotalNumberSwapping
 
static DdNode * empty
 

Macro Definition Documentation

#define ZDD_MV_OOM   (Move *)1

CFile***********************************************************************

FileName [cuddZddSymm.c]

PackageName [cudd]

Synopsis [Functions for symmetry-based ZDD variable reordering.]

Description [External procedures included in this module:

Internal procedures included in this module:

Static procedures included in this module:

]

SeeAlso [cuddSymmetry.c]

Author [Hyong-Kyoon Shin, In-Ho Moon]

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 81 of file cuddZddSymm.c.

Function Documentation

void Cudd_zddSymmProfile ( DdManager *  table,
int  lower,
int  upper 
)

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

Synopsis [Prints statistics on symmetric ZDD variables.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 145 of file cuddZddSymm.c.

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

SeeAlso []

Definition at line 197 of file cuddZddSymm.c.

201 {
202  int i;
203  DdNode *f, *f0, *f1, *f01, *f00, *f11, *f10;
204  int yindex;
205  int xsymmy = 1;
206  int xsymmyp = 1;
207  int arccount = 0;
208  int TotalRefCount = 0;
209  int symm_found;
210 
211  empty = table->zero;
212 
213  yindex = table->invpermZ[y];
214  for (i = table->subtableZ[x].slots - 1; i >= 0; i--) {
215  f = table->subtableZ[x].nodelist[i];
216  while (f != NULL) {
217  /* Find f1, f0, f11, f10, f01, f00 */
218  f1 = cuddT(f);
219  f0 = cuddE(f);
220  if ((int) f1->index == yindex) {
221  f11 = cuddT(f1);
222  f10 = cuddE(f1);
223  if (f10 != empty)
224  arccount++;
225  } else {
226  if ((int) f0->index != yindex) {
227  return(0); /* f bypasses layer y */
228  }
229  f11 = empty;
230  f10 = f1;
231  }
232  if ((int) f0->index == yindex) {
233  f01 = cuddT(f0);
234  f00 = cuddE(f0);
235  if (f00 != empty)
236  arccount++;
237  } else {
238  f01 = empty;
239  f00 = f0;
240  }
241  if (f01 != f10)
242  xsymmy = 0;
243  if (f11 != f00)
244  xsymmyp = 0;
245  if ((xsymmy == 0) && (xsymmyp == 0))
246  return(0);
247 
248  f = f->next;
249  } /* for each element of the collision list */
250  } /* for each slot of the subtable */
251 
252  /* Calculate the total reference counts of y
253  ** whose else arc is not empty.
254  */
255  for (i = table->subtableZ[y].slots - 1; i >= 0; i--) {
256  f = table->subtableZ[y].nodelist[i];
257  while (f != NIL(DdNode)) {
258  if (cuddE(f) != empty)
259  TotalRefCount += f->ref;
260  f = f->next;
261  }
262  }
263 
264  symm_found = (arccount == TotalRefCount);
265 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
266  if (symm_found) {
267  int xindex = table->invpermZ[x];
268  (void) fprintf(table->out,
269  "Found symmetry! x =%d\ty = %d\tPos(%d,%d)\n",
270  xindex,yindex,x,y);
271  }
272 #endif
273 
274  return(symm_found);
275 
276 } /* end cuddZddSymmCheck */
DdNode::ref
DdHalfWord ref
Definition: cudd.h:280
DdNode
Definition: cudd.h:278
DdManager::invpermZ
int * invpermZ
Definition: cuddInt.h:389
DdManager::zero
DdNode * zero
Definition: cuddInt.h:346
NIL
#define NIL(type)
Definition: avl.h:25
empty
static DdNode * empty
Definition: cuddZddSymm.c:103
DdManager::out
FILE * out
Definition: cuddInt.h:441
DdNode::next
DdNode * next
Definition: cudd.h:281
DdSubtable::nodelist
DdNode ** nodelist
Definition: cuddInt.h:327
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
DdNode::index
DdHalfWord index
Definition: cudd.h:279
DdSubtable::slots
unsigned int slots
Definition: cuddInt.h:329
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
DdManager::subtableZ
DdSubtable * subtableZ
Definition: cuddInt.h:366
int cuddZddSymmSifting ( DdManager *  table,
int  lower,
int  upper 
)

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

Synopsis [Symmetric sifting algorithm for ZDDs.]

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 ZDD 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 [cuddZddSymmSiftingConv]

Definition at line 302 of file cuddZddSymm.c.

306 {
307  int i;
308  int *var;
309  int nvars;
310  int x;
311  int result;
312  int symvars;
313  int symgroups;
314  int iteration;
315 #ifdef DD_STATS
316  int previousSize;
317 #endif
318 
319  nvars = table->sizeZ;
320 
321  /* Find order in which to sift variables. */
322  var = NULL;
323  zdd_entry = ABC_ALLOC(int, nvars);
324  if (zdd_entry == NULL) {
325  table->errorCode = CUDD_MEMORY_OUT;
326  goto cuddZddSymmSiftingOutOfMem;
327  }
328  var = ABC_ALLOC(int, nvars);
329  if (var == NULL) {
330  table->errorCode = CUDD_MEMORY_OUT;
331  goto cuddZddSymmSiftingOutOfMem;
332  }
333 
334  for (i = 0; i < nvars; i++) {
335  x = table->permZ[i];
336  zdd_entry[i] = table->subtableZ[x].keys;
337  var[i] = i;
338  }
339 
340  qsort((void *)var, nvars, sizeof(int), (DD_QSFP)cuddZddUniqueCompare);
341 
342  /* Initialize the symmetry of each subtable to itself. */
343  for (i = lower; i <= upper; i++)
344  table->subtableZ[i].next = i;
345 
346  iteration = ddMin(table->siftMaxVar, nvars);
347  for (i = 0; i < iteration; i++) {
348  if (zddTotalNumberSwapping >= table->siftMaxSwap)
349  break;
350  x = table->permZ[var[i]];
351 #ifdef DD_STATS
352  previousSize = table->keysZ;
353 #endif
354  if (x < lower || x > upper) continue;
355  if (table->subtableZ[x].next == (unsigned) x) {
356  result = cuddZddSymmSiftingAux(table, x, lower, upper);
357  if (!result)
358  goto cuddZddSymmSiftingOutOfMem;
359 #ifdef DD_STATS
360  if (table->keysZ < (unsigned) previousSize) {
361  (void) fprintf(table->out,"-");
362  } else if (table->keysZ > (unsigned) previousSize) {
363  (void) fprintf(table->out,"+");
364 #ifdef DD_VERBOSE
365  (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ, var[i]);
366 #endif
367  } else {
368  (void) fprintf(table->out,"=");
369  }
370  fflush(table->out);
371 #endif
372  }
373  }
374 
375  ABC_FREE(var);
376  ABC_FREE(zdd_entry);
377 
378  cuddZddSymmSummary(table, lower, upper, &symvars, &symgroups);
379 
380 #ifdef DD_STATS
381  (void) fprintf(table->out,"\n#:S_SIFTING %8d: symmetric variables\n",symvars);
382  (void) fprintf(table->out,"#:G_SIFTING %8d: symmetric groups\n",symgroups);
383 #endif
384 
385  return(1+symvars);
386 
387 cuddZddSymmSiftingOutOfMem:
388 
389  if (zdd_entry != NULL)
390  ABC_FREE(zdd_entry);
391  if (var != NULL)
392  ABC_FREE(var);
393 
394  return(0);
395 
396 } /* end of cuddZddSymmSifting */
DdSubtable::keys
unsigned int keys
Definition: cuddInt.h:330
DdManager::siftMaxSwap
int siftMaxSwap
Definition: cuddInt.h:412
DD_QSFP
int(* DD_QSFP)(const void *, const void *)
Definition: cudd.h:326
Minisat::var
int var(Lit p)
Definition: SolverTypes.h:62
zdd_entry
int * zdd_entry
Definition: cuddZddReord.c:108
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
DdManager::permZ
int * permZ
Definition: cuddInt.h:387
zddTotalNumberSwapping
int zddTotalNumberSwapping
Definition: cuddZddReord.c:110
DdManager::out
FILE * out
Definition: cuddInt.h:441
ddMin
#define ddMin(x, y)
Definition: cuddInt.h:818
DdManager::siftMaxVar
int siftMaxVar
Definition: cuddInt.h:411
cuddZddSymmSummary
static void cuddZddSymmSummary(DdManager *table, int lower, int upper, int *symvars, int *symgroups)
Definition: cuddZddSymm.c:1671
DdManager::sizeZ
int sizeZ
Definition: cuddInt.h:362
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
DdSubtable::next
unsigned int next
Definition: cuddInt.h:333
result
static int result
Definition: cuddGenetic.c:125
DdManager::keysZ
unsigned int keysZ
Definition: cuddInt.h:370
cuddZddSymmSiftingAux
static int cuddZddSymmSiftingAux(DdManager *table, int x, int x_low, int x_high)
Definition: cuddZddSymm.c:601
cuddZddUniqueCompare
int cuddZddUniqueCompare(int *ptr_x, int *ptr_y)
Definition: cuddZddReord.c:459
DdManager::errorCode
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
DdManager::subtableZ
DdSubtable * subtableZ
Definition: cuddInt.h:366
static Move * cuddZddSymmSifting_down ( DdManager *  table,
int  x,
int  x_high,
int  initial_size 
)
static

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

Synopsis [Moves x down until either it reaches the bound (x_high) or the size of the ZDD heap increases too much.]

Description [Moves x down until either it reaches the bound (x_high) or the size of the ZDD 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; ZDD_MV_OOM if memory is full.]

SideEffects [None]

SeeAlso []

Definition at line 1338 of file cuddZddSymm.c.

1343 {
1344  Move *moves;
1345  Move *move;
1346  int y;
1347  int size;
1348  int limit_size = initial_size;
1349  int i, gxtop, gybot;
1350 
1351  moves = NULL;
1352  y = cuddZddNextHigh(table, x);
1353  while (y <= x_high) {
1354  gybot = table->subtableZ[y].next;
1355  while (table->subtableZ[gybot].next != (unsigned) y)
1356  gybot = table->subtableZ[gybot].next;
1357  if (cuddZddSymmCheck(table, x, y)) {
1358  /* Symmetry found, attach symm groups */
1359  gxtop = table->subtableZ[x].next;
1360  table->subtableZ[x].next = y;
1361  i = table->subtableZ[y].next;
1362  while (table->subtableZ[i].next != (unsigned) y)
1363  i = table->subtableZ[i].next;
1364  table->subtableZ[i].next = gxtop;
1365  }
1366  else if ((table->subtableZ[x].next == (unsigned) x) &&
1367  (table->subtableZ[y].next == (unsigned) y)) {
1368  /* x and y have self symmetry */
1369  size = cuddZddSwapInPlace(table, x, y);
1370  if (size == 0)
1371  goto cuddZddSymmSifting_downOutOfMem;
1372  move = (Move *)cuddDynamicAllocNode(table);
1373  if (move == NULL)
1374  goto cuddZddSymmSifting_downOutOfMem;
1375  move->x = x;
1376  move->y = y;
1377  move->size = size;
1378  move->next = moves;
1379  moves = move;
1380  if ((double)size >
1381  (double)limit_size * table->maxGrowth)
1382  return(moves);
1383  if (size < limit_size)
1384  limit_size = size;
1385  x = y;
1386  y = cuddZddNextHigh(table, x);
1387  }
1388  else { /* Group move */
1389  size = zdd_group_move(table, x, y, &moves);
1390  if ((double)size >
1391  (double)limit_size * table->maxGrowth)
1392  return(moves);
1393  if (size < limit_size)
1394  limit_size = size;
1395  }
1396  x = gybot;
1397  y = cuddZddNextHigh(table, x);
1398  }
1399 
1400  return(moves);
1401 
1402 cuddZddSymmSifting_downOutOfMem:
1403  while (moves != NULL) {
1404  move = moves->next;
1405  cuddDeallocMove(table, moves);
1406  moves = move;
1407  }
1408  return(ZDD_MV_OOM);
1409 
1410 } /* end of cuddZddSymmSifting_down */
cuddDeallocMove
#define cuddDeallocMove(unique, node)
Definition: cuddInt.h:564
Move
Definition: cuddInt.h:492
cuddZddSymmCheck
int cuddZddSymmCheck(DdManager *table, int x, int y)
Definition: cuddZddSymm.c:197
DdManager::maxGrowth
double maxGrowth
Definition: cuddInt.h:413
cuddZddSwapInPlace
int cuddZddSwapInPlace(DdManager *table, int x, int y)
Definition: cuddZddReord.c:484
Move::x
DdHalfWord x
Definition: cuddInt.h:493
zdd_group_move
static int zdd_group_move(DdManager *table, int x, int y, Move **moves)
Definition: cuddZddSymm.c:1481
size
static int size
Definition: cuddSign.c:86
cuddZddNextHigh
int cuddZddNextHigh(DdManager *table, int x)
Definition: cuddZddReord.c:413
cuddDynamicAllocNode
DdNode * cuddDynamicAllocNode(DdManager *table)
Definition: cuddReorder.c:406
Move::y
DdHalfWord y
Definition: cuddInt.h:494
DdSubtable::next
unsigned int next
Definition: cuddInt.h:333
Move::next
struct Move * next
Definition: cuddInt.h:497
ZDD_MV_OOM
#define ZDD_MV_OOM
Definition: cuddZddSymm.c:81
Move::size
int size
Definition: cuddInt.h:496
DdManager::subtableZ
DdSubtable * subtableZ
Definition: cuddInt.h:366
static Move * cuddZddSymmSifting_up ( DdManager *  table,
int  x,
int  x_low,
int  initial_size 
)
static

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

Synopsis [Moves x up until either it reaches the bound (x_low) or the size of the ZDD heap increases too much.]

Description [Moves x up until either it reaches the bound (x_low) or the size of the ZDD 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; ZDD_MV_OOM if memory is full.]

SideEffects [None]

SeeAlso []

Definition at line 1250 of file cuddZddSymm.c.

1255 {
1256  Move *moves;
1257  Move *move;
1258  int y;
1259  int size;
1260  int limit_size = initial_size;
1261  int i, gytop;
1262 
1263  moves = NULL;
1264  y = cuddZddNextLow(table, x);
1265  while (y >= x_low) {
1266  gytop = table->subtableZ[y].next;
1267  if (cuddZddSymmCheck(table, y, x)) {
1268  /* Symmetry found, attach symm groups */
1269  table->subtableZ[y].next = x;
1270  i = table->subtableZ[x].next;
1271  while (table->subtableZ[i].next != (unsigned) x)
1272  i = table->subtableZ[i].next;
1273  table->subtableZ[i].next = gytop;
1274  }
1275  else if ((table->subtableZ[x].next == (unsigned) x) &&
1276  (table->subtableZ[y].next == (unsigned) y)) {
1277  /* x and y have self symmetry */
1278  size = cuddZddSwapInPlace(table, y, x);
1279  if (size == 0)
1280  goto cuddZddSymmSifting_upOutOfMem;
1281  move = (Move *)cuddDynamicAllocNode(table);
1282  if (move == NULL)
1283  goto cuddZddSymmSifting_upOutOfMem;
1284  move->x = y;
1285  move->y = x;
1286  move->size = size;
1287  move->next = moves;
1288  moves = move;
1289  if ((double)size >
1290  (double)limit_size * table->maxGrowth)
1291  return(moves);
1292  if (size < limit_size)
1293  limit_size = size;
1294  }
1295  else { /* Group move */
1296  size = zdd_group_move(table, y, x, &moves);
1297  if ((double)size >
1298  (double)limit_size * table->maxGrowth)
1299  return(moves);
1300  if (size < limit_size)
1301  limit_size = size;
1302  }
1303  x = gytop;
1304  y = cuddZddNextLow(table, x);
1305  }
1306 
1307  return(moves);
1308 
1309 cuddZddSymmSifting_upOutOfMem:
1310  while (moves != NULL) {
1311  move = moves->next;
1312  cuddDeallocMove(table, moves);
1313  moves = move;
1314  }
1315  return(ZDD_MV_OOM);
1316 
1317 } /* end of cuddZddSymmSifting_up */
cuddDeallocMove
#define cuddDeallocMove(unique, node)
Definition: cuddInt.h:564
Move
Definition: cuddInt.h:492
cuddZddSymmCheck
int cuddZddSymmCheck(DdManager *table, int x, int y)
Definition: cuddZddSymm.c:197
DdManager::maxGrowth
double maxGrowth
Definition: cuddInt.h:413
cuddZddSwapInPlace
int cuddZddSwapInPlace(DdManager *table, int x, int y)
Definition: cuddZddReord.c:484
Move::x
DdHalfWord x
Definition: cuddInt.h:493
zdd_group_move
static int zdd_group_move(DdManager *table, int x, int y, Move **moves)
Definition: cuddZddSymm.c:1481
size
static int size
Definition: cuddSign.c:86
cuddDynamicAllocNode
DdNode * cuddDynamicAllocNode(DdManager *table)
Definition: cuddReorder.c:406
Move::y
DdHalfWord y
Definition: cuddInt.h:494
DdSubtable::next
unsigned int next
Definition: cuddInt.h:333
Move::next
struct Move * next
Definition: cuddInt.h:497
ZDD_MV_OOM
#define ZDD_MV_OOM
Definition: cuddZddSymm.c:81
cuddZddNextLow
int cuddZddNextLow(DdManager *table, int x)
Definition: cuddZddReord.c:435
Move::size
int size
Definition: cuddInt.h:496
DdManager::subtableZ
DdSubtable * subtableZ
Definition: cuddInt.h:366
static int cuddZddSymmSiftingAux ( DdManager *  table,
int  x,
int  x_low,
int  x_high 
)
static

AutomaticStart

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

Synopsis [Given x_low <= x <= x_high moves x up and down between the boundaries.]

Description [Given x_low <= x <= x_high 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]

SeeAlso []

Definition at line 601 of file cuddZddSymm.c.

606 {
607  Move *move;
608  Move *move_up; /* list of up move */
609  Move *move_down; /* list of down move */
610  int initial_size;
611  int result;
612  int i;
613  int topbot; /* index to either top or bottom of symmetry group */
614  int init_group_size, final_group_size;
615 
616  initial_size = table->keysZ;
617 
618  move_down = NULL;
619  move_up = NULL;
620 
621  /* Look for consecutive symmetries above x. */
622  for (i = x; i > x_low; i--) {
623  if (!cuddZddSymmCheck(table, i - 1, i))
624  break;
625  /* find top of i-1's symmetry */
626  topbot = table->subtableZ[i - 1].next;
627  table->subtableZ[i - 1].next = i;
628  table->subtableZ[x].next = topbot;
629  /* x is bottom of group so its symmetry is top of i-1's
630  group */
631  i = topbot + 1; /* add 1 for i--, new i is top of symm group */
632  }
633  /* Look for consecutive symmetries below x. */
634  for (i = x; i < x_high; i++) {
635  if (!cuddZddSymmCheck(table, i, i + 1))
636  break;
637  /* find bottom of i+1's symm group */
638  topbot = i + 1;
639  while ((unsigned) topbot < table->subtableZ[topbot].next)
640  topbot = table->subtableZ[topbot].next;
641 
642  table->subtableZ[topbot].next = table->subtableZ[i].next;
643  table->subtableZ[i].next = i + 1;
644  i = topbot - 1; /* add 1 for i++,
645  new i is bottom of symm group */
646  }
647 
648  /* Now x maybe in the middle of a symmetry group. */
649  if (x == x_low) { /* Sift down */
650  /* Find bottom of x's symm group */
651  while ((unsigned) x < table->subtableZ[x].next)
652  x = table->subtableZ[x].next;
653 
654  i = table->subtableZ[x].next;
655  init_group_size = x - i + 1;
656 
657  move_down = cuddZddSymmSifting_down(table, x, x_high,
658  initial_size);
659  /* after that point x --> x_high, unless early term */
660  if (move_down == ZDD_MV_OOM)
661  goto cuddZddSymmSiftingAuxOutOfMem;
662 
663  if (move_down == NULL ||
664  table->subtableZ[move_down->y].next != move_down->y) {
665  /* symmetry detected may have to make another complete
666  pass */
667  if (move_down != NULL)
668  x = move_down->y;
669  else
670  x = table->subtableZ[x].next;
671  i = x;
672  while ((unsigned) i < table->subtableZ[i].next) {
673  i = table->subtableZ[i].next;
674  }
675  final_group_size = i - x + 1;
676 
677  if (init_group_size == final_group_size) {
678  /* No new symmetry groups detected,
679  return to best position */
680  result = cuddZddSymmSiftingBackward(table,
681  move_down, initial_size);
682  }
683  else {
684  initial_size = table->keysZ;
685  move_up = cuddZddSymmSifting_up(table, x, x_low,
686  initial_size);
687  result = cuddZddSymmSiftingBackward(table, move_up,
688  initial_size);
689  }
690  }
691  else {
692  result = cuddZddSymmSiftingBackward(table, move_down,
693  initial_size);
694  /* move backward and stop at best position */
695  }
696  if (!result)
697  goto cuddZddSymmSiftingAuxOutOfMem;
698  }
699  else if (x == x_high) { /* Sift up */
700  /* Find top of x's symm group */
701  while ((unsigned) x < table->subtableZ[x].next)
702  x = table->subtableZ[x].next;
703  x = table->subtableZ[x].next;
704 
705  i = x;
706  while ((unsigned) i < table->subtableZ[i].next) {
707  i = table->subtableZ[i].next;
708  }
709  init_group_size = i - x + 1;
710 
711  move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size);
712  /* after that point x --> x_low, unless early term */
713  if (move_up == ZDD_MV_OOM)
714  goto cuddZddSymmSiftingAuxOutOfMem;
715 
716  if (move_up == NULL ||
717  table->subtableZ[move_up->x].next != move_up->x) {
718  /* symmetry detected may have to make another complete
719  pass */
720  if (move_up != NULL)
721  x = move_up->x;
722  else {
723  while ((unsigned) x < table->subtableZ[x].next)
724  x = table->subtableZ[x].next;
725  }
726  i = table->subtableZ[x].next;
727  final_group_size = x - i + 1;
728 
729  if (init_group_size == final_group_size) {
730  /* No new symmetry groups detected,
731  return to best position */
732  result = cuddZddSymmSiftingBackward(table, move_up,
733  initial_size);
734  }
735  else {
736  initial_size = table->keysZ;
737  move_down = cuddZddSymmSifting_down(table, x, x_high,
738  initial_size);
739  result = cuddZddSymmSiftingBackward(table, move_down,
740  initial_size);
741  }
742  }
743  else {
744  result = cuddZddSymmSiftingBackward(table, move_up,
745  initial_size);
746  /* move backward and stop at best position */
747  }
748  if (!result)
749  goto cuddZddSymmSiftingAuxOutOfMem;
750  }
751  else if ((x - x_low) > (x_high - x)) { /* must go down first:
752  shorter */
753  /* Find bottom of x's symm group */
754  while ((unsigned) x < table->subtableZ[x].next)
755  x = table->subtableZ[x].next;
756 
757  move_down = cuddZddSymmSifting_down(table, x, x_high,
758  initial_size);
759  /* after that point x --> x_high, unless early term */
760  if (move_down == ZDD_MV_OOM)
761  goto cuddZddSymmSiftingAuxOutOfMem;
762 
763  if (move_down != NULL) {
764  x = move_down->y;
765  }
766  else {
767  x = table->subtableZ[x].next;
768  }
769  i = x;
770  while ((unsigned) i < table->subtableZ[i].next) {
771  i = table->subtableZ[i].next;
772  }
773  init_group_size = i - x + 1;
774 
775  move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size);
776  if (move_up == ZDD_MV_OOM)
777  goto cuddZddSymmSiftingAuxOutOfMem;
778 
779  if (move_up == NULL ||
780  table->subtableZ[move_up->x].next != move_up->x) {
781  /* symmetry detected may have to make another complete
782  pass */
783  if (move_up != NULL) {
784  x = move_up->x;
785  }
786  else {
787  while ((unsigned) x < table->subtableZ[x].next)
788  x = table->subtableZ[x].next;
789  }
790  i = table->subtableZ[x].next;
791  final_group_size = x - i + 1;
792 
793  if (init_group_size == final_group_size) {
794  /* No new symmetry groups detected,
795  return to best position */
796  result = cuddZddSymmSiftingBackward(table, move_up,
797  initial_size);
798  }
799  else {
800  while (move_down != NULL) {
801  move = move_down->next;
802  cuddDeallocMove(table, move_down);
803  move_down = move;
804  }
805  initial_size = table->keysZ;
806  move_down = cuddZddSymmSifting_down(table, x, x_high,
807  initial_size);
808  result = cuddZddSymmSiftingBackward(table, move_down,
809  initial_size);
810  }
811  }
812  else {
813  result = cuddZddSymmSiftingBackward(table, move_up,
814  initial_size);
815  /* move backward and stop at best position */
816  }
817  if (!result)
818  goto cuddZddSymmSiftingAuxOutOfMem;
819  }
820  else { /* moving up first:shorter */
821  /* Find top of x's symmetry group */
822  while ((unsigned) x < table->subtableZ[x].next)
823  x = table->subtableZ[x].next;
824  x = table->subtableZ[x].next;
825 
826  move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size);
827  /* after that point x --> x_high, unless early term */
828  if (move_up == ZDD_MV_OOM)
829  goto cuddZddSymmSiftingAuxOutOfMem;
830 
831  if (move_up != NULL) {
832  x = move_up->x;
833  }
834  else {
835  while ((unsigned) x < table->subtableZ[x].next)
836  x = table->subtableZ[x].next;
837  }
838  i = table->subtableZ[x].next;
839  init_group_size = x - i + 1;
840 
841  move_down = cuddZddSymmSifting_down(table, x, x_high,
842  initial_size);
843  if (move_down == ZDD_MV_OOM)
844  goto cuddZddSymmSiftingAuxOutOfMem;
845 
846  if (move_down == NULL ||
847  table->subtableZ[move_down->y].next != move_down->y) {
848  /* symmetry detected may have to make another complete
849  pass */
850  if (move_down != NULL) {
851  x = move_down->y;
852  }
853  else {
854  x = table->subtableZ[x].next;
855  }
856  i = x;
857  while ((unsigned) i < table->subtableZ[i].next) {
858  i = table->subtableZ[i].next;
859  }
860  final_group_size = i - x + 1;
861 
862  if (init_group_size == final_group_size) {
863  /* No new symmetries detected,
864  go back to best position */
865  result = cuddZddSymmSiftingBackward(table, move_down,
866  initial_size);
867  }
868  else {
869  while (move_up != NULL) {
870  move = move_up->next;
871  cuddDeallocMove(table, move_up);
872  move_up = move;
873  }
874  initial_size = table->keysZ;
875  move_up = cuddZddSymmSifting_up(table, x, x_low,
876  initial_size);
877  result = cuddZddSymmSiftingBackward(table, move_up,
878  initial_size);
879  }
880  }
881  else {
882  result = cuddZddSymmSiftingBackward(table, move_down,
883  initial_size);
884  /* move backward and stop at best position */
885  }
886  if (!result)
887  goto cuddZddSymmSiftingAuxOutOfMem;
888  }
889 
890  while (move_down != NULL) {
891  move = move_down->next;
892  cuddDeallocMove(table, move_down);
893  move_down = move;
894  }
895  while (move_up != NULL) {
896  move = move_up->next;
897  cuddDeallocMove(table, move_up);
898  move_up = move;
899  }
900 
901  return(1);
902 
903 cuddZddSymmSiftingAuxOutOfMem:
904  if (move_down != ZDD_MV_OOM) {
905  while (move_down != NULL) {
906  move = move_down->next;
907  cuddDeallocMove(table, move_down);
908  move_down = move;
909  }
910  }
911  if (move_up != ZDD_MV_OOM) {
912  while (move_up != NULL) {
913  move = move_up->next;
914  cuddDeallocMove(table, move_up);
915  move_up = move;
916  }
917  }
918 
919  return(0);
920 
921 } /* end of cuddZddSymmSiftingAux */
cuddDeallocMove
#define cuddDeallocMove(unique, node)
Definition: cuddInt.h:564
Move
Definition: cuddInt.h:492
cuddZddSymmCheck
int cuddZddSymmCheck(DdManager *table, int x, int y)
Definition: cuddZddSymm.c:197
cuddZddSymmSifting_down
static Move * cuddZddSymmSifting_down(DdManager *table, int x, int x_high, int initial_size)
Definition: cuddZddSymm.c:1338
cuddZddSymmSiftingBackward
static int cuddZddSymmSiftingBackward(DdManager *table, Move *moves, int size)
Definition: cuddZddSymm.c:1429
Move::x
DdHalfWord x
Definition: cuddInt.h:493
Move::y
DdHalfWord y
Definition: cuddInt.h:494
DdSubtable::next
unsigned int next
Definition: cuddInt.h:333
Move::next
struct Move * next
Definition: cuddInt.h:497
ZDD_MV_OOM
#define ZDD_MV_OOM
Definition: cuddZddSymm.c:81
result
static int result
Definition: cuddGenetic.c:125
cuddZddSymmSifting_up
static Move * cuddZddSymmSifting_up(DdManager *table, int x, int x_low, int initial_size)
Definition: cuddZddSymm.c:1250
DdManager::keysZ
unsigned int keysZ
Definition: cuddInt.h:370
DdManager::subtableZ
DdSubtable * subtableZ
Definition: cuddInt.h:366
static int cuddZddSymmSiftingBackward ( DdManager *  table,
Move *  moves,
int  size 
)
static

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

Synopsis [Given a set of moves, returns the ZDD heap to the position giving the minimum size.]

Description [Given a set of moves, returns the ZDD 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]

SeeAlso []

Definition at line 1429 of file cuddZddSymm.c.

1433 {
1434  int i;
1435  int i_best;
1436  Move *move;
1437  int res = -1;
1438 
1439  i_best = -1;
1440  for (move = moves, i = 0; move != NULL; move = move->next, i++) {
1441  if (move->size < size) {
1442  i_best = i;
1443  size = move->size;
1444  }
1445  }
1446 
1447  for (move = moves, i = 0; move != NULL; move = move->next, i++) {
1448  if (i == i_best) break;
1449  if ((table->subtableZ[move->x].next == move->x) &&
1450  (table->subtableZ[move->y].next == move->y)) {
1451  res = cuddZddSwapInPlace(table, move->x, move->y);
1452  if (!res) return(0);
1453  }
1454  else { /* Group move necessary */
1455  res = zdd_group_move_backward(table, move->x, move->y);
1456  }
1457  if (i_best == -1 && res == size)
1458  break;
1459  }
1460 
1461  return(1);
1462 
1463 } /* end of cuddZddSymmSiftingBackward */
Move
Definition: cuddInt.h:492
cuddZddSwapInPlace
int cuddZddSwapInPlace(DdManager *table, int x, int y)
Definition: cuddZddReord.c:484
Move::x
DdHalfWord x
Definition: cuddInt.h:493
size
static int size
Definition: cuddSign.c:86
Move::y
DdHalfWord y
Definition: cuddInt.h:494
DdSubtable::next
unsigned int next
Definition: cuddInt.h:333
Move::next
struct Move * next
Definition: cuddInt.h:497
Move::size
int size
Definition: cuddInt.h:496
zdd_group_move_backward
static int zdd_group_move_backward(DdManager *table, int x, int y)
Definition: cuddZddSymm.c:1588
DdManager::subtableZ
DdSubtable * subtableZ
Definition: cuddInt.h:366
int cuddZddSymmSiftingConv ( DdManager *  table,
int  lower,
int  upper 
)

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

Synopsis [Symmetric sifting to convergence algorithm for ZDDs.]

Description [Symmetric sifting to convergence algorithm for ZDDs. 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 ZDD 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 [cuddZddSymmSifting]

Definition at line 423 of file cuddZddSymm.c.

427 {
428  int i;
429  int *var;
430  int nvars;
431  int initialSize;
432  int x;
433  int result;
434  int symvars;
435  int symgroups;
436  int classes;
437  int iteration;
438 #ifdef DD_STATS
439  int previousSize;
440 #endif
441 
442  initialSize = table->keysZ;
443 
444  nvars = table->sizeZ;
445 
446  /* Find order in which to sift variables. */
447  var = NULL;
448  zdd_entry = ABC_ALLOC(int, nvars);
449  if (zdd_entry == NULL) {
450  table->errorCode = CUDD_MEMORY_OUT;
451  goto cuddZddSymmSiftingConvOutOfMem;
452  }
453  var = ABC_ALLOC(int, nvars);
454  if (var == NULL) {
455  table->errorCode = CUDD_MEMORY_OUT;
456  goto cuddZddSymmSiftingConvOutOfMem;
457  }
458 
459  for (i = 0; i < nvars; i++) {
460  x = table->permZ[i];
461  zdd_entry[i] = table->subtableZ[x].keys;
462  var[i] = i;
463  }
464 
465  qsort((void *)var, nvars, sizeof(int), (DD_QSFP)cuddZddUniqueCompare);
466 
467  /* Initialize the symmetry of each subtable to itself
468  ** for first pass of converging symmetric sifting.
469  */
470  for (i = lower; i <= upper; i++)
471  table->subtableZ[i].next = i;
472 
473  iteration = ddMin(table->siftMaxVar, table->sizeZ);
474  for (i = 0; i < iteration; i++) {
475  if (zddTotalNumberSwapping >= table->siftMaxSwap)
476  break;
477  x = table->permZ[var[i]];
478  if (x < lower || x > upper) continue;
479  /* Only sift if not in symmetry group already. */
480  if (table->subtableZ[x].next == (unsigned) x) {
481 #ifdef DD_STATS
482  previousSize = table->keysZ;
483 #endif
484  result = cuddZddSymmSiftingAux(table, x, lower, upper);
485  if (!result)
486  goto cuddZddSymmSiftingConvOutOfMem;
487 #ifdef DD_STATS
488  if (table->keysZ < (unsigned) previousSize) {
489  (void) fprintf(table->out,"-");
490  } else if (table->keysZ > (unsigned) previousSize) {
491  (void) fprintf(table->out,"+");
492 #ifdef DD_VERBOSE
493  (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ, var[i]);
494 #endif
495  } else {
496  (void) fprintf(table->out,"=");
497  }
498  fflush(table->out);
499 #endif
500  }
501  }
502 
503  /* Sifting now until convergence. */
504  while ((unsigned) initialSize > table->keysZ) {
505  initialSize = table->keysZ;
506 #ifdef DD_STATS
507  (void) fprintf(table->out,"\n");
508 #endif
509  /* Here we consider only one representative for each symmetry class. */
510  for (x = lower, classes = 0; x <= upper; x++, classes++) {
511  while ((unsigned) x < table->subtableZ[x].next)
512  x = table->subtableZ[x].next;
513  /* Here x is the largest index in a group.
514  ** Groups consists of adjacent variables.
515  ** Hence, the next increment of x will move it to a new group.
516  */
517  i = table->invpermZ[x];
518  zdd_entry[i] = table->subtableZ[x].keys;
519  var[classes] = i;
520  }
521 
522  qsort((void *)var,classes,sizeof(int),(DD_QSFP)cuddZddUniqueCompare);
523 
524  /* Now sift. */
525  iteration = ddMin(table->siftMaxVar, nvars);
526  for (i = 0; i < iteration; i++) {
527  if (zddTotalNumberSwapping >= table->siftMaxSwap)
528  break;
529  x = table->permZ[var[i]];
530  if ((unsigned) x >= table->subtableZ[x].next) {
531 #ifdef DD_STATS
532  previousSize = table->keysZ;
533 #endif
534  result = cuddZddSymmSiftingConvAux(table, x, lower, upper);
535  if (!result)
536  goto cuddZddSymmSiftingConvOutOfMem;
537 #ifdef DD_STATS
538  if (table->keysZ < (unsigned) previousSize) {
539  (void) fprintf(table->out,"-");
540  } else if (table->keysZ > (unsigned) previousSize) {
541  (void) fprintf(table->out,"+");
542 #ifdef DD_VERBOSE
543  (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ, var[i]);
544 #endif
545  } else {
546  (void) fprintf(table->out,"=");
547  }
548  fflush(table->out);
549 #endif
550  }
551  } /* for */
552  }
553 
554  cuddZddSymmSummary(table, lower, upper, &symvars, &symgroups);
555 
556 #ifdef DD_STATS
557  (void) fprintf(table->out,"\n#:S_SIFTING %8d: symmetric variables\n",
558  symvars);
559  (void) fprintf(table->out,"#:G_SIFTING %8d: symmetric groups\n",
560  symgroups);
561 #endif
562 
563  ABC_FREE(var);
564  ABC_FREE(zdd_entry);
565 
566  return(1+symvars);
567 
568 cuddZddSymmSiftingConvOutOfMem:
569 
570  if (zdd_entry != NULL)
571  ABC_FREE(zdd_entry);
572  if (var != NULL)
573  ABC_FREE(var);
574 
575  return(0);
576 
577 } /* end of cuddZddSymmSiftingConv */
DdSubtable::keys
unsigned int keys
Definition: cuddInt.h:330
DdManager::siftMaxSwap
int siftMaxSwap
Definition: cuddInt.h:412
DdManager::invpermZ
int * invpermZ
Definition: cuddInt.h:389
DD_QSFP
int(* DD_QSFP)(const void *, const void *)
Definition: cudd.h:326
Minisat::var
int var(Lit p)
Definition: SolverTypes.h:62
zdd_entry
int * zdd_entry
Definition: cuddZddReord.c:108
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
DdManager::permZ
int * permZ
Definition: cuddInt.h:387
zddTotalNumberSwapping
int zddTotalNumberSwapping
Definition: cuddZddReord.c:110
DdManager::out
FILE * out
Definition: cuddInt.h:441
ddMin
#define ddMin(x, y)
Definition: cuddInt.h:818
DdManager::siftMaxVar
int siftMaxVar
Definition: cuddInt.h:411
cuddZddSymmSummary
static void cuddZddSymmSummary(DdManager *table, int lower, int upper, int *symvars, int *symgroups)
Definition: cuddZddSymm.c:1671
DdManager::sizeZ
int sizeZ
Definition: cuddInt.h:362
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
DdSubtable::next
unsigned int next
Definition: cuddInt.h:333
result
static int result
Definition: cuddGenetic.c:125
DdManager::keysZ
unsigned int keysZ
Definition: cuddInt.h:370
cuddZddSymmSiftingAux
static int cuddZddSymmSiftingAux(DdManager *table, int x, int x_low, int x_high)
Definition: cuddZddSymm.c:601
cuddZddSymmSiftingConvAux
static int cuddZddSymmSiftingConvAux(DdManager *table, int x, int x_low, int x_high)
Definition: cuddZddSymm.c:941
cuddZddUniqueCompare
int cuddZddUniqueCompare(int *ptr_x, int *ptr_y)
Definition: cuddZddReord.c:459
DdManager::errorCode
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
DdManager::subtableZ
DdSubtable * subtableZ
Definition: cuddInt.h:366
static int cuddZddSymmSiftingConvAux ( DdManager *  table,
int  x,
int  x_low,
int  x_high 
)
static

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

Synopsis [Given x_low <= x <= x_high moves x up and down between the boundaries.]

Description [Given x_low <= x <= x_high 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]

SeeAlso []

Definition at line 941 of file cuddZddSymm.c.

946 {
947  Move *move;
948  Move *move_up; /* list of up move */
949  Move *move_down; /* list of down move */
950  int initial_size;
951  int result;
952  int i;
953  int init_group_size, final_group_size;
954 
955  initial_size = table->keysZ;
956 
957  move_down = NULL;
958  move_up = NULL;
959 
960  if (x == x_low) { /* Sift down */
961  i = table->subtableZ[x].next;
962  init_group_size = x - i + 1;
963 
964  move_down = cuddZddSymmSifting_down(table, x, x_high,
965  initial_size);
966  /* after that point x --> x_high, unless early term */
967  if (move_down == ZDD_MV_OOM)
968  goto cuddZddSymmSiftingConvAuxOutOfMem;
969 
970  if (move_down == NULL ||
971  table->subtableZ[move_down->y].next != move_down->y) {
972  /* symmetry detected may have to make another complete
973  pass */
974  if (move_down != NULL)
975  x = move_down->y;
976  else {
977  while ((unsigned) x < table->subtableZ[x].next)
978  x = table->subtableZ[x].next;
979  x = table->subtableZ[x].next;
980  }
981  i = x;
982  while ((unsigned) i < table->subtableZ[i].next) {
983  i = table->subtableZ[i].next;
984  }
985  final_group_size = i - x + 1;
986 
987  if (init_group_size == final_group_size) {
988  /* No new symmetries detected,
989  go back to best position */
990  result = cuddZddSymmSiftingBackward(table, move_down,
991  initial_size);
992  }
993  else {
994  initial_size = table->keysZ;
995  move_up = cuddZddSymmSifting_up(table, x, x_low,
996  initial_size);
997  result = cuddZddSymmSiftingBackward(table, move_up,
998  initial_size);
999  }
1000  }
1001  else {
1002  result = cuddZddSymmSiftingBackward(table, move_down,
1003  initial_size);
1004  /* move backward and stop at best position */
1005  }
1006  if (!result)
1007  goto cuddZddSymmSiftingConvAuxOutOfMem;
1008  }
1009  else if (x == x_high) { /* Sift up */
1010  /* Find top of x's symm group */
1011  while ((unsigned) x < table->subtableZ[x].next)
1012  x = table->subtableZ[x].next;
1013  x = table->subtableZ[x].next;
1014 
1015  i = x;
1016  while ((unsigned) i < table->subtableZ[i].next) {
1017  i = table->subtableZ[i].next;
1018  }
1019  init_group_size = i - x + 1;
1020 
1021  move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size);
1022  /* after that point x --> x_low, unless early term */
1023  if (move_up == ZDD_MV_OOM)
1024  goto cuddZddSymmSiftingConvAuxOutOfMem;
1025 
1026  if (move_up == NULL ||
1027  table->subtableZ[move_up->x].next != move_up->x) {
1028  /* symmetry detected may have to make another complete
1029  pass */
1030  if (move_up != NULL)
1031  x = move_up->x;
1032  else {
1033  while ((unsigned) x < table->subtableZ[x].next)
1034  x = table->subtableZ[x].next;
1035  }
1036  i = table->subtableZ[x].next;
1037  final_group_size = x - i + 1;
1038 
1039  if (init_group_size == final_group_size) {
1040  /* No new symmetry groups detected,
1041  return to best position */
1042  result = cuddZddSymmSiftingBackward(table, move_up,
1043  initial_size);
1044  }
1045  else {
1046  initial_size = table->keysZ;
1047  move_down = cuddZddSymmSifting_down(table, x, x_high,
1048  initial_size);
1049  result = cuddZddSymmSiftingBackward(table, move_down,
1050  initial_size);
1051  }
1052  }
1053  else {
1054  result = cuddZddSymmSiftingBackward(table, move_up,
1055  initial_size);
1056  /* move backward and stop at best position */
1057  }
1058  if (!result)
1059  goto cuddZddSymmSiftingConvAuxOutOfMem;
1060  }
1061  else if ((x - x_low) > (x_high - x)) { /* must go down first:
1062  shorter */
1063  move_down = cuddZddSymmSifting_down(table, x, x_high,
1064  initial_size);
1065  /* after that point x --> x_high */
1066  if (move_down == ZDD_MV_OOM)
1067  goto cuddZddSymmSiftingConvAuxOutOfMem;
1068 
1069  if (move_down != NULL) {
1070  x = move_down->y;
1071  }
1072  else {
1073  while ((unsigned) x < table->subtableZ[x].next)
1074  x = table->subtableZ[x].next;
1075  x = table->subtableZ[x].next;
1076  }
1077  i = x;
1078  while ((unsigned) i < table->subtableZ[i].next) {
1079  i = table->subtableZ[i].next;
1080  }
1081  init_group_size = i - x + 1;
1082 
1083  move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size);
1084  if (move_up == ZDD_MV_OOM)
1085  goto cuddZddSymmSiftingConvAuxOutOfMem;
1086 
1087  if (move_up == NULL ||
1088  table->subtableZ[move_up->x].next != move_up->x) {
1089  /* symmetry detected may have to make another complete
1090  pass */
1091  if (move_up != NULL) {
1092  x = move_up->x;
1093  }
1094  else {
1095  while ((unsigned) x < table->subtableZ[x].next)
1096  x = table->subtableZ[x].next;
1097  }
1098  i = table->subtableZ[x].next;
1099  final_group_size = x - i + 1;
1100 
1101  if (init_group_size == final_group_size) {
1102  /* No new symmetry groups detected,
1103  return to best position */
1104  result = cuddZddSymmSiftingBackward(table, move_up,
1105  initial_size);
1106  }
1107  else {
1108  while (move_down != NULL) {
1109  move = move_down->next;
1110  cuddDeallocMove(table, move_down);
1111  move_down = move;
1112  }
1113  initial_size = table->keysZ;
1114  move_down = cuddZddSymmSifting_down(table, x, x_high,
1115  initial_size);
1116  result = cuddZddSymmSiftingBackward(table, move_down,
1117  initial_size);
1118  }
1119  }
1120  else {
1121  result = cuddZddSymmSiftingBackward(table, move_up,
1122  initial_size);
1123  /* move backward and stop at best position */
1124  }
1125  if (!result)
1126  goto cuddZddSymmSiftingConvAuxOutOfMem;
1127  }
1128  else { /* moving up first:shorter */
1129  /* Find top of x's symmetry group */
1130  x = table->subtableZ[x].next;
1131 
1132  move_up = cuddZddSymmSifting_up(table, x, x_low, initial_size);
1133  /* after that point x --> x_high, unless early term */
1134  if (move_up == ZDD_MV_OOM)
1135  goto cuddZddSymmSiftingConvAuxOutOfMem;
1136 
1137  if (move_up != NULL) {
1138  x = move_up->x;
1139  }
1140  else {
1141  while ((unsigned) x < table->subtableZ[x].next)
1142  x = table->subtableZ[x].next;
1143  }
1144  i = table->subtableZ[x].next;
1145  init_group_size = x - i + 1;
1146 
1147  move_down = cuddZddSymmSifting_down(table, x, x_high,
1148  initial_size);
1149  if (move_down == ZDD_MV_OOM)
1150  goto cuddZddSymmSiftingConvAuxOutOfMem;
1151 
1152  if (move_down == NULL ||
1153  table->subtableZ[move_down->y].next != move_down->y) {
1154  /* symmetry detected may have to make another complete
1155  pass */
1156  if (move_down != NULL) {
1157  x = move_down->y;
1158  }
1159  else {
1160  while ((unsigned) x < table->subtableZ[x].next)
1161  x = table->subtableZ[x].next;
1162  x = table->subtableZ[x].next;
1163  }
1164  i = x;
1165  while ((unsigned) i < table->subtableZ[i].next) {
1166  i = table->subtableZ[i].next;
1167  }
1168  final_group_size = i - x + 1;
1169 
1170  if (init_group_size == final_group_size) {
1171  /* No new symmetries detected,
1172  go back to best position */
1173  result = cuddZddSymmSiftingBackward(table, move_down,
1174  initial_size);
1175  }
1176  else {
1177  while (move_up != NULL) {
1178  move = move_up->next;
1179  cuddDeallocMove(table, move_up);
1180  move_up = move;
1181  }
1182  initial_size = table->keysZ;
1183  move_up = cuddZddSymmSifting_up(table, x, x_low,
1184  initial_size);
1185  result = cuddZddSymmSiftingBackward(table, move_up,
1186  initial_size);
1187  }
1188  }
1189  else {
1190  result = cuddZddSymmSiftingBackward(table, move_down,
1191  initial_size);
1192  /* move backward and stop at best position */
1193  }
1194  if (!result)
1195  goto cuddZddSymmSiftingConvAuxOutOfMem;
1196  }
1197 
1198  while (move_down != NULL) {
1199  move = move_down->next;
1200  cuddDeallocMove(table, move_down);
1201  move_down = move;
1202  }
1203  while (move_up != NULL) {
1204  move = move_up->next;
1205  cuddDeallocMove(table, move_up);
1206  move_up = move;
1207  }
1208 
1209  return(1);
1210 
1211 cuddZddSymmSiftingConvAuxOutOfMem:
1212  if (move_down != ZDD_MV_OOM) {
1213  while (move_down != NULL) {
1214  move = move_down->next;
1215  cuddDeallocMove(table, move_down);
1216  move_down = move;
1217  }
1218  }
1219  if (move_up != ZDD_MV_OOM) {
1220  while (move_up != NULL) {
1221  move = move_up->next;
1222  cuddDeallocMove(table, move_up);
1223  move_up = move;
1224  }
1225  }
1226 
1227  return(0);
1228 
1229 } /* end of cuddZddSymmSiftingConvAux */
cuddDeallocMove
#define cuddDeallocMove(unique, node)
Definition: cuddInt.h:564
Move
Definition: cuddInt.h:492
cuddZddSymmSifting_down
static Move * cuddZddSymmSifting_down(DdManager *table, int x, int x_high, int initial_size)
Definition: cuddZddSymm.c:1338
cuddZddSymmSiftingBackward
static int cuddZddSymmSiftingBackward(DdManager *table, Move *moves, int size)
Definition: cuddZddSymm.c:1429
Move::x
DdHalfWord x
Definition: cuddInt.h:493
Move::y
DdHalfWord y
Definition: cuddInt.h:494
DdSubtable::next
unsigned int next
Definition: cuddInt.h:333
Move::next
struct Move * next
Definition: cuddInt.h:497
ZDD_MV_OOM
#define ZDD_MV_OOM
Definition: cuddZddSymm.c:81
result
static int result
Definition: cuddGenetic.c:125
cuddZddSymmSifting_up
static Move * cuddZddSymmSifting_up(DdManager *table, int x, int x_low, int initial_size)
Definition: cuddZddSymm.c:1250
DdManager::keysZ
unsigned int keysZ
Definition: cuddInt.h:370
DdManager::subtableZ
DdSubtable * subtableZ
Definition: cuddInt.h:366
static void cuddZddSymmSummary ( 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 cuddZddSymm.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->subtableZ[i].next != (unsigned) i) {
1684  TotalSymmGroups++;
1685  x = i;
1686  do {
1687  TotalSymm++;
1688  gbot = x;
1689  x = table->subtableZ[x].next;
1690  } while (x != i);
1691 #ifdef DD_DEBUG
1692  assert(table->subtableZ[gbot].next == (unsigned) i);
1693 #endif
1694  i = gbot;
1695  }
1696  }
1697  *symvars = TotalSymm;
1698  *symgroups = TotalSymmGroups;
1699 
1700  return;
1701 
1702 } /* end of cuddZddSymmSummary */
DdSubtable::next
unsigned int next
Definition: cuddInt.h:333
assert
#define assert(ex)
Definition: util_old.h:213
DdManager::subtableZ
DdSubtable * subtableZ
Definition: cuddInt.h:366
static int zdd_group_move ( 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]

SeeAlso []

Definition at line 1481 of file cuddZddSymm.c.

1486 {
1487  Move *move;
1488  int size;
1489  int i, temp, gxtop, gxbot, gybot, yprev;
1490  int swapx = -1, swapy = -1;
1491 
1492 #ifdef DD_DEBUG
1493  assert(x < y); /* we assume that x < y */
1494 #endif
1495  /* Find top and bottom for the two groups. */
1496  gxtop = table->subtableZ[x].next;
1497  gxbot = x;
1498  gybot = table->subtableZ[y].next;
1499  while (table->subtableZ[gybot].next != (unsigned) y)
1500  gybot = table->subtableZ[gybot].next;
1501  yprev = gybot;
1502 
1503  while (x <= y) {
1504  while (y > gxtop) {
1505  /* Set correct symmetries. */
1506  temp = table->subtableZ[x].next;
1507  if (temp == x)
1508  temp = y;
1509  i = gxtop;
1510  for (;;) {
1511  if (table->subtableZ[i].next == (unsigned) x) {
1512  table->subtableZ[i].next = y;
1513  break;
1514  } else {
1515  i = table->subtableZ[i].next;
1516  }
1517  }
1518  if (table->subtableZ[y].next != (unsigned) y) {
1519  table->subtableZ[x].next = table->subtableZ[y].next;
1520  } else {
1521  table->subtableZ[x].next = x;
1522  }
1523 
1524  if (yprev != y) {
1525  table->subtableZ[yprev].next = x;
1526  } else {
1527  yprev = x;
1528  }
1529  table->subtableZ[y].next = temp;
1530 
1531  size = cuddZddSwapInPlace(table, x, y);
1532  if (size == 0)
1533  goto zdd_group_moveOutOfMem;
1534  swapx = x;
1535  swapy = y;
1536  y = x;
1537  x--;
1538  } /* while y > gxtop */
1539 
1540  /* Trying to find the next y. */
1541  if (table->subtableZ[y].next <= (unsigned) y) {
1542  gybot = y;
1543  } else {
1544  y = table->subtableZ[y].next;
1545  }
1546 
1547  yprev = gxtop;
1548  gxtop++;
1549  gxbot++;
1550  x = gxbot;
1551  } /* while x <= y, end of group movement */
1552  move = (Move *)cuddDynamicAllocNode(table);
1553  if (move == NULL)
1554  goto zdd_group_moveOutOfMem;
1555  move->x = swapx;
1556  move->y = swapy;
1557  move->size = table->keysZ;
1558  move->next = *moves;
1559  *moves = move;
1560 
1561  return(table->keysZ);
1562 
1563 zdd_group_moveOutOfMem:
1564  while (*moves != NULL) {
1565  move = (*moves)->next;
1566  cuddDeallocMove(table, *moves);
1567  *moves = move;
1568  }
1569  return(0);
1570 
1571 } /* end of zdd_group_move */
cuddDeallocMove
#define cuddDeallocMove(unique, node)
Definition: cuddInt.h:564
Move
Definition: cuddInt.h:492
cuddZddSwapInPlace
int cuddZddSwapInPlace(DdManager *table, int x, int y)
Definition: cuddZddReord.c:484
Move::x
DdHalfWord x
Definition: cuddInt.h:493
size
static int size
Definition: cuddSign.c:86
cuddDynamicAllocNode
DdNode * cuddDynamicAllocNode(DdManager *table)
Definition: cuddReorder.c:406
Move::y
DdHalfWord y
Definition: cuddInt.h:494
DdSubtable::next
unsigned int next
Definition: cuddInt.h:333
Move::next
struct Move * next
Definition: cuddInt.h:497
assert
#define assert(ex)
Definition: util_old.h:213
DdManager::keysZ
unsigned int keysZ
Definition: cuddInt.h:370
Move::size
int size
Definition: cuddInt.h:496
DdManager::subtableZ
DdSubtable * subtableZ
Definition: cuddInt.h:366
static int zdd_group_move_backward ( 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 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 1588 of file cuddZddSymm.c.

1592 {
1593  int size = -1;
1594  int i, temp, gxtop, gxbot, gybot, yprev;
1595 
1596 #ifdef DD_DEBUG
1597  assert(x < y); /* we assume that x < y */
1598 #endif
1599  /* Find top and bottom of the two groups. */
1600  gxtop = table->subtableZ[x].next;
1601  gxbot = x;
1602  gybot = table->subtableZ[y].next;
1603  while (table->subtableZ[gybot].next != (unsigned) y)
1604  gybot = table->subtableZ[gybot].next;
1605  yprev = gybot;
1606 
1607  while (x <= y) {
1608  while (y > gxtop) {
1609  /* Set correct symmetries. */
1610  temp = table->subtableZ[x].next;
1611  if (temp == x)
1612  temp = y;
1613  i = gxtop;
1614  for (;;) {
1615  if (table->subtableZ[i].next == (unsigned) x) {
1616  table->subtableZ[i].next = y;
1617  break;
1618  } else {
1619  i = table->subtableZ[i].next;
1620  }
1621  }
1622  if (table->subtableZ[y].next != (unsigned) y) {
1623  table->subtableZ[x].next = table->subtableZ[y].next;
1624  } else {
1625  table->subtableZ[x].next = x;
1626  }
1627 
1628  if (yprev != y) {
1629  table->subtableZ[yprev].next = x;
1630  } else {
1631  yprev = x;
1632  }
1633  table->subtableZ[y].next = temp;
1634 
1635  size = cuddZddSwapInPlace(table, x, y);
1636  if (size == 0)
1637  return(0);
1638  y = x;
1639  x--;
1640  } /* while y > gxtop */
1641 
1642  /* Trying to find the next y. */
1643  if (table->subtableZ[y].next <= (unsigned) y) {
1644  gybot = y;
1645  } else {
1646  y = table->subtableZ[y].next;
1647  }
1648 
1649  yprev = gxtop;
1650  gxtop++;
1651  gxbot++;
1652  x = gxbot;
1653  } /* while x <= y, end of group movement backward */
1654 
1655  return(size);
1656 
1657 } /* end of zdd_group_move_backward */
cuddZddSwapInPlace
int cuddZddSwapInPlace(DdManager *table, int x, int y)
Definition: cuddZddReord.c:484
size
static int size
Definition: cuddSign.c:86
DdSubtable::next
unsigned int next
Definition: cuddInt.h:333
assert
#define assert(ex)
Definition: util_old.h:213
DdManager::subtableZ
DdSubtable * subtableZ
Definition: cuddInt.h:366

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddZddSymm.c,v 1.29 2004/08/13 18:04:54 fabio Exp $"
static

Definition at line 96 of file cuddZddSymm.c.

DdNode* empty
static

Definition at line 103 of file cuddZddSymm.c.

int* zdd_entry

Definition at line 108 of file cuddZddReord.c.

int zddTotalNumberSwapping

Definition at line 110 of file cuddZddReord.c.