📄 reo.h
字号:
/**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.2 2003/05/26 15:46:31 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 supportedtypedef 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 reorderingtypedef struct _reo_plane reo_plane; // the set of nodes on one leveltypedef struct _reo_hash reo_hash; // the entry in the hash tabletypedef struct _reo_man reo_man; // the reordering managertypedef 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
⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -