abcBridge-0.10.0.0: abc-build/src/bdd/reo/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.0 2002/15/10 03:00:00 alanmi Exp $]
***********************************************************************/
#ifndef ABC__bdd__reo__reo_h
#define ABC__bdd__reo__reo_h
#include <stdio.h>
#include <stdlib.h>
#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 ///
////////////////////////////////////////////////////////////////////////