diff options
Diffstat (limited to 'src/bdd/reo/reo.h')
| -rw-r--r-- | src/bdd/reo/reo.h | 222 |
1 files changed, 222 insertions, 0 deletions
diff --git a/src/bdd/reo/reo.h b/src/bdd/reo/reo.h new file mode 100644 index 00000000..7e4be855 --- /dev/null +++ b/src/bdd/reo/reo.h @@ -0,0 +1,222 @@ +/**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 __REO_H__ +#define __REO_H__ + +#include <stdio.h> +#include <stdlib.h> +#include "extra.h" + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +// 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 + unsigned Arg1; // the first argument + unsigned Arg2; // the second argument + unsigned Arg3; // the second 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 *)((unsigned long)(u) & ~01)) +#define Unit_Not(u) ((reo_unit *)((long)(u) ^ 01)) +#define Unit_NotCond(u,c) ((reo_unit *)((long)(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 ); + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + +#endif |