src/bdd/cudd/cuddWindow.c File Reference

#include "util_hack.h"
#include "cuddInt.h"

Include dependency graph for cuddWindow.c:

Go to the source code of this file.

Defines
#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	ARGS ((DdManager *table, int low, int high))
static int ddPermuteWindow3	ARGS ((DdManager *table, int x))
static int ddPermuteWindow4	ARGS ((DdManager *table, int w))
int	cuddWindowReorder (DdManager *table, int low, int high, Cudd_ReorderingType submethod)
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)
Variables
static char rcsid[]	DD_UNUSED = "$Id: cuddWindow.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $"

---

Define 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

static int ddPermuteWindow4 ARGS

(

(DdManager *table, int w)

)

[static]

static int ddPermuteWindow3 ARGS

(

(DdManager *table, int x)

)

[static]

static int ddWindowConv4 ARGS

(

(DdManager *table, int low, int high)

)

[static]

AutomaticStart

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 111 of file cuddWindow.c.

{

    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 */

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 330 of file cuddWindow.c.

{
    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 */

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 570 of file cuddWindow.c.

{
    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 */

static int ddWindow2	(	DdManager *	table,
		int	low,
		int	high
	)			[static]

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 183 of file cuddWindow.c.

{

    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 */

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 425 of file cuddWindow.c.

{

    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 */

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 826 of file cuddWindow.c.

{

    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 */

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 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]

Definition at line 237 of file cuddWindow.c.

{
    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 */

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 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]

Definition at line 472 of file cuddWindow.c.

{
    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 */

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 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]

Definition at line 873 of file cuddWindow.c.

{
    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 */

---

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddWindow.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $" [static]

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

FileName [cuddWindow.c]

PackageName [cudd]

Synopsis [Functions for window permutation]

Description [Internal procedures included in this module:

• cuddWindowReorder()

Static procedures included in this module:

• ddWindow2()
• ddWindowConv2()
• ddPermuteWindow3()
• ddWindow3()
• ddWindowConv3()
• ddPermuteWindow4()
• ddWindow4()
• ddWindowConv4()

]

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.]

Definition at line 57 of file cuddWindow.c.