cuddwindow.c

主要进行大规模的电路综合

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