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

  Synopsis    [Creates a new DD manager.]

  Description [Creates a new DD manager, initializes the table, the
  basic constants and the projection functions. If maxMemory is 0,
  Cudd_Init decides suitable values for the maximum size of the cache
  and for the limit for fast unique table growth based on the available
  memory. Returns a pointer to the manager if successful; NULL
  otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_Quit]

******************************************************************************/
Function
Synopsis    [Creates a new DD manager.]

Description [Creates a new DD manager, initializes the table, the
basic constants and the projection functions. If maxMemory is 0,
Cudd_Init decides suitable values for the maximum size of the cache
and for the limit for fast unique table growth based on the available
memory. Returns a pointer to the manager if successful; NULL
otherwise.]




Function Synopsis [ Creates a new DD manager . ] Description [ Creates a new DD manager initializes the table the basic constants and the projection functions . If maxMemory is 0 Cudd_Init decides suitable values for the maximum size of the cache and for the limit for fast unique table growth based on the available memory . Returns a pointer to the manager if successful ; NULL otherwise . ]
DdManager *
Cudd_Init(
  unsigned int numVars ,
  unsigned int numVarsZ ,
  unsigned int numSlots ,
  unsigned int cacheSize ,
  unsigned long maxMemory )
{
    DdManager *unique;
    int i,result;
    DdNode *one, *zero;
    unsigned int maxCacheSize;
    unsigned int looseUpTo;
    extern DD_OOMFP MMoutOfMemory;
    DD_OOMFP saveHandler;
    if (maxMemory == 0) {
        maxMemory = getSoftDataLimit();
    }
    looseUpTo = (unsigned int) ((maxMemory / sizeof(DdNode)) /
                                DD_MAX_LOOSE_FRACTION);
    unique = cuddInitTable(numVars,numVarsZ,numSlots,looseUpTo);
    if (unique == NULL) return(NULL);
    unique->maxmem = (unsigned long) maxMemory / 10 * 9;
    maxCacheSize = (unsigned int) ((maxMemory / sizeof(DdCache)) /
                                   DD_MAX_CACHE_FRACTION);
    result = cuddInitCache(unique,cacheSize,maxCacheSize);
    if (result == 0) return(NULL);
    saveHandler = MMoutOfMemory;
    MMoutOfMemory = Cudd_OutOfMem;
    unique->stash = ABC_ALLOC(char,(maxMemory / DD_STASH_FRACTION) + 4);
    MMoutOfMemory = saveHandler;
    if (unique->stash == NULL) {
        (void) fprintf(unique->err,"Unable to set aside memory\n");
    }
    unique->one = cuddUniqueConst(unique,1.0);
    if (unique->one == NULL) return(0);
    cuddRef(unique->one);
    unique->zero = cuddUniqueConst(unique,0.0);
    if (unique->zero == NULL) return(0);
    cuddRef(unique->zero);
#ifdef HAVE_IEEE_754
    if (DD_PLUS_INF_VAL != DD_PLUS_INF_VAL * 3 ||
        DD_PLUS_INF_VAL != DD_PLUS_INF_VAL / 3) {
        (void) fprintf(unique->err,"Warning: Crippled infinite values\n");
        (void) fprintf(unique->err,"Recompile without -DHAVE_IEEE_754\n");
    }
#endif
    unique->plusinfinity = cuddUniqueConst(unique,DD_PLUS_INF_VAL);
    if (unique->plusinfinity == NULL) return(0);
    cuddRef(unique->plusinfinity);
    unique->minusinfinity = cuddUniqueConst(unique,DD_MINUS_INF_VAL);
    if (unique->minusinfinity == NULL) return(0);
    cuddRef(unique->minusinfinity);
    unique->background = unique->zero;
    one = unique->one;
    zero = Cudd_Not(one);
    unique->vars = ABC_ALLOC(DdNodePtr,unique->maxSize);
    if (unique->vars == NULL) {
        unique->errorCode = CUDD_MEMORY_OUT;
        return(NULL);
    }
    for (i = 0; i < unique->size; i++) {
        unique->vars[i] = cuddUniqueInter(unique,i,one,zero);
        if (unique->vars[i] == NULL) return(0);
        cuddRef(unique->vars[i]);
    }
    if (unique->sizeZ)
        cuddZddInitUniv(unique);
    unique->memused += sizeof(DdNode *) * unique->maxSize;
    unique->bFunc = NULL;
    unique->bFunc2 = NULL;
    unique->TimeStop = 0;
    return(unique);
}
DdManager * Cudd_Init ( unsigned int numVars , unsigned int numVarsZ , unsigned int numSlots , unsigned int cacheSize , unsigned long maxMemory ) { DdManager * unique ; int i , result ; DdNode * one , * zero ; unsigned int maxCacheSize ; unsigned int looseUpTo ; extern DD_OOMFP MMoutOfMemory ; DD_OOMFP saveHandler ; if ( maxMemory == 0 ) { maxMemory = getSoftDataLimit ( ) ; } looseUpTo = ( unsigned int ) ( ( maxMemory / sizeof ( DdNode ) ) / DD_MAX_LOOSE_FRACTION ) ; unique = cuddInitTable ( numVars , numVarsZ , numSlots , looseUpTo ) ; if ( unique == NULL ) return ( NULL ) ; unique -> maxmem = ( unsigned long ) maxMemory / 10 * 9 ; maxCacheSize = ( unsigned int ) ( ( maxMemory / sizeof ( DdCache ) ) / DD_MAX_CACHE_FRACTION ) ; result = cuddInitCache ( unique , cacheSize , maxCacheSize ) ; if ( result == 0 ) return ( NULL ) ; saveHandler = MMoutOfMemory ; MMoutOfMemory = Cudd_OutOfMem ; unique -> stash = ABC_ALLOC ( char , ( maxMemory / DD_STASH_FRACTION ) + 4 ) ; MMoutOfMemory = saveHandler ; if ( unique -> stash == NULL ) { ( void ) fprintf ( unique -> err , " \n " ) ; } unique -> one = cuddUniqueConst ( unique , 1.0 ) ; if ( unique -> one == NULL ) return ( 0 ) ; cuddRef ( unique -> one ) ; unique -> zero = cuddUniqueConst ( unique , 0.0 ) ; if ( unique -> zero == NULL ) return ( 0 ) ; cuddRef ( unique -> zero ) ; #ifdef HAVE_IEEE_754 if ( DD_PLUS_INF_VAL != DD_PLUS_INF_VAL * 3 || DD_PLUS_INF_VAL != DD_PLUS_INF_VAL / 3 ) { ( void ) fprintf ( unique -> err , " \n " ) ; ( void ) fprintf ( unique -> err , " \n " ) ; } #endif unique -> plusinfinity = cuddUniqueConst ( unique , DD_PLUS_INF_VAL ) ; if ( unique -> plusinfinity == NULL ) return ( 0 ) ; cuddRef ( unique -> plusinfinity ) ; unique -> minusinfinity = cuddUniqueConst ( unique , DD_MINUS_INF_VAL ) ; if ( unique -> minusinfinity == NULL ) return ( 0 ) ; cuddRef ( unique -> minusinfinity ) ; unique -> background = unique -> zero ; one = unique -> one ; zero = Cudd_Not ( one ) ; unique -> vars = ABC_ALLOC ( DdNodePtr , unique -> maxSize ) ; if ( unique -> vars == NULL ) { unique -> errorCode = CUDD_MEMORY_OUT ; return ( NULL ) ; } for ( i = 0 ; i < unique -> size ; i ++ ) { unique -> vars [ i ] = cuddUniqueInter ( unique , i , one , zero ) ; if ( unique -> vars [ i ] == NULL ) return ( 0 ) ; cuddRef ( unique -> vars [ i ] ) ; } if ( unique -> sizeZ ) cuddZddInitUniv ( unique ) ; unique -> memused += sizeof ( DdNode * ) * unique -> maxSize ; unique -> bFunc = NULL ; unique -> bFunc2 = NULL ; unique -> TimeStop = 0 ; return ( unique ) ; }
Function
Synopsis    [Creates a new DD manager.]
Function Synopsis [ Creates a new DD manager . ]
/* initial number of BDD variables (i.e., subtables) */ /* initial number of ZDD variables (i.e., subtables) */ /* initial size of the unique tables */ /* initial size of the cache */ /* target maximum memory occupation */ /* Initialize constants. */ /* The logical zero is different from the CUDD_VALUE_TYPE zero! */ /* Create the projection functions. */