extrazddcovers.c

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

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

  FileName    [extraZddCovers.c]

  PackageName [extra]

  Synopsis    [Procedures to manipulate covers represented as ZDDs.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - February 1, 2003.]

  Revision    [$Id: extraZddCovers.c,v 1.2 2003/05/27 23:14:41 alanmi Exp $]

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

#include "util.h"
#include "cuddInt.h"
#include "extra.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

#define DD_ZDD_BDD_SUBSET_TAG			0x82

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

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

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

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


/**Automaticstart*************************************************************/

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

/**Automaticend***************************************************************/


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

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

  Synopsis    [Computes the prime product of two covers represented by ZDDs.]

  Description [Computes the prime product of two covers represented by
  ZDDs. The prime product means that the final result contains only 
  prime cubes. The cubes subsumed in larger cubes are deleted on the fly. 
  The result is also a ZDD. Returns a pointer to the result if
  successful; NULL otherwise.  The covers on which Extra_zddProduct
  operates use two ZDD variables for each function variable (one ZDD
  variable for each literal of the variable). These two ZDD variables
  should be adjacent in the order.]

  SideEffects [None]

  SeeAlso     [Extra_zddProduct Extra_zddUnateProduct]

******************************************************************************/
DdNode	*
Extra_zddPrimeProduct(
  DdManager * dd,
  DdNode * f,
  DdNode * g)
{
    DdNode	*res;

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

} /* end of Extra_zddPrimeProduct */


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

  Synopsis    [Computes the product of two covers represented by ZDDs.]

  Description [Alternative implementation of Extra_zddProduct.]

  SideEffects [None]

  SeeAlso     [Extra_zddProduct]

******************************************************************************/
DdNode	*
Extra_zddProductAlt(
  DdManager * dd,
  DdNode * f,
  DdNode * g)
{
    DdNode	*res;

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

} /* end of Extra_zddProduct */

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

  Synopsis    [Returns all cubes compatible with the given cube.]

  Description []

  SideEffects []

  SeeAlso     [Extra_zddMinimal]

******************************************************************************/
DdNode* Extra_zddCompatible( 
  DdManager * dd,     /* the DD manager */
  DdNode * zCover,    /* the cover */
  DdNode * zCube)     /* the cube */
{
    DdNode	*res;
    do {
		dd->reordered = 0;
		res = extraZddCompatible(dd, zCover, zCube);
    } while (dd->reordered == 1);
    return(res);

} /* end of Extra_zddCompatible */



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

  Synopsis    [Computes resolvents of the set of clauses w.r.t. given variables.]

  Description [Computes resolvents of the set of clauses. Clause sets are 
  represented in ZDD using the same technique as covers: one ZDD variable encodes
  positive polarity variable, another ZDD variable encodes negative ZDD variable.
  The set of variables is specified by a combination Vars, containing exactly one 
  ZDD variable (either positive or negative polarity) for each clause variable.
  Resolution is performed only w.r.t. variables in the given set. The resulting 
  clause set is minimal but may include clauses that are contained (or contain) 
  clauses from the original set.]

  SideEffects [None]

  SeeAlso     [Extra_zddPrimeProduct]

******************************************************************************/
DdNode	*
Extra_zddResolve(
  DdManager * dd,
  DdNode * S,
  DdNode * Vars)
{
    DdNode	*Res, *Set0, *Set1, *ResOne, *Temp; 
	int VarIndex;

	/* make sure that the set of vars in not empty */
	if ( S == dd->zero || S == dd->one )
		return dd->zero;
	if ( Vars == dd->one )
		return dd->zero;
	if ( Vars == dd->zero )
		return NULL;

	/* start the result */
	Res = dd->zero;
	Cudd_Ref( Res );

	/* go through variables in Vars, perform resolution and accumulate results */
	for ( ; Vars != dd->one; Vars = cuddT(Vars) )
	{
		/* make sure that Vars is a cube */
		if ( cuddE( Vars ) != dd->zero )
			return NULL;

		/* find the variable number in terms of original (not ZDD) variables */
		VarIndex = (Vars->index >> 1);

		/* compute subsets of combinations with positive/negative clause var */
		/* these subsets may not be minimal!!! */
		Set0 = Cudd_zddSubset1( dd, S, 2*VarIndex + 1 );
		if ( Set0 == NULL )
			return NULL;
		Cudd_Ref( Set0 );
		Set1 = Cudd_zddSubset1( dd, S, 2*VarIndex + 0 );
		if ( Set1 == NULL )
			return NULL;
		Cudd_Ref( Set1 );

		/* resolve the subsets */
		ResOne = Extra_zddPrimeProduct( dd, Set0, Set1 );
//		ResOne = Extra_zddProduct( dd, Set0, Set1 );
		if ( ResOne == NULL )
			return NULL;
		Cudd_Ref( ResOne );
		Cudd_RecursiveDerefZdd( dd, Set0 );
		Cudd_RecursiveDerefZdd( dd, Set1 );

		/* add these resolvents to the accumulator */
		Res = Extra_zddMinUnion( dd, Temp = Res, ResOne );
		if ( Res == NULL )
			return NULL;
		Cudd_Ref( Res );
		Cudd_RecursiveDerefZdd( dd, Temp );
		Cudd_RecursiveDerefZdd( dd, ResOne );
	}

	Cudd_Deref( Res );
	return (Res);

} /* end of Extra_zddResolve */

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

  Synopsis    [Returns irredundant sum-of-products as a ZDD.]

  Description []

  SideEffects [None]

  SeeAlso     [Extra_zddIsop]

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

DdNode *
Extra_zddIsopCover(
  DdManager * dd,  /* the manager */
  DdNode * F1,     /* the BDD for the On-Set */
  DdNode * F12)    /* the BDD for the On-Set and Dc-Set */
{
	DdNode *bIrrCover, *zIrrCover;

	/* call the irredundant cover computation */
	bIrrCover = Cudd_zddIsop( dd, F1, F12, &zIrrCover );
	// both IrrCoverBdd and IrrCoverZdd are not referenced
	if ( bIrrCover == NULL ) 
		return NULL;
	Cudd_Ref( zIrrCover );
	Cudd_Ref( bIrrCover );
	Cudd_IterDerefBdd( dd, bIrrCover );

	Cudd_Deref( zIrrCover );
	return zIrrCover;
}

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

  Synopsis    [Returns irredundant sum-of-products as a ZDD.]

  Description []

  SideEffects [None]

  SeeAlso     [Extra_zddIsop]

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

void
Extra_zddIsopPrintCover(
  DdManager * dd,  /* the manager */
  DdNode * F1,     /* the BDD for the On-Set */
  DdNode * F12)    /* the BDD for the On-Set and Dc-Set */
{
	DdNode * zIrrCover;
	/* call the irredundant cover computation */
	zIrrCover = Extra_zddIsopCover( dd, F1, F12 );  Cudd_Ref( zIrrCover );
	/* call the cover print out */
	Cudd_zddPrintCover( dd, zIrrCover );
	/* dereference */
	Cudd_RecursiveDerefZdd( dd, zIrrCover );
}


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

  Synopsis    [The procedure to count the number of cubes in the ISOP.]

  Description []

  SideEffects []

  SeeAlso     [Extra_zddIsopCoverAlt]

******************************************************************************/
DdNode * Extra_zddSimplify( 
  DdManager * dd,     /* the DD manager */
  DdNode * bFuncOn,    /* the on-set */
  DdNode * bFuncOnDc)  /* the on-set + dc-set */
{
    DdNode * res;
    do {
		dd->reordered = 0;
		res = extraZddSimplify(dd, bFuncOn, bFuncOnDc);
    } while (dd->reordered == 1);
    return(res);

} /* end of Extra_zddSimplify */

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

  Synopsis    [The alternative implementation of irredundant sum-of-products.]

  Description []

  SideEffects []

  SeeAlso     [Extra_zddMinimal]

******************************************************************************/
DdNode* Extra_zddIsopCoverAlt( 
  DdManager * dd,     /* the DD manager */
  DdNode * bFuncOn,    /* the on-set */
  DdNode * bFuncOnDc)  /* the on-set + dc-set */
{
    DdNode * res;
    do {
		dd->reordered = 0;
		res = extraZddIsopCoverAlt(dd, bFuncOn, bFuncOnDc);
    } while (dd->reordered == 1);
    return(res);

} /* end of Extra_zddIsopCoverAlt */

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

  Synopsis    [The procedure to count the number of cubes in the ISOP.]

  Description []

  SideEffects []

  SeeAlso     [Extra_zddIsopCoverAlt]

******************************************************************************/
int Extra_zddIsopCubeNum( 
  DdManager * dd,     /* the DD manager */
  DdNode * bFuncOn,    /* the on-set */
  DdNode * bFuncOnDc)  /* the on-set + dc-set */
{
    DdNode * bRes;
    int nCubes;
    do {
		dd->reordered = 0;
		bRes = extraZddIsopCubeNum(dd, bFuncOn, bFuncOnDc, &nCubes);
    } while (dd->reordered == 1);
    Cudd_Ref( bRes );
//printf( "Original BDD = %d. Final BDD = %d. Cubes = %d.\n", 
//       Cudd_DagSize(bFuncOn), Cudd_DagSize(bRes), nCubes );
    Cudd_RecursiveDeref( dd, bRes );
    return nCubes;

} /* end of Extra_zddIsopCubeNum */


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

  Synopsis    [Selecting important cubes.]

  Description [Given two covers, C and D, and an area of boolean space, Area, 
  this procedure returns the set of all such cubes c in C, for which there 
  DOES NOT EXIST a cube d in D, such that the overlap of c and Area 
  (c intersection Area) is completely contained.]

  SideEffects []

  SeeAlso     [Extra_zddNotSub]

******************************************************************************/
DdNode* Extra_zddNotContainedCubesOverArea( 
  DdManager * dd,   /* the DD manager */
  DdNode * zC,      /* the on-set */
  DdNode * zD,      /* the on-set */
  DdNode * bA)      /* the on-set + dc-set */
{
    DdNode	*res;
    do {
		dd->reordered = 0;
		res = extraZddNotContainedCubesOverArea(dd, zC, zD, bA);
    } while (dd->reordered == 1);
    return(res);

} /* end of Extra_zddNotContainedCubesOverArea */


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

  Synopsis    [Returns a disjoint cover as a ZDD.]

  Description []

  SideEffects [None]

  SeeAlso     [Extra_zddIsop]

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

DdNode *
Extra_zddDisjointCover(
  DdManager * dd,  /* the manager */
  DdNode * F)      /* the BDD whose cubes are enumerated to get the cover */
{
    DdGen * Gen;
    int * Cube;
    CUDD_VALUE_TYPE Value;
    int nVars = dd->size;
	int *VarValues, i;
	DdNode * zDisjCover, * zCube, * zTemp;

    if ( F == Cudd_ReadLogicZero(dd) )
		return dd->zero;
    if ( F == Cudd_ReadOne(dd)  )
		return dd->one;

	/* allocate temporary storage for variable values */
	assert( dd->sizeZ == 2 * dd->size );
	VarValues = (int*) malloc( dd->sizeZ * sizeof(int) );
	if ( VarValues == NULL ) 
	{
		dd->errorCode = CUDD_MEMORY_OUT;
		return NULL;
	}

	/* start the cover */
	zDisjCover = dd->zero;
	Cudd_Ref(zDisjCover);
    Cudd_ForeachCube( dd, F, Gen, Cube, Value )
    {
  		/* clean the storage */
		for ( i = 0; i < dd->sizeZ; i++ )
			VarValues[i] = 0;

  		/* clean the variable values */
		for ( i = 0; i < nVars; i++ )
            if ( Cube[i] == 0 )
//				printf( "[%d]'", i ),
				VarValues[2*i+1] = 1;
            else if ( Cube[i] == 1 )
//				printf( "[%d]", i ),
				VarValues[2*i] = 1;

		/* create the cube */
		zCube = Extra_zddCombination( dd, VarValues, dd->sizeZ );
		Cudd_Ref(zCube);

		zDisjCover = Cudd_zddUnion( dd, zTemp = zDisjCover, zCube );
		Cudd_Ref(zDisjCover);
		Cudd_RecursiveDerefZdd( dd, zTemp );
		Cudd_RecursiveDerefZdd( dd, zCube );
    }
	free(VarValues);
	Cudd_Deref( zDisjCover );
	return zDisjCover;
}

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

  Synopsis    [Selects one cube from a ZDD representing the cube cover.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode* Extra_zddSelectOneCube( 
  DdManager * dd,   /* the DD manager */
  DdNode * zS)      /* the cover */
{
    DdNode	*res;
    do {
		dd->reordered = 0;
		res = extraZddSelectOneCube(dd, zS);
    } while (dd->reordered == 1);
    return(res);

} /* end of Extra_zddSelectOneCube */


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

  Synopsis    [Selects one subset from the set of subsets represented by a ZDD.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode* Extra_zddSelectOneSubset( 
  DdManager * dd,   /* the DD manager */
  DdNode * zS)      /* the ZDD */
{
    DdNode	*res;
    do {
		dd->reordered = 0;
		res = extraZddSelectOneSubset(dd, zS);
    } while (dd->reordered == 1);
    return(res);

} /* end of Extra_zddSelectOneSubset */



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

  Synopsis    [Checks unateness of the cover.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
int Extra_zddCheckUnateness( 
  DdManager * dd, 
  DdNode *zCover)
{
	int i;
	int * s_pVarValues = (int*) malloc( dd->sizeZ * sizeof(int) );
	Extra_SupportArray( dd, zCover, s_pVarValues );
	for ( i = 0; i < dd->sizeZ/2; i++ )
		if ( s_pVarValues[ 2*i ] == 1 && s_pVarValues[ 2*i+1 ] == 1 )
		{
			free( s_pVarValues );
			return 0;
		}
	free( s_pVarValues );
	return 1;
} /* end of Extra_zddCheckUnateness */


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

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

  Synopsis    [Finds three cofactors of the cover w.r.t. to the topmost variable.]

  Description [Finds three cofactors of the cover w.r.t. to the topmost variable.
  Does not check the cover for being a constant. Assumes that ZDD variables encoding