cuddInit.c

Go to the documentation of this file.

#include "CUDD/util.h"
#include "CUDD/cuddInt.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddInit.c,v 1.34 2012/02/05 01:07:19 fabio Exp $";
#endif

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

DdManager *
Cudd_Init(
  unsigned int numVars /* initial number of BDD variables (i.e., subtables) */,
  unsigned int numVarsZ /* initial number of ZDD variables (i.e., subtables) */,
  unsigned int numSlots /* initial size of the unique tables */,
  unsigned int cacheSize /* initial size of the cache */,
  unsigned long maxMemory /* target maximum memory occupation */)
{
    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 = ALLOC(char,(maxMemory / DD_STASH_FRACTION) + 4);
    MMoutOfMemory = saveHandler;
    if (unique->stash == NULL) {
    (void) fprintf(unique->err,"Unable to set aside memory\n");
    }

    /* Initialize constants. */
    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;

    /* The logical zero is different from the CUDD_VALUE_TYPE zero! */
    one = unique->one;
    zero = Cudd_Not(one);
    /* Create the projection functions. */
    unique->vars = 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;

    return(unique);

} /* end of Cudd_Init */


void
Cudd_Quit(
  DdManager * unique)
{
    if (unique->stash != NULL) FREE(unique->stash);
    cuddFreeTable(unique);

} /* end of Cudd_Quit */


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


int
cuddZddInitUniv(
  DdManager * zdd)
{
    DdNode  *p, *res;
    int     i;

    zdd->univ = ALLOC(DdNodePtr, zdd->sizeZ);
    if (zdd->univ == NULL) {
    zdd->errorCode = CUDD_MEMORY_OUT;
    return(0);
    }

    res = DD_ONE(zdd);
    cuddRef(res);
    for (i = zdd->sizeZ - 1; i >= 0; i--) {
    unsigned int index = zdd->invpermZ[i];
    p = res;
    res = cuddUniqueInterZdd(zdd, index, p, p);
    if (res == NULL) {
        Cudd_RecursiveDerefZdd(zdd,p);
        FREE(zdd->univ);
        return(0);
    }
    cuddRef(res);
    cuddDeref(p);
    zdd->univ[i] = res;
    }

#ifdef DD_VERBOSE
    cuddZddP(zdd, zdd->univ[0]);
#endif

    return(1);

} /* end of cuddZddInitUniv */


void
cuddZddFreeUniv(
  DdManager * zdd)
{
    if (zdd->univ) {
    Cudd_RecursiveDerefZdd(zdd, zdd->univ[0]);
    FREE(zdd->univ);
    }

} /* end of cuddZddFreeUniv */


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/