Version abc70930

1 files changed, 4409 insertions, 0 deletions

diff --git a/abc70930/src/bdd/cudd/cuddAPI.c b/abc70930/src/bdd/cudd/cuddAPI.c
new file mode 100644
index 00000000..a16b82cf
--- /dev/null
+++ b/abc70930/src/bdd/cudd/cuddAPI.c
@@ -0,0 +1,4409 @@
+/**CFile***********************************************************************
+
+  FileName    [cuddAPI.c]
+
+  PackageName [cudd]
+
+  Synopsis    [Application interface functions.]
+
+  Description [External procedures included in this module:
+        <ul>
+        <li> Cudd_addNewVar()
+        <li> Cudd_addNewVarAtLevel()
+        <li> Cudd_bddNewVar()
+        <li> Cudd_bddNewVarAtLevel()
+        <li> Cudd_addIthVar()
+        <li> Cudd_bddIthVar()
+        <li> Cudd_zddIthVar()
+        <li> Cudd_zddVarsFromBddVars()
+        <li> Cudd_addConst()
+        <li> Cudd_IsNonConstant()
+        <li> Cudd_AutodynEnable()
+        <li> Cudd_AutodynDisable()
+        <li> Cudd_ReorderingStatus()
+        <li> Cudd_AutodynEnableZdd()
+        <li> Cudd_AutodynDisableZdd()
+        <li> Cudd_ReorderingStatusZdd()
+        <li> Cudd_zddRealignmentEnabled()
+        <li> Cudd_zddRealignEnable()
+        <li> Cudd_zddRealignDisable()
+        <li> Cudd_bddRealignmentEnabled()
+        <li> Cudd_bddRealignEnable()
+        <li> Cudd_bddRealignDisable()
+        <li> Cudd_ReadOne()
+        <li> Cudd_ReadZddOne()
+        <li> Cudd_ReadZero()
+        <li> Cudd_ReadLogicZero()
+        <li> Cudd_ReadPlusInfinity()
+        <li> Cudd_ReadMinusInfinity()
+        <li> Cudd_ReadBackground()
+        <li> Cudd_SetBackground()
+        <li> Cudd_ReadCacheSlots()
+        <li> Cudd_ReadCacheUsedSlots()
+        <li> Cudd_ReadCacheLookUps()
+        <li> Cudd_ReadCacheHits()
+        <li> Cudd_ReadMinHit()
+        <li> Cudd_SetMinHit()
+        <li> Cudd_ReadLooseUpTo()
+        <li> Cudd_SetLooseUpTo()
+        <li> Cudd_ReadMaxCache()
+        <li> Cudd_ReadMaxCacheHard()
+        <li> Cudd_SetMaxCacheHard()
+        <li> Cudd_ReadSize()
+        <li> Cudd_ReadSlots()
+        <li> Cudd_ReadUsedSlots()
+        <li> Cudd_ExpectedUsedSlots()
+        <li> Cudd_ReadKeys()
+        <li> Cudd_ReadDead()
+        <li> Cudd_ReadMinDead()
+        <li> Cudd_ReadReorderings()
+        <li> Cudd_ReadReorderingTime()
+        <li> Cudd_ReadGarbageCollections()
+        <li> Cudd_ReadGarbageCollectionTime()
+        <li> Cudd_ReadNodesFreed()
+        <li> Cudd_ReadNodesDropped()
+        <li> Cudd_ReadUniqueLookUps()
+        <li> Cudd_ReadUniqueLinks()
+        <li> Cudd_ReadSiftMaxVar()
+        <li> Cudd_SetSiftMaxVar()
+        <li> Cudd_ReadMaxGrowth()
+        <li> Cudd_SetMaxGrowth()
+        <li> Cudd_ReadMaxGrowthAlternate()
+        <li> Cudd_SetMaxGrowthAlternate()
+        <li> Cudd_ReadReorderingCycle()
+        <li> Cudd_SetReorderingCycle()
+        <li> Cudd_ReadTree()
+        <li> Cudd_SetTree()
+        <li> Cudd_FreeTree()
+        <li> Cudd_ReadZddTree()
+        <li> Cudd_SetZddTree()
+        <li> Cudd_FreeZddTree()
+                <li> Cudd_NodeReadIndex()
+        <li> Cudd_ReadPerm()
+        <li> Cudd_ReadInvPerm()
+        <li> Cudd_ReadVars()
+        <li> Cudd_ReadEpsilon()
+        <li> Cudd_SetEpsilon()
+        <li> Cudd_ReadGroupCheck()
+        <li> Cudd_SetGroupcheck()
+        <li> Cudd_GarbageCollectionEnabled()
+        <li> Cudd_EnableGarbageCollection()
+        <li> Cudd_DisableGarbageCollection()
+        <li> Cudd_DeadAreCounted()
+        <li> Cudd_TurnOnCountDead()
+        <li> Cudd_TurnOffCountDead()
+        <li> Cudd_ReadRecomb()
+        <li> Cudd_SetRecomb()
+        <li> Cudd_ReadSymmviolation()
+        <li> Cudd_SetSymmviolation()
+        <li> Cudd_ReadArcviolation()
+        <li> Cudd_SetArcviolation()
+        <li> Cudd_ReadPopulationSize()
+        <li> Cudd_SetPopulationSize()
+        <li> Cudd_ReadNumberXovers()
+        <li> Cudd_SetNumberXovers()
+        <li> Cudd_ReadMemoryInUse()
+        <li> Cudd_PrintInfo()
+        <li> Cudd_ReadPeakNodeCount()
+        <li> Cudd_ReadPeakLiveNodeCount()
+        <li> Cudd_ReadNodeCount()
+        <li> Cudd_zddReadNodeCount()
+        <li> Cudd_AddHook()
+        <li> Cudd_RemoveHook()
+        <li> Cudd_IsInHook()
+        <li> Cudd_StdPreReordHook()
+        <li> Cudd_StdPostReordHook()
+        <li> Cudd_EnableReorderingReporting()
+        <li> Cudd_DisableReorderingReporting()
+        <li> Cudd_ReorderingReporting()
+        <li> Cudd_ReadErrorCode()
+        <li> Cudd_ClearErrorCode()
+        <li> Cudd_ReadStdout()
+        <li> Cudd_SetStdout()
+        <li> Cudd_ReadStderr()
+        <li> Cudd_SetStderr()
+        <li> Cudd_ReadNextReordering()
+        <li> Cudd_SetNextReordering()
+        <li> Cudd_ReadSwapSteps()
+        <li> Cudd_ReadMaxLive()
+        <li> Cudd_SetMaxLive()
+        <li> Cudd_ReadMaxMemory()
+        <li> Cudd_SetMaxMemory()
+        <li> Cudd_bddBindVar()
+        <li> Cudd_bddUnbindVar()
+        <li> Cudd_bddVarIsBound()
+        <li> Cudd_bddSetPiVar()
+        <li> Cudd_bddSetPsVar()
+        <li> Cudd_bddSetNsVar()
+        <li> Cudd_bddIsPiVar()
+        <li> Cudd_bddIsPsVar()
+        <li> Cudd_bddIsNsVar()
+        <li> Cudd_bddSetPairIndex()
+        <li> Cudd_bddReadPairIndex()
+        <li> Cudd_bddSetVarToBeGrouped()
+        <li> Cudd_bddSetVarHardGroup()
+        <li> Cudd_bddResetVarToBeGrouped()
+        <li> Cudd_bddIsVarToBeGrouped()
+        <li> Cudd_bddSetVarToBeUngrouped()
+        <li> Cudd_bddIsVarToBeUngrouped()
+        <li> Cudd_bddIsVarHardGroup()
+        </ul>
+          Static procedures included in this module:
+        <ul>
+        <li> fixVarTree()
+        </ul>]
+
+  SeeAlso     []
+
+  Author      [Fabio Somenzi]
+
+  Copyright   [This file was created at the University of Colorado at
+  Boulder.  The University of Colorado at Boulder makes no warranty
+  about the suitability of this software for any purpose.  It is
+  presented on an AS IS basis.]
+
+******************************************************************************/
+
+#include    "util_hack.h"
+#include    "cuddInt.h"
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+#ifndef lint
+static char rcsid[] DD_UNUSED = "$Id: cuddAPI.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $";
+#endif
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes                                                */
+/*---------------------------------------------------------------------------*/
+
+static void fixVarTree ARGS((MtrNode *treenode, int *perm, int size));
+static int addMultiplicityGroups ARGS((DdManager *dd, MtrNode *treenode, int multiplicity, char *vmask, char *lmask));
+
+/**AutomaticEnd***************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions                                          */
+/*---------------------------------------------------------------------------*/
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns a new ADD variable.]
+
+  Description [Creates a new ADD variable.  The new variable has an
+  index equal to the largest previous index plus 1.  Returns a
+  pointer to the new variable if successful; NULL otherwise.
+  An ADD variable differs from a BDD variable because it points to the
+  arithmetic zero, instead of having a complement pointer to 1. ]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_bddNewVar Cudd_addIthVar Cudd_addConst
+  Cudd_addNewVarAtLevel]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns a new ADD variable at a specified level.]
+
+  Description [Creates a new ADD variable.  The new variable has an
+  index equal to the largest previous index plus 1 and is positioned at
+  the specified level in the order.  Returns a pointer to the new
+  variable if successful; NULL otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_addNewVar Cudd_addIthVar Cudd_bddNewVarAtLevel]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns a new BDD variable.]
+
+  Description [Creates a new BDD variable.  The new variable has an
+  index equal to the largest previous index plus 1.  Returns a
+  pointer to the new variable if successful; NULL otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_addNewVar Cudd_bddIthVar Cudd_bddNewVarAtLevel]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns a new BDD variable at a specified level.]
+
+  Description [Creates a new BDD variable.  The new variable has an
+  index equal to the largest previous index plus 1 and is positioned at
+  the specified level in the order.  Returns a pointer to the new
+  variable if successful; NULL otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_bddNewVar Cudd_bddIthVar Cudd_addNewVarAtLevel]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the ADD variable with index i.]
+
+  Description [Retrieves the ADD variable with index i if it already
+  exists, or creates a new ADD variable.  Returns a pointer to the
+  variable if successful; NULL otherwise.  An ADD variable differs from
+  a BDD variable because it points to the arithmetic zero, instead of
+  having a complement pointer to 1. ]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_addNewVar Cudd_bddIthVar Cudd_addConst
+  Cudd_addNewVarAtLevel]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the BDD variable with index i.]
+
+  Description [Retrieves the BDD variable with index i if it already
+  exists, or creates a new BDD variable.  Returns a pointer to the
+  variable if successful; NULL otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_bddNewVar Cudd_addIthVar Cudd_bddNewVarAtLevel
+  Cudd_ReadVars]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the ZDD variable with index i.]
+
+  Description [Retrieves the ZDD variable with index i if it already
+  exists, or creates a new ZDD variable.  Returns a pointer to the
+  variable if successful; NULL otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_bddIthVar Cudd_addIthVar]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Creates one or more ZDD variables for each BDD variable.]
+
+  Description [Creates one or more ZDD variables for each BDD
+  variable.  If some ZDD variables already exist, only the missing
+  variables are created.  Parameter multiplicity allows the caller to
+  control how many variables are created for each BDD variable in
+  existence. For instance, if ZDDs are used to represent covers, two
+  ZDD variables are required for each BDD variable.  The order of the
+  BDD variables is transferred to the ZDD variables. If a variable
+  group tree exists for the BDD variables, a corresponding ZDD
+  variable group tree is created by expanding the BDD variable
+  tree. In any case, the ZDD variables derived from the same BDD
+  variable are merged in a ZDD variable group. If a ZDD variable group
+  tree exists, it is freed. Returns 1 if successful; 0 otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_bddNewVar Cudd_bddIthVar Cudd_bddNewVarAtLevel]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the ADD for constant c.]
+
+  Description [Retrieves the ADD for constant c if it already
+  exists, or creates a new ADD.  Returns a pointer to the
+  ADD if successful; NULL otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_addNewVar Cudd_addIthVar]
+
+******************************************************************************/
+DdNode *
+Cudd_addConst(
+  DdManager * dd,
+  CUDD_VALUE_TYPE  c)
+{
+    return(cuddUniqueConst(dd,c));
+
+} /* end of Cudd_addConst */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns 1 if a DD node is not constant.]
+
+  Description [Returns 1 if a DD node is not constant. This function is
+  useful to test the results of Cudd_bddIteConstant, Cudd_addIteConstant,
+  Cudd_addEvalConst. These results may be a special value signifying
+  non-constant. In the other cases the macro Cudd_IsConstant can be used.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_IsConstant Cudd_bddIteConstant Cudd_addIteConstant
+  Cudd_addEvalConst]
+
+******************************************************************************/
+int
+Cudd_IsNonConstant(
+  DdNode *f)
+{
+    return(f == DD_NON_CONSTANT || !Cudd_IsConstant(f));
+
+} /* end of Cudd_IsNonConstant */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Enables automatic dynamic reordering of BDDs and ADDs.]
+
+  Description [Enables automatic dynamic reordering of BDDs and
+  ADDs. Parameter method is used to determine the method used for
+  reordering. If CUDD_REORDER_SAME is passed, the method is
+  unchanged.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_AutodynDisable Cudd_ReorderingStatus
+  Cudd_AutodynEnableZdd]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Disables automatic dynamic reordering.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_AutodynEnable Cudd_ReorderingStatus
+  Cudd_AutodynDisableZdd]
+
+******************************************************************************/
+void
+Cudd_AutodynDisable(
+  DdManager * unique)
+{
+    unique->autoDyn = 0;
+    return;
+
+} /* end of Cudd_AutodynDisable */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reports the status of automatic dynamic reordering of BDDs
+  and ADDs.]
+
+  Description [Reports the status of automatic dynamic reordering of
+  BDDs and ADDs. Parameter method is set to the reordering method
+  currently selected. Returns 1 if automatic reordering is enabled; 0
+  otherwise.]
+
+  SideEffects [Parameter method is set to the reordering method currently
+  selected.]
+
+  SeeAlso     [Cudd_AutodynEnable Cudd_AutodynDisable
+  Cudd_ReorderingStatusZdd]
+
+******************************************************************************/
+int
+Cudd_ReorderingStatus(
+  DdManager * unique,
+  Cudd_ReorderingType * method)
+{
+    *method = unique->autoMethod;
+    return(unique->autoDyn);
+
+} /* end of Cudd_ReorderingStatus */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Enables automatic dynamic reordering of ZDDs.]
+
+  Description [Enables automatic dynamic reordering of ZDDs. Parameter
+  method is used to determine the method used for reordering ZDDs. If
+  CUDD_REORDER_SAME is passed, the method is unchanged.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_AutodynDisableZdd Cudd_ReorderingStatusZdd
+  Cudd_AutodynEnable]
+
+******************************************************************************/
+void
+Cudd_AutodynEnableZdd(
+  DdManager * unique,
+  Cudd_ReorderingType method)
+{
+    unique->autoDynZ = 1;
+    if (method != CUDD_REORDER_SAME) {
+    unique->autoMethodZ = method;
+    }
+    return;
+
+} /* end of Cudd_AutodynEnableZdd */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Disables automatic dynamic reordering of ZDDs.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_AutodynEnableZdd Cudd_ReorderingStatusZdd
+  Cudd_AutodynDisable]
+
+******************************************************************************/
+void
+Cudd_AutodynDisableZdd(
+  DdManager * unique)
+{
+    unique->autoDynZ = 0;
+    return;
+
+} /* end of Cudd_AutodynDisableZdd */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reports the status of automatic dynamic reordering of ZDDs.]
+
+  Description [Reports the status of automatic dynamic reordering of
+  ZDDs. Parameter method is set to the ZDD reordering method currently
+  selected. Returns 1 if automatic reordering is enabled; 0
+  otherwise.]
+
+  SideEffects [Parameter method is set to the ZDD reordering method currently
+  selected.]
+
+  SeeAlso     [Cudd_AutodynEnableZdd Cudd_AutodynDisableZdd
+  Cudd_ReorderingStatus]
+
+******************************************************************************/
+int
+Cudd_ReorderingStatusZdd(
+  DdManager * unique,
+  Cudd_ReorderingType * method)
+{
+    *method = unique->autoMethodZ;
+    return(unique->autoDynZ);
+
+} /* end of Cudd_ReorderingStatusZdd */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Tells whether the realignment of ZDD order to BDD order is
+  enabled.]
+
+  Description [Returns 1 if the realignment of ZDD order to BDD order is
+  enabled; 0 otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_zddRealignEnable Cudd_zddRealignDisable
+  Cudd_bddRealignEnable Cudd_bddRealignDisable]
+
+******************************************************************************/
+int
+Cudd_zddRealignmentEnabled(
+  DdManager * unique)
+{
+    return(unique->realign);
+
+} /* end of Cudd_zddRealignmentEnabled */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Enables realignment of ZDD order to BDD order.]
+
+  Description [Enables realignment of the ZDD variable order to the
+  BDD variable order after the BDDs and ADDs have been reordered.  The
+  number of ZDD variables must be a multiple of the number of BDD
+  variables for realignment to make sense. If this condition is not met,
+  Cudd_ReduceHeap will return 0. Let <code>M</code> be the
+  ratio of the two numbers. For the purpose of realignment, the ZDD
+  variables from <code>M*i</code> to <code>(M+1)*i-1</code> are
+  reagarded as corresponding to BDD variable <code>i</code>. Realignment
+  is initially disabled.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReduceHeap Cudd_zddRealignDisable
+  Cudd_zddRealignmentEnabled Cudd_bddRealignDisable
+  Cudd_bddRealignmentEnabled]
+
+******************************************************************************/
+void
+Cudd_zddRealignEnable(
+  DdManager * unique)
+{
+    unique->realign = 1;
+    return;
+
+} /* end of Cudd_zddRealignEnable */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Disables realignment of ZDD order to BDD order.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_zddRealignEnable Cudd_zddRealignmentEnabled
+  Cudd_bddRealignEnable Cudd_bddRealignmentEnabled]
+
+******************************************************************************/
+void
+Cudd_zddRealignDisable(
+  DdManager * unique)
+{
+    unique->realign = 0;
+    return;
+
+} /* end of Cudd_zddRealignDisable */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Tells whether the realignment of BDD order to ZDD order is
+  enabled.]
+
+  Description [Returns 1 if the realignment of BDD order to ZDD order is
+  enabled; 0 otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_bddRealignEnable Cudd_bddRealignDisable
+  Cudd_zddRealignEnable Cudd_zddRealignDisable]
+
+******************************************************************************/
+int
+Cudd_bddRealignmentEnabled(
+  DdManager * unique)
+{
+    return(unique->realignZ);
+
+} /* end of Cudd_bddRealignmentEnabled */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Enables realignment of BDD order to ZDD order.]
+
+  Description [Enables realignment of the BDD variable order to the
+  ZDD variable order after the ZDDs have been reordered.  The
+  number of ZDD variables must be a multiple of the number of BDD
+  variables for realignment to make sense. If this condition is not met,
+  Cudd_zddReduceHeap will return 0. Let <code>M</code> be the
+  ratio of the two numbers. For the purpose of realignment, the ZDD
+  variables from <code>M*i</code> to <code>(M+1)*i-1</code> are
+  reagarded as corresponding to BDD variable <code>i</code>. Realignment
+  is initially disabled.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_zddReduceHeap Cudd_bddRealignDisable
+  Cudd_bddRealignmentEnabled Cudd_zddRealignDisable
+  Cudd_zddRealignmentEnabled]
+
+******************************************************************************/
+void
+Cudd_bddRealignEnable(
+  DdManager * unique)
+{
+    unique->realignZ = 1;
+    return;
+
+} /* end of Cudd_bddRealignEnable */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Disables realignment of ZDD order to BDD order.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_bddRealignEnable Cudd_bddRealignmentEnabled
+  Cudd_zddRealignEnable Cudd_zddRealignmentEnabled]
+
+******************************************************************************/
+void
+Cudd_bddRealignDisable(
+  DdManager * unique)
+{
+    unique->realignZ = 0;
+    return;
+
+} /* end of Cudd_bddRealignDisable */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the one constant of the manager.]
+
+  Description [Returns the one constant of the manager. The one
+  constant is common to ADDs and BDDs.]
+
+  SideEffects [None]
+
+  SeeAlso [Cudd_ReadZero Cudd_ReadLogicZero Cudd_ReadZddOne]
+
+******************************************************************************/
+DdNode *
+Cudd_ReadOne(
+  DdManager * dd)
+{
+    return(dd->one);
+
+} /* end of Cudd_ReadOne */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the ZDD for the constant 1 function.]
+
+  Description [Returns the ZDD for the constant 1 function.
+  The representation of the constant 1 function as a ZDD depends on
+  how many variables it (nominally) depends on. The index of the
+  topmost variable in the support is given as argument <code>i</code>.]
+
+  SideEffects [None]
+
+  SeeAlso [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 */
+
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the zero constant of the manager.]
+
+  Description [Returns the zero constant of the manager. The zero
+  constant is the arithmetic zero, rather than the logic zero. The
+  latter is the complement of the one constant.]
+
+  SideEffects [None]
+
+  SeeAlso [Cudd_ReadOne Cudd_ReadLogicZero]
+
+******************************************************************************/
+DdNode *
+Cudd_ReadZero(
+  DdManager * dd)
+{
+    return(DD_ZERO(dd));
+
+} /* end of Cudd_ReadZero */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the logic zero constant of the manager.]
+
+  Description [Returns the zero constant of the manager. The logic zero
+  constant is the complement of the one constant, and is distinct from
+  the arithmetic zero.]
+
+  SideEffects [None]
+
+  SeeAlso [Cudd_ReadOne Cudd_ReadZero]
+
+******************************************************************************/
+DdNode *
+Cudd_ReadLogicZero(
+  DdManager * dd)
+{
+    return(Cudd_Not(DD_ONE(dd)));
+
+} /* end of Cudd_ReadLogicZero */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads the plus-infinity constant from the manager.]
+
+  Description []
+
+  SideEffects [None]
+
+******************************************************************************/
+DdNode *
+Cudd_ReadPlusInfinity(
+  DdManager * dd)
+{
+    return(dd->plusinfinity);
+
+} /* end of Cudd_ReadPlusInfinity */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads the minus-infinity constant from the manager.]
+
+  Description []
+
+  SideEffects [None]
+
+******************************************************************************/
+DdNode *
+Cudd_ReadMinusInfinity(
+  DdManager * dd)
+{
+    return(dd->minusinfinity);
+
+} /* end of Cudd_ReadMinusInfinity */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads the background constant of the manager.]
+
+  Description []
+
+  SideEffects [None]
+
+******************************************************************************/
+DdNode *
+Cudd_ReadBackground(
+  DdManager * dd)
+{
+    return(dd->background);
+
+} /* end of Cudd_ReadBackground */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets the background constant of the manager.]
+
+  Description [Sets the background constant of the manager. It assumes
+  that the DdNode pointer bck is already referenced.]
+
+  SideEffects [None]
+
+******************************************************************************/
+void
+Cudd_SetBackground(
+  DdManager * dd,
+  DdNode * bck)
+{
+    dd->background = bck;
+
+} /* end of Cudd_SetBackground */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads the number of slots in the cache.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadCacheUsedSlots]
+
+******************************************************************************/
+unsigned int
+Cudd_ReadCacheSlots(
+  DdManager * dd)
+{
+    return(dd->cacheSlots);
+
+} /* end of Cudd_ReadCacheSlots */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads the fraction of used slots in the cache.]
+
+  Description [Reads the fraction of used slots in the cache. The unused
+  slots are those in which no valid data is stored. Garbage collection,
+  variable reordering, and cache resizing may cause used slots to become
+  unused.]
+
+  SideEffects [None]
+
+  SeeAlso     [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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the number of cache look-ups.]
+
+  Description [Returns the number of cache look-ups.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadCacheHits]
+
+******************************************************************************/
+double
+Cudd_ReadCacheLookUps(
+  DdManager * dd)
+{
+    return(dd->cacheHits + dd->cacheMisses +
+       dd->totCachehits + dd->totCacheMisses);
+
+} /* end of Cudd_ReadCacheLookUps */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the number of cache hits.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadCacheLookUps]
+
+******************************************************************************/
+double
+Cudd_ReadCacheHits(
+  DdManager * dd)
+{
+    return(dd->cacheHits + dd->totCachehits);
+
+} /* end of Cudd_ReadCacheHits */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the number of recursive calls.]
+
+  Description [Returns the number of recursive calls if the package is
+  compiled with DD_COUNT defined.]
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+double
+Cudd_ReadRecursiveCalls(
+  DdManager * dd)
+{
+#ifdef DD_COUNT
+    return(dd->recursiveCalls);
+#else
+    return(-1.0);
+#endif
+
+} /* end of Cudd_ReadRecursiveCalls */
+
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads the hit rate that causes resizinig of the computed
+  table.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_SetMinHit]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets the hit rate that causes resizinig of the computed
+  table.]
+
+  Description [Sets the minHit parameter of the manager. This
+  parameter controls the resizing of the computed table. If the hit
+  rate is larger than the specified value, and the cache is not
+  already too large, then its size is doubled.]
+
+  SideEffects [None]
+
+  SeeAlso     [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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads the looseUpTo parameter of the manager.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_SetLooseUpTo Cudd_ReadMinHit Cudd_ReadMinDead]
+
+******************************************************************************/
+unsigned int
+Cudd_ReadLooseUpTo(
+  DdManager * dd)
+{
+    return(dd->looseUpTo);
+
+} /* end of Cudd_ReadLooseUpTo */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets the looseUpTo parameter of the manager.]
+
+  Description [Sets the looseUpTo parameter of the manager. This
+  parameter of the manager controls the threshold beyond which no fast
+  growth of the unique table is allowed. The threshold is given as a
+  number of slots. If the value passed to this function is 0, the
+  function determines a suitable value based on the available memory.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadLooseUpTo Cudd_SetMinHit]
+
+******************************************************************************/
+void
+Cudd_SetLooseUpTo(
+  DdManager * dd,
+  unsigned int lut)
+{
+    if (lut == 0) {
+    long datalimit = getSoftDataLimit();
+    lut = (unsigned int) (datalimit / (sizeof(DdNode) *
+                       DD_MAX_LOOSE_FRACTION));
+    }
+    dd->looseUpTo = lut;
+
+} /* end of Cudd_SetLooseUpTo */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the soft limit for the cache size.]
+
+  Description [Returns the soft limit for the cache size. The soft limit]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadMaxCache]
+
+******************************************************************************/
+unsigned int
+Cudd_ReadMaxCache(
+  DdManager * dd)
+{
+    return(2 * dd->cacheSlots + dd->cacheSlack);
+
+} /* end of Cudd_ReadMaxCache */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads the maxCacheHard parameter of the manager.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_SetMaxCacheHard Cudd_ReadMaxCache]
+
+******************************************************************************/
+unsigned int
+Cudd_ReadMaxCacheHard(
+  DdManager * dd)
+{
+    return(dd->maxCacheHard);
+
+} /* end of Cudd_ReadMaxCache */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets the maxCacheHard parameter of the manager.]
+
+  Description [Sets the maxCacheHard parameter of the manager. The
+  cache cannot grow larger than maxCacheHard entries. This parameter
+  allows an application to control the trade-off of memory versus
+  speed. If the value passed to this function is 0, the function
+  determines a suitable maximum cache size based on the available memory.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadMaxCacheHard Cudd_SetMaxCache]
+
+******************************************************************************/
+void
+Cudd_SetMaxCacheHard(
+  DdManager * dd,
+  unsigned int mc)
+{
+    if (mc == 0) {
+    long datalimit = getSoftDataLimit();
+    mc = (unsigned int) (datalimit / (sizeof(DdCache) *
+                      DD_MAX_CACHE_FRACTION));
+    }
+    dd->maxCacheHard = mc;
+
+} /* end of Cudd_SetMaxCacheHard */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the number of BDD variables in existance.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadZddSize]
+
+******************************************************************************/
+int
+Cudd_ReadSize(
+  DdManager * dd)
+{
+    return(dd->size);
+
+} /* end of Cudd_ReadSize */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the number of ZDD variables in existance.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadSize]
+
+******************************************************************************/
+int
+Cudd_ReadZddSize(
+  DdManager * dd)
+{
+    return(dd->sizeZ);
+
+} /* end of Cudd_ReadZddSize */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the total number of slots of the unique table.]
+
+  Description [Returns the total number of slots of the unique table.
+  This number ismainly for diagnostic purposes.]
+
+  SideEffects [None]
+
+******************************************************************************/
+unsigned int
+Cudd_ReadSlots(
+  DdManager * dd)
+{
+    return(dd->slots);
+
+} /* end of Cudd_ReadSlots */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads the fraction of used slots in the unique table.]
+
+  Description [Reads the fraction of used slots in the unique
+  table. The unused slots are those in which no valid data is
+  stored. Garbage collection, variable reordering, and subtable
+  resizing may cause used slots to become unused.]
+
+  SideEffects [None]
+
+  SeeAlso     [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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Computes the expected fraction of used slots in the unique
+  table.]
+
+  Description [Computes the fraction of slots in the unique table that
+  should be in use. This expected value is based on the assumption
+  that the hash function distributes the keys randomly; it can be
+  compared with the result of Cudd_ReadUsedSlots to monitor the
+  performance of the unique table hash function.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadSlots 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 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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the number of nodes in the unique table.]
+
+  Description [Returns the total number of nodes currently in the unique
+  table, including the dead nodes.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadDead]
+
+******************************************************************************/
+unsigned int
+Cudd_ReadKeys(
+  DdManager * dd)
+{
+    return(dd->keys);
+
+} /* end of Cudd_ReadKeys */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the number of dead nodes in the unique table.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadKeys]
+
+******************************************************************************/
+unsigned int
+Cudd_ReadDead(
+  DdManager * dd)
+{
+    return(dd->dead);
+
+} /* end of Cudd_ReadDead */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads the minDead parameter of the manager.]
+
+  Description [Reads the minDead parameter of the manager. The minDead
+  parameter is used by the package to decide whether to collect garbage
+  or resize a subtable of the unique table when the subtable becomes
+  too full. The application can indirectly control the value of minDead
+  by setting the looseUpTo parameter.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadDead Cudd_ReadLooseUpTo Cudd_SetLooseUpTo]
+
+******************************************************************************/
+unsigned int
+Cudd_ReadMinDead(
+  DdManager * dd)
+{
+    return(dd->minDead);
+
+} /* end of Cudd_ReadMinDead */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the number of times reordering has occurred.]
+
+  Description [Returns the number of times reordering has occurred in the
+  manager. The number includes both the calls to Cudd_ReduceHeap from
+  the application program and those automatically performed by the
+  package. However, calls that do not even initiate reordering are not
+  counted. A call may not initiate reordering if there are fewer than
+  minsize live nodes in the manager, or if CUDD_REORDER_NONE is specified
+  as reordering method. The calls to Cudd_ShuffleHeap are not counted.]
+
+  SideEffects [None]
+
+  SeeAlso [Cudd_ReduceHeap Cudd_ReadReorderingTime]
+
+******************************************************************************/
+int
+Cudd_ReadReorderings(
+  DdManager * dd)
+{
+    return(dd->reorderings);
+
+} /* end of Cudd_ReadReorderings */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the time spent in reordering.]
+
+  Description [Returns the number of milliseconds spent reordering
+  variables since the manager was initialized. The time spent in collecting
+  garbage before reordering is included.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadReorderings]
+
+******************************************************************************/
+long
+Cudd_ReadReorderingTime(
+  DdManager * dd)
+{
+    return(dd->reordTime);
+
+} /* end of Cudd_ReadReorderingTime */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the number of times garbage collection has occurred.]
+
+  Description [Returns the number of times garbage collection has
+  occurred in the manager. The number includes both the calls from
+  reordering procedures and those caused by requests to create new
+  nodes.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadGarbageCollectionTime]
+
+******************************************************************************/
+int
+Cudd_ReadGarbageCollections(
+  DdManager * dd)
+{
+    return(dd->garbageCollections);
+
+} /* end of Cudd_ReadGarbageCollections */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the time spent in garbage collection.]
+
+  Description [Returns the number of milliseconds spent doing garbage
+  collection since the manager was initialized.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadGarbageCollections]
+
+******************************************************************************/
+long
+Cudd_ReadGarbageCollectionTime(
+  DdManager * dd)
+{
+    return(dd->GCTime);
+
+} /* end of Cudd_ReadGarbageCollectionTime */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the number of nodes freed.]
+
+  Description [Returns the number of nodes returned to the free list if the
+  keeping of this statistic is enabled; -1 otherwise. This statistic is
+  enabled only if the package is compiled with DD_STATS defined.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadNodesDropped]
+
+******************************************************************************/
+double
+Cudd_ReadNodesFreed(
+  DdManager * dd)
+{
+#ifdef DD_STATS
+    return(dd->nodesFreed);
+#else
+    return(-1.0);
+#endif
+
+} /* end of Cudd_ReadNodesFreed */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the number of nodes dropped.]
+
+  Description [Returns the number of nodes killed by dereferencing if the
+  keeping of this statistic is enabled; -1 otherwise. This statistic is
+  enabled only if the package is compiled with DD_STATS defined.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadNodesFreed]
+
+******************************************************************************/
+double
+Cudd_ReadNodesDropped(
+  DdManager * dd)
+{
+#ifdef DD_STATS
+    return(dd->nodesDropped);
+#else
+    return(-1.0);
+#endif
+
+} /* end of Cudd_ReadNodesDropped */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the number of look-ups in the unique table.]
+
+  Description [Returns the number of look-ups in the unique table if the
+  keeping of this statistic is enabled; -1 otherwise. This statistic is
+  enabled only if the package is compiled with DD_UNIQUE_PROFILE defined.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadUniqueLinks]
+
+******************************************************************************/
+double
+Cudd_ReadUniqueLookUps(
+  DdManager * dd)
+{
+#ifdef DD_UNIQUE_PROFILE
+    return(dd->uniqueLookUps);
+#else
+    return(-1.0);
+#endif
+
+} /* end of Cudd_ReadUniqueLookUps */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the number of links followed in the unique table.]
+
+  Description [Returns the number of links followed during look-ups in the
+  unique table if the keeping of this statistic is enabled; -1 otherwise.
+  If an item is found in the first position of its collision list, the
+  number of links followed is taken to be 0. If it is in second position,
+  the number of links is 1, and so on. This statistic is enabled only if
+  the package is compiled with DD_UNIQUE_PROFILE defined.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadUniqueLookUps]
+
+******************************************************************************/
+double
+Cudd_ReadUniqueLinks(
+  DdManager * dd)
+{
+#ifdef DD_UNIQUE_PROFILE
+    return(dd->uniqueLinks);
+#else
+    return(-1.0);
+#endif
+
+} /* end of Cudd_ReadUniqueLinks */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads the siftMaxVar parameter of the manager.]
+
+  Description [Reads the siftMaxVar parameter of the manager. This
+  parameter gives the maximum number of variables that will be sifted
+  for each invocation of sifting.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadSiftMaxSwap Cudd_SetSiftMaxVar]
+
+******************************************************************************/
+int
+Cudd_ReadSiftMaxVar(
+  DdManager * dd)
+{
+    return(dd->siftMaxVar);
+
+} /* end of Cudd_ReadSiftMaxVar */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets the siftMaxVar parameter of the manager.]
+
+  Description [Sets the siftMaxVar parameter of the manager. This
+  parameter gives the maximum number of variables that will be sifted
+  for each invocation of sifting.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_SetSiftMaxSwap Cudd_ReadSiftMaxVar]
+
+******************************************************************************/
+void
+Cudd_SetSiftMaxVar(
+  DdManager * dd,
+  int  smv)
+{
+    dd->siftMaxVar = smv;
+
+} /* end of Cudd_SetSiftMaxVar */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads the siftMaxSwap parameter of the manager.]
+
+  Description [Reads the siftMaxSwap parameter of the manager. This
+  parameter gives the maximum number of swaps that will be attempted
+  for each invocation of sifting. The real number of swaps may exceed
+  the set limit because the package will always complete the sifting
+  of the variable that causes the limit to be reached.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadSiftMaxVar Cudd_SetSiftMaxSwap]
+
+******************************************************************************/
+int
+Cudd_ReadSiftMaxSwap(
+  DdManager * dd)
+{
+    return(dd->siftMaxSwap);
+
+} /* end of Cudd_ReadSiftMaxSwap */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets the siftMaxSwap parameter of the manager.]
+
+  Description [Sets the siftMaxSwap parameter of the manager. This
+  parameter gives the maximum number of swaps that will be attempted
+  for each invocation of sifting. The real number of swaps may exceed
+  the set limit because the package will always complete the sifting
+  of the variable that causes the limit to be reached.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_SetSiftMaxVar Cudd_ReadSiftMaxSwap]
+
+******************************************************************************/
+void
+Cudd_SetSiftMaxSwap(
+  DdManager * dd,
+  int  sms)
+{
+    dd->siftMaxSwap = sms;
+
+} /* end of Cudd_SetSiftMaxSwap */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads the maxGrowth parameter of the manager.]
+
+  Description [Reads the maxGrowth parameter of the manager.  This
+  parameter determines how much the number of nodes can grow during
+  sifting of a variable.  Overall, sifting never increases the size of
+  the decision diagrams.  This parameter only refers to intermediate
+  results.  A lower value will speed up sifting, possibly at the
+  expense of quality.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_SetMaxGrowth Cudd_ReadMaxGrowthAlternate]
+
+******************************************************************************/
+double
+Cudd_ReadMaxGrowth(
+  DdManager * dd)
+{
+    return(dd->maxGrowth);
+
+} /* end of Cudd_ReadMaxGrowth */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets the maxGrowth parameter of the manager.]
+
+  Description [Sets the maxGrowth parameter of the manager.  This
+  parameter determines how much the number of nodes can grow during
+  sifting of a variable.  Overall, sifting never increases the size of
+  the decision diagrams.  This parameter only refers to intermediate
+  results.  A lower value will speed up sifting, possibly at the
+  expense of quality.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadMaxGrowth Cudd_SetMaxGrowthAlternate]
+
+******************************************************************************/
+void
+Cudd_SetMaxGrowth(
+  DdManager * dd,
+  double mg)
+{
+    dd->maxGrowth = mg;
+
+} /* end of Cudd_SetMaxGrowth */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads the maxGrowthAlt parameter of the manager.]
+
+  Description [Reads the maxGrowthAlt parameter of the manager.  This
+  parameter is analogous to the maxGrowth paramter, and is used every
+  given number of reorderings instead of maxGrowth.  The number of
+  reorderings is set with Cudd_SetReorderingCycle.  If the number of
+  reorderings is 0 (default) maxGrowthAlt is never used.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadMaxGrowth Cudd_SetMaxGrowthAlternate
+  Cudd_SetReorderingCycle Cudd_ReadReorderingCycle]
+
+******************************************************************************/
+double
+Cudd_ReadMaxGrowthAlternate(
+  DdManager * dd)
+{
+    return(dd->maxGrowthAlt);
+
+} /* end of Cudd_ReadMaxGrowthAlternate */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets the maxGrowthAlt parameter of the manager.]
+
+  Description [Sets the maxGrowthAlt parameter of the manager.  This
+  parameter is analogous to the maxGrowth paramter, and is used every
+  given number of reorderings instead of maxGrowth.  The number of
+  reorderings is set with Cudd_SetReorderingCycle.  If the number of
+  reorderings is 0 (default) maxGrowthAlt is never used.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadMaxGrowthAlternate Cudd_SetMaxGrowth
+  Cudd_SetReorderingCycle Cudd_ReadReorderingCycle]
+
+******************************************************************************/
+void
+Cudd_SetMaxGrowthAlternate(
+  DdManager * dd,
+  double mg)
+{
+    dd->maxGrowthAlt = mg;
+
+} /* end of Cudd_SetMaxGrowthAlternate */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads the reordCycle parameter of the manager.]
+
+  Description [Reads the reordCycle parameter of the manager.  This
+  parameter determines how often the alternate threshold on maximum
+  growth is used in reordering.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadMaxGrowthAlternate Cudd_SetMaxGrowthAlternate
+  Cudd_SetReorderingCycle]
+
+******************************************************************************/
+int
+Cudd_ReadReorderingCycle(
+  DdManager * dd)
+{
+    return(dd->reordCycle);
+
+} /* end of Cudd_ReadReorderingCycle */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets the reordCycle parameter of the manager.]
+
+  Description [Sets the reordCycle parameter of the manager.  This
+  parameter determines how often the alternate threshold on maximum
+  growth is used in reordering.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadMaxGrowthAlternate Cudd_SetMaxGrowthAlternate
+  Cudd_ReadReorderingCycle]
+
+******************************************************************************/
+void
+Cudd_SetReorderingCycle(
+  DdManager * dd,
+  int cycle)
+{
+    dd->reordCycle = cycle;
+
+} /* end of Cudd_SetReorderingCycle */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the variable group tree of the manager.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_SetTree Cudd_FreeTree Cudd_ReadZddTree]
+
+******************************************************************************/
+MtrNode *
+Cudd_ReadTree(
+  DdManager * dd)
+{
+    return(dd->tree);
+
+} /* end of Cudd_ReadTree */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets the variable group tree of the manager.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_FreeTree Cudd_ReadTree Cudd_SetZddTree]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Frees the variable group tree of the manager.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_SetTree Cudd_ReadTree Cudd_FreeZddTree]
+
+******************************************************************************/
+void
+Cudd_FreeTree(
+  DdManager * dd)
+{
+    if (dd->tree != NULL) {
+    Mtr_FreeTree(dd->tree);
+    dd->tree = NULL;
+    }
+    return;
+
+} /* end of Cudd_FreeTree */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the variable group tree of the manager.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_SetZddTree Cudd_FreeZddTree Cudd_ReadTree]
+
+******************************************************************************/
+MtrNode *
+Cudd_ReadZddTree(
+  DdManager * dd)
+{
+    return(dd->treeZ);
+
+} /* end of Cudd_ReadZddTree */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets the ZDD variable group tree of the manager.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_FreeZddTree Cudd_ReadZddTree Cudd_SetTree]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Frees the variable group tree of the manager.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_SetZddTree Cudd_ReadZddTree Cudd_FreeTree]
+
+******************************************************************************/
+void
+Cudd_FreeZddTree(
+  DdManager * dd)
+{
+    if (dd->treeZ != NULL) {
+    Mtr_FreeTree(dd->treeZ);
+    dd->treeZ = NULL;
+    }
+    return;
+
+} /* end of Cudd_FreeZddTree */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the index of the node.]
+
+  Description [Returns the index of the node. The node pointer can be
+  either regular or complemented.]
+
+  SideEffects [None]
+
+  SeeAlso [Cudd_ReadIndex]
+
+******************************************************************************/
+unsigned int
+Cudd_NodeReadIndex(
+  DdNode * node)
+{
+    return((unsigned int) Cudd_Regular(node)->index);
+
+} /* end of Cudd_NodeReadIndex */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the current position of the i-th variable in the
+  order.]
+
+  Description [Returns the current position of the i-th variable in
+  the order. If the index is CUDD_CONST_INDEX, returns
+  CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns
+  -1.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadInvPerm Cudd_ReadPermZdd]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the current position of the i-th ZDD variable in the
+  order.]
+
+  Description [Returns the current position of the i-th ZDD variable
+  in the order. If the index is CUDD_CONST_INDEX, returns
+  CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns
+  -1.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadInvPermZdd 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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the index of the variable currently in the i-th
+  position of the order.]
+
+  Description [Returns the index of the variable currently in the i-th
+  position of the order. If the index is CUDD_CONST_INDEX, returns
+  CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns -1.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadPerm Cudd_ReadInvPermZdd]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the index of the ZDD variable currently in the i-th
+  position of the order.]
+
+  Description [Returns the index of the ZDD variable currently in the
+  i-th position of the order. If the index is CUDD_CONST_INDEX, returns
+  CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns -1.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadPerm Cudd_ReadInvPermZdd]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the i-th element of the vars array.]
+
+  Description [Returns the i-th element of the vars array if it falls
+  within the array bounds; NULL otherwise. If i is the index of an
+  existing variable, this function produces the same result as
+  Cudd_bddIthVar. However, if the i-th var does not exist yet,
+  Cudd_bddIthVar will create it, whereas Cudd_ReadVars will not.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_bddIthVar]
+
+******************************************************************************/
+DdNode *
+Cudd_ReadVars(
+  DdManager * dd,
+  int  i)
+{
+    if (i < 0 || i > dd->size) return(NULL);
+    return(dd->vars[i]);
+
+} /* end of Cudd_ReadVars */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads the epsilon parameter of the manager.]
+
+  Description [Reads the epsilon parameter of the manager. The epsilon
+  parameter control the comparison between floating point numbers.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_SetEpsilon]
+
+******************************************************************************/
+CUDD_VALUE_TYPE
+Cudd_ReadEpsilon(
+  DdManager * dd)
+{
+    return(dd->epsilon);
+
+} /* end of Cudd_ReadEpsilon */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets the epsilon parameter of the manager to ep.]
+
+  Description [Sets the epsilon parameter of the manager to ep. The epsilon
+  parameter control the comparison between floating point numbers.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadEpsilon]
+
+******************************************************************************/
+void
+Cudd_SetEpsilon(
+  DdManager * dd,
+  CUDD_VALUE_TYPE  ep)
+{
+    dd->epsilon = ep;
+
+} /* end of Cudd_SetEpsilon */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads the groupcheck parameter of the manager.]
+
+  Description [Reads the groupcheck parameter of the manager. The
+  groupcheck parameter determines the aggregation criterion in group
+  sifting.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_SetGroupcheck]
+
+******************************************************************************/
+Cudd_AggregationType
+Cudd_ReadGroupcheck(
+  DdManager * dd)
+{
+    return(dd->groupcheck);
+
+} /* end of Cudd_ReadGroupCheck */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets the parameter groupcheck of the manager to gc.]
+
+  Description [Sets the parameter groupcheck of the manager to gc. The
+  groupcheck parameter determines the aggregation criterion in group
+  sifting.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadGroupCheck]
+
+******************************************************************************/
+void
+Cudd_SetGroupcheck(
+  DdManager * dd,
+  Cudd_AggregationType gc)
+{
+    dd->groupcheck = gc;
+
+} /* end of Cudd_SetGroupcheck */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Tells whether garbage collection is enabled.]
+
+  Description [Returns 1 if garbage collection is enabled; 0 otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_EnableGarbageCollection Cudd_DisableGarbageCollection]
+
+******************************************************************************/
+int
+Cudd_GarbageCollectionEnabled(
+  DdManager * dd)
+{
+    return(dd->gcEnabled);
+
+} /* end of Cudd_GarbageCollectionEnabled */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Enables garbage collection.]
+
+  Description [Enables garbage collection. Garbage collection is
+  initially enabled. Therefore it is necessary to call this function
+  only if garbage collection has been explicitly disabled.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_DisableGarbageCollection Cudd_GarbageCollectionEnabled]
+
+******************************************************************************/
+void
+Cudd_EnableGarbageCollection(
+  DdManager * dd)
+{
+    dd->gcEnabled = 1;
+
+} /* end of Cudd_EnableGarbageCollection */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Disables garbage collection.]
+
+  Description [Disables garbage collection. Garbage collection is
+  initially enabled. This function may be called to disable it.
+  However, garbage collection will still occur when a new node must be
+  created and no memory is left, or when garbage collection is required
+  for correctness. (E.g., before reordering.)]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_EnableGarbageCollection Cudd_GarbageCollectionEnabled]
+
+******************************************************************************/
+void
+Cudd_DisableGarbageCollection(
+  DdManager * dd)
+{
+    dd->gcEnabled = 0;
+
+} /* end of Cudd_DisableGarbageCollection */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Tells whether dead nodes are counted towards triggering
+  reordering.]
+
+  Description [Tells whether dead nodes are counted towards triggering
+  reordering. Returns 1 if dead nodes are counted; 0 otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_TurnOnCountDead Cudd_TurnOffCountDead]
+
+******************************************************************************/
+int
+Cudd_DeadAreCounted(
+  DdManager * dd)
+{
+    return(dd->countDead == 0 ? 1 : 0);
+
+} /* end of Cudd_DeadAreCounted */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Causes the dead nodes to be counted towards triggering
+  reordering.]
+
+  Description [Causes the dead nodes to be counted towards triggering
+  reordering. This causes more frequent reorderings. By default dead
+  nodes are not counted.]
+
+  SideEffects [Changes the manager.]
+
+  SeeAlso     [Cudd_TurnOffCountDead Cudd_DeadAreCounted]
+
+******************************************************************************/
+void
+Cudd_TurnOnCountDead(
+  DdManager * dd)
+{
+    dd->countDead = 0;
+
+} /* end of Cudd_TurnOnCountDead */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Causes the dead nodes not to be counted towards triggering
+  reordering.]
+
+  Description [Causes the dead nodes not to be counted towards
+  triggering reordering. This causes less frequent reorderings. By
+  default dead nodes are not counted. Therefore there is no need to
+  call this function unless Cudd_TurnOnCountDead has been previously
+  called.]
+
+  SideEffects [Changes the manager.]
+
+  SeeAlso     [Cudd_TurnOnCountDead Cudd_DeadAreCounted]
+
+******************************************************************************/
+void
+Cudd_TurnOffCountDead(
+  DdManager * dd)
+{
+    dd->countDead = ~0;
+
+} /* end of Cudd_TurnOffCountDead */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the current value of the recombination parameter used
+  in group sifting.]
+
+  Description [Returns the current value of the recombination
+  parameter used in group sifting. A larger (positive) value makes the
+  aggregation of variables due to the second difference criterion more
+  likely. A smaller (negative) value makes aggregation less likely.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_SetRecomb]
+
+******************************************************************************/
+int
+Cudd_ReadRecomb(
+  DdManager * dd)
+{
+    return(dd->recomb);
+
+} /* end of Cudd_ReadRecomb */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets the value of the recombination parameter used in group
+  sifting.]
+
+  Description [Sets the value of the recombination parameter used in
+  group sifting. A larger (positive) value makes the aggregation of
+  variables due to the second difference criterion more likely. A
+  smaller (negative) value makes aggregation less likely. The default
+  value is 0.]
+
+  SideEffects [Changes the manager.]
+
+  SeeAlso     [Cudd_ReadRecomb]
+
+******************************************************************************/
+void
+Cudd_SetRecomb(
+  DdManager * dd,
+  int  recomb)
+{
+    dd->recomb = recomb;
+
+} /* end of Cudd_SetRecomb */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the current value of the symmviolation parameter used
+  in group sifting.]
+
+  Description [Returns the current value of the symmviolation
+  parameter. This parameter is used in group sifting to decide how
+  many violations to the symmetry conditions <code>f10 = f01</code> or
+  <code>f11 = f00</code> are tolerable when checking for aggregation
+  due to extended symmetry. The value should be between 0 and 100. A
+  small value causes fewer variables to be aggregated. The default
+  value is 0.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_SetSymmviolation]
+
+******************************************************************************/
+int
+Cudd_ReadSymmviolation(
+  DdManager * dd)
+{
+    return(dd->symmviolation);
+
+} /* end of Cudd_ReadSymmviolation */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets the value of the symmviolation parameter used
+  in group sifting.]
+
+  Description [Sets the value of the symmviolation
+  parameter. This parameter is used in group sifting to decide how
+  many violations to the symmetry conditions <code>f10 = f01</code> or
+  <code>f11 = f00</code> are tolerable when checking for aggregation
+  due to extended symmetry. The value should be between 0 and 100. A
+  small value causes fewer variables to be aggregated. The default
+  value is 0.]
+
+  SideEffects [Changes the manager.]
+
+  SeeAlso     [Cudd_ReadSymmviolation]
+
+******************************************************************************/
+void
+Cudd_SetSymmviolation(
+  DdManager * dd,
+  int  symmviolation)
+{
+    dd->symmviolation = symmviolation;
+
+} /* end of Cudd_SetSymmviolation */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the current value of the arcviolation parameter used
+  in group sifting.]
+
+  Description [Returns the current value of the arcviolation
+  parameter. This parameter is used in group sifting to decide how
+  many arcs into <code>y</code> not coming from <code>x</code> are
+  tolerable when checking for aggregation due to extended
+  symmetry. The value should be between 0 and 100. A small value
+  causes fewer variables to be aggregated. The default value is 0.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_SetArcviolation]
+
+******************************************************************************/
+int
+Cudd_ReadArcviolation(
+  DdManager * dd)
+{
+    return(dd->arcviolation);
+
+} /* end of Cudd_ReadArcviolation */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets the value of the arcviolation parameter used
+  in group sifting.]
+
+  Description [Sets the value of the arcviolation
+  parameter. This parameter is used in group sifting to decide how
+  many arcs into <code>y</code> not coming from <code>x</code> are
+  tolerable when checking for aggregation due to extended
+  symmetry. The value should be between 0 and 100. A small value
+  causes fewer variables to be aggregated. The default value is 0.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadArcviolation]
+
+******************************************************************************/
+void
+Cudd_SetArcviolation(
+  DdManager * dd,
+  int  arcviolation)
+{
+    dd->arcviolation = arcviolation;
+
+} /* end of Cudd_SetArcviolation */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads the current size of the population used by the
+  genetic algorithm for reordering.]
+
+  Description [Reads the current size of the population used by the
+  genetic algorithm for variable reordering. A larger population size will
+  cause the genetic algorithm to take more time, but will generally
+  produce better results. The default value is 0, in which case the
+  package uses three times the number of variables as population size,
+  with a maximum of 120.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_SetPopulationSize]
+
+******************************************************************************/
+int
+Cudd_ReadPopulationSize(
+  DdManager * dd)
+{
+    return(dd->populationSize);
+
+} /* end of Cudd_ReadPopulationSize */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets the size of the population used by the
+  genetic algorithm for reordering.]
+
+  Description [Sets the size of the population used by the
+  genetic algorithm for variable reordering. A larger population size will
+  cause the genetic algorithm to take more time, but will generally
+  produce better results. The default value is 0, in which case the
+  package uses three times the number of variables as population size,
+  with a maximum of 120.]
+
+  SideEffects [Changes the manager.]
+
+  SeeAlso     [Cudd_ReadPopulationSize]
+
+******************************************************************************/
+void
+Cudd_SetPopulationSize(
+  DdManager * dd,
+  int  populationSize)
+{
+    dd->populationSize = populationSize;
+
+} /* end of Cudd_SetPopulationSize */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads the current number of crossovers used by the
+  genetic algorithm for reordering.]
+
+  Description [Reads the current number of crossovers used by the
+  genetic algorithm for variable reordering. A larger number of crossovers will
+  cause the genetic algorithm to take more time, but will generally
+  produce better results. The default value is 0, in which case the
+  package uses three times the number of variables as number of crossovers,
+  with a maximum of 60.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_SetNumberXovers]
+
+******************************************************************************/
+int
+Cudd_ReadNumberXovers(
+  DdManager * dd)
+{
+    return(dd->numberXovers);
+
+} /* end of Cudd_ReadNumberXovers */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets the number of crossovers used by the
+  genetic algorithm for reordering.]
+
+  Description [Sets the number of crossovers used by the genetic
+  algorithm for variable reordering. A larger number of crossovers
+  will cause the genetic algorithm to take more time, but will
+  generally produce better results. The default value is 0, in which
+  case the package uses three times the number of variables as number
+  of crossovers, with a maximum of 60.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadNumberXovers]
+
+******************************************************************************/
+void
+Cudd_SetNumberXovers(
+  DdManager * dd,
+  int  numberXovers)
+{
+    dd->numberXovers = numberXovers;
+
+} /* end of Cudd_SetNumberXovers */
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the memory in use by the manager measured in bytes.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+long
+Cudd_ReadMemoryInUse(
+  DdManager * dd)
+{
+    return(dd->memused);
+
+} /* end of Cudd_ReadMemoryInUse */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Prints out statistics and settings for a CUDD manager.]
+
+  Description [Prints out statistics and settings for a CUDD manager.
+  Returns 1 if successful; 0 otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+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", 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", 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",
+             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: %ld\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);
+#if 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
+#if 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);
+#if 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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reports the peak number of nodes.]
+
+  Description [Reports the peak number of nodes. This number includes
+  node on the free list. At the peak, the number of nodes on the free
+  list is guaranteed to be less than DD_MEM_CHUNK.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadNodeCount 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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reports the peak number of live nodes.]
+
+  Description [Reports the peak number of live nodes. This count is kept
+  only if CUDD is compiled with DD_STATS defined. If DD_STATS is not
+  defined, this function returns -1.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadNodeCount Cudd_PrintInfo 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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reports the number of nodes in BDDs and ADDs.]
+
+  Description [Reports the number of live nodes in BDDs and ADDs. This
+  number does not include the isolated projection functions and the
+  unused constants. These nodes that are not counted are not part of
+  the DDs manipulated by the application.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadPeakNodeCount Cudd_zddReadNodeCount]
+
+******************************************************************************/
+long
+Cudd_ReadNodeCount(
+  DdManager * dd)
+{
+    long count;
+    int i;
+
+#ifndef DD_NO_DEATH_ROW
+    cuddClearDeathRow(dd);
+#endif
+
+    count = 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 */
+
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reports the number of nodes in ZDDs.]
+
+  Description [Reports the number of nodes in ZDDs. This
+  number always includes the two constants 1 and 0.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadPeakNodeCount Cudd_ReadNodeCount]
+
+******************************************************************************/
+long
+Cudd_zddReadNodeCount(
+  DdManager * dd)
+{
+    return(dd->keysZ - dd->deadZ + 2);
+
+} /* end of Cudd_zddReadNodeCount */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Adds a function to a hook.]
+
+  Description [Adds a function to a hook. A hook is a list of
+  application-provided functions called on certain occasions by the
+  package. Returns 1 if the function is successfully added; 2 if the
+  function was already in the list; 0 otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_RemoveHook]
+
+******************************************************************************/
+int
+Cudd_AddHook(
+  DdManager * dd,
+  int (*f)(DdManager *, char *, void *) ,
+  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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Removes a function from a hook.]
+
+  Description [Removes a function from a hook. A hook is a list of
+  application-provided functions called on certain occasions by the
+  package. Returns 1 if successful; 0 the function was not in the list.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_AddHook]
+
+******************************************************************************/
+int
+Cudd_RemoveHook(
+  DdManager * dd,
+  int (*f)(DdManager *, char *, void *) ,
+  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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Checks whether a function is in a hook.]
+
+  Description [Checks whether a function is in a hook. A hook is a list of
+  application-provided functions called on certain occasions by the
+  package. Returns 1 if the function is found; 0 otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_AddHook Cudd_RemoveHook]
+
+******************************************************************************/
+int
+Cudd_IsInHook(
+  DdManager * dd,
+  int (*f)(DdManager *, char *, void *) ,
+  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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sample hook function to call before reordering.]
+
+  Description [Sample hook function to call before reordering.
+  Prints on the manager's stdout reordering method and initial size.
+  Returns 1 if successful; 0 otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_StdPostReordHook]
+
+******************************************************************************/
+int
+Cudd_StdPreReordHook(
+  DdManager *dd,
+  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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sample hook function to call after reordering.]
+
+  Description [Sample hook function to call after reordering.
+  Prints on the manager's stdout final size and reordering time.
+  Returns 1 if successful; 0 otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_StdPreReordHook]
+
+******************************************************************************/
+int
+Cudd_StdPostReordHook(
+  DdManager *dd,
+  char *str,
+  void *data)
+{
+    long initialTime = (long) data;
+    int retval;
+    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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Enables reporting of reordering stats.]
+
+  Description [Enables reporting of reordering stats.
+  Returns 1 if successful; 0 otherwise.]
+
+  SideEffects [Installs functions in the pre-reordering and post-reordering
+  hooks.]
+
+  SeeAlso     [Cudd_DisableReorderingReporting Cudd_ReorderingReporting]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Disables reporting of reordering stats.]
+
+  Description [Disables reporting of reordering stats.
+  Returns 1 if successful; 0 otherwise.]
+
+  SideEffects [Removes functions from the pre-reordering and post-reordering
+  hooks.]
+
+  SeeAlso     [Cudd_EnableReorderingReporting Cudd_ReorderingReporting]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns 1 if reporting of reordering stats is enabled.]
+
+  Description [Returns 1 if reporting of reordering stats is enabled;
+  0 otherwise.]
+
+  SideEffects [none]
+
+  SeeAlso     [Cudd_EnableReorderingReporting Cudd_DisableReorderingReporting]
+
+******************************************************************************/
+int
+Cudd_ReorderingReporting(
+  DdManager *dd)
+{
+    return(Cudd_IsInHook(dd, Cudd_StdPreReordHook, CUDD_PRE_REORDERING_HOOK));
+
+} /* end of Cudd_ReorderingReporting */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the code of the last error.]
+
+  Description [Returns the code of the last error. The error codes are
+  defined in cudd.h.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ClearErrorCode]
+
+******************************************************************************/
+Cudd_ErrorType
+Cudd_ReadErrorCode(
+  DdManager *dd)
+{
+    return(dd->errorCode);
+
+} /* end of Cudd_ReadErrorCode */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Clear the error code of a manager.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadErrorCode]
+
+******************************************************************************/
+void
+Cudd_ClearErrorCode(
+  DdManager *dd)
+{
+    dd->errorCode = CUDD_NO_ERROR;
+
+} /* end of Cudd_ClearErrorCode */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads the stdout of a manager.]
+
+  Description [Reads the stdout of a manager. This is the file pointer to
+  which messages normally going to stdout are written. It is initialized
+  to stdout. Cudd_SetStdout allows the application to redirect it.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_SetStdout Cudd_ReadStderr]
+
+******************************************************************************/
+FILE *
+Cudd_ReadStdout(
+  DdManager *dd)
+{
+    return(dd->out);
+
+} /* end of Cudd_ReadStdout */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets the stdout of a manager.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadStdout Cudd_SetStderr]
+
+******************************************************************************/
+void
+Cudd_SetStdout(
+  DdManager *dd,
+  FILE *fp)
+{
+    dd->out = fp;
+
+} /* end of Cudd_SetStdout */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads the stderr of a manager.]
+
+  Description [Reads the stderr of a manager. This is the file pointer to
+  which messages normally going to stderr are written. It is initialized
+  to stderr. Cudd_SetStderr allows the application to redirect it.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_SetStderr Cudd_ReadStdout]
+
+******************************************************************************/
+FILE *
+Cudd_ReadStderr(
+  DdManager *dd)
+{
+    return(dd->err);
+
+} /* end of Cudd_ReadStderr */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets the stderr of a manager.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadStderr Cudd_SetStdout]
+
+******************************************************************************/
+void
+Cudd_SetStderr(
+  DdManager *dd,
+  FILE *fp)
+{
+    dd->err = fp;
+
+} /* end of Cudd_SetStderr */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the threshold for the next dynamic reordering.]
+
+  Description [Returns the threshold for the next dynamic reordering.
+  The threshold is in terms of number of nodes and is in effect only
+  if reordering is enabled. The count does not include the dead nodes,
+  unless the countDead parameter of the manager has been changed from
+  its default setting.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_SetNextReordering]
+
+******************************************************************************/
+unsigned int
+Cudd_ReadNextReordering(
+  DdManager *dd)
+{
+    return(dd->nextDyn);
+
+} /* end of Cudd_ReadNextReordering */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets the threshold for the next dynamic reordering.]
+
+  Description [Sets the threshold for the next dynamic reordering.
+  The threshold is in terms of number of nodes and is in effect only
+  if reordering is enabled. The count does not include the dead nodes,
+  unless the countDead parameter of the manager has been changed from
+  its default setting.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_ReadNextReordering]
+
+******************************************************************************/
+void
+Cudd_SetNextReordering(
+  DdManager *dd,
+  unsigned int next)
+{
+    dd->nextDyn = next;
+
+} /* end of Cudd_SetNextReordering */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads the number of elementary reordering steps.]
+
+  Description []
+
+  SideEffects [none]
+
+  SeeAlso     []
+
+******************************************************************************/
+double
+Cudd_ReadSwapSteps(
+  DdManager *dd)
+{
+#ifdef DD_COUNT
+    return(dd->swapSteps);
+#else
+    return(-1);
+#endif
+
+} /* end of Cudd_ReadSwapSteps */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads the maximum allowed number of live nodes.]
+
+  Description [Reads the maximum allowed number of live nodes. When this
+  number is exceeded, the package returns NULL.]
+
+  SideEffects [none]
+
+  SeeAlso     [Cudd_SetMaxLive]
+
+******************************************************************************/
+unsigned int
+Cudd_ReadMaxLive(
+  DdManager *dd)
+{
+    return(dd->maxLive);
+
+} /* end of Cudd_ReadMaxLive */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets the maximum allowed number of live nodes.]
+
+  Description [Sets the maximum allowed number of live nodes. When this
+  number is exceeded, the package returns NULL.]
+
+  SideEffects [none]
+
+  SeeAlso     [Cudd_ReadMaxLive]
+
+******************************************************************************/
+void
+Cudd_SetMaxLive(
+  DdManager *dd,
+  unsigned int maxLive)
+{
+    dd->maxLive = maxLive;
+
+} /* end of Cudd_SetMaxLive */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads the maximum allowed memory.]
+
+  Description [Reads the maximum allowed memory. When this
+  number is exceeded, the package returns NULL.]
+
+  SideEffects [none]
+
+  SeeAlso     [Cudd_SetMaxMemory]
+
+******************************************************************************/
+long
+Cudd_ReadMaxMemory(
+  DdManager *dd)
+{
+    return(dd->maxmemhard);
+
+} /* end of Cudd_ReadMaxMemory */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets the maximum allowed memory.]
+
+  Description [Sets the maximum allowed memory. When this
+  number is exceeded, the package returns NULL.]
+
+  SideEffects [none]
+
+  SeeAlso     [Cudd_ReadMaxMemory]
+
+******************************************************************************/
+void
+Cudd_SetMaxMemory(
+  DdManager *dd,
+  long maxMemory)
+{
+    dd->maxmemhard = maxMemory;
+
+} /* end of Cudd_SetMaxMemory */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Prevents sifting of a variable.]
+
+  Description [This function sets a flag to prevent sifting of a
+  variable.  Returns 1 if successful; 0 otherwise (i.e., invalid
+  variable index).]
+
+  SideEffects [Changes the "bindVar" flag in DdSubtable.]
+
+  SeeAlso     [Cudd_bddUnbindVar]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Allows the sifting of a variable.]
+
+  Description [This function resets the flag that prevents the sifting
+  of a variable. In successive variable reorderings, the variable will
+  NOT be skipped, that is, sifted.  Initially all variables can be
+  sifted. It is necessary to call this function only to re-enable
+  sifting after a call to Cudd_bddBindVar. Returns 1 if successful; 0
+  otherwise (i.e., invalid variable index).]
+
+  SideEffects [Changes the "bindVar" flag in DdSubtable.]
+
+  SeeAlso     [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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Tells whether a variable can be sifted.]
+
+  Description [This function returns 1 if a variable is enabled for
+  sifting.  Initially all variables can be sifted. This function returns
+  0 only if there has been a previous call to Cudd_bddBindVar for that
+  variable not followed by a call to Cudd_bddUnbindVar. The function returns
+  0 also in the case in which the index of the variable is out of bounds.]
+
+  SideEffects [none]
+
+  SeeAlso     [Cudd_bddBindVar 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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets a variable type to primary input.]
+
+  Description [Sets a variable type to primary input.  The variable type is
+  used by lazy sifting.  Returns 1 if successful; 0 otherwise.]
+
+  SideEffects [modifies the manager]
+
+  SeeAlso     [Cudd_bddSetPsVar Cudd_bddSetNsVar Cudd_bddIsPiVar]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets a variable type to present state.]
+
+  Description [Sets a variable type to present state.  The variable type is
+  used by lazy sifting.  Returns 1 if successful; 0 otherwise.]
+
+  SideEffects [modifies the manager]
+
+  SeeAlso     [Cudd_bddSetPiVar Cudd_bddSetNsVar Cudd_bddIsPsVar]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets a variable type to next state.]
+
+  Description [Sets a variable type to next state.  The variable type is
+  used by lazy sifting.  Returns 1 if successful; 0 otherwise.]
+
+  SideEffects [modifies the manager]
+
+  SeeAlso     [Cudd_bddSetPiVar Cudd_bddSetPsVar Cudd_bddIsNsVar]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Checks whether a variable is primary input.]
+
+  Description [Checks whether a variable is primary input.  Returns 1 if
+  the variable's type is primary input; 0 if the variable exists but is
+  not a primary input; -1 if the variable does not exist.]
+
+  SideEffects [none]
+
+  SeeAlso     [Cudd_bddSetPiVar Cudd_bddIsPsVar Cudd_bddIsNsVar]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Checks whether a variable is present state.]
+
+  Description [Checks whether a variable is present state.  Returns 1 if
+  the variable's type is present state; 0 if the variable exists but is
+  not a present state; -1 if the variable does not exist.]
+
+  SideEffects [none]
+
+  SeeAlso     [Cudd_bddSetPsVar Cudd_bddIsPiVar Cudd_bddIsNsVar]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Checks whether a variable is next state.]
+
+  Description [Checks whether a variable is next state.  Returns 1 if
+  the variable's type is present state; 0 if the variable exists but is
+  not a present state; -1 if the variable does not exist.]
+
+  SideEffects [none]
+
+  SeeAlso     [Cudd_bddSetNsVar Cudd_bddIsPiVar 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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets a corresponding pair index for a given index.]
+
+  Description [Sets a corresponding pair index for a given index.
+  These pair indices are present and next state variable.  Returns 1 if
+  successful; 0 otherwise.]
+
+  SideEffects [modifies the manager]
+
+  SeeAlso     [Cudd_bddReadPairIndex]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads a corresponding pair index for a given index.]
+
+  Description [Reads a corresponding pair index for a given index.
+  These pair indices are present and next state variable.  Returns the
+  corresponding variable index if the variable exists; -1 otherwise.]
+
+  SideEffects [modifies the manager]
+
+  SeeAlso     [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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets a variable to be grouped.]
+
+  Description [Sets a variable to be grouped. This function is used for
+  lazy sifting.  Returns 1 if successful; 0 otherwise.]
+
+  SideEffects [modifies the manager]
+
+  SeeAlso     [Cudd_bddSetVarHardGroup Cudd_bddResetVarToBeGrouped]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets a variable to be a hard group.]
+
+  Description [Sets a variable to be a hard group.  This function is used
+  for lazy sifting.  Returns 1 if successful; 0 otherwise.]
+
+  SideEffects [modifies the manager]
+
+  SeeAlso     [Cudd_bddSetVarToBeGrouped Cudd_bddResetVarToBeGrouped
+  Cudd_bddIsVarHardGroup]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Resets a variable not to be grouped.]
+
+  Description [Resets a variable not to be grouped.  This function is
+  used for lazy sifting.  Returns 1 if successful; 0 otherwise.]
+
+  SideEffects [modifies the manager]
+
+  SeeAlso     [Cudd_bddSetVarToBeGrouped Cudd_bddSetVarHardGroup]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Checks whether a variable is set to be grouped.]
+
+  Description [Checks whether a variable is set to be grouped. This
+  function is used for lazy sifting.]
+
+  SideEffects [none]
+
+  SeeAlso     []
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Sets a variable to be ungrouped.]
+
+  Description [Sets a variable to be ungrouped. This function is used
+  for lazy sifting.  Returns 1 if successful; 0 otherwise.]
+
+  SideEffects [modifies the manager]
+
+  SeeAlso     [Cudd_bddIsVarToBeUngrouped]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Checks whether a variable is set to be ungrouped.]
+
+  Description [Checks whether a variable is set to be ungrouped. This
+  function is used for lazy sifting.  Returns 1 if the variable is marked
+  to be ungrouped; 0 if the variable exists, but it is not marked to be
+  ungrouped; -1 if the variable does not exist.]
+
+  SideEffects [none]
+
+  SeeAlso     [Cudd_bddSetVarToBeUngrouped]
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Checks whether a variable is set to be in a hard group.]
+
+  Description [Checks whether a variable is set to be in a hard group.  This
+  function is used for lazy sifting.  Returns 1 if the variable is marked
+  to be in a hard group; 0 if the variable exists, but it is not marked to be
+  in a hard group; -1 if the variable does not exist.]
+
+  SideEffects [none]
+
+  SeeAlso     [Cudd_bddSetVarHardGroup]
+
+******************************************************************************/
+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                                            */
+/*---------------------------------------------------------------------------*/
+
+
+/**Function********************************************************************
+
+  Synopsis    [Fixes a variable group tree.]
+
+  Description []
+
+  SideEffects [Changes the variable group tree.]
+
+  SeeAlso     []
+
+******************************************************************************/
+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 */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Adds multiplicity groups to a ZDD variable group tree.]
+
+  Description [Adds multiplicity groups to a ZDD variable group tree.
+  Returns 1 if successful; 0 otherwise. This function creates the groups
+  for set of ZDD variables (whose cardinality is given by parameter
+  multiplicity) that are created for each BDD variable in
+  Cudd_zddVarsFromBddVars. The crux of the matter is to determine the index
+  each new group. (The index of the first variable in the group.)
+  We first build all the groups for the children of a node, and then deal
+  with the ZDD variables that are directly attached to the node. The problem
+  for these is that the tree itself does not provide information on their
+  position inside the group. While we deal with the children of the node,
+  therefore, we keep track of all the positions they occupy. The remaining
+  positions in the tree can be freely used. Also, we keep track of all the
+  variables placed in the children. All the remaining variables are directly
+  attached to the group. We can then place any pair of variables not yet
+  grouped in any pair of available positions in the node.]
+
+  SideEffects [Changes the variable group tree.]
+
+  SeeAlso     [Cudd_zddVarsFromBddVars]
+
+******************************************************************************/
+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 */
+