src/cuBdd/cuddZddLin.c File Reference

#include "util.h"
#include "cuddInt.h"
Include dependency graph for cuddZddLin.c:

Go to the source code of this file.

Defines

#define CUDD_SWAP_MOVE   0
#define CUDD_LINEAR_TRANSFORM_MOVE   1
#define CUDD_INVERSE_TRANSFORM_MOVE   2

Functions

static int cuddZddLinearInPlace (DdManager *table, int x, int y)
static int cuddZddLinearAux (DdManager *table, int x, int xLow, int xHigh)
static Move * cuddZddLinearUp (DdManager *table, int y, int xLow, Move *prevMoves)
static Move * cuddZddLinearDown (DdManager *table, int x, int xHigh, Move *prevMoves)
static int cuddZddLinearBackward (DdManager *table, int size, Move *moves)
static Move * cuddZddUndoMoves (DdManager *table, Move *moves)
int cuddZddLinearSifting (DdManager *table, int lower, int upper)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddZddLin.c,v 1.14 2004/08/13 18:04:53 fabio Exp $"
int * zdd_entry
int zddTotalNumberSwapping
static int zddTotalNumberLinearTr
static DdNode * empty

Define Documentation

#define CUDD_INVERSE_TRANSFORM_MOVE   2

Definition at line 71 of file cuddZddLin.c.

#define CUDD_LINEAR_TRANSFORM_MOVE   1

Definition at line 70 of file cuddZddLin.c.

#define CUDD_SWAP_MOVE   0

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

FileName [cuddZddLin.c]

PackageName [cudd]

Synopsis [Procedures for dynamic variable ordering of ZDDs.]

Description [Internal procedures included in this module:

Static procedures included in this module:

]

SeeAlso [cuddLinear.c cuddZddReord.c]

Author [Fabio Somenzi]

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

Definition at line 69 of file cuddZddLin.c.

Function Documentation

static int cuddZddLinearAux ( DdManager *  table,
int  x,
int  xLow,
int  xHigh 
) [static]

Function********************************************************************

Synopsis [Given xLow <= x <= xHigh moves x up and down between the boundaries.]

Description [Given xLow <= x <= xHigh moves x up and down between the boundaries. Finds the best position and does the required changes. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 573 of file cuddZddLin.c.

00578 {
00579     Move        *move;
00580     Move        *moveUp;        /* list of up move */
00581     Move        *moveDown;      /* list of down move */
00582 
00583     int         initial_size;
00584     int         result;
00585 
00586     initial_size = table->keysZ;
00587 
00588 #ifdef DD_DEBUG
00589     assert(table->subtableZ[x].keys > 0);
00590 #endif
00591 
00592     moveDown = NULL;
00593     moveUp = NULL;
00594 
00595     if (x == xLow) {
00596         moveDown = cuddZddLinearDown(table, x, xHigh, NULL);
00597         /* At this point x --> xHigh. */
00598         if (moveDown == (Move *) CUDD_OUT_OF_MEM)
00599             goto cuddZddLinearAuxOutOfMem;
00600         /* Move backward and stop at best position. */
00601         result = cuddZddLinearBackward(table, initial_size, moveDown);
00602         if (!result)
00603             goto cuddZddLinearAuxOutOfMem;
00604 
00605     } else if (x == xHigh) {
00606         moveUp = cuddZddLinearUp(table, x, xLow, NULL);
00607         /* At this point x --> xLow. */
00608         if (moveUp == (Move *) CUDD_OUT_OF_MEM)
00609             goto cuddZddLinearAuxOutOfMem;
00610         /* Move backward and stop at best position. */
00611         result = cuddZddLinearBackward(table, initial_size, moveUp);
00612         if (!result)
00613             goto cuddZddLinearAuxOutOfMem;
00614 
00615     } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */
00616         moveDown = cuddZddLinearDown(table, x, xHigh, NULL);
00617         /* At this point x --> xHigh. */
00618         if (moveDown == (Move *) CUDD_OUT_OF_MEM)
00619             goto cuddZddLinearAuxOutOfMem;
00620         moveUp = cuddZddUndoMoves(table,moveDown);
00621 #ifdef DD_DEBUG
00622         assert(moveUp == NULL || moveUp->x == x);
00623 #endif
00624         moveUp = cuddZddLinearUp(table, x, xLow, moveUp);
00625         if (moveUp == (Move *) CUDD_OUT_OF_MEM)
00626             goto cuddZddLinearAuxOutOfMem;
00627         /* Move backward and stop at best position. */
00628         result = cuddZddLinearBackward(table, initial_size, moveUp);
00629         if (!result)
00630             goto cuddZddLinearAuxOutOfMem;
00631 
00632     } else {
00633         moveUp = cuddZddLinearUp(table, x, xLow, NULL);
00634         /* At this point x --> xHigh. */
00635         if (moveUp == (Move *) CUDD_OUT_OF_MEM)
00636             goto cuddZddLinearAuxOutOfMem;
00637         /* Then move up. */
00638         moveDown = cuddZddUndoMoves(table,moveUp);
00639 #ifdef DD_DEBUG
00640         assert(moveDown == NULL || moveDown->y == x);
00641 #endif
00642         moveDown = cuddZddLinearDown(table, x, xHigh, moveDown);
00643         if (moveDown == (Move *) CUDD_OUT_OF_MEM)
00644             goto cuddZddLinearAuxOutOfMem;
00645         /* Move backward and stop at best position. */
00646         result = cuddZddLinearBackward(table, initial_size, moveDown);
00647         if (!result)
00648             goto cuddZddLinearAuxOutOfMem;
00649     }
00650 
00651     while (moveDown != NULL) {
00652         move = moveDown->next;
00653         cuddDeallocMove(table, moveDown);
00654         moveDown = move;
00655     }
00656     while (moveUp != NULL) {
00657         move = moveUp->next;
00658         cuddDeallocMove(table, moveUp);
00659         moveUp = move;
00660     }
00661 
00662     return(1);
00663 
00664 cuddZddLinearAuxOutOfMem:
00665     if (moveDown != (Move *) CUDD_OUT_OF_MEM) {
00666         while (moveDown != NULL) {
00667             move = moveDown->next;
00668             cuddDeallocMove(table, moveDown);
00669             moveDown = move;
00670         }
00671     }
00672     if (moveUp != (Move *) CUDD_OUT_OF_MEM) {
00673         while (moveUp != NULL) {
00674             move = moveUp->next;
00675             cuddDeallocMove(table, moveUp);
00676             moveUp = move;
00677         }
00678     }
00679 
00680     return(0);
00681 
00682 } /* end of cuddZddLinearAux */

static int cuddZddLinearBackward ( DdManager *  table,
int  size,
Move *  moves 
) [static]

Function********************************************************************

Synopsis [Given a set of moves, returns the ZDD heap to the position giving the minimum size.]

Description [Given a set of moves, returns the ZDD heap to the position giving the minimum size. In case of ties, returns to the closest position giving the minimum size. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 869 of file cuddZddLin.c.

00873 {
00874     Move        *move;
00875     int         res;
00876 
00877     /* Find the minimum size among moves. */
00878     for (move = moves; move != NULL; move = move->next) {
00879         if (move->size < size) {
00880             size = move->size;
00881         }
00882     }
00883 
00884     for (move = moves; move != NULL; move = move->next) {
00885         if (move->size == size) return(1);
00886         if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) {
00887             res = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
00888             if (!res) return(0);
00889         }
00890         res = cuddZddSwapInPlace(table, move->x, move->y);
00891         if (!res)
00892             return(0);
00893         if (move->flags == CUDD_INVERSE_TRANSFORM_MOVE) {
00894             res = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
00895             if (!res) return(0);
00896         }
00897     }
00898 
00899     return(1);
00900 
00901 } /* end of cuddZddLinearBackward */

static Move * cuddZddLinearDown ( DdManager *  table,
int  x,
int  xHigh,
Move *  prevMoves 
) [static]

Function********************************************************************

Synopsis [Sifts a variable down and applies the XOR transformation.]

Description [Sifts a variable down. Moves x down until either it reaches the bound (xHigh) or the size of the ZDD heap increases too much. Returns the set of moves in case of success; NULL if memory is full.]

SideEffects [None]

SeeAlso []

Definition at line 785 of file cuddZddLin.c.

00790 {
00791     Move        *moves;
00792     Move        *move;
00793     int         y;
00794     int         size, newsize;
00795     int         limitSize;
00796 
00797     moves = prevMoves;
00798     limitSize = table->keysZ;
00799 
00800     y = cuddZddNextHigh(table, x);
00801     while (y <= xHigh) {
00802         size = cuddZddSwapInPlace(table, x, y);
00803         if (size == 0)
00804             goto cuddZddLinearDownOutOfMem;
00805         newsize = cuddZddLinearInPlace(table, x, y);
00806         if (newsize == 0)
00807             goto cuddZddLinearDownOutOfMem;
00808         move = (Move *) cuddDynamicAllocNode(table);
00809         if (move == NULL)
00810             goto cuddZddLinearDownOutOfMem;
00811         move->x = x;
00812         move->y = y;
00813         move->next = moves;
00814         moves = move;
00815         move->flags = CUDD_SWAP_MOVE;
00816         if (newsize > size) {
00817             /* Undo transformation. The transformation we apply is
00818             ** its own inverse. Hence, we just apply the transformation
00819             ** again.
00820             */
00821             newsize = cuddZddLinearInPlace(table,x,y);
00822             if (newsize == 0) goto cuddZddLinearDownOutOfMem;
00823             if (newsize != size) {
00824                 (void) fprintf(table->err,"Change in size after identity transformation! From %d to %d\n",size,newsize);
00825             }
00826         } else {
00827             size = newsize;
00828             move->flags = CUDD_LINEAR_TRANSFORM_MOVE;
00829         }
00830         move->size = size;
00831 
00832         if ((double)size > (double)limitSize * table->maxGrowth)
00833             break;
00834         if (size < limitSize)
00835             limitSize = size;
00836 
00837         x = y;
00838         y = cuddZddNextHigh(table, x);
00839     }
00840     return(moves);
00841 
00842 cuddZddLinearDownOutOfMem:
00843     while (moves != NULL) {
00844         move = moves->next;
00845         cuddDeallocMove(table, moves);
00846         moves = move;
00847     }
00848     return((Move *) CUDD_OUT_OF_MEM);
00849 
00850 } /* end of cuddZddLinearDown */

static int cuddZddLinearInPlace ( DdManager *  table,
int  x,
int  y 
) [static]

AutomaticStart

Function********************************************************************

Synopsis [Linearly combines two adjacent variables.]

Description [Linearly combines two adjacent 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. cuddZddLinearInPlace assumes that x < y. Returns the number of keys in the table if successful; 0 otherwise.]

SideEffects [None]

SeeAlso [cuddZddSwapInPlace cuddLinearInPlace]

Definition at line 251 of file cuddZddLin.c.

00255 {
00256     DdNodePtr *xlist, *ylist;
00257     int         xindex, yindex;
00258     int         xslots, yslots;
00259     int         xshift, yshift;
00260     int         oldxkeys, oldykeys;
00261     int         newxkeys, newykeys;
00262     int         i;
00263     int         posn;
00264     DdNode      *f, *f1, *f0, *f11, *f10, *f01, *f00;
00265     DdNode      *newf1, *newf0, *g, *next, *previous;
00266     DdNode      *special;
00267 
00268 #ifdef DD_DEBUG
00269     assert(x < y);
00270     assert(cuddZddNextHigh(table,x) == y);
00271     assert(table->subtableZ[x].keys != 0);
00272     assert(table->subtableZ[y].keys != 0);
00273     assert(table->subtableZ[x].dead == 0);
00274     assert(table->subtableZ[y].dead == 0);
00275 #endif
00276 
00277     zddTotalNumberLinearTr++;
00278 
00279     /* Get parameters of x subtable. */
00280     xindex   = table->invpermZ[x];
00281     xlist    = table->subtableZ[x].nodelist;
00282     oldxkeys = table->subtableZ[x].keys;
00283     xslots   = table->subtableZ[x].slots;
00284     xshift   = table->subtableZ[x].shift;
00285     newxkeys = 0;
00286 
00287     /* Get parameters of y subtable. */
00288     yindex   = table->invpermZ[y];
00289     ylist    = table->subtableZ[y].nodelist;
00290     oldykeys = table->subtableZ[y].keys;
00291     yslots   = table->subtableZ[y].slots;
00292     yshift   = table->subtableZ[y].shift;
00293     newykeys = oldykeys;
00294 
00295     /* The nodes in the x layer are put in two chains.  The chain
00296     ** pointed by g holds the normal nodes. When re-expressed they stay
00297     ** in the x list. The chain pointed by special holds the elements
00298     ** that will move to the y list.
00299     */
00300     g = special = NULL;
00301     for (i = 0; i < xslots; i++) {
00302         f = xlist[i];
00303         if (f == NULL) continue;
00304         xlist[i] = NULL;
00305         while (f != NULL) {
00306             next = f->next;
00307             f1 = cuddT(f);
00308             /* if (f1->index == yindex) */ cuddSatDec(f1->ref);
00309             f0 = cuddE(f);
00310             /* if (f0->index == yindex) */ cuddSatDec(f0->ref);
00311             if ((int) f1->index == yindex && cuddE(f1) == empty &&
00312                 (int) f0->index != yindex) {
00313                 f->next = special;
00314                 special = f;
00315             } else {
00316                 f->next = g;
00317                 g = f;
00318             }
00319             f = next;
00320         } /* while there are elements in the collision chain */
00321     } /* for each slot of the x subtable */
00322 
00323     /* Mark y nodes with pointers from above x. We mark them by
00324     **  changing their index to x.
00325     */
00326     for (i = 0; i < yslots; i++) {
00327         f = ylist[i];
00328         while (f != NULL) {
00329             if (f->ref != 0) {
00330                 f->index = xindex;
00331             }
00332             f = f->next;
00333         } /* while there are elements in the collision chain */
00334     } /* for each slot of the y subtable */
00335 
00336     /* Move special nodes to the y list. */
00337     f = special;
00338     while (f != NULL) {
00339         next = f->next;
00340         f1 = cuddT(f);
00341         f11 = cuddT(f1);
00342         cuddT(f) = f11;
00343         cuddSatInc(f11->ref);
00344         f0 = cuddE(f);
00345         cuddSatInc(f0->ref);
00346         f->index = yindex;
00347         /* Insert at the beginning of the list so that it will be
00348         ** found first if there is a duplicate. The duplicate will
00349         ** eventually be moved or garbage collected. No node
00350         ** re-expression will add a pointer to it.
00351         */
00352         posn = ddHash(f11, f0, yshift);
00353         f->next = ylist[posn];
00354         ylist[posn] = f;
00355         newykeys++;
00356         f = next;
00357     }
00358 
00359     /* Take care of the remaining x nodes that must be re-expressed.
00360     ** They form a linked list pointed by g.
00361     */
00362     f = g;
00363     while (f != NULL) {
00364 #ifdef DD_COUNT
00365         table->swapSteps++;
00366 #endif
00367         next = f->next;
00368         /* Find f1, f0, f11, f10, f01, f00. */
00369         f1 = cuddT(f);
00370         if ((int) f1->index == yindex || (int) f1->index == xindex) {
00371             f11 = cuddT(f1); f10 = cuddE(f1);
00372         } else {
00373             f11 = empty; f10 = f1;
00374         }
00375         f0 = cuddE(f);
00376         if ((int) f0->index == yindex || (int) f0->index == xindex) {
00377             f01 = cuddT(f0); f00 = cuddE(f0);
00378         } else {
00379             f01 = empty; f00 = f0;
00380         }
00381         /* Create the new T child. */
00382         if (f01 == empty) {
00383             newf1 = f10;
00384             cuddSatInc(newf1->ref);
00385         } else {
00386             /* Check ylist for triple (yindex, f01, f10). */
00387             posn = ddHash(f01, f10, yshift);
00388             /* For each element newf1 in collision list ylist[posn]. */
00389             newf1 = ylist[posn];
00390             /* Search the collision chain skipping the marked nodes. */
00391             while (newf1 != NULL) {
00392                 if (cuddT(newf1) == f01 && cuddE(newf1) == f10 &&
00393                     (int) newf1->index == yindex) {
00394                     cuddSatInc(newf1->ref);
00395                     break; /* match */
00396                 }
00397                 newf1 = newf1->next;
00398             } /* while newf1 */
00399             if (newf1 == NULL) {        /* no match */
00400                 newf1 = cuddDynamicAllocNode(table);
00401                 if (newf1 == NULL)
00402                     goto zddSwapOutOfMem;
00403                 newf1->index = yindex; newf1->ref = 1;
00404                 cuddT(newf1) = f01;
00405                 cuddE(newf1) = f10;
00406                 /* Insert newf1 in the collision list ylist[pos];
00407                 ** increase the ref counts of f01 and f10
00408                 */
00409                 newykeys++;
00410                 newf1->next = ylist[posn];
00411                 ylist[posn] = newf1;
00412                 cuddSatInc(f01->ref);
00413                 cuddSatInc(f10->ref);
00414             }
00415         }
00416         cuddT(f) = newf1;
00417 
00418         /* Do the same for f0. */
00419         /* Create the new E child. */
00420         if (f11 == empty) {
00421             newf0 = f00;
00422             cuddSatInc(newf0->ref);
00423         } else {
00424             /* Check ylist for triple (yindex, f11, f00). */
00425             posn = ddHash(f11, f00, yshift);
00426             /* For each element newf0 in collision list ylist[posn]. */
00427             newf0 = ylist[posn];
00428             while (newf0 != NULL) {
00429                 if (cuddT(newf0) == f11 && cuddE(newf0) == f00 &&
00430                     (int) newf0->index == yindex) {
00431                     cuddSatInc(newf0->ref);
00432                     break; /* match */
00433                 }
00434                 newf0 = newf0->next;
00435             } /* while newf0 */
00436             if (newf0 == NULL) {        /* no match */
00437                 newf0 = cuddDynamicAllocNode(table);
00438                 if (newf0 == NULL)
00439                     goto zddSwapOutOfMem;
00440                 newf0->index = yindex; newf0->ref = 1;
00441                 cuddT(newf0) = f11; cuddE(newf0) = f00;
00442                 /* Insert newf0 in the collision list ylist[posn];
00443                 ** increase the ref counts of f11 and f00.
00444                 */
00445                 newykeys++;
00446                 newf0->next = ylist[posn];
00447                 ylist[posn] = newf0;
00448                 cuddSatInc(f11->ref);
00449                 cuddSatInc(f00->ref);
00450             }
00451         }
00452         cuddE(f) = newf0;
00453 
00454         /* Re-insert the modified f in xlist.
00455         ** The modified f does not already exists in xlist.
00456         ** (Because of the uniqueness of the cofactors.)
00457         */
00458         posn = ddHash(newf1, newf0, xshift);
00459         newxkeys++;
00460         f->next = xlist[posn];
00461         xlist[posn] = f;
00462         f = next;
00463     } /* while f != NULL */
00464 
00465     /* GC the y layer and move the marked nodes to the x list. */
00466 
00467     /* For each node f in ylist. */
00468     for (i = 0; i < yslots; i++) {
00469         previous = NULL;
00470         f = ylist[i];
00471         while (f != NULL) {
00472             next = f->next;
00473             if (f->ref == 0) {
00474                 cuddSatDec(cuddT(f)->ref);
00475                 cuddSatDec(cuddE(f)->ref);
00476                 cuddDeallocNode(table, f);
00477                 newykeys--;
00478                 if (previous == NULL)
00479                     ylist[i] = next;
00480                 else
00481                     previous->next = next;
00482             } else if ((int) f->index == xindex) { /* move marked node */
00483                 if (previous == NULL)
00484                     ylist[i] = next;
00485                 else
00486                     previous->next = next;
00487                 f1 = cuddT(f);
00488                 cuddSatDec(f1->ref);
00489                 /* Check ylist for triple (yindex, f1, empty). */
00490                 posn = ddHash(f1, empty, yshift);
00491                 /* For each element newf1 in collision list ylist[posn]. */
00492                 newf1 = ylist[posn];
00493                 while (newf1 != NULL) {
00494                     if (cuddT(newf1) == f1 && cuddE(newf1) == empty &&
00495                         (int) newf1->index == yindex) {
00496                         cuddSatInc(newf1->ref);
00497                         break; /* match */
00498                     }
00499                     newf1 = newf1->next;
00500                 } /* while newf1 */
00501                 if (newf1 == NULL) {    /* no match */
00502                     newf1 = cuddDynamicAllocNode(table);
00503                     if (newf1 == NULL)
00504                         goto zddSwapOutOfMem;
00505                     newf1->index = yindex; newf1->ref = 1;
00506                     cuddT(newf1) = f1; cuddE(newf1) = empty;
00507                     /* Insert newf1 in the collision list ylist[posn];
00508                     ** increase the ref counts of f1 and empty.
00509                     */
00510                     newykeys++;
00511                     newf1->next = ylist[posn];
00512                     ylist[posn] = newf1;
00513                     if (posn == i && previous == NULL)
00514                         previous = newf1;
00515                     cuddSatInc(f1->ref);
00516                     cuddSatInc(empty->ref);
00517                 }
00518                 cuddT(f) = newf1;
00519                 f0 = cuddE(f);
00520                 /* Insert f in x list. */
00521                 posn = ddHash(newf1, f0, xshift);
00522                 newxkeys++;
00523                 newykeys--;
00524                 f->next = xlist[posn];
00525                 xlist[posn] = f;
00526             } else {
00527                 previous = f;
00528             }
00529             f = next;
00530         } /* while f */
00531     } /* for i */
00532 
00533     /* Set the appropriate fields in table. */
00534     table->subtableZ[x].keys     = newxkeys;
00535     table->subtableZ[y].keys     = newykeys;
00536 
00537     table->keysZ += newxkeys + newykeys - oldxkeys - oldykeys;
00538 
00539     /* Update univ section; univ[x] remains the same. */
00540     table->univ[y] = cuddT(table->univ[x]);
00541 
00542 #if 0
00543     (void) fprintf(table->out,"x = %d  y = %d\n", x, y);
00544     (void) Cudd_DebugCheck(table);
00545     (void) Cudd_CheckKeys(table);
00546 #endif
00547 
00548     return (table->keysZ);
00549 
00550 zddSwapOutOfMem:
00551     (void) fprintf(table->err, "Error: cuddZddSwapInPlace out of memory\n");
00552 
00553     return (0);
00554 
00555 } /* end of cuddZddLinearInPlace */

int cuddZddLinearSifting ( DdManager *  table,
int  lower,
int  upper 
)

AutomaticEnd Function********************************************************************

Synopsis [Implementation of the linear sifting algorithm for ZDDs.]

Description [Implementation of the linear sifting algorithm for ZDDs. Assumes that no dead nodes are present.

  1. Order all the variables according to the number of entries in each unique table.
  2. Sift the variable up and down and applies the XOR transformation, remembering each time the total size of the DD heap.
  3. Select the best permutation.
  4. Repeat 3 and 4 for all variables.

Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 152 of file cuddZddLin.c.

00156 {
00157     int i;
00158     int *var;
00159     int size;
00160     int x;
00161     int result;
00162 #ifdef DD_STATS
00163     int previousSize;
00164 #endif
00165 
00166     size = table->sizeZ;
00167     empty = table->zero;
00168 
00169     /* Find order in which to sift variables. */
00170     var = NULL;
00171     zdd_entry = ALLOC(int, size);
00172     if (zdd_entry == NULL) {
00173         table->errorCode = CUDD_MEMORY_OUT;
00174         goto cuddZddSiftingOutOfMem;
00175     }
00176     var = ALLOC(int, size);
00177     if (var == NULL) {
00178         table->errorCode = CUDD_MEMORY_OUT;
00179         goto cuddZddSiftingOutOfMem;
00180     }
00181 
00182     for (i = 0; i < size; i++) {
00183         x = table->permZ[i];
00184         zdd_entry[i] = table->subtableZ[x].keys;
00185         var[i] = i;
00186     }
00187 
00188     qsort((void *)var, size, sizeof(int), (DD_QSFP)cuddZddUniqueCompare);
00189 
00190     /* Now sift. */
00191     for (i = 0; i < ddMin(table->siftMaxVar, size); i++) {
00192         if (zddTotalNumberSwapping >= table->siftMaxSwap)
00193             break;
00194         x = table->permZ[var[i]];
00195         if (x < lower || x > upper) continue;
00196 #ifdef DD_STATS
00197         previousSize = table->keysZ;
00198 #endif
00199         result = cuddZddLinearAux(table, x, lower, upper);
00200         if (!result)
00201             goto cuddZddSiftingOutOfMem;
00202 #ifdef DD_STATS
00203         if (table->keysZ < (unsigned) previousSize) {
00204             (void) fprintf(table->out,"-");
00205         } else if (table->keysZ > (unsigned) previousSize) {
00206             (void) fprintf(table->out,"+");     /* should never happen */
00207             (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ , var[i]);
00208         } else {
00209             (void) fprintf(table->out,"=");
00210         }
00211         fflush(table->out);
00212 #endif
00213     }
00214 
00215     FREE(var);
00216     FREE(zdd_entry);
00217 
00218     return(1);
00219 
00220 cuddZddSiftingOutOfMem:
00221 
00222     if (zdd_entry != NULL) FREE(zdd_entry);
00223     if (var != NULL) FREE(var);
00224 
00225     return(0);
00226 
00227 } /* end of cuddZddLinearSifting */

static Move * cuddZddLinearUp ( DdManager *  table,
int  y,
int  xLow,
Move *  prevMoves 
) [static]

Function********************************************************************

Synopsis [Sifts a variable up applying the XOR transformation.]

Description [Sifts a variable up applying the XOR transformation. Moves y up until either it reaches the bound (xLow) or the size of the ZDD heap increases too much. Returns the set of moves in case of success; NULL if memory is full.]

SideEffects [None]

SeeAlso []

Definition at line 700 of file cuddZddLin.c.

00705 {
00706     Move        *moves;
00707     Move        *move;
00708     int         x;
00709     int         size, newsize;
00710     int         limitSize;
00711 
00712     moves = prevMoves;
00713     limitSize = table->keysZ;
00714 
00715     x = cuddZddNextLow(table, y);
00716     while (x >= xLow) {
00717         size = cuddZddSwapInPlace(table, x, y);
00718         if (size == 0)
00719             goto cuddZddLinearUpOutOfMem;
00720         newsize = cuddZddLinearInPlace(table, x, y);
00721         if (newsize == 0)
00722             goto cuddZddLinearUpOutOfMem;
00723         move = (Move *) cuddDynamicAllocNode(table);
00724         if (move == NULL)
00725             goto cuddZddLinearUpOutOfMem;
00726         move->x = x;
00727         move->y = y;
00728         move->next = moves;
00729         moves = move;
00730         move->flags = CUDD_SWAP_MOVE;
00731         if (newsize > size) {
00732             /* Undo transformation. The transformation we apply is
00733             ** its own inverse. Hence, we just apply the transformation
00734             ** again.
00735             */
00736             newsize = cuddZddLinearInPlace(table,x,y);
00737             if (newsize == 0) goto cuddZddLinearUpOutOfMem;
00738 #ifdef DD_DEBUG
00739             if (newsize != size) {
00740                 (void) fprintf(table->err,"Change in size after identity transformation! From %d to %d\n",size,newsize);
00741             }
00742 #endif
00743         } else {
00744             size = newsize;
00745             move->flags = CUDD_LINEAR_TRANSFORM_MOVE;
00746         }
00747         move->size = size;
00748 
00749         if ((double)size > (double)limitSize * table->maxGrowth)
00750             break;
00751         if (size < limitSize)
00752             limitSize = size;
00753 
00754         y = x;
00755         x = cuddZddNextLow(table, y);
00756     }
00757     return(moves);
00758 
00759 cuddZddLinearUpOutOfMem:
00760     while (moves != NULL) {
00761         move = moves->next;
00762         cuddDeallocMove(table, moves);
00763         moves = move;
00764     }
00765     return((Move *) CUDD_OUT_OF_MEM);
00766 
00767 } /* end of cuddZddLinearUp */

static Move * cuddZddUndoMoves ( DdManager *  table,
Move *  moves 
) [static]

Function********************************************************************

Synopsis [Given a set of moves, returns the ZDD heap to the order in effect before the moves.]

Description [Given a set of moves, returns the ZDD heap to the order in effect before the moves. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

Definition at line 917 of file cuddZddLin.c.

00920 {
00921     Move *invmoves = NULL;
00922     Move *move;
00923     Move *invmove;
00924     int size;
00925 
00926     for (move = moves; move != NULL; move = move->next) {
00927         invmove = (Move *) cuddDynamicAllocNode(table);
00928         if (invmove == NULL) goto cuddZddUndoMovesOutOfMem;
00929         invmove->x = move->x;
00930         invmove->y = move->y;
00931         invmove->next = invmoves;
00932         invmoves = invmove;
00933         if (move->flags == CUDD_SWAP_MOVE) {
00934             invmove->flags = CUDD_SWAP_MOVE;
00935             size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
00936             if (!size) goto cuddZddUndoMovesOutOfMem;
00937         } else if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) {
00938             invmove->flags = CUDD_INVERSE_TRANSFORM_MOVE;
00939             size = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
00940             if (!size) goto cuddZddUndoMovesOutOfMem;
00941             size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
00942             if (!size) goto cuddZddUndoMovesOutOfMem;
00943         } else { /* must be CUDD_INVERSE_TRANSFORM_MOVE */
00944 #ifdef DD_DEBUG
00945             (void) fprintf(table->err,"Unforseen event in ddUndoMoves!\n");
00946 #endif
00947             invmove->flags = CUDD_LINEAR_TRANSFORM_MOVE;
00948             size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
00949             if (!size) goto cuddZddUndoMovesOutOfMem;
00950             size = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
00951             if (!size) goto cuddZddUndoMovesOutOfMem;
00952         }
00953         invmove->size = size;
00954     }
00955 
00956     return(invmoves);
00957 
00958 cuddZddUndoMovesOutOfMem:
00959     while (invmoves != NULL) {
00960         move = invmoves->next;
00961         cuddDeallocMove(table, invmoves);
00962         invmoves = move;
00963     }
00964     return((Move *) CUDD_OUT_OF_MEM);
00965 
00966 } /* end of cuddZddUndoMoves */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddZddLin.c,v 1.14 2004/08/13 18:04:53 fabio Exp $" [static]

Definition at line 88 of file cuddZddLin.c.

DdNode* empty [static]

Definition at line 94 of file cuddZddLin.c.

int* zdd_entry

Definition at line 104 of file cuddZddReord.c.

int zddTotalNumberLinearTr [static]

Definition at line 93 of file cuddZddLin.c.

int zddTotalNumberSwapping

Definition at line 106 of file cuddZddReord.c.

Generated on Tue Jan 12 13:57:22 2010 for glu-2.2 by  doxygen 1.6.1