cuddbddabs.c

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

/**CFile***********************************************************************

  FileName    [cuddBddAbs.c]

  PackageName [cudd]

  Synopsis    [Quantification functions for BDDs.]

  Description [External procedures included in this module:
		<ul>
		<li> Cudd_bddExistAbstract()
		<li> Cudd_bddXorExistAbstract()
		<li> Cudd_bddUnivAbstract()
		<li> Cudd_bddBooleanDiff()
		<li> Cudd_bddVarIsDependent()
		</ul>
	Internal procedures included in this module:
		<ul>
		<li> cuddBddExistAbstractRecur()
		<li> cuddBddXorExistAbstractRecur()
		<li> cuddBddBooleanDiffRecur()
		</ul>
	Static procedures included in this module:
		<ul>
		<li> bddCheckPositiveCube()
		</ul>
		]

  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: cuddBddAbs.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $";
#endif

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


/**AutomaticStart*************************************************************/

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

static int bddCheckPositiveCube ARGS((DdManager *manager, DdNode *cube));

/**AutomaticEnd***************************************************************/


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


/**Function********************************************************************

  Synopsis [Existentially abstracts all the variables in cube from f.]

  Description [Existentially abstracts all the variables in cube from f.
  Returns the abstracted BDD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddUnivAbstract Cudd_addExistAbstract]

******************************************************************************/
DdNode *
Cudd_bddExistAbstract(
  DdManager * manager,
  DdNode * f,
  DdNode * cube)
{
    DdNode *res;

    if (bddCheckPositiveCube(manager, cube) == 0) {
        (void) fprintf(manager->err,
		       "Error: Can only abstract positive cubes\n");
	manager->errorCode = CUDD_INVALID_ARG;
        return(NULL);
    }

    do {
	manager->reordered = 0;
	res = cuddBddExistAbstractRecur(manager, f, cube);
    } while (manager->reordered == 1);

    return(res);

} /* end of Cudd_bddExistAbstract */


/**Function********************************************************************

  Synopsis [Takes the exclusive OR of two BDDs and simultaneously abstracts the
  variables in cube.]

  Description [Takes the exclusive OR of two BDDs and simultaneously abstracts
  the variables in cube. The variables are existentially abstracted.  Returns a
  pointer to the result is successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddUnivAbstract Cudd_bddExistAbstract Cudd_bddAndAbstract]

******************************************************************************/
DdNode *
Cudd_bddXorExistAbstract(
  DdManager * manager,
  DdNode * f,
  DdNode * g,
  DdNode * cube)
{
    DdNode *res;

    if (bddCheckPositiveCube(manager, cube) == 0) {
        (void) fprintf(manager->err,
		       "Error: Can only abstract positive cubes\n");
	manager->errorCode = CUDD_INVALID_ARG;
        return(NULL);
    }

    do {
	manager->reordered = 0;
	res = cuddBddXorExistAbstractRecur(manager, f, g, cube);
    } while (manager->reordered == 1);

    return(res);

} /* end of Cudd_bddXorExistAbstract */


/**Function********************************************************************

  Synopsis    [Universally abstracts all the variables in cube from f.]

  Description [Universally abstracts all the variables in cube from f.
  Returns the abstracted BDD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddExistAbstract Cudd_addUnivAbstract]

******************************************************************************/
DdNode *
Cudd_bddUnivAbstract(
  DdManager * manager,
  DdNode * f,
  DdNode * cube)
{
    DdNode	*res;

    if (bddCheckPositiveCube(manager, cube) == 0) {
	(void) fprintf(manager->err,
		       "Error: Can only abstract positive cubes\n");
	manager->errorCode = CUDD_INVALID_ARG;
	return(NULL);
    }

    do {
	manager->reordered = 0;
	res = cuddBddExistAbstractRecur(manager, Cudd_Not(f), cube);
    } while (manager->reordered == 1);
    if (res != NULL) res = Cudd_Not(res);

    return(res);

} /* end of Cudd_bddUnivAbstract */


/**Function********************************************************************

  Synopsis    [Computes the boolean difference of f with respect to x.]

  Description [Computes the boolean difference of f with respect to the
  variable with index x.  Returns the BDD of the boolean difference if
  successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode *
Cudd_bddBooleanDiff(
  DdManager * manager,
  DdNode * f,
  int  x)
{
    DdNode *res, *var;

    /* If the variable is not currently in the manager, f cannot
    ** depend on it.
    */
    if (x >= manager->size) return(Cudd_Not(DD_ONE(manager)));
    var = manager->vars[x];

    do {
	manager->reordered = 0;
	res = cuddBddBooleanDiffRecur(manager, Cudd_Regular(f), var);
    } while (manager->reordered == 1);

    return(res);

} /* end of Cudd_bddBooleanDiff */


/**Function********************************************************************

  Synopsis    [Checks whether a variable is dependent on others in a
  function.]

  Description [Checks whether a variable is dependent on others in a
  function.  Returns 1 if the variable is dependent; 0 otherwise. No
  new nodes are created.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
int
Cudd_bddVarIsDependent(
  DdManager *dd,		/* manager */
  DdNode *f,			/* function */
  DdNode *var			/* variable */)
{
    DdNode *F, *res, *zero, *ft, *fe;
    unsigned topf, level;
    DdNode *(*cacheOp)(DdManager *, DdNode *, DdNode *);
    int retval;

    zero = Cudd_Not(DD_ONE(dd));
    if (Cudd_IsConstant(f)) return(f == zero);

    /* From now on f is not constant. */
    F = Cudd_Regular(f);
    topf = (unsigned) dd->perm[F->index];
    level = (unsigned) dd->perm[var->index];

    /* Check terminal case. If topf > index of var, f does not depend on var.
    ** Therefore, var is not dependent in f. */
    if (topf > level) {
	return(0);
    }

    cacheOp =
	(DdNode *(*)(DdManager *, DdNode *, DdNode *)) Cudd_bddVarIsDependent;
    res = cuddCacheLookup2(dd,cacheOp,f,var);
    if (res != NULL) {
	return(res != zero);
    }

    /* Compute cofactors. */
    ft = Cudd_NotCond(cuddT(F), f != F);
    fe = Cudd_NotCond(cuddE(F), f != F);

    if (topf == level) {
	retval = Cudd_bddLeq(dd,ft,Cudd_Not(fe));
    } else {
	retval = Cudd_bddVarIsDependent(dd,ft,var) &&
	    Cudd_bddVarIsDependent(dd,fe,var);
    }

    cuddCacheInsert2(dd,cacheOp,f,var,Cudd_NotCond(zero,retval));

    return(retval);

} /* Cudd_bddVarIsDependent */


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


/**Function********************************************************************

  Synopsis    [Performs the recursive steps of Cudd_bddExistAbstract.]

  Description [Performs the recursive steps of Cudd_bddExistAbstract.
  Returns the BDD obtained by abstracting the variables
  of cube from f if successful; NULL otherwise. It is also used by
  Cudd_bddUnivAbstract.]

  SideEffects [None]

  SeeAlso     [Cudd_bddExistAbstract Cudd_bddUnivAbstract]

******************************************************************************/
DdNode *
cuddBddExistAbstractRecur(
  DdManager * manager,
  DdNode * f,
  DdNode * cube)
{
    DdNode	*F, *T, *E, *res, *res1, *res2, *one;

    statLine(manager);
    one = DD_ONE(manager);
    F = Cudd_Regular(f);

    /* Cube is guaranteed to be a cube at this point. */	
    if (cube == one || F == one) {  
        return(f);
    }
    /* From now on, f and cube are non-constant. */

    /* Abstract a variable that does not appear in f. */
    while (manager->perm[F->index] > manager->perm[cube->index]) {
	cube = cuddT(cube);
	if (cube == one) return(f);
    }

    /* Check the cache. */