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
|
/**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__
#include <stdio.h>
#include <stdlib.h>
#include "extra.h"
////////////////////////////////////////////////////////////////////////
/// 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
unsigned Arg1; // the first argument
unsigned Arg2; // the second argument
unsigned Arg3; // the second 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 *)((long)(u) ^ 01))
#define Unit_NotCond(u,c) ((reo_unit *)((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 );
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
#endif
|
