summaryrefslogtreecommitdiffstats
path: root/src/bdd/reo/reo.h
blob: 981b56dfac5a886999719765dd5afde522b65e47 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
/**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                              ///
////////////////////////////////////////////////////////////////////////