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

Last change on this file since 100 was 13, checked in by cecile, 13 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.