cuddlinear.c

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

	g = NULL;
	for (i = 0; i < xslots; i++) {
	    f = xlist[i];
	    if (f == sentinel) continue;
	    xlist[i] = sentinel;
	    if (g == NULL) {
		g = f;
	    } else {
		last->next = f;
	    }
	    while ((next = f->next) != sentinel) {
		f = next;
	    } /* while there are elements in the collision chain */
	    last = f;
	} /* for each slot of the x subtable */
	last->next = NULL;

#ifdef DD_COUNT
	table->swapSteps += oldxkeys;
#endif
	/* Take care of the x nodes that must be re-expressed.
	** They form a linked list pointed by g.
	*/
	f = g;
	while (f != NULL) {
	    next = f->next;
	    /* Find f1, f0, f11, f10, f01, f00. */
	    f1 = cuddT(f);
#ifdef DD_DEBUG
	    assert(!(Cudd_IsComplement(f1)));
#endif
	    if ((int) f1->index == yindex) {
		f11 = cuddT(f1); f10 = cuddE(f1);
	    } else {
		f11 = f10 = f1;
	    }
#ifdef DD_DEBUG
	    assert(!(Cudd_IsComplement(f11)));
#endif
	    f0 = cuddE(f);
	    comple = Cudd_IsComplement(f0);
	    f0 = Cudd_Regular(f0);
	    if ((int) f0->index == yindex) {
		f01 = cuddT(f0); f00 = cuddE(f0);
	    } else {
		f01 = f00 = f0;
	    }
	    if (comple) {
		f01 = Cudd_Not(f01);
		f00 = Cudd_Not(f00);
	    }
	    /* Decrease ref count of f1. */
	    cuddSatDec(f1->ref);
	    /* Create the new T child. */
	    if (f11 == f00) {
		newf1 = f11;
		cuddSatInc(newf1->ref);
	    } else {
		/* Check ylist for triple (yindex,f11,f00). */
		posn = ddHash(f11, f00, yshift);
		/* For each element newf1 in collision list ylist[posn]. */
		previousP = &(ylist[posn]);
		newf1 = *previousP;
		while (f11 < cuddT(newf1)) {
		    previousP = &(newf1->next);
		    newf1 = *previousP;
		}
		while (f11 == cuddT(newf1) && f00 < cuddE(newf1)) {
		    previousP = &(newf1->next);
		    newf1 = *previousP;
		}
		if (cuddT(newf1) == f11 && cuddE(newf1) == f00) {
		    cuddSatInc(newf1->ref);
		} else { /* no match */
		    newf1 = cuddDynamicAllocNode(table);
		    if (newf1 == NULL)
			goto cuddLinearOutOfMem;
		    newf1->index = yindex; newf1->ref = 1;
		    cuddT(newf1) = f11;
		    cuddE(newf1) = f00;
		    /* Insert newf1 in the collision list ylist[posn];
		    ** increase the ref counts of f11 and f00.
		    */
		    newykeys++;
		    newf1->next = *previousP;
		    *previousP = newf1;
		    cuddSatInc(f11->ref);
		    tmp = Cudd_Regular(f00);
		    cuddSatInc(tmp->ref);
		}
	    }
	    cuddT(f) = newf1;
#ifdef DD_DEBUG
	    assert(!(Cudd_IsComplement(newf1)));
#endif

	    /* Do the same for f0, keeping complement dots into account. */
	    /* decrease ref count of f0 */
	    tmp = Cudd_Regular(f0);
	    cuddSatDec(tmp->ref);
	    /* create the new E child */
	    if (f01 == f10) {
		newf0 = f01;
		tmp = Cudd_Regular(newf0);
		cuddSatInc(tmp->ref); 
	    } else {
		/* make sure f01 is regular */
		newcomplement = Cudd_IsComplement(f01);
		if (newcomplement) {
		    f01 = Cudd_Not(f01);
		    f10 = Cudd_Not(f10);
		}
		/* Check ylist for triple (yindex,f01,f10). */
		posn = ddHash(f01, f10, yshift);
		/* For each element newf0 in collision list ylist[posn]. */
		previousP = &(ylist[posn]);
		newf0 = *previousP;
		while (f01 < cuddT(newf0)) {
		    previousP = &(newf0->next);
		    newf0 = *previousP;
		}
		while (f01 == cuddT(newf0) && f10 < cuddE(newf0)) {
		    previousP = &(newf0->next);
		    newf0 = *previousP;
		}
		if (cuddT(newf0) == f01 && cuddE(newf0) == f10) {
		    cuddSatInc(newf0->ref); 
		} else { /* no match */
		    newf0 = cuddDynamicAllocNode(table);
		    if (newf0 == NULL)
			goto cuddLinearOutOfMem;
		    newf0->index = yindex; newf0->ref = 1;
		    cuddT(newf0) = f01;
		    cuddE(newf0) = f10;
		    /* Insert newf0 in the collision list ylist[posn];
		    ** increase the ref counts of f01 and f10.
		    */
		    newykeys++;
		    newf0->next = *previousP;
		    *previousP = newf0;
		    cuddSatInc(f01->ref);
		    tmp = Cudd_Regular(f10);
		    cuddSatInc(tmp->ref);
		}
		if (newcomplement) {
		    newf0 = Cudd_Not(newf0);
		}
	    }
	    cuddE(f) = newf0;

	    /* Re-insert the modified f in xlist.
	    ** The modified f does not already exists in xlist.
	    ** (Because of the uniqueness of the cofactors.)
	    */
	    posn = ddHash(newf1, newf0, xshift);
	    newxkeys++;
	    previousP = &(xlist[posn]);
	    tmp = *previousP;
	    while (newf1 < cuddT(tmp)) {
		previousP = &(tmp->next);
		tmp = *previousP;
	    }
	    while (newf1 == cuddT(tmp) && newf0 < cuddE(tmp)) {
		previousP = &(tmp->next);
		tmp = *previousP;
	    }
	    f->next = *previousP;
	    *previousP = f;
	    f = next;
	} /* while f != NULL */

	/* GC the y layer. */

	/* For each node f in ylist. */
	for (i = 0; i < yslots; i++) {
	    previousP = &(ylist[i]);
	    f = *previousP;
	    while (f != sentinel) {
		next = f->next;
		if (f->ref == 0) {
		    tmp = cuddT(f);
		    cuddSatDec(tmp->ref);
		    tmp = Cudd_Regular(cuddE(f));
		    cuddSatDec(tmp->ref);
		    cuddDeallocNode(table,f);
		    newykeys--;
		} else {
		    *previousP = f;
		    previousP = &(f->next);
		}
		f = next;
	    } /* while f */
	    *previousP = sentinel;
	} /* for every collision list */

#if DD_DEBUG
#if 0
	(void) fprintf(table->out,"Linearly combining %d and %d\n",x,y);
#endif
	count = 0;
	idcheck = 0;
	for (i = 0; i < yslots; i++) {
	    f = ylist[i];
	    while (f != sentinel) {
		count++;
		if (f->index != (DdHalfWord) yindex)
		    idcheck++;
		f = f->next;
	    }
	}
	if (count != newykeys) {
	    fprintf(table->err,"Error in finding newykeys\toldykeys = %d\tnewykeys = %d\tactual = %d\n",oldykeys,newykeys,count);
	}
	if (idcheck != 0)
	    fprintf(table->err,"Error in id's of ylist\twrong id's = %d\n",idcheck);
	count = 0;
	idcheck = 0;
	for (i = 0; i < xslots; i++) {
	    f = xlist[i];
	    while (f != sentinel) {
		count++;
		if (f->index != (DdHalfWord) xindex)
		    idcheck++;
		f = f->next;
	    }
	}
	if (count != newxkeys || newxkeys != oldxkeys) {
	    fprintf(table->err,"Error in finding newxkeys\toldxkeys = %d \tnewxkeys = %d \tactual = %d\n",oldxkeys,newxkeys,count);
	}
	if (idcheck != 0)
	    fprintf(table->err,"Error in id's of xlist\twrong id's = %d\n",idcheck);
#endif

	isolated += (table->vars[xindex]->ref == 1) +
		    (table->vars[yindex]->ref == 1);
	table->isolated += isolated;

	/* Set the appropriate fields in table. */
	table->subtables[y].keys = newykeys;

	/* Here we should update the linear combination table
	** to record that x <- x EXNOR y. This is done by complementing
	** the (x,y) entry of the table.
	*/

	table->keys += newykeys - oldykeys;

	cuddXorLinear(table,xindex,yindex);
    }

#ifdef DD_DEBUG
    if (zero) {
	(void) Cudd_DebugCheck(table);
    }
#endif

    return(table->keys - table->isolated);

cuddLinearOutOfMem:
    (void) fprintf(table->err,"Error: cuddLinearInPlace out of memory\n");

    return (0);

} /* end of cuddLinearInPlace */


/**Function********************************************************************
 
  Synopsis    [Updates the interaction matrix.]

  Description []

  SideEffects [none]

  SeeAlso     []

******************************************************************************/
static void
ddUpdateInteractionMatrix(
  DdManager * table,
  int  xindex,
  int  yindex)
{
    int i;
    for (i = 0; i < yindex; i++) {
	if (i != xindex && cuddTestInteract(table,i,yindex)) {
	    if (i < xindex) {
		cuddSetInteract(table,i,xindex);
	    } else {
		cuddSetInteract(table,xindex,i);
	    }
	}
    }
    for (i = yindex+1; i < table->size; i++) {
	if (i != xindex && cuddTestInteract(table,yindex,i)) {
	    if (i < xindex) {
		cuddSetInteract(table,i,xindex);
	    } else {
		cuddSetInteract(table,xindex,i);
	    }
	}
    }

} /* end of ddUpdateInteractionMatrix */


/**Function********************************************************************
 
  Synopsis    [Initializes the linear transform matrix.]

  Description []

  SideEffects [none]

  SeeAlso     []

******************************************************************************/
static int
cuddInitLinear(
  DdManager * table)
{
    int words;
    int wordsPerRow;
    int nvars;
    int word;
    int bit;
    int i;
    long *linear;

    nvars = table->size;
    wordsPerRow = ((nvars - 1) >> LOGBPL) + 1;
    words = wordsPerRow * nvars;
    table->linear = linear = ALLOC(long,words);
    if (linear == NULL) {
	table->errorCode = CUDD_MEMORY_OUT;
	return(0);
    }
    table->memused += words * sizeof(long);
    table->linearSize = nvars;
    for (i = 0; i < words; i++) linear[i] = 0;
    for (i = 0; i < nvars; i++) {
	word = wordsPerRow * i + (i >> LOGBPL);
	bit  = i & (BPL-1);
	linear[word] = 1 << bit;
    }
    return(1);

} /* end of cuddInitLinear */


/**Function********************************************************************
 
  Synopsis    [Resizes the linear transform matrix.]

  Description []

  SideEffects [none]

  SeeAlso     []

******************************************************************************/
static int
cuddResizeLinear(
  DdManager * table)
{
    int words,oldWords;
    int wordsPerRow,oldWordsPerRow;
    int nvars,oldNvars;
    int word,oldWord;
    int bit;
    int i,j;
    long *linear,*oldLinear;

    oldNvars = table->linearSize;
    oldWordsPerRow = ((oldNvars - 1) >> LOGBPL) + 1;
    oldWords = oldWordsPerRow * oldNvars;
    oldLinear = table->linear;

    nvars = table->size;
    wordsPerRow = ((nvars - 1) >> LOGBPL) + 1;
    words = wordsPerRow * nvars;
    table->linear = linear = ALLOC(long,words);
    if (linear == NULL) {
	table->errorCode = CUDD_MEMORY_OUT;
	return(0);
    }
    table->memused += (words - oldWords) * sizeof(long);
    for (i = 0; i < words; i++) linear[i] = 0;

    /* Copy old matrix. */
    for (i = 0; i < oldNvars; i++) {
	for (j = 0; j < oldWordsPerRow; j++) {
	    oldWord = oldWordsPerRow * i + j;
	    word = wordsPerRow * i + j;
	    linear[word] = oldLinear[oldWord];
	}
    }
    FREE(oldLinear);

    /* Add elements to the diagonal. */
    for (i = oldNvars; i < nvars; i++) {
	word = wordsPerRow * i + (i >> LOGBPL);
	bit  = i & (BPL-1);
	linear[word] = 1 << bit;
    }
    table->linearSize = nvars;

    return(1);

} /* end of cuddResizeLinear */


/**Function********************************************************************
 
  Synopsis    [XORs two rows of the linear transform matrix.]

  Description [XORs two rows of the linear transform matrix and replaces
  the first row with the result.]

  SideEffects [none]

  SeeAlso     []

******************************************************************************/
static void
cuddXorLinear(
  DdManager * table,
  int  x,
  int  y)
{
    int i;
    int nvars = table->size;
    int wordsPerRow = ((nvars - 1) >> LOGBPL) + 1;
    int xstart = wordsPerRow * x;
    int ystart = wordsPerRow * y;
    long *linear = table->linear;

    for (i = 0; i < wordsPerRow; i++) {
	linear[xstart+i] ^= linear[ystart+i];
    }

} /* end of cuddXorLinear */