summaryrefslogtreecommitdiffstats
path: root/src/bdd/cudd/cuddLinear.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/bdd/cudd/cuddLinear.c')
-rw-r--r--src/bdd/cudd/cuddLinear.c1655
1 files changed, 845 insertions, 810 deletions
diff --git a/src/bdd/cudd/cuddLinear.c b/src/bdd/cudd/cuddLinear.c
index 9cb19e95..19de9820 100644
--- a/src/bdd/cudd/cuddLinear.c
+++ b/src/bdd/cudd/cuddLinear.c
@@ -7,30 +7,57 @@
Synopsis [Functions for DD reduction by linear transformations.]
Description [ Internal procedures included in this module:
- <ul>
- <li> cuddLinearAndSifting()
- </ul>
- Static procedures included in this module:
- <ul>
- <li> ddLinearUniqueCompare()
- <li> ddLinearAndSiftingAux()
- <li> ddLinearAndSiftingUp()
- <li> ddLinearAndSiftingDown()
- <li> ddLinearAndSiftingBackward()
- <li> ddUndoMoves()
- <li> ddUpdateInteractionMatrix()
- <li> cuddLinearInPlace()
- <li> cuddInitLinear()
- <li> cuddResizeLinear()
- <li> cuddXorLinear()
- </ul>]
+ <ul>
+ <li> cuddLinearAndSifting()
+ <li> cuddLinearInPlace()
+ <li> cuddUpdateInteractionMatrix()
+ <li> cuddInitLinear()
+ <li> cuddResizeLinear()
+ </ul>
+ Static procedures included in this module:
+ <ul>
+ <li> ddLinearUniqueCompare()
+ <li> ddLinearAndSiftingAux()
+ <li> ddLinearAndSiftingUp()
+ <li> ddLinearAndSiftingDown()
+ <li> ddLinearAndSiftingBackward()
+ <li> ddUndoMoves()
+ <li> cuddXorLinear()
+ </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.]
+ 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.]
******************************************************************************/
@@ -40,6 +67,7 @@
ABC_NAMESPACE_IMPL_START
+
/*---------------------------------------------------------------------------*/
/* Constant declarations */
/*---------------------------------------------------------------------------*/
@@ -68,19 +96,19 @@ ABC_NAMESPACE_IMPL_START
/*---------------------------------------------------------------------------*/
#ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddLinear.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $";
+static char rcsid[] DD_UNUSED = "$Id: cuddLinear.c,v 1.28 2009/02/19 16:21:03 fabio Exp $";
#endif
-static int *entry;
+static int *entry;
#ifdef DD_STATS
-extern int ddTotalNumberSwapping;
-extern int ddTotalNISwaps;
-static int ddTotalNumberLinearTr;
+extern int ddTotalNumberSwapping;
+extern int ddTotalNISwaps;
+static int ddTotalNumberLinearTr;
#endif
#ifdef DD_DEBUG
-static int zero = 0;
+static int zero = 0;
#endif
/*---------------------------------------------------------------------------*/
@@ -93,17 +121,13 @@ static int zero = 0;
/* Static function prototypes */
/*---------------------------------------------------------------------------*/
-static int ddLinearUniqueCompare ARGS((int *ptrX, int *ptrY));
-static int ddLinearAndSiftingAux ARGS((DdManager *table, int x, int xLow, int xHigh));
-static Move * ddLinearAndSiftingUp ARGS((DdManager *table, int y, int xLow, Move *prevMoves));
-static Move * ddLinearAndSiftingDown ARGS((DdManager *table, int x, int xHigh, Move *prevMoves));
-static int ddLinearAndSiftingBackward ARGS((DdManager *table, int size, Move *moves));
-static Move* ddUndoMoves ARGS((DdManager *table, Move *moves));
-static int cuddLinearInPlace ARGS((DdManager *table, int x, int y));
-static void ddUpdateInteractionMatrix ARGS((DdManager *table, int xindex, int yindex));
-static int cuddInitLinear ARGS((DdManager *table));
-static int cuddResizeLinear ARGS((DdManager *table));
-static void cuddXorLinear ARGS((DdManager *table, int x, int y));
+static int ddLinearUniqueCompare (int *ptrX, int *ptrY);
+static int ddLinearAndSiftingAux (DdManager *table, int x, int xLow, int xHigh);
+static Move * ddLinearAndSiftingUp (DdManager *table, int y, int xLow, Move *prevMoves);
+static Move * ddLinearAndSiftingDown (DdManager *table, int x, int xHigh, Move *prevMoves);
+static int ddLinearAndSiftingBackward (DdManager *table, int size, Move *moves);
+static Move* ddUndoMoves (DdManager *table, Move *moves);
+static void cuddXorLinear (DdManager *table, int x, int y);
/**AutomaticEnd***************************************************************/
@@ -114,7 +138,7 @@ static void cuddXorLinear ARGS((DdManager *table, int x, int y));
/**Function********************************************************************
-
+
Synopsis [Prints the linear transform matrix.]
Description [Prints the linear transform matrix. Returns 1 in case of
@@ -136,16 +160,16 @@ Cudd_PrintLinear(
long word;
for (i = 0; i < nvars; i++) {
- for (j = 0; j < wordsPerRow; j++) {
- word = table->linear[i*wordsPerRow + j];
- for (k = 0; k < BPL; k++) {
- retval = fprintf(table->out,"%ld",word & 1);
- if (retval == 0) return(0);
- word >>= 1;
+ for (j = 0; j < wordsPerRow; j++) {
+ word = table->linear[i*wordsPerRow + j];
+ for (k = 0; k < BPL; k++) {
+ retval = fprintf(table->out,"%ld",word & 1);
+ if (retval == 0) return(0);
+ word >>= 1;
+ }
}
- }
- retval = fprintf(table->out,"\n");
- if (retval == 0) return(0);
+ retval = fprintf(table->out,"\n");
+ if (retval == 0) return(0);
}
return(1);
@@ -153,7 +177,7 @@ Cudd_PrintLinear(
/**Function********************************************************************
-
+
Synopsis [Reads an entry of the linear transform matrix.]
Description [Reads an entry of the linear transform matrix.]
@@ -218,13 +242,13 @@ cuddLinearAndSifting(
int lower,
int upper)
{
- int i;
- int *var;
- int size;
- int x;
- int result;
+ int i;
+ int *var;
+ int size;
+ int x;
+ int result;
#ifdef DD_STATS
- int previousSize;
+ int previousSize;
#endif
#ifdef DD_STATS
@@ -236,65 +260,65 @@ cuddLinearAndSifting(
var = NULL;
entry = NULL;
if (table->linear == NULL) {
- result = cuddInitLinear(table);
- if (result == 0) goto cuddLinearAndSiftingOutOfMem;
+ result = cuddInitLinear(table);
+ if (result == 0) goto cuddLinearAndSiftingOutOfMem;
#if 0
- (void) fprintf(table->out,"\n");
- result = Cudd_PrintLinear(table);
- if (result == 0) goto cuddLinearAndSiftingOutOfMem;
+ (void) fprintf(table->out,"\n");
+ result = Cudd_PrintLinear(table);
+ if (result == 0) goto cuddLinearAndSiftingOutOfMem;
#endif
} else if (table->size != table->linearSize) {
- result = cuddResizeLinear(table);
- if (result == 0) goto cuddLinearAndSiftingOutOfMem;
+ result = cuddResizeLinear(table);
+ if (result == 0) goto cuddLinearAndSiftingOutOfMem;
#if 0
- (void) fprintf(table->out,"\n");
- result = Cudd_PrintLinear(table);
- if (result == 0) goto cuddLinearAndSiftingOutOfMem;
+ (void) fprintf(table->out,"\n");
+ result = Cudd_PrintLinear(table);
+ if (result == 0) goto cuddLinearAndSiftingOutOfMem;
#endif
}
/* Find order in which to sift variables. */
entry = ABC_ALLOC(int,size);
if (entry == NULL) {
- table->errorCode = CUDD_MEMORY_OUT;
- goto cuddLinearAndSiftingOutOfMem;
+ table->errorCode = CUDD_MEMORY_OUT;
+ goto cuddLinearAndSiftingOutOfMem;
}
var = ABC_ALLOC(int,size);
if (var == NULL) {
- table->errorCode = CUDD_MEMORY_OUT;
- goto cuddLinearAndSiftingOutOfMem;
+ table->errorCode = CUDD_MEMORY_OUT;
+ goto cuddLinearAndSiftingOutOfMem;
}
for (i = 0; i < size; i++) {
- x = table->perm[i];
- entry[i] = table->subtables[x].keys;
- var[i] = i;
+ x = table->perm[i];
+ entry[i] = table->subtables[x].keys;
+ var[i] = i;
}
- qsort((void *)var,size,sizeof(int),(int (*)(const void *, const void *))ddLinearUniqueCompare);
+ qsort((void *)var,size,sizeof(int),(DD_QSFP)ddLinearUniqueCompare);
/* Now sift. */
for (i = 0; i < ddMin(table->siftMaxVar,size); i++) {
- x = table->perm[var[i]];
- if (x < lower || x > upper) continue;
+ x = table->perm[var[i]];
+ if (x < lower || x > upper) continue;
#ifdef DD_STATS
- previousSize = table->keys - table->isolated;
+ previousSize = table->keys - table->isolated;
#endif
- result = ddLinearAndSiftingAux(table,x,lower,upper);
- if (!result) goto cuddLinearAndSiftingOutOfMem;
+ result = ddLinearAndSiftingAux(table,x,lower,upper);
+ if (!result) goto cuddLinearAndSiftingOutOfMem;
#ifdef DD_STATS
- if (table->keys < (unsigned) previousSize + table->isolated) {
- (void) fprintf(table->out,"-");
- } else if (table->keys > (unsigned) previousSize + table->isolated) {
- (void) fprintf(table->out,"+"); /* should never happen */
- (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keys - table->isolated, var[i]);
- } else {
- (void) fprintf(table->out,"=");
- }
- fflush(table->out);
+ if (table->keys < (unsigned) previousSize + table->isolated) {
+ (void) fprintf(table->out,"-");
+ } else if (table->keys > (unsigned) previousSize + table->isolated) {
+ (void) fprintf(table->out,"+"); /* should never happen */
+ (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keys - table->isolated, var[i]);
+ } else {
+ (void) fprintf(table->out,"=");
+ }
+ fflush(table->out);
#endif
#ifdef DD_DEBUG
- (void) Cudd_DebugCheck(table);
+ (void) Cudd_DebugCheck(table);
#endif
}
@@ -303,7 +327,7 @@ cuddLinearAndSifting(
#ifdef DD_STATS
(void) fprintf(table->out,"\n#:L_LINSIFT %8d: linear trans.",
- ddTotalNumberLinearTr);
+ ddTotalNumberLinearTr);
#endif
return(1);
@@ -313,11 +337,520 @@ cuddLinearAndSiftingOutOfMem:
if (entry != NULL) ABC_FREE(entry);
if (var != NULL) ABC_FREE(var);
- return(0);
+ return(0);
} /* end of cuddLinearAndSifting */
+/**Function********************************************************************
+
+ Synopsis [Linearly combines two adjacent variables.]
+
+ Description [Linearly combines two adjacent variables. Specifically,
+ replaces the top variable with the exclusive nor of the two variables.
+ It assumes that no dead nodes are present on entry to this
+ procedure. The procedure then guarantees that no dead nodes will be
+ present when it terminates. cuddLinearInPlace assumes that x &lt;
+ y. Returns the number of keys in the table if successful; 0
+ otherwise.]
+
+ SideEffects [The two subtables corrresponding to variables x and y are
+ modified. The global counters of the unique table are also affected.]
+
+ SeeAlso [cuddSwapInPlace]
+
+******************************************************************************/
+int
+cuddLinearInPlace(
+ DdManager * table,
+ int x,
+ int y)
+{
+ DdNodePtr *xlist, *ylist;
+ int xindex, yindex;
+ int xslots, yslots;
+ int xshift, yshift;
+ int oldxkeys, oldykeys;
+ int newxkeys, newykeys;
+ int comple, newcomplement;
+ int i;
+ int posn;
+ int isolated;
+ DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10,*newf1,*newf0;
+ DdNode *g,*next,*last;
+ DdNodePtr *previousP;
+ DdNode *tmp;
+ DdNode *sentinel = &(table->sentinel);
+#ifdef DD_DEBUG
+ int count, idcheck;
+#endif
+
+#ifdef DD_DEBUG
+ assert(x < y);
+ assert(cuddNextHigh(table,x) == y);
+ assert(table->subtables[x].keys != 0);
+ assert(table->subtables[y].keys != 0);
+ assert(table->subtables[x].dead == 0);
+ assert(table->subtables[y].dead == 0);
+#endif
+
+ xindex = table->invperm[x];
+ yindex = table->invperm[y];
+
+ if (cuddTestInteract(table,xindex,yindex)) {
+#ifdef DD_STATS
+ ddTotalNumberLinearTr++;
+#endif
+ /* Get parameters of x subtable. */
+ xlist = table->subtables[x].nodelist;
+ oldxkeys = table->subtables[x].keys;
+ xslots = table->subtables[x].slots;
+ xshift = table->subtables[x].shift;
+
+ /* Get parameters of y subtable. */
+ ylist = table->subtables[y].nodelist;
+ oldykeys = table->subtables[y].keys;
+ yslots = table->subtables[y].slots;
+ yshift = table->subtables[y].shift;
+
+ newxkeys = 0;
+ newykeys = oldykeys;
+
+ /* Check whether the two projection functions involved in this
+ ** swap are isolated. At the end, we'll be able to tell how many
+ ** isolated projection functions are there by checking only these
+ ** two functions again. This is done to eliminate the isolated
+ ** projection functions from the node count.
+ */
+ isolated = - ((table->vars[xindex]->ref == 1) +
+ (table->vars[yindex]->ref == 1));
+
+ /* The nodes in the x layer are put in a chain.
+ ** The chain is handled as a FIFO; g points to the beginning and
+ ** last points to the end.
+ */
+ g = NULL;
+#ifdef DD_DEBUG
+ last = NULL;
+#endif
+ 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 */
+#ifdef DD_DEBUG
+ /* last is always assigned in the for loop because there is at
+ ** least one key */
+ assert(last != NULL);
+#endif
+ 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 */
+
+#ifdef 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 []
+
+******************************************************************************/
+void
+cuddUpdateInteractionMatrix(
+ 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 cuddUpdateInteractionMatrix */
+
+
+/**Function********************************************************************
+
+ Synopsis [Initializes the linear transform matrix.]
+
+ Description [Initializes the linear transform matrix. Returns 1 if
+ successful; 0 otherwise.]
+
+ SideEffects [none]
+
+ SeeAlso []
+
+******************************************************************************/
+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 = ABC_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 [Resizes the linear transform matrix. Returns 1 if
+ successful; 0 otherwise.]
+
+ SideEffects [none]
+
+ SeeAlso []
+
+******************************************************************************/
+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 = ABC_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];
+ }
+ }
+ ABC_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 */
+
+
/*---------------------------------------------------------------------------*/
/* Definition of static functions */
/*---------------------------------------------------------------------------*/
@@ -342,7 +875,7 @@ ddLinearUniqueCompare(
{
#if 0
if (entry[*ptrY] == entry[*ptrX]) {
- return((*ptrX) - (*ptrY));
+ return((*ptrX) - (*ptrY));
}
#endif
return(entry[*ptrY] - entry[*ptrX]);
@@ -371,11 +904,11 @@ ddLinearAndSiftingAux(
int xHigh)
{
- Move *move;
- Move *moveUp; /* list of up moves */
- Move *moveDown; /* list of down moves */
- int initialSize;
- int result;
+ Move *move;
+ Move *moveUp; /* list of up moves */
+ Move *moveDown; /* list of down moves */
+ int initialSize;
+ int result;
initialSize = table->keys - table->isolated;
@@ -383,73 +916,73 @@ ddLinearAndSiftingAux(
moveUp = NULL;
if (x == xLow) {
- moveDown = ddLinearAndSiftingDown(table,x,xHigh,NULL);
- /* At this point x --> xHigh unless bounding occurred. */
- if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
- /* Move backward and stop at best position. */
- result = ddLinearAndSiftingBackward(table,initialSize,moveDown);
- if (!result) goto ddLinearAndSiftingAuxOutOfMem;
+ moveDown = ddLinearAndSiftingDown(table,x,xHigh,NULL);
+ /* At this point x --> xHigh unless bounding occurred. */
+ if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
+ /* Move backward and stop at best position. */
+ result = ddLinearAndSiftingBackward(table,initialSize,moveDown);
+ if (!result) goto ddLinearAndSiftingAuxOutOfMem;
} else if (x == xHigh) {
- moveUp = ddLinearAndSiftingUp(table,x,xLow,NULL);
- /* At this point x --> xLow unless bounding occurred. */
- if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
- /* Move backward and stop at best position. */
- result = ddLinearAndSiftingBackward(table,initialSize,moveUp);
- if (!result) goto ddLinearAndSiftingAuxOutOfMem;
+ moveUp = ddLinearAndSiftingUp(table,x,xLow,NULL);
+ /* At this point x --> xLow unless bounding occurred. */
+ if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
+ /* Move backward and stop at best position. */
+ result = ddLinearAndSiftingBackward(table,initialSize,moveUp);
+ if (!result) goto ddLinearAndSiftingAuxOutOfMem;
} else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */
- moveDown = ddLinearAndSiftingDown(table,x,xHigh,NULL);
- /* At this point x --> xHigh unless bounding occurred. */
- if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
- moveUp = ddUndoMoves(table,moveDown);
+ moveDown = ddLinearAndSiftingDown(table,x,xHigh,NULL);
+ /* At this point x --> xHigh unless bounding occurred. */
+ if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
+ moveUp = ddUndoMoves(table,moveDown);
#ifdef DD_DEBUG
- assert(moveUp == NULL || moveUp->x == x);
+ assert(moveUp == NULL || moveUp->x == x);
#endif
- moveUp = ddLinearAndSiftingUp(table,x,xLow,moveUp);
- if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
- /* Move backward and stop at best position. */
- result = ddLinearAndSiftingBackward(table,initialSize,moveUp);
- if (!result) goto ddLinearAndSiftingAuxOutOfMem;
+ moveUp = ddLinearAndSiftingUp(table,x,xLow,moveUp);
+ if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
+ /* Move backward and stop at best position. */
+ result = ddLinearAndSiftingBackward(table,initialSize,moveUp);
+ if (!result) goto ddLinearAndSiftingAuxOutOfMem;
} else { /* must go up first: shorter */
- moveUp = ddLinearAndSiftingUp(table,x,xLow,NULL);
- /* At this point x --> xLow unless bounding occurred. */
- if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
- moveDown = ddUndoMoves(table,moveUp);
+ moveUp = ddLinearAndSiftingUp(table,x,xLow,NULL);
+ /* At this point x --> xLow unless bounding occurred. */
+ if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
+ moveDown = ddUndoMoves(table,moveUp);
#ifdef DD_DEBUG
- assert(moveDown == NULL || moveDown->y == x);
+ assert(moveDown == NULL || moveDown->y == x);
#endif
- moveDown = ddLinearAndSiftingDown(table,x,xHigh,moveDown);
- if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
- /* Move backward and stop at best position. */
- result = ddLinearAndSiftingBackward(table,initialSize,moveDown);
- if (!result) goto ddLinearAndSiftingAuxOutOfMem;
+ moveDown = ddLinearAndSiftingDown(table,x,xHigh,moveDown);
+ if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
+ /* Move backward and stop at best position. */
+ result = ddLinearAndSiftingBackward(table,initialSize,moveDown);
+ if (!result) goto ddLinearAndSiftingAuxOutOfMem;
}
while (moveDown != NULL) {
- move = moveDown->next;
- cuddDeallocNode(table, (DdNode *) moveDown);
- moveDown = move;
+ move = moveDown->next;
+ cuddDeallocMove(table, moveDown);
+ moveDown = move;
}
while (moveUp != NULL) {
- move = moveUp->next;
- cuddDeallocNode(table, (DdNode *) moveUp);
- moveUp = move;
+ move = moveUp->next;
+ cuddDeallocMove(table, moveUp);
+ moveUp = move;
}
return(1);
ddLinearAndSiftingAuxOutOfMem:
while (moveDown != NULL) {
- move = moveDown->next;
- cuddDeallocNode(table, (DdNode *) moveDown);
- moveDown = move;
+ move = moveDown->next;
+ cuddDeallocMove(table, moveDown);
+ moveDown = move;
}
while (moveUp != NULL) {
- move = moveUp->next;
- cuddDeallocNode(table, (DdNode *) moveUp);
- moveUp = move;
+ move = moveUp->next;
+ cuddDeallocMove(table, moveUp);
+ moveUp = move;
}
return(0);
@@ -476,14 +1009,14 @@ ddLinearAndSiftingUp(
int xLow,
Move * prevMoves)
{
- Move *moves;
- Move *move;
- int x;
- int size, newsize;
- int limitSize;
- int xindex, yindex;
- int isolated;
- int L; /* lower bound on DD size */
+ Move *moves;
+ Move *move;
+ int x;
+ int size, newsize;
+ int limitSize;
+ int xindex, yindex;
+ int isolated;
+ int L; /* lower bound on DD size */
#ifdef DD_DEBUG
int checkL;
int z;
@@ -501,84 +1034,84 @@ ddLinearAndSiftingUp(
*/
limitSize = L = table->keys - table->isolated;
for (x = xLow + 1; x < y; x++) {
- xindex = table->invperm[x];
- if (cuddTestInteract(table,xindex,yindex)) {
- isolated = table->vars[xindex]->ref == 1;
- L -= table->subtables[x].keys - isolated;
- }
+ xindex = table->invperm[x];
+ if (cuddTestInteract(table,xindex,yindex)) {
+ isolated = table->vars[xindex]->ref == 1;
+ L -= table->subtables[x].keys - isolated;
+ }
}
isolated = table->vars[yindex]->ref == 1;
L -= table->subtables[y].keys - isolated;
x = cuddNextLow(table,y);
while (x >= xLow && L <= limitSize) {
- xindex = table->invperm[x];
+ xindex = table->invperm[x];
#ifdef DD_DEBUG
- checkL = table->keys - table->isolated;
- for (z = xLow + 1; z < y; z++) {
- zindex = table->invperm[z];
- if (cuddTestInteract(table,zindex,yindex)) {
- isolated = table->vars[zindex]->ref == 1;
- checkL -= table->subtables[z].keys - isolated;
+ checkL = table->keys - table->isolated;
+ for (z = xLow + 1; z < y; z++) {
+ zindex = table->invperm[z];
+ if (cuddTestInteract(table,zindex,yindex)) {
+ isolated = table->vars[zindex]->ref == 1;
+ checkL -= table->subtables[z].keys - isolated;
+ }
+ }
+ isolated = table->vars[yindex]->ref == 1;
+ checkL -= table->subtables[y].keys - isolated;
+ if (L != checkL) {
+ (void) fprintf(table->out, "checkL(%d) != L(%d)\n",checkL,L);
}
- }
- isolated = table->vars[yindex]->ref == 1;
- checkL -= table->subtables[y].keys - isolated;
- if (L != checkL) {
- (void) fprintf(table->out, "checkL(%d) != L(%d)\n",checkL,L);
- }
#endif
- size = cuddSwapInPlace(table,x,y);
- if (size == 0) goto ddLinearAndSiftingUpOutOfMem;
- newsize = cuddLinearInPlace(table,x,y);
- if (newsize == 0) goto ddLinearAndSiftingUpOutOfMem;
- move = (Move *) cuddDynamicAllocNode(table);
- if (move == NULL) goto ddLinearAndSiftingUpOutOfMem;
- move->x = x;
- move->y = y;
- move->next = moves;
- moves = move;
- move->flags = CUDD_SWAP_MOVE;
- if (newsize >= size) {
- /* Undo transformation. The transformation we apply is
- ** its own inverse. Hence, we just apply the transformation
- ** again.
- */
+ size = cuddSwapInPlace(table,x,y);
+ if (size == 0) goto ddLinearAndSiftingUpOutOfMem;
newsize = cuddLinearInPlace(table,x,y);
if (newsize == 0) goto ddLinearAndSiftingUpOutOfMem;
+ move = (Move *) cuddDynamicAllocNode(table);
+ if (move == NULL) goto ddLinearAndSiftingUpOutOfMem;
+ move->x = x;
+ move->y = y;
+ move->next = moves;
+ moves = move;
+ move->flags = CUDD_SWAP_MOVE;
+ if (newsize >= size) {
+ /* Undo transformation. The transformation we apply is
+ ** its own inverse. Hence, we just apply the transformation
+ ** again.
+ */
+ newsize = cuddLinearInPlace(table,x,y);
+ if (newsize == 0) goto ddLinearAndSiftingUpOutOfMem;
#ifdef DD_DEBUG
- if (newsize != size) {
- (void) fprintf(table->out,"Change in size after identity transformation! From %d to %d\n",size,newsize);
- }
+ if (newsize != size) {
+ (void) fprintf(table->out,"Change in size after identity transformation! From %d to %d\n",size,newsize);
+ }
#endif
- } else if (cuddTestInteract(table,xindex,yindex)) {
- size = newsize;
- move->flags = CUDD_LINEAR_TRANSFORM_MOVE;
- ddUpdateInteractionMatrix(table,xindex,yindex);
- }
- move->size = size;
- /* Update the lower bound. */
- if (cuddTestInteract(table,xindex,yindex)) {
- isolated = table->vars[xindex]->ref == 1;
- L += table->subtables[y].keys - isolated;
- }
- if ((double) size > (double) limitSize * table->maxGrowth) break;
- if (size < limitSize) limitSize = size;
- y = x;
- x = cuddNextLow(table,y);
+ } else if (cuddTestInteract(table,xindex,yindex)) {
+ size = newsize;
+ move->flags = CUDD_LINEAR_TRANSFORM_MOVE;
+ cuddUpdateInteractionMatrix(table,xindex,yindex);
+ }
+ move->size = size;
+ /* Update the lower bound. */
+ if (cuddTestInteract(table,xindex,yindex)) {
+ isolated = table->vars[xindex]->ref == 1;
+ L += table->subtables[y].keys - isolated;
+ }
+ if ((double) size > (double) limitSize * table->maxGrowth) break;
+ if (size < limitSize) limitSize = size;
+ y = x;
+ x = cuddNextLow(table,y);
}
return(moves);
ddLinearAndSiftingUpOutOfMem:
while (moves != NULL) {
- move = moves->next;
- cuddDeallocNode(table, (DdNode *) moves);
- moves = move;
+ move = moves->next;
+ cuddDeallocMove(table, moves);
+ moves = move;
}
return((Move *) CUDD_OUT_OF_MEM);
} /* end of ddLinearAndSiftingUp */
-
+
/**Function********************************************************************
@@ -599,18 +1132,18 @@ ddLinearAndSiftingDown(
int xHigh,
Move * prevMoves)
{
- Move *moves;
- Move *move;
- int y;
- int size, newsize;
- int R; /* upper bound on node decrease */
- int limitSize;
- int xindex, yindex;
- int isolated;
+ Move *moves;
+ Move *move;
+ int y;
+ int size, newsize;
+ int R; /* upper bound on node decrease */
+ int limitSize;
+ int xindex, yindex;
+ int isolated;
#ifdef DD_DEBUG
- int checkR;
- int z;
- int zindex;
+ int checkR;
+ int z;
+ int zindex;
#endif
moves = prevMoves;
@@ -619,73 +1152,73 @@ ddLinearAndSiftingDown(
limitSize = size = table->keys - table->isolated;
R = 0;
for (y = xHigh; y > x; y--) {
- yindex = table->invperm[y];
- if (cuddTestInteract(table,xindex,yindex)) {
- isolated = table->vars[yindex]->ref == 1;
- R += table->subtables[y].keys - isolated;
- }
+ yindex = table->invperm[y];
+ if (cuddTestInteract(table,xindex,yindex)) {
+ isolated = table->vars[yindex]->ref == 1;
+ R += table->subtables[y].keys - isolated;
+ }
}
y = cuddNextHigh(table,x);
while (y <= xHigh && size - R < limitSize) {
#ifdef DD_DEBUG
- checkR = 0;
- for (z = xHigh; z > x; z--) {
- zindex = table->invperm[z];
- if (cuddTestInteract(table,xindex,zindex)) {
- isolated = table->vars[zindex]->ref == 1;
- checkR += table->subtables[z].keys - isolated;
+ checkR = 0;
+ for (z = xHigh; z > x; z--) {
+ zindex = table->invperm[z];
+ if (cuddTestInteract(table,xindex,zindex)) {
+ isolated = table->vars[zindex]->ref == 1;
+ checkR += table->subtables[z].keys - isolated;
+ }
+ }
+ if (R != checkR) {
+ (void) fprintf(table->out, "checkR(%d) != R(%d)\n",checkR,R);
}
- }
- if (R != checkR) {
- (void) fprintf(table->out, "checkR(%d) != R(%d)\n",checkR,R);
- }
#endif
- /* Update upper bound on node decrease. */
- yindex = table->invperm[y];
- if (cuddTestInteract(table,xindex,yindex)) {
- isolated = table->vars[yindex]->ref == 1;
- R -= table->subtables[y].keys - isolated;
- }
- size = cuddSwapInPlace(table,x,y);
- if (size == 0) goto ddLinearAndSiftingDownOutOfMem;
- newsize = cuddLinearInPlace(table,x,y);
- if (newsize == 0) goto ddLinearAndSiftingDownOutOfMem;
- move = (Move *) cuddDynamicAllocNode(table);
- if (move == NULL) goto ddLinearAndSiftingDownOutOfMem;
- move->x = x;
- move->y = y;
- move->next = moves;
- moves = move;
- move->flags = CUDD_SWAP_MOVE;
- if (newsize >= size) {
- /* Undo transformation. The transformation we apply is
- ** its own inverse. Hence, we just apply the transformation
- ** again.
- */
+ /* Update upper bound on node decrease. */
+ yindex = table->invperm[y];
+ if (cuddTestInteract(table,xindex,yindex)) {
+ isolated = table->vars[yindex]->ref == 1;
+ R -= table->subtables[y].keys - isolated;
+ }
+ size = cuddSwapInPlace(table,x,y);
+ if (size == 0) goto ddLinearAndSiftingDownOutOfMem;
newsize = cuddLinearInPlace(table,x,y);
if (newsize == 0) goto ddLinearAndSiftingDownOutOfMem;
- if (newsize != size) {
- (void) fprintf(table->out,"Change in size after identity transformation! From %d to %d\n",size,newsize);
+ move = (Move *) cuddDynamicAllocNode(table);
+ if (move == NULL) goto ddLinearAndSiftingDownOutOfMem;
+ move->x = x;
+ move->y = y;
+ move->next = moves;
+ moves = move;
+ move->flags = CUDD_SWAP_MOVE;
+ if (newsize >= size) {
+ /* Undo transformation. The transformation we apply is
+ ** its own inverse. Hence, we just apply the transformation
+ ** again.
+ */
+ newsize = cuddLinearInPlace(table,x,y);
+ if (newsize == 0) goto ddLinearAndSiftingDownOutOfMem;
+ if (newsize != size) {
+ (void) fprintf(table->out,"Change in size after identity transformation! From %d to %d\n",size,newsize);
+ }
+ } else if (cuddTestInteract(table,xindex,yindex)) {
+ size = newsize;
+ move->flags = CUDD_LINEAR_TRANSFORM_MOVE;
+ cuddUpdateInteractionMatrix(table,xindex,yindex);
}
- } else if (cuddTestInteract(table,xindex,yindex)) {
- size = newsize;
- move->flags = CUDD_LINEAR_TRANSFORM_MOVE;
- ddUpdateInteractionMatrix(table,xindex,yindex);
- }
- move->size = size;
- if ((double) size > (double) limitSize * table->maxGrowth) break;
- if (size < limitSize) limitSize = size;
- x = y;
- y = cuddNextHigh(table,x);
+ move->size = size;
+ if ((double) size > (double) limitSize * table->maxGrowth) break;
+ if (size < limitSize) limitSize = size;
+ x = y;
+ y = cuddNextHigh(table,x);
}
return(moves);
ddLinearAndSiftingDownOutOfMem:
while (moves != NULL) {
- move = moves->next;
- cuddDeallocNode(table, (DdNode *) moves);
- moves = move;
+ move = moves->next;
+ cuddDeallocMove(table, moves);
+ moves = move;
}
return((Move *) CUDD_OUT_OF_MEM);
@@ -712,26 +1245,26 @@ ddLinearAndSiftingBackward(
Move * moves)
{
Move *move;
- int res;
+ int res;
for (move = moves; move != NULL; move = move->next) {
- if (move->size < size) {
- size = move->size;
- }
+ if (move->size < size) {
+ size = move->size;
+ }
}
for (move = moves; move != NULL; move = move->next) {
- if (move->size == size) return(1);
- if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) {
- res = cuddLinearInPlace(table,(int)move->x,(int)move->y);
- if (!res) return(0);
- }
- res = cuddSwapInPlace(table,(int)move->x,(int)move->y);
- if (!res) return(0);
- if (move->flags == CUDD_INVERSE_TRANSFORM_MOVE) {
- res = cuddLinearInPlace(table,(int)move->x,(int)move->y);
+ if (move->size == size) return(1);
+ if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) {
+ res = cuddLinearInPlace(table,(int)move->x,(int)move->y);
+ if (!res) return(0);
+ }
+ res = cuddSwapInPlace(table,(int)move->x,(int)move->y);
if (!res) return(0);
- }
+ if (move->flags == CUDD_INVERSE_TRANSFORM_MOVE) {
+ res = cuddLinearInPlace(table,(int)move->x,(int)move->y);
+ if (!res) return(0);
+ }
}
return(1);
@@ -759,45 +1292,45 @@ ddUndoMoves(
Move *invmoves = NULL;
Move *move;
Move *invmove;
- int size;
+ int size;
for (move = moves; move != NULL; move = move->next) {
- invmove = (Move *) cuddDynamicAllocNode(table);
- if (invmove == NULL) goto ddUndoMovesOutOfMem;
- invmove->x = move->x;
- invmove->y = move->y;
- invmove->next = invmoves;
- invmoves = invmove;
- if (move->flags == CUDD_SWAP_MOVE) {
- invmove->flags = CUDD_SWAP_MOVE;
- size = cuddSwapInPlace(table,(int)move->x,(int)move->y);
- if (!size) goto ddUndoMovesOutOfMem;
- } else if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) {
- invmove->flags = CUDD_INVERSE_TRANSFORM_MOVE;
- size = cuddLinearInPlace(table,(int)move->x,(int)move->y);
- if (!size) goto ddUndoMovesOutOfMem;
- size = cuddSwapInPlace(table,(int)move->x,(int)move->y);
- if (!size) goto ddUndoMovesOutOfMem;
- } else { /* must be CUDD_INVERSE_TRANSFORM_MOVE */
+ invmove = (Move *) cuddDynamicAllocNode(table);
+ if (invmove == NULL) goto ddUndoMovesOutOfMem;
+ invmove->x = move->x;
+ invmove->y = move->y;
+ invmove->next = invmoves;
+ invmoves = invmove;
+ if (move->flags == CUDD_SWAP_MOVE) {
+ invmove->flags = CUDD_SWAP_MOVE;
+ size = cuddSwapInPlace(table,(int)move->x,(int)move->y);
+ if (!size) goto ddUndoMovesOutOfMem;
+ } else if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) {
+ invmove->flags = CUDD_INVERSE_TRANSFORM_MOVE;
+ size = cuddLinearInPlace(table,(int)move->x,(int)move->y);
+ if (!size) goto ddUndoMovesOutOfMem;
+ size = cuddSwapInPlace(table,(int)move->x,(int)move->y);
+ if (!size) goto ddUndoMovesOutOfMem;
+ } else { /* must be CUDD_INVERSE_TRANSFORM_MOVE */
#ifdef DD_DEBUG
- (void) fprintf(table->err,"Unforseen event in ddUndoMoves!\n");
+ (void) fprintf(table->err,"Unforseen event in ddUndoMoves!\n");
#endif
- invmove->flags = CUDD_LINEAR_TRANSFORM_MOVE;
- size = cuddSwapInPlace(table,(int)move->x,(int)move->y);
- if (!size) goto ddUndoMovesOutOfMem;
- size = cuddLinearInPlace(table,(int)move->x,(int)move->y);
- if (!size) goto ddUndoMovesOutOfMem;
- }
- invmove->size = size;
+ invmove->flags = CUDD_LINEAR_TRANSFORM_MOVE;
+ size = cuddSwapInPlace(table,(int)move->x,(int)move->y);
+ if (!size) goto ddUndoMovesOutOfMem;
+ size = cuddLinearInPlace(table,(int)move->x,(int)move->y);
+ if (!size) goto ddUndoMovesOutOfMem;
+ }
+ invmove->size = size;
}
return(invmoves);
ddUndoMovesOutOfMem:
while (invmoves != NULL) {
- move = invmoves->next;
- cuddDeallocNode(table, (DdNode *) invmoves);
- invmoves = move;
+ move = invmoves->next;
+ cuddDeallocMove(table, invmoves);
+ invmoves = move;
}
return((Move *) CUDD_OUT_OF_MEM);
@@ -805,506 +1338,7 @@ ddUndoMovesOutOfMem:
/**Function********************************************************************
-
- Synopsis [Linearly combines two adjacent variables.]
-
- Description [Linearly combines two adjacent variables. Specifically,
- replaces the top variable with the exclusive nor of the two variables.
- It assumes that no dead nodes are present on entry to this
- procedure. The procedure then guarantees that no dead nodes will be
- present when it terminates. cuddLinearInPlace assumes that x &lt;
- y. Returns the number of keys in the table if successful; 0
- otherwise.]
-
- SideEffects [The two subtables corrresponding to variables x and y are
- modified. The global counters of the unique table are also affected.]
-
- SeeAlso [cuddSwapInPlace]
-
-******************************************************************************/
-static int
-cuddLinearInPlace(
- DdManager * table,
- int x,
- int y)
-{
- DdNodePtr *xlist, *ylist;
- int xindex, yindex;
- int xslots, yslots;
- int xshift, yshift;
- int oldxkeys, oldykeys;
- int newxkeys, newykeys;
- int comple, newcomplement;
- int i;
- int posn;
- int isolated;
- DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10,*newf1,*newf0;
- DdNode *g,*next,*last = NULL; // Suppress "might be used uninitialized"
- DdNodePtr *previousP;
- DdNode *tmp;
- DdNode *sentinel = &(table->sentinel);
-#if DD_DEBUG
- int count, idcheck;
-#endif
-
-#ifdef DD_DEBUG
- assert(x < y);
- assert(cuddNextHigh(table,x) == y);
- assert(table->subtables[x].keys != 0);
- assert(table->subtables[y].keys != 0);
- assert(table->subtables[x].dead == 0);
- assert(table->subtables[y].dead == 0);
-#endif
-
- xindex = table->invperm[x];
- yindex = table->invperm[y];
-
- if (cuddTestInteract(table,xindex,yindex)) {
-#ifdef DD_STATS
- ddTotalNumberLinearTr++;
-#endif
- /* Get parameters of x subtable. */
- xlist = table->subtables[x].nodelist;
- oldxkeys = table->subtables[x].keys;
- xslots = table->subtables[x].slots;
- xshift = table->subtables[x].shift;
-
- /* Get parameters of y subtable. */
- ylist = table->subtables[y].nodelist;
- oldykeys = table->subtables[y].keys;
- yslots = table->subtables[y].slots;
- yshift = table->subtables[y].shift;
-
- newxkeys = 0;
- newykeys = oldykeys;
-
- /* Check whether the two projection functions involved in this
- ** swap are isolated. At the end, we'll be able to tell how many
- ** isolated projection functions are there by checking only these
- ** two functions again. This is done to eliminate the isolated
- ** projection functions from the node count.
- */
- isolated = - ((table->vars[xindex]->ref == 1) +
- (table->vars[yindex]->ref == 1));
-
- /* The nodes in the x layer are put in a chain.
- ** The chain is handled as a FIFO; g points to the beginning and
- ** last points to the end.
- */
- 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 = ABC_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 = ABC_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];
- }
- }
- ABC_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
@@ -1329,10 +1363,11 @@ cuddXorLinear(
long *linear = table->linear;
for (i = 0; i < wordsPerRow; i++) {
- linear[xstart+i] ^= linear[ystart+i];
+ linear[xstart+i] ^= linear[ystart+i];
}
} /* end of cuddXorLinear */
+
ABC_NAMESPACE_IMPL_END
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 21:36:38 +0000