cuddgencof.c

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

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

  FileName    [cuddGenCof.c]

  PackageName [cudd]

  Synopsis    [Generalized cofactors for BDDs and ADDs.]

  Description [External procedures included in this module:
		<ul>
		<li> Cudd_bddConstrain()
		<li> Cudd_bddRestrict()
		<li> Cudd_addConstrain()
		<li> Cudd_bddConstrainDecomp()
		<li> Cudd_addRestrict()
		<li> Cudd_bddCharToVect()
		<li> Cudd_bddLICompaction()
		<li> Cudd_bddSqueeze()
		<li> Cudd_SubsetCompress()
		<li> Cudd_SupersetCompress()
		</ul>
	    Internal procedures included in this module:
		<ul>
		<li> cuddBddConstrainRecur()
		<li> cuddBddRestrictRecur()
		<li> cuddAddConstrainRecur()
		<li> cuddAddRestrictRecur()
		<li> cuddBddLICompaction()
		</ul>
	    Static procedures included in this module:
	        <ul>
		<li> cuddBddConstrainDecomp()
		<li> cuddBddCharToVect()
		<li> cuddBddLICMarkEdges()
		<li> cuddBddLICBuildResult()
		<li> cuddBddSqueeze()
		</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                                                     */
/*---------------------------------------------------------------------------*/

/* Codes for edge markings in Cudd_bddLICompaction.  The codes are defined
** so that they can be bitwise ORed to implement the code priority scheme.
*/
#define DD_LIC_DC 0
#define DD_LIC_1  1
#define DD_LIC_0  2
#define DD_LIC_NL 3

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


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

/* Key for the cache used in the edge marking phase. */
typedef struct MarkCacheKey {
    DdNode *f;
    DdNode *c;
} MarkCacheKey;

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

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddGenCof.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $";
#endif

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


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

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

static int cuddBddConstrainDecomp ARGS((DdManager *dd, DdNode *f, DdNode **decomp));
static DdNode * cuddBddCharToVect ARGS((DdManager *dd, DdNode *f, DdNode *x));
static int cuddBddLICMarkEdges ARGS((DdManager *dd, DdNode *f, DdNode *c, st_table *table, st_table *cache));
static DdNode * cuddBddLICBuildResult ARGS((DdManager *dd, DdNode *f, st_table *cache, st_table *table));
static int MarkCacheHash ARGS((char *ptr, int modulus));
static int MarkCacheCompare ARGS((const char *ptr1, const char *ptr2));
static enum st_retval MarkCacheCleanUp ARGS((char *key, char *value, char *arg));
static DdNode * cuddBddSqueeze ARGS((DdManager *dd, DdNode *l, DdNode *u));

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


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


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

  Synopsis    [Computes f constrain c.]

  Description [Computes f constrain c (f @ c).
  Uses a canonical form: (f' @ c) = ( f @ c)'.  (Note: this is not true
  for c.)  List of special cases:
    <ul>
    <li> f @ 0 = 0
    <li> f @ 1 = f
    <li> 0 @ c = 0
    <li> 1 @ c = 1
    <li> f @ f = 1
    <li> f @ f'= 0
    </ul>
  Returns a pointer to the result if successful; NULL otherwise. Note that if
  F=(f1,...,fn) and reordering takes place while computing F @ c, then the
  image restriction property (Img(F,c) = Img(F @ c)) is lost.]

  SideEffects [None]

  SeeAlso     [Cudd_bddRestrict Cudd_addConstrain]

******************************************************************************/
DdNode *
Cudd_bddConstrain(
  DdManager * dd,
  DdNode * f,
  DdNode * c)
{
    DdNode *res;

    do {
	dd->reordered = 0;
	res = cuddBddConstrainRecur(dd,f,c);
    } while (dd->reordered == 1);
    return(res);

} /* end of Cudd_bddConstrain */


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

  Synopsis [BDD restrict according to Coudert and Madre's algorithm
  (ICCAD90).]

  Description [BDD restrict according to Coudert and Madre's algorithm
  (ICCAD90). Returns the restricted BDD if successful; otherwise NULL.
  If application of restrict results in a BDD larger than the input
  BDD, the input BDD is returned.]

  SideEffects [None]

  SeeAlso     [Cudd_bddConstrain Cudd_addRestrict]

******************************************************************************/
DdNode *
Cudd_bddRestrict(
  DdManager * dd,
  DdNode * f,
  DdNode * c)
{
    DdNode *suppF, *suppC, *commonSupport;
    DdNode *cplus, *res;
    int retval;
    int sizeF, sizeRes;

    /* Check terminal cases here to avoid computing supports in trivial cases.
    ** This also allows us notto check later for the case c == 0, in which
    ** there is no common support. */
    if (c == Cudd_Not(DD_ONE(dd))) return(Cudd_Not(DD_ONE(dd)));
    if (Cudd_IsConstant(f)) return(f);
    if (f == c) return(DD_ONE(dd));
    if (f == Cudd_Not(c)) return(Cudd_Not(DD_ONE(dd)));

    /* Check if supports intersect. */
    retval = Cudd_ClassifySupport(dd,f,c,&commonSupport,&suppF,&suppC);
    if (retval == 0) {
	return(NULL);
    }
    cuddRef(commonSupport); cuddRef(suppF); cuddRef(suppC);
    Cudd_IterDerefBdd(dd,suppF);

    if (commonSupport == DD_ONE(dd)) {
	Cudd_IterDerefBdd(dd,commonSupport);
	Cudd_IterDerefBdd(dd,suppC);
	return(f);
    }
    Cudd_IterDerefBdd(dd,commonSupport);

    /* Abstract from c the variables that do not appear in f. */
    cplus = Cudd_bddExistAbstract(dd, c, suppC);
    if (cplus == NULL) {
	Cudd_IterDerefBdd(dd,suppC);
	return(NULL);
    }
    cuddRef(cplus);
    Cudd_IterDerefBdd(dd,suppC);

    do {
	dd->reordered = 0;
	res = cuddBddRestrictRecur(dd, f, cplus);
    } while (dd->reordered == 1);
    if (res == NULL) {
	Cudd_IterDerefBdd(dd,cplus);
	return(NULL);
    }
    cuddRef(res);
    Cudd_IterDerefBdd(dd,cplus);
    /* Make restric safe by returning the smaller of the input and the
    ** result. */
    sizeF = Cudd_DagSize(f);
    sizeRes = Cudd_DagSize(res);
    if (sizeF <= sizeRes) {
	Cudd_IterDerefBdd(dd, res);
	return(f);
    } else {
	cuddDeref(res);
	return(res);
    }

} /* end of Cudd_bddRestrict */


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

  Synopsis    [Computes f constrain c for ADDs.]

  Description [Computes f constrain c (f @ c), for f an ADD and c a 0-1
  ADD.  List of special cases:
    <ul>
    <li> F @ 0 = 0
    <li> F @ 1 = F
    <li> 0 @ c = 0
    <li> 1 @ c = 1
    <li> F @ F = 1
    </ul>
  Returns a pointer to the result if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddConstrain]

******************************************************************************/
DdNode *
Cudd_addConstrain(
  DdManager * dd,
  DdNode * f,
  DdNode * c)
{
    DdNode *res;

    do {
	dd->reordered = 0;
	res = cuddAddConstrainRecur(dd,f,c);
    } while (dd->reordered == 1);
    return(res);

} /* end of Cudd_addConstrain */


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

  Synopsis [BDD conjunctive decomposition as in McMillan's CAV96 paper.]

  Description [BDD conjunctive decomposition as in McMillan's CAV96
  paper.  The decomposition is canonical only for a given variable
  order. If canonicity is required, variable ordering must be disabled
  after the decomposition has been computed. Returns an array with one
  entry for each BDD variable in the manager if successful; otherwise
  NULL. The components of the solution have their reference counts
  already incremented (unlike the results of most other functions in
  the package.]

  SideEffects [None]

  SeeAlso     [Cudd_bddConstrain Cudd_bddExistAbstract]

******************************************************************************/
DdNode **
Cudd_bddConstrainDecomp(
  DdManager * dd,
  DdNode * f)
{
    DdNode **decomp;
    int res;
    int i;

    /* Create an initialize decomposition array. */
    decomp = ALLOC(DdNode *,dd->size);
    if (decomp == NULL) {
	dd->errorCode = CUDD_MEMORY_OUT;
	return(NULL);
    }
    for (i = 0; i < dd->size; i++) {
	decomp[i] = NULL;
    }
    do {
	dd->reordered = 0;
	/* Clean up the decomposition array in case reordering took place. */
	for (i = 0; i < dd->size; i++) {
	    if (decomp[i] != NULL) {
		Cudd_IterDerefBdd(dd, decomp[i]);
		decomp[i] = NULL;
	    }
	}
	res = cuddBddConstrainDecomp(dd,f,decomp);
    } while (dd->reordered == 1);
    if (res == 0) {
	FREE(decomp);
	return(NULL);
    }
    /* Missing components are constant ones. */
    for (i = 0; i < dd->size; i++) {
	if (decomp[i] == NULL) {
	    decomp[i] = DD_ONE(dd);
	    cuddRef(decomp[i]);
	}
    }
    return(decomp);

} /* end of Cudd_bddConstrainDecomp */


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

  Synopsis [ADD restrict according to Coudert and Madre's algorithm
  (ICCAD90).]

  Description [ADD restrict according to Coudert and Madre's algorithm
  (ICCAD90). Returns the restricted ADD if successful; otherwise NULL.
  If application of restrict results in an ADD larger than the input
  ADD, the input ADD is returned.]

  SideEffects [None]

  SeeAlso     [Cudd_addConstrain Cudd_bddRestrict]

******************************************************************************/
DdNode *
Cudd_addRestrict(
  DdManager * dd,
  DdNode * f,
  DdNode * c)
{
    DdNode *supp_f, *supp_c;
    DdNode *res, *commonSupport;
    int intersection;
    int sizeF, sizeRes;

    /* Check if supports intersect. */
    supp_f = Cudd_Support(dd, f);
    if (supp_f == NULL) {
	return(NULL);
    }
    cuddRef(supp_f);
    supp_c = Cudd_Support(dd, c);
    if (supp_c == NULL) {
	Cudd_RecursiveDeref(dd,supp_f);
	return(NULL);
    }
    cuddRef(supp_c);
    commonSupport = Cudd_bddLiteralSetIntersection(dd, supp_f, supp_c);
    if (commonSupport == NULL) {
	Cudd_RecursiveDeref(dd,supp_f);
	Cudd_RecursiveDeref(dd,supp_c);
	return(NULL);
    }
    cuddRef(commonSupport);
    Cudd_RecursiveDeref(dd,supp_f);
    Cudd_RecursiveDeref(dd,supp_c);
    intersection = commonSupport != DD_ONE(dd);
    Cudd_RecursiveDeref(dd,commonSupport);

    if (intersection) {
	do {
	    dd->reordered = 0;
	    res = cuddAddRestrictRecur(dd, f, c);
	} while (dd->reordered == 1);
	sizeF = Cudd_DagSize(f);
	sizeRes = Cudd_DagSize(res);
	if (sizeF <= sizeRes) {
	    cuddRef(res);
	    Cudd_RecursiveDeref(dd, res);
	    return(f);
	} else {
	    return(res);
	}
    } else {
	return(f);
    }

} /* end of Cudd_addRestrict */


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

  Synopsis    [Computes a vector whose image equals a non-zero function.]

  Description [Computes a vector of BDDs whose image equals a non-zero
  function.
  The result depends on the variable order. The i-th component of the vector
  depends only on the first i variables in the order.  Each BDD in the vector
  is not larger than the BDD of the given characteristic function.  This
  function is based on the description of char-to-vect in "Verification of
  Sequential Machines Using Boolean Functional Vectors" by O. Coudert, C.
  Berthet and J. C. Madre.
  Returns a pointer to an array containing the result if successful; NULL
  otherwise. The size of the array equals the number of variables in the
  manager. The components of the solution have their reference counts 
  already incremented (unlike the results of most other functions in 
  the package.]

  SideEffects [None]

  SeeAlso     [Cudd_bddConstrain]

******************************************************************************/
DdNode **
Cudd_bddCharToVect(
  DdManager * dd,
  DdNode * f)
{
    int i, j;
    DdNode **vect;
    DdNode *res = NULL;

    if (f == Cudd_Not(DD_ONE(dd))) return(NULL);

    vect = ALLOC(DdNode *, dd->size);
    if (vect == NULL) {
	dd->errorCode = CUDD_MEMORY_OUT;
	return(NULL);
    }

    do {
	dd->reordered = 0;
	for (i = 0; i < dd->size; i++) {
	    res = cuddBddCharToVect(dd,f,dd->vars[dd->invperm[i]]);
	    if (res == NULL) {
		/* Clean up the vector array in case reordering took place. */
		for (j = 0; j < i; j++) {
		    Cudd_IterDerefBdd(dd, vect[dd->invperm[j]]);
		}
		break;
	    }
	    cuddRef(res);
	    vect[dd->invperm[i]] = res;
	}
    } while (dd->reordered == 1);
    if (res == NULL) {
	FREE(vect);
	return(NULL);
    }
    return(vect);

} /* end of Cudd_bddCharToVect */


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

  Synopsis    [Performs safe minimization of a BDD.]

  Description [Performs safe minimization of a BDD. Given the BDD
  <code>f</code> of a function to be minimized and a BDD
  <code>c</code> representing the care set, Cudd_bddLICompaction
  produces the BDD of a function that agrees with <code>f</code>
  wherever <code>c</code> is 1.  Safe minimization means that the size
  of the result is guaranteed not to exceed the size of
  <code>f</code>. This function is based on the DAC97 paper by Hong et
  al..  Returns a pointer to the result if successful; NULL
  otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddRestrict]

******************************************************************************/