abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Macros | Functions | Variables
cuddWindow.c File Reference
#include "misc/util/util_hack.h"
#include "cuddInt.h"

Go to the source code of this file.

Macros

#define ABC   1
 
#define BAC   2
 
#define BCA   3
 
#define CBA   4
 
#define CAB   5
 
#define ACB   6
 
#define ABCD   1
 
#define BACD   7
 
#define BADC   13
 
#define ABDC   8
 
#define ADBC   14
 
#define ADCB   9
 
#define DACB   15
 
#define DABC   20
 
#define DBAC   23
 
#define BDAC   19
 
#define BDCA   21
 
#define DBCA   24
 
#define DCBA   22
 
#define DCAB   18
 
#define CDAB   12
 
#define CDBA   17
 
#define CBDA   11
 
#define BCDA   16
 
#define BCAD   10
 
#define CBAD   5
 
#define CABD   3
 
#define CADB   6
 
#define ACDB   4
 
#define ACBD   2
 

Functions

static int ddWindow2 (DdManager *table, int low, int high)
 
static int ddWindowConv2 (DdManager *table, int low, int high)
 
static int ddPermuteWindow3 (DdManager *table, int x)
 
static int ddWindow3 (DdManager *table, int low, int high)
 
static int ddWindowConv3 (DdManager *table, int low, int high)
 
static int ddPermuteWindow4 (DdManager *table, int w)
 
static int ddWindow4 (DdManager *table, int low, int high)
 
static int ddWindowConv4 (DdManager *table, int low, int high)
 
int cuddWindowReorder (DdManager *table, int low, int high, Cudd_ReorderingType submethod)
 

Variables

static
ABC_NAMESPACE_IMPL_START char
rcsid[] 		DD_UNUSED = "$Id: cuddWindow.c,v 1.14 2009/02/20 02:14:58 fabio Exp $"
 

Macro Definition Documentation

#define ABC   1
#define ABCD   1
#define ABDC   8
#define ACB   6
#define ACBD   2
#define ACDB   4
#define ADBC   14
#define ADCB   9
#define BAC   2
#define BACD   7
#define BADC   13
#define BCA   3
#define BCAD   10
#define BCDA   16
#define BDAC   19
#define BDCA   21
#define CAB   5
#define CABD   3
#define CADB   6
#define CBA   4
#define CBAD   5
#define CBDA   11
#define CDAB   12
#define CDBA   17
#define DABC   20
#define DACB   15
#define DBAC   23
#define DBCA   24
#define DCAB   18
#define DCBA   22

Function Documentation

int cuddWindowReorder ( DdManager *  table,
int  low,
int  high,
Cudd_ReorderingType  submethod 
)

AutomaticEnd Function********************************************************************

Synopsis [Reorders by applying the method of the sliding window.]

Description [Reorders by applying the method of the sliding window. Tries all possible permutations to the variables in a window that slides from low to high. The size of the window is determined by submethod. Assumes that no dead nodes are present. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

Definition at line 142 of file cuddWindow.c.

147 {
148 
149  int res;
150 #ifdef DD_DEBUG
151  int supposedOpt;
152 #endif
153 
154  switch (submethod) {
155  case CUDD_REORDER_WINDOW2:
156  res = ddWindow2(table,low,high);
157  break;
158  case CUDD_REORDER_WINDOW3:
159  res = ddWindow3(table,low,high);
160  break;
161  case CUDD_REORDER_WINDOW4:
162  res = ddWindow4(table,low,high);
163  break;
164  case CUDD_REORDER_WINDOW2_CONV:
165  res = ddWindowConv2(table,low,high);
166  break;
167  case CUDD_REORDER_WINDOW3_CONV:
168  res = ddWindowConv3(table,low,high);
169 #ifdef DD_DEBUG
170  supposedOpt = table->keys - table->isolated;
171  res = ddWindow3(table,low,high);
172  if (table->keys - table->isolated != (unsigned) supposedOpt) {
173  (void) fprintf(table->err, "Convergence failed! (%d != %d)\n",
174  table->keys - table->isolated, supposedOpt);
175  }
176 #endif
177  break;
178  case CUDD_REORDER_WINDOW4_CONV:
179  res = ddWindowConv4(table,low,high);
180 #ifdef DD_DEBUG
181  supposedOpt = table->keys - table->isolated;
182  res = ddWindow4(table,low,high);
183  if (table->keys - table->isolated != (unsigned) supposedOpt) {
184  (void) fprintf(table->err,"Convergence failed! (%d != %d)\n",
185  table->keys - table->isolated, supposedOpt);
186  }
187 #endif
188  break;
189  default: return(0);
190  }
191 
192  return(res);
193 
194 } /* end of cuddWindowReorder */
ddWindow2
static int ddWindow2(DdManager *table, int low, int high)
Definition: cuddWindow.c:214
ddWindow4
static int ddWindow4(DdManager *table, int low, int high)
Definition: cuddWindow.c:857
ddWindow3
static int ddWindow3(DdManager *table, int low, int high)
Definition: cuddWindow.c:456
ddWindowConv2
static int ddWindowConv2(DdManager *table, int low, int high)
Definition: cuddWindow.c:268
DdManager::err
FILE * err
Definition: cuddInt.h:442
ddWindowConv4
static int ddWindowConv4(DdManager *table, int low, int high)
Definition: cuddWindow.c:904
DdManager::keys
unsigned int keys
Definition: cuddInt.h:369
DdManager::isolated
int isolated
Definition: cuddInt.h:385
ddWindowConv3
static int ddWindowConv3(DdManager *table, int low, int high)
Definition: cuddWindow.c:503
static int ddPermuteWindow3 ( DdManager *  table,
int  x 
)
static

Function********************************************************************

Synopsis [Tries all the permutations of the three variables between x and x+2 and retains the best.]

Description [Tries all the permutations of the three variables between x and x+2 and retains the best. Assumes that no dead nodes are present. Returns the index of the best permutation (1-6) in case of success; 0 otherwise.Assumes that no dead nodes are present. Returns the index of the best permutation (1-6) in case of success; 0 otherwise.]

SideEffects [None]

Definition at line 361 of file cuddWindow.c.

364 {
365  int y,z;
366  int size,sizeNew;
367  int best;
368 
369 #ifdef DD_DEBUG
370  assert(table->dead == 0);
371  assert(x+2 < table->size);
372 #endif
373 
374  size = table->keys - table->isolated;
375  y = x+1; z = y+1;
376 
377  /* The permutation pattern is:
378  ** (x,y)(y,z)
379  ** repeated three times to get all 3! = 6 permutations.
380  */
381 #define ABC 1
382  best = ABC;
383 
384 #define BAC 2
385  sizeNew = cuddSwapInPlace(table,x,y);
386  if (sizeNew < size) {
387  if (sizeNew == 0) return(0);
388  best = BAC;
389  size = sizeNew;
390  }
391 #define BCA 3
392  sizeNew = cuddSwapInPlace(table,y,z);
393  if (sizeNew < size) {
394  if (sizeNew == 0) return(0);
395  best = BCA;
396  size = sizeNew;
397  }
398 #define CBA 4
399  sizeNew = cuddSwapInPlace(table,x,y);
400  if (sizeNew < size) {
401  if (sizeNew == 0) return(0);
402  best = CBA;
403  size = sizeNew;
404  }
405 #define CAB 5
406  sizeNew = cuddSwapInPlace(table,y,z);
407  if (sizeNew < size) {
408  if (sizeNew == 0) return(0);
409  best = CAB;
410  size = sizeNew;
411  }
412 #define ACB 6
413  sizeNew = cuddSwapInPlace(table,x,y);
414  if (sizeNew < size) {
415  if (sizeNew == 0) return(0);
416  best = ACB;
417  size = sizeNew;
418  }
419 
420  /* Now take the shortest route to the best permuytation.
421  ** The initial permutation is ACB.
422  */
423  switch(best) {
424  case BCA: if (!cuddSwapInPlace(table,y,z)) return(0);
425  case CBA: if (!cuddSwapInPlace(table,x,y)) return(0);
426  case ABC: if (!cuddSwapInPlace(table,y,z)) return(0);
427  case ACB: break;
428  case BAC: if (!cuddSwapInPlace(table,y,z)) return(0);
429  case CAB: if (!cuddSwapInPlace(table,x,y)) return(0);
430  break;
431  default: return(0);
432  }
433 
434 #ifdef DD_DEBUG
435  assert(table->keys - table->isolated == (unsigned) size);
436 #endif
437 
438  return(best);
439 
440 } /* end of ddPermuteWindow3 */
DdManager::size
int size
Definition: cuddInt.h:361
BAC
#define BAC
DdManager::dead
unsigned int dead
Definition: cuddInt.h:371
BCA
#define BCA
CAB
#define CAB
DdManager::keys
unsigned int keys
Definition: cuddInt.h:369
size
static int size
Definition: cuddSign.c:86
ABC
#define ABC
cuddSwapInPlace
int cuddSwapInPlace(DdManager *table, int x, int y)
Definition: cuddReorder.c:761
ACB
#define ACB
assert
#define assert(ex)
Definition: util_old.h:213
DdManager::isolated
int isolated
Definition: cuddInt.h:385
pyabc_split.best
best
Definition: pyabc_split.py:400
CBA
#define CBA
static int ddPermuteWindow4 ( DdManager *  table,
int  w 
)
static

Function********************************************************************

Synopsis [Tries all the permutations of the four variables between w and w+3 and retains the best.]

Description [Tries all the permutations of the four variables between w and w+3 and retains the best. Assumes that no dead nodes are present. Returns the index of the best permutation (1-24) in case of success; 0 otherwise.]

SideEffects [None]

Definition at line 601 of file cuddWindow.c.

604 {
605  int x,y,z;
606  int size,sizeNew;
607  int best;
608 
609 #ifdef DD_DEBUG
610  assert(table->dead == 0);
611  assert(w+3 < table->size);
612 #endif
613 
614  size = table->keys - table->isolated;
615  x = w+1; y = x+1; z = y+1;
616 
617  /* The permutation pattern is:
618  * (w,x)(y,z)(w,x)(x,y)
619  * (y,z)(w,x)(y,z)(x,y)
620  * repeated three times to get all 4! = 24 permutations.
621  * This gives a hamiltonian circuit of Cayley's graph.
622  * The codes to the permutation are assigned in topological order.
623  * The permutations at lower distance from the final permutation are
624  * assigned lower codes. This way we can choose, between
625  * permutations that give the same size, one that requires the minimum
626  * number of swaps from the final permutation of the hamiltonian circuit.
627  * There is an exception to this rule: ABCD is given Code 1, to
628  * avoid oscillation when convergence is sought.
629  */
630 #define ABCD 1
631  best = ABCD;
632 
633 #define BACD 7
634  sizeNew = cuddSwapInPlace(table,w,x);
635  if (sizeNew < size) {
636  if (sizeNew == 0) return(0);
637  best = BACD;
638  size = sizeNew;
639  }
640 #define BADC 13
641  sizeNew = cuddSwapInPlace(table,y,z);
642  if (sizeNew < size) {
643  if (sizeNew == 0) return(0);
644  best = BADC;
645  size = sizeNew;
646  }
647 #define ABDC 8
648  sizeNew = cuddSwapInPlace(table,w,x);
649  if (sizeNew < size || (sizeNew == size && ABDC < best)) {
650  if (sizeNew == 0) return(0);
651  best = ABDC;
652  size = sizeNew;
653  }
654 #define ADBC 14
655  sizeNew = cuddSwapInPlace(table,x,y);
656  if (sizeNew < size) {
657  if (sizeNew == 0) return(0);
658  best = ADBC;
659  size = sizeNew;
660  }
661 #define ADCB 9
662  sizeNew = cuddSwapInPlace(table,y,z);
663  if (sizeNew < size || (sizeNew == size && ADCB < best)) {
664  if (sizeNew == 0) return(0);
665  best = ADCB;
666  size = sizeNew;
667  }
668 #define DACB 15
669  sizeNew = cuddSwapInPlace(table,w,x);
670  if (sizeNew < size) {
671  if (sizeNew == 0) return(0);
672  best = DACB;
673  size = sizeNew;
674  }
675 #define DABC 20
676  sizeNew = cuddSwapInPlace(table,y,z);
677  if (sizeNew < size) {
678  if (sizeNew == 0) return(0);
679  best = DABC;
680  size = sizeNew;
681  }
682 #define DBAC 23
683  sizeNew = cuddSwapInPlace(table,x,y);
684  if (sizeNew < size) {
685  if (sizeNew == 0) return(0);
686  best = DBAC;
687  size = sizeNew;
688  }
689 #define BDAC 19
690  sizeNew = cuddSwapInPlace(table,w,x);
691  if (sizeNew < size || (sizeNew == size && BDAC < best)) {
692  if (sizeNew == 0) return(0);
693  best = BDAC;
694  size = sizeNew;
695  }
696 #define BDCA 21
697  sizeNew = cuddSwapInPlace(table,y,z);
698  if (sizeNew < size || (sizeNew == size && BDCA < best)) {
699  if (sizeNew == 0) return(0);
700  best = BDCA;
701  size = sizeNew;
702  }
703 #define DBCA 24
704  sizeNew = cuddSwapInPlace(table,w,x);
705  if (sizeNew < size) {
706  if (sizeNew == 0) return(0);
707  best = DBCA;
708  size = sizeNew;
709  }
710 #define DCBA 22
711  sizeNew = cuddSwapInPlace(table,x,y);
712  if (sizeNew < size || (sizeNew == size && DCBA < best)) {
713  if (sizeNew == 0) return(0);
714  best = DCBA;
715  size = sizeNew;
716  }
717 #define DCAB 18
718  sizeNew = cuddSwapInPlace(table,y,z);
719  if (sizeNew < size || (sizeNew == size && DCAB < best)) {
720  if (sizeNew == 0) return(0);
721  best = DCAB;
722  size = sizeNew;
723  }
724 #define CDAB 12
725  sizeNew = cuddSwapInPlace(table,w,x);
726  if (sizeNew < size || (sizeNew == size && CDAB < best)) {
727  if (sizeNew == 0) return(0);
728  best = CDAB;
729  size = sizeNew;
730  }
731 #define CDBA 17
732  sizeNew = cuddSwapInPlace(table,y,z);
733  if (sizeNew < size || (sizeNew == size && CDBA < best)) {
734  if (sizeNew == 0) return(0);
735  best = CDBA;
736  size = sizeNew;
737  }
738 #define CBDA 11
739  sizeNew = cuddSwapInPlace(table,x,y);
740  if (sizeNew < size || (sizeNew == size && CBDA < best)) {
741  if (sizeNew == 0) return(0);
742  best = CBDA;
743  size = sizeNew;
744  }
745 #define BCDA 16
746  sizeNew = cuddSwapInPlace(table,w,x);
747  if (sizeNew < size || (sizeNew == size && BCDA < best)) {
748  if (sizeNew == 0) return(0);
749  best = BCDA;
750  size = sizeNew;
751  }
752 #define BCAD 10
753  sizeNew = cuddSwapInPlace(table,y,z);
754  if (sizeNew < size || (sizeNew == size && BCAD < best)) {
755  if (sizeNew == 0) return(0);
756  best = BCAD;
757  size = sizeNew;
758  }
759 #define CBAD 5
760  sizeNew = cuddSwapInPlace(table,w,x);
761  if (sizeNew < size || (sizeNew == size && CBAD < best)) {
762  if (sizeNew == 0) return(0);
763  best = CBAD;
764  size = sizeNew;
765  }
766 #define CABD 3
767  sizeNew = cuddSwapInPlace(table,x,y);
768  if (sizeNew < size || (sizeNew == size && CABD < best)) {
769  if (sizeNew == 0) return(0);
770  best = CABD;
771  size = sizeNew;
772  }
773 #define CADB 6
774  sizeNew = cuddSwapInPlace(table,y,z);
775  if (sizeNew < size || (sizeNew == size && CADB < best)) {
776  if (sizeNew == 0) return(0);
777  best = CADB;
778  size = sizeNew;
779  }
780 #define ACDB 4
781  sizeNew = cuddSwapInPlace(table,w,x);
782  if (sizeNew < size || (sizeNew == size && ACDB < best)) {
783  if (sizeNew == 0) return(0);
784  best = ACDB;
785  size = sizeNew;
786  }
787 #define ACBD 2
788  sizeNew = cuddSwapInPlace(table,y,z);
789  if (sizeNew < size || (sizeNew == size && ACBD < best)) {
790  if (sizeNew == 0) return(0);
791  best = ACBD;
792  size = sizeNew;
793  }
794 
795  /* Now take the shortest route to the best permutation.
796  ** The initial permutation is ACBD.
797  */
798  switch(best) {
799  case DBCA: if (!cuddSwapInPlace(table,y,z)) return(0);
800  case BDCA: if (!cuddSwapInPlace(table,x,y)) return(0);
801  case CDBA: if (!cuddSwapInPlace(table,w,x)) return(0);
802  case ADBC: if (!cuddSwapInPlace(table,y,z)) return(0);
803  case ABDC: if (!cuddSwapInPlace(table,x,y)) return(0);
804  case ACDB: if (!cuddSwapInPlace(table,y,z)) return(0);
805  case ACBD: break;
806  case DCBA: if (!cuddSwapInPlace(table,y,z)) return(0);
807  case BCDA: if (!cuddSwapInPlace(table,x,y)) return(0);
808  case CBDA: if (!cuddSwapInPlace(table,w,x)) return(0);
809  if (!cuddSwapInPlace(table,x,y)) return(0);
810  if (!cuddSwapInPlace(table,y,z)) return(0);
811  break;
812  case DBAC: if (!cuddSwapInPlace(table,x,y)) return(0);
813  case DCAB: if (!cuddSwapInPlace(table,w,x)) return(0);
814  case DACB: if (!cuddSwapInPlace(table,y,z)) return(0);
815  case BACD: if (!cuddSwapInPlace(table,x,y)) return(0);
816  case CABD: if (!cuddSwapInPlace(table,w,x)) return(0);
817  break;
818  case DABC: if (!cuddSwapInPlace(table,y,z)) return(0);
819  case BADC: if (!cuddSwapInPlace(table,x,y)) return(0);
820  case CADB: if (!cuddSwapInPlace(table,w,x)) return(0);
821  if (!cuddSwapInPlace(table,y,z)) return(0);
822  break;
823  case BDAC: if (!cuddSwapInPlace(table,x,y)) return(0);
824  case CDAB: if (!cuddSwapInPlace(table,w,x)) return(0);
825  case ADCB: if (!cuddSwapInPlace(table,y,z)) return(0);
826  case ABCD: if (!cuddSwapInPlace(table,x,y)) return(0);
827  break;
828  case BCAD: if (!cuddSwapInPlace(table,x,y)) return(0);
829  case CBAD: if (!cuddSwapInPlace(table,w,x)) return(0);
830  if (!cuddSwapInPlace(table,x,y)) return(0);
831  break;
832  default: return(0);
833  }
834 
835 #ifdef DD_DEBUG
836  assert(table->keys - table->isolated == (unsigned) size);
837 #endif
838 
839  return(best);
840 
841 } /* end of ddPermuteWindow4 */
CADB
#define CADB
DACB
#define DACB
DdManager::size
int size
Definition: cuddInt.h:361
BCAD
#define BCAD
ADCB
#define ADCB
DCBA
#define DCBA
ABDC
#define ABDC
DdManager::dead
unsigned int dead
Definition: cuddInt.h:371
BDCA
#define BDCA
DCAB
#define DCAB
DdManager::keys
unsigned int keys
Definition: cuddInt.h:369
BCDA
#define BCDA
CDBA
#define CDBA
ACBD
#define ACBD
ADBC
#define ADBC
CBDA
#define CBDA
size
static int size
Definition: cuddSign.c:86
DBAC
#define DBAC
BDAC
#define BDAC
CDAB
#define CDAB
DBCA
#define DBCA
CBAD
#define CBAD
cuddSwapInPlace
int cuddSwapInPlace(DdManager *table, int x, int y)
Definition: cuddReorder.c:761
CABD
#define CABD
assert
#define assert(ex)
Definition: util_old.h:213
DdManager::isolated
int isolated
Definition: cuddInt.h:385
ABCD
#define ABCD
BACD
#define BACD
pyabc_split.best
best
Definition: pyabc_split.py:400
BADC
#define BADC
ACDB
#define ACDB
DABC
#define DABC
static int ddWindow2 ( DdManager *  table,
int  low,
int  high 
)
static

AutomaticStart

Function********************************************************************

Synopsis [Reorders by applying a sliding window of width 2.]

Description [Reorders by applying a sliding window of width 2. Tries both permutations of the variables in a window that slides from low to high. Assumes that no dead nodes are present. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

Definition at line 214 of file cuddWindow.c.

218 {
219 
220  int x;
221  int res;
222  int size;
223 
224 #ifdef DD_DEBUG
225  assert(low >= 0 && high < table->size);
226 #endif
227 
228  if (high-low < 1) return(0);
229 
230  res = table->keys - table->isolated;
231  for (x = low; x < high; x++) {
232  size = res;
233  res = cuddSwapInPlace(table,x,x+1);
234  if (res == 0) return(0);
235  if (res >= size) { /* no improvement: undo permutation */
236  res = cuddSwapInPlace(table,x,x+1);
237  if (res == 0) return(0);
238  }
239 #ifdef DD_STATS
240  if (res < size) {
241  (void) fprintf(table->out,"-");
242  } else {
243  (void) fprintf(table->out,"=");
244  }
245  fflush(table->out);
246 #endif
247  }
248 
249  return(1);
250 
251 } /* end of ddWindow2 */
DdManager::keys
unsigned int keys
Definition: cuddInt.h:369
DdManager::out
FILE * out
Definition: cuddInt.h:441
size
static int size
Definition: cuddSign.c:86
cuddSwapInPlace
int cuddSwapInPlace(DdManager *table, int x, int y)
Definition: cuddReorder.c:761
assert
#define assert(ex)
Definition: util_old.h:213
DdManager::isolated
int isolated
Definition: cuddInt.h:385
static int ddWindow3 ( DdManager *  table,
int  low,
int  high 
)
static

Function********************************************************************

Synopsis [Reorders by applying a sliding window of width 3.]

Description [Reorders by applying a sliding window of width 3. Tries all possible permutations to the variables in a window that slides from low to high. Assumes that no dead nodes are present. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

Definition at line 456 of file cuddWindow.c.

460 {
461 
462  int x;
463  int res;
464 
465 #ifdef DD_DEBUG
466  assert(low >= 0 && high < table->size);
467 #endif
468 
469  if (high-low < 2) return(ddWindow2(table,low,high));
470 
471  for (x = low; x+1 < high; x++) {
472  res = ddPermuteWindow3(table,x);
473  if (res == 0) return(0);
474 #ifdef DD_STATS
475  if (res == ABC) {
476  (void) fprintf(table->out,"=");
477  } else {
478  (void) fprintf(table->out,"-");
479  }
480  fflush(table->out);
481 #endif
482  }
483 
484  return(1);
485 
486 } /* end of ddWindow3 */
ddPermuteWindow3
static int ddPermuteWindow3(DdManager *table, int x)
Definition: cuddWindow.c:361
ddWindow2
static int ddWindow2(DdManager *table, int low, int high)
Definition: cuddWindow.c:214
DdManager::out
FILE * out
Definition: cuddInt.h:441
size
static int size
Definition: cuddSign.c:86
ABC
#define ABC
assert
#define assert(ex)
Definition: util_old.h:213
static int ddWindow4 ( DdManager *  table,
int  low,
int  high 
)
static

Function********************************************************************

Synopsis [Reorders by applying a sliding window of width 4.]

Description [Reorders by applying a sliding window of width 4. Tries all possible permutations to the variables in a window that slides from low to high. Assumes that no dead nodes are present. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

Definition at line 857 of file cuddWindow.c.

861 {
862 
863  int w;
864  int res;
865 
866 #ifdef DD_DEBUG
867  assert(low >= 0 && high < table->size);
868 #endif
869 
870  if (high-low < 3) return(ddWindow3(table,low,high));
871 
872  for (w = low; w+2 < high; w++) {
873  res = ddPermuteWindow4(table,w);
874  if (res == 0) return(0);
875 #ifdef DD_STATS
876  if (res == ABCD) {
877  (void) fprintf(table->out,"=");
878  } else {
879  (void) fprintf(table->out,"-");
880  }
881  fflush(table->out);
882 #endif
883  }
884 
885  return(1);
886 
887 } /* end of ddWindow4 */
ddWindow3
static int ddWindow3(DdManager *table, int low, int high)
Definition: cuddWindow.c:456
ddPermuteWindow4
static int ddPermuteWindow4(DdManager *table, int w)
Definition: cuddWindow.c:601
DdManager::out
FILE * out
Definition: cuddInt.h:441
size
static int size
Definition: cuddSign.c:86
assert
#define assert(ex)
Definition: util_old.h:213
ABCD
#define ABCD
static int ddWindowConv2 ( DdManager *  table,
int  low,
int  high 
)
static

Function********************************************************************

Synopsis [Reorders by repeatedly applying a sliding window of width 2.]

Description [Reorders by repeatedly applying a sliding window of width

  1. Tries both permutations of the variables in a window that slides from low to high. Assumes that no dead nodes are present. Uses an event-driven approach to determine convergence. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

Definition at line 268 of file cuddWindow.c.

272 {
273  int x;
274  int res;
275  int nwin;
276  int newevent;
277  int *events;
278  int size;
279 
280 #ifdef DD_DEBUG
281  assert(low >= 0 && high < table->size);
282 #endif
283 
284  if (high-low < 1) return(ddWindowConv2(table,low,high));
285 
286  nwin = high-low;
287  events = ABC_ALLOC(int,nwin);
288  if (events == NULL) {
289  table->errorCode = CUDD_MEMORY_OUT;
290  return(0);
291  }
292  for (x=0; x<nwin; x++) {
293  events[x] = 1;
294  }
295 
296  res = table->keys - table->isolated;
297  do {
298  newevent = 0;
299  for (x=0; x<nwin; x++) {
300  if (events[x]) {
301  size = res;
302  res = cuddSwapInPlace(table,x+low,x+low+1);
303  if (res == 0) {
304  ABC_FREE(events);
305  return(0);
306  }
307  if (res >= size) { /* no improvement: undo permutation */
308  res = cuddSwapInPlace(table,x+low,x+low+1);
309  if (res == 0) {
310  ABC_FREE(events);
311  return(0);
312  }
313  }
314  if (res < size) {
315  if (x < nwin-1) events[x+1] = 1;
316  if (x > 0) events[x-1] = 1;
317  newevent = 1;
318  }
319  events[x] = 0;
320 #ifdef DD_STATS
321  if (res < size) {
322  (void) fprintf(table->out,"-");
323  } else {
324  (void) fprintf(table->out,"=");
325  }
326  fflush(table->out);
327 #endif
328  }
329  }
330 #ifdef DD_STATS
331  if (newevent) {
332  (void) fprintf(table->out,"|");
333  fflush(table->out);
334  }
335 #endif
336  } while (newevent);
337 
338  ABC_FREE(events);
339 
340  return(1);
341 
342 } /* end of ddWindowConv3 */
ddWindowConv2
static int ddWindowConv2(DdManager *table, int low, int high)
Definition: cuddWindow.c:268
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
DdManager::keys
unsigned int keys
Definition: cuddInt.h:369
DdManager::out
FILE * out
Definition: cuddInt.h:441
size
static int size
Definition: cuddSign.c:86
cuddSwapInPlace
int cuddSwapInPlace(DdManager *table, int x, int y)
Definition: cuddReorder.c:761
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
assert
#define assert(ex)
Definition: util_old.h:213
DdManager::isolated
int isolated
Definition: cuddInt.h:385
DdManager::errorCode
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
static int ddWindowConv3 ( DdManager *  table,
int  low,
int  high 
)
static

Function********************************************************************

Synopsis [Reorders by repeatedly applying a sliding window of width 3.]

Description [Reorders by repeatedly applying a sliding window of width

  1. Tries all possible permutations to the variables in a window that slides from low to high. Assumes that no dead nodes are present. Uses an event-driven approach to determine convergence. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

Definition at line 503 of file cuddWindow.c.

507 {
508  int x;
509  int res;
510  int nwin;
511  int newevent;
512  int *events;
513 
514 #ifdef DD_DEBUG
515  assert(low >= 0 && high < table->size);
516 #endif
517 
518  if (high-low < 2) return(ddWindowConv2(table,low,high));
519 
520  nwin = high-low-1;
521  events = ABC_ALLOC(int,nwin);
522  if (events == NULL) {
523  table->errorCode = CUDD_MEMORY_OUT;
524  return(0);
525  }
526  for (x=0; x<nwin; x++) {
527  events[x] = 1;
528  }
529 
530  do {
531  newevent = 0;
532  for (x=0; x<nwin; x++) {
533  if (events[x]) {
534  res = ddPermuteWindow3(table,x+low);
535  switch (res) {
536  case ABC:
537  break;
538  case BAC:
539  if (x < nwin-1) events[x+1] = 1;
540  if (x > 1) events[x-2] = 1;
541  newevent = 1;
542  break;
543  case BCA:
544  case CBA:
545  case CAB:
546  if (x < nwin-2) events[x+2] = 1;
547  if (x < nwin-1) events[x+1] = 1;
548  if (x > 0) events[x-1] = 1;
549  if (x > 1) events[x-2] = 1;
550  newevent = 1;
551  break;
552  case ACB:
553  if (x < nwin-2) events[x+2] = 1;
554  if (x > 0) events[x-1] = 1;
555  newevent = 1;
556  break;
557  default:
558  ABC_FREE(events);
559  return(0);
560  }
561  events[x] = 0;
562 #ifdef DD_STATS
563  if (res == ABC) {
564  (void) fprintf(table->out,"=");
565  } else {
566  (void) fprintf(table->out,"-");
567  }
568  fflush(table->out);
569 #endif
570  }
571  }
572 #ifdef DD_STATS
573  if (newevent) {
574  (void) fprintf(table->out,"|");
575  fflush(table->out);
576  }
577 #endif
578  } while (newevent);
579 
580  ABC_FREE(events);
581 
582  return(1);
583 
584 } /* end of ddWindowConv3 */
ddPermuteWindow3
static int ddPermuteWindow3(DdManager *table, int x)
Definition: cuddWindow.c:361
BAC
#define BAC
ddWindowConv2
static int ddWindowConv2(DdManager *table, int low, int high)
Definition: cuddWindow.c:268
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
BCA
#define BCA
CAB
#define CAB
DdManager::out
FILE * out
Definition: cuddInt.h:441
size
static int size
Definition: cuddSign.c:86
ABC
#define ABC
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
ACB
#define ACB
assert
#define assert(ex)
Definition: util_old.h:213
CBA
#define CBA
DdManager::errorCode
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
static int ddWindowConv4 ( DdManager *  table,
int  low,
int  high 
)
static

Function********************************************************************

Synopsis [Reorders by repeatedly applying a sliding window of width 4.]

Description [Reorders by repeatedly applying a sliding window of width

  1. Tries all possible permutations to the variables in a window that slides from low to high. Assumes that no dead nodes are present. Uses an event-driven approach to determine convergence. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

Definition at line 904 of file cuddWindow.c.

908 {
909  int x;
910  int res;
911  int nwin;
912  int newevent;
913  int *events;
914 
915 #ifdef DD_DEBUG
916  assert(low >= 0 && high < table->size);
917 #endif
918 
919  if (high-low < 3) return(ddWindowConv3(table,low,high));
920 
921  nwin = high-low-2;
922  events = ABC_ALLOC(int,nwin);
923  if (events == NULL) {
924  table->errorCode = CUDD_MEMORY_OUT;
925  return(0);
926  }
927  for (x=0; x<nwin; x++) {
928  events[x] = 1;
929  }
930 
931  do {
932  newevent = 0;
933  for (x=0; x<nwin; x++) {
934  if (events[x]) {
935  res = ddPermuteWindow4(table,x+low);
936  switch (res) {
937  case ABCD:
938  break;
939  case BACD:
940  if (x < nwin-1) events[x+1] = 1;
941  if (x > 2) events[x-3] = 1;
942  newevent = 1;
943  break;
944  case BADC:
945  if (x < nwin-3) events[x+3] = 1;
946  if (x < nwin-1) events[x+1] = 1;
947  if (x > 0) events[x-1] = 1;
948  if (x > 2) events[x-3] = 1;
949  newevent = 1;
950  break;
951  case ABDC:
952  if (x < nwin-3) events[x+3] = 1;
953  if (x > 0) events[x-1] = 1;
954  newevent = 1;
955  break;
956  case ADBC:
957  case ADCB:
958  case ACDB:
959  if (x < nwin-3) events[x+3] = 1;
960  if (x < nwin-2) events[x+2] = 1;
961  if (x > 0) events[x-1] = 1;
962  if (x > 1) events[x-2] = 1;
963  newevent = 1;
964  break;
965  case DACB:
966  case DABC:
967  case DBAC:
968  case BDAC:
969  case BDCA:
970  case DBCA:
971  case DCBA:
972  case DCAB:
973  case CDAB:
974  case CDBA:
975  case CBDA:
976  case BCDA:
977  case CADB:
978  if (x < nwin-3) events[x+3] = 1;
979  if (x < nwin-2) events[x+2] = 1;
980  if (x < nwin-1) events[x+1] = 1;
981  if (x > 0) events[x-1] = 1;
982  if (x > 1) events[x-2] = 1;
983  if (x > 2) events[x-3] = 1;
984  newevent = 1;
985  break;
986  case BCAD:
987  case CBAD:
988  case CABD:
989  if (x < nwin-2) events[x+2] = 1;
990  if (x < nwin-1) events[x+1] = 1;
991  if (x > 1) events[x-2] = 1;
992  if (x > 2) events[x-3] = 1;
993  newevent = 1;
994  break;
995  case ACBD:
996  if (x < nwin-2) events[x+2] = 1;
997  if (x > 1) events[x-2] = 1;
998  newevent = 1;
999  break;
1000  default:
1001  ABC_FREE(events);
1002  return(0);
1003  }
1004  events[x] = 0;
1005 #ifdef DD_STATS
1006  if (res == ABCD) {
1007  (void) fprintf(table->out,"=");
1008  } else {
1009  (void) fprintf(table->out,"-");
1010  }
1011  fflush(table->out);
1012 #endif
1013  }
1014  }
1015 #ifdef DD_STATS
1016  if (newevent) {
1017  (void) fprintf(table->out,"|");
1018  fflush(table->out);
1019  }
1020 #endif
1021  } while (newevent);
1022 
1023  ABC_FREE(events);
1024 
1025  return(1);
1026 
1027 } /* end of ddWindowConv4 */
CADB
#define CADB
DACB
#define DACB
BCAD
#define BCAD
ADCB
#define ADCB
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
ddPermuteWindow4
static int ddPermuteWindow4(DdManager *table, int w)
Definition: cuddWindow.c:601
DCBA
#define DCBA
ABDC
#define ABDC
BDCA
#define BDCA
DCAB
#define DCAB
DdManager::out
FILE * out
Definition: cuddInt.h:441
BCDA
#define BCDA
CDBA
#define CDBA
ACBD
#define ACBD
ADBC
#define ADBC
CBDA
#define CBDA
size
static int size
Definition: cuddSign.c:86
DBAC
#define DBAC
BDAC
#define BDAC
CDAB
#define CDAB
DBCA
#define DBCA
CBAD
#define CBAD
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
CABD
#define CABD
assert
#define assert(ex)
Definition: util_old.h:213
ABCD
#define ABCD
BACD
#define BACD
BADC
#define BADC
DdManager::errorCode
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
ddWindowConv3
static int ddWindowConv3(DdManager *table, int low, int high)
Definition: cuddWindow.c:503
ACDB
#define ACDB
DABC
#define DABC

Variable Documentation

ABC_NAMESPACE_IMPL_START char rcsid [] DD_UNUSED = "$Id: cuddWindow.c,v 1.14 2009/02/20 02:14:58 fabio Exp $"
static

CFile***********************************************************************

FileName [cuddWindow.c]

PackageName [cudd]

Synopsis [Functions for variable reordering by window permutation.]

Description [Internal procedures included in this module:

Static procedures included in this module:

]

Author [Fabio Somenzi]

Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]

Definition at line 88 of file cuddWindow.c.