extra.h

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

/*=== extraBddKmap.c ================================================================*/

/* displays the Karnaugh Map of a function */
extern void        Extra_PrintKMap ARGS((FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nVars, DdNode ** XVars, int fSuppType, char ** pVarNames));
/* displays the Karnaugh Map of a relation */
extern void        Extra_PrintKMapRelation ARGS((FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nXVars, int nYVars, DdNode ** XVars, DdNode ** YVars));

/*=== extraBddMisc.c ===============================================================*/

/* remaps the function to depend on the topmost variables on the manager. */
extern DdNode *    Extra_bddRemapUp ARGS((DdManager * dd, DdNode * bF));
/* finds one cube belonging to the on-set of the function */
extern DdNode *    Extra_bddFindOneCube ARGS((DdManager * dd, DdNode * bF));
/* finds one minterm belonging to the on-set of the function */
extern DdNode *    Extra_bddFindOneMinterm ARGS((DdManager * dd, DdNode * bF, int nVars));
/* finds one cube belonging to the on-set, with the smallest bits-to-integer value */
extern DdNode *    Extra_bddGetOneCube ARGS((DdManager * dd, DdNode * bFunc));
/* finds one minterm belonging to the on-set, with the smallest bits-to-integer value */
extern DdNode *    Extra_bddGetOneMinterm ARGS((DdManager * dd, DdNode * bFunc, DdNode * bSupp));

/* compute the random function with the given density */
extern DdNode *    Extra_bddRandomFunc ARGS((DdManager * dd, int n, double d));
/* prints the bdd in the form of disjoint sum of products */
extern void        Extra_bddPrint ARGS((DdManager * dd, DdNode * F));
/* build the set of all tuples of K variables out of N */
extern DdNode *    Extra_bddTuples ARGS((DdManager * dd, int K, DdNode *bVarsN));
extern DdNode *     extraBddTuples ARGS((DdManager * dd, DdNode *bVarsK, DdNode *bVarsN));
/* changes the polarity of vars listed in the cube */
extern DdNode *    Extra_bddChangePolarity ARGS((DdManager * dd, DdNode * bFunc, DdNode * bVars));
extern DdNode *     extraBddChangePolarity ARGS((DdManager * dd, DdNode * bFunc, DdNode * bVars));

/* converts the bit-string (nbits <= 32) into the BDD cube */
extern DdNode *    Extra_bddBitsToCube ARGS((DdManager * dd, int Code, int CodeWidth, DdNode ** pbVars));
/* computes the positive polarty cube composed of the first vars in the array */
extern DdNode *    Extra_bddComputeCube ARGS((DdManager * dd, DdNode ** bXVars, int nVars));
/* visualize the BDD/ADD/ZDD */
extern void        Extra_bddShow ARGS((DdManager * dd, DdNode * bFunc));
extern void        Extra_addShowFromBdd ARGS((DdManager * dd, DdNode * bFunc));
/* performs the boolean difference w.r.t to a cube (AKA unique quontifier) */
extern DdNode *    Extra_bddBooleanDiffCube ARGS((DdManager * dd, DdNode * bFunc, DdNode * bCube));
extern DdNode *     extraBddBooleanDiffCube ARGS((DdManager * dd, DdNode * bFunc, DdNode * bCube));


/* find the profile of a DD (the number of nodes on each level) */
extern int *       Extra_ProfileNode ARGS((DdManager * dd, DdNode * F, int * Profile));
/* find the profile of a shared set of DDs (the number of nodes on each level) */
extern int *       Extra_ProfileNodeSharing ARGS((DdManager * dd, DdNode ** pFuncs, int nFuncs, int * Profile));

/* find the profile of a DD (the number of edges of each length) */
extern int *       Extra_ProfileEdge ARGS((DdManager * dd, DdNode * F, int * Profile));
/* find the profile of a shared set of DDs (the number of edges of each length) */
extern int *       Extra_ProfileEdgeSharing ARGS((DdManager * dd, DdNode ** pFuncs, int nFuncs, int * Profile));
/* permutes variables the array of functions */
extern void        Extra_bddPermuteArray ARGS((DdManager * dd, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int *permut));
/* permutes variables the BDD and returns an ADD */
extern DdNode *    Extra_bddPermuteToAdd ARGS((DdManager * dd, DdNode * bFunc, int * Permute));

/* finds the smallest integer larger of equal than the logarithm. */
extern int         Extra_Base2Log ARGS((unsigned Num));
extern int         Extra_Base2LogDouble ARGS((double Num));
/* returns the power of two as a double */
extern double      Extra_Power2 ARGS((unsigned Num));

/* checks if the DD has at least one complement edge */
extern int         Extra_WithComplementedEdges ARGS((DdNode * bFunc));

/*=== extraBddPermute.c =================================================================*/

typedef struct _permman  permman; // the permutation manager data structure

/* starting and stopping the permutation manager */
extern permman *   Extra_PermutationManagerInit ARGS(());
extern void        Extra_PermutationManagerQuit ARGS((permman * p));
/* set/reset the key increase limit */
extern void        Extra_PermutationManagerKeyIncreaseLimitSet ARGS((permman * p, int Limit));
extern void        Extra_PermutationManagerKeyIncreaseLimitReset ARGS((permman * p));

/* permuting the BDD in a way that is more efficient than Cudd_bddPermute() */
extern DdNode *    Extra_Permute ARGS((permman * pMan, DdManager * dd, DdNode * Func, int * pPermute));
extern DdNode *    Extra_RemapUp ARGS((permman * pMan, DdManager * dd, DdNode * Func));

/*=== extraBddSupp.c =================================================================*/

/* returns the size of the support */
extern int         Extra_bddSuppSize ARGS((DdManager * dd, DdNode * bSupp));
/* returns 1 if the support contains the given BDD variable */
extern int         Extra_bddSuppContainVar ARGS((DdManager * dd, DdNode * bS, DdNode * bVar));
/* returns 1 if two supports represented as BDD cubes are overlapping */
extern int         Extra_bddSuppOverlapping ARGS((DdManager * dd, DdNode * S1, DdNode * S2));
/* returns the number of different vars in two supports */
extern int         Extra_bddSuppDifferentVars ARGS((DdManager * dd, DdNode * S1, DdNode * S2, int DiffMax));
/* checks the support containment */
extern int         Extra_bddSuppCheckContainment ARGS((DdManager * dd, DdNode * bL, DdNode * bH, DdNode ** bLarge, DdNode ** bSmall));

/* get support of the DD as an array of integers */
extern int *       Extra_SupportArray ARGS((DdManager * dd, DdNode * F, int * support));
/* get support of the array of DDs as an array of integers */
extern int *       Extra_VectorSupportArray ARGS((DdManager * dd, DdNode ** F, int n, int * support));
/* get support size and node count at the same time */
extern int         Extra_DagSizeSuppSize ARGS((DdNode * node, int * pnSuppSize));
/* get support of support and stores it in cache */
extern DdNode *    Extra_SupportCache ARGS((DdManager * dd, DdNode * f));
/* get support of the DD as a ZDD */
extern DdNode *    Extra_zddSupport ARGS((DdManager * dd, DdNode * f));
/* get support as a negative polarity BDD cube */
extern DdNode *    Extra_bddSupportNegativeCube ARGS((DdManager * dd, DdNode * f));


/*===========================================================================*/
/*    Mixed-DD procedures                                                    */
/*===========================================================================*/

/*=== extraDdShift.c =================================================================*/

/* shifts the BDD up/down by one variable */
extern DdNode *    Extra_bddShift ARGS((DdManager * dd, DdNode * bF, int fShiftUp));
extern DdNode *     extraBddShift ARGS((DdManager * dd, DdNode * bF, DdNode * bFlag));
/* stretches the BDD the given number of times  */
extern DdNode *    Extra_bddStretch ARGS((DdManager * dd, DdNode * bF, int nTimes));
extern DdNode *     extraBddStretch ARGS((DdManager * dd, DdNode * bF, DdNode * bTimes));
/* shifts the ZDD up/down by one variable */
extern DdNode *    Extra_zddShift ARGS((DdManager * dd, DdNode * zF, int fShiftUp));
extern DdNode *     extraZddShift ARGS((DdManager * dd, DdNode * zF, DdNode * zFlag));
/* swaps two variables in the BDD */
extern DdNode *    Extra_bddSwapVars ARGS((DdManager * dd, DdNode * bF, int iVar1, int iVar2));
extern DdNode *     extraBddSwapVars ARGS((DdManager * dd, DdNode * bF, DdNode * bVars));

/*=== extraDdTimed.c =================================================================*/

/* sets the timeout and spaceout for Extra_bddAnd(), Extra_bddOr(), and Extra_bddBooleanDiff() */
extern void        Extra_OperationTimeoutSet( int timeout );
extern void        Extra_OperationSpaceoutSet( int MaxNodeIncrease );
extern void        Extra_OperationTimeoutReset();
extern void        Extra_OperationSpaceoutReset();

/* the same as normal operators only with timeout and spaceout */
extern DdNode *    Extra_bddAnd( DdManager * dd, DdNode * f, DdNode * g );
extern DdNode *    Extra_bddOr( DdManager * dd, DdNode * f, DdNode * g );
extern DdNode *     extraBddAndRecur( DdManager * manager, DdNode * f, DdNode * g );
extern DdNode *    Extra_bddBooleanDiff( DdManager * manager, DdNode * f, int x );
extern DdNode *     extraBddBooleanDiffRecur( DdManager * manager, DdNode * f, DdNode * var );
extern DdNode *    Extra_bddVectorCompose( DdManager * dd, DdNode * f, DdNode ** vector );
extern DdNode *    Extra_zddIsopCoverAltTimed( DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc );
extern DdNode *    Extra_zddIsopCoverAltLimited( DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nBTracks );

/*=== extraDdTransfer.c =================================================================*/

/* convert a {A,B}DD from a manager to another with variable remapping */
extern DdNode *    Extra_TransferPermute ARGS((DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute));

/*=== extraDdUtils.c =============================================================*/

extern DdNode *    Extra_zddCoveredByArea ARGS((DdManager *dd, DdNode *zC, DdNode *bA));
extern DdNode *     extraZddCoveredByArea ARGS((DdManager *dd, DdNode *zC, DdNode *bA));
extern DdNode *    Extra_zddNotCoveredByCover ARGS((DdManager *dd, DdNode *zC, DdNode *zD));
extern DdNode *     extraZddNotCoveredByCover ARGS((DdManager *dd, DdNode *zC, DdNode *zD));
extern DdNode *    Extra_zddOverlappingWithArea ARGS((DdManager *dd, DdNode *zC, DdNode *bA));
extern DdNode *     extraZddOverlappingWithArea ARGS((DdManager *dd, DdNode *zC, DdNode *bA));
extern DdNode *    Extra_zddConvertToBdd ARGS((DdManager *dd, DdNode *zC));
extern DdNode *     extraZddConvertToBdd ARGS((DdManager *dd, DdNode *zC));
extern DdNode *    Extra_zddConvertToBddUnate ARGS((DdManager *dd, DdNode *zC));
extern DdNode *     extraZddConvertToBddUnate ARGS((DdManager *dd, DdNode *zC));
extern DdNode *    Extra_zddConvertEsopToBdd ARGS((DdManager *dd, DdNode *zC));
extern DdNode *     extraZddConvertEsopToBdd ARGS((DdManager *dd, DdNode *zC));
extern DdNode *    Extra_zddConvertToBddAndAdd ARGS((DdManager *dd, DdNode *zC, DdNode *bA));
extern DdNode *     extraZddConvertToBddAndAdd ARGS((DdManager *dd, DdNode *zC, DdNode *bA));
extern DdNode *    Extra_zddSingleCoveredArea ARGS((DdManager *dd, DdNode *zC));
extern DdNode *     extraZddSingleCoveredArea ARGS((DdManager *dd, DdNode *zC));
extern DdNode *    Extra_zddConvertBddCubeIntoZddCube ARGS((DdManager *dd, DdNode *bCube));
extern int         Extra_zddVerifyCover ARGS((DdManager * dd, DdNode * zC, DdNode * bFuncOn, DdNode * bFuncOnDc));



/*===========================================================================*/
/*    ZDD-based procedures                                                   */
/*===========================================================================*/

/*=== extraZddCovers.c ==============================================================*/

/* the result of this operation is primes contained in the product of cubes */