/**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 "bdd/extrab/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                              ///
////////////////////////////////////////////////////////////////////////