source: vis_dev/glu-2.3/src/cuBdd/cuddWindow.c @ 104

Last change on this file since 104 was 13, checked in by cecile, 13 years ago

library glu 2.3
File size: 26.9 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddWindow.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Functions for variable reordering by window permutation.]
8
9  Description [Internal procedures included in this module:
10                <ul>
11                <li> cuddWindowReorder()
12                </ul>
13        Static procedures included in this module:
14                <ul>
15                <li> ddWindow2()
16                <li> ddWindowConv2()
17                <li> ddPermuteWindow3()
18                <li> ddWindow3()
19                <li> ddWindowConv3()
20                <li> ddPermuteWindow4()
21                <li> ddWindow4()
22                <li> ddWindowConv4()
23                </ul>]
24
25  Author      [Fabio Somenzi]
26
27  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
28
29  All rights reserved.
30
31  Redistribution and use in source and binary forms, with or without
32  modification, are permitted provided that the following conditions
33  are met:
34
35  Redistributions of source code must retain the above copyright
36  notice, this list of conditions and the following disclaimer.
37
38  Redistributions in binary form must reproduce the above copyright
39  notice, this list of conditions and the following disclaimer in the
40  documentation and/or other materials provided with the distribution.
41
42  Neither the name of the University of Colorado nor the names of its
43  contributors may be used to endorse or promote products derived from
44  this software without specific prior written permission.
45
46  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
47  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
48  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
49  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
50  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
51  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
52  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
53  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
54  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
55  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
56  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
57  POSSIBILITY OF SUCH DAMAGE.]
58
59******************************************************************************/
60
61#include "util.h"
62#include "cuddInt.h"
63
64/*---------------------------------------------------------------------------*/
65/* Constant declarations                                                     */
66/*---------------------------------------------------------------------------*/
67
68
69/*---------------------------------------------------------------------------*/
70/* Stucture declarations                                                     */
71/*---------------------------------------------------------------------------*/
72
73
74/*---------------------------------------------------------------------------*/
75/* Type declarations                                                         */
76/*---------------------------------------------------------------------------*/
77
78
79/*---------------------------------------------------------------------------*/
80/* Variable declarations                                                     */
81/*---------------------------------------------------------------------------*/
82
83#ifndef lint
84static char rcsid[] DD_UNUSED = "$Id: cuddWindow.c,v 1.14 2009/02/20 02:14:58 fabio Exp $";
85#endif
86
87#ifdef DD_STATS
88extern  int     ddTotalNumberSwapping;
89extern  int     ddTotalNISwaps;
90#endif
91
92/*---------------------------------------------------------------------------*/
93/* Macro declarations                                                        */
94/*---------------------------------------------------------------------------*/
95
96
97/**AutomaticStart*************************************************************/
98
99/*---------------------------------------------------------------------------*/
100/* Static function prototypes                                                */
101/*---------------------------------------------------------------------------*/
102
103static int ddWindow2 (DdManager *table, int low, int high);
104static int ddWindowConv2 (DdManager *table, int low, int high);
105static int ddPermuteWindow3 (DdManager *table, int x);
106static int ddWindow3 (DdManager *table, int low, int high);
107static int ddWindowConv3 (DdManager *table, int low, int high);
108static int ddPermuteWindow4 (DdManager *table, int w);
109static int ddWindow4 (DdManager *table, int low, int high);
110static int ddWindowConv4 (DdManager *table, int low, int high);
111
112/**AutomaticEnd***************************************************************/
113
114
115/*---------------------------------------------------------------------------*/
116/* Definition of exported functions                                          */
117/*---------------------------------------------------------------------------*/
118
119/*---------------------------------------------------------------------------*/
120/* Definition of internal functions                                          */
121/*---------------------------------------------------------------------------*/
122
123
124/**Function********************************************************************
125
126  Synopsis    [Reorders by applying the method of the sliding window.]
127
128  Description [Reorders by applying the method of the sliding window.
129  Tries all possible permutations to the variables in a window that
130  slides from low to high. The size of the window is determined by
131  submethod.  Assumes that no dead nodes are present.  Returns 1 in
132  case of success; 0 otherwise.]
133
134  SideEffects [None]
135
136******************************************************************************/
137int
138cuddWindowReorder(
139  DdManager * table /* DD table */,
140  int low /* lowest index to reorder */,
141  int high /* highest index to reorder */,
142  Cudd_ReorderingType submethod /* window reordering option */)
143{
144
145    int res;
146#ifdef DD_DEBUG
147    int supposedOpt;
148#endif
149
150    switch (submethod) {
151    case CUDD_REORDER_WINDOW2:
152        res = ddWindow2(table,low,high);
153        break;
154    case CUDD_REORDER_WINDOW3:
155        res = ddWindow3(table,low,high);
156        break;
157    case CUDD_REORDER_WINDOW4:
158        res = ddWindow4(table,low,high);
159        break;
160    case CUDD_REORDER_WINDOW2_CONV:
161        res = ddWindowConv2(table,low,high);
162        break;
163    case CUDD_REORDER_WINDOW3_CONV:
164        res = ddWindowConv3(table,low,high);
165#ifdef DD_DEBUG
166        supposedOpt = table->keys - table->isolated;
167        res = ddWindow3(table,low,high);
168        if (table->keys - table->isolated != (unsigned) supposedOpt) {
169            (void) fprintf(table->err, "Convergence failed! (%d != %d)\n",
170                           table->keys - table->isolated, supposedOpt);
171        }
172#endif
173        break;
174    case CUDD_REORDER_WINDOW4_CONV:
175        res = ddWindowConv4(table,low,high);
176#ifdef DD_DEBUG
177        supposedOpt = table->keys - table->isolated;
178        res = ddWindow4(table,low,high);
179        if (table->keys - table->isolated != (unsigned) supposedOpt) {
180            (void) fprintf(table->err,"Convergence failed! (%d != %d)\n",
181                           table->keys - table->isolated, supposedOpt);
182        }
183#endif
184        break;
185    default: return(0);
186    }
187
188    return(res);
189
190} /* end of cuddWindowReorder */
191
192
193/*---------------------------------------------------------------------------*/
194/* Definition of static functions                                            */
195/*---------------------------------------------------------------------------*/
196
197/**Function********************************************************************
198
199  Synopsis    [Reorders by applying a sliding window of width 2.]
200
201  Description [Reorders by applying a sliding window of width 2.
202  Tries both permutations of the variables in a window
203  that slides from low to high.  Assumes that no dead nodes are
204  present.  Returns 1 in case of success; 0 otherwise.]
205
206  SideEffects [None]
207
208******************************************************************************/
209static int
210ddWindow2(
211  DdManager * table,
212  int  low,
213  int  high)
214{
215
216    int x;
217    int res;
218    int size;
219
220#ifdef DD_DEBUG
221    assert(low >= 0 && high < table->size);
222#endif
223
224    if (high-low < 1) return(0);
225
226    res = table->keys - table->isolated;
227    for (x = low; x < high; x++) {
228        size = res;
229        res = cuddSwapInPlace(table,x,x+1);
230        if (res == 0) return(0);
231        if (res >= size) { /* no improvement: undo permutation */
232            res = cuddSwapInPlace(table,x,x+1);
233            if (res == 0) return(0);
234        }
235#ifdef DD_STATS
236        if (res < size) {
237            (void) fprintf(table->out,"-");
238        } else {
239            (void) fprintf(table->out,"=");
240        }
241        fflush(table->out);
242#endif
243    }
244
245    return(1);
246
247} /* end of ddWindow2 */
248
249
250/**Function********************************************************************
251
252  Synopsis    [Reorders by repeatedly applying a sliding window of width 2.]
253
254  Description [Reorders by repeatedly applying a sliding window of width
255  2. Tries both permutations of the variables in a window
256  that slides from low to high.  Assumes that no dead nodes are
257  present.  Uses an event-driven approach to determine convergence.
258  Returns 1 in case of success; 0 otherwise.]
259
260  SideEffects [None]
261
262******************************************************************************/
263static int
264ddWindowConv2(
265  DdManager * table,
266  int  low,
267  int  high)
268{
269    int x;
270    int res;
271    int nwin;
272    int newevent;
273    int *events;
274    int size;
275
276#ifdef DD_DEBUG
277    assert(low >= 0 && high < table->size);
278#endif
279
280    if (high-low < 1) return(ddWindowConv2(table,low,high));
281
282    nwin = high-low;
283    events = ALLOC(int,nwin);
284    if (events == NULL) {
285        table->errorCode = CUDD_MEMORY_OUT;
286        return(0);
287    }
288    for (x=0; x<nwin; x++) {
289        events[x] = 1;
290    }
291
292    res = table->keys - table->isolated;
293    do {
294        newevent = 0;
295        for (x=0; x<nwin; x++) {
296            if (events[x]) {
297                size = res;
298                res = cuddSwapInPlace(table,x+low,x+low+1);
299                if (res == 0) {
300                    FREE(events);
301                    return(0);
302                }
303                if (res >= size) { /* no improvement: undo permutation */
304                    res = cuddSwapInPlace(table,x+low,x+low+1);
305                    if (res == 0) {
306                        FREE(events);
307                        return(0);
308                    }
309                }
310                if (res < size) {
311                    if (x < nwin-1)     events[x+1] = 1;
312                    if (x > 0)          events[x-1] = 1;
313                    newevent = 1;
314                }
315                events[x] = 0;
316#ifdef DD_STATS
317                if (res < size) {
318                    (void) fprintf(table->out,"-");
319                } else {
320                    (void) fprintf(table->out,"=");
321                }
322                fflush(table->out);
323#endif
324            }
325        }
326#ifdef DD_STATS
327        if (newevent) {
328            (void) fprintf(table->out,"|");
329            fflush(table->out);
330        }
331#endif
332    } while (newevent);
333
334    FREE(events);
335
336    return(1);
337
338} /* end of ddWindowConv3 */
339
340
341/**Function********************************************************************
342
343  Synopsis [Tries all the permutations of the three variables between
344  x and x+2 and retains the best.]
345
346  Description [Tries all the permutations of the three variables between
347  x and x+2 and retains the best. Assumes that no dead nodes are
348  present.  Returns the index of the best permutation (1-6) in case of
349  success; 0 otherwise.Assumes that no dead nodes are present.  Returns
350  the index of the best permutation (1-6) in case of success; 0
351  otherwise.]
352
353  SideEffects [None]
354
355******************************************************************************/
356static int
357ddPermuteWindow3(
358  DdManager * table,
359  int  x)
360{
361    int y,z;
362    int size,sizeNew;
363    int best;
364
365#ifdef DD_DEBUG
366    assert(table->dead == 0);
367    assert(x+2 < table->size);
368#endif
369
370    size = table->keys - table->isolated;
371    y = x+1; z = y+1;
372
373    /* The permutation pattern is:
374    ** (x,y)(y,z)
375    ** repeated three times to get all 3! = 6 permutations.
376    */
377#define ABC 1
378    best = ABC;
379
380#define BAC 2
381    sizeNew = cuddSwapInPlace(table,x,y);
382    if (sizeNew < size) {
383        if (sizeNew == 0) return(0);
384        best = BAC;
385        size = sizeNew;
386    }
387#define BCA 3
388    sizeNew = cuddSwapInPlace(table,y,z);
389    if (sizeNew < size) {
390        if (sizeNew == 0) return(0);
391        best = BCA;
392        size = sizeNew;
393    }
394#define CBA 4
395    sizeNew = cuddSwapInPlace(table,x,y);
396    if (sizeNew < size) {
397        if (sizeNew == 0) return(0);
398        best = CBA;
399        size = sizeNew;
400    }
401#define CAB 5
402    sizeNew = cuddSwapInPlace(table,y,z);
403    if (sizeNew < size) {
404        if (sizeNew == 0) return(0);
405        best = CAB;
406        size = sizeNew;
407    }
408#define ACB 6
409    sizeNew = cuddSwapInPlace(table,x,y);
410    if (sizeNew < size) {
411        if (sizeNew == 0) return(0);
412        best = ACB;
413        size = sizeNew;
414    }
415
416    /* Now take the shortest route to the best permuytation.
417    ** The initial permutation is ACB.
418    */
419    switch(best) {
420    case BCA: if (!cuddSwapInPlace(table,y,z)) return(0);
421    case CBA: if (!cuddSwapInPlace(table,x,y)) return(0);
422    case ABC: if (!cuddSwapInPlace(table,y,z)) return(0);
423    case ACB: break;
424    case BAC: if (!cuddSwapInPlace(table,y,z)) return(0);
425    case CAB: if (!cuddSwapInPlace(table,x,y)) return(0);
426               break;
427    default: return(0);
428    }
429
430#ifdef DD_DEBUG
431    assert(table->keys - table->isolated == (unsigned) size);
432#endif
433
434    return(best);
435
436} /* end of ddPermuteWindow3 */
437
438
439/**Function********************************************************************
440
441  Synopsis    [Reorders by applying a sliding window of width 3.]
442
443  Description [Reorders by applying a sliding window of width 3.
444  Tries all possible permutations to the variables in a
445  window that slides from low to high.  Assumes that no dead nodes are
446  present.  Returns 1 in case of success; 0 otherwise.]
447
448  SideEffects [None]
449
450******************************************************************************/
451static int
452ddWindow3(
453  DdManager * table,
454  int  low,
455  int  high)
456{
457
458    int x;
459    int res;
460
461#ifdef DD_DEBUG
462    assert(low >= 0 && high < table->size);
463#endif
464
465    if (high-low < 2) return(ddWindow2(table,low,high));
466
467    for (x = low; x+1 < high; x++) {
468        res = ddPermuteWindow3(table,x);
469        if (res == 0) return(0);
470#ifdef DD_STATS
471        if (res == ABC) {
472            (void) fprintf(table->out,"=");
473        } else {
474            (void) fprintf(table->out,"-");
475        }
476        fflush(table->out);
477#endif
478    }
479
480    return(1);
481
482} /* end of ddWindow3 */
483
484
485/**Function********************************************************************
486
487  Synopsis    [Reorders by repeatedly applying a sliding window of width 3.]
488
489  Description [Reorders by repeatedly applying a sliding window of width
490  3. Tries all possible permutations to the variables in a
491  window that slides from low to high.  Assumes that no dead nodes are
492  present.  Uses an event-driven approach to determine convergence.
493  Returns 1 in case of success; 0 otherwise.]
494
495  SideEffects [None]
496
497******************************************************************************/
498static int
499ddWindowConv3(
500  DdManager * table,
501  int  low,
502  int  high)
503{
504    int x;
505    int res;
506    int nwin;
507    int newevent;
508    int *events;
509
510#ifdef DD_DEBUG
511    assert(low >= 0 && high < table->size);
512#endif
513
514    if (high-low < 2) return(ddWindowConv2(table,low,high));
515
516    nwin = high-low-1;
517    events = ALLOC(int,nwin);
518    if (events == NULL) {
519        table->errorCode = CUDD_MEMORY_OUT;
520        return(0);
521    }
522    for (x=0; x<nwin; x++) {
523        events[x] = 1;
524    }
525
526    do {
527        newevent = 0;
528        for (x=0; x<nwin; x++) {
529            if (events[x]) {
530                res = ddPermuteWindow3(table,x+low);
531                switch (res) {
532                case ABC:
533                    break;
534                case BAC:
535                    if (x < nwin-1)     events[x+1] = 1;
536                    if (x > 1)          events[x-2] = 1;
537                    newevent = 1;
538                    break;
539                case BCA:
540                case CBA:
541                case CAB:
542                    if (x < nwin-2)     events[x+2] = 1;
543                    if (x < nwin-1)     events[x+1] = 1;
544                    if (x > 0)          events[x-1] = 1;
545                    if (x > 1)          events[x-2] = 1;
546                    newevent = 1;
547                    break;
548                case ACB:
549                    if (x < nwin-2)     events[x+2] = 1;
550                    if (x > 0)          events[x-1] = 1;
551                    newevent = 1;
552                    break;
553                default:
554                    FREE(events);
555                    return(0);
556                }
557                events[x] = 0;
558#ifdef DD_STATS
559                if (res == ABC) {
560                    (void) fprintf(table->out,"=");
561                } else {
562                    (void) fprintf(table->out,"-");
563                }
564                fflush(table->out);
565#endif
566            }
567        }
568#ifdef DD_STATS
569        if (newevent) {
570            (void) fprintf(table->out,"|");
571            fflush(table->out);
572        }
573#endif
574    } while (newevent);
575
576    FREE(events);
577
578    return(1);
579
580} /* end of ddWindowConv3 */
581
582
583/**Function********************************************************************
584
585  Synopsis [Tries all the permutations of the four variables between w
586  and w+3 and retains the best.]
587
588  Description [Tries all the permutations of the four variables between
589  w and w+3 and retains the best. Assumes that no dead nodes are
590  present.  Returns the index of the best permutation (1-24) in case of
591  success; 0 otherwise.]
592
593  SideEffects [None]
594
595******************************************************************************/
596static int
597ddPermuteWindow4(
598  DdManager * table,
599  int  w)
600{
601    int x,y,z;
602    int size,sizeNew;
603    int best;
604
605#ifdef DD_DEBUG
606    assert(table->dead == 0);
607    assert(w+3 < table->size);
608#endif
609
610    size = table->keys - table->isolated;
611    x = w+1; y = x+1; z = y+1;
612
613    /* The permutation pattern is:
614     * (w,x)(y,z)(w,x)(x,y)
615     * (y,z)(w,x)(y,z)(x,y)
616     * repeated three times to get all 4! = 24 permutations.
617     * This gives a hamiltonian circuit of Cayley's graph.
618     * The codes to the permutation are assigned in topological order.
619     * The permutations at lower distance from the final permutation are
620     * assigned lower codes. This way we can choose, between
621     * permutations that give the same size, one that requires the minimum
622     * number of swaps from the final permutation of the hamiltonian circuit.
623     * There is an exception to this rule: ABCD is given Code 1, to
624     * avoid oscillation when convergence is sought.
625     */
626#define ABCD 1
627    best = ABCD;
628
629#define BACD 7
630    sizeNew = cuddSwapInPlace(table,w,x);
631    if (sizeNew < size) {
632        if (sizeNew == 0) return(0);
633        best = BACD;
634        size = sizeNew;
635    }
636#define BADC 13
637    sizeNew = cuddSwapInPlace(table,y,z);
638    if (sizeNew < size) {
639        if (sizeNew == 0) return(0);
640        best = BADC;
641        size = sizeNew;
642    }
643#define ABDC 8
644    sizeNew = cuddSwapInPlace(table,w,x);
645    if (sizeNew < size || (sizeNew == size && ABDC < best)) {
646        if (sizeNew == 0) return(0);
647        best = ABDC;
648        size = sizeNew;
649    }
650#define ADBC 14
651    sizeNew = cuddSwapInPlace(table,x,y);
652    if (sizeNew < size) {
653        if (sizeNew == 0) return(0);
654        best = ADBC;
655        size = sizeNew;
656    }
657#define ADCB 9
658    sizeNew = cuddSwapInPlace(table,y,z);
659    if (sizeNew < size || (sizeNew == size && ADCB < best)) {
660        if (sizeNew == 0) return(0);
661        best = ADCB;
662        size = sizeNew;
663    }
664#define DACB 15
665    sizeNew = cuddSwapInPlace(table,w,x);
666    if (sizeNew < size) {
667        if (sizeNew == 0) return(0);
668        best = DACB;
669        size = sizeNew;
670    }
671#define DABC 20
672    sizeNew = cuddSwapInPlace(table,y,z);
673    if (sizeNew < size) {
674        if (sizeNew == 0) return(0);
675        best = DABC;
676        size = sizeNew;
677    }
678#define DBAC 23
679    sizeNew = cuddSwapInPlace(table,x,y);
680    if (sizeNew < size) {
681        if (sizeNew == 0) return(0);
682        best = DBAC;
683        size = sizeNew;
684    }
685#define BDAC 19
686    sizeNew = cuddSwapInPlace(table,w,x);
687    if (sizeNew < size || (sizeNew == size && BDAC < best)) {
688        if (sizeNew == 0) return(0);
689        best = BDAC;
690        size = sizeNew;
691    }
692#define BDCA 21
693    sizeNew = cuddSwapInPlace(table,y,z);
694    if (sizeNew < size || (sizeNew == size && BDCA < best)) {
695        if (sizeNew == 0) return(0);
696        best = BDCA;
697        size = sizeNew;
698    }
699#define DBCA 24
700    sizeNew = cuddSwapInPlace(table,w,x);
701    if (sizeNew < size) {
702        if (sizeNew == 0) return(0);
703        best = DBCA;
704        size = sizeNew;
705    }
706#define DCBA 22
707    sizeNew = cuddSwapInPlace(table,x,y);
708    if (sizeNew < size || (sizeNew == size && DCBA < best)) {
709        if (sizeNew == 0) return(0);
710        best = DCBA;
711        size = sizeNew;
712    }
713#define DCAB 18
714    sizeNew = cuddSwapInPlace(table,y,z);
715    if (sizeNew < size || (sizeNew == size && DCAB < best)) {
716        if (sizeNew == 0) return(0);
717        best = DCAB;
718        size = sizeNew;
719    }
720#define CDAB 12
721    sizeNew = cuddSwapInPlace(table,w,x);
722    if (sizeNew < size || (sizeNew == size && CDAB < best)) {
723        if (sizeNew == 0) return(0);
724        best = CDAB;
725        size = sizeNew;
726    }
727#define CDBA 17
728    sizeNew = cuddSwapInPlace(table,y,z);
729    if (sizeNew < size || (sizeNew == size && CDBA < best)) {
730        if (sizeNew == 0) return(0);
731        best = CDBA;
732        size = sizeNew;
733    }
734#define CBDA 11
735    sizeNew = cuddSwapInPlace(table,x,y);
736    if (sizeNew < size || (sizeNew == size && CBDA < best)) {
737        if (sizeNew == 0) return(0);
738        best = CBDA;
739        size = sizeNew;
740    }
741#define BCDA 16
742    sizeNew = cuddSwapInPlace(table,w,x);
743    if (sizeNew < size || (sizeNew == size && BCDA < best)) {
744        if (sizeNew == 0) return(0);
745        best = BCDA;
746        size = sizeNew;
747    }
748#define BCAD 10
749    sizeNew = cuddSwapInPlace(table,y,z);
750    if (sizeNew < size || (sizeNew == size && BCAD < best)) {
751        if (sizeNew == 0) return(0);
752        best = BCAD;
753        size = sizeNew;
754    }
755#define CBAD 5
756    sizeNew = cuddSwapInPlace(table,w,x);
757    if (sizeNew < size || (sizeNew == size && CBAD < best)) {
758        if (sizeNew == 0) return(0);
759        best = CBAD;
760        size = sizeNew;
761    }
762#define CABD 3
763    sizeNew = cuddSwapInPlace(table,x,y);
764    if (sizeNew < size || (sizeNew == size && CABD < best)) {
765        if (sizeNew == 0) return(0);
766        best = CABD;
767        size = sizeNew;
768    }
769#define CADB 6
770    sizeNew = cuddSwapInPlace(table,y,z);
771    if (sizeNew < size || (sizeNew == size && CADB < best)) {
772        if (sizeNew == 0) return(0);
773        best = CADB;
774        size = sizeNew;
775    }
776#define ACDB 4
777    sizeNew = cuddSwapInPlace(table,w,x);
778    if (sizeNew < size || (sizeNew == size && ACDB < best)) {
779        if (sizeNew == 0) return(0);
780        best = ACDB;
781        size = sizeNew;
782    }
783#define ACBD 2
784    sizeNew = cuddSwapInPlace(table,y,z);
785    if (sizeNew < size || (sizeNew == size && ACBD < best)) {
786        if (sizeNew == 0) return(0);
787        best = ACBD;
788        size = sizeNew;
789    }
790
791    /* Now take the shortest route to the best permutation.
792    ** The initial permutation is ACBD.
793    */
794    switch(best) {
795    case DBCA: if (!cuddSwapInPlace(table,y,z)) return(0);
796    case BDCA: if (!cuddSwapInPlace(table,x,y)) return(0);
797    case CDBA: if (!cuddSwapInPlace(table,w,x)) return(0);
798    case ADBC: if (!cuddSwapInPlace(table,y,z)) return(0);
799    case ABDC: if (!cuddSwapInPlace(table,x,y)) return(0);
800    case ACDB: if (!cuddSwapInPlace(table,y,z)) return(0);
801    case ACBD: break;
802    case DCBA: if (!cuddSwapInPlace(table,y,z)) return(0);
803    case BCDA: if (!cuddSwapInPlace(table,x,y)) return(0);
804    case CBDA: if (!cuddSwapInPlace(table,w,x)) return(0);
805               if (!cuddSwapInPlace(table,x,y)) return(0);
806               if (!cuddSwapInPlace(table,y,z)) return(0);
807               break;
808    case DBAC: if (!cuddSwapInPlace(table,x,y)) return(0);
809    case DCAB: if (!cuddSwapInPlace(table,w,x)) return(0);
810    case DACB: if (!cuddSwapInPlace(table,y,z)) return(0);
811    case BACD: if (!cuddSwapInPlace(table,x,y)) return(0);
812    case CABD: if (!cuddSwapInPlace(table,w,x)) return(0);
813               break;
814    case DABC: if (!cuddSwapInPlace(table,y,z)) return(0);
815    case BADC: if (!cuddSwapInPlace(table,x,y)) return(0);
816    case CADB: if (!cuddSwapInPlace(table,w,x)) return(0);
817               if (!cuddSwapInPlace(table,y,z)) return(0);
818               break;
819    case BDAC: if (!cuddSwapInPlace(table,x,y)) return(0);
820    case CDAB: if (!cuddSwapInPlace(table,w,x)) return(0);
821    case ADCB: if (!cuddSwapInPlace(table,y,z)) return(0);
822    case ABCD: if (!cuddSwapInPlace(table,x,y)) return(0);
823               break;
824    case BCAD: if (!cuddSwapInPlace(table,x,y)) return(0);
825    case CBAD: if (!cuddSwapInPlace(table,w,x)) return(0);
826               if (!cuddSwapInPlace(table,x,y)) return(0);
827               break;
828    default: return(0);
829    }
830
831#ifdef DD_DEBUG
832    assert(table->keys - table->isolated == (unsigned) size);
833#endif
834
835    return(best);
836
837} /* end of ddPermuteWindow4 */
838
839
840/**Function********************************************************************
841
842  Synopsis    [Reorders by applying a sliding window of width 4.]
843
844  Description [Reorders by applying a sliding window of width 4.
845  Tries all possible permutations to the variables in a
846  window that slides from low to high.  Assumes that no dead nodes are
847  present.  Returns 1 in case of success; 0 otherwise.]
848
849  SideEffects [None]
850
851******************************************************************************/
852static int
853ddWindow4(
854  DdManager * table,
855  int  low,
856  int  high)
857{
858
859    int w;
860    int res;
861
862#ifdef DD_DEBUG
863    assert(low >= 0 && high < table->size);
864#endif
865
866    if (high-low < 3) return(ddWindow3(table,low,high));
867
868    for (w = low; w+2 < high; w++) {
869        res = ddPermuteWindow4(table,w);
870        if (res == 0) return(0);
871#ifdef DD_STATS
872        if (res == ABCD) {
873            (void) fprintf(table->out,"=");
874        } else {
875            (void) fprintf(table->out,"-");
876        }
877        fflush(table->out);
878#endif
879    }
880
881    return(1);
882
883} /* end of ddWindow4 */
884
885
886/**Function********************************************************************
887
888  Synopsis    [Reorders by repeatedly applying a sliding window of width 4.]
889
890  Description [Reorders by repeatedly applying a sliding window of width
891  4. Tries all possible permutations to the variables in a
892  window that slides from low to high.  Assumes that no dead nodes are
893  present.  Uses an event-driven approach to determine convergence.
894  Returns 1 in case of success; 0 otherwise.]
895
896  SideEffects [None]
897
898******************************************************************************/
899static int
900ddWindowConv4(
901  DdManager * table,
902  int  low,
903  int  high)
904{
905    int x;
906    int res;
907    int nwin;
908    int newevent;
909    int *events;
910
911#ifdef DD_DEBUG
912    assert(low >= 0 && high < table->size);
913#endif
914
915    if (high-low < 3) return(ddWindowConv3(table,low,high));
916
917    nwin = high-low-2;
918    events = ALLOC(int,nwin);
919    if (events == NULL) {
920        table->errorCode = CUDD_MEMORY_OUT;
921        return(0);
922    }
923    for (x=0; x<nwin; x++) {
924        events[x] = 1;
925    }
926
927    do {
928        newevent = 0;
929        for (x=0; x<nwin; x++) {
930            if (events[x]) {
931                res = ddPermuteWindow4(table,x+low);
932                switch (res) {
933                case ABCD:
934                    break;
935                case BACD:
936                    if (x < nwin-1)     events[x+1] = 1;
937                    if (x > 2)          events[x-3] = 1;
938                    newevent = 1;
939                    break;
940                case BADC:
941                    if (x < nwin-3)     events[x+3] = 1;
942                    if (x < nwin-1)     events[x+1] = 1;
943                    if (x > 0)          events[x-1] = 1;
944                    if (x > 2)          events[x-3] = 1;
945                    newevent = 1;
946                    break;
947                case ABDC:
948                    if (x < nwin-3)     events[x+3] = 1;
949                    if (x > 0)          events[x-1] = 1;
950                    newevent = 1;
951                    break;
952                case ADBC:
953                case ADCB:
954                case ACDB:
955                    if (x < nwin-3)     events[x+3] = 1;
956                    if (x < nwin-2)     events[x+2] = 1;
957                    if (x > 0)          events[x-1] = 1;
958                    if (x > 1)          events[x-2] = 1;
959                    newevent = 1;
960                    break;
961                case DACB:
962                case DABC:
963                case DBAC:
964                case BDAC:
965                case BDCA:
966                case DBCA:
967                case DCBA:
968                case DCAB:
969                case CDAB:
970                case CDBA:
971                case CBDA:
972                case BCDA:
973                case CADB:
974                    if (x < nwin-3)     events[x+3] = 1;
975                    if (x < nwin-2)     events[x+2] = 1;
976                    if (x < nwin-1)     events[x+1] = 1;
977                    if (x > 0)          events[x-1] = 1;
978                    if (x > 1)          events[x-2] = 1;
979                    if (x > 2)          events[x-3] = 1;
980                    newevent = 1;
981                    break;
982                case BCAD:
983                case CBAD:
984                case CABD:
985                    if (x < nwin-2)     events[x+2] = 1;
986                    if (x < nwin-1)     events[x+1] = 1;
987                    if (x > 1)          events[x-2] = 1;
988                    if (x > 2)          events[x-3] = 1;
989                    newevent = 1;
990                    break;
991                case ACBD:
992                    if (x < nwin-2)     events[x+2] = 1;
993                    if (x > 1)          events[x-2] = 1;
994                    newevent = 1;
995                    break;
996                default:
997                    FREE(events);
998                    return(0);
999                }
1000                events[x] = 0;
1001#ifdef DD_STATS
1002                if (res == ABCD) {
1003                    (void) fprintf(table->out,"=");
1004                } else {
1005                    (void) fprintf(table->out,"-");
1006                }
1007                fflush(table->out);
1008#endif
1009            }
1010        }
1011#ifdef DD_STATS
1012        if (newevent) {
1013            (void) fprintf(table->out,"|");
1014            fflush(table->out);
1015        }
1016#endif
1017    } while (newevent);
1018
1019    FREE(events);
1020
1021    return(1);
1022
1023} /* end of ddWindowConv4 */
Note: See TracBrowser for help on using the repository browser.