/**CFile**************************************************************** FileName [reo.h] PackageName [REO: A specialized DD reordering engine.] Synopsis [External and internal declarations.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - October 15, 2002.] Revision [$Id: reo.h,v 1.0 2002/15/10 03:00:00 alanmi Exp $] ***********************************************************************/ #ifndef ABC__bdd__reo__reo_h #define ABC__bdd__reo__reo_h #include #include #include "misc/extra/extraBdd.h" //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_HEADER_START // reordering parameters #define REO_REORDER_LIMIT 1.15 // determines the quality/runtime trade-off #define REO_QUAL_PAR 3 // the quality [1 = simple lower bound, 2 = strict, larger = heuristic] // internal parameters #define REO_CONST_LEVEL 30000 // the number of the constant level #define REO_TOPREF_UNDEF 30000 // the undefined top reference #define REO_CHUNK_SIZE 5000 // the number of units allocated at one time #define REO_COST_EPSILON 0.0000001 // difference in cost large enough so that it counted as an error #define REO_HIGH_VALUE 10000000 // a large value used to initialize some variables // interface parameters #define REO_ENABLE 1 // the value of the enable flag #define REO_DISABLE 0 // the value of the disable flag // the types of minimization currently supported typedef enum { REO_MINIMIZE_NODES, REO_MINIMIZE_WIDTH, // may not work for BDDs with complemented edges REO_MINIMIZE_APL } reo_min_type; //////////////////////////////////////////////////////////////////////// /// DATA STRUCTURES /// //////////////////////////////////////////////////////////////////////// typedef struct _reo_unit reo_unit; // the unit representing one DD node during reordering typedef struct _reo_plane reo_plane; // the set of nodes on one level typedef struct _reo_hash reo_hash; // the entry in the hash table typedef struct _reo_man reo_man; // the reordering manager typedef struct _reo_test reo_test; // struct _reo_unit { short lev; // the level of this node at the beginning short TopRef; // the top level from which this node is refed (used to update BDD width) short TopRefNew; // the new top level from which this node is refed (used to update BDD width) short n; // the number of incoming edges (similar to ref count in the BDD) int Sign; // the signature reo_unit * pE; // the pointer to the "else" branch reo_unit * pT; // the pointer to the "then" branch reo_unit * Next; // the link to the next one in the list double Weight; // the probability of traversing this node }; struct _reo_plane { int fSifted; // to mark the sifted variables int statsNodes; // the number of nodes in the current level int statsWidth; // the width on the current level double statsApl; // the sum of node probabilities on this level double statsCost; // the current cost is stored here double statsCostAbove; // the current cost is stored here double statsCostBelow; // the current cost is stored here reo_unit * pHead; // the pointer to the beginning of the unit list }; struct _reo_hash { int Sign; // signature of the current cache operation reo_unit * Arg1; // the first argument reo_unit * Arg2; // the second argument reo_unit * Arg3; // the third argument }; struct _reo_man { // these paramaters can be set by the API functions int fMinWidth; // the flag to enable reordering for minimum width int fMinApl; // the flag to enable reordering for minimum APL int fVerbose; // the verbosity level int fVerify; // the flag toggling verification int fRemapUp; // the flag to enable remapping int nIters; // the number of interations of sifting to perform // parameters given by the user when reordering is called DdManager * dd; // the CUDD BDD manager int * pOrder; // the resulting variable order will be returned here // derived parameters int fThisIsAdd; // this flag is one if the function is the ADD int * pSupp; // the support of the given function int nSuppAlloc; // the max allowed number of support variables int nSupp; // the number of support variables int * pOrderInt; // the array storing the internal variable permutation double * pVarCosts; // other arrays int * pLevelOrder; // other arrays reo_unit ** pWidthCofs; // temporary storage for cofactors used during reordering for width // parameters related to cost int nNodesBeg; int nNodesCur; int nNodesEnd; int nWidthCur; int nWidthBeg; int nWidthEnd; double nAplCur; double nAplBeg; double nAplEnd; // mapping of the function into planes and back int * pMapToPlanes; // the mapping of var indexes into plane levels int * pMapToDdVarsOrig;// the mapping of plane levels into the original indexes int * pMapToDdVarsFinal;// the mapping of plane levels into the final indexes // the planes table reo_plane * pPlanes; int nPlanes; reo_unit ** pTops; int nTops; int nTopsAlloc; // the hash table reo_hash * HTable; // the table itself int nTableSize; // the size of the hash table int Signature; // the signature counter // the referenced node list int nNodesMaxAlloc; // this parameters determins how much memory is allocated DdNode ** pRefNodes; int nRefNodes; int nRefNodesAlloc; // unit memory management reo_unit * pUnitFreeList; reo_unit ** pMemChunks; int nMemChunks; int nMemChunksAlloc; int nUnitsUsed; // statistic variables int HashSuccess; int HashFailure; int nSwaps; // the number of swaps int nNISwaps; // the number of swaps without interaction }; // used to manipulate units #define Unit_Regular(u) ((reo_unit *)((ABC_PTRUINT_T)(u) & ~01)) #define Unit_Not(u) ((reo_unit *)((ABC_PTRUINT_T)(u) ^ 01)) #define Unit_NotCond(u,c) ((reo_unit *)((ABC_PTRUINT_T)(u) ^ (c))) #define Unit_IsConstant(u) ((int)((u)->lev == REO_CONST_LEVEL)) //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// // ======================= reoApi.c ======================================== extern reo_man * Extra_ReorderInit( int nDdVarsMax, int nNodesMax ); extern void Extra_ReorderQuit( reo_man * p ); extern void Extra_ReorderSetMinimizationType( reo_man * p, reo_min_type fMinType ); extern void Extra_ReorderSetRemapping( reo_man * p, int fRemapUp ); extern void Extra_ReorderSetIterations( reo_man * p, int nIters ); extern void Extra_ReorderSetVerbosity( reo_man * p, int fVerbose ); extern void Extra_ReorderSetVerification( reo_man * p, int fVerify ); extern DdNode * Extra_Reorder( reo_man * p, DdManager * dd, DdNode * Func, int * pOrder ); extern void Extra_ReorderArray( reo_man * p, DdManager * dd, DdNode * Funcs[], DdNode * FuncsRes[], int nFuncs, int * pOrder ); // ======================= reoCore.c ======================================= extern void reoReorderArray( reo_man * p, DdManager * dd, DdNode * Funcs[], DdNode * FuncsRes[], int nFuncs, int * pOrder ); extern void reoResizeStructures( reo_man * p, int nDdVarsMax, int nNodesMax, int nFuncs ); // ======================= reoProfile.c ====================================== extern void reoProfileNodesStart( reo_man * p ); extern void reoProfileAplStart( reo_man * p ); extern void reoProfileWidthStart( reo_man * p ); extern void reoProfileWidthStart2( reo_man * p ); extern void reoProfileAplPrint( reo_man * p ); extern void reoProfileNodesPrint( reo_man * p ); extern void reoProfileWidthPrint( reo_man * p ); extern void reoProfileWidthVerifyLevel( reo_plane * pPlane, int Level ); // ======================= reoSift.c ======================================= extern void reoReorderSift( reo_man * p ); // ======================= reoSwap.c ======================================= extern double reoReorderSwapAdjacentVars( reo_man * p, int Level, int fMovingUp ); // ======================= reoTransfer.c =================================== extern reo_unit * reoTransferNodesToUnits_rec( reo_man * p, DdNode * F ); extern DdNode * reoTransferUnitsToNodes_rec( reo_man * p, reo_unit * pUnit ); // ======================= reoUnits.c ====================================== extern reo_unit * reoUnitsGetNextUnit(reo_man * p ); extern void reoUnitsRecycleUnit( reo_man * p, reo_unit * pUnit ); extern void reoUnitsRecycleUnitList( reo_man * p, reo_plane * pPlane ); extern void reoUnitsAddUnitToPlane( reo_plane * pPlane, reo_unit * pUnit ); extern void reoUnitsStopDispenser( reo_man * p ); // ======================= reoTest.c ======================================= extern void Extra_ReorderTest( DdManager * dd, DdNode * Func ); extern DdNode * Extra_ReorderCudd( DdManager * dd, DdNode * aFunc, int pPermuteReo[] ); extern int Extra_bddReorderTest( DdManager * dd, DdNode * bF ); extern int Extra_addReorderTest( DdManager * dd, DdNode * aF ); ABC_NAMESPACE_HEADER_END #endif //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////