cuddAPI.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: cuddAPI.c,v 1.64 2012/02/05 01:07:18 fabio Exp $";
#endif

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

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

static void fixVarTree (MtrNode *treenode, int *perm, int size);
static int addMultiplicityGroups (DdManager *dd, MtrNode *treenode, int multiplicity, char *vmask, char *lmask);

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


DdNode *
Cudd_addNewVar(
  DdManager * dd)
{
    DdNode *res;

    if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL);
    do {
    dd->reordered = 0;
    res = cuddUniqueInter(dd,dd->size,DD_ONE(dd),DD_ZERO(dd));
    } while (dd->reordered == 1);

    return(res);

} /* end of Cudd_addNewVar */


DdNode *
Cudd_addNewVarAtLevel(
  DdManager * dd,
  int  level)
{
    DdNode *res;

    if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL);
    if (level >= dd->size) return(Cudd_addIthVar(dd,level));
    if (!cuddInsertSubtables(dd,1,level)) return(NULL);
    do {
    dd->reordered = 0;
    res = cuddUniqueInter(dd,dd->size - 1,DD_ONE(dd),DD_ZERO(dd));
    } while (dd->reordered == 1);

    return(res);

} /* end of Cudd_addNewVarAtLevel */


DdNode *
Cudd_bddNewVar(
  DdManager * dd)
{
    DdNode *res;

    if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL);
    res = cuddUniqueInter(dd,dd->size,dd->one,Cudd_Not(dd->one));

    return(res);

} /* end of Cudd_bddNewVar */


DdNode *
Cudd_bddNewVarAtLevel(
  DdManager * dd,
  int  level)
{
    DdNode *res;

    if ((unsigned int) dd->size >= CUDD_MAXINDEX - 1) return(NULL);
    if (level >= dd->size) return(Cudd_bddIthVar(dd,level));
    if (!cuddInsertSubtables(dd,1,level)) return(NULL);
    res = dd->vars[dd->size - 1];

    return(res);

} /* end of Cudd_bddNewVarAtLevel */


DdNode *
Cudd_addIthVar(
  DdManager * dd,
  int  i)
{
    DdNode *res;

    if ((unsigned int) i >= CUDD_MAXINDEX - 1) return(NULL);
    do {
    dd->reordered = 0;
    res = cuddUniqueInter(dd,i,DD_ONE(dd),DD_ZERO(dd));
    } while (dd->reordered == 1);

    return(res);

} /* end of Cudd_addIthVar */


DdNode *
Cudd_bddIthVar(
  DdManager * dd,
  int  i)
{
    DdNode *res;

    if ((unsigned int) i >= CUDD_MAXINDEX - 1) return(NULL);
    if (i < dd->size) {
    res = dd->vars[i];
    } else {
    res = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one));
    }

    return(res);

} /* end of Cudd_bddIthVar */


DdNode *
Cudd_zddIthVar(
  DdManager * dd,
  int  i)
{
    DdNode *res;
    DdNode *zvar;
    DdNode *lower;
    int j;

    if ((unsigned int) i >= CUDD_MAXINDEX - 1) return(NULL);

    /* The i-th variable function has the following structure:
    ** at the level corresponding to index i there is a node whose "then"
    ** child points to the universe, and whose "else" child points to zero.
    ** Above that level there are nodes with identical children.
    */

    /* First we build the node at the level of index i. */
    lower = (i < dd->sizeZ - 1) ? dd->univ[dd->permZ[i]+1] : DD_ONE(dd);
    do {
    dd->reordered = 0;
    zvar = cuddUniqueInterZdd(dd, i, lower, DD_ZERO(dd));
    } while (dd->reordered == 1);

    if (zvar == NULL)
    return(NULL);
    cuddRef(zvar);

    /* Now we add the "filler" nodes above the level of index i. */
    for (j = dd->permZ[i] - 1; j >= 0; j--) {
    do {
        dd->reordered = 0;
        res = cuddUniqueInterZdd(dd, dd->invpermZ[j], zvar, zvar);
    } while (dd->reordered == 1);
    if (res == NULL) {
        Cudd_RecursiveDerefZdd(dd,zvar);
        return(NULL);
    }
    cuddRef(res);
    Cudd_RecursiveDerefZdd(dd,zvar);
    zvar = res;
    }
    cuddDeref(zvar);
    return(zvar);

} /* end of Cudd_zddIthVar */


int
Cudd_zddVarsFromBddVars(
  DdManager * dd /* DD manager */,
  int multiplicity /* how many ZDD variables are created for each BDD variable */)
{
    int res;
    int i, j;
    int allnew;
    int *permutation;

    if (multiplicity < 1) return(0);
    allnew = dd->sizeZ == 0;
    if (dd->size * multiplicity > dd->sizeZ) {
    res = cuddResizeTableZdd(dd,dd->size * multiplicity - 1);
    if (res == 0) return(0);
    }
    /* Impose the order of the BDD variables to the ZDD variables. */
    if (allnew) {
    for (i = 0; i < dd->size; i++) {
        for (j = 0; j < multiplicity; j++) {
        dd->permZ[i * multiplicity + j] =
            dd->perm[i] * multiplicity + j;
        dd->invpermZ[dd->permZ[i * multiplicity + j]] =
            i * multiplicity + j;
        }
    }
    for (i = 0; i < dd->sizeZ; i++) {
        dd->univ[i]->index = dd->invpermZ[i];
    }
    } else {
    permutation = ALLOC(int,dd->sizeZ);
    if (permutation == NULL) {
        dd->errorCode = CUDD_MEMORY_OUT;
        return(0);
    }
    for (i = 0; i < dd->size; i++) {
        for (j = 0; j < multiplicity; j++) {
        permutation[i * multiplicity + j] =
            dd->invperm[i] * multiplicity + j;
        }
    }
    for (i = dd->size * multiplicity; i < dd->sizeZ; i++) {
        permutation[i] = i;
    }
    res = Cudd_zddShuffleHeap(dd, permutation);
    FREE(permutation);
    if (res == 0) return(0);
    }
    /* Copy and expand the variable group tree if it exists. */
    if (dd->treeZ != NULL) {
    Cudd_FreeZddTree(dd);
    }
    if (dd->tree != NULL) {
    dd->treeZ = Mtr_CopyTree(dd->tree, multiplicity);
    if (dd->treeZ == NULL) return(0);
    } else if (multiplicity > 1) {
    dd->treeZ = Mtr_InitGroupTree(0, dd->sizeZ);
    if (dd->treeZ == NULL) return(0);
    dd->treeZ->index = dd->invpermZ[0];
    }
    /* Create groups for the ZDD variables derived from the same BDD variable.
    */
    if (multiplicity > 1) {
    char *vmask, *lmask;

    vmask = ALLOC(char, dd->size);
    if (vmask == NULL) {
        dd->errorCode = CUDD_MEMORY_OUT;
        return(0);
    }
    lmask =  ALLOC(char, dd->size);
    if (lmask == NULL) {
        dd->errorCode = CUDD_MEMORY_OUT;
        return(0);
    }
    for (i = 0; i < dd->size; i++) {
        vmask[i] = lmask[i] = 0;
    }
    res = addMultiplicityGroups(dd,dd->treeZ,multiplicity,vmask,lmask);
    FREE(vmask);
    FREE(lmask);
    if (res == 0) return(0);
    }
    return(1);

} /* end of Cudd_zddVarsFromBddVars */


DdNode *
Cudd_addConst(
  DdManager * dd,
  CUDD_VALUE_TYPE  c)
{
    return(cuddUniqueConst(dd,c));

} /* end of Cudd_addConst */


int
Cudd_IsNonConstant(
  DdNode *f)
{
    return(f == DD_NON_CONSTANT || !Cudd_IsConstant(f));

} /* end of Cudd_IsNonConstant */


unsigned long
Cudd_ReadStartTime(
  DdManager * unique)
{
    return unique->startTime;

} /* end of Cudd_ReadStartTime */


unsigned long
Cudd_ReadElapsedTime(
  DdManager * unique)
{
  return util_cpu_time() - unique->startTime;

} /* end of Cudd_ReadElapsedTime */


void
Cudd_SetStartTime(
  DdManager * unique,
  unsigned long st)
{
    unique->startTime = st;

} /* end of Cudd_SetStartTime */


void
Cudd_ResetStartTime(
  DdManager * unique)
{
    unique->startTime = util_cpu_time();

} /* end of Cudd_ResetStartTime */


unsigned long
Cudd_ReadTimeLimit(
  DdManager * unique)
{
    return unique->timeLimit;

} /* end of Cudd_ReadTimeLimit */


void
Cudd_SetTimeLimit(
  DdManager * unique,
  unsigned long tl)
{
    unique->timeLimit = tl;

} /* end of Cudd_SetTimeLimit */


void
Cudd_UpdateTimeLimit(
  DdManager * unique)
{
    unsigned long elapsed;
    if (unique->timeLimit == ~0UL)
        return;
    elapsed = util_cpu_time() - unique->startTime;
    if (unique->timeLimit >= elapsed) {
        unique->timeLimit -= elapsed;
    } else {
        unique->timeLimit = 0;
    }

} /* end of Cudd_UpdateTimeLimit */


void
Cudd_IncreaseTimeLimit(
  DdManager * unique,
  unsigned long increase)
{
    if (unique->timeLimit == ~0UL)
        unique->timeLimit = increase;
    else
        unique->timeLimit += increase;

} /* end of Cudd_IncreaseTimeLimit */


void
Cudd_UnsetTimeLimit(
  DdManager * unique)
{
    unique->timeLimit = ~0UL;

} /* end of Cudd_UnsetTimeLimit */


int
Cudd_TimeLimited(
  DdManager * unique)
{
    return unique->timeLimit != ~0UL;

} /* end of Cudd_TimeLimited */


void
Cudd_AutodynEnable(
  DdManager * unique,
  Cudd_ReorderingType  method)
{
    unique->autoDyn = 1;
    if (method != CUDD_REORDER_SAME) {
    unique->autoMethod = method;
    }
#ifndef DD_NO_DEATH_ROW
    /* If reordering is enabled, using the death row causes too many
    ** invocations. Hence, we shrink the death row to just one entry.
    */
    cuddClearDeathRow(unique);
    unique->deathRowDepth = 1;
    unique->deadMask = unique->deathRowDepth - 1;
    if ((unsigned) unique->nextDead > unique->deadMask) {
    unique->nextDead = 0;
    }
    unique->deathRow = REALLOC(DdNodePtr, unique->deathRow,
    unique->deathRowDepth);
#endif
    return;

} /* end of Cudd_AutodynEnable */


void
Cudd_AutodynDisable(
  DdManager * unique)
{
    unique->autoDyn = 0;
    return;

} /* end of Cudd_AutodynDisable */


int
Cudd_ReorderingStatus(
  DdManager * unique,
  Cudd_ReorderingType * method)
{
    *method = unique->autoMethod;
    return(unique->autoDyn);

} /* end of Cudd_ReorderingStatus */


void
Cudd_AutodynEnableZdd(
  DdManager * unique,
  Cudd_ReorderingType method)
{
    unique->autoDynZ = 1;
    if (method != CUDD_REORDER_SAME) {
    unique->autoMethodZ = method;
    }
    return;

} /* end of Cudd_AutodynEnableZdd */


void
Cudd_AutodynDisableZdd(
  DdManager * unique)
{
    unique->autoDynZ = 0;
    return;

} /* end of Cudd_AutodynDisableZdd */


int
Cudd_ReorderingStatusZdd(
  DdManager * unique,
  Cudd_ReorderingType * method)
{
    *method = unique->autoMethodZ;
    return(unique->autoDynZ);

} /* end of Cudd_ReorderingStatusZdd */


int
Cudd_zddRealignmentEnabled(
  DdManager * unique)
{
    return(unique->realign);

} /* end of Cudd_zddRealignmentEnabled */


void
Cudd_zddRealignEnable(
  DdManager * unique)
{
    unique->realign = 1;
    return;

} /* end of Cudd_zddRealignEnable */


void
Cudd_zddRealignDisable(
  DdManager * unique)
{
    unique->realign = 0;
    return;

} /* end of Cudd_zddRealignDisable */


int
Cudd_bddRealignmentEnabled(
  DdManager * unique)
{
    return(unique->realignZ);

} /* end of Cudd_bddRealignmentEnabled */


void
Cudd_bddRealignEnable(
  DdManager * unique)
{
    unique->realignZ = 1;
    return;

} /* end of Cudd_bddRealignEnable */


void
Cudd_bddRealignDisable(
  DdManager * unique)
{
    unique->realignZ = 0;
    return;

} /* end of Cudd_bddRealignDisable */


DdNode *
Cudd_ReadOne(
  DdManager * dd)
{
    return(dd->one);

} /* end of Cudd_ReadOne */


DdNode *
Cudd_ReadZddOne(
  DdManager * dd,
  int  i)
{
    if (i < 0)
    return(NULL);
    return(i < dd->sizeZ ? dd->univ[i] : DD_ONE(dd));

} /* end of Cudd_ReadZddOne */



DdNode *
Cudd_ReadZero(
  DdManager * dd)
{
    return(DD_ZERO(dd));

} /* end of Cudd_ReadZero */


DdNode *
Cudd_ReadLogicZero(
  DdManager * dd)
{
    return(Cudd_Not(DD_ONE(dd)));

} /* end of Cudd_ReadLogicZero */


DdNode *
Cudd_ReadPlusInfinity(
  DdManager * dd)
{
    return(dd->plusinfinity);

} /* end of Cudd_ReadPlusInfinity */


DdNode *
Cudd_ReadMinusInfinity(
  DdManager * dd)
{
    return(dd->minusinfinity);

} /* end of Cudd_ReadMinusInfinity */


DdNode *
Cudd_ReadBackground(
  DdManager * dd)
{
    return(dd->background);

} /* end of Cudd_ReadBackground */


void
Cudd_SetBackground(
  DdManager * dd,
  DdNode * bck)
{
    dd->background = bck;

} /* end of Cudd_SetBackground */


unsigned int
Cudd_ReadCacheSlots(
  DdManager * dd)
{
    return(dd->cacheSlots);

} /* end of Cudd_ReadCacheSlots */


double
Cudd_ReadCacheUsedSlots(
  DdManager * dd)
{
    unsigned long used = 0;
    int slots = dd->cacheSlots;
    DdCache *cache = dd->cache;
    int i;

    for (i = 0; i < slots; i++) {
    used += cache[i].h != 0;
    }

    return((double)used / (double) dd->cacheSlots);

} /* end of Cudd_ReadCacheUsedSlots */


double
Cudd_ReadCacheLookUps(
  DdManager * dd)
{
    return(dd->cacheHits + dd->cacheMisses +
       dd->totCachehits + dd->totCacheMisses);

} /* end of Cudd_ReadCacheLookUps */


double
Cudd_ReadCacheHits(
  DdManager * dd)
{
    return(dd->cacheHits + dd->totCachehits);

} /* end of Cudd_ReadCacheHits */


double
Cudd_ReadRecursiveCalls(
  DdManager * dd)
{
#ifdef DD_COUNT
    return(dd->recursiveCalls);
#else
    return(-1.0);
#endif

} /* end of Cudd_ReadRecursiveCalls */



unsigned int
Cudd_ReadMinHit(
  DdManager * dd)
{
    /* Internally, the package manipulates the ratio of hits to
    ** misses instead of the ratio of hits to accesses. */
    return((unsigned int) (0.5 + 100 * dd->minHit / (1 + dd->minHit)));

} /* end of Cudd_ReadMinHit */


void
Cudd_SetMinHit(
  DdManager * dd,
  unsigned int hr)
{
    /* Internally, the package manipulates the ratio of hits to
    ** misses instead of the ratio of hits to accesses. */
    dd->minHit = (double) hr / (100.0 - (double) hr);

} /* end of Cudd_SetMinHit */


unsigned int
Cudd_ReadLooseUpTo(
  DdManager * dd)
{
    return(dd->looseUpTo);

} /* end of Cudd_ReadLooseUpTo */


void
Cudd_SetLooseUpTo(
  DdManager * dd,
  unsigned int lut)
{
    if (lut == 0) {
    unsigned long datalimit = getSoftDataLimit();
    lut = (unsigned int) (datalimit / (sizeof(DdNode) *
                       DD_MAX_LOOSE_FRACTION));
    }
    dd->looseUpTo = lut;

} /* end of Cudd_SetLooseUpTo */


unsigned int
Cudd_ReadMaxCache(
  DdManager * dd)
{
    return(2 * dd->cacheSlots + dd->cacheSlack);

} /* end of Cudd_ReadMaxCache */


unsigned int
Cudd_ReadMaxCacheHard(
  DdManager * dd)
{
    return(dd->maxCacheHard);

} /* end of Cudd_ReadMaxCache */


void
Cudd_SetMaxCacheHard(
  DdManager * dd,
  unsigned int mc)
{
    if (mc == 0) {
    unsigned long datalimit = getSoftDataLimit();
    mc = (unsigned int) (datalimit / (sizeof(DdCache) *
                      DD_MAX_CACHE_FRACTION));
    }
    dd->maxCacheHard = mc;

} /* end of Cudd_SetMaxCacheHard */


int
Cudd_ReadSize(
  DdManager * dd)
{
    return(dd->size);

} /* end of Cudd_ReadSize */


int
Cudd_ReadZddSize(
  DdManager * dd)
{
    return(dd->sizeZ);

} /* end of Cudd_ReadZddSize */


unsigned int
Cudd_ReadSlots(
  DdManager * dd)
{
    return(dd->slots);

} /* end of Cudd_ReadSlots */


double
Cudd_ReadUsedSlots(
  DdManager * dd)
{
    unsigned long used = 0;
    int i, j;
    int size = dd->size;
    DdNodePtr *nodelist;
    DdSubtable *subtable;
    DdNode *node;
    DdNode *sentinel = &(dd->sentinel);

    /* Scan each BDD/ADD subtable. */
    for (i = 0; i < size; i++) {
    subtable = &(dd->subtables[i]);
    nodelist = subtable->nodelist;
    for (j = 0; (unsigned) j < subtable->slots; j++) {
        node = nodelist[j];
        if (node != sentinel) {
        used++;
        }
    }
    }

    /* Scan the ZDD subtables. */
    size = dd->sizeZ;

    for (i = 0; i < size; i++) {
    subtable = &(dd->subtableZ[i]);
    nodelist = subtable->nodelist;
    for (j = 0; (unsigned) j < subtable->slots; j++) {
        node = nodelist[j];
        if (node != NULL) {
        used++;
        }
    }
    }

    /* Constant table. */
    subtable = &(dd->constants);
    nodelist = subtable->nodelist;
    for (j = 0; (unsigned) j < subtable->slots; j++) {
    node = nodelist[j];
    if (node != NULL) {
        used++;
    }
    }

    return((double)used / (double) dd->slots);

} /* end of Cudd_ReadUsedSlots */


double
Cudd_ExpectedUsedSlots(
  DdManager * dd)
{
    int i;
    int size = dd->size;
    DdSubtable *subtable;
    double empty = 0.0;

    /* To each subtable we apply the corollary to Theorem 8.5 (occupancy
    ** distribution) from Sedgewick and Flajolet's Analysis of Algorithms.
    ** The corollary says that for a table with M buckets and a load ratio
    ** of r, the expected number of empty buckets is asymptotically given
    ** by M * exp(-r).
    */

    /* Scan each BDD/ADD subtable. */
    for (i = 0; i < size; i++) {
    subtable = &(dd->subtables[i]);
    empty += (double) subtable->slots *
        exp(-(double) subtable->keys / (double) subtable->slots);
    }

    /* Scan the ZDD subtables. */
    size = dd->sizeZ;

    for (i = 0; i < size; i++) {
    subtable = &(dd->subtableZ[i]);
    empty += (double) subtable->slots *
        exp(-(double) subtable->keys / (double) subtable->slots);
    }

    /* Constant table. */
    subtable = &(dd->constants);
    empty += (double) subtable->slots *
    exp(-(double) subtable->keys / (double) subtable->slots);

    return(1.0 - empty / (double) dd->slots);

} /* end of Cudd_ExpectedUsedSlots */


unsigned int
Cudd_ReadKeys(
  DdManager * dd)
{
    return(dd->keys);

} /* end of Cudd_ReadKeys */


unsigned int
Cudd_ReadDead(
  DdManager * dd)
{
    return(dd->dead);

} /* end of Cudd_ReadDead */


unsigned int
Cudd_ReadMinDead(
  DdManager * dd)
{
    return(dd->minDead);

} /* end of Cudd_ReadMinDead */


unsigned int
Cudd_ReadReorderings(
  DdManager * dd)
{
    return(dd->reorderings);

} /* end of Cudd_ReadReorderings */


unsigned int
Cudd_ReadMaxReorderings(
  DdManager * dd)
{
    return(dd->maxReorderings);

} /* end of Cudd_ReadMaxReorderings */


void
Cudd_SetMaxReorderings(
  DdManager * dd, unsigned int mr)
{
    dd->maxReorderings = mr;

} /* end of Cudd_SetMaxReorderings */


long
Cudd_ReadReorderingTime(
  DdManager * dd)
{
    return(dd->reordTime);

} /* end of Cudd_ReadReorderingTime */


int
Cudd_ReadGarbageCollections(
  DdManager * dd)
{
    return(dd->garbageCollections);

} /* end of Cudd_ReadGarbageCollections */


long
Cudd_ReadGarbageCollectionTime(
  DdManager * dd)
{
    return(dd->GCTime);

} /* end of Cudd_ReadGarbageCollectionTime */


double
Cudd_ReadNodesFreed(
  DdManager * dd)
{
#ifdef DD_STATS
    return(dd->nodesFreed);
#else
    return(-1.0);
#endif

} /* end of Cudd_ReadNodesFreed */


double
Cudd_ReadNodesDropped(
  DdManager * dd)
{
#ifdef DD_STATS
    return(dd->nodesDropped);
#else
    return(-1.0);
#endif

} /* end of Cudd_ReadNodesDropped */


double
Cudd_ReadUniqueLookUps(
  DdManager * dd)
{
#ifdef DD_UNIQUE_PROFILE
    return(dd->uniqueLookUps);
#else
    return(-1.0);
#endif

} /* end of Cudd_ReadUniqueLookUps */


double
Cudd_ReadUniqueLinks(
  DdManager * dd)
{
#ifdef DD_UNIQUE_PROFILE
    return(dd->uniqueLinks);
#else
    return(-1.0);
#endif

} /* end of Cudd_ReadUniqueLinks */


int
Cudd_ReadSiftMaxVar(
  DdManager * dd)
{
    return(dd->siftMaxVar);

} /* end of Cudd_ReadSiftMaxVar */


void
Cudd_SetSiftMaxVar(
  DdManager * dd,
  int  smv)
{
    dd->siftMaxVar = smv;

} /* end of Cudd_SetSiftMaxVar */


int
Cudd_ReadSiftMaxSwap(
  DdManager * dd)
{
    return(dd->siftMaxSwap);

} /* end of Cudd_ReadSiftMaxSwap */


void
Cudd_SetSiftMaxSwap(
  DdManager * dd,
  int  sms)
{
    dd->siftMaxSwap = sms;

} /* end of Cudd_SetSiftMaxSwap */


double
Cudd_ReadMaxGrowth(
  DdManager * dd)
{
    return(dd->maxGrowth);

} /* end of Cudd_ReadMaxGrowth */


void
Cudd_SetMaxGrowth(
  DdManager * dd,
  double mg)
{
    dd->maxGrowth = mg;

} /* end of Cudd_SetMaxGrowth */


double
Cudd_ReadMaxGrowthAlternate(
  DdManager * dd)
{
    return(dd->maxGrowthAlt);

} /* end of Cudd_ReadMaxGrowthAlternate */


void
Cudd_SetMaxGrowthAlternate(
  DdManager * dd,
  double mg)
{
    dd->maxGrowthAlt = mg;

} /* end of Cudd_SetMaxGrowthAlternate */


int
Cudd_ReadReorderingCycle(
  DdManager * dd)
{
    return(dd->reordCycle);

} /* end of Cudd_ReadReorderingCycle */


void
Cudd_SetReorderingCycle(
  DdManager * dd,
  int cycle)
{
    dd->reordCycle = cycle;

} /* end of Cudd_SetReorderingCycle */


MtrNode *
Cudd_ReadTree(
  DdManager * dd)
{
    return(dd->tree);

} /* end of Cudd_ReadTree */


void
Cudd_SetTree(
  DdManager * dd,
  MtrNode * tree)
{
    if (dd->tree != NULL) {
    Mtr_FreeTree(dd->tree);
    }
    dd->tree = tree;
    if (tree == NULL) return;

    fixVarTree(tree, dd->perm, dd->size);
    return;

} /* end of Cudd_SetTree */


void
Cudd_FreeTree(
  DdManager * dd)
{
    if (dd->tree != NULL) {
    Mtr_FreeTree(dd->tree);
    dd->tree = NULL;
    }
    return;

} /* end of Cudd_FreeTree */


MtrNode *
Cudd_ReadZddTree(
  DdManager * dd)
{
    return(dd->treeZ);

} /* end of Cudd_ReadZddTree */


void
Cudd_SetZddTree(
  DdManager * dd,
  MtrNode * tree)
{
    if (dd->treeZ != NULL) {
    Mtr_FreeTree(dd->treeZ);
    }
    dd->treeZ = tree;
    if (tree == NULL) return;

    fixVarTree(tree, dd->permZ, dd->sizeZ);
    return;

} /* end of Cudd_SetZddTree */


void
Cudd_FreeZddTree(
  DdManager * dd)
{
    if (dd->treeZ != NULL) {
    Mtr_FreeTree(dd->treeZ);
    dd->treeZ = NULL;
    }
    return;

} /* end of Cudd_FreeZddTree */


unsigned int
Cudd_NodeReadIndex(
  DdNode * node)
{
    return((unsigned int) Cudd_Regular(node)->index);

} /* end of Cudd_NodeReadIndex */


int
Cudd_ReadPerm(
  DdManager * dd,
  int  i)
{
    if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX);
    if (i < 0 || i >= dd->size) return(-1);
    return(dd->perm[i]);

} /* end of Cudd_ReadPerm */


int
Cudd_ReadPermZdd(
  DdManager * dd,
  int  i)
{
    if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX);
    if (i < 0 || i >= dd->sizeZ) return(-1);
    return(dd->permZ[i]);

} /* end of Cudd_ReadPermZdd */


int
Cudd_ReadInvPerm(
  DdManager * dd,
  int  i)
{
    if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX);
    if (i < 0 || i >= dd->size) return(-1);
    return(dd->invperm[i]);

} /* end of Cudd_ReadInvPerm */


int
Cudd_ReadInvPermZdd(
  DdManager * dd,
  int  i)
{
    if (i == CUDD_CONST_INDEX) return(CUDD_CONST_INDEX);
    if (i < 0 || i >= dd->sizeZ) return(-1);
    return(dd->invpermZ[i]);

} /* end of Cudd_ReadInvPermZdd */


DdNode *
Cudd_ReadVars(
  DdManager * dd,
  int  i)
{
    if (i < 0 || i > dd->size) return(NULL);
    return(dd->vars[i]);

} /* end of Cudd_ReadVars */


CUDD_VALUE_TYPE
Cudd_ReadEpsilon(
  DdManager * dd)
{
    return(dd->epsilon);

} /* end of Cudd_ReadEpsilon */


void
Cudd_SetEpsilon(
  DdManager * dd,
  CUDD_VALUE_TYPE  ep)
{
    dd->epsilon = ep;

} /* end of Cudd_SetEpsilon */


Cudd_AggregationType
Cudd_ReadGroupcheck(
  DdManager * dd)
{
    return(dd->groupcheck);

} /* end of Cudd_ReadGroupCheck */


void
Cudd_SetGroupcheck(
  DdManager * dd,
  Cudd_AggregationType gc)
{
    dd->groupcheck = gc;

} /* end of Cudd_SetGroupcheck */


int
Cudd_GarbageCollectionEnabled(
  DdManager * dd)
{
    return(dd->gcEnabled);

} /* end of Cudd_GarbageCollectionEnabled */


void
Cudd_EnableGarbageCollection(
  DdManager * dd)
{
    dd->gcEnabled = 1;

} /* end of Cudd_EnableGarbageCollection */


void
Cudd_DisableGarbageCollection(
  DdManager * dd)
{
    dd->gcEnabled = 0;

} /* end of Cudd_DisableGarbageCollection */


int
Cudd_DeadAreCounted(
  DdManager * dd)
{
    return(dd->countDead == 0 ? 1 : 0);

} /* end of Cudd_DeadAreCounted */


void
Cudd_TurnOnCountDead(
  DdManager * dd)
{
    dd->countDead = 0;

} /* end of Cudd_TurnOnCountDead */


void
Cudd_TurnOffCountDead(
  DdManager * dd)
{
    dd->countDead = ~0;

} /* end of Cudd_TurnOffCountDead */


int
Cudd_ReadRecomb(
  DdManager * dd)
{
    return(dd->recomb);

} /* end of Cudd_ReadRecomb */


void
Cudd_SetRecomb(
  DdManager * dd,
  int  recomb)
{
    dd->recomb = recomb;

} /* end of Cudd_SetRecomb */


int
Cudd_ReadSymmviolation(
  DdManager * dd)
{
    return(dd->symmviolation);

} /* end of Cudd_ReadSymmviolation */


void
Cudd_SetSymmviolation(
  DdManager * dd,
  int  symmviolation)
{
    dd->symmviolation = symmviolation;

} /* end of Cudd_SetSymmviolation */


int
Cudd_ReadArcviolation(
  DdManager * dd)
{
    return(dd->arcviolation);

} /* end of Cudd_ReadArcviolation */


void
Cudd_SetArcviolation(
  DdManager * dd,
  int  arcviolation)
{
    dd->arcviolation = arcviolation;

} /* end of Cudd_SetArcviolation */


int
Cudd_ReadPopulationSize(
  DdManager * dd)
{
    return(dd->populationSize);

} /* end of Cudd_ReadPopulationSize */


void
Cudd_SetPopulationSize(
  DdManager * dd,
  int  populationSize)
{
    dd->populationSize = populationSize;

} /* end of Cudd_SetPopulationSize */


int
Cudd_ReadNumberXovers(
  DdManager * dd)
{
    return(dd->numberXovers);

} /* end of Cudd_ReadNumberXovers */


void
Cudd_SetNumberXovers(
  DdManager * dd,
  int  numberXovers)
{
    dd->numberXovers = numberXovers;

} /* end of Cudd_SetNumberXovers */


unsigned int
Cudd_ReadOrderRandomization(
  DdManager * dd)
{
    return(dd->randomizeOrder);

} /* end of Cudd_ReadOrderRandomization */


void
Cudd_SetOrderRandomization(
  DdManager * dd,
  unsigned int factor)
{
    dd->randomizeOrder = factor;

} /* end of Cudd_SetOrderRandomization */


unsigned long
Cudd_ReadMemoryInUse(
  DdManager * dd)
{
    return(dd->memused);

} /* end of Cudd_ReadMemoryInUse */


int
Cudd_PrintInfo(
  DdManager * dd,
  FILE * fp)
{
    int retval;
    Cudd_ReorderingType autoMethod, autoMethodZ;

    /* Modifiable parameters. */
    retval = fprintf(fp,"**** CUDD modifiable parameters ****\n");
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Hard limit for cache size: %u\n",
             Cudd_ReadMaxCacheHard(dd));
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Cache hit threshold for resizing: %u%%\n",
             Cudd_ReadMinHit(dd));
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Garbage collection enabled: %s\n",
             Cudd_GarbageCollectionEnabled(dd) ? "yes" : "no");
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Limit for fast unique table growth: %u\n",
             Cudd_ReadLooseUpTo(dd));
    if (retval == EOF) return(0);
    retval = fprintf(fp,
             "Maximum number of variables sifted per reordering: %d\n",
             Cudd_ReadSiftMaxVar(dd));
    if (retval == EOF) return(0);
    retval = fprintf(fp,
             "Maximum number of variable swaps per reordering: %d\n",
             Cudd_ReadSiftMaxSwap(dd));
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Maximum growth while sifting a variable: %g\n",
             Cudd_ReadMaxGrowth(dd));
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Dynamic reordering of BDDs enabled: %s\n",
             Cudd_ReorderingStatus(dd,&autoMethod) ? "yes" : "no");
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Default BDD reordering method: %d\n",
             (int) autoMethod);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Dynamic reordering of ZDDs enabled: %s\n",
             Cudd_ReorderingStatusZdd(dd,&autoMethodZ) ? "yes" : "no");
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Default ZDD reordering method: %d\n",
             (int) autoMethodZ);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Realignment of ZDDs to BDDs enabled: %s\n",
             Cudd_zddRealignmentEnabled(dd) ? "yes" : "no");
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Realignment of BDDs to ZDDs enabled: %s\n",
             Cudd_bddRealignmentEnabled(dd) ? "yes" : "no");
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Dead nodes counted in triggering reordering: %s\n",
             Cudd_DeadAreCounted(dd) ? "yes" : "no");
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Group checking criterion: %d\n",
             (int) Cudd_ReadGroupcheck(dd));
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Recombination threshold: %d\n", Cudd_ReadRecomb(dd));
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Symmetry violation threshold: %d\n",
             Cudd_ReadSymmviolation(dd));
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Arc violation threshold: %d\n",
             Cudd_ReadArcviolation(dd));
    if (retval == EOF) return(0);
    retval = fprintf(fp,"GA population size: %d\n",
             Cudd_ReadPopulationSize(dd));
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of crossovers for GA: %d\n",
             Cudd_ReadNumberXovers(dd));
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Next reordering threshold: %u\n",
             Cudd_ReadNextReordering(dd));
    if (retval == EOF) return(0);

    /* Non-modifiable parameters. */
    retval = fprintf(fp,"**** CUDD non-modifiable parameters ****\n");
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Memory in use: %lu\n", Cudd_ReadMemoryInUse(dd));
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Peak number of nodes: %ld\n",
             Cudd_ReadPeakNodeCount(dd));
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Peak number of live nodes: %d\n",
             Cudd_ReadPeakLiveNodeCount(dd));
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of BDD variables: %d\n", dd->size);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of ZDD variables: %d\n", dd->sizeZ);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of cache entries: %u\n", dd->cacheSlots);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of cache look-ups: %.0f\n",
             Cudd_ReadCacheLookUps(dd));
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of cache hits: %.0f\n",
             Cudd_ReadCacheHits(dd));
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of cache insertions: %.0f\n",
             dd->cacheinserts);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of cache collisions: %.0f\n",
             dd->cachecollisions);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of cache deletions: %.0f\n",
             dd->cachedeletions);
    if (retval == EOF) return(0);
    retval = cuddCacheProfile(dd,fp);
    if (retval == 0) return(0);
    retval = fprintf(fp,"Soft limit for cache size: %u\n",
             Cudd_ReadMaxCache(dd));
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of buckets in unique table: %u\n", dd->slots);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Used buckets in unique table: %.2f%% (expected %.2f%%)\n",
             100.0 * Cudd_ReadUsedSlots(dd),
             100.0 * Cudd_ExpectedUsedSlots(dd));
    if (retval == EOF) return(0);
#ifdef DD_UNIQUE_PROFILE
    retval = fprintf(fp,"Unique lookups: %.0f\n", dd->uniqueLookUps);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Unique links: %.0f (%g per lookup)\n",
        dd->uniqueLinks, dd->uniqueLinks / dd->uniqueLookUps);
    if (retval == EOF) return(0);
#endif
    retval = fprintf(fp,"Number of BDD and ADD nodes: %u\n", dd->keys);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of ZDD nodes: %u\n", dd->keysZ);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of dead BDD and ADD nodes: %u\n", dd->dead);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Number of dead ZDD nodes: %u\n", dd->deadZ);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Total number of nodes allocated: %.0f\n",
             dd->allocated);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Total number of nodes reclaimed: %.0f\n",
             dd->reclaimed);
    if (retval == EOF) return(0);
#ifdef DD_STATS
    retval = fprintf(fp,"Nodes freed: %.0f\n", dd->nodesFreed);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Nodes dropped: %.0f\n", dd->nodesDropped);
    if (retval == EOF) return(0);
#endif
#ifdef DD_COUNT
    retval = fprintf(fp,"Number of recursive calls: %.0f\n",
             Cudd_ReadRecursiveCalls(dd));
    if (retval == EOF) return(0);
#endif
    retval = fprintf(fp,"Garbage collections so far: %d\n",
             Cudd_ReadGarbageCollections(dd));
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Time for garbage collection: %.2f sec\n",
             ((double)Cudd_ReadGarbageCollectionTime(dd)/1000.0));
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Reorderings so far: %d\n", dd->reorderings);
    if (retval == EOF) return(0);
    retval = fprintf(fp,"Time for reordering: %.2f sec\n",
             ((double)Cudd_ReadReorderingTime(dd)/1000.0));
    if (retval == EOF) return(0);
#ifdef DD_COUNT
    retval = fprintf(fp,"Node swaps in reordering: %.0f\n",
    Cudd_ReadSwapSteps(dd));
    if (retval == EOF) return(0);
#endif

    return(1);

} /* end of Cudd_PrintInfo */


long
Cudd_ReadPeakNodeCount(
  DdManager * dd)
{
    long count = 0;
    DdNodePtr *scan = dd->memoryList;

    while (scan != NULL) {
    count += DD_MEM_CHUNK;
    scan = (DdNodePtr *) *scan;
    }
    return(count);

} /* end of Cudd_ReadPeakNodeCount */


int
Cudd_ReadPeakLiveNodeCount(
  DdManager * dd)
{
    unsigned int live = dd->keys - dd->dead;

    if (live > dd->peakLiveNodes) {
    dd->peakLiveNodes = live;
    }
    return((int)dd->peakLiveNodes);

} /* end of Cudd_ReadPeakLiveNodeCount */


long
Cudd_ReadNodeCount(
  DdManager * dd)
{
    long count;
    int i;

#ifndef DD_NO_DEATH_ROW
    cuddClearDeathRow(dd);
#endif

    count = (long) (dd->keys - dd->dead);

    /* Count isolated projection functions. Their number is subtracted
    ** from the node count because they are not part of the BDDs.
    */
    for (i=0; i < dd->size; i++) {
    if (dd->vars[i]->ref == 1) count--;
    }
    /* Subtract from the count the unused constants. */
    if (DD_ZERO(dd)->ref == 1) count--;
    if (DD_PLUS_INFINITY(dd)->ref == 1) count--;
    if (DD_MINUS_INFINITY(dd)->ref == 1) count--;

    return(count);

} /* end of Cudd_ReadNodeCount */



long
Cudd_zddReadNodeCount(
  DdManager * dd)
{
    return((long)(dd->keysZ - dd->deadZ + 2));

} /* end of Cudd_zddReadNodeCount */


int
Cudd_AddHook(
  DdManager * dd,
  DD_HFP f,
  Cudd_HookType where)
{
    DdHook **hook, *nextHook, *newHook;

    switch (where) {
    case CUDD_PRE_GC_HOOK:
    hook = &(dd->preGCHook);
    break;
    case CUDD_POST_GC_HOOK:
    hook = &(dd->postGCHook);
    break;
    case CUDD_PRE_REORDERING_HOOK:
    hook = &(dd->preReorderingHook);
    break;
    case CUDD_POST_REORDERING_HOOK:
    hook = &(dd->postReorderingHook);
    break;
    default:
    return(0);
    }
    /* Scan the list and find whether the function is already there.
    ** If so, just return. */
    nextHook = *hook;
    while (nextHook != NULL) {
    if (nextHook->f == f) {
        return(2);
    }
    hook = &(nextHook->next);
    nextHook = nextHook->next;
    }
    /* The function was not in the list. Create a new item and append it
    ** to the end of the list. */
    newHook = ALLOC(DdHook,1);
    if (newHook == NULL) {
    dd->errorCode = CUDD_MEMORY_OUT;
    return(0);
    }
    newHook->next = NULL;
    newHook->f = f;
    *hook = newHook;
    return(1);

} /* end of Cudd_AddHook */


int
Cudd_RemoveHook(
  DdManager * dd,
  DD_HFP f,
  Cudd_HookType where)
{
    DdHook **hook, *nextHook;

    switch (where) {
    case CUDD_PRE_GC_HOOK:
    hook = &(dd->preGCHook);
    break;
    case CUDD_POST_GC_HOOK:
    hook = &(dd->postGCHook);
    break;
    case CUDD_PRE_REORDERING_HOOK:
    hook = &(dd->preReorderingHook);
    break;
    case CUDD_POST_REORDERING_HOOK:
    hook = &(dd->postReorderingHook);
    break;
    default:
    return(0);
    }
    nextHook = *hook;
    while (nextHook != NULL) {
    if (nextHook->f == f) {
        *hook = nextHook->next;
        FREE(nextHook);
        return(1);
    }
    hook = &(nextHook->next);
    nextHook = nextHook->next;
    }

    return(0);

} /* end of Cudd_RemoveHook */


int
Cudd_IsInHook(
  DdManager * dd,
  DD_HFP f,
  Cudd_HookType where)
{
    DdHook *hook;

    switch (where) {
    case CUDD_PRE_GC_HOOK:
    hook = dd->preGCHook;
    break;
    case CUDD_POST_GC_HOOK:
    hook = dd->postGCHook;
    break;
    case CUDD_PRE_REORDERING_HOOK:
    hook = dd->preReorderingHook;
    break;
    case CUDD_POST_REORDERING_HOOK:
    hook = dd->postReorderingHook;
    break;
    default:
    return(0);
    }
    /* Scan the list and find whether the function is already there. */
    while (hook != NULL) {
    if (hook->f == f) {
        return(1);
    }
    hook = hook->next;
    }
    return(0);

} /* end of Cudd_IsInHook */


int
Cudd_StdPreReordHook(
  DdManager *dd,
  const char *str,
  void *data)
{
    Cudd_ReorderingType method = (Cudd_ReorderingType) (ptruint) data;
    int retval;

    retval = fprintf(dd->out,"%s reordering with ", str);
    if (retval == EOF) return(0);
    switch (method) {
    case CUDD_REORDER_SIFT_CONVERGE:
    case CUDD_REORDER_SYMM_SIFT_CONV:
    case CUDD_REORDER_GROUP_SIFT_CONV:
    case CUDD_REORDER_WINDOW2_CONV:
    case CUDD_REORDER_WINDOW3_CONV:
    case CUDD_REORDER_WINDOW4_CONV:
    case CUDD_REORDER_LINEAR_CONVERGE:
    retval = fprintf(dd->out,"converging ");
    if (retval == EOF) return(0);
    break;
    default:
    break;
    }
    switch (method) {
    case CUDD_REORDER_RANDOM:
    case CUDD_REORDER_RANDOM_PIVOT:
    retval = fprintf(dd->out,"random");
    break;
    case CUDD_REORDER_SIFT:
    case CUDD_REORDER_SIFT_CONVERGE:
    retval = fprintf(dd->out,"sifting");
    break;
    case CUDD_REORDER_SYMM_SIFT:
    case CUDD_REORDER_SYMM_SIFT_CONV:
    retval = fprintf(dd->out,"symmetric sifting");
    break;
    case CUDD_REORDER_LAZY_SIFT:
    retval = fprintf(dd->out,"lazy sifting");
    break;
    case CUDD_REORDER_GROUP_SIFT:
    case CUDD_REORDER_GROUP_SIFT_CONV:
    retval = fprintf(dd->out,"group sifting");
    break;
    case CUDD_REORDER_WINDOW2:
    case CUDD_REORDER_WINDOW3:
    case CUDD_REORDER_WINDOW4:
    case CUDD_REORDER_WINDOW2_CONV:
    case CUDD_REORDER_WINDOW3_CONV:
    case CUDD_REORDER_WINDOW4_CONV:
    retval = fprintf(dd->out,"window");
    break;
    case CUDD_REORDER_ANNEALING:
    retval = fprintf(dd->out,"annealing");
    break;
    case CUDD_REORDER_GENETIC:
    retval = fprintf(dd->out,"genetic");
    break;
    case CUDD_REORDER_LINEAR:
    case CUDD_REORDER_LINEAR_CONVERGE:
    retval = fprintf(dd->out,"linear sifting");
    break;
    case CUDD_REORDER_EXACT:
    retval = fprintf(dd->out,"exact");
    break;
    default:
    return(0);
    }
    if (retval == EOF) return(0);

    retval = fprintf(dd->out,": from %ld to ... ", strcmp(str, "BDD") == 0 ?
             Cudd_ReadNodeCount(dd) : Cudd_zddReadNodeCount(dd));
    if (retval == EOF) return(0);
    fflush(dd->out);
    return(1);

} /* end of Cudd_StdPreReordHook */


int
Cudd_StdPostReordHook(
  DdManager *dd,
  const char *str,
  void *data)
{
    unsigned long initialTime = (long) data;
    int retval;
    unsigned long finalTime = util_cpu_time();
    double totalTimeSec = (double)(finalTime - initialTime) / 1000.0;

    retval = fprintf(dd->out,"%ld nodes in %g sec\n", strcmp(str, "BDD") == 0 ?
             Cudd_ReadNodeCount(dd) : Cudd_zddReadNodeCount(dd),
             totalTimeSec);
    if (retval == EOF) return(0);
    retval = fflush(dd->out);
    if (retval == EOF) return(0);
    return(1);

} /* end of Cudd_StdPostReordHook */


int
Cudd_EnableReorderingReporting(
  DdManager *dd)
{
    if (!Cudd_AddHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK)) {
    return(0);
    }
    if (!Cudd_AddHook(dd, Cudd_StdPostReordHook, CUDD_POST_REORDERING_HOOK)) {
    return(0);
    }
    return(1);

} /* end of Cudd_EnableReorderingReporting */


int
Cudd_DisableReorderingReporting(
  DdManager *dd)
{
    if (!Cudd_RemoveHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK)) {
    return(0);
    }
    if (!Cudd_RemoveHook(dd, Cudd_StdPostReordHook, CUDD_POST_REORDERING_HOOK)) {
    return(0);
    }
    return(1);

} /* end of Cudd_DisableReorderingReporting */


int
Cudd_ReorderingReporting(
  DdManager *dd)
{
    return(Cudd_IsInHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK));

} /* end of Cudd_ReorderingReporting */


int
Cudd_PrintGroupedOrder(
  DdManager * dd,
  const char *str,
  void *data)
{
    int isBdd = strcmp(str, "ZDD");
    MtrNode *tree = isBdd ? dd->tree : dd->treeZ;
    int *invperm = isBdd ? dd->invperm : dd->invpermZ;
    int size = isBdd ? dd->size : dd->sizeZ;
    if (tree == NULL) {
        int i, retval;
        for (i=0; i < size; i++) {
            retval = fprintf(dd->out, "%c%d", i==0 ? '(' : ',', invperm[i]);
            if (retval == EOF) return(0);
        }
        retval = fprintf(dd->out,")\n");
        return (retval != EOF);
    } else {
        return Mtr_PrintGroupedOrder(tree,invperm,dd->out);
    }
        
} /* end of Cudd_PrintGroupedOrder */


int
Cudd_EnableOrderingMonitoring(
  DdManager *dd)
{
    if (!Cudd_AddHook(dd, Cudd_PrintGroupedOrder, CUDD_PRE_REORDERING_HOOK)) {
    return(0);
    }
    if (!Cudd_AddHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK)) {
    return(0);
    }
    if (!Cudd_AddHook(dd, Cudd_StdPostReordHook, CUDD_POST_REORDERING_HOOK)) {
    return(0);
    }
    if (!Cudd_AddHook(dd, Cudd_PrintGroupedOrder, CUDD_POST_REORDERING_HOOK)) {
    return(0);
    }
    return(1);

} /* end of Cudd_EnableOrderingMonitoring */


int
Cudd_DisableOrderingMonitoring(
  DdManager *dd)
{
    if (!Cudd_RemoveHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK)) {
    return(0);
    }
    if (!Cudd_RemoveHook(dd, Cudd_PrintGroupedOrder, CUDD_PRE_REORDERING_HOOK)) {
    return(0);
    }
    if (!Cudd_RemoveHook(dd, Cudd_PrintGroupedOrder, CUDD_POST_REORDERING_HOOK)) {
    return(0);
    }
    if (!Cudd_RemoveHook(dd, Cudd_StdPostReordHook, CUDD_POST_REORDERING_HOOK)) {
    return(0);
    }
    return(1);

} /* end of Cudd_DisableOrderingMonitoring */


int
Cudd_OrderingMonitoring(
  DdManager *dd)
{
    return(Cudd_IsInHook(dd, Cudd_PrintGroupedOrder, CUDD_PRE_REORDERING_HOOK));

} /* end of Cudd_OrderingMonitoring */


Cudd_ErrorType
Cudd_ReadErrorCode(
  DdManager *dd)
{
    return(dd->errorCode);

} /* end of Cudd_ReadErrorCode */


void
Cudd_ClearErrorCode(
  DdManager *dd)
{
    dd->errorCode = CUDD_NO_ERROR;

} /* end of Cudd_ClearErrorCode */


FILE *
Cudd_ReadStdout(
  DdManager *dd)
{
    return(dd->out);

} /* end of Cudd_ReadStdout */


void
Cudd_SetStdout(
  DdManager *dd,
  FILE *fp)
{
    dd->out = fp;

} /* end of Cudd_SetStdout */


FILE *
Cudd_ReadStderr(
  DdManager *dd)
{
    return(dd->err);

} /* end of Cudd_ReadStderr */


void
Cudd_SetStderr(
  DdManager *dd,
  FILE *fp)
{
    dd->err = fp;

} /* end of Cudd_SetStderr */


unsigned int
Cudd_ReadNextReordering(
  DdManager *dd)
{
    return(dd->nextDyn);

} /* end of Cudd_ReadNextReordering */


void
Cudd_SetNextReordering(
  DdManager *dd,
  unsigned int next)
{
    dd->nextDyn = next;

} /* end of Cudd_SetNextReordering */


double
Cudd_ReadSwapSteps(
  DdManager *dd)
{
#ifdef DD_COUNT
    return(dd->swapSteps);
#else
    return(-1);
#endif

} /* end of Cudd_ReadSwapSteps */


unsigned int
Cudd_ReadMaxLive(
  DdManager *dd)
{
    return(dd->maxLive);

} /* end of Cudd_ReadMaxLive */


void
Cudd_SetMaxLive(
  DdManager *dd,
  unsigned int maxLive)
{
    dd->maxLive = maxLive;

} /* end of Cudd_SetMaxLive */


unsigned long
Cudd_ReadMaxMemory(
  DdManager *dd)
{
    return(dd->maxmemhard);

} /* end of Cudd_ReadMaxMemory */


void
Cudd_SetMaxMemory(
  DdManager *dd,
  unsigned long maxMemory)
{
    dd->maxmemhard = maxMemory;

} /* end of Cudd_SetMaxMemory */


int
Cudd_bddBindVar(
  DdManager *dd /* manager */,
  int index /* variable index */)
{
    if (index >= dd->size || index < 0) return(0);
    dd->subtables[dd->perm[index]].bindVar = 1;
    return(1);

} /* end of Cudd_bddBindVar */


int
Cudd_bddUnbindVar(
  DdManager *dd /* manager */,
  int index /* variable index */)
{
    if (index >= dd->size || index < 0) return(0);
    dd->subtables[dd->perm[index]].bindVar = 0;
    return(1);

} /* end of Cudd_bddUnbindVar */


int
Cudd_bddVarIsBound(
  DdManager *dd /* manager */,
  int index /* variable index */)
{
    if (index >= dd->size || index < 0) return(0);
    return(dd->subtables[dd->perm[index]].bindVar);

} /* end of Cudd_bddVarIsBound */


int
Cudd_bddSetPiVar(
  DdManager *dd /* manager */,
  int index /* variable index */)
{
    if (index >= dd->size || index < 0) return (0);
    dd->subtables[dd->perm[index]].varType = CUDD_VAR_PRIMARY_INPUT;
    return(1);

} /* end of Cudd_bddSetPiVar */


int
Cudd_bddSetPsVar(
  DdManager *dd /* manager */,
  int index /* variable index */)
{
    if (index >= dd->size || index < 0) return (0);
    dd->subtables[dd->perm[index]].varType = CUDD_VAR_PRESENT_STATE;
    return(1);

} /* end of Cudd_bddSetPsVar */


int
Cudd_bddSetNsVar(
  DdManager *dd /* manager */,
  int index /* variable index */)
{
    if (index >= dd->size || index < 0) return (0);
    dd->subtables[dd->perm[index]].varType = CUDD_VAR_NEXT_STATE;
    return(1);

} /* end of Cudd_bddSetNsVar */


int
Cudd_bddIsPiVar(
  DdManager *dd /* manager */,
  int index /* variable index */)
{
    if (index >= dd->size || index < 0) return -1;
    return (dd->subtables[dd->perm[index]].varType == CUDD_VAR_PRIMARY_INPUT);

} /* end of Cudd_bddIsPiVar */


int
Cudd_bddIsPsVar(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return -1;
    return (dd->subtables[dd->perm[index]].varType == CUDD_VAR_PRESENT_STATE);

} /* end of Cudd_bddIsPsVar */


int
Cudd_bddIsNsVar(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return -1;
    return (dd->subtables[dd->perm[index]].varType == CUDD_VAR_NEXT_STATE);

} /* end of Cudd_bddIsNsVar */


int
Cudd_bddSetPairIndex(
  DdManager *dd /* manager */,
  int index /* variable index */,
  int pairIndex /* corresponding variable index */)
{
    if (index >= dd->size || index < 0) return(0);
    dd->subtables[dd->perm[index]].pairIndex = pairIndex;
    return(1);

} /* end of Cudd_bddSetPairIndex */


int
Cudd_bddReadPairIndex(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return -1;
    return dd->subtables[dd->perm[index]].pairIndex;

} /* end of Cudd_bddReadPairIndex */


int
Cudd_bddSetVarToBeGrouped(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return(0);
    if (dd->subtables[dd->perm[index]].varToBeGrouped <= CUDD_LAZY_SOFT_GROUP) {
    dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_SOFT_GROUP;
    }
    return(1);

} /* end of Cudd_bddSetVarToBeGrouped */


int
Cudd_bddSetVarHardGroup(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return(0);
    dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_HARD_GROUP;
    return(1);

} /* end of Cudd_bddSetVarHardGrouped */


int
Cudd_bddResetVarToBeGrouped(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return(0);
    if (dd->subtables[dd->perm[index]].varToBeGrouped <=
    CUDD_LAZY_SOFT_GROUP) {
    dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_NONE;
    }
    return(1);

} /* end of Cudd_bddResetVarToBeGrouped */


int
Cudd_bddIsVarToBeGrouped(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return(-1);
    if (dd->subtables[dd->perm[index]].varToBeGrouped == CUDD_LAZY_UNGROUP)
    return(0);
    else
    return(dd->subtables[dd->perm[index]].varToBeGrouped);

} /* end of Cudd_bddIsVarToBeGrouped */


int
Cudd_bddSetVarToBeUngrouped(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return(0);
    dd->subtables[dd->perm[index]].varToBeGrouped = CUDD_LAZY_UNGROUP;
    return(1);

} /* end of Cudd_bddSetVarToBeGrouped */


int
Cudd_bddIsVarToBeUngrouped(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return(-1);
    return dd->subtables[dd->perm[index]].varToBeGrouped == CUDD_LAZY_UNGROUP;

} /* end of Cudd_bddIsVarToBeGrouped */


int
Cudd_bddIsVarHardGroup(
  DdManager *dd,
  int index)
{
    if (index >= dd->size || index < 0) return(-1);
    if (dd->subtables[dd->perm[index]].varToBeGrouped == CUDD_LAZY_HARD_GROUP)
    return(1);
    return(0);

} /* end of Cudd_bddIsVarToBeGrouped */


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

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


static void
fixVarTree(
  MtrNode * treenode,
  int * perm,
  int  size)
{
    treenode->index = treenode->low;
    treenode->low = ((int) treenode->index < size) ?
    perm[treenode->index] : treenode->index;
    if (treenode->child != NULL)
    fixVarTree(treenode->child, perm, size);
    if (treenode->younger != NULL)
    fixVarTree(treenode->younger, perm, size);
    return;

} /* end of fixVarTree */


static int
addMultiplicityGroups(
  DdManager *dd /* manager */,
  MtrNode *treenode /* current tree node */,
  int multiplicity /* how many ZDD vars per BDD var */,
  char *vmask /* variable pairs for which a group has been already built */,
  char *lmask /* levels for which a group has already been built*/)
{
    int startV, stopV, startL;
    int i, j;
    MtrNode *auxnode = treenode;

    while (auxnode != NULL) {
    if (auxnode->child != NULL) {
        addMultiplicityGroups(dd,auxnode->child,multiplicity,vmask,lmask);
    }
    /* Build remaining groups. */
    startV = dd->permZ[auxnode->index] / multiplicity;
    startL = auxnode->low / multiplicity;
    stopV = startV + auxnode->size / multiplicity;
    /* Walk down vmask starting at startV and build missing groups. */
    for (i = startV, j = startL; i < stopV; i++) {
        if (vmask[i] == 0) {
        MtrNode *node;
        while (lmask[j] == 1) j++;
        node = Mtr_MakeGroup(auxnode, j * multiplicity, multiplicity,
                     MTR_FIXED);
        if (node == NULL) {
            return(0);
        }
        node->index = dd->invpermZ[i * multiplicity];
        vmask[i] = 1;
        lmask[j] = 1;
        }
    }
    auxnode = auxnode->younger;
    }
    return(1);

} /* end of addMultiplicityGroups */