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
cuddAnnealing(DdManager * table,int lower,int upper)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
stopping_criterion(int c1,int c2,int c3,int c4,double temp)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
random_generator(void)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
ddExchange(DdManager * table,int x,int y,double temp)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
ddJumpingAux(DdManager * table,int x,int x_low,int x_high,double temp)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 *
ddJumpingUp(DdManager * table,int x,int x_low,int initial_size)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 *
ddJumpingDown(DdManager * table,int x,int x_high,int initial_size)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
siftBackwardProb(DdManager * table,Move * moves,int size,double temp)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
copyOrder(DdManager * table,int * array,int lower,int upper)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
restoreOrder(DdManager * table,int * array,int lower,int upper)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
823