abc/src/bdd/cudd/cuddTable.c
/**Function********************************************************************

  Synopsis [Increases the number of ZDD subtables in a unique table so
  that it meets or exceeds index.]

  Description [Increases the number of ZDD subtables in a unique table so
  that it meets or exceeds index.  When new ZDD variables are created, it
  is possible to preserve the functions unchanged, or it is possible to
  preserve the covers unchanged, but not both. cuddResizeTableZdd preserves
  the covers.  Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     [ddResizeTable]

******************************************************************************/
Function
Synopsis [Increases the number of ZDD subtables in a unique table so
that it meets or exceeds index.]

Description [Increases the number of ZDD subtables in a unique table so
that it meets or exceeds index.  When new ZDD variables are created, it
is possible to preserve the functions unchanged, or it is possible to
preserve the covers unchanged, but not both. cuddResizeTableZdd preserves
the covers.  Returns 1 if successful; 0 otherwise.]




Function Synopsis [ Increases the number of ZDD subtables in a unique table so that it meets or exceeds index . ] Description [ Increases the number of ZDD subtables in a unique table so that it meets or exceeds index . When new ZDD variables are created it is possible to preserve the functions unchanged or it is possible to preserve the covers unchanged but not both . cuddResizeTableZdd preserves the covers . Returns 1 if successful ; 0 otherwise . ]
int
cuddResizeTableZdd(
  DdManager * unique,
  int  index)
{
    DdSubtable *newsubtables;
    DdNodePtr *newnodelist;
    int oldsize,newsize;
    int i,j,reorderSave;
    unsigned int numSlots = unique->initSlots;
    int *newperm, *newinvperm;
    oldsize = unique->sizeZ;
    if (index < unique->maxSizeZ) {
        for (i = oldsize; i <= index; i++) {
            unique->subtableZ[i].slots = numSlots;
            unique->subtableZ[i].shift = sizeof(int) * 8 -
                cuddComputeFloorLog2(numSlots);
            unique->subtableZ[i].keys = 0;
            unique->subtableZ[i].maxKeys = numSlots * DD_MAX_SUBTABLE_DENSITY;
            unique->subtableZ[i].dead = 0;
            unique->permZ[i] = i;
            unique->invpermZ[i] = i;
            newnodelist = unique->subtableZ[i].nodelist =
                ABC_ALLOC(DdNodePtr, numSlots);
            if (newnodelist == NULL) {
                unique->errorCode = CUDD_MEMORY_OUT;
                return(0);
            }
            for (j = 0; (unsigned) j < numSlots; j++) {
                newnodelist[j] = NULL;
            }
        }
    } else {
        newsize = index + DD_DEFAULT_RESIZE;
#ifdef DD_VERBOSE
        (void) fprintf(unique->err,
                       "Increasing the ZDD table size from %d to %d\n",
            unique->maxSizeZ, newsize);
#endif
        newsubtables = ABC_ALLOC(DdSubtable,newsize);
        if (newsubtables == NULL) {
            unique->errorCode = CUDD_MEMORY_OUT;
            return(0);
        }
        newperm = ABC_ALLOC(int,newsize);
        if (newperm == NULL) {
            unique->errorCode = CUDD_MEMORY_OUT;
            return(0);
        }
        newinvperm = ABC_ALLOC(int,newsize);
        if (newinvperm == NULL) {
            unique->errorCode = CUDD_MEMORY_OUT;
            return(0);
        }
        unique->memused += (newsize - unique->maxSizeZ) * ((numSlots+1) *
            sizeof(DdNode *) + 2 * sizeof(int) + sizeof(DdSubtable));
        if (newsize > unique->maxSize) {
            ABC_FREE(unique->stack);
            unique->stack = ABC_ALLOC(DdNodePtr,newsize + 1);
            if (unique->stack == NULL) {
                unique->errorCode = CUDD_MEMORY_OUT;
                return(0);
            }
            unique->stack[0] = NULL; 
            unique->memused +=
                (newsize - ddMax(unique->maxSize,unique->maxSizeZ))
                * sizeof(DdNode *);
        }
        for (i = 0; i < oldsize; i++) {
            newsubtables[i].slots = unique->subtableZ[i].slots;
            newsubtables[i].shift = unique->subtableZ[i].shift;
            newsubtables[i].keys = unique->subtableZ[i].keys;
            newsubtables[i].maxKeys = unique->subtableZ[i].maxKeys;
            newsubtables[i].dead = unique->subtableZ[i].dead;
            newsubtables[i].nodelist = unique->subtableZ[i].nodelist;
            newperm[i] = unique->permZ[i];
            newinvperm[i] = unique->invpermZ[i];
        }
        for (i = oldsize; i <= index; i++) {
            newsubtables[i].slots = numSlots;
            newsubtables[i].shift = sizeof(int) * 8 -
                cuddComputeFloorLog2(numSlots);
            newsubtables[i].keys = 0;
            newsubtables[i].maxKeys = numSlots * DD_MAX_SUBTABLE_DENSITY;
            newsubtables[i].dead = 0;
            newperm[i] = i;
            newinvperm[i] = i;
            newnodelist = newsubtables[i].nodelist = ABC_ALLOC(DdNodePtr, numSlots);
            if (newnodelist == NULL) {
                unique->errorCode = CUDD_MEMORY_OUT;
                return(0);
            }
            for (j = 0; (unsigned) j < numSlots; j++) {
                newnodelist[j] = NULL;
            }
        }
        ABC_FREE(unique->subtableZ);
        unique->subtableZ = newsubtables;
        unique->maxSizeZ = newsize;
        ABC_FREE(unique->permZ);
        unique->permZ = newperm;
        ABC_FREE(unique->invpermZ);
        unique->invpermZ = newinvperm;
    }
    unique->slots += (index + 1 - unique->sizeZ) * numSlots;
    ddFixLimits(unique);
    unique->sizeZ = index + 1;
    reorderSave = unique->autoDynZ;
    unique->autoDynZ = 0;
    cuddZddFreeUniv(unique);
    if (!cuddZddInitUniv(unique)) {
        unique->autoDynZ = reorderSave;
        return(0);
    }
    unique->autoDynZ = reorderSave;
    return(1);
}
int cuddResizeTableZdd ( DdManager * unique , int index ) { DdSubtable * newsubtables ; DdNodePtr * newnodelist ; int oldsize , newsize ; int i , j , reorderSave ; unsigned int numSlots = unique -> initSlots ; int * newperm , * newinvperm ; oldsize = unique -> sizeZ ; if ( index < unique -> maxSizeZ ) { for ( i = oldsize ; i <= index ; i ++ ) { unique -> subtableZ [ i ] . slots = numSlots ; unique -> subtableZ [ i ] . shift = sizeof ( int ) * 8 - cuddComputeFloorLog2 ( numSlots ) ; unique -> subtableZ [ i ] . keys = 0 ; unique -> subtableZ [ i ] . maxKeys = numSlots * DD_MAX_SUBTABLE_DENSITY ; unique -> subtableZ [ i ] . dead = 0 ; unique -> permZ [ i ] = i ; unique -> invpermZ [ i ] = i ; newnodelist = unique -> subtableZ [ i ] . nodelist = ABC_ALLOC ( DdNodePtr , numSlots ) ; if ( newnodelist == NULL ) { unique -> errorCode = CUDD_MEMORY_OUT ; return ( 0 ) ; } for ( j = 0 ; ( unsigned ) j < numSlots ; j ++ ) { newnodelist [ j ] = NULL ; } } } else { newsize = index + DD_DEFAULT_RESIZE ; #ifdef DD_VERBOSE ( void ) fprintf ( unique -> err , " \n " , unique -> maxSizeZ , newsize ) ; #endif newsubtables = ABC_ALLOC ( DdSubtable , newsize ) ; if ( newsubtables == NULL ) { unique -> errorCode = CUDD_MEMORY_OUT ; return ( 0 ) ; } newperm = ABC_ALLOC ( int , newsize ) ; if ( newperm == NULL ) { unique -> errorCode = CUDD_MEMORY_OUT ; return ( 0 ) ; } newinvperm = ABC_ALLOC ( int , newsize ) ; if ( newinvperm == NULL ) { unique -> errorCode = CUDD_MEMORY_OUT ; return ( 0 ) ; } unique -> memused += ( newsize - unique -> maxSizeZ ) * ( ( numSlots + 1 ) * sizeof ( DdNode * ) + 2 * sizeof ( int ) + sizeof ( DdSubtable ) ) ; if ( newsize > unique -> maxSize ) { ABC_FREE ( unique -> stack ) ; unique -> stack = ABC_ALLOC ( DdNodePtr , newsize + 1 ) ; if ( unique -> stack == NULL ) { unique -> errorCode = CUDD_MEMORY_OUT ; return ( 0 ) ; } unique -> stack [ 0 ] = NULL ; unique -> memused += ( newsize - ddMax ( unique -> maxSize , unique -> maxSizeZ ) ) * sizeof ( DdNode * ) ; } for ( i = 0 ; i < oldsize ; i ++ ) { newsubtables [ i ] . slots = unique -> subtableZ [ i ] . slots ; newsubtables [ i ] . shift = unique -> subtableZ [ i ] . shift ; newsubtables [ i ] . keys = unique -> subtableZ [ i ] . keys ; newsubtables [ i ] . maxKeys = unique -> subtableZ [ i ] . maxKeys ; newsubtables [ i ] . dead = unique -> subtableZ [ i ] . dead ; newsubtables [ i ] . nodelist = unique -> subtableZ [ i ] . nodelist ; newperm [ i ] = unique -> permZ [ i ] ; newinvperm [ i ] = unique -> invpermZ [ i ] ; } for ( i = oldsize ; i <= index ; i ++ ) { newsubtables [ i ] . slots = numSlots ; newsubtables [ i ] . shift = sizeof ( int ) * 8 - cuddComputeFloorLog2 ( numSlots ) ; newsubtables [ i ] . keys = 0 ; newsubtables [ i ] . maxKeys = numSlots * DD_MAX_SUBTABLE_DENSITY ; newsubtables [ i ] . dead = 0 ; newperm [ i ] = i ; newinvperm [ i ] = i ; newnodelist = newsubtables [ i ] . nodelist = ABC_ALLOC ( DdNodePtr , numSlots ) ; if ( newnodelist == NULL ) { unique -> errorCode = CUDD_MEMORY_OUT ; return ( 0 ) ; } for ( j = 0 ; ( unsigned ) j < numSlots ; j ++ ) { newnodelist [ j ] = NULL ; } } ABC_FREE ( unique -> subtableZ ) ; unique -> subtableZ = newsubtables ; unique -> maxSizeZ = newsize ; ABC_FREE ( unique -> permZ ) ; unique -> permZ = newperm ; ABC_FREE ( unique -> invpermZ ) ; unique -> invpermZ = newinvperm ; } unique -> slots += ( index + 1 - unique -> sizeZ ) * numSlots ; ddFixLimits ( unique ) ; unique -> sizeZ = index + 1 ; reorderSave = unique -> autoDynZ ; unique -> autoDynZ = 0 ; cuddZddFreeUniv ( unique ) ; if ( ! cuddZddInitUniv ( unique ) ) { unique -> autoDynZ = reorderSave ; return ( 0 ) ; } unique -> autoDynZ = reorderSave ; return ( 1 ) ; }
Function
Synopsis [Increases the number of ZDD subtables in a unique table so
that it meets or exceeds index.]
Function Synopsis [ Increases the number of ZDD subtables in a unique table so that it meets or exceeds index . ]
/* Easy case: there is still room in the current table. */ /* The current table is too small: we need to allocate a new,
        ** larger one; move all old subtables, and initialize the new
        ** subtables up to index included.
        */ /* to suppress harmless UMR */ /* Now that the table is in a coherent state, update the ZDD
    ** universe. We need to temporarily disable reordering,
    ** because we cannot reorder without universe in place.
    */