Version abc70930

1 files changed, 0 insertions, 232 deletions

diff --git a/src/bdd/reo/reo.h b/src/bdd/reo/reo.h
deleted file mode 100644
index 1a31242a..00000000
--- a/src/bdd/reo/reo.h
+++ /dev/null
@@ -1,232 +0,0 @@
-/**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__
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-#include <stdio.h>
-#include <stdlib.h>
-#include "extra.h"
-
-//#pragma warning( disable : 4514 )
-
-////////////////////////////////////////////////////////////////////////
-///                     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
-    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))
-
-////////////////////////////////////////////////////////////////////////
-///                   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 ); 
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                         END OF FILE                              ///
-////////////////////////////////////////////////////////////////////////