source: vis_dev/glu-2.3/src/cuBdd/cuddInteract.c@ 76

Last change on this file since 76 was 13, checked in by cecile, 15 years ago

library glu 2.3
File size: 12.5 KB
Line 
1/**CFile***********************************************************************
2
3 FileName [cuddInteract.c]
4
5 PackageName [cudd]
6
7 Synopsis [Functions to manipulate the variable interaction matrix.]
8
9 Description [Internal procedures included in this file:
10 <ul>
11 <li> cuddSetInteract()
12 <li> cuddTestInteract()
13 <li> cuddInitInteract()
14 </ul>
15 Static procedures included in this file:
16 <ul>
17 <li> ddSuppInteract()
18 <li> ddClearLocal()
19 <li> ddUpdateInteract()
20 <li> ddClearGlobal()
21 </ul>
22 The interaction matrix tells whether two variables are
23 both in the support of some function of the DD. The main use of the
24 interaction matrix is in the in-place swapping. Indeed, if two
25 variables do not interact, there is no arc connecting the two layers;
26 therefore, the swap can be performed in constant time, without
27 scanning the subtables. Another use of the interaction matrix is in
28 the computation of the lower bounds for sifting. Finally, the
29 interaction matrix can be used to speed up aggregation checks in
30 symmetric and group sifting.<p>
31 The computation of the interaction matrix is done with a series of
32 depth-first searches. The searches start from those nodes that have
33 only external references. The matrix is stored as a packed array of bits;
34 since it is symmetric, only the upper triangle is kept in memory.
35 As a final remark, we note that there may be variables that do
36 intercat, but that for a given variable order have no arc connecting
37 their layers when they are adjacent.]
38
39 SeeAlso []
40
41 Author [Fabio Somenzi]
42
43 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
44
45 All rights reserved.
46
47 Redistribution and use in source and binary forms, with or without
48 modification, are permitted provided that the following conditions
49 are met:
50
51 Redistributions of source code must retain the above copyright
52 notice, this list of conditions and the following disclaimer.
53
54 Redistributions in binary form must reproduce the above copyright
55 notice, this list of conditions and the following disclaimer in the
56 documentation and/or other materials provided with the distribution.
57
58 Neither the name of the University of Colorado nor the names of its
59 contributors may be used to endorse or promote products derived from
60 this software without specific prior written permission.
61
62 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
63 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
64 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
65 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
66 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
67 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
68 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
69 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
70 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
71 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
72 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
73 POSSIBILITY OF SUCH DAMAGE.]
74
75******************************************************************************/
76
77#include "util.h"
78#include "cuddInt.h"
79
80/*---------------------------------------------------------------------------*/
81/* Constant declarations */
82/*---------------------------------------------------------------------------*/
83
84#if SIZEOF_LONG == 8
85#define BPL 64
86#define LOGBPL 6
87#else
88#define BPL 32
89#define LOGBPL 5
90#endif
91
92/*---------------------------------------------------------------------------*/
93/* Stucture declarations */
94/*---------------------------------------------------------------------------*/
95
96
97/*---------------------------------------------------------------------------*/
98/* Type declarations */
99/*---------------------------------------------------------------------------*/
100
101
102/*---------------------------------------------------------------------------*/
103/* Variable declarations */
104/*---------------------------------------------------------------------------*/
105
106#ifndef lint
107static char rcsid[] DD_UNUSED = "$Id: cuddInteract.c,v 1.12 2004/08/13 18:04:49 fabio Exp $";
108#endif
109
110/*---------------------------------------------------------------------------*/
111/* Macro declarations */
112/*---------------------------------------------------------------------------*/
113
114
115/**AutomaticStart*************************************************************/
116
117/*---------------------------------------------------------------------------*/
118/* Static function prototypes */
119/*---------------------------------------------------------------------------*/
120
121static void ddSuppInteract (DdNode *f, int *support);
122static void ddClearLocal (DdNode *f);
123static void ddUpdateInteract (DdManager *table, int *support);
124static void ddClearGlobal (DdManager *table);
125
126/**AutomaticEnd***************************************************************/
127
128
129/*---------------------------------------------------------------------------*/
130/* Definition of exported functions */
131/*---------------------------------------------------------------------------*/
132
133
134/*---------------------------------------------------------------------------*/
135/* Definition of internal functions */
136/*---------------------------------------------------------------------------*/
137
138
139/**Function********************************************************************
140
141 Synopsis [Set interaction matrix entries.]
142
143 Description [Given a pair of variables 0 <= x < y < table->size,
144 sets the corresponding bit of the interaction matrix to 1.]
145
146 SideEffects [None]
147
148 SeeAlso []
149
150******************************************************************************/
151void
152cuddSetInteract(
153 DdManager * table,
154 int x,
155 int y)
156{
157 int posn, word, bit;
158
159#ifdef DD_DEBUG
160 assert(x < y);
161 assert(y < table->size);
162 assert(x >= 0);
163#endif
164
165 posn = ((((table->size << 1) - x - 3) * x) >> 1) + y - 1;
166 word = posn >> LOGBPL;
167 bit = posn & (BPL-1);
168 table->interact[word] |= 1L << bit;
169
170} /* end of cuddSetInteract */
171
172
173/**Function********************************************************************
174
175 Synopsis [Test interaction matrix entries.]
176
177 Description [Given a pair of variables 0 <= x < y < table->size,
178 tests whether the corresponding bit of the interaction matrix is 1.
179 Returns the value of the bit.]
180
181 SideEffects [None]
182
183 SeeAlso []
184
185******************************************************************************/
186int
187cuddTestInteract(
188 DdManager * table,
189 int x,
190 int y)
191{
192 int posn, word, bit, result;
193
194 if (x > y) {
195 int tmp = x;
196 x = y;
197 y = tmp;
198 }
199#ifdef DD_DEBUG
200 assert(x < y);
201 assert(y < table->size);
202 assert(x >= 0);
203#endif
204
205 posn = ((((table->size << 1) - x - 3) * x) >> 1) + y - 1;
206 word = posn >> LOGBPL;
207 bit = posn & (BPL-1);
208 result = (table->interact[word] >> bit) & 1L;
209 return(result);
210
211} /* end of cuddTestInteract */
212
213
214/**Function********************************************************************
215
216 Synopsis [Initializes the interaction matrix.]
217
218 Description [Initializes the interaction matrix. The interaction
219 matrix is implemented as a bit vector storing the upper triangle of
220 the symmetric interaction matrix. The bit vector is kept in an array
221 of long integers. The computation is based on a series of depth-first
222 searches, one for each root of the DAG. Two flags are needed: The
223 local visited flag uses the LSB of the then pointer. The global
224 visited flag uses the LSB of the next pointer.
225 Returns 1 if successful; 0 otherwise.]
226
227 SideEffects [None]
228
229 SeeAlso []
230
231******************************************************************************/
232int
233cuddInitInteract(
234 DdManager * table)
235{
236 int i,j,k;
237 int words;
238 long *interact;
239 int *support;
240 DdNode *f;
241 DdNode *sentinel = &(table->sentinel);
242 DdNodePtr *nodelist;
243 int slots;
244 int n = table->size;
245
246 words = ((n * (n-1)) >> (1 + LOGBPL)) + 1;
247 table->interact = interact = ALLOC(long,words);
248 if (interact == NULL) {
249 table->errorCode = CUDD_MEMORY_OUT;
250 return(0);
251 }
252 for (i = 0; i < words; i++) {
253 interact[i] = 0;
254 }
255
256 support = ALLOC(int,n);
257 if (support == NULL) {
258 table->errorCode = CUDD_MEMORY_OUT;
259 FREE(interact);
260 return(0);
261 }
262
263 for (i = 0; i < n; i++) {
264 nodelist = table->subtables[i].nodelist;
265 slots = table->subtables[i].slots;
266 for (j = 0; j < slots; j++) {
267 f = nodelist[j];
268 while (f != sentinel) {
269 /* A node is a root of the DAG if it cannot be
270 ** reached by nodes above it. If a node was never
271 ** reached during the previous depth-first searches,
272 ** then it is a root, and we start a new depth-first
273 ** search from it.
274 */
275 if (!Cudd_IsComplement(f->next)) {
276 for (k = 0; k < n; k++) {
277 support[k] = 0;
278 }
279 ddSuppInteract(f,support);
280 ddClearLocal(f);
281 ddUpdateInteract(table,support);
282 }
283 f = Cudd_Regular(f->next);
284 }
285 }
286 }
287 ddClearGlobal(table);
288
289 FREE(support);
290 return(1);
291
292} /* end of cuddInitInteract */
293
294
295/*---------------------------------------------------------------------------*/
296/* Definition of static functions */
297/*---------------------------------------------------------------------------*/
298
299
300/**Function********************************************************************
301
302 Synopsis [Find the support of f.]
303
304 Description [Performs a DFS from f. Uses the LSB of the then pointer
305 as visited flag.]
306
307 SideEffects [Accumulates in support the variables on which f depends.]
308
309 SeeAlso []
310
311******************************************************************************/
312static void
313ddSuppInteract(
314 DdNode * f,
315 int * support)
316{
317 if (cuddIsConstant(f) || Cudd_IsComplement(cuddT(f))) {
318 return;
319 }
320
321 support[f->index] = 1;
322 ddSuppInteract(cuddT(f),support);
323 ddSuppInteract(Cudd_Regular(cuddE(f)),support);
324 /* mark as visited */
325 cuddT(f) = Cudd_Complement(cuddT(f));
326 f->next = Cudd_Complement(f->next);
327 return;
328
329} /* end of ddSuppInteract */
330
331
332/**Function********************************************************************
333
334 Synopsis [Performs a DFS from f, clearing the LSB of the then pointers.]
335
336 Description []
337
338 SideEffects [None]
339
340 SeeAlso []
341
342******************************************************************************/
343static void
344ddClearLocal(
345 DdNode * f)
346{
347 if (cuddIsConstant(f) || !Cudd_IsComplement(cuddT(f))) {
348 return;
349 }
350 /* clear visited flag */
351 cuddT(f) = Cudd_Regular(cuddT(f));
352 ddClearLocal(cuddT(f));
353 ddClearLocal(Cudd_Regular(cuddE(f)));
354 return;
355
356} /* end of ddClearLocal */
357
358
359/**Function********************************************************************
360
361 Synopsis [Marks as interacting all pairs of variables that appear in
362 support.]
363
364 Description [If support[i] == support[j] == 1, sets the (i,j) entry
365 of the interaction matrix to 1.]
366
367 SideEffects [None]
368
369 SeeAlso []
370
371******************************************************************************/
372static void
373ddUpdateInteract(
374 DdManager * table,
375 int * support)
376{
377 int i,j;
378 int n = table->size;
379
380 for (i = 0; i < n-1; i++) {
381 if (support[i] == 1) {
382 for (j = i+1; j < n; j++) {
383 if (support[j] == 1) {
384 cuddSetInteract(table,i,j);
385 }
386 }
387 }
388 }
389
390} /* end of ddUpdateInteract */
391
392
393/**Function********************************************************************
394
395 Synopsis [Scans the DD and clears the LSB of the next pointers.]
396
397 Description [The LSB of the next pointers are used as markers to tell
398 whether a node was reached by at least one DFS. Once the interaction
399 matrix is built, these flags are reset.]
400
401 SideEffects [None]
402
403 SeeAlso []
404
405******************************************************************************/
406static void
407ddClearGlobal(
408 DdManager * table)
409{
410 int i,j;
411 DdNode *f;
412 DdNode *sentinel = &(table->sentinel);
413 DdNodePtr *nodelist;
414 int slots;
415
416 for (i = 0; i < table->size; i++) {
417 nodelist = table->subtables[i].nodelist;
418 slots = table->subtables[i].slots;
419 for (j = 0; j < slots; j++) {
420 f = nodelist[j];
421 while (f != sentinel) {
422 f->next = Cudd_Regular(f->next);
423 f = f->next;
424 }
425 }
426 }
427
428} /* end of ddClearGlobal */
429
Note: See TracBrowser for help on using the repository browser.