summaryrefslogtreecommitdiffstats
path: root/abc70930/src/bdd/cudd/cuddWindow.c
diff options
context:
space:
mode:
Diffstat (limited to 'abc70930/src/bdd/cudd/cuddWindow.c')
-rw-r--r--abc70930/src/bdd/cudd/cuddWindow.c997
1 files changed, 0 insertions, 997 deletions
diff --git a/abc70930/src/bdd/cudd/cuddWindow.c b/abc70930/src/bdd/cudd/cuddWindow.c
deleted file mode 100644
index 9ceb79b2..00000000
--- a/abc70930/src/bdd/cudd/cuddWindow.c
+++ /dev/null
@@ -1,997 +0,0 @@
-/**CFile***********************************************************************
-
- FileName [cuddWindow.c]
-
- PackageName [cudd]
-
- Synopsis [Functions for window permutation]
-
- Description [Internal procedures included in this module:
- <ul>
- <li> cuddWindowReorder()
- </ul>
- Static procedures included in this module:
- <ul>
- <li> ddWindow2()
- <li> ddWindowConv2()
- <li> ddPermuteWindow3()
- <li> ddWindow3()
- <li> ddWindowConv3()
- <li> ddPermuteWindow4()
- <li> ddWindow4()
- <li> ddWindowConv4()
- </ul>]
-
- Author [Fabio Somenzi]
-
- Copyright [This file was created at the University of Colorado at
- Boulder. The University of Colorado at Boulder makes no warranty
- about the suitability of this software for any purpose. It is
- presented on an AS IS basis.]
-
-******************************************************************************/
-
-#include "util_hack.h"
-#include "cuddInt.h"
-
-/*---------------------------------------------------------------------------*/
-/* Constant declarations */
-/*---------------------------------------------------------------------------*/
-
-
-/*---------------------------------------------------------------------------*/
-/* Stucture declarations */
-/*---------------------------------------------------------------------------*/
-
-
-/*---------------------------------------------------------------------------*/
-/* Type declarations */
-/*---------------------------------------------------------------------------*/
-
-
-/*---------------------------------------------------------------------------*/
-/* Variable declarations */
-/*---------------------------------------------------------------------------*/
-
-#ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddWindow.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $";
-#endif
-
-#ifdef DD_STATS
-extern int ddTotalNumberSwapping;
-extern int ddTotalNISwaps;
-#endif
-
-/*---------------------------------------------------------------------------*/
-/* Macro declarations */
-/*---------------------------------------------------------------------------*/
-
-
-/**AutomaticStart*************************************************************/
-
-/*---------------------------------------------------------------------------*/
-/* Static function prototypes */
-/*---------------------------------------------------------------------------*/
-
-static int ddWindow2 ARGS((DdManager *table, int low, int high));
-static int ddWindowConv2 ARGS((DdManager *table, int low, int high));
-static int ddPermuteWindow3 ARGS((DdManager *table, int x));
-static int ddWindow3 ARGS((DdManager *table, int low, int high));
-static int ddWindowConv3 ARGS((DdManager *table, int low, int high));
-static int ddPermuteWindow4 ARGS((DdManager *table, int w));
-static int ddWindow4 ARGS((DdManager *table, int low, int high));
-static int ddWindowConv4 ARGS((DdManager *table, int low, int high));
-
-/**AutomaticEnd***************************************************************/
-
-
-/*---------------------------------------------------------------------------*/
-/* Definition of exported functions */
-/*---------------------------------------------------------------------------*/
-
-/*---------------------------------------------------------------------------*/
-/* Definition of internal functions */
-/*---------------------------------------------------------------------------*/
-
-
-/**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]
-
-******************************************************************************/
-int
-cuddWindowReorder(
- DdManager * table /* DD table */,
- int low /* lowest index to reorder */,
- int high /* highest index to reorder */,
- Cudd_ReorderingType submethod /* window reordering option */)
-{
-
- int res;
-#ifdef DD_DEBUG
- int supposedOpt;
-#endif
-
- switch (submethod) {
- case CUDD_REORDER_WINDOW2:
- res = ddWindow2(table,low,high);
- break;
- case CUDD_REORDER_WINDOW3:
- res = ddWindow3(table,low,high);
- break;
- case CUDD_REORDER_WINDOW4:
- res = ddWindow4(table,low,high);
- break;
- case CUDD_REORDER_WINDOW2_CONV:
- res = ddWindowConv2(table,low,high);
- break;
- case CUDD_REORDER_WINDOW3_CONV:
- res = ddWindowConv3(table,low,high);
-#ifdef DD_DEBUG
- supposedOpt = table->keys - table->isolated;
- res = ddWindow3(table,low,high);
- if (table->keys - table->isolated != (unsigned) supposedOpt) {
- (void) fprintf(table->err, "Convergence failed! (%d != %d)\n",
- table->keys - table->isolated, supposedOpt);
- }
-#endif
- break;
- case CUDD_REORDER_WINDOW4_CONV:
- res = ddWindowConv4(table,low,high);
-#ifdef DD_DEBUG
- supposedOpt = table->keys - table->isolated;
- res = ddWindow4(table,low,high);
- if (table->keys - table->isolated != (unsigned) supposedOpt) {
- (void) fprintf(table->err,"Convergence failed! (%d != %d)\n",
- table->keys - table->isolated, supposedOpt);
- }
-#endif
- break;
- default: return(0);
- }
-
- return(res);
-
-} /* end of cuddWindowReorder */
-
-
-/*---------------------------------------------------------------------------*/
-/* Definition of static functions */
-/*---------------------------------------------------------------------------*/
-
-/**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]
-
-******************************************************************************/
-static int
-ddWindow2(
- DdManager * table,
- int low,
- int high)
-{
-
- int x;
- int res;
- int size;
-
-#ifdef DD_DEBUG
- assert(low >= 0 && high < table->size);
-#endif
-
- if (high-low < 1) return(0);
-
- res = table->keys - table->isolated;
- for (x = low; x < high; x++) {
- size = res;
- res = cuddSwapInPlace(table,x,x+1);
- if (res == 0) return(0);
- if (res >= size) { /* no improvement: undo permutation */
- res = cuddSwapInPlace(table,x,x+1);
- if (res == 0) return(0);
- }
-#ifdef DD_STATS
- if (res < size) {
- (void) fprintf(table->out,"-");
- } else {
- (void) fprintf(table->out,"=");
- }
- fflush(table->out);
-#endif
- }
-
- return(1);
-
-} /* end of ddWindow2 */
-
-
-/**Function********************************************************************
-
- Synopsis [Reorders by repeatedly applying a sliding window of width 2.]
-
- Description [Reorders by repeatedly 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. Uses an event-driven approach to determine convergence.
- Returns 1 in case of success; 0 otherwise.]
-
- SideEffects [None]
-
-******************************************************************************/
-static int
-ddWindowConv2(
- DdManager * table,
- int low,
- int high)
-{
- int x;
- int res;
- int nwin;
- int newevent;
- int *events;
- int size;
-
-#ifdef DD_DEBUG
- assert(low >= 0 && high < table->size);
-#endif
-
- if (high-low < 1) return(ddWindowConv2(table,low,high));
-
- nwin = high-low;
- events = ALLOC(int,nwin);
- if (events == NULL) {
- table->errorCode = CUDD_MEMORY_OUT;
- return(0);
- }
- for (x=0; x<nwin; x++) {
- events[x] = 1;
- }
-
- res = table->keys - table->isolated;
- do {
- newevent = 0;
- for (x=0; x<nwin; x++) {
- if (events[x]) {
- size = res;
- res = cuddSwapInPlace(table,x+low,x+low+1);
- if (res == 0) {
- FREE(events);
- return(0);
- }
- if (res >= size) { /* no improvement: undo permutation */
- res = cuddSwapInPlace(table,x+low,x+low+1);
- if (res == 0) {
- FREE(events);
- return(0);
- }
- }
- if (res < size) {
- if (x < nwin-1) events[x+1] = 1;
- if (x > 0) events[x-1] = 1;
- newevent = 1;
- }
- events[x] = 0;
-#ifdef DD_STATS
- if (res < size) {
- (void) fprintf(table->out,"-");
- } else {
- (void) fprintf(table->out,"=");
- }
- fflush(table->out);
-#endif
- }
- }
-#ifdef DD_STATS
- if (newevent) {
- (void) fprintf(table->out,"|");
- fflush(table->out);
- }
-#endif
- } while (newevent);
-
- FREE(events);
-
- return(1);
-
-} /* end of ddWindowConv3 */
-
-
-/**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]
-
-******************************************************************************/
-static int
-ddPermuteWindow3(
- DdManager * table,
- int x)
-{
- int y,z;
- int size,sizeNew;
- int best;
-
-#ifdef DD_DEBUG
- assert(table->dead == 0);
- assert(x+2 < table->size);
-#endif
-
- size = table->keys - table->isolated;
- y = x+1; z = y+1;
-
- /* The permutation pattern is:
- ** (x,y)(y,z)
- ** repeated three times to get all 3! = 6 permutations.
- */
-#define ABC 1
- best = ABC;
-
-#define BAC 2
- sizeNew = cuddSwapInPlace(table,x,y);
- if (sizeNew < size) {
- if (sizeNew == 0) return(0);
- best = BAC;
- size = sizeNew;
- }
-#define BCA 3
- sizeNew = cuddSwapInPlace(table,y,z);
- if (sizeNew < size) {
- if (sizeNew == 0) return(0);
- best = BCA;
- size = sizeNew;
- }
-#define CBA 4
- sizeNew = cuddSwapInPlace(table,x,y);
- if (sizeNew < size) {
- if (sizeNew == 0) return(0);
- best = CBA;
- size = sizeNew;
- }
-#define CAB 5
- sizeNew = cuddSwapInPlace(table,y,z);
- if (sizeNew < size) {
- if (sizeNew == 0) return(0);
- best = CAB;
- size = sizeNew;
- }
-#define ACB 6
- sizeNew = cuddSwapInPlace(table,x,y);
- if (sizeNew < size) {
- if (sizeNew == 0) return(0);
- best = ACB;
- size = sizeNew;
- }
-
- /* Now take the shortest route to the best permuytation.
- ** The initial permutation is ACB.
- */
- switch(best) {
- case BCA: if (!cuddSwapInPlace(table,y,z)) return(0);
- case CBA: if (!cuddSwapInPlace(table,x,y)) return(0);
- case ABC: if (!cuddSwapInPlace(table,y,z)) return(0);
- case ACB: break;
- case BAC: if (!cuddSwapInPlace(table,y,z)) return(0);
- case CAB: if (!cuddSwapInPlace(table,x,y)) return(0);
- break;
- default: return(0);
- }
-
-#ifdef DD_DEBUG
- assert(table->keys - table->isolated == (unsigned) size);
-#endif
-
- return(best);
-
-} /* end of ddPermuteWindow3 */
-
-
-/**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]
-
-******************************************************************************/
-static int
-ddWindow3(
- DdManager * table,
- int low,
- int high)
-{
-
- int x;
- int res;
-
-#ifdef DD_DEBUG
- assert(low >= 0 && high < table->size);
-#endif
-
- if (high-low < 2) return(ddWindow2(table,low,high));
-
- for (x = low; x+1 < high; x++) {
- res = ddPermuteWindow3(table,x);
- if (res == 0) return(0);
-#ifdef DD_STATS
- if (res == ABC) {
- (void) fprintf(table->out,"=");
- } else {
- (void) fprintf(table->out,"-");
- }
- fflush(table->out);
-#endif
- }
-
- return(1);
-
-} /* end of ddWindow3 */
-
-
-/**Function********************************************************************
-
- Synopsis [Reorders by repeatedly applying a sliding window of width 3.]
-
- Description [Reorders by repeatedly 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. Uses an event-driven approach to determine convergence.
- Returns 1 in case of success; 0 otherwise.]
-
- SideEffects [None]
-
-******************************************************************************/
-static int
-ddWindowConv3(
- DdManager * table,
- int low,
- int high)
-{
- int x;
- int res;
- int nwin;
- int newevent;
- int *events;
-
-#ifdef DD_DEBUG
- assert(low >= 0 && high < table->size);
-#endif
-
- if (high-low < 2) return(ddWindowConv2(table,low,high));
-
- nwin = high-low-1;
- events = ALLOC(int,nwin);
- if (events == NULL) {
- table->errorCode = CUDD_MEMORY_OUT;
- return(0);
- }
- for (x=0; x<nwin; x++) {
- events[x] = 1;
- }
-
- do {
- newevent = 0;
- for (x=0; x<nwin; x++) {
- if (events[x]) {
- res = ddPermuteWindow3(table,x+low);
- switch (res) {
- case ABC:
- break;
- case BAC:
- if (x < nwin-1) events[x+1] = 1;
- if (x > 1) events[x-2] = 1;
- newevent = 1;
- break;
- case BCA:
- case CBA:
- case CAB:
- if (x < nwin-2) events[x+2] = 1;
- if (x < nwin-1) events[x+1] = 1;
- if (x > 0) events[x-1] = 1;
- if (x > 1) events[x-2] = 1;
- newevent = 1;
- break;
- case ACB:
- if (x < nwin-2) events[x+2] = 1;
- if (x > 0) events[x-1] = 1;
- newevent = 1;
- break;
- default:
- FREE(events);
- return(0);
- }
- events[x] = 0;
-#ifdef DD_STATS
- if (res == ABC) {
- (void) fprintf(table->out,"=");
- } else {
- (void) fprintf(table->out,"-");
- }
- fflush(table->out);
-#endif
- }
- }
-#ifdef DD_STATS
- if (newevent) {
- (void) fprintf(table->out,"|");
- fflush(table->out);
- }
-#endif
- } while (newevent);
-
- FREE(events);
-
- return(1);
-
-} /* end of ddWindowConv3 */
-
-
-/**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]
-
-******************************************************************************/
-static int
-ddPermuteWindow4(
- DdManager * table,
- int w)
-{
- int x,y,z;
- int size,sizeNew;
- int best;
-
-#ifdef DD_DEBUG
- assert(table->dead == 0);
- assert(w+3 < table->size);
-#endif
-
- size = table->keys - table->isolated;
- x = w+1; y = x+1; z = y+1;
-
- /* The permutation pattern is:
- * (w,x)(y,z)(w,x)(x,y)
- * (y,z)(w,x)(y,z)(x,y)
- * repeated three times to get all 4! = 24 permutations.
- * This gives a hamiltonian circuit of Cayley's graph.
- * The codes to the permutation are assigned in topological order.
- * The permutations at lower distance from the final permutation are
- * assigned lower codes. This way we can choose, between
- * permutations that give the same size, one that requires the minimum
- * number of swaps from the final permutation of the hamiltonian circuit.
- * There is an exception to this rule: ABCD is given Code 1, to
- * avoid oscillation when convergence is sought.
- */
-#define ABCD 1
- best = ABCD;
-
-#define BACD 7
- sizeNew = cuddSwapInPlace(table,w,x);
- if (sizeNew < size) {
- if (sizeNew == 0) return(0);
- best = BACD;
- size = sizeNew;
- }
-#define BADC 13
- sizeNew = cuddSwapInPlace(table,y,z);
- if (sizeNew < size) {
- if (sizeNew == 0) return(0);
- best = BADC;
- size = sizeNew;
- }
-#define ABDC 8
- sizeNew = cuddSwapInPlace(table,w,x);
- if (sizeNew < size || (sizeNew == size && ABDC < best)) {
- if (sizeNew == 0) return(0);
- best = ABDC;
- size = sizeNew;
- }
-#define ADBC 14
- sizeNew = cuddSwapInPlace(table,x,y);
- if (sizeNew < size) {
- if (sizeNew == 0) return(0);
- best = ADBC;
- size = sizeNew;
- }
-#define ADCB 9
- sizeNew = cuddSwapInPlace(table,y,z);
- if (sizeNew < size || (sizeNew == size && ADCB < best)) {
- if (sizeNew == 0) return(0);
- best = ADCB;
- size = sizeNew;
- }
-#define DACB 15
- sizeNew = cuddSwapInPlace(table,w,x);
- if (sizeNew < size) {
- if (sizeNew == 0) return(0);
- best = DACB;
- size = sizeNew;
- }
-#define DABC 20
- sizeNew = cuddSwapInPlace(table,y,z);
- if (sizeNew < size) {
- if (sizeNew == 0) return(0);
- best = DABC;
- size = sizeNew;
- }
-#define DBAC 23
- sizeNew = cuddSwapInPlace(table,x,y);
- if (sizeNew < size) {
- if (sizeNew == 0) return(0);
- best = DBAC;
- size = sizeNew;
- }
-#define BDAC 19
- sizeNew = cuddSwapInPlace(table,w,x);
- if (sizeNew < size || (sizeNew == size && BDAC < best)) {
- if (sizeNew == 0) return(0);
- best = BDAC;
- size = sizeNew;
- }
-#define BDCA 21
- sizeNew = cuddSwapInPlace(table,y,z);
- if (sizeNew < size || (sizeNew == size && BDCA < best)) {
- if (sizeNew == 0) return(0);
- best = BDCA;
- size = sizeNew;
- }
-#define DBCA 24
- sizeNew = cuddSwapInPlace(table,w,x);
- if (sizeNew < size) {
- if (sizeNew == 0) return(0);
- best = DBCA;
- size = sizeNew;
- }
-#define DCBA 22
- sizeNew = cuddSwapInPlace(table,x,y);
- if (sizeNew < size || (sizeNew == size && DCBA < best)) {
- if (sizeNew == 0) return(0);
- best = DCBA;
- size = sizeNew;
- }
-#define DCAB 18
- sizeNew = cuddSwapInPlace(table,y,z);
- if (sizeNew < size || (sizeNew == size && DCAB < best)) {
- if (sizeNew == 0) return(0);
- best = DCAB;
- size = sizeNew;
- }
-#define CDAB 12
- sizeNew = cuddSwapInPlace(table,w,x);
- if (sizeNew < size || (sizeNew == size && CDAB < best)) {
- if (sizeNew == 0) return(0);
- best = CDAB;
- size = sizeNew;
- }
-#define CDBA 17
- sizeNew = cuddSwapInPlace(table,y,z);
- if (sizeNew < size || (sizeNew == size && CDBA < best)) {
- if (sizeNew == 0) return(0);
- best = CDBA;
- size = sizeNew;
- }
-#define CBDA 11
- sizeNew = cuddSwapInPlace(table,x,y);
- if (sizeNew < size || (sizeNew == size && CBDA < best)) {
- if (sizeNew == 0) return(0);
- best = CBDA;
- size = sizeNew;
- }
-#define BCDA 16
- sizeNew = cuddSwapInPlace(table,w,x);
- if (sizeNew < size || (sizeNew == size && BCDA < best)) {
- if (sizeNew == 0) return(0);
- best = BCDA;
- size = sizeNew;
- }
-#define BCAD 10
- sizeNew = cuddSwapInPlace(table,y,z);
- if (sizeNew < size || (sizeNew == size && BCAD < best)) {
- if (sizeNew == 0) return(0);
- best = BCAD;
- size = sizeNew;
- }
-#define CBAD 5
- sizeNew = cuddSwapInPlace(table,w,x);
- if (sizeNew < size || (sizeNew == size && CBAD < best)) {
- if (sizeNew == 0) return(0);
- best = CBAD;
- size = sizeNew;
- }
-#define CABD 3
- sizeNew = cuddSwapInPlace(table,x,y);
- if (sizeNew < size || (sizeNew == size && CABD < best)) {
- if (sizeNew == 0) return(0);
- best = CABD;
- size = sizeNew;
- }
-#define CADB 6
- sizeNew = cuddSwapInPlace(table,y,z);
- if (sizeNew < size || (sizeNew == size && CADB < best)) {
- if (sizeNew == 0) return(0);
- best = CADB;
- size = sizeNew;
- }
-#define ACDB 4
- sizeNew = cuddSwapInPlace(table,w,x);
- if (sizeNew < size || (sizeNew == size && ACDB < best)) {
- if (sizeNew == 0) return(0);
- best = ACDB;
- size = sizeNew;
- }
-#define ACBD 2
- sizeNew = cuddSwapInPlace(table,y,z);
- if (sizeNew < size || (sizeNew == size && ACBD < best)) {
- if (sizeNew == 0) return(0);
- best = ACBD;
- size = sizeNew;
- }
-
- /* Now take the shortest route to the best permutation.
- ** The initial permutation is ACBD.
- */
- switch(best) {
- case DBCA: if (!cuddSwapInPlace(table,y,z)) return(0);
- case BDCA: if (!cuddSwapInPlace(table,x,y)) return(0);
- case CDBA: if (!cuddSwapInPlace(table,w,x)) return(0);
- case ADBC: if (!cuddSwapInPlace(table,y,z)) return(0);
- case ABDC: if (!cuddSwapInPlace(table,x,y)) return(0);
- case ACDB: if (!cuddSwapInPlace(table,y,z)) return(0);
- case ACBD: break;
- case DCBA: if (!cuddSwapInPlace(table,y,z)) return(0);
- case BCDA: if (!cuddSwapInPlace(table,x,y)) return(0);
- case CBDA: if (!cuddSwapInPlace(table,w,x)) return(0);
- if (!cuddSwapInPlace(table,x,y)) return(0);
- if (!cuddSwapInPlace(table,y,z)) return(0);
- break;
- case DBAC: if (!cuddSwapInPlace(table,x,y)) return(0);
- case DCAB: if (!cuddSwapInPlace(table,w,x)) return(0);
- case DACB: if (!cuddSwapInPlace(table,y,z)) return(0);
- case BACD: if (!cuddSwapInPlace(table,x,y)) return(0);
- case CABD: if (!cuddSwapInPlace(table,w,x)) return(0);
- break;
- case DABC: if (!cuddSwapInPlace(table,y,z)) return(0);
- case BADC: if (!cuddSwapInPlace(table,x,y)) return(0);
- case CADB: if (!cuddSwapInPlace(table,w,x)) return(0);
- if (!cuddSwapInPlace(table,y,z)) return(0);
- break;
- case BDAC: if (!cuddSwapInPlace(table,x,y)) return(0);
- case CDAB: if (!cuddSwapInPlace(table,w,x)) return(0);
- case ADCB: if (!cuddSwapInPlace(table,y,z)) return(0);
- case ABCD: if (!cuddSwapInPlace(table,x,y)) return(0);
- break;
- case BCAD: if (!cuddSwapInPlace(table,x,y)) return(0);
- case CBAD: if (!cuddSwapInPlace(table,w,x)) return(0);
- if (!cuddSwapInPlace(table,x,y)) return(0);
- break;
- default: return(0);
- }
-
-#ifdef DD_DEBUG
- assert(table->keys - table->isolated == (unsigned) size);
-#endif
-
- return(best);
-
-} /* end of ddPermuteWindow4 */
-
-
-/**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]
-
-******************************************************************************/
-static int
-ddWindow4(
- DdManager * table,
- int low,
- int high)
-{
-
- int w;
- int res;
-
-#ifdef DD_DEBUG
- assert(low >= 0 && high < table->size);
-#endif
-
- if (high-low < 3) return(ddWindow3(table,low,high));
-
- for (w = low; w+2 < high; w++) {
- res = ddPermuteWindow4(table,w);
- if (res == 0) return(0);
-#ifdef DD_STATS
- if (res == ABCD) {
- (void) fprintf(table->out,"=");
- } else {
- (void) fprintf(table->out,"-");
- }
- fflush(table->out);
-#endif
- }
-
- return(1);
-
-} /* end of ddWindow4 */
-
-
-/**Function********************************************************************
-
- Synopsis [Reorders by repeatedly applying a sliding window of width 4.]
-
- Description [Reorders by repeatedly 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. Uses an event-driven approach to determine convergence.
- Returns 1 in case of success; 0 otherwise.]
-
- SideEffects [None]
-
-******************************************************************************/
-static int
-ddWindowConv4(
- DdManager * table,
- int low,
- int high)
-{
- int x;
- int res;
- int nwin;
- int newevent;
- int *events;
-
-#ifdef DD_DEBUG
- assert(low >= 0 && high < table->size);
-#endif
-
- if (high-low < 3) return(ddWindowConv3(table,low,high));
-
- nwin = high-low-2;
- events = ALLOC(int,nwin);
- if (events == NULL) {
- table->errorCode = CUDD_MEMORY_OUT;
- return(0);
- }
- for (x=0; x<nwin; x++) {
- events[x] = 1;
- }
-
- do {
- newevent = 0;
- for (x=0; x<nwin; x++) {
- if (events[x]) {
- res = ddPermuteWindow4(table,x+low);
- switch (res) {
- case ABCD:
- break;
- case BACD:
- if (x < nwin-1) events[x+1] = 1;
- if (x > 2) events[x-3] = 1;
- newevent = 1;
- break;
- case BADC:
- if (x < nwin-3) events[x+3] = 1;
- if (x < nwin-1) events[x+1] = 1;
- if (x > 0) events[x-1] = 1;
- if (x > 2) events[x-3] = 1;
- newevent = 1;
- break;
- case ABDC:
- if (x < nwin-3) events[x+3] = 1;
- if (x > 0) events[x-1] = 1;
- newevent = 1;
- break;
- case ADBC:
- case ADCB:
- case ACDB:
- if (x < nwin-3) events[x+3] = 1;
- if (x < nwin-2) events[x+2] = 1;
- if (x > 0) events[x-1] = 1;
- if (x > 1) events[x-2] = 1;
- newevent = 1;
- break;
- case DACB:
- case DABC:
- case DBAC:
- case BDAC:
- case BDCA:
- case DBCA:
- case DCBA:
- case DCAB:
- case CDAB:
- case CDBA:
- case CBDA:
- case BCDA:
- case CADB:
- if (x < nwin-3) events[x+3] = 1;
- if (x < nwin-2) events[x+2] = 1;
- if (x < nwin-1) events[x+1] = 1;
- if (x > 0) events[x-1] = 1;
- if (x > 1) events[x-2] = 1;
- if (x > 2) events[x-3] = 1;
- newevent = 1;
- break;
- case BCAD:
- case CBAD:
- case CABD:
- if (x < nwin-2) events[x+2] = 1;
- if (x < nwin-1) events[x+1] = 1;
- if (x > 1) events[x-2] = 1;
- if (x > 2) events[x-3] = 1;
- newevent = 1;
- break;
- case ACBD:
- if (x < nwin-2) events[x+2] = 1;
- if (x > 1) events[x-2] = 1;
- newevent = 1;
- break;
- default:
- FREE(events);
- return(0);
- }
- events[x] = 0;
-#ifdef DD_STATS
- if (res == ABCD) {
- (void) fprintf(table->out,"=");
- } else {
- (void) fprintf(table->out,"-");
- }
- fflush(table->out);
-#endif
- }
- }
-#ifdef DD_STATS
- if (newevent) {
- (void) fprintf(table->out,"|");
- fflush(table->out);
- }
-#endif
- } while (newevent);
-
- FREE(events);
-
- return(1);
-
-} /* end of ddWindowConv4 */
-
generated by cgit v1.2.3 (git 2.25.1) at 2025-08-06 22:16:22 +0000