cudddecomp.c

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

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

  FileName    [cuddDecomp.c]

  PackageName [cudd]

  Synopsis    [Functions for BDD decomposition.]

  Description [External procedures included in this file:
		<ul>
		<li> Cudd_bddApproxConjDecomp()
		<li> Cudd_bddApproxDisjDecomp()
		<li> Cudd_bddIterConjDecomp()
		<li> Cudd_bddIterDisjDecomp()
		<li> Cudd_bddGenConjDecomp()
		<li> Cudd_bddGenDisjDecomp()
		<li> Cudd_bddVarConjDecomp()
		<li> Cudd_bddVarDisjDecomp()
		</ul>
	Static procedures included in this module:
		<ul>
		<li> cuddConjunctsAux()
		<li> CreateBotDist()
		<li> BuildConjuncts()
		<li> ConjunctsFree()
		</ul>]

  Author      [Kavita Ravi, 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                                                     */
/*---------------------------------------------------------------------------*/
#define DEPTH 5
#define THRESHOLD 10
#define NONE 0
#define PAIR_ST 1
#define PAIR_CR 2
#define G_ST 3
#define G_CR 4
#define H_ST 5
#define H_CR 6
#define BOTH_G 7
#define BOTH_H 8

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

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/
typedef struct Conjuncts {
    DdNode *g;
    DdNode *h;
} Conjuncts;

typedef struct  NodeStat {
    int distance;
    int localRef;
} NodeStat;


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

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

static	DdNode	*one, *zero;
long lastTimeG;

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


#define FactorsNotStored(factors)  ((int)((long)(factors) & 01))

#define FactorsComplement(factors) ((Conjuncts *)((long)(factors) | 01))

#define FactorsUncomplement(factors) ((Conjuncts *)((long)(factors) ^ 01))

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

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

static NodeStat * CreateBotDist ARGS((DdNode * node, st_table * distanceTable));
static double CountMinterms ARGS((DdNode * node, double max, st_table * mintermTable, FILE *fp));
static void ConjunctsFree ARGS((DdManager * dd, Conjuncts * factors));
static int PairInTables ARGS((DdNode * g, DdNode * h, st_table * ghTable));
static Conjuncts * CheckTablesCacheAndReturn ARGS((DdNode * node, DdNode * g, DdNode * h, st_table * ghTable, st_table * cacheTable));
static Conjuncts * PickOnePair ARGS((DdNode * node, DdNode * g1, DdNode * h1, DdNode * g2, DdNode * h2, st_table * ghTable, st_table * cacheTable));
static Conjuncts * CheckInTables ARGS((DdNode * node, DdNode * g1, DdNode * h1, DdNode * g2, DdNode * h2, st_table * ghTable, st_table * cacheTable, int * outOfMem));
static Conjuncts * ZeroCase ARGS((DdManager * dd, DdNode * node, Conjuncts * factorsNv, st_table * ghTable, st_table * cacheTable, int switched));
static Conjuncts * BuildConjuncts ARGS((DdManager * dd, DdNode * node, st_table * distanceTable, st_table * cacheTable, int approxDistance, int maxLocalRef, st_table * ghTable, st_table * mintermTable));
static int cuddConjunctsAux ARGS((DdManager * dd, DdNode * f, DdNode ** c1, DdNode ** c2));

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


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


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

  Synopsis    [Performs two-way conjunctive decomposition of a BDD.]

  Description [Performs two-way conjunctive decomposition of a
  BDD. This procedure owes its name to the use of supersetting to
  obtain an initial factor of the given function. Returns the number
  of conjuncts produced, that is, 2 if successful; 1 if no meaningful
  decomposition was found; 0 otherwise. The conjuncts produced by this
  procedure tend to be imbalanced.]

  SideEffects [The factors are returned in an array as side effects.
  The array is allocated by this function. It is the caller's responsibility
  to free it. On successful completion, the conjuncts are already
  referenced. If the function returns 0, the array for the conjuncts is
  not allocated. If the function returns 1, the only factor equals the
  function to be decomposed.]

  SeeAlso     [Cudd_bddApproxDisjDecomp Cudd_bddIterConjDecomp
  Cudd_bddGenConjDecomp Cudd_bddVarConjDecomp Cudd_RemapOverApprox
  Cudd_bddSqueeze Cudd_bddLICompaction]

******************************************************************************/
int
Cudd_bddApproxConjDecomp(
  DdManager * dd /* manager */,
  DdNode * f /* function to be decomposed */,
  DdNode *** conjuncts /* address of the first factor */)
{
    DdNode *superset1, *superset2, *glocal, *hlocal;
    int nvars = Cudd_SupportSize(dd,f);

    /* Find a tentative first factor by overapproximation and minimization. */
    superset1 = Cudd_RemapOverApprox(dd,f,nvars,0,1.0);
    if (superset1 == NULL) return(0);
    cuddRef(superset1);
    superset2 = Cudd_bddSqueeze(dd,f,superset1);
    if (superset2 == NULL) {
	Cudd_RecursiveDeref(dd,superset1);
	return(0);
    }
    cuddRef(superset2);
    Cudd_RecursiveDeref(dd,superset1);

    /* Compute the second factor by minimization. */
    hlocal = Cudd_bddLICompaction(dd,f,superset2);
    if (hlocal == NULL) {
	Cudd_RecursiveDeref(dd,superset2);
	return(0);
    }
    cuddRef(hlocal);

    /* Refine the first factor by minimization. If h turns out to be f, this
    ** step guarantees that g will be 1. */
    glocal = Cudd_bddLICompaction(dd,superset2,hlocal);
    if (glocal == NULL) {
	Cudd_RecursiveDeref(dd,superset2);
	Cudd_RecursiveDeref(dd,hlocal);
	return(0);
    }
    cuddRef(glocal);
    Cudd_RecursiveDeref(dd,superset2);

    if (glocal != DD_ONE(dd)) {
	if (hlocal != DD_ONE(dd)) {
	    *conjuncts = ALLOC(DdNode *,2);
	    if (*conjuncts == NULL) {
		Cudd_RecursiveDeref(dd,glocal);
		Cudd_RecursiveDeref(dd,hlocal);
		dd->errorCode = CUDD_MEMORY_OUT;
		return(0);
	    }
	    (*conjuncts)[0] = glocal;
	    (*conjuncts)[1] = hlocal;
	    return(2);
	} else {
	    Cudd_RecursiveDeref(dd,hlocal);
	    *conjuncts = ALLOC(DdNode *,1);
	    if (*conjuncts == NULL) {
		Cudd_RecursiveDeref(dd,glocal);
		dd->errorCode = CUDD_MEMORY_OUT;
		return(0);
	    }
	    (*conjuncts)[0] = glocal;
	    return(1);
	}
    } else {
	Cudd_RecursiveDeref(dd,glocal);
	*conjuncts = ALLOC(DdNode *,1);
	if (*conjuncts == NULL) {
	    Cudd_RecursiveDeref(dd,hlocal);
	    dd->errorCode = CUDD_MEMORY_OUT;
	    return(0);
	}
	(*conjuncts)[0] = hlocal;
	return(1);
    }

} /* end of Cudd_bddApproxConjDecomp */


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

  Synopsis    [Performs two-way disjunctive decomposition of a BDD.]

  Description [Performs two-way disjunctive decomposition of a BDD.
  Returns the number of disjuncts produced, that is, 2 if successful;
  1 if no meaningful decomposition was found; 0 otherwise. The
  disjuncts produced by this procedure tend to be imbalanced.]

  SideEffects [The two disjuncts are returned in an array as side effects.
  The array is allocated by this function. It is the caller's responsibility
  to free it. On successful completion, the disjuncts are already
  referenced. If the function returns 0, the array for the disjuncts is
  not allocated. If the function returns 1, the only factor equals the
  function to be decomposed.]

  SeeAlso     [Cudd_bddApproxConjDecomp Cudd_bddIterDisjDecomp
  Cudd_bddGenDisjDecomp Cudd_bddVarDisjDecomp]

******************************************************************************/
int
Cudd_bddApproxDisjDecomp(
  DdManager * dd /* manager */,
  DdNode * f /* function to be decomposed */,
  DdNode *** disjuncts /* address of the array of the disjuncts */)
{
    int result, i;

    result = Cudd_bddApproxConjDecomp(dd,Cudd_Not(f),disjuncts);
    for (i = 0; i < result; i++) {
	(*disjuncts)[i] = Cudd_Not((*disjuncts)[i]);
    }
    return(result);

} /* end of Cudd_bddApproxDisjDecomp */


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

  Synopsis    [Performs two-way conjunctive decomposition of a BDD.]

  Description [Performs two-way conjunctive decomposition of a
  BDD. This procedure owes its name to the iterated use of
  supersetting to obtain a factor of the given function. Returns the
  number of conjuncts produced, that is, 2 if successful; 1 if no
  meaningful decomposition was found; 0 otherwise. The conjuncts
  produced by this procedure tend to be imbalanced.]

  SideEffects [The factors are returned in an array as side effects.
  The array is allocated by this function. It is the caller's responsibility
  to free it. On successful completion, the conjuncts are already
  referenced. If the function returns 0, the array for the conjuncts is
  not allocated. If the function returns 1, the only factor equals the
  function to be decomposed.]

  SeeAlso     [Cudd_bddIterDisjDecomp Cudd_bddApproxConjDecomp
  Cudd_bddGenConjDecomp Cudd_bddVarConjDecomp Cudd_RemapOverApprox
  Cudd_bddSqueeze Cudd_bddLICompaction]

******************************************************************************/
int
Cudd_bddIterConjDecomp(
  DdManager * dd /* manager */,
  DdNode * f /* function to be decomposed */,
  DdNode *** conjuncts /* address of the array of conjuncts */)
{
    DdNode *superset1, *superset2, *old[2], *res[2];
    int sizeOld, sizeNew;
    int nvars = Cudd_SupportSize(dd,f);

    old[0] = DD_ONE(dd);
    cuddRef(old[0]);
    old[1] = f;
    cuddRef(old[1]);
    sizeOld = Cudd_SharingSize(old,2);

    do {
	/* Find a tentative first factor by overapproximation and
	** minimization. */
	superset1 = Cudd_RemapOverApprox(dd,old[1],nvars,0,1.0);
	if (superset1 == NULL) {
	    Cudd_RecursiveDeref(dd,old[0]);
	    Cudd_RecursiveDeref(dd,old[1]);
	    return(0);
	}
	cuddRef(superset1);
	superset2 = Cudd_bddSqueeze(dd,old[1],superset1);
	if (superset2 == NULL) {
	    Cudd_RecursiveDeref(dd,old[0]);
	    Cudd_RecursiveDeref(dd,old[1]);
	    Cudd_RecursiveDeref(dd,superset1);
	    return(0);
	}
	cuddRef(superset2);
	Cudd_RecursiveDeref(dd,superset1);
	res[0] = Cudd_bddAnd(dd,old[0],superset2);
	if (res[0] == NULL) {
	    Cudd_RecursiveDeref(dd,superset2);
	    Cudd_RecursiveDeref(dd,old[0]);
	    Cudd_RecursiveDeref(dd,old[1]);
	    return(0);
	}
	cuddRef(res[0]);
	Cudd_RecursiveDeref(dd,superset2);
	if (res[0] == old[0]) {
	    Cudd_RecursiveDeref(dd,res[0]);
	    break;	/* avoid infinite loop */
	}

	/* Compute the second factor by minimization. */
	res[1] = Cudd_bddLICompaction(dd,old[1],res[0]);
	if (res[1] == NULL) {
	    Cudd_RecursiveDeref(dd,old[0]);
	    Cudd_RecursiveDeref(dd,old[1]);
	    return(0);
	}
	cuddRef(res[1]);

	sizeNew = Cudd_SharingSize(res,2);
	if (sizeNew <= sizeOld) {
	    Cudd_RecursiveDeref(dd,old[0]);
	    old[0] = res[0];
	    Cudd_RecursiveDeref(dd,old[1]);
	    old[1] = res[1];
	    sizeOld = sizeNew;
	} else {
	    Cudd_RecursiveDeref(dd,res[0]);
	    Cudd_RecursiveDeref(dd,res[1]);
	    break;
	}

    } while (1);

    /* Refine the first factor by minimization. If h turns out to
    ** be f, this step guarantees that g will be 1. */
    superset1 = Cudd_bddLICompaction(dd,old[0],old[1]);
    if (superset1 == NULL) {
	Cudd_RecursiveDeref(dd,old[0]);
	Cudd_RecursiveDeref(dd,old[1]);
	return(0);
    }
    cuddRef(superset1);
    Cudd_RecursiveDeref(dd,old[0]);
    old[0] = superset1;

    if (old[0] != DD_ONE(dd)) {
	if (old[1] != DD_ONE(dd)) {
	    *conjuncts = ALLOC(DdNode *,2);
	    if (*conjuncts == NULL) {
		Cudd_RecursiveDeref(dd,old[0]);
		Cudd_RecursiveDeref(dd,old[1]);
		dd->errorCode = CUDD_MEMORY_OUT;
		return(0);
	    }
	    (*conjuncts)[0] = old[0];
	    (*conjuncts)[1] = old[1];
	    return(2);
	} else {
	    Cudd_RecursiveDeref(dd,old[1]);
	    *conjuncts = ALLOC(DdNode *,1);
	    if (*conjuncts == NULL) {
		Cudd_RecursiveDeref(dd,old[0]);
		dd->errorCode = CUDD_MEMORY_OUT;
		return(0);
	    }
	    (*conjuncts)[0] = old[0];
	    return(1);
	}
    } else {
	Cudd_RecursiveDeref(dd,old[0]);
	*conjuncts = ALLOC(DdNode *,1);
	if (*conjuncts == NULL) {
	    Cudd_RecursiveDeref(dd,old[1]);
	    dd->errorCode = CUDD_MEMORY_OUT;
	    return(0);
	}
	(*conjuncts)[0] = old[1];
	return(1);
    }

} /* end of Cudd_bddIterConjDecomp */


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

  Synopsis    [Performs two-way disjunctive decomposition of a BDD.]

  Description [Performs two-way disjunctive decomposition of a BDD.
  Returns the number of disjuncts produced, that is, 2 if successful;
  1 if no meaningful decomposition was found; 0 otherwise. The
  disjuncts produced by this procedure tend to be imbalanced.]

  SideEffects [The two disjuncts are returned in an array as side effects.
  The array is allocated by this function. It is the caller's responsibility
  to free it. On successful completion, the disjuncts are already
  referenced. If the function returns 0, the array for the disjuncts is
  not allocated. If the function returns 1, the only factor equals the
  function to be decomposed.]

  SeeAlso     [Cudd_bddIterConjDecomp Cudd_bddApproxDisjDecomp
  Cudd_bddGenDisjDecomp Cudd_bddVarDisjDecomp]

******************************************************************************/
int
Cudd_bddIterDisjDecomp(
  DdManager * dd /* manager */,
  DdNode * f /* function to be decomposed */,
  DdNode *** disjuncts /* address of the array of the disjuncts */)
{
    int result, i;