src/bdd/reo/reo.h

Go to the documentation of this file.

#ifndef __REO_H__
#define __REO_H__

#ifdef __cplusplus
extern "C" {
#endif

#include <stdio.h>
#include <stdlib.h>
#include "extra.h"

//#pragma warning( disable : 4514 )


// 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;


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 *)((unsigned long)(u) & ~01))
#define Unit_Not(u)         ((reo_unit *)((unsigned long)(u) ^ 01))
#define Unit_NotCond(u,c)   ((reo_unit *)((unsigned long)(u) ^ (c)))
#define Unit_IsConstant(u)  ((int)((u)->lev == REO_CONST_LEVEL))


// ======================= 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 ); 

#ifdef __cplusplus
}
#endif

#endif

---