cuddapi.c

主要进行大规模的电路综合

/**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.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