abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cuddAnneal.c
Go to the documentation of this file.
1 /**CFile***********************************************************************
2 
3  FileName [cuddAnneal.c]
4 
5  PackageName [cudd]
6 
7  Synopsis [Reordering of DDs based on simulated annealing]
8 
9  Description [Internal procedures included in this file:
10  <ul>
11  <li> cuddAnnealing()
12  </ul>
13  Static procedures included in this file:
14  <ul>
15  <li> stopping_criterion()
16  <li> random_generator()
17  <li> ddExchange()
18  <li> ddJumpingAux()
19  <li> ddJumpingUp()
20  <li> ddJumpingDown()
21  <li> siftBackwardProb()
22  <li> copyOrder()
23  <li> restoreOrder()
24  </ul>
25  ]
26 
27  SeeAlso []
28 
29  Author [Jae-Young Jang, Jorgen Sivesind]
30 
31  Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
32 
33  All rights reserved.
34 
35  Redistribution and use in source and binary forms, with or without
36  modification, are permitted provided that the following conditions
37  are met:
38 
39  Redistributions of source code must retain the above copyright
40  notice, this list of conditions and the following disclaimer.
41 
42  Redistributions in binary form must reproduce the above copyright
43  notice, this list of conditions and the following disclaimer in the
44  documentation and/or other materials provided with the distribution.
45 
46  Neither the name of the University of Colorado nor the names of its
47  contributors may be used to endorse or promote products derived from
48  this software without specific prior written permission.
49 
50  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
51  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
52  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
53  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
54  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
55  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
56  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
57  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
58  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
59  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
60  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
61  POSSIBILITY OF SUCH DAMAGE.]
62 
63 ******************************************************************************/
64 
65 #include "misc/util/util_hack.h"
66 #include "cuddInt.h"
67 
68 ABC_NAMESPACE_IMPL_START
69 
70 
71 
72 /*---------------------------------------------------------------------------*/
73 /* Constant declarations */
74 /*---------------------------------------------------------------------------*/
75 
76 /* Annealing parameters */
77 #define BETA 0.6
78 #define ALPHA 0.90
79 #define EXC_PROB 0.4
80 #define JUMP_UP_PROB 0.36
81 #define MAXGEN_RATIO 15.0
82 #define STOP_TEMP 1.0
83 
84 /*---------------------------------------------------------------------------*/
85 /* Stucture declarations */
86 /*---------------------------------------------------------------------------*/
87 
88 
89 /*---------------------------------------------------------------------------*/
90 /* Type declarations */
91 /*---------------------------------------------------------------------------*/
92 
93 
94 /*---------------------------------------------------------------------------*/
95 /* Variable declarations */
96 /*---------------------------------------------------------------------------*/
97 
98 #ifndef lint
99 static char rcsid[] DD_UNUSED = "$Id: cuddAnneal.c,v 1.14 2004/08/13 18:04:46 fabio Exp $";
100 #endif
101 
102 #ifdef DD_STATS
103 extern int ddTotalNumberSwapping;
104 extern int ddTotalNISwaps;
105 static int tosses;
106 static int acceptances;
107 #endif
108 
109 /*---------------------------------------------------------------------------*/
110 /* Macro declarations */
111 /*---------------------------------------------------------------------------*/
112 
113 
114 /**AutomaticStart*************************************************************/
115 
116 /*---------------------------------------------------------------------------*/
117 /* Static function prototypes */
118 /*---------------------------------------------------------------------------*/
119 
120 static int stopping_criterion (int c1, int c2, int c3, int c4, double temp);
121 static double random_generator (void);
122 static int ddExchange (DdManager *table, int x, int y, double temp);
123 static int ddJumpingAux (DdManager *table, int x, int x_low, int x_high, double temp);
124 static Move * ddJumpingUp (DdManager *table, int x, int x_low, int initial_size);
125 static Move * ddJumpingDown (DdManager *table, int x, int x_high, int initial_size);
126 static int siftBackwardProb (DdManager *table, Move *moves, int size, double temp);
127 static void copyOrder (DdManager *table, int *array, int lower, int upper);
128 static int restoreOrder (DdManager *table, int *array, int lower, int upper);
129 
130 /**AutomaticEnd***************************************************************/
131 
132 
133 /*---------------------------------------------------------------------------*/
134 /* Definition of exported functions */
135 /*---------------------------------------------------------------------------*/
136 
137 /*---------------------------------------------------------------------------*/
138 /* Definition of internal functions */
139 /*---------------------------------------------------------------------------*/
140 
141 
142 /**Function********************************************************************
143 
144  Synopsis [Get new variable-order by simulated annealing algorithm.]
145 
146  Description [Get x, y by random selection. Choose either
147  exchange or jump randomly. In case of jump, choose between jump_up
148  and jump_down randomly. Do exchange or jump and get optimal case.
149  Loop until there is no improvement or temperature reaches
150  minimum. Returns 1 in case of success; 0 otherwise.]
151 
152  SideEffects [None]
153 
154  SeeAlso []
155 
156 ******************************************************************************/
157 int
158 cuddAnnealing(
159  DdManager * table,
160  int lower,
161  int upper)
162 {
163  int nvars;
164  int size;
165  int x,y;
166  int result;
167  int c1, c2, c3, c4;
168  int BestCost;
169  int *BestOrder;
170  double NewTemp, temp;
171  double rand1;
172  int innerloop, maxGen;
173  int ecount, ucount, dcount;
174 
175  nvars = upper - lower + 1;
176 
177  result = cuddSifting(table,lower,upper);
178 #ifdef DD_STATS
179  (void) fprintf(table->out,"\n");
180 #endif
181  if (result == 0) return(0);
182 
183  size = table->keys - table->isolated;
184 
185  /* Keep track of the best order. */
186  BestCost = size;
187  BestOrder = ABC_ALLOC(int,nvars);
188  if (BestOrder == NULL) {
189  table->errorCode = CUDD_MEMORY_OUT;
190  return(0);
191  }
192  copyOrder(table,BestOrder,lower,upper);
193 
194  temp = BETA * size;
195  maxGen = (int) (MAXGEN_RATIO * nvars);
196 
197  c1 = size + 10;
198  c2 = c1 + 10;
199  c3 = size;
200  c4 = c2 + 10;
201  ecount = ucount = dcount = 0;
202 
203  while (!stopping_criterion(c1, c2, c3, c4, temp)) {
204 #ifdef DD_STATS
205  (void) fprintf(table->out,"temp=%f\tsize=%d\tgen=%d\t",
206  temp,size,maxGen);
207  tosses = acceptances = 0;
208 #endif
209  for (innerloop = 0; innerloop < maxGen; innerloop++) {
210  /* Choose x, y randomly. */
211  x = (int) Cudd_Random() % nvars;
212  do {
213  y = (int) Cudd_Random() % nvars;
214  } while (x == y);
215  x += lower;
216  y += lower;
217  if (x > y) {
218  int tmp = x;
219  x = y;
220  y = tmp;
221  }
222 
223  /* Choose move with roulette wheel. */
224  rand1 = random_generator();
225  if (rand1 < EXC_PROB) {
226  result = ddExchange(table,x,y,temp); /* exchange */
227  ecount++;
228 #if 0
229  (void) fprintf(table->out,
230  "Exchange of %d and %d: size = %d\n",
231  x,y,table->keys - table->isolated);
232 #endif
233  } else if (rand1 < EXC_PROB + JUMP_UP_PROB) {
234  result = ddJumpingAux(table,y,x,y,temp); /* jumping_up */
235  ucount++;
236 #if 0
237  (void) fprintf(table->out,
238  "Jump up of %d to %d: size = %d\n",
239  y,x,table->keys - table->isolated);
240 #endif
241  } else {
242  result = ddJumpingAux(table,x,x,y,temp); /* jumping_down */
243  dcount++;
244 #if 0
245  (void) fprintf(table->out,
246  "Jump down of %d to %d: size = %d\n",
247  x,y,table->keys - table->isolated);
248 #endif
249  }
250 
251  if (!result) {
252  ABC_FREE(BestOrder);
253  return(0);
254  }
255 
256  size = table->keys - table->isolated; /* keep current size */
257  if (size < BestCost) { /* update best order */
258  BestCost = size;
259  copyOrder(table,BestOrder,lower,upper);
260  }
261  }
262  c1 = c2;
263  c2 = c3;
264  c3 = c4;
265  c4 = size;
266  NewTemp = ALPHA * temp;
267  if (NewTemp >= 1.0) {
268  maxGen = (int)(log(NewTemp) / log(temp) * maxGen);
269  }
270  temp = NewTemp; /* control variable */
271 #ifdef DD_STATS
272  (void) fprintf(table->out,"uphill = %d\taccepted = %d\n",
273  tosses,acceptances);
274  fflush(table->out);
275 #endif
276  }
277 
278  result = restoreOrder(table,BestOrder,lower,upper);
279  ABC_FREE(BestOrder);
280  if (!result) return(0);
281 #ifdef DD_STATS
282  fprintf(table->out,"#:N_EXCHANGE %8d : total exchanges\n",ecount);
283  fprintf(table->out,"#:N_JUMPUP %8d : total jumps up\n",ucount);
284  fprintf(table->out,"#:N_JUMPDOWN %8d : total jumps down",dcount);
285 #endif
286  return(1);
287 
288 } /* end of cuddAnnealing */
289 
290 
291 /*---------------------------------------------------------------------------*/
292 /* Definition of static functions */
293 /*---------------------------------------------------------------------------*/
294 
295 /**Function********************************************************************
296 
297  Synopsis [Checks termination condition.]
298 
299  Description [If temperature is STOP_TEMP or there is no improvement
300  then terminates. Returns 1 if the termination criterion is met; 0
301  otherwise.]
302 
303  SideEffects [None]
304 
305  SeeAlso []
306 
307 ******************************************************************************/
308 static int
309 stopping_criterion(
310  int c1,
311  int c2,
312  int c3,
313  int c4,
314  double temp)
315 {
316  if (STOP_TEMP < temp) {
317  return(0);
318  } else if ((c1 == c2) && (c1 == c3) && (c1 == c4)) {
319  return(1);
320  } else {
321  return(0);
322  }
323 
324 } /* end of stopping_criterion */
325 
326 
327 /**Function********************************************************************
328 
329  Synopsis [Random number generator.]
330 
331  Description [Returns a double precision value between 0.0 and 1.0.]
332 
333  SideEffects [None]
334 
335  SeeAlso []
336 
337 ******************************************************************************/
338 static double
339 random_generator(void)
340 {
341  return((double)(Cudd_Random() / 2147483561.0));
342 
343 } /* end of random_generator */
344 
345 
346 /**Function********************************************************************
347 
348  Synopsis [This function is for exchanging two variables, x and y.]
349 
350  Description [This is the same funcion as ddSwapping except for
351  comparison expression. Use probability function, exp(-size_change/temp).]
352 
353  SideEffects [None]
354 
355  SeeAlso []
356 
357 ******************************************************************************/
358 static int
359 ddExchange(
360  DdManager * table,
361  int x,
362  int y,
363  double temp)
364 {
365  Move *move,*moves;
366  int tmp;
367  int x_ref,y_ref;
368  int x_next,y_next;
369  int size, result;
370  int initial_size, limit_size;
371 
372  x_ref = x;
373  y_ref = y;
374 
375  x_next = cuddNextHigh(table,x);
376  y_next = cuddNextLow(table,y);
377  moves = NULL;
378  initial_size = limit_size = table->keys - table->isolated;
379 
380  for (;;) {
381  if (x_next == y_next) {
382  size = cuddSwapInPlace(table,x,x_next);
383  if (size == 0) goto ddExchangeOutOfMem;
384  move = (Move *)cuddDynamicAllocNode(table);
385  if (move == NULL) goto ddExchangeOutOfMem;
386  move->x = x;
387  move->y = x_next;
388  move->size = size;
389  move->next = moves;
390  moves = move;
391  size = cuddSwapInPlace(table,y_next,y);
392  if (size == 0) goto ddExchangeOutOfMem;
393  move = (Move *)cuddDynamicAllocNode(table);
394  if (move == NULL) goto ddExchangeOutOfMem;
395  move->x = y_next;
396  move->y = y;
397  move->size = size;
398  move->next = moves;
399  moves = move;
400  size = cuddSwapInPlace(table,x,x_next);
401  if (size == 0) goto ddExchangeOutOfMem;
402  move = (Move *)cuddDynamicAllocNode(table);
403  if (move == NULL) goto ddExchangeOutOfMem;
404  move->x = x;
405  move->y = x_next;
406  move->size = size;
407  move->next = moves;
408  moves = move;
409 
410  tmp = x;
411  x = y;
412  y = tmp;
413  } else if (x == y_next) {
414  size = cuddSwapInPlace(table,x,x_next);
415  if (size == 0) goto ddExchangeOutOfMem;
416  move = (Move *)cuddDynamicAllocNode(table);
417  if (move == NULL) goto ddExchangeOutOfMem;
418  move->x = x;
419  move->y = x_next;
420  move->size = size;
421  move->next = moves;
422  moves = move;
423  tmp = x;
424  x = y;
425  y = tmp;
426  } else {
427  size = cuddSwapInPlace(table,x,x_next);
428  if (size == 0) goto ddExchangeOutOfMem;
429  move = (Move *)cuddDynamicAllocNode(table);
430  if (move == NULL) goto ddExchangeOutOfMem;
431  move->x = x;
432  move->y = x_next;
433  move->size = size;
434  move->next = moves;
435  moves = move;
436  size = cuddSwapInPlace(table,y_next,y);
437  if (size == 0) goto ddExchangeOutOfMem;
438  move = (Move *)cuddDynamicAllocNode(table);
439  if (move == NULL) goto ddExchangeOutOfMem;
440  move->x = y_next;
441  move->y = y;
442  move->size = size;
443  move->next = moves;
444  moves = move;
445  x = x_next;
446  y = y_next;
447  }
448 
449  x_next = cuddNextHigh(table,x);
450  y_next = cuddNextLow(table,y);
451  if (x_next > y_ref) break;
452 
453  if ((double) size > DD_MAX_REORDER_GROWTH * (double) limit_size) {
454  break;
455  } else if (size < limit_size) {
456  limit_size = size;
457  }
458  }
459 
460  if (y_next>=x_ref) {
461  size = cuddSwapInPlace(table,y_next,y);
462  if (size == 0) goto ddExchangeOutOfMem;
463  move = (Move *)cuddDynamicAllocNode(table);
464  if (move == NULL) goto ddExchangeOutOfMem;
465  move->x = y_next;
466  move->y = y;
467  move->size = size;
468  move->next = moves;
469  moves = move;
470  }
471 
472  /* move backward and stop at best position or accept uphill move */
473  result = siftBackwardProb(table,moves,initial_size,temp);
474  if (!result) goto ddExchangeOutOfMem;
475 
476  while (moves != NULL) {
477  move = moves->next;
478  cuddDeallocMove(table, moves);
479  moves = move;
480  }
481  return(1);
482 
483 ddExchangeOutOfMem:
484  while (moves != NULL) {
485  move = moves->next;
486  cuddDeallocMove(table, moves);
487  moves = move;
488  }
489  return(0);
490 
491 } /* end of ddExchange */
492 
493 
494 /**Function********************************************************************
495 
496  Synopsis [Moves a variable to a specified position.]
497 
498  Description [If x==x_low, it executes jumping_down. If x==x_high, it
499  executes jumping_up. This funcion is similar to ddSiftingAux. Returns
500  1 in case of success; 0 otherwise.]
501 
502  SideEffects [None]
503 
504  SeeAlso []
505 
506 ******************************************************************************/
507 static int
508 ddJumpingAux(
509  DdManager * table,
510  int x,
511  int x_low,
512  int x_high,
513  double temp)
514 {
515  Move *move;
516  Move *moves; /* list of moves */
517  int initial_size;
518  int result;
519 
520  initial_size = table->keys - table->isolated;
521 
522 #ifdef DD_DEBUG
523  assert(table->subtables[x].keys > 0);
524 #endif
525 
526  moves = NULL;
527 
528  if (cuddNextLow(table,x) < x_low) {
529  if (cuddNextHigh(table,x) > x_high) return(1);
530  moves = ddJumpingDown(table,x,x_high,initial_size);
531  /* after that point x --> x_high unless early termination */
532  if (moves == NULL) goto ddJumpingAuxOutOfMem;
533  /* move backward and stop at best position or accept uphill move */
534  result = siftBackwardProb(table,moves,initial_size,temp);
535  if (!result) goto ddJumpingAuxOutOfMem;
536  } else if (cuddNextHigh(table,x) > x_high) {
537  moves = ddJumpingUp(table,x,x_low,initial_size);
538  /* after that point x --> x_low unless early termination */
539  if (moves == NULL) goto ddJumpingAuxOutOfMem;
540  /* move backward and stop at best position or accept uphill move */
541  result = siftBackwardProb(table,moves,initial_size,temp);
542  if (!result) goto ddJumpingAuxOutOfMem;
543  } else {
544  (void) fprintf(table->err,"Unexpected condition in ddJumping\n");
545  goto ddJumpingAuxOutOfMem;
546  }
547  while (moves != NULL) {
548  move = moves->next;
549  cuddDeallocMove(table, moves);
550  moves = move;
551  }
552  return(1);
553 
554 ddJumpingAuxOutOfMem:
555  while (moves != NULL) {
556  move = moves->next;
557  cuddDeallocMove(table, moves);
558  moves = move;
559  }
560  return(0);
561 
562 } /* end of ddJumpingAux */
563 
564 
565 /**Function********************************************************************
566 
567  Synopsis [This function is for jumping up.]
568 
569  Description [This is a simplified version of ddSiftingUp. It does not
570  use lower bounding. Returns the set of moves in case of success; NULL
571  if memory is full.]
572 
573  SideEffects [None]
574 
575  SeeAlso []
576 
577 ******************************************************************************/
578 static Move *
579 ddJumpingUp(
580  DdManager * table,
581  int x,
582  int x_low,
583  int initial_size)
584 {
585  Move *moves;
586  Move *move;
587  int y;
588  int size;
589  int limit_size = initial_size;
590 
591  moves = NULL;
592  y = cuddNextLow(table,x);
593  while (y >= x_low) {
594  size = cuddSwapInPlace(table,y,x);
595  if (size == 0) goto ddJumpingUpOutOfMem;
596  move = (Move *)cuddDynamicAllocNode(table);
597  if (move == NULL) goto ddJumpingUpOutOfMem;
598  move->x = y;
599  move->y = x;
600  move->size = size;
601  move->next = moves;
602  moves = move;
603  if ((double) size > table->maxGrowth * (double) limit_size) {
604  break;
605  } else if (size < limit_size) {
606  limit_size = size;
607  }
608  x = y;
609  y = cuddNextLow(table,x);
610  }
611  return(moves);
612 
613 ddJumpingUpOutOfMem:
614  while (moves != NULL) {
615  move = moves->next;
616  cuddDeallocMove(table, moves);
617  moves = move;
618  }
619  return(NULL);
620 
621 } /* end of ddJumpingUp */
622 
623 
624 /**Function********************************************************************
625 
626  Synopsis [This function is for jumping down.]
627 
628  Description [This is a simplified version of ddSiftingDown. It does not
629  use lower bounding. Returns the set of moves in case of success; NULL
630  if memory is full.]
631 
632  SideEffects [None]
633 
634  SeeAlso []
635 
636 ******************************************************************************/
637 static Move *
638 ddJumpingDown(
639  DdManager * table,
640  int x,
641  int x_high,
642  int initial_size)
643 {
644  Move *moves;
645  Move *move;
646  int y;
647  int size;
648  int limit_size = initial_size;
649 
650  moves = NULL;
651  y = cuddNextHigh(table,x);
652  while (y <= x_high) {
653  size = cuddSwapInPlace(table,x,y);
654  if (size == 0) goto ddJumpingDownOutOfMem;
655  move = (Move *)cuddDynamicAllocNode(table);
656  if (move == NULL) goto ddJumpingDownOutOfMem;
657  move->x = x;
658  move->y = y;
659  move->size = size;
660  move->next = moves;
661  moves = move;
662  if ((double) size > table->maxGrowth * (double) limit_size) {
663  break;
664  } else if (size < limit_size) {
665  limit_size = size;
666  }
667  x = y;
668  y = cuddNextHigh(table,x);
669  }
670  return(moves);
671 
672 ddJumpingDownOutOfMem:
673  while (moves != NULL) {
674  move = moves->next;
675  cuddDeallocMove(table, moves);
676  moves = move;
677  }
678  return(NULL);
679 
680 } /* end of ddJumpingDown */
681 
682 
683 /**Function********************************************************************
684 
685  Synopsis [Returns the DD to the best position encountered during
686  sifting if there was improvement.]
687 
688  Description [Otherwise, "tosses a coin" to decide whether to keep
689  the current configuration or return the DD to the original
690  one. Returns 1 in case of success; 0 otherwise.]
691 
692  SideEffects [None]
693 
694  SeeAlso []
695 
696 ******************************************************************************/
697 static int
698 siftBackwardProb(
699  DdManager * table,
700  Move * moves,
701  int size,
702  double temp)
703 {
704  Move *move;
705  int res;
706  int best_size = size;
707  double coin, threshold;
708 
709  /* Look for best size during the last sifting */
710  for (move = moves; move != NULL; move = move->next) {
711  if (move->size < best_size) {
712  best_size = move->size;
713  }
714  }
715 
716  /* If best_size equals size, the last sifting did not produce any
717  ** improvement. We now toss a coin to decide whether to retain
718  ** this change or not.
719  */
720  if (best_size == size) {
721  coin = random_generator();
722 #ifdef DD_STATS
723  tosses++;
724 #endif
725  threshold = exp(-((double)(table->keys - table->isolated - size))/temp);
726  if (coin < threshold) {
727 #ifdef DD_STATS
728  acceptances++;
729 #endif
730  return(1);
731  }
732  }
733 
734  /* Either there was improvement, or we have decided not to
735  ** accept the uphill move. Go to best position.
736  */
737  res = table->keys - table->isolated;
738  for (move = moves; move != NULL; move = move->next) {
739  if (res == best_size) return(1);
740  res = cuddSwapInPlace(table,(int)move->x,(int)move->y);
741  if (!res) return(0);
742  }
743 
744  return(1);
745 
746 } /* end of sift_backward_prob */
747 
748 
749 /**Function********************************************************************
750 
751  Synopsis [Copies the current variable order to array.]
752 
753  Description [Copies the current variable order to array.
754  At the same time inverts the permutation.]
755 
756  SideEffects [None]
757 
758  SeeAlso []
759 
760 ******************************************************************************/
761 static void
762 copyOrder(
763  DdManager * table,
764  int * array,
765  int lower,
766  int upper)
767 {
768  int i;
769  int nvars;
770 
771  nvars = upper - lower + 1;
772  for (i = 0; i < nvars; i++) {
773  array[i] = table->invperm[i+lower];
774  }
775 
776 } /* end of copyOrder */
777 
778 
779 /**Function********************************************************************
780 
781  Synopsis [Restores the variable order in array by a series of sifts up.]
782 
783  Description [Restores the variable order in array by a series of sifts up.
784  Returns 1 in case of success; 0 otherwise.]
785 
786  SideEffects [None]
787 
788  SeeAlso []
789 
790 ******************************************************************************/
791 static int
792 restoreOrder(
793  DdManager * table,
794  int * array,
795  int lower,
796  int upper)
797 {
798  int i, x, y, size;
799  int nvars = upper - lower + 1;
800 
801  for (i = 0; i < nvars; i++) {
802  x = table->perm[array[i]];
803 #ifdef DD_DEBUG
804  assert(x >= lower && x <= upper);
805 #endif
806  y = cuddNextLow(table,x);
807  while (y >= i + lower) {
808  size = cuddSwapInPlace(table,y,x);
809  if (size == 0) return(0);
810  x = y;
811  y = cuddNextLow(table,x);
812  }
813  }
814 
815  return(1);
816 
817 } /* end of restoreOrder */
818 
819 
820 ABC_NAMESPACE_IMPL_END
821 
822 
DdSubtable::keys
unsigned int keys
Definition: cuddInt.h:330
cuddDeallocMove
#define cuddDeallocMove(unique, node)
Definition: cuddInt.h:564
stopping_criterion
static int stopping_criterion(int c1, int c2, int c3, int c4, double temp)
Definition: cuddAnneal.c:309
copyOrder
static void copyOrder(DdManager *table, int *array, int lower, int upper)
Definition: cuddAnneal.c:762
random_generator
static double random_generator(void)
Definition: cuddAnneal.c:339
Move
Definition: cuddInt.h:492
ALPHA
#define ALPHA
Definition: cuddAnneal.c:78
cuddNextLow
int cuddNextLow(DdManager *table, int x)
Definition: cuddReorder.c:738
cuddSifting
int cuddSifting(DdManager *table, int lower, int upper)
Definition: cuddReorder.c:508
DdManager::maxGrowth
double maxGrowth
Definition: cuddInt.h:413
DdManager::err
FILE * err
Definition: cuddInt.h:442
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
DdManager::subtables
DdSubtable * subtables
Definition: cuddInt.h:365
restoreOrder
static int restoreOrder(DdManager *table, int *array, int lower, int upper)
Definition: cuddAnneal.c:792
util_hack.h
ddExchange
static int ddExchange(DdManager *table, int x, int y, double temp)
Definition: cuddAnneal.c:359
BETA
#define BETA
Definition: cuddAnneal.c:77
Cudd_Random
long Cudd_Random(void)
Definition: cuddUtil.c:2702
ddTotalNumberSwapping
int ddTotalNumberSwapping
Definition: cuddReorder.c:107
DdManager::keys
unsigned int keys
Definition: cuddInt.h:369
DdManager::out
FILE * out
Definition: cuddInt.h:441
Move::x
DdHalfWord x
Definition: cuddInt.h:493
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
size
static int size
Definition: cuddSign.c:86
EXC_PROB
#define EXC_PROB
Definition: cuddAnneal.c:79
ddJumpingAux
static int ddJumpingAux(DdManager *table, int x, int x_low, int x_high, double temp)
Definition: cuddAnneal.c:508
cuddDynamicAllocNode
DdNode * cuddDynamicAllocNode(DdManager *table)
Definition: cuddReorder.c:406
DD_UNUSED
static char rcsid[] DD_UNUSED
Definition: cuddAnneal.c:99
ddJumpingUp
static Move * ddJumpingUp(DdManager *table, int x, int x_low, int initial_size)
Definition: cuddAnneal.c:579
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
cuddNextHigh
int cuddNextHigh(DdManager *table, int x)
Definition: cuddReorder.c:716
cuddSwapInPlace
int cuddSwapInPlace(DdManager *table, int x, int y)
Definition: cuddReorder.c:761
siftBackwardProb
static int siftBackwardProb(DdManager *table, Move *moves, int size, double temp)
Definition: cuddAnneal.c:698
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Move::y
DdHalfWord y
Definition: cuddInt.h:494
JUMP_UP_PROB
#define JUMP_UP_PROB
Definition: cuddAnneal.c:80
cuddAnnealing
int cuddAnnealing(DdManager *table, int lower, int upper)
Definition: cuddAnneal.c:158
DD_MAX_REORDER_GROWTH
#define DD_MAX_REORDER_GROWTH
Definition: cuddInt.h:150
ddJumpingDown
static Move * ddJumpingDown(DdManager *table, int x, int x_high, int initial_size)
Definition: cuddAnneal.c:638
Move::next
struct Move * next
Definition: cuddInt.h:497
assert
#define assert(ex)
Definition: util_old.h:213
DdManager::invperm
int * invperm
Definition: cuddInt.h:388
result
static int result
Definition: cuddGenetic.c:125
DdManager::isolated
int isolated
Definition: cuddInt.h:385
MAXGEN_RATIO
#define MAXGEN_RATIO
Definition: cuddAnneal.c:81
DdManager::perm
int * perm
Definition: cuddInt.h:386
Move::size
int size
Definition: cuddInt.h:496
DdManager::errorCode
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
STOP_TEMP
#define STOP_TEMP
Definition: cuddAnneal.c:82