abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cuddZddSymm.c
Go to the documentation of this file.
1 /**CFile***********************************************************************
2 
3  FileName [cuddZddSymm.c]
4 
5  PackageName [cudd]
6 
7  Synopsis [Functions for symmetry-based ZDD variable reordering.]
8 
9  Description [External procedures included in this module:
10  <ul>
11  <li> Cudd_zddSymmProfile()
12  </ul>
13  Internal procedures included in this module:
14  <ul>
15  <li> cuddZddSymmCheck()
16  <li> cuddZddSymmSifting()
17  <li> cuddZddSymmSiftingConv()
18  </ul>
19  Static procedures included in this module:
20  <ul>
21  <li> cuddZddUniqueCompare()
22  <li> cuddZddSymmSiftingAux()
23  <li> cuddZddSymmSiftingConvAux()
24  <li> cuddZddSymmSifting_up()
25  <li> cuddZddSymmSifting_down()
26  <li> zdd_group_move()
27  <li> cuddZddSymmSiftingBackward()
28  <li> zdd_group_move_backward()
29  </ul>
30  ]
31 
32  SeeAlso [cuddSymmetry.c]
33 
34  Author [Hyong-Kyoon Shin, In-Ho Moon]
35 
36  Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
37 
38  All rights reserved.
39 
40  Redistribution and use in source and binary forms, with or without
41  modification, are permitted provided that the following conditions
42  are met:
43 
44  Redistributions of source code must retain the above copyright
45  notice, this list of conditions and the following disclaimer.
46 
47  Redistributions in binary form must reproduce the above copyright
48  notice, this list of conditions and the following disclaimer in the
49  documentation and/or other materials provided with the distribution.
50 
51  Neither the name of the University of Colorado nor the names of its
52  contributors may be used to endorse or promote products derived from
53  this software without specific prior written permission.
54 
55  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
56  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
57  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
58  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
59  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
60  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
61  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
62  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
63  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
64  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
65  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
66  POSSIBILITY OF SUCH DAMAGE.]
67 
68 ******************************************************************************/
69 
70 #include "misc/util/util_hack.h"
71 #include "cuddInt.h"
72 
73 ABC_NAMESPACE_IMPL_START
74 
75 
76 
77 /*---------------------------------------------------------------------------*/
78 /* Constant declarations */
79 /*---------------------------------------------------------------------------*/
80 
81 #define ZDD_MV_OOM (Move *)1
82 
83 /*---------------------------------------------------------------------------*/
84 /* Stucture declarations */
85 /*---------------------------------------------------------------------------*/
86 
87 /*---------------------------------------------------------------------------*/
88 /* Type declarations */
89 /*---------------------------------------------------------------------------*/
90 
91 /*---------------------------------------------------------------------------*/
92 /* Variable declarations */
93 /*---------------------------------------------------------------------------*/
94 
95 #ifndef lint
96 static char rcsid[] DD_UNUSED = "$Id: cuddZddSymm.c,v 1.29 2004/08/13 18:04:54 fabio Exp $";
97 #endif
98 
99 extern int *zdd_entry;
100 
101 extern int zddTotalNumberSwapping;
102 
103 static DdNode *empty;
104 
105 /*---------------------------------------------------------------------------*/
106 /* Macro declarations */
107 /*---------------------------------------------------------------------------*/
108 
109 
110 /**AutomaticStart*************************************************************/
111 
112 /*---------------------------------------------------------------------------*/
113 /* Static function prototypes */
114 /*---------------------------------------------------------------------------*/
115 
116 static int cuddZddSymmSiftingAux (DdManager *table, int x, int x_low, int x_high);
117 static int cuddZddSymmSiftingConvAux (DdManager *table, int x, int x_low, int x_high);
118 static Move * cuddZddSymmSifting_up (DdManager *table, int x, int x_low, int initial_size);
119 static Move * cuddZddSymmSifting_down (DdManager *table, int x, int x_high, int initial_size);
120 static int cuddZddSymmSiftingBackward (DdManager *table, Move *moves, int size);
121 static int zdd_group_move (DdManager *table, int x, int y, Move **moves);
122 static int zdd_group_move_backward (DdManager *table, int x, int y);
123 static void cuddZddSymmSummary (DdManager *table, int lower, int upper, int *symvars, int *symgroups);
124 
125 /**AutomaticEnd***************************************************************/
126 
127 
128 /*---------------------------------------------------------------------------*/
129 /* Definition of exported functions */
130 /*---------------------------------------------------------------------------*/
131 
132 
133 /**Function********************************************************************
134 
135  Synopsis [Prints statistics on symmetric ZDD variables.]
136 
137  Description []
138 
139  SideEffects [None]
140 
141  SeeAlso []
142 
143 ******************************************************************************/
144 void
145 Cudd_zddSymmProfile(
146  DdManager * table,
147  int lower,
148  int upper)
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 */
176 
177 
178 /*---------------------------------------------------------------------------*/
179 /* Definition of internal functions */
180 /*---------------------------------------------------------------------------*/
181 
182 
183 /**Function********************************************************************
184 
185  Synopsis [Checks for symmetry of x and y.]
186 
187  Description [Checks for symmetry of x and y. Ignores projection
188  functions, unless they are isolated. Returns 1 in case of
189  symmetry; 0 otherwise.]
190 
191  SideEffects [None]
192 
193  SeeAlso []
194 
195 ******************************************************************************/
196 int
197 cuddZddSymmCheck(
198  DdManager * table,
199  int x,
200  int y)
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 */
277 
278 
279 /**Function********************************************************************
280 
281  Synopsis [Symmetric sifting algorithm for ZDDs.]
282 
283  Description [Symmetric sifting algorithm.
284  Assumes that no dead nodes are present.
285  <ol>
286  <li> Order all the variables according to the number of entries in
287  each unique subtable.
288  <li> Sift the variable up and down, remembering each time the total
289  size of the ZDD heap and grouping variables that are symmetric.
290  <li> Select the best permutation.
291  <li> Repeat 3 and 4 for all variables.
292  </ol>
293  Returns 1 plus the number of symmetric variables if successful; 0
294  otherwise.]
295 
296  SideEffects [None]
297 
298  SeeAlso [cuddZddSymmSiftingConv]
299 
300 ******************************************************************************/
301 int
302 cuddZddSymmSifting(
303  DdManager * table,
304  int lower,
305  int upper)
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 */
397 
398 
399 /**Function********************************************************************
400 
401  Synopsis [Symmetric sifting to convergence algorithm for ZDDs.]
402 
403  Description [Symmetric sifting to convergence algorithm for ZDDs.
404  Assumes that no dead nodes are present.
405  <ol>
406  <li> Order all the variables according to the number of entries in
407  each unique subtable.
408  <li> Sift the variable up and down, remembering each time the total
409  size of the ZDD heap and grouping variables that are symmetric.
410  <li> Select the best permutation.
411  <li> Repeat 3 and 4 for all variables.
412  <li> Repeat 1-4 until no further improvement.
413  </ol>
414  Returns 1 plus the number of symmetric variables if successful; 0
415  otherwise.]
416 
417  SideEffects [None]
418 
419  SeeAlso [cuddZddSymmSifting]
420 
421 ******************************************************************************/
422 int
423 cuddZddSymmSiftingConv(
424  DdManager * table,
425  int lower,
426  int upper)
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 */
578 
579 
580 /*---------------------------------------------------------------------------*/
581 /* Definition of static functions */
582 /*---------------------------------------------------------------------------*/
583 
584 
585 /**Function********************************************************************
586 
587  Synopsis [Given x_low <= x <= x_high moves x up and down between the
588  boundaries.]
589 
590  Description [Given x_low <= x <= x_high moves x up and down between the
591  boundaries. Finds the best position and does the required changes.
592  Assumes that x is not part of a symmetry group. Returns 1 if
593  successful; 0 otherwise.]
594 
595  SideEffects [None]
596 
597  SeeAlso []
598 
599 ******************************************************************************/
600 static int
601 cuddZddSymmSiftingAux(
602  DdManager * table,
603  int x,
604  int x_low,
605  int x_high)
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 */
922 
923 
924 /**Function********************************************************************
925 
926  Synopsis [Given x_low <= x <= x_high moves x up and down between the
927  boundaries.]
928 
929  Description [Given x_low <= x <= x_high moves x up and down between the
930  boundaries. Finds the best position and does the required changes.
931  Assumes that x is either an isolated variable, or it is the bottom of
932  a symmetry group. All symmetries may not have been found, because of
933  exceeded growth limit. Returns 1 if successful; 0 otherwise.]
934 
935  SideEffects [None]
936 
937  SeeAlso []
938 
939 ******************************************************************************/
940 static int
941 cuddZddSymmSiftingConvAux(
942  DdManager * table,
943  int x,
944  int x_low,
945  int x_high)
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 */
1230 
1231 
1232 /**Function********************************************************************
1233 
1234  Synopsis [Moves x up until either it reaches the bound (x_low) or
1235  the size of the ZDD heap increases too much.]
1236 
1237  Description [Moves x up until either it reaches the bound (x_low) or
1238  the size of the ZDD heap increases too much. Assumes that x is the top
1239  of a symmetry group. Checks x for symmetry to the adjacent
1240  variables. If symmetry is found, the symmetry group of x is merged
1241  with the symmetry group of the other variable. Returns the set of
1242  moves in case of success; ZDD_MV_OOM if memory is full.]
1243 
1244  SideEffects [None]
1245 
1246  SeeAlso []
1247 
1248 ******************************************************************************/
1249 static Move *
1250 cuddZddSymmSifting_up(
1251  DdManager * table,
1252  int x,
1253  int x_low,
1254  int initial_size)
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 */
1318 
1319 
1320 /**Function********************************************************************
1321 
1322  Synopsis [Moves x down until either it reaches the bound (x_high) or
1323  the size of the ZDD heap increases too much.]
1324 
1325  Description [Moves x down until either it reaches the bound (x_high)
1326  or the size of the ZDD heap increases too much. Assumes that x is the
1327  bottom of a symmetry group. Checks x for symmetry to the adjacent
1328  variables. If symmetry is found, the symmetry group of x is merged
1329  with the symmetry group of the other variable. Returns the set of
1330  moves in case of success; ZDD_MV_OOM if memory is full.]
1331 
1332  SideEffects [None]
1333 
1334  SeeAlso []
1335 
1336 ******************************************************************************/
1337 static Move *
1338 cuddZddSymmSifting_down(
1339  DdManager * table,
1340  int x,
1341  int x_high,
1342  int initial_size)
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 */
1411 
1412 
1413 /**Function********************************************************************
1414 
1415  Synopsis [Given a set of moves, returns the ZDD heap to the position
1416  giving the minimum size.]
1417 
1418  Description [Given a set of moves, returns the ZDD heap to the
1419  position giving the minimum size. In case of ties, returns to the
1420  closest position giving the minimum size. Returns 1 in case of
1421  success; 0 otherwise.]
1422 
1423  SideEffects [None]
1424 
1425  SeeAlso []
1426 
1427 ******************************************************************************/
1428 static int
1429 cuddZddSymmSiftingBackward(
1430  DdManager * table,
1431  Move * moves,
1432  int size)
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 */
1464 
1465 
1466 /**Function********************************************************************
1467 
1468  Synopsis [Swaps two groups.]
1469 
1470  Description [Swaps two groups. x is assumed to be the bottom variable
1471  of the first group. y is assumed to be the top variable of the second
1472  group. Updates the list of moves. Returns the number of keys in the
1473  table if successful; 0 otherwise.]
1474 
1475  SideEffects [None]
1476 
1477  SeeAlso []
1478 
1479 ******************************************************************************/
1480 static int
1481 zdd_group_move(
1482  DdManager * table,
1483  int x,
1484  int y,
1485  Move ** moves)
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 */
1572 
1573 
1574 /**Function********************************************************************
1575 
1576  Synopsis [Undoes the swap of two groups.]
1577 
1578  Description [Undoes the swap of two groups. x is assumed to be the
1579  bottom variable of the first group. y is assumed to be the top
1580  variable of the second group. Returns 1 if successful; 0 otherwise.]
1581 
1582  SideEffects [None]
1583 
1584  SeeAlso []
1585 
1586 ******************************************************************************/
1587 static int
1588 zdd_group_move_backward(
1589  DdManager * table,
1590  int x,
1591  int y)
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 */
1658 
1659 
1660 /**Function********************************************************************
1661 
1662  Synopsis [Counts numbers of symmetric variables and symmetry
1663  groups.]
1664 
1665  Description []
1666 
1667  SideEffects [None]
1668 
1669 ******************************************************************************/
1670 static void
1671 cuddZddSymmSummary(
1672  DdManager * table,
1673  int lower,
1674  int upper,
1675  int * symvars,
1676  int * symgroups)
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 */
1703 
1704 
1705 ABC_NAMESPACE_IMPL_END
1706 
1707 
DdNode::ref
DdHalfWord ref
Definition: cudd.h:280
DdSubtable::keys
unsigned int keys
Definition: cuddInt.h:330
DD_UNUSED
static char rcsid[] DD_UNUSED
Definition: cuddZddSymm.c:96
cuddDeallocMove
#define cuddDeallocMove(unique, node)
Definition: cuddInt.h:564
DdNode
Definition: cudd.h:278
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
Move
Definition: cuddInt.h:492
cuddZddSymmCheck
int cuddZddSymmCheck(DdManager *table, int x, int y)
Definition: cuddZddSymm.c:197
DdManager::zero
DdNode * zero
Definition: cuddInt.h:346
DdManager::maxGrowth
double maxGrowth
Definition: cuddInt.h:413
cuddZddSwapInPlace
int cuddZddSwapInPlace(DdManager *table, int x, int y)
Definition: cuddZddReord.c:484
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
NIL
#define NIL(type)
Definition: avl.h:25
cuddZddSymmSifting
int cuddZddSymmSifting(DdManager *table, int lower, int upper)
Definition: cuddZddSymm.c:302
cuddZddSymmSifting_down
static Move * cuddZddSymmSifting_down(DdManager *table, int x, int x_high, int initial_size)
Definition: cuddZddSymm.c:1338
util_hack.h
cuddZddSymmSiftingBackward
static int cuddZddSymmSiftingBackward(DdManager *table, Move *moves, int size)
Definition: cuddZddSymm.c:1429
zddTotalNumberSwapping
int zddTotalNumberSwapping
Definition: cuddZddReord.c:110
empty
static DdNode * empty
Definition: cuddZddSymm.c:103
DdManager::out
FILE * out
Definition: cuddInt.h:441
Cudd_zddSymmProfile
void Cudd_zddSymmProfile(DdManager *table, int lower, int upper)
Definition: cuddZddSymm.c:145
Move::x
DdHalfWord x
Definition: cuddInt.h:493
DdNode::next
DdNode * next
Definition: cudd.h:281
zdd_group_move
static int zdd_group_move(DdManager *table, int x, int y, Move **moves)
Definition: cuddZddSymm.c:1481
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
DdSubtable::nodelist
DdNode ** nodelist
Definition: cuddInt.h:327
size
static int size
Definition: cuddSign.c:86
ddMin
#define ddMin(x, y)
Definition: cuddInt.h:818
cuddZddNextHigh
int cuddZddNextHigh(DdManager *table, int x)
Definition: cuddZddReord.c:413
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
cuddDynamicAllocNode
DdNode * cuddDynamicAllocNode(DdManager *table)
Definition: cuddReorder.c:406
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
DdManager::siftMaxVar
int siftMaxVar
Definition: cuddInt.h:411
cuddZddSymmSiftingConv
int cuddZddSymmSiftingConv(DdManager *table, int lower, int upper)
Definition: cuddZddSymm.c:423
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
DdNode::index
DdHalfWord index
Definition: cudd.h:279
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
DdSubtable::slots
unsigned int slots
Definition: cuddInt.h:329
Move::y
DdHalfWord y
Definition: cuddInt.h:494
DdSubtable::next
unsigned int next
Definition: cuddInt.h:333
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
Move::next
struct Move * next
Definition: cuddInt.h:497
ZDD_MV_OOM
#define ZDD_MV_OOM
Definition: cuddZddSymm.c:81
assert
#define assert(ex)
Definition: util_old.h:213
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
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
cuddZddNextLow
int cuddZddNextLow(DdManager *table, int x)
Definition: cuddZddReord.c:435
Move::size
int size
Definition: cuddInt.h:496
DdManager::errorCode
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
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