source: vis_dev/glu-2.1/src/calBdd/calInteract.c @ 6

Last change on this file since 6 was 6, checked in by cecile, 14 years ago

Ajout de glus pour dev VIS mod
File size: 10.7 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [calInteract.c]
4
5  PackageName [cal]
6
7  Synopsis    [Functions to manipulate the variable interaction matrix.]
8
9  Description [
10  The interaction matrix tells whether two variables are
11  both in the support of some function of the DD. The main use of the
12  interaction matrix is in the in-place swapping. Indeed, if two
13  variables do not interact, there is no arc connecting the two layers;
14  therefore, the swap can be performed in constant time, without
15  scanning the subtables. Another use of the interaction matrix is in
16  the computation of the lower bounds for sifting. Finally, the
17  interaction matrix can be used to speed up aggregation checks in
18  symmetric and group sifting.<p>
19  The computation of the interaction matrix is done with a series of
20  depth-first searches. The searches start from those nodes that have
21  only external references. The matrix is stored as a packed array of bits;
22  since it is symmetric, only the upper triangle is kept in memory.
23  As a final remark, we note that there may be variables that do
24  intercat, but that for a given variable order have no arc connecting
25  their layers when they are adjacent.]
26
27  SeeAlso     []
28
29  Author      [Original author:Fabio Somenzi. Modified for CAL package
30  by Rajeev K. Ranjan]
31
32  Copyright [ This file was created at the University of Colorado at
33  Boulder.  The University of Colorado at Boulder makes no warranty
34  about the suitability of this software for any purpose.  It is
35  presented on an AS IS basis.]
36
37******************************************************************************/
38
39#include "calInt.h"
40
41/*---------------------------------------------------------------------------*/
42/* Constant declarations                                                     */
43/*---------------------------------------------------------------------------*/
44
45#if SIZEOF_LONG == 8
46#define BPL 64
47#define LOGBPL 6
48#else
49#define BPL 32
50#define LOGBPL 5
51#endif
52
53/*---------------------------------------------------------------------------*/
54/* Stucture declarations                                                     */
55/*---------------------------------------------------------------------------*/
56
57
58/*---------------------------------------------------------------------------*/
59/* Type declarations                                                         */
60/*---------------------------------------------------------------------------*/
61
62
63/*---------------------------------------------------------------------------*/
64/* Variable declarations                                                     */
65/*---------------------------------------------------------------------------*/
66
67
68/*---------------------------------------------------------------------------*/
69/* Macro declarations                                                        */
70/*---------------------------------------------------------------------------*/
71
72
73/**AutomaticStart*************************************************************/
74
75/*---------------------------------------------------------------------------*/
76/* Static function prototypes                                                */
77/*---------------------------------------------------------------------------*/
78
79static void ddSuppInteract(Cal_BddManager_t *bddManager, Cal_Bdd_t f, int *support);
80static void ddClearLocal(Cal_Bdd_t f);
81static void ddUpdateInteract(Cal_BddManager_t *bddManager, int *support);
82
83/**AutomaticEnd***************************************************************/
84
85
86/*---------------------------------------------------------------------------*/
87/* Definition of exported functions                                          */
88/*---------------------------------------------------------------------------*/
89
90
91/*---------------------------------------------------------------------------*/
92/* Definition of internal functions                                          */
93/*---------------------------------------------------------------------------*/
94
95
96/**Function********************************************************************
97
98  Synopsis    [Set interaction matrix entries.]
99
100  Description [Given a pair of variables 0 <= x < y < table->size,
101  sets the corresponding bit of the interaction matrix to 1.]
102
103  SideEffects [None]
104
105  SeeAlso     []
106
107******************************************************************************/
108void
109CalSetInteract(Cal_BddManager_t *bddManager, int x, int y)
110{
111    int posn, word, bit;
112
113    Cal_Assert(x < y);
114    Cal_Assert(y < bddManager->numVars);
115    Cal_Assert(x >= 0);
116
117    posn = ((((bddManager->numVars << 1) - x - 3) * x) >> 1) + y - 1;
118    word = posn >> LOGBPL;
119    bit = posn & (BPL-1);
120    bddManager->interact[word] |= 1 << bit;
121
122} /* end of CalSetInteract */
123
124
125/**Function********************************************************************
126
127  Synopsis    [Test interaction matrix entries.]
128
129  Description [Given a pair of variables 0 <= x < y < bddManager->numVars,
130  tests whether the corresponding bit of the interaction matrix is 1.
131  Returns the value of the bit.]
132
133  SideEffects [None]
134
135  SeeAlso     []
136
137******************************************************************************/
138int
139CalTestInteract(Cal_BddManager_t *bddManager, int x, int y)
140{
141    int posn, word, bit, result;
142
143    x -= 1; 
144    y -= 1;
145   
146    if (x > y) {
147        int tmp = x;
148        x = y;
149        y = tmp;
150    }
151    Cal_Assert(x < y);
152    Cal_Assert(y < bddManager->numVars);
153    Cal_Assert(x >= 0);
154
155    posn = ((((bddManager->numVars << 1) - x - 3) * x) >> 1) + y - 1;
156    word = posn >> LOGBPL;
157    bit = posn & (BPL-1);
158    result = (bddManager->interact[word] >> bit) & 1;
159    return(result);
160
161} /* end of CalTestInteract */
162
163
164/**Function********************************************************************
165
166  Synopsis    [Initializes the interaction matrix.]
167
168  Description [Initializes the interaction matrix. The interaction
169  matrix is implemented as a bit vector storing the upper triangle of
170  the symmetric interaction matrix. The bit vector is kept in an array
171  of long integers. The computation is based on a series of depth-first
172  searches, one for each root of the DAG. A local flag (the mark bits)
173  is used.]
174
175  SideEffects [None]
176
177  SeeAlso     []
178
179******************************************************************************/
180int
181CalInitInteract(Cal_BddManager_t *bddManager)
182{
183  int i,k;
184  int words;
185  long *interact;
186  int *support;
187  long numBins;
188  CalBddNode_t **bins, *bddNode, *nextBddNode;
189 
190  int n = bddManager->numVars;
191 
192  words = ((n * (n-1)) >> (1 + LOGBPL)) + 1;
193  bddManager->interact = interact = Cal_MemAlloc(long, words);
194  if (interact == NULL) return(0);
195  for (i = 0; i < words; i++) {
196      interact[i] = 0;
197  }
198 
199  support = Cal_MemAlloc(int, n);
200  if (support == Cal_Nil(int)) {
201    Cal_MemFree(interact);
202    return(0);
203  }
204  bins = bddManager->uniqueTable[0]->bins;
205  numBins = bddManager->uniqueTable[0]->numBins;
206  for (i=0; i<numBins; i++){
207    for (bddNode = bins[i]; bddNode; bddNode = nextBddNode) {
208      Cal_Bdd_t internalBdd;
209      nextBddNode = CalBddNodeGetNextBddNode(bddNode);
210      CalBddNodeGetThenBdd(bddNode, internalBdd);
211      for (k = 0; k < n; k++) {
212        support[k] = 0;
213      }
214      ddSuppInteract(bddManager, internalBdd, support);
215      ddClearLocal(internalBdd);
216      ddUpdateInteract(bddManager, support);
217    }
218  }
219  /* If there are some results pending in the pipeline, we need to
220     take those into account as well */
221
222  if (bddManager->pipelineState == CREATE){
223    CalRequestNode_t **requestNodeListArray =
224        bddManager->requestNodeListArray; 
225    Cal_Bdd_t resultBdd;
226    for (i=0;
227         i<bddManager->pipelineDepth-bddManager->currentPipelineDepth;
228         i++){
229      for (bddNode = *requestNodeListArray; bddNode;
230           bddNode = nextBddNode){ 
231        nextBddNode = CalBddNodeGetNextBddNode(bddNode);
232        Cal_Assert(CalBddNodeIsForwarded(bddNode));
233        CalBddNodeGetThenBdd(bddNode, resultBdd);
234        Cal_Assert(CalBddIsForwarded(resultBdd) == 0);
235        for (k = 0; k < n; k++) {
236          support[k] = 0;
237        }
238        ddSuppInteract(bddManager, resultBdd, support);
239        ddClearLocal(resultBdd);
240        ddUpdateInteract(bddManager, support);
241      }
242      requestNodeListArray++;
243    }
244  }
245 
246 
247  Cal_MemFree(support);
248  return(1);
249 
250} /* end of CalInitInteract */
251
252
253/*---------------------------------------------------------------------------*/
254/* Definition of static functions                                            */
255/*---------------------------------------------------------------------------*/
256
257
258/**Function********************************************************************
259
260  Synopsis    [Find the support of f.]
261
262  Description [Performs a DFS from f. Uses the LSB of the then pointer
263  as visited flag.]
264
265  SideEffects [Accumulates in support the variables on which f depends.]
266
267  SeeAlso     []
268
269******************************************************************************/
270static void
271ddSuppInteract(Cal_BddManager_t *bddManager, Cal_Bdd_t f, int *support)
272{
273  Cal_Bdd_t thenBdd, elseBdd;
274
275  if (CalBddIsBddConst(f) || CalBddIsMarked(f)){
276    return;
277  }
278  support[f.bddId-1] = 1;
279  CalBddGetThenBdd(f, thenBdd);
280  CalBddGetElseBdd(f, elseBdd);
281  ddSuppInteract(bddManager, thenBdd, support);
282  ddSuppInteract(bddManager, elseBdd, support);
283  CalBddMark(f);
284  return;
285} /* end of ddSuppInteract */
286
287
288/**Function********************************************************************
289
290  Synopsis    [Performs a DFS from f, clearing the LSB of the then pointers.]
291
292  Description []
293
294  SideEffects [None]
295
296  SeeAlso     []
297
298******************************************************************************/
299static void
300ddClearLocal(Cal_Bdd_t f)
301{
302  Cal_Bdd_t thenBdd;
303  Cal_Bdd_t elseBdd;
304  CalBddGetElseBdd(f, elseBdd); 
305  if (CalBddIsBddConst(f) || !CalBddIsMarked(f)){
306    return;
307  }
308  /* clear visited flag */
309  CalBddUnmark(f);
310  CalBddGetThenBdd(f, thenBdd);
311  CalBddGetElseBdd(f, elseBdd);
312  ddClearLocal(thenBdd);
313  ddClearLocal(elseBdd);
314  return;
315} /* end of ddClearLocal */
316
317
318/**Function********************************************************************
319
320  Synopsis [Marks as interacting all pairs of variables that appear in
321  support.]
322
323  Description [If support[i] == support[j] == 1, sets the (i,j) entry
324  of the interaction matrix to 1.]
325
326  SideEffects [None]
327
328  SeeAlso     []
329
330******************************************************************************/
331static void
332ddUpdateInteract(Cal_BddManager_t *bddManager, int *support)
333{
334  int i,j;
335  int n = bddManager->numVars;
336 
337  for (i = 0; i < n-1; i++) {
338        if (support[i] == 1) {
339      for (j = i+1; j < n; j++) {
340                if (support[j] == 1) {
341          CalSetInteract(bddManager, i, j);
342                }
343      }
344        }
345  }
346} /* end of ddUpdateInteract */
347
348
Note: See TracBrowser for help on using the repository browser.