SVF
cuddWindow.c
Go to the documentation of this file.
1 
61 #include "CUDD/util.h"
62 #include "CUDD/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
84 static char rcsid[] DD_UNUSED = "$Id: cuddWindow.c,v 1.15 2012/02/05 01:07:19 fabio Exp $";
85 #endif
86 
87 #ifdef DD_STATS
88 extern int ddTotalNumberSwapping;
89 extern int ddTotalNISwaps;
90 #endif
91 
92 /*---------------------------------------------------------------------------*/
93 /* Macro declarations */
94 /*---------------------------------------------------------------------------*/
95 
96 
99 /*---------------------------------------------------------------------------*/
100 /* Static function prototypes */
101 /*---------------------------------------------------------------------------*/
102 
103 static int ddWindow2 (DdManager *table, int low, int high);
104 static int ddWindowConv2 (DdManager *table, int low, int high);
105 static int ddPermuteWindow3 (DdManager *table, int x);
106 static int ddWindow3 (DdManager *table, int low, int high);
107 static int ddWindowConv3 (DdManager *table, int low, int high);
108 static int ddPermuteWindow4 (DdManager *table, int w);
109 static int ddWindow4 (DdManager *table, int low, int high);
110 static int ddWindowConv4 (DdManager *table, int low, int high);
111 
115 /*---------------------------------------------------------------------------*/
116 /* Definition of exported functions */
117 /*---------------------------------------------------------------------------*/
118 
119 /*---------------------------------------------------------------------------*/
120 /* Definition of internal functions */
121 /*---------------------------------------------------------------------------*/
122 
123 
137 int
138 cuddWindowReorder(
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 
209 static int
210 ddWindow2(
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 
263 static int
264 ddWindowConv2(
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 
356 static int
357 ddPermuteWindow3(
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 
451 static int
452 ddWindow3(
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 
498 static int
499 ddWindowConv3(
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 
596 static int
597 ddPermuteWindow4(
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 
852 static int
853 ddWindow4(
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 
899 static int
900 ddWindowConv4(
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 */
ddPermuteWindow3
static int ddPermuteWindow3(DdManager *table, int x)
Definition: cuddWindow.c:357
CADB
#define CADB
DACB
#define DACB
ddWindow2
static int ddWindow2(DdManager *table, int low, int high)
Definition: cuddWindow.c:210
ddWindow4
static int ddWindow4(DdManager *table, int low, int high)
Definition: cuddWindow.c:853
FREE
#define FREE(obj)
Definition: util.h:80
ddWindow3
static int ddWindow3(DdManager *table, int low, int high)
Definition: cuddWindow.c:452
assert
#define assert(ex)
Definition: util.h:141
DdManager::size
int size
Definition: cuddInt.h:345
BCAD
#define BCAD
BAC
#define BAC
ddWindowConv2
static int ddWindowConv2(DdManager *table, int low, int high)
Definition: cuddWindow.c:264
DdManager::err
FILE * err
Definition: cuddInt.h:424
ddWindowConv4
static int ddWindowConv4(DdManager *table, int low, int high)
Definition: cuddWindow.c:900
ADCB
#define ADCB
ddPermuteWindow4
static int ddPermuteWindow4(DdManager *table, int w)
Definition: cuddWindow.c:597
DCBA
#define DCBA
ABDC
#define ABDC
cuddWindowReorder
int cuddWindowReorder(DdManager *table, int low, int high, Cudd_ReorderingType submethod)
Definition: cuddWindow.c:138
DdManager::dead
unsigned int dead
Definition: cuddInt.h:355
ddTotalNumberSwapping
int ddTotalNumberSwapping
Definition: cuddReorder.c:103
BCA
#define BCA
BDCA
#define BDCA
CAB
#define CAB
DCAB
#define DCAB
DdManager::keys
unsigned int keys
Definition: cuddInt.h:353
ALLOC
#define ALLOC(type, num)
Definition: util.h:76
DdManager::out
FILE * out
Definition: cuddInt.h:423
BCDA
#define BCDA
CDBA
#define CDBA
ACBD
#define ACBD
ADBC
#define ADBC
CBDA
#define CBDA
DBAC
#define DBAC
ABC
#define ABC
BDAC
#define BDAC
CDAB
#define CDAB
DBCA
#define DBCA
CBAD
#define CBAD
cuddSwapInPlace
int cuddSwapInPlace(DdManager *table, int x, int y)
Definition: cuddReorder.c:760
ACB
#define ACB
CABD
#define CABD
DdManager::isolated
int isolated
Definition: cuddInt.h:368
ABCD
#define ABCD
BACD
#define BACD
BADC
#define BADC
CBA
#define CBA
Cudd_ReorderingType
Cudd_ReorderingType
Definition: cudd.h:147
DdManager::errorCode
Cudd_ErrorType errorCode
Definition: cuddInt.h:425
ddWindowConv3
static int ddWindowConv3(DdManager *table, int low, int high)
Definition: cuddWindow.c:499
ACDB
#define ACDB
DD_UNUSED
static char rcsid [] DD_UNUSED
Definition: cuddWindow.c:84
DABC
#define DABC
Generated by   doxygen 1.8.13